%------------------------------------------------------------------------------
% File : E-SAT---3.5.1
% Problem : SEU515^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 : n010.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 08:26:32 AM UTC 2026
% Result : Theorem 0.23s 0.29s
% Output : CNFRefutation 0.23s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU515^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 : n010.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:48:03 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.24 Running higher-order theorem proving
% 0.08/0.26 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.BYu6oItNT0/E---3.1_2880201.p
% 0.23/0.29 % Version: 3.5.1-ho
% 0.23/0.29 % Preprocessing class: HSMSSLSSMLLCHFA.
% 0.23/0.29 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.23/0.29 % Starting new_ho_10 with 1500s (5) cores
% 0.23/0.29 % Starting sh5l with 300s (1) cores
% 0.23/0.29 % Starting new_bool_1 with 300s (1) cores
% 0.23/0.29 % Starting new_bool_2 with 300s (1) cores
% 0.23/0.29 % new_bool_2 with pid 2880238 completed with status 0
% 0.23/0.29 % Result found by new_bool_2
% 0.23/0.29 % Preprocessing class: HSMSSLSSMLLCHFA.
% 0.23/0.29 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.23/0.29 % Starting new_ho_10 with 1500s (5) cores
% 0.23/0.29 % Starting sh5l with 300s (1) cores
% 0.23/0.29 % Starting new_bool_1 with 300s (1) cores
% 0.23/0.29 % Starting new_bool_2 with 300s (1) cores
% 0.23/0.29 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,1.5,,3,20000,1.0))
% 0.23/0.29 % SinE strategy is GSinE(CountFormulas,hypos,1.5,,3,20000,1.0)
% 0.23/0.29 % Search class: HGHSF-FFMM31-SHFSMSBN
% 0.23/0.29 % partial match(2): HGHSM-FFMS31-SHFSMSBN
% 0.23/0.29 % Scheduled 5 strats onto 1 cores with 300 seconds (300 total)
% 0.23/0.29 % Starting SubtermCWHack with 31s (1) cores
% 0.23/0.29 % SubtermCWHack with pid 2880240 completed with status 0
% 0.23/0.29 % Result found by SubtermCWHack
% 0.23/0.29 % Preprocessing class: HSMSSLSSMLLCHFA.
% 0.23/0.29 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.23/0.29 % Starting new_ho_10 with 1500s (5) cores
% 0.23/0.29 % Starting sh5l with 300s (1) cores
% 0.23/0.29 % Starting new_bool_1 with 300s (1) cores
% 0.23/0.29 % Starting new_bool_2 with 300s (1) cores
% 0.23/0.29 % (lift_lambdas = 0, lambda_to_forall = 0,unroll_only_formulas = 0, sine = GSinE(CountFormulas,hypos,1.5,,3,20000,1.0))
% 0.23/0.29 % SinE strategy is GSinE(CountFormulas,hypos,1.5,,3,20000,1.0)
% 0.23/0.29 % Search class: HGHSF-FFMM31-SHFSMSBN
% 0.23/0.29 % partial match(2): HGHSM-FFMS31-SHFSMSBN
% 0.23/0.29 % Scheduled 5 strats onto 1 cores with 300 seconds (300 total)
% 0.23/0.29 % Starting SubtermCWHack with 31s (1) cores
% 0.23/0.29 % Preprocessing time : 0.002 s
% 0.23/0.29
% 0.23/0.29 % Proof found!
% 0.23/0.29 % SZS status Theorem
% 0.23/0.29 % SZS output start CNFRefutation
% 0.23/0.29 thf(decl_23, type, in: $i > $i > $o).
% 0.23/0.29 thf(decl_24, type, exu: ($i > $o) > $o).
% 0.23/0.29 thf(decl_25, type, setextAx: $o).
% 0.23/0.29 thf(decl_26, type, emptyset: $i).
% 0.23/0.29 thf(decl_27, type, emptysetAx: $o).
% 0.23/0.29 thf(decl_28, type, setadjoin: $i > $i > $i).
% 0.23/0.29 thf(decl_29, type, setadjoinAx: $o).
% 0.23/0.29 thf(decl_30, type, powerset: $i > $i).
% 0.23/0.29 thf(decl_31, type, powersetAx: $o).
% 0.23/0.29 thf(decl_33, type, setunionAx: $o).
% 0.23/0.29 thf(decl_34, type, omega: $i).
% 0.23/0.29 thf(decl_35, type, omega0Ax: $o).
% 0.23/0.29 thf(decl_36, type, omegaSAx: $o).
% 0.23/0.29 thf(decl_37, type, omegaIndAx: $o).
% 0.23/0.29 thf(decl_38, type, replAx: $o).
% 0.23/0.29 thf(decl_39, type, foundationAx: $o).
% 0.23/0.29 thf(decl_40, type, wellorderingAx: $o).
% 0.23/0.29 thf(decl_42, type, descrp: $o).
% 0.23/0.29 thf(decl_43, type, dsetconstr: $i > ($i > $o) > $i).
% 0.23/0.29 thf(decl_44, type, dsetconstrI: $o).
% 0.23/0.29 thf(decl_45, type, dsetconstrEL: $o).
% 0.23/0.29 thf(decl_46, type, dsetconstrER: $o).
% 0.23/0.29 thf(decl_47, type, exuE1: $o).
% 0.23/0.29 thf(decl_48, type, prop2set: $o > $i).
% 0.23/0.29 thf(decl_49, type, prop2setE: $o).
% 0.23/0.29 thf(decl_50, type, emptysetE: $o).
% 0.23/0.29 thf(decl_51, type, emptysetimpfalse: $o).
% 0.23/0.29 thf(decl_52, type, notinemptyset: $o).
% 0.23/0.29 thf(decl_53, type, exuE3e: $o).
% 0.23/0.29 thf(decl_54, type, setext: $o).
% 0.23/0.29 thf(decl_55, type, emptyI: $o).
% 0.23/0.29 thf(decl_56, type, noeltsimpempty: $o).
% 0.23/0.29 thf(decl_57, type, setbeta: $o).
% 0.23/0.29 thf(decl_58, type, nonempty: $i > $o).
% 0.23/0.29 thf(decl_59, type, nonemptyE1: $o).
% 0.23/0.29 thf(decl_60, type, nonemptyI: $o).
% 0.23/0.29 thf(decl_61, type, nonemptyI1: $o).
% 0.23/0.29 thf(decl_62, type, setadjoinIL: $o).
% 0.23/0.29 thf(decl_63, type, emptyinunitempty: $o).
% 0.23/0.29 thf(decl_64, type, setadjoinIR: $o).
% 0.23/0.29 thf(decl_65, type, epred1_0: $o).
% 0.23/0.29 thf(decl_66, type, esk1_2: $i > $i > $i).
% 0.23/0.29 thf(decl_67, type, esk2_2: $i > $i > $i).
% 0.23/0.29 thf(decl_68, type, esk3_1: $i > $i).
% 0.23/0.29 thf(decl_69, type, esk4_2: ($i > $i > $o) > $i > $i).
% 0.23/0.29 thf(decl_70, type, esk5_3: ($i > $i > $o) > $i > $i > $i).
% 0.23/0.29 thf(decl_71, type, esk6_2: ($i > $i > $o) > $i > $i).
% 0.23/0.29 thf(decl_72, type, esk7_3: ($i > $i > $o) > $i > $i > $i).
% 0.23/0.29 thf(decl_73, type, esk8_1: $i > $i).
% 0.23/0.29 thf(decl_74, type, esk9_2: ($i > $o) > $i > $i).
% 0.23/0.29 thf(decl_75, type, esk10_1: ($i > $o) > $i).
% 0.23/0.29 thf(decl_76, type, esk11_2: ($i > $o) > $i > $i).
% 0.23/0.29 thf(decl_77, type, esk12_1: ($i > $o) > $i).
% 0.23/0.29 thf(decl_78, type, esk13_2: $i > $i > $i).
% 0.23/0.29 thf(decl_79, type, esk14_2: $i > $i > $i).
% 0.23/0.29 thf(decl_80, type, esk15_1: $i > $i).
% 0.23/0.29 thf(decl_81, type, esk16_1: $i > $i).
% 0.23/0.29 thf(decl_82, type, esk17_1: $i > $i).
% 0.23/0.29 thf(decl_83, type, esk18_0: $i).
% 0.23/0.29 thf(decl_84, type, esk19_0: $i).
% 0.23/0.29 thf(decl_85, type, esk20_0: $i).
% 0.23/0.29 thf(decl_86, type, epred2_0: $o).
% 0.23/0.29 thf(exuE3e, axiom, ((exuE3e)<=>![X1:$i > $o]:(((exu @ (^[X2:$i]:((X1 @ X2))))=>?[X2:$i]:((X1 @ X2))))), file('/export/starexec/sandbox2/tmp/tmp.BYu6oItNT0/E---3.1_2880201.p', exuE3e)).
% 0.23/0.29 thf(exu, axiom, ((exu)=(^[X1:$i > $o]:(?[X2:$i]:((((X1 @ X2))&(![X3:$i]:((((X1 @ X3))=>(((X2)=(X3))))))))))), file('/export/starexec/sandbox2/tmp/tmp.BYu6oItNT0/E---3.1_2880201.p', exu)).
% 0.23/0.29 thf(nonempty, axiom, ((nonempty)=(^[X2:$i]:(((X2)!=(emptyset))))), file('/export/starexec/sandbox2/tmp/tmp.BYu6oItNT0/E---3.1_2880201.p', nonempty)).
% 0.23/0.29 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.BYu6oItNT0/E---3.1_2880201.p', nonemptyI)).
% 0.23/0.29 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.BYu6oItNT0/E---3.1_2880201.p', replAx)).
% 0.23/0.29 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.BYu6oItNT0/E---3.1_2880201.p', exuE1)).
% 0.23/0.29 thf(prop2set, axiom, ((prop2set)=(^[X10:$o]:(dsetconstr @ (powerset @ emptyset) @ (^[X2:$i]:((X10)))))), file('/export/starexec/sandbox2/tmp/tmp.BYu6oItNT0/E---3.1_2880201.p', prop2set)).
% 0.23/0.29 thf(setadjoinE, 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)=>![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.BYu6oItNT0/E---3.1_2880201.p', setadjoinE)).
% 0.23/0.29 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.BYu6oItNT0/E---3.1_2880201.p', setbeta)).
% 0.23/0.29 thf(nonemptyE1, axiom, ((nonemptyE1)<=>![X4:$i]:(((nonempty @ X4)=>?[X2:$i]:((in @ X2 @ X4))))), file('/export/starexec/sandbox2/tmp/tmp.BYu6oItNT0/E---3.1_2880201.p', nonemptyE1)).
% 0.23/0.29 thf(nonemptyI1, axiom, ((nonemptyI1)<=>![X4:$i]:((?[X2:$i]:((in @ X2 @ X4))=>(nonempty @ X4)))), file('/export/starexec/sandbox2/tmp/tmp.BYu6oItNT0/E---3.1_2880201.p', nonemptyI1)).
% 0.23/0.29 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.BYu6oItNT0/E---3.1_2880201.p', dsetconstrEL)).
% 0.23/0.29 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.BYu6oItNT0/E---3.1_2880201.p', dsetconstrI)).
% 0.23/0.29 thf(prop2setE, axiom, ((prop2setE)<=>![X11:$o, X2:$i]:(((in @ X2 @ (prop2set @ ((X11))))=>(X11)))), file('/export/starexec/sandbox2/tmp/tmp.BYu6oItNT0/E---3.1_2880201.p', prop2setE)).
% 0.23/0.29 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.BYu6oItNT0/E---3.1_2880201.p', dsetconstrER)).
% 0.23/0.29 thf(notinemptyset, axiom, ((notinemptyset)<=>![X2:$i]:(~((in @ X2 @ emptyset)))), file('/export/starexec/sandbox2/tmp/tmp.BYu6oItNT0/E---3.1_2880201.p', notinemptyset)).
% 0.23/0.29 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.BYu6oItNT0/E---3.1_2880201.p', setext)).
% 0.23/0.29 thf(emptyI, axiom, ((emptyI)<=>![X4:$i]:((![X2:$i]:(~((in @ X2 @ X4)))=>((X4)=(emptyset))))), file('/export/starexec/sandbox2/tmp/tmp.BYu6oItNT0/E---3.1_2880201.p', emptyI)).
% 0.23/0.29 thf(noeltsimpempty, axiom, ((noeltsimpempty)<=>![X4:$i]:((![X2:$i]:(~((in @ X2 @ X4)))=>((X4)=(emptyset))))), file('/export/starexec/sandbox2/tmp/tmp.BYu6oItNT0/E---3.1_2880201.p', noeltsimpempty)).
% 0.23/0.29 thf(setadjoinIL, axiom, ((setadjoinIL)<=>![X2:$i, X3:$i]:((in @ X2 @ (setadjoin @ X2 @ X3)))), file('/export/starexec/sandbox2/tmp/tmp.BYu6oItNT0/E---3.1_2880201.p', setadjoinIL)).
% 0.23/0.29 thf(emptyinunitempty, axiom, ((emptyinunitempty)<=>(in @ emptyset @ (setadjoin @ emptyset @ emptyset))), file('/export/starexec/sandbox2/tmp/tmp.BYu6oItNT0/E---3.1_2880201.p', emptyinunitempty)).
% 0.23/0.29 thf(setadjoinIR, axiom, ((setadjoinIR)<=>![X2:$i, X4:$i, X3:$i]:(((in @ X3 @ X4)=>(in @ X3 @ (setadjoin @ X2 @ X4))))), file('/export/starexec/sandbox2/tmp/tmp.BYu6oItNT0/E---3.1_2880201.p', setadjoinIR)).
% 0.23/0.29 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.BYu6oItNT0/E---3.1_2880201.p', powersetAx)).
% 0.23/0.29 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.BYu6oItNT0/E---3.1_2880201.p', setadjoinAx)).
% 0.23/0.29 thf(emptysetAx, axiom, ((emptysetAx)<=>![X2:$i]:(~((in @ X2 @ emptyset)))), file('/export/starexec/sandbox2/tmp/tmp.BYu6oItNT0/E---3.1_2880201.p', emptysetAx)).
% 0.23/0.29 thf(setextAx, axiom, ((setextAx)<=>![X4:$i, X5:$i]:((![X2:$i]:(((in @ X2 @ X4)<=>(in @ X2 @ X5)))=>((X4)=(X5))))), file('/export/starexec/sandbox2/tmp/tmp.BYu6oItNT0/E---3.1_2880201.p', setextAx)).
% 0.23/0.29 thf(omega0Ax, axiom, ((omega0Ax)<=>(in @ emptyset @ omega)), file('/export/starexec/sandbox2/tmp/tmp.BYu6oItNT0/E---3.1_2880201.p', omega0Ax)).
% 0.23/0.29 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.BYu6oItNT0/E---3.1_2880201.p', wellorderingAx)).
% 0.23/0.29 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.BYu6oItNT0/E---3.1_2880201.p', foundationAx)).
% 0.23/0.29 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.BYu6oItNT0/E---3.1_2880201.p', omegaIndAx)).
% 0.23/0.29 thf(omegaSAx, axiom, ((omegaSAx)<=>![X2:$i]:(((in @ X2 @ omega)=>(in @ (setadjoin @ X2 @ X2) @ omega)))), file('/export/starexec/sandbox2/tmp/tmp.BYu6oItNT0/E---3.1_2880201.p', omegaSAx)).
% 0.23/0.29 thf(emptysetE, axiom, ((emptysetE)<=>![X2:$i]:(((in @ X2 @ emptyset)=>![X12:$o]:((X12))))), file('/export/starexec/sandbox2/tmp/tmp.BYu6oItNT0/E---3.1_2880201.p', emptysetE)).
% 0.23/0.29 thf(emptysetimpfalse, axiom, ((emptysetimpfalse)<=>![X2:$i]:(((in @ X2 @ emptyset)=>~($true)))), file('/export/starexec/sandbox2/tmp/tmp.BYu6oItNT0/E---3.1_2880201.p', emptysetimpfalse)).
% 0.23/0.29 thf(c_0_33, plain, ((exuE3e)<=>![X1:$i > $o]:(((exu @ (^[Z0:$i]:((X1 @ Z0))))=>?[X2:$i]:((X1 @ X2))))), inference(fof_simplification,[status(thm)],[exuE3e])).
% 0.23/0.29 thf(c_0_34, plain, ((exu)=(^[Z0:$i > $o]:(?[X2:$i]:((((Z0 @ X2))&(![X3:$i]:((((Z0 @ X3))=>(((X2)=(X3))))))))))), inference(fof_simplification,[status(thm)],[exu])).
% 0.23/0.29 thf(c_0_35, plain, ((nonempty)=(^[Z0:$i]:(((Z0)!=(emptyset))))), inference(fof_simplification,[status(thm)],[nonempty])).
% 0.23/0.29 thf(c_0_36, 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.23/0.29 thf(c_0_37, 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.23/0.29 thf(c_0_38, 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.23/0.29 thf(c_0_39, plain, ((prop2set)=(^[Z0:$o]:(dsetconstr @ (powerset @ emptyset) @ (^[Z1:$i]:((Z0)))))), inference(fof_simplification,[status(thm)],[prop2set])).
% 0.23/0.29 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)=>![X2:$i, X4:$i, X3:$i]:(((in @ X3 @ (setadjoin @ X2 @ X4))=>![X13:$o]:(((((X3)=(X2))=>(X13))=>(((in @ X3 @ X4)=>(X13))=>(X13)))))))))))))))))))))))))))))))))))))), inference(assume_negation,[status(cth)],[setadjoinE])).
% 0.23/0.29 thf(c_0_41, plain, ((exuE3e)=(![X1:$i > $o]:((((?[X108:$i]:(((((X1 @ X108)))&(![X109:$i]:(((((X1 @ X109)))=>(((X108)=(X109))))))))))=>(?[X2:$i]:((X1 @ X2))))))), inference(apply_def,[status(thm)],[c_0_33, c_0_34])).
% 0.23/0.29 thf(c_0_42, 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.23/0.29 thf(c_0_43, axiom, ((nonemptyE1)=(![X4:$i]:((((((X4)!=(emptyset))))=>(?[X2:$i]:((in @ X2 @ X4))))))), inference(apply_def,[status(thm)],[nonemptyE1, c_0_35])).
% 0.23/0.29 thf(c_0_44, 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_36, c_0_35])).
% 0.23/0.29 thf(c_0_45, axiom, ((nonemptyI1)=(![X4:$i]:(((?[X2:$i]:((in @ X2 @ X4)))=>((((X4)!=(emptyset)))))))), inference(apply_def,[status(thm)],[nonemptyI1, c_0_35])).
% 0.23/0.29 thf(c_0_46, 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.23/0.29 thf(c_0_47, 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.23/0.29 thf(c_0_48, plain, ((replAx)=(![X6:$i > $i > $o, X4:$i]:(((![X2:$i]:((((in @ X2 @ X4))=>((?[X104:$i]:(((((X6 @ X2 @ X104)))&(![X105:$i]:(((((X6 @ X2 @ X105)))=>(((X104)=(X105)))))))))))))=>(?[X5:$i]:(![X2:$i]:((((in @ X2 @ X5))<=>(?[X3:$i]:((((in @ X3 @ X4))&((X6 @ X3 @ X2))))))))))))), inference(apply_def,[status(thm)],[c_0_37, c_0_34])).
% 0.23/0.29 thf(c_0_49, plain, ((exuE1)=(![X1:$i > $o]:((((?[X106:$i]:(((((X1 @ X106)))&(![X107:$i]:(((((X1 @ X107)))=>(((X106)=(X107))))))))))=>(?[X2:$i]:((((X1 @ X2))&(![X3:$i]:((((X1 @ X3))=>(((X2)=(X3))))))))))))), inference(apply_def,[status(thm)],[c_0_38, c_0_34])).
% 0.23/0.29 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_39])).
% 0.23/0.29 thf(c_0_51, 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.23/0.29 thf(c_0_52, plain, ((epred1_0)<=>![X136:$i]:(?[X137:$i]:((((![X138:$i]:(((in @ X138 @ X137)=>![X139:$i]:(((in @ X139 @ X138)=>(in @ X139 @ X136)))))&![X140:$i, X141:$i]:((((in @ X140 @ X136)&(in @ X141 @ X136))=>(![X142:$i]:(((in @ X142 @ X137)=>((in @ X140 @ X142)<=>(in @ X141 @ X142))))=>((X140)=(X141))))))&![X143:$i, X144:$i]:((((in @ X143 @ X137)&(in @ X144 @ X137))=>(![X145:$i]:(((in @ X145 @ X143)=>(in @ X145 @ X144)))|![X146:$i]:(((in @ X146 @ X144)=>(in @ X146 @ X143)))))))&![X147:$i]:(((![X148:$i]:(((in @ X148 @ X147)=>(in @ X148 @ X136)))&?[X149:$i]:((in @ X149 @ X147)))=>?[X150:$i, X151:$i]:(((((in @ X150 @ X137)&(in @ X151 @ X147))&~(?[X152:$i]:(((in @ X152 @ X150)&(in @ X152 @ X147)))))&![X153:$i]:(((in @ X153 @ X137)=>(![X154:$i]:(((in @ X154 @ X153)=>(in @ X154 @ X150)))|(in @ X151 @ X153)))))))))))), introduced(definition)).
% 0.23/0.29 thf(c_0_53, negated_conjecture, ~((![X110:$i, X111:$i]:((![X112:$i]:(((in @ X112 @ X110)<=>(in @ X112 @ X111)))=>((X110)=(X111))))=>(![X113:$i]:(~(in @ X113 @ emptyset))=>(![X114:$i, X115:$i, X116:$i]:(((in @ X116 @ (setadjoin @ X114 @ X115))<=>(((X116)=(X114))|(in @ X116 @ X115))))=>(![X117:$i, X118:$i]:(((in @ X118 @ (powerset @ X117))<=>![X119:$i]:(((in @ X119 @ X118)=>(in @ X119 @ X117)))))=>((setunionAx)=>((in @ emptyset @ omega)=>(![X120:$i]:(((in @ X120 @ omega)=>(in @ (setadjoin @ X120 @ X120) @ omega)))=>(![X121:$i]:((((in @ emptyset @ X121)&![X122:$i]:((((in @ X122 @ omega)&(in @ X122 @ X121))=>(in @ (setadjoin @ X122 @ X122) @ X121))))=>![X123:$i]:(((in @ X123 @ omega)=>(in @ X123 @ X121)))))=>(![X124:$i > $i > $o, X125:$i]:((![X126:$i]:(((in @ X126 @ X125)=>?[X127:$i]:(((X124 @ X126 @ X127)&![X128:$i]:(((X124 @ X126 @ X128)=>((X127)=(X128))))))))=>?[X129:$i]:(![X130:$i]:(((in @ X130 @ X129)<=>?[X131:$i]:(((in @ X131 @ X125)&(X124 @ X131 @ X130))))))))=>(![X132:$i]:((?[X133:$i]:((in @ X133 @ X132))=>?[X134:$i]:(((in @ X134 @ X132)&~(?[X135:$i]:(((in @ X135 @ X134)&(in @ X135 @ X132))))))))=>((epred1_0)=>((descrp)=>(![X155:$i, X156:$i > $o, X157:$i]:(((in @ X157 @ X155)=>((X156 @ X157)=>(in @ X157 @ (dsetconstr @ X155 @ (^[Z0:$i]:((X156 @ Z0))))))))=>(![X158:$i, X159:$i > $o, X160:$i]:(((in @ X160 @ (dsetconstr @ X158 @ (^[Z0:$i]:((X159 @ Z0)))))=>(in @ X160 @ X158)))=>(![X161:$i, X162:$i > $o, X163:$i]:(((in @ X163 @ (dsetconstr @ X161 @ (^[Z0:$i]:((X162 @ Z0)))))=>(X162 @ X163)))=>(![X164:$i > $o]:((?[X165:$i]:(((X164 @ X165)&![X166:$i]:(((X164 @ X166)=>((X165)=(X166))))))=>?[X167:$i]:(((X164 @ X167)&![X168:$i]:(((X164 @ X168)=>((X167)=(X168))))))))=>(![X169:$o, X170:$i]:(((in @ X170 @ (dsetconstr @ (powerset @ emptyset) @ (^[Z0:$i]:((X169)))))=>(X169)))=>(![X171:$i]:(((in @ X171 @ emptyset)=>![X172:$o]:((X172))))=>(![X173:$i]:(~(in @ X173 @ emptyset))=>(![X174:$i]:(~(in @ X174 @ emptyset))=>(![X175:$i > $o]:((?[X176:$i]:(((X175 @ X176)&![X177:$i]:(((X175 @ X177)=>((X176)=(X177))))))=>?[X178:$i]:((X175 @ X178))))=>(![X179:$i, X180:$i]:((![X181:$i]:(((in @ X181 @ X179)=>(in @ X181 @ X180)))=>(![X182:$i]:(((in @ X182 @ X180)=>(in @ X182 @ X179)))=>((X179)=(X180)))))=>(![X183:$i]:((![X184:$i]:(~(in @ X184 @ X183))=>((X183)=(emptyset))))=>(![X185:$i]:((![X186:$i]:(~(in @ X186 @ X185))=>((X185)=(emptyset))))=>(![X187:$i, X188:$i > $o, X189:$i]:(((in @ X189 @ X187)=>((in @ X189 @ (dsetconstr @ X187 @ (^[Z0:$i]:((X188 @ Z0)))))<=>(X188 @ X189))))=>(![X190:$i]:((((X190)!=(emptyset))=>?[X191:$i]:((in @ X191 @ X190))))=>(![X192:$i, X193:$i > $o, X194:$i]:(((in @ X194 @ X192)=>((X193 @ X194)=>((dsetconstr @ X192 @ (^[Z0:$i]:((X193 @ Z0))))!=(emptyset)))))=>(![X195:$i]:((?[X196:$i]:((in @ X196 @ X195))=>((X195)!=(emptyset))))=>(![X197:$i, X198:$i]:((in @ X197 @ (setadjoin @ X197 @ X198)))=>((in @ emptyset @ (setadjoin @ emptyset @ emptyset))=>(![X199:$i, X200:$i, X201:$i]:(((in @ X201 @ X200)=>(in @ X201 @ (setadjoin @ X199 @ X200))))=>![X2:$i, X4:$i, X3:$i]:(((in @ X3 @ (setadjoin @ X2 @ X4))=>![X13:$o]:(((((X3)=(X2))=>(X13))=>(((in @ X3 @ X4)=>(X13))=>(X13)))))))))))))))))))))))))))))))))))))), inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(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_40, notinemptyset]), c_0_41]), setext]), emptyI]), noeltsimpempty]), c_0_42]), c_0_43]), c_0_44]), c_0_45]), setadjoinIL]), emptyinunitempty]), setadjoinIR]), powersetAx]), setadjoinAx]), emptysetAx]), setextAx]), omega0Ax]), c_0_46]), c_0_47]), wellorderingAx]), foundationAx]), c_0_48]), omegaIndAx]), omegaSAx]), c_0_49]), c_0_50]), emptysetE]), emptysetimpfalse]), c_0_51])]), c_0_52])).
% 0.23/0.29 thf(c_0_54, negated_conjecture, ![X202:$i, X203:$i, X205:$i, X206:$i, X207:$i, X208:$i, X209:$i, X210:$i, X211:$i, X212:$i, X213:$i, X215:$i, X216:$i, X218:$i, X219:$i > $i > $o, X220:$i, X222:$i, X225:$i, X227:$i, X228:$i, X229:$i, X230:$i, X232:$i, X233:$i, X234:$i > $o, X235:$i, X236:$i, X237:$i > $o, X238:$i, X239:$i, X240:$i > $o, X241:$i, X242:$i > $o, X243:$i, X246:$i, X247:$o, X248:$i, X249:$i, X250:$o, X251:$i, X252:$i, X253:$i > $o, X254:$i, X257:$i, X258:$i, X261:$i, X263:$i, X265:$i, X266:$i > $o, X267:$i, X268:$i, X270:$i, X271:$i > $o, X272:$i, X273:$i, X274:$i, X275:$i, X276:$i, X277:$i, X278:$i, X279:$i]:((((~(in @ (esk1_2 @ X202 @ X203) @ X202)|~(in @ (esk1_2 @ X202 @ X203) @ X203)|((X202)=(X203)))&((in @ (esk1_2 @ X202 @ X203) @ X202)|(in @ (esk1_2 @ X202 @ X203) @ X203)|((X202)=(X203))))&(~(in @ X205 @ emptyset)&(((~(in @ X208 @ (setadjoin @ X206 @ X207))|(((X208)=(X206))|(in @ X208 @ X207)))&((((X208)!=(X206))|(in @ X208 @ (setadjoin @ X206 @ X207)))&(~(in @ X208 @ X207)|(in @ X208 @ (setadjoin @ X206 @ X207)))))&(((~(in @ X210 @ (powerset @ X209))|(~(in @ X211 @ X210)|(in @ X211 @ X209)))&(((in @ (esk2_2 @ X212 @ X213) @ X213)|(in @ X213 @ (powerset @ X212)))&(~(in @ (esk2_2 @ X212 @ X213) @ X212)|(in @ X213 @ (powerset @ X212)))))&((setunionAx)&((in @ emptyset @ omega)&((~(in @ X215 @ omega)|(in @ (setadjoin @ X215 @ X215) @ omega))&(((((in @ (esk3_1 @ X216) @ omega)|~(in @ emptyset @ X216)|(~(in @ X218 @ omega)|(in @ X218 @ X216)))&((in @ (esk3_1 @ X216) @ X216)|~(in @ emptyset @ X216)|(~(in @ X218 @ omega)|(in @ X218 @ X216))))&(~(in @ (setadjoin @ (esk3_1 @ X216) @ (esk3_1 @ X216)) @ X216)|~(in @ emptyset @ X216)|(~(in @ X218 @ omega)|(in @ X218 @ X216))))&((((((in @ (esk7_3 @ X219 @ X220 @ X225) @ X220)|~(in @ X225 @ (esk6_2 @ X219 @ X220))|(in @ (esk4_2 @ X219 @ X220) @ X220))&((X219 @ (esk7_3 @ X219 @ X220 @ X225) @ X225)|~(in @ X225 @ (esk6_2 @ X219 @ X220))|(in @ (esk4_2 @ X219 @ X220) @ X220)))&(~(in @ X228 @ X220)|~(X219 @ X228 @ X227)|(in @ X227 @ (esk6_2 @ X219 @ X220))|(in @ (esk4_2 @ X219 @ X220) @ X220)))&(((((in @ (esk7_3 @ X219 @ X220 @ X225) @ X220)|~(in @ X225 @ (esk6_2 @ X219 @ X220))|((X219 @ (esk4_2 @ X219 @ X220) @ (esk5_3 @ X219 @ X220 @ X222))|~(X219 @ (esk4_2 @ X219 @ X220) @ X222)))&((X219 @ (esk7_3 @ X219 @ X220 @ X225) @ X225)|~(in @ X225 @ (esk6_2 @ X219 @ X220))|((X219 @ (esk4_2 @ X219 @ X220) @ (esk5_3 @ X219 @ X220 @ X222))|~(X219 @ (esk4_2 @ X219 @ X220) @ X222))))&(~(in @ X228 @ X220)|~(X219 @ X228 @ X227)|(in @ X227 @ (esk6_2 @ X219 @ X220))|((X219 @ (esk4_2 @ X219 @ X220) @ (esk5_3 @ X219 @ X220 @ X222))|~(X219 @ (esk4_2 @ X219 @ X220) @ X222))))&((((in @ (esk7_3 @ X219 @ X220 @ X225) @ X220)|~(in @ X225 @ (esk6_2 @ X219 @ X220))|(((X222)!=(esk5_3 @ X219 @ X220 @ X222))|~(X219 @ (esk4_2 @ X219 @ X220) @ X222)))&((X219 @ (esk7_3 @ X219 @ X220 @ X225) @ X225)|~(in @ X225 @ (esk6_2 @ X219 @ X220))|(((X222)!=(esk5_3 @ X219 @ X220 @ X222))|~(X219 @ (esk4_2 @ X219 @ X220) @ X222))))&(~(in @ X228 @ X220)|~(X219 @ X228 @ X227)|(in @ X227 @ (esk6_2 @ X219 @ X220))|(((X222)!=(esk5_3 @ X219 @ X220 @ X222))|~(X219 @ (esk4_2 @ X219 @ X220) @ X222))))))&((((in @ (esk8_1 @ X229) @ X229)|~(in @ X230 @ X229))&(~(in @ X232 @ (esk8_1 @ X229))|~(in @ X232 @ X229)|~(in @ X230 @ X229)))&((epred1_0)&((descrp)&((~(in @ X235 @ X233)|(~(X234 @ X235)|(in @ X235 @ (dsetconstr @ X233 @ (^[Z0:$i]:((X234 @ Z0)))))))&((~(in @ X238 @ (dsetconstr @ X236 @ (^[Z0:$i]:((X237 @ Z0)))))|(in @ X238 @ X236))&((~(in @ X241 @ (dsetconstr @ X239 @ (^[Z0:$i]:((X240 @ Z0)))))|(X240 @ X241))&(((((X242 @ (esk10_1 @ X242))|((X242 @ (esk9_2 @ X242 @ X243))|~(X242 @ X243)))&(~(X242 @ X246)|((esk10_1 @ X242)=(X246))|((X242 @ (esk9_2 @ X242 @ X243))|~(X242 @ X243))))&(((X242 @ (esk10_1 @ X242))|(((X243)!=(esk9_2 @ X242 @ X243))|~(X242 @ X243)))&(~(X242 @ X246)|((esk10_1 @ X242)=(X246))|(((X243)!=(esk9_2 @ X242 @ X243))|~(X242 @ X243)))))&((~(in @ X248 @ (dsetconstr @ (powerset @ emptyset) @ (^[Z0:$i]:((X247)))))|(X247))&((~(in @ X249 @ emptyset)|(X250))&(~(in @ X251 @ emptyset)&(~(in @ X252 @ emptyset)&((((X253 @ (esk11_2 @ X253 @ X254))|~(X253 @ X254)|(X253 @ (esk12_1 @ X253)))&(((X254)!=(esk11_2 @ X253 @ X254))|~(X253 @ X254)|(X253 @ (esk12_1 @ X253))))&(((((in @ (esk14_2 @ X257 @ X258) @ X258)|((X257)=(X258))|(in @ (esk13_2 @ X257 @ X258) @ X257))&(~(in @ (esk14_2 @ X257 @ X258) @ X257)|((X257)=(X258))|(in @ (esk13_2 @ X257 @ X258) @ X257)))&(((in @ (esk14_2 @ X257 @ X258) @ X258)|((X257)=(X258))|~(in @ (esk13_2 @ X257 @ X258) @ X258))&(~(in @ (esk14_2 @ X257 @ X258) @ X257)|((X257)=(X258))|~(in @ (esk13_2 @ X257 @ X258) @ X258))))&(((in @ (esk15_1 @ X261) @ X261)|((X261)=(emptyset)))&(((in @ (esk16_1 @ X263) @ X263)|((X263)=(emptyset)))&(((~(in @ X267 @ (dsetconstr @ X265 @ (^[Z0:$i]:((X266 @ Z0)))))|(X266 @ X267)|~(in @ X267 @ X265))&(~(X266 @ X267)|(in @ X267 @ (dsetconstr @ X265 @ (^[Z0:$i]:((X266 @ Z0)))))|~(in @ X267 @ X265)))&((((X268)=(emptyset))|(in @ (esk17_1 @ X268) @ X268))&((~(in @ X272 @ X270)|(~(X271 @ X272)|((dsetconstr @ X270 @ (^[Z0:$i]:((X271 @ Z0))))!=(emptyset))))&((~(in @ X274 @ X273)|((X273)!=(emptyset)))&((in @ X275 @ (setadjoin @ X275 @ X276))&((in @ emptyset @ (setadjoin @ emptyset @ emptyset))&((~(in @ X279 @ X278)|(in @ X279 @ (setadjoin @ X277 @ X278)))&((in @ esk20_0 @ (setadjoin @ esk18_0 @ esk19_0))&((((esk20_0)!=(esk18_0))|(epred2_0))&((~(in @ esk20_0 @ esk19_0)|(epred2_0))&~(epred2_0)))))))))))))))))))))))))))))))))))), inference(distribute,[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_53])])])])])])).
% 0.23/0.29 thf(c_0_55, negated_conjecture, ((epred2_0)|((esk20_0)!=(esk18_0))), inference(split_conjunct,[status(thm)],[c_0_54])).
% 0.23/0.29 thf(c_0_56, negated_conjecture, ~((epred2_0)), inference(split_conjunct,[status(thm)],[c_0_54])).
% 0.23/0.29 thf(c_0_57, negated_conjecture, ((epred2_0)|~((in @ esk20_0 @ esk19_0))), inference(split_conjunct,[status(thm)],[c_0_54])).
% 0.23/0.29 thf(c_0_58, negated_conjecture, ![X2:$i, X3:$i, X4:$i]:((((X2)=(X3))|(in @ X2 @ X4)|~((in @ X2 @ (setadjoin @ X3 @ X4))))), inference(split_conjunct,[status(thm)],[c_0_54])).
% 0.23/0.29 thf(c_0_59, negated_conjecture, (in @ esk20_0 @ (setadjoin @ esk18_0 @ esk19_0)), inference(split_conjunct,[status(thm)],[c_0_54])).
% 0.23/0.29 thf(c_0_60, negated_conjecture, ((esk18_0)!=(esk20_0)), inference(sr,[status(thm)],[c_0_55, c_0_56])).
% 0.23/0.29 thf(c_0_61, negated_conjecture, ~((in @ esk20_0 @ esk19_0)), inference(sr,[status(thm)],[c_0_57, c_0_56])).
% 0.23/0.29 thf(c_0_62, negated_conjecture, ($false), inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_58, c_0_59]), c_0_60]), c_0_61]), ['proof']).
% 0.23/0.29 % SZS output end CNFRefutation
% 0.23/0.29 % Parsed axioms : 77
% 0.23/0.29 % Removed by relevancy pruning/SinE : 44
% 0.23/0.29 % Initial clauses : 72
% 0.23/0.29 % Removed in clause preprocessing : 0
% 0.23/0.29 % Initial clauses in saturation : 72
% 0.23/0.29 % Processed clauses : 64
% 0.23/0.29 % ...of these trivial : 0
% 0.23/0.29 % ...subsumed : 16
% 0.23/0.29 % ...remaining for further processing : 48
% 0.23/0.29 % Other redundant clauses eliminated : 2
% 0.23/0.29 % Clauses deleted for lack of memory : 0
% 0.23/0.29 % Backward-subsumed : 0
% 0.23/0.29 % Backward-rewritten : 3
% 0.23/0.29 % Generated clauses : 87
% 0.23/0.29 % ...of the previous two non-redundant : 67
% 0.23/0.29 % ...aggressively subsumed : 0
% 0.23/0.29 % Contextual simplify-reflections : 0
% 0.23/0.29 % Paramodulations : 85
% 0.23/0.29 % Factorizations : 0
% 0.23/0.29 % NegExts : 0
% 0.23/0.29 % Equation resolutions : 2
% 0.23/0.29 % Disequality decompositions : 0
% 0.23/0.29 % Total rewrite steps : 13
% 0.23/0.29 % ...of those cached : 3
% 0.23/0.29 % Propositional unsat checks : 0
% 0.23/0.29 % Propositional check models : 0
% 0.23/0.29 % Propositional check unsatisfiable : 0
% 0.23/0.29 % Propositional clauses : 0
% 0.23/0.29 % Propositional clauses after purity: 0
% 0.23/0.29 % Propositional unsat core size : 0
% 0.23/0.29 % Propositional preprocessing time : 0.000
% 0.23/0.29 % Propositional encoding time : 0.000
% 0.23/0.29 % Propositional solver time : 0.000
% 0.23/0.29 % Success case prop preproc time : 0.000
% 0.23/0.29 % Success case prop encoding time : 0.000
% 0.23/0.29 % Success case prop solver time : 0.000
% 0.23/0.29 % Current number of processed clauses : 43
% 0.23/0.29 % Positive orientable unit clauses : 12
% 0.23/0.29 % Positive unorientable unit clauses: 0
% 0.23/0.29 % Negative unit clauses : 4
% 0.23/0.29 % Non-unit-clauses : 27
% 0.23/0.29 % Current number of unprocessed clauses: 75
% 0.23/0.29 % ...number of literals in the above : 247
% 0.23/0.29 % Current number of archived formulas : 0
% 0.23/0.29 % Current number of archived clauses : 3
% 0.23/0.29 % Clause-clause subsumption calls (NU) : 177
% 0.23/0.29 % Rec. Clause-clause subsumption calls : 162
% 0.23/0.29 % Non-unit clause-clause subsumptions : 8
% 0.23/0.29 % Unit Clause-clause subsumption calls : 32
% 0.23/0.29 % Rewrite failures with RHS unbound : 0
% 0.23/0.29 % BW rewrite match attempts : 8
% 0.23/0.29 % BW rewrite match successes : 3
% 0.23/0.29 % Condensation attempts : 0
% 0.23/0.29 % Condensation successes : 0
% 0.23/0.29 % Termbank termtop insertions : 8754
% 0.23/0.29 % Search garbage collected termcells : 2821
% 0.23/0.29
% 0.23/0.29 % -------------------------------------------------
% 0.23/0.29 % User time : 0.010 s
% 0.23/0.29 % System time : 0.003 s
% 0.23/0.29 % Total time : 0.013 s
% 0.23/0.29 % Maximum resident set size: 4484 pages
% 0.23/0.29
% 0.23/0.29 % -------------------------------------------------
% 0.23/0.29 % User time : 0.014 s
% 0.23/0.29 % System time : 0.006 s
% 0.23/0.29 % Total time : 0.021 s
% 0.23/0.29 % Maximum resident set size: 4864 pages
% 0.23/0.29 % E exiting
%------------------------------------------------------------------------------