%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : SEU655^1 : TPTP v9.3.1. Released v3.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:24:54 AM UTC 2026
% Result : Theorem 3.24s 0.78s
% Output : CNFRefutation 3.24s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU655^1 : TPTP v9.3.1. Released v3.7.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.17 % Computer : n007.cluster.edu
% 0.09/0.17 % Model : x86_64 x86_64
% 0.09/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.17 % Memory : 8046.5625MB
% 0.09/0.17 % OS : Linux 6.8.0-71-generic
% 0.09/0.17 % CPULimit : 300
% 0.09/0.17 % WCLimit : 300
% 0.09/0.17 % DateTime : Tue Sep 29 14:01:10 UTC 2026
% 0.09/0.17 % CPUTime :
% 0.09/0.17 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.22 Running higher-order theorem proving
% 0.09/0.26 Running: /export/starexec/sandbox/solver/bin/eprover-ho --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox/tmp/tmp.45u3Cojn4q/E---3.1_3416988.p
% 3.24/0.78 % Version: 3.5.1-ho
% 3.24/0.78 % Preprocessing class: HSLMSLSSLLLCHSA.
% 3.24/0.78 % Scheduled 5 strats onto 8 cores with 300 seconds (2400 total)
% 3.24/0.78 % Starting ho_unfolding_5 with 1200s (4) cores
% 3.24/0.78 % Starting pre_casc_3 with 300s (1) cores
% 3.24/0.78 % Starting new_ho_10_cnf2 with 300s (1) cores
% 3.24/0.78 % Starting full_lambda_10 with 300s (1) cores
% 3.24/0.78 % Starting ehoh_best_nonlift_rwall with 300s (1) cores
% 3.24/0.78 % pre_casc_3 with pid 3417002 completed with status 0
% 3.24/0.78 % Result found by pre_casc_3
% 3.24/0.78 % Preprocessing class: HSLMSLSSLLLCHSA.
% 3.24/0.78 % Scheduled 5 strats onto 8 cores with 300 seconds (2400 total)
% 3.24/0.78 % Starting ho_unfolding_5 with 1200s (4) cores
% 3.24/0.78 % Starting pre_casc_3 with 300s (1) cores
% 3.24/0.78 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = GSinE(CountFormulas,hypos,10,,5,20000,3.0,true))
% 3.24/0.78 % SinE strategy is GSinE(CountFormulas,hypos,10,,5,20000,3.0,true)
% 3.24/0.78 % Search class: HGHSM-FFMM32-MHSMMSBN
% 3.24/0.78 % partial match(2): HGHSM-FSLM32-MHSMMSBN
% 3.24/0.78 % Scheduled 11 strats onto 1 cores with 300 seconds (300 total)
% 3.24/0.78 % Starting SubtermCWHack with 31s (1) cores
% 3.24/0.78 % SubtermCWHack with pid 3417007 completed with status 0
% 3.24/0.78 % Result found by SubtermCWHack
% 3.24/0.78 % Preprocessing class: HSLMSLSSLLLCHSA.
% 3.24/0.78 % Scheduled 5 strats onto 8 cores with 300 seconds (2400 total)
% 3.24/0.78 % Starting ho_unfolding_5 with 1200s (4) cores
% 3.24/0.78 % Starting pre_casc_3 with 300s (1) cores
% 3.24/0.78 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = GSinE(CountFormulas,hypos,10,,5,20000,3.0,true))
% 3.24/0.78 % SinE strategy is GSinE(CountFormulas,hypos,10,,5,20000,3.0,true)
% 3.24/0.78 % Search class: HGHSM-FFMM32-MHSMMSBN
% 3.24/0.78 % partial match(2): HGHSM-FSLM32-MHSMMSBN
% 3.24/0.78 % Scheduled 11 strats onto 1 cores with 300 seconds (300 total)
% 3.24/0.78 % Starting SubtermCWHack with 31s (1) cores
% 3.24/0.78 % Preprocessing time : 0.003 s
% 3.24/0.78
% 3.24/0.78 % Proof found!
% 3.24/0.78 % SZS status Theorem
% 3.24/0.78 % SZS output start CNFRefutation
% 3.24/0.78 thf(decl_23, type, in: $i > $i > $o).
% 3.24/0.78 thf(decl_25, type, setextAx: $o).
% 3.24/0.78 thf(decl_26, type, emptyset: $i).
% 3.24/0.78 thf(decl_27, type, emptysetAx: $o).
% 3.24/0.78 thf(decl_28, type, setadjoin: $i > $i > $i).
% 3.24/0.78 thf(decl_29, type, setadjoinAx: $o).
% 3.24/0.78 thf(decl_30, type, powerset: $i > $i).
% 3.24/0.78 thf(decl_31, type, powersetAx: $o).
% 3.24/0.78 thf(decl_32, type, setunion: $i > $i).
% 3.24/0.78 thf(decl_33, type, setunionAx: $o).
% 3.24/0.78 thf(decl_35, type, omega0Ax: $o).
% 3.24/0.78 thf(decl_36, type, omegaSAx: $o).
% 3.24/0.78 thf(decl_37, type, omegaIndAx: $o).
% 3.24/0.78 thf(decl_38, type, replAx: $o).
% 3.24/0.78 thf(decl_39, type, foundationAx: $o).
% 3.24/0.78 thf(decl_40, type, wellorderingAx: $o).
% 3.24/0.78 thf(decl_42, type, descrp: $o).
% 3.24/0.78 thf(decl_43, type, dsetconstr: $i > ($i > $o) > $i).
% 3.24/0.78 thf(decl_44, type, dsetconstrI: $o).
% 3.24/0.78 thf(decl_45, type, dsetconstrEL: $o).
% 3.24/0.78 thf(decl_46, type, dsetconstrER: $o).
% 3.24/0.78 thf(decl_47, type, exuE1: $o).
% 3.24/0.78 thf(decl_49, type, prop2setE: $o).
% 3.24/0.78 thf(decl_50, type, emptysetE: $o).
% 3.24/0.78 thf(decl_51, type, emptysetimpfalse: $o).
% 3.24/0.78 thf(decl_52, type, notinemptyset: $o).
% 3.24/0.78 thf(decl_53, type, exuE3e: $o).
% 3.24/0.78 thf(decl_54, type, setext: $o).
% 3.24/0.78 thf(decl_55, type, emptyI: $o).
% 3.24/0.78 thf(decl_56, type, noeltsimpempty: $o).
% 3.24/0.78 thf(decl_57, type, setbeta: $o).
% 3.24/0.78 thf(decl_59, type, nonemptyE1: $o).
% 3.24/0.78 thf(decl_60, type, nonemptyI: $o).
% 3.24/0.78 thf(decl_61, type, nonemptyI1: $o).
% 3.24/0.78 thf(decl_62, type, setadjoinIL: $o).
% 3.24/0.78 thf(decl_63, type, emptyinunitempty: $o).
% 3.24/0.78 thf(decl_64, type, setadjoinIR: $o).
% 3.24/0.78 thf(decl_65, type, setadjoinE: $o).
% 3.24/0.78 thf(decl_66, type, setadjoinOr: $o).
% 3.24/0.78 thf(decl_67, type, setoftrueEq: $o).
% 3.24/0.78 thf(decl_68, type, powersetI: $o).
% 3.24/0.78 thf(decl_69, type, emptyinPowerset: $o).
% 3.24/0.78 thf(decl_70, type, emptyInPowerset: $o).
% 3.24/0.78 thf(decl_71, type, powersetE: $o).
% 3.24/0.78 thf(decl_72, type, setunionI: $o).
% 3.24/0.78 thf(decl_73, type, setunionE: $o).
% 3.24/0.78 thf(decl_74, type, subPowSU: $o).
% 3.24/0.78 thf(decl_75, type, exuE2: $o).
% 3.24/0.78 thf(decl_76, type, nonemptyImpWitness: $o).
% 3.24/0.78 thf(decl_77, type, uniqinunit: $o).
% 3.24/0.78 thf(decl_78, type, notinsingleton: $o).
% 3.24/0.78 thf(decl_79, type, eqinunit: $o).
% 3.24/0.78 thf(decl_80, type, singletonsswitch: $o).
% 3.24/0.78 thf(decl_81, type, upairsetE: $o).
% 3.24/0.78 thf(decl_82, type, upairsetIL: $o).
% 3.24/0.78 thf(decl_83, type, upairsetIR: $o).
% 3.24/0.78 thf(decl_84, type, emptyE1: $o).
% 3.24/0.78 thf(decl_85, type, vacuousDall: $o).
% 3.24/0.78 thf(decl_86, type, quantDeMorgan1: $o).
% 3.24/0.78 thf(decl_87, type, quantDeMorgan2: $o).
% 3.24/0.78 thf(decl_88, type, quantDeMorgan3: $o).
% 3.24/0.78 thf(decl_89, type, quantDeMorgan4: $o).
% 3.24/0.78 thf(decl_90, type, prop2setI: $o).
% 3.24/0.78 thf(decl_92, type, prop2set2propI: $o).
% 3.24/0.78 thf(decl_93, type, notdexE: $o).
% 3.24/0.78 thf(decl_94, type, notdallE: $o).
% 3.24/0.78 thf(decl_95, type, exuI1: $o).
% 3.24/0.78 thf(decl_96, type, exuI3: $o).
% 3.24/0.78 thf(decl_97, type, exuI2: $o).
% 3.24/0.78 thf(decl_98, type, inCongP: $o).
% 3.24/0.78 thf(decl_99, type, in__Cong: $o).
% 3.24/0.78 thf(decl_100, type, exuE3u: $o).
% 3.24/0.78 thf(decl_101, type, exu__Cong: $o).
% 3.24/0.78 thf(decl_102, type, emptyset__Cong: $o).
% 3.24/0.78 thf(decl_103, type, setadjoin__Cong: $o).
% 3.24/0.78 thf(decl_104, type, powerset__Cong: $o).
% 3.24/0.78 thf(decl_105, type, setunion__Cong: $o).
% 3.24/0.78 thf(decl_106, type, omega__Cong: $o).
% 3.24/0.78 thf(decl_107, type, exuEu: $o).
% 3.24/0.78 thf(decl_108, type, descr__Cong: $o).
% 3.24/0.78 thf(decl_109, type, dsetconstr__Cong: $o).
% 3.24/0.78 thf(decl_113, type, subsetI1: $o).
% 3.24/0.78 thf(decl_114, type, eqimpsubset2: $o).
% 3.24/0.78 thf(decl_115, type, eqimpsubset1: $o).
% 3.24/0.78 thf(decl_116, type, subsetI2: $o).
% 3.24/0.78 thf(decl_117, type, emptysetsubset: $o).
% 3.24/0.78 thf(decl_118, type, subsetE: $o).
% 3.24/0.78 thf(decl_119, type, subsetE2: $o).
% 3.24/0.78 thf(decl_120, type, notsubsetI: $o).
% 3.24/0.78 thf(decl_121, type, notequalI1: $o).
% 3.24/0.78 thf(decl_122, type, notequalI2: $o).
% 3.24/0.78 thf(decl_123, type, subsetRefl: $o).
% 3.24/0.78 thf(decl_124, type, subsetTrans: $o).
% 3.24/0.78 thf(decl_125, type, setadjoinSub: $o).
% 3.24/0.78 thf(decl_126, type, setadjoinSub2: $o).
% 3.24/0.78 thf(decl_127, type, subset2powerset: $o).
% 3.24/0.78 thf(decl_128, type, setextsub: $o).
% 3.24/0.78 thf(decl_129, type, subsetemptysetimpeq: $o).
% 3.24/0.78 thf(decl_130, type, powersetI1: $o).
% 3.24/0.78 thf(decl_131, type, powersetE1: $o).
% 3.24/0.78 thf(decl_132, type, inPowerset: $o).
% 3.24/0.78 thf(decl_133, type, powersetsubset: $o).
% 3.24/0.78 thf(decl_134, type, sepInPowerset: $o).
% 3.24/0.78 thf(decl_135, type, sepSubset: $o).
% 3.24/0.78 thf(decl_136, type, binunion: $i > $i > $i).
% 3.24/0.78 thf(decl_137, type, binunionIL: $o).
% 3.24/0.78 thf(decl_138, type, upairset2IR: $o).
% 3.24/0.78 thf(decl_139, type, binunionIR: $o).
% 3.24/0.78 thf(decl_140, type, binunionEcases: $o).
% 3.24/0.78 thf(decl_141, type, binunionE: $o).
% 3.24/0.78 thf(decl_142, type, binunionLsub: $o).
% 3.24/0.78 thf(decl_143, type, binunionRsub: $o).
% 3.24/0.78 thf(decl_145, type, binintersectI: $o).
% 3.24/0.78 thf(decl_146, type, binintersectSubset5: $o).
% 3.24/0.78 thf(decl_147, type, binintersectEL: $o).
% 3.24/0.78 thf(decl_148, type, binintersectLsub: $o).
% 3.24/0.78 thf(decl_149, type, binintersectSubset2: $o).
% 3.24/0.78 thf(decl_150, type, binintersectSubset3: $o).
% 3.24/0.78 thf(decl_151, type, binintersectER: $o).
% 3.24/0.78 thf(decl_152, type, disjointsetsI1: $o).
% 3.24/0.78 thf(decl_153, type, binintersectRsub: $o).
% 3.24/0.78 thf(decl_154, type, binintersectSubset4: $o).
% 3.24/0.78 thf(decl_155, type, binintersectSubset1: $o).
% 3.24/0.78 thf(decl_156, type, bs114d: $o).
% 3.24/0.78 thf(decl_159, type, setminusI: $o).
% 3.24/0.78 thf(decl_160, type, setminusEL: $o).
% 3.24/0.78 thf(decl_161, type, setminusER: $o).
% 3.24/0.78 thf(decl_162, type, setminusSubset2: $o).
% 3.24/0.78 thf(decl_163, type, setminusERneg: $o).
% 3.24/0.78 thf(decl_164, type, setminusELneg: $o).
% 3.24/0.78 thf(decl_165, type, setminusILneg: $o).
% 3.24/0.78 thf(decl_166, type, setminusIRneg: $o).
% 3.24/0.78 thf(decl_167, type, setminusLsub: $o).
% 3.24/0.78 thf(decl_168, type, setminusSubset1: $o).
% 3.24/0.78 thf(decl_170, type, symdiffE: $o).
% 3.24/0.78 thf(decl_171, type, symdiffI1: $o).
% 3.24/0.78 thf(decl_172, type, symdiffI2: $o).
% 3.24/0.78 thf(decl_173, type, symdiffIneg1: $o).
% 3.24/0.78 thf(decl_174, type, symdiffIneg2: $o).
% 3.24/0.78 thf(decl_175, type, iskpair: $i > $o).
% 3.24/0.78 thf(decl_176, type, secondinupair: $o).
% 3.24/0.78 thf(decl_177, type, setukpairIL: $o).
% 3.24/0.78 thf(decl_178, type, setukpairIR: $o).
% 3.24/0.78 thf(decl_179, type, kpairiskpair: $o).
% 3.24/0.78 thf(decl_180, type, kpair: $i > $i > $i).
% 3.24/0.78 thf(decl_181, type, kpairp: $o).
% 3.24/0.78 thf(decl_182, type, cartprod: $i > $i > $i).
% 3.24/0.78 thf(decl_183, type, singletonsubset: $o).
% 3.24/0.78 thf(decl_184, type, singletoninpowerset: $o).
% 3.24/0.78 thf(decl_185, type, singletoninpowunion: $o).
% 3.24/0.78 thf(decl_186, type, upairset2E: $o).
% 3.24/0.78 thf(decl_187, type, upairsubunion: $o).
% 3.24/0.78 thf(decl_188, type, upairinpowunion: $o).
% 3.24/0.78 thf(decl_189, type, ubforcartprodlem1: $o).
% 3.24/0.78 thf(decl_190, type, ubforcartprodlem2: $o).
% 3.24/0.78 thf(decl_191, type, ubforcartprodlem3: $o).
% 3.24/0.78 thf(decl_192, type, cartprodpairin: $o).
% 3.24/0.78 thf(decl_193, type, cartprodmempair1: $o).
% 3.24/0.78 thf(decl_194, type, cartprodmempair: $o).
% 3.24/0.78 thf(decl_195, type, setunionE2: $o).
% 3.24/0.78 thf(decl_196, type, setunionsingleton1: $o).
% 3.24/0.78 thf(decl_197, type, setunionsingleton2: $o).
% 3.24/0.78 thf(decl_198, type, setunionsingleton: $o).
% 3.24/0.78 thf(decl_199, type, singleton: $i > $o).
% 3.24/0.78 thf(decl_200, type, singletonprop: $o).
% 3.24/0.78 thf(decl_201, type, ex1: $i > ($i > $o) > $o).
% 3.24/0.78 thf(decl_202, type, ex1E1: $o).
% 3.24/0.78 thf(decl_203, type, ex1I: $o).
% 3.24/0.78 thf(decl_204, type, ex1I2: $o).
% 3.24/0.78 thf(decl_205, type, singletonsuniq: $o).
% 3.24/0.78 thf(decl_210, type, setukpairinjL1: $o).
% 3.24/0.78 thf(decl_211, type, kfstsingleton: $o).
% 3.24/0.78 thf(decl_212, type, theprop: $o).
% 3.24/0.78 thf(decl_213, type, kfst: $i > $i).
% 3.24/0.78 thf(decl_214, type, kfstpairEq: $o).
% 3.24/0.78 thf(decl_215, type, cartprodfstin: $o).
% 3.24/0.78 thf(decl_216, type, setukpairinjL2: $o).
% 3.24/0.78 thf(decl_217, type, setukpairinjL: $o).
% 3.24/0.78 thf(decl_218, type, setukpairinjR11: $o).
% 3.24/0.78 thf(decl_219, type, setukpairinjR12: $o).
% 3.24/0.78 thf(decl_220, type, setukpairinjR1: $o).
% 3.24/0.78 thf(decl_221, type, upairequniteq: $o).
% 3.24/0.78 thf(decl_222, type, setukpairinjR2: $o).
% 3.24/0.78 thf(decl_223, type, setukpairinjR: $o).
% 3.24/0.78 thf(decl_224, type, esk1_2: $i > $i > $i).
% 3.24/0.78 thf(decl_225, type, esk2_2: $i > $i > $i).
% 3.24/0.78 thf(decl_226, type, esk3_2: $i > $i > $i).
% 3.24/0.78 thf(decl_227, type, esk4_2: $i > $i > $i).
% 3.24/0.78 thf(decl_228, type, esk5_3: $i > $i > $i > $i).
% 3.24/0.78 thf(decl_229, type, esk6_3: $i > $i > $i > $i).
% 3.24/0.78 thf(decl_230, type, esk7_3: $i > $i > $i > $i).
% 3.24/0.78 thf(decl_231, type, esk8_3: $i > $i > $i > $i).
% 3.24/0.78 thf(decl_232, type, esk9_2: $i > ($i > $o) > $i).
% 3.24/0.78 thf(decl_233, type, esk10_2: $i > ($i > $o) > $i).
% 3.24/0.78 thf(decl_234, type, esk11_2: $i > ($i > $o) > $i).
% 3.24/0.78 thf(decl_235, type, esk12_2: $i > ($i > $o) > $i).
% 3.24/0.78 thf(decl_236, type, esk13_3: $i > ($i > $o) > $i > $i).
% 3.24/0.78 thf(decl_237, type, esk14_3: $i > ($i > $o) > $i > $i).
% 3.24/0.78 thf(decl_238, type, esk15_2: $i > ($i > $o) > $i).
% 3.24/0.78 thf(decl_239, type, esk16_2: $i > ($i > $o) > $i).
% 3.24/0.78 thf(decl_240, type, esk17_2: $i > ($i > $o) > $i).
% 3.24/0.78 thf(decl_241, type, esk18_1: $i > $i).
% 3.24/0.78 thf(decl_242, type, esk19_0: $i).
% 3.24/0.78 thf(decl_243, type, esk20_0: $i).
% 3.24/0.78 thf(decl_244, type, esk21_0: $i).
% 3.24/0.78 thf(decl_245, type, epred1_0: $i > $o).
% 3.24/0.78 thf(ex1, axiom, ((ex1)=(^[X4:$i, X1:$i > $o]:((singleton @ (dsetconstr @ X4 @ (^[X2:$i]:((X1 @ X2)))))))), file('/export/starexec/sandbox/tmp/tmp.45u3Cojn4q/E---3.1_3416988.p', ex1)).
% 3.24/0.78 thf(singleton, axiom, ((singleton)=(^[X4:$i]:(?[X2:$i]:((((in @ X2 @ X4))&(((X4)=(setadjoin @ X2 @ emptyset)))))))), file('/export/starexec/sandbox/tmp/tmp.45u3Cojn4q/E---3.1_3416988.p', singleton)).
% 3.24/0.78 thf(ex1I2, axiom, ((ex1I2)<=>![X4:$i, X1:$i > $o]:((![X2:$i]:(((in @ X2 @ X4)=>![X3:$i]:(((in @ X3 @ X4)=>((X1 @ X2)=>((X1 @ X3)=>((X2)=(X3))))))))=>(?[X2:$i]:(((in @ X2 @ X4)&(X1 @ X2)))=>(ex1 @ X4 @ (^[X2:$i]:((X1 @ X2)))))))), file('/export/starexec/sandbox/tmp/tmp.45u3Cojn4q/E---3.1_3416988.p', ex1I2)).
% 3.24/0.78 thf(ex1I, axiom, ((ex1I)<=>![X4:$i, X1:$i > $o, X2:$i]:(((in @ X2 @ X4)=>((X1 @ X2)=>(![X3:$i]:(((in @ X3 @ X4)=>((X1 @ X3)=>((X3)=(X2)))))=>(ex1 @ X4 @ (^[X3:$i]:((X1 @ X3))))))))), file('/export/starexec/sandbox/tmp/tmp.45u3Cojn4q/E---3.1_3416988.p', ex1I)).
% 3.24/0.78 thf(ex1E1, axiom, ((ex1E1)<=>![X4:$i, X1:$i > $o]:(((ex1 @ X4 @ (^[X2:$i]:((X1 @ X2))))=>?[X2:$i]:(((in @ X2 @ X4)&(X1 @ X2)))))), file('/export/starexec/sandbox/tmp/tmp.45u3Cojn4q/E---3.1_3416988.p', ex1E1)).
% 3.24/0.78 thf(iskpair, axiom, ((iskpair)=(^[X4:$i]:(?[X2:$i]:((((in @ X2 @ (setunion @ X4)))&(?[X3:$i]:((((in @ X3 @ (setunion @ X4)))&(((X4)=(setadjoin @ (setadjoin @ X2 @ emptyset) @ (setadjoin @ (setadjoin @ X2 @ (setadjoin @ X3 @ emptyset)) @ emptyset)))))))))))), file('/export/starexec/sandbox/tmp/tmp.45u3Cojn4q/E---3.1_3416988.p', iskpair)).
% 3.24/0.78 thf(kfstsingleton, axiom, ((kfstsingleton)<=>![X18:$i]:(((iskpair @ X18)=>(singleton @ (dsetconstr @ (setunion @ X18) @ (^[X2:$i]:((in @ (setadjoin @ X2 @ emptyset) @ X18)))))))), file('/export/starexec/sandbox/tmp/tmp.45u3Cojn4q/E---3.1_3416988.p', kfstsingleton)).
% 3.24/0.78 thf(singletonprop, axiom, ((singletonprop)<=>![X4:$i, X1:$i > $o]:((![X2:$i]:(((in @ X2 @ X4)=>![X3:$i]:(((in @ X3 @ X4)=>((X1 @ X2)=>((X1 @ X3)=>((X2)=(X3))))))))=>(?[X2:$i]:(((in @ X2 @ X4)&(X1 @ X2)))=>(singleton @ (dsetconstr @ X4 @ (^[X2:$i]:((X1 @ X2))))))))), file('/export/starexec/sandbox/tmp/tmp.45u3Cojn4q/E---3.1_3416988.p', singletonprop)).
% 3.24/0.78 thf(ksndsingleton, conjecture, ((setextAx)=>((emptysetAx)=>((setadjoinAx)=>((powersetAx)=>((setunionAx)=>((omega0Ax)=>((omegaSAx)=>((omegaIndAx)=>((replAx)=>((foundationAx)=>((wellorderingAx)=>((descrp)=>((dsetconstrI)=>((dsetconstrEL)=>((dsetconstrER)=>((exuE1)=>((prop2setE)=>((emptysetE)=>((emptysetimpfalse)=>((notinemptyset)=>((exuE3e)=>((setext)=>((emptyI)=>((noeltsimpempty)=>((setbeta)=>((nonemptyE1)=>((nonemptyI)=>((nonemptyI1)=>((setadjoinIL)=>((emptyinunitempty)=>((setadjoinIR)=>((setadjoinE)=>((setadjoinOr)=>((setoftrueEq)=>((powersetI)=>((emptyinPowerset)=>((emptyInPowerset)=>((powersetE)=>((setunionI)=>((setunionE)=>((subPowSU)=>((exuE2)=>((nonemptyImpWitness)=>((uniqinunit)=>((notinsingleton)=>((eqinunit)=>((singletonsswitch)=>((upairsetE)=>((upairsetIL)=>((upairsetIR)=>((emptyE1)=>((vacuousDall)=>((quantDeMorgan1)=>((quantDeMorgan2)=>((quantDeMorgan3)=>((quantDeMorgan4)=>((prop2setI)=>((prop2set2propI)=>((notdexE)=>((notdallE)=>((exuI1)=>((exuI3)=>((exuI2)=>((inCongP)=>((in__Cong)=>((exuE3u)=>((exu__Cong)=>((emptyset__Cong)=>((setadjoin__Cong)=>((powerset__Cong)=>((setunion__Cong)=>((omega__Cong)=>((exuEu)=>((descr__Cong)=>((dsetconstr__Cong)=>((subsetI1)=>((eqimpsubset2)=>((eqimpsubset1)=>((subsetI2)=>((emptysetsubset)=>((subsetE)=>((subsetE2)=>((notsubsetI)=>((notequalI1)=>((notequalI2)=>((subsetRefl)=>((subsetTrans)=>((setadjoinSub)=>((setadjoinSub2)=>((subset2powerset)=>((setextsub)=>((subsetemptysetimpeq)=>((powersetI1)=>((powersetE1)=>((inPowerset)=>((powersetsubset)=>((sepInPowerset)=>((sepSubset)=>((binunionIL)=>((upairset2IR)=>((binunionIR)=>((binunionEcases)=>((binunionE)=>((binunionLsub)=>((binunionRsub)=>((binintersectI)=>((binintersectSubset5)=>((binintersectEL)=>((binintersectLsub)=>((binintersectSubset2)=>((binintersectSubset3)=>((binintersectER)=>((disjointsetsI1)=>((binintersectRsub)=>((binintersectSubset4)=>((binintersectSubset1)=>((bs114d)=>((setminusI)=>((setminusEL)=>((setminusER)=>((setminusSubset2)=>((setminusERneg)=>((setminusELneg)=>((setminusILneg)=>((setminusIRneg)=>((setminusLsub)=>((setminusSubset1)=>((symdiffE)=>((symdiffI1)=>((symdiffI2)=>((symdiffIneg1)=>((symdiffIneg2)=>((secondinupair)=>((setukpairIL)=>((setukpairIR)=>((kpairiskpair)=>((kpairp)=>((singletonsubset)=>((singletoninpowerset)=>((singletoninpowunion)=>((upairset2E)=>((upairsubunion)=>((upairinpowunion)=>((ubforcartprodlem1)=>((ubforcartprodlem2)=>((ubforcartprodlem3)=>((cartprodpairin)=>((cartprodmempair1)=>((cartprodmempair)=>((setunionE2)=>((setunionsingleton1)=>((setunionsingleton2)=>((setunionsingleton)=>((singletonprop)=>((ex1E1)=>((ex1I)=>((ex1I2)=>((singletonsuniq)=>((setukpairinjL1)=>((kfstsingleton)=>((theprop)=>((kfstpairEq)=>((cartprodfstin)=>((setukpairinjL2)=>((setukpairinjL)=>((setukpairinjR11)=>((setukpairinjR12)=>((setukpairinjR1)=>((upairequniteq)=>((setukpairinjR2)=>((setukpairinjR)=>![X18:$i]:(((iskpair @ X18)=>(singleton @ (dsetconstr @ (setunion @ X18) @ (^[X2:$i]:(((X18)=(kpair @ (kfst @ X18) @ X2))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), file('/export/starexec/sandbox/tmp/tmp.45u3Cojn4q/E---3.1_3416988.p', ksndsingleton)).
% 3.24/0.78 thf(cartprodmempair, axiom, ((cartprodmempair)<=>![X4:$i, X5:$i, X18:$i]:(((in @ X18 @ (cartprod @ X4 @ X5))=>(iskpair @ X18)))), file('/export/starexec/sandbox/tmp/tmp.45u3Cojn4q/E---3.1_3416988.p', cartprodmempair)).
% 3.24/0.78 thf(kpairiskpair, axiom, ((kpairiskpair)<=>![X2:$i, X3:$i]:((iskpair @ (setadjoin @ (setadjoin @ X2 @ emptyset) @ (setadjoin @ (setadjoin @ X2 @ (setadjoin @ X3 @ emptyset)) @ emptyset))))), file('/export/starexec/sandbox/tmp/tmp.45u3Cojn4q/E---3.1_3416988.p', kpairiskpair)).
% 3.24/0.78 thf(kpairp, axiom, ((kpairp)<=>![X2:$i, X3:$i]:((iskpair @ (kpair @ X2 @ X3)))), file('/export/starexec/sandbox/tmp/tmp.45u3Cojn4q/E---3.1_3416988.p', kpairp)).
% 3.24/0.78 thf(theprop, axiom, ((theprop)<=>![X21:$i]:(((singleton @ X21)=>(in @ (setunion @ X21) @ X21)))), file('/export/starexec/sandbox/tmp/tmp.45u3Cojn4q/E---3.1_3416988.p', theprop)).
% 3.24/0.78 thf(cartprodfstin, axiom, ((cartprodfstin)<=>![X4:$i, X5:$i, X18:$i]:(((in @ X18 @ (cartprod @ X4 @ X5))=>(in @ (kfst @ X18) @ X4)))), file('/export/starexec/sandbox/tmp/tmp.45u3Cojn4q/E---3.1_3416988.p', cartprodfstin)).
% 3.24/0.78 thf(setukpairinjR, axiom, ((setukpairinjR)<=>![X2:$i, X3:$i, X14:$i, X18:$i]:((((kpair @ X2 @ X3)=(kpair @ X14 @ X18))=>((X3)=(X18))))), file('/export/starexec/sandbox/tmp/tmp.45u3Cojn4q/E---3.1_3416988.p', setukpairinjR)).
% 3.24/0.78 thf(setukpairinjL, axiom, ((setukpairinjL)<=>![X2:$i, X3:$i, X14:$i, X18:$i]:((((kpair @ X2 @ X3)=(kpair @ X14 @ X18))=>((X2)=(X14))))), file('/export/starexec/sandbox/tmp/tmp.45u3Cojn4q/E---3.1_3416988.p', setukpairinjL)).
% 3.24/0.78 thf(kfstpairEq, axiom, ((kfstpairEq)<=>![X2:$i, X3:$i]:(((kfst @ (kpair @ X2 @ X3))=(X2)))), file('/export/starexec/sandbox/tmp/tmp.45u3Cojn4q/E---3.1_3416988.p', kfstpairEq)).
% 3.24/0.78 thf(cartprodmempair1, axiom, ((cartprodmempair1)<=>![X4:$i, X5:$i, X18:$i]:(((in @ X18 @ (cartprod @ X4 @ X5))=>?[X2:$i]:(((in @ X2 @ X4)&?[X3:$i]:(((in @ X3 @ X5)&((X18)=(kpair @ X2 @ X3))))))))), file('/export/starexec/sandbox/tmp/tmp.45u3Cojn4q/E---3.1_3416988.p', cartprodmempair1)).
% 3.24/0.78 thf(cartprodpairin, axiom, ((cartprodpairin)<=>![X4:$i, X5:$i, X2:$i]:(((in @ X2 @ X4)=>![X3:$i]:(((in @ X3 @ X5)=>(in @ (kpair @ X2 @ X3) @ (cartprod @ X4 @ X5))))))), file('/export/starexec/sandbox/tmp/tmp.45u3Cojn4q/E---3.1_3416988.p', cartprodpairin)).
% 3.24/0.78 thf(ubforcartprodlem3, axiom, ((ubforcartprodlem3)<=>![X4:$i, X5:$i, X2:$i]:(((in @ X2 @ X4)=>![X3:$i]:(((in @ X3 @ X5)=>(in @ (kpair @ X2 @ X3) @ (powerset @ (powerset @ (binunion @ X4 @ X5))))))))), file('/export/starexec/sandbox/tmp/tmp.45u3Cojn4q/E---3.1_3416988.p', ubforcartprodlem3)).
% 3.24/0.78 thf(kpair, axiom, ((kpair)=(^[X2:$i, X3:$i]:(setadjoin @ (setadjoin @ X2 @ emptyset) @ (setadjoin @ (setadjoin @ X2 @ (setadjoin @ X3 @ emptyset)) @ emptyset)))), file('/export/starexec/sandbox/tmp/tmp.45u3Cojn4q/E---3.1_3416988.p', kpair)).
% 3.24/0.78 thf(c_0_21, plain, ((ex1)=(^[Z0:$i, Z1:$i > $o]:((?[X82:$i]:((((in @ X82 @ (dsetconstr @ Z0 @ (^[Z2:$i]:((Z1 @ Z2))))))&(((dsetconstr @ Z0 @ (^[Z2:$i]:((Z1 @ Z2))))=(setadjoin @ X82 @ emptyset))))))))), inference(fof_simplification,[status(thm)],[ex1])).
% 3.24/0.78 thf(c_0_22, plain, ((singleton)=(^[Z0:$i]:(?[X2:$i]:((((in @ X2 @ Z0))&(((Z0)=(setadjoin @ X2 @ emptyset)))))))), inference(fof_simplification,[status(thm)],[singleton])).
% 3.24/0.78 thf(c_0_23, plain, ((ex1I2)<=>![X4:$i, X1:$i > $o]:((![X2:$i]:(((in @ X2 @ X4)=>![X3:$i]:(((in @ X3 @ X4)=>((X1 @ X2)=>((X1 @ X3)=>((X2)=(X3))))))))=>(?[X2:$i]:(((in @ X2 @ X4)&(X1 @ X2)))=>(ex1 @ X4 @ (^[Z0:$i]:((X1 @ Z0)))))))), inference(fof_simplification,[status(thm)],[ex1I2])).
% 3.24/0.78 thf(c_0_24, plain, ((ex1)=(^[Z0:$i, Z1:$i > $o]:((?[X82:$i]:((((in @ X82 @ (dsetconstr @ Z0 @ (^[Z2:$i]:((Z1 @ Z2))))))&(((dsetconstr @ Z0 @ (^[Z2:$i]:((Z1 @ Z2))))=(setadjoin @ X82 @ emptyset))))))))), inference(apply_def,[status(thm)],[c_0_21, c_0_22])).
% 3.24/0.78 thf(c_0_25, plain, ((ex1I)<=>![X4:$i, X1:$i > $o, X2:$i]:(((in @ X2 @ X4)=>((X1 @ X2)=>(![X3:$i]:(((in @ X3 @ X4)=>((X1 @ X3)=>((X3)=(X2)))))=>(ex1 @ X4 @ (^[Z0:$i]:((X1 @ Z0))))))))), inference(fof_simplification,[status(thm)],[ex1I])).
% 3.24/0.78 thf(c_0_26, plain, ((ex1E1)<=>![X4:$i, X1:$i > $o]:(((ex1 @ X4 @ (^[Z0:$i]:((X1 @ Z0))))=>?[X2:$i]:(((in @ X2 @ X4)&(X1 @ X2)))))), inference(fof_simplification,[status(thm)],[ex1E1])).
% 3.24/0.78 thf(c_0_27, plain, ((iskpair)=(^[Z0:$i]:(?[X2:$i]:((((in @ X2 @ (setunion @ Z0)))&(?[X3:$i]:((((in @ X3 @ (setunion @ Z0)))&(((Z0)=(setadjoin @ (setadjoin @ X2 @ emptyset) @ (setadjoin @ (setadjoin @ X2 @ (setadjoin @ X3 @ emptyset)) @ emptyset)))))))))))), inference(fof_simplification,[status(thm)],[iskpair])).
% 3.24/0.78 thf(c_0_28, plain, ((kfstsingleton)<=>![X18:$i]:(((iskpair @ X18)=>(singleton @ (dsetconstr @ (setunion @ X18) @ (^[Z0:$i]:((in @ (setadjoin @ Z0 @ emptyset) @ X18)))))))), inference(fof_simplification,[status(thm)],[kfstsingleton])).
% 3.24/0.78 thf(c_0_29, plain, ((singletonprop)<=>![X4:$i, X1:$i > $o]:((![X2:$i]:(((in @ X2 @ X4)=>![X3:$i]:(((in @ X3 @ X4)=>((X1 @ X2)=>((X1 @ X3)=>((X2)=(X3))))))))=>(?[X2:$i]:(((in @ X2 @ X4)&(X1 @ X2)))=>(singleton @ (dsetconstr @ X4 @ (^[Z0:$i]:((X1 @ Z0))))))))), inference(fof_simplification,[status(thm)],[singletonprop])).
% 3.24/0.78 thf(c_0_30, negated_conjecture, ~(((setextAx)=>((emptysetAx)=>((setadjoinAx)=>((powersetAx)=>((setunionAx)=>((omega0Ax)=>((omegaSAx)=>((omegaIndAx)=>((replAx)=>((foundationAx)=>((wellorderingAx)=>((descrp)=>((dsetconstrI)=>((dsetconstrEL)=>((dsetconstrER)=>((exuE1)=>((prop2setE)=>((emptysetE)=>((emptysetimpfalse)=>((notinemptyset)=>((exuE3e)=>((setext)=>((emptyI)=>((noeltsimpempty)=>((setbeta)=>((nonemptyE1)=>((nonemptyI)=>((nonemptyI1)=>((setadjoinIL)=>((emptyinunitempty)=>((setadjoinIR)=>((setadjoinE)=>((setadjoinOr)=>((setoftrueEq)=>((powersetI)=>((emptyinPowerset)=>((emptyInPowerset)=>((powersetE)=>((setunionI)=>((setunionE)=>((subPowSU)=>((exuE2)=>((nonemptyImpWitness)=>((uniqinunit)=>((notinsingleton)=>((eqinunit)=>((singletonsswitch)=>((upairsetE)=>((upairsetIL)=>((upairsetIR)=>((emptyE1)=>((vacuousDall)=>((quantDeMorgan1)=>((quantDeMorgan2)=>((quantDeMorgan3)=>((quantDeMorgan4)=>((prop2setI)=>((prop2set2propI)=>((notdexE)=>((notdallE)=>((exuI1)=>((exuI3)=>((exuI2)=>((inCongP)=>((in__Cong)=>((exuE3u)=>((exu__Cong)=>((emptyset__Cong)=>((setadjoin__Cong)=>((powerset__Cong)=>((setunion__Cong)=>((omega__Cong)=>((exuEu)=>((descr__Cong)=>((dsetconstr__Cong)=>((subsetI1)=>((eqimpsubset2)=>((eqimpsubset1)=>((subsetI2)=>((emptysetsubset)=>((subsetE)=>((subsetE2)=>((notsubsetI)=>((notequalI1)=>((notequalI2)=>((subsetRefl)=>((subsetTrans)=>((setadjoinSub)=>((setadjoinSub2)=>((subset2powerset)=>((setextsub)=>((subsetemptysetimpeq)=>((powersetI1)=>((powersetE1)=>((inPowerset)=>((powersetsubset)=>((sepInPowerset)=>((sepSubset)=>((binunionIL)=>((upairset2IR)=>((binunionIR)=>((binunionEcases)=>((binunionE)=>((binunionLsub)=>((binunionRsub)=>((binintersectI)=>((binintersectSubset5)=>((binintersectEL)=>((binintersectLsub)=>((binintersectSubset2)=>((binintersectSubset3)=>((binintersectER)=>((disjointsetsI1)=>((binintersectRsub)=>((binintersectSubset4)=>((binintersectSubset1)=>((bs114d)=>((setminusI)=>((setminusEL)=>((setminusER)=>((setminusSubset2)=>((setminusERneg)=>((setminusELneg)=>((setminusILneg)=>((setminusIRneg)=>((setminusLsub)=>((setminusSubset1)=>((symdiffE)=>((symdiffI1)=>((symdiffI2)=>((symdiffIneg1)=>((symdiffIneg2)=>((secondinupair)=>((setukpairIL)=>((setukpairIR)=>((kpairiskpair)=>((kpairp)=>((singletonsubset)=>((singletoninpowerset)=>((singletoninpowunion)=>((upairset2E)=>((upairsubunion)=>((upairinpowunion)=>((ubforcartprodlem1)=>((ubforcartprodlem2)=>((ubforcartprodlem3)=>((cartprodpairin)=>((cartprodmempair1)=>((cartprodmempair)=>((setunionE2)=>((setunionsingleton1)=>((setunionsingleton2)=>((setunionsingleton)=>((singletonprop)=>((ex1E1)=>((ex1I)=>((ex1I2)=>((singletonsuniq)=>((setukpairinjL1)=>((kfstsingleton)=>((theprop)=>((kfstpairEq)=>((cartprodfstin)=>((setukpairinjL2)=>((setukpairinjL)=>((setukpairinjR11)=>((setukpairinjR12)=>((setukpairinjR1)=>((upairequniteq)=>((setukpairinjR2)=>((setukpairinjR)=>![X18:$i]:(((iskpair @ X18)=>(singleton @ (dsetconstr @ (setunion @ X18) @ (^[X2:$i]:(((X18)=(kpair @ (kfst @ X18) @ X2)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), inference(assume_negation,[status(cth)],[ksndsingleton])).
% 3.24/0.78 thf(c_0_31, plain, ((ex1I2)=(![X4:$i, X1:$i > $o]:(((![X2:$i]:((((in @ X2 @ X4))=>(![X3:$i]:((((in @ X3 @ X4))=>((((X1 @ X2))=>((((X1 @ X3))=>(((X2)=(X3)))))))))))))=>(((?[X2:$i]:((((in @ X2 @ X4))&((X1 @ X2)))))=>((?[X85:$i]:((((in @ X85 @ (dsetconstr @ X4 @ (^[Z0:$i]:(((X1 @ Z0)))))))&(((dsetconstr @ X4 @ (^[Z0:$i]:(((X1 @ Z0)))))=(setadjoin @ X85 @ emptyset))))))))))))), inference(apply_def,[status(thm)],[c_0_23, c_0_24])).
% 3.24/0.78 thf(c_0_32, plain, ((ex1I)=(![X4:$i, X1:$i > $o, X2:$i]:((((in @ X2 @ X4))=>((((X1 @ X2))=>(((![X3:$i]:((((in @ X3 @ X4))=>((((X1 @ X3))=>(((X3)=(X2))))))))=>((?[X84:$i]:((((in @ X84 @ (dsetconstr @ X4 @ (^[Z0:$i]:(((X1 @ Z0)))))))&(((dsetconstr @ X4 @ (^[Z0:$i]:(((X1 @ Z0)))))=(setadjoin @ X84 @ emptyset))))))))))))))), inference(apply_def,[status(thm)],[c_0_25, c_0_24])).
% 3.24/0.78 thf(c_0_33, plain, ((ex1E1)=(![X4:$i, X1:$i > $o]:((((?[X83:$i]:((((in @ X83 @ (dsetconstr @ X4 @ (^[Z0:$i]:(((X1 @ Z0)))))))&(((dsetconstr @ X4 @ (^[Z0:$i]:(((X1 @ Z0)))))=(setadjoin @ X83 @ emptyset)))))))=>(?[X2:$i]:((((in @ X2 @ X4))&((X1 @ X2))))))))), inference(apply_def,[status(thm)],[c_0_26, c_0_24])).
% 3.24/0.78 thf(c_0_34, axiom, ((cartprodmempair)=(![X4:$i, X5:$i, X18:$i]:((((in @ X18 @ (cartprod @ X4 @ X5)))=>((?[X79:$i]:((((in @ X79 @ (setunion @ X18)))&(?[X80:$i]:((((in @ X80 @ (setunion @ X18)))&(((X18)=(setadjoin @ (setadjoin @ X79 @ emptyset) @ (setadjoin @ (setadjoin @ X79 @ (setadjoin @ X80 @ emptyset)) @ emptyset))))))))))))))), inference(apply_def,[status(thm)],[cartprodmempair, c_0_27])).
% 3.24/0.78 thf(c_0_35, axiom, ((kpairiskpair)=(![X2:$i, X3:$i]:((?[X75:$i]:((((in @ X75 @ (setunion @ (setadjoin @ (setadjoin @ X2 @ emptyset) @ (setadjoin @ (setadjoin @ X2 @ (setadjoin @ X3 @ emptyset)) @ emptyset)))))&(?[X76:$i]:((((in @ X76 @ (setunion @ (setadjoin @ (setadjoin @ X2 @ emptyset) @ (setadjoin @ (setadjoin @ X2 @ (setadjoin @ X3 @ emptyset)) @ emptyset)))))&(((setadjoin @ (setadjoin @ X2 @ emptyset) @ (setadjoin @ (setadjoin @ X2 @ (setadjoin @ X3 @ emptyset)) @ emptyset))=(setadjoin @ (setadjoin @ X75 @ emptyset) @ (setadjoin @ (setadjoin @ X75 @ (setadjoin @ X76 @ emptyset)) @ emptyset))))))))))))), inference(apply_def,[status(thm)],[kpairiskpair, c_0_27])).
% 3.24/0.78 thf(c_0_36, axiom, ((kpairp)=(![X2:$i, X3:$i]:((?[X77:$i]:((((in @ X77 @ (setunion @ (kpair @ X2 @ X3))))&(?[X78:$i]:((((in @ X78 @ (setunion @ (kpair @ X2 @ X3))))&(((kpair @ X2 @ X3)=(setadjoin @ (setadjoin @ X77 @ emptyset) @ (setadjoin @ (setadjoin @ X77 @ (setadjoin @ X78 @ emptyset)) @ emptyset))))))))))))), inference(apply_def,[status(thm)],[kpairp, c_0_27])).
% 3.24/0.78 thf(c_0_37, axiom, ((theprop)=(![X21:$i]:((((?[X89:$i]:((((in @ X89 @ X21))&(((X21)=(setadjoin @ X89 @ emptyset)))))))=>((in @ (setunion @ X21) @ X21)))))), inference(apply_def,[status(thm)],[theprop, c_0_22])).
% 3.24/0.78 thf(c_0_38, plain, ((kfstsingleton)=(![X18:$i]:((((?[X86:$i]:((((in @ X86 @ (setunion @ X18)))&(?[X87:$i]:((((in @ X87 @ (setunion @ X18)))&(((X18)=(setadjoin @ (setadjoin @ X86 @ emptyset) @ (setadjoin @ (setadjoin @ X86 @ (setadjoin @ X87 @ emptyset)) @ emptyset)))))))))))=>((?[X88:$i]:((((in @ X88 @ (dsetconstr @ (setunion @ X18) @ (^[Z0:$i]:((in @ (setadjoin @ Z0 @ emptyset) @ X18))))))&(((dsetconstr @ (setunion @ X18) @ (^[Z0:$i]:((in @ (setadjoin @ Z0 @ emptyset) @ X18))))=(setadjoin @ X88 @ emptyset))))))))))), inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[c_0_28, c_0_27]), c_0_22])).
% 3.24/0.78 thf(c_0_39, plain, ((singletonprop)=(![X4:$i, X1:$i > $o]:(((![X2:$i]:((((in @ X2 @ X4))=>(![X3:$i]:((((in @ X3 @ X4))=>((((X1 @ X2))=>((((X1 @ X3))=>(((X2)=(X3)))))))))))))=>(((?[X2:$i]:((((in @ X2 @ X4))&((X1 @ X2)))))=>((?[X81:$i]:((((in @ X81 @ (dsetconstr @ X4 @ (^[Z0:$i]:((X1 @ Z0))))))&(((dsetconstr @ X4 @ (^[Z0:$i]:((X1 @ Z0))))=(setadjoin @ X81 @ emptyset))))))))))))), inference(apply_def,[status(thm)],[c_0_29, c_0_22])).
% 3.24/0.78 thf(c_0_40, negated_conjecture, ~(((setextAx)=>((emptysetAx)=>((setadjoinAx)=>((powersetAx)=>((setunionAx)=>((omega0Ax)=>((omegaSAx)=>((omegaIndAx)=>((replAx)=>((foundationAx)=>((wellorderingAx)=>((descrp)=>((dsetconstrI)=>((dsetconstrEL)=>((dsetconstrER)=>((exuE1)=>((prop2setE)=>((emptysetE)=>((emptysetimpfalse)=>((notinemptyset)=>((exuE3e)=>((setext)=>((emptyI)=>((noeltsimpempty)=>((setbeta)=>((nonemptyE1)=>((nonemptyI)=>((nonemptyI1)=>((setadjoinIL)=>((emptyinunitempty)=>((setadjoinIR)=>((setadjoinE)=>((setadjoinOr)=>((setoftrueEq)=>((powersetI)=>((emptyinPowerset)=>((emptyInPowerset)=>((powersetE)=>((setunionI)=>((setunionE)=>((subPowSU)=>((exuE2)=>((nonemptyImpWitness)=>((uniqinunit)=>((notinsingleton)=>((eqinunit)=>((singletonsswitch)=>((upairsetE)=>((upairsetIL)=>((upairsetIR)=>((emptyE1)=>((vacuousDall)=>((quantDeMorgan1)=>((quantDeMorgan2)=>((quantDeMorgan3)=>((quantDeMorgan4)=>((prop2setI)=>((prop2set2propI)=>((notdexE)=>((notdallE)=>((exuI1)=>((exuI3)=>((exuI2)=>((inCongP)=>((in__Cong)=>((exuE3u)=>((exu__Cong)=>((emptyset__Cong)=>((setadjoin__Cong)=>((powerset__Cong)=>((setunion__Cong)=>((omega__Cong)=>((exuEu)=>((descr__Cong)=>((dsetconstr__Cong)=>((subsetI1)=>((eqimpsubset2)=>((eqimpsubset1)=>((subsetI2)=>((emptysetsubset)=>((subsetE)=>((subsetE2)=>((notsubsetI)=>((notequalI1)=>((notequalI2)=>((subsetRefl)=>((subsetTrans)=>((setadjoinSub)=>((setadjoinSub2)=>((subset2powerset)=>((setextsub)=>((subsetemptysetimpeq)=>((powersetI1)=>((powersetE1)=>((inPowerset)=>((powersetsubset)=>((sepInPowerset)=>((sepSubset)=>((binunionIL)=>((upairset2IR)=>((binunionIR)=>((binunionEcases)=>((binunionE)=>((binunionLsub)=>((binunionRsub)=>((binintersectI)=>((binintersectSubset5)=>((binintersectEL)=>((binintersectLsub)=>((binintersectSubset2)=>((binintersectSubset3)=>((binintersectER)=>((disjointsetsI1)=>((binintersectRsub)=>((binintersectSubset4)=>((binintersectSubset1)=>((bs114d)=>((setminusI)=>((setminusEL)=>((setminusER)=>((setminusSubset2)=>((setminusERneg)=>((setminusELneg)=>((setminusILneg)=>((setminusIRneg)=>((setminusLsub)=>((setminusSubset1)=>((symdiffE)=>((symdiffI1)=>((symdiffI2)=>((symdiffIneg1)=>((symdiffIneg2)=>((secondinupair)=>((setukpairIL)=>((setukpairIR)=>(![X90:$i, X91:$i]:(?[X92:$i]:(((in @ X92 @ (setunion @ (setadjoin @ (setadjoin @ X90 @ emptyset) @ (setadjoin @ (setadjoin @ X90 @ (setadjoin @ X91 @ emptyset)) @ emptyset))))&?[X93:$i]:(((in @ X93 @ (setunion @ (setadjoin @ (setadjoin @ X90 @ emptyset) @ (setadjoin @ (setadjoin @ X90 @ (setadjoin @ X91 @ emptyset)) @ emptyset))))&((setadjoin @ (setadjoin @ X90 @ emptyset) @ (setadjoin @ (setadjoin @ X90 @ (setadjoin @ X91 @ emptyset)) @ emptyset))=(setadjoin @ (setadjoin @ X92 @ emptyset) @ (setadjoin @ (setadjoin @ X92 @ (setadjoin @ X93 @ emptyset)) @ emptyset))))))))=>(![X94:$i, X95:$i]:(?[X96:$i]:(((in @ X96 @ (setunion @ (kpair @ X94 @ X95)))&?[X97:$i]:(((in @ X97 @ (setunion @ (kpair @ X94 @ X95)))&((kpair @ X94 @ X95)=(setadjoin @ (setadjoin @ X96 @ emptyset) @ (setadjoin @ (setadjoin @ X96 @ (setadjoin @ X97 @ emptyset)) @ emptyset))))))))=>((singletonsubset)=>((singletoninpowerset)=>((singletoninpowunion)=>((upairset2E)=>((upairsubunion)=>((upairinpowunion)=>((ubforcartprodlem1)=>((ubforcartprodlem2)=>(![X98:$i, X99:$i, X100:$i]:(((in @ X100 @ X98)=>![X101:$i]:(((in @ X101 @ X99)=>(in @ (kpair @ X100 @ X101) @ (powerset @ (powerset @ (binunion @ X98 @ X99))))))))=>(![X102:$i, X103:$i, X104:$i]:(((in @ X104 @ X102)=>![X105:$i]:(((in @ X105 @ X103)=>(in @ (kpair @ X104 @ X105) @ (cartprod @ X102 @ X103))))))=>(![X106:$i, X107:$i, X108:$i]:(((in @ X108 @ (cartprod @ X106 @ X107))=>?[X109:$i]:(((in @ X109 @ X106)&?[X110:$i]:(((in @ X110 @ X107)&((X108)=(kpair @ X109 @ X110))))))))=>(![X111:$i, X112:$i, X113:$i]:(((in @ X113 @ (cartprod @ X111 @ X112))=>?[X114:$i]:(((in @ X114 @ (setunion @ X113))&?[X115:$i]:(((in @ X115 @ (setunion @ X113))&((X113)=(setadjoin @ (setadjoin @ X114 @ emptyset) @ (setadjoin @ (setadjoin @ X114 @ (setadjoin @ X115 @ emptyset)) @ emptyset)))))))))=>((setunionE2)=>((setunionsingleton1)=>((setunionsingleton2)=>((setunionsingleton)=>(![X116:$i, X117:$i > $o]:((![X118:$i]:(((in @ X118 @ X116)=>![X119:$i]:(((in @ X119 @ X116)=>((X117 @ X118)=>((X117 @ X119)=>((X118)=(X119))))))))=>(?[X120:$i]:(((in @ X120 @ X116)&(X117 @ X120)))=>?[X121:$i]:(((in @ X121 @ (dsetconstr @ X116 @ X117))&((dsetconstr @ X116 @ X117)=(setadjoin @ X121 @ emptyset)))))))=>(![X122:$i, X123:$i > $o]:((?[X124:$i]:(((in @ X124 @ (dsetconstr @ X122 @ X123))&((dsetconstr @ X122 @ X123)=(setadjoin @ X124 @ emptyset))))=>?[X125:$i]:(((in @ X125 @ X122)&(X123 @ X125)))))=>(![X126:$i, X127:$i > $o, X128:$i]:(((in @ X128 @ X126)=>((X127 @ X128)=>(![X129:$i]:(((in @ X129 @ X126)=>((X127 @ X129)=>((X129)=(X128)))))=>?[X130:$i]:(((in @ X130 @ (dsetconstr @ X126 @ X127))&((dsetconstr @ X126 @ X127)=(setadjoin @ X130 @ emptyset))))))))=>(![X131:$i, X132:$i > $o]:((![X133:$i]:(((in @ X133 @ X131)=>![X134:$i]:(((in @ X134 @ X131)=>((X132 @ X133)=>((X132 @ X134)=>((X133)=(X134))))))))=>(?[X135:$i]:(((in @ X135 @ X131)&(X132 @ X135)))=>?[X136:$i]:(((in @ X136 @ (dsetconstr @ X131 @ X132))&((dsetconstr @ X131 @ X132)=(setadjoin @ X136 @ emptyset)))))))=>((singletonsuniq)=>((setukpairinjL1)=>(![X137:$i]:((?[X138:$i]:(((in @ X138 @ (setunion @ X137))&?[X139:$i]:(((in @ X139 @ (setunion @ X137))&((X137)=(setadjoin @ (setadjoin @ X138 @ emptyset) @ (setadjoin @ (setadjoin @ X138 @ (setadjoin @ X139 @ emptyset)) @ emptyset)))))))=>?[X140:$i]:(((in @ X140 @ (dsetconstr @ (setunion @ X137) @ (^[Z0:$i]:((in @ (setadjoin @ Z0 @ emptyset) @ X137)))))&((dsetconstr @ (setunion @ X137) @ (^[Z0:$i]:((in @ (setadjoin @ Z0 @ emptyset) @ X137))))=(setadjoin @ X140 @ emptyset))))))=>(![X141:$i]:((?[X142:$i]:(((in @ X142 @ X141)&((X141)=(setadjoin @ X142 @ emptyset))))=>(in @ (setunion @ X141) @ X141)))=>(![X143:$i, X144:$i]:(((kfst @ (kpair @ X143 @ X144))=(X143)))=>(![X145:$i, X146:$i, X147:$i]:(((in @ X147 @ (cartprod @ X145 @ X146))=>(in @ (kfst @ X147) @ X145)))=>((setukpairinjL2)=>(![X148:$i, X149:$i, X150:$i, X151:$i]:((((kpair @ X148 @ X149)=(kpair @ X150 @ X151))=>((X148)=(X150))))=>((setukpairinjR11)=>((setukpairinjR12)=>((setukpairinjR1)=>((upairequniteq)=>((setukpairinjR2)=>(![X152:$i, X153:$i, X154:$i, X155:$i]:((((kpair @ X152 @ X153)=(kpair @ X154 @ X155))=>((X153)=(X155))))=>![X18:$i]:((?[X156:$i]:(((in @ X156 @ (setunion @ X18))&?[X157:$i]:(((in @ X157 @ (setunion @ X18))&((X18)=(setadjoin @ (setadjoin @ X156 @ emptyset) @ (setadjoin @ (setadjoin @ X156 @ (setadjoin @ X157 @ emptyset)) @ emptyset)))))))=>?[X158:$i]:(((in @ X158 @ (dsetconstr @ (setunion @ X18) @ (^[Z0:$i]:(((X18)=(kpair @ (kfst @ X18) @ Z0))))))&((dsetconstr @ (setunion @ X18) @ (^[Z0:$i]:(((X18)=(kpair @ (kfst @ X18) @ Z0)))))=(setadjoin @ X158 @ emptyset)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), 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(fof_simplification,[status(thm)],[c_0_30]), c_0_31]), c_0_32]), c_0_33]), c_0_34]), c_0_35]), c_0_27]), cartprodfstin]), setukpairinjR]), setukpairinjL]), kfstpairEq]), cartprodmempair1]), cartprodpairin]), ubforcartprodlem3]), c_0_36]), c_0_37]), c_0_38]), c_0_39]), c_0_22])])).
% 3.24/0.78 thf(c_0_41, plain, ![X159:$i, X160:$i]:(((kpair @ X159 @ X160)=(setadjoin @ (setadjoin @ X159 @ emptyset) @ (setadjoin @ (setadjoin @ X159 @ (setadjoin @ X160 @ emptyset)) @ emptyset)))), inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[kpair])])).
% 3.24/0.78 thf(c_0_42, negated_conjecture, ![X161:$i, X162:$i, X165:$i, X166:$i, X169:$i, X170:$i, X171:$i, X172:$i, X173:$i, X174:$i, X175:$i, X176:$i, X177:$i, X178:$i, X179:$i, X182:$i, X183:$i, X184:$i, X187:$i, X188:$i > $o, X191:$i, X193:$i, X194:$i > $o, X195:$i, X197:$i, X198:$i > $o, X199:$i, X202:$i, X203:$i > $o, X206:$i, X208:$i, X209:$i, X210:$i, X212:$i, X213:$i, X214:$i, X215:$i, X216:$i, X217:$i, X218:$i, X219:$i, X220:$i, X221:$i, X222:$i, X223:$i, X224:$i, X225:$i, X226:$i, X230:$i]:(((setextAx)&((emptysetAx)&((setadjoinAx)&((powersetAx)&((setunionAx)&((omega0Ax)&((omegaSAx)&((omegaIndAx)&((replAx)&((foundationAx)&((wellorderingAx)&((descrp)&((dsetconstrI)&((dsetconstrEL)&((dsetconstrER)&((exuE1)&((prop2setE)&((emptysetE)&((emptysetimpfalse)&((notinemptyset)&((exuE3e)&((setext)&((emptyI)&((noeltsimpempty)&((setbeta)&((nonemptyE1)&((nonemptyI)&((nonemptyI1)&((setadjoinIL)&((emptyinunitempty)&((setadjoinIR)&((setadjoinE)&((setadjoinOr)&((setoftrueEq)&((powersetI)&((emptyinPowerset)&((emptyInPowerset)&((powersetE)&((setunionI)&((setunionE)&((subPowSU)&((exuE2)&((nonemptyImpWitness)&((uniqinunit)&((notinsingleton)&((eqinunit)&((singletonsswitch)&((upairsetE)&((upairsetIL)&((upairsetIR)&((emptyE1)&((vacuousDall)&((quantDeMorgan1)&((quantDeMorgan2)&((quantDeMorgan3)&((quantDeMorgan4)&((prop2setI)&((prop2set2propI)&((notdexE)&((notdallE)&((exuI1)&((exuI3)&((exuI2)&((inCongP)&((in__Cong)&((exuE3u)&((exu__Cong)&((emptyset__Cong)&((setadjoin__Cong)&((powerset__Cong)&((setunion__Cong)&((omega__Cong)&((exuEu)&((descr__Cong)&((dsetconstr__Cong)&((subsetI1)&((eqimpsubset2)&((eqimpsubset1)&((subsetI2)&((emptysetsubset)&((subsetE)&((subsetE2)&((notsubsetI)&((notequalI1)&((notequalI2)&((subsetRefl)&((subsetTrans)&((setadjoinSub)&((setadjoinSub2)&((subset2powerset)&((setextsub)&((subsetemptysetimpeq)&((powersetI1)&((powersetE1)&((inPowerset)&((powersetsubset)&((sepInPowerset)&((sepSubset)&((binunionIL)&((upairset2IR)&((binunionIR)&((binunionEcases)&((binunionE)&((binunionLsub)&((binunionRsub)&((binintersectI)&((binintersectSubset5)&((binintersectEL)&((binintersectLsub)&((binintersectSubset2)&((binintersectSubset3)&((binintersectER)&((disjointsetsI1)&((binintersectRsub)&((binintersectSubset4)&((binintersectSubset1)&((bs114d)&((setminusI)&((setminusEL)&((setminusER)&((setminusSubset2)&((setminusERneg)&((setminusELneg)&((setminusILneg)&((setminusIRneg)&((setminusLsub)&((setminusSubset1)&((symdiffE)&((symdiffI1)&((symdiffI2)&((symdiffIneg1)&((symdiffIneg2)&((secondinupair)&((setukpairIL)&((setukpairIR)&(((in @ (esk1_2 @ X161 @ X162) @ (setunion @ (setadjoin @ (setadjoin @ X161 @ emptyset) @ (setadjoin @ (setadjoin @ X161 @ (setadjoin @ X162 @ emptyset)) @ emptyset))))&((in @ (esk2_2 @ X161 @ X162) @ (setunion @ (setadjoin @ (setadjoin @ X161 @ emptyset) @ (setadjoin @ (setadjoin @ X161 @ (setadjoin @ X162 @ emptyset)) @ emptyset))))&((setadjoin @ (setadjoin @ X161 @ emptyset) @ (setadjoin @ (setadjoin @ X161 @ (setadjoin @ X162 @ emptyset)) @ emptyset))=(setadjoin @ (setadjoin @ (esk1_2 @ X161 @ X162) @ emptyset) @ (setadjoin @ (setadjoin @ (esk1_2 @ X161 @ X162) @ (setadjoin @ (esk2_2 @ X161 @ X162) @ emptyset)) @ emptyset)))))&(((in @ (esk3_2 @ X165 @ X166) @ (setunion @ (kpair @ X165 @ X166)))&((in @ (esk4_2 @ X165 @ X166) @ (setunion @ (kpair @ X165 @ X166)))&((kpair @ X165 @ X166)=(setadjoin @ (setadjoin @ (esk3_2 @ X165 @ X166) @ emptyset) @ (setadjoin @ (setadjoin @ (esk3_2 @ X165 @ X166) @ (setadjoin @ (esk4_2 @ X165 @ X166) @ emptyset)) @ emptyset)))))&((singletonsubset)&((singletoninpowerset)&((singletoninpowunion)&((upairset2E)&((upairsubunion)&((upairinpowunion)&((ubforcartprodlem1)&((ubforcartprodlem2)&((~(in @ X171 @ X169)|(~(in @ X172 @ X170)|(in @ (kpair @ X171 @ X172) @ (powerset @ (powerset @ (binunion @ X169 @ X170))))))&((~(in @ X175 @ X173)|(~(in @ X176 @ X174)|(in @ (kpair @ X175 @ X176) @ (cartprod @ X173 @ X174))))&((((in @ (esk5_3 @ X177 @ X178 @ X179) @ X177)|~(in @ X179 @ (cartprod @ X177 @ X178)))&(((in @ (esk6_3 @ X177 @ X178 @ X179) @ X178)|~(in @ X179 @ (cartprod @ X177 @ X178)))&(((X179)=(kpair @ (esk5_3 @ X177 @ X178 @ X179) @ (esk6_3 @ X177 @ X178 @ X179)))|~(in @ X179 @ (cartprod @ X177 @ X178)))))&((((in @ (esk7_3 @ X182 @ X183 @ X184) @ (setunion @ X184))|~(in @ X184 @ (cartprod @ X182 @ X183)))&(((in @ (esk8_3 @ X182 @ X183 @ X184) @ (setunion @ X184))|~(in @ X184 @ (cartprod @ X182 @ X183)))&(((X184)=(setadjoin @ (setadjoin @ (esk7_3 @ X182 @ X183 @ X184) @ emptyset) @ (setadjoin @ (setadjoin @ (esk7_3 @ X182 @ X183 @ X184) @ (setadjoin @ (esk8_3 @ X182 @ X183 @ X184) @ emptyset)) @ emptyset)))|~(in @ X184 @ (cartprod @ X182 @ X183)))))&((setunionE2)&((setunionsingleton1)&((setunionsingleton2)&((setunionsingleton)&(((((in @ (esk11_2 @ X187 @ X188) @ (dsetconstr @ X187 @ X188))|(~(in @ X191 @ X187)|~(X188 @ X191))|(in @ (esk9_2 @ X187 @ X188) @ X187))&(((dsetconstr @ X187 @ X188)=(setadjoin @ (esk11_2 @ X187 @ X188) @ emptyset))|(~(in @ X191 @ X187)|~(X188 @ X191))|(in @ (esk9_2 @ X187 @ X188) @ X187)))&((((in @ (esk11_2 @ X187 @ X188) @ (dsetconstr @ X187 @ X188))|(~(in @ X191 @ X187)|~(X188 @ X191))|(in @ (esk10_2 @ X187 @ X188) @ X187))&(((dsetconstr @ X187 @ X188)=(setadjoin @ (esk11_2 @ X187 @ X188) @ emptyset))|(~(in @ X191 @ X187)|~(X188 @ X191))|(in @ (esk10_2 @ X187 @ X188) @ X187)))&((((in @ (esk11_2 @ X187 @ X188) @ (dsetconstr @ X187 @ X188))|(~(in @ X191 @ X187)|~(X188 @ X191))|(X188 @ (esk9_2 @ X187 @ X188)))&(((dsetconstr @ X187 @ X188)=(setadjoin @ (esk11_2 @ X187 @ X188) @ emptyset))|(~(in @ X191 @ X187)|~(X188 @ X191))|(X188 @ (esk9_2 @ X187 @ X188))))&((((in @ (esk11_2 @ X187 @ X188) @ (dsetconstr @ X187 @ X188))|(~(in @ X191 @ X187)|~(X188 @ X191))|(X188 @ (esk10_2 @ X187 @ X188)))&(((dsetconstr @ X187 @ X188)=(setadjoin @ (esk11_2 @ X187 @ X188) @ emptyset))|(~(in @ X191 @ X187)|~(X188 @ X191))|(X188 @ (esk10_2 @ X187 @ X188))))&(((in @ (esk11_2 @ X187 @ X188) @ (dsetconstr @ X187 @ X188))|(~(in @ X191 @ X187)|~(X188 @ X191))|((esk9_2 @ X187 @ X188)!=(esk10_2 @ X187 @ X188)))&(((dsetconstr @ X187 @ X188)=(setadjoin @ (esk11_2 @ X187 @ X188) @ emptyset))|(~(in @ X191 @ X187)|~(X188 @ X191))|((esk9_2 @ X187 @ X188)!=(esk10_2 @ X187 @ X188))))))))&((((in @ (esk12_2 @ X193 @ X194) @ X193)|(~(in @ X195 @ (dsetconstr @ X193 @ X194))|((dsetconstr @ X193 @ X194)!=(setadjoin @ X195 @ emptyset))))&((X194 @ (esk12_2 @ X193 @ X194))|(~(in @ X195 @ (dsetconstr @ X193 @ X194))|((dsetconstr @ X193 @ X194)!=(setadjoin @ X195 @ emptyset)))))&(((((in @ (esk14_3 @ X197 @ X198 @ X199) @ (dsetconstr @ X197 @ X198))|(in @ (esk13_3 @ X197 @ X198 @ X199) @ X197)|~(X198 @ X199)|~(in @ X199 @ X197))&(((dsetconstr @ X197 @ X198)=(setadjoin @ (esk14_3 @ X197 @ X198 @ X199) @ emptyset))|(in @ (esk13_3 @ X197 @ X198 @ X199) @ X197)|~(X198 @ X199)|~(in @ X199 @ X197)))&((((in @ (esk14_3 @ X197 @ X198 @ X199) @ (dsetconstr @ X197 @ X198))|(X198 @ (esk13_3 @ X197 @ X198 @ X199))|~(X198 @ X199)|~(in @ X199 @ X197))&(((dsetconstr @ X197 @ X198)=(setadjoin @ (esk14_3 @ X197 @ X198 @ X199) @ emptyset))|(X198 @ (esk13_3 @ X197 @ X198 @ X199))|~(X198 @ X199)|~(in @ X199 @ X197)))&(((in @ (esk14_3 @ X197 @ X198 @ X199) @ (dsetconstr @ X197 @ X198))|((esk13_3 @ X197 @ X198 @ X199)!=(X199))|~(X198 @ X199)|~(in @ X199 @ X197))&(((dsetconstr @ X197 @ X198)=(setadjoin @ (esk14_3 @ X197 @ X198 @ X199) @ emptyset))|((esk13_3 @ X197 @ X198 @ X199)!=(X199))|~(X198 @ X199)|~(in @ X199 @ X197)))))&(((((in @ (esk17_2 @ X202 @ X203) @ (dsetconstr @ X202 @ X203))|(~(in @ X206 @ X202)|~(X203 @ X206))|(in @ (esk15_2 @ X202 @ X203) @ X202))&(((dsetconstr @ X202 @ X203)=(setadjoin @ (esk17_2 @ X202 @ X203) @ emptyset))|(~(in @ X206 @ X202)|~(X203 @ X206))|(in @ (esk15_2 @ X202 @ X203) @ X202)))&((((in @ (esk17_2 @ X202 @ X203) @ (dsetconstr @ X202 @ X203))|(~(in @ X206 @ X202)|~(X203 @ X206))|(in @ (esk16_2 @ X202 @ X203) @ X202))&(((dsetconstr @ X202 @ X203)=(setadjoin @ (esk17_2 @ X202 @ X203) @ emptyset))|(~(in @ X206 @ X202)|~(X203 @ X206))|(in @ (esk16_2 @ X202 @ X203) @ X202)))&((((in @ (esk17_2 @ X202 @ X203) @ (dsetconstr @ X202 @ X203))|(~(in @ X206 @ X202)|~(X203 @ X206))|(X203 @ (esk15_2 @ X202 @ X203)))&(((dsetconstr @ X202 @ X203)=(setadjoin @ (esk17_2 @ X202 @ X203) @ emptyset))|(~(in @ X206 @ X202)|~(X203 @ X206))|(X203 @ (esk15_2 @ X202 @ X203))))&((((in @ (esk17_2 @ X202 @ X203) @ (dsetconstr @ X202 @ X203))|(~(in @ X206 @ X202)|~(X203 @ X206))|(X203 @ (esk16_2 @ X202 @ X203)))&(((dsetconstr @ X202 @ X203)=(setadjoin @ (esk17_2 @ X202 @ X203) @ emptyset))|(~(in @ X206 @ X202)|~(X203 @ X206))|(X203 @ (esk16_2 @ X202 @ X203))))&(((in @ (esk17_2 @ X202 @ X203) @ (dsetconstr @ X202 @ X203))|(~(in @ X206 @ X202)|~(X203 @ X206))|((esk15_2 @ X202 @ X203)!=(esk16_2 @ X202 @ X203)))&(((dsetconstr @ X202 @ X203)=(setadjoin @ (esk17_2 @ X202 @ X203) @ emptyset))|(~(in @ X206 @ X202)|~(X203 @ X206))|((esk15_2 @ X202 @ X203)!=(esk16_2 @ X202 @ X203))))))))&((singletonsuniq)&((setukpairinjL1)&((((in @ (esk18_1 @ X208) @ (dsetconstr @ (setunion @ X208) @ (^[Z0:$i]:((in @ (setadjoin @ Z0 @ emptyset) @ X208)))))|(~(in @ X209 @ (setunion @ X208))|(~(in @ X210 @ (setunion @ X208))|((X208)!=(setadjoin @ (setadjoin @ X209 @ emptyset) @ (setadjoin @ (setadjoin @ X209 @ (setadjoin @ X210 @ emptyset)) @ emptyset))))))&(((dsetconstr @ (setunion @ X208) @ (^[Z0:$i]:((in @ (setadjoin @ Z0 @ emptyset) @ X208))))=(setadjoin @ (esk18_1 @ X208) @ emptyset))|(~(in @ X209 @ (setunion @ X208))|(~(in @ X210 @ (setunion @ X208))|((X208)!=(setadjoin @ (setadjoin @ X209 @ emptyset) @ (setadjoin @ (setadjoin @ X209 @ (setadjoin @ X210 @ emptyset)) @ emptyset)))))))&((~(in @ X213 @ X212)|((X212)!=(setadjoin @ X213 @ emptyset))|(in @ (setunion @ X212) @ X212))&(((kfst @ (kpair @ X214 @ X215))=(X214))&((~(in @ X218 @ (cartprod @ X216 @ X217))|(in @ (kfst @ X218) @ X216))&((setukpairinjL2)&((((kpair @ X219 @ X220)!=(kpair @ X221 @ X222))|((X219)=(X221)))&((setukpairinjR11)&((setukpairinjR12)&((setukpairinjR1)&((upairequniteq)&((setukpairinjR2)&((((kpair @ X223 @ X224)!=(kpair @ X225 @ X226))|((X224)=(X226)))&(((in @ esk20_0 @ (setunion @ esk19_0))&((in @ esk21_0 @ (setunion @ esk19_0))&((esk19_0)=(setadjoin @ (setadjoin @ esk20_0 @ emptyset) @ (setadjoin @ (setadjoin @ esk20_0 @ (setadjoin @ esk21_0 @ emptyset)) @ emptyset)))))&(~(in @ X230 @ (dsetconstr @ (setunion @ esk19_0) @ (^[Z0:$i]:(((esk19_0)=(kpair @ (kfst @ esk19_0) @ Z0))))))|((dsetconstr @ (setunion @ esk19_0) @ (^[Z0:$i]:(((esk19_0)=(kpair @ (kfst @ esk19_0) @ Z0)))))!=(setadjoin @ X230 @ emptyset)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_40])])])])])])).
% 3.24/0.78 thf(c_0_43, plain, ![X231:$i, X232:$i]:(((kpair @ X231 @ X232)=(setadjoin @ (setadjoin @ X231 @ emptyset) @ (setadjoin @ (setadjoin @ X231 @ (setadjoin @ X232 @ emptyset)) @ emptyset)))), inference(variable_rename,[status(thm)],[c_0_41])).
% 3.24/0.78 thf(c_0_44, negated_conjecture, ((esk19_0)=(setadjoin @ (setadjoin @ esk20_0 @ emptyset) @ (setadjoin @ (setadjoin @ esk20_0 @ (setadjoin @ esk21_0 @ emptyset)) @ emptyset))), inference(split_conjunct,[status(thm)],[c_0_42])).
% 3.24/0.78 thf(c_0_45, plain, ![X2:$i, X3:$i]:(((kpair @ X2 @ X3)=(setadjoin @ (setadjoin @ X2 @ emptyset) @ (setadjoin @ (setadjoin @ X2 @ (setadjoin @ X3 @ emptyset)) @ emptyset)))), inference(split_conjunct,[status(thm)],[c_0_43])).
% 3.24/0.78 thf(c_0_46, plain, ![X239:$i]:(((~(epred1_0 @ X239)|((esk19_0)=(kpair @ (kfst @ esk19_0) @ X239)))&(((esk19_0)!=(kpair @ (kfst @ esk19_0) @ X239))|(epred1_0 @ X239)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[])])])).
% 3.24/0.78 thf(c_0_47, negated_conjecture, ![X3:$i, X2:$i]:(((kfst @ (kpair @ X2 @ X3))=(X2))), inference(split_conjunct,[status(thm)],[c_0_42])).
% 3.24/0.78 thf(c_0_48, negated_conjecture, ((kpair @ esk20_0 @ esk21_0)=(esk19_0)), inference(rw,[status(thm)],[c_0_44, c_0_45])).
% 3.24/0.78 thf(c_0_49, plain, ![X233:$i]:(((epred1_0 @ X233)<=>((esk19_0)=(kpair @ (kfst @ esk19_0) @ X233)))), introduced(definition)).
% 3.24/0.78 thf(c_0_50, plain, ![X2:$i]:(((epred1_0 @ X2)|((esk19_0)!=(kpair @ (kfst @ esk19_0) @ X2)))), inference(split_conjunct,[status(thm)],[c_0_46])).
% 3.24/0.78 thf(c_0_51, negated_conjecture, ((kfst @ esk19_0)=(esk20_0)), inference(spm,[status(thm)],[c_0_47, c_0_48])).
% 3.24/0.78 thf(c_0_52, negated_conjecture, ![X2:$i, X3:$i, X4:$i, X5:$i]:((((X3)=(X5))|((kpair @ X2 @ X3)!=(kpair @ X4 @ X5)))), inference(split_conjunct,[status(thm)],[c_0_42])).
% 3.24/0.78 thf(c_0_53, plain, ![X2:$i]:((((esk19_0)=(kpair @ (kfst @ esk19_0) @ X2))|~((epred1_0 @ X2)))), inference(split_conjunct,[status(thm)],[c_0_46])).
% 3.24/0.78 thf(c_0_54, negated_conjecture, ![X2:$i]:((~((((in @ X2 @ (dsetconstr @ (setunion @ esk19_0) @ epred1_0)))=(($true))))|((dsetconstr @ (setunion @ esk19_0) @ epred1_0)!=(setadjoin @ X2 @ emptyset)))), inference(lift_lambdas,[status(thm)],[inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_42]), c_0_49]), c_0_49])).
% 3.24/0.78 thf(c_0_55, negated_conjecture, ![X1:$i > $o, X2:$i, X3:$i]:(((in @ (esk11_2 @ X2 @ X1) @ (dsetconstr @ X2 @ X1))|(X1 @ (esk10_2 @ X2 @ X1))|~((in @ X3 @ X2))|~((X1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_42])).
% 3.24/0.78 thf(c_0_56, negated_conjecture, (in @ esk21_0 @ (setunion @ esk19_0)), inference(split_conjunct,[status(thm)],[c_0_42])).
% 3.24/0.78 thf(c_0_57, plain, ![X2:$i]:(((epred1_0 @ X2)|((kpair @ esk20_0 @ X2)!=(esk19_0)))), inference(rw,[status(thm)],[c_0_50, c_0_51])).
% 3.24/0.78 thf(c_0_58, plain, ![X2:$i, X4:$i, X3:$i]:((((X2)=(X3))|((kpair @ X4 @ X2)!=(esk19_0))|~((epred1_0 @ X3)))), inference(spm,[status(thm)],[c_0_52, c_0_53])).
% 3.24/0.78 thf(c_0_59, negated_conjecture, ![X1:$i > $o, X2:$i, X3:$i]:((((dsetconstr @ X2 @ X1)=(setadjoin @ (esk11_2 @ X2 @ X1) @ emptyset))|(X1 @ (esk10_2 @ X2 @ X1))|~((in @ X3 @ X2))|~((X1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_42])).
% 3.24/0.78 thf(c_0_60, negated_conjecture, ![X1:$i > $o, X2:$i, X3:$i]:(((in @ (esk11_2 @ X2 @ X1) @ (dsetconstr @ X2 @ X1))|(X1 @ (esk9_2 @ X2 @ X1))|~((in @ X3 @ X2))|~((X1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_42])).
% 3.24/0.78 thf(c_0_61, negated_conjecture, ![X1:$i > $o, X2:$i, X3:$i]:((((dsetconstr @ X2 @ X1)=(setadjoin @ (esk11_2 @ X2 @ X1) @ emptyset))|(X1 @ (esk9_2 @ X2 @ X1))|~((in @ X3 @ X2))|~((X1 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_42])).
% 3.24/0.78 thf(c_0_62, negated_conjecture, ![X2:$i]:((((dsetconstr @ (setunion @ esk19_0) @ epred1_0)!=(setadjoin @ X2 @ emptyset))|~((in @ X2 @ (dsetconstr @ (setunion @ esk19_0) @ epred1_0))))), inference(cn,[status(thm)],[c_0_54])).
% 3.24/0.78 thf(c_0_63, negated_conjecture, ![X1:$i > $o]:(((in @ (esk11_2 @ (setunion @ esk19_0) @ X1) @ (dsetconstr @ (setunion @ esk19_0) @ X1))|(X1 @ (esk10_2 @ (setunion @ esk19_0) @ X1))|~((X1 @ esk21_0)))), inference(spm,[status(thm)],[c_0_55, c_0_56])).
% 3.24/0.78 thf(c_0_64, negated_conjecture, (epred1_0 @ esk21_0), inference(spm,[status(thm)],[c_0_57, c_0_48])).
% 3.24/0.78 thf(c_0_65, plain, ![X2:$i]:((((esk21_0)=(X2))|~((epred1_0 @ X2)))), inference(spm,[status(thm)],[c_0_58, c_0_48])).
% 3.24/0.78 thf(c_0_66, negated_conjecture, ![X1:$i > $o]:((((setadjoin @ (esk11_2 @ (setunion @ esk19_0) @ X1) @ emptyset)=(dsetconstr @ (setunion @ esk19_0) @ X1))|(X1 @ (esk10_2 @ (setunion @ esk19_0) @ X1))|~((X1 @ esk21_0)))), inference(spm,[status(thm)],[c_0_59, c_0_56])).
% 3.24/0.78 thf(c_0_67, negated_conjecture, ![X1:$i > $o]:(((in @ (esk11_2 @ (setunion @ esk19_0) @ X1) @ (dsetconstr @ (setunion @ esk19_0) @ X1))|(X1 @ (esk9_2 @ (setunion @ esk19_0) @ X1))|~((X1 @ esk21_0)))), inference(spm,[status(thm)],[c_0_60, c_0_56])).
% 3.24/0.78 thf(c_0_68, negated_conjecture, ![X1:$i > $o]:((((setadjoin @ (esk11_2 @ (setunion @ esk19_0) @ X1) @ emptyset)=(dsetconstr @ (setunion @ esk19_0) @ X1))|(X1 @ (esk9_2 @ (setunion @ esk19_0) @ X1))|~((X1 @ esk21_0)))), inference(spm,[status(thm)],[c_0_61, c_0_56])).
% 3.24/0.78 thf(c_0_69, negated_conjecture, ![X3:$i, X2:$i, X1:$i > $o]:((((dsetconstr @ X2 @ X1)=(setadjoin @ (esk11_2 @ X2 @ X1) @ emptyset))|~((in @ X3 @ X2))|~((X1 @ X3))|((esk9_2 @ X2 @ X1)!=(esk10_2 @ X2 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_42])).
% 3.24/0.78 thf(c_0_70, negated_conjecture, ((epred1_0 @ (esk10_2 @ (setunion @ esk19_0) @ epred1_0))|((setadjoin @ (esk11_2 @ (setunion @ esk19_0) @ epred1_0) @ emptyset)!=(dsetconstr @ (setunion @ esk19_0) @ epred1_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_62, c_0_63]), c_0_64])])).
% 3.24/0.78 thf(c_0_71, plain, (((setadjoin @ (esk11_2 @ (setunion @ esk19_0) @ epred1_0) @ emptyset)=(dsetconstr @ (setunion @ esk19_0) @ epred1_0))|((esk10_2 @ (setunion @ esk19_0) @ epred1_0)=(esk21_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_65, c_0_66]), c_0_64])])).
% 3.24/0.78 thf(c_0_72, negated_conjecture, ((epred1_0 @ (esk9_2 @ (setunion @ esk19_0) @ epred1_0))|((setadjoin @ (esk11_2 @ (setunion @ esk19_0) @ epred1_0) @ emptyset)!=(dsetconstr @ (setunion @ esk19_0) @ epred1_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_62, c_0_67]), c_0_64])])).
% 3.24/0.78 thf(c_0_73, plain, (((setadjoin @ (esk11_2 @ (setunion @ esk19_0) @ epred1_0) @ emptyset)=(dsetconstr @ (setunion @ esk19_0) @ epred1_0))|((esk9_2 @ (setunion @ esk19_0) @ epred1_0)=(esk21_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_65, c_0_68]), c_0_64])])).
% 3.24/0.78 thf(c_0_74, negated_conjecture, ![X3:$i, X2:$i, X1:$i > $o]:(((in @ (esk11_2 @ X2 @ X1) @ (dsetconstr @ X2 @ X1))|~((in @ X3 @ X2))|~((X1 @ X3))|((esk9_2 @ X2 @ X1)!=(esk10_2 @ X2 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_42])).
% 3.24/0.78 thf(c_0_75, negated_conjecture, ![X1:$i > $o]:((((setadjoin @ (esk11_2 @ (setunion @ esk19_0) @ X1) @ emptyset)=(dsetconstr @ (setunion @ esk19_0) @ X1))|((esk10_2 @ (setunion @ esk19_0) @ X1)!=(esk9_2 @ (setunion @ esk19_0) @ X1))|~((X1 @ esk21_0)))), inference(spm,[status(thm)],[c_0_69, c_0_56])).
% 3.24/0.78 thf(c_0_76, plain, ((esk10_2 @ (setunion @ esk19_0) @ epred1_0)=(esk21_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_65, c_0_70]), c_0_71])).
% 3.24/0.78 thf(c_0_77, plain, ((esk9_2 @ (setunion @ esk19_0) @ epred1_0)=(esk21_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_65, c_0_72]), c_0_73])).
% 3.24/0.78 thf(c_0_78, negated_conjecture, ![X1:$i > $o]:(((in @ (esk11_2 @ (setunion @ esk19_0) @ X1) @ (dsetconstr @ (setunion @ esk19_0) @ X1))|((esk10_2 @ (setunion @ esk19_0) @ X1)!=(esk9_2 @ (setunion @ esk19_0) @ X1))|~((X1 @ esk21_0)))), inference(spm,[status(thm)],[c_0_74, c_0_56])).
% 3.24/0.78 thf(c_0_79, plain, ((setadjoin @ (esk11_2 @ (setunion @ esk19_0) @ epred1_0) @ emptyset)=(dsetconstr @ (setunion @ esk19_0) @ epred1_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_75, c_0_76]), c_0_77]), c_0_64])])).
% 3.24/0.78 thf(c_0_80, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_62, c_0_78]), c_0_79]), c_0_76]), c_0_77]), c_0_64])]), ['proof']).
% 3.24/0.78 % SZS output end CNFRefutation
% 3.24/0.78 % Parsed axioms : 379
% 3.24/0.78 % Removed by relevancy pruning/SinE : 358
% 3.24/0.78 % Initial clauses : 213
% 3.24/0.78 % Removed in clause preprocessing : 0
% 3.24/0.78 % Initial clauses in saturation : 213
% 3.24/0.78 % Processed clauses : 3553
% 3.24/0.78 % ...of these trivial : 11
% 3.24/0.78 % ...subsumed : 2406
% 3.24/0.78 % ...remaining for further processing : 1136
% 3.24/0.78 % Other redundant clauses eliminated : 83
% 3.24/0.78 % Clauses deleted for lack of memory : 0
% 3.24/0.78 % Backward-subsumed : 75
% 3.24/0.78 % Backward-rewritten : 83
% 3.24/0.78 % Generated clauses : 26971
% 3.24/0.78 % ...of the previous two non-redundant : 25981
% 3.24/0.78 % ...aggressively subsumed : 0
% 3.24/0.78 % Contextual simplify-reflections : 4
% 3.24/0.78 % Paramodulations : 26884
% 3.24/0.78 % Factorizations : 0
% 3.24/0.78 % NegExts : 0
% 3.24/0.78 % Equation resolutions : 87
% 3.24/0.78 % Disequality decompositions : 0
% 3.24/0.78 % Total rewrite steps : 5598
% 3.24/0.78 % ...of those cached : 5416
% 3.24/0.78 % Propositional unsat checks : 0
% 3.24/0.78 % Propositional check models : 0
% 3.24/0.78 % Propositional check unsatisfiable : 0
% 3.24/0.78 % Propositional clauses : 0
% 3.24/0.78 % Propositional clauses after purity: 0
% 3.24/0.78 % Propositional unsat core size : 0
% 3.24/0.78 % Propositional preprocessing time : 0.000
% 3.24/0.78 % Propositional encoding time : 0.000
% 3.24/0.78 % Propositional solver time : 0.000
% 3.24/0.78 % Success case prop preproc time : 0.000
% 3.24/0.78 % Success case prop encoding time : 0.000
% 3.24/0.78 % Success case prop solver time : 0.000
% 3.24/0.78 % Current number of processed clauses : 975
% 3.24/0.78 % Positive orientable unit clauses : 178
% 3.24/0.78 % Positive unorientable unit clauses: 0
% 3.24/0.78 % Negative unit clauses : 0
% 3.24/0.78 % Non-unit-clauses : 797
% 3.24/0.78 % Current number of unprocessed clauses: 21313
% 3.24/0.78 % ...number of literals in the above : 113146
% 3.24/0.78 % Current number of archived formulas : 0
% 3.24/0.78 % Current number of archived clauses : 158
% 3.24/0.78 % Clause-clause subsumption calls (NU) : 143986
% 3.24/0.78 % Rec. Clause-clause subsumption calls : 54770
% 3.24/0.78 % Non-unit clause-clause subsumptions : 2481
% 3.24/0.78 % Unit Clause-clause subsumption calls : 986
% 3.24/0.78 % Rewrite failures with RHS unbound : 0
% 3.24/0.78 % BW rewrite match attempts : 66
% 3.24/0.78 % BW rewrite match successes : 51
% 3.24/0.78 % Condensation attempts : 0
% 3.24/0.78 % Condensation successes : 0
% 3.24/0.78 % Termbank termtop insertions : 691693
% 3.24/0.78 % Search garbage collected termcells : 5987
% 3.24/0.78
% 3.24/0.78 % -------------------------------------------------
% 3.24/0.78 % User time : 0.440 s
% 3.24/0.78 % System time : 0.020 s
% 3.24/0.78 % Total time : 0.459 s
% 3.24/0.78 % Maximum resident set size: 5548 pages
% 3.24/0.78
% 3.24/0.78 % -------------------------------------------------
% 3.24/0.78 % User time : 0.449 s
% 3.24/0.78 % System time : 0.024 s
% 3.24/0.78 % Total time : 0.473 s
% 3.24/0.78 % Maximum resident set size: 5120 pages
% 3.24/0.78 % E exiting
%------------------------------------------------------------------------------