%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SEU291+1 : 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 : n028.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:11:22 PM UTC 2026
% Result : Theorem 1.72s 1.85s
% Output : CNFRefutation 1.72s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 17
% Syntax : Number of formulae : 95 ( 15 unt; 0 def)
% Number of atoms : 270 ( 63 equ)
% Maximal formula atoms : 26 ( 2 avg)
% Number of connectives : 290 ( 115 ~; 120 |; 31 &)
% ( 4 <=>; 20 =>; 0 <=; 0 <~>)
% Maximal formula depth : 14 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 12 ( 10 usr; 1 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 5 con; 0-3 aty)
% Number of variables : 164 ( 11 sgn 77 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(redefinition_k4_relset_1,axiom,
! [X1,X2,X3] :
( relation_of2(X3,X1,X2)
=> relation_dom_as_subset(X1,X2,X3) = relation_dom(X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_k4_relset_1) ).
fof(d1_funct_2,axiom,
! [X1,X2,X3] :
( relation_of2_as_subset(X3,X1,X2)
=> ( ( ( X2 = empty_set
=> X1 = empty_set )
=> ( quasi_total(X3,X1,X2)
<=> X1 = relation_dom_as_subset(X1,X2,X3) ) )
& ( X2 = empty_set
=> ( X1 = empty_set
| ( quasi_total(X3,X1,X2)
<=> X3 = empty_set ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_funct_2) ).
fof(redefinition_m2_relset_1,axiom,
! [X1,X2,X3] :
( relation_of2_as_subset(X3,X1,X2)
<=> relation_of2(X3,X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(dt_k4_relset_1,axiom,
! [X1,X2,X3] :
( relation_of2(X3,X1,X2)
=> element(relation_dom_as_subset(X1,X2,X3),powerset(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k4_relset_1) ).
fof(t9_funct_2,conjecture,
! [X1,X2,X3,X4] :
( ( function(X4)
& quasi_total(X4,X1,X2)
& relation_of2_as_subset(X4,X1,X2) )
=> ( subset(X2,X3)
=> ( ( X2 = empty_set
& X1 != empty_set )
| ( function(X4)
& quasi_total(X4,X1,X3)
& relation_of2_as_subset(X4,X1,X3) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t9_funct_2) ).
fof(fc5_relat_1,axiom,
! [X1] :
( ( ~ empty(X1)
& relation(X1) )
=> ~ empty(relation_dom(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc5_relat_1) ).
fof(t3_subset,axiom,
! [X1,X2] :
( element(X1,powerset(X2))
<=> subset(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t3_subset) ).
fof(t3_xboole_1,axiom,
! [X1] :
( subset(X1,empty_set)
=> X1 = empty_set ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t3_xboole_1) ).
fof(t5_subset,axiom,
! [X1,X2,X3] :
~ ( in(X1,X2)
& element(X2,powerset(X3))
& empty(X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t5_subset) ).
fof(t16_relset_1,axiom,
! [X1,X2,X3,X4] :
( relation_of2_as_subset(X4,X3,X1)
=> ( subset(X1,X2)
=> relation_of2_as_subset(X4,X3,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t16_relset_1) ).
fof(t6_boole,axiom,
! [X1] :
( empty(X1)
=> X1 = empty_set ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t6_boole) ).
fof(fc7_relat_1,axiom,
! [X1] :
( empty(X1)
=> ( empty(relation_dom(X1))
& relation(relation_dom(X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc7_relat_1) ).
fof(cc1_relset_1,axiom,
! [X1,X2,X3] :
( element(X3,powerset(cartesian_product2(X1,X2)))
=> relation(X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cc1_relset_1) ).
fof(dt_m2_relset_1,axiom,
! [X1,X2,X3] :
( relation_of2_as_subset(X3,X1,X2)
=> element(X3,powerset(cartesian_product2(X1,X2))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_m2_relset_1) ).
fof(t2_subset,axiom,
! [X1,X2] :
( element(X1,X2)
=> ( empty(X2)
| in(X1,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2_subset) ).
fof(fc12_relat_1,axiom,
( empty(empty_set)
& relation(empty_set)
& relation_empty_yielding(empty_set) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc12_relat_1) ).
fof(existence_m1_subset_1,axiom,
! [X1] :
? [X2] : element(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_m1_subset_1) ).
fof(c_0_17,plain,
! [X139,X140,X141] :
( ~ relation_of2(X141,X139,X140)
| relation_dom_as_subset(X139,X140,X141) = relation_dom(X141) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[redefinition_k4_relset_1])]) ).
fof(c_0_18,plain,
! [X97,X98,X99] :
( ( ~ quasi_total(X99,X97,X98)
| X97 = relation_dom_as_subset(X97,X98,X99)
| X98 = empty_set
| ~ relation_of2_as_subset(X99,X97,X98) )
& ( X97 != relation_dom_as_subset(X97,X98,X99)
| quasi_total(X99,X97,X98)
| X98 = empty_set
| ~ relation_of2_as_subset(X99,X97,X98) )
& ( ~ quasi_total(X99,X97,X98)
| X97 = relation_dom_as_subset(X97,X98,X99)
| X97 != empty_set
| ~ relation_of2_as_subset(X99,X97,X98) )
& ( X97 != relation_dom_as_subset(X97,X98,X99)
| quasi_total(X99,X97,X98)
| X97 != empty_set
| ~ relation_of2_as_subset(X99,X97,X98) )
& ( ~ quasi_total(X99,X97,X98)
| X99 = empty_set
| X97 = empty_set
| X98 != empty_set
| ~ relation_of2_as_subset(X99,X97,X98) )
& ( X99 != empty_set
| quasi_total(X99,X97,X98)
| X97 = empty_set
| X98 != empty_set
| ~ relation_of2_as_subset(X99,X97,X98) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[d1_funct_2])])]) ).
fof(c_0_19,plain,
! [X142,X143,X144] :
( ( ~ relation_of2_as_subset(X144,X142,X143)
| relation_of2(X144,X142,X143) )
& ( ~ relation_of2(X144,X142,X143)
| relation_of2_as_subset(X144,X142,X143) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[redefinition_m2_relset_1])]) ).
fof(c_0_20,plain,
! [X100,X101,X102] :
( ~ relation_of2(X102,X100,X101)
| element(relation_dom_as_subset(X100,X101,X102),powerset(X100)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[dt_k4_relset_1])]) ).
cnf(c_0_21,plain,
( relation_dom_as_subset(X2,X3,X1) = relation_dom(X1)
| ~ relation_of2(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[c_0_17]) ).
cnf(c_0_22,plain,
( X2 = relation_dom_as_subset(X2,X3,X1)
| X3 = empty_set
| ~ quasi_total(X1,X2,X3)
| ~ relation_of2_as_subset(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[c_0_18]) ).
cnf(c_0_23,plain,
( relation_of2_as_subset(X1,X2,X3)
| ~ relation_of2(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[c_0_19]) ).
fof(c_0_24,negated_conjecture,
~ ! [X1,X2,X3,X4] :
( ( function(X4)
& quasi_total(X4,X1,X2)
& relation_of2_as_subset(X4,X1,X2) )
=> ( subset(X2,X3)
=> ( ( X2 = empty_set
& X1 != empty_set )
| ( function(X4)
& quasi_total(X4,X1,X3)
& relation_of2_as_subset(X4,X1,X3) ) ) ) ),
inference(assume_negation,[status(cth)],[t9_funct_2]) ).
cnf(c_0_25,plain,
( element(relation_dom_as_subset(X2,X3,X1),powerset(X2))
| ~ relation_of2(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[c_0_20]) ).
cnf(c_0_26,plain,
( quasi_total(X3,X1,X2)
| X2 = empty_set
| X1 != relation_dom_as_subset(X1,X2,X3)
| ~ relation_of2_as_subset(X3,X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_18]) ).
cnf(c_0_27,plain,
( X1 = relation_dom(X2)
| X3 = empty_set
| ~ relation_of2(X2,X1,X3)
| ~ quasi_total(X2,X1,X3) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_21,c_0_22]),c_0_23]) ).
cnf(c_0_28,plain,
( relation_of2(X1,X2,X3)
| ~ relation_of2_as_subset(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[c_0_19]) ).
fof(c_0_29,negated_conjecture,
( function(esk21_0)
& quasi_total(esk21_0,esk18_0,esk19_0)
& relation_of2_as_subset(esk21_0,esk18_0,esk19_0)
& subset(esk19_0,esk20_0)
& ( esk19_0 != empty_set
| esk18_0 = empty_set )
& ( ~ function(esk21_0)
| ~ quasi_total(esk21_0,esk18_0,esk20_0)
| ~ relation_of2_as_subset(esk21_0,esk18_0,esk20_0) ) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_24])])]) ).
fof(c_0_30,plain,
! [X1] :
( ( ~ empty(X1)
& relation(X1) )
=> ~ empty(relation_dom(X1)) ),
inference(fof_simplification,[status(thm)],[fc5_relat_1]) ).
fof(c_0_31,plain,
! [X154,X155] :
( ( ~ element(X154,powerset(X155))
| subset(X154,X155) )
& ( ~ subset(X154,X155)
| element(X154,powerset(X155)) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t3_subset])]) ).
cnf(c_0_32,plain,
( element(relation_dom(X1),powerset(X2))
| ~ relation_of2(X1,X2,X3) ),
inference(spm,[status(thm)],[c_0_25,c_0_21]) ).
cnf(c_0_33,plain,
( X1 = empty_set
| quasi_total(X2,relation_dom(X2),X1)
| ~ relation_of2(X2,relation_dom(X2),X1) ),
inference(csr,[status(thm)],[inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_26,c_0_21])]),c_0_23]) ).
cnf(c_0_34,plain,
( X1 = relation_dom(X2)
| X3 = empty_set
| ~ quasi_total(X2,X1,X3)
| ~ relation_of2_as_subset(X2,X1,X3) ),
inference(spm,[status(thm)],[c_0_27,c_0_28]) ).
cnf(c_0_35,negated_conjecture,
quasi_total(esk21_0,esk18_0,esk19_0),
inference(split_conjunct,[status(thm)],[c_0_29]) ).
cnf(c_0_36,negated_conjecture,
relation_of2_as_subset(esk21_0,esk18_0,esk19_0),
inference(split_conjunct,[status(thm)],[c_0_29]) ).
fof(c_0_37,plain,
! [X117] :
( empty(X117)
| ~ relation(X117)
| ~ empty(relation_dom(X117)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_30])]) ).
fof(c_0_38,plain,
! [X156] :
( ~ subset(X156,empty_set)
| X156 = empty_set ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t3_xboole_1])]) ).
cnf(c_0_39,plain,
( subset(X1,X2)
| ~ element(X1,powerset(X2)) ),
inference(split_conjunct,[status(thm)],[c_0_31]) ).
fof(c_0_40,plain,
! [X160,X161,X162] :
( ~ in(X160,X161)
| ~ element(X161,powerset(X162))
| ~ empty(X162) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t5_subset])]) ).
cnf(c_0_41,plain,
( element(relation_dom(X1),powerset(X2))
| ~ relation_of2_as_subset(X1,X2,X3) ),
inference(spm,[status(thm)],[c_0_32,c_0_28]) ).
cnf(c_0_42,negated_conjecture,
( ~ function(esk21_0)
| ~ quasi_total(esk21_0,esk18_0,esk20_0)
| ~ relation_of2_as_subset(esk21_0,esk18_0,esk20_0) ),
inference(split_conjunct,[status(thm)],[c_0_29]) ).
cnf(c_0_43,negated_conjecture,
function(esk21_0),
inference(split_conjunct,[status(thm)],[c_0_29]) ).
cnf(c_0_44,plain,
( X1 = empty_set
| quasi_total(X2,relation_dom(X2),X1)
| ~ relation_of2_as_subset(X2,relation_dom(X2),X1) ),
inference(spm,[status(thm)],[c_0_33,c_0_28]) ).
cnf(c_0_45,negated_conjecture,
( relation_dom(esk21_0) = esk18_0
| esk19_0 = empty_set ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_34,c_0_35]),c_0_36])]) ).
fof(c_0_46,plain,
! [X146,X147,X148,X149] :
( ~ relation_of2_as_subset(X149,X148,X146)
| ~ subset(X146,X147)
| relation_of2_as_subset(X149,X148,X147) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t16_relset_1])]) ).
fof(c_0_47,plain,
! [X163] :
( ~ empty(X163)
| X163 = empty_set ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t6_boole])]) ).
fof(c_0_48,plain,
! [X118] :
( ( empty(relation_dom(X118))
| ~ empty(X118) )
& ( relation(relation_dom(X118))
| ~ empty(X118) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[fc7_relat_1])])]) ).
cnf(c_0_49,plain,
( empty(X1)
| ~ relation(X1)
| ~ empty(relation_dom(X1)) ),
inference(split_conjunct,[status(thm)],[c_0_37]) ).
cnf(c_0_50,plain,
( X1 = empty_set
| ~ subset(X1,empty_set) ),
inference(split_conjunct,[status(thm)],[c_0_38]) ).
cnf(c_0_51,plain,
( subset(relation_dom_as_subset(X1,X2,X3),X1)
| ~ relation_of2(X3,X1,X2) ),
inference(spm,[status(thm)],[c_0_39,c_0_25]) ).
fof(c_0_52,plain,
! [X93,X94,X95] :
( ~ element(X95,powerset(cartesian_product2(X93,X94)))
| relation(X95) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[cc1_relset_1])]) ).
fof(c_0_53,plain,
! [X103,X104,X105] :
( ~ relation_of2_as_subset(X105,X103,X104)
| element(X105,powerset(cartesian_product2(X103,X104))) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[dt_m2_relset_1])]) ).
cnf(c_0_54,plain,
( quasi_total(X3,X1,X2)
| X1 != relation_dom_as_subset(X1,X2,X3)
| X1 != empty_set
| ~ relation_of2_as_subset(X3,X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_18]) ).
cnf(c_0_55,plain,
( ~ in(X1,X2)
| ~ element(X2,powerset(X3))
| ~ empty(X3) ),
inference(split_conjunct,[status(thm)],[c_0_40]) ).
cnf(c_0_56,negated_conjecture,
element(relation_dom(esk21_0),powerset(esk18_0)),
inference(spm,[status(thm)],[c_0_41,c_0_36]) ).
fof(c_0_57,plain,
! [X152,X153] :
( ~ element(X152,X153)
| empty(X153)
| in(X152,X153) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t2_subset])]) ).
cnf(c_0_58,negated_conjecture,
( ~ quasi_total(esk21_0,esk18_0,esk20_0)
| ~ relation_of2_as_subset(esk21_0,esk18_0,esk20_0) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_42,c_0_43])]) ).
cnf(c_0_59,negated_conjecture,
( esk19_0 = empty_set
| X1 = empty_set
| quasi_total(esk21_0,esk18_0,X1)
| ~ relation_of2_as_subset(esk21_0,esk18_0,X1) ),
inference(spm,[status(thm)],[c_0_44,c_0_45]) ).
cnf(c_0_60,plain,
( relation_of2_as_subset(X1,X2,X4)
| ~ relation_of2_as_subset(X1,X2,X3)
| ~ subset(X3,X4) ),
inference(split_conjunct,[status(thm)],[c_0_46]) ).
cnf(c_0_61,plain,
( X1 = empty_set
| ~ empty(X1) ),
inference(split_conjunct,[status(thm)],[c_0_47]) ).
cnf(c_0_62,plain,
( empty(relation_dom(X1))
| ~ empty(X1) ),
inference(split_conjunct,[status(thm)],[c_0_48]) ).
cnf(c_0_63,plain,
( empty(X1)
| ~ relation_of2(X1,X2,X3)
| ~ relation(X1)
| ~ empty(relation_dom_as_subset(X2,X3,X1)) ),
inference(spm,[status(thm)],[c_0_49,c_0_21]) ).
cnf(c_0_64,plain,
( relation_dom_as_subset(empty_set,X1,X2) = empty_set
| ~ relation_of2(X2,empty_set,X1) ),
inference(spm,[status(thm)],[c_0_50,c_0_51]) ).
cnf(c_0_65,plain,
empty(empty_set),
inference(split_conjunct,[status(thm)],[fc12_relat_1]) ).
cnf(c_0_66,plain,
( relation(X1)
| ~ element(X1,powerset(cartesian_product2(X2,X3))) ),
inference(split_conjunct,[status(thm)],[c_0_52]) ).
cnf(c_0_67,plain,
( element(X1,powerset(cartesian_product2(X2,X3)))
| ~ relation_of2_as_subset(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[c_0_53]) ).
cnf(c_0_68,plain,
( quasi_total(X1,empty_set,X2)
| relation_dom_as_subset(empty_set,X2,X1) != empty_set
| ~ relation_of2_as_subset(X1,empty_set,X2) ),
inference(er,[status(thm)],[c_0_54]) ).
cnf(c_0_69,negated_conjecture,
( ~ empty(esk18_0)
| ~ in(X1,relation_dom(esk21_0)) ),
inference(spm,[status(thm)],[c_0_55,c_0_56]) ).
cnf(c_0_70,plain,
( empty(X2)
| in(X1,X2)
| ~ element(X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_57]) ).
fof(c_0_71,plain,
! [X109] : element(esk2_1(X109),X109),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[existence_m1_subset_1])]) ).
cnf(c_0_72,negated_conjecture,
( esk20_0 = empty_set
| esk19_0 = empty_set
| ~ relation_of2_as_subset(esk21_0,esk18_0,esk20_0) ),
inference(spm,[status(thm)],[c_0_58,c_0_59]) ).
cnf(c_0_73,negated_conjecture,
( relation_of2_as_subset(esk21_0,esk18_0,X1)
| ~ subset(esk19_0,X1) ),
inference(spm,[status(thm)],[c_0_60,c_0_36]) ).
cnf(c_0_74,negated_conjecture,
subset(esk19_0,esk20_0),
inference(split_conjunct,[status(thm)],[c_0_29]) ).
cnf(c_0_75,plain,
( relation_dom(X1) = empty_set
| ~ empty(X1) ),
inference(spm,[status(thm)],[c_0_61,c_0_62]) ).
cnf(c_0_76,negated_conjecture,
( esk18_0 = empty_set
| esk19_0 != empty_set ),
inference(split_conjunct,[status(thm)],[c_0_29]) ).
cnf(c_0_77,plain,
( empty(X1)
| ~ relation_of2(X1,empty_set,X2)
| ~ relation(X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_63,c_0_64]),c_0_65])]) ).
cnf(c_0_78,plain,
( relation(X1)
| ~ relation_of2_as_subset(X1,X2,X3) ),
inference(spm,[status(thm)],[c_0_66,c_0_67]) ).
cnf(c_0_79,plain,
( quasi_total(X1,empty_set,X2)
| ~ relation_of2(X1,empty_set,X2) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_68,c_0_64]),c_0_23]) ).
cnf(c_0_80,negated_conjecture,
( empty(relation_dom(esk21_0))
| ~ element(X1,relation_dom(esk21_0))
| ~ empty(esk18_0) ),
inference(spm,[status(thm)],[c_0_69,c_0_70]) ).
cnf(c_0_81,plain,
element(esk2_1(X1),X1),
inference(split_conjunct,[status(thm)],[c_0_71]) ).
cnf(c_0_82,negated_conjecture,
( esk19_0 = empty_set
| esk20_0 = empty_set ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_72,c_0_73]),c_0_74])]) ).
cnf(c_0_83,negated_conjecture,
( esk18_0 = empty_set
| ~ empty(esk21_0) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_75,c_0_45]),c_0_76]) ).
cnf(c_0_84,plain,
( empty(X1)
| ~ relation_of2_as_subset(X1,empty_set,X2) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_77,c_0_28]),c_0_78]) ).
cnf(c_0_85,plain,
( quasi_total(X1,empty_set,X2)
| ~ relation_of2_as_subset(X1,empty_set,X2) ),
inference(spm,[status(thm)],[c_0_79,c_0_28]) ).
cnf(c_0_86,negated_conjecture,
( empty(relation_dom(esk21_0))
| ~ empty(esk18_0) ),
inference(spm,[status(thm)],[c_0_80,c_0_81]) ).
cnf(c_0_87,negated_conjecture,
relation(esk21_0),
inference(spm,[status(thm)],[c_0_78,c_0_36]) ).
cnf(c_0_88,negated_conjecture,
esk19_0 = empty_set,
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_74,c_0_82]),c_0_50]) ).
cnf(c_0_89,negated_conjecture,
( relation_of2_as_subset(esk21_0,empty_set,X1)
| ~ subset(esk19_0,X1)
| ~ empty(esk21_0) ),
inference(spm,[status(thm)],[c_0_73,c_0_83]) ).
cnf(c_0_90,negated_conjecture,
~ relation_of2_as_subset(esk21_0,empty_set,esk20_0),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_58,c_0_83]),c_0_84]),c_0_85]) ).
cnf(c_0_91,negated_conjecture,
( empty(esk21_0)
| ~ empty(esk18_0) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_49,c_0_86]),c_0_87])]) ).
cnf(c_0_92,negated_conjecture,
esk18_0 = empty_set,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_76,c_0_88])]) ).
cnf(c_0_93,negated_conjecture,
~ empty(esk21_0),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_89,c_0_74]),c_0_90]) ).
cnf(c_0_94,negated_conjecture,
$false,
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_91,c_0_92]),c_0_65])]),c_0_93]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SEU291+1 : 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.16/0.33 % Computer : n028.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:55:46 EDT 2026
% 0.16/0.33 % CPUTime :
% 0.16/0.34 % start to proof: theBenchmark
% 1.72/1.85 % Version : CSE_E---1.7
% 1.72/1.85 % Problem : theBenchmark.p
% 1.72/1.85 % SZS status Theorem for theBenchmark.p
% 1.72/1.85 % SZS output start CNFRefutation
% See solution above
% 1.72/1.85 % Total time : 1.369s
%------------------------------------------------------------------------------