E-SAT---3.5.1.THM-CRf.s

%------------------------------------------------------------------------------
% File     : E-SAT---3.5.1
% Problem  : SEU598^1 : TPTP v9.3.1. Released v3.7.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM

% Computer : n026.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:26:51 AM UTC 2026

% Result   : Theorem 1.55s 0.47s
% Output   : CNFRefutation 1.55s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02  % Problem  : SEU598^1 : TPTP v9.3.1. Released v3.7.0.
% 0.00/0.04  % Command  : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.16  % Computer : n026.cluster.edu
% 0.09/0.16  % Model    : x86_64 x86_64
% 0.09/0.16  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.16  % Memory   : 8046.5625MB
% 0.09/0.16  % OS       : Linux 6.8.0-71-generic
% 0.09/0.16  % CPULimit : 300
% 0.09/0.16  % WCLimit  : 300
% 0.09/0.16  % DateTime : Tue Sep 29 13:59:12 UTC 2026
% 0.09/0.16  % CPUTime  : 
% 0.09/0.16  Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.20  Running higher-order theorem proving
% 0.09/0.23  Running: /export/starexec/sandbox2/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/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p
% 1.55/0.47  % Version: 3.5.1-ho
% 1.55/0.47  % Preprocessing class: HSLMSLSSLLLCHFA.
% 1.55/0.47  % Scheduled 8 strats onto 8 cores with 300 seconds (2400 total)
% 1.55/0.47  % Starting ehoh_best5 with 300s (1) cores
% 1.55/0.47  % Starting almost_fo_3_lam with 300s (1) cores
% 1.55/0.47  % Starting new_bool_5 with 300s (1) cores
% 1.55/0.47  % Starting pre_casc_3 with 300s (1) cores
% 1.55/0.47  % Starting ho_unfolding_8 with 300s (1) cores
% 1.55/0.47  % Starting new_ho_10_cnf2 with 300s (1) cores
% 1.55/0.47  % Starting new_bool_3 with 300s (1) cores
% 1.55/0.47  % Starting new_ho_5 with 300s (1) cores
% 1.55/0.47  % new_ho_5 with pid 639125 completed with status 9
% 1.55/0.47  % new_ho_10_cnf2 with pid 639123 completed with status 0
% 1.55/0.47  % Result found by new_ho_10_cnf2
% 1.55/0.47  % Preprocessing class: HSLMSLSSLLLCHFA.
% 1.55/0.47  % Scheduled 8 strats onto 8 cores with 300 seconds (2400 total)
% 1.55/0.47  % Starting ehoh_best5 with 300s (1) cores
% 1.55/0.47  % Starting almost_fo_3_lam with 300s (1) cores
% 1.55/0.47  % Starting new_bool_5 with 300s (1) cores
% 1.55/0.47  % Starting pre_casc_3 with 300s (1) cores
% 1.55/0.47  % Starting ho_unfolding_8 with 300s (1) cores
% 1.55/0.47  % Starting new_ho_10_cnf2 with 300s (1) cores
% 1.55/0.47  % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 1.55/0.47  % No SInE strategy applied
% 1.55/0.47  % Search class: HGHSM-FSLM31-SHFMMSBN
% 1.55/0.47  % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 1.55/0.47  % Starting SubtermCWHack with 28s (1) cores
% 1.55/0.47  % SubtermCWHack with pid 639128 completed with status 0
% 1.55/0.47  % Result found by SubtermCWHack
% 1.55/0.47  % Preprocessing class: HSLMSLSSLLLCHFA.
% 1.55/0.47  % Scheduled 8 strats onto 8 cores with 300 seconds (2400 total)
% 1.55/0.47  % Starting ehoh_best5 with 300s (1) cores
% 1.55/0.47  % Starting almost_fo_3_lam with 300s (1) cores
% 1.55/0.47  % Starting new_bool_5 with 300s (1) cores
% 1.55/0.47  % Starting pre_casc_3 with 300s (1) cores
% 1.55/0.47  % Starting ho_unfolding_8 with 300s (1) cores
% 1.55/0.47  % Starting new_ho_10_cnf2 with 300s (1) cores
% 1.55/0.47  % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 1.55/0.47  % No SInE strategy applied
% 1.55/0.47  % Search class: HGHSM-FSLM31-SHFMMSBN
% 1.55/0.47  % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 1.55/0.47  % Starting SubtermCWHack with 28s (1) cores
% 1.55/0.47  % Preprocessing time       : 0.003 s
% 1.55/0.47  
% 1.55/0.47  % Proof found!
% 1.55/0.47  % SZS status Theorem
% 1.55/0.47  % SZS output start CNFRefutation
% 1.55/0.47  thf(decl_23, type, in: $i > $i > $o).
% 1.55/0.47  thf(decl_24, type, exu: ($i > $o) > $o).
% 1.55/0.47  thf(decl_25, type, setextAx: $o).
% 1.55/0.47  thf(decl_26, type, emptyset: $i).
% 1.55/0.47  thf(decl_27, type, emptysetAx: $o).
% 1.55/0.47  thf(decl_28, type, setadjoin: $i > $i > $i).
% 1.55/0.47  thf(decl_29, type, setadjoinAx: $o).
% 1.55/0.47  thf(decl_30, type, powerset: $i > $i).
% 1.55/0.47  thf(decl_31, type, powersetAx: $o).
% 1.55/0.47  thf(decl_32, type, setunion: $i > $i).
% 1.55/0.47  thf(decl_33, type, setunionAx: $o).
% 1.55/0.47  thf(decl_34, type, omega: $i).
% 1.55/0.47  thf(decl_35, type, omega0Ax: $o).
% 1.55/0.47  thf(decl_36, type, omegaSAx: $o).
% 1.55/0.47  thf(decl_37, type, omegaIndAx: $o).
% 1.55/0.47  thf(decl_38, type, replAx: $o).
% 1.55/0.47  thf(decl_39, type, foundationAx: $o).
% 1.55/0.47  thf(decl_40, type, wellorderingAx: $o).
% 1.55/0.47  thf(decl_41, type, descr: ($i > $o) > $i).
% 1.55/0.47  thf(decl_42, type, descrp: $o).
% 1.55/0.47  thf(decl_43, type, dsetconstr: $i > ($i > $o) > $i).
% 1.55/0.47  thf(decl_44, type, dsetconstrI: $o).
% 1.55/0.47  thf(decl_45, type, dsetconstrEL: $o).
% 1.55/0.47  thf(decl_46, type, dsetconstrER: $o).
% 1.55/0.47  thf(decl_47, type, exuE1: $o).
% 1.55/0.47  thf(decl_48, type, prop2set: $o > $i).
% 1.55/0.47  thf(decl_49, type, prop2setE: $o).
% 1.55/0.47  thf(decl_50, type, emptysetE: $o).
% 1.55/0.47  thf(decl_51, type, emptysetimpfalse: $o).
% 1.55/0.47  thf(decl_52, type, notinemptyset: $o).
% 1.55/0.47  thf(decl_53, type, exuE3e: $o).
% 1.55/0.47  thf(decl_54, type, setext: $o).
% 1.55/0.47  thf(decl_55, type, emptyI: $o).
% 1.55/0.47  thf(decl_56, type, noeltsimpempty: $o).
% 1.55/0.47  thf(decl_57, type, setbeta: $o).
% 1.55/0.47  thf(decl_58, type, nonempty: $i > $o).
% 1.55/0.47  thf(decl_59, type, nonemptyE1: $o).
% 1.55/0.47  thf(decl_60, type, nonemptyI: $o).
% 1.55/0.47  thf(decl_61, type, nonemptyI1: $o).
% 1.55/0.47  thf(decl_62, type, setadjoinIL: $o).
% 1.55/0.47  thf(decl_63, type, emptyinunitempty: $o).
% 1.55/0.47  thf(decl_64, type, setadjoinIR: $o).
% 1.55/0.47  thf(decl_65, type, setadjoinE: $o).
% 1.55/0.47  thf(decl_66, type, setadjoinOr: $o).
% 1.55/0.47  thf(decl_67, type, setoftrueEq: $o).
% 1.55/0.47  thf(decl_68, type, powersetI: $o).
% 1.55/0.47  thf(decl_69, type, emptyinPowerset: $o).
% 1.55/0.47  thf(decl_70, type, emptyInPowerset: $o).
% 1.55/0.47  thf(decl_71, type, powersetE: $o).
% 1.55/0.47  thf(decl_72, type, setunionI: $o).
% 1.55/0.47  thf(decl_73, type, setunionE: $o).
% 1.55/0.47  thf(decl_74, type, subPowSU: $o).
% 1.55/0.47  thf(decl_75, type, exuE2: $o).
% 1.55/0.47  thf(decl_76, type, nonemptyImpWitness: $o).
% 1.55/0.47  thf(decl_77, type, uniqinunit: $o).
% 1.55/0.47  thf(decl_78, type, notinsingleton: $o).
% 1.55/0.47  thf(decl_79, type, eqinunit: $o).
% 1.55/0.47  thf(decl_80, type, singletonsswitch: $o).
% 1.55/0.47  thf(decl_81, type, upairsetE: $o).
% 1.55/0.47  thf(decl_82, type, upairsetIL: $o).
% 1.55/0.47  thf(decl_83, type, upairsetIR: $o).
% 1.55/0.47  thf(decl_84, type, emptyE1: $o).
% 1.55/0.47  thf(decl_85, type, vacuousDall: $o).
% 1.55/0.47  thf(decl_86, type, quantDeMorgan1: $o).
% 1.55/0.47  thf(decl_87, type, quantDeMorgan2: $o).
% 1.55/0.47  thf(decl_88, type, quantDeMorgan3: $o).
% 1.55/0.47  thf(decl_89, type, quantDeMorgan4: $o).
% 1.55/0.47  thf(decl_90, type, prop2setI: $o).
% 1.55/0.47  thf(decl_91, type, set2prop: $i > $o).
% 1.55/0.47  thf(decl_92, type, prop2set2propI: $o).
% 1.55/0.47  thf(decl_93, type, notdexE: $o).
% 1.55/0.47  thf(decl_94, type, notdallE: $o).
% 1.55/0.47  thf(decl_95, type, exuI1: $o).
% 1.55/0.47  thf(decl_96, type, exuI3: $o).
% 1.55/0.47  thf(decl_97, type, exuI2: $o).
% 1.55/0.47  thf(decl_98, type, inCongP: $o).
% 1.55/0.47  thf(decl_99, type, in__Cong: $o).
% 1.55/0.47  thf(decl_100, type, exuE3u: $o).
% 1.55/0.47  thf(decl_101, type, exu__Cong: $o).
% 1.55/0.47  thf(decl_102, type, emptyset__Cong: $o).
% 1.55/0.47  thf(decl_103, type, setadjoin__Cong: $o).
% 1.55/0.47  thf(decl_104, type, powerset__Cong: $o).
% 1.55/0.47  thf(decl_105, type, setunion__Cong: $o).
% 1.55/0.47  thf(decl_106, type, omega__Cong: $o).
% 1.55/0.47  thf(decl_107, type, exuEu: $o).
% 1.55/0.47  thf(decl_108, type, descr__Cong: $o).
% 1.55/0.47  thf(decl_109, type, dsetconstr__Cong: $o).
% 1.55/0.47  thf(decl_110, type, subset: $i > $i > $o).
% 1.55/0.47  thf(decl_113, type, subsetI1: $o).
% 1.55/0.47  thf(decl_114, type, eqimpsubset2: $o).
% 1.55/0.47  thf(decl_115, type, eqimpsubset1: $o).
% 1.55/0.47  thf(decl_116, type, subsetI2: $o).
% 1.55/0.47  thf(decl_117, type, emptysetsubset: $o).
% 1.55/0.47  thf(decl_118, type, subsetE: $o).
% 1.55/0.47  thf(decl_119, type, subsetE2: $o).
% 1.55/0.47  thf(decl_120, type, notsubsetI: $o).
% 1.55/0.47  thf(decl_121, type, notequalI1: $o).
% 1.55/0.47  thf(decl_122, type, notequalI2: $o).
% 1.55/0.47  thf(decl_123, type, subsetRefl: $o).
% 1.55/0.47  thf(decl_124, type, subsetTrans: $o).
% 1.55/0.47  thf(decl_125, type, setadjoinSub: $o).
% 1.55/0.47  thf(decl_126, type, setadjoinSub2: $o).
% 1.55/0.47  thf(decl_127, type, subset2powerset: $o).
% 1.55/0.47  thf(decl_128, type, setextsub: $o).
% 1.55/0.47  thf(decl_129, type, subsetemptysetimpeq: $o).
% 1.55/0.47  thf(decl_130, type, powersetI1: $o).
% 1.55/0.47  thf(decl_131, type, powersetE1: $o).
% 1.55/0.47  thf(decl_132, type, inPowerset: $o).
% 1.55/0.47  thf(decl_133, type, powersetsubset: $o).
% 1.55/0.47  thf(decl_134, type, sepInPowerset: $o).
% 1.55/0.47  thf(decl_135, type, sepSubset: $o).
% 1.55/0.47  thf(decl_136, type, binunion: $i > $i > $i).
% 1.55/0.47  thf(decl_137, type, binunionIL: $o).
% 1.55/0.47  thf(decl_138, type, upairset2IR: $o).
% 1.55/0.47  thf(decl_139, type, binunionIR: $o).
% 1.55/0.47  thf(decl_140, type, binunionEcases: $o).
% 1.55/0.47  thf(decl_141, type, binunionE: $o).
% 1.55/0.47  thf(decl_142, type, binunionLsub: $o).
% 1.55/0.47  thf(decl_143, type, binunionRsub: $o).
% 1.55/0.47  thf(decl_144, type, binintersect: $i > $i > $i).
% 1.55/0.47  thf(decl_145, type, binintersectI: $o).
% 1.55/0.47  thf(decl_146, type, binintersectSubset5: $o).
% 1.55/0.47  thf(decl_147, type, binintersectEL: $o).
% 1.55/0.47  thf(decl_148, type, binintersectLsub: $o).
% 1.55/0.47  thf(decl_149, type, binintersectSubset2: $o).
% 1.55/0.47  thf(decl_150, type, binintersectSubset3: $o).
% 1.55/0.47  thf(decl_151, type, binintersectER: $o).
% 1.55/0.47  thf(decl_152, type, disjointsetsI1: $o).
% 1.55/0.47  thf(decl_153, type, binintersectRsub: $o).
% 1.55/0.47  thf(decl_154, type, epred1_0: $o).
% 1.55/0.47  thf(decl_155, type, esk1_2: $i > $i > $i).
% 1.55/0.47  thf(decl_156, type, esk2_2: $i > $i > $i).
% 1.55/0.47  thf(decl_157, type, esk3_2: $i > $i > $i).
% 1.55/0.47  thf(decl_158, type, esk4_1: $i > $i).
% 1.55/0.47  thf(decl_159, type, esk5_2: ($i > $i > $o) > $i > $i).
% 1.55/0.47  thf(decl_160, type, esk6_3: ($i > $i > $o) > $i > $i > $i).
% 1.55/0.47  thf(decl_161, type, esk7_2: ($i > $i > $o) > $i > $i).
% 1.55/0.47  thf(decl_162, type, esk8_3: ($i > $i > $o) > $i > $i > $i).
% 1.55/0.47  thf(decl_163, type, esk9_1: $i > $i).
% 1.55/0.47  thf(decl_164, type, esk10_2: ($i > $o) > $i > $i).
% 1.55/0.47  thf(decl_165, type, esk11_2: ($i > $o) > $i > $i).
% 1.55/0.47  thf(decl_166, type, esk12_1: ($i > $o) > $i).
% 1.55/0.47  thf(decl_167, type, esk13_2: ($i > $o) > $i > $i).
% 1.55/0.47  thf(decl_168, type, esk14_1: ($i > $o) > $i).
% 1.55/0.47  thf(decl_169, type, esk15_2: $i > $i > $i).
% 1.55/0.47  thf(decl_170, type, esk16_2: $i > $i > $i).
% 1.55/0.47  thf(decl_171, type, esk17_1: $i > $i).
% 1.55/0.47  thf(decl_172, type, esk18_1: $i > $i).
% 1.55/0.47  thf(decl_173, type, esk19_1: $i > $i).
% 1.55/0.47  thf(decl_174, type, esk20_2: $i > $i > $i).
% 1.55/0.47  thf(decl_175, type, esk21_3: $i > $i > $o > $i).
% 1.55/0.47  thf(decl_176, type, esk22_2: ($i > $o) > $i > $i).
% 1.55/0.47  thf(decl_177, type, esk23_1: ($i > $o) > $i).
% 1.55/0.47  thf(decl_178, type, esk24_1: $i > $i).
% 1.55/0.47  thf(decl_179, type, esk25_2: $i > ($i > $o) > $i).
% 1.55/0.47  thf(decl_180, type, esk26_2: $i > ($i > $o) > $i).
% 1.55/0.47  thf(decl_181, type, esk27_2: $i > ($i > $o) > $i).
% 1.55/0.47  thf(decl_182, type, esk28_2: $i > ($i > $o) > $i).
% 1.55/0.47  thf(decl_183, type, esk29_2: $i > ($i > $o) > $i).
% 1.55/0.47  thf(decl_184, type, esk30_2: $i > ($i > $o) > $i).
% 1.55/0.47  thf(decl_185, type, esk31_2: ($i > $o) > $i > $i).
% 1.55/0.47  thf(decl_186, type, esk32_1: ($i > $o) > $i).
% 1.55/0.47  thf(decl_187, type, esk33_1: ($i > $o) > $i).
% 1.55/0.47  thf(decl_188, type, esk34_1: ($i > $o) > $i).
% 1.55/0.47  thf(decl_189, type, esk35_1: ($i > $o) > $i).
% 1.55/0.47  thf(decl_190, type, esk36_2: ($i > $o) > $i > $i).
% 1.55/0.47  thf(decl_191, type, esk37_1: ($i > $o) > $i).
% 1.55/0.47  thf(decl_192, type, esk38_2: ($i > $o) > $i > $i).
% 1.55/0.47  thf(decl_193, type, esk39_2: ($i > $o) > ($i > $o) > $i).
% 1.55/0.47  thf(decl_194, type, esk40_2: ($i > $o) > ($i > $o) > $i).
% 1.55/0.47  thf(decl_195, type, esk41_3: ($i > $o) > ($i > $o) > $i > $i).
% 1.55/0.47  thf(decl_196, type, esk42_2: ($i > $o) > ($i > $o) > $i).
% 1.55/0.47  thf(decl_197, type, esk43_3: ($i > $o) > ($i > $o) > $i > $i).
% 1.55/0.47  thf(decl_198, type, esk44_2: ($i > $o) > ($i > $o) > $i).
% 1.55/0.47  thf(decl_199, type, esk45_2: ($i > $o) > $i > $i).
% 1.55/0.47  thf(decl_200, type, esk46_2: ($i > $o) > ($i > $o) > $i).
% 1.55/0.47  thf(decl_201, type, esk47_2: ($i > $o) > ($i > $o) > $i).
% 1.55/0.47  thf(decl_202, type, esk48_3: ($i > $o) > ($i > $o) > $i > $i).
% 1.55/0.47  thf(decl_203, type, esk49_3: ($i > $o) > ($i > $o) > $i > $i).
% 1.55/0.47  thf(decl_204, type, esk50_4: $i > $i > ($i > $o) > ($i > $o) > $i).
% 1.55/0.47  thf(decl_205, type, esk51_4: $i > $i > ($i > $o) > ($i > $o) > $i).
% 1.55/0.47  thf(decl_206, type, esk52_2: $i > $i > $i).
% 1.55/0.47  thf(decl_207, type, esk53_2: $i > $i > $i).
% 1.55/0.47  thf(decl_208, type, esk54_2: $i > $i > $i).
% 1.55/0.47  thf(decl_209, type, esk55_0: $i).
% 1.55/0.47  thf(decl_210, type, esk56_0: $i).
% 1.55/0.47  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/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', replAx)).
% 1.55/0.47  thf(exu, axiom, ((exu)=(^[X1:$i > $o]:(?[X2:$i]:((((X1 @ X2))&(![X3:$i]:((((X1 @ X3))=>(((X2)=(X3))))))))))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', exu)).
% 1.55/0.47  thf(descrp, axiom, ((descrp)<=>![X1:$i > $o]:(((exu @ (^[X2:$i]:((X1 @ X2))))=>(X1 @ (descr @ (^[X2:$i]:((X1 @ X2)))))))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', descrp)).
% 1.55/0.47  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/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', exuE1)).
% 1.55/0.47  thf(exuE3e, axiom, ((exuE3e)<=>![X1:$i > $o]:(((exu @ (^[X2:$i]:((X1 @ X2))))=>?[X2:$i]:((X1 @ X2))))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', exuE3e)).
% 1.55/0.47  thf(nonempty, axiom, ((nonempty)=(^[X2:$i]:(((X2)!=(emptyset))))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', nonempty)).
% 1.55/0.47  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/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', nonemptyI)).
% 1.55/0.47  thf(exuE2, axiom, ((exuE2)<=>![X1:$i > $o]:(((exu @ (^[X2:$i]:((X1 @ X2))))=>?[X2:$i]:(![X3:$i]:(((X1 @ X3)<=>((X3)=(X2)))))))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', exuE2)).
% 1.55/0.47  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/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', exuI1)).
% 1.55/0.47  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/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', exuI3)).
% 1.55/0.47  thf(exuI2, axiom, ((exuI2)<=>![X1:$i > $o]:((?[X2:$i]:(![X3:$i]:(((X1 @ X3)<=>((X3)=(X2)))))=>(exu @ (^[X2:$i]:((X1 @ X2))))))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', exuI2)).
% 1.55/0.47  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/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', exuE3u)).
% 1.55/0.47  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/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', exu__Cong)).
% 1.55/0.47  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/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', exuEu)).
% 1.55/0.47  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/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', descr__Cong)).
% 1.55/0.47  thf(binintersectSubset4, 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)=>![X4:$i, X5:$i]:(((subset @ X5 @ X4)=>((binintersect @ X4 @ X5)=(X5)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', binintersectSubset4)).
% 1.55/0.47  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/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', dsetconstrI)).
% 1.55/0.47  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/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', dsetconstrEL)).
% 1.55/0.47  thf(dsetconstrER, axiom, ((dsetconstrER)<=>![X4:$i, X1:$i > $o, X2:$i]:(((in @ X2 @ (dsetconstr @ X4 @ (^[X3:$i]:((X1 @ X3)))))=>(X1 @ X2)))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', dsetconstrER)).
% 1.55/0.47  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/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', setbeta)).
% 1.55/0.47  thf(nonemptyE1, axiom, ((nonemptyE1)<=>![X4:$i]:(((nonempty @ X4)=>?[X2:$i]:((in @ X2 @ X4))))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', nonemptyE1)).
% 1.55/0.47  thf(nonemptyI1, axiom, ((nonemptyI1)<=>![X4:$i]:((?[X2:$i]:((in @ X2 @ X4))=>(nonempty @ X4)))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', nonemptyI1)).
% 1.55/0.47  thf(setoftrueEq, axiom, ((setoftrueEq)<=>![X4:$i]:(((dsetconstr @ X4 @ (^[X2:$i]:(($true))))=(X4)))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', setoftrueEq)).
% 1.55/0.47  thf(nonemptyImpWitness, axiom, ((nonemptyImpWitness)<=>![X4:$i]:(((nonempty @ X4)=>?[X2:$i]:(((in @ X2 @ X4)&($true)))))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', nonemptyImpWitness)).
% 1.55/0.47  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/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', emptyE1)).
% 1.55/0.47  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/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', dsetconstr__Cong)).
% 1.55/0.47  thf(sepInPowerset, axiom, ((sepInPowerset)<=>![X4:$i, X1:$i > $o]:((in @ (dsetconstr @ X4 @ (^[X2:$i]:((X1 @ X2)))) @ (powerset @ X4)))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', sepInPowerset)).
% 1.55/0.47  thf(sepSubset, axiom, ((sepSubset)<=>![X4:$i, X1:$i > $o]:((subset @ (dsetconstr @ X4 @ (^[X2:$i]:((X1 @ X2)))) @ X4))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', sepSubset)).
% 1.55/0.47  thf(setextAx, axiom, ((setextAx)<=>![X4:$i, X5:$i]:((![X2:$i]:(((in @ X2 @ X4)<=>(in @ X2 @ X5)))=>((X4)=(X5))))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', setextAx)).
% 1.55/0.47  thf(emptysetAx, axiom, ((emptysetAx)<=>![X2:$i]:(~((in @ X2 @ emptyset)))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', emptysetAx)).
% 1.55/0.47  thf(setadjoinAx, axiom, ((setadjoinAx)<=>![X2:$i, X4:$i, X3:$i]:(((in @ X3 @ (setadjoin @ X2 @ X4))<=>(((X3)=(X2))|(in @ X3 @ X4))))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', setadjoinAx)).
% 1.55/0.47  thf(powersetAx, axiom, ((powersetAx)<=>![X4:$i, X5:$i]:(((in @ X5 @ (powerset @ X4))<=>![X2:$i]:(((in @ X2 @ X5)=>(in @ X2 @ X4)))))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', powersetAx)).
% 1.55/0.47  thf(setunionAx, axiom, ((setunionAx)<=>![X4:$i, X2:$i]:(((in @ X2 @ (setunion @ X4))<=>?[X5:$i]:(((in @ X2 @ X5)&(in @ X5 @ X4)))))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', setunionAx)).
% 1.55/0.47  thf(omega0Ax, axiom, ((omega0Ax)<=>(in @ emptyset @ omega)), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', omega0Ax)).
% 1.55/0.47  thf(omegaSAx, axiom, ((omegaSAx)<=>![X2:$i]:(((in @ X2 @ omega)=>(in @ (setadjoin @ X2 @ X2) @ omega)))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', omegaSAx)).
% 1.55/0.47  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/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', omegaIndAx)).
% 1.55/0.47  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/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', foundationAx)).
% 1.55/0.47  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/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', wellorderingAx)).
% 1.55/0.47  thf(prop2setE, axiom, ((prop2setE)<=>![X10:$o, X2:$i]:(((in @ X2 @ (prop2set @ ((X10))))=>(X10)))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', prop2setE)).
% 1.55/0.47  thf(emptysetE, axiom, ((emptysetE)<=>![X2:$i]:(((in @ X2 @ emptyset)=>![X11:$o]:((X11))))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', emptysetE)).
% 1.55/0.47  thf(emptysetimpfalse, axiom, ((emptysetimpfalse)<=>![X2:$i]:(((in @ X2 @ emptyset)=>~($true)))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', emptysetimpfalse)).
% 1.55/0.47  thf(notinemptyset, axiom, ((notinemptyset)<=>![X2:$i]:(~((in @ X2 @ emptyset)))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', notinemptyset)).
% 1.55/0.47  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/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', setext)).
% 1.55/0.47  thf(emptyI, axiom, ((emptyI)<=>![X4:$i]:((![X2:$i]:(~((in @ X2 @ X4)))=>((X4)=(emptyset))))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', emptyI)).
% 1.55/0.47  thf(noeltsimpempty, axiom, ((noeltsimpempty)<=>![X4:$i]:((![X2:$i]:(~((in @ X2 @ X4)))=>((X4)=(emptyset))))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', noeltsimpempty)).
% 1.55/0.47  thf(setadjoinIL, axiom, ((setadjoinIL)<=>![X2:$i, X3:$i]:((in @ X2 @ (setadjoin @ X2 @ X3)))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', setadjoinIL)).
% 1.55/0.47  thf(emptyinunitempty, axiom, ((emptyinunitempty)<=>(in @ emptyset @ (setadjoin @ emptyset @ emptyset))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', emptyinunitempty)).
% 1.55/0.47  thf(setadjoinIR, axiom, ((setadjoinIR)<=>![X2:$i, X4:$i, X3:$i]:(((in @ X3 @ X4)=>(in @ X3 @ (setadjoin @ X2 @ X4))))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', setadjoinIR)).
% 1.55/0.47  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/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', setadjoinE)).
% 1.55/0.47  thf(setadjoinOr, axiom, ((setadjoinOr)<=>![X2:$i, X4:$i, X3:$i]:(((in @ X3 @ (setadjoin @ X2 @ X4))=>(((X3)=(X2))|(in @ X3 @ X4))))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', setadjoinOr)).
% 1.55/0.47  thf(powersetI, axiom, ((powersetI)<=>![X4:$i, X5:$i]:((![X2:$i]:(((in @ X2 @ X5)=>(in @ X2 @ X4)))=>(in @ X5 @ (powerset @ X4))))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', powersetI)).
% 1.55/0.47  thf(emptyinPowerset, axiom, ((emptyinPowerset)<=>![X4:$i]:((in @ emptyset @ (powerset @ X4)))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', emptyinPowerset)).
% 1.55/0.47  thf(emptyInPowerset, axiom, ((emptyInPowerset)<=>![X4:$i]:((in @ emptyset @ (powerset @ X4)))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', emptyInPowerset)).
% 1.55/0.47  thf(powersetE, axiom, ((powersetE)<=>![X4:$i, X5:$i, X2:$i]:(((in @ X5 @ (powerset @ X4))=>((in @ X2 @ X5)=>(in @ X2 @ X4))))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', powersetE)).
% 1.55/0.47  thf(setunionI, axiom, ((setunionI)<=>![X4:$i, X2:$i, X5:$i]:(((in @ X2 @ X5)=>((in @ X5 @ X4)=>(in @ X2 @ (setunion @ X4)))))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', setunionI)).
% 1.55/0.47  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/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', setunionE)).
% 1.55/0.47  thf(subPowSU, axiom, ((subPowSU)<=>![X4:$i, X2:$i]:(((in @ X2 @ X4)=>(in @ X2 @ (powerset @ (setunion @ X4)))))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', subPowSU)).
% 1.55/0.47  thf(uniqinunit, axiom, ((uniqinunit)<=>![X2:$i, X3:$i]:(((in @ X2 @ (setadjoin @ X3 @ emptyset))=>((X2)=(X3))))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', uniqinunit)).
% 1.55/0.48  thf(notinsingleton, axiom, ((notinsingleton)<=>![X2:$i, X3:$i]:((((X2)!=(X3))=>~((in @ X3 @ (setadjoin @ X2 @ emptyset)))))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', notinsingleton)).
% 1.55/0.48  thf(eqinunit, axiom, ((eqinunit)<=>![X2:$i, X3:$i]:((((X2)=(X3))=>(in @ X2 @ (setadjoin @ X3 @ emptyset))))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', eqinunit)).
% 1.55/0.48  thf(singletonsswitch, axiom, ((singletonsswitch)<=>![X2:$i, X3:$i]:(((in @ X2 @ (setadjoin @ X3 @ emptyset))=>(in @ X3 @ (setadjoin @ X2 @ emptyset))))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', singletonsswitch)).
% 1.55/0.48  thf(upairsetE, axiom, ((upairsetE)<=>![X2:$i, X3:$i, X14:$i]:(((in @ X14 @ (setadjoin @ X2 @ (setadjoin @ X3 @ emptyset)))=>(((X14)=(X2))|((X14)=(X3)))))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', upairsetE)).
% 1.55/0.48  thf(upairsetIL, axiom, ((upairsetIL)<=>![X2:$i, X3:$i]:((in @ X2 @ (setadjoin @ X2 @ (setadjoin @ X3 @ emptyset))))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', upairsetIL)).
% 1.55/0.48  thf(upairsetIR, axiom, ((upairsetIR)<=>![X2:$i, X3:$i]:((in @ X3 @ (setadjoin @ X2 @ (setadjoin @ X3 @ emptyset))))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', upairsetIR)).
% 1.55/0.48  thf(vacuousDall, axiom, ((vacuousDall)<=>![X1:$i > $o, X2:$i]:(((in @ X2 @ emptyset)=>(X1 @ X2)))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', vacuousDall)).
% 1.55/0.48  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/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', quantDeMorgan1)).
% 1.55/0.48  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/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', quantDeMorgan2)).
% 1.55/0.48  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/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', quantDeMorgan3)).
% 1.55/0.48  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/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', quantDeMorgan4)).
% 1.55/0.48  thf(prop2setI, axiom, ((prop2setI)<=>![X15:$o]:(((X15)=>(in @ emptyset @ (prop2set @ ((X15))))))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', prop2setI)).
% 1.55/0.48  thf(prop2set2propI, axiom, ((prop2set2propI)<=>![X16:$o]:(((X16)=>(set2prop @ (prop2set @ ((X16))))))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', prop2set2propI)).
% 1.55/0.48  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/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', notdexE)).
% 1.55/0.48  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/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', notdallE)).
% 1.55/0.48  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/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', inCongP)).
% 1.55/0.48  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/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', in__Cong)).
% 1.55/0.48  thf(emptyset__Cong, axiom, ((emptyset__Cong)<=>((emptyset)=(emptyset))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', emptyset__Cong)).
% 1.55/0.48  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/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', setadjoin__Cong)).
% 1.55/0.48  thf(powerset__Cong, axiom, ((powerset__Cong)<=>![X4:$i, X5:$i]:((((X4)=(X5))=>((powerset @ X4)=(powerset @ X5))))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', powerset__Cong)).
% 1.55/0.48  thf(setunion__Cong, axiom, ((setunion__Cong)<=>![X4:$i, X5:$i]:((((X4)=(X5))=>((setunion @ X4)=(setunion @ X5))))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', setunion__Cong)).
% 1.55/0.48  thf(omega__Cong, axiom, ((omega__Cong)<=>((omega)=(omega))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', omega__Cong)).
% 1.55/0.48  thf(subsetI1, axiom, ((subsetI1)<=>![X4:$i, X5:$i]:((![X2:$i]:(((in @ X2 @ X4)=>(in @ X2 @ X5)))=>(subset @ X4 @ X5)))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', subsetI1)).
% 1.55/0.48  thf(eqimpsubset2, axiom, ((eqimpsubset2)<=>![X4:$i, X5:$i]:((((X4)=(X5))=>(subset @ X5 @ X4)))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', eqimpsubset2)).
% 1.55/0.48  thf(eqimpsubset1, axiom, ((eqimpsubset1)<=>![X4:$i, X5:$i]:((((X4)=(X5))=>(subset @ X4 @ X5)))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', eqimpsubset1)).
% 1.55/0.48  thf(subsetI2, axiom, ((subsetI2)<=>![X4:$i, X5:$i]:((![X2:$i]:(((in @ X2 @ X4)=>(in @ X2 @ X5)))=>(subset @ X4 @ X5)))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', subsetI2)).
% 1.55/0.48  thf(emptysetsubset, axiom, ((emptysetsubset)<=>![X4:$i]:((subset @ emptyset @ X4))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', emptysetsubset)).
% 1.55/0.48  thf(subsetE, axiom, ((subsetE)<=>![X4:$i, X5:$i, X2:$i]:(((subset @ X4 @ X5)=>((in @ X2 @ X4)=>(in @ X2 @ X5))))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', subsetE)).
% 1.55/0.48  thf(subsetE2, axiom, ((subsetE2)<=>![X4:$i, X5:$i, X2:$i]:(((subset @ X4 @ X5)=>(~((in @ X2 @ X5))=>~((in @ X2 @ X4)))))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', subsetE2)).
% 1.55/0.48  thf(notsubsetI, axiom, ((notsubsetI)<=>![X4:$i, X5:$i, X2:$i]:(((in @ X2 @ X4)=>(~((in @ X2 @ X5))=>~((subset @ X4 @ X5)))))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', notsubsetI)).
% 1.55/0.48  thf(notequalI1, axiom, ((notequalI1)<=>![X4:$i, X5:$i]:((~((subset @ X4 @ X5))=>((X4)!=(X5))))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', notequalI1)).
% 1.55/0.48  thf(notequalI2, axiom, ((notequalI2)<=>![X4:$i, X5:$i, X2:$i]:(((in @ X2 @ X4)=>(~((in @ X2 @ X5))=>((X4)!=(X5)))))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', notequalI2)).
% 1.55/0.48  thf(subsetRefl, axiom, ((subsetRefl)<=>![X4:$i]:((subset @ X4 @ X4))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', subsetRefl)).
% 1.55/0.48  thf(subsetTrans, axiom, ((subsetTrans)<=>![X4:$i, X5:$i, X7:$i]:(((subset @ X4 @ X5)=>((subset @ X5 @ X7)=>(subset @ X4 @ X7))))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', subsetTrans)).
% 1.55/0.48  thf(setadjoinSub, axiom, ((setadjoinSub)<=>![X2:$i, X4:$i]:((subset @ X4 @ (setadjoin @ X2 @ X4)))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', setadjoinSub)).
% 1.55/0.48  thf(setadjoinSub2, axiom, ((setadjoinSub2)<=>![X4:$i, X2:$i, X5:$i]:(((subset @ X4 @ X5)=>(subset @ X4 @ (setadjoin @ X2 @ X5))))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', setadjoinSub2)).
% 1.55/0.48  thf(subset2powerset, axiom, ((subset2powerset)<=>![X4:$i, X5:$i]:(((subset @ X4 @ X5)=>(in @ X4 @ (powerset @ X5))))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', subset2powerset)).
% 1.55/0.48  thf(setextsub, axiom, ((setextsub)<=>![X4:$i, X5:$i]:(((subset @ X4 @ X5)=>((subset @ X5 @ X4)=>((X4)=(X5)))))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', setextsub)).
% 1.55/0.48  thf(subsetemptysetimpeq, axiom, ((subsetemptysetimpeq)<=>![X4:$i]:(((subset @ X4 @ emptyset)=>((X4)=(emptyset))))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', subsetemptysetimpeq)).
% 1.55/0.48  thf(powersetI1, axiom, ((powersetI1)<=>![X4:$i, X5:$i]:(((subset @ X5 @ X4)=>(in @ X5 @ (powerset @ X4))))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', powersetI1)).
% 1.55/0.48  thf(powersetE1, axiom, ((powersetE1)<=>![X4:$i, X5:$i]:(((in @ X5 @ (powerset @ X4))=>(subset @ X5 @ X4)))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', powersetE1)).
% 1.55/0.48  thf(inPowerset, axiom, ((inPowerset)<=>![X4:$i]:((in @ X4 @ (powerset @ X4)))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', inPowerset)).
% 1.55/0.48  thf(powersetsubset, axiom, ((powersetsubset)<=>![X4:$i, X5:$i]:(((subset @ X4 @ X5)=>(subset @ (powerset @ X4) @ (powerset @ X5))))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', powersetsubset)).
% 1.55/0.48  thf(binunionIL, axiom, ((binunionIL)<=>![X4:$i, X5:$i, X2:$i]:(((in @ X2 @ X4)=>(in @ X2 @ (binunion @ X4 @ X5))))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', binunionIL)).
% 1.55/0.48  thf(upairset2IR, axiom, ((upairset2IR)<=>![X2:$i, X3:$i]:((in @ X3 @ (setadjoin @ X2 @ (setadjoin @ X3 @ emptyset))))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', upairset2IR)).
% 1.55/0.48  thf(binunionIR, axiom, ((binunionIR)<=>![X4:$i, X5:$i, X2:$i]:(((in @ X2 @ X5)=>(in @ X2 @ (binunion @ X4 @ X5))))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', binunionIR)).
% 1.55/0.48  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/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', binunionEcases)).
% 1.55/0.48  thf(binunionE, axiom, ((binunionE)<=>![X4:$i, X5:$i, X2:$i]:(((in @ X2 @ (binunion @ X4 @ X5))=>((in @ X2 @ X4)|(in @ X2 @ X5))))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', binunionE)).
% 1.55/0.48  thf(binunionLsub, axiom, ((binunionLsub)<=>![X4:$i, X5:$i]:((subset @ X4 @ (binunion @ X4 @ X5)))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', binunionLsub)).
% 1.55/0.48  thf(binunionRsub, axiom, ((binunionRsub)<=>![X4:$i, X5:$i]:((subset @ X5 @ (binunion @ X4 @ X5)))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', binunionRsub)).
% 1.55/0.48  thf(binintersectI, axiom, ((binintersectI)<=>![X4:$i, X5:$i, X2:$i]:(((in @ X2 @ X4)=>((in @ X2 @ X5)=>(in @ X2 @ (binintersect @ X4 @ X5)))))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', binintersectI)).
% 1.55/0.48  thf(binintersectSubset5, axiom, ((binintersectSubset5)<=>![X4:$i, X5:$i, X7:$i]:(((subset @ X7 @ X4)=>((subset @ X7 @ X5)=>(subset @ X7 @ (binintersect @ X4 @ X5)))))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', binintersectSubset5)).
% 1.55/0.48  thf(binintersectEL, axiom, ((binintersectEL)<=>![X4:$i, X5:$i, X2:$i]:(((in @ X2 @ (binintersect @ X4 @ X5))=>(in @ X2 @ X4)))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', binintersectEL)).
% 1.55/0.48  thf(binintersectLsub, axiom, ((binintersectLsub)<=>![X4:$i, X5:$i]:((subset @ (binintersect @ X4 @ X5) @ X4))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', binintersectLsub)).
% 1.55/0.48  thf(binintersectSubset2, axiom, ((binintersectSubset2)<=>![X4:$i, X5:$i]:(((subset @ X4 @ X5)=>((binintersect @ X4 @ X5)=(X4))))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', binintersectSubset2)).
% 1.55/0.48  thf(binintersectSubset3, axiom, ((binintersectSubset3)<=>![X4:$i, X5:$i]:((((binintersect @ X4 @ X5)=(X5))=>(subset @ X5 @ X4)))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', binintersectSubset3)).
% 1.55/0.48  thf(binintersectER, axiom, ((binintersectER)<=>![X4:$i, X5:$i, X2:$i]:(((in @ X2 @ (binintersect @ X4 @ X5))=>(in @ X2 @ X5)))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', binintersectER)).
% 1.55/0.48  thf(disjointsetsI1, axiom, ((disjointsetsI1)<=>![X4:$i, X5:$i]:((~(?[X2:$i]:(((in @ X2 @ X4)&(in @ X2 @ X5))))=>((binintersect @ X4 @ X5)=(emptyset))))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', disjointsetsI1)).
% 1.55/0.48  thf(binintersectRsub, axiom, ((binintersectRsub)<=>![X4:$i, X5:$i]:((subset @ (binintersect @ X4 @ X5) @ X5))), file('/export/starexec/sandbox2/tmp/tmp.zBPaLQpNHc/E---3.1_639105.p', binintersectRsub)).
% 1.55/0.48  thf(c_0_117, 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])).
% 1.55/0.48  thf(c_0_118, plain, ((exu)=(^[Z0:$i > $o]:(?[X2:$i]:((((Z0 @ X2))&(![X3:$i]:((((Z0 @ X3))=>(((X2)=(X3))))))))))), inference(fof_simplification,[status(thm)],[exu])).
% 1.55/0.48  thf(c_0_119, plain, ((descrp)<=>![X1:$i > $o]:(((exu @ (^[Z0:$i]:((X1 @ Z0))))=>(X1 @ (descr @ (^[Z0:$i]:((X1 @ Z0)))))))), inference(fof_simplification,[status(thm)],[descrp])).
% 1.55/0.48  thf(c_0_120, 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])).
% 1.55/0.48  thf(c_0_121, plain, ((exuE3e)<=>![X1:$i > $o]:(((exu @ (^[Z0:$i]:((X1 @ Z0))))=>?[X2:$i]:((X1 @ X2))))), inference(fof_simplification,[status(thm)],[exuE3e])).
% 1.55/0.48  thf(c_0_122, plain, ((nonempty)=(^[Z0:$i]:(((Z0)!=(emptyset))))), inference(fof_simplification,[status(thm)],[nonempty])).
% 1.55/0.48  thf(c_0_123, 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])).
% 1.55/0.48  thf(c_0_124, plain, ((exuE2)<=>![X1:$i > $o]:(((exu @ (^[Z0:$i]:((X1 @ Z0))))=>?[X2:$i]:(![X3:$i]:(((X1 @ X3)<=>((X3)=(X2)))))))), inference(fof_simplification,[status(thm)],[exuE2])).
% 1.55/0.48  thf(c_0_125, 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])).
% 1.55/0.48  thf(c_0_126, 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])).
% 1.55/0.48  thf(c_0_127, plain, ((exuI2)<=>![X1:$i > $o]:((?[X2:$i]:(![X3:$i]:(((X1 @ X3)<=>((X3)=(X2)))))=>(exu @ (^[Z0:$i]:((X1 @ Z0))))))), inference(fof_simplification,[status(thm)],[exuI2])).
% 1.55/0.48  thf(c_0_128, 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])).
% 1.55/0.48  thf(c_0_129, 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])).
% 1.55/0.48  thf(c_0_130, 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])).
% 1.55/0.48  thf(c_0_131, 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])).
% 1.55/0.48  thf(c_0_132, 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)=>![X4:$i, X5:$i]:(((subset @ X5 @ X4)=>((binintersect @ X4 @ X5)=(X5))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), inference(assume_negation,[status(cth)],[binintersectSubset4])).
% 1.55/0.48  thf(c_0_133, plain, ((replAx)=(![X6:$i > $i > $o, X4:$i]:(((![X2:$i]:((((in @ X2 @ X4))=>((?[X326:$i]:(((((X6 @ X2 @ X326)))&(![X327:$i]:(((((X6 @ X2 @ X327)))=>(((X326)=(X327)))))))))))))=>(?[X5:$i]:(![X2:$i]:((((in @ X2 @ X5))<=>(?[X3:$i]:((((in @ X3 @ X4))&((X6 @ X3 @ X2))))))))))))), inference(apply_def,[status(thm)],[c_0_117, c_0_118])).
% 1.55/0.48  thf(c_0_134, plain, ((descrp)=(![X1:$i > $o]:((((?[X328:$i]:(((((X1 @ X328)))&(![X329:$i]:(((((X1 @ X329)))=>(((X328)=(X329))))))))))=>((X1 @ (descr @ (^[Z0:$i]:((X1 @ Z0)))))))))), inference(apply_def,[status(thm)],[c_0_119, c_0_118])).
% 1.55/0.48  thf(c_0_135, 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])).
% 1.55/0.48  thf(c_0_136, 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])).
% 1.55/0.48  thf(c_0_137, 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])).
% 1.55/0.48  thf(c_0_138, plain, ((exuE1)=(![X1:$i > $o]:((((?[X330:$i]:(((((X1 @ X330)))&(![X331:$i]:(((((X1 @ X331)))=>(((X330)=(X331))))))))))=>(?[X2:$i]:((((X1 @ X2))&(![X3:$i]:((((X1 @ X3))=>(((X2)=(X3))))))))))))), inference(apply_def,[status(thm)],[c_0_120, c_0_118])).
% 1.55/0.48  thf(c_0_139, plain, ((exuE3e)=(![X1:$i > $o]:((((?[X332:$i]:(((((X1 @ X332)))&(![X333:$i]:(((((X1 @ X333)))=>(((X332)=(X333))))))))))=>(?[X2:$i]:((X1 @ X2))))))), inference(apply_def,[status(thm)],[c_0_121, c_0_118])).
% 1.55/0.48  thf(c_0_140, 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])).
% 1.55/0.48  thf(c_0_141, axiom, ((nonemptyE1)=(![X4:$i]:((((((X4)!=(emptyset))))=>(?[X2:$i]:((in @ X2 @ X4))))))), inference(apply_def,[status(thm)],[nonemptyE1, c_0_122])).
% 1.55/0.48  thf(c_0_142, plain, ((nonemptyI)=(![X4:$i, X1:$i > $o, X2:$i]:((((in @ X2 @ X4))=>((((X1 @ X2))=>((((dsetconstr @ X4 @ (^[Z0:$i]:((X1 @ Z0))))!=(emptyset)))))))))), inference(apply_def,[status(thm)],[c_0_123, c_0_122])).
% 1.55/0.48  thf(c_0_143, axiom, ((nonemptyI1)=(![X4:$i]:(((?[X2:$i]:((in @ X2 @ X4)))=>((((X4)!=(emptyset)))))))), inference(apply_def,[status(thm)],[nonemptyI1, c_0_122])).
% 1.55/0.48  thf(c_0_144, plain, ((setoftrueEq)<=>![X4:$i]:(((dsetconstr @ X4 @ (^[Z0:$i]:(($true))))=(X4)))), inference(fof_simplification,[status(thm)],[setoftrueEq])).
% 1.55/0.48  thf(c_0_145, plain, ((exuE2)=(![X1:$i > $o]:((((?[X334:$i]:(((((X1 @ X334)))&(![X335:$i]:(((((X1 @ X335)))=>(((X334)=(X335))))))))))=>(?[X2:$i]:(![X3:$i]:((((X1 @ X3))<=>(((X3)=(X2))))))))))), inference(apply_def,[status(thm)],[c_0_124, c_0_118])).
% 1.55/0.48  thf(c_0_146, axiom, ((nonemptyImpWitness)=(![X4:$i]:((((((X4)!=(emptyset))))=>(?[X2:$i]:((((in @ X2 @ X4))&(($true))))))))), inference(apply_def,[status(thm)],[nonemptyImpWitness, c_0_122])).
% 1.55/0.48  thf(c_0_147, 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])).
% 1.55/0.48  thf(c_0_148, plain, ((exuI1)=(![X1:$i > $o]:(((?[X2:$i]:((((X1 @ X2))&(![X3:$i]:((((X1 @ X3))=>(((X2)=(X3)))))))))=>((?[X336:$i]:(((((X1 @ X336)))&(![X337:$i]:(((((X1 @ X337)))=>(((X336)=(X337)))))))))))))), inference(apply_def,[status(thm)],[c_0_125, c_0_118])).
% 1.55/0.48  thf(c_0_149, plain, ((exuI3)=(![X1:$i > $o]:(((?[X2:$i]:((X1 @ X2)))=>(((![X2:$i, X3:$i]:((((X1 @ X2))=>((((X1 @ X3))=>(((X2)=(X3))))))))=>((?[X338:$i]:(((((X1 @ X338)))&(![X339:$i]:(((((X1 @ X339)))=>(((X338)=(X339)))))))))))))))), inference(apply_def,[status(thm)],[c_0_126, c_0_118])).
% 1.55/0.48  thf(c_0_150, plain, ((exuI2)=(![X1:$i > $o]:(((?[X2:$i]:(![X3:$i]:((((X1 @ X3))<=>(((X3)=(X2)))))))=>((?[X340:$i]:(((((X1 @ X340)))&(![X341:$i]:(((((X1 @ X341)))=>(((X340)=(X341)))))))))))))), inference(apply_def,[status(thm)],[c_0_127, c_0_118])).
% 1.55/0.48  thf(c_0_151, plain, ((exuE3u)=(![X1:$i > $o]:((((?[X342:$i]:(((((X1 @ X342)))&(![X343:$i]:(((((X1 @ X343)))=>(((X342)=(X343))))))))))=>(![X2:$i, X3:$i]:((((X1 @ X2))=>((((X1 @ X3))=>(((X2)=(X3)))))))))))), inference(apply_def,[status(thm)],[c_0_128, c_0_118])).
% 1.55/0.48  thf(c_0_152, plain, ((exu__Cong)=(![X1:$i > $o, X17:$i > $o]:(((![X2:$i, X3:$i]:(((((X2)=(X3)))=>((((X1 @ X2))<=>((X17 @ X3)))))))=>((((?[X344:$i]:(((((X1 @ X344)))&(![X345:$i]:(((((X1 @ X345)))=>(((X344)=(X345))))))))))<=>((?[X346:$i]:(((((X17 @ X346)))&(![X347:$i]:(((((X17 @ X347)))=>(((X346)=(X347)))))))))))))))), inference(apply_def,[status(thm)],[c_0_129, c_0_118])).
% 1.55/0.48  thf(c_0_153, plain, ((exuEu)=(![X1:$i > $o]:((((?[X348:$i]:(((((X1 @ X348)))&(![X349:$i]:(((((X1 @ X349)))=>(((X348)=(X349))))))))))=>(![X2:$i, X3:$i]:((((X1 @ X2))=>((((X1 @ X3))=>(((X2)=(X3)))))))))))), inference(apply_def,[status(thm)],[c_0_130, c_0_118])).
% 1.55/0.48  thf(c_0_154, plain, ((descr__Cong)=(![X1:$i > $o, X17:$i > $o]:(((![X2:$i, X3:$i]:(((((X2)=(X3)))=>((((X1 @ X2))<=>((X17 @ X3)))))))=>((((?[X350:$i]:(((((X1 @ X350)))&(![X351:$i]:(((((X1 @ X351)))=>(((X350)=(X351))))))))))=>((((?[X352:$i]:(((((X17 @ X352)))&(![X353:$i]:(((((X17 @ X353)))=>(((X352)=(X353))))))))))=>(((descr @ (^[Z0:$i]:((X1 @ Z0))))=(descr @ (^[Z0:$i]:((X17 @ Z0)))))))))))))), inference(apply_def,[status(thm)],[c_0_131, c_0_118])).
% 1.55/0.48  thf(c_0_155, 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])).
% 1.55/0.48  thf(c_0_156, plain, ((sepInPowerset)<=>![X4:$i, X1:$i > $o]:((in @ (dsetconstr @ X4 @ (^[Z0:$i]:((X1 @ Z0)))) @ (powerset @ X4)))), inference(fof_simplification,[status(thm)],[sepInPowerset])).
% 1.55/0.48  thf(c_0_157, plain, ((sepSubset)<=>![X4:$i, X1:$i > $o]:((subset @ (dsetconstr @ X4 @ (^[Z0:$i]:((X1 @ Z0)))) @ X4))), inference(fof_simplification,[status(thm)],[sepSubset])).
% 1.55/0.48  thf(c_0_158, plain, ((epred1_0)<=>![X383:$i]:(?[X384:$i]:((((![X385:$i]:(((in @ X385 @ X384)=>![X386:$i]:(((in @ X386 @ X385)=>(in @ X386 @ X383)))))&![X387:$i, X388:$i]:((((in @ X387 @ X383)&(in @ X388 @ X383))=>(![X389:$i]:(((in @ X389 @ X384)=>((in @ X387 @ X389)<=>(in @ X388 @ X389))))=>((X387)=(X388))))))&![X390:$i, X391:$i]:((((in @ X390 @ X384)&(in @ X391 @ X384))=>(![X392:$i]:(((in @ X392 @ X390)=>(in @ X392 @ X391)))|![X393:$i]:(((in @ X393 @ X391)=>(in @ X393 @ X390)))))))&![X394:$i]:(((![X395:$i]:(((in @ X395 @ X394)=>(in @ X395 @ X383)))&?[X396:$i]:((in @ X396 @ X394)))=>?[X397:$i, X398:$i]:(((((in @ X397 @ X384)&(in @ X398 @ X394))&~(?[X399:$i]:(((in @ X399 @ X397)&(in @ X399 @ X394)))))&![X400:$i]:(((in @ X400 @ X384)=>(![X401:$i]:(((in @ X401 @ X400)=>(in @ X401 @ X397)))|(in @ X398 @ X400)))))))))))), introduced(definition)).
% 1.55/0.48  thf(c_0_159, negated_conjecture, ~((![X354:$i, X355:$i]:((![X356:$i]:(((in @ X356 @ X354)<=>(in @ X356 @ X355)))=>((X354)=(X355))))=>(![X357:$i]:(~(in @ X357 @ emptyset))=>(![X358:$i, X359:$i, X360:$i]:(((in @ X360 @ (setadjoin @ X358 @ X359))<=>(((X360)=(X358))|(in @ X360 @ X359))))=>(![X361:$i, X362:$i]:(((in @ X362 @ (powerset @ X361))<=>![X363:$i]:(((in @ X363 @ X362)=>(in @ X363 @ X361)))))=>(![X364:$i, X365:$i]:(((in @ X365 @ (setunion @ X364))<=>?[X366:$i]:(((in @ X365 @ X366)&(in @ X366 @ X364)))))=>((in @ emptyset @ omega)=>(![X367:$i]:(((in @ X367 @ omega)=>(in @ (setadjoin @ X367 @ X367) @ omega)))=>(![X368:$i]:((((in @ emptyset @ X368)&![X369:$i]:((((in @ X369 @ omega)&(in @ X369 @ X368))=>(in @ (setadjoin @ X369 @ X369) @ X368))))=>![X370:$i]:(((in @ X370 @ omega)=>(in @ X370 @ X368)))))=>(![X371:$i > $i > $o, X372:$i]:((![X373:$i]:(((in @ X373 @ X372)=>?[X374:$i]:(((X371 @ X373 @ X374)&![X375:$i]:(((X371 @ X373 @ X375)=>((X374)=(X375))))))))=>?[X376:$i]:(![X377:$i]:(((in @ X377 @ X376)<=>?[X378:$i]:(((in @ X378 @ X372)&(X371 @ X378 @ X377))))))))=>(![X379:$i]:((?[X380:$i]:((in @ X380 @ X379))=>?[X381:$i]:(((in @ X381 @ X379)&~(?[X382:$i]:(((in @ X382 @ X381)&(in @ X382 @ X379))))))))=>((epred1_0)=>(![X402:$i > $o]:((?[X403:$i]:(((X402 @ X403)&![X404:$i]:(((X402 @ X404)=>((X403)=(X404))))))=>(X402 @ (descr @ (^[Z0:$i]:(X402 @ Z0))))))=>(![X405:$i, X406:$i > $o, X407:$i]:(((in @ X407 @ X405)=>((X406 @ X407)=>(in @ X407 @ (dsetconstr @ X405 @ X406)))))=>(![X408:$i, X409:$i > $o, X410:$i]:(((in @ X410 @ (dsetconstr @ X408 @ X409))=>(in @ X410 @ X408)))=>(![X411:$i, X412:$i > $o, X413:$i]:(((in @ X413 @ (dsetconstr @ X411 @ X412))=>(X412 @ X413)))=>(![X414:$i > $o]:((?[X415:$i]:(((X414 @ X415)&![X416:$i]:(((X414 @ X416)=>((X415)=(X416))))))=>?[X417:$i]:(((X414 @ X417)&![X418:$i]:(((X414 @ X418)=>((X417)=(X418))))))))=>(![X419:$o, X420:$i]:(((in @ X420 @ (prop2set @ ((X419))))=>(X419)))=>(![X421:$i]:(((in @ X421 @ emptyset)=>![X422:$o]:((X422))))=>(![X423:$i]:(((in @ X423 @ emptyset)=>~($true)))=>(![X424:$i]:(~(in @ X424 @ emptyset))=>(![X425:$i > $o]:((?[X426:$i]:(((X425 @ X426)&![X427:$i]:(((X425 @ X427)=>((X426)=(X427))))))=>?[X428:$i]:((X425 @ X428))))=>(![X429:$i, X430:$i]:((![X431:$i]:(((in @ X431 @ X429)=>(in @ X431 @ X430)))=>(![X432:$i]:(((in @ X432 @ X430)=>(in @ X432 @ X429)))=>((X429)=(X430)))))=>(![X433:$i]:((![X434:$i]:(~(in @ X434 @ X433))=>((X433)=(emptyset))))=>(![X435:$i]:((![X436:$i]:(~(in @ X436 @ X435))=>((X435)=(emptyset))))=>(![X437:$i, X438:$i > $o, X439:$i]:(((in @ X439 @ X437)=>((in @ X439 @ (dsetconstr @ X437 @ X438))<=>(X438 @ X439))))=>(![X440:$i]:((((X440)!=(emptyset))=>?[X441:$i]:((in @ X441 @ X440))))=>(![X442:$i, X443:$i > $o, X444:$i]:(((in @ X444 @ X442)=>((X443 @ X444)=>((dsetconstr @ X442 @ X443)!=(emptyset)))))=>(![X445:$i]:((?[X446:$i]:((in @ X446 @ X445))=>((X445)!=(emptyset))))=>(![X447:$i, X448:$i]:((in @ X447 @ (setadjoin @ X447 @ X448)))=>((in @ emptyset @ (setadjoin @ emptyset @ emptyset))=>(![X449:$i, X450:$i, X451:$i]:(((in @ X451 @ X450)=>(in @ X451 @ (setadjoin @ X449 @ X450))))=>(![X452:$i, X453:$i, X454:$i]:(((in @ X454 @ (setadjoin @ X452 @ X453))=>![X455:$o]:(((((X454)=(X452))=>(X455))=>(((in @ X454 @ X453)=>(X455))=>(X455))))))=>(![X456:$i, X457:$i, X458:$i]:(((in @ X458 @ (setadjoin @ X456 @ X457))=>(((X458)=(X456))|(in @ X458 @ X457))))=>(![X459:$i]:(((dsetconstr @ X459 @ (^[Z0:$i]:($true)))=(X459)))=>(![X460:$i, X461:$i]:((![X462:$i]:(((in @ X462 @ X461)=>(in @ X462 @ X460)))=>(in @ X461 @ (powerset @ X460))))=>(![X463:$i]:((in @ emptyset @ (powerset @ X463)))=>(![X464:$i]:((in @ emptyset @ (powerset @ X464)))=>(![X465:$i, X466:$i, X467:$i]:(((in @ X466 @ (powerset @ X465))=>((in @ X467 @ X466)=>(in @ X467 @ X465))))=>(![X468:$i, X469:$i, X470:$i]:(((in @ X469 @ X470)=>((in @ X470 @ X468)=>(in @ X469 @ (setunion @ X468)))))=>(![X471:$i, X472:$i]:(((in @ X472 @ (setunion @ X471))=>![X473:$o]:((![X474:$i]:(((in @ X472 @ X474)=>((in @ X474 @ X471)=>(X473))))=>(X473)))))=>(![X475:$i, X476:$i]:(((in @ X476 @ X475)=>(in @ X476 @ (powerset @ (setunion @ X475)))))=>(![X477:$i > $o]:((?[X478:$i]:(((X477 @ X478)&![X479:$i]:(((X477 @ X479)=>((X478)=(X479))))))=>?[X480:$i]:(![X481:$i]:(((X477 @ X481)<=>((X481)=(X480)))))))=>(![X482:$i]:((((X482)!=(emptyset))=>?[X483:$i]:(((in @ X483 @ X482)&$true))))=>(![X484:$i, X485:$i]:(((in @ X484 @ (setadjoin @ X485 @ emptyset))=>((X484)=(X485))))=>(![X486:$i, X487:$i]:((((X486)!=(X487))=>~(in @ X487 @ (setadjoin @ X486 @ emptyset))))=>(![X488:$i, X489:$i]:((((X488)=(X489))=>(in @ X488 @ (setadjoin @ X489 @ emptyset))))=>(![X490:$i, X491:$i]:(((in @ X490 @ (setadjoin @ X491 @ emptyset))=>(in @ X491 @ (setadjoin @ X490 @ emptyset))))=>(![X492:$i, X493:$i, X494:$i]:(((in @ X494 @ (setadjoin @ X492 @ (setadjoin @ X493 @ emptyset)))=>(((X494)=(X492))|((X494)=(X493)))))=>(![X495:$i, X496:$i]:((in @ X495 @ (setadjoin @ X495 @ (setadjoin @ X496 @ emptyset))))=>(![X497:$i, X498:$i]:((in @ X498 @ (setadjoin @ X497 @ (setadjoin @ X498 @ emptyset))))=>(![X499:$i, X500:$i > $o]:((?[X501:$i]:(((in @ X501 @ X499)&(X500 @ X501)))=>(((dsetconstr @ X499 @ X500)=(emptyset))=>~($true))))=>(![X502:$i > $o, X503:$i]:(((in @ X503 @ emptyset)=>(X502 @ X503)))=>(![X504:$i, X505:$i > $o]:((~(![X506:$i]:(((in @ X506 @ X504)=>(X505 @ X506))))=>?[X507:$i]:(((in @ X507 @ X504)&~((X505 @ X507))))))=>(![X508:$i, X509:$i > $o]:((![X510:$i]:(((in @ X510 @ X508)=>~((X509 @ X510))))=>~(?[X511:$i]:(((in @ X511 @ X508)&(X509 @ X511))))))=>(![X512:$i, X513:$i > $o]:((~(?[X514:$i]:(((in @ X514 @ X512)&(X513 @ X514))))=>![X515:$i]:(((in @ X515 @ X512)=>~((X513 @ X515))))))=>(![X516:$i, X517:$i > $o]:((?[X518:$i]:(((in @ X518 @ X516)&~((X517 @ X518))))=>~(![X519:$i]:(((in @ X519 @ X516)=>(X517 @ X519))))))=>(![X520:$o]:(((X520)=>(in @ emptyset @ (prop2set @ ((X520))))))=>(![X521:$o]:(((X521)=>(set2prop @ (prop2set @ ((X521))))))=>(![X522:$i, X523:$i > $o]:((~(?[X524:$i]:(((in @ X524 @ X522)&(X523 @ X524))))=>![X525:$i]:(((in @ X525 @ X522)=>~((X523 @ X525))))))=>(![X526:$i, X527:$i > $o]:((~(![X528:$i]:(((in @ X528 @ X526)=>(X527 @ X528))))=>?[X529:$i]:(((in @ X529 @ X526)&~((X527 @ X529))))))=>(![X530:$i > $o]:((?[X531:$i]:(((X530 @ X531)&![X532:$i]:(((X530 @ X532)=>((X531)=(X532))))))=>?[X533:$i]:(((X530 @ X533)&![X534:$i]:(((X530 @ X534)=>((X533)=(X534))))))))=>(![X535:$i > $o]:((?[X536:$i]:((X535 @ X536))=>(![X537:$i, X538:$i]:(((X535 @ X537)=>((X535 @ X538)=>((X537)=(X538)))))=>?[X539:$i]:(((X535 @ X539)&![X540:$i]:(((X535 @ X540)=>((X539)=(X540)))))))))=>(![X541:$i > $o]:((?[X542:$i]:(![X543:$i]:(((X541 @ X543)<=>((X543)=(X542)))))=>?[X544:$i]:(((X541 @ X544)&![X545:$i]:(((X541 @ X545)=>((X544)=(X545))))))))=>(![X546:$i, X547:$i]:((((X546)=(X547))=>![X548:$i, X549:$i]:((((X548)=(X549))=>((in @ X548 @ X546)=>(in @ X549 @ X547))))))=>(![X550:$i, X551:$i]:((((X550)=(X551))=>![X552:$i, X553:$i]:((((X552)=(X553))=>((in @ X552 @ X550)<=>(in @ X553 @ X551))))))=>(![X554:$i > $o]:((?[X555:$i]:(((X554 @ X555)&![X556:$i]:(((X554 @ X556)=>((X555)=(X556))))))=>![X557:$i, X558:$i]:(((X554 @ X557)=>((X554 @ X558)=>((X557)=(X558)))))))=>(![X559:$i > $o, X560:$i > $o]:((![X561:$i, X562:$i]:((((X561)=(X562))=>((X559 @ X561)<=>(X560 @ X562))))=>(?[X563:$i]:(((X559 @ X563)&![X564:$i]:(((X559 @ X564)=>((X563)=(X564))))))<=>?[X565:$i]:(((X560 @ X565)&![X566:$i]:(((X560 @ X566)=>((X565)=(X566)))))))))=>(((emptyset)=(emptyset))=>(![X567:$i, X568:$i]:((((X567)=(X568))=>![X569:$i, X570:$i]:((((X569)=(X570))=>((setadjoin @ X567 @ X569)=(setadjoin @ X568 @ X570))))))=>(![X571:$i, X572:$i]:((((X571)=(X572))=>((powerset @ X571)=(powerset @ X572))))=>(![X573:$i, X574:$i]:((((X573)=(X574))=>((setunion @ X573)=(setunion @ X574))))=>(((omega)=(omega))=>(![X575:$i > $o]:((?[X576:$i]:(((X575 @ X576)&![X577:$i]:(((X575 @ X577)=>((X576)=(X577))))))=>![X578:$i, X579:$i]:(((X575 @ X578)=>((X575 @ X579)=>((X578)=(X579)))))))=>(![X580:$i > $o, X581:$i > $o]:((![X582:$i, X583:$i]:((((X582)=(X583))=>((X580 @ X582)<=>(X581 @ X583))))=>(?[X584:$i]:(((X580 @ X584)&![X585:$i]:(((X580 @ X585)=>((X584)=(X585))))))=>(?[X586:$i]:(((X581 @ X586)&![X587:$i]:(((X581 @ X587)=>((X586)=(X587))))))=>((descr @ X580)=(descr @ X581))))))=>(![X588:$i, X589:$i]:((((X588)=(X589))=>![X590:$i > $o, X591:$i > $o]:((![X592:$i]:(((in @ X592 @ X588)=>![X593:$i]:(((in @ X593 @ X589)=>(((X592)=(X593))=>((X590 @ X592)<=>(X591 @ X593)))))))=>((dsetconstr @ X588 @ X590)=(dsetconstr @ X589 @ X591))))))=>(![X594:$i, X595:$i]:((![X596:$i]:(((in @ X596 @ X594)=>(in @ X596 @ X595)))=>(subset @ X594 @ X595)))=>(![X597:$i, X598:$i]:((((X597)=(X598))=>(subset @ X598 @ X597)))=>(![X599:$i, X600:$i]:((((X599)=(X600))=>(subset @ X599 @ X600)))=>(![X601:$i, X602:$i]:((![X603:$i]:(((in @ X603 @ X601)=>(in @ X603 @ X602)))=>(subset @ X601 @ X602)))=>(![X604:$i]:((subset @ emptyset @ X604))=>(![X605:$i, X606:$i, X607:$i]:(((subset @ X605 @ X606)=>((in @ X607 @ X605)=>(in @ X607 @ X606))))=>(![X608:$i, X609:$i, X610:$i]:(((subset @ X608 @ X609)=>(~(in @ X610 @ X609)=>~(in @ X610 @ X608))))=>(![X611:$i, X612:$i, X613:$i]:(((in @ X613 @ X611)=>(~(in @ X613 @ X612)=>~(subset @ X611 @ X612))))=>(![X614:$i, X615:$i]:((~(subset @ X614 @ X615)=>((X614)!=(X615))))=>(![X616:$i, X617:$i, X618:$i]:(((in @ X618 @ X616)=>(~(in @ X618 @ X617)=>((X616)!=(X617)))))=>(![X619:$i]:((subset @ X619 @ X619))=>(![X620:$i, X621:$i, X622:$i]:(((subset @ X620 @ X621)=>((subset @ X621 @ X622)=>(subset @ X620 @ X622))))=>(![X623:$i, X624:$i]:((subset @ X624 @ (setadjoin @ X623 @ X624)))=>(![X625:$i, X626:$i, X627:$i]:(((subset @ X625 @ X627)=>(subset @ X625 @ (setadjoin @ X626 @ X627))))=>(![X628:$i, X629:$i]:(((subset @ X628 @ X629)=>(in @ X628 @ (powerset @ X629))))=>(![X630:$i, X631:$i]:(((subset @ X630 @ X631)=>((subset @ X631 @ X630)=>((X630)=(X631)))))=>(![X632:$i]:(((subset @ X632 @ emptyset)=>((X632)=(emptyset))))=>(![X633:$i, X634:$i]:(((subset @ X634 @ X633)=>(in @ X634 @ (powerset @ X633))))=>(![X635:$i, X636:$i]:(((in @ X636 @ (powerset @ X635))=>(subset @ X636 @ X635)))=>(![X637:$i]:((in @ X637 @ (powerset @ X637)))=>(![X638:$i, X639:$i]:(((subset @ X638 @ X639)=>(subset @ (powerset @ X638) @ (powerset @ X639))))=>(![X640:$i, X641:$i > $o]:((in @ (dsetconstr @ X640 @ X641) @ (powerset @ X640)))=>(![X642:$i, X643:$i > $o]:((subset @ (dsetconstr @ X642 @ X643) @ X642))=>(![X644:$i, X645:$i, X646:$i]:(((in @ X646 @ X644)=>(in @ X646 @ (binunion @ X644 @ X645))))=>(![X647:$i, X648:$i]:((in @ X648 @ (setadjoin @ X647 @ (setadjoin @ X648 @ emptyset))))=>(![X649:$i, X650:$i, X651:$i]:(((in @ X651 @ X650)=>(in @ X651 @ (binunion @ X649 @ X650))))=>(![X652:$i, X653:$i, X654:$i, X655:$o]:(((in @ X654 @ (binunion @ X652 @ X653))=>(((in @ X654 @ X652)=>(X655))=>(((in @ X654 @ X653)=>(X655))=>(X655)))))=>(![X656:$i, X657:$i, X658:$i]:(((in @ X658 @ (binunion @ X656 @ X657))=>((in @ X658 @ X656)|(in @ X658 @ X657))))=>(![X659:$i, X660:$i]:((subset @ X659 @ (binunion @ X659 @ X660)))=>(![X661:$i, X662:$i]:((subset @ X662 @ (binunion @ X661 @ X662)))=>(![X663:$i, X664:$i, X665:$i]:(((in @ X665 @ X663)=>((in @ X665 @ X664)=>(in @ X665 @ (binintersect @ X663 @ X664)))))=>(![X666:$i, X667:$i, X668:$i]:(((subset @ X668 @ X666)=>((subset @ X668 @ X667)=>(subset @ X668 @ (binintersect @ X666 @ X667)))))=>(![X669:$i, X670:$i, X671:$i]:(((in @ X671 @ (binintersect @ X669 @ X670))=>(in @ X671 @ X669)))=>(![X672:$i, X673:$i]:((subset @ (binintersect @ X672 @ X673) @ X672))=>(![X674:$i, X675:$i]:(((subset @ X674 @ X675)=>((binintersect @ X674 @ X675)=(X674))))=>(![X676:$i, X677:$i]:((((binintersect @ X676 @ X677)=(X677))=>(subset @ X677 @ X676)))=>(![X678:$i, X679:$i, X680:$i]:(((in @ X680 @ (binintersect @ X678 @ X679))=>(in @ X680 @ X679)))=>(![X681:$i, X682:$i]:((~(?[X683:$i]:(((in @ X683 @ X681)&(in @ X683 @ X682))))=>((binintersect @ X681 @ X682)=(emptyset))))=>(![X684:$i, X685:$i]:((subset @ (binintersect @ X684 @ X685) @ X685))=>![X4:$i, X5:$i]:(((subset @ X5 @ X4)=>((binintersect @ X4 @ X5)=(X5))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), 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)],[c_0_132, setextAx]), emptysetAx]), setadjoinAx]), powersetAx]), setunionAx]), omega0Ax]), omegaSAx]), omegaIndAx]), c_0_133]), foundationAx]), wellorderingAx]), c_0_134]), c_0_135]), c_0_136]), c_0_137]), c_0_138]), prop2setE]), emptysetE]), emptysetimpfalse]), notinemptyset]), c_0_139]), setext]), emptyI]), noeltsimpempty]), c_0_140]), c_0_141]), c_0_142]), c_0_143]), setadjoinIL]), emptyinunitempty]), setadjoinIR]), setadjoinE]), setadjoinOr]), c_0_144]), powersetI]), emptyinPowerset]), emptyInPowerset]), powersetE]), setunionI]), setunionE]), subPowSU]), c_0_145]), c_0_146]), uniqinunit]), notinsingleton]), eqinunit]), singletonsswitch]), upairsetE]), upairsetIL]), upairsetIR]), c_0_147]), vacuousDall]), quantDeMorgan1]), quantDeMorgan2]), quantDeMorgan3]), quantDeMorgan4]), prop2setI]), prop2set2propI]), notdexE]), notdallE]), c_0_148]), c_0_149]), c_0_150]), inCongP]), in__Cong]), c_0_151]), c_0_152]), emptyset__Cong]), setadjoin__Cong]), powerset__Cong]), setunion__Cong]), omega__Cong]), c_0_153]), c_0_154]), c_0_155]), subsetI1]), eqimpsubset2]), eqimpsubset1]), subsetI2]), emptysetsubset]), subsetE]), subsetE2]), notsubsetI]), notequalI1]), notequalI2]), subsetRefl]), subsetTrans]), setadjoinSub]), setadjoinSub2]), subset2powerset]), setextsub]), subsetemptysetimpeq]), powersetI1]), powersetE1]), inPowerset]), powersetsubset]), c_0_156]), c_0_157]), binunionIL]), upairset2IR]), binunionIR]), binunionEcases]), binunionE]), binunionLsub]), binunionRsub]), binintersectI]), binintersectSubset5]), binintersectEL]), binintersectLsub]), binintersectSubset2]), binintersectSubset3]), binintersectER]), disjointsetsI1]), binintersectRsub])])]), c_0_158])).
% 1.55/0.48  thf(c_0_160, negated_conjecture, ![X686:$i, X687:$i, X689:$i, X690:$i, X691:$i, X692:$i, X693:$i, X694:$i, X695:$i, X696:$i, X697:$i, X699:$i, X700:$i, X702:$i, X703:$i, X704:$i, X705:$i, X706:$i, X708:$i, X709:$i > $i > $o, X710:$i, X712:$i, X715:$i, X717:$i, X718:$i, X719:$i, X720:$i, X722:$i, X723:$i > $o, X724:$i, X726:$i, X727:$i > $o, X728:$i, X729:$i, X730:$i > $o, X731:$i, X732:$i, X733:$i > $o, X734:$i, X735:$i > $o, X736:$i, X739:$i, X740:$o, X741:$i, X742:$i, X743:$o, X744:$i, X745:$i, X746:$i > $o, X747:$i, X750:$i, X751:$i, X754:$i, X756:$i, X758:$i, X759:$i > $o, X760:$i, X761:$i, X763:$i, X764:$i > $o, X765:$i, X766:$i, X767:$i, X768:$i, X769:$i, X770:$i, X771:$i, X772:$i, X773:$i, X774:$i, X775:$i, X776:$o, X777:$i, X778:$i, X779:$i, X780:$i, X781:$i, X782:$i, X784:$i, X785:$i, X786:$i, X787:$i, X788:$i, X789:$i, X790:$i, X791:$i, X792:$i, X793:$i, X794:$o, X796:$i, X797:$i, X798:$i > $o, X799:$i, X802:$i, X803:$i, X804:$i, X806:$i, X807:$i, X808:$i, X809:$i, X810:$i, X811:$i, X812:$i, X813:$i, X814:$i, X815:$i, X816:$i, X817:$i, X818:$i, X819:$i, X820:$i, X821:$i, X822:$i > $o, X823:$i, X824:$i > $o, X825:$i, X826:$i, X827:$i > $o, X828:$i, X830:$i, X831:$i > $o, X833:$i, X834:$i, X835:$i > $o, X837:$i, X838:$i, X839:$i > $o, X840:$i, X842:$o, X843:$o, X844:$i, X845:$i > $o, X847:$i, X848:$i, X849:$i > $o, X850:$i, X852:$i > $o, X853:$i, X856:$i, X857:$i > $o, X858:$i, X862:$i, X863:$i > $o, X864:$i, X867:$i, X868:$i, X869:$i, X870:$i, X871:$i, X872:$i, X873:$i, X874:$i, X875:$i, X876:$i > $o, X877:$i, X879:$i, X880:$i, X881:$i > $o, X882:$i > $o, X885:$i, X888:$i, X889:$i, X892:$i, X893:$i, X894:$i, X895:$i, X896:$i, X897:$i, X898:$i, X899:$i, X900:$i, X901:$i > $o, X902:$i, X904:$i, X905:$i, X906:$i > $o, X907:$i > $o, X910:$i, X912:$i, X914:$i, X915:$i, X916:$i > $o, X917:$i > $o, X920:$i, X921:$i, X923:$i, X924:$i, X925:$i, X926:$i, X927:$i, X928:$i, X930:$i, X931:$i, X932:$i, X933:$i, X934:$i, X935:$i, X936:$i, X937:$i, X938:$i, X939:$i, X940:$i, X941:$i, X942:$i, X943:$i, X944:$i, X945:$i, X946:$i, X947:$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 > $o, X968:$i, X969:$i > $o, X970:$i, X971:$i, X972:$i, X973:$i, X974:$i, X975:$i, X976:$i, X977:$i, X978:$i, X979:$i, X980:$i, X981:$o, X982:$i, X983:$i, X984:$i, X985:$i, X986:$i, X987:$i, X988:$i, X989:$i, X990:$i, X991:$i, X992:$i, X993:$i, X994:$i, X995:$i, X996:$i, X997:$i, X998:$i, X999:$i, X1000:$i, X1001:$i, X1002:$i, X1003:$i, X1004:$i, X1005:$i, X1006:$i, X1007:$i, X1008:$i, X1010:$i, X1011:$i]:((((~(in @ (esk1_2 @ X686 @ X687) @ X686)|~(in @ (esk1_2 @ X686 @ X687) @ X687)|((X686)=(X687)))&((in @ (esk1_2 @ X686 @ X687) @ X686)|(in @ (esk1_2 @ X686 @ X687) @ X687)|((X686)=(X687))))&(~(in @ X689 @ emptyset)&(((~(in @ X692 @ (setadjoin @ X690 @ X691))|(((X692)=(X690))|(in @ X692 @ X691)))&((((X692)!=(X690))|(in @ X692 @ (setadjoin @ X690 @ X691)))&(~(in @ X692 @ X691)|(in @ X692 @ (setadjoin @ X690 @ X691)))))&(((~(in @ X694 @ (powerset @ X693))|(~(in @ X695 @ X694)|(in @ X695 @ X693)))&(((in @ (esk2_2 @ X696 @ X697) @ X697)|(in @ X697 @ (powerset @ X696)))&(~(in @ (esk2_2 @ X696 @ X697) @ X696)|(in @ X697 @ (powerset @ X696)))))&(((((in @ X700 @ (esk3_2 @ X699 @ X700))|~(in @ X700 @ (setunion @ X699)))&((in @ (esk3_2 @ X699 @ X700) @ X699)|~(in @ X700 @ (setunion @ X699))))&(~(in @ X703 @ X704)|~(in @ X704 @ X702)|(in @ X703 @ (setunion @ X702))))&((in @ emptyset @ omega)&((~(in @ X705 @ omega)|(in @ (setadjoin @ X705 @ X705) @ omega))&(((((in @ (esk4_1 @ X706) @ omega)|~(in @ emptyset @ X706)|(~(in @ X708 @ omega)|(in @ X708 @ X706)))&((in @ (esk4_1 @ X706) @ X706)|~(in @ emptyset @ X706)|(~(in @ X708 @ omega)|(in @ X708 @ X706))))&(~(in @ (setadjoin @ (esk4_1 @ X706) @ (esk4_1 @ X706)) @ X706)|~(in @ emptyset @ X706)|(~(in @ X708 @ omega)|(in @ X708 @ X706))))&((((((in @ (esk8_3 @ X709 @ X710 @ X715) @ X710)|~(in @ X715 @ (esk7_2 @ X709 @ X710))|(in @ (esk5_2 @ X709 @ X710) @ X710))&((X709 @ (esk8_3 @ X709 @ X710 @ X715) @ X715)|~(in @ X715 @ (esk7_2 @ X709 @ X710))|(in @ (esk5_2 @ X709 @ X710) @ X710)))&(~(in @ X718 @ X710)|~(X709 @ X718 @ X717)|(in @ X717 @ (esk7_2 @ X709 @ X710))|(in @ (esk5_2 @ X709 @ X710) @ X710)))&(((((in @ (esk8_3 @ X709 @ X710 @ X715) @ X710)|~(in @ X715 @ (esk7_2 @ X709 @ X710))|((X709 @ (esk5_2 @ X709 @ X710) @ (esk6_3 @ X709 @ X710 @ X712))|~(X709 @ (esk5_2 @ X709 @ X710) @ X712)))&((X709 @ (esk8_3 @ X709 @ X710 @ X715) @ X715)|~(in @ X715 @ (esk7_2 @ X709 @ X710))|((X709 @ (esk5_2 @ X709 @ X710) @ (esk6_3 @ X709 @ X710 @ X712))|~(X709 @ (esk5_2 @ X709 @ X710) @ X712))))&(~(in @ X718 @ X710)|~(X709 @ X718 @ X717)|(in @ X717 @ (esk7_2 @ X709 @ X710))|((X709 @ (esk5_2 @ X709 @ X710) @ (esk6_3 @ X709 @ X710 @ X712))|~(X709 @ (esk5_2 @ X709 @ X710) @ X712))))&((((in @ (esk8_3 @ X709 @ X710 @ X715) @ X710)|~(in @ X715 @ (esk7_2 @ X709 @ X710))|(((X712)!=(esk6_3 @ X709 @ X710 @ X712))|~(X709 @ (esk5_2 @ X709 @ X710) @ X712)))&((X709 @ (esk8_3 @ X709 @ X710 @ X715) @ X715)|~(in @ X715 @ (esk7_2 @ X709 @ X710))|(((X712)!=(esk6_3 @ X709 @ X710 @ X712))|~(X709 @ (esk5_2 @ X709 @ X710) @ X712))))&(~(in @ X718 @ X710)|~(X709 @ X718 @ X717)|(in @ X717 @ (esk7_2 @ X709 @ X710))|(((X712)!=(esk6_3 @ X709 @ X710 @ X712))|~(X709 @ (esk5_2 @ X709 @ X710) @ X712))))))&((((in @ (esk9_1 @ X719) @ X719)|~(in @ X720 @ X719))&(~(in @ X722 @ (esk9_1 @ X719))|~(in @ X722 @ X719)|~(in @ X720 @ X719)))&((epred1_0)&((((X723 @ (esk10_2 @ X723 @ X724))|~(X723 @ X724)|(X723 @ (descr @ X723)))&(((X724)!=(esk10_2 @ X723 @ X724))|~(X723 @ X724)|(X723 @ (descr @ X723))))&((~(in @ X728 @ X726)|(~(X727 @ X728)|(in @ X728 @ (dsetconstr @ X726 @ X727))))&((~(in @ X731 @ (dsetconstr @ X729 @ X730))|(in @ X731 @ X729))&((~(in @ X734 @ (dsetconstr @ X732 @ X733))|(X733 @ X734))&(((((X735 @ (esk12_1 @ X735))|((X735 @ (esk11_2 @ X735 @ X736))|~(X735 @ X736)))&(~(X735 @ X739)|((esk12_1 @ X735)=(X739))|((X735 @ (esk11_2 @ X735 @ X736))|~(X735 @ X736))))&(((X735 @ (esk12_1 @ X735))|(((X736)!=(esk11_2 @ X735 @ X736))|~(X735 @ X736)))&(~(X735 @ X739)|((esk12_1 @ X735)=(X739))|(((X736)!=(esk11_2 @ X735 @ X736))|~(X735 @ X736)))))&((~(in @ X741 @ (prop2set @ ((X740))))|(X740))&((~(in @ X742 @ emptyset)|(X743))&((~(in @ X744 @ emptyset)|~($true))&(~(in @ X745 @ emptyset)&((((X746 @ (esk13_2 @ X746 @ X747))|~(X746 @ X747)|(X746 @ (esk14_1 @ X746)))&(((X747)!=(esk13_2 @ X746 @ X747))|~(X746 @ X747)|(X746 @ (esk14_1 @ X746))))&(((((in @ (esk16_2 @ X750 @ X751) @ X751)|((X750)=(X751))|(in @ (esk15_2 @ X750 @ X751) @ X750))&(~(in @ (esk16_2 @ X750 @ X751) @ X750)|((X750)=(X751))|(in @ (esk15_2 @ X750 @ X751) @ X750)))&(((in @ (esk16_2 @ X750 @ X751) @ X751)|((X750)=(X751))|~(in @ (esk15_2 @ X750 @ X751) @ X751))&(~(in @ (esk16_2 @ X750 @ X751) @ X750)|((X750)=(X751))|~(in @ (esk15_2 @ X750 @ X751) @ X751))))&(((in @ (esk17_1 @ X754) @ X754)|((X754)=(emptyset)))&(((in @ (esk18_1 @ X756) @ X756)|((X756)=(emptyset)))&(((~(in @ X760 @ (dsetconstr @ X758 @ X759))|(X759 @ X760)|~(in @ X760 @ X758))&(~(X759 @ X760)|(in @ X760 @ (dsetconstr @ X758 @ X759))|~(in @ X760 @ X758)))&((((X761)=(emptyset))|(in @ (esk19_1 @ X761) @ X761))&((~(in @ X765 @ X763)|(~(X764 @ X765)|((dsetconstr @ X763 @ X764)!=(emptyset))))&((~(in @ X767 @ X766)|((X766)!=(emptyset)))&((in @ X768 @ (setadjoin @ X768 @ X769))&((in @ emptyset @ (setadjoin @ emptyset @ emptyset))&((~(in @ X772 @ X771)|(in @ X772 @ (setadjoin @ X770 @ X771)))&(((((in @ X775 @ X774)|(X776)|((X775)=(X773))|~(in @ X775 @ (setadjoin @ X773 @ X774)))&(~(X776)|(X776)|((X775)=(X773))|~(in @ X775 @ (setadjoin @ X773 @ X774))))&(((in @ X775 @ X774)|(X776)|~(X776)|~(in @ X775 @ (setadjoin @ X773 @ X774)))&(~(X776)|(X776)|~(X776)|~(in @ X775 @ (setadjoin @ X773 @ X774)))))&((~(in @ X779 @ (setadjoin @ X777 @ X778))|(((X779)=(X777))|(in @ X779 @ X778)))&(((dsetconstr @ X780 @ (^[Z0:$i]:($true)))=(X780))&((((in @ (esk20_2 @ X781 @ X782) @ X782)|(in @ X782 @ (powerset @ X781)))&(~(in @ (esk20_2 @ X781 @ X782) @ X781)|(in @ X782 @ (powerset @ X781))))&((in @ emptyset @ (powerset @ X784))&((in @ emptyset @ (powerset @ X785))&((~(in @ X787 @ (powerset @ X786))|(~(in @ X788 @ X787)|(in @ X788 @ X786)))&((~(in @ X790 @ X791)|(~(in @ X791 @ X789)|(in @ X790 @ (setunion @ X789))))&((((in @ X793 @ (esk21_3 @ X792 @ X793 @ X794))|(X794)|~(in @ X793 @ (setunion @ X792)))&(((in @ (esk21_3 @ X792 @ X793 @ X794) @ X792)|(X794)|~(in @ X793 @ (setunion @ X792)))&(~(X794)|(X794)|~(in @ X793 @ (setunion @ X792)))))&((~(in @ X797 @ X796)|(in @ X797 @ (powerset @ (setunion @ X796))))&((((~(X798 @ X802)|((X802)=(esk23_1 @ X798))|((X798 @ (esk22_2 @ X798 @ X799))|~(X798 @ X799)))&(((X803)!=(esk23_1 @ X798))|(X798 @ X803)|((X798 @ (esk22_2 @ X798 @ X799))|~(X798 @ X799))))&((~(X798 @ X802)|((X802)=(esk23_1 @ X798))|(((X799)!=(esk22_2 @ X798 @ X799))|~(X798 @ X799)))&(((X803)!=(esk23_1 @ X798))|(X798 @ X803)|(((X799)!=(esk22_2 @ X798 @ X799))|~(X798 @ X799)))))&((((in @ (esk24_1 @ X804) @ X804)|((X804)=(emptyset)))&(($true)|((X804)=(emptyset))))&((~(in @ X806 @ (setadjoin @ X807 @ emptyset))|((X806)=(X807)))&((((X808)=(X809))|~(in @ X809 @ (setadjoin @ X808 @ emptyset)))&((((X810)!=(X811))|(in @ X810 @ (setadjoin @ X811 @ emptyset)))&((~(in @ X812 @ (setadjoin @ X813 @ emptyset))|(in @ X813 @ (setadjoin @ X812 @ emptyset)))&((~(in @ X816 @ (setadjoin @ X814 @ (setadjoin @ X815 @ emptyset)))|(((X816)=(X814))|((X816)=(X815))))&((in @ X817 @ (setadjoin @ X817 @ (setadjoin @ X818 @ emptyset)))&((in @ X820 @ (setadjoin @ X819 @ (setadjoin @ X820 @ emptyset)))&((~(in @ X823 @ X821)|~(X822 @ X823)|(((dsetconstr @ X821 @ X822)!=(emptyset))|~($true)))&((~(in @ X825 @ emptyset)|(X824 @ X825))&((((in @ (esk25_2 @ X826 @ X827) @ X826)|(~(in @ X828 @ X826)|(X827 @ X828)))&(~(X827 @ (esk25_2 @ X826 @ X827))|(~(in @ X828 @ X826)|(X827 @ X828))))&((((in @ (esk26_2 @ X830 @ X831) @ X830)|(~(in @ X833 @ X830)|~(X831 @ X833)))&((X831 @ (esk26_2 @ X830 @ X831))|(~(in @ X833 @ X830)|~(X831 @ X833))))&((((in @ (esk27_2 @ X834 @ X835) @ X834)|(~(in @ X837 @ X834)|~(X835 @ X837)))&((X835 @ (esk27_2 @ X834 @ X835))|(~(in @ X837 @ X834)|~(X835 @ X837))))&((((in @ (esk28_2 @ X838 @ X839) @ X838)|(~(in @ X840 @ X838)|(X839 @ X840)))&(~(X839 @ (esk28_2 @ X838 @ X839))|(~(in @ X840 @ X838)|(X839 @ X840))))&((~(X842)|(in @ emptyset @ (prop2set @ ((X842)))))&((~(X843)|(set2prop @ (prop2set @ ((X843)))))&((((in @ (esk29_2 @ X844 @ X845) @ X844)|(~(in @ X847 @ X844)|~(X845 @ X847)))&((X845 @ (esk29_2 @ X844 @ X845))|(~(in @ X847 @ X844)|~(X845 @ X847))))&((((in @ (esk30_2 @ X848 @ X849) @ X848)|(~(in @ X850 @ X848)|(X849 @ X850)))&(~(X849 @ (esk30_2 @ X848 @ X849))|(~(in @ X850 @ X848)|(X849 @ X850))))&(((((X852 @ (esk32_1 @ X852))|((X852 @ (esk31_2 @ X852 @ X853))|~(X852 @ X853)))&(~(X852 @ X856)|((esk32_1 @ X852)=(X856))|((X852 @ (esk31_2 @ X852 @ X853))|~(X852 @ X853))))&(((X852 @ (esk32_1 @ X852))|(((X853)!=(esk31_2 @ X852 @ X853))|~(X852 @ X853)))&(~(X852 @ X856)|((esk32_1 @ X852)=(X856))|(((X853)!=(esk31_2 @ X852 @ X853))|~(X852 @ X853)))))&(((((X857 @ (esk35_1 @ X857))|(X857 @ (esk33_1 @ X857))|~(X857 @ X858))&(~(X857 @ X862)|((esk35_1 @ X857)=(X862))|(X857 @ (esk33_1 @ X857))|~(X857 @ X858)))&((((X857 @ (esk35_1 @ X857))|(X857 @ (esk34_1 @ X857))|~(X857 @ X858))&(~(X857 @ X862)|((esk35_1 @ X857)=(X862))|(X857 @ (esk34_1 @ X857))|~(X857 @ X858)))&(((X857 @ (esk35_1 @ X857))|((esk33_1 @ X857)!=(esk34_1 @ X857))|~(X857 @ X858))&(~(X857 @ X862)|((esk35_1 @ X857)=(X862))|((esk33_1 @ X857)!=(esk34_1 @ X857))|~(X857 @ X858)))))&(((((X863 @ (esk37_1 @ X863))|(~(X863 @ (esk36_2 @ X863 @ X864))|((esk36_2 @ X863 @ X864)!=(X864))))&(~(X863 @ X867)|((esk37_1 @ X863)=(X867))|(~(X863 @ (esk36_2 @ X863 @ X864))|((esk36_2 @ X863 @ X864)!=(X864)))))&(((X863 @ (esk37_1 @ X863))|((X863 @ (esk36_2 @ X863 @ X864))|((esk36_2 @ X863 @ X864)=(X864))))&(~(X863 @ X867)|((esk37_1 @ X863)=(X867))|((X863 @ (esk36_2 @ X863 @ X864))|((esk36_2 @ X863 @ X864)=(X864))))))&((((X868)!=(X869))|(((X870)!=(X871))|(~(in @ X870 @ X868)|(in @ X871 @ X869))))&(((~(in @ X874 @ X872)|(in @ X875 @ X873)|((X874)!=(X875))|((X872)!=(X873)))&(~(in @ X875 @ X873)|(in @ X874 @ X872)|((X874)!=(X875))|((X872)!=(X873))))&((((X876 @ (esk38_2 @ X876 @ X877))|~(X876 @ X877)|(~(X876 @ X879)|(~(X876 @ X880)|((X879)=(X880)))))&(((X877)!=(esk38_2 @ X876 @ X877))|~(X876 @ X877)|(~(X876 @ X879)|(~(X876 @ X880)|((X879)=(X880))))))&(((((((X882 @ (esk42_2 @ X881 @ X882))|((X881 @ (esk41_3 @ X881 @ X882 @ X885))|~(X881 @ X885))|((esk39_2 @ X881 @ X882)=(esk40_2 @ X881 @ X882)))&(~(X882 @ X888)|((esk42_2 @ X881 @ X882)=(X888))|((X881 @ (esk41_3 @ X881 @ X882 @ X885))|~(X881 @ X885))|((esk39_2 @ X881 @ X882)=(esk40_2 @ X881 @ X882))))&(((X882 @ (esk42_2 @ X881 @ X882))|(((X885)!=(esk41_3 @ X881 @ X882 @ X885))|~(X881 @ X885))|((esk39_2 @ X881 @ X882)=(esk40_2 @ X881 @ X882)))&(~(X882 @ X888)|((esk42_2 @ X881 @ X882)=(X888))|(((X885)!=(esk41_3 @ X881 @ X882 @ X885))|~(X881 @ X885))|((esk39_2 @ X881 @ X882)=(esk40_2 @ X881 @ X882)))))&((((X881 @ (esk44_2 @ X881 @ X882))|((X882 @ (esk43_3 @ X881 @ X882 @ X889))|~(X882 @ X889))|((esk39_2 @ X881 @ X882)=(esk40_2 @ X881 @ X882)))&(~(X881 @ X892)|((esk44_2 @ X881 @ X882)=(X892))|((X882 @ (esk43_3 @ X881 @ X882 @ X889))|~(X882 @ X889))|((esk39_2 @ X881 @ X882)=(esk40_2 @ X881 @ X882))))&(((X881 @ (esk44_2 @ X881 @ X882))|(((X889)!=(esk43_3 @ X881 @ X882 @ X889))|~(X882 @ X889))|((esk39_2 @ X881 @ X882)=(esk40_2 @ X881 @ X882)))&(~(X881 @ X892)|((esk44_2 @ X881 @ X882)=(X892))|(((X889)!=(esk43_3 @ X881 @ X882 @ X889))|~(X882 @ X889))|((esk39_2 @ X881 @ X882)=(esk40_2 @ X881 @ X882))))))&((((((X882 @ (esk42_2 @ X881 @ X882))|((X881 @ (esk41_3 @ X881 @ X882 @ X885))|~(X881 @ X885))|(~(X881 @ (esk39_2 @ X881 @ X882))|~(X882 @ (esk40_2 @ X881 @ X882))))&(~(X882 @ X888)|((esk42_2 @ X881 @ X882)=(X888))|((X881 @ (esk41_3 @ X881 @ X882 @ X885))|~(X881 @ X885))|(~(X881 @ (esk39_2 @ X881 @ X882))|~(X882 @ (esk40_2 @ X881 @ X882)))))&(((X882 @ (esk42_2 @ X881 @ X882))|(((X885)!=(esk41_3 @ X881 @ X882 @ X885))|~(X881 @ X885))|(~(X881 @ (esk39_2 @ X881 @ X882))|~(X882 @ (esk40_2 @ X881 @ X882))))&(~(X882 @ X888)|((esk42_2 @ X881 @ X882)=(X888))|(((X885)!=(esk41_3 @ X881 @ X882 @ X885))|~(X881 @ X885))|(~(X881 @ (esk39_2 @ X881 @ X882))|~(X882 @ (esk40_2 @ X881 @ X882))))))&((((X881 @ (esk44_2 @ X881 @ X882))|((X882 @ (esk43_3 @ X881 @ X882 @ X889))|~(X882 @ X889))|(~(X881 @ (esk39_2 @ X881 @ X882))|~(X882 @ (esk40_2 @ X881 @ X882))))&(~(X881 @ X892)|((esk44_2 @ X881 @ X882)=(X892))|((X882 @ (esk43_3 @ X881 @ X882 @ X889))|~(X882 @ X889))|(~(X881 @ (esk39_2 @ X881 @ X882))|~(X882 @ (esk40_2 @ X881 @ X882)))))&(((X881 @ (esk44_2 @ X881 @ X882))|(((X889)!=(esk43_3 @ X881 @ X882 @ X889))|~(X882 @ X889))|(~(X881 @ (esk39_2 @ X881 @ X882))|~(X882 @ (esk40_2 @ X881 @ X882))))&(~(X881 @ X892)|((esk44_2 @ X881 @ X882)=(X892))|(((X889)!=(esk43_3 @ X881 @ X882 @ X889))|~(X882 @ X889))|(~(X881 @ (esk39_2 @ X881 @ X882))|~(X882 @ (esk40_2 @ X881 @ X882)))))))&(((((X882 @ (esk42_2 @ X881 @ X882))|((X881 @ (esk41_3 @ X881 @ X882 @ X885))|~(X881 @ X885))|((X881 @ (esk39_2 @ X881 @ X882))|(X882 @ (esk40_2 @ X881 @ X882))))&(~(X882 @ X888)|((esk42_2 @ X881 @ X882)=(X888))|((X881 @ (esk41_3 @ X881 @ X882 @ X885))|~(X881 @ X885))|((X881 @ (esk39_2 @ X881 @ X882))|(X882 @ (esk40_2 @ X881 @ X882)))))&(((X882 @ (esk42_2 @ X881 @ X882))|(((X885)!=(esk41_3 @ X881 @ X882 @ X885))|~(X881 @ X885))|((X881 @ (esk39_2 @ X881 @ X882))|(X882 @ (esk40_2 @ X881 @ X882))))&(~(X882 @ X888)|((esk42_2 @ X881 @ X882)=(X888))|(((X885)!=(esk41_3 @ X881 @ X882 @ X885))|~(X881 @ X885))|((X881 @ (esk39_2 @ X881 @ X882))|(X882 @ (esk40_2 @ X881 @ X882))))))&((((X881 @ (esk44_2 @ X881 @ X882))|((X882 @ (esk43_3 @ X881 @ X882 @ X889))|~(X882 @ X889))|((X881 @ (esk39_2 @ X881 @ X882))|(X882 @ (esk40_2 @ X881 @ X882))))&(~(X881 @ X892)|((esk44_2 @ X881 @ X882)=(X892))|((X882 @ (esk43_3 @ X881 @ X882 @ X889))|~(X882 @ X889))|((X881 @ (esk39_2 @ X881 @ X882))|(X882 @ (esk40_2 @ X881 @ X882)))))&(((X881 @ (esk44_2 @ X881 @ X882))|(((X889)!=(esk43_3 @ X881 @ X882 @ X889))|~(X882 @ X889))|((X881 @ (esk39_2 @ X881 @ X882))|(X882 @ (esk40_2 @ X881 @ X882))))&(~(X881 @ X892)|((esk44_2 @ X881 @ X882)=(X892))|(((X889)!=(esk43_3 @ X881 @ X882 @ X889))|~(X882 @ X889))|((X881 @ (esk39_2 @ X881 @ X882))|(X882 @ (esk40_2 @ X881 @ X882)))))))))&(((emptyset)=(emptyset))&((((X893)!=(X894))|(((X895)!=(X896))|((setadjoin @ X893 @ X895)=(setadjoin @ X894 @ X896))))&((((X897)!=(X898))|((powerset @ X897)=(powerset @ X898)))&((((X899)!=(X900))|((setunion @ X899)=(setunion @ X900)))&(((omega)=(omega))&((((X901 @ (esk45_2 @ X901 @ X902))|~(X901 @ X902)|(~(X901 @ X904)|(~(X901 @ X905)|((X904)=(X905)))))&(((X902)!=(esk45_2 @ X901 @ X902))|~(X901 @ X902)|(~(X901 @ X904)|(~(X901 @ X905)|((X904)=(X905))))))&((((((X907 @ (esk49_3 @ X906 @ X907 @ X912))|~(X907 @ X912)|((descr @ X906)=(descr @ X907))|((X906 @ (esk48_3 @ X906 @ X907 @ X910))|~(X906 @ X910))|((esk46_2 @ X906 @ X907)=(esk47_2 @ X906 @ X907)))&(((X912)!=(esk49_3 @ X906 @ X907 @ X912))|~(X907 @ X912)|((descr @ X906)=(descr @ X907))|((X906 @ (esk48_3 @ X906 @ X907 @ X910))|~(X906 @ X910))|((esk46_2 @ X906 @ X907)=(esk47_2 @ X906 @ X907))))&(((X907 @ (esk49_3 @ X906 @ X907 @ X912))|~(X907 @ X912)|((descr @ X906)=(descr @ X907))|(((X910)!=(esk48_3 @ X906 @ X907 @ X910))|~(X906 @ X910))|((esk46_2 @ X906 @ X907)=(esk47_2 @ X906 @ X907)))&(((X912)!=(esk49_3 @ X906 @ X907 @ X912))|~(X907 @ X912)|((descr @ X906)=(descr @ X907))|(((X910)!=(esk48_3 @ X906 @ X907 @ X910))|~(X906 @ X910))|((esk46_2 @ X906 @ X907)=(esk47_2 @ X906 @ X907)))))&(((((X907 @ (esk49_3 @ X906 @ X907 @ X912))|~(X907 @ X912)|((descr @ X906)=(descr @ X907))|((X906 @ (esk48_3 @ X906 @ X907 @ X910))|~(X906 @ X910))|(~(X906 @ (esk46_2 @ X906 @ X907))|~(X907 @ (esk47_2 @ X906 @ X907))))&(((X912)!=(esk49_3 @ X906 @ X907 @ X912))|~(X907 @ X912)|((descr @ X906)=(descr @ X907))|((X906 @ (esk48_3 @ X906 @ X907 @ X910))|~(X906 @ X910))|(~(X906 @ (esk46_2 @ X906 @ X907))|~(X907 @ (esk47_2 @ X906 @ X907)))))&(((X907 @ (esk49_3 @ X906 @ X907 @ X912))|~(X907 @ X912)|((descr @ X906)=(descr @ X907))|(((X910)!=(esk48_3 @ X906 @ X907 @ X910))|~(X906 @ X910))|(~(X906 @ (esk46_2 @ X906 @ X907))|~(X907 @ (esk47_2 @ X906 @ X907))))&(((X912)!=(esk49_3 @ X906 @ X907 @ X912))|~(X907 @ X912)|((descr @ X906)=(descr @ X907))|(((X910)!=(esk48_3 @ X906 @ X907 @ X910))|~(X906 @ X910))|(~(X906 @ (esk46_2 @ X906 @ X907))|~(X907 @ (esk47_2 @ X906 @ X907))))))&((((X907 @ (esk49_3 @ X906 @ X907 @ X912))|~(X907 @ X912)|((descr @ X906)=(descr @ X907))|((X906 @ (esk48_3 @ X906 @ X907 @ X910))|~(X906 @ X910))|((X906 @ (esk46_2 @ X906 @ X907))|(X907 @ (esk47_2 @ X906 @ X907))))&(((X912)!=(esk49_3 @ X906 @ X907 @ X912))|~(X907 @ X912)|((descr @ X906)=(descr @ X907))|((X906 @ (esk48_3 @ X906 @ X907 @ X910))|~(X906 @ X910))|((X906 @ (esk46_2 @ X906 @ X907))|(X907 @ (esk47_2 @ X906 @ X907)))))&(((X907 @ (esk49_3 @ X906 @ X907 @ X912))|~(X907 @ X912)|((descr @ X906)=(descr @ X907))|(((X910)!=(esk48_3 @ X906 @ X907 @ X910))|~(X906 @ X910))|((X906 @ (esk46_2 @ X906 @ X907))|(X907 @ (esk47_2 @ X906 @ X907))))&(((X912)!=(esk49_3 @ X906 @ X907 @ X912))|~(X907 @ X912)|((descr @ X906)=(descr @ X907))|(((X910)!=(esk48_3 @ X906 @ X907 @ X910))|~(X906 @ X910))|((X906 @ (esk46_2 @ X906 @ X907))|(X907 @ (esk47_2 @ X906 @ X907))))))))&((((in @ (esk50_4 @ X914 @ X915 @ X916 @ X917) @ X914)|((dsetconstr @ X914 @ X916)=(dsetconstr @ X915 @ X917))|((X914)!=(X915)))&(((in @ (esk51_4 @ X914 @ X915 @ X916 @ X917) @ X915)|((dsetconstr @ X914 @ X916)=(dsetconstr @ X915 @ X917))|((X914)!=(X915)))&((((esk50_4 @ X914 @ X915 @ X916 @ X917)=(esk51_4 @ X914 @ X915 @ X916 @ X917))|((dsetconstr @ X914 @ X916)=(dsetconstr @ X915 @ X917))|((X914)!=(X915)))&((~(X916 @ (esk50_4 @ X914 @ X915 @ X916 @ X917))|~(X917 @ (esk51_4 @ X914 @ X915 @ X916 @ X917))|((dsetconstr @ X914 @ X916)=(dsetconstr @ X915 @ X917))|((X914)!=(X915)))&((X916 @ (esk50_4 @ X914 @ X915 @ X916 @ X917))|(X917 @ (esk51_4 @ X914 @ X915 @ X916 @ X917))|((dsetconstr @ X914 @ X916)=(dsetconstr @ X915 @ X917))|((X914)!=(X915)))))))&((((in @ (esk52_2 @ X920 @ X921) @ X920)|(subset @ X920 @ X921))&(~(in @ (esk52_2 @ X920 @ X921) @ X921)|(subset @ X920 @ X921)))&((((X923)!=(X924))|(subset @ X924 @ X923))&((((X925)!=(X926))|(subset @ X925 @ X926))&((((in @ (esk53_2 @ X927 @ X928) @ X927)|(subset @ X927 @ X928))&(~(in @ (esk53_2 @ X927 @ X928) @ X928)|(subset @ X927 @ X928)))&((subset @ emptyset @ X930)&((~(subset @ X931 @ X932)|(~(in @ X933 @ X931)|(in @ X933 @ X932)))&((~(subset @ X934 @ X935)|((in @ X936 @ X935)|~(in @ X936 @ X934)))&((~(in @ X939 @ X937)|((in @ X939 @ X938)|~(subset @ X937 @ X938)))&(((subset @ X940 @ X941)|((X940)!=(X941)))&((~(in @ X944 @ X942)|((in @ X944 @ X943)|((X942)!=(X943))))&((subset @ X945 @ X945)&((~(subset @ X946 @ X947)|(~(subset @ X947 @ X948)|(subset @ X946 @ X948)))&((subset @ X950 @ (setadjoin @ X949 @ X950))&((~(subset @ X951 @ X953)|(subset @ X951 @ (setadjoin @ X952 @ X953)))&((~(subset @ X954 @ X955)|(in @ X954 @ (powerset @ X955)))&((~(subset @ X956 @ X957)|(~(subset @ X957 @ X956)|((X956)=(X957))))&((~(subset @ X958 @ emptyset)|((X958)=(emptyset)))&((~(subset @ X960 @ X959)|(in @ X960 @ (powerset @ X959)))&((~(in @ X962 @ (powerset @ X961))|(subset @ X962 @ X961))&((in @ X963 @ (powerset @ X963))&((~(subset @ X964 @ X965)|(subset @ (powerset @ X964) @ (powerset @ X965)))&((in @ (dsetconstr @ X966 @ X967) @ (powerset @ X966))&((subset @ (dsetconstr @ X968 @ X969) @ X968)&((~(in @ X972 @ X970)|(in @ X972 @ (binunion @ X970 @ X971)))&((in @ X974 @ (setadjoin @ X973 @ (setadjoin @ X974 @ emptyset)))&((~(in @ X977 @ X976)|(in @ X977 @ (binunion @ X975 @ X976)))&(((((in @ X980 @ X979)|(X981)|(in @ X980 @ X978)|~(in @ X980 @ (binunion @ X978 @ X979)))&(~(X981)|(X981)|(in @ X980 @ X978)|~(in @ X980 @ (binunion @ X978 @ X979))))&(((in @ X980 @ X979)|(X981)|~(X981)|~(in @ X980 @ (binunion @ X978 @ X979)))&(~(X981)|(X981)|~(X981)|~(in @ X980 @ (binunion @ X978 @ X979)))))&((~(in @ X984 @ (binunion @ X982 @ X983))|((in @ X984 @ X982)|(in @ X984 @ X983)))&((subset @ X985 @ (binunion @ X985 @ X986))&((subset @ X988 @ (binunion @ X987 @ X988))&((~(in @ X991 @ X989)|(~(in @ X991 @ X990)|(in @ X991 @ (binintersect @ X989 @ X990))))&((~(subset @ X994 @ X992)|(~(subset @ X994 @ X993)|(subset @ X994 @ (binintersect @ X992 @ X993))))&((~(in @ X997 @ (binintersect @ X995 @ X996))|(in @ X997 @ X995))&((subset @ (binintersect @ X998 @ X999) @ X998)&((~(subset @ X1000 @ X1001)|((binintersect @ X1000 @ X1001)=(X1000)))&((((binintersect @ X1002 @ X1003)!=(X1003))|(subset @ X1003 @ X1002))&((~(in @ X1006 @ (binintersect @ X1004 @ X1005))|(in @ X1006 @ X1005))&((((in @ (esk54_2 @ X1007 @ X1008) @ X1007)|((binintersect @ X1007 @ X1008)=(emptyset)))&((in @ (esk54_2 @ X1007 @ X1008) @ X1008)|((binintersect @ X1007 @ X1008)=(emptyset))))&((subset @ (binintersect @ X1010 @ X1011) @ X1011)&((subset @ esk56_0 @ esk55_0)&((binintersect @ esk55_0 @ esk56_0)!=(esk56_0)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), 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_159])])])])])])])).
% 1.55/0.48  thf(c_0_161, negated_conjecture, ![X3:$i, X2:$i]:((((X2)=(X3))|~((subset @ X2 @ X3))|~((subset @ X3 @ X2)))), inference(split_conjunct,[status(thm)],[c_0_160])).
% 1.55/0.48  thf(c_0_162, negated_conjecture, ![X2:$i, X3:$i]:((subset @ (binintersect @ X2 @ X3) @ X3)), inference(split_conjunct,[status(thm)],[c_0_160])).
% 1.55/0.48  thf(c_0_163, negated_conjecture, ![X2:$i, X3:$i]:((((binintersect @ X2 @ X3)=(X3))|~((subset @ X3 @ (binintersect @ X2 @ X3))))), inference(spm,[status(thm)],[c_0_161, c_0_162])).
% 1.55/0.48  thf(c_0_164, negated_conjecture, ![X2:$i, X3:$i, X4:$i]:(((subset @ X2 @ (binintersect @ X3 @ X4))|~((subset @ X2 @ X3))|~((subset @ X2 @ X4)))), inference(split_conjunct,[status(thm)],[c_0_160])).
% 1.55/0.48  thf(c_0_165, negated_conjecture, ![X2:$i]:((subset @ X2 @ X2)), inference(split_conjunct,[status(thm)],[c_0_160])).
% 1.55/0.48  thf(c_0_166, negated_conjecture, ((binintersect @ esk55_0 @ esk56_0)!=(esk56_0)), inference(split_conjunct,[status(thm)],[c_0_160])).
% 1.55/0.48  thf(c_0_167, negated_conjecture, ![X3:$i, X2:$i]:((((binintersect @ X2 @ X3)=(X3))|~((subset @ X3 @ X2)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_163, c_0_164]), c_0_165])])).
% 1.55/0.48  thf(c_0_168, negated_conjecture, (subset @ esk56_0 @ esk55_0), inference(split_conjunct,[status(thm)],[c_0_160])).
% 1.55/0.48  thf(c_0_169, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_166, c_0_167]), c_0_168])]), ['proof']).
% 1.55/0.48  % SZS output end CNFRefutation
% 1.55/0.48  % Parsed axioms                        : 248
% 1.55/0.48  % Removed by relevancy pruning/SinE    : 0
% 1.55/0.48  % Initial clauses                      : 363
% 1.55/0.48  % Removed in clause preprocessing      : 149
% 1.55/0.48  % Initial clauses in saturation        : 214
% 1.55/0.48  % Processed clauses                    : 1414
% 1.55/0.48  % ...of these trivial                  : 9
% 1.55/0.48  % ...subsumed                          : 823
% 1.55/0.48  % ...remaining for further processing  : 582
% 1.55/0.48  % Other redundant clauses eliminated   : 16
% 1.55/0.48  % Clauses deleted for lack of memory   : 0
% 1.55/0.48  % Backward-subsumed                    : 1
% 1.55/0.48  % Backward-rewritten                   : 6
% 1.55/0.48  % Generated clauses                    : 18348
% 1.55/0.48  % ...of the previous two non-redundant : 15475
% 1.55/0.48  % ...aggressively subsumed             : 0
% 1.55/0.48  % Contextual simplify-reflections      : 2
% 1.55/0.48  % Paramodulations                      : 18330
% 1.55/0.48  % Factorizations                       : 2
% 1.55/0.48  % NegExts                              : 0
% 1.55/0.48  % Equation resolutions                 : 16
% 1.55/0.48  % Disequality decompositions           : 0
% 1.55/0.48  % Total rewrite steps                  : 5591
% 1.55/0.48  % ...of those cached                   : 5393
% 1.55/0.48  % Propositional unsat checks           : 0
% 1.55/0.48  %    Propositional check models        : 0
% 1.55/0.48  %    Propositional check unsatisfiable : 0
% 1.55/0.48  %    Propositional clauses             : 0
% 1.55/0.48  %    Propositional clauses after purity: 0
% 1.55/0.48  %    Propositional unsat core size     : 0
% 1.55/0.48  %    Propositional preprocessing time  : 0.000
% 1.55/0.48  %    Propositional encoding time       : 0.000
% 1.55/0.48  %    Propositional solver time         : 0.000
% 1.55/0.48  %    Success case prop preproc time    : 0.000
% 1.55/0.48  %    Success case prop encoding time   : 0.000
% 1.55/0.48  %    Success case prop solver time     : 0.000
% 1.55/0.48  % Current number of processed clauses  : 567
% 1.55/0.48  %    Positive orientable unit clauses  : 198
% 1.55/0.48  %    Positive unorientable unit clauses: 0
% 1.55/0.48  %    Negative unit clauses             : 4
% 1.55/0.48  %    Non-unit-clauses                  : 365
% 1.55/0.48  % Current number of unprocessed clauses: 14205
% 1.55/0.48  % ...number of literals in the above   : 50919
% 1.55/0.48  % Current number of archived formulas  : 0
% 1.55/0.48  % Current number of archived clauses   : 7
% 1.55/0.48  % Clause-clause subsumption calls (NU) : 16124
% 1.55/0.48  % Rec. Clause-clause subsumption calls : 8838
% 1.55/0.48  % Non-unit clause-clause subsumptions  : 603
% 1.55/0.48  % Unit Clause-clause subsumption calls : 79
% 1.55/0.48  % Rewrite failures with RHS unbound    : 0
% 1.55/0.48  % BW rewrite match attempts            : 1019
% 1.55/0.48  % BW rewrite match successes           : 4
% 1.55/0.48  % Condensation attempts                : 0
% 1.55/0.48  % Condensation successes               : 0
% 1.55/0.48  % Termbank termtop insertions          : 378751
% 1.55/0.48  % Search garbage collected termcells   : 11632
% 1.55/0.48  
% 1.55/0.48  % -------------------------------------------------
% 1.55/0.48  % User time                : 0.201 s
% 1.55/0.48  % System time              : 0.014 s
% 1.55/0.48  % Total time               : 0.215 s
% 1.55/0.48  % Maximum resident set size: 6432 pages
% 1.55/0.48  
% 1.55/0.48  % -------------------------------------------------
% 1.55/0.48  % User time                : 0.260 s
% 1.55/0.48  % System time              : 0.048 s
% 1.55/0.48  % Total time               : 0.308 s
% 1.55/0.48  % Maximum resident set size: 5120 pages
% 1.55/0.48  % E exiting
%------------------------------------------------------------------------------