%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : SEU655^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 : n002.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:54 AM UTC 2026
% Result : Theorem 0.13s 0.26s
% Output : CNFRefutation 0.13s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU655^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.13/0.17 % Computer : n002.cluster.edu
% 0.13/0.17 % Model : x86_64 x86_64
% 0.13/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.17 % Memory : 8046.5625MB
% 0.13/0.17 % OS : Linux 6.8.0-71-generic
% 0.13/0.17 % CPULimit : 300
% 0.13/0.17 % WCLimit : 300
% 0.13/0.17 % DateTime : Tue Sep 29 14:05:52 UTC 2026
% 0.13/0.18 % CPUTime :
% 0.13/0.18 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.22 Running higher-order theorem proving
% 0.13/0.23 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.ZsvHlv9XJG/E---3.1_1341058.p
% 0.13/0.26 % Version: 3.5.1-ho
% 0.13/0.26 % Preprocessing class: HSSSSLSSSLMNHSA.
% 0.13/0.26 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.13/0.26 % Starting new_ho_10 with 1500s (5) cores
% 0.13/0.26 % Starting new_ho_7 with 300s (1) cores
% 0.13/0.26 % Starting lpo8_lambda_fix with 300s (1) cores
% 0.13/0.26 % Starting lpo9_lambda_fix with 300s (1) cores
% 0.13/0.26 % lpo9_lambda_fix with pid 1341089 completed with status 0
% 0.13/0.26 % Result found by lpo9_lambda_fix
% 0.13/0.26 % Preprocessing class: HSSSSLSSSLMNHSA.
% 0.13/0.26 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.13/0.26 % Starting new_ho_10 with 1500s (5) cores
% 0.13/0.26 % Starting new_ho_7 with 300s (1) cores
% 0.13/0.26 % Starting lpo8_lambda_fix with 300s (1) cores
% 0.13/0.26 % Starting lpo9_lambda_fix with 300s (1) cores
% 0.13/0.26 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = gf500_gu_R04_F100_L20000)
% 0.13/0.26 % SinE strategy is gf500_gu_R04_F100_L20000
% 0.13/0.26 % Search class: HGHSS-FFMS32-MHSFMSBN
% 0.13/0.26 % partial match(3): HGHSS-FFMS31-SHSSMSBN
% 0.13/0.26 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 0.13/0.26 % Starting SubtermCWHack with 28s (1) cores
% 0.13/0.26 % SubtermCWHack with pid 1341094 completed with status 0
% 0.13/0.26 % Result found by SubtermCWHack
% 0.13/0.26 % Preprocessing class: HSSSSLSSSLMNHSA.
% 0.13/0.26 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.13/0.26 % Starting new_ho_10 with 1500s (5) cores
% 0.13/0.26 % Starting new_ho_7 with 300s (1) cores
% 0.13/0.26 % Starting lpo8_lambda_fix with 300s (1) cores
% 0.13/0.26 % Starting lpo9_lambda_fix with 300s (1) cores
% 0.13/0.26 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = gf500_gu_R04_F100_L20000)
% 0.13/0.26 % SinE strategy is gf500_gu_R04_F100_L20000
% 0.13/0.26 % Search class: HGHSS-FFMS32-MHSFMSBN
% 0.13/0.26 % partial match(3): HGHSS-FFMS31-SHSSMSBN
% 0.13/0.26 % Scheduled 7 strats onto 1 cores with 300 seconds (300 total)
% 0.13/0.26 % Starting SubtermCWHack with 28s (1) cores
% 0.13/0.26 % Preprocessing time : 0.001 s
% 0.13/0.26
% 0.13/0.26 % Proof found!
% 0.13/0.26 % SZS status Theorem
% 0.13/0.26 % SZS output start CNFRefutation
% 0.13/0.26 thf(decl_23, type, in: $i > $i > $o).
% 0.13/0.26 thf(decl_24, type, emptyset: $i).
% 0.13/0.26 thf(decl_25, type, setadjoin: $i > $i > $i).
% 0.13/0.26 thf(decl_26, type, setunion: $i > $i).
% 0.13/0.26 thf(decl_27, type, dsetconstr: $i > ($i > $o) > $i).
% 0.13/0.26 thf(decl_28, type, iskpair: $i > $o).
% 0.13/0.26 thf(decl_29, type, kpair: $i > $i > $i).
% 0.13/0.26 thf(decl_30, type, singleton: $i > $o).
% 0.13/0.26 thf(decl_31, type, ex1: $i > ($i > $o) > $o).
% 0.13/0.26 thf(decl_32, type, ex1I: $o).
% 0.13/0.26 thf(decl_33, type, kfst: $i > $i).
% 0.13/0.26 thf(decl_34, type, kfstpairEq: $o).
% 0.13/0.26 thf(decl_35, type, setukpairinjR: $o).
% 0.13/0.26 thf(decl_36, type, esk1_3: $i > ($i > $o) > $i > $i).
% 0.13/0.26 thf(decl_37, type, esk2_3: $i > ($i > $o) > $i > $i).
% 0.13/0.26 thf(decl_38, type, esk3_0: $i).
% 0.13/0.26 thf(decl_39, type, esk4_0: $i).
% 0.13/0.26 thf(decl_40, type, esk5_0: $i).
% 0.13/0.26 thf(decl_41, type, epred1_0: $i > $o).
% 0.13/0.26 thf(ex1, axiom, ((ex1)=(^[X1:$i, X4:$i > $o]:((singleton @ (dsetconstr @ X1 @ (^[X2:$i]:((X4 @ X2)))))))), file('/export/starexec/sandbox2/tmp/tmp.ZsvHlv9XJG/E---3.1_1341058.p', ex1)).
% 0.13/0.26 thf(singleton, axiom, ((singleton)=(^[X1:$i]:(?[X2:$i]:((((in @ X2 @ X1))&(((X1)=(setadjoin @ X2 @ emptyset)))))))), file('/export/starexec/sandbox2/tmp/tmp.ZsvHlv9XJG/E---3.1_1341058.p', singleton)).
% 0.13/0.26 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/sandbox2/tmp/tmp.ZsvHlv9XJG/E---3.1_1341058.p', ex1I)).
% 0.13/0.26 thf(ksndsingleton, conjecture, ((ex1I)=>((kfstpairEq)=>((setukpairinjR)=>![X6:$i]:(((iskpair @ X6)=>(singleton @ (dsetconstr @ (setunion @ X6) @ (^[X2:$i]:(((X6)=(kpair @ (kfst @ X6) @ X2))))))))))), file('/export/starexec/sandbox2/tmp/tmp.ZsvHlv9XJG/E---3.1_1341058.p', ksndsingleton)).
% 0.13/0.26 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/sandbox2/tmp/tmp.ZsvHlv9XJG/E---3.1_1341058.p', iskpair)).
% 0.13/0.26 thf(setukpairinjR, axiom, ((setukpairinjR)<=>![X2:$i, X3:$i, X5:$i, X6:$i]:((((kpair @ X2 @ X3)=(kpair @ X5 @ X6))=>((X3)=(X6))))), file('/export/starexec/sandbox2/tmp/tmp.ZsvHlv9XJG/E---3.1_1341058.p', setukpairinjR)).
% 0.13/0.26 thf(kfstpairEq, axiom, ((kfstpairEq)<=>![X2:$i, X3:$i]:(((kfst @ (kpair @ X2 @ X3))=(X2)))), file('/export/starexec/sandbox2/tmp/tmp.ZsvHlv9XJG/E---3.1_1341058.p', kfstpairEq)).
% 0.13/0.26 thf(kpair, axiom, ((kpair)=(^[X2:$i, X3:$i]:(setadjoin @ (setadjoin @ X2 @ emptyset) @ (setadjoin @ (setadjoin @ X2 @ (setadjoin @ X3 @ emptyset)) @ emptyset)))), file('/export/starexec/sandbox2/tmp/tmp.ZsvHlv9XJG/E---3.1_1341058.p', kpair)).
% 0.13/0.26 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.13/0.26 thf(c_0_9, plain, ((singleton)=(^[Z0:$i]:(?[X2:$i]:((((in @ X2 @ Z0))&(((Z0)=(setadjoin @ X2 @ emptyset)))))))), inference(fof_simplification,[status(thm)],[singleton])).
% 0.13/0.26 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.13/0.26 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.13/0.26 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.13/0.26 thf(c_0_13, 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.13/0.26 thf(c_0_14, 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.13/0.26 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_14]), setukpairinjR]), kfstpairEq]), c_0_9])])).
% 0.13/0.26 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.13/0.26 thf(c_0_17, negated_conjecture, ![X36:$i, X37:$i > $o, X38:$i, X41:$i, X42:$i, X43:$i, X44:$i, X45:$i, X46:$i, X50:$i]:((((((in @ (esk2_3 @ X36 @ X37 @ X38) @ (dsetconstr @ X36 @ X37))|(in @ (esk1_3 @ X36 @ X37 @ X38) @ X36)|~(X37 @ X38)|~(in @ X38 @ X36))&(((dsetconstr @ X36 @ X37)=(setadjoin @ (esk2_3 @ X36 @ X37 @ X38) @ emptyset))|(in @ (esk1_3 @ X36 @ X37 @ X38) @ X36)|~(X37 @ X38)|~(in @ X38 @ X36)))&((((in @ (esk2_3 @ X36 @ X37 @ X38) @ (dsetconstr @ X36 @ X37))|(X37 @ (esk1_3 @ X36 @ X37 @ X38))|~(X37 @ X38)|~(in @ X38 @ X36))&(((dsetconstr @ X36 @ X37)=(setadjoin @ (esk2_3 @ X36 @ X37 @ X38) @ emptyset))|(X37 @ (esk1_3 @ X36 @ X37 @ X38))|~(X37 @ X38)|~(in @ X38 @ X36)))&(((in @ (esk2_3 @ X36 @ X37 @ X38) @ (dsetconstr @ X36 @ X37))|((esk1_3 @ X36 @ X37 @ X38)!=(X38))|~(X37 @ X38)|~(in @ X38 @ X36))&(((dsetconstr @ X36 @ X37)=(setadjoin @ (esk2_3 @ X36 @ X37 @ X38) @ emptyset))|((esk1_3 @ X36 @ X37 @ X38)!=(X38))|~(X37 @ X38)|~(in @ X38 @ X36)))))&(((kfst @ (kpair @ X41 @ X42))=(X41))&((((kpair @ X43 @ X44)!=(kpair @ X45 @ X46))|((X44)=(X46)))&(((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 @ X50 @ (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 @ X50 @ 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.13/0.26 thf(c_0_18, plain, ![X51:$i, X52:$i]:(((kpair @ X51 @ X52)=(setadjoin @ (setadjoin @ X51 @ emptyset) @ (setadjoin @ (setadjoin @ X51 @ (setadjoin @ X52 @ emptyset)) @ emptyset)))), inference(variable_rename,[status(thm)],[c_0_16])).
% 0.13/0.26 thf(c_0_19, 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.13/0.26 thf(c_0_20, plain, ![X53:$i]:(((epred1_0 @ X53)<=>((esk3_0)=(kpair @ (kfst @ esk3_0) @ X53)))), introduced(definition)).
% 0.13/0.26 thf(c_0_21, 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.13/0.26 thf(c_0_22, 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.13/0.26 thf(c_0_23, 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.13/0.26 thf(c_0_24, plain, ![X1:$i]:((((esk3_0)=(kpair @ (kfst @ esk3_0) @ X1))|~((epred1_0 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_19])).
% 0.13/0.26 thf(c_0_25, 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_20]), c_0_20])).
% 0.13/0.26 thf(c_0_26, negated_conjecture, ![X2:$i, X1:$i]:(((kfst @ (kpair @ X1 @ X2))=(X1))), inference(split_conjunct,[status(thm)],[c_0_17])).
% 0.13/0.26 thf(c_0_27, negated_conjecture, ((kpair @ esk4_0 @ esk5_0)=(esk3_0)), inference(rw,[status(thm)],[c_0_21, c_0_22])).
% 0.13/0.26 thf(c_0_28, plain, ![X1:$i, X3:$i, X2:$i]:((((X1)=(X2))|((kpair @ X3 @ X1)!=(esk3_0))|~((epred1_0 @ X2)))), inference(spm,[status(thm)],[c_0_23, c_0_24])).
% 0.13/0.26 thf(c_0_29, 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_25])).
% 0.13/0.26 thf(c_0_30, 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.13/0.26 thf(c_0_31, 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.13/0.26 thf(c_0_32, plain, ![X1:$i]:(((epred1_0 @ X1)|((esk3_0)!=(kpair @ (kfst @ esk3_0) @ X1)))), inference(split_conjunct,[status(thm)],[c_0_19])).
% 0.13/0.26 thf(c_0_33, negated_conjecture, ((kfst @ esk3_0)=(esk4_0)), inference(spm,[status(thm)],[c_0_26, c_0_27])).
% 0.13/0.26 thf(c_0_34, 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.13/0.26 thf(c_0_35, 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.13/0.26 thf(c_0_36, plain, ![X1:$i]:((((esk5_0)=(X1))|~((epred1_0 @ X1)))), inference(spm,[status(thm)],[c_0_28, c_0_27])).
% 0.13/0.26 thf(c_0_37, 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_29, c_0_30]), c_0_31])).
% 0.13/0.26 thf(c_0_38, plain, ![X1:$i]:(((epred1_0 @ X1)|((kpair @ esk4_0 @ X1)!=(esk3_0)))), inference(rw,[status(thm)],[c_0_32, c_0_33])).
% 0.13/0.26 thf(c_0_39, 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_29, c_0_34]), c_0_35])).
% 0.13/0.26 thf(c_0_40, 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_36, c_0_37])).
% 0.13/0.26 thf(c_0_41, negated_conjecture, (in @ esk5_0 @ (setunion @ esk3_0)), inference(split_conjunct,[status(thm)],[c_0_17])).
% 0.13/0.26 thf(c_0_42, negated_conjecture, (epred1_0 @ esk5_0), inference(spm,[status(thm)],[c_0_38, c_0_27])).
% 0.13/0.26 thf(c_0_43, plain, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_39, c_0_40])]), c_0_41]), c_0_42])]), ['proof']).
% 0.13/0.26 % SZS output end CNFRefutation
% 0.13/0.26 % Parsed axioms : 21
% 0.13/0.26 % Removed by relevancy pruning/SinE : 13
% 0.13/0.26 % Initial clauses : 15
% 0.13/0.26 % Removed in clause preprocessing : 0
% 0.13/0.26 % Initial clauses in saturation : 15
% 0.13/0.26 % Processed clauses : 77
% 0.13/0.26 % ...of these trivial : 0
% 0.13/0.26 % ...subsumed : 34
% 0.13/0.26 % ...remaining for further processing : 43
% 0.13/0.26 % Other redundant clauses eliminated : 1
% 0.13/0.26 % Clauses deleted for lack of memory : 0
% 0.13/0.26 % Backward-subsumed : 0
% 0.13/0.26 % Backward-rewritten : 3
% 0.13/0.26 % Generated clauses : 146
% 0.13/0.26 % ...of the previous two non-redundant : 133
% 0.13/0.26 % ...aggressively subsumed : 0
% 0.13/0.26 % Contextual simplify-reflections : 2
% 0.13/0.26 % Paramodulations : 143
% 0.13/0.26 % Factorizations : 0
% 0.13/0.26 % NegExts : 0
% 0.13/0.26 % Equation resolutions : 3
% 0.13/0.26 % Disequality decompositions : 0
% 0.13/0.26 % Total rewrite steps : 40
% 0.13/0.26 % ...of those cached : 24
% 0.13/0.26 % Propositional unsat checks : 0
% 0.13/0.26 % Propositional check models : 0
% 0.13/0.26 % Propositional check unsatisfiable : 0
% 0.13/0.26 % Propositional clauses : 0
% 0.13/0.26 % Propositional clauses after purity: 0
% 0.13/0.26 % Propositional unsat core size : 0
% 0.13/0.26 % Propositional preprocessing time : 0.000
% 0.13/0.26 % Propositional encoding time : 0.000
% 0.13/0.26 % Propositional solver time : 0.000
% 0.13/0.26 % Success case prop preproc time : 0.000
% 0.13/0.26 % Success case prop encoding time : 0.000
% 0.13/0.26 % Success case prop solver time : 0.000
% 0.13/0.26 % Current number of processed clauses : 40
% 0.13/0.26 % Positive orientable unit clauses : 10
% 0.13/0.26 % Positive unorientable unit clauses: 0
% 0.13/0.26 % Negative unit clauses : 0
% 0.13/0.26 % Non-unit-clauses : 30
% 0.13/0.26 % Current number of unprocessed clauses: 71
% 0.13/0.26 % ...number of literals in the above : 307
% 0.13/0.26 % Current number of archived formulas : 0
% 0.13/0.26 % Current number of archived clauses : 3
% 0.13/0.26 % Clause-clause subsumption calls (NU) : 90
% 0.13/0.26 % Rec. Clause-clause subsumption calls : 81
% 0.13/0.26 % Non-unit clause-clause subsumptions : 36
% 0.13/0.26 % Unit Clause-clause subsumption calls : 0
% 0.13/0.26 % Rewrite failures with RHS unbound : 0
% 0.13/0.26 % BW rewrite match attempts : 2
% 0.13/0.26 % BW rewrite match successes : 2
% 0.13/0.26 % Condensation attempts : 0
% 0.13/0.26 % Condensation successes : 0
% 0.13/0.26 % Termbank termtop insertions : 4585
% 0.13/0.26 % Search garbage collected termcells : 566
% 0.13/0.26
% 0.13/0.26 % -------------------------------------------------
% 0.13/0.26 % User time : 0.007 s
% 0.13/0.26 % System time : 0.002 s
% 0.13/0.26 % Total time : 0.009 s
% 0.13/0.26 % Maximum resident set size: 3648 pages
% 0.13/0.26
% 0.13/0.26 % -------------------------------------------------
% 0.13/0.26 % User time : 0.008 s
% 0.13/0.26 % System time : 0.007 s
% 0.13/0.26 % Total time : 0.015 s
% 0.13/0.26 % Maximum resident set size: 4608 pages
% 0.13/0.26 % E exiting
%------------------------------------------------------------------------------