%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SET676+3 : TPTP v9.2.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 05:08:18 PM UTC 2026
% Result : Theorem 0.29s 1.61s
% Output : CNFRefutation 0.38s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SET676+3 : TPTP v9.2.1. Released v2.2.0.
% 0.00/0.12 % Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.16/0.33 % Computer : n019.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % WCLimit : 300
% 0.16/0.33 % DateTime : Tue May 5 02:31:59 EDT 2026
% 0.16/0.33 % CPUTime :
% 0.16/0.34 % start to proof: theBenchmark
% 0.29/1.61 % Version : CSE_E---1.7
% 0.29/1.61 % Problem : theBenchmark.p
% 0.29/1.61 % SZS status Theorem for theBenchmark.p
% 0.29/1.61 % SZS output start CNFRefutation
% 0.29/1.61 fof(p13, axiom, ![X1]:(ilf_type(X1,set_type)=>![X2]:((~(empty(X2))&ilf_type(X2,set_type))=>(ilf_type(X1,member_type(X2))<=>member(X1,X2)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', p13)).
% 0.29/1.61 fof(p15, axiom, ![X1]:(ilf_type(X1,set_type)=>(empty(X1)<=>![X2]:(ilf_type(X2,set_type)=>~(member(X2,X1))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', p15)).
% 0.29/1.61 fof(prove_relset_1_41, conjecture, ![X1]:(ilf_type(X1,set_type)=>ilf_type(cross_product(X1,X1),identity_relation_of_type(X1))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', prove_relset_1_41)).
% 0.29/1.61 fof(p14, axiom, ![X1]:((~(empty(X1))&ilf_type(X1,set_type))=>?[X2]:ilf_type(X2,member_type(X1))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', p14)).
% 0.29/1.61 fof(p12, axiom, ![X1]:(ilf_type(X1,set_type)=>(~(empty(power_set(X1)))&ilf_type(power_set(X1),set_type))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', p12)).
% 0.29/1.61 fof(p2, axiom, ![X1]:(ilf_type(X1,set_type)=>![X2]:(ilf_type(X2,set_type)=>![X3]:(ilf_type(X3,set_type)=>(member(X3,cross_product(X1,X2))<=>?[X4]:(ilf_type(X4,set_type)&?[X5]:(((ilf_type(X5,set_type)&member(X4,X1))&member(X5,X2))&X3=ordered_pair(X4,X5))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', p2)).
% 0.29/1.61 fof(p7, axiom, ![X1]:(ilf_type(X1,set_type)=>![X2]:(ilf_type(X2,set_type)=>(![X3]:(ilf_type(X3,subset_type(cross_product(X1,X2)))=>ilf_type(X3,relation_type(X1,X2)))&![X4]:(ilf_type(X4,relation_type(X1,X2))=>ilf_type(X4,subset_type(cross_product(X1,X2))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', p7)).
% 0.29/1.61 fof(p18, axiom, ![X1]:(ilf_type(X1,set_type)=>![X2]:(ilf_type(X2,set_type)=>![X3]:(ilf_type(X3,subset_type(cross_product(X1,X2)))=>relation_like(X3)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', p18)).
% 0.29/1.61 fof(p16, axiom, ![X1]:(ilf_type(X1,set_type)=>(relation_like(X1)<=>![X2]:(ilf_type(X2,set_type)=>(member(X2,X1)=>?[X3]:(ilf_type(X3,set_type)&?[X4]:(ilf_type(X4,set_type)&X2=ordered_pair(X3,X4))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', p16)).
% 0.29/1.61 fof(p11, axiom, ![X1]:(ilf_type(X1,set_type)=>![X2]:(ilf_type(X2,set_type)=>(member(X1,power_set(X2))<=>![X3]:(ilf_type(X3,set_type)=>(member(X3,X1)=>member(X3,X2)))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', p11)).
% 0.29/1.61 fof(p4, axiom, ![X1]:(ilf_type(X1,set_type)=>![X2]:(ilf_type(X2,set_type)=>(ilf_type(X2,identity_relation_of_type(X1))<=>ilf_type(X2,relation_type(X1,X1))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', p4)).
% 0.29/1.61 fof(p9, axiom, ![X1]:(ilf_type(X1,set_type)=>![X2]:(ilf_type(X2,set_type)=>(ilf_type(X2,subset_type(X1))<=>ilf_type(X2,member_type(power_set(X1)))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', p9)).
% 0.29/1.61 fof(p8, axiom, ![X1]:(ilf_type(X1,set_type)=>![X2]:(ilf_type(X2,set_type)=>?[X3]:ilf_type(X3,relation_type(X2,X1)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', p8)).
% 0.29/1.61 fof(p1, axiom, ![X1]:(ilf_type(X1,set_type)=>![X2]:(ilf_type(X2,set_type)=>ilf_type(cross_product(X1,X2),relation_type(X1,X2)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', p1)).
% 0.29/1.61 fof(p6, axiom, ![X1]:(ilf_type(X1,set_type)=>![X2]:(ilf_type(X2,set_type)=>ilf_type(ordered_pair(X1,X2),set_type))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', p6)).
% 0.29/1.61 fof(p3, axiom, ![X1]:(ilf_type(X1,set_type)=>![X2]:(ilf_type(X2,set_type)=>ilf_type(cross_product(X1,X2),set_type))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', p3)).
% 0.29/1.61 fof(p10, axiom, ![X1]:(ilf_type(X1,set_type)=>?[X2]:ilf_type(X2,subset_type(X1))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', p10)).
% 0.29/1.61 fof(p5, axiom, ![X1]:(ilf_type(X1,set_type)=>?[X2]:ilf_type(X2,identity_relation_of_type(X1))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', p5)).
% 0.29/1.61 fof(p17, axiom, ![X1]:((empty(X1)&ilf_type(X1,set_type))=>relation_like(X1)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', p17)).
% 0.29/1.61 fof(p19, axiom, ![X1]:ilf_type(X1,set_type), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', p19)).
% 0.29/1.61 fof(i_0_20, plain, ![X1]:(ilf_type(X1,set_type)=>![X2]:((~empty(X2)&ilf_type(X2,set_type))=>(ilf_type(X1,member_type(X2))<=>member(X1,X2)))), inference(fof_simplification,[status(thm)],[p13])).
% 0.29/1.61 fof(i_0_21, plain, ![X1]:(ilf_type(X1,set_type)=>(empty(X1)<=>![X2]:(ilf_type(X2,set_type)=>~member(X2,X1)))), inference(fof_simplification,[status(thm)],[p15])).
% 0.29/1.61 fof(i_0_22, negated_conjecture, ~(![X1]:(ilf_type(X1,set_type)=>ilf_type(cross_product(X1,X1),identity_relation_of_type(X1)))), inference(assume_negation,[status(cth)],[prove_relset_1_41])).
% 0.29/1.61 fof(i_0_23, plain, ![X1]:((~empty(X1)&ilf_type(X1,set_type))=>?[X2]:ilf_type(X2,member_type(X1))), inference(fof_simplification,[status(thm)],[p14])).
% 0.29/1.61 fof(i_0_24, plain, ![X1]:(ilf_type(X1,set_type)=>(~empty(power_set(X1))&ilf_type(power_set(X1),set_type))), inference(fof_simplification,[status(thm)],[p12])).
% 0.29/1.61 fof(i_0_25, plain, ![X54, X55, X56, X59, X60]:(((ilf_type(esk1_3(X54,X55,X56),set_type)|~member(X56,cross_product(X54,X55))|~ilf_type(X56,set_type)|~ilf_type(X55,set_type)|~ilf_type(X54,set_type))&((((ilf_type(esk2_3(X54,X55,X56),set_type)|~member(X56,cross_product(X54,X55))|~ilf_type(X56,set_type)|~ilf_type(X55,set_type)|~ilf_type(X54,set_type))&(member(esk1_3(X54,X55,X56),X54)|~member(X56,cross_product(X54,X55))|~ilf_type(X56,set_type)|~ilf_type(X55,set_type)|~ilf_type(X54,set_type)))&(member(esk2_3(X54,X55,X56),X55)|~member(X56,cross_product(X54,X55))|~ilf_type(X56,set_type)|~ilf_type(X55,set_type)|~ilf_type(X54,set_type)))&(X56=ordered_pair(esk1_3(X54,X55,X56),esk2_3(X54,X55,X56))|~member(X56,cross_product(X54,X55))|~ilf_type(X56,set_type)|~ilf_type(X55,set_type)|~ilf_type(X54,set_type))))&(~ilf_type(X59,set_type)|(~ilf_type(X60,set_type)|~member(X59,X54)|~member(X60,X55)|X56!=ordered_pair(X59,X60))|member(X56,cross_product(X54,X55))|~ilf_type(X56,set_type)|~ilf_type(X55,set_type)|~ilf_type(X54,set_type))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p2])])])])])).
% 0.29/1.61 fof(i_0_26, plain, ![X69, X70, X71, X72]:((~ilf_type(X71,subset_type(cross_product(X69,X70)))|ilf_type(X71,relation_type(X69,X70))|~ilf_type(X70,set_type)|~ilf_type(X69,set_type))&(~ilf_type(X72,relation_type(X69,X70))|ilf_type(X72,subset_type(cross_product(X69,X70)))|~ilf_type(X70,set_type)|~ilf_type(X69,set_type))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p7])])])])).
% 0.29/1.61 fof(i_0_27, plain, ![X100, X101, X102]:(~ilf_type(X100,set_type)|(~ilf_type(X101,set_type)|(~ilf_type(X102,subset_type(cross_product(X100,X101)))|relation_like(X102)))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p18])])])).
% 0.29/1.61 fof(i_0_28, plain, ![X92, X93, X97, X98]:(((ilf_type(esk9_2(X92,X93),set_type)|~member(X93,X92)|~ilf_type(X93,set_type)|~relation_like(X92)|~ilf_type(X92,set_type))&((ilf_type(esk10_2(X92,X93),set_type)|~member(X93,X92)|~ilf_type(X93,set_type)|~relation_like(X92)|~ilf_type(X92,set_type))&(X93=ordered_pair(esk9_2(X92,X93),esk10_2(X92,X93))|~member(X93,X92)|~ilf_type(X93,set_type)|~relation_like(X92)|~ilf_type(X92,set_type))))&((ilf_type(esk11_1(X92),set_type)|relation_like(X92)|~ilf_type(X92,set_type))&((member(esk11_1(X92),X92)|relation_like(X92)|~ilf_type(X92,set_type))&(~ilf_type(X97,set_type)|(~ilf_type(X98,set_type)|esk11_1(X92)!=ordered_pair(X97,X98))|relation_like(X92)|~ilf_type(X92,set_type))))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p16])])])])])).
% 0.29/1.61 fof(i_0_29, plain, ![X80, X81, X82]:((~member(X80,power_set(X81))|(~ilf_type(X82,set_type)|(~member(X82,X80)|member(X82,X81)))|~ilf_type(X81,set_type)|~ilf_type(X80,set_type))&((ilf_type(esk6_2(X80,X81),set_type)|member(X80,power_set(X81))|~ilf_type(X81,set_type)|~ilf_type(X80,set_type))&((member(esk6_2(X80,X81),X80)|member(X80,power_set(X81))|~ilf_type(X81,set_type)|~ilf_type(X80,set_type))&(~member(esk6_2(X80,X81),X81)|member(X80,power_set(X81))|~ilf_type(X81,set_type)|~ilf_type(X80,set_type))))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p11])])])])])).
% 0.29/1.61 fof(i_0_30, plain, ![X63, X64]:((~ilf_type(X64,identity_relation_of_type(X63))|ilf_type(X64,relation_type(X63,X63))|~ilf_type(X64,set_type)|~ilf_type(X63,set_type))&(~ilf_type(X64,relation_type(X63,X63))|ilf_type(X64,identity_relation_of_type(X63))|~ilf_type(X64,set_type)|~ilf_type(X63,set_type))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p4])])])])).
% 0.29/1.61 fof(i_0_31, plain, ![X76, X77]:((~ilf_type(X77,subset_type(X76))|ilf_type(X77,member_type(power_set(X76)))|~ilf_type(X77,set_type)|~ilf_type(X76,set_type))&(~ilf_type(X77,member_type(power_set(X76)))|ilf_type(X77,subset_type(X76))|~ilf_type(X77,set_type)|~ilf_type(X76,set_type))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p9])])])])).
% 0.29/1.61 fof(i_0_32, plain, ![X73, X74]:(~ilf_type(X73,set_type)|(~ilf_type(X74,set_type)|ilf_type(esk4_2(X73,X74),relation_type(X74,X73)))), inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p8])])])])).
% 0.29/1.61 fof(i_0_33, plain, ![X52, X53]:(~ilf_type(X52,set_type)|(~ilf_type(X53,set_type)|ilf_type(cross_product(X52,X53),relation_type(X52,X53)))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p1])])])).
% 0.29/1.61 fof(i_0_34, plain, ![X85, X86]:((~ilf_type(X85,member_type(X86))|member(X85,X86)|(empty(X86)|~ilf_type(X86,set_type))|~ilf_type(X85,set_type))&(~member(X85,X86)|ilf_type(X85,member_type(X86))|(empty(X86)|~ilf_type(X86,set_type))|~ilf_type(X85,set_type))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_20])])])])).
% 0.29/1.61 fof(i_0_35, plain, ![X67, X68]:(~ilf_type(X67,set_type)|(~ilf_type(X68,set_type)|ilf_type(ordered_pair(X67,X68),set_type))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p6])])])).
% 0.29/1.61 fof(i_0_36, plain, ![X61, X62]:(~ilf_type(X61,set_type)|(~ilf_type(X62,set_type)|ilf_type(cross_product(X61,X62),set_type))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p3])])])).
% 0.29/1.61 fof(i_0_37, plain, ![X89, X90]:((~empty(X89)|(~ilf_type(X90,set_type)|~member(X90,X89))|~ilf_type(X89,set_type))&((ilf_type(esk8_1(X89),set_type)|empty(X89)|~ilf_type(X89,set_type))&(member(esk8_1(X89),X89)|empty(X89)|~ilf_type(X89,set_type)))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_21])])])])])).
% 0.29/1.61 fof(i_0_38, negated_conjecture, (ilf_type(esk12_0,set_type)&~ilf_type(cross_product(esk12_0,esk12_0),identity_relation_of_type(esk12_0))), inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_22])])])).
% 0.29/1.61 fof(i_0_39, plain, ![X87]:(empty(X87)|~ilf_type(X87,set_type)|ilf_type(esk7_1(X87),member_type(X87))), inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_23])])])).
% 0.29/1.61 fof(i_0_40, plain, ![X78]:(~ilf_type(X78,set_type)|ilf_type(esk5_1(X78),subset_type(X78))), inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p10])])])).
% 0.29/1.61 fof(i_0_41, plain, ![X65]:(~ilf_type(X65,set_type)|ilf_type(esk3_1(X65),identity_relation_of_type(X65))), inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p5])])])).
% 0.29/1.61 fof(i_0_42, plain, ![X84]:((~empty(power_set(X84))|~ilf_type(X84,set_type))&(ilf_type(power_set(X84),set_type)|~ilf_type(X84,set_type))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_24])])])).
% 0.29/1.61 fof(i_0_43, plain, ![X99]:(~empty(X99)|~ilf_type(X99,set_type)|relation_like(X99)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[p17])])).
% 0.29/1.61 fof(i_0_44, plain, ![X103]:ilf_type(X103,set_type), inference(variable_rename,[status(thm)],[p19])).
% 0.29/1.61 cnf(i_0_45, plain, (X1=ordered_pair(esk1_3(X2,X3,X1),esk2_3(X2,X3,X1))|~member(X1,cross_product(X2,X3))|~ilf_type(X1,set_type)|~ilf_type(X3,set_type)|~ilf_type(X2,set_type)), inference(split_conjunct,[status(thm)],[i_0_25]), ['final']).
% 0.29/1.61 cnf(i_0_46, plain, (member(esk2_3(X1,X2,X3),X2)|~member(X3,cross_product(X1,X2))|~ilf_type(X3,set_type)|~ilf_type(X2,set_type)|~ilf_type(X1,set_type)), inference(split_conjunct,[status(thm)],[i_0_25]), ['final']).
% 0.29/1.61 cnf(i_0_47, plain, (member(esk1_3(X1,X2,X3),X1)|~member(X3,cross_product(X1,X2))|~ilf_type(X3,set_type)|~ilf_type(X2,set_type)|~ilf_type(X1,set_type)), inference(split_conjunct,[status(thm)],[i_0_25]), ['final']).
% 0.29/1.61 cnf(i_0_48, plain, (ilf_type(esk2_3(X1,X2,X3),set_type)|~member(X3,cross_product(X1,X2))|~ilf_type(X3,set_type)|~ilf_type(X2,set_type)|~ilf_type(X1,set_type)), inference(split_conjunct,[status(thm)],[i_0_25]), ['final']).
% 0.29/1.61 cnf(i_0_49, plain, (ilf_type(esk1_3(X1,X2,X3),set_type)|~member(X3,cross_product(X1,X2))|~ilf_type(X3,set_type)|~ilf_type(X2,set_type)|~ilf_type(X1,set_type)), inference(split_conjunct,[status(thm)],[i_0_25]), ['final']).
% 0.29/1.61 cnf(i_0_50, plain, (member(X5,cross_product(X3,X4))|~ilf_type(X1,set_type)|~ilf_type(X2,set_type)|~member(X1,X3)|~member(X2,X4)|X5!=ordered_pair(X1,X2)|~ilf_type(X5,set_type)|~ilf_type(X4,set_type)|~ilf_type(X3,set_type)), inference(split_conjunct,[status(thm)],[i_0_25]), ['final']).
% 0.29/1.61 cnf(i_0_51, plain, (ilf_type(X1,relation_type(X2,X3))|~ilf_type(X1,subset_type(cross_product(X2,X3)))|~ilf_type(X3,set_type)|~ilf_type(X2,set_type)), inference(split_conjunct,[status(thm)],[i_0_26]), ['final']).
% 0.29/1.61 cnf(i_0_52, plain, (ilf_type(X1,subset_type(cross_product(X2,X3)))|~ilf_type(X1,relation_type(X2,X3))|~ilf_type(X3,set_type)|~ilf_type(X2,set_type)), inference(split_conjunct,[status(thm)],[i_0_26]), ['final']).
% 0.29/1.61 cnf(i_0_53, plain, (relation_like(X3)|~ilf_type(X1,set_type)|~ilf_type(X2,set_type)|~ilf_type(X3,subset_type(cross_product(X1,X2)))), inference(split_conjunct,[status(thm)],[i_0_27]), ['final']).
% 0.29/1.61 cnf(i_0_54, plain, (X1=ordered_pair(esk9_2(X2,X1),esk10_2(X2,X1))|~member(X1,X2)|~ilf_type(X1,set_type)|~relation_like(X2)|~ilf_type(X2,set_type)), inference(split_conjunct,[status(thm)],[i_0_28]), ['final']).
% 0.29/1.61 cnf(i_0_55, plain, (member(X3,X2)|~member(X1,power_set(X2))|~ilf_type(X3,set_type)|~member(X3,X1)|~ilf_type(X2,set_type)|~ilf_type(X1,set_type)), inference(split_conjunct,[status(thm)],[i_0_29]), ['final']).
% 0.29/1.61 cnf(i_0_56, plain, (member(X1,power_set(X2))|~member(esk6_2(X1,X2),X2)|~ilf_type(X2,set_type)|~ilf_type(X1,set_type)), inference(split_conjunct,[status(thm)],[i_0_29]), ['final']).
% 0.29/1.61 cnf(i_0_57, plain, (ilf_type(X1,identity_relation_of_type(X2))|~ilf_type(X1,relation_type(X2,X2))|~ilf_type(X1,set_type)|~ilf_type(X2,set_type)), inference(split_conjunct,[status(thm)],[i_0_30]), ['final']).
% 0.29/1.61 cnf(i_0_58, plain, (ilf_type(X1,relation_type(X2,X2))|~ilf_type(X1,identity_relation_of_type(X2))|~ilf_type(X1,set_type)|~ilf_type(X2,set_type)), inference(split_conjunct,[status(thm)],[i_0_30]), ['final']).
% 0.29/1.61 cnf(i_0_59, plain, (ilf_type(X1,subset_type(X2))|~ilf_type(X1,member_type(power_set(X2)))|~ilf_type(X1,set_type)|~ilf_type(X2,set_type)), inference(split_conjunct,[status(thm)],[i_0_31]), ['final']).
% 0.29/1.61 cnf(i_0_60, plain, (ilf_type(esk10_2(X1,X2),set_type)|~member(X2,X1)|~ilf_type(X2,set_type)|~relation_like(X1)|~ilf_type(X1,set_type)), inference(split_conjunct,[status(thm)],[i_0_28]), ['final']).
% 0.29/1.61 cnf(i_0_61, plain, (ilf_type(esk9_2(X1,X2),set_type)|~member(X2,X1)|~ilf_type(X2,set_type)|~relation_like(X1)|~ilf_type(X1,set_type)), inference(split_conjunct,[status(thm)],[i_0_28]), ['final']).
% 0.29/1.61 cnf(i_0_62, plain, (ilf_type(esk4_2(X1,X2),relation_type(X2,X1))|~ilf_type(X1,set_type)|~ilf_type(X2,set_type)), inference(split_conjunct,[status(thm)],[i_0_32]), ['final']).
% 0.29/1.61 cnf(i_0_63, plain, (ilf_type(cross_product(X1,X2),relation_type(X1,X2))|~ilf_type(X1,set_type)|~ilf_type(X2,set_type)), inference(split_conjunct,[status(thm)],[i_0_33]), ['final']).
% 0.29/1.61 cnf(i_0_64, plain, (ilf_type(X1,member_type(power_set(X2)))|~ilf_type(X1,subset_type(X2))|~ilf_type(X1,set_type)|~ilf_type(X2,set_type)), inference(split_conjunct,[status(thm)],[i_0_31]), ['final']).
% 0.29/1.61 cnf(i_0_65, plain, (member(esk6_2(X1,X2),X1)|member(X1,power_set(X2))|~ilf_type(X2,set_type)|~ilf_type(X1,set_type)), inference(split_conjunct,[status(thm)],[i_0_29]), ['final']).
% 0.29/1.61 cnf(i_0_66, plain, (ilf_type(esk6_2(X1,X2),set_type)|member(X1,power_set(X2))|~ilf_type(X2,set_type)|~ilf_type(X1,set_type)), inference(split_conjunct,[status(thm)],[i_0_29]), ['final']).
% 0.29/1.61 cnf(i_0_67, plain, (relation_like(X3)|~ilf_type(X1,set_type)|~ilf_type(X2,set_type)|esk11_1(X3)!=ordered_pair(X1,X2)|~ilf_type(X3,set_type)), inference(split_conjunct,[status(thm)],[i_0_28]), ['final']).
% 0.29/1.61 cnf(i_0_68, plain, (member(X1,X2)|empty(X2)|~ilf_type(X1,member_type(X2))|~ilf_type(X2,set_type)|~ilf_type(X1,set_type)), inference(split_conjunct,[status(thm)],[i_0_34]), ['final']).
% 0.29/1.61 cnf(i_0_69, plain, (ilf_type(X1,member_type(X2))|empty(X2)|~member(X1,X2)|~ilf_type(X2,set_type)|~ilf_type(X1,set_type)), inference(split_conjunct,[status(thm)],[i_0_34]), ['final']).
% 0.29/1.61 cnf(i_0_70, plain, (ilf_type(ordered_pair(X1,X2),set_type)|~ilf_type(X1,set_type)|~ilf_type(X2,set_type)), inference(split_conjunct,[status(thm)],[i_0_35]), ['final']).
% 0.29/1.61 cnf(i_0_71, plain, (ilf_type(cross_product(X1,X2),set_type)|~ilf_type(X1,set_type)|~ilf_type(X2,set_type)), inference(split_conjunct,[status(thm)],[i_0_36]), ['final']).
% 0.29/1.61 cnf(i_0_72, plain, (~empty(X1)|~ilf_type(X2,set_type)|~member(X2,X1)|~ilf_type(X1,set_type)), inference(split_conjunct,[status(thm)],[i_0_37]), ['final']).
% 0.29/1.61 cnf(i_0_73, negated_conjecture, (~ilf_type(cross_product(esk12_0,esk12_0),identity_relation_of_type(esk12_0))), inference(split_conjunct,[status(thm)],[i_0_38]), ['final']).
% 0.29/1.61 cnf(i_0_74, plain, (empty(X1)|ilf_type(esk7_1(X1),member_type(X1))|~ilf_type(X1,set_type)), inference(split_conjunct,[status(thm)],[i_0_39]), ['final']).
% 0.29/1.61 cnf(i_0_75, plain, (ilf_type(esk5_1(X1),subset_type(X1))|~ilf_type(X1,set_type)), inference(split_conjunct,[status(thm)],[i_0_40]), ['final']).
% 0.29/1.61 cnf(i_0_76, plain, (ilf_type(esk3_1(X1),identity_relation_of_type(X1))|~ilf_type(X1,set_type)), inference(split_conjunct,[status(thm)],[i_0_41]), ['final']).
% 0.29/1.61 cnf(i_0_77, plain, (member(esk11_1(X1),X1)|relation_like(X1)|~ilf_type(X1,set_type)), inference(split_conjunct,[status(thm)],[i_0_28]), ['final']).
% 0.29/1.61 cnf(i_0_78, plain, (member(esk8_1(X1),X1)|empty(X1)|~ilf_type(X1,set_type)), inference(split_conjunct,[status(thm)],[i_0_37]), ['final']).
% 0.29/1.61 cnf(i_0_79, plain, (ilf_type(esk11_1(X1),set_type)|relation_like(X1)|~ilf_type(X1,set_type)), inference(split_conjunct,[status(thm)],[i_0_28]), ['final']).
% 0.29/1.61 cnf(i_0_80, plain, (ilf_type(esk8_1(X1),set_type)|empty(X1)|~ilf_type(X1,set_type)), inference(split_conjunct,[status(thm)],[i_0_37]), ['final']).
% 0.29/1.61 cnf(i_0_81, plain, (ilf_type(power_set(X1),set_type)|~ilf_type(X1,set_type)), inference(split_conjunct,[status(thm)],[i_0_42]), ['final']).
% 0.29/1.61 cnf(i_0_82, plain, (~empty(power_set(X1))|~ilf_type(X1,set_type)), inference(split_conjunct,[status(thm)],[i_0_42]), ['final']).
% 0.29/1.61 cnf(i_0_83, plain, (relation_like(X1)|~empty(X1)|~ilf_type(X1,set_type)), inference(split_conjunct,[status(thm)],[i_0_43]), ['final']).
% 0.29/1.61 cnf(i_0_84, plain, (ilf_type(X1,set_type)), inference(split_conjunct,[status(thm)],[i_0_44]), ['final']).
% 0.29/1.61 cnf(i_0_85, negated_conjecture, (ilf_type(esk12_0,set_type)), inference(split_conjunct,[status(thm)],[i_0_38]), ['final']).
% 0.29/1.61 cnf(i_0_86, axiom, (X1=X1)).
% 0.29/1.61 cnf(i_0_87, axiom, (X1=X2|X2!=X1)).
% 0.29/1.61 cnf(i_0_88, axiom, (X1=X2|X1!=X3|X3!=X2)).
% 0.29/1.61 cnf(i_0_89, axiom, (X1!=X2|ordered_pair(X1,X3)=ordered_pair(X2,X3))).
% 0.29/1.61 cnf(i_0_90, axiom, (X1!=X2|ordered_pair(X3,X1)=ordered_pair(X3,X2))).
% 0.29/1.61 cnf(i_0_91, axiom, (X1!=X2|esk11_1(X1)=esk11_1(X2))).
% 0.29/1.61 cnf(i_0_92, axiom, (X1!=X2|~member(X1,X3)|member(X2,X3))).
% 0.29/1.61 cnf(i_0_93, axiom, (X1!=X2|~member(X3,X1)|member(X3,X2))).
% 0.29/1.61 cnf(i_0_94, axiom, (X1!=X2|~ilf_type(X1,X3)|ilf_type(X2,X3))).
% 0.29/1.61 cnf(i_0_95, axiom, (X1!=X2|~ilf_type(X3,X1)|ilf_type(X3,X2))).
% 0.29/1.61 cnf(i_0_96, axiom, (X1!=X2|~relation_like(X1)|relation_like(X2))).
% 0.29/1.62 cnf(i_0_97, axiom, (X1!=X2|~empty(X1)|empty(X2))).
% 0.38/1.72 cnf(i_0_86, axiom, (X1=X1)).
% 0.38/1.72 cnf(i_0_87, axiom, (X1=X2|X2!=X1)).
% 0.38/1.72 cnf(i_0_88, axiom, (X1=X2|X1!=X3|X3!=X2)).
% 0.38/1.72 cnf(i_0_89, axiom, (X1!=X2|ordered_pair(X1,X3)=ordered_pair(X2,X3))).
% 0.38/1.72 cnf(i_0_90, axiom, (X1!=X2|ordered_pair(X3,X1)=ordered_pair(X3,X2))).
% 0.38/1.72 cnf(i_0_91, axiom, (X1!=X2|esk11_1(X1)=esk11_1(X2))).
% 0.38/1.72 cnf(i_0_92, axiom, (X1!=X2|~member(X1,X3)|member(X2,X3))).
% 0.38/1.72 cnf(i_0_93, axiom, (X1!=X2|~member(X3,X1)|member(X3,X2))).
% 0.38/1.72 cnf(i_0_94, axiom, (X1!=X2|~ilf_type(X1,X3)|ilf_type(X2,X3))).
% 0.38/1.72 cnf(i_0_95, axiom, (X1!=X2|~ilf_type(X3,X1)|ilf_type(X3,X2))).
% 0.38/1.72 cnf(i_0_96, axiom, (X1!=X2|~relation_like(X1)|relation_like(X2))).
% 0.38/1.72 cnf(i_0_97, axiom, (X1!=X2|~empty(X1)|empty(X2))).
% 0.38/1.72 cnf(i_0_98, plain, (~member(X1,X2)|~member(X3,X4)|~ilf_type(ordered_pair(X1,X3),set_type)|~ilf_type(X4,set_type)|~ilf_type(X2,set_type)|member(ordered_pair(X1,X3),cross_product(X2,X4))|~ilf_type(X1,set_type)|~ilf_type(X3,set_type)), inference(equality_inference,[],[50])).
% 0.38/1.72 cnf(i_0_99, plain, (ilf_type(esk5_1(X1),subset_type(X1))), inference(scs_inference,[],[i_0_84,i_0_75])).
% 0.38/1.72 cnf(i_0_100, plain, (~ilf_type(X1,set_type)|ilf_type(esk5_1(X1),subset_type(X1))), inference(rename_variables,[],[i_0_75])).
% 0.38/1.72 cnf(i_0_101, plain, (ilf_type(esk3_1(X1),identity_relation_of_type(X1))), inference(scs_inference,[],[i_0_84,i_0_75,i_0_76])).
% 0.38/1.72 cnf(i_0_102, plain, (~ilf_type(X1,set_type)|ilf_type(esk3_1(X1),identity_relation_of_type(X1))), inference(rename_variables,[],[i_0_76])).
% 0.38/1.72 cnf(i_0_103, plain, (set_type!=identity_relation_of_type(esk12_0)), inference(scs_inference,[],[i_0_73,i_0_84,i_0_75,i_0_76,i_0_95])).
% 0.38/1.72 cnf(i_0_104, plain, (ilf_type(X1,set_type)), inference(rename_variables,[],[i_0_84])).
% 0.38/1.72 cnf(i_0_105, plain, (ilf_type(esk4_2(X1,X1),relation_type(X1,X1))), inference(scs_inference,[],[i_0_73,i_0_84,i_0_104,i_0_75,i_0_76,i_0_95,i_0_62])).
% 0.38/1.72 cnf(i_0_106, plain, (~ilf_type(X1,set_type)|~ilf_type(X2,set_type)|ilf_type(esk4_2(X1,X2),relation_type(X2,X1))), inference(rename_variables,[],[i_0_62])).
% 0.38/1.72 cnf(i_0_107, plain, (ilf_type(cross_product(X1,X1),relation_type(X1,X1))), inference(scs_inference,[],[i_0_73,i_0_84,i_0_104,i_0_75,i_0_76,i_0_95,i_0_62,i_0_63])).
% 0.38/1.72 cnf(i_0_108, plain, (~ilf_type(X1,set_type)|~ilf_type(X2,set_type)|ilf_type(cross_product(X1,X2),relation_type(X1,X2))), inference(rename_variables,[],[i_0_63])).
% 0.38/1.72 cnf(i_0_109, plain, (~ilf_type(cross_product(esk12_0,esk12_0),set_type)), inference(scs_inference,[],[i_0_73,i_0_84,i_0_104,i_0_75,i_0_76,i_0_95,i_0_62,i_0_63,i_0_57])).
% 0.38/1.72 cnf(i_0_110, plain, (ilf_type(X1,set_type)), inference(rename_variables,[],[i_0_84])).
% 0.38/1.72 cnf(i_0_111, plain, (~ilf_type(X1,relation_type(X2,X2))|~ilf_type(X1,set_type)|~ilf_type(X2,set_type)|ilf_type(X1,identity_relation_of_type(X2))), inference(rename_variables,[],[i_0_57])).
% 0.38/1.72 cnf(i_0_112, plain, (ilf_type(esk5_1(cross_product(esk12_0,esk12_0)),relation_type(esk12_0,esk12_0))), inference(scs_inference,[],[i_0_73,i_0_84,i_0_104,i_0_110,i_0_75,i_0_76,i_0_95,i_0_62,i_0_63,i_0_57,i_0_51])).
% 0.38/1.72 cnf(i_0_113, plain, (ilf_type(X1,set_type)), inference(rename_variables,[],[i_0_84])).
% 0.38/1.72 cnf(i_0_114, plain, (~ilf_type(X1,subset_type(cross_product(X2,X3)))|~ilf_type(X3,set_type)|~ilf_type(X2,set_type)|ilf_type(X1,relation_type(X2,X3))), inference(rename_variables,[],[i_0_51])).
% 0.38/1.72 cnf(i_0_115, plain, (relation_like(esk5_1(cross_product(esk12_0,esk12_0)))), inference(scs_inference,[],[i_0_73,i_0_84,i_0_104,i_0_110,i_0_113,i_0_75,i_0_76,i_0_95,i_0_62,i_0_63,i_0_57,i_0_51,i_0_53])).
% 0.38/1.72 cnf(i_0_116, plain, (ilf_type(X1,set_type)), inference(rename_variables,[],[i_0_84])).
% 0.38/1.72 cnf(i_0_117, plain, (~ilf_type(X1,subset_type(cross_product(X2,X3)))|~ilf_type(X2,set_type)|~ilf_type(X3,set_type)|relation_like(X1)), inference(rename_variables,[],[i_0_53])).
% 0.38/1.72 cnf(i_0_118, plain, (X1!=cross_product(esk12_0,esk12_0)|~ilf_type(X1,identity_relation_of_type(esk12_0))), inference(scs_inference,[],[i_0_73,i_0_84,i_0_104,i_0_110,i_0_113,i_0_75,i_0_76,i_0_95,i_0_62,i_0_63,i_0_57,i_0_51,i_0_53,i_0_94])).
% 0.38/1.72 cnf(i_0_119, plain, (relation_like(X1)|member(esk11_1(X1),X1)), inference(scs_inference,[],[i_0_73,i_0_84,i_0_104,i_0_110,i_0_113,i_0_116,i_0_75,i_0_76,i_0_95,i_0_62,i_0_63,i_0_57,i_0_51,i_0_53,i_0_94,i_0_77])).
% 0.38/1.72 cnf(i_0_120, plain, (~ilf_type(X1,set_type)|member(esk11_1(X1),X1)|relation_like(X1)), inference(rename_variables,[],[i_0_77])).
% 0.38/1.72 cnf(i_0_121, plain, (empty(X1)|member(esk8_1(X1),X1)), inference(scs_inference,[],[i_0_73,i_0_84,i_0_104,i_0_110,i_0_113,i_0_116,i_0_75,i_0_76,i_0_95,i_0_62,i_0_63,i_0_57,i_0_51,i_0_53,i_0_94,i_0_77,i_0_78])).
% 0.38/1.72 cnf(i_0_122, plain, (~ilf_type(X1,set_type)|member(esk8_1(X1),X1)|empty(X1)), inference(rename_variables,[],[i_0_78])).
% 0.38/1.72 cnf(i_0_123, plain, (~empty(X1)|relation_like(X1)), inference(scs_inference,[],[i_0_73,i_0_84,i_0_104,i_0_110,i_0_113,i_0_116,i_0_75,i_0_76,i_0_95,i_0_62,i_0_63,i_0_57,i_0_51,i_0_53,i_0_94,i_0_77,i_0_78,i_0_83])).
% 0.38/1.72 cnf(i_0_124, plain, (~ilf_type(X1,set_type)|~empty(X1)|relation_like(X1)), inference(rename_variables,[],[i_0_83])).
% 0.38/1.72 cnf(i_0_125, plain, (relation_like(X1)|esk5_1(cross_product(esk12_0,esk12_0))!=X1), inference(scs_inference,[],[i_0_73,i_0_84,i_0_104,i_0_110,i_0_113,i_0_116,i_0_75,i_0_76,i_0_95,i_0_62,i_0_63,i_0_57,i_0_51,i_0_53,i_0_94,i_0_77,i_0_78,i_0_83,i_0_96])).
% 0.38/1.72 cnf(i_0_126, plain, (~member(X1,X1)|~empty(X1)), inference(scs_inference,[],[i_0_73,i_0_84,i_0_104,i_0_110,i_0_113,i_0_116,i_0_75,i_0_76,i_0_95,i_0_62,i_0_63,i_0_57,i_0_51,i_0_53,i_0_94,i_0_77,i_0_78,i_0_83,i_0_96,i_0_72])).
% 0.38/1.72 cnf(i_0_127, plain, (~ilf_type(X1,set_type)|~ilf_type(X2,set_type)|~member(X2,X1)|~empty(X1)), inference(rename_variables,[],[i_0_72])).
% 0.38/1.72 cnf(i_0_128, plain, (~ilf_type(cross_product(esk12_0,esk12_0),identity_relation_of_type(esk12_0))), inference(equality_inference,[],[118])).
% 0.38/1.72 cnf(i_0_129, plain, (relation_like(esk5_1(cross_product(esk12_0,esk12_0)))), inference(equality_inference,[],[125])).
% 0.38/1.72 cnf(i_0_130,plain, ($false), inference(scs_inference,[],[i_0+109, i_0_84]), ['proof']).
% 0.38/1.72 % SZS output end CNFRefutation
% 0.38/1.72 % Total time : 1.268s
%------------------------------------------------------------------------------