%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : SEU518^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 : n005.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:20 AM UTC 2026
% Result : Theorem 0.24s 0.30s
% Output : CNFRefutation 0.24s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU518^1 : TPTP v9.3.1. Released v3.7.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.19 % Computer : n005.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Tue Sep 29 13:47:46 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.25 Running higher-order theorem proving
% 0.08/0.27 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.fRsDliPzTO/E---3.1_1692218.p
% 0.24/0.30 % Version: 3.5.1-ho
% 0.24/0.30 % Preprocessing class: HSMSSLSSMLLCHFA.
% 0.24/0.30 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.24/0.30 % Starting new_ho_10 with 1500s (5) cores
% 0.24/0.30 % Starting sh5l with 300s (1) cores
% 0.24/0.30 % Starting new_bool_1 with 300s (1) cores
% 0.24/0.30 % Starting new_bool_2 with 300s (1) cores
% 0.24/0.30 % new_bool_1 with pid 1692243 completed with status 0
% 0.24/0.30 % Result found by new_bool_1
% 0.24/0.30 % Preprocessing class: HSMSSLSSMLLCHFA.
% 0.24/0.30 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.24/0.30 % Starting new_ho_10 with 1500s (5) cores
% 0.24/0.30 % Starting sh5l with 300s (1) cores
% 0.24/0.30 % Starting new_bool_1 with 300s (1) cores
% 0.24/0.30 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,1.5,,3,20000,1.0))
% 0.24/0.30 % SinE strategy is GSinE(CountFormulas,hypos,1.5,,3,20000,1.0)
% 0.24/0.30 % Search class: HGHSS-FFMS31-SHFSMSBN
% 0.24/0.30 % Scheduled 5 strats onto 1 cores with 300 seconds (300 total)
% 0.24/0.30 % Starting SubtermCWHack with 31s (1) cores
% 0.24/0.30 % SubtermCWHack with pid 1692246 completed with status 0
% 0.24/0.30 % Result found by SubtermCWHack
% 0.24/0.30 % Preprocessing class: HSMSSLSSMLLCHFA.
% 0.24/0.30 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.24/0.30 % Starting new_ho_10 with 1500s (5) cores
% 0.24/0.30 % Starting sh5l with 300s (1) cores
% 0.24/0.30 % Starting new_bool_1 with 300s (1) cores
% 0.24/0.30 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,1.5,,3,20000,1.0))
% 0.24/0.30 % SinE strategy is GSinE(CountFormulas,hypos,1.5,,3,20000,1.0)
% 0.24/0.30 % Search class: HGHSS-FFMS31-SHFSMSBN
% 0.24/0.30 % Scheduled 5 strats onto 1 cores with 300 seconds (300 total)
% 0.24/0.30 % Starting SubtermCWHack with 31s (1) cores
% 0.24/0.30 % Preprocessing time : 0.003 s
% 0.24/0.30
% 0.24/0.30 % Proof found!
% 0.24/0.30 % SZS status Theorem
% 0.24/0.30 % SZS output start CNFRefutation
% 0.24/0.30 thf(decl_23, type, in: $i > $i > $o).
% 0.24/0.30 thf(decl_24, type, exu: ($i > $o) > $o).
% 0.24/0.30 thf(decl_25, type, setextAx: $o).
% 0.24/0.30 thf(decl_26, type, emptyset: $i).
% 0.24/0.30 thf(decl_27, type, emptysetAx: $o).
% 0.24/0.30 thf(decl_28, type, setadjoin: $i > $i > $i).
% 0.24/0.30 thf(decl_29, type, setadjoinAx: $o).
% 0.24/0.30 thf(decl_30, type, powerset: $i > $i).
% 0.24/0.30 thf(decl_31, type, powersetAx: $o).
% 0.24/0.30 thf(decl_33, type, setunionAx: $o).
% 0.24/0.30 thf(decl_34, type, omega: $i).
% 0.24/0.30 thf(decl_35, type, omega0Ax: $o).
% 0.24/0.30 thf(decl_36, type, omegaSAx: $o).
% 0.24/0.30 thf(decl_37, type, omegaIndAx: $o).
% 0.24/0.30 thf(decl_38, type, replAx: $o).
% 0.24/0.30 thf(decl_39, type, foundationAx: $o).
% 0.24/0.30 thf(decl_40, type, wellorderingAx: $o).
% 0.24/0.30 thf(decl_42, type, descrp: $o).
% 0.24/0.30 thf(decl_43, type, dsetconstr: $i > ($i > $o) > $i).
% 0.24/0.30 thf(decl_44, type, dsetconstrI: $o).
% 0.24/0.30 thf(decl_45, type, dsetconstrEL: $o).
% 0.24/0.30 thf(decl_46, type, dsetconstrER: $o).
% 0.24/0.30 thf(decl_47, type, exuE1: $o).
% 0.24/0.30 thf(decl_48, type, prop2set: $o > $i).
% 0.24/0.30 thf(decl_49, type, prop2setE: $o).
% 0.24/0.30 thf(decl_50, type, emptysetE: $o).
% 0.24/0.30 thf(decl_51, type, emptysetimpfalse: $o).
% 0.24/0.30 thf(decl_52, type, notinemptyset: $o).
% 0.24/0.30 thf(decl_53, type, exuE3e: $o).
% 0.24/0.30 thf(decl_54, type, setext: $o).
% 0.24/0.30 thf(decl_55, type, emptyI: $o).
% 0.24/0.30 thf(decl_56, type, noeltsimpempty: $o).
% 0.24/0.30 thf(decl_57, type, setbeta: $o).
% 0.24/0.30 thf(decl_58, type, nonempty: $i > $o).
% 0.24/0.30 thf(decl_59, type, nonemptyE1: $o).
% 0.24/0.30 thf(decl_60, type, nonemptyI: $o).
% 0.24/0.30 thf(decl_61, type, nonemptyI1: $o).
% 0.24/0.30 thf(decl_62, type, setadjoinIL: $o).
% 0.24/0.30 thf(decl_63, type, emptyinunitempty: $o).
% 0.24/0.31 thf(decl_64, type, setadjoinIR: $o).
% 0.24/0.31 thf(decl_65, type, setadjoinE: $o).
% 0.24/0.31 thf(decl_66, type, setadjoinOr: $o).
% 0.24/0.31 thf(decl_67, type, setoftrueEq: $o).
% 0.24/0.31 thf(decl_68, type, epred1_0: $o).
% 0.24/0.31 thf(decl_69, type, esk1_2: $i > $i > $i).
% 0.24/0.31 thf(decl_70, type, esk2_2: $i > $i > $i).
% 0.24/0.31 thf(decl_71, type, esk3_1: $i > $i).
% 0.24/0.31 thf(decl_72, type, esk4_2: ($i > $i > $o) > $i > $i).
% 0.24/0.31 thf(decl_73, type, esk5_3: ($i > $i > $o) > $i > $i > $i).
% 0.24/0.31 thf(decl_74, type, esk6_2: ($i > $i > $o) > $i > $i).
% 0.24/0.31 thf(decl_75, type, esk7_3: ($i > $i > $o) > $i > $i > $i).
% 0.24/0.31 thf(decl_76, type, esk8_1: $i > $i).
% 0.24/0.31 thf(decl_77, type, esk9_2: ($i > $o) > $i > $i).
% 0.24/0.31 thf(decl_78, type, esk10_1: ($i > $o) > $i).
% 0.24/0.31 thf(decl_79, type, esk11_2: ($i > $o) > $i > $i).
% 0.24/0.31 thf(decl_80, type, esk12_1: ($i > $o) > $i).
% 0.24/0.31 thf(decl_81, type, esk13_2: $i > $i > $i).
% 0.24/0.31 thf(decl_82, type, esk14_2: $i > $i > $i).
% 0.24/0.31 thf(decl_83, type, esk15_1: $i > $i).
% 0.24/0.31 thf(decl_84, type, esk16_1: $i > $i).
% 0.24/0.31 thf(decl_85, type, esk17_1: $i > $i).
% 0.24/0.31 thf(decl_86, type, esk18_0: $i).
% 0.24/0.31 thf(decl_87, type, esk19_0: $i).
% 0.24/0.31 thf(nonempty, axiom, ((nonempty)=(^[X2:$i]:(((X2)!=(emptyset))))), file('/export/starexec/sandbox2/tmp/tmp.fRsDliPzTO/E---3.1_1692218.p', nonempty)).
% 0.24/0.31 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.fRsDliPzTO/E---3.1_1692218.p', nonemptyI)).
% 0.24/0.31 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.fRsDliPzTO/E---3.1_1692218.p', replAx)).
% 0.24/0.31 thf(exu, axiom, ((exu)=(^[X1:$i > $o]:(?[X2:$i]:((((X1 @ X2))&(![X3:$i]:((((X1 @ X3))=>(((X2)=(X3))))))))))), file('/export/starexec/sandbox2/tmp/tmp.fRsDliPzTO/E---3.1_1692218.p', exu)).
% 0.24/0.31 thf(prop2set, axiom, ((prop2set)=(^[X10:$o]:(dsetconstr @ (powerset @ emptyset) @ (^[X2:$i]:((X10)))))), file('/export/starexec/sandbox2/tmp/tmp.fRsDliPzTO/E---3.1_1692218.p', prop2set)).
% 0.24/0.31 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.fRsDliPzTO/E---3.1_1692218.p', exuE1)).
% 0.24/0.31 thf(exuE3e, axiom, ((exuE3e)<=>![X1:$i > $o]:(((exu @ (^[X2:$i]:((X1 @ X2))))=>?[X2:$i]:((X1 @ X2))))), file('/export/starexec/sandbox2/tmp/tmp.fRsDliPzTO/E---3.1_1692218.p', exuE3e)).
% 0.24/0.31 thf(powersetI, 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)=>![X4:$i, X5:$i]:((![X2:$i]:(((in @ X2 @ X5)=>(in @ X2 @ X4)))=>(in @ X5 @ (powerset @ X4)))))))))))))))))))))))))))))))))))))), file('/export/starexec/sandbox2/tmp/tmp.fRsDliPzTO/E---3.1_1692218.p', powersetI)).
% 0.24/0.31 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.fRsDliPzTO/E---3.1_1692218.p', setbeta)).
% 0.24/0.31 thf(nonemptyE1, axiom, ((nonemptyE1)<=>![X4:$i]:(((nonempty @ X4)=>?[X2:$i]:((in @ X2 @ X4))))), file('/export/starexec/sandbox2/tmp/tmp.fRsDliPzTO/E---3.1_1692218.p', nonemptyE1)).
% 0.24/0.31 thf(nonemptyI1, axiom, ((nonemptyI1)<=>![X4:$i]:((?[X2:$i]:((in @ X2 @ X4))=>(nonempty @ X4)))), file('/export/starexec/sandbox2/tmp/tmp.fRsDliPzTO/E---3.1_1692218.p', nonemptyI1)).
% 0.24/0.31 thf(setoftrueEq, axiom, ((setoftrueEq)<=>![X4:$i]:(((dsetconstr @ X4 @ (^[X2:$i]:(($true))))=(X4)))), file('/export/starexec/sandbox2/tmp/tmp.fRsDliPzTO/E---3.1_1692218.p', setoftrueEq)).
% 0.24/0.31 thf(prop2setE, axiom, ((prop2setE)<=>![X11:$o, X2:$i]:(((in @ X2 @ (prop2set @ ((X11))))=>(X11)))), file('/export/starexec/sandbox2/tmp/tmp.fRsDliPzTO/E---3.1_1692218.p', prop2setE)).
% 0.24/0.31 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.fRsDliPzTO/E---3.1_1692218.p', dsetconstrER)).
% 0.24/0.31 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.fRsDliPzTO/E---3.1_1692218.p', dsetconstrEL)).
% 0.24/0.31 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.fRsDliPzTO/E---3.1_1692218.p', dsetconstrI)).
% 0.24/0.31 thf(setadjoinIL, axiom, ((setadjoinIL)<=>![X2:$i, X3:$i]:((in @ X2 @ (setadjoin @ X2 @ X3)))), file('/export/starexec/sandbox2/tmp/tmp.fRsDliPzTO/E---3.1_1692218.p', setadjoinIL)).
% 0.24/0.31 thf(emptyinunitempty, axiom, ((emptyinunitempty)<=>(in @ emptyset @ (setadjoin @ emptyset @ emptyset))), file('/export/starexec/sandbox2/tmp/tmp.fRsDliPzTO/E---3.1_1692218.p', emptyinunitempty)).
% 0.24/0.31 thf(setadjoinIR, axiom, ((setadjoinIR)<=>![X2:$i, X4:$i, X3:$i]:(((in @ X3 @ X4)=>(in @ X3 @ (setadjoin @ X2 @ X4))))), file('/export/starexec/sandbox2/tmp/tmp.fRsDliPzTO/E---3.1_1692218.p', setadjoinIR)).
% 0.24/0.31 thf(setextAx, axiom, ((setextAx)<=>![X4:$i, X5:$i]:((![X2:$i]:(((in @ X2 @ X4)<=>(in @ X2 @ X5)))=>((X4)=(X5))))), file('/export/starexec/sandbox2/tmp/tmp.fRsDliPzTO/E---3.1_1692218.p', setextAx)).
% 0.24/0.31 thf(setadjoinE, axiom, ((setadjoinE)<=>![X2:$i, X4:$i, X3:$i]:(((in @ X3 @ (setadjoin @ X2 @ X4))=>![X13:$o]:(((((X3)=(X2))=>(X13))=>(((in @ X3 @ X4)=>(X13))=>(X13))))))), file('/export/starexec/sandbox2/tmp/tmp.fRsDliPzTO/E---3.1_1692218.p', setadjoinE)).
% 0.24/0.31 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.fRsDliPzTO/E---3.1_1692218.p', setadjoinOr)).
% 0.24/0.31 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.fRsDliPzTO/E---3.1_1692218.p', powersetAx)).
% 0.24/0.31 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.fRsDliPzTO/E---3.1_1692218.p', foundationAx)).
% 0.24/0.31 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.fRsDliPzTO/E---3.1_1692218.p', omegaIndAx)).
% 0.24/0.31 thf(omegaSAx, axiom, ((omegaSAx)<=>![X2:$i]:(((in @ X2 @ omega)=>(in @ (setadjoin @ X2 @ X2) @ omega)))), file('/export/starexec/sandbox2/tmp/tmp.fRsDliPzTO/E---3.1_1692218.p', omegaSAx)).
% 0.24/0.31 thf(omega0Ax, axiom, ((omega0Ax)<=>(in @ emptyset @ omega)), file('/export/starexec/sandbox2/tmp/tmp.fRsDliPzTO/E---3.1_1692218.p', omega0Ax)).
% 0.24/0.31 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.fRsDliPzTO/E---3.1_1692218.p', setadjoinAx)).
% 0.24/0.31 thf(emptysetAx, axiom, ((emptysetAx)<=>![X2:$i]:(~((in @ X2 @ emptyset)))), file('/export/starexec/sandbox2/tmp/tmp.fRsDliPzTO/E---3.1_1692218.p', emptysetAx)).
% 0.24/0.31 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.fRsDliPzTO/E---3.1_1692218.p', wellorderingAx)).
% 0.24/0.31 thf(emptysetimpfalse, axiom, ((emptysetimpfalse)<=>![X2:$i]:(((in @ X2 @ emptyset)=>~($true)))), file('/export/starexec/sandbox2/tmp/tmp.fRsDliPzTO/E---3.1_1692218.p', emptysetimpfalse)).
% 0.24/0.31 thf(emptysetE, axiom, ((emptysetE)<=>![X2:$i]:(((in @ X2 @ emptyset)=>![X12:$o]:((X12))))), file('/export/starexec/sandbox2/tmp/tmp.fRsDliPzTO/E---3.1_1692218.p', emptysetE)).
% 0.24/0.31 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.fRsDliPzTO/E---3.1_1692218.p', setext)).
% 0.24/0.31 thf(emptyI, axiom, ((emptyI)<=>![X4:$i]:((![X2:$i]:(~((in @ X2 @ X4)))=>((X4)=(emptyset))))), file('/export/starexec/sandbox2/tmp/tmp.fRsDliPzTO/E---3.1_1692218.p', emptyI)).
% 0.24/0.31 thf(noeltsimpempty, axiom, ((noeltsimpempty)<=>![X4:$i]:((![X2:$i]:(~((in @ X2 @ X4)))=>((X4)=(emptyset))))), file('/export/starexec/sandbox2/tmp/tmp.fRsDliPzTO/E---3.1_1692218.p', noeltsimpempty)).
% 0.24/0.31 thf(notinemptyset, axiom, ((notinemptyset)<=>![X2:$i]:(~((in @ X2 @ emptyset)))), file('/export/starexec/sandbox2/tmp/tmp.fRsDliPzTO/E---3.1_1692218.p', notinemptyset)).
% 0.24/0.31 thf(c_0_36, plain, ((nonempty)=(^[Z0:$i]:(((Z0)!=(emptyset))))), inference(fof_simplification,[status(thm)],[nonempty])).
% 0.24/0.31 thf(c_0_37, 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])).
% 0.24/0.31 thf(c_0_38, 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])).
% 0.24/0.31 thf(c_0_39, plain, ((exu)=(^[Z0:$i > $o]:(?[X2:$i]:((((Z0 @ X2))&(![X3:$i]:((((Z0 @ X3))=>(((X2)=(X3))))))))))), inference(fof_simplification,[status(thm)],[exu])).
% 0.24/0.31 thf(c_0_40, plain, ((prop2set)=(^[Z0:$o]:(dsetconstr @ (powerset @ emptyset) @ (^[Z1:$i]:((Z0)))))), inference(fof_simplification,[status(thm)],[prop2set])).
% 0.24/0.31 thf(c_0_41, 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])).
% 0.24/0.31 thf(c_0_42, plain, ((exuE3e)<=>![X1:$i > $o]:(((exu @ (^[Z0:$i]:((X1 @ Z0))))=>?[X2:$i]:((X1 @ X2))))), inference(fof_simplification,[status(thm)],[exuE3e])).
% 0.24/0.31 thf(c_0_43, 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)=>![X4:$i, X5:$i]:((![X2:$i]:(((in @ X2 @ X5)=>(in @ X2 @ X4)))=>(in @ X5 @ (powerset @ X4))))))))))))))))))))))))))))))))))))))), inference(assume_negation,[status(cth)],[powersetI])).
% 0.24/0.31 thf(c_0_44, 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])).
% 0.24/0.31 thf(c_0_45, axiom, ((nonemptyE1)=(![X4:$i]:((((((X4)!=(emptyset))))=>(?[X2:$i]:((in @ X2 @ X4))))))), inference(apply_def,[status(thm)],[nonemptyE1, c_0_36])).
% 0.24/0.31 thf(c_0_46, 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_37, c_0_36])).
% 0.24/0.31 thf(c_0_47, axiom, ((nonemptyI1)=(![X4:$i]:(((?[X2:$i]:((in @ X2 @ X4)))=>((((X4)!=(emptyset)))))))), inference(apply_def,[status(thm)],[nonemptyI1, c_0_36])).
% 0.24/0.31 thf(c_0_48, plain, ((setoftrueEq)<=>![X4:$i]:(((dsetconstr @ X4 @ (^[Z0:$i]:(($true))))=(X4)))), inference(fof_simplification,[status(thm)],[setoftrueEq])).
% 0.24/0.31 thf(c_0_49, plain, ((replAx)=(![X6:$i > $i > $o, X4:$i]:(((![X2:$i]:((((in @ X2 @ X4))=>((?[X111:$i]:(((((X6 @ X2 @ X111)))&(![X112:$i]:(((((X6 @ X2 @ X112)))=>(((X111)=(X112)))))))))))))=>(?[X5:$i]:(![X2:$i]:((((in @ X2 @ X5))<=>(?[X3:$i]:((((in @ X3 @ X4))&((X6 @ X3 @ X2))))))))))))), inference(apply_def,[status(thm)],[c_0_38, c_0_39])).
% 0.24/0.31 thf(c_0_50, axiom, ((prop2setE)=(![X11:$o, X2:$i]:((((in @ X2 @ (dsetconstr @ (powerset @ emptyset) @ (^[Z0:$i]:(((X11)))))))=>((X11)))))), inference(apply_def,[status(thm)],[prop2setE, c_0_40])).
% 0.24/0.31 thf(c_0_51, plain, ((exuE1)=(![X1:$i > $o]:((((?[X113:$i]:(((((X1 @ X113)))&(![X114:$i]:(((((X1 @ X114)))=>(((X113)=(X114))))))))))=>(?[X2:$i]:((((X1 @ X2))&(![X3:$i]:((((X1 @ X3))=>(((X2)=(X3))))))))))))), inference(apply_def,[status(thm)],[c_0_41, c_0_39])).
% 0.24/0.31 thf(c_0_52, 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])).
% 0.24/0.31 thf(c_0_53, 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])).
% 0.24/0.31 thf(c_0_54, 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])).
% 0.24/0.31 thf(c_0_55, plain, ((exuE3e)=(![X1:$i > $o]:((((?[X115:$i]:(((((X1 @ X115)))&(![X116:$i]:(((((X1 @ X116)))=>(((X115)=(X116))))))))))=>(?[X2:$i]:((X1 @ X2))))))), inference(apply_def,[status(thm)],[c_0_42, c_0_39])).
% 0.24/0.31 thf(c_0_56, plain, ((epred1_0)<=>![X143:$i]:(?[X144:$i]:((((![X145:$i]:(((in @ X145 @ X144)=>![X146:$i]:(((in @ X146 @ X145)=>(in @ X146 @ X143)))))&![X147:$i, X148:$i]:((((in @ X147 @ X143)&(in @ X148 @ X143))=>(![X149:$i]:(((in @ X149 @ X144)=>((in @ X147 @ X149)<=>(in @ X148 @ X149))))=>((X147)=(X148))))))&![X150:$i, X151:$i]:((((in @ X150 @ X144)&(in @ X151 @ X144))=>(![X152:$i]:(((in @ X152 @ X150)=>(in @ X152 @ X151)))|![X153:$i]:(((in @ X153 @ X151)=>(in @ X153 @ X150)))))))&![X154:$i]:(((![X155:$i]:(((in @ X155 @ X154)=>(in @ X155 @ X143)))&?[X156:$i]:((in @ X156 @ X154)))=>?[X157:$i, X158:$i]:(((((in @ X157 @ X144)&(in @ X158 @ X154))&~(?[X159:$i]:(((in @ X159 @ X157)&(in @ X159 @ X154)))))&![X160:$i]:(((in @ X160 @ X144)=>(![X161:$i]:(((in @ X161 @ X160)=>(in @ X161 @ X157)))|(in @ X158 @ X160)))))))))))), introduced(definition)).
% 0.24/0.31 thf(c_0_57, negated_conjecture, ~((![X117:$i, X118:$i]:((![X119:$i]:(((in @ X119 @ X117)<=>(in @ X119 @ X118)))=>((X117)=(X118))))=>(![X120:$i]:(~(in @ X120 @ emptyset))=>(![X121:$i, X122:$i, X123:$i]:(((in @ X123 @ (setadjoin @ X121 @ X122))<=>(((X123)=(X121))|(in @ X123 @ X122))))=>(![X124:$i, X125:$i]:(((in @ X125 @ (powerset @ X124))<=>![X126:$i]:(((in @ X126 @ X125)=>(in @ X126 @ X124)))))=>((setunionAx)=>((in @ emptyset @ omega)=>(![X127:$i]:(((in @ X127 @ omega)=>(in @ (setadjoin @ X127 @ X127) @ omega)))=>(![X128:$i]:((((in @ emptyset @ X128)&![X129:$i]:((((in @ X129 @ omega)&(in @ X129 @ X128))=>(in @ (setadjoin @ X129 @ X129) @ X128))))=>![X130:$i]:(((in @ X130 @ omega)=>(in @ X130 @ X128)))))=>(![X131:$i > $i > $o, X132:$i]:((![X133:$i]:(((in @ X133 @ X132)=>?[X134:$i]:(((X131 @ X133 @ X134)&![X135:$i]:(((X131 @ X133 @ X135)=>((X134)=(X135))))))))=>?[X136:$i]:(![X137:$i]:(((in @ X137 @ X136)<=>?[X138:$i]:(((in @ X138 @ X132)&(X131 @ X138 @ X137))))))))=>(![X139:$i]:((?[X140:$i]:((in @ X140 @ X139))=>?[X141:$i]:(((in @ X141 @ X139)&~(?[X142:$i]:(((in @ X142 @ X141)&(in @ X142 @ X139))))))))=>((epred1_0)=>((descrp)=>(![X162:$i, X163:$i > $o, X164:$i]:(((in @ X164 @ X162)=>((X163 @ X164)=>(in @ X164 @ (dsetconstr @ X162 @ X163)))))=>(![X165:$i, X166:$i > $o, X167:$i]:(((in @ X167 @ (dsetconstr @ X165 @ X166))=>(in @ X167 @ X165)))=>(![X168:$i, X169:$i > $o, X170:$i]:(((in @ X170 @ (dsetconstr @ X168 @ X169))=>(X169 @ X170)))=>(![X171:$i > $o]:((?[X172:$i]:(((X171 @ X172)&![X173:$i]:(((X171 @ X173)=>((X172)=(X173))))))=>?[X174:$i]:(((X171 @ X174)&![X175:$i]:(((X171 @ X175)=>((X174)=(X175))))))))=>(![X176:$o, X177:$i]:(((in @ X177 @ (dsetconstr @ (powerset @ emptyset) @ (^[Z0:$i]:((X176)))))=>(X176)))=>(![X178:$i]:(((in @ X178 @ emptyset)=>![X179:$o]:((X179))))=>(![X180:$i]:(((in @ X180 @ emptyset)=>~($true)))=>(![X181:$i]:(~(in @ X181 @ emptyset))=>(![X182:$i > $o]:((?[X183:$i]:(((X182 @ X183)&![X184:$i]:(((X182 @ X184)=>((X183)=(X184))))))=>?[X185:$i]:((X182 @ X185))))=>(![X186:$i, X187:$i]:((![X188:$i]:(((in @ X188 @ X186)=>(in @ X188 @ X187)))=>(![X189:$i]:(((in @ X189 @ X187)=>(in @ X189 @ X186)))=>((X186)=(X187)))))=>(![X190:$i]:((![X191:$i]:(~(in @ X191 @ X190))=>((X190)=(emptyset))))=>(![X192:$i]:((![X193:$i]:(~(in @ X193 @ X192))=>((X192)=(emptyset))))=>(![X194:$i, X195:$i > $o, X196:$i]:(((in @ X196 @ X194)=>((in @ X196 @ (dsetconstr @ X194 @ X195))<=>(X195 @ X196))))=>(![X197:$i]:((((X197)!=(emptyset))=>?[X198:$i]:((in @ X198 @ X197))))=>(![X199:$i, X200:$i > $o, X201:$i]:(((in @ X201 @ X199)=>((X200 @ X201)=>((dsetconstr @ X199 @ X200)!=(emptyset)))))=>(![X202:$i]:((?[X203:$i]:((in @ X203 @ X202))=>((X202)!=(emptyset))))=>(![X204:$i, X205:$i]:((in @ X204 @ (setadjoin @ X204 @ X205)))=>((in @ emptyset @ (setadjoin @ emptyset @ emptyset))=>(![X206:$i, X207:$i, X208:$i]:(((in @ X208 @ X207)=>(in @ X208 @ (setadjoin @ X206 @ X207))))=>(![X209:$i, X210:$i, X211:$i]:(((in @ X211 @ (setadjoin @ X209 @ X210))=>![X212:$o]:(((((X211)=(X209))=>(X212))=>(((in @ X211 @ X210)=>(X212))=>(X212))))))=>(![X213:$i, X214:$i, X215:$i]:(((in @ X215 @ (setadjoin @ X213 @ X214))=>(((X215)=(X213))|(in @ X215 @ X214))))=>(![X216:$i]:(((dsetconstr @ X216 @ (^[Z0:$i]:($true)))=(X216)))=>![X4:$i, X5:$i]:((![X2:$i]:(((in @ X2 @ X5)=>(in @ X2 @ X4)))=>(in @ X5 @ (powerset @ X4))))))))))))))))))))))))))))))))))))))), 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)],[c_0_43, c_0_44]), c_0_45]), c_0_46]), c_0_47]), setadjoinIL]), emptyinunitempty]), setadjoinIR]), setextAx]), setadjoinE]), setadjoinOr]), c_0_48]), powersetAx]), foundationAx]), c_0_49]), omegaIndAx]), omegaSAx]), omega0Ax]), setadjoinAx]), emptysetAx]), wellorderingAx]), emptysetimpfalse]), emptysetE]), c_0_50]), c_0_51]), c_0_52]), c_0_53]), c_0_54]), c_0_55]), setext]), emptyI]), noeltsimpempty]), notinemptyset])])]), c_0_56])).
% 0.24/0.31 thf(c_0_58, negated_conjecture, ![X217:$i, X218:$i, X220:$i, X221:$i, X222:$i, X223:$i, X224:$i, X225:$i, X226:$i, X227:$i, X228:$i, X230:$i, X231:$i, X233:$i, X234:$i > $i > $o, X235:$i, X237:$i, X240:$i, X242:$i, X243:$i, X244:$i, X245:$i, X247:$i, X248:$i, X249:$i > $o, X250:$i, X251:$i, X252:$i > $o, X253:$i, X254:$i, X255:$i > $o, X256:$i, X257:$i > $o, X258:$i, X261:$i, X262:$o, X263:$i, X264:$i, X265:$o, X266:$i, X267:$i, X268:$i > $o, X269:$i, X272:$i, X273:$i, X276:$i, X278:$i, X280:$i, X281:$i > $o, X282:$i, X283:$i, X285:$i, X286:$i > $o, X287:$i, X288:$i, X289:$i, X290:$i, X291:$i, X292:$i, X293:$i, X294:$i, X295:$i, X296:$i, X297:$i, X298:$o, X299:$i, X300:$i, X301:$i, X302:$i, X305:$i]:((((~(in @ (esk1_2 @ X217 @ X218) @ X217)|~(in @ (esk1_2 @ X217 @ X218) @ X218)|((X217)=(X218)))&((in @ (esk1_2 @ X217 @ X218) @ X217)|(in @ (esk1_2 @ X217 @ X218) @ X218)|((X217)=(X218))))&(~(in @ X220 @ emptyset)&(((~(in @ X223 @ (setadjoin @ X221 @ X222))|(((X223)=(X221))|(in @ X223 @ X222)))&((((X223)!=(X221))|(in @ X223 @ (setadjoin @ X221 @ X222)))&(~(in @ X223 @ X222)|(in @ X223 @ (setadjoin @ X221 @ X222)))))&(((~(in @ X225 @ (powerset @ X224))|(~(in @ X226 @ X225)|(in @ X226 @ X224)))&(((in @ (esk2_2 @ X227 @ X228) @ X228)|(in @ X228 @ (powerset @ X227)))&(~(in @ (esk2_2 @ X227 @ X228) @ X227)|(in @ X228 @ (powerset @ X227)))))&((setunionAx)&((in @ emptyset @ omega)&((~(in @ X230 @ omega)|(in @ (setadjoin @ X230 @ X230) @ omega))&(((((in @ (esk3_1 @ X231) @ omega)|~(in @ emptyset @ X231)|(~(in @ X233 @ omega)|(in @ X233 @ X231)))&((in @ (esk3_1 @ X231) @ X231)|~(in @ emptyset @ X231)|(~(in @ X233 @ omega)|(in @ X233 @ X231))))&(~(in @ (setadjoin @ (esk3_1 @ X231) @ (esk3_1 @ X231)) @ X231)|~(in @ emptyset @ X231)|(~(in @ X233 @ omega)|(in @ X233 @ X231))))&((((((in @ (esk7_3 @ X234 @ X235 @ X240) @ X235)|~(in @ X240 @ (esk6_2 @ X234 @ X235))|(in @ (esk4_2 @ X234 @ X235) @ X235))&((X234 @ (esk7_3 @ X234 @ X235 @ X240) @ X240)|~(in @ X240 @ (esk6_2 @ X234 @ X235))|(in @ (esk4_2 @ X234 @ X235) @ X235)))&(~(in @ X243 @ X235)|~(X234 @ X243 @ X242)|(in @ X242 @ (esk6_2 @ X234 @ X235))|(in @ (esk4_2 @ X234 @ X235) @ X235)))&(((((in @ (esk7_3 @ X234 @ X235 @ X240) @ X235)|~(in @ X240 @ (esk6_2 @ X234 @ X235))|((X234 @ (esk4_2 @ X234 @ X235) @ (esk5_3 @ X234 @ X235 @ X237))|~(X234 @ (esk4_2 @ X234 @ X235) @ X237)))&((X234 @ (esk7_3 @ X234 @ X235 @ X240) @ X240)|~(in @ X240 @ (esk6_2 @ X234 @ X235))|((X234 @ (esk4_2 @ X234 @ X235) @ (esk5_3 @ X234 @ X235 @ X237))|~(X234 @ (esk4_2 @ X234 @ X235) @ X237))))&(~(in @ X243 @ X235)|~(X234 @ X243 @ X242)|(in @ X242 @ (esk6_2 @ X234 @ X235))|((X234 @ (esk4_2 @ X234 @ X235) @ (esk5_3 @ X234 @ X235 @ X237))|~(X234 @ (esk4_2 @ X234 @ X235) @ X237))))&((((in @ (esk7_3 @ X234 @ X235 @ X240) @ X235)|~(in @ X240 @ (esk6_2 @ X234 @ X235))|(((X237)!=(esk5_3 @ X234 @ X235 @ X237))|~(X234 @ (esk4_2 @ X234 @ X235) @ X237)))&((X234 @ (esk7_3 @ X234 @ X235 @ X240) @ X240)|~(in @ X240 @ (esk6_2 @ X234 @ X235))|(((X237)!=(esk5_3 @ X234 @ X235 @ X237))|~(X234 @ (esk4_2 @ X234 @ X235) @ X237))))&(~(in @ X243 @ X235)|~(X234 @ X243 @ X242)|(in @ X242 @ (esk6_2 @ X234 @ X235))|(((X237)!=(esk5_3 @ X234 @ X235 @ X237))|~(X234 @ (esk4_2 @ X234 @ X235) @ X237))))))&((((in @ (esk8_1 @ X244) @ X244)|~(in @ X245 @ X244))&(~(in @ X247 @ (esk8_1 @ X244))|~(in @ X247 @ X244)|~(in @ X245 @ X244)))&((epred1_0)&((descrp)&((~(in @ X250 @ X248)|(~(X249 @ X250)|(in @ X250 @ (dsetconstr @ X248 @ X249))))&((~(in @ X253 @ (dsetconstr @ X251 @ X252))|(in @ X253 @ X251))&((~(in @ X256 @ (dsetconstr @ X254 @ X255))|(X255 @ X256))&(((((X257 @ (esk10_1 @ X257))|((X257 @ (esk9_2 @ X257 @ X258))|~(X257 @ X258)))&(~(X257 @ X261)|((esk10_1 @ X257)=(X261))|((X257 @ (esk9_2 @ X257 @ X258))|~(X257 @ X258))))&(((X257 @ (esk10_1 @ X257))|(((X258)!=(esk9_2 @ X257 @ X258))|~(X257 @ X258)))&(~(X257 @ X261)|((esk10_1 @ X257)=(X261))|(((X258)!=(esk9_2 @ X257 @ X258))|~(X257 @ X258)))))&((~(in @ X263 @ (dsetconstr @ (powerset @ emptyset) @ (^[Z0:$i]:((X262)))))|(X262))&((~(in @ X264 @ emptyset)|(X265))&((~(in @ X266 @ emptyset)|~($true))&(~(in @ X267 @ emptyset)&((((X268 @ (esk11_2 @ X268 @ X269))|~(X268 @ X269)|(X268 @ (esk12_1 @ X268)))&(((X269)!=(esk11_2 @ X268 @ X269))|~(X268 @ X269)|(X268 @ (esk12_1 @ X268))))&(((((in @ (esk14_2 @ X272 @ X273) @ X273)|((X272)=(X273))|(in @ (esk13_2 @ X272 @ X273) @ X272))&(~(in @ (esk14_2 @ X272 @ X273) @ X272)|((X272)=(X273))|(in @ (esk13_2 @ X272 @ X273) @ X272)))&(((in @ (esk14_2 @ X272 @ X273) @ X273)|((X272)=(X273))|~(in @ (esk13_2 @ X272 @ X273) @ X273))&(~(in @ (esk14_2 @ X272 @ X273) @ X272)|((X272)=(X273))|~(in @ (esk13_2 @ X272 @ X273) @ X273))))&(((in @ (esk15_1 @ X276) @ X276)|((X276)=(emptyset)))&(((in @ (esk16_1 @ X278) @ X278)|((X278)=(emptyset)))&(((~(in @ X282 @ (dsetconstr @ X280 @ X281))|(X281 @ X282)|~(in @ X282 @ X280))&(~(X281 @ X282)|(in @ X282 @ (dsetconstr @ X280 @ X281))|~(in @ X282 @ X280)))&((((X283)=(emptyset))|(in @ (esk17_1 @ X283) @ X283))&((~(in @ X287 @ X285)|(~(X286 @ X287)|((dsetconstr @ X285 @ X286)!=(emptyset))))&((~(in @ X289 @ X288)|((X288)!=(emptyset)))&((in @ X290 @ (setadjoin @ X290 @ X291))&((in @ emptyset @ (setadjoin @ emptyset @ emptyset))&((~(in @ X294 @ X293)|(in @ X294 @ (setadjoin @ X292 @ X293)))&(((((in @ X297 @ X296)|(X298)|((X297)=(X295))|~(in @ X297 @ (setadjoin @ X295 @ X296)))&(~(X298)|(X298)|((X297)=(X295))|~(in @ X297 @ (setadjoin @ X295 @ X296))))&(((in @ X297 @ X296)|(X298)|~(X298)|~(in @ X297 @ (setadjoin @ X295 @ X296)))&(~(X298)|(X298)|~(X298)|~(in @ X297 @ (setadjoin @ X295 @ X296)))))&((~(in @ X301 @ (setadjoin @ X299 @ X300))|(((X301)=(X299))|(in @ X301 @ X300)))&(((dsetconstr @ X302 @ (^[Z0:$i]:($true)))=(X302))&((~(in @ X305 @ esk19_0)|(in @ X305 @ esk18_0))&~(in @ esk19_0 @ (powerset @ esk18_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_57])])])])])])])).
% 0.24/0.31 thf(c_0_59, negated_conjecture, ![X2:$i]:(((in @ X2 @ esk18_0)|~((in @ X2 @ esk19_0)))), inference(split_conjunct,[status(thm)],[c_0_58])).
% 0.24/0.31 thf(c_0_60, negated_conjecture, ![X3:$i, X2:$i]:(((in @ (esk2_2 @ X2 @ X3) @ X3)|(in @ X3 @ (powerset @ X2)))), inference(split_conjunct,[status(thm)],[c_0_58])).
% 0.24/0.31 thf(c_0_61, negated_conjecture, ![X3:$i, X2:$i]:(((in @ X3 @ (powerset @ X2))|~((in @ (esk2_2 @ X2 @ X3) @ X2)))), inference(split_conjunct,[status(thm)],[c_0_58])).
% 0.24/0.31 thf(c_0_62, negated_conjecture, ![X2:$i]:(((in @ (esk2_2 @ X2 @ esk19_0) @ esk18_0)|(in @ esk19_0 @ (powerset @ X2)))), inference(spm,[status(thm)],[c_0_59, c_0_60])).
% 0.24/0.31 thf(c_0_63, negated_conjecture, ~((in @ esk19_0 @ (powerset @ esk18_0))), inference(split_conjunct,[status(thm)],[c_0_58])).
% 0.24/0.31 thf(c_0_64, negated_conjecture, ($false), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_61, c_0_62]), c_0_63]), ['proof']).
% 0.24/0.31 % SZS output end CNFRefutation
% 0.24/0.31 % Parsed axioms : 83
% 0.24/0.31 % Removed by relevancy pruning/SinE : 47
% 0.24/0.31 % Initial clauses : 76
% 0.24/0.31 % Removed in clause preprocessing : 3
% 0.24/0.31 % Initial clauses in saturation : 73
% 0.24/0.31 % Processed clauses : 59
% 0.24/0.31 % ...of these trivial : 0
% 0.24/0.31 % ...subsumed : 17
% 0.24/0.31 % ...remaining for further processing : 42
% 0.24/0.31 % Other redundant clauses eliminated : 2
% 0.24/0.31 % Clauses deleted for lack of memory : 0
% 0.24/0.31 % Backward-subsumed : 0
% 0.24/0.31 % Backward-rewritten : 2
% 0.24/0.31 % Generated clauses : 57
% 0.24/0.31 % ...of the previous two non-redundant : 46
% 0.24/0.31 % ...aggressively subsumed : 0
% 0.24/0.31 % Contextual simplify-reflections : 0
% 0.24/0.31 % Paramodulations : 55
% 0.24/0.31 % Factorizations : 0
% 0.24/0.31 % NegExts : 0
% 0.24/0.31 % Equation resolutions : 2
% 0.24/0.31 % Disequality decompositions : 0
% 0.24/0.31 % Total rewrite steps : 12
% 0.24/0.31 % ...of those cached : 5
% 0.24/0.31 % Propositional unsat checks : 0
% 0.24/0.31 % Propositional check models : 0
% 0.24/0.31 % Propositional check unsatisfiable : 0
% 0.24/0.31 % Propositional clauses : 0
% 0.24/0.31 % Propositional clauses after purity: 0
% 0.24/0.31 % Propositional unsat core size : 0
% 0.24/0.31 % Propositional preprocessing time : 0.000
% 0.24/0.31 % Propositional encoding time : 0.000
% 0.24/0.31 % Propositional solver time : 0.000
% 0.24/0.31 % Success case prop preproc time : 0.000
% 0.24/0.31 % Success case prop encoding time : 0.000
% 0.24/0.31 % Success case prop solver time : 0.000
% 0.24/0.31 % Current number of processed clauses : 38
% 0.24/0.31 % Positive orientable unit clauses : 12
% 0.24/0.31 % Positive unorientable unit clauses: 0
% 0.24/0.31 % Negative unit clauses : 2
% 0.24/0.31 % Non-unit-clauses : 24
% 0.24/0.31 % Current number of unprocessed clauses: 59
% 0.24/0.31 % ...number of literals in the above : 206
% 0.24/0.31 % Current number of archived formulas : 0
% 0.24/0.31 % Current number of archived clauses : 2
% 0.24/0.31 % Clause-clause subsumption calls (NU) : 140
% 0.24/0.31 % Rec. Clause-clause subsumption calls : 136
% 0.24/0.31 % Non-unit clause-clause subsumptions : 10
% 0.24/0.31 % Unit Clause-clause subsumption calls : 49
% 0.24/0.31 % Rewrite failures with RHS unbound : 0
% 0.24/0.31 % BW rewrite match attempts : 8
% 0.24/0.31 % BW rewrite match successes : 2
% 0.24/0.31 % Condensation attempts : 0
% 0.24/0.31 % Condensation successes : 0
% 0.24/0.31 % Termbank termtop insertions : 9896
% 0.24/0.31 % Search garbage collected termcells : 3616
% 0.24/0.31
% 0.24/0.31 % -------------------------------------------------
% 0.24/0.31 % User time : 0.013 s
% 0.24/0.31 % System time : 0.005 s
% 0.24/0.31 % Total time : 0.019 s
% 0.24/0.31 % Maximum resident set size: 4488 pages
% 0.24/0.31
% 0.24/0.31 % -------------------------------------------------
% 0.24/0.31 % User time : 0.015 s
% 0.24/0.31 % System time : 0.012 s
% 0.24/0.31 % Total time : 0.026 s
% 0.24/0.31 % Maximum resident set size: 4608 pages
% 0.24/0.31 % E exiting
%------------------------------------------------------------------------------