%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : SEU678^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 : n003.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:00 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 : SEU678^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.06/0.19 % Computer : n003.cluster.edu
% 0.06/0.19 % Model : x86_64 x86_64
% 0.06/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.19 % Memory : 8046.5625MB
% 0.06/0.19 % OS : Linux 6.8.0-71-generic
% 0.06/0.19 % CPULimit : 300
% 0.06/0.19 % WCLimit : 300
% 0.06/0.19 % DateTime : Tue Sep 29 14:09:29 UTC 2026
% 0.06/0.19 % CPUTime :
% 0.06/0.19 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.06/0.23 Running higher-order theorem proving
% 0.06/0.24 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.HKJlclg9NH/E---3.1_2560332.p
% 0.21/0.27 % Version: 3.5.1-ho
% 0.21/0.27 % partial match(2): HSMSSLSSMLLCHSA
% 0.21/0.27 % Preprocessing class: HSSSSLSSMLLNHSA.
% 0.21/0.27 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.21/0.27 % Starting new_ho_10 with 1500s (5) cores
% 0.21/0.27 % Starting sh5l with 300s (1) cores
% 0.21/0.27 % Starting new_bool_1 with 300s (1) cores
% 0.21/0.27 % Starting new_bool_2 with 300s (1) cores
% 0.21/0.27 % new_ho_10 with pid 2560345 completed with status 0
% 0.21/0.27 % Result found by new_ho_10
% 0.21/0.27 % partial match(2): HSMSSLSSMLLCHSA
% 0.21/0.27 % Preprocessing class: HSSSSLSSMLLNHSA.
% 0.21/0.27 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.21/0.27 % Starting new_ho_10 with 1500s (5) cores
% 0.21/0.27 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.21/0.27 % No SInE strategy applied
% 0.21/0.27 % Search class: HGHSS-FFMF32-SHSSMMBN
% 0.21/0.27 % partial match(2): HGUNS-FFMF32-SHSSMMBN
% 0.21/0.27 % Scheduled 6 strats onto 5 cores with 1500 seconds (1500 total)
% 0.21/0.27 % Starting SubtermCWHack with 151s (1) cores
% 0.21/0.27 % Starting new_ho_10 with 750s (1) cores
% 0.21/0.27 % Starting sh5l with 188s (1) cores
% 0.21/0.27 % Starting ehoh_best_sine_rwall with 188s (1) cores
% 0.21/0.27 % Starting lpo1_def_fix with 188s (1) cores
% 0.21/0.27 % SubtermCWHack with pid 2560352 completed with status 0
% 0.21/0.27 % Result found by SubtermCWHack
% 0.21/0.27 % partial match(2): HSMSSLSSMLLCHSA
% 0.21/0.27 % Preprocessing class: HSSSSLSSMLLNHSA.
% 0.21/0.27 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.21/0.27 % Starting new_ho_10 with 1500s (5) cores
% 0.21/0.27 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.21/0.27 % No SInE strategy applied
% 0.21/0.27 % Search class: HGHSS-FFMF32-SHSSMMBN
% 0.21/0.27 % partial match(2): HGUNS-FFMF32-SHSSMMBN
% 0.21/0.27 % Scheduled 6 strats onto 5 cores with 1500 seconds (1500 total)
% 0.21/0.27 % Starting SubtermCWHack with 151s (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, setadjoin: $i > $i > $i).
% 0.21/0.27 thf(decl_26, type, dsetconstr: $i > ($i > $o) > $i).
% 0.21/0.27 thf(decl_27, type, subset: $i > $i > $o).
% 0.21/0.27 thf(decl_28, type, kpair: $i > $i > $i).
% 0.21/0.27 thf(decl_29, type, cartprod: $i > $i > $i).
% 0.21/0.27 thf(decl_30, type, singleton: $i > $o).
% 0.21/0.27 thf(decl_31, type, ex1: $i > ($i > $o) > $o).
% 0.21/0.27 thf(decl_32, type, ex1I: $o).
% 0.21/0.27 thf(decl_33, type, breln: $i > $i > $i > $o).
% 0.21/0.27 thf(decl_34, type, dpsetconstr: $i > $i > ($i > $i > $o) > $i).
% 0.21/0.27 thf(decl_35, type, dpsetconstrI: $o).
% 0.21/0.27 thf(decl_36, type, setOfPairsIsBReln: $o).
% 0.21/0.27 thf(decl_37, type, dpsetconstrERa: $o).
% 0.21/0.27 thf(decl_38, type, func: $i > $i > $i > $o).
% 0.21/0.27 thf(decl_39, type, esk1_3: $i > ($i > $o) > $i > $i).
% 0.21/0.27 thf(decl_40, type, esk2_3: $i > ($i > $o) > $i > $i).
% 0.21/0.27 thf(decl_41, type, esk3_0: $i).
% 0.21/0.27 thf(decl_42, type, esk4_0: $i).
% 0.21/0.27 thf(decl_43, type, esk5_0: $i > $i).
% 0.21/0.27 thf(decl_44, type, esk6_0: $i).
% 0.21/0.27 thf(decl_45, type, epred1_0: $i > $i > $o).
% 0.21/0.27 thf(decl_46, type, epred2_0: $i > $o).
% 0.21/0.27 thf(ex1, axiom, ((ex1)=(^[X1:$i, X3:$i > $o]:((singleton @ (dsetconstr @ X1 @ (^[X2:$i]:((X3 @ X2)))))))), file('/export/starexec/sandbox2/tmp/tmp.HKJlclg9NH/E---3.1_2560332.p', ex1)).
% 0.21/0.27 thf(singleton, axiom, ((singleton)=(^[X1:$i]:(?[X2:$i]:((((in @ X2 @ X1))&(((X1)=(setadjoin @ X2 @ emptyset)))))))), file('/export/starexec/sandbox2/tmp/tmp.HKJlclg9NH/E---3.1_2560332.p', singleton)).
% 0.21/0.27 thf(ex1I, axiom, ((ex1I)<=>![X1:$i, X3:$i > $o, X2:$i]:(((in @ X2 @ X1)=>((X3 @ X2)=>(![X4:$i]:(((in @ X4 @ X1)=>((X3 @ X4)=>((X4)=(X2)))))=>(ex1 @ X1 @ (^[X4:$i]:((X3 @ X4))))))))), file('/export/starexec/sandbox2/tmp/tmp.HKJlclg9NH/E---3.1_2560332.p', ex1I)).
% 0.21/0.27 thf(setOfPairsIsBReln, axiom, ((setOfPairsIsBReln)<=>![X1:$i, X5:$i, X10:$i > $i > $o]:((breln @ X1 @ X5 @ (dpsetconstr @ X1 @ X5 @ (^[X2:$i, X4:$i]:((X10 @ X2 @ X4))))))), file('/export/starexec/sandbox2/tmp/tmp.HKJlclg9NH/E---3.1_2560332.p', setOfPairsIsBReln)).
% 0.21/0.27 thf(breln, axiom, ((breln)=(^[X1:$i, X5:$i, X6:$i]:((subset @ X6 @ (cartprod @ X1 @ X5))))), file('/export/starexec/sandbox2/tmp/tmp.HKJlclg9NH/E---3.1_2560332.p', breln)).
% 0.21/0.27 thf(func, axiom, ((func)=(^[X1:$i, X5:$i, X12:$i]:((((breln @ X1 @ X5 @ X12))&(![X2:$i]:((((in @ X2 @ X1))=>((ex1 @ X5 @ (^[X4:$i]:((in @ (kpair @ X2 @ X4) @ X12)))))))))))), file('/export/starexec/sandbox2/tmp/tmp.HKJlclg9NH/E---3.1_2560332.p', func)).
% 0.21/0.27 thf(lamProp, conjecture, ((ex1I)=>((dpsetconstrI)=>((setOfPairsIsBReln)=>((dpsetconstrERa)=>![X1:$i, X5:$i, X13:$i > $i]:((![X2:$i]:(((in @ X2 @ X1)=>(in @ (X13 @ X2) @ X5)))=>(func @ X1 @ X5 @ (dpsetconstr @ X1 @ X5 @ (^[X2:$i, X4:$i]:(((X13 @ X2)=(X4)))))))))))), file('/export/starexec/sandbox2/tmp/tmp.HKJlclg9NH/E---3.1_2560332.p', lamProp)).
% 0.21/0.27 thf(dpsetconstrI, axiom, ((dpsetconstrI)<=>![X1:$i, X5:$i, X7:$i > $i > $o, X2:$i]:(((in @ X2 @ X1)=>![X4:$i]:(((in @ X4 @ X5)=>((X7 @ X2 @ X4)=>(in @ (kpair @ X2 @ X4) @ (dpsetconstr @ X1 @ X5 @ (^[X8:$i, X9:$i]:((X7 @ X8 @ X9))))))))))), file('/export/starexec/sandbox2/tmp/tmp.HKJlclg9NH/E---3.1_2560332.p', dpsetconstrI)).
% 0.21/0.27 thf(dpsetconstrERa, axiom, ((dpsetconstrERa)<=>![X1:$i, X5:$i, X11:$i > $i > $o, X2:$i]:(((in @ X2 @ X1)=>![X4:$i]:(((in @ X4 @ X5)=>((in @ (kpair @ X2 @ X4) @ (dpsetconstr @ X1 @ X5 @ (^[X8:$i, X9:$i]:((X11 @ X8 @ X9)))))=>(X11 @ X2 @ X4))))))), file('/export/starexec/sandbox2/tmp/tmp.HKJlclg9NH/E---3.1_2560332.p', dpsetconstrERa)).
% 0.21/0.27 thf(c_0_9, plain, ((ex1)=(^[Z0:$i, Z1:$i > $o]:((?[X35:$i]:((((in @ X35 @ (dsetconstr @ Z0 @ (^[Z2:$i]:((Z1 @ Z2))))))&(((dsetconstr @ Z0 @ (^[Z2:$i]:((Z1 @ Z2))))=(setadjoin @ X35 @ emptyset))))))))), inference(fof_simplification,[status(thm)],[ex1])).
% 0.21/0.27 thf(c_0_10, plain, ((singleton)=(^[Z0:$i]:(?[X2:$i]:((((in @ X2 @ Z0))&(((Z0)=(setadjoin @ X2 @ emptyset)))))))), inference(fof_simplification,[status(thm)],[singleton])).
% 0.21/0.27 thf(c_0_11, plain, ((ex1I)<=>![X1:$i, X3:$i > $o, X2:$i]:(((in @ X2 @ X1)=>((X3 @ X2)=>(![X4:$i]:(((in @ X4 @ X1)=>((X3 @ X4)=>((X4)=(X2)))))=>(ex1 @ X1 @ (^[Z0:$i]:((X3 @ Z0))))))))), inference(fof_simplification,[status(thm)],[ex1I])).
% 0.21/0.27 thf(c_0_12, plain, ((ex1)=(^[Z0:$i, Z1:$i > $o]:((?[X35:$i]:((((in @ X35 @ (dsetconstr @ Z0 @ (^[Z2:$i]:((Z1 @ Z2))))))&(((dsetconstr @ Z0 @ (^[Z2:$i]:((Z1 @ Z2))))=(setadjoin @ X35 @ emptyset))))))))), inference(apply_def,[status(thm)],[c_0_9, c_0_10])).
% 0.21/0.27 thf(c_0_13, plain, ((setOfPairsIsBReln)<=>![X1:$i, X5:$i, X10:$i > $i > $o]:((breln @ X1 @ X5 @ (dpsetconstr @ X1 @ X5 @ (^[Z0:$i, Z1:$i]:((X10 @ Z0 @ Z1))))))), inference(fof_simplification,[status(thm)],[setOfPairsIsBReln])).
% 0.21/0.27 thf(c_0_14, plain, ((breln)=(^[Z0:$i, Z1:$i, Z2:$i]:((subset @ Z2 @ (cartprod @ Z0 @ Z1))))), inference(fof_simplification,[status(thm)],[breln])).
% 0.21/0.27 thf(c_0_15, plain, ((func)=(^[Z0:$i, Z1:$i, Z2:$i]:(((((subset @ Z2 @ (cartprod @ Z0 @ Z1))))&(![X2:$i]:((((in @ X2 @ Z0))=>((?[X37:$i]:((((in @ X37 @ (dsetconstr @ Z1 @ (^[Z3:$i]:(((in @ (kpair @ X2 @ Z3) @ Z2)))))))&(((dsetconstr @ Z1 @ (^[Z3:$i]:(((in @ (kpair @ X2 @ Z3) @ Z2)))))=(setadjoin @ X37 @ emptyset)))))))))))))), inference(fof_simplification,[status(thm)],[func])).
% 0.21/0.27 thf(c_0_16, negated_conjecture, ~(((ex1I)=>((dpsetconstrI)=>((setOfPairsIsBReln)=>((dpsetconstrERa)=>![X1:$i, X5:$i, X13:$i > $i]:((![X2:$i]:(((in @ X2 @ X1)=>(in @ (X13 @ X2) @ X5)))=>(func @ X1 @ X5 @ (dpsetconstr @ X1 @ X5 @ (^[X2:$i, X4:$i]:(((X13 @ X2)=(X4))))))))))))), inference(assume_negation,[status(cth)],[lamProp])).
% 0.21/0.27 thf(c_0_17, plain, ((ex1I)=(![X1:$i, X3:$i > $o, X2:$i]:((((in @ X2 @ X1))=>((((X3 @ X2))=>(((![X4:$i]:((((in @ X4 @ X1))=>((((X3 @ X4))=>(((X4)=(X2))))))))=>((?[X36:$i]:((((in @ X36 @ (dsetconstr @ X1 @ (^[Z0:$i]:(((X3 @ Z0)))))))&(((dsetconstr @ X1 @ (^[Z0:$i]:(((X3 @ Z0)))))=(setadjoin @ X36 @ emptyset))))))))))))))), inference(apply_def,[status(thm)],[c_0_11, c_0_12])).
% 0.21/0.27 thf(c_0_18, plain, ((dpsetconstrI)<=>![X1:$i, X5:$i, X7:$i > $i > $o, X2:$i]:(((in @ X2 @ X1)=>![X4:$i]:(((in @ X4 @ X5)=>((X7 @ X2 @ X4)=>(in @ (kpair @ X2 @ X4) @ (dpsetconstr @ X1 @ X5 @ (^[Z0:$i, Z1:$i]:((X7 @ Z0 @ Z1))))))))))), inference(fof_simplification,[status(thm)],[dpsetconstrI])).
% 0.21/0.27 thf(c_0_19, plain, ((setOfPairsIsBReln)=(![X1:$i, X5:$i, X10:$i > $i > $o]:(((subset @ (dpsetconstr @ X1 @ X5 @ (^[Z0:$i, Z1:$i]:((X10 @ Z0 @ Z1)))) @ (cartprod @ X1 @ X5)))))), inference(apply_def,[status(thm)],[c_0_13, c_0_14])).
% 0.21/0.27 thf(c_0_20, plain, ((dpsetconstrERa)<=>![X1:$i, X5:$i, X11:$i > $i > $o, X2:$i]:(((in @ X2 @ X1)=>![X4:$i]:(((in @ X4 @ X5)=>((in @ (kpair @ X2 @ X4) @ (dpsetconstr @ X1 @ X5 @ (^[Z0:$i, Z1:$i]:((X11 @ Z0 @ Z1)))))=>(X11 @ X2 @ X4))))))), inference(fof_simplification,[status(thm)],[dpsetconstrERa])).
% 0.21/0.27 thf(c_0_21, plain, ((func)=(^[Z0:$i, Z1:$i, Z2:$i]:(((((subset @ Z2 @ (cartprod @ Z0 @ Z1))))&(![X2:$i]:((((in @ X2 @ Z0))=>((?[X37:$i]:((((in @ X37 @ (dsetconstr @ Z1 @ (^[Z3:$i]:(((in @ (kpair @ X2 @ Z3) @ Z2)))))))&(((dsetconstr @ Z1 @ (^[Z3:$i]:(((in @ (kpair @ X2 @ Z3) @ Z2)))))=(setadjoin @ X37 @ emptyset)))))))))))))), inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[c_0_15, c_0_12]), c_0_14])).
% 0.21/0.27 thf(c_0_22, negated_conjecture, ~((![X38:$i, X39:$i > $o, X40:$i]:(((in @ X40 @ X38)=>((X39 @ X40)=>(![X41:$i]:(((in @ X41 @ X38)=>((X39 @ X41)=>((X41)=(X40)))))=>?[X42:$i]:(((in @ X42 @ (dsetconstr @ X38 @ X39))&((dsetconstr @ X38 @ X39)=(setadjoin @ X42 @ emptyset))))))))=>(![X43:$i, X44:$i, X45:$i > $i > $o, X46:$i]:(((in @ X46 @ X43)=>![X47:$i]:(((in @ X47 @ X44)=>((X45 @ X46 @ X47)=>(in @ (kpair @ X46 @ X47) @ (dpsetconstr @ X43 @ X44 @ X45)))))))=>(![X48:$i, X49:$i, X50:$i > $i > $o]:((subset @ (dpsetconstr @ X48 @ X49 @ X50) @ (cartprod @ X48 @ X49)))=>(![X51:$i, X52:$i, X53:$i > $i > $o, X54:$i]:(((in @ X54 @ X51)=>![X55:$i]:(((in @ X55 @ X52)=>((in @ (kpair @ X54 @ X55) @ (dpsetconstr @ X51 @ X52 @ X53))=>(X53 @ X54 @ X55))))))=>![X1:$i, X5:$i, X13:$i > $i]:((![X2:$i]:(((in @ X2 @ X1)=>(in @ (X13 @ X2) @ X5)))=>((subset @ (dpsetconstr @ X1 @ X5 @ (^[Z0:$i]:($eq @ (X13 @ Z0)))) @ (cartprod @ X1 @ X5))&![X56:$i]:(((in @ X56 @ X1)=>?[X57:$i]:(((in @ X57 @ (dsetconstr @ X5 @ (^[Z0:$i]:((in @ (kpair @ X56 @ Z0) @ (dpsetconstr @ X1 @ X5 @ (^[Z1:$i]:($eq @ (X13 @ Z1)))))))))&((dsetconstr @ X5 @ (^[Z0:$i]:((in @ (kpair @ X56 @ Z0) @ (dpsetconstr @ X1 @ X5 @ (^[Z1:$i]:($eq @ (X13 @ Z1))))))))=(setadjoin @ X57 @ 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_16]), c_0_17]), c_0_18]), c_0_19]), c_0_20]), c_0_21])])).
% 0.21/0.27 thf(c_0_23, negated_conjecture, ![X58:$i, X59:$i > $o, X60:$i, X63:$i, X64:$i, X65:$i > $i > $o, X66:$i, X67:$i, X68:$i, X69:$i, X70:$i > $i > $o, X71:$i, X72:$i, X73:$i > $i > $o, X74:$i, X75:$i, X79:$i, X81:$i]:((((((in @ (esk2_3 @ X58 @ X59 @ X60) @ (dsetconstr @ X58 @ X59))|(in @ (esk1_3 @ X58 @ X59 @ X60) @ X58)|~(X59 @ X60)|~(in @ X60 @ X58))&(((dsetconstr @ X58 @ X59)=(setadjoin @ (esk2_3 @ X58 @ X59 @ X60) @ emptyset))|(in @ (esk1_3 @ X58 @ X59 @ X60) @ X58)|~(X59 @ X60)|~(in @ X60 @ X58)))&((((in @ (esk2_3 @ X58 @ X59 @ X60) @ (dsetconstr @ X58 @ X59))|(X59 @ (esk1_3 @ X58 @ X59 @ X60))|~(X59 @ X60)|~(in @ X60 @ X58))&(((dsetconstr @ X58 @ X59)=(setadjoin @ (esk2_3 @ X58 @ X59 @ X60) @ emptyset))|(X59 @ (esk1_3 @ X58 @ X59 @ X60))|~(X59 @ X60)|~(in @ X60 @ X58)))&(((in @ (esk2_3 @ X58 @ X59 @ X60) @ (dsetconstr @ X58 @ X59))|((esk1_3 @ X58 @ X59 @ X60)!=(X60))|~(X59 @ X60)|~(in @ X60 @ X58))&(((dsetconstr @ X58 @ X59)=(setadjoin @ (esk2_3 @ X58 @ X59 @ X60) @ emptyset))|((esk1_3 @ X58 @ X59 @ X60)!=(X60))|~(X59 @ X60)|~(in @ X60 @ X58)))))&((~(in @ X66 @ X63)|(~(in @ X67 @ X64)|(~(X65 @ X66 @ X67)|(in @ (kpair @ X66 @ X67) @ (dpsetconstr @ X63 @ X64 @ X65)))))&((subset @ (dpsetconstr @ X68 @ X69 @ X70) @ (cartprod @ X68 @ X69))&((~(in @ X74 @ X71)|(~(in @ X75 @ X72)|(~(in @ (kpair @ X74 @ X75) @ (dpsetconstr @ X71 @ X72 @ X73))|(X73 @ X74 @ X75))))&((~(in @ X79 @ esk3_0)|(in @ (esk5_0 @ X79) @ esk4_0))&(((in @ esk6_0 @ esk3_0)|~(subset @ (dpsetconstr @ esk3_0 @ esk4_0 @ (^[Z0:$i]:($eq @ (esk5_0 @ Z0)))) @ (cartprod @ esk3_0 @ esk4_0)))&(~(in @ X81 @ (dsetconstr @ esk4_0 @ (^[Z0:$i]:((in @ (kpair @ esk6_0 @ Z0) @ (dpsetconstr @ esk3_0 @ esk4_0 @ (^[Z1:$i]:($eq @ (esk5_0 @ Z1)))))))))|((dsetconstr @ esk4_0 @ (^[Z0:$i]:((in @ (kpair @ esk6_0 @ Z0) @ (dpsetconstr @ esk3_0 @ esk4_0 @ (^[Z1:$i]:($eq @ (esk5_0 @ Z1))))))))!=(setadjoin @ X81 @ emptyset))|~(subset @ (dpsetconstr @ esk3_0 @ esk4_0 @ (^[Z0:$i]:($eq @ (esk5_0 @ Z0)))) @ (cartprod @ esk3_0 @ esk4_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_22])])])])])])).
% 0.21/0.27 thf(c_0_24, plain, ![X82:$i]:(((epred1_0 @ X82)=($eq @ (esk5_0 @ X82)))), introduced(definition)).
% 0.21/0.27 thf(c_0_25, plain, ![X88:$i]:(((epred1_0 @ X88)=($eq @ (esk5_0 @ X88)))), inference(variable_rename,[status(thm)],[])).
% 0.21/0.27 thf(c_0_26, plain, ![X89:$i]:(((~(epred2_0 @ X89)|(in @ (kpair @ esk6_0 @ X89) @ (dpsetconstr @ esk3_0 @ esk4_0 @ epred1_0)))&(~(in @ (kpair @ esk6_0 @ X89) @ (dpsetconstr @ esk3_0 @ esk4_0 @ epred1_0))|(epred2_0 @ X89)))), inference(fof_nnf,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[])])])).
% 0.21/0.27 thf(c_0_27, negated_conjecture, ((in @ esk6_0 @ esk3_0)|~((((subset @ (dpsetconstr @ esk3_0 @ esk4_0 @ epred1_0) @ (cartprod @ esk3_0 @ esk4_0)))=(($true))))), inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_23]), c_0_24])).
% 0.21/0.27 thf(c_0_28, negated_conjecture, ![X1:$i, X7:$i > $i > $o, X2:$i]:((subset @ (dpsetconstr @ X1 @ X2 @ X7) @ (cartprod @ X1 @ X2))), inference(split_conjunct,[status(thm)],[c_0_23])).
% 0.21/0.27 thf(c_0_29, plain, ![X1:$i]:(((epred1_0 @ X1)=($eq @ (esk5_0 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_25])).
% 0.21/0.27 thf(c_0_30, plain, ![X1:$i]:(((epred2_0 @ X1)|~((in @ (kpair @ esk6_0 @ X1) @ (dpsetconstr @ esk3_0 @ esk4_0 @ epred1_0))))), inference(split_conjunct,[status(thm)],[c_0_26])).
% 0.21/0.27 thf(c_0_31, negated_conjecture, ![X2:$i, X1:$i, X7:$i > $i > $o, X5:$i, X4:$i]:(((in @ (kpair @ X1 @ X4) @ (dpsetconstr @ X2 @ X5 @ X7))|~((in @ X1 @ X2))|~((in @ X4 @ X5))|~((X7 @ X1 @ X4)))), inference(split_conjunct,[status(thm)],[c_0_23])).
% 0.21/0.27 thf(c_0_32, negated_conjecture, (in @ esk6_0 @ esk3_0), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(cn,[status(thm)],[c_0_27]), c_0_28])])).
% 0.21/0.27 thf(c_0_33, plain, ![X1:$i, X90:$i]:((((esk5_0 @ X1)=(X90))<=>(epred1_0 @ X1 @ X90))), inference(arg_cong,[status(thm)],[c_0_29])).
% 0.21/0.27 thf(c_0_34, plain, ![X83:$i]:(((epred2_0 @ X83)<=>(in @ (kpair @ esk6_0 @ X83) @ (dpsetconstr @ esk3_0 @ esk4_0 @ epred1_0)))), introduced(definition)).
% 0.21/0.27 thf(c_0_35, negated_conjecture, ![X3:$i > $o, X2:$i, X1:$i]:((((dsetconstr @ X1 @ X3)=(setadjoin @ (esk2_3 @ X1 @ X3 @ X2) @ emptyset))|(X3 @ (esk1_3 @ X1 @ X3 @ X2))|~((X3 @ X2))|~((in @ X2 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_23])).
% 0.21/0.27 thf(c_0_36, negated_conjecture, ![X1:$i]:(((in @ (esk5_0 @ X1) @ esk4_0)|~((in @ X1 @ esk3_0)))), inference(split_conjunct,[status(thm)],[c_0_23])).
% 0.21/0.27 thf(c_0_37, plain, ![X1:$i]:(((epred2_0 @ X1)|~((in @ X1 @ esk4_0))|~((epred1_0 @ esk6_0 @ X1)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_30, c_0_31]), c_0_32])])).
% 0.21/0.27 thf(c_0_38, plain, ![X1:$i]:((epred1_0 @ X1 @ (esk5_0 @ X1))), inference(er,[status(thm)],[inference(dynamic_cnf,[status(thm)],[c_0_33])])).
% 0.21/0.27 thf(c_0_39, negated_conjecture, ![X1:$i]:((~((((in @ X1 @ (dsetconstr @ esk4_0 @ epred2_0)))=(($true))))|((dsetconstr @ esk4_0 @ epred2_0)!=(setadjoin @ X1 @ emptyset))|~((((subset @ (dpsetconstr @ esk3_0 @ esk4_0 @ epred1_0) @ (cartprod @ esk3_0 @ esk4_0)))=(($true)))))), inference(lift_lambdas,[status(thm)],[inference(lift_lambdas,[status(thm)],[inference(lift_lambdas,[status(thm)],[inference(lift_lambdas,[status(thm)],[inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_23]), c_0_24]), c_0_34]), c_0_24]), c_0_34]), c_0_24])).
% 0.21/0.27 thf(c_0_40, negated_conjecture, ![X3:$i > $o, X2:$i, X1:$i]:((((dsetconstr @ X1 @ X3)=(setadjoin @ (esk2_3 @ X1 @ X3 @ X2) @ emptyset))|(in @ (esk1_3 @ X1 @ X3 @ X2) @ X1)|~((X3 @ X2))|~((in @ X2 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_23])).
% 0.21/0.27 thf(c_0_41, negated_conjecture, ![X3:$i > $o, X1:$i]:((((setadjoin @ (esk2_3 @ esk4_0 @ X3 @ (esk5_0 @ X1)) @ emptyset)=(dsetconstr @ esk4_0 @ X3))|(X3 @ (esk1_3 @ esk4_0 @ X3 @ (esk5_0 @ X1)))|~((in @ X1 @ esk3_0))|~((X3 @ (esk5_0 @ X1))))), inference(spm,[status(thm)],[c_0_35, c_0_36])).
% 0.21/0.27 thf(c_0_42, plain, ((epred2_0 @ (esk5_0 @ esk6_0))|~((in @ (esk5_0 @ esk6_0) @ esk4_0))), inference(spm,[status(thm)],[c_0_37, c_0_38])).
% 0.21/0.27 thf(c_0_43, negated_conjecture, ![X1:$i, X2:$i, X4:$i, X5:$i, X7:$i > $i > $o]:(((X7 @ X1 @ X4)|~((in @ X1 @ X2))|~((in @ X4 @ X5))|~((in @ (kpair @ X1 @ X4) @ (dpsetconstr @ X2 @ X5 @ X7))))), inference(split_conjunct,[status(thm)],[c_0_23])).
% 0.21/0.27 thf(c_0_44, plain, ![X1:$i]:(((in @ (kpair @ esk6_0 @ X1) @ (dpsetconstr @ esk3_0 @ esk4_0 @ epred1_0))|~((epred2_0 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_26])).
% 0.21/0.27 thf(c_0_45, negated_conjecture, ![X1:$i]:((((setadjoin @ X1 @ emptyset)!=(dsetconstr @ esk4_0 @ epred2_0))|~((in @ X1 @ (dsetconstr @ esk4_0 @ epred2_0))))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(cn,[status(thm)],[c_0_39]), c_0_28])])).
% 0.21/0.27 thf(c_0_46, negated_conjecture, ![X3:$i > $o, X1:$i]:((((setadjoin @ (esk2_3 @ esk4_0 @ X3 @ (esk5_0 @ X1)) @ emptyset)=(dsetconstr @ esk4_0 @ X3))|(in @ (esk1_3 @ esk4_0 @ X3 @ (esk5_0 @ X1)) @ esk4_0)|~((in @ X1 @ esk3_0))|~((X3 @ (esk5_0 @ X1))))), inference(spm,[status(thm)],[c_0_40, c_0_36])).
% 0.21/0.27 thf(c_0_47, negated_conjecture, ![X3:$i > $o]:((((setadjoin @ (esk2_3 @ esk4_0 @ X3 @ (esk5_0 @ esk6_0)) @ emptyset)=(dsetconstr @ esk4_0 @ X3))|(X3 @ (esk1_3 @ esk4_0 @ X3 @ (esk5_0 @ esk6_0)))|~((X3 @ (esk5_0 @ esk6_0))))), inference(spm,[status(thm)],[c_0_41, c_0_32])).
% 0.21/0.27 thf(c_0_48, negated_conjecture, (epred2_0 @ (esk5_0 @ esk6_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_42, c_0_36]), c_0_32])])).
% 0.21/0.27 thf(c_0_49, plain, ![X1:$i, X2:$i]:((((esk5_0 @ X1)=(X2))|~((epred1_0 @ X1 @ X2)))), inference(dynamic_cnf,[status(thm)],[c_0_33])).
% 0.21/0.27 thf(c_0_50, plain, ![X1:$i]:(((epred1_0 @ esk6_0 @ X1)|~((in @ X1 @ esk4_0))|~((epred2_0 @ X1)))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_43, c_0_44]), c_0_32])])).
% 0.21/0.27 thf(c_0_51, negated_conjecture, ![X3:$i > $o, X1:$i]:(((in @ (esk1_3 @ esk4_0 @ X3 @ (esk5_0 @ X1)) @ esk4_0)|((dsetconstr @ esk4_0 @ X3)!=(dsetconstr @ esk4_0 @ epred2_0))|~((in @ (esk2_3 @ esk4_0 @ X3 @ (esk5_0 @ X1)) @ (dsetconstr @ esk4_0 @ epred2_0)))|~((in @ X1 @ esk3_0))|~((X3 @ (esk5_0 @ X1))))), inference(spm,[status(thm)],[c_0_45, c_0_46])).
% 0.21/0.27 thf(c_0_52, negated_conjecture, ![X3:$i > $o, X2:$i, X1:$i]:(((in @ (esk2_3 @ X1 @ X3 @ X2) @ (dsetconstr @ X1 @ X3))|(in @ (esk1_3 @ X1 @ X3 @ X2) @ X1)|~((X3 @ X2))|~((in @ X2 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_23])).
% 0.21/0.27 thf(c_0_53, negated_conjecture, (((setadjoin @ (esk2_3 @ esk4_0 @ epred2_0 @ (esk5_0 @ esk6_0)) @ emptyset)=(dsetconstr @ esk4_0 @ epred2_0))|(epred2_0 @ (esk1_3 @ esk4_0 @ epred2_0 @ (esk5_0 @ esk6_0)))), inference(spm,[status(thm)],[c_0_47, c_0_48])).
% 0.21/0.27 thf(c_0_54, negated_conjecture, ![X3:$i > $o, X2:$i, X1:$i]:((((dsetconstr @ X1 @ X3)=(setadjoin @ (esk2_3 @ X1 @ X3 @ X2) @ emptyset))|((esk1_3 @ X1 @ X3 @ X2)!=(X2))|~((X3 @ X2))|~((in @ X2 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_23])).
% 0.21/0.27 thf(c_0_55, plain, ![X1:$i]:((((esk5_0 @ esk6_0)=(X1))|~((in @ X1 @ esk4_0))|~((epred2_0 @ X1)))), inference(spm,[status(thm)],[c_0_49, c_0_50])).
% 0.21/0.27 thf(c_0_56, negated_conjecture, ![X1:$i]:(((in @ (esk1_3 @ esk4_0 @ epred2_0 @ (esk5_0 @ X1)) @ esk4_0)|~((in @ X1 @ esk3_0))|~((epred2_0 @ (esk5_0 @ X1))))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_51, c_0_52]), c_0_36])).
% 0.21/0.27 thf(c_0_57, negated_conjecture, ((epred2_0 @ (esk1_3 @ esk4_0 @ epred2_0 @ (esk5_0 @ esk6_0)))|~((in @ (esk2_3 @ esk4_0 @ epred2_0 @ (esk5_0 @ esk6_0)) @ (dsetconstr @ esk4_0 @ epred2_0)))), inference(spm,[status(thm)],[c_0_45, c_0_53])).
% 0.21/0.27 thf(c_0_58, negated_conjecture, ![X3:$i > $o, X2:$i, X1:$i]:(((in @ (esk2_3 @ X1 @ X3 @ X2) @ (dsetconstr @ X1 @ X3))|(X3 @ (esk1_3 @ X1 @ X3 @ X2))|~((X3 @ X2))|~((in @ X2 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_23])).
% 0.21/0.27 thf(c_0_59, negated_conjecture, ![X1:$i, X3:$i > $o, X2:$i]:((((dsetconstr @ X1 @ X3)!=(dsetconstr @ esk4_0 @ epred2_0))|((esk1_3 @ X1 @ X3 @ X2)!=(X2))|~((in @ (esk2_3 @ X1 @ X3 @ X2) @ (dsetconstr @ esk4_0 @ epred2_0)))|~((in @ X2 @ X1))|~((X3 @ X2)))), inference(spm,[status(thm)],[c_0_45, c_0_54])).
% 0.21/0.27 thf(c_0_60, negated_conjecture, ![X3:$i > $o, X2:$i, X1:$i]:(((in @ (esk2_3 @ X1 @ X3 @ X2) @ (dsetconstr @ X1 @ X3))|((esk1_3 @ X1 @ X3 @ X2)!=(X2))|~((X3 @ X2))|~((in @ X2 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_23])).
% 0.21/0.27 thf(c_0_61, plain, ![X1:$i]:((((esk1_3 @ esk4_0 @ epred2_0 @ (esk5_0 @ X1))=(esk5_0 @ esk6_0))|~((epred2_0 @ (esk1_3 @ esk4_0 @ epred2_0 @ (esk5_0 @ X1))))|~((in @ X1 @ esk3_0))|~((epred2_0 @ (esk5_0 @ X1))))), inference(spm,[status(thm)],[c_0_55, c_0_56])).
% 0.21/0.27 thf(c_0_62, negated_conjecture, ((epred2_0 @ (esk1_3 @ esk4_0 @ epred2_0 @ (esk5_0 @ esk6_0)))|~((in @ (esk5_0 @ esk6_0) @ esk4_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_57, c_0_58]), c_0_48])])).
% 0.21/0.27 thf(c_0_63, negated_conjecture, ![X1:$i]:((((esk1_3 @ esk4_0 @ epred2_0 @ X1)!=(X1))|~((in @ X1 @ esk4_0))|~((epred2_0 @ X1)))), inference(spm,[status(thm)],[c_0_59, c_0_60])).
% 0.21/0.27 thf(c_0_64, negated_conjecture, (((esk1_3 @ esk4_0 @ epred2_0 @ (esk5_0 @ esk6_0))=(esk5_0 @ esk6_0))|~((in @ (esk5_0 @ esk6_0) @ esk4_0))), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_61, c_0_62]), c_0_32]), c_0_48])])).
% 0.21/0.27 thf(c_0_65, negated_conjecture, ~((in @ (esk5_0 @ esk6_0) @ esk4_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_63, c_0_64]), c_0_48])])).
% 0.21/0.27 thf(c_0_66, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_65, c_0_36]), c_0_32])]), ['proof']).
% 0.21/0.27 % SZS output end CNFRefutation
% 0.21/0.27 % Parsed axioms : 25
% 0.21/0.27 % Removed by relevancy pruning/SinE : 0
% 0.21/0.27 % Initial clauses : 31
% 0.21/0.27 % Removed in clause preprocessing : 16
% 0.21/0.27 % Initial clauses in saturation : 15
% 0.21/0.27 % Processed clauses : 51
% 0.21/0.27 % ...of these trivial : 2
% 0.21/0.27 % ...subsumed : 3
% 0.21/0.27 % ...remaining for further processing : 46
% 0.21/0.27 % Other redundant clauses eliminated : 1
% 0.21/0.27 % Clauses deleted for lack of memory : 0
% 0.21/0.27 % Backward-subsumed : 2
% 0.21/0.27 % Backward-rewritten : 1
% 0.21/0.27 % Generated clauses : 57
% 0.21/0.27 % ...of the previous two non-redundant : 50
% 0.21/0.27 % ...aggressively subsumed : 0
% 0.21/0.27 % Contextual simplify-reflections : 1
% 0.21/0.27 % Paramodulations : 53
% 0.21/0.27 % Factorizations : 0
% 0.21/0.27 % NegExts : 0
% 0.21/0.27 % Equation resolutions : 1
% 0.21/0.27 % Disequality decompositions : 0
% 0.21/0.27 % Total rewrite steps : 17
% 0.21/0.27 % ...of those cached : 14
% 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 : 42
% 0.21/0.27 % Positive orientable unit clauses : 5
% 0.21/0.27 % Positive unorientable unit clauses: 0
% 0.21/0.27 % Negative unit clauses : 1
% 0.21/0.27 % Non-unit-clauses : 36
% 0.21/0.27 % Current number of unprocessed clauses: 14
% 0.21/0.27 % ...number of literals in the above : 78
% 0.21/0.27 % Current number of archived formulas : 0
% 0.21/0.27 % Current number of archived clauses : 4
% 0.21/0.27 % Clause-clause subsumption calls (NU) : 216
% 0.21/0.27 % Rec. Clause-clause subsumption calls : 69
% 0.21/0.27 % Non-unit clause-clause subsumptions : 4
% 0.21/0.27 % Unit Clause-clause subsumption calls : 13
% 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 : 5150
% 0.21/0.27 % Search garbage collected termcells : 979
% 0.21/0.27
% 0.21/0.27 % -------------------------------------------------
% 0.21/0.27 % User time : 0.009 s
% 0.21/0.27 % System time : 0.006 s
% 0.21/0.27 % Total time : 0.016 s
% 0.21/0.27 % Maximum resident set size: 3664 pages
% 0.21/0.27
% 0.21/0.27 % -------------------------------------------------
% 0.21/0.27 % User time : 0.030 s
% 0.21/0.27 % System time : 0.017 s
% 0.21/0.27 % Total time : 0.047 s
% 0.21/0.27 % Maximum resident set size: 4864 pages
% 0.21/0.27 % E exiting
%------------------------------------------------------------------------------