%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : SEU770^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 : n011.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:33 AM UTC 2026
% Result : Theorem 7.55s 1.24s
% Output : CNFRefutation 7.55s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU770^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.10/0.17 % Computer : n011.cluster.edu
% 0.10/0.17 % Model : x86_64 x86_64
% 0.10/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.17 % Memory : 8046.5625MB
% 0.10/0.17 % OS : Linux 6.8.0-71-generic
% 0.10/0.17 % CPULimit : 300
% 0.10/0.17 % WCLimit : 300
% 0.10/0.17 % DateTime : Tue Sep 29 14:24:01 UTC 2026
% 0.10/0.17 % CPUTime :
% 0.10/0.17 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.21 Running higher-order theorem proving
% 0.10/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.4GulGKTwbg/E---3.1_161017.p
% 7.55/1.24 % Version: 3.5.1-ho
% 7.55/1.24 % partial match(2): HSMSSMSSMLMNHSN
% 7.55/1.24 % Preprocessing class: HSMSSLSSMLMNHSA.
% 7.55/1.24 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 7.55/1.24 % Starting ho_unfolding_3 with 1500s (5) cores
% 7.55/1.24 % Starting ehoh_best2_full_lfho with 300s (1) cores
% 7.55/1.24 % Starting almost_fo_3_lam with 300s (1) cores
% 7.55/1.24 % Starting post_as_ho1 with 300s (1) cores
% 7.55/1.24 % ho_unfolding_3 with pid 161030 completed with status 0
% 7.55/1.24 % Result found by ho_unfolding_3
% 7.55/1.24 % partial match(2): HSMSSMSSMLMNHSN
% 7.55/1.24 % Preprocessing class: HSMSSLSSMLMNHSA.
% 7.55/1.24 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 7.55/1.24 % Starting ho_unfolding_3 with 1500s (5) cores
% 7.55/1.24 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 7.55/1.24 % No SInE strategy applied
% 7.55/1.24 % Search class: HGHSF-FFMS31-SHSSMSBN
% 7.55/1.24 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 7.55/1.24 % Starting SubtermCWHack with 136s (1) cores
% 7.55/1.24 % Starting ho_unfolding_3 with 151s (1) cores
% 7.55/1.24 % Starting ho_unfolding_4 with 136s (1) cores
% 7.55/1.24 % Starting ehoh_best with 136s (1) cores
% 7.55/1.24 % Starting sh6 with 136s (1) cores
% 7.55/1.24 % ho_unfolding_4 with pid 161037 completed with status 0
% 7.55/1.24 % Result found by ho_unfolding_4
% 7.55/1.24 % partial match(2): HSMSSMSSMLMNHSN
% 7.55/1.24 % Preprocessing class: HSMSSLSSMLMNHSA.
% 7.55/1.24 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 7.55/1.24 % Starting ho_unfolding_3 with 1500s (5) cores
% 7.55/1.24 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 7.55/1.24 % No SInE strategy applied
% 7.55/1.24 % Search class: HGHSF-FFMS31-SHSSMSBN
% 7.55/1.24 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 7.55/1.24 % Starting SubtermCWHack with 136s (1) cores
% 7.55/1.24 % Starting ho_unfolding_3 with 151s (1) cores
% 7.55/1.24 % Starting ho_unfolding_4 with 136s (1) cores
% 7.55/1.24 % Preprocessing time : 0.002 s
% 7.55/1.24 % Presaturation interreduction done
% 7.55/1.24
% 7.55/1.24 % Proof found!
% 7.55/1.24 % SZS status Theorem
% 7.55/1.24 % SZS output start CNFRefutation
% 7.55/1.24 thf(decl_23, type, in: $i > $i > $o).
% 7.55/1.24 thf(decl_24, type, emptyset: $i).
% 7.55/1.24 thf(decl_25, type, powerset: $i > $i).
% 7.55/1.24 thf(decl_26, type, dsetconstr: $i > ($i > $o) > $i).
% 7.55/1.24 thf(decl_27, type, dsetconstrI: $o).
% 7.55/1.24 thf(decl_28, type, dsetconstrEL: $o).
% 7.55/1.24 thf(decl_29, type, dsetconstrER: $o).
% 7.55/1.24 thf(decl_30, type, nonempty: $i > $o).
% 7.55/1.24 thf(decl_31, type, nonemptyI: $o).
% 7.55/1.24 thf(decl_32, type, powersetI: $o).
% 7.55/1.24 thf(decl_33, type, kpair: $i > $i > $i).
% 7.55/1.24 thf(decl_34, type, singleton: $i > $o).
% 7.55/1.24 thf(decl_35, type, ex1: $i > ($i > $o) > $o).
% 7.55/1.24 thf(decl_36, type, ex1I: $o).
% 7.55/1.24 thf(decl_37, type, breln1Set: $i > $i).
% 7.55/1.24 thf(decl_38, type, transitive: $i > $i > $o).
% 7.55/1.24 thf(decl_39, type, antisymmetric: $i > $i > $o).
% 7.55/1.24 thf(decl_40, type, reflexive: $i > $i > $o).
% 7.55/1.24 thf(decl_41, type, refllinearorder: $i > $i > $o).
% 7.55/1.24 thf(decl_42, type, reflwellordering: $i > $i > $o).
% 7.55/1.24 thf(decl_43, type, epred1_2: $i > $i > $o).
% 7.55/1.24 thf(decl_44, type, esk1_2: $i > $i > $i).
% 7.55/1.24 thf(decl_45, type, esk2_3: $i > ($i > $o) > $i > $i).
% 7.55/1.24 thf(decl_46, type, esk3_0: $i).
% 7.55/1.24 thf(decl_47, type, esk4_0: $i).
% 7.55/1.24 thf(decl_48, type, epred2_0: $i > $i > $o).
% 7.55/1.24 thf(decl_49, type, esk5_1: $i > $i).
% 7.55/1.24 thf(decl_50, type, esk6_0: $i).
% 7.55/1.24 thf(decl_51, type, esk7_0: $i).
% 7.55/1.24 thf(decl_52, type, esk8_3: $i > $i > $i > $i).
% 7.55/1.24 thf(decl_53, type, epred3_0: $i > $o).
% 7.55/1.24 thf(decl_54, type, esk9_1: $i > $i).
% 7.55/1.24 thf(refllinearorder, axiom, ((refllinearorder)=(^[X1:$i, X6:$i]:((((((((reflexive @ X1 @ X6))&((transitive @ X1 @ X6))))&((antisymmetric @ X1 @ X6))))&(![X3:$i]:((((in @ X3 @ X1))=>(![X4:$i]:((((in @ X4 @ X1))=>((((in @ (kpair @ X3 @ X4) @ X6))|((in @ (kpair @ X4 @ X3) @ X6)))))))))))))), file('/export/starexec/sandbox/tmp/tmp.4GulGKTwbg/E---3.1_161017.p', refllinearorder)).
% 7.55/1.24 thf(antisymmetric, axiom, ((antisymmetric)=(^[X1:$i, X6:$i]:(![X3:$i]:((((in @ X3 @ X1))=>(![X4:$i]:((((in @ X4 @ X1))=>((((((in @ (kpair @ X3 @ X4) @ X6))&((in @ (kpair @ X4 @ X3) @ X6))))=>(((X3)=(X4))))))))))))), file('/export/starexec/sandbox/tmp/tmp.4GulGKTwbg/E---3.1_161017.p', antisymmetric)).
% 7.55/1.24 thf(nonemptyI, axiom, ((nonemptyI)<=>![X1:$i, X2:$i > $o, X3:$i]:(((in @ X3 @ X1)=>((X2 @ X3)=>(nonempty @ (dsetconstr @ X1 @ (^[X4:$i]:((X2 @ X4))))))))), file('/export/starexec/sandbox/tmp/tmp.4GulGKTwbg/E---3.1_161017.p', nonemptyI)).
% 7.55/1.24 thf(nonempty, axiom, ((nonempty)=(^[X3:$i]:(((X3)!=(emptyset))))), file('/export/starexec/sandbox/tmp/tmp.4GulGKTwbg/E---3.1_161017.p', nonempty)).
% 7.55/1.24 thf(ex1I, axiom, ((ex1I)<=>![X1:$i, X2:$i > $o, X3:$i]:(((in @ X3 @ X1)=>((X2 @ X3)=>(![X4:$i]:(((in @ X4 @ X1)=>((X2 @ X4)=>((X4)=(X3)))))=>(ex1 @ X1 @ (^[X4:$i]:((X2 @ X4))))))))), file('/export/starexec/sandbox/tmp/tmp.4GulGKTwbg/E---3.1_161017.p', ex1I)).
% 7.55/1.24 thf(ex1, axiom, ((ex1)=(^[X1:$i, X2:$i > $o]:((singleton @ (dsetconstr @ X1 @ (^[X3:$i]:((X2 @ X3)))))))), file('/export/starexec/sandbox/tmp/tmp.4GulGKTwbg/E---3.1_161017.p', ex1)).
% 7.55/1.24 thf(reflwellordering, axiom, ((reflwellordering)=(^[X1:$i, X6:$i]:((((refllinearorder @ X1 @ X6))&(![X7:$i]:((((in @ X7 @ (powerset @ X1)))=>((((nonempty @ X7))=>(?[X3:$i]:((((in @ X3 @ X7))&(![X4:$i]:((((in @ X4 @ X7))=>((in @ (kpair @ X3 @ X4) @ X6))))))))))))))))), file('/export/starexec/sandbox/tmp/tmp.4GulGKTwbg/E---3.1_161017.p', reflwellordering)).
% 7.55/1.24 thf(choice2fnsingleton, conjecture, ((dsetconstrI)=>((dsetconstrEL)=>((dsetconstrER)=>((nonemptyI)=>((powersetI)=>((ex1I)=>![X1:$i, X5:$i, X8:$i > $i > $o]:((![X3:$i]:(((in @ X3 @ X1)=>?[X4:$i]:(((in @ X4 @ X5)&(X8 @ X3 @ X4)))))=>![X6:$i]:(((in @ X6 @ (breln1Set @ X5))=>((reflwellordering @ X5 @ X6)=>![X3:$i]:(((in @ X3 @ X1)=>(singleton @ (dsetconstr @ X5 @ (^[X4:$i]:((((X8 @ X3 @ X4))&(![X9:$i]:((((in @ X9 @ X5))=>((((X8 @ X3 @ X9))=>((in @ (kpair @ X4 @ X9) @ X6))))))))))))))))))))))))), file('/export/starexec/sandbox/tmp/tmp.4GulGKTwbg/E---3.1_161017.p', choice2fnsingleton)).
% 7.55/1.24 thf(dsetconstrI, axiom, ((dsetconstrI)<=>![X1:$i, X2:$i > $o, X3:$i]:(((in @ X3 @ X1)=>((X2 @ X3)=>(in @ X3 @ (dsetconstr @ X1 @ (^[X4:$i]:((X2 @ X4))))))))), file('/export/starexec/sandbox/tmp/tmp.4GulGKTwbg/E---3.1_161017.p', dsetconstrI)).
% 7.55/1.24 thf(dsetconstrEL, axiom, ((dsetconstrEL)<=>![X1:$i, X2:$i > $o, X3:$i]:(((in @ X3 @ (dsetconstr @ X1 @ (^[X4:$i]:((X2 @ X4)))))=>(in @ X3 @ X1)))), file('/export/starexec/sandbox/tmp/tmp.4GulGKTwbg/E---3.1_161017.p', dsetconstrEL)).
% 7.55/1.24 thf(dsetconstrER, axiom, ((dsetconstrER)<=>![X1:$i, X2:$i > $o, X3:$i]:(((in @ X3 @ (dsetconstr @ X1 @ (^[X4:$i]:((X2 @ X4)))))=>(X2 @ X3)))), file('/export/starexec/sandbox/tmp/tmp.4GulGKTwbg/E---3.1_161017.p', dsetconstrER)).
% 7.55/1.24 thf(powersetI, axiom, ((powersetI)<=>![X1:$i, X5:$i]:((![X3:$i]:(((in @ X3 @ X5)=>(in @ X3 @ X1)))=>(in @ X5 @ (powerset @ X1))))), file('/export/starexec/sandbox/tmp/tmp.4GulGKTwbg/E---3.1_161017.p', powersetI)).
% 7.55/1.24 thf(c_0_12, plain, ((refllinearorder)=(^[Z0:$i, Z1:$i]:((((((((reflexive @ Z0 @ Z1))&((transitive @ Z0 @ Z1))))&((![X36:$i]:((((in @ X36 @ Z0))=>(![X37:$i]:((((in @ X37 @ Z0))=>((((((in @ (kpair @ X36 @ X37) @ Z1))&((in @ (kpair @ X37 @ X36) @ Z1))))=>(((X36)=(X37))))))))))))))&(![X3:$i]:((((in @ X3 @ Z0))=>(![X4:$i]:((((in @ X4 @ Z0))=>((((in @ (kpair @ X3 @ X4) @ Z1))|((in @ (kpair @ X4 @ X3) @ Z1)))))))))))))), inference(fof_simplification,[status(thm)],[refllinearorder])).
% 7.55/1.24 thf(c_0_13, plain, ((antisymmetric)=(^[Z0:$i, Z1:$i]:(![X3:$i]:((((in @ X3 @ Z0))=>(![X4:$i]:((((in @ X4 @ Z0))=>((((((in @ (kpair @ X3 @ X4) @ Z1))&((in @ (kpair @ X4 @ X3) @ Z1))))=>(((X3)=(X4))))))))))))), inference(fof_simplification,[status(thm)],[antisymmetric])).
% 7.55/1.24 thf(c_0_14, plain, ((nonemptyI)<=>![X1:$i, X2:$i > $o, X3:$i]:(((in @ X3 @ X1)=>((X2 @ X3)=>(nonempty @ (dsetconstr @ X1 @ (^[Z0:$i]:((X2 @ Z0))))))))), inference(fof_simplification,[status(thm)],[nonemptyI])).
% 7.55/1.24 thf(c_0_15, plain, ((nonempty)=(^[Z0:$i]:(((Z0)!=(emptyset))))), inference(fof_simplification,[status(thm)],[nonempty])).
% 7.55/1.24 thf(c_0_16, plain, ((ex1I)<=>![X1:$i, X2:$i > $o, X3:$i]:(((in @ X3 @ X1)=>((X2 @ X3)=>(![X4:$i]:(((in @ X4 @ X1)=>((X2 @ X4)=>((X4)=(X3)))))=>(ex1 @ X1 @ (^[Z0:$i]:((X2 @ Z0))))))))), inference(fof_simplification,[status(thm)],[ex1I])).
% 7.55/1.24 thf(c_0_17, plain, ((ex1)=(^[Z0:$i, Z1:$i > $o]:((singleton @ (dsetconstr @ Z0 @ (^[Z2:$i]:((Z1 @ Z2)))))))), inference(fof_simplification,[status(thm)],[ex1])).
% 7.55/1.24 thf(c_0_18, plain, ((reflwellordering)=(^[Z0:$i, Z1:$i]:(((((((((((reflexive @ Z0 @ Z1))&((transitive @ Z0 @ Z1))))&((![X38:$i]:((((in @ X38 @ Z0))=>(![X39:$i]:((((in @ X39 @ Z0))=>((((((in @ (kpair @ X38 @ X39) @ Z1))&((in @ (kpair @ X39 @ X38) @ Z1))))=>(((X38)=(X39))))))))))))))&(![X40:$i]:((((in @ X40 @ Z0))=>(![X41:$i]:((((in @ X41 @ Z0))=>((((in @ (kpair @ X40 @ X41) @ Z1))|((in @ (kpair @ X41 @ X40) @ Z1)))))))))))))&(![X7:$i]:((((in @ X7 @ (powerset @ Z0)))=>((((((X7)!=(emptyset))))=>(?[X3:$i]:((((in @ X3 @ X7))&(![X4:$i]:((((in @ X4 @ X7))=>((in @ (kpair @ X3 @ X4) @ Z1))))))))))))))))), inference(fof_simplification,[status(thm)],[reflwellordering])).
% 7.55/1.24 thf(c_0_19, plain, ((refllinearorder)=(^[Z0:$i, Z1:$i]:((((((((reflexive @ Z0 @ Z1))&((transitive @ Z0 @ Z1))))&((![X36:$i]:((((in @ X36 @ Z0))=>(![X37:$i]:((((in @ X37 @ Z0))=>((((((in @ (kpair @ X36 @ X37) @ Z1))&((in @ (kpair @ X37 @ X36) @ Z1))))=>(((X36)=(X37))))))))))))))&(![X3:$i]:((((in @ X3 @ Z0))=>(![X4:$i]:((((in @ X4 @ Z0))=>((((in @ (kpair @ X3 @ X4) @ Z1))|((in @ (kpair @ X4 @ X3) @ Z1)))))))))))))), inference(apply_def,[status(thm)],[c_0_12, c_0_13])).
% 7.55/1.24 thf(c_0_20, negated_conjecture, ~(((dsetconstrI)=>((dsetconstrEL)=>((dsetconstrER)=>((nonemptyI)=>((powersetI)=>((ex1I)=>![X1:$i, X5:$i, X8:$i > $i > $o]:((![X3:$i]:(((in @ X3 @ X1)=>?[X4:$i]:(((in @ X4 @ X5)&(X8 @ X3 @ X4)))))=>![X6:$i]:(((in @ X6 @ (breln1Set @ X5))=>((reflwellordering @ X5 @ X6)=>![X3:$i]:(((in @ X3 @ X1)=>(singleton @ (dsetconstr @ X5 @ (^[X4:$i]:((((X8 @ X3 @ X4))&(![X9:$i]:((((in @ X9 @ X5))=>((((X8 @ X3 @ X9))=>((in @ (kpair @ X4 @ X9) @ X6)))))))))))))))))))))))))), inference(assume_negation,[status(cth)],[choice2fnsingleton])).
% 7.55/1.24 thf(c_0_21, plain, ((dsetconstrI)<=>![X1:$i, X2:$i > $o, X3:$i]:(((in @ X3 @ X1)=>((X2 @ X3)=>(in @ X3 @ (dsetconstr @ X1 @ (^[Z0:$i]:((X2 @ Z0))))))))), inference(fof_simplification,[status(thm)],[dsetconstrI])).
% 7.55/1.24 thf(c_0_22, plain, ((dsetconstrEL)<=>![X1:$i, X2:$i > $o, X3:$i]:(((in @ X3 @ (dsetconstr @ X1 @ (^[Z0:$i]:((X2 @ Z0)))))=>(in @ X3 @ X1)))), inference(fof_simplification,[status(thm)],[dsetconstrEL])).
% 7.55/1.24 thf(c_0_23, plain, ((dsetconstrER)<=>![X1:$i, X2:$i > $o, X3:$i]:(((in @ X3 @ (dsetconstr @ X1 @ (^[Z0:$i]:((X2 @ Z0)))))=>(X2 @ X3)))), inference(fof_simplification,[status(thm)],[dsetconstrER])).
% 7.55/1.24 thf(c_0_24, plain, ((nonemptyI)=(![X1:$i, X2:$i > $o, X3:$i]:((((in @ X3 @ X1))=>((((X2 @ X3))=>((((dsetconstr @ X1 @ (^[Z0:$i]:((X2 @ Z0))))!=(emptyset)))))))))), inference(apply_def,[status(thm)],[c_0_14, c_0_15])).
% 7.55/1.24 thf(c_0_25, plain, ((ex1I)=(![X1:$i, X2:$i > $o, X3:$i]:((((in @ X3 @ X1))=>((((X2 @ X3))=>(((![X4:$i]:((((in @ X4 @ X1))=>((((X2 @ X4))=>(((X4)=(X3))))))))=>(((singleton @ (dsetconstr @ X1 @ (^[Z0:$i]:(((X2 @ Z0)))))))))))))))), inference(apply_def,[status(thm)],[c_0_16, c_0_17])).
% 7.55/1.24 thf(c_0_26, plain, ((reflwellordering)=(^[Z0:$i, Z1:$i]:(((((((((((reflexive @ Z0 @ Z1))&((transitive @ Z0 @ Z1))))&((![X38:$i]:((((in @ X38 @ Z0))=>(![X39:$i]:((((in @ X39 @ Z0))=>((((((in @ (kpair @ X38 @ X39) @ Z1))&((in @ (kpair @ X39 @ X38) @ Z1))))=>(((X38)=(X39))))))))))))))&(![X40:$i]:((((in @ X40 @ Z0))=>(![X41:$i]:((((in @ X41 @ Z0))=>((((in @ (kpair @ X40 @ X41) @ Z1))|((in @ (kpair @ X41 @ X40) @ Z1)))))))))))))&(![X7:$i]:((((in @ X7 @ (powerset @ Z0)))=>((((((X7)!=(emptyset))))=>(?[X3:$i]:((((in @ X3 @ X7))&(![X4:$i]:((((in @ X4 @ X7))=>((in @ (kpair @ X3 @ X4) @ Z1))))))))))))))))), inference(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[c_0_18, c_0_15]), c_0_19])).
% 7.55/1.24 thf(c_0_27, plain, ![X5:$i, X6:$i]:(((epred1_2 @ X6 @ X5)<=>(((((reflexive @ X5 @ X6)&(transitive @ X5 @ X6))&![X61:$i]:(((in @ X61 @ X5)=>![X62:$i]:(((in @ X62 @ X5)=>(((in @ (kpair @ X61 @ X62) @ X6)&(in @ (kpair @ X62 @ X61) @ X6))=>((X61)=(X62))))))))&![X63:$i]:(((in @ X63 @ X5)=>![X64:$i]:(((in @ X64 @ X5)=>((in @ (kpair @ X63 @ X64) @ X6)|(in @ (kpair @ X64 @ X63) @ X6)))))))&![X65:$i]:(((in @ X65 @ (powerset @ X5))=>(((X65)!=(emptyset))=>?[X66:$i]:(((in @ X66 @ X65)&![X67:$i]:(((in @ X67 @ X65)=>(in @ (kpair @ X66 @ X67) @ X6))))))))))), introduced(definition)).
% 7.55/1.24 thf(c_0_28, negated_conjecture, ~((![X42:$i, X43:$i > $o, X44:$i]:(((in @ X44 @ X42)=>((X43 @ X44)=>(in @ X44 @ (dsetconstr @ X42 @ X43)))))=>(![X45:$i, X46:$i > $o, X47:$i]:(((in @ X47 @ (dsetconstr @ X45 @ X46))=>(in @ X47 @ X45)))=>(![X48:$i, X49:$i > $o, X50:$i]:(((in @ X50 @ (dsetconstr @ X48 @ X49))=>(X49 @ X50)))=>(![X51:$i, X52:$i > $o, X53:$i]:(((in @ X53 @ X51)=>((X52 @ X53)=>((dsetconstr @ X51 @ X52)!=(emptyset)))))=>(![X54:$i, X55:$i]:((![X56:$i]:(((in @ X56 @ X55)=>(in @ X56 @ X54)))=>(in @ X55 @ (powerset @ X54))))=>(![X57:$i, X58:$i > $o, X59:$i]:(((in @ X59 @ X57)=>((X58 @ X59)=>(![X60:$i]:(((in @ X60 @ X57)=>((X58 @ X60)=>((X60)=(X59)))))=>(singleton @ (dsetconstr @ X57 @ X58))))))=>![X1:$i, X5:$i, X8:$i > $i > $o]:((![X3:$i]:(((in @ X3 @ X1)=>?[X4:$i]:(((in @ X4 @ X5)&(X8 @ X3 @ X4)))))=>![X6:$i]:(((in @ X6 @ (breln1Set @ X5))=>((epred1_2 @ X6 @ X5)=>![X3:$i]:(((in @ X3 @ X1)=>(singleton @ (dsetconstr @ X5 @ (^[Z0:$i]:(((X8 @ X3 @ Z0)&(![X9:$i]:((((in @ X9 @ X5))=>(((X8 @ X3 @ X9)=>((in @ (kpair @ Z0 @ X9) @ X6)))))))))))))))))))))))))), inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[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(apply_def,[status(thm)],[inference(apply_def,[status(thm)],[inference(fof_simplification,[status(thm)],[c_0_20]), c_0_21]), c_0_22]), c_0_23]), c_0_24]), powersetI]), c_0_25]), c_0_26])])]), c_0_27])).
% 7.55/1.24 thf(c_0_29, negated_conjecture, ![X68:$i, X69:$i > $o, X70:$i, X71:$i, X72:$i > $o, X73:$i, X74:$i, X75:$i > $o, X76:$i, X77:$i, X78:$i > $o, X79:$i, X80:$i, X81:$i, X83:$i, X84:$i > $o, X85:$i, X90:$i]:(((~(in @ X70 @ X68)|(~(X69 @ X70)|(in @ X70 @ (dsetconstr @ X68 @ X69))))&((~(in @ X73 @ (dsetconstr @ X71 @ X72))|(in @ X73 @ X71))&((~(in @ X76 @ (dsetconstr @ X74 @ X75))|(X75 @ X76))&((~(in @ X79 @ X77)|(~(X78 @ X79)|((dsetconstr @ X77 @ X78)!=(emptyset))))&((((in @ (esk1_2 @ X80 @ X81) @ X81)|(in @ X81 @ (powerset @ X80)))&(~(in @ (esk1_2 @ X80 @ X81) @ X80)|(in @ X81 @ (powerset @ X80))))&((((in @ (esk2_3 @ X83 @ X84 @ X85) @ X83)|(singleton @ (dsetconstr @ X83 @ X84))|~(X84 @ X85)|~(in @ X85 @ X83))&(((X84 @ (esk2_3 @ X83 @ X84 @ X85))|(singleton @ (dsetconstr @ X83 @ X84))|~(X84 @ X85)|~(in @ X85 @ X83))&(((esk2_3 @ X83 @ X84 @ X85)!=(X85))|(singleton @ (dsetconstr @ X83 @ X84))|~(X84 @ X85)|~(in @ X85 @ X83))))&((((in @ (esk5_1 @ X90) @ esk4_0)|~(in @ X90 @ esk3_0))&((epred2_0 @ X90 @ (esk5_1 @ X90))|~(in @ X90 @ esk3_0)))&((in @ esk6_0 @ (breln1Set @ esk4_0))&((epred1_2 @ esk6_0 @ esk4_0)&((in @ esk7_0 @ esk3_0)&~(singleton @ (dsetconstr @ esk4_0 @ (^[Z0:$i]:(((epred2_0 @ esk7_0 @ Z0)&(![X9:$i]:((((in @ X9 @ esk4_0))=>(((epred2_0 @ esk7_0 @ X9)=>((in @ (kpair @ Z0 @ X9) @ 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_28])])])])])])).
% 7.55/1.24 thf(c_0_30, plain, ![X5:$i, X6:$i]:(((epred1_2 @ X6 @ X5)=>(((((reflexive @ X5 @ X6)&(transitive @ X5 @ X6))&![X61:$i]:(((in @ X61 @ X5)=>![X62:$i]:(((in @ X62 @ X5)=>(((in @ (kpair @ X61 @ X62) @ X6)&(in @ (kpair @ X62 @ X61) @ X6))=>((X61)=(X62))))))))&![X63:$i]:(((in @ X63 @ X5)=>![X64:$i]:(((in @ X64 @ X5)=>((in @ (kpair @ X63 @ X64) @ X6)|(in @ (kpair @ X64 @ X63) @ X6)))))))&![X65:$i]:(((in @ X65 @ (powerset @ X5))=>(((X65)!=(emptyset))=>?[X66:$i]:(((in @ X66 @ X65)&![X67:$i]:(((in @ X67 @ X65)=>(in @ (kpair @ X66 @ X67) @ X6))))))))))), inference(split_equiv,[status(thm)],[c_0_27])).
% 7.55/1.24 thf(c_0_31, negated_conjecture, ![X1:$i, X3:$i, X2:$i > $o]:(((in @ X1 @ X3)|~((in @ X1 @ (dsetconstr @ X3 @ X2))))), inference(split_conjunct,[status(thm)],[c_0_29])).
% 7.55/1.24 thf(c_0_32, negated_conjecture, ![X3:$i, X1:$i]:(((in @ (esk1_2 @ X1 @ X3) @ X3)|(in @ X3 @ (powerset @ X1)))), inference(split_conjunct,[status(thm)],[c_0_29])).
% 7.55/1.24 thf(c_0_33, plain, ![X94:$i, X95:$i, X96:$i, X97:$i, X98:$i, X99:$i, X100:$i, X102:$i]:(((((((reflexive @ X94 @ X95)|~(epred1_2 @ X95 @ X94))&((transitive @ X94 @ X95)|~(epred1_2 @ X95 @ X94)))&(~(in @ X96 @ X94)|(~(in @ X97 @ X94)|(~(in @ (kpair @ X96 @ X97) @ X95)|~(in @ (kpair @ X97 @ X96) @ X95)|((X96)=(X97))))|~(epred1_2 @ X95 @ X94)))&(~(in @ X98 @ X94)|(~(in @ X99 @ X94)|((in @ (kpair @ X98 @ X99) @ X95)|(in @ (kpair @ X99 @ X98) @ X95)))|~(epred1_2 @ X95 @ X94)))&(((in @ (esk8_3 @ X94 @ X95 @ X100) @ X100)|((X100)=(emptyset))|~(in @ X100 @ (powerset @ X94))|~(epred1_2 @ X95 @ X94))&(~(in @ X102 @ X100)|(in @ (kpair @ (esk8_3 @ X94 @ X95 @ X100) @ X102) @ X95)|((X100)=(emptyset))|~(in @ X100 @ (powerset @ X94))|~(epred1_2 @ X95 @ X94))))), 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_30])])])])])])).
% 7.55/1.24 thf(c_0_34, negated_conjecture, ![X3:$i, X1:$i]:(((in @ X3 @ (powerset @ X1))|~((in @ (esk1_2 @ X1 @ X3) @ X1)))), inference(split_conjunct,[status(thm)],[c_0_29])).
% 7.55/1.24 thf(c_0_35, negated_conjecture, ![X3:$i, X2:$i > $o, X1:$i]:(((in @ (esk1_2 @ X1 @ (dsetconstr @ X3 @ X2)) @ X3)|(in @ (dsetconstr @ X3 @ X2) @ (powerset @ X1)))), inference(spm,[status(thm)],[c_0_31, c_0_32])).
% 7.55/1.24 thf(c_0_36, plain, ![X105:$i, X106:$i]:(((((epred2_0 @ esk7_0 @ X105)|~(epred3_0 @ X105))&(~(in @ X106 @ esk4_0)|(~(epred2_0 @ esk7_0 @ X106)|(in @ (kpair @ X105 @ X106) @ esk6_0))|~(epred3_0 @ X105)))&(((in @ (esk9_1 @ X105) @ esk4_0)|~(epred2_0 @ esk7_0 @ X105)|(epred3_0 @ X105))&(((epred2_0 @ esk7_0 @ (esk9_1 @ X105))|~(epred2_0 @ esk7_0 @ X105)|(epred3_0 @ X105))&(~(in @ (kpair @ X105 @ (esk9_1 @ X105)) @ esk6_0)|~(epred2_0 @ esk7_0 @ X105)|(epred3_0 @ X105)))))), 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)],[])])])])])])).
% 7.55/1.24 thf(c_0_37, plain, ![X1:$i, X3:$i, X5:$i, X4:$i]:(((in @ (kpair @ (esk8_3 @ X4 @ X5 @ X3) @ X1) @ X5)|((X3)=(emptyset))|~((in @ X1 @ X3))|~((in @ X3 @ (powerset @ X4)))|~((epred1_2 @ X5 @ X4)))), inference(split_conjunct,[status(thm)],[c_0_33])).
% 7.55/1.24 thf(c_0_38, negated_conjecture, ![X2:$i > $o, X1:$i]:((in @ (dsetconstr @ X1 @ X2) @ (powerset @ X1))), inference(spm,[status(thm)],[c_0_34, c_0_35])).
% 7.55/1.24 thf(c_0_39, plain, ![X4:$i, X3:$i, X1:$i]:(((in @ (esk8_3 @ X1 @ X3 @ X4) @ X4)|((X4)=(emptyset))|~((in @ X4 @ (powerset @ X1)))|~((epred1_2 @ X3 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_33])).
% 7.55/1.24 thf(c_0_40, plain, ![X1:$i, X4:$i, X5:$i, X3:$i]:((((X1)=(X4))|~((in @ X1 @ X3))|~((in @ X4 @ X3))|~((in @ (kpair @ X1 @ X4) @ X5))|~((in @ (kpair @ X4 @ X1) @ X5))|~((epred1_2 @ X5 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_33])).
% 7.55/1.24 thf(c_0_41, plain, ![X1:$i, X3:$i]:(((in @ (kpair @ X3 @ X1) @ esk6_0)|~((in @ X1 @ esk4_0))|~((epred2_0 @ esk7_0 @ X1))|~((epred3_0 @ X3)))), inference(split_conjunct,[status(thm)],[c_0_36])).
% 7.55/1.24 thf(c_0_42, plain, ![X4:$i, X3:$i, X2:$i > $o, X1:$i]:((((dsetconstr @ X1 @ X2)=(emptyset))|(in @ (kpair @ (esk8_3 @ X1 @ X3 @ (dsetconstr @ X1 @ X2)) @ X4) @ X3)|~((in @ X4 @ (dsetconstr @ X1 @ X2)))|~((epred1_2 @ X3 @ X1)))), inference(spm,[status(thm)],[c_0_37, c_0_38])).
% 7.55/1.24 thf(c_0_43, negated_conjecture, ![X3:$i, X2:$i > $o, X1:$i]:(((in @ X1 @ (dsetconstr @ X3 @ X2))|~((in @ X1 @ X3))|~((X2 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_29])).
% 7.55/1.24 thf(c_0_44, negated_conjecture, ![X1:$i, X3:$i, X2:$i > $o]:((~((in @ X1 @ X3))|~((X2 @ X1))|((dsetconstr @ X3 @ X2)!=(emptyset)))), inference(split_conjunct,[status(thm)],[c_0_29])).
% 7.55/1.24 thf(c_0_45, plain, ![X3:$i, X2:$i > $o, X1:$i]:((((dsetconstr @ X1 @ X2)=(emptyset))|(in @ (esk8_3 @ X1 @ X3 @ (dsetconstr @ X1 @ X2)) @ (dsetconstr @ X1 @ X2))|~((epred1_2 @ X3 @ X1)))), inference(spm,[status(thm)],[c_0_39, c_0_38])).
% 7.55/1.24 thf(c_0_46, negated_conjecture, (epred1_2 @ esk6_0 @ esk4_0), inference(split_conjunct,[status(thm)],[c_0_29])).
% 7.55/1.24 thf(c_0_47, plain, ![X1:$i, X4:$i, X3:$i]:((((X1)=(X3))|~((in @ (kpair @ X1 @ X3) @ esk6_0))|~((epred1_2 @ esk6_0 @ X4))|~((in @ X1 @ esk4_0))|~((epred2_0 @ esk7_0 @ X1))|~((in @ X3 @ X4))|~((in @ X1 @ X4))|~((epred3_0 @ X3)))), inference(spm,[status(thm)],[c_0_40, c_0_41])).
% 7.55/1.24 thf(c_0_48, negated_conjecture, ![X1:$i, X3:$i, X2:$i > $o, X4:$i]:(((in @ (kpair @ (esk8_3 @ X1 @ X3 @ (dsetconstr @ X1 @ X2)) @ X4) @ X3)|~((epred1_2 @ X3 @ X1))|~((in @ X4 @ X1))|~((X2 @ X4)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_42, c_0_43]), c_0_44])).
% 7.55/1.24 thf(c_0_49, negated_conjecture, ![X2:$i > $o]:((((dsetconstr @ esk4_0 @ X2)=(emptyset))|(in @ (esk8_3 @ esk4_0 @ esk6_0 @ (dsetconstr @ esk4_0 @ X2)) @ (dsetconstr @ esk4_0 @ X2)))), inference(spm,[status(thm)],[c_0_45, c_0_46])).
% 7.55/1.24 thf(c_0_50, plain, ![X1:$i, X2:$i > $o, X4:$i, X3:$i]:((((esk8_3 @ X1 @ esk6_0 @ (dsetconstr @ X1 @ X2))=(X3))|~((in @ (esk8_3 @ X1 @ esk6_0 @ (dsetconstr @ X1 @ X2)) @ esk4_0))|~((epred2_0 @ esk7_0 @ (esk8_3 @ X1 @ esk6_0 @ (dsetconstr @ X1 @ X2))))|~((in @ (esk8_3 @ X1 @ esk6_0 @ (dsetconstr @ X1 @ X2)) @ X4))|~((epred1_2 @ esk6_0 @ X4))|~((epred1_2 @ esk6_0 @ X1))|~((in @ X3 @ X4))|~((in @ X3 @ X1))|~((epred3_0 @ X3))|~((X2 @ X3)))), inference(spm,[status(thm)],[c_0_47, c_0_48])).
% 7.55/1.24 thf(c_0_51, negated_conjecture, ![X2:$i > $o]:((((dsetconstr @ esk4_0 @ X2)=(emptyset))|(in @ (esk8_3 @ esk4_0 @ esk6_0 @ (dsetconstr @ esk4_0 @ X2)) @ esk4_0))), inference(spm,[status(thm)],[c_0_31, c_0_49])).
% 7.55/1.24 thf(c_0_52, negated_conjecture, ![X3:$i, X2:$i > $o, X1:$i]:((((esk8_3 @ esk4_0 @ esk6_0 @ (dsetconstr @ esk4_0 @ X2))=(X1))|~((epred2_0 @ esk7_0 @ (esk8_3 @ esk4_0 @ esk6_0 @ (dsetconstr @ esk4_0 @ X2))))|~((in @ (esk8_3 @ esk4_0 @ esk6_0 @ (dsetconstr @ esk4_0 @ X2)) @ X3))|~((epred1_2 @ esk6_0 @ X3))|~((in @ X1 @ esk4_0))|~((in @ X1 @ X3))|~((epred3_0 @ X1))|~((X2 @ X1)))), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_50, c_0_51]), c_0_46])]), c_0_44])).
% 7.55/1.24 thf(c_0_53, plain, ![X1:$i]:(((epred2_0 @ esk7_0 @ X1)|~((epred3_0 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_36])).
% 7.55/1.24 thf(c_0_54, plain, ![X3:$i, X2:$i > $o, X1:$i]:((((esk8_3 @ esk4_0 @ esk6_0 @ (dsetconstr @ esk4_0 @ X2))=(X1))|~((in @ (esk8_3 @ esk4_0 @ esk6_0 @ (dsetconstr @ esk4_0 @ X2)) @ X3))|~((epred3_0 @ (esk8_3 @ esk4_0 @ esk6_0 @ (dsetconstr @ esk4_0 @ X2))))|~((epred1_2 @ esk6_0 @ X3))|~((in @ X1 @ esk4_0))|~((in @ X1 @ X3))|~((epred3_0 @ X1))|~((X2 @ X1)))), inference(spm,[status(thm)],[c_0_52, c_0_53])).
% 7.55/1.24 thf(c_0_55, negated_conjecture, ![X1:$i, X3:$i, X2:$i > $o]:(((X2 @ X1)|~((in @ X1 @ (dsetconstr @ X3 @ X2))))), inference(split_conjunct,[status(thm)],[c_0_29])).
% 7.55/1.24 thf(c_0_56, negated_conjecture, ![X2:$i > $o, X1:$i]:((((esk8_3 @ esk4_0 @ esk6_0 @ (dsetconstr @ esk4_0 @ X2))=(X1))|~((epred3_0 @ (esk8_3 @ esk4_0 @ esk6_0 @ (dsetconstr @ esk4_0 @ X2))))|~((in @ X1 @ esk4_0))|~((epred3_0 @ X1))|~((X2 @ X1)))), inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_54, c_0_51]), c_0_46])]), c_0_44])).
% 7.55/1.24 thf(c_0_57, negated_conjecture, ![X2:$i > $o]:((((dsetconstr @ esk4_0 @ X2)=(emptyset))|(X2 @ (esk8_3 @ esk4_0 @ esk6_0 @ (dsetconstr @ esk4_0 @ X2))))), inference(spm,[status(thm)],[c_0_55, c_0_49])).
% 7.55/1.24 thf(c_0_58, plain, ![X1:$i]:(((epred3_0 @ X1)|~((in @ (kpair @ X1 @ (esk9_1 @ X1)) @ esk6_0))|~((epred2_0 @ esk7_0 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_36])).
% 7.55/1.24 thf(c_0_59, plain, ![X1:$i]:(((in @ (esk9_1 @ X1) @ esk4_0)|(epred3_0 @ X1)|~((epred2_0 @ esk7_0 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_36])).
% 7.55/1.24 thf(c_0_60, plain, ![X1:$i]:(((epred2_0 @ esk7_0 @ (esk9_1 @ X1))|(epred3_0 @ X1)|~((epred2_0 @ esk7_0 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_36])).
% 7.55/1.24 thf(c_0_61, negated_conjecture, ![X1:$i]:((((esk8_3 @ esk4_0 @ esk6_0 @ (dsetconstr @ esk4_0 @ epred3_0))=(X1))|~((in @ X1 @ esk4_0))|~((epred3_0 @ X1)))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_56, c_0_57]), c_0_44])).
% 7.55/1.24 thf(c_0_62, plain, ![X2:$i > $o, X1:$i]:(((epred3_0 @ (esk8_3 @ X1 @ esk6_0 @ (dsetconstr @ X1 @ X2)))|~((in @ (esk9_1 @ (esk8_3 @ X1 @ esk6_0 @ (dsetconstr @ X1 @ X2))) @ X1))|~((epred2_0 @ esk7_0 @ (esk8_3 @ X1 @ esk6_0 @ (dsetconstr @ X1 @ X2))))|~((X2 @ (esk9_1 @ (esk8_3 @ X1 @ esk6_0 @ (dsetconstr @ X1 @ X2)))))|~((epred1_2 @ esk6_0 @ X1)))), inference(spm,[status(thm)],[c_0_58, c_0_48])).
% 7.55/1.24 thf(c_0_63, plain, (((dsetconstr @ esk4_0 @ (epred2_0 @ esk7_0))=(emptyset))|(in @ (esk9_1 @ (esk8_3 @ esk4_0 @ esk6_0 @ (dsetconstr @ esk4_0 @ (epred2_0 @ esk7_0)))) @ esk4_0)|(epred3_0 @ (esk8_3 @ esk4_0 @ esk6_0 @ (dsetconstr @ esk4_0 @ (epred2_0 @ esk7_0))))), inference(spm,[status(thm)],[c_0_59, c_0_57])).
% 7.55/1.24 thf(c_0_64, plain, (((dsetconstr @ esk4_0 @ (epred2_0 @ esk7_0))=(emptyset))|(epred2_0 @ esk7_0 @ (esk9_1 @ (esk8_3 @ esk4_0 @ esk6_0 @ (dsetconstr @ esk4_0 @ (epred2_0 @ esk7_0)))))|(epred3_0 @ (esk8_3 @ esk4_0 @ esk6_0 @ (dsetconstr @ esk4_0 @ (epred2_0 @ esk7_0))))), inference(spm,[status(thm)],[c_0_60, c_0_57])).
% 7.55/1.24 thf(c_0_65, negated_conjecture, ![X2:$i > $o]:((((esk8_3 @ esk4_0 @ esk6_0 @ (dsetconstr @ esk4_0 @ epred3_0))=(esk8_3 @ esk4_0 @ esk6_0 @ (dsetconstr @ esk4_0 @ X2)))|((dsetconstr @ esk4_0 @ X2)=(emptyset))|~((epred3_0 @ (esk8_3 @ esk4_0 @ esk6_0 @ (dsetconstr @ esk4_0 @ X2)))))), inference(spm,[status(thm)],[c_0_61, c_0_51])).
% 7.55/1.24 thf(c_0_66, plain, (((dsetconstr @ esk4_0 @ (epred2_0 @ esk7_0))=(emptyset))|(epred3_0 @ (esk8_3 @ esk4_0 @ esk6_0 @ (dsetconstr @ esk4_0 @ (epred2_0 @ esk7_0))))), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_62, c_0_63]), c_0_46])]), c_0_57]), c_0_64])).
% 7.55/1.24 thf(c_0_67, negated_conjecture, (((esk8_3 @ esk4_0 @ esk6_0 @ (dsetconstr @ esk4_0 @ (epred2_0 @ esk7_0)))=(esk8_3 @ esk4_0 @ esk6_0 @ (dsetconstr @ esk4_0 @ epred3_0)))|((dsetconstr @ esk4_0 @ (epred2_0 @ esk7_0))=(emptyset))), inference(spm,[status(thm)],[c_0_65, c_0_66])).
% 7.55/1.24 thf(c_0_68, plain, ![X104:$i]:(((epred3_0 @ X104)<=>((epred2_0 @ esk7_0 @ X104)&![X103:$i]:(((in @ X103 @ esk4_0)=>((epred2_0 @ esk7_0 @ X103)=>(in @ (kpair @ X104 @ X103) @ esk6_0))))))), introduced(definition)).
% 7.55/1.24 thf(c_0_69, negated_conjecture, ![X3:$i, X2:$i > $o, X1:$i]:(((in @ (esk2_3 @ X1 @ X2 @ X3) @ X1)|(singleton @ (dsetconstr @ X1 @ X2))|~((X2 @ X3))|~((in @ X3 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_29])).
% 7.55/1.24 thf(c_0_70, negated_conjecture, (((dsetconstr @ esk4_0 @ (epred2_0 @ esk7_0))=(emptyset))|(in @ (esk8_3 @ esk4_0 @ esk6_0 @ (dsetconstr @ esk4_0 @ epred3_0)) @ esk4_0)), inference(spm,[status(thm)],[c_0_51, c_0_67])).
% 7.55/1.24 thf(c_0_71, negated_conjecture, ~((((singleton @ (dsetconstr @ esk4_0 @ epred3_0)))=(($true)))), inference(lift_lambdas,[status(thm)],[inference(split_conjunct,[status(thm)],[c_0_29]), c_0_68])).
% 7.55/1.24 thf(c_0_72, negated_conjecture, ![X3:$i, X2:$i > $o, X1:$i]:(((X2 @ (esk2_3 @ X1 @ X2 @ X3))|(singleton @ (dsetconstr @ X1 @ X2))|~((X2 @ X3))|~((in @ X3 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_29])).
% 7.55/1.24 thf(c_0_73, negated_conjecture, ![X2:$i > $o]:((((dsetconstr @ esk4_0 @ (epred2_0 @ esk7_0))=(emptyset))|(in @ (esk2_3 @ esk4_0 @ X2 @ (esk8_3 @ esk4_0 @ esk6_0 @ (dsetconstr @ esk4_0 @ epred3_0))) @ esk4_0)|(singleton @ (dsetconstr @ esk4_0 @ X2))|~((X2 @ (esk8_3 @ esk4_0 @ esk6_0 @ (dsetconstr @ esk4_0 @ epred3_0)))))), inference(spm,[status(thm)],[c_0_69, c_0_70])).
% 7.55/1.24 thf(c_0_74, plain, (((dsetconstr @ esk4_0 @ (epred2_0 @ esk7_0))=(emptyset))|(epred3_0 @ (esk8_3 @ esk4_0 @ esk6_0 @ (dsetconstr @ esk4_0 @ epred3_0)))), inference(spm,[status(thm)],[c_0_66, c_0_67])).
% 7.55/1.24 thf(c_0_75, negated_conjecture, ~((singleton @ (dsetconstr @ esk4_0 @ epred3_0))), inference(cn,[status(thm)],[c_0_71])).
% 7.55/1.24 thf(c_0_76, negated_conjecture, ![X2:$i > $o]:((((dsetconstr @ esk4_0 @ (epred2_0 @ esk7_0))=(emptyset))|(X2 @ (esk2_3 @ esk4_0 @ X2 @ (esk8_3 @ esk4_0 @ esk6_0 @ (dsetconstr @ esk4_0 @ epred3_0))))|(singleton @ (dsetconstr @ esk4_0 @ X2))|~((X2 @ (esk8_3 @ esk4_0 @ esk6_0 @ (dsetconstr @ esk4_0 @ epred3_0)))))), inference(spm,[status(thm)],[c_0_72, c_0_70])).
% 7.55/1.24 thf(c_0_77, plain, (((dsetconstr @ esk4_0 @ (epred2_0 @ esk7_0))=(emptyset))|(in @ (esk2_3 @ esk4_0 @ epred3_0 @ (esk8_3 @ esk4_0 @ esk6_0 @ (dsetconstr @ esk4_0 @ epred3_0))) @ esk4_0)), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_73, c_0_74]), c_0_75])).
% 7.55/1.24 thf(c_0_78, plain, (((dsetconstr @ esk4_0 @ (epred2_0 @ esk7_0))=(emptyset))|(epred3_0 @ (esk2_3 @ esk4_0 @ epred3_0 @ (esk8_3 @ esk4_0 @ esk6_0 @ (dsetconstr @ esk4_0 @ epred3_0))))), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_76, c_0_74]), c_0_75])).
% 7.55/1.24 thf(c_0_79, negated_conjecture, ![X3:$i, X2:$i > $o, X1:$i]:(((singleton @ (dsetconstr @ X1 @ X2))|((esk2_3 @ X1 @ X2 @ X3)!=(X3))|~((X2 @ X3))|~((in @ X3 @ X1)))), inference(split_conjunct,[status(thm)],[c_0_29])).
% 7.55/1.24 thf(c_0_80, negated_conjecture, (((esk2_3 @ esk4_0 @ epred3_0 @ (esk8_3 @ esk4_0 @ esk6_0 @ (dsetconstr @ esk4_0 @ epred3_0)))=(esk8_3 @ esk4_0 @ esk6_0 @ (dsetconstr @ esk4_0 @ epred3_0)))|((dsetconstr @ esk4_0 @ (epred2_0 @ esk7_0))=(emptyset))), inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_61, c_0_77]), c_0_78])).
% 7.55/1.24 thf(c_0_81, negated_conjecture, ((dsetconstr @ esk4_0 @ (epred2_0 @ esk7_0))=(emptyset)), inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_79, c_0_80]), c_0_75]), c_0_74]), c_0_70])).
% 7.55/1.24 thf(c_0_82, negated_conjecture, ![X1:$i]:((~((in @ X1 @ esk4_0))|~((epred2_0 @ esk7_0 @ X1)))), inference(spm,[status(thm)],[c_0_44, c_0_81])).
% 7.55/1.24 thf(c_0_83, negated_conjecture, ![X1:$i]:(((epred2_0 @ X1 @ (esk5_1 @ X1))|~((in @ X1 @ esk3_0)))), inference(split_conjunct,[status(thm)],[c_0_29])).
% 7.55/1.24 thf(c_0_84, negated_conjecture, (in @ esk7_0 @ esk3_0), inference(split_conjunct,[status(thm)],[c_0_29])).
% 7.55/1.24 thf(c_0_85, negated_conjecture, ~((in @ (esk5_1 @ esk7_0) @ esk4_0)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_82, c_0_83]), c_0_84])])).
% 7.55/1.24 thf(c_0_86, negated_conjecture, ![X1:$i]:(((in @ (esk5_1 @ X1) @ esk4_0)|~((in @ X1 @ esk3_0)))), inference(split_conjunct,[status(thm)],[c_0_29])).
% 7.55/1.24 thf(c_0_87, negated_conjecture, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_85, c_0_86]), c_0_84])]), ['proof']).
% 7.55/1.24 % SZS output end CNFRefutation
% 7.55/1.24 % Parsed axioms : 32
% 7.55/1.24 % Removed by relevancy pruning/SinE : 0
% 7.55/1.24 % Initial clauses : 46
% 7.55/1.24 % Removed in clause preprocessing : 20
% 7.55/1.24 % Initial clauses in saturation : 26
% 7.55/1.24 % Processed clauses : 1407
% 7.55/1.24 % ...of these trivial : 0
% 7.55/1.24 % ...subsumed : 335
% 7.55/1.24 % ...remaining for further processing : 1072
% 7.55/1.24 % Other redundant clauses eliminated : 0
% 7.55/1.24 % Clauses deleted for lack of memory : 0
% 7.55/1.24 % Backward-subsumed : 65
% 7.55/1.24 % Backward-rewritten : 144
% 7.55/1.24 % Generated clauses : 14997
% 7.55/1.24 % ...of the previous two non-redundant : 14961
% 7.55/1.24 % ...aggressively subsumed : 0
% 7.55/1.24 % Contextual simplify-reflections : 27
% 7.55/1.24 % Paramodulations : 14987
% 7.55/1.24 % Factorizations : 10
% 7.55/1.24 % NegExts : 0
% 7.55/1.24 % Equation resolutions : 0
% 7.55/1.24 % Disequality decompositions : 0
% 7.55/1.24 % Total rewrite steps : 373
% 7.55/1.24 % ...of those cached : 346
% 7.55/1.24 % Propositional unsat checks : 0
% 7.55/1.24 % Propositional check models : 0
% 7.55/1.24 % Propositional check unsatisfiable : 0
% 7.55/1.24 % Propositional clauses : 0
% 7.55/1.24 % Propositional clauses after purity: 0
% 7.55/1.24 % Propositional unsat core size : 0
% 7.55/1.24 % Propositional preprocessing time : 0.000
% 7.55/1.24 % Propositional encoding time : 0.000
% 7.55/1.24 % Propositional solver time : 0.000
% 7.55/1.24 % Success case prop preproc time : 0.000
% 7.55/1.24 % Success case prop encoding time : 0.000
% 7.55/1.24 % Success case prop solver time : 0.000
% 7.55/1.24 % Current number of processed clauses : 837
% 7.55/1.24 % Positive orientable unit clauses : 20
% 7.55/1.24 % Positive unorientable unit clauses: 0
% 7.55/1.24 % Negative unit clauses : 2
% 7.55/1.24 % Non-unit-clauses : 815
% 7.55/1.24 % Current number of unprocessed clauses: 13594
% 7.55/1.24 % ...number of literals in the above : 64753
% 7.55/1.24 % Current number of archived formulas : 0
% 7.55/1.24 % Current number of archived clauses : 235
% 7.55/1.24 % Clause-clause subsumption calls (NU) : 87678
% 7.55/1.24 % Rec. Clause-clause subsumption calls : 35469
% 7.55/1.24 % Non-unit clause-clause subsumptions : 425
% 7.55/1.24 % Unit Clause-clause subsumption calls : 1173
% 7.55/1.24 % Rewrite failures with RHS unbound : 0
% 7.55/1.24 % BW rewrite match attempts : 87
% 7.55/1.24 % BW rewrite match successes : 3
% 7.55/1.24 % Condensation attempts : 0
% 7.55/1.24 % Condensation successes : 0
% 7.55/1.24 % Termbank termtop insertions : 696848
% 7.55/1.24 % Search garbage collected termcells : 1377
% 7.55/1.24
% 7.55/1.24 % -------------------------------------------------
% 7.55/1.24 % User time : 0.812 s
% 7.55/1.24 % System time : 0.033 s
% 7.55/1.24 % Total time : 0.846 s
% 7.55/1.24 % Maximum resident set size: 3872 pages
% 7.55/1.24
% 7.55/1.24 % -------------------------------------------------
% 7.55/1.24 % User time : 4.495 s
% 7.55/1.24 % System time : 0.133 s
% 7.55/1.24 % Total time : 4.628 s
% 7.55/1.24 % Maximum resident set size: 4864 pages
% 7.55/1.24 % E exiting
%------------------------------------------------------------------------------