%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : SEU818^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 : n004.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:45 AM UTC 2026
% Result : Theorem 0.13s 0.23s
% Output : CNFRefutation 0.13s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU818^2 : TPTP v9.3.1. Released v3.7.0.
% 0.00/0.04 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.16 % Computer : n004.cluster.edu
% 0.13/0.16 % Model : x86_64 x86_64
% 0.13/0.16 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.16 % Memory : 8046.5625MB
% 0.13/0.16 % OS : Linux 6.8.0-71-generic
% 0.13/0.16 % CPULimit : 300
% 0.13/0.16 % WCLimit : 300
% 0.13/0.16 % DateTime : Tue Sep 29 14:34:21 UTC 2026
% 0.13/0.16 % CPUTime :
% 0.13/0.16 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.20 Running higher-order theorem proving
% 0.13/0.21 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.A13u6GLM3x/E---3.1_1370492.p
% 0.13/0.23 % Version: 3.5.1-ho
% 0.13/0.23 % Preprocessing class: HSSSSLSSSLSNSFN.
% 0.13/0.23 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.13/0.23 % Starting new_ho_10 with 1500s (5) cores
% 0.13/0.23 % Starting ehoh_best_sine_rwall with 300s (1) cores
% 0.13/0.23 % Starting lpo1_def_fix with 300s (1) cores
% 0.13/0.23 % Starting ehoh_best8_lambda with 300s (1) cores
% 0.13/0.23 % ehoh_best_sine_rwall with pid 1370506 completed with status 0
% 0.13/0.23 % Result found by ehoh_best_sine_rwall
% 0.13/0.23 % Preprocessing class: HSSSSLSSSLSNSFN.
% 0.13/0.23 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.13/0.23 % Starting new_ho_10 with 1500s (5) cores
% 0.13/0.23 % Starting ehoh_best_sine_rwall with 300s (1) cores
% 0.13/0.23 % (lift_lambdas = 0, lambda_to_forall = 1,unroll_only_formulas = 0, sine = gf500_gu_R04_F100_L20000)
% 0.13/0.23 % SinE strategy is gf500_gu_R04_F100_L20000
% 0.13/0.23 % Search class: HGHSF-FFMF21-SSFFMFNN
% 0.13/0.23 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 0.13/0.23 % Starting SubtermCWHack with 28s (1) cores
% 0.13/0.23 % SubtermCWHack with pid 1370509 completed with status 0
% 0.13/0.23 % Result found by SubtermCWHack
% 0.13/0.23 % Preprocessing class: HSSSSLSSSLSNSFN.
% 0.13/0.23 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.13/0.23 % Starting new_ho_10 with 1500s (5) cores
% 0.13/0.23 % Starting ehoh_best_sine_rwall with 300s (1) cores
% 0.13/0.23 % (lift_lambdas = 0, lambda_to_forall = 1,unroll_only_formulas = 0, sine = gf500_gu_R04_F100_L20000)
% 0.13/0.23 % SinE strategy is gf500_gu_R04_F100_L20000
% 0.13/0.23 % Search class: HGHSF-FFMF21-SSFFMFNN
% 0.13/0.23 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 0.13/0.23 % Starting SubtermCWHack with 28s (1) cores
% 0.13/0.23 % Preprocessing time : 0.002 s
% 0.13/0.23
% 0.13/0.23 % Proof found!
% 0.13/0.23 % SZS status Theorem
% 0.13/0.23 % SZS output start CNFRefutation
% 0.13/0.23 thf(decl_23, type, in: $i > $i > $o).
% 0.13/0.23 thf(decl_24, type, emptyset: $i).
% 0.13/0.23 thf(decl_25, type, powerset: $i > $i).
% 0.13/0.23 thf(decl_26, type, nonempty: $i > $o).
% 0.13/0.23 thf(decl_27, type, subset: $i > $i > $o).
% 0.13/0.23 thf(decl_28, type, subsetI1: $o).
% 0.13/0.23 thf(decl_29, type, transitiveset: $i > $o).
% 0.13/0.23 thf(decl_30, type, stricttotalorderedByIn: $i > $o).
% 0.13/0.23 thf(decl_31, type, wellorderedByIn: $i > $o).
% 0.13/0.23 thf(decl_32, type, ordinal: $i > $o).
% 0.13/0.23 thf(decl_33, type, ordinalTransSet: $o).
% 0.13/0.23 thf(decl_34, type, epred1_1: $i > $o).
% 0.13/0.23 thf(decl_35, type, epred2_1: $i > $o).
% 0.13/0.23 thf(decl_36, type, esk1_2: $i > $i > $i).
% 0.13/0.23 thf(decl_37, type, esk2_1: $i > $i).
% 0.13/0.23 thf(decl_38, type, esk3_1: $i > $i).
% 0.13/0.23 thf(decl_39, type, esk4_1: $i > $i).
% 0.13/0.23 thf(decl_40, type, esk5_2: $i > $i > $i).
% 0.13/0.23 thf(decl_41, type, esk6_0: $i).
% 0.13/0.23 thf(decl_42, type, esk7_0: $i).
% 0.13/0.23 thf(decl_48, type, esk13_2: $i > $i > $i).
% 0.13/0.23 thf(wellorderedByIn, axiom, ((wellorderedByIn)=(^[X2:$i]:((((stricttotalorderedByIn @ X2))&(![X4:$i]:((((in @ X4 @ (powerset @ X2)))=>((((nonempty @ X4))=>(?[X1:$i]:((((in @ X1 @ X4))&(![X5:$i]:((((in @ X5 @ X4))=>(((((X1)=(X5)))|((in @ X1 @ X5))))))))))))))))))), file('/export/starexec/sandbox2/tmp/tmp.A13u6GLM3x/E---3.1_1370492.p', wellorderedByIn)).
% 0.13/0.23 thf(stricttotalorderedByIn, axiom, ((stricttotalorderedByIn)=(^[X2:$i]:(((((![X1:$i]:((((in @ X1 @ X2))=>(![X4:$i]:((((in @ X4 @ X2))=>(![X5:$i]:((((in @ X5 @ X2))=>((((((in @ X1 @ X4))&((in @ X4 @ X5))))=>((in @ X1 @ X5)))))))))))))&(![X4:$i]:((((in @ X4 @ X2))=>(![X5:$i]:((((in @ X5 @ X2))=>(((((((X4)=(X5)))|((in @ X4 @ X5))))|((in @ X5 @ X4))))))))))))&(![X4:$i]:((((in @ X4 @ X2))=>(~((in @ X4 @ X4)))))))))), file('/export/starexec/sandbox2/tmp/tmp.A13u6GLM3x/E---3.1_1370492.p', stricttotalorderedByIn)).
% 0.13/0.23 thf(nonempty, axiom, ((nonempty)=(^[X1:$i]:(((X1)!=(emptyset))))), file('/export/starexec/sandbox2/tmp/tmp.A13u6GLM3x/E---3.1_1370492.p', nonempty)).
% 0.13/0.23 thf(ordinal, axiom, ((ordinal)=(^[X1:$i]:((((transitiveset @ X1))&((wellorderedByIn @ X1)))))), file('/export/starexec/sandbox2/tmp/tmp.A13u6GLM3x/E---3.1_1370492.p', ordinal)).
% 0.13/0.23 thf(transitiveset, axiom, ((transitiveset)=(^[X2:$i]:(![X4:$i]:((((in @ X4 @ X2))=>((subset @ X4 @ X2))))))), file('/export/starexec/sandbox2/tmp/tmp.A13u6GLM3x/E---3.1_1370492.p', transitiveset)).
% 0.13/0.23 thf(ordinalTransSet1, conjecture, ((subsetI1)=>((ordinalTransSet)=>![X4:$i]:(((ordinal @ X4)=>![X2:$i]:(((in @ X2 @ X4)=>(subset @ X2 @ X4))))))), file('/export/starexec/sandbox2/tmp/tmp.A13u6GLM3x/E---3.1_1370492.p', ordinalTransSet1)).
% 0.13/0.23 thf(ordinalTransSet, axiom, ((ordinalTransSet)<=>![X4:$i]:(((ordinal @ X4)=>![X1:$i, X2:$i]:(((in @ X2 @ X4)=>((in @ X1 @ X2)=>(in @ X1 @ X4))))))), file('/export/starexec/sandbox2/tmp/tmp.A13u6GLM3x/E---3.1_1370492.p', ordinalTransSet)).
% 0.13/0.23 thf(subsetI1, axiom, ((subsetI1)<=>![X2:$i, X3:$i]:((![X1:$i]:(((in @ X1 @ X2)=>(in @ X1 @ X3)))=>(subset @ X2 @ X3)))), file('/export/starexec/sandbox2/tmp/tmp.A13u6GLM3x/E---3.1_1370492.p', subsetI1)).
% 0.13/0.23 thf(c_0_8, plain, ((wellorderedByIn)=(^[Z0:$i]:((((((((![X14:$i]:((((in @ X14 @ Z0))=>(![X15:$i]:((((in @ X15 @ Z0))=>(![X16:$i]:((((in @ X16 @ Z0))=>((((((in @ X14 @ X15))&((in @ X15 @ X16))))=>((in @ X14 @ X16)))))))))))))&(![X17:$i]:((((in @ X17 @ Z0))=>(![X18:$i]:((((in @ X18 @ Z0))=>(((((((X17)=(X18)))|((in @ X17 @ X18))))|((in @ X18 @ X17))))))))))))&(![X19:$i]:((((in @ X19 @ Z0))=>(~((in @ X19 @ X19)))))))))&(![X4:$i]:((((in @ X4 @ (powerset @ Z0)))=>((((((X4)!=(emptyset))))=>(?[X1:$i]:((((in @ X1 @ X4))&(![X5:$i]:((((in @ X5 @ X4))=>(((((X1)=(X5)))|((in @ X1 @ X5))))))))))))))))))), inference(fof_simplification,[status(thm)],[wellorderedByIn])).
% 0.13/0.23 thf(c_0_9, plain, ((stricttotalorderedByIn)=(^[Z0:$i]:(((((![X1:$i]:((((in @ X1 @ Z0))=>(![X4:$i]:((((in @ X4 @ Z0))=>(![X5:$i]:((((in @ X5 @ Z0))=>((((((in @ X1 @ X4))&((in @ X4 @ X5))))=>((in @ X1 @ X5)))))))))))))&(![X4:$i]:((((in @ X4 @ Z0))=>(![X5:$i]:((((in @ X5 @ Z0))=>(((((((X4)=(X5)))|((in @ X4 @ X5))))|((in @ X5 @ X4))))))))))))&(![X4:$i]:((((in @ X4 @ Z0))=>(~((in @ X4 @ X4)))))))))), inference(fof_simplification,[status(thm)],[stricttotalorderedByIn])).
% 0.13/0.23 thf(c_0_10, plain, ((nonempty)=(^[Z0:$i]:(((Z0)!=(emptyset))))), inference(fof_simplification,[status(thm)],[nonempty])).
% 0.13/0.23 thf(c_0_11, plain, ((ordinal)=(^[Z0:$i]:((((![X20:$i]:((((in @ X20 @ Z0))=>((subset @ X20 @ Z0))))))&(((((((((![X21:$i]:((((in @ X21 @ Z0))=>(![X22:$i]:((((in @ X22 @ Z0))=>(![X23:$i]:((((in @ X23 @ Z0))=>((((((in @ X21 @ X22))&((in @ X22 @ X23))))=>((in @ X21 @ X23)))))))))))))&(![X24:$i]:((((in @ X24 @ Z0))=>(![X25:$i]:((((in @ X25 @ Z0))=>(((((((X24)=(X25)))|((in @ X24 @ X25))))|((in @ X25 @ X24))))))))))))&(![X26:$i]:((((in @ X26 @ Z0))=>(~((in @ X26 @ X26)))))))))&(![X27:$i]:((((in @ X27 @ (powerset @ Z0)))=>((((((X27)!=(emptyset))))=>(?[X28:$i]:((((in @ X28 @ X27))&(![X29:$i]:((((in @ X29 @ X27))=>(((((X28)=(X29)))|((in @ X28 @ X29)))))))))))))))))))))), inference(fof_simplification,[status(thm)],[ordinal])).
% 0.13/0.23 thf(c_0_12, plain, ((transitiveset)=(^[Z0:$i]:(![X4:$i]:((((in @ X4 @ Z0))=>((subset @ X4 @ Z0))))))), inference(fof_simplification,[status(thm)],[transitiveset])).
% 0.13/0.23 thf(c_0_13, plain, ((wellorderedByIn)=(^[Z0:$i]:((((((((![X14:$i]:((((in @ X14 @ Z0))=>(![X15:$i]:((((in @ X15 @ Z0))=>(![X16:$i]:((((in @ X16 @ Z0))=>((((((in @ X14 @ X15))&((in @ X15 @ X16))))=>((in @ X14 @ X16)))))))))))))&(![X17:$i]:((((in @ X17 @ Z0))=>(![X18:$i]:((((in @ X18 @ Z0))=>(((((((X17)=(X18)))|((in @ X17 @ X18))))|((in @ X18 @ X17))))))))))))&(![X19:$i]:((((in @ X19 @ Z0))=>(~((in @ X19 @ X19)))))))))&(![X4:$i]:((((in @ X4 @ (powerset @ Z0)))=>((((((X4)!=(emptyset))))=>(?[X1:$i]:((((in @ X1 @ X4))&(![X5:$i]:((((in @ X5 @ X4))=>(((((X1)=(X5)))|((in @ X1 @ X5))))))))))))))))))), inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[c_0_8, c_0_9]), c_0_10])).
% 0.13/0.23 thf(c_0_14, plain, ((ordinal)=(^[Z0:$i]:((((![X20:$i]:((((in @ X20 @ Z0))=>((subset @ X20 @ Z0))))))&(((((((((![X21:$i]:((((in @ X21 @ Z0))=>(![X22:$i]:((((in @ X22 @ Z0))=>(![X23:$i]:((((in @ X23 @ Z0))=>((((((in @ X21 @ X22))&((in @ X22 @ X23))))=>((in @ X21 @ X23)))))))))))))&(![X24:$i]:((((in @ X24 @ Z0))=>(![X25:$i]:((((in @ X25 @ Z0))=>(((((((X24)=(X25)))|((in @ X24 @ X25))))|((in @ X25 @ X24))))))))))))&(![X26:$i]:((((in @ X26 @ Z0))=>(~((in @ X26 @ X26)))))))))&(![X27:$i]:((((in @ X27 @ (powerset @ Z0)))=>((((((X27)!=(emptyset))))=>(?[X28:$i]:((((in @ X28 @ X27))&(![X29:$i]:((((in @ X29 @ X27))=>(((((X28)=(X29)))|((in @ X28 @ X29)))))))))))))))))))))), inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[c_0_11, c_0_12]), c_0_13])).
% 0.13/0.23 thf(c_0_15, plain, ![X4:$i]:(((epred2_1 @ X4)<=>(![X56:$i]:(((in @ X56 @ X4)=>(subset @ X56 @ X4)))&(((![X57:$i]:(((in @ X57 @ X4)=>![X58:$i]:(((in @ X58 @ X4)=>![X59:$i]:(((in @ X59 @ X4)=>(((in @ X57 @ X58)&(in @ X58 @ X59))=>(in @ X57 @ X59))))))))&![X60:$i]:(((in @ X60 @ X4)=>![X61:$i]:(((in @ X61 @ X4)=>(((X60)=(X61))|(in @ X60 @ X61)|(in @ X61 @ X60)))))))&![X62:$i]:(((in @ X62 @ X4)=>~(in @ X62 @ X62))))&![X63:$i]:(((in @ X63 @ (powerset @ X4))=>(((X63)!=(emptyset))=>?[X64:$i]:(((in @ X64 @ X63)&![X65:$i]:(((in @ X65 @ X63)=>(((X64)=(X65))|(in @ X64 @ X65))))))))))))), introduced(definition)).
% 0.13/0.23 thf(c_0_16, negated_conjecture, ~(((subsetI1)=>((ordinalTransSet)=>![X4:$i]:(((ordinal @ X4)=>![X2:$i]:(((in @ X2 @ X4)=>(subset @ X2 @ X4)))))))), inference(assume_negation,[status(cth)],[ordinalTransSet1])).
% 0.13/0.23 thf(c_0_17, axiom, ((ordinalTransSet)=(![X4:$i]:(((((((![X30:$i]:((((in @ X30 @ X4))=>((subset @ X30 @ X4))))))&(((((((((![X31:$i]:((((in @ X31 @ X4))=>(![X32:$i]:((((in @ X32 @ X4))=>(![X33:$i]:((((in @ X33 @ X4))=>((((((in @ X31 @ X32))&((in @ X32 @ X33))))=>((in @ X31 @ X33)))))))))))))&(![X34:$i]:((((in @ X34 @ X4))=>(![X35:$i]:((((in @ X35 @ X4))=>(((((((X34)=(X35)))|((in @ X34 @ X35))))|((in @ X35 @ X34))))))))))))&(![X36:$i]:((((in @ X36 @ X4))=>(~((in @ X36 @ X36)))))))))&(![X37:$i]:((((in @ X37 @ (powerset @ X4)))=>((((((X37)!=(emptyset))))=>(?[X38:$i]:((((in @ X38 @ X37))&(![X39:$i]:((((in @ X39 @ X37))=>(((((X38)=(X39)))|((in @ X38 @ X39)))))))))))))))))))))=>(![X1:$i, X2:$i]:((((in @ X2 @ X4))=>((((in @ X1 @ X2))=>((in @ X1 @ X4))))))))))), inference(apply_def,[status(thm)],[ordinalTransSet, c_0_14])).
% 0.13/0.23 thf(c_0_18, plain, ![X43:$i]:(((epred1_1 @ X43)<=>(![X45:$i]:(((in @ X45 @ X43)=>![X46:$i]:(((in @ X46 @ X43)=>![X47:$i]:(((in @ X47 @ X43)=>(((in @ X45 @ X46)&(in @ X46 @ X47))=>(in @ X45 @ X47))))))))&![X48:$i]:(((in @ X48 @ X43)=>![X49:$i]:(((in @ X49 @ X43)=>(((X48)=(X49))|(in @ X48 @ X49)|(in @ X49 @ X48))))))))), introduced(definition)).
% 0.13/0.23 thf(c_0_19, plain, ![X4:$i]:(((epred2_1 @ X4)=>(![X56:$i]:(((in @ X56 @ X4)=>(subset @ X56 @ X4)))&(((![X57:$i]:(((in @ X57 @ X4)=>![X58:$i]:(((in @ X58 @ X4)=>![X59:$i]:(((in @ X59 @ X4)=>(((in @ X57 @ X58)&(in @ X58 @ X59))=>(in @ X57 @ X59))))))))&![X60:$i]:(((in @ X60 @ X4)=>![X61:$i]:(((in @ X61 @ X4)=>(((X60)=(X61))|(in @ X60 @ X61)|(in @ X61 @ X60)))))))&![X62:$i]:(((in @ X62 @ X4)=>~(in @ X62 @ X62))))&![X63:$i]:(((in @ X63 @ (powerset @ X4))=>(((X63)!=(emptyset))=>?[X64:$i]:(((in @ X64 @ X63)&![X65:$i]:(((in @ X65 @ X63)=>(((X64)=(X65))|(in @ X64 @ X65))))))))))))), inference(split_equiv,[status(thm)],[c_0_15])).
% 0.13/0.23 thf(c_0_20, negated_conjecture, ~((![X40:$i, X41:$i]:((![X42:$i]:(((in @ X42 @ X40)=>(in @ X42 @ X41)))=>(subset @ X40 @ X41)))=>(![X43:$i]:(((![X44:$i]:(((in @ X44 @ X43)=>(subset @ X44 @ X43)))&(((epred1_1 @ X43)&![X50:$i]:(((in @ X50 @ X43)=>~(in @ X50 @ X50))))&![X51:$i]:(((in @ X51 @ (powerset @ X43))=>(((X51)!=(emptyset))=>?[X52:$i]:(((in @ X52 @ X51)&![X53:$i]:(((in @ X53 @ X51)=>(((X52)=(X53))|(in @ X52 @ X53)))))))))))=>![X54:$i, X55:$i]:(((in @ X55 @ X43)=>((in @ X54 @ X55)=>(in @ X54 @ X43))))))=>![X4:$i]:(((epred2_1 @ X4)=>![X2:$i]:(((in @ X2 @ X4)=>(subset @ X2 @ X4)))))))), inference(apply_def,[status(thm)],[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)],[c_0_16, c_0_17]), c_0_14]), subsetI1])]), c_0_18]), c_0_15])).
% 0.13/0.23 thf(c_0_21, plain, ![X85:$i, X86:$i, X87:$i, X88:$i, X89:$i, X90:$i, X91:$i, X92:$i, X93:$i, X95:$i]:(((~(in @ X86 @ X85)|(subset @ X86 @ X85)|~(epred2_1 @ X85))&((((~(in @ X87 @ X85)|(~(in @ X88 @ X85)|(~(in @ X89 @ X85)|(~(in @ X87 @ X88)|~(in @ X88 @ X89)|(in @ X87 @ X89))))|~(epred2_1 @ X85))&(~(in @ X90 @ X85)|(~(in @ X91 @ X85)|(((X90)=(X91))|(in @ X90 @ X91)|(in @ X91 @ X90)))|~(epred2_1 @ X85)))&(~(in @ X92 @ X85)|~(in @ X92 @ X92)|~(epred2_1 @ X85)))&(((in @ (esk13_2 @ X85 @ X93) @ X93)|((X93)=(emptyset))|~(in @ X93 @ (powerset @ X85))|~(epred2_1 @ X85))&(~(in @ X95 @ X93)|(((esk13_2 @ X85 @ X93)=(X95))|(in @ (esk13_2 @ X85 @ X93) @ X95))|((X93)=(emptyset))|~(in @ X93 @ (powerset @ X85))|~(epred2_1 @ X85)))))), 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_19])])])])])])).
% 0.13/0.23 thf(c_0_22, negated_conjecture, ![X66:$i, X67:$i, X69:$i, X73:$i, X75:$i, X76:$i]:(((((in @ (esk1_2 @ X66 @ X67) @ X66)|(subset @ X66 @ X67))&(~(in @ (esk1_2 @ X66 @ X67) @ X67)|(subset @ X66 @ X67)))&((((((in @ (esk4_1 @ X69) @ (powerset @ X69))|((in @ (esk3_1 @ X69) @ X69)|~(epred1_1 @ X69))|(in @ (esk2_1 @ X69) @ X69)|(~(in @ X76 @ X69)|(~(in @ X75 @ X76)|(in @ X75 @ X69))))&((((esk4_1 @ X69)!=(emptyset))|((in @ (esk3_1 @ X69) @ X69)|~(epred1_1 @ X69))|(in @ (esk2_1 @ X69) @ X69)|(~(in @ X76 @ X69)|(~(in @ X75 @ X76)|(in @ X75 @ X69))))&(((in @ (esk5_2 @ X69 @ X73) @ (esk4_1 @ X69))|~(in @ X73 @ (esk4_1 @ X69))|((in @ (esk3_1 @ X69) @ X69)|~(epred1_1 @ X69))|(in @ (esk2_1 @ X69) @ X69)|(~(in @ X76 @ X69)|(~(in @ X75 @ X76)|(in @ X75 @ X69))))&((((X73)!=(esk5_2 @ X69 @ X73))|~(in @ X73 @ (esk4_1 @ X69))|((in @ (esk3_1 @ X69) @ X69)|~(epred1_1 @ X69))|(in @ (esk2_1 @ X69) @ X69)|(~(in @ X76 @ X69)|(~(in @ X75 @ X76)|(in @ X75 @ X69))))&(~(in @ X73 @ (esk5_2 @ X69 @ X73))|~(in @ X73 @ (esk4_1 @ X69))|((in @ (esk3_1 @ X69) @ X69)|~(epred1_1 @ X69))|(in @ (esk2_1 @ X69) @ X69)|(~(in @ X76 @ X69)|(~(in @ X75 @ X76)|(in @ X75 @ X69))))))))&(((in @ (esk4_1 @ X69) @ (powerset @ X69))|((in @ (esk3_1 @ X69) @ (esk3_1 @ X69))|~(epred1_1 @ X69))|(in @ (esk2_1 @ X69) @ X69)|(~(in @ X76 @ X69)|(~(in @ X75 @ X76)|(in @ X75 @ X69))))&((((esk4_1 @ X69)!=(emptyset))|((in @ (esk3_1 @ X69) @ (esk3_1 @ X69))|~(epred1_1 @ X69))|(in @ (esk2_1 @ X69) @ X69)|(~(in @ X76 @ X69)|(~(in @ X75 @ X76)|(in @ X75 @ X69))))&(((in @ (esk5_2 @ X69 @ X73) @ (esk4_1 @ X69))|~(in @ X73 @ (esk4_1 @ X69))|((in @ (esk3_1 @ X69) @ (esk3_1 @ X69))|~(epred1_1 @ X69))|(in @ (esk2_1 @ X69) @ X69)|(~(in @ X76 @ X69)|(~(in @ X75 @ X76)|(in @ X75 @ X69))))&((((X73)!=(esk5_2 @ X69 @ X73))|~(in @ X73 @ (esk4_1 @ X69))|((in @ (esk3_1 @ X69) @ (esk3_1 @ X69))|~(epred1_1 @ X69))|(in @ (esk2_1 @ X69) @ X69)|(~(in @ X76 @ X69)|(~(in @ X75 @ X76)|(in @ X75 @ X69))))&(~(in @ X73 @ (esk5_2 @ X69 @ X73))|~(in @ X73 @ (esk4_1 @ X69))|((in @ (esk3_1 @ X69) @ (esk3_1 @ X69))|~(epred1_1 @ X69))|(in @ (esk2_1 @ X69) @ X69)|(~(in @ X76 @ X69)|(~(in @ X75 @ X76)|(in @ X75 @ X69)))))))))&((((in @ (esk4_1 @ X69) @ (powerset @ X69))|((in @ (esk3_1 @ X69) @ X69)|~(epred1_1 @ X69))|~(subset @ (esk2_1 @ X69) @ X69)|(~(in @ X76 @ X69)|(~(in @ X75 @ X76)|(in @ X75 @ X69))))&((((esk4_1 @ X69)!=(emptyset))|((in @ (esk3_1 @ X69) @ X69)|~(epred1_1 @ X69))|~(subset @ (esk2_1 @ X69) @ X69)|(~(in @ X76 @ X69)|(~(in @ X75 @ X76)|(in @ X75 @ X69))))&(((in @ (esk5_2 @ X69 @ X73) @ (esk4_1 @ X69))|~(in @ X73 @ (esk4_1 @ X69))|((in @ (esk3_1 @ X69) @ X69)|~(epred1_1 @ X69))|~(subset @ (esk2_1 @ X69) @ X69)|(~(in @ X76 @ X69)|(~(in @ X75 @ X76)|(in @ X75 @ X69))))&((((X73)!=(esk5_2 @ X69 @ X73))|~(in @ X73 @ (esk4_1 @ X69))|((in @ (esk3_1 @ X69) @ X69)|~(epred1_1 @ X69))|~(subset @ (esk2_1 @ X69) @ X69)|(~(in @ X76 @ X69)|(~(in @ X75 @ X76)|(in @ X75 @ X69))))&(~(in @ X73 @ (esk5_2 @ X69 @ X73))|~(in @ X73 @ (esk4_1 @ X69))|((in @ (esk3_1 @ X69) @ X69)|~(epred1_1 @ X69))|~(subset @ (esk2_1 @ X69) @ X69)|(~(in @ X76 @ X69)|(~(in @ X75 @ X76)|(in @ X75 @ X69))))))))&(((in @ (esk4_1 @ X69) @ (powerset @ X69))|((in @ (esk3_1 @ X69) @ (esk3_1 @ X69))|~(epred1_1 @ X69))|~(subset @ (esk2_1 @ X69) @ X69)|(~(in @ X76 @ X69)|(~(in @ X75 @ X76)|(in @ X75 @ X69))))&((((esk4_1 @ X69)!=(emptyset))|((in @ (esk3_1 @ X69) @ (esk3_1 @ X69))|~(epred1_1 @ X69))|~(subset @ (esk2_1 @ X69) @ X69)|(~(in @ X76 @ X69)|(~(in @ X75 @ X76)|(in @ X75 @ X69))))&(((in @ (esk5_2 @ X69 @ X73) @ (esk4_1 @ X69))|~(in @ X73 @ (esk4_1 @ X69))|((in @ (esk3_1 @ X69) @ (esk3_1 @ X69))|~(epred1_1 @ X69))|~(subset @ (esk2_1 @ X69) @ X69)|(~(in @ X76 @ X69)|(~(in @ X75 @ X76)|(in @ X75 @ X69))))&((((X73)!=(esk5_2 @ X69 @ X73))|~(in @ X73 @ (esk4_1 @ X69))|((in @ (esk3_1 @ X69) @ (esk3_1 @ X69))|~(epred1_1 @ X69))|~(subset @ (esk2_1 @ X69) @ X69)|(~(in @ X76 @ X69)|(~(in @ X75 @ X76)|(in @ X75 @ X69))))&(~(in @ X73 @ (esk5_2 @ X69 @ X73))|~(in @ X73 @ (esk4_1 @ X69))|((in @ (esk3_1 @ X69) @ (esk3_1 @ X69))|~(epred1_1 @ X69))|~(subset @ (esk2_1 @ X69) @ X69)|(~(in @ X76 @ X69)|(~(in @ X75 @ X76)|(in @ X75 @ X69))))))))))&((epred2_1 @ esk6_0)&((in @ esk7_0 @ esk6_0)&~(subset @ esk7_0 @ esk6_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(fof_nnf,[status(thm)],[c_0_20])])])])])])).
% 0.13/0.23 thf(c_0_23, plain, ![X1:$i, X2:$i]:(((subset @ X1 @ X2)|~((in @ X1 @ X2))|~((epred2_1 @ X2)))), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.13/0.23 thf(c_0_24, negated_conjecture, (epred2_1 @ esk6_0), inference(split_conjunct,[status(thm)],[c_0_22])).
% 0.13/0.23 thf(c_0_25, negated_conjecture, ~((subset @ esk7_0 @ esk6_0)), inference(split_conjunct,[status(thm)],[c_0_22])).
% 0.13/0.23 thf(c_0_26, negated_conjecture, ![X1:$i]:(((subset @ X1 @ esk6_0)|~((in @ X1 @ esk6_0)))), inference(spm,[status(thm)],[c_0_23, c_0_24])).
% 0.13/0.23 thf(c_0_27, negated_conjecture, (in @ esk7_0 @ esk6_0), inference(split_conjunct,[status(thm)],[c_0_22])).
% 0.13/0.23 thf(c_0_28, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_25, c_0_26]), c_0_27])]), ['proof']).
% 0.13/0.23 % SZS output end CNFRefutation
% 0.13/0.23 % Parsed axioms : 19
% 0.13/0.23 % Removed by relevancy pruning/SinE : 11
% 0.13/0.23 % Initial clauses : 61
% 0.13/0.23 % Removed in clause preprocessing : 0
% 0.13/0.23 % Initial clauses in saturation : 61
% 0.13/0.23 % Processed clauses : 5
% 0.13/0.23 % ...of these trivial : 0
% 0.13/0.23 % ...subsumed : 0
% 0.13/0.23 % ...remaining for further processing : 5
% 0.13/0.23 % Other redundant clauses eliminated : 0
% 0.13/0.23 % Clauses deleted for lack of memory : 0
% 0.13/0.23 % Backward-subsumed : 0
% 0.13/0.23 % Backward-rewritten : 0
% 0.13/0.23 % Generated clauses : 2
% 0.13/0.23 % ...of the previous two non-redundant : 1
% 0.13/0.23 % ...aggressively subsumed : 0
% 0.13/0.23 % Contextual simplify-reflections : 0
% 0.13/0.23 % Paramodulations : 2
% 0.13/0.23 % Factorizations : 0
% 0.13/0.23 % NegExts : 0
% 0.13/0.23 % Equation resolutions : 0
% 0.13/0.23 % Disequality decompositions : 0
% 0.13/0.23 % Total rewrite steps : 1
% 0.13/0.23 % ...of those cached : 0
% 0.13/0.23 % Propositional unsat checks : 0
% 0.13/0.23 % Propositional check models : 0
% 0.13/0.23 % Propositional check unsatisfiable : 0
% 0.13/0.23 % Propositional clauses : 0
% 0.13/0.23 % Propositional clauses after purity: 0
% 0.13/0.23 % Propositional unsat core size : 0
% 0.13/0.23 % Propositional preprocessing time : 0.000
% 0.13/0.23 % Propositional encoding time : 0.000
% 0.13/0.23 % Propositional solver time : 0.000
% 0.13/0.23 % Success case prop preproc time : 0.000
% 0.13/0.23 % Success case prop encoding time : 0.000
% 0.13/0.23 % Success case prop solver time : 0.000
% 0.13/0.23 % Current number of processed clauses : 5
% 0.13/0.23 % Positive orientable unit clauses : 2
% 0.13/0.23 % Positive unorientable unit clauses: 0
% 0.13/0.23 % Negative unit clauses : 1
% 0.13/0.23 % Non-unit-clauses : 2
% 0.13/0.23 % Current number of unprocessed clauses: 57
% 0.13/0.23 % ...number of literals in the above : 272
% 0.13/0.23 % Current number of archived formulas : 0
% 0.13/0.23 % Current number of archived clauses : 0
% 0.13/0.23 % Clause-clause subsumption calls (NU) : 1
% 0.13/0.23 % Rec. Clause-clause subsumption calls : 1
% 0.13/0.23 % Non-unit clause-clause subsumptions : 0
% 0.13/0.23 % Unit Clause-clause subsumption calls : 0
% 0.13/0.23 % Rewrite failures with RHS unbound : 0
% 0.13/0.23 % BW rewrite match attempts : 0
% 0.13/0.23 % BW rewrite match successes : 0
% 0.13/0.23 % Condensation attempts : 0
% 0.13/0.23 % Condensation successes : 0
% 0.13/0.23 % Termbank termtop insertions : 4454
% 0.13/0.23 % Search garbage collected termcells : 1244
% 0.13/0.23
% 0.13/0.23 % -------------------------------------------------
% 0.13/0.23 % User time : 0.008 s
% 0.13/0.23 % System time : 0.003 s
% 0.13/0.23 % Total time : 0.010 s
% 0.13/0.23 % Maximum resident set size: 3900 pages
% 0.13/0.23
% 0.13/0.23 % -------------------------------------------------
% 0.13/0.23 % User time : 0.010 s
% 0.13/0.23 % System time : 0.004 s
% 0.13/0.23 % Total time : 0.014 s
% 0.13/0.23 % Maximum resident set size: 4864 pages
% 0.13/0.23 % E exiting
%------------------------------------------------------------------------------