%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : SEU643^2 : TPTP v9.3.1. Released v3.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n019.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:51 AM UTC 2026
% Result : Theorem 0.09s 0.25s
% Output : CNFRefutation 0.09s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU643^2 : TPTP v9.3.1. Released v3.7.0.
% 0.00/0.04 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.16 % Computer : n019.cluster.edu
% 0.09/0.16 % Model : x86_64 x86_64
% 0.09/0.16 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.16 % Memory : 8046.5625MB
% 0.09/0.16 % OS : Linux 6.8.0-71-generic
% 0.09/0.16 % CPULimit : 300
% 0.09/0.16 % WCLimit : 300
% 0.09/0.16 % DateTime : Tue Sep 29 14:02:17 UTC 2026
% 0.09/0.16 % CPUTime :
% 0.09/0.16 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.21 Running higher-order theorem proving
% 0.09/0.22 Running: /export/starexec/sandbox/solver/bin/eprover-ho --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox/tmp/tmp.247oEMRmxk/E---3.1_818394.p
% 0.09/0.25 % Version: 3.5.1-ho
% 0.09/0.25 % Preprocessing class: HSSSSLSSSLMNHSA.
% 0.09/0.25 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.09/0.25 % Starting new_ho_10 with 1500s (5) cores
% 0.09/0.25 % Starting new_ho_7 with 300s (1) cores
% 0.09/0.25 % Starting lpo8_lambda_fix with 300s (1) cores
% 0.09/0.25 % Starting lpo9_lambda_fix with 300s (1) cores
% 0.09/0.25 % new_ho_10 with pid 818427 completed with status 0
% 0.09/0.25 % Result found by new_ho_10
% 0.09/0.25 % Preprocessing class: HSSSSLSSSLMNHSA.
% 0.09/0.25 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.09/0.25 % Starting new_ho_10 with 1500s (5) cores
% 0.09/0.25 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.09/0.25 % No SInE strategy applied
% 0.09/0.25 % Search class: HGHSF-FFSS32-MHSFMSBN
% 0.09/0.25 % partial match(4): HGHSM-FSLS32-MHSFFSBN
% 0.09/0.25 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 0.09/0.25 % Starting SubtermCWHack with 136s (1) cores
% 0.09/0.25 % Starting new_ho_10 with 151s (1) cores
% 0.09/0.25 % Starting new_ho_4 with 136s (1) cores
% 0.09/0.25 % Starting pre_casc_6 with 136s (1) cores
% 0.09/0.25 % Starting additional_ho_6 with 136s (1) cores
% 0.09/0.25 % SubtermCWHack with pid 818434 completed with status 0
% 0.09/0.25 % Result found by SubtermCWHack
% 0.09/0.25 % Preprocessing class: HSSSSLSSSLMNHSA.
% 0.09/0.25 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.09/0.25 % Starting new_ho_10 with 1500s (5) cores
% 0.09/0.25 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.09/0.25 % No SInE strategy applied
% 0.09/0.25 % Search class: HGHSF-FFSS32-MHSFMSBN
% 0.09/0.25 % partial match(4): HGHSM-FSLS32-MHSFFSBN
% 0.09/0.25 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 0.09/0.25 % Starting SubtermCWHack with 136s (1) cores
% 0.09/0.25 % Preprocessing time : 0.001 s
% 0.09/0.25
% 0.09/0.25 % Proof found!
% 0.09/0.25 % SZS status Theorem
% 0.09/0.25 % SZS output start CNFRefutation
% 0.09/0.25 thf(decl_23, type, in: $i > $i > $o).
% 0.09/0.25 thf(decl_24, type, emptyset: $i).
% 0.09/0.25 thf(decl_25, type, setadjoin: $i > $i > $i).
% 0.09/0.25 thf(decl_26, type, setunion: $i > $i).
% 0.09/0.25 thf(decl_27, type, dsetconstr: $i > ($i > $o) > $i).
% 0.09/0.25 thf(decl_28, type, setadjoinIL: $o).
% 0.09/0.25 thf(decl_29, type, iskpair: $i > $o).
% 0.09/0.25 thf(decl_30, type, singleton: $i > $o).
% 0.09/0.25 thf(decl_31, type, ex1: $i > ($i > $o) > $o).
% 0.09/0.25 thf(decl_32, type, ex1I: $o).
% 0.09/0.25 thf(decl_33, type, setukpairinjL1: $o).
% 0.09/0.25 thf(decl_34, type, esk1_3: $i > ($i > $o) > $i > $i).
% 0.09/0.25 thf(decl_35, type, esk2_3: $i > ($i > $o) > $i > $i).
% 0.09/0.25 thf(decl_36, type, esk3_0: $i).
% 0.09/0.25 thf(decl_37, type, esk4_0: $i).
% 0.09/0.25 thf(decl_38, type, esk5_0: $i).
% 0.09/0.25 thf(decl_39, type, epred1_0: $i > $o).
% 0.09/0.25 thf(ex1, axiom, ((ex1)=(^[X3:$i, X4:$i > $o]:((singleton @ (dsetconstr @ X3 @ (^[X1:$i]:((X4 @ X1)))))))), file('/export/starexec/sandbox/tmp/tmp.247oEMRmxk/E---3.1_818394.p', ex1)).
% 0.09/0.25 thf(singleton, axiom, ((singleton)=(^[X3:$i]:(?[X1:$i]:((((in @ X1 @ X3))&(((X3)=(setadjoin @ X1 @ emptyset)))))))), file('/export/starexec/sandbox/tmp/tmp.247oEMRmxk/E---3.1_818394.p', singleton)).
% 0.09/0.25 thf(ex1I, axiom, ((ex1I)<=>![X3:$i, X4:$i > $o, X1:$i]:(((in @ X1 @ X3)=>((X4 @ X1)=>(![X2:$i]:(((in @ X2 @ X3)=>((X4 @ X2)=>((X2)=(X1)))))=>(ex1 @ X3 @ (^[X2:$i]:((X4 @ X2))))))))), file('/export/starexec/sandbox/tmp/tmp.247oEMRmxk/E---3.1_818394.p', ex1I)).
% 0.09/0.25 thf(kfstsingleton, conjecture, ((setadjoinIL)=>((ex1I)=>((setukpairinjL1)=>![X6:$i]:(((iskpair @ X6)=>(singleton @ (dsetconstr @ (setunion @ X6) @ (^[X1:$i]:((in @ (setadjoin @ X1 @ emptyset) @ X6)))))))))), file('/export/starexec/sandbox/tmp/tmp.247oEMRmxk/E---3.1_818394.p', kfstsingleton)).
% 0.09/0.25 thf(iskpair, axiom, ((iskpair)=(^[X3:$i]:(?[X1:$i]:((((in @ X1 @ (setunion @ X3)))&(?[X2:$i]:((((in @ X2 @ (setunion @ X3)))&(((X3)=(setadjoin @ (setadjoin @ X1 @ emptyset) @ (setadjoin @ (setadjoin @ X1 @ (setadjoin @ X2 @ emptyset)) @ emptyset)))))))))))), file('/export/starexec/sandbox/tmp/tmp.247oEMRmxk/E---3.1_818394.p', iskpair)).
% 0.09/0.25 thf(setadjoinIL, axiom, ((setadjoinIL)<=>![X1:$i, X2:$i]:((in @ X1 @ (setadjoin @ X1 @ X2)))), file('/export/starexec/sandbox/tmp/tmp.247oEMRmxk/E---3.1_818394.p', setadjoinIL)).
% 0.09/0.25 thf(setukpairinjL1, axiom, ((setukpairinjL1)<=>![X1:$i, X2:$i, X5:$i]:(((in @ (setadjoin @ X5 @ emptyset) @ (setadjoin @ (setadjoin @ X1 @ emptyset) @ (setadjoin @ (setadjoin @ X1 @ (setadjoin @ X2 @ emptyset)) @ emptyset)))=>((X1)=(X5))))), file('/export/starexec/sandbox/tmp/tmp.247oEMRmxk/E---3.1_818394.p', setukpairinjL1)).
% 0.09/0.25 thf(c_0_7, plain, ((ex1)=(^[Z0:$i, Z1:$i > $o]:((?[X17:$i]:((((in @ X17 @ (dsetconstr @ Z0 @ (^[Z2:$i]:((Z1 @ Z2))))))&(((dsetconstr @ Z0 @ (^[Z2:$i]:((Z1 @ Z2))))=(setadjoin @ X17 @ emptyset))))))))), inference(fof_simplification,[status(thm)],[ex1])).
% 0.09/0.25 thf(c_0_8, plain, ((singleton)=(^[Z0:$i]:(?[X1:$i]:((((in @ X1 @ Z0))&(((Z0)=(setadjoin @ X1 @ emptyset)))))))), inference(fof_simplification,[status(thm)],[singleton])).
% 0.09/0.25 thf(c_0_9, plain, ((ex1I)<=>![X3:$i, X4:$i > $o, X1:$i]:(((in @ X1 @ X3)=>((X4 @ X1)=>(![X2:$i]:(((in @ X2 @ X3)=>((X4 @ X2)=>((X2)=(X1)))))=>(ex1 @ X3 @ (^[Z0:$i]:((X4 @ Z0))))))))), inference(fof_simplification,[status(thm)],[ex1I])).
% 0.09/0.25 thf(c_0_10, plain, ((ex1)=(^[Z0:$i, Z1:$i > $o]:((?[X17:$i]:((((in @ X17 @ (dsetconstr @ Z0 @ (^[Z2:$i]:((Z1 @ Z2))))))&(((dsetconstr @ Z0 @ (^[Z2:$i]:((Z1 @ Z2))))=(setadjoin @ X17 @ emptyset))))))))), inference(apply_def,[status(thm)],[c_0_7, c_0_8])).
% 0.09/0.25 thf(c_0_11, negated_conjecture, ~(((setadjoinIL)=>((ex1I)=>((setukpairinjL1)=>![X6:$i]:(((iskpair @ X6)=>(singleton @ (dsetconstr @ (setunion @ X6) @ (^[X1:$i]:((in @ (setadjoin @ X1 @ emptyset) @ X6))))))))))), inference(assume_negation,[status(cth)],[kfstsingleton])).
% 0.09/0.25 thf(c_0_12, plain, ((iskpair)=(^[Z0:$i]:(?[X1:$i]:((((in @ X1 @ (setunion @ Z0)))&(?[X2:$i]:((((in @ X2 @ (setunion @ Z0)))&(((Z0)=(setadjoin @ (setadjoin @ X1 @ emptyset) @ (setadjoin @ (setadjoin @ X1 @ (setadjoin @ X2 @ emptyset)) @ emptyset)))))))))))), inference(fof_simplification,[status(thm)],[iskpair])).
% 0.09/0.25 thf(c_0_13, plain, ((ex1I)=(![X3:$i, X4:$i > $o, X1:$i]:((((in @ X1 @ X3))=>((((X4 @ X1))=>(((![X2:$i]:((((in @ X2 @ X3))=>((((X4 @ X2))=>(((X2)=(X1))))))))=>((?[X18:$i]:((((in @ X18 @ (dsetconstr @ X3 @ (^[Z0:$i]:(((X4 @ Z0)))))))&(((dsetconstr @ X3 @ (^[Z0:$i]:(((X4 @ Z0)))))=(setadjoin @ X18 @ emptyset))))))))))))))), inference(apply_def,[status(thm)],[c_0_9, c_0_10])).
% 0.09/0.25 thf(c_0_14, negated_conjecture, ~((![X19:$i, X20:$i]:((in @ X19 @ (setadjoin @ X19 @ X20)))=>(![X21:$i, X22:$i > $o, X23:$i]:(((in @ X23 @ X21)=>((X22 @ X23)=>(![X24:$i]:(((in @ X24 @ X21)=>((X22 @ X24)=>((X24)=(X23)))))=>?[X25:$i]:(((in @ X25 @ (dsetconstr @ X21 @ X22))&((dsetconstr @ X21 @ X22)=(setadjoin @ X25 @ emptyset))))))))=>(![X26:$i, X27:$i, X28:$i]:(((in @ (setadjoin @ X28 @ emptyset) @ (setadjoin @ (setadjoin @ X26 @ emptyset) @ (setadjoin @ (setadjoin @ X26 @ (setadjoin @ X27 @ emptyset)) @ emptyset)))=>((X26)=(X28))))=>![X6:$i]:((?[X29:$i]:(((in @ X29 @ (setunion @ X6))&?[X30:$i]:(((in @ X30 @ (setunion @ X6))&((X6)=(setadjoin @ (setadjoin @ X29 @ emptyset) @ (setadjoin @ (setadjoin @ X29 @ (setadjoin @ X30 @ emptyset)) @ emptyset)))))))=>?[X31:$i]:(((in @ X31 @ (dsetconstr @ (setunion @ X6) @ (^[Z0:$i]:((in @ (setadjoin @ Z0 @ emptyset) @ X6)))))&((dsetconstr @ (setunion @ X6) @ (^[Z0:$i]:((in @ (setadjoin @ Z0 @ emptyset) @ X6))))=(setadjoin @ X31 @ emptyset)))))))))), inference(fool_unroll,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[c_0_11]), setadjoinIL]), c_0_12]), c_0_8]), c_0_13]), setukpairinjL1])])).
% 0.09/0.25 thf(c_0_15, negated_conjecture, ![X32:$i, X33:$i, X34:$i, X35:$i > $o, X36:$i, X39:$i, X40:$i, X41:$i, X45:$i]:(((in @ X32 @ (setadjoin @ X32 @ X33))&(((((in @ (esk2_3 @ X34 @ X35 @ X36) @ (dsetconstr @ X34 @ X35))|(in @ (esk1_3 @ X34 @ X35 @ X36) @ X34)|~(X35 @ X36)|~(in @ X36 @ X34))&(((dsetconstr @ X34 @ X35)=(setadjoin @ (esk2_3 @ X34 @ X35 @ X36) @ emptyset))|(in @ (esk1_3 @ X34 @ X35 @ X36) @ X34)|~(X35 @ X36)|~(in @ X36 @ X34)))&((((in @ (esk2_3 @ X34 @ X35 @ X36) @ (dsetconstr @ X34 @ X35))|(X35 @ (esk1_3 @ X34 @ X35 @ X36))|~(X35 @ X36)|~(in @ X36 @ X34))&(((dsetconstr @ X34 @ X35)=(setadjoin @ (esk2_3 @ X34 @ X35 @ X36) @ emptyset))|(X35 @ (esk1_3 @ X34 @ X35 @ X36))|~(X35 @ X36)|~(in @ X36 @ X34)))&(((in @ (esk2_3 @ X34 @ X35 @ X36) @ (dsetconstr @ X34 @ X35))|((esk1_3 @ X34 @ X35 @ X36)!=(X36))|~(X35 @ X36)|~(in @ X36 @ X34))&(((dsetconstr @ X34 @ X35)=(setadjoin @ (esk2_3 @ X34 @ X35 @ X36) @ emptyset))|((esk1_3 @ X34 @ X35 @ X36)!=(X36))|~(X35 @ X36)|~(in @ X36 @ X34)))))&((~(in @ (setadjoin @ X41 @ emptyset) @ (setadjoin @ (setadjoin @ X39 @ emptyset) @ (setadjoin @ (setadjoin @ X39 @ (setadjoin @ X40 @ emptyset)) @ emptyset)))|((X39)=(X41)))&(((in @ esk4_0 @ (setunion @ esk3_0))&((in @ esk5_0 @ (setunion @ esk3_0))&((esk3_0)=(setadjoin @ (setadjoin @ esk4_0 @ emptyset) @ (setadjoin @ (setadjoin @ esk4_0 @ (setadjoin @ esk5_0 @ emptyset)) @ emptyset)))))&(~(in @ X45 @ (dsetconstr @ (setunion @ esk3_0) @ (^[Z0:$i]:((in @ (setadjoin @ Z0 @ emptyset) @ esk3_0)))))|((dsetconstr @ (setunion @ esk3_0) @ (^[Z0:$i]:((in @ (setadjoin @ Z0 @ emptyset) @ esk3_0))))!=(setadjoin @ X45 @ 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_14])])])])])])).
% 0.09/0.25 thf(c_0_16, plain, ![X48:$i]:(((~(epred1_0 @ X48)|(in @ (setadjoin @ X48 @ emptyset) @ esk3_0))&(~(in @ (setadjoin @ X48 @ emptyset) @ esk3_0)|(epred1_0 @ X48)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[])])])).
% 0.09/0.25 thf(c_0_17, negated_conjecture, ![X1:$i, X2:$i]:((in @ X1 @ (setadjoin @ X1 @ X2))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.09/0.25 thf(c_0_18, negated_conjecture, ((esk3_0)=(setadjoin @ (setadjoin @ esk4_0 @ emptyset) @ (setadjoin @ (setadjoin @ esk4_0 @ (setadjoin @ esk5_0 @ emptyset)) @ emptyset))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.09/0.25 thf(c_0_19, negated_conjecture, ![X4:$i > $o, X2:$i, X1:$i]:((((dsetconstr @ X1 @ X4)=(setadjoin @ (esk2_3 @ X1 @ X4 @ X2) @ emptyset))|(X4 @ (esk1_3 @ X1 @ X4 @ X2))|~((X4 @ X2))|~((in @ X2 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.09/0.25 thf(c_0_20, negated_conjecture, (in @ esk4_0 @ (setunion @ esk3_0)), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.09/0.25 thf(c_0_21, plain, ![X1:$i]:(((epred1_0 @ X1)|~((in @ (setadjoin @ X1 @ emptyset) @ esk3_0)))), inference(split_conjunct,[status(thm)],[c_0_16])).
% 0.09/0.25 thf(c_0_22, negated_conjecture, (in @ (setadjoin @ esk4_0 @ emptyset) @ esk3_0), inference(spm,[status(thm)],[c_0_17, c_0_18])).
% 0.09/0.25 thf(c_0_23, plain, ![X46:$i]:(((epred1_0 @ X46)<=>(in @ (setadjoin @ X46 @ emptyset) @ esk3_0))), introduced(definition)).
% 0.09/0.25 thf(c_0_24, negated_conjecture, ![X4:$i > $o]:((((setadjoin @ (esk2_3 @ (setunion @ esk3_0) @ X4 @ esk4_0) @ emptyset)=(dsetconstr @ (setunion @ esk3_0) @ X4))|(X4 @ (esk1_3 @ (setunion @ esk3_0) @ X4 @ esk4_0))|~((X4 @ esk4_0)))), inference(spm,[status(thm)],[c_0_19, c_0_20])).
% 0.09/0.25 thf(c_0_25, plain, (epred1_0 @ esk4_0), inference(spm,[status(thm)],[c_0_21, c_0_22])).
% 0.09/0.25 thf(c_0_26, negated_conjecture, ![X1:$i, X2:$i, X3:$i]:((((X2)=(X1))|~((in @ (setadjoin @ X1 @ emptyset) @ (setadjoin @ (setadjoin @ X2 @ emptyset) @ (setadjoin @ (setadjoin @ X2 @ (setadjoin @ X3 @ emptyset)) @ emptyset)))))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.09/0.25 thf(c_0_27, negated_conjecture, ![X1:$i]:((~((((in @ X1 @ (dsetconstr @ (setunion @ esk3_0) @ epred1_0)))=(($true))))|((dsetconstr @ (setunion @ esk3_0) @ epred1_0)!=(setadjoin @ X1 @ emptyset)))), inference(lift_lambdas,[status(thm)],[inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_15]), c_0_23]), c_0_23])).
% 0.09/0.25 thf(c_0_28, plain, (((setadjoin @ (esk2_3 @ (setunion @ esk3_0) @ epred1_0 @ esk4_0) @ emptyset)=(dsetconstr @ (setunion @ esk3_0) @ epred1_0))|(epred1_0 @ (esk1_3 @ (setunion @ esk3_0) @ epred1_0 @ esk4_0))), inference(spm,[status(thm)],[c_0_24, c_0_25])).
% 0.09/0.25 thf(c_0_29, negated_conjecture, ![X1:$i]:((((X1)=(esk4_0))|~((in @ (setadjoin @ X1 @ emptyset) @ esk3_0)))), inference(spm,[status(thm)],[c_0_26, c_0_18])).
% 0.09/0.25 thf(c_0_30, plain, ![X1:$i]:(((in @ (setadjoin @ X1 @ emptyset) @ esk3_0)|~((epred1_0 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_16])).
% 0.09/0.25 thf(c_0_31, negated_conjecture, ![X1:$i]:((((dsetconstr @ (setunion @ esk3_0) @ epred1_0)!=(setadjoin @ X1 @ emptyset))|~((in @ X1 @ (dsetconstr @ (setunion @ esk3_0) @ epred1_0))))), inference(cn,[status(thm)],[c_0_27])).
% 0.09/0.25 thf(c_0_32, negated_conjecture, ((in @ (esk2_3 @ (setunion @ esk3_0) @ epred1_0 @ esk4_0) @ (dsetconstr @ (setunion @ esk3_0) @ epred1_0))|(epred1_0 @ (esk1_3 @ (setunion @ esk3_0) @ epred1_0 @ esk4_0))), inference(spm,[status(thm)],[c_0_17, c_0_28])).
% 0.09/0.25 thf(c_0_33, negated_conjecture, ![X4:$i > $o, X2:$i, X1:$i]:(((in @ (esk2_3 @ X1 @ X4 @ X2) @ (dsetconstr @ X1 @ X4))|((esk1_3 @ X1 @ X4 @ X2)!=(X2))|~((X4 @ X2))|~((in @ X2 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.09/0.25 thf(c_0_34, negated_conjecture, ![X4:$i > $o, X2:$i, X1:$i]:((((dsetconstr @ X1 @ X4)=(setadjoin @ (esk2_3 @ X1 @ X4 @ X2) @ emptyset))|((esk1_3 @ X1 @ X4 @ X2)!=(X2))|~((X4 @ X2))|~((in @ X2 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_15])).
% 0.09/0.25 thf(c_0_35, plain, ![X1:$i]:((((X1)=(esk4_0))|~((epred1_0 @ X1)))), inference(spm,[status(thm)],[c_0_29, c_0_30])).
% 0.09/0.25 thf(c_0_36, negated_conjecture, (epred1_0 @ (esk1_3 @ (setunion @ esk3_0) @ epred1_0 @ esk4_0)), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_31, c_0_32]), c_0_28])).
% 0.09/0.25 thf(c_0_37, negated_conjecture, ![X1:$i]:((((esk1_3 @ (setunion @ esk3_0) @ epred1_0 @ X1)!=(X1))|~((in @ X1 @ (setunion @ esk3_0)))|~((epred1_0 @ X1)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_31, c_0_33]), c_0_34])).
% 0.09/0.25 thf(c_0_38, plain, ((esk1_3 @ (setunion @ esk3_0) @ epred1_0 @ esk4_0)=(esk4_0)), inference(spm,[status(thm)],[c_0_35, c_0_36])).
% 0.09/0.25 thf(c_0_39, plain, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_37, c_0_38]), c_0_20]), c_0_25])]), ['proof']).
% 0.09/0.25 % SZS output end CNFRefutation
% 0.09/0.25 % Parsed axioms : 18
% 0.09/0.25 % Removed by relevancy pruning/SinE : 0
% 0.09/0.25 % Initial clauses : 25
% 0.09/0.25 % Removed in clause preprocessing : 11
% 0.09/0.25 % Initial clauses in saturation : 14
% 0.09/0.25 % Processed clauses : 74
% 0.09/0.25 % ...of these trivial : 0
% 0.09/0.25 % ...subsumed : 7
% 0.09/0.25 % ...remaining for further processing : 67
% 0.09/0.25 % Other redundant clauses eliminated : 2
% 0.09/0.25 % Clauses deleted for lack of memory : 0
% 0.09/0.25 % Backward-subsumed : 8
% 0.09/0.25 % Backward-rewritten : 3
% 0.09/0.25 % Generated clauses : 191
% 0.09/0.25 % ...of the previous two non-redundant : 166
% 0.09/0.25 % ...aggressively subsumed : 0
% 0.09/0.25 % Contextual simplify-reflections : 5
% 0.09/0.25 % Paramodulations : 189
% 0.09/0.25 % Factorizations : 0
% 0.09/0.25 % NegExts : 0
% 0.09/0.25 % Equation resolutions : 2
% 0.09/0.25 % Disequality decompositions : 0
% 0.09/0.25 % Total rewrite steps : 71
% 0.09/0.25 % ...of those cached : 64
% 0.09/0.25 % Propositional unsat checks : 0
% 0.09/0.25 % Propositional check models : 0
% 0.09/0.25 % Propositional check unsatisfiable : 0
% 0.09/0.25 % Propositional clauses : 0
% 0.09/0.25 % Propositional clauses after purity: 0
% 0.09/0.25 % Propositional unsat core size : 0
% 0.09/0.25 % Propositional preprocessing time : 0.000
% 0.09/0.25 % Propositional encoding time : 0.000
% 0.09/0.25 % Propositional solver time : 0.000
% 0.09/0.25 % Success case prop preproc time : 0.000
% 0.09/0.25 % Success case prop encoding time : 0.000
% 0.09/0.25 % Success case prop solver time : 0.000
% 0.09/0.25 % Current number of processed clauses : 56
% 0.09/0.25 % Positive orientable unit clauses : 7
% 0.09/0.25 % Positive unorientable unit clauses: 0
% 0.09/0.25 % Negative unit clauses : 0
% 0.09/0.25 % Non-unit-clauses : 49
% 0.09/0.25 % Current number of unprocessed clauses: 103
% 0.09/0.25 % ...number of literals in the above : 494
% 0.09/0.25 % Current number of archived formulas : 0
% 0.09/0.25 % Current number of archived clauses : 11
% 0.09/0.25 % Clause-clause subsumption calls (NU) : 220
% 0.09/0.25 % Rec. Clause-clause subsumption calls : 157
% 0.09/0.25 % Non-unit clause-clause subsumptions : 18
% 0.09/0.25 % Unit Clause-clause subsumption calls : 4
% 0.09/0.25 % Rewrite failures with RHS unbound : 0
% 0.09/0.25 % BW rewrite match attempts : 2
% 0.09/0.25 % BW rewrite match successes : 2
% 0.09/0.25 % Condensation attempts : 0
% 0.09/0.25 % Condensation successes : 0
% 0.09/0.25 % Termbank termtop insertions : 8010
% 0.09/0.25 % Search garbage collected termcells : 557
% 0.09/0.25
% 0.09/0.25 % -------------------------------------------------
% 0.09/0.25 % User time : 0.009 s
% 0.09/0.25 % System time : 0.003 s
% 0.09/0.25 % Total time : 0.013 s
% 0.09/0.25 % Maximum resident set size: 3644 pages
% 0.09/0.25
% 0.09/0.25 % -------------------------------------------------
% 0.09/0.25 % User time : 0.034 s
% 0.09/0.25 % System time : 0.009 s
% 0.09/0.25 % Total time : 0.043 s
% 0.09/0.25 % Maximum resident set size: 4864 pages
% 0.09/0.25 % E exiting
%------------------------------------------------------------------------------