%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SEU164+3 : TPTP v9.2.1. Bugfixed v4.0.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 : n024.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:53 PM UTC 2026
% Result : Theorem 50.17s 25.55s
% Output : CNFRefutation 51.53s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 26)
% Comments :
%------------------------------------------------------------------------------
fof(antisymmetry_r2_hidden,axiom,
! [X1,X2] :
( in(X1,X2)
=> ~ in(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',antisymmetry_r2_hidden) ).
fof(t99_zfmisc_1,conjecture,
! [X1] : union(powerset(X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t99_zfmisc_1) ).
fof(rc2_xboole_0,axiom,
? [X1] : ~ empty(X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc2_xboole_0) ).
fof(d4_tarski,axiom,
! [X1,X2] :
( X2 = union(X1)
<=> ! [X3] :
( in(X3,X2)
<=> ? [X4] :
( in(X3,X4)
& in(X4,X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d4_tarski) ).
fof(d1_zfmisc_1,axiom,
! [X1,X2] :
( X2 = powerset(X1)
<=> ! [X3] :
( in(X3,X2)
<=> subset(X3,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_zfmisc_1) ).
fof(t2_tarski,axiom,
! [X1,X2] :
( ! [X3] :
( in(X3,X1)
<=> in(X3,X2) )
=> X1 = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_tarski) ).
fof(d1_tarski,axiom,
! [X1,X2] :
( X2 = singleton(X1)
<=> ! [X3] :
( in(X3,X2)
<=> X3 = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_tarski) ).
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(l2_zfmisc_1,axiom,
! [X1,X2] :
( subset(singleton(X1),X2)
<=> in(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l2_zfmisc_1) ).
fof(reflexivity_r1_tarski,axiom,
! [X1,X2] : subset(X1,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',reflexivity_r1_tarski) ).
fof(rc1_xboole_0,axiom,
? [X1] : empty(X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc1_xboole_0) ).
fof(i_0_11,plain,
! [X1,X2] :
( in(X1,X2)
=> ~ in(X2,X1) ),
inference(fof_simplification,[status(thm)],[antisymmetry_r2_hidden]) ).
fof(i_0_12,negated_conjecture,
~ ! [X1] : union(powerset(X1)) = X1,
inference(assume_negation,[status(cth)],[t99_zfmisc_1]) ).
fof(i_0_13,plain,
? [X1] : ~ empty(X1),
inference(fof_simplification,[status(thm)],[rc2_xboole_0]) ).
fof(i_0_14,plain,
! [X52,X53,X54,X56,X57,X58,X59,X61] :
( ( in(X54,esk4_3(X52,X53,X54))
| ~ in(X54,X53)
| X53 != union(X52) )
& ( in(esk4_3(X52,X53,X54),X52)
| ~ in(X54,X53)
| X53 != union(X52) )
& ( ~ in(X56,X57)
| ~ in(X57,X52)
| in(X56,X53)
| X53 != union(X52) )
& ( ~ in(esk5_2(X58,X59),X59)
| ~ in(esk5_2(X58,X59),X61)
| ~ in(X61,X58)
| X59 = union(X58) )
& ( in(esk5_2(X58,X59),esk6_2(X58,X59))
| in(esk5_2(X58,X59),X59)
| X59 = union(X58) )
& ( in(esk6_2(X58,X59),X58)
| in(esk5_2(X58,X59),X59)
| X59 = union(X58) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[d4_tarski])])])])])]) ).
fof(i_0_15,plain,
! [X39,X40,X41,X42,X43,X44] :
( ( ~ in(X41,X40)
| subset(X41,X39)
| X40 != powerset(X39) )
& ( ~ subset(X42,X39)
| in(X42,X40)
| X40 != powerset(X39) )
& ( ~ in(esk2_2(X43,X44),X44)
| ~ subset(esk2_2(X43,X44),X43)
| X44 = powerset(X43) )
& ( in(esk2_2(X43,X44),X44)
| subset(esk2_2(X43,X44),X43)
| X44 = powerset(X43) ) ),
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)],[d1_zfmisc_1])])])])])]) ).
fof(i_0_16,plain,
! [X68,X69] :
( ( ~ in(esk9_2(X68,X69),X68)
| ~ in(esk9_2(X68,X69),X69)
| X68 = X69 )
& ( in(esk9_2(X68,X69),X68)
| in(esk9_2(X68,X69),X69)
| X68 = X69 ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[t2_tarski])])])]) ).
fof(i_0_17,plain,
! [X32,X33,X34,X35,X36,X37] :
( ( ~ in(X34,X33)
| X34 = X32
| X33 != singleton(X32) )
& ( X35 != X32
| in(X35,X33)
| X33 != singleton(X32) )
& ( ~ in(esk1_2(X36,X37),X37)
| esk1_2(X36,X37) != X36
| X37 = singleton(X36) )
& ( in(esk1_2(X36,X37),X37)
| esk1_2(X36,X37) = X36
| X37 = singleton(X36) ) ),
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)],[d1_tarski])])])])])]) ).
fof(i_0_18,plain,
! [X46,X47,X48,X49,X50] :
( ( ~ subset(X46,X47)
| ~ in(X48,X46)
| in(X48,X47) )
& ( in(esk3_2(X49,X50),X49)
| subset(X49,X50) )
& ( ~ in(esk3_2(X49,X50),X50)
| subset(X49,X50) ) ),
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_19,plain,
! [X63,X64] :
( ( ~ subset(singleton(X63),X64)
| in(X63,X64) )
& ( ~ in(X63,X64)
| subset(singleton(X63),X64) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[l2_zfmisc_1])]) ).
fof(i_0_20,plain,
! [X30,X31] :
( ~ in(X30,X31)
| ~ in(X31,X30) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_11])]) ).
fof(i_0_21,plain,
! [X67] : subset(X67,X67),
inference(variable_rename,[status(thm)],[inference(fof_simplification,[status(thm)],[reflexivity_r1_tarski])]) ).
fof(i_0_22,negated_conjecture,
union(powerset(esk10_0)) != esk10_0,
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_12])])]) ).
fof(i_0_23,plain,
~ empty(esk8_0),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[i_0_13])]) ).
fof(i_0_24,plain,
empty(esk7_0),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[rc1_xboole_0])]) ).
cnf(i_0_25,plain,
( X2 = union(X1)
| ~ in(esk5_2(X1,X2),X2)
| ~ in(esk5_2(X1,X2),X3)
| ~ in(X3,X1) ),
inference(split_conjunct,[status(thm)],[i_0_14]),
[final] ).
cnf(i_0_26,plain,
( in(esk4_3(X1,X2,X3),X1)
| ~ in(X3,X2)
| X2 != union(X1) ),
inference(split_conjunct,[status(thm)],[i_0_14]),
[final] ).
cnf(i_0_27,plain,
( in(X1,esk4_3(X2,X3,X1))
| ~ in(X1,X3)
| X3 != union(X2) ),
inference(split_conjunct,[status(thm)],[i_0_14]),
[final] ).
cnf(i_0_28,plain,
( X2 = powerset(X1)
| ~ in(esk2_2(X1,X2),X2)
| ~ subset(esk2_2(X1,X2),X1) ),
inference(split_conjunct,[status(thm)],[i_0_15]),
[final] ).
cnf(i_0_29,plain,
( X1 = X2
| ~ in(esk9_2(X1,X2),X1)
| ~ in(esk9_2(X1,X2),X2) ),
inference(split_conjunct,[status(thm)],[i_0_16]),
[final] ).
cnf(i_0_30,plain,
( in(esk5_2(X1,X2),esk6_2(X1,X2))
| in(esk5_2(X1,X2),X2)
| X2 = union(X1) ),
inference(split_conjunct,[status(thm)],[i_0_14]),
[final] ).
cnf(i_0_31,plain,
( X2 = singleton(X1)
| ~ in(esk1_2(X1,X2),X2)
| esk1_2(X1,X2) != X1 ),
inference(split_conjunct,[status(thm)],[i_0_17]),
[final] ).
cnf(i_0_32,plain,
( in(esk6_2(X1,X2),X1)
| in(esk5_2(X1,X2),X2)
| X2 = union(X1) ),
inference(split_conjunct,[status(thm)],[i_0_14]),
[final] ).
cnf(i_0_33,plain,
( in(esk2_2(X1,X2),X2)
| subset(esk2_2(X1,X2),X1)
| X2 = powerset(X1) ),
inference(split_conjunct,[status(thm)],[i_0_15]),
[final] ).
cnf(i_0_34,plain,
( in(esk9_2(X1,X2),X1)
| in(esk9_2(X1,X2),X2)
| X1 = X2 ),
inference(split_conjunct,[status(thm)],[i_0_16]),
[final] ).
cnf(i_0_35,plain,
( subset(X1,X2)
| ~ in(esk3_2(X1,X2),X2) ),
inference(split_conjunct,[status(thm)],[i_0_18]),
[final] ).
cnf(i_0_36,plain,
( in(X1,X4)
| ~ in(X1,X2)
| ~ in(X2,X3)
| X4 != union(X3) ),
inference(split_conjunct,[status(thm)],[i_0_14]),
[final] ).
cnf(i_0_37,plain,
( in(esk1_2(X1,X2),X2)
| esk1_2(X1,X2) = X1
| X2 = singleton(X1) ),
inference(split_conjunct,[status(thm)],[i_0_17]),
[final] ).
cnf(i_0_38,plain,
( in(X3,X2)
| ~ subset(X1,X2)
| ~ in(X3,X1) ),
inference(split_conjunct,[status(thm)],[i_0_18]),
[final] ).
cnf(i_0_39,plain,
( in(esk3_2(X1,X2),X1)
| subset(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_18]),
[final] ).
cnf(i_0_40,plain,
( in(X1,X2)
| ~ subset(singleton(X1),X2) ),
inference(split_conjunct,[status(thm)],[i_0_19]),
[final] ).
cnf(i_0_41,plain,
( subset(X1,X3)
| ~ in(X1,X2)
| X2 != powerset(X3) ),
inference(split_conjunct,[status(thm)],[i_0_15]),
[final] ).
cnf(i_0_42,plain,
( in(X1,X3)
| ~ subset(X1,X2)
| X3 != powerset(X2) ),
inference(split_conjunct,[status(thm)],[i_0_15]),
[final] ).
cnf(i_0_43,plain,
( ~ in(X1,X2)
| ~ in(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_20]),
[final] ).
cnf(i_0_44,plain,
( subset(singleton(X1),X2)
| ~ in(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_19]),
[final] ).
cnf(i_0_45,plain,
( X1 = X3
| ~ in(X1,X2)
| X2 != singleton(X3) ),
inference(split_conjunct,[status(thm)],[i_0_17]),
[final] ).
cnf(i_0_46,plain,
( in(X1,X3)
| X1 != X2
| X3 != singleton(X2) ),
inference(split_conjunct,[status(thm)],[i_0_17]),
[final] ).
cnf(i_0_47,plain,
subset(X1,X1),
inference(split_conjunct,[status(thm)],[i_0_21]),
[final] ).
cnf(i_0_48,negated_conjecture,
union(powerset(esk10_0)) != esk10_0,
inference(split_conjunct,[status(thm)],[i_0_22]),
[final] ).
cnf(i_0_49,plain,
~ empty(esk8_0),
inference(split_conjunct,[status(thm)],[i_0_23]),
[final] ).
cnf(i_0_50,plain,
empty(esk7_0),
inference(split_conjunct,[status(thm)],[i_0_24]),
[final] ).
cnf(i_0_51,axiom,
X1 = X1 ).
cnf(i_0_52,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_53,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_54,axiom,
( X1 != X2
| union(X1) = union(X2) ) ).
cnf(i_0_55,axiom,
( X1 != X2
| powerset(X1) = powerset(X2) ) ).
cnf(i_0_56,axiom,
( X1 != X2
| singleton(X1) = singleton(X2) ) ).
cnf(i_0_57,axiom,
( X1 != X2
| esk1_2(X1,X3) = esk1_2(X2,X3) ) ).
cnf(i_0_58,axiom,
( X1 != X2
| esk1_2(X3,X1) = esk1_2(X3,X2) ) ).
cnf(i_0_59,axiom,
( X1 != X2
| ~ in(X1,X3)
| in(X2,X3) ) ).
cnf(i_0_60,axiom,
( X1 != X2
| ~ in(X3,X1)
| in(X3,X2) ) ).
cnf(i_0_61,axiom,
( X1 != X2
| ~ subset(X1,X3)
| subset(X2,X3) ) ).
cnf(i_0_62,axiom,
( X1 != X2
| ~ subset(X3,X1)
| subset(X3,X2) ) ).
cnf(i_0_63,axiom,
( X1 != X2
| ~ empty(X1)
| empty(X2) ) ).
cnf(i_0_51_001,axiom,
X1 = X1 ).
cnf(i_0_52_002,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_53_003,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_54_004,axiom,
( X1 != X2
| union(X1) = union(X2) ) ).
cnf(i_0_55_005,axiom,
( X1 != X2
| powerset(X1) = powerset(X2) ) ).
cnf(i_0_56_006,axiom,
( X1 != X2
| singleton(X1) = singleton(X2) ) ).
cnf(i_0_57_007,axiom,
( X1 != X2
| esk1_2(X1,X3) = esk1_2(X2,X3) ) ).
cnf(i_0_58_008,axiom,
( X1 != X2
| esk1_2(X3,X1) = esk1_2(X3,X2) ) ).
cnf(i_0_59_009,axiom,
( X1 != X2
| ~ in(X1,X3)
| in(X2,X3) ) ).
cnf(i_0_60_010,axiom,
( X1 != X2
| ~ in(X3,X1)
| in(X3,X2) ) ).
cnf(i_0_61_011,axiom,
( X1 != X2
| ~ subset(X1,X3)
| subset(X2,X3) ) ).
cnf(i_0_62_012,axiom,
( X1 != X2
| ~ subset(X3,X1)
| subset(X3,X2) ) ).
cnf(i_0_63_013,axiom,
( X1 != X2
| ~ empty(X1)
| empty(X2) ) ).
cnf(i_0_64,plain,
( ~ in(X1,union(X2))
| in(esk4_3(X2,union(X2),X1),X2) ),
inference(equality_inference,[],[26]) ).
cnf(i_0_65,plain,
( ~ in(X1,union(X2))
| in(X1,esk4_3(X2,union(X2),X1)) ),
inference(equality_inference,[],[27]) ).
cnf(i_0_66,plain,
( in(X1,union(X2))
| ~ in(X1,X3)
| ~ in(X3,X2) ),
inference(equality_inference,[],[36]) ).
cnf(i_0_67,plain,
( subset(X1,X2)
| ~ in(X1,powerset(X2)) ),
inference(equality_inference,[],[41]) ).
cnf(i_0_68,plain,
( in(X1,powerset(X2))
| ~ subset(X1,X2) ),
inference(equality_inference,[],[42]) ).
cnf(i_0_69,plain,
( X1 = X2
| ~ in(X1,singleton(X2)) ),
inference(equality_inference,[],[45]) ).
cnf(i_0_70,plain,
in(X1,powerset(X1)),
inference(scs_inference,[],[i_0_47,i_0_68]) ).
cnf(i_0_71,plain,
( ~ subset(X1,X2)
| in(X1,powerset(X2)) ),
inference(rename_variables,[],[i_0_68]) ).
cnf(i_0_72,plain,
in(X1,singleton(X1)),
inference(scs_inference,[],[i_0_47,i_0_68,i_0_40]) ).
cnf(i_0_73,plain,
subset(X1,X1),
inference(rename_variables,[],[i_0_47]) ).
cnf(i_0_74,plain,
( ~ subset(singleton(X1),X2)
| in(X1,X2) ),
inference(rename_variables,[],[i_0_40]) ).
cnf(i_0_75,plain,
~ in(powerset(singleton(X1)),singleton(X1)),
inference(scs_inference,[],[i_0_47,i_0_68,i_0_40,i_0_43]) ).
cnf(i_0_76,plain,
( ~ in(X1,X2)
| ~ in(X2,X1) ),
inference(rename_variables,[],[i_0_43]) ).
cnf(i_0_77,plain,
X1 != powerset(singleton(X1)),
inference(scs_inference,[],[i_0_47,i_0_68,i_0_40,i_0_43,i_0_59]) ).
cnf(i_0_78,plain,
esk7_0 != esk8_0,
inference(scs_inference,[],[i_0_47,i_0_49,i_0_50,i_0_68,i_0_40,i_0_43,i_0_59,i_0_63]) ).
cnf(i_0_79,plain,
X1 != singleton(powerset(X1)),
inference(scs_inference,[],[i_0_47,i_0_49,i_0_50,i_0_68,i_0_40,i_0_43,i_0_59,i_0_63,i_0_55]) ).
cnf(i_0_80,plain,
( in(esk1_2(powerset(X1),X1),X1)
| esk1_2(powerset(X1),X1) = powerset(X1) ),
inference(scs_inference,[],[i_0_47,i_0_49,i_0_50,i_0_68,i_0_40,i_0_43,i_0_59,i_0_63,i_0_55,i_0_37]) ).
cnf(i_0_81,plain,
( X1 = singleton(X2)
| in(esk1_2(X2,X1),X1)
| esk1_2(X2,X1) = X2 ),
inference(rename_variables,[],[i_0_37]) ).
cnf(i_0_82,plain,
( esk1_2(powerset(X1),X1) != powerset(X1)
| esk1_2(powerset(X1),X1) = powerset(X1) ),
inference(scs_inference,[],[i_0_47,i_0_49,i_0_50,i_0_68,i_0_40,i_0_43,i_0_59,i_0_63,i_0_55,i_0_37,i_0_31]) ).
cnf(i_0_83,plain,
( ~ in(esk1_2(X1,X2),X2)
| esk1_2(X1,X2) != X1
| X2 = singleton(X1) ),
inference(rename_variables,[],[i_0_31]) ).
cnf(i_0_84,plain,
( ~ in(powerset(singleton(powerset(X1))),powerset(X1))
| esk1_2(powerset(X1),X1) = powerset(X1)
| subset(esk2_2(singleton(powerset(X1)),powerset(X1)),singleton(powerset(X1)))
| in(esk2_2(singleton(powerset(X1)),powerset(X1)),powerset(X1)) ),
inference(scs_inference,[],[i_0_47,i_0_49,i_0_50,i_0_68,i_0_40,i_0_43,i_0_59,i_0_63,i_0_55,i_0_37,i_0_31,i_0_66,i_0_60,i_0_33]) ).
cnf(i_0_85,plain,
~ in(powerset(X1),X1),
inference(scs_inference,[],[i_0_70,i_0_43]) ).
cnf(i_0_86,plain,
( ~ in(X1,X2)
| ~ in(X2,X1) ),
inference(rename_variables,[],[i_0_43]) ).
cnf(i_0_87,plain,
singleton(powerset(X1)) != X1,
inference(scs_inference,[],[i_0_70,i_0_72,i_0_43,i_0_60]) ).
cnf(i_0_88,plain,
in(X1,singleton(X1)),
inference(rename_variables,[],[i_0_72]) ).
cnf(i_0_89,plain,
powerset(singleton(X1)) != X1,
inference(scs_inference,[],[i_0_70,i_0_72,i_0_43,i_0_60,i_0_56]) ).
cnf(i_0_90,plain,
( in(esk2_2(singleton(X1),X1),X1)
| subset(esk2_2(singleton(X1),X1),singleton(X1)) ),
inference(scs_inference,[],[i_0_70,i_0_77,i_0_72,i_0_43,i_0_60,i_0_56,i_0_33]) ).
cnf(i_0_91,plain,
( X1 = powerset(X2)
| in(esk2_2(X2,X1),X1)
| subset(esk2_2(X2,X1),X2) ),
inference(rename_variables,[],[i_0_33]) ).
cnf(i_0_92,plain,
( ~ subset(esk2_2(singleton(X1),X1),singleton(X1))
| subset(esk2_2(singleton(X1),X1),singleton(X1)) ),
inference(scs_inference,[],[i_0_70,i_0_77,i_0_72,i_0_43,i_0_60,i_0_56,i_0_33,i_0_28]) ).
cnf(i_0_93,plain,
( ~ in(esk2_2(X1,X2),X2)
| ~ subset(esk2_2(X1,X2),X1)
| X2 = powerset(X1) ),
inference(rename_variables,[],[i_0_28]) ).
cnf(i_0_94,plain,
subset(X1,X1),
inference(rename_variables,[],[i_0_47]) ).
cnf(i_0_95,plain,
in(X1,powerset(X1)),
inference(rename_variables,[],[i_0_70]) ).
cnf(i_0_96,plain,
in(X1,singleton(X1)),
inference(rename_variables,[],[i_0_72]) ).
cnf(i_0_97,plain,
~ in(powerset(singleton(X1)),singleton(X1)),
inference(rename_variables,[],[i_0_75]) ).
cnf(i_0_99,plain,
~ in(singleton(X1),X1),
inference(scs_inference,[],[i_0_72,i_0_43]) ).
cnf(i_0_100,plain,
( ~ in(X1,X2)
| ~ in(X2,X1) ),
inference(rename_variables,[],[i_0_43]) ).
cnf(i_0_101,plain,
~ subset(powerset(powerset(X1)),X1),
inference(scs_inference,[],[i_0_70,i_0_85,i_0_72,i_0_43,i_0_38]) ).
cnf(i_0_102,plain,
in(X1,powerset(X1)),
inference(rename_variables,[],[i_0_70]) ).
cnf(i_0_103,plain,
( ~ in(X1,X2)
| in(X1,X3)
| ~ subset(X2,X3) ),
inference(rename_variables,[],[i_0_38]) ).
cnf(i_0_104,plain,
powerset(powerset(X1)) != X1,
inference(scs_inference,[],[i_0_70,i_0_102,i_0_85,i_0_72,i_0_43,i_0_38,i_0_60]) ).
cnf(i_0_105,plain,
in(X1,powerset(X1)),
inference(rename_variables,[],[i_0_70]) ).
cnf(i_0_106,plain,
X1 != powerset(powerset(X1)),
inference(scs_inference,[],[i_0_70,i_0_102,i_0_105,i_0_85,i_0_72,i_0_43,i_0_38,i_0_60,i_0_59]) ).
cnf(i_0_107,plain,
~ in(powerset(X1),X1),
inference(rename_variables,[],[i_0_85]) ).
cnf(i_0_108,plain,
( in(esk2_2(powerset(X1),X1),X1)
| subset(esk2_2(powerset(X1),X1),powerset(X1)) ),
inference(scs_inference,[],[i_0_70,i_0_102,i_0_105,i_0_85,i_0_72,i_0_43,i_0_38,i_0_60,i_0_59,i_0_33]) ).
cnf(i_0_109,plain,
( X1 = powerset(X2)
| in(esk2_2(X2,X1),X1)
| subset(esk2_2(X2,X1),X2) ),
inference(rename_variables,[],[i_0_33]) ).
cnf(i_0_110,plain,
( ~ subset(esk2_2(powerset(X1),X1),powerset(X1))
| subset(esk2_2(powerset(X1),X1),powerset(X1)) ),
inference(scs_inference,[],[i_0_70,i_0_102,i_0_105,i_0_85,i_0_72,i_0_43,i_0_38,i_0_60,i_0_59,i_0_33,i_0_28]) ).
cnf(i_0_111,plain,
( ~ in(esk2_2(X1,X2),X2)
| ~ subset(esk2_2(X1,X2),X1)
| X2 = powerset(X1) ),
inference(rename_variables,[],[i_0_28]) ).
cnf(i_0_112,plain,
singleton(powerset(X1)) != X1,
inference(rename_variables,[],[i_0_87]) ).
cnf(i_0_113,plain,
( ~ in(powerset(union(X1)),esk2_2(powerset(X1),X1))
| subset(esk2_2(powerset(X1),X1),powerset(X1)) ),
inference(scs_inference,[],[i_0_70,i_0_102,i_0_105,i_0_87,i_0_85,i_0_107,i_0_72,i_0_43,i_0_38,i_0_60,i_0_59,i_0_33,i_0_28,i_0_30,i_0_66]) ).
cnf(i_0_114,plain,
~ in(powerset(X1),X1),
inference(rename_variables,[],[i_0_85]) ).
cnf(i_0_115,plain,
( ~ in(X1,X2)
| in(X3,union(X2))
| ~ in(X3,X1) ),
inference(rename_variables,[],[i_0_66]) ).
cnf(i_0_116,plain,
singleton(powerset(X1)) != X1,
inference(rename_variables,[],[i_0_87]) ).
cnf(i_0_117,plain,
( subset(esk2_2(powerset(X1),X1),powerset(X1))
| in(esk1_2(X2,singleton(powerset(singleton(X2)))),singleton(powerset(singleton(X2))))
| esk1_2(X2,singleton(powerset(singleton(X2)))) = X2 ),
inference(scs_inference,[],[i_0_70,i_0_102,i_0_105,i_0_87,i_0_112,i_0_85,i_0_107,i_0_72,i_0_43,i_0_38,i_0_60,i_0_59,i_0_33,i_0_28,i_0_66,i_0_37]) ).
cnf(i_0_118,plain,
~ subset(powerset(singleton(X1)),X1),
inference(scs_inference,[],[i_0_70,i_0_99,i_0_38]) ).
cnf(i_0_119,plain,
in(X1,powerset(X1)),
inference(rename_variables,[],[i_0_70]) ).
cnf(i_0_120,plain,
( ~ in(X1,X2)
| in(X1,X3)
| ~ subset(X2,X3) ),
inference(rename_variables,[],[i_0_38]) ).
cnf(i_0_121,plain,
~ subset(singleton(singleton(X1)),X1),
inference(scs_inference,[],[i_0_99,i_0_72,i_0_38]) ).
cnf(i_0_122,plain,
in(X1,singleton(X1)),
inference(rename_variables,[],[i_0_72]) ).
cnf(i_0_123,plain,
( ~ in(X1,X2)
| in(X1,X3)
| ~ subset(X2,X3) ),
inference(rename_variables,[],[i_0_38]) ).
cnf(i_0_124,plain,
X1 != singleton(singleton(X1)),
inference(scs_inference,[],[i_0_47,i_0_99,i_0_72,i_0_38,i_0_61]) ).
cnf(i_0_125,plain,
( X1 != X2
| ~ subset(singleton(singleton(X2)),X1) ),
inference(scs_inference,[],[i_0_47,i_0_99,i_0_72,i_0_38,i_0_61,i_0_62]) ).
cnf(i_0_126,plain,
( X1 = union(X2)
| in(esk5_2(X2,X1),esk6_2(X2,X1))
| in(esk5_2(X2,X1),X1) ),
inference(rename_variables,[],[i_0_30]) ).
cnf(i_0_127,plain,
~ in(powerset(X1),X1),
inference(rename_variables,[],[i_0_85]) ).
cnf(i_0_128,plain,
~ in(singleton(X1),X1),
inference(rename_variables,[],[i_0_99]) ).
cnf(i_0_129,plain,
in(X1,powerset(X1)),
inference(rename_variables,[],[i_0_70]) ).
cnf(i_0_130,plain,
~ in(singleton(X1),X1),
inference(rename_variables,[],[i_0_99]) ).
cnf(i_0_132,plain,
~ subset(singleton(singleton(X1)),X1),
inference(equality_inference,[],[125]) ).
cnf(i_0_133,plain,
singleton(singleton(X1)) != X1,
inference(scs_inference,[],[i_0_47,i_0_125]) ).
cnf(i_0_134,plain,
subset(X1,X1),
inference(rename_variables,[],[i_0_47]) ).
cnf(i_0_135,plain,
( in(esk1_2(singleton(X1),X1),X1)
| esk1_2(singleton(X1),X1) = singleton(X1) ),
inference(scs_inference,[],[i_0_124,i_0_47,i_0_125,i_0_37]) ).
cnf(i_0_136,plain,
( X1 = singleton(X2)
| in(esk1_2(X2,X1),X1)
| esk1_2(X2,X1) = X2 ),
inference(rename_variables,[],[i_0_37]) ).
cnf(i_0_137,plain,
( ~ in(X1,esk1_2(singleton(X1),X1))
| esk1_2(singleton(X1),X1) = singleton(X1) ),
inference(scs_inference,[],[i_0_124,i_0_47,i_0_125,i_0_37,i_0_43]) ).
cnf(i_0_138,plain,
( ~ in(X1,X2)
| ~ in(X2,X1) ),
inference(rename_variables,[],[i_0_43]) ).
cnf(i_0_139,plain,
( esk1_2(singleton(X1),X1) != singleton(X1)
| esk1_2(singleton(X1),X1) = singleton(X1) ),
inference(scs_inference,[],[i_0_124,i_0_47,i_0_125,i_0_37,i_0_43,i_0_31]) ).
cnf(i_0_140,plain,
( ~ in(esk1_2(X1,X2),X2)
| esk1_2(X1,X2) != X1
| X2 = singleton(X1) ),
inference(rename_variables,[],[i_0_31]) ).
cnf(i_0_141,plain,
powerset(singleton(X1)) != X1,
inference(rename_variables,[],[i_0_89]) ).
cnf(i_0_142,plain,
( ~ in(singleton(union(X1)),esk1_2(singleton(X1),X1))
| esk1_2(singleton(X1),X1) = singleton(X1) ),
inference(scs_inference,[],[i_0_89,i_0_124,i_0_47,i_0_99,i_0_125,i_0_37,i_0_43,i_0_31,i_0_30,i_0_66]) ).
cnf(i_0_143,plain,
~ in(singleton(X1),X1),
inference(rename_variables,[],[i_0_99]) ).
cnf(i_0_144,plain,
( ~ in(X1,X2)
| in(X3,union(X2))
| ~ in(X3,X1) ),
inference(rename_variables,[],[i_0_66]) ).
cnf(i_0_145,plain,
in(X1,powerset(X1)),
inference(rename_variables,[],[i_0_70]) ).
cnf(i_0_146,plain,
~ in(singleton(X1),X1),
inference(rename_variables,[],[i_0_99]) ).
cnf(i_0_148,plain,
~ subset(singleton(powerset(X1)),X1),
inference(scs_inference,[],[i_0_85,i_0_72,i_0_38]) ).
cnf(i_0_149,plain,
in(X1,singleton(X1)),
inference(rename_variables,[],[i_0_72]) ).
cnf(i_0_150,plain,
( ~ in(X1,X2)
| in(X1,X3)
| ~ subset(X2,X3) ),
inference(rename_variables,[],[i_0_38]) ).
cnf(i_0_151,plain,
esk10_0 != union(powerset(esk10_0)),
inference(scs_inference,[],[i_0_48,i_0_52]) ).
cnf(i_0_152,plain,
~ in(union(powerset(esk10_0)),singleton(esk10_0)),
inference(scs_inference,[],[i_0_48,i_0_52,i_0_69]) ).
cnf(i_0_153,plain,
( X1 = X2
| ~ in(X1,singleton(X2)) ),
inference(rename_variables,[],[i_0_69]) ).
cnf(i_0_154,plain,
~ in(powerset(singleton(X1)),powerset(X1)),
inference(scs_inference,[],[i_0_48,i_0_118,i_0_52,i_0_69,i_0_67]) ).
cnf(i_0_155,plain,
( subset(X1,X2)
| ~ in(X1,powerset(X2)) ),
inference(rename_variables,[],[i_0_67]) ).
cnf(i_0_156,plain,
subset(singleton(X1),powerset(X1)),
inference(scs_inference,[],[i_0_48,i_0_118,i_0_70,i_0_52,i_0_69,i_0_67,i_0_44]) ).
cnf(i_0_157,plain,
( ~ in(X1,X2)
| subset(singleton(X1),X2) ),
inference(rename_variables,[],[i_0_44]) ).
cnf(i_0_158,plain,
singleton(esk7_0) != singleton(esk8_0),
inference(scs_inference,[],[i_0_48,i_0_78,i_0_118,i_0_72,i_0_70,i_0_52,i_0_69,i_0_67,i_0_44,i_0_45]) ).
cnf(i_0_159,plain,
in(X1,singleton(X1)),
inference(rename_variables,[],[i_0_72]) ).
cnf(i_0_160,plain,
( X1 = X2
| ~ in(X1,X3)
| X3 != singleton(X2) ),
inference(rename_variables,[],[i_0_45]) ).
cnf(i_0_161,plain,
( singleton(X1) != union(X2)
| in(esk4_3(X2,singleton(X1),X1),X2) ),
inference(scs_inference,[],[i_0_48,i_0_78,i_0_118,i_0_72,i_0_159,i_0_70,i_0_52,i_0_69,i_0_67,i_0_44,i_0_45,i_0_26]) ).
cnf(i_0_162,plain,
( ~ in(X1,X2)
| in(esk4_3(X3,X2,X1),X3)
| X2 != union(X3) ),
inference(rename_variables,[],[i_0_26]) ).
cnf(i_0_163,plain,
~ in(singleton(powerset(X1)),singleton(X1)),
inference(scs_inference,[],[i_0_48,i_0_78,i_0_118,i_0_72,i_0_159,i_0_99,i_0_70,i_0_52,i_0_69,i_0_67,i_0_44,i_0_45,i_0_26,i_0_38]) ).
cnf(i_0_164,plain,
~ in(singleton(X1),X1),
inference(rename_variables,[],[i_0_99]) ).
cnf(i_0_165,plain,
( ~ subset(X1,X2)
| in(X3,X2)
| ~ in(X3,X1) ),
inference(rename_variables,[],[i_0_38]) ).
cnf(i_0_166,plain,
( X1 != esk10_0
| union(powerset(esk10_0)) != X1 ),
inference(scs_inference,[],[i_0_48,i_0_78,i_0_118,i_0_72,i_0_159,i_0_99,i_0_70,i_0_52,i_0_69,i_0_67,i_0_44,i_0_45,i_0_26,i_0_38,i_0_53]) ).
cnf(i_0_167,plain,
~ in(singleton(esk7_0),singleton(singleton(esk8_0))),
inference(scs_inference,[],[i_0_158,i_0_69]) ).
cnf(i_0_168,plain,
( X1 = X2
| ~ in(X1,singleton(X2)) ),
inference(rename_variables,[],[i_0_69]) ).
cnf(i_0_169,plain,
~ in(singleton(singleton(X1)),powerset(X1)),
inference(scs_inference,[],[i_0_158,i_0_121,i_0_69,i_0_67]) ).
cnf(i_0_170,plain,
( subset(X1,X2)
| ~ in(X1,powerset(X2)) ),
inference(rename_variables,[],[i_0_67]) ).
cnf(i_0_171,plain,
~ subset(singleton(singleton(esk7_0)),singleton(singleton(esk8_0))),
inference(scs_inference,[],[i_0_158,i_0_121,i_0_69,i_0_67,i_0_40]) ).
cnf(i_0_172,plain,
( in(X1,X2)
| ~ subset(singleton(X1),X2) ),
inference(rename_variables,[],[i_0_40]) ).
cnf(i_0_173,plain,
singleton(esk8_0) != singleton(esk7_0),
inference(scs_inference,[],[i_0_158,i_0_121,i_0_69,i_0_67,i_0_40,i_0_52]) ).
cnf(i_0_174,plain,
singleton(singleton(esk8_0)) != powerset(powerset(esk7_0)),
inference(scs_inference,[],[i_0_156,i_0_158,i_0_121,i_0_69,i_0_67,i_0_40,i_0_52,i_0_42]) ).
cnf(i_0_175,plain,
subset(singleton(X1),powerset(X1)),
inference(rename_variables,[],[i_0_156]) ).
cnf(i_0_176,plain,
( in(X1,X2)
| ~ subset(X1,X3)
| X2 != powerset(X3) ),
inference(rename_variables,[],[i_0_42]) ).
cnf(i_0_177,plain,
~ in(powerset(powerset(X1)),singleton(X1)),
inference(scs_inference,[],[i_0_156,i_0_175,i_0_158,i_0_121,i_0_85,i_0_69,i_0_67,i_0_40,i_0_52,i_0_42,i_0_38]) ).
cnf(i_0_178,plain,
~ in(powerset(X1),X1),
inference(rename_variables,[],[i_0_85]) ).
cnf(i_0_179,plain,
( in(X1,X2)
| ~ subset(X3,X2)
| ~ in(X1,X3) ),
inference(rename_variables,[],[i_0_38]) ).
cnf(i_0_180,plain,
( singleton(X1) != union(X2)
| in(X1,esk4_3(X2,singleton(X1),X1)) ),
inference(scs_inference,[],[i_0_156,i_0_175,i_0_158,i_0_121,i_0_72,i_0_85,i_0_69,i_0_67,i_0_40,i_0_52,i_0_42,i_0_38,i_0_27]) ).
cnf(i_0_181,plain,
( ~ in(X1,X2)
| in(X1,esk4_3(X3,X2,X1))
| X2 != union(X3) ),
inference(rename_variables,[],[i_0_27]) ).
cnf(i_0_182,plain,
( powerset(singleton(X1)) != X2
| powerset(X1) != singleton(X2) ),
inference(scs_inference,[],[i_0_156,i_0_175,i_0_158,i_0_154,i_0_121,i_0_72,i_0_85,i_0_69,i_0_67,i_0_40,i_0_52,i_0_42,i_0_38,i_0_27,i_0_46]) ).
cnf(i_0_183,plain,
( in(X1,X2)
| X1 != X3
| X2 != singleton(X3) ),
inference(rename_variables,[],[i_0_46]) ).
cnf(i_0_184,plain,
~ in(singleton(esk8_0),singleton(singleton(esk7_0))),
inference(scs_inference,[],[i_0_173,i_0_69]) ).
cnf(i_0_185,plain,
( X1 = X2
| ~ in(X1,singleton(X2)) ),
inference(rename_variables,[],[i_0_69]) ).
cnf(i_0_186,plain,
~ subset(singleton(singleton(esk8_0)),singleton(singleton(esk7_0))),
inference(scs_inference,[],[i_0_173,i_0_69,i_0_40]) ).
cnf(i_0_187,plain,
( in(X1,X2)
| ~ subset(singleton(X1),X2) ),
inference(rename_variables,[],[i_0_40]) ).
cnf(i_0_188,plain,
powerset(powerset(esk7_0)) != singleton(singleton(esk8_0)),
inference(scs_inference,[],[i_0_173,i_0_174,i_0_69,i_0_40,i_0_52]) ).
cnf(i_0_189,plain,
~ in(esk5_2(powerset(esk10_0),esk10_0),esk10_0),
inference(scs_inference,[],[i_0_173,i_0_151,i_0_174,i_0_70,i_0_69,i_0_40,i_0_52,i_0_25]) ).
cnf(i_0_190,plain,
in(X1,powerset(X1)),
inference(rename_variables,[],[i_0_70]) ).
cnf(i_0_191,plain,
( X1 = union(X2)
| ~ in(X3,X2)
| ~ in(esk5_2(X2,X1),X3)
| ~ in(esk5_2(X2,X1),X1) ),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_192,plain,
( ~ in(esk9_2(singleton(esk8_0),singleton(esk7_0)),singleton(esk7_0))
| ~ in(esk9_2(singleton(esk8_0),singleton(esk7_0)),singleton(esk8_0)) ),
inference(scs_inference,[],[i_0_173,i_0_151,i_0_174,i_0_70,i_0_69,i_0_40,i_0_52,i_0_25,i_0_29]) ).
cnf(i_0_193,plain,
( X1 = X2
| ~ in(esk9_2(X1,X2),X2)
| ~ in(esk9_2(X1,X2),X1) ),
inference(rename_variables,[],[i_0_29]) ).
cnf(i_0_194,plain,
( ~ in(esk9_2(singleton(esk8_0),singleton(esk7_0)),singleton(esk8_0))
| in(esk9_2(singleton(esk8_0),singleton(esk7_0)),singleton(esk8_0)) ),
inference(scs_inference,[],[i_0_173,i_0_151,i_0_174,i_0_70,i_0_69,i_0_40,i_0_52,i_0_25,i_0_29,i_0_34]) ).
cnf(i_0_195,plain,
( X1 = X2
| in(esk9_2(X1,X2),X2)
| in(esk9_2(X1,X2),X1) ),
inference(rename_variables,[],[i_0_34]) ).
cnf(i_0_196,plain,
( ~ in(esk9_2(singleton(esk8_0),singleton(esk7_0)),singleton(esk8_0))
| in(esk5_2(powerset(esk10_0),esk10_0),esk6_2(powerset(esk10_0),esk10_0)) ),
inference(scs_inference,[],[i_0_173,i_0_151,i_0_174,i_0_70,i_0_69,i_0_40,i_0_52,i_0_25,i_0_29,i_0_34,i_0_30]) ).
cnf(i_0_197,plain,
( in(esk5_2(X1,X2),X2)
| in(esk5_2(X1,X2),esk6_2(X1,X2))
| X2 = union(X1) ),
inference(rename_variables,[],[i_0_30]) ).
cnf(i_0_198,plain,
( esk6_2(powerset(esk10_0),esk10_0) != esk10_0
| ~ in(esk9_2(singleton(esk8_0),singleton(esk7_0)),singleton(esk8_0)) ),
inference(scs_inference,[],[i_0_173,i_0_151,i_0_174,i_0_70,i_0_69,i_0_40,i_0_52,i_0_25,i_0_29,i_0_34,i_0_30,i_0_60]) ).
cnf(i_0_199,plain,
( esk9_2(singleton(esk8_0),singleton(esk7_0)) != singleton(powerset(esk8_0))
| ~ in(esk9_2(singleton(esk8_0),singleton(esk7_0)),singleton(esk8_0)) ),
inference(scs_inference,[],[i_0_173,i_0_163,i_0_151,i_0_174,i_0_70,i_0_69,i_0_40,i_0_52,i_0_25,i_0_29,i_0_34,i_0_30,i_0_60,i_0_59]) ).
cnf(i_0_200,plain,
~ in(singleton(powerset(X1)),singleton(X1)),
inference(rename_variables,[],[i_0_163]) ).
cnf(i_0_201,plain,
( ~ in(esk6_2(powerset(esk10_0),esk10_0),esk5_2(powerset(esk10_0),esk10_0))
| ~ in(esk9_2(singleton(esk8_0),singleton(esk7_0)),singleton(esk8_0)) ),
inference(scs_inference,[],[i_0_173,i_0_163,i_0_151,i_0_174,i_0_70,i_0_69,i_0_40,i_0_52,i_0_25,i_0_29,i_0_34,i_0_30,i_0_60,i_0_59,i_0_43]) ).
cnf(i_0_202,plain,
( ~ in(X1,X2)
| ~ in(X2,X1) ),
inference(rename_variables,[],[i_0_43]) ).
cnf(i_0_204,plain,
~ in(esk7_0,singleton(esk8_0)),
inference(scs_inference,[],[i_0_78,i_0_69]) ).
cnf(i_0_205,plain,
( X1 = X2
| ~ in(X1,singleton(X2)) ),
inference(rename_variables,[],[i_0_69]) ).
cnf(i_0_206,plain,
~ subset(singleton(esk7_0),singleton(esk8_0)),
inference(scs_inference,[],[i_0_78,i_0_69,i_0_40]) ).
cnf(i_0_207,plain,
( in(X1,X2)
| ~ subset(singleton(X1),X2) ),
inference(rename_variables,[],[i_0_40]) ).
cnf(i_0_208,plain,
esk8_0 != esk7_0,
inference(scs_inference,[],[i_0_78,i_0_69,i_0_40,i_0_52]) ).
cnf(i_0_209,plain,
in(esk6_2(powerset(esk10_0),esk10_0),powerset(esk10_0)),
inference(scs_inference,[],[i_0_189,i_0_78,i_0_151,i_0_69,i_0_40,i_0_52,i_0_32]) ).
cnf(i_0_210,plain,
( X1 = union(X2)
| in(esk6_2(X2,X1),X2)
| in(esk5_2(X2,X1),X1) ),
inference(rename_variables,[],[i_0_32]) ).
cnf(i_0_211,plain,
singleton(singleton(esk7_0)) != powerset(singleton(esk8_0)),
inference(scs_inference,[],[i_0_189,i_0_78,i_0_151,i_0_72,i_0_69,i_0_40,i_0_52,i_0_32,i_0_41]) ).
cnf(i_0_212,plain,
in(X1,singleton(X1)),
inference(rename_variables,[],[i_0_72]) ).
cnf(i_0_213,plain,
( subset(X1,X2)
| ~ in(X1,X3)
| X3 != powerset(X2) ),
inference(rename_variables,[],[i_0_41]) ).
cnf(i_0_214,plain,
~ in(esk3_2(singleton(esk7_0),singleton(esk8_0)),singleton(esk8_0)),
inference(scs_inference,[],[i_0_189,i_0_78,i_0_151,i_0_72,i_0_69,i_0_40,i_0_52,i_0_32,i_0_41,i_0_35]) ).
cnf(i_0_215,plain,
( subset(X1,X2)
| ~ in(esk3_2(X1,X2),X2) ),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_216,plain,
in(esk3_2(singleton(esk7_0),singleton(esk8_0)),singleton(esk7_0)),
inference(scs_inference,[],[i_0_189,i_0_78,i_0_151,i_0_72,i_0_69,i_0_40,i_0_52,i_0_32,i_0_41,i_0_35,i_0_39]) ).
cnf(i_0_217,plain,
( subset(X1,X2)
| in(esk3_2(X1,X2),X1) ),
inference(rename_variables,[],[i_0_39]) ).
cnf(i_0_218,plain,
~ in(singleton(esk7_0),powerset(singleton(esk8_0))),
inference(scs_inference,[],[i_0_189,i_0_78,i_0_151,i_0_72,i_0_69,i_0_40,i_0_52,i_0_32,i_0_41,i_0_35,i_0_39,i_0_67]) ).
cnf(i_0_219,plain,
( subset(X1,X2)
| ~ in(X1,powerset(X2)) ),
inference(rename_variables,[],[i_0_67]) ).
cnf(i_0_220,plain,
~ in(powerset(esk10_0),esk6_2(powerset(esk10_0),esk10_0)),
inference(scs_inference,[],[i_0_189,i_0_78,i_0_151,i_0_72,i_0_69,i_0_40,i_0_52,i_0_32,i_0_41,i_0_35,i_0_39,i_0_67,i_0_43]) ).
cnf(i_0_221,plain,
( ~ in(X1,X2)
| ~ in(X2,X1) ),
inference(rename_variables,[],[i_0_43]) ).
cnf(i_0_222,plain,
( ~ subset(esk2_2(powerset(X1),X1),powerset(X1))
| ~ in(esk2_2(powerset(X1),X1),X1) ),
inference(scs_inference,[],[i_0_189,i_0_106,i_0_78,i_0_151,i_0_72,i_0_69,i_0_40,i_0_52,i_0_32,i_0_41,i_0_35,i_0_39,i_0_67,i_0_43,i_0_28]) ).
cnf(i_0_223,plain,
( X1 = powerset(X2)
| ~ subset(esk2_2(X2,X1),X2)
| ~ in(esk2_2(X2,X1),X1) ),
inference(rename_variables,[],[i_0_28]) ).
cnf(i_0_224,plain,
powerset(singleton(esk7_0)) != singleton(singleton(esk8_0)),
inference(scs_inference,[],[i_0_189,i_0_171,i_0_106,i_0_78,i_0_156,i_0_151,i_0_72,i_0_69,i_0_40,i_0_52,i_0_32,i_0_41,i_0_35,i_0_39,i_0_67,i_0_43,i_0_28,i_0_62]) ).
cnf(i_0_225,plain,
subset(singleton(X1),powerset(X1)),
inference(rename_variables,[],[i_0_156]) ).
cnf(i_0_226,plain,
singleton(singleton(esk8_0)) != singleton(singleton(esk7_0)),
inference(scs_inference,[],[i_0_189,i_0_171,i_0_106,i_0_78,i_0_156,i_0_151,i_0_47,i_0_72,i_0_69,i_0_40,i_0_52,i_0_32,i_0_41,i_0_35,i_0_39,i_0_67,i_0_43,i_0_28,i_0_62,i_0_61]) ).
cnf(i_0_227,plain,
subset(X1,X1),
inference(rename_variables,[],[i_0_47]) ).
cnf(i_0_228,plain,
( in(esk2_2(powerset(X1),X1),X1)
| ~ in(esk2_2(powerset(X1),X1),X1) ),
inference(scs_inference,[],[i_0_189,i_0_171,i_0_106,i_0_78,i_0_156,i_0_151,i_0_47,i_0_72,i_0_69,i_0_40,i_0_52,i_0_32,i_0_41,i_0_35,i_0_39,i_0_67,i_0_43,i_0_28,i_0_62,i_0_61,i_0_108]) ).
cnf(i_0_229,plain,
( subset(esk2_2(powerset(X1),X1),powerset(X1))
| in(esk2_2(powerset(X1),X1),X1) ),
inference(rename_variables,[],[i_0_108]) ).
cnf(i_0_230,plain,
( ~ in(powerset(powerset(X1)),esk6_2(powerset(esk10_0),esk10_0))
| ~ in(esk2_2(powerset(X2),X2),X2)
| singleton(X1) != union(powerset(esk10_0)) ),
inference(scs_inference,[],[i_0_177,i_0_189,i_0_171,i_0_106,i_0_78,i_0_156,i_0_151,i_0_47,i_0_72,i_0_69,i_0_40,i_0_52,i_0_32,i_0_41,i_0_35,i_0_39,i_0_67,i_0_43,i_0_28,i_0_62,i_0_61,i_0_108,i_0_36]) ).
cnf(i_0_231,plain,
~ in(esk8_0,singleton(esk7_0)),
inference(scs_inference,[],[i_0_208,i_0_69]) ).
cnf(i_0_232,plain,
( X1 = X2
| ~ in(X1,singleton(X2)) ),
inference(rename_variables,[],[i_0_69]) ).
cnf(i_0_233,plain,
~ subset(singleton(powerset(esk10_0)),esk6_2(powerset(esk10_0),esk10_0)),
inference(scs_inference,[],[i_0_208,i_0_220,i_0_69,i_0_40]) ).
cnf(i_0_234,plain,
( in(X1,X2)
| ~ subset(singleton(X1),X2) ),
inference(rename_variables,[],[i_0_40]) ).
cnf(i_0_235,plain,
~ in(singleton(esk7_0),esk3_2(singleton(esk7_0),singleton(esk8_0))),
inference(scs_inference,[],[i_0_208,i_0_216,i_0_220,i_0_69,i_0_40,i_0_43]) ).
cnf(i_0_236,plain,
( ~ in(X1,X2)
| ~ in(X2,X1) ),
inference(rename_variables,[],[i_0_43]) ).
cnf(i_0_237,plain,
powerset(singleton(esk8_0)) != singleton(singleton(esk7_0)),
inference(scs_inference,[],[i_0_208,i_0_216,i_0_220,i_0_211,i_0_69,i_0_40,i_0_43,i_0_52]) ).
cnf(i_0_238,plain,
singleton(esk8_0) != powerset(esk7_0),
inference(scs_inference,[],[i_0_208,i_0_204,i_0_216,i_0_220,i_0_211,i_0_47,i_0_69,i_0_40,i_0_43,i_0_52,i_0_42]) ).
cnf(i_0_239,plain,
subset(X1,X1),
inference(rename_variables,[],[i_0_47]) ).
cnf(i_0_240,plain,
( ~ subset(X1,X2)
| in(X1,X3)
| X3 != powerset(X2) ),
inference(rename_variables,[],[i_0_42]) ).
cnf(i_0_241,plain,
powerset(singleton(esk7_0)) != powerset(singleton(esk8_0)),
inference(scs_inference,[],[i_0_208,i_0_206,i_0_204,i_0_216,i_0_220,i_0_211,i_0_47,i_0_70,i_0_69,i_0_40,i_0_43,i_0_52,i_0_42,i_0_41]) ).
cnf(i_0_242,plain,
in(X1,powerset(X1)),
inference(rename_variables,[],[i_0_70]) ).
cnf(i_0_243,plain,
( ~ in(X1,X2)
| subset(X1,X3)
| X2 != powerset(X3) ),
inference(rename_variables,[],[i_0_41]) ).
cnf(i_0_244,plain,
( esk1_2(esk8_0,singleton(esk7_0)) != esk8_0
| ~ in(esk1_2(esk8_0,singleton(esk7_0)),singleton(esk7_0)) ),
inference(scs_inference,[],[i_0_208,i_0_206,i_0_204,i_0_216,i_0_220,i_0_211,i_0_158,i_0_47,i_0_70,i_0_69,i_0_40,i_0_43,i_0_52,i_0_42,i_0_41,i_0_31]) ).
cnf(i_0_245,plain,
( X1 = singleton(X2)
| esk1_2(X2,X1) != X2
| ~ in(esk1_2(X2,X1),X1) ),
inference(rename_variables,[],[i_0_31]) ).
cnf(i_0_247,plain,
~ in(singleton(esk8_0),singleton(powerset(esk7_0))),
inference(scs_inference,[],[i_0_238,i_0_69]) ).
cnf(i_0_248,plain,
( X1 = X2
| ~ in(X1,singleton(X2)) ),
inference(rename_variables,[],[i_0_69]) ).
cnf(i_0_249,plain,
~ subset(singleton(esk8_0),singleton(esk7_0)),
inference(scs_inference,[],[i_0_238,i_0_231,i_0_69,i_0_40]) ).
cnf(i_0_250,plain,
( in(X1,X2)
| ~ subset(singleton(X1),X2) ),
inference(rename_variables,[],[i_0_40]) ).
cnf(i_0_251,plain,
powerset(esk7_0) != singleton(esk8_0),
inference(scs_inference,[],[i_0_238,i_0_231,i_0_69,i_0_40,i_0_52]) ).
cnf(i_0_252,plain,
singleton(singleton(esk8_0)) != singleton(powerset(esk7_0)),
inference(scs_inference,[],[i_0_238,i_0_231,i_0_72,i_0_69,i_0_40,i_0_52,i_0_45]) ).
cnf(i_0_253,plain,
in(X1,singleton(X1)),
inference(rename_variables,[],[i_0_72]) ).
cnf(i_0_254,plain,
( X1 = X2
| ~ in(X1,X3)
| X3 != singleton(X2) ),
inference(rename_variables,[],[i_0_45]) ).
cnf(i_0_255,plain,
singleton(esk7_0) != powerset(esk8_0),
inference(scs_inference,[],[i_0_238,i_0_231,i_0_72,i_0_47,i_0_69,i_0_40,i_0_52,i_0_45,i_0_42]) ).
cnf(i_0_256,plain,
subset(X1,X1),
inference(rename_variables,[],[i_0_47]) ).
cnf(i_0_257,plain,
( in(X1,X2)
| ~ subset(X1,X3)
| X2 != powerset(X3) ),
inference(rename_variables,[],[i_0_42]) ).
cnf(i_0_258,plain,
singleton(singleton(esk8_0)) != powerset(singleton(esk7_0)),
inference(scs_inference,[],[i_0_238,i_0_231,i_0_72,i_0_253,i_0_47,i_0_69,i_0_40,i_0_52,i_0_45,i_0_42,i_0_41]) ).
cnf(i_0_259,plain,
in(X1,singleton(X1)),
inference(rename_variables,[],[i_0_72]) ).
cnf(i_0_260,plain,
( subset(X1,X2)
| ~ in(X1,X3)
| X3 != powerset(X2) ),
inference(rename_variables,[],[i_0_41]) ).
cnf(i_0_261,plain,
~ in(esk3_2(singleton(esk8_0),singleton(esk7_0)),singleton(esk7_0)),
inference(scs_inference,[],[i_0_238,i_0_231,i_0_72,i_0_253,i_0_47,i_0_69,i_0_40,i_0_52,i_0_45,i_0_42,i_0_41,i_0_35]) ).
cnf(i_0_262,plain,
( subset(X1,X2)
| ~ in(esk3_2(X1,X2),X2) ),
inference(rename_variables,[],[i_0_35]) ).
cnf(i_0_263,plain,
in(esk3_2(singleton(esk8_0),singleton(esk7_0)),singleton(esk8_0)),
inference(scs_inference,[],[i_0_238,i_0_231,i_0_72,i_0_253,i_0_47,i_0_69,i_0_40,i_0_52,i_0_45,i_0_42,i_0_41,i_0_35,i_0_39]) ).
cnf(i_0_264,plain,
( subset(X1,X2)
| in(esk3_2(X1,X2),X1) ),
inference(rename_variables,[],[i_0_39]) ).
cnf(i_0_265,plain,
~ in(singleton(esk8_0),powerset(singleton(esk7_0))),
inference(scs_inference,[],[i_0_238,i_0_231,i_0_72,i_0_253,i_0_47,i_0_69,i_0_40,i_0_52,i_0_45,i_0_42,i_0_41,i_0_35,i_0_39,i_0_67]) ).
cnf(i_0_266,plain,
( subset(X1,X2)
| ~ in(X1,powerset(X2)) ),
inference(rename_variables,[],[i_0_67]) ).
cnf(i_0_267,plain,
~ in(singleton(esk8_0),esk3_2(singleton(esk8_0),singleton(esk7_0))),
inference(scs_inference,[],[i_0_238,i_0_231,i_0_72,i_0_253,i_0_47,i_0_69,i_0_40,i_0_52,i_0_45,i_0_42,i_0_41,i_0_35,i_0_39,i_0_67,i_0_43]) ).
cnf(i_0_268,plain,
( ~ in(X1,X2)
| ~ in(X2,X1) ),
inference(rename_variables,[],[i_0_43]) ).
cnf(i_0_269,plain,
( esk8_0 != X1
| singleton(esk7_0) != singleton(X1) ),
inference(scs_inference,[],[i_0_238,i_0_231,i_0_72,i_0_253,i_0_47,i_0_69,i_0_40,i_0_52,i_0_45,i_0_42,i_0_41,i_0_35,i_0_39,i_0_67,i_0_43,i_0_46]) ).
cnf(i_0_270,plain,
( in(X1,X2)
| X1 != X3
| X2 != singleton(X3) ),
inference(rename_variables,[],[i_0_46]) ).
cnf(i_0_271,plain,
( powerset(X1) != union(X2)
| in(esk4_3(X2,powerset(X1),X1),X2) ),
inference(scs_inference,[],[i_0_238,i_0_231,i_0_72,i_0_253,i_0_47,i_0_70,i_0_69,i_0_40,i_0_52,i_0_45,i_0_42,i_0_41,i_0_35,i_0_39,i_0_67,i_0_43,i_0_46,i_0_26]) ).
cnf(i_0_272,plain,
( ~ in(X1,X2)
| in(esk4_3(X3,X2,X1),X3)
| X2 != union(X3) ),
inference(rename_variables,[],[i_0_26]) ).
cnf(i_0_273,plain,
~ in(powerset(esk7_0),singleton(singleton(esk8_0))),
inference(scs_inference,[],[i_0_251,i_0_69]) ).
cnf(i_0_274,plain,
( X1 = X2
| ~ in(X1,singleton(X2)) ),
inference(rename_variables,[],[i_0_69]) ).
cnf(i_0_275,plain,
~ subset(singleton(singleton(esk7_0)),esk3_2(singleton(esk7_0),singleton(esk8_0))),
inference(scs_inference,[],[i_0_251,i_0_235,i_0_69,i_0_40]) ).
cnf(i_0_276,plain,
( in(X1,X2)
| ~ subset(singleton(X1),X2) ),
inference(rename_variables,[],[i_0_40]) ).
cnf(i_0_277,plain,
powerset(esk8_0) != singleton(esk7_0),
inference(scs_inference,[],[i_0_251,i_0_255,i_0_235,i_0_69,i_0_40,i_0_52]) ).
cnf(i_0_278,plain,
powerset(singleton(esk8_0)) != powerset(singleton(esk7_0)),
inference(scs_inference,[],[i_0_249,i_0_251,i_0_255,i_0_235,i_0_70,i_0_69,i_0_40,i_0_52,i_0_41]) ).
cnf(i_0_279,plain,
in(X1,powerset(X1)),
inference(rename_variables,[],[i_0_70]) ).
cnf(i_0_280,plain,
( ~ in(X1,X2)
| subset(X1,X3)
| X2 != powerset(X3) ),
inference(rename_variables,[],[i_0_41]) ).
cnf(i_0_281,plain,
( powerset(X1) != union(X2)
| in(X1,esk4_3(X2,powerset(X1),X1)) ),
inference(scs_inference,[],[i_0_249,i_0_251,i_0_255,i_0_235,i_0_70,i_0_279,i_0_69,i_0_40,i_0_52,i_0_41,i_0_27]) ).
cnf(i_0_282,plain,
( ~ in(X1,X2)
| in(X1,esk4_3(X3,X2,X1))
| X2 != union(X3) ),
inference(rename_variables,[],[i_0_27]) ).
cnf(i_0_283,plain,
( ~ in(esk9_2(powerset(esk7_0),singleton(esk8_0)),singleton(esk8_0))
| ~ in(esk9_2(powerset(esk7_0),singleton(esk8_0)),powerset(esk7_0)) ),
inference(scs_inference,[],[i_0_249,i_0_251,i_0_255,i_0_235,i_0_70,i_0_279,i_0_69,i_0_40,i_0_52,i_0_41,i_0_27,i_0_29]) ).
cnf(i_0_284,plain,
( X1 = X2
| ~ in(esk9_2(X1,X2),X2)
| ~ in(esk9_2(X1,X2),X1) ),
inference(rename_variables,[],[i_0_29]) ).
cnf(i_0_285,plain,
~ in(powerset(esk8_0),singleton(singleton(esk7_0))),
inference(scs_inference,[],[i_0_277,i_0_69]) ).
cnf(i_0_286,plain,
( X1 = X2
| ~ in(X1,singleton(X2)) ),
inference(rename_variables,[],[i_0_69]) ).
cnf(i_0_287,plain,
~ subset(singleton(singleton(esk8_0)),esk3_2(singleton(esk8_0),singleton(esk7_0))),
inference(scs_inference,[],[i_0_277,i_0_267,i_0_69,i_0_40]) ).
cnf(i_0_288,plain,
( in(X1,X2)
| ~ subset(singleton(X1),X2) ),
inference(rename_variables,[],[i_0_40]) ).
cnf(i_0_289,plain,
singleton(singleton(esk7_0)) != singleton(singleton(esk8_0)),
inference(scs_inference,[],[i_0_277,i_0_267,i_0_226,i_0_69,i_0_40,i_0_52]) ).
cnf(i_0_290,plain,
in(esk5_2(powerset(esk10_0),esk10_0),esk6_2(powerset(esk10_0),esk10_0)),
inference(scs_inference,[],[i_0_277,i_0_267,i_0_226,i_0_189,i_0_151,i_0_69,i_0_40,i_0_52,i_0_30]) ).
cnf(i_0_291,plain,
( in(esk5_2(X1,X2),X2)
| in(esk5_2(X1,X2),esk6_2(X1,X2))
| X2 = union(X1) ),
inference(rename_variables,[],[i_0_30]) ).
cnf(i_0_292,plain,
esk6_2(powerset(esk10_0),esk10_0) != esk10_0,
inference(scs_inference,[],[i_0_277,i_0_267,i_0_226,i_0_189,i_0_151,i_0_69,i_0_40,i_0_52,i_0_30,i_0_60]) ).
cnf(i_0_293,plain,
esk3_2(singleton(esk8_0),singleton(esk7_0)) != esk3_2(singleton(esk7_0),singleton(esk8_0)),
inference(scs_inference,[],[i_0_277,i_0_214,i_0_263,i_0_267,i_0_226,i_0_189,i_0_151,i_0_69,i_0_40,i_0_52,i_0_30,i_0_60,i_0_59]) ).
cnf(i_0_294,plain,
~ in(esk6_2(powerset(esk10_0),esk10_0),esk5_2(powerset(esk10_0),esk10_0)),
inference(scs_inference,[],[i_0_277,i_0_214,i_0_263,i_0_267,i_0_226,i_0_189,i_0_151,i_0_69,i_0_40,i_0_52,i_0_30,i_0_60,i_0_59,i_0_43]) ).
cnf(i_0_295,plain,
( ~ in(X1,X2)
| ~ in(X2,X1) ),
inference(rename_variables,[],[i_0_43]) ).
cnf(i_0_296,plain,
in(esk5_2(powerset(esk10_0),esk10_0),union(powerset(esk10_0))),
inference(scs_inference,[],[i_0_277,i_0_214,i_0_263,i_0_209,i_0_267,i_0_226,i_0_189,i_0_151,i_0_69,i_0_40,i_0_52,i_0_30,i_0_60,i_0_59,i_0_43,i_0_66]) ).
cnf(i_0_297,plain,
( ~ in(X1,X2)
| in(X1,union(X3))
| ~ in(X2,X3) ),
inference(rename_variables,[],[i_0_66]) ).
cnf(i_0_298,plain,
( in(esk9_2(powerset(esk8_0),singleton(esk7_0)),singleton(esk7_0))
| in(esk9_2(powerset(esk8_0),singleton(esk7_0)),powerset(esk8_0)) ),
inference(scs_inference,[],[i_0_277,i_0_214,i_0_263,i_0_209,i_0_267,i_0_226,i_0_189,i_0_151,i_0_69,i_0_40,i_0_52,i_0_30,i_0_60,i_0_59,i_0_43,i_0_66,i_0_34]) ).
cnf(i_0_299,plain,
( X1 = X2
| in(esk9_2(X1,X2),X2)
| in(esk9_2(X1,X2),X1) ),
inference(rename_variables,[],[i_0_34]) ).
cnf(i_0_300,plain,
( ~ in(esk9_2(powerset(esk8_0),singleton(esk7_0)),powerset(esk8_0))
| in(esk9_2(powerset(esk8_0),singleton(esk7_0)),powerset(esk8_0)) ),
inference(scs_inference,[],[i_0_277,i_0_214,i_0_263,i_0_209,i_0_267,i_0_226,i_0_189,i_0_151,i_0_69,i_0_40,i_0_52,i_0_30,i_0_60,i_0_59,i_0_43,i_0_66,i_0_34,i_0_29]) ).
cnf(i_0_301,plain,
( ~ in(esk9_2(X1,X2),X2)
| X1 = X2
| ~ in(esk9_2(X1,X2),X1) ),
inference(rename_variables,[],[i_0_29]) ).
cnf(i_0_303,plain,
~ in(esk6_2(powerset(esk10_0),esk10_0),singleton(esk10_0)),
inference(scs_inference,[],[i_0_292,i_0_69]) ).
cnf(i_0_304,plain,
( X1 = X2
| ~ in(X1,singleton(X2)) ),
inference(rename_variables,[],[i_0_69]) ).
cnf(i_0_305,plain,
~ subset(singleton(singleton(esk8_0)),powerset(singleton(esk7_0))),
inference(scs_inference,[],[i_0_265,i_0_292,i_0_69,i_0_40]) ).
cnf(i_0_306,plain,
( in(X1,X2)
| ~ subset(singleton(X1),X2) ),
inference(rename_variables,[],[i_0_40]) ).
cnf(i_0_307,plain,
~ in(union(powerset(esk10_0)),esk5_2(powerset(esk10_0),esk10_0)),
inference(scs_inference,[],[i_0_265,i_0_292,i_0_296,i_0_69,i_0_40,i_0_43]) ).
cnf(i_0_308,plain,
( ~ in(X1,X2)
| ~ in(X2,X1) ),
inference(rename_variables,[],[i_0_43]) ).
cnf(i_0_309,plain,
esk10_0 != esk6_2(powerset(esk10_0),esk10_0),
inference(scs_inference,[],[i_0_265,i_0_292,i_0_296,i_0_69,i_0_40,i_0_43,i_0_52]) ).
cnf(i_0_310,plain,
powerset(esk10_0) != singleton(esk10_0),
inference(scs_inference,[],[i_0_265,i_0_292,i_0_296,i_0_209,i_0_69,i_0_40,i_0_43,i_0_52,i_0_45]) ).
cnf(i_0_311,plain,
( ~ in(X1,X2)
| X1 = X3
| X2 != singleton(X3) ),
inference(rename_variables,[],[i_0_45]) ).
cnf(i_0_312,plain,
( ~ in(esk9_2(esk8_0,esk7_0),esk7_0)
| ~ in(esk9_2(esk8_0,esk7_0),esk8_0) ),
inference(scs_inference,[],[i_0_265,i_0_292,i_0_296,i_0_208,i_0_209,i_0_69,i_0_40,i_0_43,i_0_52,i_0_45,i_0_29]) ).
cnf(i_0_313,plain,
( X1 = X2
| ~ in(esk9_2(X1,X2),X2)
| ~ in(esk9_2(X1,X2),X1) ),
inference(rename_variables,[],[i_0_29]) ).
cnf(i_0_314,plain,
powerset(singleton(esk7_0)) != powerset(powerset(esk8_0)),
inference(scs_inference,[],[i_0_265,i_0_292,i_0_296,i_0_208,i_0_209,i_0_156,i_0_69,i_0_40,i_0_43,i_0_52,i_0_45,i_0_29,i_0_42]) ).
cnf(i_0_315,plain,
subset(singleton(X1),powerset(X1)),
inference(rename_variables,[],[i_0_156]) ).
cnf(i_0_316,plain,
( in(X1,X2)
| ~ subset(X1,X3)
| X2 != powerset(X3) ),
inference(rename_variables,[],[i_0_42]) ).
cnf(i_0_317,plain,
( ~ in(esk9_2(esk8_0,esk7_0),esk8_0)
| in(esk9_2(esk8_0,esk7_0),esk8_0) ),
inference(scs_inference,[],[i_0_265,i_0_292,i_0_296,i_0_208,i_0_209,i_0_156,i_0_69,i_0_40,i_0_43,i_0_52,i_0_45,i_0_29,i_0_42,i_0_34]) ).
cnf(i_0_318,plain,
( in(esk9_2(X1,X2),X2)
| X1 = X2
| in(esk9_2(X1,X2),X1) ),
inference(rename_variables,[],[i_0_34]) ).
cnf(i_0_319,plain,
( esk7_0 != union(singleton(esk8_0))
| ~ in(esk9_2(esk8_0,esk7_0),esk8_0) ),
inference(scs_inference,[],[i_0_265,i_0_292,i_0_296,i_0_208,i_0_209,i_0_156,i_0_72,i_0_69,i_0_40,i_0_43,i_0_52,i_0_45,i_0_29,i_0_42,i_0_34,i_0_36]) ).
cnf(i_0_320,plain,
in(X1,singleton(X1)),
inference(rename_variables,[],[i_0_72]) ).
cnf(i_0_321,plain,
( ~ in(X1,X2)
| in(X1,X3)
| ~ in(X2,X4)
| X3 != union(X4) ),
inference(rename_variables,[],[i_0_36]) ).
cnf(i_0_323,plain,
~ in(powerset(esk10_0),singleton(singleton(esk10_0))),
inference(scs_inference,[],[i_0_310,i_0_69]) ).
cnf(i_0_324,plain,
( X1 = X2
| ~ in(X1,singleton(X2)) ),
inference(rename_variables,[],[i_0_69]) ).
cnf(i_0_325,plain,
~ subset(singleton(singleton(esk8_0)),singleton(powerset(esk7_0))),
inference(scs_inference,[],[i_0_310,i_0_247,i_0_69,i_0_40]) ).
cnf(i_0_326,plain,
( in(X1,X2)
| ~ subset(singleton(X1),X2) ),
inference(rename_variables,[],[i_0_40]) ).
cnf(i_0_327,plain,
singleton(esk10_0) != powerset(esk10_0),
inference(scs_inference,[],[i_0_310,i_0_247,i_0_69,i_0_40,i_0_52]) ).
cnf(i_0_328,plain,
singleton(powerset(esk10_0)) != singleton(singleton(esk10_0)),
inference(scs_inference,[],[i_0_310,i_0_247,i_0_72,i_0_69,i_0_40,i_0_52,i_0_45]) ).
cnf(i_0_329,plain,
in(X1,singleton(X1)),
inference(rename_variables,[],[i_0_72]) ).
cnf(i_0_330,plain,
( X1 = X2
| ~ in(X1,X3)
| X3 != singleton(X2) ),
inference(rename_variables,[],[i_0_45]) ).
cnf(i_0_331,plain,
singleton(singleton(esk7_0)) != powerset(powerset(esk8_0)),
inference(scs_inference,[],[i_0_310,i_0_184,i_0_247,i_0_156,i_0_72,i_0_69,i_0_40,i_0_52,i_0_45,i_0_42]) ).
cnf(i_0_332,plain,
subset(singleton(X1),powerset(X1)),
inference(rename_variables,[],[i_0_156]) ).
cnf(i_0_333,plain,
( ~ subset(X1,X2)
| in(X1,X3)
| X3 != powerset(X2) ),
inference(rename_variables,[],[i_0_42]) ).
cnf(i_0_334,plain,
( esk1_2(esk10_0,powerset(esk10_0)) != esk10_0
| ~ in(esk1_2(esk10_0,powerset(esk10_0)),powerset(esk10_0)) ),
inference(scs_inference,[],[i_0_310,i_0_184,i_0_247,i_0_156,i_0_72,i_0_69,i_0_40,i_0_52,i_0_45,i_0_42,i_0_31]) ).
cnf(i_0_335,plain,
( X1 = singleton(X2)
| esk1_2(X2,X1) != X2
| ~ in(esk1_2(X2,X1),X1) ),
inference(rename_variables,[],[i_0_31]) ).
cnf(i_0_336,plain,
( ~ in(esk1_2(esk10_0,powerset(esk10_0)),powerset(esk10_0))
| in(esk1_2(esk10_0,powerset(esk10_0)),powerset(esk10_0)) ),
inference(scs_inference,[],[i_0_310,i_0_184,i_0_247,i_0_156,i_0_72,i_0_69,i_0_40,i_0_52,i_0_45,i_0_42,i_0_31,i_0_37]) ).
cnf(i_0_337,plain,
( esk1_2(X1,X2) = X1
| in(esk1_2(X1,X2),X2)
| X2 = singleton(X1) ),
inference(rename_variables,[],[i_0_37]) ).
cnf(i_0_338,plain,
( union(powerset(esk10_0)) != X1
| ~ in(esk1_2(esk10_0,powerset(esk10_0)),powerset(esk10_0))
| singleton(esk10_0) != singleton(X1) ),
inference(scs_inference,[],[i_0_310,i_0_152,i_0_184,i_0_247,i_0_156,i_0_72,i_0_69,i_0_40,i_0_52,i_0_45,i_0_42,i_0_31,i_0_37,i_0_46]) ).
cnf(i_0_339,plain,
~ in(singleton(esk10_0),singleton(powerset(esk10_0))),
inference(scs_inference,[],[i_0_327,i_0_69]) ).
cnf(i_0_340,plain,
( X1 = X2
| ~ in(X1,singleton(X2)) ),
inference(rename_variables,[],[i_0_69]) ).
cnf(i_0_341,plain,
~ subset(singleton(powerset(esk7_0)),singleton(singleton(esk8_0))),
inference(scs_inference,[],[i_0_327,i_0_273,i_0_69,i_0_40]) ).
cnf(i_0_342,plain,
( in(X1,X2)
| ~ subset(singleton(X1),X2) ),
inference(rename_variables,[],[i_0_40]) ).
cnf(i_0_343,plain,
esk3_2(singleton(esk7_0),singleton(esk8_0)) != esk3_2(singleton(esk8_0),singleton(esk7_0)),
inference(scs_inference,[],[i_0_327,i_0_273,i_0_293,i_0_69,i_0_40,i_0_52]) ).
cnf(i_0_344,plain,
singleton(singleton(esk10_0)) != powerset(powerset(esk10_0)),
inference(scs_inference,[],[i_0_327,i_0_273,i_0_323,i_0_293,i_0_47,i_0_69,i_0_40,i_0_52,i_0_42]) ).
cnf(i_0_345,plain,
subset(X1,X1),
inference(rename_variables,[],[i_0_47]) ).
cnf(i_0_346,plain,
( in(X1,X2)
| ~ subset(X1,X3)
| X2 != powerset(X3) ),
inference(rename_variables,[],[i_0_42]) ).
cnf(i_0_347,plain,
( ~ subset(esk2_2(esk10_0,singleton(esk10_0)),esk10_0)
| ~ in(esk2_2(esk10_0,singleton(esk10_0)),singleton(esk10_0)) ),
inference(scs_inference,[],[i_0_327,i_0_273,i_0_323,i_0_293,i_0_47,i_0_69,i_0_40,i_0_52,i_0_42,i_0_28]) ).
cnf(i_0_348,plain,
( X1 = powerset(X2)
| ~ subset(esk2_2(X2,X1),X2)
| ~ in(esk2_2(X2,X1),X1) ),
inference(rename_variables,[],[i_0_28]) ).
cnf(i_0_349,plain,
( in(esk9_2(singleton(esk10_0),powerset(esk10_0)),powerset(esk10_0))
| in(esk9_2(singleton(esk10_0),powerset(esk10_0)),singleton(esk10_0)) ),
inference(scs_inference,[],[i_0_327,i_0_273,i_0_323,i_0_293,i_0_47,i_0_69,i_0_40,i_0_52,i_0_42,i_0_28,i_0_34]) ).
cnf(i_0_350,plain,
( X1 = X2
| in(esk9_2(X1,X2),X2)
| in(esk9_2(X1,X2),X1) ),
inference(rename_variables,[],[i_0_34]) ).
cnf(i_0_351,plain,
~ in(singleton(esk7_0),singleton(powerset(esk8_0))),
inference(scs_inference,[],[i_0_255,i_0_69]) ).
cnf(i_0_352,plain,
( X1 = X2
| ~ in(X1,singleton(X2)) ),
inference(rename_variables,[],[i_0_69]) ).
cnf(i_0_353,plain,
~ subset(singleton(powerset(esk8_0)),singleton(singleton(esk7_0))),
inference(scs_inference,[],[i_0_285,i_0_255,i_0_69,i_0_40]) ).
cnf(i_0_354,plain,
( in(X1,X2)
| ~ subset(singleton(X1),X2) ),
inference(rename_variables,[],[i_0_40]) ).
cnf(i_0_355,plain,
powerset(powerset(esk8_0)) != singleton(singleton(esk7_0)),
inference(scs_inference,[],[i_0_285,i_0_331,i_0_255,i_0_69,i_0_40,i_0_52]) ).
cnf(i_0_356,plain,
singleton(powerset(esk10_0)) != powerset(powerset(esk10_0)),
inference(scs_inference,[],[i_0_285,i_0_339,i_0_331,i_0_255,i_0_156,i_0_69,i_0_40,i_0_52,i_0_42]) ).
cnf(i_0_357,plain,
subset(singleton(X1),powerset(X1)),
inference(rename_variables,[],[i_0_156]) ).
cnf(i_0_358,plain,
( ~ subset(X1,X2)
| in(X1,X3)
| X3 != powerset(X2) ),
inference(rename_variables,[],[i_0_42]) ).
cnf(i_0_359,plain,
( subset(esk5_2(powerset(esk10_0),esk10_0),X1)
| esk6_2(powerset(esk10_0),esk10_0) != powerset(X1) ),
inference(scs_inference,[],[i_0_285,i_0_339,i_0_331,i_0_290,i_0_255,i_0_156,i_0_69,i_0_40,i_0_52,i_0_42,i_0_41]) ).
cnf(i_0_360,plain,
( ~ in(X1,X2)
| subset(X1,X3)
| X2 != powerset(X3) ),
inference(rename_variables,[],[i_0_41]) ).
cnf(i_0_361,plain,
( ~ in(esk3_2(singleton(esk8_0),singleton(esk7_0)),esk5_2(powerset(esk10_0),esk10_0))
| esk6_2(powerset(esk10_0),esk10_0) != powerset(singleton(esk7_0)) ),
inference(scs_inference,[],[i_0_261,i_0_285,i_0_339,i_0_331,i_0_290,i_0_255,i_0_156,i_0_69,i_0_40,i_0_52,i_0_42,i_0_41,i_0_38]) ).
cnf(i_0_362,plain,
( ~ subset(X1,X2)
| in(X3,X2)
| ~ in(X3,X1) ),
inference(rename_variables,[],[i_0_38]) ).
cnf(i_0_363,plain,
( subset(esk5_2(powerset(esk10_0),esk10_0),X1)
| singleton(esk7_0) != X1
| esk6_2(powerset(esk10_0),esk10_0) != powerset(singleton(esk7_0)) ),
inference(scs_inference,[],[i_0_261,i_0_285,i_0_339,i_0_331,i_0_290,i_0_255,i_0_156,i_0_69,i_0_40,i_0_52,i_0_42,i_0_41,i_0_38,i_0_62]) ).
cnf(i_0_364,plain,
~ subset(singleton(singleton(esk7_0)),singleton(powerset(esk8_0))),
inference(scs_inference,[],[i_0_351,i_0_40]) ).
cnf(i_0_365,plain,
( in(X1,X2)
| ~ subset(singleton(X1),X2) ),
inference(rename_variables,[],[i_0_40]) ).
cnf(i_0_366,plain,
singleton(powerset(esk7_0)) != singleton(singleton(esk8_0)),
inference(scs_inference,[],[i_0_351,i_0_252,i_0_40,i_0_52]) ).
cnf(i_0_367,plain,
singleton(singleton(esk7_0)) != singleton(powerset(esk8_0)),
inference(scs_inference,[],[i_0_351,i_0_252,i_0_255,i_0_72,i_0_40,i_0_52,i_0_45]) ).
cnf(i_0_368,plain,
in(X1,singleton(X1)),
inference(rename_variables,[],[i_0_72]) ).
cnf(i_0_369,plain,
( X1 = X2
| ~ in(X1,X3)
| X3 != singleton(X2) ),
inference(rename_variables,[],[i_0_45]) ).
cnf(i_0_370,plain,
singleton(powerset(esk8_0)) != powerset(powerset(esk7_0)),
inference(scs_inference,[],[i_0_351,i_0_252,i_0_255,i_0_156,i_0_72,i_0_40,i_0_52,i_0_45,i_0_42]) ).
cnf(i_0_371,plain,
subset(singleton(X1),powerset(X1)),
inference(rename_variables,[],[i_0_156]) ).
cnf(i_0_372,plain,
( in(X1,X2)
| ~ subset(X1,X3)
| X2 != powerset(X3) ),
inference(rename_variables,[],[i_0_42]) ).
cnf(i_0_373,plain,
esk3_2(singleton(esk7_0),singleton(esk8_0)) != singleton(powerset(esk7_0)),
inference(scs_inference,[],[i_0_351,i_0_252,i_0_163,i_0_216,i_0_255,i_0_156,i_0_72,i_0_40,i_0_52,i_0_45,i_0_42,i_0_59]) ).
cnf(i_0_374,plain,
~ in(singleton(powerset(X1)),singleton(X1)),
inference(rename_variables,[],[i_0_163]) ).
cnf(i_0_375,plain,
( ~ in(esk6_2(powerset(esk10_0),esk10_0),esk3_2(singleton(esk7_0),singleton(esk8_0)))
| singleton(esk10_0) != union(singleton(esk7_0)) ),
inference(scs_inference,[],[i_0_303,i_0_351,i_0_252,i_0_163,i_0_216,i_0_255,i_0_156,i_0_72,i_0_40,i_0_52,i_0_45,i_0_42,i_0_59,i_0_36]) ).
cnf(i_0_376,plain,
( in(X1,X2)
| ~ in(X3,X4)
| ~ in(X1,X3)
| X2 != union(X4) ),
inference(rename_variables,[],[i_0_36]) ).
cnf(i_0_377,plain,
( ~ in(esk9_2(singleton(esk7_0),powerset(esk8_0)),powerset(esk8_0))
| ~ in(esk9_2(singleton(esk7_0),powerset(esk8_0)),singleton(esk7_0)) ),
inference(scs_inference,[],[i_0_303,i_0_351,i_0_252,i_0_163,i_0_216,i_0_255,i_0_156,i_0_72,i_0_40,i_0_52,i_0_45,i_0_42,i_0_59,i_0_36,i_0_29]) ).
cnf(i_0_378,plain,
( X1 = X2
| ~ in(esk9_2(X1,X2),X2)
| ~ in(esk9_2(X1,X2),X1) ),
inference(rename_variables,[],[i_0_29]) ).
cnf(i_0_379,plain,
~ subset(singleton(singleton(esk7_0)),powerset(singleton(esk8_0))),
inference(scs_inference,[],[i_0_218,i_0_40]) ).
cnf(i_0_380,plain,
( in(X1,X2)
| ~ subset(singleton(X1),X2) ),
inference(rename_variables,[],[i_0_40]) ).
cnf(i_0_381,plain,
singleton(powerset(esk7_0)) != esk3_2(singleton(esk7_0),singleton(esk8_0)),
inference(scs_inference,[],[i_0_373,i_0_218,i_0_40,i_0_52]) ).
cnf(i_0_382,plain,
( esk6_2(powerset(esk10_0),esk10_0) != X1
| esk5_2(powerset(esk10_0),esk10_0) != singleton(X1) ),
inference(scs_inference,[],[i_0_294,i_0_373,i_0_218,i_0_40,i_0_52,i_0_46]) ).
cnf(i_0_383,plain,
( in(X1,X2)
| X1 != X3
| X2 != singleton(X3) ),
inference(rename_variables,[],[i_0_46]) ).
cnf(i_0_384,plain,
powerset(esk10_0) != esk5_2(powerset(esk10_0),esk10_0),
inference(scs_inference,[],[i_0_294,i_0_373,i_0_218,i_0_209,i_0_40,i_0_52,i_0_46,i_0_60]) ).
cnf(i_0_385,plain,
in(X1,singleton(X1)),
inference(rename_variables,[],[i_0_72]) ).
cnf(i_0_386,plain,
( X1 = X2
| ~ in(X1,singleton(X2)) ),
inference(rename_variables,[],[i_0_69]) ).
cnf(i_0_388,plain,
~ subset(singleton(powerset(esk10_0)),singleton(singleton(esk10_0))),
inference(scs_inference,[],[i_0_323,i_0_40]) ).
cnf(i_0_389,plain,
( in(X1,X2)
| ~ subset(singleton(X1),X2) ),
inference(rename_variables,[],[i_0_40]) ).
cnf(i_0_390,plain,
esk5_2(powerset(esk10_0),esk10_0) != powerset(esk10_0),
inference(scs_inference,[],[i_0_384,i_0_323,i_0_40,i_0_52]) ).
cnf(i_0_391,plain,
~ in(esk5_2(powerset(esk10_0),esk10_0),singleton(powerset(esk10_0))),
inference(scs_inference,[],[i_0_384,i_0_323,i_0_40,i_0_52,i_0_69]) ).
cnf(i_0_392,plain,
( X1 = X2
| ~ in(X1,singleton(X2)) ),
inference(rename_variables,[],[i_0_69]) ).
cnf(i_0_393,plain,
( ~ in(union(powerset(esk10_0)),esk3_2(singleton(esk8_0),singleton(esk7_0)))
| esk5_2(powerset(esk10_0),esk10_0) != union(singleton(esk8_0)) ),
inference(scs_inference,[],[i_0_384,i_0_307,i_0_323,i_0_263,i_0_40,i_0_52,i_0_69,i_0_36]) ).
cnf(i_0_394,plain,
( ~ in(X1,X2)
| ~ in(X3,X1)
| in(X3,X4)
| X4 != union(X2) ),
inference(rename_variables,[],[i_0_36]) ).
cnf(i_0_395,plain,
( ~ subset(esk2_2(esk7_0,singleton(esk8_0)),esk7_0)
| ~ in(esk2_2(esk7_0,singleton(esk8_0)),singleton(esk8_0)) ),
inference(scs_inference,[],[i_0_384,i_0_307,i_0_323,i_0_263,i_0_238,i_0_40,i_0_52,i_0_69,i_0_36,i_0_28]) ).
cnf(i_0_396,plain,
( X1 = powerset(X2)
| ~ subset(esk2_2(X2,X1),X2)
| ~ in(esk2_2(X2,X1),X1) ),
inference(rename_variables,[],[i_0_28]) ).
cnf(i_0_397,plain,
~ subset(singleton(singleton(esk10_0)),singleton(powerset(esk10_0))),
inference(scs_inference,[],[i_0_339,i_0_40]) ).
cnf(i_0_398,plain,
( in(X1,X2)
| ~ subset(singleton(X1),X2) ),
inference(rename_variables,[],[i_0_40]) ).
cnf(i_0_399,plain,
powerset(powerset(esk8_0)) != powerset(singleton(esk7_0)),
inference(scs_inference,[],[i_0_314,i_0_339,i_0_40,i_0_52]) ).
cnf(i_0_400,plain,
esk6_2(powerset(esk10_0),esk10_0) != singleton(powerset(esk10_0)),
inference(scs_inference,[],[i_0_390,i_0_314,i_0_339,i_0_290,i_0_40,i_0_52,i_0_45]) ).
cnf(i_0_401,plain,
( ~ in(X1,X2)
| X1 = X3
| X2 != singleton(X3) ),
inference(rename_variables,[],[i_0_45]) ).
cnf(i_0_402,plain,
singleton(powerset(esk10_0)) != union(powerset(esk10_0)),
inference(scs_inference,[],[i_0_390,i_0_391,i_0_314,i_0_339,i_0_290,i_0_209,i_0_40,i_0_52,i_0_45,i_0_36]) ).
cnf(i_0_403,plain,
( ~ in(X1,X2)
| in(X1,X3)
| ~ in(X2,X4)
| X3 != union(X4) ),
inference(rename_variables,[],[i_0_36]) ).
cnf(i_0_404,plain,
( esk1_2(esk8_0,powerset(esk7_0)) != esk8_0
| ~ in(esk1_2(esk8_0,powerset(esk7_0)),powerset(esk7_0)) ),
inference(scs_inference,[],[i_0_390,i_0_391,i_0_314,i_0_339,i_0_290,i_0_251,i_0_209,i_0_40,i_0_52,i_0_45,i_0_36,i_0_31]) ).
cnf(i_0_405,plain,
( X1 = singleton(X2)
| esk1_2(X2,X1) != X2
| ~ in(esk1_2(X2,X1),X1) ),
inference(rename_variables,[],[i_0_31]) ).
cnf(i_0_406,plain,
( in(esk9_2(powerset(esk7_0),singleton(esk8_0)),singleton(esk8_0))
| in(esk9_2(powerset(esk7_0),singleton(esk8_0)),powerset(esk7_0)) ),
inference(scs_inference,[],[i_0_390,i_0_391,i_0_314,i_0_339,i_0_290,i_0_251,i_0_209,i_0_40,i_0_52,i_0_45,i_0_36,i_0_31,i_0_34]) ).
cnf(i_0_407,plain,
( X1 = X2
| in(esk9_2(X1,X2),X2)
| in(esk9_2(X1,X2),X1) ),
inference(rename_variables,[],[i_0_34]) ).
cnf(i_0_408,plain,
singleton(powerset(esk10_0)) != esk6_2(powerset(esk10_0),esk10_0),
inference(scs_inference,[],[i_0_400,i_0_52]) ).
cnf(i_0_409,plain,
union(powerset(esk10_0)) != singleton(powerset(esk10_0)),
inference(scs_inference,[],[i_0_400,i_0_390,i_0_296,i_0_52,i_0_45]) ).
cnf(i_0_410,plain,
( X1 = X2
| ~ in(X1,X3)
| X3 != singleton(X2) ),
inference(rename_variables,[],[i_0_45]) ).
cnf(i_0_411,plain,
( ~ in(singleton(esk7_0),esk3_2(singleton(esk8_0),singleton(esk7_0)))
| singleton(singleton(esk8_0)) != union(singleton(esk8_0)) ),
inference(scs_inference,[],[i_0_400,i_0_167,i_0_390,i_0_263,i_0_296,i_0_52,i_0_45,i_0_36]) ).
cnf(i_0_412,plain,
( in(X1,X2)
| ~ in(X3,X4)
| ~ in(X1,X3)
| X2 != union(X4) ),
inference(rename_variables,[],[i_0_36]) ).
cnf(i_0_413,plain,
( ~ subset(singleton(singleton(esk7_0)),esk3_2(singleton(esk8_0),singleton(esk7_0)))
| singleton(singleton(esk8_0)) != union(singleton(esk8_0)) ),
inference(scs_inference,[],[i_0_400,i_0_167,i_0_390,i_0_263,i_0_296,i_0_52,i_0_45,i_0_36,i_0_40]) ).
cnf(i_0_414,plain,
( in(X1,X2)
| ~ subset(singleton(X1),X2) ),
inference(rename_variables,[],[i_0_40]) ).
cnf(i_0_415,plain,
( singleton(singleton(esk8_0)) != union(singleton(esk8_0))
| in(esk5_2(powerset(esk10_0),singleton(powerset(esk10_0))),singleton(powerset(esk10_0)))
| in(esk6_2(powerset(esk10_0),singleton(powerset(esk10_0))),powerset(esk10_0)) ),
inference(scs_inference,[],[i_0_400,i_0_402,i_0_167,i_0_390,i_0_263,i_0_296,i_0_52,i_0_45,i_0_36,i_0_40,i_0_32]) ).
cnf(i_0_416,plain,
( ~ in(esk9_2(esk7_0,esk8_0),esk8_0)
| ~ in(esk9_2(esk7_0,esk8_0),esk7_0) ),
inference(scs_inference,[],[i_0_78,i_0_29]) ).
cnf(i_0_417,plain,
( X1 = X2
| ~ in(esk9_2(X1,X2),X2)
| ~ in(esk9_2(X1,X2),X1) ),
inference(rename_variables,[],[i_0_29]) ).
cnf(i_0_418,plain,
( ~ in(esk9_2(esk7_0,esk8_0),esk7_0)
| in(esk9_2(esk7_0,esk8_0),esk7_0) ),
inference(scs_inference,[],[i_0_78,i_0_29,i_0_34]) ).
cnf(i_0_419,plain,
( in(esk9_2(X1,X2),X2)
| X1 = X2
| in(esk9_2(X1,X2),X1) ),
inference(rename_variables,[],[i_0_34]) ).
cnf(i_0_420,plain,
( esk8_0 != union(powerset(esk7_0))
| ~ in(esk9_2(esk7_0,esk8_0),esk7_0) ),
inference(scs_inference,[],[i_0_78,i_0_70,i_0_29,i_0_34,i_0_36]) ).
cnf(i_0_421,plain,
in(X1,powerset(X1)),
inference(rename_variables,[],[i_0_70]) ).
cnf(i_0_422,plain,
( ~ in(X1,X2)
| ~ in(X2,X3)
| in(X1,X4)
| X4 != union(X3) ),
inference(rename_variables,[],[i_0_36]) ).
cnf(i_0_423,plain,
( ~ subset(singleton(esk9_2(esk7_0,esk8_0)),esk8_0)
| ~ in(esk9_2(esk7_0,esk8_0),esk7_0) ),
inference(scs_inference,[],[i_0_78,i_0_70,i_0_29,i_0_34,i_0_36,i_0_40]) ).
cnf(i_0_424,plain,
( in(X1,X2)
| ~ subset(singleton(X1),X2) ),
inference(rename_variables,[],[i_0_40]) ).
cnf(i_0_425,plain,
( ~ in(esk9_2(esk7_0,esk8_0),esk7_0)
| singleton(esk7_0) != union(X1)
| in(esk4_3(X1,singleton(esk7_0),esk3_2(singleton(esk7_0),singleton(esk8_0))),X1) ),
inference(scs_inference,[],[i_0_78,i_0_216,i_0_70,i_0_29,i_0_34,i_0_36,i_0_40,i_0_26]) ).
cnf(i_0_426,plain,
esk6_2(powerset(esk10_0),esk10_0) != powerset(powerset(esk10_0)),
inference(scs_inference,[],[i_0_220,i_0_47,i_0_42]) ).
cnf(i_0_427,plain,
subset(X1,X1),
inference(rename_variables,[],[i_0_47]) ).
cnf(i_0_428,plain,
( in(X1,X2)
| ~ subset(X1,X3)
| X2 != powerset(X3) ),
inference(rename_variables,[],[i_0_42]) ).
cnf(i_0_429,plain,
esk3_2(singleton(esk8_0),singleton(esk7_0)) != powerset(powerset(esk8_0)),
inference(scs_inference,[],[i_0_177,i_0_220,i_0_263,i_0_47,i_0_42,i_0_59]) ).
cnf(i_0_430,plain,
~ in(powerset(powerset(X1)),singleton(X1)),
inference(rename_variables,[],[i_0_177]) ).
cnf(i_0_431,plain,
( in(esk9_2(esk8_0,esk7_0),esk7_0)
| in(esk9_2(esk8_0,esk7_0),esk8_0) ),
inference(scs_inference,[],[i_0_177,i_0_220,i_0_208,i_0_263,i_0_47,i_0_42,i_0_59,i_0_34]) ).
cnf(i_0_432,plain,
( X1 = X2
| in(esk9_2(X1,X2),X2)
| in(esk9_2(X1,X2),X1) ),
inference(rename_variables,[],[i_0_34]) ).
cnf(i_0_433,plain,
( in(esk9_2(esk8_0,esk7_0),esk8_0)
| subset(singleton(esk9_2(esk8_0,esk7_0)),esk7_0) ),
inference(scs_inference,[],[i_0_177,i_0_220,i_0_208,i_0_263,i_0_47,i_0_42,i_0_59,i_0_34,i_0_44]) ).
cnf(i_0_434,plain,
( ~ in(X1,X2)
| subset(singleton(X1),X2) ),
inference(rename_variables,[],[i_0_44]) ).
cnf(i_0_435,plain,
( ~ in(esk7_0,esk9_2(esk8_0,esk7_0))
| in(esk9_2(esk8_0,esk7_0),esk8_0) ),
inference(scs_inference,[],[i_0_177,i_0_220,i_0_208,i_0_263,i_0_47,i_0_42,i_0_59,i_0_34,i_0_44,i_0_43]) ).
cnf(i_0_436,plain,
( ~ in(X1,X2)
| ~ in(X2,X1) ),
inference(rename_variables,[],[i_0_43]) ).
cnf(i_0_437,plain,
( singleton(esk8_0) != union(X1)
| in(esk9_2(esk8_0,esk7_0),esk8_0)
| in(esk3_2(singleton(esk8_0),singleton(esk7_0)),esk4_3(X1,singleton(esk8_0),esk3_2(singleton(esk8_0),singleton(esk7_0)))) ),
inference(scs_inference,[],[i_0_177,i_0_220,i_0_208,i_0_263,i_0_47,i_0_42,i_0_59,i_0_34,i_0_44,i_0_43,i_0_27]) ).
cnf(i_0_438,plain,
powerset(powerset(esk10_0)) != esk6_2(powerset(esk10_0),esk10_0),
inference(scs_inference,[],[i_0_426,i_0_52]) ).
cnf(i_0_439,plain,
singleton(powerset(esk8_0)) != singleton(singleton(esk7_0)),
inference(scs_inference,[],[i_0_426,i_0_277,i_0_72,i_0_52,i_0_45]) ).
cnf(i_0_440,plain,
in(X1,singleton(X1)),
inference(rename_variables,[],[i_0_72]) ).
cnf(i_0_441,plain,
( X1 = X2
| ~ in(X1,X3)
| X3 != singleton(X2) ),
inference(rename_variables,[],[i_0_45]) ).
cnf(i_0_442,plain,
( ~ in(singleton(singleton(X1)),esk3_2(singleton(esk7_0),singleton(esk8_0)))
| powerset(X1) != union(singleton(esk7_0)) ),
inference(scs_inference,[],[i_0_426,i_0_169,i_0_277,i_0_216,i_0_72,i_0_52,i_0_45,i_0_36]) ).
cnf(i_0_443,plain,
( ~ in(X1,X2)
| in(X3,X4)
| ~ in(X3,X1)
| X4 != union(X2) ),
inference(rename_variables,[],[i_0_36]) ).
cnf(i_0_444,plain,
( singleton(singleton(X1)) != X2
| powerset(X1) != singleton(X2) ),
inference(scs_inference,[],[i_0_426,i_0_169,i_0_277,i_0_216,i_0_72,i_0_52,i_0_45,i_0_36,i_0_46]) ).
cnf(i_0_445,plain,
( in(X1,X2)
| X1 != X3
| X2 != singleton(X3) ),
inference(rename_variables,[],[i_0_46]) ).
cnf(i_0_446,plain,
( ~ subset(esk2_2(esk8_0,singleton(esk7_0)),esk8_0)
| ~ in(esk2_2(esk8_0,singleton(esk7_0)),singleton(esk7_0)) ),
inference(scs_inference,[],[i_0_255,i_0_28]) ).
cnf(i_0_447,plain,
( X1 = powerset(X2)
| ~ subset(esk2_2(X2,X1),X2)
| ~ in(esk2_2(X2,X1),X1) ),
inference(rename_variables,[],[i_0_28]) ).
cnf(i_0_448,plain,
( esk1_2(singleton(X1),X1) != singleton(X1)
| ~ in(esk1_2(singleton(X1),X1),X1) ),
inference(scs_inference,[],[i_0_124,i_0_255,i_0_28,i_0_31]) ).
cnf(i_0_449,plain,
( X1 = singleton(X2)
| esk1_2(X2,X1) != X2
| ~ in(esk1_2(X2,X1),X1) ),
inference(rename_variables,[],[i_0_31]) ).
cnf(i_0_450,plain,
esk3_2(singleton(esk7_0),singleton(esk8_0)) = esk7_0,
inference(scs_inference,[],[i_0_216,i_0_69]) ).
cnf(i_0_451,plain,
( ~ in(X1,singleton(X2))
| X1 = X2 ),
inference(rename_variables,[],[i_0_69]) ).
cnf(i_0_452,plain,
esk7_0 = esk3_2(singleton(esk7_0),singleton(esk8_0)),
inference(scs_inference,[],[i_0_216,i_0_69,i_0_52]) ).
cnf(i_0_453,plain,
subset(esk7_0,esk3_2(singleton(esk7_0),singleton(esk8_0))),
inference(scs_inference,[],[i_0_216,i_0_47,i_0_69,i_0_52,i_0_61]) ).
cnf(i_0_454,plain,
subset(X1,X1),
inference(rename_variables,[],[i_0_47]) ).
cnf(i_0_455,plain,
esk7_0 != esk3_2(singleton(esk8_0),singleton(esk7_0)),
inference(scs_inference,[],[i_0_343,i_0_216,i_0_47,i_0_69,i_0_52,i_0_61,i_0_53]) ).
cnf(i_0_456,plain,
subset(esk3_2(singleton(esk7_0),singleton(esk8_0)),esk7_0),
inference(scs_inference,[],[i_0_343,i_0_216,i_0_47,i_0_454,i_0_69,i_0_52,i_0_61,i_0_53,i_0_62]) ).
cnf(i_0_457,plain,
subset(X1,X1),
inference(rename_variables,[],[i_0_47]) ).
cnf(i_0_458,plain,
in(esk3_2(singleton(esk7_0),singleton(esk8_0)),powerset(esk7_0)),
inference(scs_inference,[],[i_0_343,i_0_216,i_0_47,i_0_454,i_0_70,i_0_69,i_0_52,i_0_61,i_0_53,i_0_62,i_0_59]) ).
cnf(i_0_459,plain,
in(X1,powerset(X1)),
inference(rename_variables,[],[i_0_70]) ).
cnf(i_0_460,plain,
~ in(powerset(esk7_0),esk3_2(singleton(esk7_0),singleton(esk8_0))),
inference(scs_inference,[],[i_0_343,i_0_216,i_0_47,i_0_454,i_0_70,i_0_69,i_0_52,i_0_61,i_0_53,i_0_62,i_0_59,i_0_43]) ).
cnf(i_0_461,plain,
( ~ in(X1,X2)
| ~ in(X2,X1) ),
inference(rename_variables,[],[i_0_43]) ).
cnf(i_0_462,plain,
( subset(esk5_2(powerset(esk10_0),esk10_0),X1)
| union(powerset(esk10_0)) != powerset(X1) ),
inference(scs_inference,[],[i_0_343,i_0_296,i_0_216,i_0_47,i_0_454,i_0_70,i_0_69,i_0_52,i_0_61,i_0_53,i_0_62,i_0_59,i_0_43,i_0_41]) ).
cnf(i_0_463,plain,
( ~ in(X1,X2)
| subset(X1,X3)
| X2 != powerset(X3) ),
inference(rename_variables,[],[i_0_41]) ).
cnf(i_0_464,plain,
( singleton(powerset(esk10_0)) != powerset(X1)
| union(powerset(esk10_0)) != powerset(X1) ),
inference(scs_inference,[],[i_0_343,i_0_391,i_0_296,i_0_216,i_0_47,i_0_454,i_0_70,i_0_69,i_0_52,i_0_61,i_0_53,i_0_62,i_0_59,i_0_43,i_0_41,i_0_42]) ).
cnf(i_0_465,plain,
( ~ subset(X1,X2)
| in(X1,X3)
| X3 != powerset(X2) ),
inference(rename_variables,[],[i_0_42]) ).
cnf(i_0_467,plain,
~ subset(singleton(powerset(esk7_0)),esk3_2(singleton(esk7_0),singleton(esk8_0))),
inference(scs_inference,[],[i_0_460,i_0_40]) ).
cnf(i_0_468,plain,
( in(X1,X2)
| ~ subset(singleton(X1),X2) ),
inference(rename_variables,[],[i_0_40]) ).
cnf(i_0_469,plain,
esk3_2(singleton(esk8_0),singleton(esk7_0)) != esk7_0,
inference(scs_inference,[],[i_0_460,i_0_455,i_0_40,i_0_52]) ).
cnf(i_0_470,plain,
esk3_2(singleton(esk7_0),singleton(esk8_0)) != powerset(powerset(esk7_0)),
inference(scs_inference,[],[i_0_460,i_0_455,i_0_47,i_0_40,i_0_52,i_0_42]) ).
cnf(i_0_471,plain,
subset(X1,X1),
inference(rename_variables,[],[i_0_47]) ).
cnf(i_0_472,plain,
( in(X1,X2)
| ~ subset(X1,X3)
| X2 != powerset(X3) ),
inference(rename_variables,[],[i_0_42]) ).
cnf(i_0_473,plain,
singleton(singleton(esk7_0)) != esk3_2(singleton(esk7_0),singleton(esk8_0)),
inference(scs_inference,[],[i_0_460,i_0_450,i_0_455,i_0_133,i_0_47,i_0_40,i_0_52,i_0_42,i_0_53]) ).
cnf(i_0_474,plain,
singleton(singleton(X1)) != X1,
inference(rename_variables,[],[i_0_133]) ).
cnf(i_0_475,plain,
powerset(powerset(esk7_0)) != esk3_2(singleton(esk7_0),singleton(esk8_0)),
inference(scs_inference,[],[i_0_460,i_0_450,i_0_455,i_0_133,i_0_47,i_0_70,i_0_40,i_0_52,i_0_42,i_0_53,i_0_60]) ).
cnf(i_0_476,plain,
in(X1,powerset(X1)),
inference(rename_variables,[],[i_0_70]) ).
cnf(i_0_477,plain,
esk6_2(powerset(esk10_0),esk10_0) != powerset(singleton(esk10_0)),
inference(scs_inference,[],[i_0_460,i_0_450,i_0_455,i_0_133,i_0_154,i_0_209,i_0_47,i_0_70,i_0_40,i_0_52,i_0_42,i_0_53,i_0_60,i_0_59]) ).
cnf(i_0_478,plain,
~ in(powerset(singleton(X1)),powerset(X1)),
inference(rename_variables,[],[i_0_154]) ).
cnf(i_0_479,plain,
( ~ in(esk9_2(singleton(esk7_0),singleton(esk8_0)),singleton(esk8_0))
| ~ in(esk9_2(singleton(esk7_0),singleton(esk8_0)),singleton(esk7_0)) ),
inference(scs_inference,[],[i_0_460,i_0_450,i_0_455,i_0_133,i_0_154,i_0_158,i_0_209,i_0_47,i_0_70,i_0_40,i_0_52,i_0_42,i_0_53,i_0_60,i_0_59,i_0_29]) ).
cnf(i_0_480,plain,
( X1 = X2
| ~ in(esk9_2(X1,X2),X2)
| ~ in(esk9_2(X1,X2),X1) ),
inference(rename_variables,[],[i_0_29]) ).
cnf(i_0_481,plain,
( ~ in(esk9_2(singleton(esk7_0),singleton(esk8_0)),singleton(esk7_0))
| in(esk9_2(singleton(esk7_0),singleton(esk8_0)),singleton(esk7_0)) ),
inference(scs_inference,[],[i_0_460,i_0_450,i_0_455,i_0_133,i_0_154,i_0_158,i_0_209,i_0_47,i_0_70,i_0_40,i_0_52,i_0_42,i_0_53,i_0_60,i_0_59,i_0_29,i_0_34]) ).
cnf(i_0_482,plain,
( X1 = X2
| in(esk9_2(X1,X2),X2)
| in(esk9_2(X1,X2),X1) ),
inference(rename_variables,[],[i_0_34]) ).
cnf(i_0_483,plain,
( ~ in(esk9_2(union(powerset(esk10_0)),esk10_0),union(powerset(esk10_0)))
| ~ in(esk9_2(union(powerset(esk10_0)),esk10_0),esk10_0)
| ~ in(esk9_2(singleton(esk7_0),singleton(esk8_0)),singleton(esk7_0)) ),
inference(scs_inference,[],[i_0_48,i_0_460,i_0_450,i_0_455,i_0_133,i_0_154,i_0_158,i_0_209,i_0_47,i_0_70,i_0_40,i_0_52,i_0_42,i_0_53,i_0_60,i_0_59,i_0_29,i_0_34,i_0_480]) ).
cnf(i_0_484,plain,
powerset(singleton(esk7_0)) != esk3_2(singleton(esk7_0),singleton(esk8_0)),
inference(scs_inference,[],[i_0_275,i_0_156,i_0_62]) ).
cnf(i_0_485,plain,
subset(singleton(X1),powerset(X1)),
inference(rename_variables,[],[i_0_156]) ).
cnf(i_0_486,plain,
( union(powerset(esk10_0)) != X1
| singleton(esk10_0) != singleton(X1) ),
inference(scs_inference,[],[i_0_275,i_0_152,i_0_156,i_0_62,i_0_46]) ).
cnf(i_0_487,plain,
( in(X1,X2)
| X1 != X3
| X2 != singleton(X3) ),
inference(rename_variables,[],[i_0_46]) ).
cnf(i_0_488,plain,
esk3_2(singleton(esk7_0),singleton(esk8_0)) != singleton(singleton(esk7_0)),
inference(scs_inference,[],[i_0_452,i_0_275,i_0_152,i_0_124,i_0_156,i_0_62,i_0_46,i_0_53]) ).
cnf(i_0_489,plain,
X1 != singleton(singleton(X1)),
inference(rename_variables,[],[i_0_124]) ).
cnf(i_0_490,plain,
in(X1,singleton(X1)),
inference(rename_variables,[],[i_0_72]) ).
cnf(i_0_491,plain,
( X1 = X2
| ~ in(X1,singleton(X2)) ),
inference(rename_variables,[],[i_0_69]) ).
cnf(i_0_492,plain,
powerset(powerset(X1)) != X1,
inference(rename_variables,[],[i_0_104]) ).
cnf(i_0_493,plain,
( singleton(esk10_0) != singleton(union(powerset(esk10_0)))
| in(esk5_2(X1,powerset(powerset(union(X1)))),powerset(powerset(union(X1))))
| in(esk6_2(X1,powerset(powerset(union(X1)))),X1) ),
inference(scs_inference,[],[i_0_452,i_0_275,i_0_104,i_0_152,i_0_124,i_0_156,i_0_72,i_0_62,i_0_46,i_0_53,i_0_69,i_0_32]) ).
cnf(i_0_494,plain,
esk3_2(singleton(esk8_0),singleton(esk7_0)) = esk8_0,
inference(scs_inference,[],[i_0_263,i_0_69]) ).
cnf(i_0_495,plain,
( ~ in(X1,singleton(X2))
| X1 = X2 ),
inference(rename_variables,[],[i_0_69]) ).
cnf(i_0_496,plain,
esk8_0 = esk3_2(singleton(esk8_0),singleton(esk7_0)),
inference(scs_inference,[],[i_0_263,i_0_69,i_0_52]) ).
cnf(i_0_497,plain,
subset(esk3_2(singleton(esk8_0),singleton(esk7_0)),esk8_0),
inference(scs_inference,[],[i_0_263,i_0_47,i_0_69,i_0_52,i_0_62]) ).
cnf(i_0_498,plain,
subset(X1,X1),
inference(rename_variables,[],[i_0_47]) ).
cnf(i_0_499,plain,
~ empty(esk3_2(singleton(esk8_0),singleton(esk7_0))),
inference(scs_inference,[],[i_0_49,i_0_263,i_0_47,i_0_69,i_0_52,i_0_62,i_0_63]) ).
cnf(i_0_500,plain,
singleton(singleton(esk10_0)) != singleton(powerset(esk10_0)),
inference(scs_inference,[],[i_0_327,i_0_49,i_0_263,i_0_47,i_0_72,i_0_69,i_0_52,i_0_62,i_0_63,i_0_45]) ).
cnf(i_0_501,plain,
in(X1,singleton(X1)),
inference(rename_variables,[],[i_0_72]) ).
cnf(i_0_502,plain,
( X1 = X2
| ~ in(X1,X3)
| X3 != singleton(X2) ),
inference(rename_variables,[],[i_0_45]) ).
cnf(i_0_503,plain,
singleton(powerset(esk7_0)) != powerset(powerset(esk8_0)),
inference(scs_inference,[],[i_0_247,i_0_327,i_0_49,i_0_263,i_0_156,i_0_47,i_0_72,i_0_69,i_0_52,i_0_62,i_0_63,i_0_45,i_0_42]) ).
cnf(i_0_504,plain,
subset(singleton(X1),powerset(X1)),
inference(rename_variables,[],[i_0_156]) ).
cnf(i_0_505,plain,
( in(X1,X2)
| ~ subset(X1,X3)
| X2 != powerset(X3) ),
inference(rename_variables,[],[i_0_42]) ).
cnf(i_0_506,plain,
powerset(powerset(esk8_0)) != esk3_2(singleton(esk8_0),singleton(esk7_0)),
inference(scs_inference,[],[i_0_429,i_0_52]) ).
cnf(i_0_507,plain,
subset(esk8_0,esk3_2(singleton(esk8_0),singleton(esk7_0))),
inference(scs_inference,[],[i_0_494,i_0_429,i_0_47,i_0_52,i_0_61]) ).
cnf(i_0_508,plain,
subset(X1,X1),
inference(rename_variables,[],[i_0_47]) ).
cnf(i_0_509,plain,
powerset(singleton(esk8_0)) != esk3_2(singleton(esk8_0),singleton(esk7_0)),
inference(scs_inference,[],[i_0_494,i_0_287,i_0_429,i_0_156,i_0_47,i_0_52,i_0_61,i_0_62]) ).
cnf(i_0_510,plain,
subset(singleton(X1),powerset(X1)),
inference(rename_variables,[],[i_0_156]) ).
cnf(i_0_511,plain,
empty(esk3_2(singleton(esk7_0),singleton(esk8_0))),
inference(scs_inference,[],[i_0_494,i_0_287,i_0_429,i_0_452,i_0_50,i_0_156,i_0_47,i_0_52,i_0_61,i_0_62,i_0_63]) ).
cnf(i_0_512,plain,
~ in(powerset(esk8_0),esk3_2(singleton(esk8_0),singleton(esk7_0))),
inference(scs_inference,[],[i_0_494,i_0_497,i_0_287,i_0_429,i_0_452,i_0_50,i_0_85,i_0_156,i_0_47,i_0_52,i_0_61,i_0_62,i_0_63,i_0_38]) ).
cnf(i_0_513,plain,
~ in(powerset(X1),X1),
inference(rename_variables,[],[i_0_85]) ).
cnf(i_0_514,plain,
( in(X1,X2)
| ~ subset(X3,X2)
| ~ in(X1,X3) ),
inference(rename_variables,[],[i_0_38]) ).
cnf(i_0_515,plain,
in(esk3_2(singleton(esk8_0),singleton(esk7_0)),powerset(esk8_0)),
inference(scs_inference,[],[i_0_494,i_0_496,i_0_497,i_0_287,i_0_429,i_0_452,i_0_50,i_0_85,i_0_156,i_0_47,i_0_70,i_0_52,i_0_61,i_0_62,i_0_63,i_0_38,i_0_59]) ).
cnf(i_0_516,plain,
in(X1,powerset(X1)),
inference(rename_variables,[],[i_0_70]) ).
cnf(i_0_517,plain,
( ~ subset(esk2_2(singleton(X1),X1),singleton(X1))
| ~ in(esk2_2(singleton(X1),X1),X1) ),
inference(scs_inference,[],[i_0_494,i_0_496,i_0_497,i_0_287,i_0_429,i_0_452,i_0_50,i_0_77,i_0_85,i_0_156,i_0_47,i_0_70,i_0_52,i_0_61,i_0_62,i_0_63,i_0_38,i_0_59,i_0_28]) ).
cnf(i_0_518,plain,
( X1 = powerset(X2)
| ~ subset(esk2_2(X2,X1),X2)
| ~ in(esk2_2(X2,X1),X1) ),
inference(rename_variables,[],[i_0_28]) ).
cnf(i_0_519,plain,
( esk1_2(powerset(X1),X1) != powerset(X1)
| ~ in(esk1_2(powerset(X1),X1),X1) ),
inference(scs_inference,[],[i_0_494,i_0_496,i_0_497,i_0_287,i_0_429,i_0_452,i_0_79,i_0_50,i_0_77,i_0_85,i_0_156,i_0_47,i_0_70,i_0_52,i_0_61,i_0_62,i_0_63,i_0_38,i_0_59,i_0_28,i_0_31]) ).
cnf(i_0_520,plain,
( X1 = singleton(X2)
| esk1_2(X2,X1) != X2
| ~ in(esk1_2(X2,X1),X1) ),
inference(rename_variables,[],[i_0_31]) ).
cnf(i_0_521,plain,
~ subset(singleton(powerset(esk8_0)),esk3_2(singleton(esk8_0),singleton(esk7_0))),
inference(scs_inference,[],[i_0_512,i_0_40]) ).
cnf(i_0_522,plain,
( in(X1,X2)
| ~ subset(singleton(X1),X2) ),
inference(rename_variables,[],[i_0_40]) ).
cnf(i_0_523,plain,
( subset(esk3_2(singleton(esk8_0),singleton(esk7_0)),X1)
| powerset(esk8_0) != powerset(X1) ),
inference(scs_inference,[],[i_0_515,i_0_512,i_0_40,i_0_41]) ).
cnf(i_0_524,plain,
( ~ in(X1,X2)
| subset(X1,X3)
| X2 != powerset(X3) ),
inference(rename_variables,[],[i_0_41]) ).
cnf(i_0_525,plain,
( singleton(esk7_0) != powerset(X1)
| powerset(esk8_0) != powerset(X1) ),
inference(scs_inference,[],[i_0_515,i_0_512,i_0_261,i_0_40,i_0_41,i_0_42]) ).
cnf(i_0_526,plain,
( ~ subset(X1,X2)
| in(X1,X3)
| X3 != powerset(X2) ),
inference(rename_variables,[],[i_0_42]) ).
cnf(i_0_527,plain,
( powerset(esk8_0) != powerset(X1)
| powerset(esk8_0) != union(X2)
| in(esk4_3(X2,powerset(esk8_0),esk3_2(singleton(esk8_0),singleton(esk7_0))),X2) ),
inference(scs_inference,[],[i_0_515,i_0_512,i_0_261,i_0_40,i_0_41,i_0_42,i_0_26]) ).
cnf(i_0_528,plain,
subset(esk3_2(singleton(esk8_0),singleton(esk7_0)),esk8_0),
inference(equality_inference,[],[523]) ).
cnf(i_0_529,plain,
powerset(singleton(esk10_0)) != esk6_2(powerset(esk10_0),esk10_0),
inference(scs_inference,[],[i_0_477,i_0_52]) ).
cnf(i_0_530,plain,
powerset(singleton(esk8_0)) != powerset(powerset(esk7_0)),
inference(scs_inference,[],[i_0_477,i_0_218,i_0_156,i_0_52,i_0_42]) ).
cnf(i_0_531,plain,
subset(singleton(X1),powerset(X1)),
inference(rename_variables,[],[i_0_156]) ).
cnf(i_0_532,plain,
( in(X1,X2)
| ~ subset(X1,X3)
| X2 != powerset(X3) ),
inference(rename_variables,[],[i_0_42]) ).
cnf(i_0_533,plain,
( ~ in(esk9_2(powerset(esk8_0),singleton(esk7_0)),singleton(esk7_0))
| ~ in(esk9_2(powerset(esk8_0),singleton(esk7_0)),powerset(esk8_0)) ),
inference(scs_inference,[],[i_0_477,i_0_218,i_0_277,i_0_156,i_0_52,i_0_42,i_0_29]) ).
cnf(i_0_534,plain,
( X1 = X2
| ~ in(esk9_2(X1,X2),X2)
| ~ in(esk9_2(X1,X2),X1) ),
inference(rename_variables,[],[i_0_29]) ).
cnf(i_0_535,plain,
( ~ in(esk3_2(singleton(esk7_0),singleton(esk8_0)),esk3_2(singleton(esk8_0),singleton(esk7_0)))
| singleton(esk8_0) != union(powerset(esk8_0)) ),
inference(scs_inference,[],[i_0_477,i_0_214,i_0_218,i_0_515,i_0_277,i_0_156,i_0_52,i_0_42,i_0_29,i_0_36]) ).
cnf(i_0_536,plain,
( ~ in(X1,X2)
| in(X3,X4)
| ~ in(X3,X1)
| X4 != union(X2) ),
inference(rename_variables,[],[i_0_36]) ).
cnf(i_0_537,plain,
esk8_0 != esk3_2(singleton(esk7_0),singleton(esk8_0)),
inference(scs_inference,[],[i_0_293,i_0_494,i_0_53]) ).
cnf(i_0_538,plain,
( esk6_2(powerset(esk10_0),esk10_0) != X1
| singleton(esk10_0) != singleton(X1) ),
inference(scs_inference,[],[i_0_303,i_0_293,i_0_494,i_0_53,i_0_46]) ).
cnf(i_0_539,plain,
( in(X1,X2)
| X1 != X3
| X2 != singleton(X3) ),
inference(rename_variables,[],[i_0_46]) ).
cnf(i_0_540,plain,
( in(esk9_2(singleton(esk8_0),singleton(esk7_0)),singleton(esk7_0))
| in(esk9_2(singleton(esk8_0),singleton(esk7_0)),singleton(esk8_0)) ),
inference(scs_inference,[],[i_0_303,i_0_293,i_0_494,i_0_173,i_0_53,i_0_46,i_0_34]) ).
cnf(i_0_541,plain,
( X1 = X2
| in(esk9_2(X1,X2),X2)
| in(esk9_2(X1,X2),X1) ),
inference(rename_variables,[],[i_0_34]) ).
cnf(i_0_542,plain,
singleton(powerset(esk8_0)) != esk3_2(singleton(esk8_0),singleton(esk7_0)),
inference(scs_inference,[],[i_0_512,i_0_72,i_0_60]) ).
cnf(i_0_543,plain,
in(X1,singleton(X1)),
inference(rename_variables,[],[i_0_72]) ).
cnf(i_0_544,plain,
( esk1_2(esk7_0,singleton(esk8_0)) != esk7_0
| ~ in(esk1_2(esk7_0,singleton(esk8_0)),singleton(esk8_0)) ),
inference(scs_inference,[],[i_0_512,i_0_173,i_0_72,i_0_60,i_0_31]) ).
cnf(i_0_545,plain,
( X1 = singleton(X2)
| esk1_2(X2,X1) != X2
| ~ in(esk1_2(X2,X1),X1) ),
inference(rename_variables,[],[i_0_31]) ).
cnf(i_0_547,plain,
powerset(singleton(esk8_0)) != singleton(powerset(esk7_0)),
inference(scs_inference,[],[i_0_238,i_0_70,i_0_45]) ).
cnf(i_0_548,plain,
in(X1,powerset(X1)),
inference(rename_variables,[],[i_0_70]) ).
cnf(i_0_549,plain,
( X1 = X2
| ~ in(X1,X3)
| X3 != singleton(X2) ),
inference(rename_variables,[],[i_0_45]) ).
cnf(i_0_550,plain,
( subset(esk3_2(singleton(esk7_0),singleton(esk8_0)),X1)
| powerset(esk7_0) != powerset(X1) ),
inference(scs_inference,[],[i_0_458,i_0_238,i_0_70,i_0_45,i_0_41]) ).
cnf(i_0_551,plain,
( ~ in(X1,X2)
| subset(X1,X3)
| X2 != powerset(X3) ),
inference(rename_variables,[],[i_0_41]) ).
cnf(i_0_552,plain,
( subset(esk7_0,X1)
| powerset(esk7_0) != powerset(X1) ),
inference(scs_inference,[],[i_0_458,i_0_450,i_0_238,i_0_70,i_0_45,i_0_41,i_0_61]) ).
cnf(i_0_553,plain,
in(X1,powerset(X1)),
inference(rename_variables,[],[i_0_70]) ).
cnf(i_0_554,plain,
( X1 = union(X2)
| ~ in(esk5_2(X2,X1),X3)
| ~ in(X3,X2)
| ~ in(esk5_2(X2,X1),X1) ),
inference(rename_variables,[],[i_0_25]) ).
cnf(i_0_555,plain,
( ~ in(powerset(esk5_2(powerset(esk10_0),singleton(powerset(esk10_0)))),powerset(esk10_0))
| powerset(esk7_0) != powerset(X1)
| ~ in(esk5_2(powerset(esk10_0),singleton(powerset(esk10_0))),singleton(powerset(esk10_0))) ),
inference(scs_inference,[],[i_0_458,i_0_402,i_0_450,i_0_238,i_0_70,i_0_548,i_0_45,i_0_41,i_0_61,i_0_25]) ).
cnf(i_0_556,plain,
subset(esk3_2(singleton(esk7_0),singleton(esk8_0)),esk7_0),
inference(equality_inference,[],[550]) ).
cnf(i_0_557,plain,
subset(esk7_0,esk7_0),
inference(equality_inference,[],[552]) ).
cnf(i_0_558,plain,
( ~ in(esk5_2(powerset(esk10_0),singleton(powerset(esk10_0))),singleton(powerset(esk10_0)))
| ~ in(powerset(esk5_2(powerset(esk10_0),singleton(powerset(esk10_0)))),powerset(esk10_0)) ),
inference(equality_inference,[],[555]) ).
cnf(i_0_559,plain,
esk3_2(singleton(esk7_0),singleton(esk8_0)) != esk8_0,
inference(scs_inference,[],[i_0_537,i_0_52]) ).
cnf(i_0_560,plain,
( ~ in(esk9_2(singleton(esk10_0),powerset(esk10_0)),powerset(esk10_0))
| ~ in(esk9_2(singleton(esk10_0),powerset(esk10_0)),singleton(esk10_0)) ),
inference(scs_inference,[],[i_0_537,i_0_327,i_0_52,i_0_29]) ).
cnf(i_0_561,plain,
( X1 = X2
| ~ in(esk9_2(X1,X2),X2)
| ~ in(esk9_2(X1,X2),X1) ),
inference(rename_variables,[],[i_0_29]) ).
cnf(i_0_562,plain,
( ~ in(esk9_2(singleton(esk10_0),powerset(esk10_0)),singleton(esk10_0))
| in(esk9_2(singleton(esk10_0),powerset(esk10_0)),singleton(esk10_0)) ),
inference(scs_inference,[],[i_0_537,i_0_327,i_0_52,i_0_29,i_0_34]) ).
cnf(i_0_563,plain,
( in(esk9_2(X1,X2),X2)
| X1 = X2
| in(esk9_2(X1,X2),X1) ),
inference(rename_variables,[],[i_0_34]) ).
cnf(i_0_564,plain,
subset(singleton(X1),powerset(X1)),
inference(rename_variables,[],[i_0_156]) ).
cnf(i_0_565,plain,
( ~ subset(esk9_2(singleton(esk10_0),powerset(esk10_0)),esk10_0)
| ~ in(esk9_2(singleton(esk10_0),powerset(esk10_0)),singleton(esk10_0)) ),
inference(scs_inference,[],[i_0_537,i_0_327,i_0_156,i_0_52,i_0_29,i_0_34,i_0_38,i_0_68]) ).
cnf(i_0_566,plain,
( in(X1,powerset(X2))
| ~ subset(X1,X2) ),
inference(rename_variables,[],[i_0_68]) ).
cnf(i_0_567,plain,
( ~ in(esk9_2(singleton(esk10_0),powerset(esk10_0)),singleton(esk10_0))
| powerset(esk7_0) != union(X1)
| in(esk3_2(singleton(esk7_0),singleton(esk8_0)),esk4_3(X1,powerset(esk7_0),esk3_2(singleton(esk7_0),singleton(esk8_0)))) ),
inference(scs_inference,[],[i_0_537,i_0_458,i_0_327,i_0_156,i_0_52,i_0_29,i_0_34,i_0_38,i_0_68,i_0_27]) ).
cnf(i_0_568,plain,
( in(esk9_2(esk7_0,esk8_0),esk8_0)
| in(esk9_2(esk7_0,esk8_0),esk7_0) ),
inference(scs_inference,[],[i_0_78,i_0_34]) ).
cnf(i_0_569,plain,
( X1 = X2
| in(esk9_2(X1,X2),X2)
| in(esk9_2(X1,X2),X1) ),
inference(rename_variables,[],[i_0_34]) ).
cnf(i_0_570,plain,
( in(esk9_2(esk7_0,esk8_0),esk3_2(singleton(esk8_0),singleton(esk7_0)))
| in(esk9_2(esk7_0,esk8_0),esk7_0) ),
inference(scs_inference,[],[i_0_496,i_0_78,i_0_34,i_0_60]) ).
cnf(i_0_571,plain,
( in(esk9_2(esk7_0,esk8_0),esk7_0)
| subset(singleton(esk9_2(esk7_0,esk8_0)),esk8_0) ),
inference(scs_inference,[],[i_0_496,i_0_78,i_0_34,i_0_60,i_0_44]) ).
cnf(i_0_572,plain,
( ~ in(X1,X2)
| subset(singleton(X1),X2) ),
inference(rename_variables,[],[i_0_44]) ).
cnf(i_0_573,plain,
( ~ in(esk8_0,esk9_2(esk7_0,esk8_0))
| in(esk9_2(esk7_0,esk8_0),esk7_0) ),
inference(scs_inference,[],[i_0_496,i_0_78,i_0_34,i_0_60,i_0_44,i_0_43]) ).
cnf(i_0_574,plain,
( ~ in(X1,X2)
| ~ in(X2,X1) ),
inference(rename_variables,[],[i_0_43]) ).
cnf(i_0_575,plain,
singleton(singleton(X1)) != X1,
inference(rename_variables,[],[i_0_133]) ).
cnf(i_0_576,plain,
( in(esk5_2(X1,singleton(singleton(union(X1)))),singleton(singleton(union(X1))))
| in(esk9_2(esk7_0,esk8_0),esk7_0)
| in(esk6_2(X1,singleton(singleton(union(X1)))),X1) ),
inference(scs_inference,[],[i_0_133,i_0_496,i_0_78,i_0_34,i_0_60,i_0_44,i_0_43,i_0_32]) ).
cnf(i_0_577,plain,
esk3_2(singleton(esk8_0),singleton(esk7_0)) != singleton(powerset(esk8_0)),
inference(scs_inference,[],[i_0_496,i_0_79,i_0_53]) ).
cnf(i_0_578,plain,
X1 != singleton(powerset(X1)),
inference(rename_variables,[],[i_0_79]) ).
cnf(i_0_579,plain,
( union(powerset(esk10_0)) != X1
| esk5_2(powerset(esk10_0),esk10_0) != singleton(X1) ),
inference(scs_inference,[],[i_0_307,i_0_496,i_0_79,i_0_53,i_0_46]) ).
cnf(i_0_580,plain,
( in(X1,X2)
| X1 != X3
| X2 != singleton(X3) ),
inference(rename_variables,[],[i_0_46]) ).
cnf(i_0_581,plain,
( in(esk9_2(singleton(esk7_0),singleton(esk8_0)),singleton(esk8_0))
| in(esk9_2(singleton(esk7_0),singleton(esk8_0)),singleton(esk7_0)) ),
inference(scs_inference,[],[i_0_158,i_0_34]) ).
cnf(i_0_582,plain,
( X1 = X2
| in(esk9_2(X1,X2),X2)
| in(esk9_2(X1,X2),X1) ),
inference(rename_variables,[],[i_0_34]) ).
cnf(i_0_583,plain,
( esk9_2(singleton(esk7_0),singleton(esk8_0)) != esk7_0
| in(esk9_2(singleton(esk7_0),singleton(esk8_0)),singleton(esk7_0)) ),
inference(scs_inference,[],[i_0_204,i_0_158,i_0_34,i_0_59]) ).
cnf(i_0_584,plain,
( ~ in(singleton(esk8_0),esk9_2(singleton(esk7_0),singleton(esk8_0)))
| in(esk9_2(singleton(esk7_0),singleton(esk8_0)),singleton(esk7_0)) ),
inference(scs_inference,[],[i_0_204,i_0_158,i_0_34,i_0_59,i_0_43]) ).
cnf(i_0_585,plain,
( ~ in(X1,X2)
| ~ in(X2,X1) ),
inference(rename_variables,[],[i_0_43]) ).
cnf(i_0_586,plain,
( esk9_2(singleton(esk7_0),singleton(esk8_0)) = esk8_0
| in(esk9_2(singleton(esk7_0),singleton(esk8_0)),singleton(esk7_0)) ),
inference(scs_inference,[],[i_0_204,i_0_158,i_0_34,i_0_59,i_0_43,i_0_69]) ).
cnf(i_0_587,plain,
( ~ in(X1,singleton(X2))
| X1 = X2 ),
inference(rename_variables,[],[i_0_69]) ).
cnf(i_0_588,plain,
( esk8_0 = esk9_2(singleton(esk7_0),singleton(esk8_0))
| in(esk9_2(singleton(esk7_0),singleton(esk8_0)),singleton(esk7_0)) ),
inference(scs_inference,[],[i_0_204,i_0_158,i_0_34,i_0_59,i_0_43,i_0_69,i_0_52]) ).
cnf(i_0_589,plain,
( X1 = singleton(X2)
| esk1_2(X2,X1) != X2
| ~ in(esk1_2(X2,X1),X1) ),
inference(rename_variables,[],[i_0_31]) ).
cnf(i_0_590,plain,
( ~ in(esk1_2(singleton(esk8_0),singleton(singleton(esk7_0))),singleton(singleton(esk7_0)))
| esk1_2(singleton(esk8_0),singleton(singleton(esk7_0))) != singleton(esk8_0)
| in(esk9_2(singleton(esk7_0),singleton(esk8_0)),singleton(esk7_0)) ),
inference(scs_inference,[],[i_0_289,i_0_204,i_0_158,i_0_34,i_0_59,i_0_43,i_0_69,i_0_52,i_0_31]) ).
cnf(i_0_591,plain,
powerset(powerset(esk8_0)) != singleton(powerset(esk7_0)),
inference(scs_inference,[],[i_0_503,i_0_52]) ).
cnf(i_0_592,plain,
( subset(esk6_2(powerset(esk10_0),esk10_0),X1)
| powerset(esk10_0) != powerset(X1) ),
inference(scs_inference,[],[i_0_503,i_0_209,i_0_52,i_0_41]) ).
cnf(i_0_593,plain,
( ~ in(X1,X2)
| subset(X1,X3)
| X2 != powerset(X3) ),
inference(rename_variables,[],[i_0_41]) ).
cnf(i_0_594,plain,
( singleton(esk10_0) != powerset(X1)
| powerset(esk10_0) != powerset(X1) ),
inference(scs_inference,[],[i_0_503,i_0_303,i_0_209,i_0_52,i_0_41,i_0_42]) ).
cnf(i_0_595,plain,
( ~ subset(X1,X2)
| in(X1,X3)
| X3 != powerset(X2) ),
inference(rename_variables,[],[i_0_42]) ).
cnf(i_0_596,plain,
( subset(esk6_2(powerset(esk10_0),esk10_0),esk3_2(singleton(esk7_0),singleton(esk8_0)))
| powerset(esk10_0) != powerset(esk7_0) ),
inference(scs_inference,[],[i_0_503,i_0_303,i_0_452,i_0_209,i_0_52,i_0_41,i_0_42,i_0_62]) ).
cnf(i_0_597,plain,
( ~ in(singleton(esk10_0),singleton(powerset(esk7_0)))
| powerset(esk10_0) != powerset(esk7_0) ),
inference(scs_inference,[],[i_0_503,i_0_303,i_0_452,i_0_209,i_0_52,i_0_41,i_0_42,i_0_62,i_0_69]) ).
cnf(i_0_598,plain,
( X1 = X2
| ~ in(X1,singleton(X2)) ),
inference(rename_variables,[],[i_0_69]) ).
cnf(i_0_599,plain,
( ~ subset(singleton(singleton(esk10_0)),singleton(powerset(esk7_0)))
| powerset(esk10_0) != powerset(esk7_0) ),
inference(scs_inference,[],[i_0_503,i_0_303,i_0_452,i_0_209,i_0_52,i_0_41,i_0_42,i_0_62,i_0_69,i_0_40]) ).
cnf(i_0_600,plain,
( in(X1,X2)
| ~ subset(singleton(X1),X2) ),
inference(rename_variables,[],[i_0_40]) ).
cnf(i_0_601,plain,
( powerset(esk10_0) != powerset(esk7_0)
| powerset(esk7_0) != union(X1)
| in(esk4_3(X1,powerset(esk7_0),esk3_2(singleton(esk7_0),singleton(esk8_0))),X1) ),
inference(scs_inference,[],[i_0_503,i_0_303,i_0_458,i_0_452,i_0_209,i_0_52,i_0_41,i_0_42,i_0_62,i_0_69,i_0_40,i_0_26]) ).
cnf(i_0_602,plain,
subset(esk6_2(powerset(esk10_0),esk10_0),esk10_0),
inference(equality_inference,[],[592]) ).
cnf(i_0_603,plain,
$false,
inference(scs_inference,[],[i_0_602,i_0_189,i_0_290,i_0_38]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.07 % Problem : SEU164+3 : TPTP v9.2.1. Bugfixed v4.0.0.
% 0.00/0.07 % 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.07/0.25 % Computer : n024.cluster.edu
% 0.07/0.25 % Model : x86_64 x86_64
% 0.07/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.25 % Memory : 8042.1875MB
% 0.07/0.25 % OS : Linux 3.10.0-693.el7.x86_64
% 0.07/0.25 % CPULimit : 300
% 0.07/0.25 % WCLimit : 300
% 0.07/0.25 % DateTime : Mon May 4 21:45:57 EDT 2026
% 0.07/0.25 % CPUTime :
% 0.07/0.26 % start to proof: theBenchmark
% 50.17/25.55 % Version : CSE_E---1.7
% 50.17/25.55 % Problem : theBenchmark.p
% 50.17/25.55 % SZS status Theorem for theBenchmark.p
% 50.17/25.55 % SZS output start CNFRefutation
% See solution above
% 51.53/26.20 % Total time : 25.289s
%------------------------------------------------------------------------------