%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SEU186+2 : TPTP v9.2.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n020.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:10:59 PM UTC 2026
% Result : Theorem 4.35s 3.33s
% Output : CNFRefutation 4.35s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 27
% Syntax : Number of formulae : 141 ( 50 unt; 0 def)
% Number of atoms : 423 ( 126 equ)
% Maximal formula atoms : 28 ( 3 avg)
% Number of connectives : 477 ( 195 ~; 170 |; 75 &)
% ( 20 <=>; 17 =>; 0 <=; 0 <~>)
% Maximal formula depth : 23 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 32 ( 32 usr; 2 con; 0-4 aty)
% Number of variables : 321 ( 24 sgn 188 !; 10 ?)
% Comments :
%------------------------------------------------------------------------------
fof(d6_relat_1,axiom,
! [X1] :
( relation(X1)
=> relation_field(X1) = set_union2(relation_dom(X1),relation_rng(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d6_relat_1) ).
fof(commutativity_k2_xboole_0,axiom,
! [X1,X2] : set_union2(X1,X2) = set_union2(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_k2_xboole_0) ).
fof(t56_relat_1,conjecture,
! [X1] :
( relation(X1)
=> ( ! [X2,X3] : ~ in(ordered_pair(X2,X3),X1)
=> X1 = empty_set ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t56_relat_1) ).
fof(d4_xboole_0,axiom,
! [X1,X2,X3] :
( X3 = set_difference(X1,X2)
<=> ! [X4] :
( in(X4,X3)
<=> ( in(X4,X1)
& ~ in(X4,X2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d4_xboole_0) ).
fof(t7_xboole_1,lemma,
! [X1,X2] : subset(X1,set_union2(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_xboole_1) ).
fof(d1_xboole_0,axiom,
! [X1] :
( X1 = empty_set
<=> ! [X2] : ~ in(X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_xboole_0) ).
fof(t3_xboole_0,lemma,
! [X1,X2] :
( ~ ( ~ disjoint(X1,X2)
& ! [X3] :
~ ( in(X3,X1)
& in(X3,X2) ) )
& ~ ( ? [X3] :
( in(X3,X1)
& in(X3,X2) )
& disjoint(X1,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t3_xboole_0) ).
fof(l32_xboole_1,lemma,
! [X1,X2] :
( set_difference(X1,X2) = empty_set
<=> subset(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',l32_xboole_1) ).
fof(t83_xboole_1,lemma,
! [X1,X2] :
( disjoint(X1,X2)
<=> set_difference(X1,X2) = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t83_xboole_1) ).
fof(d5_tarski,axiom,
! [X1,X2] : ordered_pair(X1,X2) = unordered_pair(unordered_pair(X1,X2),singleton(X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d5_tarski) ).
fof(t69_enumset1,lemma,
! [X1] : unordered_pair(X1,X1) = singleton(X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t69_enumset1) ).
fof(d3_tarski,axiom,
! [X1,X2] :
( subset(X1,X2)
<=> ! [X3] :
( in(X3,X1)
=> in(X3,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d3_tarski) ).
fof(t4_xboole_0,lemma,
! [X1,X2] :
( ~ ( ~ disjoint(X1,X2)
& ! [X3] : ~ in(X3,set_intersection2(X1,X2)) )
& ~ ( ? [X3] : in(X3,set_intersection2(X1,X2))
& disjoint(X1,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t4_xboole_0) ).
fof(d4_relat_1,axiom,
! [X1] :
( relation(X1)
=> ! [X2] :
( X2 = relation_dom(X1)
<=> ! [X3] :
( in(X3,X2)
<=> ? [X4] : in(ordered_pair(X3,X4),X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d4_relat_1) ).
fof(t12_xboole_1,lemma,
! [X1,X2] :
( subset(X1,X2)
=> set_union2(X1,X2) = X2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t12_xboole_1) ).
fof(t48_xboole_1,lemma,
! [X1,X2] : set_difference(X1,set_difference(X1,X2)) = set_intersection2(X1,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t48_xboole_1) ).
fof(commutativity_k2_tarski,axiom,
! [X1,X2] : unordered_pair(X1,X2) = unordered_pair(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_k2_tarski) ).
fof(antisymmetry_r2_hidden,axiom,
! [X1,X2] :
( in(X1,X2)
=> ~ in(X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',antisymmetry_r2_hidden) ).
fof(t9_tarski,axiom,
! [X1] :
? [X2] :
( in(X1,X2)
& ! [X3,X4] :
( ( in(X3,X2)
& subset(X4,X3) )
=> in(X4,X2) )
& ! [X3] :
~ ( in(X3,X2)
& ! [X4] :
~ ( in(X4,X2)
& ! [X5] :
( subset(X5,X3)
=> in(X5,X4) ) ) )
& ! [X3] :
~ ( subset(X3,X2)
& ~ are_equipotent(X3,X2)
& ~ in(X3,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t9_tarski) ).
fof(t3_boole,axiom,
! [X1] : set_difference(X1,empty_set) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t3_boole) ).
fof(t2_tarski,axiom,
! [X1,X2] :
( ! [X3] :
( in(X3,X1)
<=> in(X3,X2) )
=> X1 = X2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2_tarski) ).
fof(d2_zfmisc_1,axiom,
! [X1,X2,X3] :
( X3 = cartesian_product2(X1,X2)
<=> ! [X4] :
( in(X4,X3)
<=> ? [X5,X6] :
( in(X5,X1)
& in(X6,X2)
& X4 = ordered_pair(X5,X6) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d2_zfmisc_1) ).
fof(d2_xboole_0,axiom,
! [X1,X2,X3] :
( X3 = set_union2(X1,X2)
<=> ! [X4] :
( in(X4,X3)
<=> ( in(X4,X1)
| in(X4,X2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d2_xboole_0) ).
fof(t65_zfmisc_1,lemma,
! [X1,X2] :
( set_difference(X1,singleton(X2)) = X1
<=> ~ in(X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t65_zfmisc_1) ).
fof(t21_relat_1,lemma,
! [X1] :
( relation(X1)
=> subset(X1,cartesian_product2(relation_dom(X1),relation_rng(X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t21_relat_1) ).
fof(d5_relat_1,axiom,
! [X1] :
( relation(X1)
=> ! [X2] :
( X2 = relation_rng(X1)
<=> ! [X3] :
( in(X3,X2)
<=> ? [X4] : in(ordered_pair(X4,X3),X1) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d5_relat_1) ).
fof(t1_boole,axiom,
! [X1] : set_union2(X1,empty_set) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_boole) ).
fof(c_0_27,plain,
! [X505] :
( ~ relation(X505)
| relation_field(X505) = set_union2(relation_dom(X505),relation_rng(X505)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[d6_relat_1])]) ).
fof(c_0_28,plain,
! [X363,X364] : set_union2(X363,X364) = set_union2(X364,X363),
inference(variable_rename,[status(thm)],[commutativity_k2_xboole_0]) ).
fof(c_0_29,negated_conjecture,
~ ! [X1] :
( relation(X1)
=> ( ! [X2,X3] : ~ in(ordered_pair(X2,X3),X1)
=> X1 = empty_set ) ),
inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[t56_relat_1])]) ).
cnf(c_0_30,plain,
( relation_field(X1) = set_union2(relation_dom(X1),relation_rng(X1))
| ~ relation(X1) ),
inference(split_conjunct,[status(thm)],[c_0_27]) ).
cnf(c_0_31,plain,
set_union2(X1,X2) = set_union2(X2,X1),
inference(split_conjunct,[status(thm)],[c_0_28]) ).
fof(c_0_32,negated_conjecture,
! [X749,X750] :
( relation(esk48_0)
& ~ in(ordered_pair(X749,X750),esk48_0)
& esk48_0 != empty_set ),
inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_29])])])]) ).
fof(c_0_33,plain,
! [X1,X2,X3] :
( X3 = set_difference(X1,X2)
<=> ! [X4] :
( in(X4,X3)
<=> ( in(X4,X1)
& ~ in(X4,X2) ) ) ),
inference(fof_simplification,[status(thm)],[d4_xboole_0]) ).
fof(c_0_34,lemma,
! [X767,X768] : subset(X767,set_union2(X767,X768)),
inference(variable_rename,[status(thm)],[t7_xboole_1]) ).
cnf(c_0_35,plain,
( set_union2(relation_rng(X1),relation_dom(X1)) = relation_field(X1)
| ~ relation(X1) ),
inference(rw,[status(thm)],[c_0_30,c_0_31]) ).
cnf(c_0_36,negated_conjecture,
relation(esk48_0),
inference(split_conjunct,[status(thm)],[c_0_32]) ).
fof(c_0_37,plain,
! [X1] :
( X1 = empty_set
<=> ! [X2] : ~ in(X2,X1) ),
inference(fof_simplification,[status(thm)],[d1_xboole_0]) ).
fof(c_0_38,lemma,
! [X1,X2] :
( ~ ( ~ disjoint(X1,X2)
& ! [X3] :
~ ( in(X3,X1)
& in(X3,X2) ) )
& ~ ( ? [X3] :
( in(X3,X1)
& in(X3,X2) )
& disjoint(X1,X2) ) ),
inference(fof_simplification,[status(thm)],[t3_xboole_0]) ).
fof(c_0_39,plain,
! [X482,X483,X484,X485,X486,X487,X488,X489] :
( ( in(X485,X482)
| ~ in(X485,X484)
| X484 != set_difference(X482,X483) )
& ( ~ in(X485,X483)
| ~ in(X485,X484)
| X484 != set_difference(X482,X483) )
& ( ~ in(X486,X482)
| in(X486,X483)
| in(X486,X484)
| X484 != set_difference(X482,X483) )
& ( ~ in(esk25_3(X487,X488,X489),X489)
| ~ in(esk25_3(X487,X488,X489),X487)
| in(esk25_3(X487,X488,X489),X488)
| X489 = set_difference(X487,X488) )
& ( in(esk25_3(X487,X488,X489),X487)
| in(esk25_3(X487,X488,X489),X489)
| X489 = set_difference(X487,X488) )
& ( ~ in(esk25_3(X487,X488,X489),X488)
| in(esk25_3(X487,X488,X489),X489)
| X489 = set_difference(X487,X488) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_33])])])])])]) ).
fof(c_0_40,lemma,
! [X584,X585] :
( ( set_difference(X584,X585) != empty_set
| subset(X584,X585) )
& ( ~ subset(X584,X585)
| set_difference(X584,X585) = empty_set ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[l32_xboole_1])]) ).
cnf(c_0_41,lemma,
subset(X1,set_union2(X1,X2)),
inference(split_conjunct,[status(thm)],[c_0_34]) ).
cnf(c_0_42,negated_conjecture,
set_union2(relation_rng(esk48_0),relation_dom(esk48_0)) = relation_field(esk48_0),
inference(spm,[status(thm)],[c_0_35,c_0_36]) ).
fof(c_0_43,plain,
! [X397,X398,X399] :
( ( X397 != empty_set
| ~ in(X398,X397) )
& ( in(esk8_1(X399),X399)
| X399 = empty_set ) ),
inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_37])])])])]) ).
fof(c_0_44,lemma,
! [X700,X701,X703,X704,X705] :
( ( in(esk46_2(X700,X701),X700)
| disjoint(X700,X701) )
& ( in(esk46_2(X700,X701),X701)
| disjoint(X700,X701) )
& ( ~ in(X705,X703)
| ~ in(X705,X704)
| ~ disjoint(X703,X704) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_38])])])])])]) ).
fof(c_0_45,lemma,
! [X769,X770] :
( ( ~ disjoint(X769,X770)
| set_difference(X769,X770) = X769 )
& ( set_difference(X769,X770) != X769
| disjoint(X769,X770) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t83_xboole_1])]) ).
cnf(c_0_46,plain,
( in(X1,X3)
| in(X1,X4)
| ~ in(X1,X2)
| X4 != set_difference(X2,X3) ),
inference(split_conjunct,[status(thm)],[c_0_39]) ).
cnf(c_0_47,lemma,
( set_difference(X1,X2) = empty_set
| ~ subset(X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_40]) ).
cnf(c_0_48,lemma,
subset(relation_rng(esk48_0),relation_field(esk48_0)),
inference(spm,[status(thm)],[c_0_41,c_0_42]) ).
cnf(c_0_49,plain,
( X1 != empty_set
| ~ in(X2,X1) ),
inference(split_conjunct,[status(thm)],[c_0_43]) ).
cnf(c_0_50,lemma,
( ~ in(X1,X2)
| ~ in(X1,X3)
| ~ disjoint(X2,X3) ),
inference(split_conjunct,[status(thm)],[c_0_44]) ).
cnf(c_0_51,lemma,
( disjoint(X1,X2)
| set_difference(X1,X2) != X1 ),
inference(split_conjunct,[status(thm)],[c_0_45]) ).
cnf(c_0_52,plain,
( in(X1,set_difference(X2,X3))
| in(X1,X3)
| ~ in(X1,X2) ),
inference(er,[status(thm)],[c_0_46]) ).
cnf(c_0_53,lemma,
set_difference(relation_rng(esk48_0),relation_field(esk48_0)) = empty_set,
inference(spm,[status(thm)],[c_0_47,c_0_48]) ).
cnf(c_0_54,plain,
~ in(X1,empty_set),
inference(er,[status(thm)],[c_0_49]) ).
fof(c_0_55,plain,
! [X503,X504] : ordered_pair(X503,X504) = unordered_pair(unordered_pair(X503,X504),singleton(X503)),
inference(variable_rename,[status(thm)],[d5_tarski]) ).
fof(c_0_56,lemma,
! [X761] : unordered_pair(X761,X761) = singleton(X761),
inference(variable_rename,[status(thm)],[t69_enumset1]) ).
cnf(c_0_57,lemma,
( set_difference(X1,X2) != X1
| ~ in(X3,X2)
| ~ in(X3,X1) ),
inference(spm,[status(thm)],[c_0_50,c_0_51]) ).
cnf(c_0_58,lemma,
( in(X1,relation_field(esk48_0))
| ~ in(X1,relation_rng(esk48_0)) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_52,c_0_53]),c_0_54]) ).
fof(c_0_59,plain,
! [X445,X446,X447,X448,X449] :
( ( ~ subset(X445,X446)
| ~ in(X447,X445)
| in(X447,X446) )
& ( in(esk17_2(X448,X449),X448)
| subset(X448,X449) )
& ( ~ in(esk17_2(X448,X449),X449)
| subset(X448,X449) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[d3_tarski])])])])])]) ).
fof(c_0_60,lemma,
! [X1,X2] :
( ~ ( ~ disjoint(X1,X2)
& ! [X3] : ~ in(X3,set_intersection2(X1,X2)) )
& ~ ( ? [X3] : in(X3,set_intersection2(X1,X2))
& disjoint(X1,X2) ) ),
inference(fof_simplification,[status(thm)],[t4_xboole_0]) ).
fof(c_0_61,plain,
! [X460,X461,X462,X464,X465,X466,X468] :
( ( ~ in(X462,X461)
| in(ordered_pair(X462,esk19_3(X460,X461,X462)),X460)
| X461 != relation_dom(X460)
| ~ relation(X460) )
& ( ~ in(ordered_pair(X464,X465),X460)
| in(X464,X461)
| X461 != relation_dom(X460)
| ~ relation(X460) )
& ( ~ in(esk20_2(X460,X466),X466)
| ~ in(ordered_pair(esk20_2(X460,X466),X468),X460)
| X466 = relation_dom(X460)
| ~ relation(X460) )
& ( in(esk20_2(X460,X466),X466)
| in(ordered_pair(esk20_2(X460,X466),esk21_2(X460,X466)),X460)
| X466 = relation_dom(X460)
| ~ relation(X460) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[d4_relat_1])])])])])]) ).
cnf(c_0_62,plain,
ordered_pair(X1,X2) = unordered_pair(unordered_pair(X1,X2),singleton(X1)),
inference(split_conjunct,[status(thm)],[c_0_55]) ).
cnf(c_0_63,lemma,
unordered_pair(X1,X1) = singleton(X1),
inference(split_conjunct,[status(thm)],[c_0_56]) ).
fof(c_0_64,lemma,
! [X636,X637] :
( ~ subset(X636,X637)
| set_union2(X636,X637) = X637 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t12_xboole_1])]) ).
cnf(c_0_65,lemma,
( relation_rng(esk48_0) != empty_set
| ~ in(X1,relation_rng(esk48_0)) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_57,c_0_53]),c_0_58]) ).
cnf(c_0_66,plain,
( in(esk17_2(X1,X2),X1)
| subset(X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_59]) ).
fof(c_0_67,lemma,
! [X736,X737,X739,X740,X741] :
( ( disjoint(X736,X737)
| in(esk47_2(X736,X737),set_intersection2(X736,X737)) )
& ( ~ in(X741,set_intersection2(X739,X740))
| ~ disjoint(X739,X740) ) ),
inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_60])])])])]) ).
fof(c_0_68,lemma,
! [X730,X731] : set_difference(X730,set_difference(X730,X731)) = set_intersection2(X730,X731),
inference(variable_rename,[status(thm)],[t48_xboole_1]) ).
cnf(c_0_69,lemma,
subset(X1,set_union2(X2,X1)),
inference(spm,[status(thm)],[c_0_41,c_0_31]) ).
cnf(c_0_70,plain,
( in(ordered_pair(X1,esk19_3(X3,X2,X1)),X3)
| ~ in(X1,X2)
| X2 != relation_dom(X3)
| ~ relation(X3) ),
inference(split_conjunct,[status(thm)],[c_0_61]) ).
cnf(c_0_71,plain,
ordered_pair(X1,X2) = unordered_pair(unordered_pair(X1,X2),unordered_pair(X1,X1)),
inference(rw,[status(thm)],[c_0_62,c_0_63]) ).
fof(c_0_72,plain,
! [X361,X362] : unordered_pair(X361,X362) = unordered_pair(X362,X361),
inference(variable_rename,[status(thm)],[commutativity_k2_tarski]) ).
cnf(c_0_73,lemma,
( set_union2(X1,X2) = X2
| ~ subset(X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_64]) ).
cnf(c_0_74,lemma,
( subset(relation_rng(esk48_0),X1)
| relation_rng(esk48_0) != empty_set ),
inference(spm,[status(thm)],[c_0_65,c_0_66]) ).
cnf(c_0_75,negated_conjecture,
~ in(ordered_pair(X1,X2),esk48_0),
inference(split_conjunct,[status(thm)],[c_0_32]) ).
fof(c_0_76,plain,
! [X1,X2] :
( in(X1,X2)
=> ~ in(X2,X1) ),
inference(fof_simplification,[status(thm)],[antisymmetry_r2_hidden]) ).
fof(c_0_77,plain,
! [X1] :
? [X2] :
( in(X1,X2)
& ! [X3,X4] :
( ( in(X3,X2)
& subset(X4,X3) )
=> in(X4,X2) )
& ! [X3] :
~ ( in(X3,X2)
& ! [X4] :
~ ( in(X4,X2)
& ! [X5] :
( subset(X5,X3)
=> in(X5,X4) ) ) )
& ! [X3] :
~ ( subset(X3,X2)
& ~ are_equipotent(X3,X2)
& ~ in(X3,X2) ) ),
inference(fof_simplification,[status(thm)],[t9_tarski]) ).
cnf(c_0_78,lemma,
( ~ in(X1,set_intersection2(X2,X3))
| ~ disjoint(X2,X3) ),
inference(split_conjunct,[status(thm)],[c_0_67]) ).
cnf(c_0_79,lemma,
set_difference(X1,set_difference(X1,X2)) = set_intersection2(X1,X2),
inference(split_conjunct,[status(thm)],[c_0_68]) ).
cnf(c_0_80,negated_conjecture,
subset(relation_dom(esk48_0),relation_field(esk48_0)),
inference(spm,[status(thm)],[c_0_69,c_0_42]) ).
fof(c_0_81,plain,
! [X697] : set_difference(X697,empty_set) = X697,
inference(variable_rename,[status(thm)],[t3_boole]) ).
fof(c_0_82,plain,
! [X669,X670] :
( ( ~ in(esk45_2(X669,X670),X669)
| ~ in(esk45_2(X669,X670),X670)
| X669 = X670 )
& ( in(esk45_2(X669,X670),X669)
| in(esk45_2(X669,X670),X670)
| X669 = X670 ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t2_tarski])])])]) ).
cnf(c_0_83,plain,
( in(unordered_pair(unordered_pair(X1,esk19_3(X3,X2,X1)),unordered_pair(X1,X1)),X3)
| X2 != relation_dom(X3)
| ~ relation(X3)
| ~ in(X1,X2) ),
inference(rw,[status(thm)],[c_0_70,c_0_71]) ).
cnf(c_0_84,plain,
unordered_pair(X1,X2) = unordered_pair(X2,X1),
inference(split_conjunct,[status(thm)],[c_0_72]) ).
cnf(c_0_85,lemma,
( set_union2(relation_rng(esk48_0),X1) = X1
| relation_rng(esk48_0) != empty_set ),
inference(spm,[status(thm)],[c_0_73,c_0_74]) ).
cnf(c_0_86,negated_conjecture,
~ in(unordered_pair(unordered_pair(X1,X2),unordered_pair(X1,X1)),esk48_0),
inference(rw,[status(thm)],[c_0_75,c_0_71]) ).
fof(c_0_87,plain,
! [X428,X429,X430,X431,X434,X435,X436,X437,X438,X439,X441,X442] :
( ( in(esk12_4(X428,X429,X430,X431),X428)
| ~ in(X431,X430)
| X430 != cartesian_product2(X428,X429) )
& ( in(esk13_4(X428,X429,X430,X431),X429)
| ~ in(X431,X430)
| X430 != cartesian_product2(X428,X429) )
& ( X431 = ordered_pair(esk12_4(X428,X429,X430,X431),esk13_4(X428,X429,X430,X431))
| ~ in(X431,X430)
| X430 != cartesian_product2(X428,X429) )
& ( ~ in(X435,X428)
| ~ in(X436,X429)
| X434 != ordered_pair(X435,X436)
| in(X434,X430)
| X430 != cartesian_product2(X428,X429) )
& ( ~ in(esk14_3(X437,X438,X439),X439)
| ~ in(X441,X437)
| ~ in(X442,X438)
| esk14_3(X437,X438,X439) != ordered_pair(X441,X442)
| X439 = cartesian_product2(X437,X438) )
& ( in(esk15_3(X437,X438,X439),X437)
| in(esk14_3(X437,X438,X439),X439)
| X439 = cartesian_product2(X437,X438) )
& ( in(esk16_3(X437,X438,X439),X438)
| in(esk14_3(X437,X438,X439),X439)
| X439 = cartesian_product2(X437,X438) )
& ( esk14_3(X437,X438,X439) = ordered_pair(esk15_3(X437,X438,X439),esk16_3(X437,X438,X439))
| in(esk14_3(X437,X438,X439),X439)
| X439 = cartesian_product2(X437,X438) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[d2_zfmisc_1])])])])])]) ).
fof(c_0_88,plain,
! [X356,X357] :
( ~ in(X356,X357)
| ~ in(X357,X356) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_76])]) ).
fof(c_0_89,plain,
! [X782,X784,X785,X786,X788,X789] :
( in(X782,esk49_1(X782))
& ( ~ in(X784,esk49_1(X782))
| ~ subset(X785,X784)
| in(X785,esk49_1(X782)) )
& ( in(esk50_2(X782,X786),esk49_1(X782))
| ~ in(X786,esk49_1(X782)) )
& ( ~ subset(X788,X786)
| in(X788,esk50_2(X782,X786))
| ~ in(X786,esk49_1(X782)) )
& ( ~ subset(X789,esk49_1(X782))
| are_equipotent(X789,esk49_1(X782))
| in(X789,esk49_1(X782)) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_77])])])])]) ).
fof(c_0_90,plain,
! [X419,X420,X421,X422,X423,X424,X425,X426] :
( ( ~ in(X422,X421)
| in(X422,X419)
| in(X422,X420)
| X421 != set_union2(X419,X420) )
& ( ~ in(X423,X419)
| in(X423,X421)
| X421 != set_union2(X419,X420) )
& ( ~ in(X423,X420)
| in(X423,X421)
| X421 != set_union2(X419,X420) )
& ( ~ in(esk11_3(X424,X425,X426),X424)
| ~ in(esk11_3(X424,X425,X426),X426)
| X426 = set_union2(X424,X425) )
& ( ~ in(esk11_3(X424,X425,X426),X425)
| ~ in(esk11_3(X424,X425,X426),X426)
| X426 = set_union2(X424,X425) )
& ( in(esk11_3(X424,X425,X426),X426)
| in(esk11_3(X424,X425,X426),X424)
| in(esk11_3(X424,X425,X426),X425)
| X426 = set_union2(X424,X425) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[d2_xboole_0])])])])])]) ).
cnf(c_0_91,lemma,
( ~ disjoint(X2,X3)
| ~ in(X1,set_difference(X2,set_difference(X2,X3))) ),
inference(rw,[status(thm)],[c_0_78,c_0_79]) ).
cnf(c_0_92,lemma,
set_difference(relation_dom(esk48_0),relation_field(esk48_0)) = empty_set,
inference(spm,[status(thm)],[c_0_47,c_0_80]) ).
cnf(c_0_93,plain,
set_difference(X1,empty_set) = X1,
inference(split_conjunct,[status(thm)],[c_0_81]) ).
cnf(c_0_94,plain,
( in(esk45_2(X1,X2),X1)
| in(esk45_2(X1,X2),X2)
| X1 = X2 ),
inference(split_conjunct,[status(thm)],[c_0_82]) ).
cnf(c_0_95,plain,
( in(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,esk19_3(X2,relation_dom(X2),X1))),X2)
| ~ relation(X2)
| ~ in(X1,relation_dom(X2)) ),
inference(er,[status(thm)],[inference(rw,[status(thm)],[c_0_83,c_0_84])]) ).
cnf(c_0_96,negated_conjecture,
( relation_dom(esk48_0) = relation_field(esk48_0)
| relation_rng(esk48_0) != empty_set ),
inference(spm,[status(thm)],[c_0_42,c_0_85]) ).
cnf(c_0_97,negated_conjecture,
~ in(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,X2)),esk48_0),
inference(spm,[status(thm)],[c_0_86,c_0_84]) ).
cnf(c_0_98,plain,
( in(esk12_4(X1,X2,X3,X4),X1)
| ~ in(X4,X3)
| X3 != cartesian_product2(X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_87]) ).
cnf(c_0_99,plain,
( ~ in(X1,X2)
| ~ in(X2,X1) ),
inference(split_conjunct,[status(thm)],[c_0_88]) ).
cnf(c_0_100,plain,
in(X1,esk49_1(X1)),
inference(split_conjunct,[status(thm)],[c_0_89]) ).
cnf(c_0_101,plain,
( in(X1,X3)
| ~ in(X1,X2)
| X3 != set_union2(X4,X2) ),
inference(split_conjunct,[status(thm)],[c_0_90]) ).
fof(c_0_102,lemma,
! [X1,X2] :
( set_difference(X1,singleton(X2)) = X1
<=> ~ in(X2,X1) ),
inference(fof_simplification,[status(thm)],[t65_zfmisc_1]) ).
fof(c_0_103,lemma,
! [X658] :
( ~ relation(X658)
| subset(X658,cartesian_product2(relation_dom(X658),relation_rng(X658))) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t21_relat_1])]) ).
cnf(c_0_104,lemma,
( ~ disjoint(relation_dom(esk48_0),relation_field(esk48_0))
| ~ in(X1,relation_dom(esk48_0)) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_91,c_0_92]),c_0_93]) ).
cnf(c_0_105,plain,
( empty_set = X1
| in(esk45_2(empty_set,X1),X1) ),
inference(spm,[status(thm)],[c_0_54,c_0_94]) ).
cnf(c_0_106,negated_conjecture,
( relation_rng(esk48_0) != empty_set
| ~ in(X1,relation_field(esk48_0)) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_95,c_0_96]),c_0_36])]),c_0_97]) ).
cnf(c_0_107,lemma,
( in(esk46_2(X1,X2),X2)
| disjoint(X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_44]) ).
cnf(c_0_108,plain,
( in(esk12_4(X1,X2,cartesian_product2(X1,X2),X3),X1)
| ~ in(X3,cartesian_product2(X1,X2)) ),
inference(er,[status(thm)],[c_0_98]) ).
cnf(c_0_109,plain,
~ in(esk49_1(X1),X1),
inference(spm,[status(thm)],[c_0_99,c_0_100]) ).
cnf(c_0_110,plain,
( in(X1,set_union2(X2,X3))
| ~ in(X1,X3) ),
inference(er,[status(thm)],[c_0_101]) ).
fof(c_0_111,lemma,
! [X759,X760] :
( ( set_difference(X759,singleton(X760)) != X759
| ~ in(X760,X759) )
& ( in(X760,X759)
| set_difference(X759,singleton(X760)) = X759 ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_102])]) ).
cnf(c_0_112,lemma,
( subset(X1,cartesian_product2(relation_dom(X1),relation_rng(X1)))
| ~ relation(X1) ),
inference(split_conjunct,[status(thm)],[c_0_103]) ).
cnf(c_0_113,lemma,
( relation_dom(esk48_0) = empty_set
| ~ disjoint(relation_dom(esk48_0),relation_field(esk48_0)) ),
inference(spm,[status(thm)],[c_0_104,c_0_105]) ).
cnf(c_0_114,lemma,
( disjoint(X1,relation_field(esk48_0))
| relation_rng(esk48_0) != empty_set ),
inference(spm,[status(thm)],[c_0_106,c_0_107]) ).
cnf(c_0_115,plain,
~ in(X1,cartesian_product2(empty_set,X2)),
inference(spm,[status(thm)],[c_0_54,c_0_108]) ).
fof(c_0_116,plain,
! [X491,X492,X493,X495,X496,X497,X499] :
( ( ~ in(X493,X492)
| in(ordered_pair(esk26_3(X491,X492,X493),X493),X491)
| X492 != relation_rng(X491)
| ~ relation(X491) )
& ( ~ in(ordered_pair(X496,X495),X491)
| in(X495,X492)
| X492 != relation_rng(X491)
| ~ relation(X491) )
& ( ~ in(esk27_2(X491,X497),X497)
| ~ in(ordered_pair(X499,esk27_2(X491,X497)),X491)
| X497 = relation_rng(X491)
| ~ relation(X491) )
& ( in(esk27_2(X491,X497),X497)
| in(ordered_pair(esk28_2(X491,X497),esk27_2(X491,X497)),X491)
| X497 = relation_rng(X491)
| ~ relation(X491) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[d5_relat_1])])])])])]) ).
cnf(c_0_117,plain,
( in(X1,X2)
| ~ in(X1,X3)
| X3 != set_difference(X2,X4) ),
inference(split_conjunct,[status(thm)],[c_0_39]) ).
cnf(c_0_118,plain,
~ in(esk49_1(set_union2(X1,X2)),X2),
inference(spm,[status(thm)],[c_0_109,c_0_110]) ).
cnf(c_0_119,lemma,
set_union2(relation_field(esk48_0),relation_rng(esk48_0)) = relation_field(esk48_0),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_73,c_0_48]),c_0_31]) ).
cnf(c_0_120,lemma,
( in(X1,X2)
| set_difference(X2,singleton(X1)) = X2 ),
inference(split_conjunct,[status(thm)],[c_0_111]) ).
cnf(c_0_121,negated_conjecture,
subset(esk48_0,cartesian_product2(relation_dom(esk48_0),relation_rng(esk48_0))),
inference(spm,[status(thm)],[c_0_112,c_0_36]) ).
cnf(c_0_122,lemma,
( relation_dom(esk48_0) = empty_set
| relation_rng(esk48_0) != empty_set ),
inference(spm,[status(thm)],[c_0_113,c_0_114]) ).
cnf(c_0_123,plain,
cartesian_product2(empty_set,X1) = empty_set,
inference(spm,[status(thm)],[c_0_115,c_0_105]) ).
fof(c_0_124,plain,
! [X649] : set_union2(X649,empty_set) = X649,
inference(variable_rename,[status(thm)],[t1_boole]) ).
cnf(c_0_125,plain,
( in(ordered_pair(esk26_3(X3,X2,X1),X1),X3)
| ~ in(X1,X2)
| X2 != relation_rng(X3)
| ~ relation(X3) ),
inference(split_conjunct,[status(thm)],[c_0_116]) ).
cnf(c_0_126,plain,
( in(X1,X2)
| ~ in(X1,set_difference(X2,X3)) ),
inference(er,[status(thm)],[c_0_117]) ).
cnf(c_0_127,plain,
( in(esk8_1(X1),X1)
| X1 = empty_set ),
inference(split_conjunct,[status(thm)],[c_0_43]) ).
cnf(c_0_128,lemma,
~ in(esk49_1(relation_field(esk48_0)),relation_rng(esk48_0)),
inference(spm,[status(thm)],[c_0_118,c_0_119]) ).
cnf(c_0_129,lemma,
( set_difference(X2,unordered_pair(X1,X1)) = X2
| in(X1,X2) ),
inference(rw,[status(thm)],[c_0_120,c_0_63]) ).
cnf(c_0_130,lemma,
( subset(esk48_0,empty_set)
| relation_rng(esk48_0) != empty_set ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_121,c_0_122]),c_0_123]) ).
cnf(c_0_131,plain,
set_union2(X1,empty_set) = X1,
inference(split_conjunct,[status(thm)],[c_0_124]) ).
cnf(c_0_132,negated_conjecture,
esk48_0 != empty_set,
inference(split_conjunct,[status(thm)],[c_0_32]) ).
cnf(c_0_133,plain,
( in(unordered_pair(unordered_pair(esk26_3(X3,X2,X1),X1),unordered_pair(esk26_3(X3,X2,X1),esk26_3(X3,X2,X1))),X3)
| X2 != relation_rng(X3)
| ~ relation(X3)
| ~ in(X1,X2) ),
inference(rw,[status(thm)],[c_0_125,c_0_71]) ).
cnf(c_0_134,plain,
( set_difference(X1,X2) = empty_set
| in(esk8_1(set_difference(X1,X2)),X1) ),
inference(spm,[status(thm)],[c_0_126,c_0_127]) ).
cnf(c_0_135,lemma,
set_difference(relation_rng(esk48_0),unordered_pair(esk49_1(relation_field(esk48_0)),esk49_1(relation_field(esk48_0)))) = relation_rng(esk48_0),
inference(spm,[status(thm)],[c_0_128,c_0_129]) ).
cnf(c_0_136,lemma,
relation_rng(esk48_0) != empty_set,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_73,c_0_130]),c_0_131]),c_0_132]) ).
cnf(c_0_137,plain,
( in(unordered_pair(unordered_pair(X1,esk26_3(X2,relation_rng(X2),X1)),unordered_pair(esk26_3(X2,relation_rng(X2),X1),esk26_3(X2,relation_rng(X2),X1))),X2)
| ~ relation(X2)
| ~ in(X1,relation_rng(X2)) ),
inference(er,[status(thm)],[inference(rw,[status(thm)],[c_0_133,c_0_84])]) ).
cnf(c_0_138,lemma,
in(esk8_1(relation_rng(esk48_0)),relation_rng(esk48_0)),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_134,c_0_135]),c_0_136]) ).
cnf(c_0_139,negated_conjecture,
~ in(unordered_pair(unordered_pair(X1,X2),unordered_pair(X2,X2)),esk48_0),
inference(spm,[status(thm)],[c_0_86,c_0_84]) ).
cnf(c_0_140,lemma,
$false,
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_137,c_0_138]),c_0_36])]),c_0_139]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SEU186+2 : TPTP v9.2.1. Released v3.3.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.15/0.33 % Computer : n020.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % WCLimit : 300
% 0.15/0.33 % DateTime : Tue May 5 02:47:20 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.34 % start to proof: theBenchmark
% 4.35/3.33 % Version : CSE_E---1.7
% 4.35/3.33 % Problem : theBenchmark.p
% 4.35/3.33 % SZS status Theorem for theBenchmark.p
% 4.35/3.33 % SZS output start CNFRefutation
% See solution above
% 4.35/3.35 % Total time : 2.427s
%------------------------------------------------------------------------------