%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SEU211+1 : TPTP v9.2.1. Released v3.3.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 : n015.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:04 PM UTC 2026
% Result : Theorem 186.73s 142.50s
% Output : CNFRefutation 192.93s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named c_0_42)
% Comments :
%------------------------------------------------------------------------------
fof(fc1_zfmisc_1,axiom,
! [X1,X2] : ~ empty(ordered_pair(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_zfmisc_1) ).
fof(d14_relat_1,axiom,
! [X1] :
( relation(X1)
=> ! [X2,X3] :
( X3 = relation_inverse_image(X1,X2)
<=> ! [X4] :
( in(X4,X3)
<=> ? [X5] :
( in(ordered_pair(X4,X5),X1)
& in(X5,X2) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d14_relat_1) ).
fof(d5_tarski,axiom,
! [X1,X2] : ordered_pair(X1,X2) = unordered_pair(unordered_pair(X1,X2),singleton(X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d5_tarski) ).
fof(t178_relat_1,conjecture,
! [X1,X2,X3] :
( relation(X3)
=> ( subset(X1,X2)
=> subset(relation_inverse_image(X3,X1),relation_inverse_image(X3,X2)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t178_relat_1) ).
fof(fc3_subset_1,axiom,
! [X1,X2] : ~ empty(unordered_pair(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc3_subset_1) ).
fof(antisymmetry_r2_hidden,axiom,
! [X1,X2] :
( in(X1,X2)
=> ~ in(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',antisymmetry_r2_hidden) ).
fof(rc1_subset_1,axiom,
! [X1] :
( ~ empty(X1)
=> ? [X2] :
( element(X2,powerset(X1))
& ~ empty(X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc1_subset_1) ).
fof(fc1_subset_1,axiom,
! [X1] : ~ empty(powerset(X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_subset_1) ).
fof(fc2_subset_1,axiom,
! [X1] : ~ empty(singleton(X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc2_subset_1) ).
fof(rc2_xboole_0,axiom,
? [X1] : ~ empty(X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc2_xboole_0) ).
fof(rc2_relat_1,axiom,
? [X1] :
( ~ empty(X1)
& relation(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc2_relat_1) ).
fof(d3_tarski,axiom,
! [X1,X2] :
( subset(X1,X2)
<=> ! [X3] :
( in(X3,X1)
=> in(X3,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d3_tarski) ).
fof(t4_subset,axiom,
! [X1,X2,X3] :
( ( in(X1,X2)
& element(X2,powerset(X3)) )
=> element(X1,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t4_subset) ).
fof(t5_subset,axiom,
! [X1,X2,X3] :
~ ( in(X1,X2)
& element(X2,powerset(X3))
& empty(X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5_subset) ).
fof(t3_subset,axiom,
! [X1,X2] :
( element(X1,powerset(X2))
<=> subset(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t3_subset) ).
fof(t2_subset,axiom,
! [X1,X2] :
( element(X1,X2)
=> ( empty(X2)
| in(X1,X2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_subset) ).
fof(t1_subset,axiom,
! [X1,X2] :
( in(X1,X2)
=> element(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t1_subset) ).
fof(t7_boole,axiom,
! [X1,X2] :
~ ( in(X1,X2)
& empty(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t7_boole) ).
fof(commutativity_k2_tarski,axiom,
! [X1,X2] : unordered_pair(X1,X2) = unordered_pair(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_k2_tarski) ).
fof(rc2_subset_1,axiom,
! [X1] :
? [X2] :
( element(X2,powerset(X1))
& empty(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc2_subset_1) ).
fof(existence_m1_subset_1,axiom,
! [X1] :
? [X2] : element(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',existence_m1_subset_1) ).
fof(t8_boole,axiom,
! [X1,X2] :
~ ( empty(X1)
& X1 != X2
& empty(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t8_boole) ).
fof(reflexivity_r1_tarski,axiom,
! [X1,X2] : subset(X1,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',reflexivity_r1_tarski) ).
fof(cc1_relat_1,axiom,
! [X1] :
( empty(X1)
=> relation(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc1_relat_1) ).
fof(t6_boole,axiom,
! [X1] :
( empty(X1)
=> X1 = empty_set ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t6_boole) ).
fof(rc1_relat_1,axiom,
? [X1] :
( empty(X1)
& relation(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc1_relat_1) ).
fof(rc1_xboole_0,axiom,
? [X1] : empty(X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc1_xboole_0) ).
fof(fc4_relat_1,axiom,
( empty(empty_set)
& relation(empty_set) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc4_relat_1) ).
fof(fc1_xboole_0,axiom,
empty(empty_set),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_xboole_0) ).
fof(i_0_29,plain,
! [X1,X2] : ~ empty(ordered_pair(X1,X2)),
inference(fof_simplification,[status(thm)],[fc1_zfmisc_1]) ).
fof(i_0_30,plain,
! [X64,X65,X66,X67,X69,X70,X71,X72,X74] :
( ( in(ordered_pair(X67,esk1_4(X64,X65,X66,X67)),X64)
| ~ in(X67,X66)
| X66 != relation_inverse_image(X64,X65)
| ~ relation(X64) )
& ( in(esk1_4(X64,X65,X66,X67),X65)
| ~ in(X67,X66)
| X66 != relation_inverse_image(X64,X65)
| ~ relation(X64) )
& ( ~ in(ordered_pair(X69,X70),X64)
| ~ in(X70,X65)
| in(X69,X66)
| X66 != relation_inverse_image(X64,X65)
| ~ relation(X64) )
& ( ~ in(esk2_3(X64,X71,X72),X72)
| ~ in(ordered_pair(esk2_3(X64,X71,X72),X74),X64)
| ~ in(X74,X71)
| X72 = relation_inverse_image(X64,X71)
| ~ relation(X64) )
& ( in(ordered_pair(esk2_3(X64,X71,X72),esk3_3(X64,X71,X72)),X64)
| in(esk2_3(X64,X71,X72),X72)
| X72 = relation_inverse_image(X64,X71)
| ~ relation(X64) )
& ( in(esk3_3(X64,X71,X72),X71)
| in(esk2_3(X64,X71,X72),X72)
| X72 = relation_inverse_image(X64,X71)
| ~ relation(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)],[d14_relat_1])])])])])]) ).
fof(i_0_31,plain,
! [X82,X83] : ordered_pair(X82,X83) = unordered_pair(unordered_pair(X82,X83),singleton(X82)),
inference(variable_rename,[status(thm)],[d5_tarski]) ).
fof(i_0_32,plain,
! [X87,X88] : ~ empty(ordered_pair(X87,X88)),
inference(variable_rename,[status(thm)],[i_0_29]) ).
fof(i_0_33,negated_conjecture,
~ ! [X1,X2,X3] :
( relation(X3)
=> ( subset(X1,X2)
=> subset(relation_inverse_image(X3,X1),relation_inverse_image(X3,X2)) ) ),
inference(assume_negation,[status(cth)],[t178_relat_1]) ).
fof(i_0_34,plain,
! [X1,X2] : ~ empty(unordered_pair(X1,X2)),
inference(fof_simplification,[status(thm)],[fc3_subset_1]) ).
fof(i_0_35,plain,
! [X1,X2] :
( in(X1,X2)
=> ~ in(X2,X1) ),
inference(fof_simplification,[status(thm)],[antisymmetry_r2_hidden]) ).
fof(i_0_36,plain,
! [X1] :
( ~ empty(X1)
=> ? [X2] :
( element(X2,powerset(X1))
& ~ empty(X2) ) ),
inference(fof_simplification,[status(thm)],[rc1_subset_1]) ).
fof(i_0_37,plain,
! [X1] : ~ empty(powerset(X1)),
inference(fof_simplification,[status(thm)],[fc1_subset_1]) ).
fof(i_0_38,plain,
! [X1] : ~ empty(singleton(X1)),
inference(fof_simplification,[status(thm)],[fc2_subset_1]) ).
fof(i_0_39,plain,
? [X1] : ~ empty(X1),
inference(fof_simplification,[status(thm)],[rc2_xboole_0]) ).
fof(i_0_40,plain,
? [X1] :
( ~ empty(X1)
& relation(X1) ),
inference(fof_simplification,[status(thm)],[rc2_relat_1]) ).
cnf(i_0_41,plain,
( in(ordered_pair(X1,esk1_4(X2,X3,X4,X1)),X2)
| ~ in(X1,X4)
| X4 != relation_inverse_image(X2,X3)
| ~ relation(X2) ),
inference(split_conjunct,[status(thm)],[i_0_30]) ).
cnf(i_0_42,plain,
ordered_pair(X1,X2) = unordered_pair(unordered_pair(X1,X2),singleton(X1)),
inference(split_conjunct,[status(thm)],[i_0_31]) ).
cnf(i_0_43,plain,
( X3 = relation_inverse_image(X1,X2)
| ~ in(esk2_3(X1,X2,X3),X3)
| ~ in(ordered_pair(esk2_3(X1,X2,X3),X4),X1)
| ~ in(X4,X2)
| ~ relation(X1) ),
inference(split_conjunct,[status(thm)],[i_0_30]) ).
cnf(i_0_44,plain,
( in(ordered_pair(esk2_3(X1,X2,X3),esk3_3(X1,X2,X3)),X1)
| in(esk2_3(X1,X2,X3),X3)
| X3 = relation_inverse_image(X1,X2)
| ~ relation(X1) ),
inference(split_conjunct,[status(thm)],[i_0_30]) ).
cnf(i_0_45,plain,
( in(X1,X5)
| ~ in(ordered_pair(X1,X2),X3)
| ~ in(X2,X4)
| X5 != relation_inverse_image(X3,X4)
| ~ relation(X3) ),
inference(split_conjunct,[status(thm)],[i_0_30]) ).
cnf(i_0_46,plain,
~ empty(ordered_pair(X1,X2)),
inference(split_conjunct,[status(thm)],[i_0_32]) ).
fof(i_0_47,negated_conjecture,
( relation(esk14_0)
& subset(esk12_0,esk13_0)
& ~ subset(relation_inverse_image(esk14_0,esk12_0),relation_inverse_image(esk14_0,esk13_0)) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_33])])]) ).
fof(i_0_48,plain,
! [X76,X77,X78,X79,X80] :
( ( ~ subset(X76,X77)
| ~ in(X78,X76)
| in(X78,X77) )
& ( in(esk4_2(X79,X80),X79)
| subset(X79,X80) )
& ( ~ in(esk4_2(X79,X80),X80)
| subset(X79,X80) ) ),
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_49,plain,
! [X110,X111,X112] :
( ~ in(X110,X111)
| ~ element(X111,powerset(X112))
| element(X110,X112) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t4_subset])]) ).
fof(i_0_50,plain,
! [X113,X114,X115] :
( ~ in(X113,X114)
| ~ element(X114,powerset(X115))
| ~ empty(X115) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t5_subset])]) ).
fof(i_0_51,plain,
! [X90,X91] : ~ empty(unordered_pair(X90,X91)),
inference(variable_rename,[status(thm)],[i_0_34]) ).
fof(i_0_52,plain,
! [X108,X109] :
( ( ~ element(X108,powerset(X109))
| subset(X108,X109) )
& ( ~ subset(X108,X109)
| element(X108,powerset(X109)) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t3_subset])]) ).
fof(i_0_53,plain,
! [X59,X60] :
( ~ in(X59,X60)
| ~ in(X60,X59) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_35])]) ).
fof(i_0_54,plain,
! [X106,X107] :
( ~ element(X106,X107)
| empty(X107)
| in(X106,X107) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t2_subset])]) ).
fof(i_0_55,plain,
! [X104,X105] :
( ~ in(X104,X105)
| element(X104,X105) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t1_subset])]) ).
fof(i_0_56,plain,
! [X93] :
( ( element(esk7_1(X93),powerset(X93))
| empty(X93) )
& ( ~ empty(esk7_1(X93))
| empty(X93) ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_36])])])]) ).
fof(i_0_57,plain,
! [X117,X118] :
( ~ in(X117,X118)
| ~ empty(X118) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t7_boole])]) ).
fof(i_0_58,plain,
! [X62,X63] : unordered_pair(X62,X63) = unordered_pair(X63,X62),
inference(variable_rename,[status(thm)],[commutativity_k2_tarski]) ).
fof(i_0_59,plain,
! [X97] :
( element(esk10_1(X97),powerset(X97))
& empty(esk10_1(X97)) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[rc2_subset_1])]) ).
fof(i_0_60,plain,
! [X84] : element(esk5_1(X84),X84),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[existence_m1_subset_1])]) ).
fof(i_0_61,plain,
! [X86] : ~ empty(powerset(X86)),
inference(variable_rename,[status(thm)],[i_0_37]) ).
fof(i_0_62,plain,
! [X89] : ~ empty(singleton(X89)),
inference(variable_rename,[status(thm)],[i_0_38]) ).
fof(i_0_63,plain,
! [X119,X120] :
( ~ empty(X119)
| X119 = X120
| ~ empty(X120) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t8_boole])]) ).
fof(i_0_64,plain,
! [X100] : subset(X100,X100),
inference(variable_rename,[status(thm)],[inference(fof_simplification,[status(thm)],[reflexivity_r1_tarski])]) ).
fof(i_0_65,plain,
! [X61] :
( ~ empty(X61)
| relation(X61) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[cc1_relat_1])]) ).
fof(i_0_66,plain,
! [X116] :
( ~ empty(X116)
| X116 = empty_set ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t6_boole])]) ).
fof(i_0_67,plain,
~ empty(esk11_0),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[i_0_39])]) ).
fof(i_0_68,plain,
( ~ empty(esk9_0)
& relation(esk9_0) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[i_0_40])]) ).
fof(i_0_69,plain,
( empty(esk6_0)
& relation(esk6_0) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[rc1_relat_1])]) ).
fof(i_0_70,plain,
empty(esk8_0),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[rc1_xboole_0])]) ).
cnf(i_0_71,plain,
( in(unordered_pair(unordered_pair(X1,esk1_4(X2,X3,X4,X1)),singleton(X1)),X2)
| X4 != relation_inverse_image(X2,X3)
| ~ relation(X2)
| ~ in(X1,X4) ),
inference(rw,[status(thm)],[i_0_41,c_0_42]),
[final] ).
cnf(i_0_72,plain,
( X3 = relation_inverse_image(X1,X2)
| ~ relation(X1)
| ~ in(X4,X2)
| ~ in(esk2_3(X1,X2,X3),X3)
| ~ in(unordered_pair(unordered_pair(esk2_3(X1,X2,X3),X4),singleton(esk2_3(X1,X2,X3))),X1) ),
inference(rw,[status(thm)],[i_0_43,c_0_42]),
[final] ).
cnf(i_0_73,plain,
( X3 = relation_inverse_image(X1,X2)
| in(esk2_3(X1,X2,X3),X3)
| in(unordered_pair(unordered_pair(esk2_3(X1,X2,X3),esk3_3(X1,X2,X3)),singleton(esk2_3(X1,X2,X3))),X1)
| ~ relation(X1) ),
inference(rw,[status(thm)],[i_0_44,c_0_42]),
[final] ).
cnf(i_0_74,plain,
( in(esk1_4(X1,X2,X3,X4),X2)
| ~ in(X4,X3)
| X3 != relation_inverse_image(X1,X2)
| ~ relation(X1) ),
inference(split_conjunct,[status(thm)],[i_0_30]),
[final] ).
cnf(i_0_75,plain,
( in(esk3_3(X1,X2,X3),X2)
| in(esk2_3(X1,X2,X3),X3)
| X3 = relation_inverse_image(X1,X2)
| ~ relation(X1) ),
inference(split_conjunct,[status(thm)],[i_0_30]),
[final] ).
cnf(i_0_76,plain,
( in(X1,X5)
| X5 != relation_inverse_image(X3,X4)
| ~ relation(X3)
| ~ in(X2,X4)
| ~ in(unordered_pair(unordered_pair(X1,X2),singleton(X1)),X3) ),
inference(rw,[status(thm)],[i_0_45,c_0_42]),
[final] ).
cnf(i_0_77,plain,
~ empty(unordered_pair(unordered_pair(X1,X2),singleton(X1))),
inference(rw,[status(thm)],[i_0_46,c_0_42]),
[final] ).
cnf(i_0_78,negated_conjecture,
~ subset(relation_inverse_image(esk14_0,esk12_0),relation_inverse_image(esk14_0,esk13_0)),
inference(split_conjunct,[status(thm)],[i_0_47]),
[final] ).
cnf(i_0_79,plain,
( subset(X1,X2)
| ~ in(esk4_2(X1,X2),X2) ),
inference(split_conjunct,[status(thm)],[i_0_48]),
[final] ).
cnf(i_0_80,plain,
( element(X1,X3)
| ~ in(X1,X2)
| ~ element(X2,powerset(X3)) ),
inference(split_conjunct,[status(thm)],[i_0_49]),
[final] ).
cnf(i_0_81,plain,
( ~ in(X1,X2)
| ~ element(X2,powerset(X3))
| ~ empty(X3) ),
inference(split_conjunct,[status(thm)],[i_0_50]),
[final] ).
cnf(i_0_82,plain,
( in(X3,X2)
| ~ subset(X1,X2)
| ~ in(X3,X1) ),
inference(split_conjunct,[status(thm)],[i_0_48]),
[final] ).
cnf(i_0_83,plain,
( in(esk4_2(X1,X2),X1)
| subset(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_48]),
[final] ).
cnf(i_0_84,plain,
~ empty(unordered_pair(X1,X2)),
inference(split_conjunct,[status(thm)],[i_0_51]),
[final] ).
cnf(i_0_85,plain,
( subset(X1,X2)
| ~ element(X1,powerset(X2)) ),
inference(split_conjunct,[status(thm)],[i_0_52]),
[final] ).
cnf(i_0_86,plain,
( ~ in(X1,X2)
| ~ in(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_53]),
[final] ).
cnf(i_0_87,plain,
( element(X1,powerset(X2))
| ~ subset(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_52]),
[final] ).
cnf(i_0_88,plain,
( empty(X2)
| in(X1,X2)
| ~ element(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_54]),
[final] ).
cnf(i_0_89,plain,
( element(X1,X2)
| ~ in(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_55]),
[final] ).
cnf(i_0_90,plain,
( element(esk7_1(X1),powerset(X1))
| empty(X1) ),
inference(split_conjunct,[status(thm)],[i_0_56]),
[final] ).
cnf(i_0_91,plain,
( ~ in(X1,X2)
| ~ empty(X2) ),
inference(split_conjunct,[status(thm)],[i_0_57]),
[final] ).
cnf(i_0_92,plain,
unordered_pair(X1,X2) = unordered_pair(X2,X1),
inference(split_conjunct,[status(thm)],[i_0_58]),
[final] ).
cnf(i_0_93,plain,
element(esk10_1(X1),powerset(X1)),
inference(split_conjunct,[status(thm)],[i_0_59]),
[final] ).
cnf(i_0_94,plain,
( empty(X1)
| ~ empty(esk7_1(X1)) ),
inference(split_conjunct,[status(thm)],[i_0_56]),
[final] ).
cnf(i_0_95,plain,
element(esk5_1(X1),X1),
inference(split_conjunct,[status(thm)],[i_0_60]),
[final] ).
cnf(i_0_96,plain,
~ empty(powerset(X1)),
inference(split_conjunct,[status(thm)],[i_0_61]),
[final] ).
cnf(i_0_97,plain,
~ empty(singleton(X1)),
inference(split_conjunct,[status(thm)],[i_0_62]),
[final] ).
cnf(i_0_98,plain,
( X1 = X2
| ~ empty(X1)
| ~ empty(X2) ),
inference(split_conjunct,[status(thm)],[i_0_63]),
[final] ).
cnf(i_0_99,plain,
subset(X1,X1),
inference(split_conjunct,[status(thm)],[i_0_64]),
[final] ).
cnf(i_0_100,plain,
( relation(X1)
| ~ empty(X1) ),
inference(split_conjunct,[status(thm)],[i_0_65]),
[final] ).
cnf(i_0_101,negated_conjecture,
subset(esk12_0,esk13_0),
inference(split_conjunct,[status(thm)],[i_0_47]),
[final] ).
cnf(i_0_102,plain,
empty(esk10_1(X1)),
inference(split_conjunct,[status(thm)],[i_0_59]),
[final] ).
cnf(i_0_103,plain,
( X1 = empty_set
| ~ empty(X1) ),
inference(split_conjunct,[status(thm)],[i_0_66]),
[final] ).
cnf(i_0_104,plain,
~ empty(esk11_0),
inference(split_conjunct,[status(thm)],[i_0_67]),
[final] ).
cnf(i_0_105,plain,
~ empty(esk9_0),
inference(split_conjunct,[status(thm)],[i_0_68]),
[final] ).
cnf(i_0_106,negated_conjecture,
relation(esk14_0),
inference(split_conjunct,[status(thm)],[i_0_47]),
[final] ).
cnf(i_0_107,plain,
relation(esk9_0),
inference(split_conjunct,[status(thm)],[i_0_68]),
[final] ).
cnf(i_0_108,plain,
relation(esk6_0),
inference(split_conjunct,[status(thm)],[i_0_69]),
[final] ).
cnf(i_0_109,plain,
relation(empty_set),
inference(split_conjunct,[status(thm)],[fc4_relat_1]),
[final] ).
cnf(i_0_110,plain,
empty(esk8_0),
inference(split_conjunct,[status(thm)],[i_0_70]),
[final] ).
cnf(i_0_111,plain,
empty(esk6_0),
inference(split_conjunct,[status(thm)],[i_0_69]),
[final] ).
cnf(i_0_112,plain,
empty(empty_set),
inference(split_conjunct,[status(thm)],[fc4_relat_1]),
[final] ).
cnf(i_0_113,plain,
empty(empty_set),
inference(split_conjunct,[status(thm)],[fc1_xboole_0]),
[final] ).
cnf(i_0_114,axiom,
X1 = X1 ).
cnf(i_0_115,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_116,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_117,axiom,
( X1 != X2
| unordered_pair(X1,X3) = unordered_pair(X2,X3) ) ).
cnf(i_0_118,axiom,
( X1 != X2
| unordered_pair(X3,X1) = unordered_pair(X3,X2) ) ).
cnf(i_0_119,axiom,
( X1 != X2
| relation_inverse_image(X1,X3) = relation_inverse_image(X2,X3) ) ).
cnf(i_0_120,axiom,
( X1 != X2
| relation_inverse_image(X3,X1) = relation_inverse_image(X3,X2) ) ).
cnf(i_0_121,axiom,
( X1 != X2
| ~ in(X1,X3)
| in(X2,X3) ) ).
cnf(i_0_122,axiom,
( X1 != X2
| ~ in(X3,X1)
| in(X3,X2) ) ).
cnf(i_0_123,axiom,
( X1 != X2
| ~ relation(X1)
| relation(X2) ) ).
cnf(i_0_124,axiom,
( X1 != X2
| ~ empty(X1)
| empty(X2) ) ).
cnf(i_0_125,axiom,
( X1 != X2
| ~ subset(X1,X3)
| subset(X2,X3) ) ).
cnf(i_0_126,axiom,
( X1 != X2
| ~ subset(X3,X1)
| subset(X3,X2) ) ).
cnf(i_0_127,axiom,
( X1 != X2
| ~ element(X1,X3)
| element(X2,X3) ) ).
cnf(i_0_128,axiom,
( X1 != X2
| ~ element(X3,X1)
| element(X3,X2) ) ).
cnf(i_0_2157,plain,
~ in(X1,relation_inverse_image(relation_inverse_image(esk6_0,X2),X3)),
inference(scs_inference,[],[i_0_2084,i_0_2014,i_0_1948,i_0_2058,i_0_2032,i_0_2103,i_0_2098,i_0_2130,i_0_2141,i_0_1857,i_0_2064,i_0_2006,i_0_1930,i_0_1832,i_0_229,i_0_667,i_0_1508,i_0_1913,i_0_1872,i_0_1915,i_0_1771,i_0_1440,i_0_226,i_0_2155,i_0_109,i_0_95,i_0_107,i_0_99,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_128,i_0_127,i_0_80,i_0_81,i_0_88,i_0_126,i_0_116,i_0_124,i_0_122,i_0_125,i_0_74,i_0_73,i_0_71]) ).
cnf(i_0_2168,plain,
~ subset(powerset(X1),relation_inverse_image(esk14_0,relation_inverse_image(empty_set,X2))),
inference(scs_inference,[],[i_0_2134,i_0_87]) ).
cnf(i_0_2170,plain,
subset(esk7_1(esk7_1(esk7_1(esk13_0))),esk7_1(esk7_1(esk13_0))),
inference(scs_inference,[],[i_0_2134,i_0_1990,i_0_87,i_0_85]) ).
cnf(i_0_2172,plain,
~ in(powerset(X1),powerset(relation_inverse_image(esk10_1(esk8_0),X2))),
inference(scs_inference,[],[i_0_2118,i_0_2134,i_0_1990,i_0_87,i_0_85,i_0_89]) ).
cnf(i_0_2174,plain,
in(esk4_2(unordered_pair(X1,X2),relation_inverse_image(esk8_0,X3)),unordered_pair(X1,X2)),
inference(scs_inference,[],[i_0_2118,i_0_2134,i_0_1990,i_0_271,i_0_87,i_0_85,i_0_89,i_0_83]) ).
cnf(i_0_2178,plain,
relation_inverse_image(relation_inverse_image(empty_set,X1),X2) != esk9_0,
inference(scs_inference,[],[i_0_2142,i_0_2146,i_0_2118,i_0_2134,i_0_1990,i_0_271,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115]) ).
cnf(i_0_2180,plain,
relation_inverse_image(esk14_0,relation_inverse_image(empty_set,X1)) != esk14_0,
inference(scs_inference,[],[i_0_2142,i_0_2146,i_0_2118,i_0_2134,i_0_2018,i_0_2021,i_0_1990,i_0_271,i_0_1950,i_0_1365,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_128,i_0_127]) ).
cnf(i_0_2190,plain,
~ in(X1,relation_inverse_image(relation_inverse_image(esk6_0,X2),X3)),
inference(rename_variables,[],[i_0_2157]) ).
cnf(i_0_2203,plain,
~ in(X1,relation_inverse_image(relation_inverse_image(esk6_0,X2),X3)),
inference(rename_variables,[],[i_0_2157]) ).
cnf(i_0_2207,plain,
~ in(X1,relation_inverse_image(relation_inverse_image(esk6_0,X2),X3)),
inference(rename_variables,[],[i_0_2157]) ).
cnf(i_0_2215,plain,
~ in(X1,relation_inverse_image(relation_inverse_image(esk6_0,X2),X3)),
inference(rename_variables,[],[i_0_2157]) ).
cnf(i_0_2248,plain,
~ in(X1,relation_inverse_image(relation_inverse_image(esk6_0,X2),X3)),
inference(rename_variables,[],[i_0_2157]) ).
cnf(i_0_2261,plain,
in(esk4_2(unordered_pair(X1,X2),relation_inverse_image(esk8_0,X3)),unordered_pair(X1,X2)),
inference(rename_variables,[],[i_0_2174]) ).
cnf(i_0_2268,plain,
~ in(X1,relation_inverse_image(relation_inverse_image(esk6_0,X2),X3)),
inference(rename_variables,[],[i_0_2157]) ).
cnf(i_0_2271,plain,
~ in(X1,relation_inverse_image(relation_inverse_image(esk6_0,X2),X3)),
inference(rename_variables,[],[i_0_2157]) ).
cnf(i_0_2278,plain,
~ in(X1,relation_inverse_image(relation_inverse_image(esk6_0,X2),X3)),
inference(rename_variables,[],[i_0_2157]) ).
cnf(i_0_2282,plain,
in(esk4_2(unordered_pair(X1,X2),relation_inverse_image(esk8_0,X3)),unordered_pair(X1,X2)),
inference(rename_variables,[],[i_0_2174]) ).
cnf(i_0_2529,plain,
~ in(X1,relation_inverse_image(relation_inverse_image(esk6_0,X2),X3)),
inference(rename_variables,[],[i_0_2157]) ).
cnf(i_0_2536,plain,
~ in(X1,relation_inverse_image(relation_inverse_image(esk6_0,X2),X3)),
inference(rename_variables,[],[i_0_2157]) ).
cnf(i_0_2805,plain,
~ in(X1,relation_inverse_image(relation_inverse_image(esk6_0,X2),X3)),
inference(rename_variables,[],[i_0_2157]) ).
cnf(i_0_2189,plain,
empty(relation_inverse_image(relation_inverse_image(esk6_0,empty_set),empty_set)),
inference(scs_inference,[],[i_0_1823,i_0_2157,i_0_1879,i_0_2144,i_0_2142,i_0_2146,i_0_2185,i_0_2118,i_0_2134,i_0_2018,i_0_2021,i_0_1990,i_0_271,i_0_1950,i_0_1926,i_0_1711,i_0_1365,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_128,i_0_127,i_0_82,i_0_80,i_0_81,i_0_88]) ).
cnf(i_0_2195,plain,
empty_set != esk7_1(esk7_1(esk7_1(esk13_0))),
inference(scs_inference,[],[i_0_1823,i_0_2027,i_0_2157,i_0_1879,i_0_2144,i_0_2142,i_0_2111,i_0_2146,i_0_2185,i_0_2118,i_0_2134,i_0_2018,i_0_2021,i_0_2089,i_0_1990,i_0_271,i_0_643,i_0_1950,i_0_1926,i_0_1711,i_0_1365,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_128,i_0_127,i_0_82,i_0_80,i_0_81,i_0_88,i_0_126,i_0_116]) ).
cnf(i_0_2196,plain,
relation_inverse_image(esk9_0,relation_inverse_image(esk6_0,X1)) != esk7_1(esk7_1(esk14_0)),
inference(scs_inference,[],[i_0_1823,i_0_2027,i_0_2157,i_0_1879,i_0_2144,i_0_2142,i_0_2111,i_0_2146,i_0_2185,i_0_2118,i_0_2134,i_0_2018,i_0_2021,i_0_2089,i_0_1990,i_0_271,i_0_643,i_0_1950,i_0_1625,i_0_1926,i_0_1711,i_0_1365,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_128,i_0_127,i_0_82,i_0_80,i_0_81,i_0_88,i_0_126,i_0_116,i_0_124]) ).
cnf(i_0_2205,plain,
relation_inverse_image(relation_inverse_image(esk6_0,X1),X2) = relation_inverse_image(esk10_1(X3),X4),
inference(scs_inference,[],[i_0_1823,i_0_2027,i_0_2157,i_0_2190,i_0_2203,i_0_1879,i_0_2144,i_0_2142,i_0_2111,i_0_2146,i_0_2185,i_0_2118,i_0_2134,i_0_2018,i_0_2021,i_0_2154,i_0_2089,i_0_1990,i_0_271,i_0_643,i_0_1509,i_0_2084,i_0_1889,i_0_1950,i_0_1625,i_0_1926,i_0_1711,i_0_1365,i_0_268,i_0_177,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_128,i_0_127,i_0_82,i_0_80,i_0_81,i_0_88,i_0_126,i_0_116,i_0_124,i_0_122,i_0_125,i_0_74,i_0_73]) ).
cnf(i_0_2210,plain,
unordered_pair(empty_set,X1) != relation_inverse_image(esk6_0,X2),
inference(scs_inference,[],[i_0_1823,i_0_2027,i_0_2157,i_0_2190,i_0_2203,i_0_1879,i_0_2144,i_0_2142,i_0_2111,i_0_2146,i_0_2185,i_0_2198,i_0_2118,i_0_2134,i_0_2018,i_0_2021,i_0_2154,i_0_2089,i_0_1990,i_0_271,i_0_643,i_0_1509,i_0_2084,i_0_1889,i_0_1950,i_0_1625,i_0_1926,i_0_1711,i_0_1365,i_0_175,i_0_268,i_0_177,i_0_108,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_128,i_0_127,i_0_82,i_0_80,i_0_81,i_0_88,i_0_126,i_0_116,i_0_124,i_0_122,i_0_125,i_0_74,i_0_73,i_0_71]) ).
cnf(i_0_2218,plain,
~ empty(esk7_1(relation_inverse_image(esk14_0,esk12_0))),
inference(scs_inference,[],[i_0_1823,i_0_2027,i_0_2157,i_0_2190,i_0_2203,i_0_2207,i_0_1879,i_0_2144,i_0_2142,i_0_2111,i_0_2146,i_0_2185,i_0_2198,i_0_2118,i_0_2134,i_0_2018,i_0_2021,i_0_2154,i_0_2089,i_0_1990,i_0_523,i_0_271,i_0_643,i_0_1509,i_0_1416,i_0_2084,i_0_1889,i_0_1950,i_0_1625,i_0_1926,i_0_1711,i_0_1365,i_0_175,i_0_268,i_0_177,i_0_2206,i_0_108,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_128,i_0_127,i_0_82,i_0_80,i_0_81,i_0_88,i_0_126,i_0_116,i_0_124,i_0_122,i_0_125,i_0_74,i_0_73,i_0_71,i_0_75,i_0_94]) ).
cnf(i_0_2237,plain,
~ in(unordered_pair(X1,X2),esk4_2(unordered_pair(X1,X2),relation_inverse_image(esk8_0,X3))),
inference(scs_inference,[],[i_0_2174,i_0_2200,i_0_2168,i_0_2187,i_0_288,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86]) ).
cnf(i_0_2239,plain,
relation_inverse_image(esk6_0,X1) != unordered_pair(empty_set,X2),
inference(scs_inference,[],[i_0_2210,i_0_2174,i_0_2200,i_0_2168,i_0_2187,i_0_288,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115]) ).
cnf(i_0_2241,plain,
relation_inverse_image(relation_inverse_image(esk6_0,X1),X2) = relation_inverse_image(esk10_1(X3),X4),
inference(rename_variables,[],[i_0_2205]) ).
cnf(i_0_2243,plain,
element(relation_inverse_image(empty_set,X1),powerset(relation_inverse_image(empty_set,X2))),
inference(scs_inference,[],[i_0_2210,i_0_2174,i_0_2200,i_0_2168,i_0_2205,i_0_2116,i_0_2187,i_0_288,i_0_2042,i_0_1654,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_128,i_0_127]) ).
cnf(i_0_2247,plain,
empty(relation_inverse_image(relation_inverse_image(esk6_0,X1),empty_set)),
inference(scs_inference,[],[i_0_2210,i_0_2174,i_0_2200,i_0_2189,i_0_2168,i_0_2205,i_0_2116,i_0_2187,i_0_288,i_0_2042,i_0_2157,i_0_1654,i_0_2242,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_128,i_0_127,i_0_81,i_0_88]) ).
cnf(i_0_2256,plain,
relation_inverse_image(relation_inverse_image(esk6_0,X1),X2) = relation_inverse_image(esk10_1(X3),X4),
inference(rename_variables,[],[i_0_2205]) ).
cnf(i_0_2279,plain,
unordered_pair(empty_set,X1) != relation_inverse_image(esk6_0,X2),
inference(rename_variables,[],[i_0_2210]) ).
cnf(i_0_2254,plain,
esk14_0 != relation_inverse_image(relation_inverse_image(esk6_0,X1),X2),
inference(scs_inference,[],[i_0_2210,i_0_2174,i_0_2200,i_0_2189,i_0_2168,i_0_2205,i_0_2241,i_0_2116,i_0_2037,i_0_2187,i_0_2095,i_0_288,i_0_2042,i_0_2157,i_0_1513,i_0_1654,i_0_2242,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_128,i_0_127,i_0_81,i_0_88,i_0_126,i_0_116]) ).
cnf(i_0_2257,plain,
empty(relation_inverse_image(esk14_0,relation_inverse_image(esk10_1(esk8_0),X1))),
inference(scs_inference,[],[i_0_2210,i_0_2174,i_0_2200,i_0_2189,i_0_2168,i_0_2205,i_0_2241,i_0_2116,i_0_2037,i_0_2187,i_0_2095,i_0_288,i_0_2042,i_0_2157,i_0_1513,i_0_343,i_0_1654,i_0_2242,i_0_1666,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_128,i_0_127,i_0_81,i_0_88,i_0_126,i_0_116,i_0_124]) ).
cnf(i_0_2270,plain,
relation_inverse_image(relation_inverse_image(esk6_0,X1),X2) = relation_inverse_image(esk6_0,X3),
inference(scs_inference,[],[i_0_2210,i_0_2174,i_0_2261,i_0_2200,i_0_2189,i_0_2168,i_0_2205,i_0_2241,i_0_2116,i_0_2176,i_0_2037,i_0_2222,i_0_2260,i_0_2263,i_0_2187,i_0_2095,i_0_288,i_0_2042,i_0_2157,i_0_2248,i_0_2268,i_0_1513,i_0_343,i_0_1401,i_0_1654,i_0_2242,i_0_1666,i_0_175,i_0_108,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_128,i_0_127,i_0_81,i_0_88,i_0_126,i_0_116,i_0_124,i_0_122,i_0_121,i_0_125,i_0_74,i_0_73]) ).
cnf(i_0_2274,plain,
unordered_pair(X1,X2) != relation_inverse_image(esk6_0,X3),
inference(scs_inference,[],[i_0_2210,i_0_2174,i_0_2261,i_0_2200,i_0_2189,i_0_2168,i_0_2205,i_0_2241,i_0_2116,i_0_2176,i_0_2037,i_0_2222,i_0_2260,i_0_2263,i_0_2187,i_0_2095,i_0_288,i_0_2042,i_0_2157,i_0_2248,i_0_2268,i_0_1513,i_0_343,i_0_1401,i_0_1654,i_0_2242,i_0_1666,i_0_175,i_0_2272,i_0_108,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_128,i_0_127,i_0_81,i_0_88,i_0_126,i_0_116,i_0_124,i_0_122,i_0_121,i_0_125,i_0_74,i_0_73,i_0_71]) ).
cnf(i_0_2287,plain,
subset(esk7_1(relation_inverse_image(esk14_0,esk12_0)),relation_inverse_image(esk14_0,esk12_0)),
inference(scs_inference,[],[i_0_2220,i_0_2245,i_0_87,i_0_85]) ).
cnf(i_0_2291,plain,
in(esk4_2(singleton(X1),relation_inverse_image(esk6_0,X2)),singleton(X1)),
inference(scs_inference,[],[i_0_2220,i_0_2245,i_0_668,i_0_87,i_0_85,i_0_89,i_0_83]) ).
cnf(i_0_2370,plain,
~ in(unordered_pair(X1,X2),esk4_2(unordered_pair(X1,X2),relation_inverse_image(esk8_0,X3))),
inference(rename_variables,[],[i_0_2237]) ).
cnf(i_0_2750,plain,
~ element(singleton(X1),powerset(relation_inverse_image(esk8_0,X2))),
inference(scs_inference,[],[i_0_2251,i_0_554,i_0_87,i_0_85]) ).
cnf(i_0_2295,plain,
relation_inverse_image(esk6_0,X1) != unordered_pair(X2,X3),
inference(scs_inference,[],[i_0_2274,i_0_2277,i_0_2220,i_0_2245,i_0_668,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115]) ).
cnf(i_0_2298,plain,
element(relation_inverse_image(esk6_0,X1),powerset(relation_inverse_image(empty_set,empty_set))),
inference(scs_inference,[],[i_0_2274,i_0_2281,i_0_2270,i_0_2277,i_0_2220,i_0_2004,i_0_2245,i_0_668,i_0_1441,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_128,i_0_127]) ).
cnf(i_0_2299,plain,
relation_inverse_image(relation_inverse_image(esk6_0,X1),X2) = relation_inverse_image(esk6_0,X3),
inference(rename_variables,[],[i_0_2270]) ).
cnf(i_0_2309,plain,
relation_inverse_image(relation_inverse_image(esk6_0,X1),X2) = relation_inverse_image(esk6_0,X3),
inference(rename_variables,[],[i_0_2270]) ).
cnf(i_0_2335,plain,
esk14_0 != relation_inverse_image(relation_inverse_image(esk6_0,X1),X2),
inference(rename_variables,[],[i_0_2254]) ).
cnf(i_0_2323,plain,
in(esk2_3(esk6_0,X1,unordered_pair(X2,X3)),unordered_pair(X2,X3)),
inference(scs_inference,[],[i_0_2274,i_0_2281,i_0_2270,i_0_2299,i_0_2218,i_0_2247,i_0_2277,i_0_2220,i_0_2004,i_0_2235,i_0_2223,i_0_2317,i_0_2224,i_0_2225,i_0_2245,i_0_2172,i_0_2264,i_0_2149,i_0_1605,i_0_668,i_0_1441,i_0_175,i_0_95,i_0_108,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_128,i_0_127,i_0_80,i_0_81,i_0_88,i_0_126,i_0_116,i_0_124,i_0_122,i_0_121,i_0_125,i_0_73]) ).
cnf(i_0_2329,plain,
in(esk2_3(empty_set,relation_inverse_image(relation_inverse_image(empty_set,X1),X2),esk9_0),esk9_0),
inference(scs_inference,[],[i_0_2274,i_0_2281,i_0_2270,i_0_2299,i_0_2218,i_0_2247,i_0_2277,i_0_2220,i_0_2004,i_0_2235,i_0_2223,i_0_2317,i_0_2224,i_0_2312,i_0_2225,i_0_2245,i_0_2172,i_0_2264,i_0_2039,i_0_2149,i_0_1605,i_0_668,i_0_1996,i_0_1441,i_0_226,i_0_175,i_0_95,i_0_109,i_0_108,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_128,i_0_127,i_0_80,i_0_81,i_0_88,i_0_126,i_0_116,i_0_124,i_0_122,i_0_121,i_0_125,i_0_73,i_0_71,i_0_75]) ).
cnf(i_0_2333,plain,
relation_inverse_image(relation_inverse_image(esk6_0,X1),empty_set) = empty_set,
inference(scs_inference,[],[i_0_2274,i_0_2281,i_0_2270,i_0_2299,i_0_2218,i_0_2247,i_0_2277,i_0_2220,i_0_2004,i_0_2235,i_0_2223,i_0_2317,i_0_2224,i_0_2312,i_0_2225,i_0_2245,i_0_2172,i_0_2264,i_0_2039,i_0_2149,i_0_1605,i_0_668,i_0_1996,i_0_1441,i_0_226,i_0_175,i_0_95,i_0_109,i_0_108,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_128,i_0_127,i_0_80,i_0_81,i_0_88,i_0_126,i_0_116,i_0_124,i_0_122,i_0_121,i_0_125,i_0_73,i_0_71,i_0_75,i_0_103]) ).
cnf(i_0_2339,plain,
~ element(esk9_0,powerset(relation_inverse_image(esk8_0,X1))),
inference(scs_inference,[],[i_0_2308,i_0_608,i_0_87,i_0_85]) ).
cnf(i_0_2345,plain,
~ in(singleton(X1),esk4_2(singleton(X1),relation_inverse_image(esk6_0,X2))),
inference(scs_inference,[],[i_0_2291,i_0_2308,i_0_2285,i_0_2303,i_0_608,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86]) ).
cnf(i_0_2347,plain,
esk14_0 != relation_inverse_image(esk14_0,relation_inverse_image(empty_set,X1)),
inference(scs_inference,[],[i_0_2291,i_0_2308,i_0_2285,i_0_2180,i_0_2303,i_0_608,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115]) ).
cnf(i_0_2353,plain,
in(esk2_3(esk6_0,X1,unordered_pair(X2,X3)),unordered_pair(X2,X3)),
inference(rename_variables,[],[i_0_2323]) ).
cnf(i_0_2357,plain,
in(esk2_3(esk6_0,X1,esk12_0),esk13_0),
inference(scs_inference,[],[i_0_1839,i_0_2291,i_0_2323,i_0_2308,i_0_1373,i_0_2285,i_0_2180,i_0_2303,i_0_2257,i_0_1561,i_0_1776,i_0_1498,i_0_608,i_0_1444,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_128,i_0_127,i_0_80,i_0_81,i_0_88]) ).
cnf(i_0_2361,plain,
empty_set != esk7_1(relation_inverse_image(esk14_0,esk12_0)),
inference(scs_inference,[],[i_0_1839,i_0_2291,i_0_2323,i_0_2308,i_0_1373,i_0_2285,i_0_2180,i_0_2333,i_0_2314,i_0_2303,i_0_2257,i_0_1971,i_0_1561,i_0_1776,i_0_1637,i_0_1498,i_0_608,i_0_1444,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_128,i_0_127,i_0_80,i_0_81,i_0_88,i_0_126,i_0_116]) ).
cnf(i_0_2363,plain,
empty(relation_inverse_image(esk14_0,relation_inverse_image(esk6_0,X1))),
inference(scs_inference,[],[i_0_1839,i_0_2291,i_0_2323,i_0_2308,i_0_1373,i_0_2285,i_0_2180,i_0_2333,i_0_2314,i_0_2303,i_0_2257,i_0_1971,i_0_1561,i_0_1776,i_0_1637,i_0_1498,i_0_1339,i_0_608,i_0_1444,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_128,i_0_127,i_0_80,i_0_81,i_0_88,i_0_126,i_0_116,i_0_124]) ).
cnf(i_0_2367,plain,
in(esk2_3(esk6_0,X1,unordered_pair(X2,X3)),unordered_pair(X2,X3)),
inference(rename_variables,[],[i_0_2323]) ).
cnf(i_0_2516,plain,
relation_inverse_image(relation_inverse_image(esk6_0,X1),empty_set) = empty_set,
inference(rename_variables,[],[i_0_2333]) ).
cnf(i_0_2376,plain,
singleton(X1) != relation_inverse_image(esk10_1(X2),X3),
inference(scs_inference,[],[i_0_1839,i_0_2291,i_0_2323,i_0_2353,i_0_2308,i_0_1373,i_0_2285,i_0_2237,i_0_2180,i_0_2333,i_0_2314,i_0_2326,i_0_2303,i_0_2257,i_0_1971,i_0_1704,i_0_1561,i_0_1776,i_0_1571,i_0_2366,i_0_1637,i_0_1498,i_0_1339,i_0_608,i_0_1444,i_0_268,i_0_177,i_0_99,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_128,i_0_127,i_0_80,i_0_81,i_0_88,i_0_126,i_0_116,i_0_124,i_0_122,i_0_121,i_0_125,i_0_74,i_0_71]) ).
cnf(i_0_2390,plain,
~ in(esk9_0,powerset(relation_inverse_image(esk8_0,X1))),
inference(scs_inference,[],[i_0_2339,i_0_2079,i_0_1837,i_0_87,i_0_85,i_0_89]) ).
cnf(i_0_2392,plain,
in(esk4_2(esk12_0,relation_inverse_image(empty_set,X1)),esk12_0),
inference(scs_inference,[],[i_0_2339,i_0_2079,i_0_1837,i_0_635,i_0_87,i_0_85,i_0_89,i_0_83]) ).
cnf(i_0_2394,plain,
~ in(esk13_0,esk2_3(esk6_0,X1,esk12_0)),
inference(scs_inference,[],[i_0_2357,i_0_2339,i_0_2079,i_0_1837,i_0_635,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86]) ).
cnf(i_0_2396,plain,
esk7_1(relation_inverse_image(esk14_0,esk12_0)) != empty_set,
inference(scs_inference,[],[i_0_2357,i_0_2361,i_0_2339,i_0_2079,i_0_1837,i_0_635,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115]) ).
cnf(i_0_2397,plain,
~ element(esk13_0,powerset(relation_inverse_image(esk14_0,relation_inverse_image(esk6_0,X1)))),
inference(scs_inference,[],[i_0_2357,i_0_2363,i_0_2361,i_0_2339,i_0_2079,i_0_1837,i_0_635,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_81]) ).
cnf(i_0_2798,plain,
~ subset(singleton(X1),relation_inverse_image(esk14_0,relation_inverse_image(esk10_1(esk8_0),X2))),
inference(scs_inference,[],[i_0_2355,i_0_87]) ).
cnf(i_0_2425,plain,
esk11_0 != relation_inverse_image(empty_set,X1),
inference(scs_inference,[],[i_0_2357,i_0_2363,i_0_2361,i_0_2339,i_0_2139,i_0_2341,i_0_2079,i_0_2311,i_0_2380,i_0_2371,i_0_1837,i_0_1895,i_0_1643,i_0_2213,i_0_1367,i_0_1450,i_0_599,i_0_573,i_0_2326,i_0_2405,i_0_2414,i_0_1930,i_0_1993,i_0_635,i_0_1711,i_0_226,i_0_95,i_0_109,i_0_106,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_81,i_0_128,i_0_127,i_0_88,i_0_126,i_0_116,i_0_124,i_0_122,i_0_121,i_0_125,i_0_131,i_0_74,i_0_71]) ).
cnf(i_0_2430,plain,
singleton(X1) != relation_inverse_image(esk10_1(X2),X3),
inference(rename_variables,[],[i_0_2376]) ).
cnf(i_0_2432,plain,
~ empty(esk7_1(esk4_2(esk14_0,powerset(relation_inverse_image(esk8_0,X1))))),
inference(scs_inference,[],[i_0_2357,i_0_2376,i_0_2363,i_0_2361,i_0_2339,i_0_2139,i_0_2341,i_0_2079,i_0_2311,i_0_2380,i_0_2371,i_0_1837,i_0_1895,i_0_1643,i_0_2213,i_0_1367,i_0_1450,i_0_599,i_0_573,i_0_2326,i_0_2405,i_0_2414,i_0_2423,i_0_1930,i_0_1993,i_0_635,i_0_1711,i_0_226,i_0_95,i_0_109,i_0_177,i_0_106,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_81,i_0_128,i_0_127,i_0_88,i_0_126,i_0_116,i_0_124,i_0_122,i_0_121,i_0_125,i_0_131,i_0_74,i_0_71,i_0_75,i_0_94]) ).
cnf(i_0_2440,plain,
in(esk5_1(esk7_1(relation_inverse_image(esk14_0,esk12_0))),relation_inverse_image(esk14_0,esk12_0)),
inference(scs_inference,[],[i_0_2357,i_0_2287,i_0_2376,i_0_2363,i_0_2361,i_0_2339,i_0_2139,i_0_2341,i_0_2079,i_0_2311,i_0_2380,i_0_2371,i_0_1837,i_0_1895,i_0_1643,i_0_2305,i_0_2213,i_0_1367,i_0_1450,i_0_599,i_0_573,i_0_2326,i_0_2405,i_0_2414,i_0_2423,i_0_1930,i_0_1993,i_0_635,i_0_2218,i_0_1711,i_0_226,i_0_95,i_0_109,i_0_177,i_0_106,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_81,i_0_128,i_0_127,i_0_88,i_0_126,i_0_116,i_0_124,i_0_122,i_0_121,i_0_125,i_0_131,i_0_74,i_0_71,i_0_75,i_0_94,i_0_90,i_0_117,i_0_118,i_0_119,i_0_120,i_0_82]) ).
cnf(i_0_2450,plain,
~ element(esk12_0,powerset(relation_inverse_image(esk6_0,X1))),
inference(scs_inference,[],[i_0_2408,i_0_520,i_0_87,i_0_85]) ).
cnf(i_0_2452,plain,
~ in(esk13_0,powerset(relation_inverse_image(esk14_0,relation_inverse_image(esk6_0,X1)))),
inference(scs_inference,[],[i_0_2408,i_0_2397,i_0_520,i_0_87,i_0_85,i_0_89]) ).
cnf(i_0_2456,plain,
~ in(esk12_0,esk4_2(esk12_0,relation_inverse_image(empty_set,X1))),
inference(scs_inference,[],[i_0_2408,i_0_2386,i_0_2392,i_0_2397,i_0_520,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86]) ).
cnf(i_0_2458,plain,
relation_inverse_image(empty_set,X1) != esk11_0,
inference(scs_inference,[],[i_0_2425,i_0_2408,i_0_2386,i_0_2392,i_0_2397,i_0_520,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115]) ).
cnf(i_0_2465,plain,
element(relation_inverse_image(esk8_0,X1),powerset(relation_inverse_image(empty_set,X2))),
inference(scs_inference,[],[i_0_2425,i_0_2408,i_0_2386,i_0_2392,i_0_1952,i_0_2129,i_0_2404,i_0_2397,i_0_2420,i_0_516,i_0_520,i_0_1508,i_0_1419,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_81,i_0_88,i_0_128,i_0_127]) ).
cnf(i_0_2471,plain,
empty(relation_inverse_image(esk9_0,relation_inverse_image(empty_set,X1))),
inference(scs_inference,[],[i_0_2425,i_0_2408,i_0_2396,i_0_2386,i_0_2392,i_0_1952,i_0_2129,i_0_2404,i_0_2397,i_0_2417,i_0_2420,i_0_1633,i_0_776,i_0_516,i_0_1849,i_0_520,i_0_1508,i_0_2363,i_0_1419,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_81,i_0_88,i_0_128,i_0_127,i_0_126,i_0_116,i_0_124]) ).
cnf(i_0_2501,plain,
in(esk4_2(unordered_pair(X1,X2),relation_inverse_image(esk6_0,X3)),unordered_pair(X1,X2)),
inference(scs_inference,[],[i_0_2454,i_0_2434,i_0_2300,i_0_579,i_0_87,i_0_85,i_0_89,i_0_83]) ).
cnf(i_0_2514,plain,
~ element(esk12_0,powerset(relation_inverse_image(esk6_0,X1))),
inference(rename_variables,[],[i_0_2450]) ).
cnf(i_0_2562,plain,
element(relation_inverse_image(esk8_0,X1),powerset(relation_inverse_image(empty_set,X2))),
inference(rename_variables,[],[i_0_2465]) ).
cnf(i_0_2571,plain,
in(esk4_2(unordered_pair(X1,X2),relation_inverse_image(esk6_0,X3)),unordered_pair(X1,X2)),
inference(rename_variables,[],[i_0_2501]) ).
cnf(i_0_2508,plain,
~ element(esk14_0,powerset(relation_inverse_image(esk9_0,relation_inverse_image(empty_set,X1)))),
inference(scs_inference,[],[i_0_2471,i_0_2454,i_0_2410,i_0_2482,i_0_2434,i_0_2300,i_0_1500,i_0_579,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_80,i_0_81]) ).
cnf(i_0_2512,plain,
powerset(esk13_0) != powerset(relation_inverse_image(esk6_0,X1)),
inference(scs_inference,[],[i_0_2471,i_0_2450,i_0_2454,i_0_2410,i_0_2482,i_0_2434,i_0_2300,i_0_2488,i_0_1500,i_0_579,i_0_1432,i_0_1365,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_80,i_0_81,i_0_88,i_0_128]) ).
cnf(i_0_2513,plain,
relation_inverse_image(relation_inverse_image(esk6_0,empty_set),X1) != esk12_0,
inference(scs_inference,[],[i_0_2471,i_0_2450,i_0_2337,i_0_2454,i_0_2410,i_0_2482,i_0_2434,i_0_2300,i_0_2488,i_0_1500,i_0_579,i_0_1432,i_0_1365,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_80,i_0_81,i_0_88,i_0_128,i_0_127]) ).
cnf(i_0_2515,plain,
subset(relation_inverse_image(relation_inverse_image(esk6_0,empty_set),empty_set),empty_set),
inference(scs_inference,[],[i_0_2471,i_0_2450,i_0_2337,i_0_2454,i_0_2410,i_0_2482,i_0_2434,i_0_2300,i_0_2488,i_0_1500,i_0_2333,i_0_1797,i_0_579,i_0_1432,i_0_1365,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_80,i_0_81,i_0_88,i_0_128,i_0_127,i_0_126]) ).
cnf(i_0_2533,plain,
relation_inverse_image(esk9_0,relation_inverse_image(empty_set,X1)) = empty_set,
inference(scs_inference,[],[i_0_2471,i_0_2450,i_0_2337,i_0_2454,i_0_2452,i_0_2410,i_0_2482,i_0_2434,i_0_2300,i_0_2432,i_0_2473,i_0_2488,i_0_1069,i_0_1276,i_0_1500,i_0_2333,i_0_1797,i_0_1733,i_0_2223,i_0_2235,i_0_579,i_0_2157,i_0_1432,i_0_1365,i_0_177,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_80,i_0_81,i_0_88,i_0_128,i_0_127,i_0_126,i_0_116,i_0_124,i_0_122,i_0_121,i_0_125,i_0_74,i_0_79,i_0_103]) ).
cnf(i_0_2544,plain,
~ element(powerset(X1),powerset(relation_inverse_image(esk14_0,relation_inverse_image(esk6_0,X2)))),
inference(scs_inference,[],[i_0_2515,i_0_446,i_0_87,i_0_85]) ).
cnf(i_0_2546,plain,
~ in(esk14_0,powerset(relation_inverse_image(esk9_0,relation_inverse_image(empty_set,X1)))),
inference(scs_inference,[],[i_0_2515,i_0_2508,i_0_446,i_0_87,i_0_85,i_0_89]) ).
cnf(i_0_2550,plain,
~ in(unordered_pair(X1,X2),esk4_2(unordered_pair(X1,X2),relation_inverse_image(esk6_0,X3))),
inference(scs_inference,[],[i_0_2501,i_0_2515,i_0_2495,i_0_2508,i_0_446,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86]) ).
cnf(i_0_2552,plain,
powerset(relation_inverse_image(esk6_0,X1)) != powerset(esk13_0),
inference(scs_inference,[],[i_0_2501,i_0_2512,i_0_2515,i_0_2495,i_0_2508,i_0_446,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115]) ).
cnf(i_0_2559,plain,
element(esk5_1(relation_inverse_image(esk9_0,relation_inverse_image(empty_set,X1))),empty_set),
inference(scs_inference,[],[i_0_2501,i_0_2512,i_0_2515,i_0_2533,i_0_2495,i_0_2508,i_0_2506,i_0_2510,i_0_1627,i_0_2404,i_0_446,i_0_1444,i_0_95,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_80,i_0_81,i_0_88,i_0_128]) ).
cnf(i_0_2565,plain,
esk13_0 != relation_inverse_image(esk8_0,X1),
inference(scs_inference,[],[i_0_2501,i_0_2465,i_0_2512,i_0_2515,i_0_2533,i_0_2467,i_0_2495,i_0_2413,i_0_2508,i_0_2506,i_0_2505,i_0_2510,i_0_1627,i_0_2404,i_0_1305,i_0_446,i_0_1444,i_0_95,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_80,i_0_81,i_0_88,i_0_128,i_0_127,i_0_126,i_0_116]) ).
cnf(i_0_2577,plain,
in(esk2_3(esk10_1(X1),relation_inverse_image(relation_inverse_image(esk6_0,X2),X3),esk14_0),esk14_0),
inference(scs_inference,[],[i_0_2501,i_0_2465,i_0_2512,i_0_2515,i_0_2533,i_0_2467,i_0_2495,i_0_2413,i_0_2528,i_0_2508,i_0_2506,i_0_2505,i_0_2568,i_0_2262,i_0_2510,i_0_1572,i_0_2570,i_0_1627,i_0_2404,i_0_1305,i_0_446,i_0_1444,i_0_169,i_0_1535,i_0_268,i_0_95,i_0_177,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_80,i_0_81,i_0_88,i_0_128,i_0_127,i_0_126,i_0_116,i_0_124,i_0_122,i_0_121,i_0_125,i_0_73]) ).
cnf(i_0_2582,plain,
unordered_pair(X1,X2) != relation_inverse_image(esk8_0,X3),
inference(scs_inference,[],[i_0_2501,i_0_2571,i_0_2465,i_0_2512,i_0_2515,i_0_2533,i_0_2467,i_0_2495,i_0_2413,i_0_2528,i_0_2508,i_0_2506,i_0_2505,i_0_2568,i_0_2262,i_0_2510,i_0_1572,i_0_2570,i_0_1627,i_0_2404,i_0_1305,i_0_446,i_0_1444,i_0_169,i_0_1535,i_0_268,i_0_134,i_0_95,i_0_136,i_0_177,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_80,i_0_81,i_0_88,i_0_128,i_0_127,i_0_126,i_0_116,i_0_124,i_0_122,i_0_121,i_0_125,i_0_73,i_0_71]) ).
cnf(i_0_2585,plain,
in(esk2_3(esk9_0,relation_inverse_image(esk14_0,relation_inverse_image(esk8_0,X1)),esk12_0),esk12_0),
inference(scs_inference,[],[i_0_2501,i_0_2571,i_0_2465,i_0_2512,i_0_2515,i_0_2533,i_0_2467,i_0_2495,i_0_2413,i_0_2528,i_0_2508,i_0_2506,i_0_2505,i_0_2568,i_0_2262,i_0_2510,i_0_486,i_0_1572,i_0_2570,i_0_1627,i_0_2404,i_0_1305,i_0_446,i_0_1444,i_0_169,i_0_1535,i_0_143,i_0_268,i_0_134,i_0_95,i_0_136,i_0_107,i_0_177,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_80,i_0_81,i_0_88,i_0_128,i_0_127,i_0_126,i_0_116,i_0_124,i_0_122,i_0_121,i_0_125,i_0_73,i_0_71,i_0_75]) ).
cnf(i_0_2618,plain,
relation_inverse_image(esk9_0,relation_inverse_image(empty_set,X1)) = empty_set,
inference(rename_variables,[],[i_0_2533]) ).
cnf(i_0_2786,plain,
esk13_0 != relation_inverse_image(esk8_0,X1),
inference(rename_variables,[],[i_0_2565]) ).
cnf(i_0_2613,plain,
element(relation_inverse_image(esk6_0,X1),powerset(X2)),
inference(scs_inference,[],[i_0_2463,i_0_2569,i_0_2604,i_0_2567,i_0_2555,i_0_2401,i_0_2436,i_0_2553,i_0_402,i_0_1625,i_0_1498,i_0_2326,i_0_1441,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_80,i_0_81,i_0_88,i_0_128,i_0_127]) ).
cnf(i_0_2617,plain,
empty_set != esk7_1(esk4_2(esk14_0,powerset(relation_inverse_image(esk8_0,X1)))),
inference(scs_inference,[],[i_0_2463,i_0_2563,i_0_2569,i_0_2604,i_0_2567,i_0_2555,i_0_2401,i_0_2520,i_0_2436,i_0_2553,i_0_402,i_0_2533,i_0_599,i_0_1625,i_0_1498,i_0_2326,i_0_1441,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_80,i_0_81,i_0_88,i_0_128,i_0_127,i_0_126,i_0_116]) ).
cnf(i_0_2627,plain,
esk9_0 != relation_inverse_image(empty_set,X1),
inference(scs_inference,[],[i_0_2463,i_0_2563,i_0_2569,i_0_2604,i_0_2546,i_0_2585,i_0_2567,i_0_2555,i_0_2401,i_0_2520,i_0_2436,i_0_2553,i_0_402,i_0_2533,i_0_1638,i_0_2264,i_0_2432,i_0_2473,i_0_2213,i_0_1577,i_0_599,i_0_1625,i_0_1498,i_0_2326,i_0_1441,i_0_226,i_0_109,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_80,i_0_81,i_0_88,i_0_128,i_0_127,i_0_126,i_0_116,i_0_124,i_0_122,i_0_121,i_0_125,i_0_71]) ).
cnf(i_0_2636,plain,
~ empty(esk7_1(esk7_1(esk4_2(esk14_0,powerset(relation_inverse_image(esk8_0,X1)))))),
inference(scs_inference,[],[i_0_2463,i_0_2563,i_0_2569,i_0_2604,i_0_2546,i_0_2585,i_0_2567,i_0_2470,i_0_2555,i_0_2401,i_0_2520,i_0_2436,i_0_2553,i_0_402,i_0_2533,i_0_1638,i_0_2264,i_0_2432,i_0_2473,i_0_2213,i_0_1577,i_0_599,i_0_1625,i_0_1498,i_0_2326,i_0_1441,i_0_226,i_0_189,i_0_109,i_0_106,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_80,i_0_81,i_0_88,i_0_128,i_0_127,i_0_126,i_0_116,i_0_124,i_0_122,i_0_121,i_0_125,i_0_71,i_0_75,i_0_100,i_0_94]) ).
cnf(i_0_2638,plain,
element(esk7_1(esk7_1(esk7_1(esk9_0))),powerset(esk7_1(esk7_1(esk9_0)))),
inference(scs_inference,[],[i_0_2463,i_0_2563,i_0_2569,i_0_2604,i_0_2546,i_0_2585,i_0_2567,i_0_2470,i_0_2555,i_0_2401,i_0_2520,i_0_2436,i_0_2553,i_0_402,i_0_2533,i_0_1638,i_0_2264,i_0_2432,i_0_2473,i_0_2213,i_0_1577,i_0_599,i_0_1559,i_0_1625,i_0_1498,i_0_2326,i_0_1441,i_0_226,i_0_189,i_0_109,i_0_106,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_80,i_0_81,i_0_88,i_0_128,i_0_127,i_0_126,i_0_116,i_0_124,i_0_122,i_0_121,i_0_125,i_0_71,i_0_75,i_0_100,i_0_94,i_0_90]) ).
cnf(i_0_2647,plain,
esk12_0 != relation_inverse_image(relation_inverse_image(empty_set,empty_set),X1),
inference(scs_inference,[],[i_0_1939,i_0_2463,i_0_2563,i_0_2569,i_0_2604,i_0_2546,i_0_2585,i_0_2567,i_0_2470,i_0_2535,i_0_2555,i_0_2401,i_0_2520,i_0_2436,i_0_2553,i_0_1272,i_0_402,i_0_2533,i_0_1638,i_0_2264,i_0_2432,i_0_2473,i_0_2213,i_0_1577,i_0_599,i_0_1559,i_0_1625,i_0_1498,i_0_2326,i_0_1441,i_0_226,i_0_189,i_0_109,i_0_106,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_80,i_0_81,i_0_88,i_0_128,i_0_127,i_0_126,i_0_116,i_0_124,i_0_122,i_0_121,i_0_125,i_0_71,i_0_75,i_0_100,i_0_94,i_0_90,i_0_117,i_0_118,i_0_119,i_0_120,i_0_82,i_0_123,i_0_2443]) ).
cnf(i_0_2648,plain,
relation(relation_inverse_image(empty_set,empty_set)),
inference(scs_inference,[],[i_0_2634,i_0_2442]) ).
cnf(i_0_2649,plain,
~ in(X1,relation_inverse_image(relation_inverse_image(esk10_1(X2),X3),X4)),
inference(scs_inference,[],[i_0_2634,i_0_2445]) ).
cnf(i_0_2652,plain,
~ element(powerset(X1),powerset(relation_inverse_image(esk9_0,relation_inverse_image(esk8_0,X2)))),
inference(scs_inference,[],[i_0_2615,i_0_364,i_0_87,i_0_85]) ).
cnf(i_0_2654,plain,
~ in(powerset(X1),powerset(relation_inverse_image(esk14_0,relation_inverse_image(esk6_0,X2)))),
inference(scs_inference,[],[i_0_2615,i_0_2544,i_0_364,i_0_87,i_0_85,i_0_89]) ).
cnf(i_0_2660,plain,
relation_inverse_image(esk8_0,X1) != unordered_pair(X2,X3),
inference(scs_inference,[],[i_0_2582,i_0_2615,i_0_2591,i_0_2544,i_0_2644,i_0_364,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115]) ).
cnf(i_0_2667,plain,
relation_inverse_image(esk6_0,X1) != esk14_0,
inference(scs_inference,[],[i_0_2582,i_0_2613,i_0_2615,i_0_2591,i_0_2544,i_0_2644,i_0_2459,i_0_2131,i_0_2531,i_0_1956,i_0_364,i_0_1365,i_0_96,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_81,i_0_88,i_0_128,i_0_127]) ).
cnf(i_0_2668,plain,
element(relation_inverse_image(esk6_0,X1),powerset(X2)),
inference(rename_variables,[],[i_0_2613]) ).
cnf(i_0_2673,plain,
empty(relation_inverse_image(esk9_0,relation_inverse_image(esk8_0,X1))),
inference(scs_inference,[],[i_0_2582,i_0_2613,i_0_2615,i_0_2591,i_0_2525,i_0_2544,i_0_2644,i_0_2459,i_0_2131,i_0_2531,i_0_2619,i_0_2225,i_0_1956,i_0_364,i_0_442,i_0_1637,i_0_2363,i_0_1365,i_0_96,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_81,i_0_88,i_0_128,i_0_127,i_0_126,i_0_116,i_0_124]) ).
cnf(i_0_2726,plain,
esk12_0 != relation_inverse_image(relation_inverse_image(empty_set,empty_set),X1),
inference(rename_variables,[],[i_0_2647]) ).
cnf(i_0_2746,plain,
esk12_0 != relation_inverse_image(relation_inverse_image(empty_set,empty_set),X1),
inference(rename_variables,[],[i_0_2647]) ).
cnf(i_0_2819,plain,
element(relation_inverse_image(esk6_0,X1),powerset(X2)),
inference(rename_variables,[],[i_0_2613]) ).
cnf(i_0_2692,plain,
~ in(X1,relation_inverse_image(relation_inverse_image(esk10_1(X2),X3),X4)),
inference(scs_inference,[],[i_0_2648,i_0_1553]) ).
cnf(i_0_2695,plain,
subset(esk7_1(esk7_1(esk7_1(esk9_0))),esk7_1(esk7_1(esk9_0))),
inference(scs_inference,[],[i_0_2661,i_0_2638,i_0_87,i_0_85]) ).
cnf(i_0_2699,plain,
subset(relation_inverse_image(relation_inverse_image(esk10_1(X1),X2),X3),X4),
inference(scs_inference,[],[i_0_2649,i_0_2661,i_0_2630,i_0_2638,i_0_87,i_0_85,i_0_89,i_0_83]) ).
cnf(i_0_2700,plain,
~ in(X1,relation_inverse_image(relation_inverse_image(esk10_1(X2),X3),X4)),
inference(rename_variables,[],[i_0_2649]) ).
cnf(i_0_2707,plain,
in(esk5_1(esk7_1(esk13_0)),esk7_1(esk13_0)),
inference(scs_inference,[],[i_0_2673,i_0_2649,i_0_2661,i_0_2630,i_0_2638,i_0_2439,i_0_1496,i_0_95,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_81,i_0_88]) ).
cnf(i_0_2713,plain,
element(relation_inverse_image(esk10_1(X1),X2),powerset(relation_inverse_image(esk6_0,X3))),
inference(scs_inference,[],[i_0_2673,i_0_2448,i_0_2595,i_0_2649,i_0_2661,i_0_2630,i_0_2638,i_0_2439,i_0_2602,i_0_2098,i_0_1496,i_0_95,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_81,i_0_88,i_0_128,i_0_127]) ).
cnf(i_0_2717,plain,
relation_inverse_image(esk9_0,relation_inverse_image(esk8_0,X1)) != esk7_1(esk7_1(esk7_1(esk13_0))),
inference(scs_inference,[],[i_0_2673,i_0_2448,i_0_2595,i_0_2649,i_0_2661,i_0_2630,i_0_2638,i_0_2439,i_0_2602,i_0_1947,i_0_1725,i_0_2098,i_0_1988,i_0_1496,i_0_95,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_81,i_0_88,i_0_128,i_0_127,i_0_116,i_0_124]) ).
cnf(i_0_2719,plain,
~ in(X1,relation_inverse_image(relation_inverse_image(esk10_1(X2),X3),X4)),
inference(rename_variables,[],[i_0_2649]) ).
cnf(i_0_2727,plain,
~ in(X1,relation_inverse_image(relation_inverse_image(esk10_1(X2),X3),X4)),
inference(rename_variables,[],[i_0_2649]) ).
cnf(i_0_2744,plain,
~ in(X1,relation_inverse_image(relation_inverse_image(esk10_1(X2),X3),X4)),
inference(rename_variables,[],[i_0_2649]) ).
cnf(i_0_2771,plain,
relation_inverse_image(esk8_0,X1) != unordered_pair(X2,X3),
inference(rename_variables,[],[i_0_2660]) ).
cnf(i_0_2731,plain,
relation_inverse_image(esk9_0,relation_inverse_image(esk8_0,X1)) = empty_set,
inference(scs_inference,[],[i_0_2648,i_0_2673,i_0_2647,i_0_2448,i_0_2595,i_0_2649,i_0_2700,i_0_2719,i_0_2654,i_0_2661,i_0_2624,i_0_2630,i_0_2638,i_0_2439,i_0_2602,i_0_1947,i_0_1725,i_0_2098,i_0_1805,i_0_2223,i_0_1988,i_0_1496,i_0_95,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_81,i_0_88,i_0_128,i_0_127,i_0_116,i_0_124,i_0_122,i_0_121,i_0_125,i_0_75,i_0_710,i_0_103]) ).
cnf(i_0_2756,plain,
~ in(esk7_1(esk13_0),esk5_1(esk7_1(esk13_0))),
inference(scs_inference,[],[i_0_2707,i_0_2693,i_0_2251,i_0_2705,i_0_554,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86]) ).
cnf(i_0_2758,plain,
relation_inverse_image(esk8_0,X1) != esk13_0,
inference(scs_inference,[],[i_0_2565,i_0_2707,i_0_2693,i_0_2251,i_0_2705,i_0_554,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115]) ).
cnf(i_0_2759,plain,
element(esk5_1(esk7_1(esk13_0)),esk13_0),
inference(scs_inference,[],[i_0_2565,i_0_2707,i_0_2693,i_0_2251,i_0_2705,i_0_1500,i_0_554,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_80]) ).
cnf(i_0_2763,plain,
in(esk5_1(esk7_1(esk7_1(esk13_0))),esk7_1(esk7_1(esk13_0))),
inference(scs_inference,[],[i_0_2565,i_0_2707,i_0_2693,i_0_2251,i_0_2705,i_0_1500,i_0_2404,i_0_1742,i_0_554,i_0_95,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_80,i_0_81,i_0_88]) ).
cnf(i_0_2780,plain,
~ in(X1,relation_inverse_image(relation_inverse_image(esk10_1(X2),X3),X4)),
inference(rename_variables,[],[i_0_2692]) ).
cnf(i_0_2787,plain,
~ in(X1,relation_inverse_image(relation_inverse_image(esk10_1(X2),X3),X4)),
inference(rename_variables,[],[i_0_2692]) ).
cnf(i_0_2813,plain,
~ in(X1,relation_inverse_image(relation_inverse_image(esk10_1(X2),X3),X4)),
inference(rename_variables,[],[i_0_2692]) ).
cnf(i_0_2836,plain,
~ in(X1,relation_inverse_image(relation_inverse_image(esk10_1(X2),X3),X4)),
inference(rename_variables,[],[i_0_2692]) ).
cnf(i_0_2804,plain,
subset(relation_inverse_image(relation_inverse_image(esk6_0,X1),X2),X3),
inference(scs_inference,[],[i_0_2754,i_0_2355,i_0_2072,i_0_2157,i_0_87,i_0_85,i_0_89,i_0_83]) ).
cnf(i_0_2809,plain,
empty_set = relation_inverse_image(esk9_0,relation_inverse_image(esk8_0,X1)),
inference(scs_inference,[],[i_0_2754,i_0_2355,i_0_2072,i_0_2731,i_0_2157,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115]) ).
cnf(i_0_2770,plain,
relation_inverse_image(relation_inverse_image(empty_set,empty_set),X1) != unordered_pair(X2,X3),
inference(scs_inference,[],[i_0_2660,i_0_2565,i_0_2707,i_0_2729,i_0_2769,i_0_2693,i_0_2251,i_0_2705,i_0_2603,i_0_2465,i_0_1992,i_0_1500,i_0_2404,i_0_1742,i_0_554,i_0_95,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_80,i_0_81,i_0_88,i_0_128,i_0_127,i_0_116]) ).
cnf(i_0_2772,plain,
empty(relation_inverse_image(relation_inverse_image(empty_set,empty_set),X1)),
inference(scs_inference,[],[i_0_2660,i_0_2565,i_0_2707,i_0_2729,i_0_2769,i_0_2693,i_0_2251,i_0_2705,i_0_2603,i_0_2465,i_0_1992,i_0_1500,i_0_2404,i_0_1742,i_0_554,i_0_1535,i_0_95,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_80,i_0_81,i_0_88,i_0_128,i_0_127,i_0_116,i_0_124]) ).
cnf(i_0_2777,plain,
subset(relation_inverse_image(relation_inverse_image(empty_set,empty_set),X1),X2),
inference(scs_inference,[],[i_0_2660,i_0_2565,i_0_2707,i_0_2729,i_0_2769,i_0_2773,i_0_2693,i_0_2251,i_0_2705,i_0_2603,i_0_2656,i_0_2465,i_0_1992,i_0_2767,i_0_1500,i_0_2404,i_0_1742,i_0_554,i_0_169,i_0_1535,i_0_95,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_80,i_0_81,i_0_88,i_0_128,i_0_127,i_0_116,i_0_124,i_0_122,i_0_125]) ).
cnf(i_0_2785,plain,
in(esk2_3(esk8_0,relation_inverse_image(relation_inverse_image(esk10_1(X1),X2),X3),esk13_0),esk13_0),
inference(scs_inference,[],[i_0_2660,i_0_2565,i_0_2707,i_0_2729,i_0_2769,i_0_2773,i_0_2693,i_0_2251,i_0_2692,i_0_2780,i_0_2705,i_0_2603,i_0_2656,i_0_2465,i_0_1992,i_0_2767,i_0_1795,i_0_1500,i_0_2404,i_0_2634,i_0_1742,i_0_554,i_0_169,i_0_2648,i_0_2326,i_0_1535,i_0_95,i_0_136,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_80,i_0_81,i_0_88,i_0_128,i_0_127,i_0_116,i_0_124,i_0_122,i_0_125,i_0_74,i_0_71,i_0_75]) ).
cnf(i_0_2962,plain,
element(relation_inverse_image(relation_inverse_image(esk6_0,X1),X2),powerset(X3)),
inference(scs_inference,[],[i_0_2804,i_0_87]) ).
cnf(i_0_2964,plain,
~ element(esk12_0,powerset(relation_inverse_image(esk8_0,X1))),
inference(scs_inference,[],[i_0_2804,i_0_478,i_0_87,i_0_85]) ).
cnf(i_0_2797,plain,
in(esk5_1(esk7_1(esk13_0)),esk7_1(esk13_0)),
inference(equality_inference,[],[2796]) ).
cnf(i_0_2812,plain,
empty(relation_inverse_image(relation_inverse_image(esk10_1(X1),X2),empty_set)),
inference(scs_inference,[],[i_0_2772,i_0_2754,i_0_2355,i_0_2072,i_0_2731,i_0_2692,i_0_2157,i_0_1654,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_81,i_0_88]) ).
cnf(i_0_2818,plain,
relation_inverse_image(esk6_0,X1) != esk9_0,
inference(scs_inference,[],[i_0_2772,i_0_2754,i_0_2355,i_0_2072,i_0_2731,i_0_1901,i_0_2613,i_0_1759,i_0_2692,i_0_2187,i_0_2157,i_0_1654,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_81,i_0_88,i_0_128,i_0_127]) ).
cnf(i_0_2820,plain,
relation_inverse_image(relation_inverse_image(empty_set,empty_set),X1) != esk13_0,
inference(scs_inference,[],[i_0_2758,i_0_2772,i_0_2754,i_0_2355,i_0_2072,i_0_2731,i_0_1901,i_0_2613,i_0_1759,i_0_2729,i_0_2692,i_0_2187,i_0_2157,i_0_1654,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_81,i_0_88,i_0_128,i_0_127,i_0_116]) ).
cnf(i_0_2822,plain,
relation_inverse_image(relation_inverse_image(empty_set,empty_set),X1) != esk7_1(esk9_0),
inference(scs_inference,[],[i_0_2758,i_0_2772,i_0_2754,i_0_2355,i_0_2072,i_0_2731,i_0_1901,i_0_2613,i_0_1759,i_0_2729,i_0_2692,i_0_2187,i_0_1363,i_0_2157,i_0_1654,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_81,i_0_88,i_0_128,i_0_127,i_0_116,i_0_124]) ).
cnf(i_0_2825,plain,
in(relation_inverse_image(esk9_0,relation_inverse_image(esk8_0,X1)),powerset(X2)),
inference(scs_inference,[],[i_0_2758,i_0_2772,i_0_2754,i_0_2355,i_0_2072,i_0_2731,i_0_1901,i_0_2684,i_0_2613,i_0_1759,i_0_2729,i_0_2692,i_0_2187,i_0_1795,i_0_1363,i_0_2157,i_0_1654,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_81,i_0_88,i_0_128,i_0_127,i_0_116,i_0_124,i_0_122,i_0_121]) ).
cnf(i_0_2832,plain,
in(esk2_3(empty_set,X1,esk9_0),esk9_0),
inference(scs_inference,[],[i_0_2627,i_0_2758,i_0_2772,i_0_2754,i_0_1723,i_0_2355,i_0_2072,i_0_2731,i_0_1901,i_0_2684,i_0_2613,i_0_1759,i_0_2729,i_0_2692,i_0_2187,i_0_1467,i_0_1795,i_0_632,i_0_1363,i_0_2634,i_0_2157,i_0_1654,i_0_226,i_0_109,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_81,i_0_88,i_0_128,i_0_127,i_0_116,i_0_124,i_0_122,i_0_121,i_0_125,i_0_74,i_0_73]) ).
cnf(i_0_2839,plain,
relation(relation_inverse_image(esk9_0,relation_inverse_image(esk8_0,X1))),
inference(scs_inference,[],[i_0_2627,i_0_2758,i_0_2772,i_0_2754,i_0_1723,i_0_2355,i_0_2782,i_0_2072,i_0_2731,i_0_1901,i_0_2684,i_0_2613,i_0_1759,i_0_2729,i_0_2692,i_0_2813,i_0_2187,i_0_1467,i_0_1795,i_0_632,i_0_1363,i_0_2634,i_0_2157,i_0_1654,i_0_226,i_0_109,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_81,i_0_88,i_0_128,i_0_127,i_0_116,i_0_124,i_0_122,i_0_121,i_0_125,i_0_74,i_0_73,i_0_75,i_0_310]) ).
cnf(i_0_2840,plain,
relation(relation_inverse_image(relation_inverse_image(empty_set,empty_set),X1)),
inference(scs_inference,[],[i_0_2627,i_0_2758,i_0_2772,i_0_2754,i_0_1723,i_0_2355,i_0_2782,i_0_2072,i_0_2731,i_0_1901,i_0_2684,i_0_2613,i_0_1759,i_0_2729,i_0_2692,i_0_2813,i_0_2187,i_0_1467,i_0_1795,i_0_632,i_0_1363,i_0_2634,i_0_2157,i_0_1654,i_0_226,i_0_109,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_81,i_0_88,i_0_128,i_0_127,i_0_116,i_0_124,i_0_122,i_0_121,i_0_125,i_0_74,i_0_73,i_0_75,i_0_310,i_0_100]) ).
cnf(i_0_2842,plain,
~ empty(esk7_1(esk7_1(relation_inverse_image(esk14_0,esk12_0)))),
inference(scs_inference,[],[i_0_2627,i_0_2758,i_0_2772,i_0_2754,i_0_1723,i_0_2355,i_0_2782,i_0_2072,i_0_2731,i_0_1901,i_0_2684,i_0_2613,i_0_1759,i_0_2729,i_0_2692,i_0_2813,i_0_2187,i_0_1467,i_0_1795,i_0_632,i_0_1363,i_0_2218,i_0_2634,i_0_2157,i_0_1654,i_0_226,i_0_109,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_81,i_0_88,i_0_128,i_0_127,i_0_116,i_0_124,i_0_122,i_0_121,i_0_125,i_0_74,i_0_73,i_0_75,i_0_310,i_0_100,i_0_94]) ).
cnf(i_0_2844,plain,
element(esk7_1(esk7_1(esk7_1(esk14_0))),powerset(esk7_1(esk7_1(esk14_0)))),
inference(scs_inference,[],[i_0_2627,i_0_2758,i_0_2772,i_0_2754,i_0_1723,i_0_2355,i_0_2782,i_0_2072,i_0_2731,i_0_1901,i_0_2684,i_0_2613,i_0_1759,i_0_2729,i_0_2692,i_0_2813,i_0_2187,i_0_1467,i_0_1795,i_0_632,i_0_1363,i_0_2218,i_0_1625,i_0_2634,i_0_2157,i_0_1654,i_0_226,i_0_109,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_81,i_0_88,i_0_128,i_0_127,i_0_116,i_0_124,i_0_122,i_0_121,i_0_125,i_0_74,i_0_73,i_0_75,i_0_310,i_0_100,i_0_94,i_0_90]) ).
cnf(i_0_2850,plain,
in(esk5_1(esk7_1(esk7_1(esk13_0))),esk7_1(esk13_0)),
inference(scs_inference,[],[i_0_2627,i_0_2758,i_0_2060,i_0_2772,i_0_2754,i_0_2763,i_0_1723,i_0_2355,i_0_2782,i_0_2072,i_0_2731,i_0_1901,i_0_2684,i_0_2613,i_0_1759,i_0_2729,i_0_2692,i_0_2813,i_0_2187,i_0_1467,i_0_1795,i_0_632,i_0_1363,i_0_2218,i_0_1625,i_0_2634,i_0_2157,i_0_1654,i_0_226,i_0_109,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_81,i_0_88,i_0_128,i_0_127,i_0_116,i_0_124,i_0_122,i_0_121,i_0_125,i_0_74,i_0_73,i_0_75,i_0_310,i_0_100,i_0_94,i_0_90,i_0_117,i_0_118,i_0_119,i_0_120,i_0_82]) ).
cnf(i_0_2857,plain,
~ in(X1,relation_inverse_image(relation_inverse_image(esk9_0,relation_inverse_image(esk8_0,X2)),X3)),
inference(scs_inference,[],[i_0_2627,i_0_2758,i_0_2060,i_0_2772,i_0_2754,i_0_2763,i_0_1723,i_0_2355,i_0_2782,i_0_2072,i_0_2731,i_0_1901,i_0_2704,i_0_1447,i_0_2684,i_0_2613,i_0_1759,i_0_2729,i_0_2692,i_0_2813,i_0_2187,i_0_1467,i_0_1795,i_0_632,i_0_1363,i_0_2218,i_0_1625,i_0_2634,i_0_2157,i_0_1654,i_0_226,i_0_189,i_0_109,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_81,i_0_88,i_0_128,i_0_127,i_0_116,i_0_124,i_0_122,i_0_121,i_0_125,i_0_74,i_0_73,i_0_75,i_0_310,i_0_100,i_0_94,i_0_90,i_0_117,i_0_118,i_0_119,i_0_120,i_0_82,i_0_123,i_0_71,i_0_1314]) ).
cnf(i_0_2861,plain,
element(relation_inverse_image(relation_inverse_image(empty_set,empty_set),X1),powerset(X2)),
inference(scs_inference,[],[i_0_2777,i_0_87]) ).
cnf(i_0_2863,plain,
~ element(esk12_0,powerset(relation_inverse_image(esk14_0,relation_inverse_image(esk6_0,X1)))),
inference(scs_inference,[],[i_0_2777,i_0_481,i_0_87,i_0_85]) ).
cnf(i_0_2865,plain,
~ in(singleton(X1),powerset(relation_inverse_image(esk8_0,X2))),
inference(scs_inference,[],[i_0_2777,i_0_2750,i_0_481,i_0_87,i_0_85,i_0_89]) ).
cnf(i_0_2869,plain,
~ in(esk9_0,esk2_3(empty_set,X1,esk9_0)),
inference(scs_inference,[],[i_0_2832,i_0_2777,i_0_2750,i_0_2798,i_0_481,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86]) ).
cnf(i_0_2871,plain,
esk14_0 != relation_inverse_image(esk6_0,X1),
inference(scs_inference,[],[i_0_2667,i_0_2832,i_0_2777,i_0_2750,i_0_2798,i_0_481,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115]) ).
cnf(i_0_2876,plain,
relation(relation_inverse_image(relation_inverse_image(empty_set,empty_set),X1)),
inference(rename_variables,[],[i_0_2840]) ).
cnf(i_0_2879,plain,
~ element(esk9_0,powerset(relation_inverse_image(relation_inverse_image(esk10_1(X1),X2),empty_set))),
inference(scs_inference,[],[i_0_2667,i_0_2832,i_0_2840,i_0_2777,i_0_2750,i_0_2798,i_0_2812,i_0_718,i_0_481,i_0_1996,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_130,i_0_129,i_0_81]) ).
cnf(i_0_2882,plain,
~ in(X1,relation_inverse_image(relation_inverse_image(esk9_0,relation_inverse_image(esk8_0,X2)),X3)),
inference(rename_variables,[],[i_0_2857]) ).
cnf(i_0_2885,plain,
element(esk5_1(esk6_0),relation_inverse_image(esk9_0,relation_inverse_image(esk8_0,X1))),
inference(scs_inference,[],[i_0_2667,i_0_2832,i_0_1521,i_0_2840,i_0_2777,i_0_2750,i_0_2809,i_0_2857,i_0_2798,i_0_2812,i_0_718,i_0_481,i_0_1996,i_0_1654,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_130,i_0_129,i_0_81,i_0_88,i_0_128]) ).
cnf(i_0_2904,plain,
~ in(X1,relation_inverse_image(relation_inverse_image(esk9_0,relation_inverse_image(esk8_0,X2)),X3)),
inference(rename_variables,[],[i_0_2857]) ).
cnf(i_0_2907,plain,
relation(relation_inverse_image(relation_inverse_image(empty_set,empty_set),X1)),
inference(rename_variables,[],[i_0_2840]) ).
cnf(i_0_2909,plain,
~ in(X1,relation_inverse_image(relation_inverse_image(esk9_0,relation_inverse_image(esk8_0,X2)),X3)),
inference(rename_variables,[],[i_0_2857]) ).
cnf(i_0_2953,plain,
relation(relation_inverse_image(esk9_0,relation_inverse_image(esk8_0,X1))),
inference(rename_variables,[],[i_0_2839]) ).
cnf(i_0_2966,plain,
~ in(esk12_0,powerset(relation_inverse_image(esk14_0,relation_inverse_image(esk6_0,X1)))),
inference(scs_inference,[],[i_0_2804,i_0_2863,i_0_478,i_0_87,i_0_85,i_0_89]) ).
cnf(i_0_2979,plain,
element(relation_inverse_image(relation_inverse_image(empty_set,empty_set),X1),powerset(X2)),
inference(rename_variables,[],[i_0_2861]) ).
cnf(i_0_2993,plain,
relation(relation_inverse_image(esk9_0,relation_inverse_image(esk8_0,X1))),
inference(rename_variables,[],[i_0_2839]) ).
cnf(i_0_3005,plain,
~ in(X1,relation_inverse_image(relation_inverse_image(esk9_0,relation_inverse_image(esk8_0,X2)),X3)),
inference(rename_variables,[],[i_0_2857]) ).
cnf(i_0_3050,plain,
~ in(X1,relation_inverse_image(relation_inverse_image(esk9_0,relation_inverse_image(esk8_0,X2)),X3)),
inference(rename_variables,[],[i_0_2857]) ).
cnf(i_0_2921,plain,
~ subset(esk9_0,relation_inverse_image(relation_inverse_image(esk10_1(X1),X2),empty_set)),
inference(scs_inference,[],[i_0_2879,i_0_87]) ).
cnf(i_0_2923,plain,
subset(esk7_1(esk7_1(esk7_1(esk14_0))),esk7_1(esk7_1(esk14_0))),
inference(scs_inference,[],[i_0_2844,i_0_2879,i_0_87,i_0_85]) ).
cnf(i_0_2939,plain,
element(empty_set,powerset(relation_inverse_image(empty_set,X1))),
inference(scs_inference,[],[i_0_1773,i_0_2847,i_0_2875,i_0_2842,i_0_2881,i_0_2867,i_0_2844,i_0_2879,i_0_2809,i_0_1567,i_0_2465,i_0_95,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_81,i_0_88,i_0_128,i_0_127]) ).
cnf(i_0_2957,plain,
esk14_0 != relation_inverse_image(esk6_0,X1),
inference(rename_variables,[],[i_0_2871]) ).
cnf(i_0_2947,plain,
in(relation_inverse_image(esk14_0,relation_inverse_image(esk6_0,X1)),powerset(X2)),
inference(scs_inference,[],[i_0_1773,i_0_2847,i_0_2848,i_0_2849,i_0_2875,i_0_2928,i_0_2842,i_0_2881,i_0_2867,i_0_2844,i_0_2879,i_0_2825,i_0_2809,i_0_1567,i_0_380,i_0_2465,i_0_95,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_81,i_0_88,i_0_128,i_0_127,i_0_116,i_0_124,i_0_122,i_0_121]) ).
cnf(i_0_2968,plain,
in(esk4_2(esk9_0,relation_inverse_image(relation_inverse_image(esk10_1(X1),X2),empty_set)),esk9_0),
inference(scs_inference,[],[i_0_2804,i_0_2863,i_0_2921,i_0_478,i_0_87,i_0_85,i_0_89,i_0_83]) ).
cnf(i_0_2972,plain,
esk9_0 != relation_inverse_image(esk6_0,X1),
inference(scs_inference,[],[i_0_2818,i_0_2804,i_0_2863,i_0_2921,i_0_2725,i_0_478,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115]) ).
cnf(i_0_2975,plain,
in(esk5_1(esk7_1(esk13_0)),esk13_0),
inference(scs_inference,[],[i_0_2818,i_0_2947,i_0_2804,i_0_2759,i_0_2863,i_0_2921,i_0_2725,i_0_2812,i_0_1444,i_0_478,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_81,i_0_88]) ).
cnf(i_0_2977,plain,
powerset(esk13_0) != powerset(relation_inverse_image(esk14_0,relation_inverse_image(esk6_0,X1))),
inference(scs_inference,[],[i_0_2818,i_0_2947,i_0_2804,i_0_2759,i_0_2863,i_0_2921,i_0_2725,i_0_2812,i_0_1444,i_0_478,i_0_1365,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_81,i_0_88,i_0_128]) ).
cnf(i_0_2978,plain,
relation_inverse_image(relation_inverse_image(empty_set,empty_set),X1) != esk12_0,
inference(scs_inference,[],[i_0_2818,i_0_2861,i_0_2947,i_0_2804,i_0_2759,i_0_2863,i_0_2921,i_0_2725,i_0_2812,i_0_1444,i_0_478,i_0_1365,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_81,i_0_88,i_0_128,i_0_127]) ).
cnf(i_0_2980,plain,
empty_set != esk7_1(esk7_1(relation_inverse_image(esk14_0,esk12_0))),
inference(scs_inference,[],[i_0_2818,i_0_2861,i_0_2947,i_0_2804,i_0_2759,i_0_2863,i_0_2921,i_0_2960,i_0_2944,i_0_2725,i_0_2812,i_0_1444,i_0_478,i_0_1365,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_81,i_0_88,i_0_128,i_0_127,i_0_116]) ).
cnf(i_0_2982,plain,
empty(relation_inverse_image(relation_inverse_image(empty_set,X1),empty_set)),
inference(scs_inference,[],[i_0_2818,i_0_2861,i_0_2947,i_0_2804,i_0_2759,i_0_2863,i_0_2921,i_0_2960,i_0_2944,i_0_2725,i_0_2812,i_0_1376,i_0_1444,i_0_478,i_0_1365,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_81,i_0_88,i_0_128,i_0_127,i_0_116,i_0_124]) ).
cnf(i_0_2998,plain,
~ subset(powerset(X1),relation_inverse_image(relation_inverse_image(esk10_1(X2),X3),empty_set)),
inference(scs_inference,[],[i_0_2973,i_0_87]) ).
cnf(i_0_3007,plain,
~ in(esk13_0,esk5_1(esk7_1(esk13_0))),
inference(scs_inference,[],[i_0_2975,i_0_2991,i_0_2973,i_0_2886,i_0_2857,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86]) ).
cnf(i_0_3010,plain,
~ element(esk13_0,powerset(relation_inverse_image(relation_inverse_image(empty_set,X1),empty_set))),
inference(scs_inference,[],[i_0_2982,i_0_2975,i_0_2941,i_0_2991,i_0_2973,i_0_2886,i_0_2857,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_81]) ).
cnf(i_0_3023,plain,
in(relation_inverse_image(esk9_0,relation_inverse_image(empty_set,X1)),powerset(X2)),
inference(scs_inference,[],[i_0_2982,i_0_2939,i_0_2975,i_0_2941,i_0_2991,i_0_2973,i_0_2886,i_0_2911,i_0_2947,i_0_2857,i_0_1986,i_0_776,i_0_731,i_0_2842,i_0_2809,i_0_95,i_0_96,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_81,i_0_88,i_0_128,i_0_127,i_0_116,i_0_124,i_0_122,i_0_121]) ).
cnf(i_0_3033,plain,
relation(relation_inverse_image(relation_inverse_image(empty_set,X1),empty_set)),
inference(scs_inference,[],[i_0_2982,i_0_2939,i_0_2975,i_0_2941,i_0_2320,i_0_2991,i_0_2973,i_0_2886,i_0_2911,i_0_2829,i_0_2947,i_0_2857,i_0_2932,i_0_1986,i_0_1367,i_0_776,i_0_731,i_0_2842,i_0_2809,i_0_632,i_0_2634,i_0_95,i_0_96,i_0_106,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_81,i_0_88,i_0_128,i_0_127,i_0_116,i_0_124,i_0_122,i_0_121,i_0_125,i_0_131,i_0_75,i_0_100]) ).
cnf(i_0_3035,plain,
~ empty(esk7_1(esk7_1(esk7_1(relation_inverse_image(esk14_0,esk12_0))))),
inference(scs_inference,[],[i_0_2982,i_0_2939,i_0_2975,i_0_2941,i_0_2320,i_0_2991,i_0_2973,i_0_2886,i_0_2911,i_0_2829,i_0_2947,i_0_2857,i_0_2932,i_0_1986,i_0_1367,i_0_776,i_0_731,i_0_2842,i_0_2809,i_0_632,i_0_2634,i_0_95,i_0_96,i_0_106,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_81,i_0_88,i_0_128,i_0_127,i_0_116,i_0_124,i_0_122,i_0_121,i_0_125,i_0_131,i_0_75,i_0_100,i_0_94]) ).
cnf(i_0_3037,plain,
element(esk7_1(esk12_0),powerset(esk12_0)),
inference(scs_inference,[],[i_0_2982,i_0_2939,i_0_2975,i_0_2941,i_0_2320,i_0_2991,i_0_2973,i_0_2886,i_0_2911,i_0_2829,i_0_2947,i_0_2857,i_0_2932,i_0_1986,i_0_1367,i_0_776,i_0_731,i_0_2842,i_0_2809,i_0_632,i_0_2634,i_0_738,i_0_95,i_0_96,i_0_106,i_0_87,i_0_85,i_0_89,i_0_83,i_0_86,i_0_115,i_0_81,i_0_88,i_0_128,i_0_127,i_0_116,i_0_124,i_0_122,i_0_121,i_0_125,i_0_131,i_0_75,i_0_100,i_0_94,i_0_90]) ).
cnf(c_0_117,plain,
( in(unordered_pair(unordered_pair(X1,esk1_4(X2,X3,X4,X1)),singleton(X1)),X2)
| X4 != relation_inverse_image(X2,X3)
| ~ relation(X2)
| ~ in(X1,X4) ),
i_0_71 ).
cnf(c_0_118,plain,
unordered_pair(X1,X2) = unordered_pair(X2,X1),
i_0_92 ).
cnf(c_0_119,negated_conjecture,
~ subset(relation_inverse_image(esk14_0,esk12_0),relation_inverse_image(esk14_0,esk13_0)),
i_0_78 ).
cnf(c_0_120,plain,
( in(esk4_2(X1,X2),X1)
| subset(X1,X2) ),
i_0_83 ).
cnf(c_0_121,plain,
( in(esk1_4(X1,X2,X3,X4),X2)
| ~ in(X4,X3)
| X3 != relation_inverse_image(X1,X2)
| ~ relation(X1) ),
i_0_74 ).
cnf(c_0_122,plain,
( in(X1,X2)
| X2 != relation_inverse_image(X3,X4)
| ~ relation(X3)
| ~ in(X5,X4)
| ~ in(unordered_pair(unordered_pair(X1,X5),singleton(X1)),X3) ),
i_0_76 ).
cnf(c_0_123,plain,
( in(unordered_pair(singleton(X1),unordered_pair(X1,esk1_4(X2,X3,relation_inverse_image(X2,X3),X1))),X2)
| ~ relation(X2)
| ~ in(X1,relation_inverse_image(X2,X3)) ),
inference(er,[status(thm)],[inference(rw,[status(thm)],[c_0_117,c_0_118])]) ).
cnf(c_0_124,negated_conjecture,
in(esk4_2(relation_inverse_image(esk14_0,esk12_0),relation_inverse_image(esk14_0,esk13_0)),relation_inverse_image(esk14_0,esk12_0)),
inference(spm,[status(thm)],[c_0_119,c_0_120]) ).
cnf(c_0_125,negated_conjecture,
relation(esk14_0),
i_0_106 ).
cnf(c_0_126,plain,
( in(X1,X2)
| ~ subset(X3,X2)
| ~ in(X1,X3) ),
i_0_82 ).
cnf(c_0_127,negated_conjecture,
subset(esk12_0,esk13_0),
i_0_101 ).
cnf(c_0_128,plain,
( in(esk1_4(X1,X2,relation_inverse_image(X1,X2),X3),X2)
| ~ relation(X1)
| ~ in(X3,relation_inverse_image(X1,X2)) ),
inference(er,[status(thm)],[c_0_121]) ).
cnf(c_0_129,plain,
( in(X1,relation_inverse_image(X2,X3))
| ~ relation(X2)
| ~ in(unordered_pair(singleton(X1),unordered_pair(X1,X4)),X2)
| ~ in(X4,X3) ),
inference(er,[status(thm)],[inference(rw,[status(thm)],[c_0_122,c_0_118])]) ).
cnf(c_0_130,negated_conjecture,
in(unordered_pair(singleton(esk4_2(relation_inverse_image(esk14_0,esk12_0),relation_inverse_image(esk14_0,esk13_0))),unordered_pair(esk4_2(relation_inverse_image(esk14_0,esk12_0),relation_inverse_image(esk14_0,esk13_0)),esk1_4(esk14_0,esk12_0,relation_inverse_image(esk14_0,esk12_0),esk4_2(relation_inverse_image(esk14_0,esk12_0),relation_inverse_image(esk14_0,esk13_0))))),esk14_0),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_123,c_0_124]),c_0_125])]) ).
cnf(c_0_131,negated_conjecture,
( in(X1,esk13_0)
| ~ in(X1,esk12_0) ),
inference(spm,[status(thm)],[c_0_126,c_0_127]) ).
cnf(c_0_132,negated_conjecture,
in(esk1_4(esk14_0,esk12_0,relation_inverse_image(esk14_0,esk12_0),esk4_2(relation_inverse_image(esk14_0,esk12_0),relation_inverse_image(esk14_0,esk13_0))),esk12_0),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_128,c_0_124]),c_0_125])]) ).
cnf(c_0_133,plain,
( subset(X1,X2)
| ~ in(esk4_2(X1,X2),X2) ),
i_0_79 ).
cnf(c_0_134,plain,
( in(esk4_2(relation_inverse_image(esk14_0,esk12_0),relation_inverse_image(esk14_0,esk13_0)),relation_inverse_image(esk14_0,X1))
| ~ in(esk1_4(esk14_0,esk12_0,relation_inverse_image(esk14_0,esk12_0),esk4_2(relation_inverse_image(esk14_0,esk12_0),relation_inverse_image(esk14_0,esk13_0))),X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_129,c_0_130]),c_0_125])]) ).
cnf(c_0_135,negated_conjecture,
in(esk1_4(esk14_0,esk12_0,relation_inverse_image(esk14_0,esk12_0),esk4_2(relation_inverse_image(esk14_0,esk12_0),relation_inverse_image(esk14_0,esk13_0))),esk13_0),
inference(spm,[status(thm)],[c_0_131,c_0_132]) ).
cnf(c_0_136,negated_conjecture,
~ in(esk4_2(relation_inverse_image(esk14_0,esk12_0),relation_inverse_image(esk14_0,esk13_0)),relation_inverse_image(esk14_0,esk13_0)),
inference(spm,[status(thm)],[c_0_119,c_0_133]) ).
cnf(c_0_137,negated_conjecture,
$false,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_134,c_0_135]),c_0_136]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SEU211+1 : TPTP v9.2.1. Released v3.3.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 : n015.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:48:17 EDT 2026
% 0.16/0.33 % CPUTime :
% 0.16/0.34 % start to proof: theBenchmark
% 186.73/142.50 % Version : CSE_E---1.7
% 186.73/142.50 % Problem : theBenchmark.p
% 186.73/142.50 % SZS status Theorem for theBenchmark.p
% 186.73/142.50 % SZS output start CNFRefutation
% See solution above
% 192.93/148.75 % Total time : 142.094s
%------------------------------------------------------------------------------