%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SEU141+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 : n017.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:45 PM UTC 2026
% Result : Theorem 212.10s 135.43s
% Output : CNFRefutation 213.60s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named i_0_196)
% Comments :
%------------------------------------------------------------------------------
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(t4_xboole_0,axiom,
! [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(antisymmetry_r2_hidden,axiom,
! [X1,X2] :
( in(X1,X2)
=> ~ in(X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',antisymmetry_r2_hidden) ).
fof(t83_xboole_1,conjecture,
! [X1,X2] :
( disjoint(X1,X2)
<=> set_difference(X1,X2) = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t83_xboole_1) ).
fof(rc2_xboole_0,axiom,
? [X1] : ~ empty(X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc2_xboole_0) ).
fof(d3_xboole_0,axiom,
! [X1,X2,X3] :
( X3 = set_intersection2(X1,X2)
<=> ! [X4] :
( in(X4,X3)
<=> ( in(X4,X1)
& in(X4,X2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d3_xboole_0) ).
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(d10_xboole_0,axiom,
! [X1,X2] :
( X1 = X2
<=> ( subset(X1,X2)
& subset(X2,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d10_xboole_0) ).
fof(symmetry_r1_xboole_0,axiom,
! [X1,X2] :
( disjoint(X1,X2)
=> disjoint(X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',symmetry_r1_xboole_0) ).
fof(d7_xboole_0,axiom,
! [X1,X2] :
( disjoint(X1,X2)
<=> set_intersection2(X1,X2) = empty_set ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d7_xboole_0) ).
fof(t7_boole,axiom,
! [X1,X2] :
~ ( in(X1,X2)
& empty(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t7_boole) ).
fof(commutativity_k3_xboole_0,axiom,
! [X1,X2] : set_intersection2(X1,X2) = set_intersection2(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_k3_xboole_0) ).
fof(t8_boole,axiom,
! [X1,X2] :
~ ( empty(X1)
& X1 != X2
& empty(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t8_boole) ).
fof(idempotence_k3_xboole_0,axiom,
! [X1,X2] : set_intersection2(X1,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',idempotence_k3_xboole_0) ).
fof(reflexivity_r1_tarski,axiom,
! [X1,X2] : subset(X1,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity_r1_tarski) ).
fof(t3_boole,axiom,
! [X1] : set_difference(X1,empty_set) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t3_boole) ).
fof(t4_boole,axiom,
! [X1] : set_difference(empty_set,X1) = empty_set,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t4_boole) ).
fof(t2_boole,axiom,
! [X1] : set_intersection2(X1,empty_set) = empty_set,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2_boole) ).
fof(t6_boole,axiom,
! [X1] :
( empty(X1)
=> X1 = empty_set ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t6_boole) ).
fof(rc1_xboole_0,axiom,
? [X1] : empty(X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rc1_xboole_0) ).
fof(fc1_xboole_0,axiom,
empty(empty_set),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_xboole_0) ).
fof(i_0_21,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(i_0_22,plain,
! [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(i_0_23,plain,
! [X1,X2] :
( in(X1,X2)
=> ~ in(X2,X1) ),
inference(fof_simplification,[status(thm)],[antisymmetry_r2_hidden]) ).
fof(i_0_24,negated_conjecture,
~ ! [X1,X2] :
( disjoint(X1,X2)
<=> set_difference(X1,X2) = X1 ),
inference(assume_negation,[status(cth)],[t83_xboole_1]) ).
fof(i_0_25,plain,
? [X1] : ~ empty(X1),
inference(fof_simplification,[status(thm)],[rc2_xboole_0]) ).
fof(i_0_26,plain,
! [X58,X59,X60,X61,X62,X63,X64,X65] :
( ( in(X61,X58)
| ~ in(X61,X60)
| X60 != set_intersection2(X58,X59) )
& ( in(X61,X59)
| ~ in(X61,X60)
| X60 != set_intersection2(X58,X59) )
& ( ~ in(X62,X58)
| ~ in(X62,X59)
| in(X62,X60)
| X60 != set_intersection2(X58,X59) )
& ( ~ in(esk2_3(X63,X64,X65),X65)
| ~ in(esk2_3(X63,X64,X65),X63)
| ~ in(esk2_3(X63,X64,X65),X64)
| X65 = set_intersection2(X63,X64) )
& ( in(esk2_3(X63,X64,X65),X63)
| in(esk2_3(X63,X64,X65),X65)
| X65 = set_intersection2(X63,X64) )
& ( in(esk2_3(X63,X64,X65),X64)
| in(esk2_3(X63,X64,X65),X65)
| X65 = set_intersection2(X63,X64) ) ),
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_xboole_0])])])])])]) ).
fof(i_0_27,plain,
! [X67,X68,X69,X70,X71,X72,X73,X74] :
( ( in(X70,X67)
| ~ in(X70,X69)
| X69 != set_difference(X67,X68) )
& ( ~ in(X70,X68)
| ~ in(X70,X69)
| X69 != set_difference(X67,X68) )
& ( ~ in(X71,X67)
| in(X71,X68)
| in(X71,X69)
| X69 != set_difference(X67,X68) )
& ( ~ in(esk3_3(X72,X73,X74),X74)
| ~ in(esk3_3(X72,X73,X74),X72)
| in(esk3_3(X72,X73,X74),X73)
| X74 = set_difference(X72,X73) )
& ( in(esk3_3(X72,X73,X74),X72)
| in(esk3_3(X72,X73,X74),X74)
| X74 = set_difference(X72,X73) )
& ( ~ in(esk3_3(X72,X73,X74),X73)
| in(esk3_3(X72,X73,X74),X74)
| X74 = set_difference(X72,X73) ) ),
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)],[i_0_21])])])])])]) ).
fof(i_0_28,plain,
! [X87,X88,X90,X91,X92] :
( ( disjoint(X87,X88)
| in(esk6_2(X87,X88),set_intersection2(X87,X88)) )
& ( ~ in(X92,set_intersection2(X90,X91))
| ~ disjoint(X90,X91) ) ),
inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_22])])])])]) ).
fof(i_0_29,plain,
! [X52,X53,X54,X55,X56] :
( ( ~ subset(X52,X53)
| ~ in(X54,X52)
| in(X54,X53) )
& ( in(esk1_2(X55,X56),X55)
| subset(X55,X56) )
& ( ~ in(esk1_2(X55,X56),X56)
| subset(X55,X56) ) ),
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(i_0_30,plain,
! [X50,X51] :
( ( subset(X50,X51)
| X50 != X51 )
& ( subset(X51,X50)
| X50 != X51 )
& ( ~ subset(X50,X51)
| ~ subset(X51,X50)
| X50 = X51 ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[d10_xboole_0])])]) ).
fof(i_0_31,plain,
! [X46,X47] :
( ~ in(X46,X47)
| ~ in(X47,X46) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_23])]) ).
fof(i_0_32,plain,
! [X82,X83] :
( ~ disjoint(X82,X83)
| disjoint(X83,X82) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[symmetry_r1_xboole_0])]) ).
fof(i_0_33,plain,
! [X76,X77] :
( ( ~ disjoint(X76,X77)
| set_intersection2(X76,X77) = empty_set )
& ( set_intersection2(X76,X77) != empty_set
| disjoint(X76,X77) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[d7_xboole_0])]) ).
fof(i_0_34,negated_conjecture,
( ( ~ disjoint(esk7_0,esk8_0)
| set_difference(esk7_0,esk8_0) != esk7_0 )
& ( disjoint(esk7_0,esk8_0)
| set_difference(esk7_0,esk8_0) = esk7_0 ) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_24])])]) ).
fof(i_0_35,plain,
! [X94,X95] :
( ~ in(X94,X95)
| ~ empty(X95) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t7_boole])]) ).
fof(i_0_36,plain,
! [X48,X49] : set_intersection2(X48,X49) = set_intersection2(X49,X48),
inference(variable_rename,[status(thm)],[commutativity_k3_xboole_0]) ).
fof(i_0_37,plain,
! [X98,X99] :
( ~ empty(X98)
| X98 = X99
| ~ empty(X99) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t8_boole])]) ).
fof(i_0_38,plain,
! [X78] : set_intersection2(X78,X78) = X78,
inference(variable_rename,[status(thm)],[inference(fof_simplification,[status(thm)],[idempotence_k3_xboole_0])]) ).
fof(i_0_39,plain,
! [X81] : subset(X81,X81),
inference(variable_rename,[status(thm)],[inference(fof_simplification,[status(thm)],[reflexivity_r1_tarski])]) ).
fof(i_0_40,plain,
! [X85] : set_difference(X85,empty_set) = X85,
inference(variable_rename,[status(thm)],[t3_boole]) ).
fof(i_0_41,plain,
! [X86] : set_difference(empty_set,X86) = empty_set,
inference(variable_rename,[status(thm)],[t4_boole]) ).
fof(i_0_42,plain,
! [X84] : set_intersection2(X84,empty_set) = empty_set,
inference(variable_rename,[status(thm)],[t2_boole]) ).
fof(i_0_43,plain,
! [X93] :
( ~ empty(X93)
| X93 = empty_set ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t6_boole])]) ).
fof(i_0_44,plain,
~ empty(esk5_0),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[i_0_25])]) ).
fof(i_0_45,plain,
empty(esk4_0),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[rc1_xboole_0])]) ).
cnf(i_0_46,plain,
( X3 = set_intersection2(X1,X2)
| ~ in(esk2_3(X1,X2,X3),X3)
| ~ in(esk2_3(X1,X2,X3),X1)
| ~ in(esk2_3(X1,X2,X3),X2) ),
inference(split_conjunct,[status(thm)],[i_0_26]),
[final] ).
cnf(i_0_47,plain,
( in(esk3_3(X1,X2,X3),X2)
| X3 = set_difference(X1,X2)
| ~ in(esk3_3(X1,X2,X3),X3)
| ~ in(esk3_3(X1,X2,X3),X1) ),
inference(split_conjunct,[status(thm)],[i_0_27]),
[final] ).
cnf(i_0_48,plain,
( in(esk3_3(X1,X2,X3),X3)
| X3 = set_difference(X1,X2)
| ~ in(esk3_3(X1,X2,X3),X2) ),
inference(split_conjunct,[status(thm)],[i_0_27]),
[final] ).
cnf(i_0_49,plain,
( in(esk3_3(X1,X2,X3),X1)
| in(esk3_3(X1,X2,X3),X3)
| X3 = set_difference(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_27]),
[final] ).
cnf(i_0_50,plain,
( in(esk2_3(X1,X2,X3),X1)
| in(esk2_3(X1,X2,X3),X3)
| X3 = set_intersection2(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_26]),
[final] ).
cnf(i_0_51,plain,
( in(esk2_3(X1,X2,X3),X2)
| in(esk2_3(X1,X2,X3),X3)
| X3 = set_intersection2(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_26]),
[final] ).
cnf(i_0_52,plain,
( ~ in(X1,set_intersection2(X2,X3))
| ~ disjoint(X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_28]),
[final] ).
cnf(i_0_53,plain,
( in(X1,X4)
| ~ in(X1,X2)
| ~ in(X1,X3)
| X4 != set_intersection2(X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_26]),
[final] ).
cnf(i_0_54,plain,
( disjoint(X1,X2)
| in(esk6_2(X1,X2),set_intersection2(X1,X2)) ),
inference(split_conjunct,[status(thm)],[i_0_28]),
[final] ).
cnf(i_0_55,plain,
( subset(X1,X2)
| ~ in(esk1_2(X1,X2),X2) ),
inference(split_conjunct,[status(thm)],[i_0_29]),
[final] ).
cnf(i_0_56,plain,
( in(X1,X3)
| in(X1,X4)
| ~ in(X1,X2)
| X4 != set_difference(X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_27]),
[final] ).
cnf(i_0_57,plain,
( ~ in(X1,X2)
| ~ in(X1,X3)
| X3 != set_difference(X4,X2) ),
inference(split_conjunct,[status(thm)],[i_0_27]),
[final] ).
cnf(i_0_58,plain,
( in(X1,X2)
| ~ in(X1,X3)
| X3 != set_difference(X2,X4) ),
inference(split_conjunct,[status(thm)],[i_0_27]),
[final] ).
cnf(i_0_59,plain,
( in(X1,X2)
| ~ in(X1,X3)
| X3 != set_intersection2(X2,X4) ),
inference(split_conjunct,[status(thm)],[i_0_26]),
[final] ).
cnf(i_0_60,plain,
( in(X1,X2)
| ~ in(X1,X3)
| X3 != set_intersection2(X4,X2) ),
inference(split_conjunct,[status(thm)],[i_0_26]),
[final] ).
cnf(i_0_61,plain,
( in(X3,X2)
| ~ subset(X1,X2)
| ~ in(X3,X1) ),
inference(split_conjunct,[status(thm)],[i_0_29]),
[final] ).
cnf(i_0_62,plain,
( in(esk1_2(X1,X2),X1)
| subset(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_29]),
[final] ).
cnf(i_0_63,plain,
( X1 = X2
| ~ subset(X1,X2)
| ~ subset(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_30]),
[final] ).
cnf(i_0_64,plain,
( ~ in(X1,X2)
| ~ in(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_31]),
[final] ).
cnf(i_0_65,plain,
( disjoint(X2,X1)
| ~ disjoint(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_32]),
[final] ).
cnf(i_0_66,plain,
( disjoint(X1,X2)
| set_intersection2(X1,X2) != empty_set ),
inference(split_conjunct,[status(thm)],[i_0_33]),
[final] ).
cnf(i_0_67,plain,
( set_intersection2(X1,X2) = empty_set
| ~ disjoint(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_33]),
[final] ).
cnf(i_0_68,negated_conjecture,
( ~ disjoint(esk7_0,esk8_0)
| set_difference(esk7_0,esk8_0) != esk7_0 ),
inference(split_conjunct,[status(thm)],[i_0_34]),
[final] ).
cnf(i_0_69,plain,
( ~ in(X1,X2)
| ~ empty(X2) ),
inference(split_conjunct,[status(thm)],[i_0_35]),
[final] ).
cnf(i_0_70,plain,
set_intersection2(X1,X2) = set_intersection2(X2,X1),
inference(split_conjunct,[status(thm)],[i_0_36]),
[final] ).
cnf(i_0_71,negated_conjecture,
( disjoint(esk7_0,esk8_0)
| set_difference(esk7_0,esk8_0) = esk7_0 ),
inference(split_conjunct,[status(thm)],[i_0_34]),
[final] ).
cnf(i_0_72,plain,
( subset(X1,X2)
| X1 != X2 ),
inference(split_conjunct,[status(thm)],[i_0_30]),
[final] ).
cnf(i_0_73,plain,
( subset(X1,X2)
| X2 != X1 ),
inference(split_conjunct,[status(thm)],[i_0_30]),
[final] ).
cnf(i_0_74,plain,
( X1 = X2
| ~ empty(X1)
| ~ empty(X2) ),
inference(split_conjunct,[status(thm)],[i_0_37]),
[final] ).
cnf(i_0_75,plain,
set_intersection2(X1,X1) = X1,
inference(split_conjunct,[status(thm)],[i_0_38]),
[final] ).
cnf(i_0_76,plain,
subset(X1,X1),
inference(split_conjunct,[status(thm)],[i_0_39]),
[final] ).
cnf(i_0_77,plain,
set_difference(X1,empty_set) = X1,
inference(split_conjunct,[status(thm)],[i_0_40]),
[final] ).
cnf(i_0_78,plain,
set_difference(empty_set,X1) = empty_set,
inference(split_conjunct,[status(thm)],[i_0_41]),
[final] ).
cnf(i_0_79,plain,
set_intersection2(X1,empty_set) = empty_set,
inference(split_conjunct,[status(thm)],[i_0_42]),
[final] ).
cnf(i_0_80,plain,
( X1 = empty_set
| ~ empty(X1) ),
inference(split_conjunct,[status(thm)],[i_0_43]),
[final] ).
cnf(i_0_81,plain,
~ empty(esk5_0),
inference(split_conjunct,[status(thm)],[i_0_44]),
[final] ).
cnf(i_0_82,plain,
empty(esk4_0),
inference(split_conjunct,[status(thm)],[i_0_45]),
[final] ).
cnf(i_0_83,plain,
empty(empty_set),
inference(split_conjunct,[status(thm)],[fc1_xboole_0]),
[final] ).
cnf(i_0_84,axiom,
X1 = X1 ).
cnf(i_0_85,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_86,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_87,axiom,
( X1 != X2
| set_intersection2(X1,X3) = set_intersection2(X2,X3) ) ).
cnf(i_0_88,axiom,
( X1 != X2
| set_intersection2(X3,X1) = set_intersection2(X3,X2) ) ).
cnf(i_0_89,axiom,
( X1 != X2
| set_difference(X1,X3) = set_difference(X2,X3) ) ).
cnf(i_0_90,axiom,
( X1 != X2
| set_difference(X3,X1) = set_difference(X3,X2) ) ).
cnf(i_0_91,axiom,
( X1 != X2
| ~ in(X1,X3)
| in(X2,X3) ) ).
cnf(i_0_92,axiom,
( X1 != X2
| ~ in(X3,X1)
| in(X3,X2) ) ).
cnf(i_0_93,axiom,
( X1 != X2
| ~ disjoint(X1,X3)
| disjoint(X2,X3) ) ).
cnf(i_0_94,axiom,
( X1 != X2
| ~ disjoint(X3,X1)
| disjoint(X3,X2) ) ).
cnf(i_0_95,axiom,
( X1 != X2
| ~ subset(X1,X3)
| subset(X2,X3) ) ).
cnf(i_0_96,axiom,
( X1 != X2
| ~ subset(X3,X1)
| subset(X3,X2) ) ).
cnf(i_0_97,axiom,
( X1 != X2
| ~ empty(X1)
| empty(X2) ) ).
cnf(i_0_324,plain,
disjoint(set_intersection2(esk4_0,X1),X2),
inference(scs_inference,[],[i_0_196,i_0_305,i_0_308,i_0_64,i_0_62,i_0_54]) ).
cnf(i_0_342,plain,
~ in(X1,set_difference(empty_set,X2)),
inference(rename_variables,[],[i_0_308]) ).
cnf(i_0_965,plain,
~ in(X1,set_difference(empty_set,X2)),
inference(rename_variables,[],[i_0_308]) ).
cnf(i_0_977,plain,
subset(empty_set,X1),
inference(rename_variables,[],[i_0_288]) ).
cnf(i_0_1163,plain,
~ in(X1,set_difference(empty_set,X2)),
inference(rename_variables,[],[i_0_308]) ).
cnf(i_0_1167,plain,
~ in(X1,set_difference(empty_set,X2)),
inference(rename_variables,[],[i_0_308]) ).
cnf(i_0_1171,plain,
~ in(X1,set_difference(empty_set,X2)),
inference(rename_variables,[],[i_0_308]) ).
cnf(i_0_1175,plain,
subset(empty_set,X1),
inference(rename_variables,[],[i_0_288]) ).
cnf(i_0_1200,plain,
subset(empty_set,X1),
inference(rename_variables,[],[i_0_288]) ).
cnf(i_0_1229,plain,
subset(empty_set,X1),
inference(rename_variables,[],[i_0_288]) ).
cnf(i_0_1314,plain,
~ in(esk1_2(esk5_0,esk4_0),set_difference(X1,esk5_0)),
inference(scs_inference,[],[i_0_1251,i_0_100]) ).
cnf(i_0_327,plain,
~ in(X1,set_difference(set_difference(empty_set,X2),X3)),
inference(scs_inference,[],[i_0_196,i_0_305,i_0_308,i_0_322,i_0_64,i_0_62,i_0_54,i_0_101]) ).
cnf(i_0_329,plain,
~ in(X1,set_intersection2(set_difference(empty_set,X2),X3)),
inference(scs_inference,[],[i_0_196,i_0_305,i_0_308,i_0_322,i_0_64,i_0_62,i_0_54,i_0_101,i_0_102]) ).
cnf(i_0_331,plain,
~ in(X1,set_intersection2(X2,set_difference(empty_set,X3))),
inference(scs_inference,[],[i_0_196,i_0_305,i_0_308,i_0_322,i_0_64,i_0_62,i_0_54,i_0_101,i_0_102,i_0_103]) ).
cnf(i_0_341,plain,
~ in(X1,set_intersection2(X2,empty_set)),
inference(scs_inference,[],[i_0_313,i_0_244,i_0_120,i_0_196,i_0_305,i_0_308,i_0_322,i_0_64,i_0_62,i_0_54,i_0_101,i_0_102,i_0_103,i_0_72,i_0_73,i_0_85,i_0_99,i_0_60]) ).
cnf(i_0_344,plain,
~ subset(set_intersection2(esk5_0,esk5_0),set_intersection2(X1,esk4_0)),
inference(scs_inference,[],[i_0_313,i_0_244,i_0_120,i_0_339,i_0_196,i_0_305,i_0_308,i_0_322,i_0_64,i_0_62,i_0_54,i_0_101,i_0_102,i_0_103,i_0_72,i_0_73,i_0_85,i_0_99,i_0_60,i_0_61]) ).
cnf(i_0_347,plain,
~ in(X1,set_intersection2(empty_set,X2)),
inference(scs_inference,[],[i_0_70,i_0_313,i_0_244,i_0_120,i_0_339,i_0_196,i_0_305,i_0_308,i_0_322,i_0_64,i_0_62,i_0_54,i_0_101,i_0_102,i_0_103,i_0_72,i_0_73,i_0_85,i_0_99,i_0_60,i_0_61,i_0_92]) ).
cnf(i_0_349,plain,
empty_set != set_intersection2(set_difference(esk5_0,empty_set),set_difference(esk5_0,empty_set)),
inference(scs_inference,[],[i_0_70,i_0_172,i_0_313,i_0_122,i_0_244,i_0_120,i_0_339,i_0_196,i_0_305,i_0_308,i_0_322,i_0_64,i_0_62,i_0_54,i_0_101,i_0_102,i_0_103,i_0_72,i_0_73,i_0_85,i_0_99,i_0_60,i_0_61,i_0_92,i_0_86]) ).
cnf(i_0_351,plain,
disjoint(X1,set_intersection2(esk4_0,X2)),
inference(scs_inference,[],[i_0_70,i_0_172,i_0_313,i_0_122,i_0_244,i_0_120,i_0_339,i_0_196,i_0_305,i_0_308,i_0_322,i_0_64,i_0_62,i_0_54,i_0_101,i_0_102,i_0_103,i_0_72,i_0_73,i_0_85,i_0_99,i_0_60,i_0_61,i_0_92,i_0_86,i_0_65]) ).
cnf(i_0_356,plain,
~ subset(set_intersection2(esk5_0,esk5_0),set_intersection2(esk4_0,X1)),
inference(scs_inference,[],[i_0_70,i_0_348,i_0_172,i_0_313,i_0_122,i_0_244,i_0_120,i_0_339,i_0_196,i_0_305,i_0_308,i_0_322,i_0_163,i_0_64,i_0_62,i_0_54,i_0_101,i_0_102,i_0_103,i_0_72,i_0_73,i_0_85,i_0_99,i_0_60,i_0_61,i_0_92,i_0_86,i_0_65,i_0_51,i_0_96]) ).
cnf(i_0_1033,plain,
subset(set_difference(empty_set,X1),X2),
inference(rename_variables,[],[i_0_321]) ).
cnf(i_0_1109,plain,
subset(set_difference(empty_set,X1),X2),
inference(rename_variables,[],[i_0_321]) ).
cnf(i_0_1235,plain,
subset(set_difference(empty_set,X1),X2),
inference(rename_variables,[],[i_0_321]) ).
cnf(i_0_1281,plain,
subset(set_difference(empty_set,X1),X2),
inference(rename_variables,[],[i_0_321]) ).
cnf(i_0_1290,plain,
subset(set_difference(empty_set,X1),X2),
inference(rename_variables,[],[i_0_321]) ).
cnf(i_0_360,plain,
subset(set_intersection2(empty_set,X1),X2),
inference(scs_inference,[],[i_0_347,i_0_353,i_0_64,i_0_62]) ).
cnf(i_0_361,plain,
~ in(X1,set_intersection2(empty_set,X2)),
inference(rename_variables,[],[i_0_347]) ).
cnf(i_0_363,plain,
disjoint(set_intersection2(X1,esk4_0),X2),
inference(scs_inference,[],[i_0_347,i_0_353,i_0_223,i_0_64,i_0_62,i_0_54]) ).
cnf(i_0_378,plain,
~ in(X1,set_intersection2(empty_set,X2)),
inference(rename_variables,[],[i_0_347]) ).
cnf(i_0_381,plain,
~ in(X1,set_intersection2(empty_set,X2)),
inference(rename_variables,[],[i_0_347]) ).
cnf(i_0_392,plain,
subset(set_intersection2(X1,empty_set),X2),
inference(scs_inference,[],[i_0_338,i_0_341,i_0_64,i_0_62]) ).
cnf(i_0_393,plain,
~ in(X1,set_intersection2(X2,empty_set)),
inference(rename_variables,[],[i_0_341]) ).
cnf(i_0_402,plain,
~ in(X1,set_intersection2(set_difference(empty_set,X2),X3)),
inference(rename_variables,[],[i_0_329]) ).
cnf(i_0_408,plain,
~ in(X1,set_intersection2(empty_set,X2)),
inference(rename_variables,[],[i_0_347]) ).
cnf(i_0_411,plain,
~ in(X1,set_intersection2(empty_set,X2)),
inference(rename_variables,[],[i_0_347]) ).
cnf(i_0_444,plain,
~ in(X1,set_intersection2(empty_set,X2)),
inference(rename_variables,[],[i_0_347]) ).
cnf(i_0_447,plain,
~ in(X1,set_intersection2(empty_set,X2)),
inference(rename_variables,[],[i_0_347]) ).
cnf(i_0_475,plain,
~ in(X1,set_intersection2(empty_set,X2)),
inference(rename_variables,[],[i_0_347]) ).
cnf(i_0_478,plain,
~ in(X1,set_intersection2(empty_set,X2)),
inference(rename_variables,[],[i_0_347]) ).
cnf(i_0_496,plain,
~ in(X1,set_intersection2(empty_set,X2)),
inference(rename_variables,[],[i_0_347]) ).
cnf(i_0_511,plain,
~ in(X1,set_intersection2(empty_set,X2)),
inference(rename_variables,[],[i_0_347]) ).
cnf(i_0_527,plain,
~ in(X1,set_intersection2(empty_set,X2)),
inference(rename_variables,[],[i_0_347]) ).
cnf(i_0_674,plain,
~ subset(set_difference(set_intersection2(esk5_0,esk5_0),empty_set),set_intersection2(esk4_0,X1)),
inference(scs_inference,[],[i_0_77,i_0_356,i_0_95]) ).
cnf(i_0_759,plain,
~ subset(set_difference(set_intersection2(esk5_0,esk5_0),empty_set),set_intersection2(X1,esk4_0)),
inference(scs_inference,[],[i_0_77,i_0_344,i_0_95]) ).
cnf(i_0_765,plain,
~ in(set_difference(set_intersection2(esk5_0,esk5_0),empty_set),esk3_3(esk5_0,empty_set,esk4_0)),
inference(scs_inference,[],[i_0_77,i_0_760,i_0_762,i_0_764,i_0_271,i_0_273,i_0_344,i_0_252,i_0_95,i_0_93,i_0_94,i_0_91]) ).
cnf(i_0_767,plain,
~ subset(set_intersection2(esk5_0,esk5_0),set_difference(set_intersection2(X1,esk4_0),empty_set)),
inference(scs_inference,[],[i_0_77,i_0_760,i_0_762,i_0_764,i_0_766,i_0_271,i_0_273,i_0_344,i_0_252,i_0_95,i_0_93,i_0_94,i_0_91,i_0_96]) ).
cnf(i_0_943,plain,
~ in(X1,set_intersection2(X2,empty_set)),
inference(rename_variables,[],[i_0_341]) ).
cnf(i_0_969,plain,
set_intersection2(X1,esk4_0) != set_intersection2(esk5_0,esk5_0),
inference(scs_inference,[],[i_0_344,i_0_73]) ).
cnf(i_0_988,plain,
set_intersection2(esk4_0,X1) != set_intersection2(esk5_0,esk5_0),
inference(scs_inference,[],[i_0_356,i_0_73]) ).
cnf(i_0_990,plain,
set_intersection2(esk5_0,esk5_0) != set_intersection2(esk4_0,X1),
inference(scs_inference,[],[i_0_356,i_0_73,i_0_72]) ).
cnf(i_0_1011,plain,
~ in(X1,set_intersection2(X2,empty_set)),
inference(rename_variables,[],[i_0_341]) ).
cnf(i_0_1015,plain,
~ in(X1,set_intersection2(X2,empty_set)),
inference(rename_variables,[],[i_0_341]) ).
cnf(i_0_1019,plain,
~ in(X1,set_intersection2(X2,empty_set)),
inference(rename_variables,[],[i_0_341]) ).
cnf(i_0_366,plain,
~ in(X1,set_difference(set_intersection2(empty_set,X2),X3)),
inference(scs_inference,[],[i_0_347,i_0_361,i_0_353,i_0_223,i_0_64,i_0_62,i_0_54,i_0_101]) ).
cnf(i_0_368,plain,
~ in(X1,set_intersection2(set_intersection2(empty_set,X2),X3)),
inference(scs_inference,[],[i_0_347,i_0_361,i_0_353,i_0_223,i_0_64,i_0_62,i_0_54,i_0_101,i_0_102]) ).
cnf(i_0_370,plain,
~ in(X1,set_intersection2(X2,set_intersection2(empty_set,X3))),
inference(scs_inference,[],[i_0_347,i_0_361,i_0_353,i_0_223,i_0_64,i_0_62,i_0_54,i_0_101,i_0_102,i_0_103]) ).
cnf(i_0_372,plain,
subset(set_difference(X1,empty_set),X1),
inference(scs_inference,[],[i_0_347,i_0_361,i_0_353,i_0_223,i_0_77,i_0_64,i_0_62,i_0_54,i_0_101,i_0_102,i_0_103,i_0_72]) ).
cnf(i_0_374,plain,
subset(X1,set_difference(X1,empty_set)),
inference(scs_inference,[],[i_0_347,i_0_361,i_0_353,i_0_223,i_0_77,i_0_64,i_0_62,i_0_54,i_0_101,i_0_102,i_0_103,i_0_72,i_0_73]) ).
cnf(i_0_376,plain,
X1 = set_difference(X1,empty_set),
inference(scs_inference,[],[i_0_347,i_0_361,i_0_353,i_0_223,i_0_77,i_0_64,i_0_62,i_0_54,i_0_101,i_0_102,i_0_103,i_0_72,i_0_73,i_0_85]) ).
cnf(i_0_388,plain,
disjoint(X1,set_intersection2(X2,esk4_0)),
inference(scs_inference,[],[i_0_70,i_0_384,i_0_347,i_0_361,i_0_378,i_0_337,i_0_275,i_0_244,i_0_353,i_0_223,i_0_77,i_0_64,i_0_62,i_0_54,i_0_101,i_0_102,i_0_103,i_0_72,i_0_73,i_0_85,i_0_99,i_0_61,i_0_96,i_0_86,i_0_65]) ).
cnf(i_0_395,plain,
~ in(X1,set_difference(set_intersection2(X2,empty_set),X3)),
inference(scs_inference,[],[i_0_338,i_0_341,i_0_393,i_0_64,i_0_62,i_0_101]) ).
cnf(i_0_397,plain,
~ in(X1,set_intersection2(set_intersection2(X2,empty_set),X3)),
inference(scs_inference,[],[i_0_338,i_0_341,i_0_393,i_0_64,i_0_62,i_0_101,i_0_102]) ).
cnf(i_0_399,plain,
~ in(X1,set_intersection2(X2,set_intersection2(X3,empty_set))),
inference(scs_inference,[],[i_0_338,i_0_341,i_0_393,i_0_64,i_0_62,i_0_101,i_0_102,i_0_103]) ).
cnf(i_0_401,plain,
disjoint(set_difference(empty_set,X1),X2),
inference(scs_inference,[],[i_0_329,i_0_338,i_0_341,i_0_393,i_0_64,i_0_62,i_0_101,i_0_102,i_0_103,i_0_54]) ).
cnf(i_0_1086,plain,
subset(set_intersection2(empty_set,X1),X2),
inference(rename_variables,[],[i_0_360]) ).
cnf(i_0_1103,plain,
subset(set_intersection2(X1,empty_set),X2),
inference(rename_variables,[],[i_0_392]) ).
cnf(i_0_407,plain,
in(esk3_3(esk5_0,empty_set,esk4_0),set_difference(esk5_0,set_intersection2(empty_set,X1))),
inference(scs_inference,[],[i_0_385,i_0_347,i_0_234,i_0_329,i_0_338,i_0_341,i_0_393,i_0_64,i_0_62,i_0_101,i_0_102,i_0_103,i_0_54,i_0_73,i_0_85,i_0_99]) ).
cnf(i_0_410,plain,
~ subset(set_intersection2(esk5_0,esk5_0),set_intersection2(empty_set,X1)),
inference(scs_inference,[],[i_0_385,i_0_347,i_0_408,i_0_244,i_0_234,i_0_329,i_0_338,i_0_341,i_0_393,i_0_64,i_0_62,i_0_101,i_0_102,i_0_103,i_0_54,i_0_73,i_0_85,i_0_99,i_0_61]) ).
cnf(i_0_413,plain,
~ subset(set_intersection2(esk5_0,esk5_0),set_intersection2(X1,empty_set)),
inference(scs_inference,[],[i_0_70,i_0_385,i_0_347,i_0_408,i_0_244,i_0_234,i_0_329,i_0_338,i_0_341,i_0_393,i_0_64,i_0_62,i_0_101,i_0_102,i_0_103,i_0_54,i_0_73,i_0_85,i_0_99,i_0_61,i_0_96]) ).
cnf(i_0_415,plain,
~ in(esk5_0,esk2_3(set_difference(esk5_0,empty_set),set_difference(esk5_0,empty_set),esk4_0)),
inference(scs_inference,[],[i_0_70,i_0_376,i_0_385,i_0_347,i_0_408,i_0_244,i_0_213,i_0_234,i_0_329,i_0_338,i_0_341,i_0_393,i_0_64,i_0_62,i_0_101,i_0_102,i_0_103,i_0_54,i_0_73,i_0_85,i_0_99,i_0_61,i_0_96,i_0_91]) ).
cnf(i_0_416,plain,
X1 = set_difference(X1,empty_set),
inference(rename_variables,[],[i_0_376]) ).
cnf(i_0_417,plain,
empty_set != set_difference(esk5_0,empty_set),
inference(scs_inference,[],[i_0_70,i_0_376,i_0_385,i_0_349,i_0_347,i_0_408,i_0_113,i_0_244,i_0_213,i_0_234,i_0_329,i_0_338,i_0_341,i_0_393,i_0_64,i_0_62,i_0_101,i_0_102,i_0_103,i_0_54,i_0_73,i_0_85,i_0_99,i_0_61,i_0_96,i_0_91,i_0_86]) ).
cnf(i_0_419,plain,
disjoint(X1,set_difference(empty_set,X2)),
inference(scs_inference,[],[i_0_70,i_0_376,i_0_385,i_0_349,i_0_347,i_0_408,i_0_113,i_0_244,i_0_213,i_0_234,i_0_329,i_0_338,i_0_341,i_0_393,i_0_64,i_0_62,i_0_101,i_0_102,i_0_103,i_0_54,i_0_73,i_0_85,i_0_99,i_0_61,i_0_96,i_0_91,i_0_86,i_0_65]) ).
cnf(i_0_421,plain,
in(esk3_3(esk5_0,empty_set,empty_set),esk5_0),
inference(scs_inference,[],[i_0_70,i_0_376,i_0_385,i_0_349,i_0_347,i_0_408,i_0_113,i_0_244,i_0_213,i_0_234,i_0_329,i_0_338,i_0_341,i_0_393,i_0_163,i_0_64,i_0_62,i_0_101,i_0_102,i_0_103,i_0_54,i_0_73,i_0_85,i_0_99,i_0_61,i_0_96,i_0_91,i_0_86,i_0_65,i_0_49]) ).
cnf(i_0_424,plain,
in(esk3_3(esk5_0,empty_set,empty_set),set_intersection2(esk5_0,esk5_0)),
inference(scs_inference,[],[i_0_70,i_0_376,i_0_385,i_0_349,i_0_347,i_0_408,i_0_113,i_0_244,i_0_213,i_0_234,i_0_329,i_0_338,i_0_341,i_0_393,i_0_163,i_0_64,i_0_62,i_0_101,i_0_102,i_0_103,i_0_54,i_0_73,i_0_85,i_0_99,i_0_61,i_0_96,i_0_91,i_0_86,i_0_65,i_0_49,i_0_98]) ).
cnf(i_0_426,plain,
~ in(esk3_3(esk5_0,empty_set,empty_set),set_difference(X1,esk5_0)),
inference(scs_inference,[],[i_0_70,i_0_376,i_0_385,i_0_349,i_0_347,i_0_408,i_0_113,i_0_244,i_0_213,i_0_234,i_0_329,i_0_338,i_0_341,i_0_393,i_0_163,i_0_64,i_0_62,i_0_101,i_0_102,i_0_103,i_0_54,i_0_73,i_0_85,i_0_99,i_0_61,i_0_96,i_0_91,i_0_86,i_0_65,i_0_49,i_0_98,i_0_100]) ).
cnf(i_0_439,plain,
~ in(X1,set_intersection2(set_intersection2(empty_set,X2),X3)),
inference(rename_variables,[],[i_0_368]) ).
cnf(i_0_452,plain,
X1 = set_difference(X1,empty_set),
inference(rename_variables,[],[i_0_376]) ).
cnf(i_0_460,plain,
X1 = set_difference(X1,empty_set),
inference(rename_variables,[],[i_0_376]) ).
cnf(i_0_470,plain,
~ in(X1,set_intersection2(set_intersection2(X2,empty_set),X3)),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_473,plain,
X1 = set_difference(X1,empty_set),
inference(rename_variables,[],[i_0_376]) ).
cnf(i_0_555,plain,
X1 = set_difference(X1,empty_set),
inference(rename_variables,[],[i_0_376]) ).
cnf(i_0_564,plain,
X1 = set_difference(X1,empty_set),
inference(rename_variables,[],[i_0_376]) ).
cnf(i_0_940,plain,
X1 = set_difference(X1,empty_set),
inference(rename_variables,[],[i_0_376]) ).
cnf(i_0_982,plain,
subset(X1,set_difference(X1,empty_set)),
inference(rename_variables,[],[i_0_374]) ).
cnf(i_0_1197,plain,
X1 = set_difference(X1,empty_set),
inference(rename_variables,[],[i_0_376]) ).
cnf(i_0_428,plain,
~ in(esk3_3(esk5_0,empty_set,empty_set),set_difference(X1,set_intersection2(esk5_0,esk5_0))),
inference(scs_inference,[],[i_0_424,i_0_100]) ).
cnf(i_0_430,plain,
~ in(set_intersection2(esk5_0,esk5_0),esk3_3(esk5_0,empty_set,empty_set)),
inference(scs_inference,[],[i_0_424,i_0_100,i_0_64]) ).
cnf(i_0_432,plain,
~ in(esk5_0,set_difference(esk3_3(esk5_0,empty_set,esk4_0),X1)),
inference(scs_inference,[],[i_0_424,i_0_242,i_0_100,i_0_64,i_0_101]) ).
cnf(i_0_434,plain,
~ in(esk5_0,set_intersection2(esk3_3(esk5_0,empty_set,esk4_0),X1)),
inference(scs_inference,[],[i_0_424,i_0_242,i_0_100,i_0_64,i_0_101,i_0_102]) ).
cnf(i_0_436,plain,
~ in(esk5_0,set_intersection2(X1,esk3_3(esk5_0,empty_set,esk4_0))),
inference(scs_inference,[],[i_0_424,i_0_242,i_0_100,i_0_64,i_0_101,i_0_102,i_0_103]) ).
cnf(i_0_438,plain,
disjoint(set_intersection2(empty_set,X1),X2),
inference(scs_inference,[],[i_0_424,i_0_368,i_0_242,i_0_100,i_0_64,i_0_101,i_0_102,i_0_103,i_0_54]) ).
cnf(i_0_446,plain,
~ subset(set_difference(esk5_0,empty_set),set_intersection2(empty_set,X1)),
inference(scs_inference,[],[i_0_424,i_0_347,i_0_444,i_0_207,i_0_368,i_0_242,i_0_100,i_0_64,i_0_101,i_0_102,i_0_103,i_0_54,i_0_98,i_0_99,i_0_61]) ).
cnf(i_0_449,plain,
~ subset(set_difference(esk5_0,empty_set),set_intersection2(X1,empty_set)),
inference(scs_inference,[],[i_0_70,i_0_424,i_0_347,i_0_444,i_0_207,i_0_368,i_0_242,i_0_100,i_0_64,i_0_101,i_0_102,i_0_103,i_0_54,i_0_98,i_0_99,i_0_61,i_0_96]) ).
cnf(i_0_451,plain,
~ in(esk5_0,esk2_3(set_difference(esk5_0,empty_set),set_difference(esk5_0,empty_set),empty_set)),
inference(scs_inference,[],[i_0_70,i_0_424,i_0_376,i_0_347,i_0_444,i_0_207,i_0_358,i_0_368,i_0_242,i_0_100,i_0_64,i_0_101,i_0_102,i_0_103,i_0_54,i_0_98,i_0_99,i_0_61,i_0_96,i_0_91]) ).
cnf(i_0_453,plain,
set_intersection2(empty_set,X1) = empty_set,
inference(scs_inference,[],[i_0_70,i_0_450,i_0_424,i_0_376,i_0_347,i_0_444,i_0_207,i_0_358,i_0_368,i_0_242,i_0_79,i_0_100,i_0_64,i_0_101,i_0_102,i_0_103,i_0_54,i_0_98,i_0_99,i_0_61,i_0_96,i_0_91,i_0_86]) ).
cnf(i_0_456,plain,
disjoint(X1,set_intersection2(empty_set,X2)),
inference(scs_inference,[],[i_0_70,i_0_450,i_0_424,i_0_376,i_0_347,i_0_444,i_0_207,i_0_358,i_0_368,i_0_242,i_0_79,i_0_100,i_0_64,i_0_101,i_0_102,i_0_103,i_0_54,i_0_98,i_0_99,i_0_61,i_0_96,i_0_91,i_0_86,i_0_65]) ).
cnf(i_0_458,plain,
empty_set = set_intersection2(empty_set,X1),
inference(scs_inference,[],[i_0_70,i_0_450,i_0_424,i_0_376,i_0_347,i_0_444,i_0_207,i_0_358,i_0_368,i_0_242,i_0_79,i_0_100,i_0_64,i_0_101,i_0_102,i_0_103,i_0_54,i_0_98,i_0_99,i_0_61,i_0_96,i_0_91,i_0_86,i_0_65,i_0_85]) ).
cnf(i_0_459,plain,
~ subset(esk5_0,set_intersection2(empty_set,X1)),
inference(scs_inference,[],[i_0_70,i_0_450,i_0_424,i_0_376,i_0_452,i_0_347,i_0_444,i_0_207,i_0_358,i_0_368,i_0_242,i_0_79,i_0_100,i_0_64,i_0_101,i_0_102,i_0_103,i_0_54,i_0_98,i_0_99,i_0_61,i_0_96,i_0_91,i_0_86,i_0_65,i_0_85,i_0_95]) ).
cnf(i_0_518,plain,
~ in(esk5_0,esk3_3(esk5_0,empty_set,empty_set)),
inference(scs_inference,[],[i_0_421,i_0_64]) ).
cnf(i_0_520,plain,
~ in(esk5_0,set_difference(esk3_3(esk5_0,empty_set,empty_set),X1)),
inference(scs_inference,[],[i_0_421,i_0_64,i_0_101]) ).
cnf(i_0_522,plain,
~ in(esk5_0,set_intersection2(esk3_3(esk5_0,empty_set,empty_set),X1)),
inference(scs_inference,[],[i_0_421,i_0_64,i_0_101,i_0_102]) ).
cnf(i_0_524,plain,
~ in(esk5_0,set_intersection2(X1,esk3_3(esk5_0,empty_set,empty_set))),
inference(scs_inference,[],[i_0_421,i_0_64,i_0_101,i_0_102,i_0_103]) ).
cnf(i_0_545,plain,
~ in(set_difference(esk5_0,set_intersection2(empty_set,X1)),esk3_3(esk5_0,empty_set,esk4_0)),
inference(scs_inference,[],[i_0_407,i_0_64]) ).
cnf(i_0_547,plain,
esk4_0 != set_difference(set_difference(esk5_0,empty_set),empty_set),
inference(scs_inference,[],[i_0_232,i_0_407,i_0_77,i_0_64,i_0_86]) ).
cnf(i_0_549,plain,
in(esk3_3(set_difference(esk5_0,empty_set),empty_set,esk4_0),set_difference(esk5_0,empty_set)),
inference(scs_inference,[],[i_0_232,i_0_114,i_0_407,i_0_77,i_0_64,i_0_86,i_0_49]) ).
cnf(i_0_695,plain,
~ subset(set_difference(set_intersection2(esk5_0,esk5_0),empty_set),set_intersection2(X1,empty_set)),
inference(scs_inference,[],[i_0_77,i_0_413,i_0_95]) ).
cnf(i_0_697,plain,
~ disjoint(set_difference(set_intersection2(esk5_0,esk5_0),empty_set),esk5_0),
inference(scs_inference,[],[i_0_77,i_0_696,i_0_565,i_0_413,i_0_95,i_0_93]) ).
cnf(i_0_699,plain,
~ disjoint(set_intersection2(esk5_0,esk5_0),set_difference(esk5_0,empty_set)),
inference(scs_inference,[],[i_0_77,i_0_696,i_0_698,i_0_565,i_0_413,i_0_95,i_0_93,i_0_94]) ).
cnf(i_0_774,plain,
~ subset(set_difference(set_intersection2(esk5_0,esk5_0),empty_set),set_intersection2(empty_set,X1)),
inference(scs_inference,[],[i_0_77,i_0_410,i_0_95]) ).
cnf(i_0_776,plain,
~ disjoint(set_difference(esk5_0,empty_set),esk5_0),
inference(scs_inference,[],[i_0_77,i_0_775,i_0_248,i_0_410,i_0_95,i_0_93]) ).
cnf(c_0_358,plain,
( in(X1,X2)
| ~ in(X1,X3)
| X3 != set_intersection2(X4,X2) ),
i_0_60 ).
cnf(c_0_359,plain,
( ~ in(X1,X2)
| ~ in(X1,X3)
| X3 != set_difference(X4,X2) ),
i_0_57 ).
cnf(c_0_360,plain,
( in(X1,X2)
| ~ in(X1,set_intersection2(X3,X2)) ),
inference(er,[status(thm)],[c_0_358]) ).
cnf(c_0_361,plain,
( disjoint(X1,X2)
| in(esk6_2(X1,X2),set_intersection2(X1,X2)) ),
i_0_54 ).
cnf(c_0_362,plain,
set_intersection2(X1,X2) = set_intersection2(X2,X1),
i_0_70 ).
cnf(c_0_363,plain,
~ in(X1,set_intersection2(X2,empty_set)),
i_0_341 ).
cnf(c_0_364,plain,
set_intersection2(X1,empty_set) = empty_set,
i_0_79 ).
cnf(c_0_365,plain,
( in(X1,X2)
| ~ in(X1,X3)
| ~ in(X1,X4)
| X2 != set_intersection2(X3,X4) ),
i_0_53 ).
cnf(c_0_366,plain,
( ~ in(X1,set_difference(X2,X3))
| ~ in(X1,X3) ),
inference(er,[status(thm)],[c_0_359]) ).
cnf(c_0_367,plain,
( disjoint(X1,X2)
| in(esk6_2(X1,X2),X2) ),
inference(spm,[status(thm)],[c_0_360,c_0_361]) ).
cnf(c_0_368,plain,
( disjoint(X1,X2)
| in(esk6_2(X1,X2),set_intersection2(X2,X1)) ),
inference(spm,[status(thm)],[c_0_361,c_0_362]) ).
cnf(c_0_369,plain,
( ~ in(X1,set_intersection2(X2,X3))
| ~ disjoint(X2,X3) ),
i_0_52 ).
cnf(c_0_370,plain,
~ in(X1,empty_set),
inference(rw,[status(thm)],[c_0_363,c_0_364]) ).
cnf(c_0_371,plain,
( in(esk3_3(X1,X2,X3),X1)
| in(esk3_3(X1,X2,X3),X3)
| X3 = set_difference(X1,X2) ),
i_0_49 ).
cnf(c_0_372,plain,
set_difference(empty_set,X1) = empty_set,
i_0_78 ).
cnf(c_0_373,plain,
( in(X1,set_intersection2(X2,X3))
| ~ in(X1,X3)
| ~ in(X1,X2) ),
inference(er,[status(thm)],[c_0_365]) ).
cnf(c_0_374,plain,
( disjoint(X1,X2)
| ~ disjoint(X2,X1) ),
i_0_65 ).
cnf(c_0_375,negated_conjecture,
( disjoint(esk7_0,esk8_0)
| set_difference(esk7_0,esk8_0) = esk7_0 ),
i_0_71 ).
cnf(c_0_376,plain,
( disjoint(X1,set_difference(X2,X3))
| ~ in(esk6_2(X1,set_difference(X2,X3)),X3) ),
inference(spm,[status(thm)],[c_0_366,c_0_367]) ).
cnf(c_0_377,plain,
( disjoint(X1,X2)
| in(esk6_2(X1,X2),X1) ),
inference(spm,[status(thm)],[c_0_360,c_0_368]) ).
cnf(c_0_378,plain,
( set_intersection2(X1,X2) = empty_set
| ~ disjoint(X1,X2) ),
i_0_67 ).
cnf(c_0_379,plain,
( ~ disjoint(X1,X2)
| ~ in(X3,set_intersection2(X2,X1)) ),
inference(spm,[status(thm)],[c_0_369,c_0_362]) ).
cnf(c_0_380,plain,
( X1 = empty_set
| in(esk3_3(empty_set,X2,X1),X1) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_370,c_0_371]),c_0_372]) ).
cnf(c_0_381,plain,
( ~ disjoint(X1,X2)
| ~ in(X3,X2)
| ~ in(X3,X1) ),
inference(spm,[status(thm)],[c_0_369,c_0_373]) ).
cnf(c_0_382,negated_conjecture,
( set_difference(esk7_0,esk8_0) = esk7_0
| disjoint(esk8_0,esk7_0) ),
inference(spm,[status(thm)],[c_0_374,c_0_375]) ).
cnf(c_0_383,plain,
( in(esk3_3(X1,X2,X3),X2)
| X3 = set_difference(X1,X2)
| ~ in(esk3_3(X1,X2,X3),X3)
| ~ in(esk3_3(X1,X2,X3),X1) ),
i_0_47 ).
cnf(c_0_384,plain,
( set_difference(X1,X2) = X1
| in(esk3_3(X1,X2,X1),X1) ),
inference(ef,[status(thm)],[c_0_371]) ).
cnf(c_0_385,negated_conjecture,
( ~ disjoint(esk7_0,esk8_0)
| set_difference(esk7_0,esk8_0) != esk7_0 ),
i_0_68 ).
cnf(c_0_386,plain,
( disjoint(X1,X2)
| set_intersection2(X1,X2) != empty_set ),
i_0_66 ).
cnf(c_0_387,plain,
disjoint(X1,set_difference(X2,X1)),
inference(spm,[status(thm)],[c_0_376,c_0_377]) ).
cnf(c_0_388,negated_conjecture,
( set_difference(esk7_0,esk8_0) = esk7_0
| set_intersection2(esk7_0,esk8_0) = empty_set ),
inference(spm,[status(thm)],[c_0_378,c_0_375]) ).
cnf(c_0_389,plain,
( set_intersection2(X1,X2) = empty_set
| ~ disjoint(X2,X1) ),
inference(spm,[status(thm)],[c_0_379,c_0_380]) ).
cnf(c_0_390,negated_conjecture,
( ~ in(X1,esk7_0)
| ~ in(X1,esk8_0) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_381,c_0_382]),c_0_359]) ).
cnf(c_0_391,plain,
( set_difference(X1,X2) = X1
| in(esk3_3(X1,X2,X1),X2) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_383,c_0_384]),c_0_384]) ).
cnf(c_0_392,negated_conjecture,
( set_difference(esk7_0,esk8_0) != esk7_0
| set_intersection2(esk7_0,esk8_0) != empty_set ),
inference(spm,[status(thm)],[c_0_385,c_0_386]) ).
cnf(c_0_393,negated_conjecture,
set_intersection2(esk7_0,esk8_0) = empty_set,
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_387,c_0_388]),c_0_389]) ).
cnf(c_0_394,negated_conjecture,
( set_difference(X1,esk8_0) = X1
| ~ in(esk3_3(X1,esk8_0,X1),esk7_0) ),
inference(spm,[status(thm)],[c_0_390,c_0_391]) ).
cnf(c_0_395,negated_conjecture,
set_difference(esk7_0,esk8_0) != esk7_0,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_392,c_0_393])]) ).
cnf(c_0_396,plain,
$false,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_394,c_0_384]),c_0_395]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SEU141+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 : n017.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:43:43 EDT 2026
% 0.16/0.33 % CPUTime :
% 0.16/0.34 % start to proof: theBenchmark
% 212.10/135.43 % Version : CSE_E---1.7
% 212.10/135.43 % Problem : theBenchmark.p
% 212.10/135.43 % SZS status Theorem for theBenchmark.p
% 212.10/135.43 % SZS output start CNFRefutation
% See solution above
% 213.60/136.95 % Total time : 134.496s
%------------------------------------------------------------------------------