%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : SEU820^2 : 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 : n001.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:25:46 AM UTC 2026
% Result : Theorem 0.21s 0.27s
% Output : CNFRefutation 0.21s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU820^2 : 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 : n001.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 14:40:35 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.24 Running higher-order theorem proving
% 0.08/0.25 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.T0KnFb004D/E---3.1_1335253.p
% 0.21/0.27 % Version: 3.5.1-ho
% 0.21/0.27 % partial match(1): HSSSSLSSSLSNSFA
% 0.21/0.27 % Preprocessing class: HSSSSLSSMLSNSFA.
% 0.21/0.27 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.21/0.27 % Starting post_as_ho5 with 1500s (5) cores
% 0.21/0.27 % Starting post_as_ho10 with 300s (1) cores
% 0.21/0.27 % Starting post_as_ho4 with 300s (1) cores
% 0.21/0.27 % Starting sh5l with 300s (1) cores
% 0.21/0.27 % post_as_ho10 with pid 1335282 completed with status 0
% 0.21/0.27 % Result found by post_as_ho10
% 0.21/0.27 % partial match(1): HSSSSLSSSLSNSFA
% 0.21/0.27 % Preprocessing class: HSSSSLSSMLSNSFA.
% 0.21/0.27 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.21/0.27 % Starting post_as_ho5 with 1500s (5) cores
% 0.21/0.27 % Starting post_as_ho10 with 300s (1) cores
% 0.21/0.27 % (lift_lambdas = 0, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.21/0.27 % No SInE strategy applied
% 0.21/0.27 % Search class: HGUSF-FFMM11-SSFSMFBN
% 0.21/0.27 % partial match(4): HGHSF-FFMM11-SSSFFFBN
% 0.21/0.27 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 0.21/0.27 % Starting SubtermCWHack with 28s (1) cores
% 0.21/0.27 % SubtermCWHack with pid 1335292 completed with status 0
% 0.21/0.27 % Result found by SubtermCWHack
% 0.21/0.27 % partial match(1): HSSSSLSSSLSNSFA
% 0.21/0.27 % Preprocessing class: HSSSSLSSMLSNSFA.
% 0.21/0.27 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.21/0.27 % Starting post_as_ho5 with 1500s (5) cores
% 0.21/0.27 % Starting post_as_ho10 with 300s (1) cores
% 0.21/0.27 % (lift_lambdas = 0, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.21/0.27 % No SInE strategy applied
% 0.21/0.27 % Search class: HGUSF-FFMM11-SSFSMFBN
% 0.21/0.27 % partial match(4): HGHSF-FFMM11-SSSFFFBN
% 0.21/0.27 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 0.21/0.27 % Starting SubtermCWHack with 28s (1) cores
% 0.21/0.27 % Preprocessing time : 0.002 s
% 0.21/0.27
% 0.21/0.27 % Proof found!
% 0.21/0.27 % SZS status Theorem
% 0.21/0.27 % SZS output start CNFRefutation
% 0.21/0.27 thf(decl_23, type, in: $i > $i > $o).
% 0.21/0.27 thf(decl_24, type, emptyset: $i).
% 0.21/0.27 thf(decl_25, type, powerset: $i > $i).
% 0.21/0.27 thf(decl_26, type, nonempty: $i > $o).
% 0.21/0.27 thf(decl_27, type, vacuousDall: $o).
% 0.21/0.27 thf(decl_28, type, subset: $i > $i > $o).
% 0.21/0.27 thf(decl_29, type, subsetemptysetimpeq: $o).
% 0.21/0.27 thf(decl_30, type, powersetE1: $o).
% 0.21/0.27 thf(decl_31, type, transitiveset: $i > $o).
% 0.21/0.27 thf(decl_32, type, stricttotalorderedByIn: $i > $o).
% 0.21/0.27 thf(decl_33, type, wellorderedByIn: $i > $o).
% 0.21/0.27 thf(decl_34, type, ordinal: $i > $o).
% 0.21/0.27 thf(decl_35, type, epred1_0: $o).
% 0.21/0.27 thf(decl_36, type, esk1_0: $i).
% 0.21/0.27 thf(decl_37, type, esk2_0: $i).
% 0.21/0.27 thf(decl_38, type, esk3_0: $i).
% 0.21/0.27 thf(decl_39, type, esk4_1: $i > $i).
% 0.21/0.27 thf(decl_40, type, esk5_0: $i).
% 0.21/0.27 thf(decl_41, type, esk6_0: $i).
% 0.21/0.27 thf(decl_42, type, esk7_0: $i).
% 0.21/0.27 thf(decl_43, type, esk8_0: $i).
% 0.21/0.27 thf(decl_44, type, esk9_0: $i).
% 0.21/0.27 thf(wellorderedByIn, axiom, ((wellorderedByIn)=(^[X3:$i]:((((stricttotalorderedByIn @ X3))&(![X5:$i]:((((in @ X5 @ (powerset @ X3)))=>((((nonempty @ X5))=>(?[X1:$i]:((((in @ X1 @ X5))&(![X6:$i]:((((in @ X6 @ X5))=>(((((X1)=(X6)))|((in @ X1 @ X6))))))))))))))))))), file('/export/starexec/sandbox2/tmp/tmp.T0KnFb004D/E---3.1_1335253.p', wellorderedByIn)).
% 0.21/0.27 thf(nonempty, axiom, ((nonempty)=(^[X1:$i]:(((X1)!=(emptyset))))), file('/export/starexec/sandbox2/tmp/tmp.T0KnFb004D/E---3.1_1335253.p', nonempty)).
% 0.21/0.27 thf(stricttotalorderedByIn, axiom, ((stricttotalorderedByIn)=(^[X3:$i]:(((((![X1:$i]:((((in @ X1 @ X3))=>(![X5:$i]:((((in @ X5 @ X3))=>(![X6:$i]:((((in @ X6 @ X3))=>((((((in @ X1 @ X5))&((in @ X5 @ X6))))=>((in @ X1 @ X6)))))))))))))&(![X5:$i]:((((in @ X5 @ X3))=>(![X6:$i]:((((in @ X6 @ X3))=>(((((((X5)=(X6)))|((in @ X5 @ X6))))|((in @ X6 @ X5))))))))))))&(![X5:$i]:((((in @ X5 @ X3))=>(~((in @ X5 @ X5)))))))))), file('/export/starexec/sandbox2/tmp/tmp.T0KnFb004D/E---3.1_1335253.p', stricttotalorderedByIn)).
% 0.21/0.27 thf(ordinal, axiom, ((ordinal)=(^[X1:$i]:((((transitiveset @ X1))&((wellorderedByIn @ X1)))))), file('/export/starexec/sandbox2/tmp/tmp.T0KnFb004D/E---3.1_1335253.p', ordinal)).
% 0.21/0.27 thf(transitiveset, axiom, ((transitiveset)=(^[X3:$i]:(![X5:$i]:((((in @ X5 @ X3))=>((subset @ X5 @ X3))))))), file('/export/starexec/sandbox2/tmp/tmp.T0KnFb004D/E---3.1_1335253.p', transitiveset)).
% 0.21/0.27 thf(emptysetOrdinal, conjecture, ((vacuousDall)=>((subsetemptysetimpeq)=>((powersetE1)=>(ordinal @ emptyset)))), file('/export/starexec/sandbox2/tmp/tmp.T0KnFb004D/E---3.1_1335253.p', emptysetOrdinal)).
% 0.21/0.27 thf(vacuousDall, axiom, ((vacuousDall)<=>![X2:$i > $o, X1:$i]:(((in @ X1 @ emptyset)=>(X2 @ X1)))), file('/export/starexec/sandbox2/tmp/tmp.T0KnFb004D/E---3.1_1335253.p', vacuousDall)).
% 0.21/0.27 thf(subsetemptysetimpeq, axiom, ((subsetemptysetimpeq)<=>![X3:$i]:(((subset @ X3 @ emptyset)=>((X3)=(emptyset))))), file('/export/starexec/sandbox2/tmp/tmp.T0KnFb004D/E---3.1_1335253.p', subsetemptysetimpeq)).
% 0.21/0.27 thf(powersetE1, axiom, ((powersetE1)<=>![X3:$i, X4:$i]:(((in @ X4 @ (powerset @ X3))=>(subset @ X4 @ X3)))), file('/export/starexec/sandbox2/tmp/tmp.T0KnFb004D/E---3.1_1335253.p', powersetE1)).
% 0.21/0.27 thf(c_0_9, plain, ((wellorderedByIn)=(^[Z0:$i]:((((((((![X12:$i]:((((in @ X12 @ Z0))=>(![X13:$i]:((((in @ X13 @ Z0))=>(![X14:$i]:((((in @ X14 @ Z0))=>((((((in @ X12 @ X13))&((in @ X13 @ X14))))=>((in @ X12 @ X14)))))))))))))&(![X15:$i]:((((in @ X15 @ Z0))=>(![X16:$i]:((((in @ X16 @ Z0))=>(((((((X15)=(X16)))|((in @ X15 @ X16))))|((in @ X16 @ X15))))))))))))&(![X17:$i]:((((in @ X17 @ Z0))=>(~((in @ X17 @ X17)))))))))&(![X5:$i]:((((in @ X5 @ (powerset @ Z0)))=>((((((X5)!=(emptyset))))=>(?[X1:$i]:((((in @ X1 @ X5))&(![X6:$i]:((((in @ X6 @ X5))=>(((((X1)=(X6)))|((in @ X1 @ X6))))))))))))))))))), inference(fof_simplification,[status(thm)],[wellorderedByIn])).
% 0.21/0.27 thf(c_0_10, plain, ((nonempty)=(^[Z0:$i]:(((Z0)!=(emptyset))))), inference(fof_simplification,[status(thm)],[nonempty])).
% 0.21/0.27 thf(c_0_11, plain, ((stricttotalorderedByIn)=(^[Z0:$i]:(((((![X1:$i]:((((in @ X1 @ Z0))=>(![X5:$i]:((((in @ X5 @ Z0))=>(![X6:$i]:((((in @ X6 @ Z0))=>((((((in @ X1 @ X5))&((in @ X5 @ X6))))=>((in @ X1 @ X6)))))))))))))&(![X5:$i]:((((in @ X5 @ Z0))=>(![X6:$i]:((((in @ X6 @ Z0))=>(((((((X5)=(X6)))|((in @ X5 @ X6))))|((in @ X6 @ X5))))))))))))&(![X5:$i]:((((in @ X5 @ Z0))=>(~((in @ X5 @ X5)))))))))), inference(fof_simplification,[status(thm)],[stricttotalorderedByIn])).
% 0.21/0.27 thf(c_0_12, plain, ((ordinal)=(^[Z0:$i]:((((![X18:$i]:((((in @ X18 @ Z0))=>((subset @ X18 @ Z0))))))&(((((((((![X19:$i]:((((in @ X19 @ Z0))=>(![X20:$i]:((((in @ X20 @ Z0))=>(![X21:$i]:((((in @ X21 @ Z0))=>((((((in @ X19 @ X20))&((in @ X20 @ X21))))=>((in @ X19 @ X21)))))))))))))&(![X22:$i]:((((in @ X22 @ Z0))=>(![X23:$i]:((((in @ X23 @ Z0))=>(((((((X22)=(X23)))|((in @ X22 @ X23))))|((in @ X23 @ X22))))))))))))&(![X24:$i]:((((in @ X24 @ Z0))=>(~((in @ X24 @ X24)))))))))&(![X25:$i]:((((in @ X25 @ (powerset @ Z0)))=>((((((X25)!=(emptyset))))=>(?[X26:$i]:((((in @ X26 @ X25))&(![X27:$i]:((((in @ X27 @ X25))=>(((((X26)=(X27)))|((in @ X26 @ X27)))))))))))))))))))))), inference(fof_simplification,[status(thm)],[ordinal])).
% 0.21/0.27 thf(c_0_13, plain, ((transitiveset)=(^[Z0:$i]:(![X5:$i]:((((in @ X5 @ Z0))=>((subset @ X5 @ Z0))))))), inference(fof_simplification,[status(thm)],[transitiveset])).
% 0.21/0.27 thf(c_0_14, plain, ((wellorderedByIn)=(^[Z0:$i]:((((((((![X12:$i]:((((in @ X12 @ Z0))=>(![X13:$i]:((((in @ X13 @ Z0))=>(![X14:$i]:((((in @ X14 @ Z0))=>((((((in @ X12 @ X13))&((in @ X13 @ X14))))=>((in @ X12 @ X14)))))))))))))&(![X15:$i]:((((in @ X15 @ Z0))=>(![X16:$i]:((((in @ X16 @ Z0))=>(((((((X15)=(X16)))|((in @ X15 @ X16))))|((in @ X16 @ X15))))))))))))&(![X17:$i]:((((in @ X17 @ Z0))=>(~((in @ X17 @ X17)))))))))&(![X5:$i]:((((in @ X5 @ (powerset @ Z0)))=>((((((X5)!=(emptyset))))=>(?[X1:$i]:((((in @ X1 @ X5))&(![X6:$i]:((((in @ X6 @ X5))=>(((((X1)=(X6)))|((in @ X1 @ X6))))))))))))))))))), inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[c_0_9, c_0_10]), c_0_11])).
% 0.21/0.27 thf(c_0_15, negated_conjecture, ~(((vacuousDall)=>((subsetemptysetimpeq)=>((powersetE1)=>(ordinal @ emptyset))))), inference(assume_negation,[status(cth)],[emptysetOrdinal])).
% 0.21/0.27 thf(c_0_16, plain, ((ordinal)=(^[Z0:$i]:((((![X18:$i]:((((in @ X18 @ Z0))=>((subset @ X18 @ Z0))))))&(((((((((![X19:$i]:((((in @ X19 @ Z0))=>(![X20:$i]:((((in @ X20 @ Z0))=>(![X21:$i]:((((in @ X21 @ Z0))=>((((((in @ X19 @ X20))&((in @ X20 @ X21))))=>((in @ X19 @ X21)))))))))))))&(![X22:$i]:((((in @ X22 @ Z0))=>(![X23:$i]:((((in @ X23 @ Z0))=>(((((((X22)=(X23)))|((in @ X22 @ X23))))|((in @ X23 @ X22))))))))))))&(![X24:$i]:((((in @ X24 @ Z0))=>(~((in @ X24 @ X24)))))))))&(![X25:$i]:((((in @ X25 @ (powerset @ Z0)))=>((((((X25)!=(emptyset))))=>(?[X26:$i]:((((in @ X26 @ X25))&(![X27:$i]:((((in @ X27 @ X25))=>(((((X26)=(X27)))|((in @ X26 @ X27)))))))))))))))))))))), inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[c_0_12, c_0_13]), c_0_14])).
% 0.21/0.27 thf(c_0_17, plain, ((epred1_0)<=>(![X34:$i]:(((in @ X34 @ emptyset)=>![X35:$i]:(((in @ X35 @ emptyset)=>![X36:$i]:(((in @ X36 @ emptyset)=>(((in @ X34 @ X35)&(in @ X35 @ X36))=>(in @ X34 @ X36))))))))&![X37:$i]:(((in @ X37 @ emptyset)=>![X38:$i]:(((in @ X38 @ emptyset)=>(((X37)=(X38))|(in @ X37 @ X38)|(in @ X38 @ X37)))))))), introduced(definition)).
% 0.21/0.27 thf(c_0_18, negated_conjecture, ~((![X28:$i > $o, X29:$i]:(((in @ X29 @ emptyset)=>(X28 @ X29)))=>(![X30:$i]:(((subset @ X30 @ emptyset)=>((X30)=(emptyset))))=>(![X31:$i, X32:$i]:(((in @ X32 @ (powerset @ X31))=>(subset @ X32 @ X31)))=>(![X33:$i]:(((in @ X33 @ emptyset)=>(subset @ X33 @ emptyset)))&(((epred1_0)&![X39:$i]:(((in @ X39 @ emptyset)=>~(in @ X39 @ X39))))&![X40:$i]:(((in @ X40 @ (powerset @ emptyset))=>(((X40)!=(emptyset))=>?[X41:$i]:(((in @ X41 @ X40)&![X42:$i]:(((in @ X42 @ X40)=>(((X41)=(X42))|(in @ X41 @ X42))))))))))))))), 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)],[c_0_15, vacuousDall]), subsetemptysetimpeq]), powersetE1]), c_0_16])]), c_0_17])).
% 0.21/0.27 thf(c_0_19, plain, ((![X34:$i]:(((in @ X34 @ emptyset)=>![X35:$i]:(((in @ X35 @ emptyset)=>![X36:$i]:(((in @ X36 @ emptyset)=>(((in @ X34 @ X35)&(in @ X35 @ X36))=>(in @ X34 @ X36))))))))&![X37:$i]:(((in @ X37 @ emptyset)=>![X38:$i]:(((in @ X38 @ emptyset)=>(((X37)=(X38))|(in @ X37 @ X38)|(in @ X38 @ X37)))))))=>(epred1_0)), inference(split_equiv,[status(thm)],[c_0_17])).
% 0.21/0.27 thf(c_0_20, negated_conjecture, ![X43:$i > $o, X44:$i, X45:$i, X46:$i, X47:$i, X51:$i]:(((~(in @ X44 @ emptyset)|(X43 @ X44))&((~(subset @ X45 @ emptyset)|((X45)=(emptyset)))&((~(in @ X47 @ (powerset @ X46))|(subset @ X47 @ X46))&(((((in @ esk3_0 @ (powerset @ emptyset))|((in @ esk2_0 @ emptyset)|~(epred1_0))|(in @ esk1_0 @ emptyset))&((((esk3_0)!=(emptyset))|((in @ esk2_0 @ emptyset)|~(epred1_0))|(in @ esk1_0 @ emptyset))&(((in @ (esk4_1 @ X51) @ esk3_0)|~(in @ X51 @ esk3_0)|((in @ esk2_0 @ emptyset)|~(epred1_0))|(in @ esk1_0 @ emptyset))&((((X51)!=(esk4_1 @ X51))|~(in @ X51 @ esk3_0)|((in @ esk2_0 @ emptyset)|~(epred1_0))|(in @ esk1_0 @ emptyset))&(~(in @ X51 @ (esk4_1 @ X51))|~(in @ X51 @ esk3_0)|((in @ esk2_0 @ emptyset)|~(epred1_0))|(in @ esk1_0 @ emptyset))))))&(((in @ esk3_0 @ (powerset @ emptyset))|((in @ esk2_0 @ esk2_0)|~(epred1_0))|(in @ esk1_0 @ emptyset))&((((esk3_0)!=(emptyset))|((in @ esk2_0 @ esk2_0)|~(epred1_0))|(in @ esk1_0 @ emptyset))&(((in @ (esk4_1 @ X51) @ esk3_0)|~(in @ X51 @ esk3_0)|((in @ esk2_0 @ esk2_0)|~(epred1_0))|(in @ esk1_0 @ emptyset))&((((X51)!=(esk4_1 @ X51))|~(in @ X51 @ esk3_0)|((in @ esk2_0 @ esk2_0)|~(epred1_0))|(in @ esk1_0 @ emptyset))&(~(in @ X51 @ (esk4_1 @ X51))|~(in @ X51 @ esk3_0)|((in @ esk2_0 @ esk2_0)|~(epred1_0))|(in @ esk1_0 @ emptyset)))))))&((((in @ esk3_0 @ (powerset @ emptyset))|((in @ esk2_0 @ emptyset)|~(epred1_0))|~(subset @ esk1_0 @ emptyset))&((((esk3_0)!=(emptyset))|((in @ esk2_0 @ emptyset)|~(epred1_0))|~(subset @ esk1_0 @ emptyset))&(((in @ (esk4_1 @ X51) @ esk3_0)|~(in @ X51 @ esk3_0)|((in @ esk2_0 @ emptyset)|~(epred1_0))|~(subset @ esk1_0 @ emptyset))&((((X51)!=(esk4_1 @ X51))|~(in @ X51 @ esk3_0)|((in @ esk2_0 @ emptyset)|~(epred1_0))|~(subset @ esk1_0 @ emptyset))&(~(in @ X51 @ (esk4_1 @ X51))|~(in @ X51 @ esk3_0)|((in @ esk2_0 @ emptyset)|~(epred1_0))|~(subset @ esk1_0 @ emptyset))))))&(((in @ esk3_0 @ (powerset @ emptyset))|((in @ esk2_0 @ esk2_0)|~(epred1_0))|~(subset @ esk1_0 @ emptyset))&((((esk3_0)!=(emptyset))|((in @ esk2_0 @ esk2_0)|~(epred1_0))|~(subset @ esk1_0 @ emptyset))&(((in @ (esk4_1 @ X51) @ esk3_0)|~(in @ X51 @ esk3_0)|((in @ esk2_0 @ esk2_0)|~(epred1_0))|~(subset @ esk1_0 @ emptyset))&((((X51)!=(esk4_1 @ X51))|~(in @ X51 @ esk3_0)|((in @ esk2_0 @ esk2_0)|~(epred1_0))|~(subset @ esk1_0 @ emptyset))&(~(in @ X51 @ (esk4_1 @ X51))|~(in @ X51 @ esk3_0)|((in @ esk2_0 @ esk2_0)|~(epred1_0))|~(subset @ esk1_0 @ 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_18])])])])])])).
% 0.21/0.27 thf(c_0_21, plain, ((((in @ esk8_0 @ emptyset)|(in @ esk5_0 @ emptyset)|(epred1_0))&(((in @ esk9_0 @ emptyset)|(in @ esk5_0 @ emptyset)|(epred1_0))&(((((esk8_0)!=(esk9_0))|(in @ esk5_0 @ emptyset)|(epred1_0))&(~(in @ esk8_0 @ esk9_0)|(in @ esk5_0 @ emptyset)|(epred1_0)))&(~(in @ esk9_0 @ esk8_0)|(in @ esk5_0 @ emptyset)|(epred1_0)))))&((((in @ esk8_0 @ emptyset)|(in @ esk6_0 @ emptyset)|(epred1_0))&(((in @ esk9_0 @ emptyset)|(in @ esk6_0 @ emptyset)|(epred1_0))&(((((esk8_0)!=(esk9_0))|(in @ esk6_0 @ emptyset)|(epred1_0))&(~(in @ esk8_0 @ esk9_0)|(in @ esk6_0 @ emptyset)|(epred1_0)))&(~(in @ esk9_0 @ esk8_0)|(in @ esk6_0 @ emptyset)|(epred1_0)))))&((((in @ esk8_0 @ emptyset)|(in @ esk7_0 @ emptyset)|(epred1_0))&(((in @ esk9_0 @ emptyset)|(in @ esk7_0 @ emptyset)|(epred1_0))&(((((esk8_0)!=(esk9_0))|(in @ esk7_0 @ emptyset)|(epred1_0))&(~(in @ esk8_0 @ esk9_0)|(in @ esk7_0 @ emptyset)|(epred1_0)))&(~(in @ esk9_0 @ esk8_0)|(in @ esk7_0 @ emptyset)|(epred1_0)))))&(((((in @ esk8_0 @ emptyset)|(in @ esk5_0 @ esk6_0)|(epred1_0))&(((in @ esk9_0 @ emptyset)|(in @ esk5_0 @ esk6_0)|(epred1_0))&(((((esk8_0)!=(esk9_0))|(in @ esk5_0 @ esk6_0)|(epred1_0))&(~(in @ esk8_0 @ esk9_0)|(in @ esk5_0 @ esk6_0)|(epred1_0)))&(~(in @ esk9_0 @ esk8_0)|(in @ esk5_0 @ esk6_0)|(epred1_0)))))&(((in @ esk8_0 @ emptyset)|(in @ esk6_0 @ esk7_0)|(epred1_0))&(((in @ esk9_0 @ emptyset)|(in @ esk6_0 @ esk7_0)|(epred1_0))&(((((esk8_0)!=(esk9_0))|(in @ esk6_0 @ esk7_0)|(epred1_0))&(~(in @ esk8_0 @ esk9_0)|(in @ esk6_0 @ esk7_0)|(epred1_0)))&(~(in @ esk9_0 @ esk8_0)|(in @ esk6_0 @ esk7_0)|(epred1_0))))))&(((in @ esk8_0 @ emptyset)|~(in @ esk5_0 @ esk7_0)|(epred1_0))&(((in @ esk9_0 @ emptyset)|~(in @ esk5_0 @ esk7_0)|(epred1_0))&(((((esk8_0)!=(esk9_0))|~(in @ esk5_0 @ esk7_0)|(epred1_0))&(~(in @ esk8_0 @ esk9_0)|~(in @ esk5_0 @ esk7_0)|(epred1_0)))&(~(in @ esk9_0 @ esk8_0)|~(in @ esk5_0 @ esk7_0)|(epred1_0))))))))), inference(distribute,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_19])])])])])).
% 0.21/0.27 thf(c_0_22, negated_conjecture, ![X2:$i > $o, X1:$i]:(((X2 @ X1)|~((in @ X1 @ emptyset)))), inference(split_conjunct,[status(thm)],[c_0_20])).
% 0.21/0.27 thf(c_0_23, plain, ((in @ esk9_0 @ emptyset)|(in @ esk7_0 @ emptyset)|(epred1_0)), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.21/0.27 thf(c_0_24, negated_conjecture, ![X2:$i > $o]:(((in @ esk9_0 @ emptyset)|(X2 @ esk7_0)|(epred1_0))), inference(spm,[status(thm)],[c_0_22, c_0_23])).
% 0.21/0.27 thf(c_0_25, plain, ((in @ esk7_0 @ emptyset)|(epred1_0)|~((in @ esk8_0 @ esk9_0))), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.21/0.27 thf(c_0_26, negated_conjecture, ![X2:$i > $o, X7:$i > $o]:(((X2 @ esk7_0)|(X7 @ esk9_0)|(epred1_0))), inference(spm,[status(thm)],[c_0_22, c_0_24])).
% 0.21/0.27 thf(c_0_27, plain, ((in @ esk9_0 @ emptyset)|(epred1_0)|~((in @ esk5_0 @ esk7_0))), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.21/0.27 thf(c_0_28, negated_conjecture, ![X2:$i > $o]:(((X2 @ esk7_0)|(epred1_0))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_22, c_0_25]), c_0_26])).
% 0.21/0.27 thf(c_0_29, plain, ((in @ esk9_0 @ emptyset)|(epred1_0)), inference(csr,[status(thm)],[c_0_27, c_0_28])).
% 0.21/0.27 thf(c_0_30, plain, ((epred1_0)|~((in @ esk8_0 @ esk9_0))|~((in @ esk5_0 @ esk7_0))), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.21/0.27 thf(c_0_31, negated_conjecture, ![X2:$i > $o]:(((X2 @ esk9_0)|(epred1_0))), inference(spm,[status(thm)],[c_0_22, c_0_29])).
% 0.21/0.27 thf(c_0_32, negated_conjecture, ((in @ esk3_0 @ (powerset @ emptyset))|(in @ esk2_0 @ emptyset)|(in @ esk1_0 @ emptyset)|~((epred1_0))), inference(split_conjunct,[status(thm)],[c_0_20])).
% 0.21/0.27 thf(c_0_33, plain, (epred1_0), inference(csr,[status(thm)],[inference(csr,[status(thm)],[c_0_30, c_0_31]), c_0_28])).
% 0.21/0.27 thf(c_0_34, negated_conjecture, ![X1:$i, X3:$i]:(((subset @ X1 @ X3)|~((in @ X1 @ (powerset @ X3))))), inference(split_conjunct,[status(thm)],[c_0_20])).
% 0.21/0.27 thf(c_0_35, negated_conjecture, ((in @ esk3_0 @ (powerset @ emptyset))|(in @ esk2_0 @ emptyset)|(in @ esk1_0 @ emptyset)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_32, c_0_33])])).
% 0.21/0.27 thf(c_0_36, negated_conjecture, ((in @ esk2_0 @ emptyset)|(in @ esk1_0 @ emptyset)|((esk3_0)!=(emptyset))|~((epred1_0))), inference(split_conjunct,[status(thm)],[c_0_20])).
% 0.21/0.27 thf(c_0_37, negated_conjecture, ![X1:$i]:((((X1)=(emptyset))|~((subset @ X1 @ emptyset)))), inference(split_conjunct,[status(thm)],[c_0_20])).
% 0.21/0.27 thf(c_0_38, negated_conjecture, ((in @ esk1_0 @ emptyset)|(in @ esk2_0 @ emptyset)|(subset @ esk3_0 @ emptyset)), inference(spm,[status(thm)],[c_0_34, c_0_35])).
% 0.21/0.27 thf(c_0_39, negated_conjecture, ((in @ esk1_0 @ emptyset)|(in @ esk2_0 @ emptyset)|((esk3_0)!=(emptyset))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_36, c_0_33])])).
% 0.21/0.27 thf(c_0_40, negated_conjecture, ((in @ esk2_0 @ emptyset)|(in @ esk1_0 @ emptyset)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_37, c_0_38]), c_0_39])).
% 0.21/0.27 thf(c_0_41, negated_conjecture, ![X2:$i > $o]:(((in @ esk2_0 @ emptyset)|(X2 @ esk1_0))), inference(spm,[status(thm)],[c_0_22, c_0_40])).
% 0.21/0.27 thf(c_0_42, negated_conjecture, ($false), inference(flex_resolve,[status(thm)],[inference(spm,[status(thm)],[c_0_22, c_0_41])]), ['proof']).
% 0.21/0.27 % SZS output end CNFRefutation
% 0.21/0.27 % Parsed axioms : 21
% 0.21/0.27 % Removed by relevancy pruning/SinE : 0
% 0.21/0.27 % Initial clauses : 65
% 0.21/0.27 % Removed in clause preprocessing : 12
% 0.21/0.27 % Initial clauses in saturation : 53
% 0.21/0.27 % Processed clauses : 70
% 0.21/0.27 % ...of these trivial : 1
% 0.21/0.27 % ...subsumed : 5
% 0.21/0.27 % ...remaining for further processing : 63
% 0.21/0.27 % Other redundant clauses eliminated : 0
% 0.21/0.27 % Clauses deleted for lack of memory : 0
% 0.21/0.27 % Backward-subsumed : 36
% 0.21/0.27 % Backward-rewritten : 17
% 0.21/0.27 % Generated clauses : 31
% 0.21/0.27 % ...of the previous two non-redundant : 34
% 0.21/0.27 % ...aggressively subsumed : 0
% 0.21/0.27 % Contextual simplify-reflections : 11
% 0.21/0.27 % Paramodulations : 31
% 0.21/0.27 % Factorizations : 0
% 0.21/0.27 % NegExts : 0
% 0.21/0.27 % Equation resolutions : 0
% 0.21/0.27 % Disequality decompositions : 0
% 0.21/0.27 % Total rewrite steps : 20
% 0.21/0.27 % ...of those cached : 19
% 0.21/0.27 % Propositional unsat checks : 0
% 0.21/0.27 % Propositional check models : 0
% 0.21/0.27 % Propositional check unsatisfiable : 0
% 0.21/0.27 % Propositional clauses : 0
% 0.21/0.27 % Propositional clauses after purity: 0
% 0.21/0.27 % Propositional unsat core size : 0
% 0.21/0.27 % Propositional preprocessing time : 0.000
% 0.21/0.27 % Propositional encoding time : 0.000
% 0.21/0.27 % Propositional solver time : 0.000
% 0.21/0.27 % Success case prop preproc time : 0.000
% 0.21/0.27 % Success case prop encoding time : 0.000
% 0.21/0.27 % Success case prop solver time : 0.000
% 0.21/0.27 % Current number of processed clauses : 10
% 0.21/0.27 % Positive orientable unit clauses : 1
% 0.21/0.27 % Positive unorientable unit clauses: 0
% 0.21/0.27 % Negative unit clauses : 0
% 0.21/0.27 % Non-unit-clauses : 9
% 0.21/0.27 % Current number of unprocessed clauses: 15
% 0.21/0.27 % ...number of literals in the above : 72
% 0.21/0.27 % Current number of archived formulas : 0
% 0.21/0.27 % Current number of archived clauses : 53
% 0.21/0.27 % Clause-clause subsumption calls (NU) : 495
% 0.21/0.27 % Rec. Clause-clause subsumption calls : 258
% 0.21/0.27 % Non-unit clause-clause subsumptions : 52
% 0.21/0.27 % Unit Clause-clause subsumption calls : 0
% 0.21/0.27 % Rewrite failures with RHS unbound : 0
% 0.21/0.27 % BW rewrite match attempts : 1
% 0.21/0.27 % BW rewrite match successes : 1
% 0.21/0.27 % Condensation attempts : 0
% 0.21/0.27 % Condensation successes : 0
% 0.21/0.27 % Termbank termtop insertions : 4281
% 0.21/0.27 % Search garbage collected termcells : 780
% 0.21/0.27
% 0.21/0.27 % -------------------------------------------------
% 0.21/0.27 % User time : 0.010 s
% 0.21/0.27 % System time : 0.003 s
% 0.21/0.27 % Total time : 0.013 s
% 0.21/0.27 % Maximum resident set size: 3648 pages
% 0.21/0.27
% 0.21/0.27 % -------------------------------------------------
% 0.21/0.27 % User time : 0.013 s
% 0.21/0.27 % System time : 0.007 s
% 0.21/0.27 % Total time : 0.020 s
% 0.21/0.27 % Maximum resident set size: 4864 pages
% 0.21/0.27 % E exiting
%------------------------------------------------------------------------------