%------------------------------------------------------------------------------
% File : E-SAT---3.5.1
% Problem : SEU655^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 : n006.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:27:05 AM UTC 2026
% Result : Theorem 0.08s 0.25s
% Output : CNFRefutation 0.08s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU655^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.08/0.17 % Computer : n006.cluster.edu
% 0.08/0.17 % Model : x86_64 x86_64
% 0.08/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.17 % Memory : 8046.5625MB
% 0.08/0.17 % OS : Linux 6.8.0-71-generic
% 0.08/0.17 % CPULimit : 300
% 0.08/0.17 % WCLimit : 300
% 0.08/0.17 % DateTime : Tue Sep 29 14:02:54 UTC 2026
% 0.08/0.17 % CPUTime :
% 0.08/0.17 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.21 Running higher-order theorem proving
% 0.08/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.XUS5Mi7Kj4/E---3.1_765506.p
% 0.08/0.25 % Version: 3.5.1-ho
% 0.08/0.25 % Preprocessing class: HSSSSLSSSLMNHSA.
% 0.08/0.25 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.08/0.25 % Starting new_ho_10 with 1500s (5) cores
% 0.08/0.25 % Starting new_ho_7 with 300s (1) cores
% 0.08/0.25 % Starting lpo8_lambda_fix with 300s (1) cores
% 0.08/0.25 % Starting lpo9_lambda_fix with 300s (1) cores
% 0.08/0.25 % new_ho_10 with pid 765519 completed with status 0
% 0.08/0.25 % Result found by new_ho_10
% 0.08/0.25 % Preprocessing class: HSSSSLSSSLMNHSA.
% 0.08/0.25 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.08/0.25 % Starting new_ho_10 with 1500s (5) cores
% 0.08/0.25 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.08/0.25 % No SInE strategy applied
% 0.08/0.25 % Search class: HGHSS-FFMS32-MHSFMSBN
% 0.08/0.25 % partial match(3): HGHSS-FFMS31-SHSSMSBN
% 0.08/0.25 % Scheduled 5 strats onto 5 cores with 1500 seconds (1500 total)
% 0.08/0.25 % Starting SubtermCWHack with 151s (1) cores
% 0.08/0.25 % Starting new_ho_10 with 901s (1) cores
% 0.08/0.25 % Starting sh5l with 151s (1) cores
% 0.08/0.25 % Starting new_bool_1 with 151s (1) cores
% 0.08/0.25 % Starting new_bool_2 with 146s (1) cores
% 0.08/0.25 % new_ho_10 with pid 765527 completed with status 0
% 0.08/0.25 % Result found by new_ho_10
% 0.08/0.25 % Preprocessing class: HSSSSLSSSLMNHSA.
% 0.08/0.25 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.08/0.25 % Starting new_ho_10 with 1500s (5) cores
% 0.08/0.25 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.08/0.25 % No SInE strategy applied
% 0.08/0.25 % Search class: HGHSS-FFMS32-MHSFMSBN
% 0.08/0.25 % partial match(3): HGHSS-FFMS31-SHSSMSBN
% 0.08/0.25 % Scheduled 5 strats onto 5 cores with 1500 seconds (1500 total)
% 0.08/0.25 % Starting SubtermCWHack with 151s (1) cores
% 0.08/0.25 % Starting new_ho_10 with 901s (1) cores
% 0.08/0.25 % Preprocessing time : 0.001 s
% 0.08/0.25 % Presaturation interreduction done
% 0.08/0.25
% 0.08/0.25 % Proof found!
% 0.08/0.25 % SZS status Theorem
% 0.08/0.25 % SZS output start CNFRefutation
% 0.08/0.25 thf(decl_23, type, in: $i > $i > $o).
% 0.08/0.25 thf(decl_24, type, emptyset: $i).
% 0.08/0.25 thf(decl_25, type, setadjoin: $i > $i > $i).
% 0.08/0.25 thf(decl_26, type, setunion: $i > $i).
% 0.08/0.25 thf(decl_27, type, dsetconstr: $i > ($i > $o) > $i).
% 0.08/0.25 thf(decl_28, type, iskpair: $i > $o).
% 0.08/0.25 thf(decl_29, type, kpair: $i > $i > $i).
% 0.08/0.25 thf(decl_30, type, singleton: $i > $o).
% 0.08/0.25 thf(decl_31, type, ex1: $i > ($i > $o) > $o).
% 0.08/0.25 thf(decl_32, type, ex1I: $o).
% 0.08/0.25 thf(decl_33, type, kfst: $i > $i).
% 0.08/0.25 thf(decl_34, type, kfstpairEq: $o).
% 0.08/0.25 thf(decl_35, type, setukpairinjR: $o).
% 0.08/0.25 thf(decl_36, type, esk1_3: $i > ($i > $o) > $i > $i).
% 0.08/0.25 thf(decl_37, type, esk2_3: $i > ($i > $o) > $i > $i).
% 0.08/0.25 thf(decl_38, type, esk3_0: $i).
% 0.08/0.25 thf(decl_39, type, esk4_0: $i).
% 0.08/0.25 thf(decl_40, type, esk5_0: $i).
% 0.08/0.25 thf(decl_41, type, epred1_0: $i > $o).
% 0.08/0.25 thf(ex1, axiom, ((ex1)=(^[X1:$i, X4:$i > $o]:((singleton @ (dsetconstr @ X1 @ (^[X2:$i]:((X4 @ X2)))))))), file('/export/starexec/sandbox/tmp/tmp.XUS5Mi7Kj4/E---3.1_765506.p', ex1)).
% 0.08/0.25 thf(singleton, axiom, ((singleton)=(^[X1:$i]:(?[X2:$i]:((((in @ X2 @ X1))&(((X1)=(setadjoin @ X2 @ emptyset)))))))), file('/export/starexec/sandbox/tmp/tmp.XUS5Mi7Kj4/E---3.1_765506.p', singleton)).
% 0.08/0.25 thf(ex1I, axiom, ((ex1I)<=>![X1:$i, X4:$i > $o, X2:$i]:(((in @ X2 @ X1)=>((X4 @ X2)=>(![X3:$i]:(((in @ X3 @ X1)=>((X4 @ X3)=>((X3)=(X2)))))=>(ex1 @ X1 @ (^[X3:$i]:((X4 @ X3))))))))), file('/export/starexec/sandbox/tmp/tmp.XUS5Mi7Kj4/E---3.1_765506.p', ex1I)).
% 0.08/0.25 thf(ksndsingleton, conjecture, ((ex1I)=>((kfstpairEq)=>((setukpairinjR)=>![X6:$i]:(((iskpair @ X6)=>(singleton @ (dsetconstr @ (setunion @ X6) @ (^[X2:$i]:(((X6)=(kpair @ (kfst @ X6) @ X2))))))))))), file('/export/starexec/sandbox/tmp/tmp.XUS5Mi7Kj4/E---3.1_765506.p', ksndsingleton)).
% 0.08/0.25 thf(iskpair, axiom, ((iskpair)=(^[X1:$i]:(?[X2:$i]:((((in @ X2 @ (setunion @ X1)))&(?[X3:$i]:((((in @ X3 @ (setunion @ X1)))&(((X1)=(setadjoin @ (setadjoin @ X2 @ emptyset) @ (setadjoin @ (setadjoin @ X2 @ (setadjoin @ X3 @ emptyset)) @ emptyset)))))))))))), file('/export/starexec/sandbox/tmp/tmp.XUS5Mi7Kj4/E---3.1_765506.p', iskpair)).
% 0.08/0.25 thf(kfstpairEq, axiom, ((kfstpairEq)<=>![X2:$i, X3:$i]:(((kfst @ (kpair @ X2 @ X3))=(X2)))), file('/export/starexec/sandbox/tmp/tmp.XUS5Mi7Kj4/E---3.1_765506.p', kfstpairEq)).
% 0.08/0.25 thf(setukpairinjR, axiom, ((setukpairinjR)<=>![X2:$i, X3:$i, X5:$i, X6:$i]:((((kpair @ X2 @ X3)=(kpair @ X5 @ X6))=>((X3)=(X6))))), file('/export/starexec/sandbox/tmp/tmp.XUS5Mi7Kj4/E---3.1_765506.p', setukpairinjR)).
% 0.08/0.25 thf(kpair, axiom, ((kpair)=(^[X2:$i, X3:$i]:(setadjoin @ (setadjoin @ X2 @ emptyset) @ (setadjoin @ (setadjoin @ X2 @ (setadjoin @ X3 @ emptyset)) @ emptyset)))), file('/export/starexec/sandbox/tmp/tmp.XUS5Mi7Kj4/E---3.1_765506.p', kpair)).
% 0.08/0.25 thf(c_0_8, plain, ((ex1)=(^[Z0:$i, Z1:$i > $o]:((?[X18:$i]:((((in @ X18 @ (dsetconstr @ Z0 @ (^[Z2:$i]:((Z1 @ Z2))))))&(((dsetconstr @ Z0 @ (^[Z2:$i]:((Z1 @ Z2))))=(setadjoin @ X18 @ emptyset))))))))), inference(fof_simplification,[status(thm)],[ex1])).
% 0.08/0.25 thf(c_0_9, plain, ((singleton)=(^[Z0:$i]:(?[X2:$i]:((((in @ X2 @ Z0))&(((Z0)=(setadjoin @ X2 @ emptyset)))))))), inference(fof_simplification,[status(thm)],[singleton])).
% 0.08/0.25 thf(c_0_10, plain, ((ex1I)<=>![X1:$i, X4:$i > $o, X2:$i]:(((in @ X2 @ X1)=>((X4 @ X2)=>(![X3:$i]:(((in @ X3 @ X1)=>((X4 @ X3)=>((X3)=(X2)))))=>(ex1 @ X1 @ (^[Z0:$i]:((X4 @ Z0))))))))), inference(fof_simplification,[status(thm)],[ex1I])).
% 0.08/0.25 thf(c_0_11, plain, ((ex1)=(^[Z0:$i, Z1:$i > $o]:((?[X18:$i]:((((in @ X18 @ (dsetconstr @ Z0 @ (^[Z2:$i]:((Z1 @ Z2))))))&(((dsetconstr @ Z0 @ (^[Z2:$i]:((Z1 @ Z2))))=(setadjoin @ X18 @ emptyset))))))))), inference(apply_def,[status(thm)],[c_0_8, c_0_9])).
% 0.08/0.25 thf(c_0_12, negated_conjecture, ~(((ex1I)=>((kfstpairEq)=>((setukpairinjR)=>![X6:$i]:(((iskpair @ X6)=>(singleton @ (dsetconstr @ (setunion @ X6) @ (^[X2:$i]:(((X6)=(kpair @ (kfst @ X6) @ X2)))))))))))), inference(assume_negation,[status(cth)],[ksndsingleton])).
% 0.08/0.25 thf(c_0_13, plain, ((iskpair)=(^[Z0:$i]:(?[X2:$i]:((((in @ X2 @ (setunion @ Z0)))&(?[X3:$i]:((((in @ X3 @ (setunion @ Z0)))&(((Z0)=(setadjoin @ (setadjoin @ X2 @ emptyset) @ (setadjoin @ (setadjoin @ X2 @ (setadjoin @ X3 @ emptyset)) @ emptyset)))))))))))), inference(fof_simplification,[status(thm)],[iskpair])).
% 0.08/0.25 thf(c_0_14, plain, ((ex1I)=(![X1:$i, X4:$i > $o, X2:$i]:((((in @ X2 @ X1))=>((((X4 @ X2))=>(((![X3:$i]:((((in @ X3 @ X1))=>((((X4 @ X3))=>(((X3)=(X2))))))))=>((?[X19:$i]:((((in @ X19 @ (dsetconstr @ X1 @ (^[Z0:$i]:(((X4 @ Z0)))))))&(((dsetconstr @ X1 @ (^[Z0:$i]:(((X4 @ Z0)))))=(setadjoin @ X19 @ emptyset))))))))))))))), inference(apply_def,[status(thm)],[c_0_10, c_0_11])).
% 0.08/0.25 thf(c_0_15, negated_conjecture, ~((![X20:$i, X21:$i > $o, X22:$i]:(((in @ X22 @ X20)=>((X21 @ X22)=>(![X23:$i]:(((in @ X23 @ X20)=>((X21 @ X23)=>((X23)=(X22)))))=>?[X24:$i]:(((in @ X24 @ (dsetconstr @ X20 @ X21))&((dsetconstr @ X20 @ X21)=(setadjoin @ X24 @ emptyset))))))))=>(![X25:$i, X26:$i]:(((kfst @ (kpair @ X25 @ X26))=(X25)))=>(![X27:$i, X28:$i, X29:$i, X30:$i]:((((kpair @ X27 @ X28)=(kpair @ X29 @ X30))=>((X28)=(X30))))=>![X6:$i]:((?[X31:$i]:(((in @ X31 @ (setunion @ X6))&?[X32:$i]:(((in @ X32 @ (setunion @ X6))&((X6)=(setadjoin @ (setadjoin @ X31 @ emptyset) @ (setadjoin @ (setadjoin @ X31 @ (setadjoin @ X32 @ emptyset)) @ emptyset)))))))=>?[X33:$i]:(((in @ X33 @ (dsetconstr @ (setunion @ X6) @ (^[Z0:$i]:(((X6)=(kpair @ (kfst @ X6) @ Z0))))))&((dsetconstr @ (setunion @ X6) @ (^[Z0:$i]:(((X6)=(kpair @ (kfst @ X6) @ Z0)))))=(setadjoin @ X33 @ 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_12]), c_0_13]), c_0_9]), c_0_14]), kfstpairEq]), setukpairinjR])])).
% 0.08/0.25 thf(c_0_16, plain, ![X34:$i, X35:$i]:(((kpair @ X34 @ X35)=(setadjoin @ (setadjoin @ X34 @ emptyset) @ (setadjoin @ (setadjoin @ X34 @ (setadjoin @ X35 @ emptyset)) @ emptyset)))), inference(fof_simplification,[status(thm)],[inference(fof_simplification,[status(thm)],[kpair])])).
% 0.08/0.25 thf(c_0_17, negated_conjecture, ![X38:$i, X39:$i > $o, X40:$i, X43:$i, X44:$i, X45:$i, X46:$i, X47:$i, X48:$i, X52:$i]:((((((in @ (esk2_3 @ X38 @ X39 @ X40) @ (dsetconstr @ X38 @ X39))|(in @ (esk1_3 @ X38 @ X39 @ X40) @ X38)|~(X39 @ X40)|~(in @ X40 @ X38))&(((dsetconstr @ X38 @ X39)=(setadjoin @ (esk2_3 @ X38 @ X39 @ X40) @ emptyset))|(in @ (esk1_3 @ X38 @ X39 @ X40) @ X38)|~(X39 @ X40)|~(in @ X40 @ X38)))&((((in @ (esk2_3 @ X38 @ X39 @ X40) @ (dsetconstr @ X38 @ X39))|(X39 @ (esk1_3 @ X38 @ X39 @ X40))|~(X39 @ X40)|~(in @ X40 @ X38))&(((dsetconstr @ X38 @ X39)=(setadjoin @ (esk2_3 @ X38 @ X39 @ X40) @ emptyset))|(X39 @ (esk1_3 @ X38 @ X39 @ X40))|~(X39 @ X40)|~(in @ X40 @ X38)))&(((in @ (esk2_3 @ X38 @ X39 @ X40) @ (dsetconstr @ X38 @ X39))|((esk1_3 @ X38 @ X39 @ X40)!=(X40))|~(X39 @ X40)|~(in @ X40 @ X38))&(((dsetconstr @ X38 @ X39)=(setadjoin @ (esk2_3 @ X38 @ X39 @ X40) @ emptyset))|((esk1_3 @ X38 @ X39 @ X40)!=(X40))|~(X39 @ X40)|~(in @ X40 @ X38)))))&(((kfst @ (kpair @ X43 @ X44))=(X43))&((((kpair @ X45 @ X46)!=(kpair @ X47 @ X48))|((X46)=(X48)))&(((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 @ X52 @ (dsetconstr @ (setunion @ esk3_0) @ (^[Z0:$i]:(((esk3_0)=(kpair @ (kfst @ esk3_0) @ Z0))))))|((dsetconstr @ (setunion @ esk3_0) @ (^[Z0:$i]:(((esk3_0)=(kpair @ (kfst @ esk3_0) @ Z0)))))!=(setadjoin @ X52 @ 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_15])])])])])])).
% 0.08/0.25 thf(c_0_18, plain, ![X36:$i, X37:$i]:(((kpair @ X36 @ X37)=(setadjoin @ (setadjoin @ X36 @ emptyset) @ (setadjoin @ (setadjoin @ X36 @ (setadjoin @ X37 @ emptyset)) @ emptyset)))), inference(variable_rename,[status(thm)],[c_0_16])).
% 0.08/0.25 thf(c_0_19, 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_17])).
% 0.08/0.25 thf(c_0_20, plain, ![X1:$i, X2:$i]:(((kpair @ X1 @ X2)=(setadjoin @ (setadjoin @ X1 @ emptyset) @ (setadjoin @ (setadjoin @ X1 @ (setadjoin @ X2 @ emptyset)) @ emptyset)))), inference(split_conjunct,[status(thm)],[c_0_18])).
% 0.08/0.25 thf(c_0_21, plain, ![X55:$i]:(((~(epred1_0 @ X55)|((esk3_0)=(kpair @ (kfst @ esk3_0) @ X55)))&(((esk3_0)!=(kpair @ (kfst @ esk3_0) @ X55))|(epred1_0 @ X55)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[])])])).
% 0.08/0.25 thf(c_0_22, negated_conjecture, ![X2:$i, X1:$i]:(((kfst @ (kpair @ X1 @ X2))=(X1))), inference(split_conjunct,[status(thm)],[c_0_17])).
% 0.08/0.25 thf(c_0_23, negated_conjecture, ((kpair @ esk4_0 @ esk5_0)=(esk3_0)), inference(rw,[status(thm)],[c_0_19, c_0_20])).
% 0.08/0.25 thf(c_0_24, plain, ![X53:$i]:(((epred1_0 @ X53)<=>((esk3_0)=(kpair @ (kfst @ esk3_0) @ X53)))), introduced(definition)).
% 0.08/0.25 thf(c_0_25, negated_conjecture, ![X1:$i, X2:$i, X3:$i, X5:$i]:((((X2)=(X5))|((kpair @ X1 @ X2)!=(kpair @ X3 @ X5)))), inference(split_conjunct,[status(thm)],[c_0_17])).
% 0.08/0.25 thf(c_0_26, plain, ![X1:$i]:((((esk3_0)=(kpair @ (kfst @ esk3_0) @ X1))|~((epred1_0 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.08/0.25 thf(c_0_27, negated_conjecture, ((kfst @ esk3_0)=(esk4_0)), inference(spm,[status(thm)],[c_0_22, c_0_23])).
% 0.08/0.25 thf(c_0_28, 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_17]), c_0_24]), c_0_24])).
% 0.08/0.25 thf(c_0_29, negated_conjecture, ![X2:$i, X1:$i]:((((X1)=(esk5_0))|((kpair @ X2 @ X1)!=(esk3_0)))), inference(spm,[status(thm)],[c_0_25, c_0_23])).
% 0.08/0.25 thf(c_0_30, plain, ![X1:$i]:((((kpair @ esk4_0 @ X1)=(esk3_0))|~((epred1_0 @ X1)))), inference(rw,[status(thm)],[c_0_26, c_0_27])).
% 0.08/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_28])).
% 0.08/0.25 thf(c_0_32, negated_conjecture, ![X4:$i > $o, X2:$i, X1:$i]:(((in @ (esk2_3 @ X1 @ X4 @ X2) @ (dsetconstr @ X1 @ X4))|(X4 @ (esk1_3 @ X1 @ X4 @ X2))|~((X4 @ X2))|~((in @ X2 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_17])).
% 0.08/0.25 thf(c_0_33, 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_17])).
% 0.08/0.25 thf(c_0_34, plain, ![X1:$i]:(((epred1_0 @ X1)|((esk3_0)!=(kpair @ (kfst @ esk3_0) @ X1)))), inference(split_conjunct,[status(thm)],[c_0_21])).
% 0.08/0.25 thf(c_0_35, 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_17])).
% 0.08/0.25 thf(c_0_36, 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_17])).
% 0.08/0.25 thf(c_0_37, plain, ![X1:$i]:((((X1)=(esk5_0))|~((epred1_0 @ X1)))), inference(spm,[status(thm)],[c_0_29, c_0_30])).
% 0.08/0.25 thf(c_0_38, negated_conjecture, ![X1:$i]:(((epred1_0 @ (esk1_3 @ (setunion @ esk3_0) @ epred1_0 @ X1))|~((in @ X1 @ (setunion @ esk3_0)))|~((epred1_0 @ X1)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_31, c_0_32]), c_0_33])).
% 0.08/0.25 thf(c_0_39, plain, ![X1:$i]:(((epred1_0 @ X1)|((kpair @ esk4_0 @ X1)!=(esk3_0)))), inference(rw,[status(thm)],[c_0_34, c_0_27])).
% 0.08/0.25 thf(c_0_40, 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_35]), c_0_36])).
% 0.08/0.25 thf(c_0_41, plain, ![X1:$i]:((((esk1_3 @ (setunion @ esk3_0) @ epred1_0 @ X1)=(esk5_0))|~((in @ X1 @ (setunion @ esk3_0)))|~((epred1_0 @ X1)))), inference(spm,[status(thm)],[c_0_37, c_0_38])).
% 0.08/0.25 thf(c_0_42, negated_conjecture, (in @ esk5_0 @ (setunion @ esk3_0)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 0.08/0.25 thf(c_0_43, negated_conjecture, (epred1_0 @ esk5_0), inference(spm,[status(thm)],[c_0_39, c_0_23])).
% 0.08/0.25 thf(c_0_44, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_40, c_0_41])]), c_0_42]), c_0_43])]), ['proof']).
% 0.08/0.25 % SZS output end CNFRefutation
% 0.08/0.25 % Parsed axioms : 21
% 0.08/0.25 % Removed by relevancy pruning/SinE : 0
% 0.08/0.25 % Initial clauses : 28
% 0.08/0.25 % Removed in clause preprocessing : 13
% 0.08/0.25 % Initial clauses in saturation : 15
% 0.08/0.25 % Processed clauses : 58
% 0.08/0.25 % ...of these trivial : 0
% 0.08/0.25 % ...subsumed : 4
% 0.08/0.25 % ...remaining for further processing : 54
% 0.08/0.25 % Other redundant clauses eliminated : 2
% 0.08/0.25 % Clauses deleted for lack of memory : 0
% 0.08/0.25 % Backward-subsumed : 0
% 0.08/0.25 % Backward-rewritten : 2
% 0.08/0.25 % Generated clauses : 85
% 0.08/0.25 % ...of the previous two non-redundant : 76
% 0.08/0.25 % ...aggressively subsumed : 0
% 0.08/0.25 % Contextual simplify-reflections : 3
% 0.08/0.25 % Paramodulations : 82
% 0.08/0.25 % Factorizations : 0
% 0.08/0.25 % NegExts : 0
% 0.08/0.25 % Equation resolutions : 3
% 0.08/0.25 % Disequality decompositions : 0
% 0.08/0.25 % Total rewrite steps : 18
% 0.08/0.25 % ...of those cached : 10
% 0.08/0.25 % Propositional unsat checks : 0
% 0.08/0.25 % Propositional check models : 0
% 0.08/0.25 % Propositional check unsatisfiable : 0
% 0.08/0.25 % Propositional clauses : 0
% 0.08/0.25 % Propositional clauses after purity: 0
% 0.08/0.25 % Propositional unsat core size : 0
% 0.08/0.25 % Propositional preprocessing time : 0.000
% 0.08/0.25 % Propositional encoding time : 0.000
% 0.08/0.25 % Propositional solver time : 0.000
% 0.08/0.25 % Success case prop preproc time : 0.000
% 0.08/0.25 % Success case prop encoding time : 0.000
% 0.08/0.25 % Success case prop solver time : 0.000
% 0.08/0.25 % Current number of processed clauses : 37
% 0.08/0.25 % Positive orientable unit clauses : 8
% 0.08/0.25 % Positive unorientable unit clauses: 0
% 0.08/0.25 % Negative unit clauses : 0
% 0.08/0.25 % Non-unit-clauses : 29
% 0.08/0.25 % Current number of unprocessed clauses: 47
% 0.08/0.25 % ...number of literals in the above : 260
% 0.08/0.25 % Current number of archived formulas : 0
% 0.08/0.25 % Current number of archived clauses : 17
% 0.08/0.25 % Clause-clause subsumption calls (NU) : 118
% 0.08/0.25 % Rec. Clause-clause subsumption calls : 56
% 0.08/0.25 % Non-unit clause-clause subsumptions : 7
% 0.08/0.25 % Unit Clause-clause subsumption calls : 3
% 0.08/0.25 % Rewrite failures with RHS unbound : 0
% 0.08/0.25 % BW rewrite match attempts : 2
% 0.08/0.25 % BW rewrite match successes : 2
% 0.08/0.25 % Condensation attempts : 58
% 0.08/0.25 % Condensation successes : 0
% 0.08/0.25 % Termbank termtop insertions : 5062
% 0.08/0.25 % Search garbage collected termcells : 567
% 0.08/0.25
% 0.08/0.25 % -------------------------------------------------
% 0.08/0.25 % User time : 0.007 s
% 0.08/0.25 % System time : 0.005 s
% 0.08/0.25 % Total time : 0.011 s
% 0.08/0.25 % Maximum resident set size: 3648 pages
% 0.08/0.25
% 0.08/0.25 % -------------------------------------------------
% 0.08/0.25 % User time : 0.025 s
% 0.08/0.25 % System time : 0.014 s
% 0.08/0.25 % Total time : 0.039 s
% 0.08/0.25 % Maximum resident set size: 4864 pages
% 0.08/0.25 % E exiting
%------------------------------------------------------------------------------