%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SET065+1 : TPTP v9.2.1. Bugfixed v5.4.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 : n022.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:07:07 PM UTC 2026
% Result : Theorem 0.40s 1.61s
% Output : CNFRefutation 0.84s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named c_0_53)
% Comments :
%------------------------------------------------------------------------------
fof(image_defn,axiom,
! [X1,X6] : image(X6,X1) = range_of(restrict(X6,X1,universal_class)),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',image_defn) ).
fof(range_of_defn,axiom,
! [X5] : range_of(X5) = domain_of(inverse(X5)),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',range_of_defn) ).
fof(inverse_defn,axiom,
! [X2] : inverse(X2) = domain_of(flip(cross_product(X2,universal_class))),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',inverse_defn) ).
fof(ordered_pair_defn,axiom,
! [X1,X2] : ordered_pair(X1,X2) = unordered_pair(singleton(X1),unordered_pair(X1,singleton(X2))),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',ordered_pair_defn) ).
fof(singleton_set_defn,axiom,
! [X1] : singleton(X1) = unordered_pair(X1,X1),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',singleton_set_defn) ).
fof(apply_defn,axiom,
! [X9,X2] : apply(X9,X2) = sum_class(image(X9,singleton(X2))),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',apply_defn) ).
fof(successor_defn,axiom,
! [X1] : successor(X1) = union(X1,singleton(X1)),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',successor_defn) ).
fof(compose_defn2,axiom,
! [X6,X8,X3,X4] :
( member(ordered_pair(X3,X4),compose(X8,X6))
<=> ( member(X3,universal_class)
& member(X4,image(X8,image(X6,singleton(X3)))) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',compose_defn2) ).
fof(restrict_defn,axiom,
! [X1,X6,X2] : restrict(X6,X1,X2) = intersection(X6,cross_product(X1,X2)),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',restrict_defn) ).
fof(flip_defn,axiom,
! [X3,X4,X7,X1] :
( member(ordered_pair(ordered_pair(X3,X4),X7),flip(X1))
<=> ( member(ordered_pair(ordered_pair(X3,X4),X7),cross_product(cross_product(universal_class,universal_class),universal_class))
& member(ordered_pair(ordered_pair(X4,X3),X7),X1) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',flip_defn) ).
fof(rotate_defn,axiom,
! [X1,X3,X4,X7] :
( member(ordered_pair(ordered_pair(X3,X4),X7),rotate(X1))
<=> ( member(ordered_pair(ordered_pair(X3,X4),X7),cross_product(cross_product(universal_class,universal_class),universal_class))
& member(ordered_pair(ordered_pair(X4,X7),X3),X1) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',rotate_defn) ).
fof(choice,axiom,
? [X9] :
( function(X9)
& ! [X2] :
( member(X2,universal_class)
=> ( X2 = null_class
| member(apply(X9,X2),X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',choice) ).
fof(inductive_defn,axiom,
! [X1] :
( inductive(X1)
<=> ( member(null_class,X1)
& subclass(image(successor_relation,X1),X1) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',inductive_defn) ).
fof(replacement,axiom,
! [X1,X9] :
( ( member(X1,universal_class)
& function(X9) )
=> member(image(X9,X1),universal_class) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',replacement) ).
fof(function_defn,axiom,
! [X9] :
( function(X9)
<=> ( subclass(X9,cross_product(universal_class,universal_class))
& subclass(compose(X9,inverse(X9)),identity_relation) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',function_defn) ).
fof(cross_product_defn,axiom,
! [X3,X4,X1,X2] :
( member(ordered_pair(X3,X4),cross_product(X1,X2))
<=> ( member(X3,X1)
& member(X4,X2) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',cross_product_defn) ).
fof(successor_relation_defn2,axiom,
! [X1,X2] :
( member(ordered_pair(X1,X2),successor_relation)
<=> ( member(X1,universal_class)
& member(X2,universal_class)
& successor(X1) = X2 ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',successor_relation_defn2) ).
fof(element_relation_defn,axiom,
! [X1,X2] :
( member(ordered_pair(X1,X2),element_relation)
<=> ( member(X2,universal_class)
& member(X1,X2) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',element_relation_defn) ).
fof(first_second,axiom,
! [X1,X2] :
( ( member(X1,universal_class)
& member(X2,universal_class) )
=> ( first(ordered_pair(X1,X2)) = X1
& second(ordered_pair(X1,X2)) = X2 ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',first_second) ).
fof(cross_product,axiom,
! [X1,X2,X5] :
( member(X5,cross_product(X1,X2))
=> X5 = ordered_pair(first(X5),second(X5)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',cross_product) ).
fof(identity_relation,axiom,
! [X5] :
( member(X5,identity_relation)
<=> ? [X1] :
( member(X1,universal_class)
& X5 = ordered_pair(X1,X1) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',identity_relation) ).
fof(domain_of,axiom,
! [X1,X5] :
( member(X5,domain_of(X1))
<=> ( member(X5,universal_class)
& restrict(X1,singleton(X5),universal_class) != null_class ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',domain_of) ).
fof(complement,axiom,
! [X1,X5] :
( member(X5,complement(X1))
<=> ( member(X5,universal_class)
& ~ member(X5,X1) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',complement) ).
fof(null_class_defn,axiom,
! [X1] : ~ member(X1,null_class),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',null_class_defn) ).
fof(union_defn,axiom,
! [X1,X2,X5] :
( member(X5,union(X1,X2))
<=> ( member(X5,X1)
| member(X5,X2) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',union_defn) ).
fof(intersection,axiom,
! [X1,X2,X5] :
( member(X5,intersection(X1,X2))
<=> ( member(X5,X1)
& member(X5,X2) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',intersection) ).
fof(flip,axiom,
! [X1] : subclass(flip(X1),cross_product(cross_product(universal_class,universal_class),universal_class)),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',flip) ).
fof(rotate,axiom,
! [X1] : subclass(rotate(X1),cross_product(cross_product(universal_class,universal_class),universal_class)),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',rotate) ).
fof(subclass_defn,axiom,
! [X1,X2] :
( subclass(X1,X2)
<=> ! [X3] :
( member(X3,X1)
=> member(X3,X2) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',subclass_defn) ).
fof(unordered_pair_defn,axiom,
! [X3,X1,X2] :
( member(X3,unordered_pair(X1,X2))
<=> ( member(X3,universal_class)
& ( X3 = X1
| X3 = X2 ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',unordered_pair_defn) ).
fof(sum_class_defn,axiom,
! [X3,X1] :
( member(X3,sum_class(X1))
<=> ? [X2] :
( member(X3,X2)
& member(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',sum_class_defn) ).
fof(disjoint_defn,axiom,
! [X1,X2] :
( disjoint(X1,X2)
<=> ! [X3] :
~ ( member(X3,X1)
& member(X3,X2) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',disjoint_defn) ).
fof(power_class_defn,axiom,
! [X3,X1] :
( member(X3,power_class(X1))
<=> ( member(X3,universal_class)
& subclass(X3,X1) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',power_class_defn) ).
fof(compose_defn1,axiom,
! [X6,X8] : subclass(compose(X8,X6),cross_product(universal_class,universal_class)),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',compose_defn1) ).
fof(extensionality,axiom,
! [X1,X2] :
( X1 = X2
<=> ( subclass(X1,X2)
& subclass(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',extensionality) ).
fof(power_class,axiom,
! [X3] :
( member(X3,universal_class)
=> member(power_class(X3),universal_class) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',power_class) ).
fof(sum_class,axiom,
! [X1] :
( member(X1,universal_class)
=> member(sum_class(X1),universal_class) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',sum_class) ).
fof(unordered_pair,axiom,
! [X1,X2] : member(unordered_pair(X1,X2),universal_class),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',unordered_pair) ).
fof(regularity,axiom,
! [X1] :
( X1 != null_class
=> ? [X3] :
( member(X3,universal_class)
& member(X3,X1)
& disjoint(X3,X1) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',regularity) ).
fof(infinity,axiom,
? [X1] :
( member(X1,universal_class)
& inductive(X1)
& ! [X2] :
( inductive(X2)
=> subclass(X1,X2) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',infinity) ).
fof(null_class_is_a_set,conjecture,
member(null_class,universal_class),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',null_class_is_a_set) ).
fof(class_elements_are_sets,axiom,
! [X1] : subclass(X1,universal_class),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',class_elements_are_sets) ).
fof(successor_relation_defn1,axiom,
subclass(successor_relation,cross_product(universal_class,universal_class)),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',successor_relation_defn1) ).
fof(element_relation,axiom,
subclass(element_relation,cross_product(universal_class,universal_class)),
file('/export/starexec/sandbox2/benchmark/Axioms/SET005+0.ax',element_relation) ).
fof(i_0_44,plain,
! [X153,X154] : image(X154,X153) = range_of(restrict(X154,X153,universal_class)),
inference(variable_rename,[status(thm)],[image_defn]) ).
fof(i_0_45,plain,
! [X152] : range_of(X152) = domain_of(inverse(X152)),
inference(variable_rename,[status(thm)],[range_of_defn]) ).
fof(i_0_46,plain,
! [X151] : inverse(X151) = domain_of(flip(cross_product(X151,universal_class))),
inference(variable_rename,[status(thm)],[inverse_defn]) ).
fof(i_0_47,plain,
! [X111,X112] : ordered_pair(X111,X112) = unordered_pair(singleton(X111),unordered_pair(X111,singleton(X112))),
inference(variable_rename,[status(thm)],[ordered_pair_defn]) ).
fof(i_0_48,plain,
! [X110] : singleton(X110) = unordered_pair(X110,X110),
inference(variable_rename,[status(thm)],[singleton_set_defn]) ).
fof(i_0_49,plain,
! [X189,X190] : apply(X189,X190) = sum_class(image(X189,singleton(X190))),
inference(variable_rename,[status(thm)],[apply_defn]) ).
fof(i_0_50,plain,
! [X148] : successor(X148) = union(X148,singleton(X148)),
inference(variable_rename,[status(thm)],[successor_defn]) ).
fof(i_0_51,plain,
! [X170,X171,X172,X173] :
( ( member(X172,universal_class)
| ~ member(ordered_pair(X172,X173),compose(X171,X170)) )
& ( member(X173,image(X171,image(X170,singleton(X172))))
| ~ member(ordered_pair(X172,X173),compose(X171,X170)) )
& ( ~ member(X172,universal_class)
| ~ member(X173,image(X171,image(X170,singleton(X172))))
| member(ordered_pair(X172,X173),compose(X171,X170)) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[compose_defn2])])]) ).
cnf(i_0_52,plain,
image(X1,X2) = range_of(restrict(X1,X2,universal_class)),
inference(split_conjunct,[status(thm)],[i_0_44]) ).
cnf(i_0_53,plain,
range_of(X1) = domain_of(inverse(X1)),
inference(split_conjunct,[status(thm)],[i_0_45]) ).
cnf(i_0_54,plain,
inverse(X1) = domain_of(flip(cross_product(X1,universal_class))),
inference(split_conjunct,[status(thm)],[i_0_46]) ).
fof(i_0_55,plain,
! [X129,X130,X131] : restrict(X130,X129,X131) = intersection(X130,cross_product(X129,X131)),
inference(variable_rename,[status(thm)],[restrict_defn]) ).
cnf(i_0_56,plain,
ordered_pair(X1,X2) = unordered_pair(singleton(X1),unordered_pair(X1,singleton(X2))),
inference(split_conjunct,[status(thm)],[i_0_47]) ).
cnf(i_0_57,plain,
singleton(X1) = unordered_pair(X1,X1),
inference(split_conjunct,[status(thm)],[i_0_48]) ).
fof(i_0_58,plain,
! [X140,X141,X142,X143] :
( ( member(ordered_pair(ordered_pair(X140,X141),X142),cross_product(cross_product(universal_class,universal_class),universal_class))
| ~ member(ordered_pair(ordered_pair(X140,X141),X142),flip(X143)) )
& ( member(ordered_pair(ordered_pair(X141,X140),X142),X143)
| ~ member(ordered_pair(ordered_pair(X140,X141),X142),flip(X143)) )
& ( ~ member(ordered_pair(ordered_pair(X140,X141),X142),cross_product(cross_product(universal_class,universal_class),universal_class))
| ~ member(ordered_pair(ordered_pair(X141,X140),X142),X143)
| member(ordered_pair(ordered_pair(X140,X141),X142),flip(X143)) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[flip_defn])])]) ).
fof(i_0_59,plain,
! [X135,X136,X137,X138] :
( ( member(ordered_pair(ordered_pair(X136,X137),X138),cross_product(cross_product(universal_class,universal_class),universal_class))
| ~ member(ordered_pair(ordered_pair(X136,X137),X138),rotate(X135)) )
& ( member(ordered_pair(ordered_pair(X137,X138),X136),X135)
| ~ member(ordered_pair(ordered_pair(X136,X137),X138),rotate(X135)) )
& ( ~ member(ordered_pair(ordered_pair(X136,X137),X138),cross_product(cross_product(universal_class,universal_class),universal_class))
| ~ member(ordered_pair(ordered_pair(X137,X138),X136),X135)
| member(ordered_pair(ordered_pair(X136,X137),X138),rotate(X135)) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[rotate_defn])])]) ).
fof(i_0_60,plain,
! [X192] :
( function(esk7_0)
& ( ~ member(X192,universal_class)
| X192 = null_class
| member(apply(esk7_0,X192),X192) ) ),
inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[choice])])])]) ).
cnf(i_0_61,plain,
apply(X1,X2) = sum_class(image(X1,singleton(X2))),
inference(split_conjunct,[status(thm)],[i_0_49]) ).
fof(i_0_62,plain,
! [X155] :
( ( member(null_class,X155)
| ~ inductive(X155) )
& ( subclass(image(successor_relation,X155),X155)
| ~ inductive(X155) )
& ( ~ member(null_class,X155)
| ~ subclass(image(successor_relation,X155),X155)
| inductive(X155) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inductive_defn])])]) ).
fof(i_0_63,plain,
! [X179,X180] :
( ~ member(X179,universal_class)
| ~ function(X180)
| member(image(X180,X179),universal_class) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[replacement])]) ).
fof(i_0_64,plain,
! [X178] :
( ( subclass(X178,cross_product(universal_class,universal_class))
| ~ function(X178) )
& ( subclass(compose(X178,inverse(X178)),identity_relation)
| ~ function(X178) )
& ( ~ subclass(X178,cross_product(universal_class,universal_class))
| ~ subclass(compose(X178,inverse(X178)),identity_relation)
| function(X178) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[function_defn])])]) ).
fof(i_0_65,plain,
! [X113,X114,X115,X116] :
( ( member(X113,X115)
| ~ member(ordered_pair(X113,X114),cross_product(X115,X116)) )
& ( member(X114,X116)
| ~ member(ordered_pair(X113,X114),cross_product(X115,X116)) )
& ( ~ member(X113,X115)
| ~ member(X114,X116)
| member(ordered_pair(X113,X114),cross_product(X115,X116)) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[cross_product_defn])])]) ).
fof(i_0_66,plain,
! [X149,X150] :
( ( member(X149,universal_class)
| ~ member(ordered_pair(X149,X150),successor_relation) )
& ( member(X150,universal_class)
| ~ member(ordered_pair(X149,X150),successor_relation) )
& ( successor(X149) = X150
| ~ member(ordered_pair(X149,X150),successor_relation) )
& ( ~ member(X149,universal_class)
| ~ member(X150,universal_class)
| successor(X149) != X150
| member(ordered_pair(X149,X150),successor_relation) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[successor_relation_defn2])])]) ).
cnf(i_0_67,plain,
successor(X1) = union(X1,singleton(X1)),
inference(split_conjunct,[status(thm)],[i_0_50]) ).
fof(i_0_68,plain,
! [X122,X123] :
( ( member(X123,universal_class)
| ~ member(ordered_pair(X122,X123),element_relation) )
& ( member(X122,X123)
| ~ member(ordered_pair(X122,X123),element_relation) )
& ( ~ member(X123,universal_class)
| ~ member(X122,X123)
| member(ordered_pair(X122,X123),element_relation) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[element_relation_defn])])]) ).
fof(i_0_69,plain,
! [X117,X118] :
( ( first(ordered_pair(X117,X118)) = X117
| ~ member(X117,universal_class)
| ~ member(X118,universal_class) )
& ( second(ordered_pair(X117,X118)) = X118
| ~ member(X117,universal_class)
| ~ member(X118,universal_class) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[first_second])])]) ).
fof(i_0_70,plain,
! [X119,X120,X121] :
( ~ member(X121,cross_product(X119,X120))
| X121 = ordered_pair(first(X121),second(X121)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[cross_product])]) ).
fof(i_0_71,plain,
! [X174,X176,X177] :
( ( member(esk4_1(X174),universal_class)
| ~ member(X174,identity_relation) )
& ( X174 = ordered_pair(esk4_1(X174),esk4_1(X174))
| ~ member(X174,identity_relation) )
& ( ~ member(X177,universal_class)
| X176 != ordered_pair(X177,X177)
| member(X176,identity_relation) ) ),
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)],[identity_relation])])])])])]) ).
fof(i_0_72,plain,
! [X133,X134] :
( ( member(X134,universal_class)
| ~ member(X134,domain_of(X133)) )
& ( restrict(X133,singleton(X134),universal_class) != null_class
| ~ member(X134,domain_of(X133)) )
& ( ~ member(X134,universal_class)
| restrict(X133,singleton(X134),universal_class) = null_class
| member(X134,domain_of(X133)) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[domain_of])])]) ).
fof(i_0_73,plain,
! [X1,X5] :
( member(X5,complement(X1))
<=> ( member(X5,universal_class)
& ~ member(X5,X1) ) ),
inference(fof_simplification,[status(thm)],[complement]) ).
fof(i_0_74,plain,
! [X1] : ~ member(X1,null_class),
inference(fof_simplification,[status(thm)],[null_class_defn]) ).
cnf(i_0_75,plain,
( member(ordered_pair(X1,X2),compose(X3,X4))
| ~ member(X1,universal_class)
| ~ member(X2,image(X3,image(X4,singleton(X1)))) ),
inference(split_conjunct,[status(thm)],[i_0_51]) ).
cnf(i_0_76,plain,
image(X1,X2) = domain_of(domain_of(flip(cross_product(restrict(X1,X2,universal_class),universal_class)))),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_52,c_0_53]),c_0_54]) ).
cnf(i_0_77,plain,
restrict(X1,X2,X3) = intersection(X1,cross_product(X2,X3)),
inference(split_conjunct,[status(thm)],[i_0_55]) ).
cnf(i_0_78,plain,
ordered_pair(X1,X2) = unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_56,c_0_57]),c_0_57]) ).
cnf(i_0_79,plain,
( member(X1,image(X2,image(X3,singleton(X4))))
| ~ member(ordered_pair(X4,X1),compose(X2,X3)) ),
inference(split_conjunct,[status(thm)],[i_0_51]) ).
cnf(i_0_80,plain,
( member(ordered_pair(ordered_pair(X1,X2),X3),flip(X4))
| ~ member(ordered_pair(ordered_pair(X1,X2),X3),cross_product(cross_product(universal_class,universal_class),universal_class))
| ~ member(ordered_pair(ordered_pair(X2,X1),X3),X4) ),
inference(split_conjunct,[status(thm)],[i_0_58]) ).
cnf(i_0_81,plain,
( member(ordered_pair(ordered_pair(X1,X2),X3),rotate(X4))
| ~ member(ordered_pair(ordered_pair(X1,X2),X3),cross_product(cross_product(universal_class,universal_class),universal_class))
| ~ member(ordered_pair(ordered_pair(X2,X3),X1),X4) ),
inference(split_conjunct,[status(thm)],[i_0_59]) ).
cnf(i_0_82,plain,
( member(ordered_pair(ordered_pair(X1,X2),X3),cross_product(cross_product(universal_class,universal_class),universal_class))
| ~ member(ordered_pair(ordered_pair(X1,X2),X3),flip(X4)) ),
inference(split_conjunct,[status(thm)],[i_0_58]) ).
cnf(i_0_83,plain,
( member(ordered_pair(ordered_pair(X1,X2),X3),cross_product(cross_product(universal_class,universal_class),universal_class))
| ~ member(ordered_pair(ordered_pair(X1,X2),X3),rotate(X4)) ),
inference(split_conjunct,[status(thm)],[i_0_59]) ).
cnf(i_0_84,plain,
( member(ordered_pair(ordered_pair(X1,X2),X3),X4)
| ~ member(ordered_pair(ordered_pair(X2,X1),X3),flip(X4)) ),
inference(split_conjunct,[status(thm)],[i_0_58]) ).
cnf(i_0_85,plain,
( member(ordered_pair(ordered_pair(X1,X2),X3),X4)
| ~ member(ordered_pair(ordered_pair(X3,X1),X2),rotate(X4)) ),
inference(split_conjunct,[status(thm)],[i_0_59]) ).
cnf(i_0_86,plain,
( X1 = null_class
| member(apply(esk7_0,X1),X1)
| ~ member(X1,universal_class) ),
inference(split_conjunct,[status(thm)],[i_0_60]) ).
cnf(i_0_87,plain,
apply(X1,X2) = sum_class(image(X1,unordered_pair(X2,X2))),
inference(rw,[status(thm)],[i_0_61,c_0_57]) ).
cnf(i_0_88,plain,
( inductive(X1)
| ~ member(null_class,X1)
| ~ subclass(image(successor_relation,X1),X1) ),
inference(split_conjunct,[status(thm)],[i_0_62]) ).
cnf(i_0_89,plain,
( member(image(X2,X1),universal_class)
| ~ member(X1,universal_class)
| ~ function(X2) ),
inference(split_conjunct,[status(thm)],[i_0_63]) ).
cnf(i_0_90,plain,
( subclass(image(successor_relation,X1),X1)
| ~ inductive(X1) ),
inference(split_conjunct,[status(thm)],[i_0_62]) ).
cnf(i_0_91,plain,
( function(X1)
| ~ subclass(X1,cross_product(universal_class,universal_class))
| ~ subclass(compose(X1,inverse(X1)),identity_relation) ),
inference(split_conjunct,[status(thm)],[i_0_64]) ).
cnf(i_0_92,plain,
( member(X1,X2)
| ~ member(ordered_pair(X1,X3),cross_product(X2,X4)) ),
inference(split_conjunct,[status(thm)],[i_0_65]) ).
cnf(i_0_93,plain,
( member(X1,X2)
| ~ member(ordered_pair(X3,X1),cross_product(X4,X2)) ),
inference(split_conjunct,[status(thm)],[i_0_65]) ).
cnf(i_0_94,plain,
( member(X1,universal_class)
| ~ member(ordered_pair(X1,X2),compose(X3,X4)) ),
inference(split_conjunct,[status(thm)],[i_0_51]) ).
cnf(i_0_95,plain,
( successor(X1) = X2
| ~ member(ordered_pair(X1,X2),successor_relation) ),
inference(split_conjunct,[status(thm)],[i_0_66]) ).
cnf(i_0_96,plain,
successor(X1) = union(X1,unordered_pair(X1,X1)),
inference(rw,[status(thm)],[i_0_67,c_0_57]) ).
cnf(i_0_97,plain,
( member(X1,X2)
| ~ member(ordered_pair(X1,X2),element_relation) ),
inference(split_conjunct,[status(thm)],[i_0_68]) ).
cnf(i_0_98,plain,
( member(X1,universal_class)
| ~ member(ordered_pair(X1,X2),successor_relation) ),
inference(split_conjunct,[status(thm)],[i_0_66]) ).
cnf(i_0_99,plain,
( member(X1,universal_class)
| ~ member(ordered_pair(X2,X1),successor_relation) ),
inference(split_conjunct,[status(thm)],[i_0_66]) ).
cnf(i_0_100,plain,
( member(X1,universal_class)
| ~ member(ordered_pair(X2,X1),element_relation) ),
inference(split_conjunct,[status(thm)],[i_0_68]) ).
cnf(i_0_101,plain,
( member(ordered_pair(X1,X2),successor_relation)
| ~ member(X1,universal_class)
| ~ member(X2,universal_class)
| successor(X1) != X2 ),
inference(split_conjunct,[status(thm)],[i_0_66]) ).
cnf(i_0_102,plain,
( member(ordered_pair(X1,X3),cross_product(X2,X4))
| ~ member(X1,X2)
| ~ member(X3,X4) ),
inference(split_conjunct,[status(thm)],[i_0_65]) ).
cnf(i_0_103,plain,
( member(ordered_pair(X2,X1),element_relation)
| ~ member(X1,universal_class)
| ~ member(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_68]) ).
cnf(i_0_104,plain,
( second(ordered_pair(X1,X2)) = X2
| ~ member(X1,universal_class)
| ~ member(X2,universal_class) ),
inference(split_conjunct,[status(thm)],[i_0_69]) ).
cnf(i_0_105,plain,
( first(ordered_pair(X1,X2)) = X1
| ~ member(X1,universal_class)
| ~ member(X2,universal_class) ),
inference(split_conjunct,[status(thm)],[i_0_69]) ).
cnf(i_0_106,plain,
( X1 = ordered_pair(first(X1),second(X1))
| ~ member(X1,cross_product(X2,X3)) ),
inference(split_conjunct,[status(thm)],[i_0_70]) ).
cnf(i_0_107,plain,
( subclass(compose(X1,inverse(X1)),identity_relation)
| ~ function(X1) ),
inference(split_conjunct,[status(thm)],[i_0_64]) ).
cnf(i_0_108,plain,
( X1 = ordered_pair(esk4_1(X1),esk4_1(X1))
| ~ member(X1,identity_relation) ),
inference(split_conjunct,[status(thm)],[i_0_71]) ).
cnf(i_0_109,plain,
( member(X2,identity_relation)
| ~ member(X1,universal_class)
| X2 != ordered_pair(X1,X1) ),
inference(split_conjunct,[status(thm)],[i_0_71]) ).
cnf(i_0_110,plain,
( restrict(X1,singleton(X2),universal_class) != null_class
| ~ member(X2,domain_of(X1)) ),
inference(split_conjunct,[status(thm)],[i_0_72]) ).
cnf(i_0_111,plain,
( restrict(X2,singleton(X1),universal_class) = null_class
| member(X1,domain_of(X2))
| ~ member(X1,universal_class) ),
inference(split_conjunct,[status(thm)],[i_0_72]) ).
fof(i_0_112,plain,
! [X145,X146,X147] :
( ( ~ member(X147,union(X145,X146))
| member(X147,X145)
| member(X147,X146) )
& ( ~ member(X147,X145)
| member(X147,union(X145,X146)) )
& ( ~ member(X147,X146)
| member(X147,union(X145,X146)) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[union_defn])])]) ).
fof(i_0_113,plain,
! [X124,X125,X126] :
( ( member(X126,X124)
| ~ member(X126,intersection(X124,X125)) )
& ( member(X126,X125)
| ~ member(X126,intersection(X124,X125)) )
& ( ~ member(X126,X124)
| ~ member(X126,X125)
| member(X126,intersection(X124,X125)) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[intersection])])]) ).
fof(i_0_114,plain,
! [X144] : subclass(flip(X144),cross_product(cross_product(universal_class,universal_class),universal_class)),
inference(variable_rename,[status(thm)],[flip]) ).
fof(i_0_115,plain,
! [X139] : subclass(rotate(X139),cross_product(cross_product(universal_class,universal_class),universal_class)),
inference(variable_rename,[status(thm)],[rotate]) ).
fof(i_0_116,plain,
! [X96,X97,X98,X99,X100] :
( ( ~ subclass(X96,X97)
| ~ member(X98,X96)
| member(X98,X97) )
& ( member(esk1_2(X99,X100),X99)
| subclass(X99,X100) )
& ( ~ member(esk1_2(X99,X100),X100)
| subclass(X99,X100) ) ),
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)],[subclass_defn])])])])])]) ).
fof(i_0_117,plain,
! [X105,X106,X107] :
( ( member(X105,universal_class)
| ~ member(X105,unordered_pair(X106,X107)) )
& ( X105 = X106
| X105 = X107
| ~ member(X105,unordered_pair(X106,X107)) )
& ( X105 != X106
| ~ member(X105,universal_class)
| member(X105,unordered_pair(X106,X107)) )
& ( X105 != X107
| ~ member(X105,universal_class)
| member(X105,unordered_pair(X106,X107)) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[unordered_pair_defn])])]) ).
fof(i_0_118,plain,
! [X158,X159,X161,X162,X163] :
( ( member(X158,esk3_2(X158,X159))
| ~ member(X158,sum_class(X159)) )
& ( member(esk3_2(X158,X159),X159)
| ~ member(X158,sum_class(X159)) )
& ( ~ member(X161,X163)
| ~ member(X163,X162)
| member(X161,sum_class(X162)) ) ),
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)],[sum_class_defn])])])])])]) ).
fof(i_0_119,plain,
! [X181,X182,X183,X184,X185] :
( ( ~ disjoint(X181,X182)
| ~ member(X183,X181)
| ~ member(X183,X182) )
& ( member(esk5_2(X184,X185),X184)
| disjoint(X184,X185) )
& ( member(esk5_2(X184,X185),X185)
| disjoint(X184,X185) ) ),
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)],[disjoint_defn])])])])])]) ).
fof(i_0_120,plain,
! [X165,X166] :
( ( member(X165,universal_class)
| ~ member(X165,power_class(X166)) )
& ( subclass(X165,X166)
| ~ member(X165,power_class(X166)) )
& ( ~ member(X165,universal_class)
| ~ subclass(X165,X166)
| member(X165,power_class(X166)) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[power_class_defn])])]) ).
fof(i_0_121,plain,
! [X168,X169] : subclass(compose(X169,X168),cross_product(universal_class,universal_class)),
inference(variable_rename,[status(thm)],[compose_defn1]) ).
fof(i_0_122,plain,
! [X127,X128] :
( ( member(X128,universal_class)
| ~ member(X128,complement(X127)) )
& ( ~ member(X128,X127)
| ~ member(X128,complement(X127)) )
& ( ~ member(X128,universal_class)
| member(X128,X127)
| member(X128,complement(X127)) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_73])])]) ).
fof(i_0_123,plain,
! [X103,X104] :
( ( subclass(X103,X104)
| X103 != X104 )
& ( subclass(X104,X103)
| X103 != X104 )
& ( ~ subclass(X103,X104)
| ~ subclass(X104,X103)
| X103 = X104 ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[extensionality])])]) ).
fof(i_0_124,plain,
! [X167] :
( ~ member(X167,universal_class)
| member(power_class(X167),universal_class) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[power_class])]) ).
fof(i_0_125,plain,
! [X164] :
( ~ member(X164,universal_class)
| member(sum_class(X164),universal_class) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sum_class])]) ).
fof(i_0_126,plain,
! [X108,X109] : member(unordered_pair(X108,X109),universal_class),
inference(variable_rename,[status(thm)],[unordered_pair]) ).
fof(i_0_127,plain,
! [X187] :
( ( member(esk6_1(X187),universal_class)
| X187 = null_class )
& ( member(esk6_1(X187),X187)
| X187 = null_class )
& ( disjoint(esk6_1(X187),X187)
| X187 = null_class ) ),
inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[regularity])])])]) ).
fof(i_0_128,plain,
! [X132] : ~ member(X132,null_class),
inference(variable_rename,[status(thm)],[i_0_74]) ).
fof(i_0_129,plain,
! [X157] :
( member(esk2_0,universal_class)
& inductive(esk2_0)
& ( ~ inductive(X157)
| subclass(esk2_0,X157) ) ),
inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[infinity])])])]) ).
fof(i_0_130,negated_conjecture,
~ member(null_class,universal_class),
inference(fof_simplification,[status(thm)],[inference(assume_negation,[status(cth)],[null_class_is_a_set])]) ).
fof(i_0_131,plain,
! [X102] : subclass(X102,universal_class),
inference(variable_rename,[status(thm)],[class_elements_are_sets]) ).
cnf(i_0_132,plain,
( member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),compose(X3,X4))
| ~ member(X1,universal_class)
| ~ member(X2,domain_of(domain_of(flip(cross_product(intersection(X3,cross_product(domain_of(domain_of(flip(cross_product(intersection(X4,cross_product(unordered_pair(X1,X1),universal_class)),universal_class)))),universal_class)),universal_class))))) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_75,c_0_57]),c_0_76]),c_0_76]),c_0_77]),c_0_77]),c_0_78]),
[final] ).
cnf(i_0_133,plain,
( member(X1,domain_of(domain_of(flip(cross_product(intersection(X2,cross_product(domain_of(domain_of(flip(cross_product(intersection(X3,cross_product(unordered_pair(X4,X4),universal_class)),universal_class)))),universal_class)),universal_class)))))
| ~ member(unordered_pair(unordered_pair(X4,X4),unordered_pair(X4,unordered_pair(X1,X1))),compose(X2,X3)) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_79,c_0_57]),c_0_76]),c_0_76]),c_0_77]),c_0_77]),c_0_78]),
[final] ).
cnf(i_0_134,plain,
( member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2)))),unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),unordered_pair(X3,X3))),flip(X4))
| ~ member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X1,X1))),unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X1,X1)))),unordered_pair(unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X1,X1))),unordered_pair(X3,X3))),X4)
| ~ member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2)))),unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),unordered_pair(X3,X3))),cross_product(cross_product(universal_class,universal_class),universal_class)) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_80,c_0_78]),c_0_78]),c_0_78]),c_0_78]),c_0_78]),c_0_78]),
[final] ).
cnf(i_0_135,plain,
( member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2)))),unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),unordered_pair(X3,X3))),rotate(X4))
| ~ member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X3,X3))),unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X3,X3)))),unordered_pair(unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X3,X3))),unordered_pair(X1,X1))),X4)
| ~ member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2)))),unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),unordered_pair(X3,X3))),cross_product(cross_product(universal_class,universal_class),universal_class)) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_81,c_0_78]),c_0_78]),c_0_78]),c_0_78]),c_0_78]),c_0_78]),
[final] ).
cnf(i_0_136,plain,
( member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2)))),unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),unordered_pair(X3,X3))),cross_product(cross_product(universal_class,universal_class),universal_class))
| ~ member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2)))),unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),unordered_pair(X3,X3))),flip(X4)) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_82,c_0_78]),c_0_78]),c_0_78]),c_0_78]),
[final] ).
cnf(i_0_137,plain,
( member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2)))),unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),unordered_pair(X3,X3))),cross_product(cross_product(universal_class,universal_class),universal_class))
| ~ member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2)))),unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),unordered_pair(X3,X3))),rotate(X4)) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_83,c_0_78]),c_0_78]),c_0_78]),c_0_78]),
[final] ).
cnf(i_0_138,plain,
( member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2)))),unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),unordered_pair(X3,X3))),X4)
| ~ member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X1,X1))),unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X1,X1)))),unordered_pair(unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X1,X1))),unordered_pair(X3,X3))),flip(X4)) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_84,c_0_78]),c_0_78]),c_0_78]),c_0_78]),
[final] ).
cnf(i_0_139,plain,
( member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2)))),unordered_pair(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),unordered_pair(X3,X3))),X4)
| ~ member(unordered_pair(unordered_pair(unordered_pair(unordered_pair(X3,X3),unordered_pair(X3,unordered_pair(X1,X1))),unordered_pair(unordered_pair(X3,X3),unordered_pair(X3,unordered_pair(X1,X1)))),unordered_pair(unordered_pair(unordered_pair(X3,X3),unordered_pair(X3,unordered_pair(X1,X1))),unordered_pair(X2,X2))),rotate(X4)) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_85,c_0_78]),c_0_78]),c_0_78]),c_0_78]),
[final] ).
cnf(i_0_140,plain,
( X1 = null_class
| member(sum_class(domain_of(domain_of(flip(cross_product(intersection(esk7_0,cross_product(unordered_pair(X1,X1),universal_class)),universal_class))))),X1)
| ~ member(X1,universal_class) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_86,c_0_87]),c_0_76]),c_0_77]),
[final] ).
cnf(i_0_141,plain,
( inductive(X1)
| ~ member(null_class,X1)
| ~ subclass(domain_of(domain_of(flip(cross_product(intersection(successor_relation,cross_product(X1,universal_class)),universal_class)))),X1) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_88,c_0_76]),c_0_77]),
[final] ).
cnf(i_0_142,plain,
( member(domain_of(domain_of(flip(cross_product(intersection(X2,cross_product(X1,universal_class)),universal_class)))),universal_class)
| ~ function(X2)
| ~ member(X1,universal_class) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_89,c_0_76]),c_0_77]),
[final] ).
cnf(i_0_143,plain,
( subclass(domain_of(domain_of(flip(cross_product(intersection(successor_relation,cross_product(X1,universal_class)),universal_class)))),X1)
| ~ inductive(X1) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_90,c_0_76]),c_0_77]),
[final] ).
cnf(i_0_144,plain,
( function(X1)
| ~ subclass(X1,cross_product(universal_class,universal_class))
| ~ subclass(compose(X1,domain_of(flip(cross_product(X1,universal_class)))),identity_relation) ),
inference(rw,[status(thm)],[i_0_91,c_0_54]),
[final] ).
cnf(i_0_145,plain,
( member(X1,X2)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X3,X3))),cross_product(X2,X4)) ),
inference(rw,[status(thm)],[i_0_92,c_0_78]),
[final] ).
cnf(i_0_146,plain,
( member(X1,X2)
| ~ member(unordered_pair(unordered_pair(X3,X3),unordered_pair(X3,unordered_pair(X1,X1))),cross_product(X4,X2)) ),
inference(rw,[status(thm)],[i_0_93,c_0_78]),
[final] ).
cnf(i_0_147,plain,
( member(X1,universal_class)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),compose(X3,X4)) ),
inference(rw,[status(thm)],[i_0_94,c_0_78]),
[final] ).
cnf(i_0_148,plain,
( union(X1,unordered_pair(X1,X1)) = X2
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),successor_relation) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_95,c_0_96]),c_0_78]),
[final] ).
cnf(i_0_149,plain,
( member(X1,X2)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),element_relation) ),
inference(rw,[status(thm)],[i_0_97,c_0_78]),
[final] ).
cnf(i_0_150,plain,
( member(X1,universal_class)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),successor_relation) ),
inference(rw,[status(thm)],[i_0_98,c_0_78]),
[final] ).
cnf(i_0_151,plain,
( member(X1,universal_class)
| ~ member(unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X1,X1))),successor_relation) ),
inference(rw,[status(thm)],[i_0_99,c_0_78]),
[final] ).
cnf(i_0_152,plain,
( member(X1,universal_class)
| ~ member(unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X1,X1))),element_relation) ),
inference(rw,[status(thm)],[i_0_100,c_0_78]),
[final] ).
cnf(i_0_153,plain,
( member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),successor_relation)
| union(X1,unordered_pair(X1,X1)) != X2
| ~ member(X2,universal_class)
| ~ member(X1,universal_class) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_101,c_0_96]),c_0_78]),
[final] ).
cnf(i_0_154,plain,
( member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X3,X3))),cross_product(X2,X4))
| ~ member(X3,X4)
| ~ member(X1,X2) ),
inference(rw,[status(thm)],[i_0_102,c_0_78]),
[final] ).
cnf(i_0_155,plain,
( member(unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X1,X1))),element_relation)
| ~ member(X2,X1)
| ~ member(X1,universal_class) ),
inference(rw,[status(thm)],[i_0_103,c_0_78]),
[final] ).
cnf(i_0_156,plain,
( second(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2)))) = X2
| ~ member(X2,universal_class)
| ~ member(X1,universal_class) ),
inference(rw,[status(thm)],[i_0_104,c_0_78]),
[final] ).
cnf(i_0_157,plain,
( first(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2)))) = X1
| ~ member(X2,universal_class)
| ~ member(X1,universal_class) ),
inference(rw,[status(thm)],[i_0_105,c_0_78]),
[final] ).
cnf(i_0_158,plain,
( X1 = unordered_pair(unordered_pair(first(X1),first(X1)),unordered_pair(first(X1),unordered_pair(second(X1),second(X1))))
| ~ member(X1,cross_product(X2,X3)) ),
inference(rw,[status(thm)],[i_0_106,c_0_78]),
[final] ).
cnf(i_0_159,plain,
( subclass(compose(X1,domain_of(flip(cross_product(X1,universal_class)))),identity_relation)
| ~ function(X1) ),
inference(rw,[status(thm)],[i_0_107,c_0_54]),
[final] ).
cnf(i_0_160,plain,
( X1 = unordered_pair(unordered_pair(esk4_1(X1),esk4_1(X1)),unordered_pair(esk4_1(X1),unordered_pair(esk4_1(X1),esk4_1(X1))))
| ~ member(X1,identity_relation) ),
inference(rw,[status(thm)],[i_0_108,c_0_78]),
[final] ).
cnf(i_0_161,plain,
( member(X2,identity_relation)
| X2 != unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X1,X1)))
| ~ member(X1,universal_class) ),
inference(rw,[status(thm)],[i_0_109,c_0_78]),
[final] ).
cnf(i_0_162,plain,
( intersection(X1,cross_product(unordered_pair(X2,X2),universal_class)) != null_class
| ~ member(X2,domain_of(X1)) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_110,c_0_57]),c_0_77]),
[final] ).
cnf(i_0_163,plain,
( intersection(X2,cross_product(unordered_pair(X1,X1),universal_class)) = null_class
| member(X1,domain_of(X2))
| ~ member(X1,universal_class) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_111,c_0_57]),c_0_77]),
[final] ).
cnf(i_0_164,plain,
( member(X1,X2)
| member(X1,X3)
| ~ member(X1,union(X2,X3)) ),
inference(split_conjunct,[status(thm)],[i_0_112]),
[final] ).
cnf(i_0_165,plain,
( member(X1,intersection(X2,X3))
| ~ member(X1,X2)
| ~ member(X1,X3) ),
inference(split_conjunct,[status(thm)],[i_0_113]),
[final] ).
cnf(i_0_166,plain,
subclass(flip(X1),cross_product(cross_product(universal_class,universal_class),universal_class)),
inference(split_conjunct,[status(thm)],[i_0_114]),
[final] ).
cnf(i_0_167,plain,
subclass(rotate(X1),cross_product(cross_product(universal_class,universal_class),universal_class)),
inference(split_conjunct,[status(thm)],[i_0_115]),
[final] ).
cnf(i_0_168,plain,
( subclass(X1,X2)
| ~ member(esk1_2(X1,X2),X2) ),
inference(split_conjunct,[status(thm)],[i_0_116]),
[final] ).
cnf(i_0_169,plain,
( member(X1,X2)
| ~ member(X1,intersection(X2,X3)) ),
inference(split_conjunct,[status(thm)],[i_0_113]),
[final] ).
cnf(i_0_170,plain,
( member(X1,X2)
| ~ member(X1,intersection(X3,X2)) ),
inference(split_conjunct,[status(thm)],[i_0_113]),
[final] ).
cnf(i_0_171,plain,
( member(X1,universal_class)
| ~ member(X1,unordered_pair(X2,X3)) ),
inference(split_conjunct,[status(thm)],[i_0_117]),
[final] ).
cnf(i_0_172,plain,
( member(esk3_2(X1,X2),X2)
| ~ member(X1,sum_class(X2)) ),
inference(split_conjunct,[status(thm)],[i_0_118]),
[final] ).
cnf(i_0_173,plain,
( member(X1,esk3_2(X1,X2))
| ~ member(X1,sum_class(X2)) ),
inference(split_conjunct,[status(thm)],[i_0_118]),
[final] ).
cnf(i_0_174,plain,
( ~ disjoint(X1,X2)
| ~ member(X3,X1)
| ~ member(X3,X2) ),
inference(split_conjunct,[status(thm)],[i_0_119]),
[final] ).
cnf(i_0_175,plain,
( X1 = X2
| X1 = X3
| ~ member(X1,unordered_pair(X2,X3)) ),
inference(split_conjunct,[status(thm)],[i_0_117]),
[final] ).
cnf(i_0_176,plain,
( member(X1,sum_class(X3))
| ~ member(X1,X2)
| ~ member(X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_118]),
[final] ).
cnf(i_0_177,plain,
( member(X1,unordered_pair(X2,X3))
| X1 != X2
| ~ member(X1,universal_class) ),
inference(split_conjunct,[status(thm)],[i_0_117]),
[final] ).
cnf(i_0_178,plain,
( member(X1,unordered_pair(X3,X2))
| X1 != X2
| ~ member(X1,universal_class) ),
inference(split_conjunct,[status(thm)],[i_0_117]),
[final] ).
cnf(i_0_179,plain,
( member(X1,power_class(X2))
| ~ member(X1,universal_class)
| ~ subclass(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_120]),
[final] ).
cnf(i_0_180,plain,
( member(X1,union(X2,X3))
| ~ member(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_112]),
[final] ).
cnf(i_0_181,plain,
( member(X1,union(X3,X2))
| ~ member(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_112]),
[final] ).
cnf(i_0_182,plain,
subclass(compose(X1,X2),cross_product(universal_class,universal_class)),
inference(split_conjunct,[status(thm)],[i_0_121]),
[final] ).
cnf(i_0_183,plain,
( member(X3,X2)
| ~ subclass(X1,X2)
| ~ member(X3,X1) ),
inference(split_conjunct,[status(thm)],[i_0_116]),
[final] ).
cnf(i_0_184,plain,
( member(X1,X2)
| member(X1,complement(X2))
| ~ member(X1,universal_class) ),
inference(split_conjunct,[status(thm)],[i_0_122]),
[final] ).
cnf(i_0_185,plain,
( ~ member(X1,X2)
| ~ member(X1,complement(X2)) ),
inference(split_conjunct,[status(thm)],[i_0_122]),
[final] ).
cnf(i_0_186,plain,
( member(esk5_2(X1,X2),X1)
| disjoint(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_119]),
[final] ).
cnf(i_0_187,plain,
( member(esk5_2(X1,X2),X2)
| disjoint(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_119]),
[final] ).
cnf(i_0_188,plain,
( member(esk1_2(X1,X2),X1)
| subclass(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_116]),
[final] ).
cnf(i_0_189,plain,
( X1 = X2
| ~ subclass(X1,X2)
| ~ subclass(X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_123]),
[final] ).
cnf(i_0_190,plain,
( subclass(X1,X2)
| ~ member(X1,power_class(X2)) ),
inference(split_conjunct,[status(thm)],[i_0_120]),
[final] ).
cnf(i_0_191,plain,
( member(X1,universal_class)
| ~ member(X1,power_class(X2)) ),
inference(split_conjunct,[status(thm)],[i_0_120]),
[final] ).
cnf(i_0_192,plain,
( member(X1,universal_class)
| ~ member(X1,domain_of(X2)) ),
inference(split_conjunct,[status(thm)],[i_0_72]),
[final] ).
cnf(i_0_193,plain,
( member(X1,universal_class)
| ~ member(X1,complement(X2)) ),
inference(split_conjunct,[status(thm)],[i_0_122]),
[final] ).
cnf(i_0_194,plain,
( subclass(X1,cross_product(universal_class,universal_class))
| ~ function(X1) ),
inference(split_conjunct,[status(thm)],[i_0_64]),
[final] ).
cnf(i_0_195,plain,
( member(esk4_1(X1),universal_class)
| ~ member(X1,identity_relation) ),
inference(split_conjunct,[status(thm)],[i_0_71]),
[final] ).
cnf(i_0_196,plain,
( member(power_class(X1),universal_class)
| ~ member(X1,universal_class) ),
inference(split_conjunct,[status(thm)],[i_0_124]),
[final] ).
cnf(i_0_197,plain,
( member(sum_class(X1),universal_class)
| ~ member(X1,universal_class) ),
inference(split_conjunct,[status(thm)],[i_0_125]),
[final] ).
cnf(i_0_198,plain,
member(unordered_pair(X1,X2),universal_class),
inference(split_conjunct,[status(thm)],[i_0_126]),
[final] ).
cnf(i_0_199,plain,
subclass(successor_relation,cross_product(universal_class,universal_class)),
inference(split_conjunct,[status(thm)],[successor_relation_defn1]),
[final] ).
cnf(i_0_200,plain,
subclass(element_relation,cross_product(universal_class,universal_class)),
inference(split_conjunct,[status(thm)],[element_relation]),
[final] ).
cnf(i_0_201,plain,
( disjoint(esk6_1(X1),X1)
| X1 = null_class ),
inference(split_conjunct,[status(thm)],[i_0_127]),
[final] ).
cnf(i_0_202,plain,
( member(esk6_1(X1),X1)
| X1 = null_class ),
inference(split_conjunct,[status(thm)],[i_0_127]),
[final] ).
cnf(i_0_203,plain,
( member(esk6_1(X1),universal_class)
| X1 = null_class ),
inference(split_conjunct,[status(thm)],[i_0_127]),
[final] ).
cnf(i_0_204,plain,
~ member(X1,null_class),
inference(split_conjunct,[status(thm)],[i_0_128]),
[final] ).
cnf(i_0_205,plain,
( member(null_class,X1)
| ~ inductive(X1) ),
inference(split_conjunct,[status(thm)],[i_0_62]),
[final] ).
cnf(i_0_206,plain,
( subclass(esk2_0,X1)
| ~ inductive(X1) ),
inference(split_conjunct,[status(thm)],[i_0_129]),
[final] ).
cnf(i_0_207,plain,
( subclass(X1,X2)
| X1 != X2 ),
inference(split_conjunct,[status(thm)],[i_0_123]),
[final] ).
cnf(i_0_208,plain,
( subclass(X1,X2)
| X2 != X1 ),
inference(split_conjunct,[status(thm)],[i_0_123]),
[final] ).
cnf(i_0_209,negated_conjecture,
~ member(null_class,universal_class),
inference(split_conjunct,[status(thm)],[i_0_130]),
[final] ).
cnf(i_0_210,plain,
subclass(X1,universal_class),
inference(split_conjunct,[status(thm)],[i_0_131]),
[final] ).
cnf(i_0_211,plain,
member(esk2_0,universal_class),
inference(split_conjunct,[status(thm)],[i_0_129]),
[final] ).
cnf(i_0_212,plain,
function(esk7_0),
inference(split_conjunct,[status(thm)],[i_0_60]),
[final] ).
cnf(i_0_213,plain,
inductive(esk2_0),
inference(split_conjunct,[status(thm)],[i_0_129]),
[final] ).
cnf(i_0_214,axiom,
X1 = X1 ).
cnf(i_0_215,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_216,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_217,axiom,
( X1 != X2
| unordered_pair(X1,X3) = unordered_pair(X2,X3) ) ).
cnf(i_0_218,axiom,
( X1 != X2
| unordered_pair(X3,X1) = unordered_pair(X3,X2) ) ).
cnf(i_0_219,axiom,
( X1 != X2
| second(X1) = second(X2) ) ).
cnf(i_0_220,axiom,
( X1 != X2
| first(X1) = first(X2) ) ).
cnf(i_0_221,axiom,
( X1 != X2
| intersection(X1,X3) = intersection(X2,X3) ) ).
cnf(i_0_222,axiom,
( X1 != X2
| intersection(X3,X1) = intersection(X3,X2) ) ).
cnf(i_0_223,axiom,
( X1 != X2
| union(X1,X3) = union(X2,X3) ) ).
cnf(i_0_224,axiom,
( X1 != X2
| union(X3,X1) = union(X3,X2) ) ).
cnf(i_0_225,axiom,
( X1 != X2
| ~ member(X1,X3)
| member(X2,X3) ) ).
cnf(i_0_226,axiom,
( X1 != X2
| ~ member(X3,X1)
| member(X3,X2) ) ).
cnf(i_0_227,axiom,
( X1 != X2
| ~ inductive(X1)
| inductive(X2) ) ).
cnf(i_0_228,axiom,
( X1 != X2
| ~ subclass(X1,X3)
| subclass(X2,X3) ) ).
cnf(i_0_229,axiom,
( X1 != X2
| ~ subclass(X3,X1)
| subclass(X3,X2) ) ).
cnf(i_0_230,axiom,
( X1 != X2
| ~ function(X1)
| function(X2) ) ).
cnf(i_0_231,axiom,
( X1 != X2
| ~ disjoint(X1,X3)
| disjoint(X2,X3) ) ).
cnf(i_0_232,axiom,
( X1 != X2
| ~ disjoint(X3,X1)
| disjoint(X3,X2) ) ).
cnf(i_0_214_001,axiom,
X1 = X1 ).
cnf(i_0_215_002,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_216_003,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_217_004,axiom,
( X1 != X2
| unordered_pair(X1,X3) = unordered_pair(X2,X3) ) ).
cnf(i_0_218_005,axiom,
( X1 != X2
| unordered_pair(X3,X1) = unordered_pair(X3,X2) ) ).
cnf(i_0_219_006,axiom,
( X1 != X2
| second(X1) = second(X2) ) ).
cnf(i_0_220_007,axiom,
( X1 != X2
| first(X1) = first(X2) ) ).
cnf(i_0_221_008,axiom,
( X1 != X2
| intersection(X1,X3) = intersection(X2,X3) ) ).
cnf(i_0_222_009,axiom,
( X1 != X2
| intersection(X3,X1) = intersection(X3,X2) ) ).
cnf(i_0_223_010,axiom,
( X1 != X2
| union(X1,X3) = union(X2,X3) ) ).
cnf(i_0_224_011,axiom,
( X1 != X2
| union(X3,X1) = union(X3,X2) ) ).
cnf(i_0_225_012,axiom,
( X1 != X2
| ~ member(X1,X3)
| member(X2,X3) ) ).
cnf(i_0_226_013,axiom,
( X1 != X2
| ~ member(X3,X1)
| member(X3,X2) ) ).
cnf(i_0_227_014,axiom,
( X1 != X2
| ~ inductive(X1)
| inductive(X2) ) ).
cnf(i_0_228_015,axiom,
( X1 != X2
| ~ subclass(X1,X3)
| subclass(X2,X3) ) ).
cnf(i_0_229_016,axiom,
( X1 != X2
| ~ subclass(X3,X1)
| subclass(X3,X2) ) ).
cnf(i_0_230_017,axiom,
( X1 != X2
| ~ function(X1)
| function(X2) ) ).
cnf(i_0_231_018,axiom,
( X1 != X2
| ~ disjoint(X1,X3)
| disjoint(X2,X3) ) ).
cnf(i_0_232_019,axiom,
( X1 != X2
| ~ disjoint(X3,X1)
| disjoint(X3,X2) ) ).
cnf(i_0_233,plain,
( ~ member(union(X1,unordered_pair(X1,X1)),universal_class)
| ~ member(X1,universal_class)
| member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(union(X1,unordered_pair(X1,X1)),union(X1,unordered_pair(X1,X1))))),successor_relation) ),
inference(equality_inference,[],[153]) ).
cnf(i_0_234,plain,
( ~ member(X1,universal_class)
| member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X1,X1))),identity_relation) ),
inference(equality_inference,[],[161]) ).
cnf(i_0_235,plain,
( ~ member(X1,universal_class)
| member(X1,unordered_pair(X1,X2)) ),
inference(equality_inference,[],[177]) ).
cnf(i_0_236,plain,
( ~ member(X1,universal_class)
| member(X1,unordered_pair(X2,X1)) ),
inference(equality_inference,[],[178]) ).
cnf(i_0_237,plain,
subclass(X1,X1),
inference(equality_inference,[],[207]) ).
cnf(i_0_238,plain,
subclass(X1,X1),
inference(equality_inference,[],[208]) ).
cnf(i_0_239,plain,
~ member(null_class,unordered_pair(X1,X2)),
inference(scs_inference,[],[i_0_209,i_0_171]) ).
cnf(i_0_240,plain,
( member(X1,universal_class)
| ~ member(X1,unordered_pair(X2,X3)) ),
inference(rename_variables,[],[i_0_171]) ).
cnf(i_0_241,plain,
~ member(null_class,power_class(X1)),
inference(scs_inference,[],[i_0_209,i_0_171,i_0_191]) ).
cnf(i_0_242,plain,
( member(X1,universal_class)
| ~ member(X1,power_class(X2)) ),
inference(rename_variables,[],[i_0_191]) ).
cnf(i_0_243,plain,
~ member(null_class,domain_of(X1)),
inference(scs_inference,[],[i_0_209,i_0_171,i_0_191,i_0_192]) ).
cnf(i_0_244,plain,
( member(X1,universal_class)
| ~ member(X1,domain_of(X2)) ),
inference(rename_variables,[],[i_0_192]) ).
cnf(i_0_245,plain,
~ member(null_class,complement(X1)),
inference(scs_inference,[],[i_0_209,i_0_171,i_0_191,i_0_192,i_0_193]) ).
cnf(i_0_246,plain,
( member(X1,universal_class)
| ~ member(X1,complement(X2)) ),
inference(rename_variables,[],[i_0_193]) ).
cnf(i_0_247,plain,
~ inductive(universal_class),
inference(scs_inference,[],[i_0_209,i_0_171,i_0_191,i_0_192,i_0_193,i_0_205]) ).
cnf(i_0_248,plain,
( member(null_class,X1)
| ~ inductive(X1) ),
inference(rename_variables,[],[i_0_205]) ).
cnf(i_0_249,plain,
~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(null_class,null_class))),compose(X2,X3)),
inference(scs_inference,[],[i_0_209,i_0_171,i_0_191,i_0_192,i_0_193,i_0_205,i_0_133]) ).
cnf(i_0_250,plain,
( member(X1,domain_of(domain_of(flip(cross_product(intersection(X2,cross_product(domain_of(domain_of(flip(cross_product(intersection(X3,cross_product(unordered_pair(X4,X4),universal_class)),universal_class)))),universal_class)),universal_class)))))
| ~ member(unordered_pair(unordered_pair(X4,X4),unordered_pair(X4,unordered_pair(X1,X1))),compose(X2,X3)) ),
inference(rename_variables,[],[i_0_133]) ).
cnf(i_0_251,plain,
disjoint(null_class,X1),
inference(scs_inference,[],[i_0_209,i_0_204,i_0_171,i_0_191,i_0_192,i_0_193,i_0_205,i_0_133,i_0_186]) ).
cnf(i_0_252,plain,
~ member(X1,null_class),
inference(rename_variables,[],[i_0_204]) ).
cnf(i_0_253,plain,
( member(esk5_2(X1,X2),X1)
| disjoint(X1,X2) ),
inference(rename_variables,[],[i_0_186]) ).
cnf(i_0_254,plain,
disjoint(X1,null_class),
inference(scs_inference,[],[i_0_209,i_0_204,i_0_252,i_0_171,i_0_191,i_0_192,i_0_193,i_0_205,i_0_133,i_0_186,i_0_187]) ).
cnf(i_0_255,plain,
~ member(X1,null_class),
inference(rename_variables,[],[i_0_204]) ).
cnf(i_0_256,plain,
( member(esk5_2(X1,X2),X2)
| disjoint(X1,X2) ),
inference(rename_variables,[],[i_0_187]) ).
cnf(i_0_257,plain,
subclass(null_class,X1),
inference(scs_inference,[],[i_0_209,i_0_204,i_0_252,i_0_255,i_0_171,i_0_191,i_0_192,i_0_193,i_0_205,i_0_133,i_0_186,i_0_187,i_0_188]) ).
cnf(i_0_258,plain,
~ member(X1,null_class),
inference(rename_variables,[],[i_0_204]) ).
cnf(i_0_259,plain,
( member(esk1_2(X1,X2),X1)
| subclass(X1,X2) ),
inference(rename_variables,[],[i_0_188]) ).
cnf(i_0_260,plain,
member(esk2_0,unordered_pair(esk2_0,X1)),
inference(scs_inference,[],[i_0_209,i_0_204,i_0_252,i_0_255,i_0_211,i_0_171,i_0_191,i_0_192,i_0_193,i_0_205,i_0_133,i_0_186,i_0_187,i_0_188,i_0_235]) ).
cnf(i_0_261,plain,
( ~ member(X1,universal_class)
| member(X1,unordered_pair(X1,X2)) ),
inference(rename_variables,[],[i_0_235]) ).
cnf(i_0_262,plain,
member(esk2_0,unordered_pair(X1,esk2_0)),
inference(scs_inference,[],[i_0_209,i_0_204,i_0_252,i_0_255,i_0_211,i_0_171,i_0_191,i_0_192,i_0_193,i_0_205,i_0_133,i_0_186,i_0_187,i_0_188,i_0_235,i_0_236]) ).
cnf(i_0_263,plain,
( ~ member(X1,universal_class)
| member(X1,unordered_pair(X2,X1)) ),
inference(rename_variables,[],[i_0_236]) ).
cnf(i_0_264,plain,
~ subclass(universal_class,null_class),
inference(scs_inference,[],[i_0_209,i_0_204,i_0_252,i_0_255,i_0_258,i_0_211,i_0_171,i_0_191,i_0_192,i_0_193,i_0_205,i_0_133,i_0_186,i_0_187,i_0_188,i_0_235,i_0_236,i_0_183]) ).
cnf(i_0_265,plain,
~ member(X1,null_class),
inference(rename_variables,[],[i_0_204]) ).
cnf(i_0_266,plain,
( ~ member(X1,X2)
| member(X1,X3)
| ~ subclass(X2,X3) ),
inference(rename_variables,[],[i_0_183]) ).
cnf(i_0_267,plain,
esk2_0 != null_class,
inference(scs_inference,[],[i_0_209,i_0_204,i_0_252,i_0_255,i_0_258,i_0_211,i_0_171,i_0_191,i_0_192,i_0_193,i_0_205,i_0_133,i_0_186,i_0_187,i_0_188,i_0_235,i_0_236,i_0_183,i_0_225]) ).
cnf(i_0_268,plain,
universal_class != null_class,
inference(scs_inference,[],[i_0_209,i_0_204,i_0_252,i_0_255,i_0_258,i_0_265,i_0_211,i_0_171,i_0_191,i_0_192,i_0_193,i_0_205,i_0_133,i_0_186,i_0_187,i_0_188,i_0_235,i_0_236,i_0_183,i_0_225,i_0_226]) ).
cnf(i_0_269,plain,
~ member(X1,null_class),
inference(rename_variables,[],[i_0_204]) ).
cnf(i_0_270,plain,
member(esk2_0,power_class(esk2_0)),
inference(scs_inference,[],[i_0_209,i_0_237,i_0_204,i_0_252,i_0_255,i_0_258,i_0_265,i_0_211,i_0_171,i_0_191,i_0_192,i_0_193,i_0_205,i_0_133,i_0_186,i_0_187,i_0_188,i_0_235,i_0_236,i_0_183,i_0_225,i_0_226,i_0_179]) ).
cnf(i_0_271,plain,
subclass(X1,X1),
inference(rename_variables,[],[i_0_237]) ).
cnf(i_0_272,plain,
( ~ member(X1,universal_class)
| member(X1,power_class(X2))
| ~ subclass(X1,X2) ),
inference(rename_variables,[],[i_0_179]) ).
cnf(i_0_273,plain,
esk2_0 != universal_class,
inference(scs_inference,[],[i_0_209,i_0_237,i_0_204,i_0_252,i_0_255,i_0_258,i_0_265,i_0_211,i_0_213,i_0_171,i_0_191,i_0_192,i_0_193,i_0_205,i_0_133,i_0_186,i_0_187,i_0_188,i_0_235,i_0_236,i_0_183,i_0_225,i_0_226,i_0_179,i_0_227]) ).
cnf(i_0_274,plain,
null_class != universal_class,
inference(scs_inference,[],[i_0_209,i_0_237,i_0_271,i_0_204,i_0_252,i_0_255,i_0_258,i_0_265,i_0_211,i_0_213,i_0_171,i_0_191,i_0_192,i_0_193,i_0_205,i_0_133,i_0_186,i_0_187,i_0_188,i_0_235,i_0_236,i_0_183,i_0_225,i_0_226,i_0_179,i_0_227,i_0_228]) ).
cnf(i_0_275,plain,
subclass(X1,X1),
inference(rename_variables,[],[i_0_237]) ).
cnf(i_0_276,plain,
disjoint(esk6_1(esk2_0),esk2_0),
inference(scs_inference,[],[i_0_209,i_0_237,i_0_271,i_0_204,i_0_252,i_0_255,i_0_258,i_0_265,i_0_211,i_0_213,i_0_171,i_0_191,i_0_192,i_0_193,i_0_205,i_0_133,i_0_186,i_0_187,i_0_188,i_0_235,i_0_236,i_0_183,i_0_225,i_0_226,i_0_179,i_0_227,i_0_228,i_0_201]) ).
cnf(i_0_277,plain,
( X1 = null_class
| disjoint(esk6_1(X1),X1) ),
inference(rename_variables,[],[i_0_201]) ).
cnf(i_0_278,plain,
member(esk6_1(esk2_0),esk2_0),
inference(scs_inference,[],[i_0_209,i_0_237,i_0_271,i_0_204,i_0_252,i_0_255,i_0_258,i_0_265,i_0_211,i_0_213,i_0_171,i_0_191,i_0_192,i_0_193,i_0_205,i_0_133,i_0_186,i_0_187,i_0_188,i_0_235,i_0_236,i_0_183,i_0_225,i_0_226,i_0_179,i_0_227,i_0_228,i_0_201,i_0_202]) ).
cnf(i_0_279,plain,
( X1 = null_class
| member(esk6_1(X1),X1) ),
inference(rename_variables,[],[i_0_202]) ).
cnf(i_0_280,plain,
( esk2_0 != X1
| member(esk2_0,unordered_pair(X1,X2)) ),
inference(scs_inference,[],[i_0_209,i_0_237,i_0_271,i_0_204,i_0_252,i_0_255,i_0_258,i_0_265,i_0_211,i_0_213,i_0_171,i_0_191,i_0_192,i_0_193,i_0_205,i_0_133,i_0_186,i_0_187,i_0_188,i_0_235,i_0_236,i_0_183,i_0_225,i_0_226,i_0_179,i_0_227,i_0_228,i_0_201,i_0_202,i_0_177]) ).
cnf(i_0_281,plain,
( ~ member(X1,universal_class)
| member(X1,unordered_pair(X2,X3))
| X1 != X2 ),
inference(rename_variables,[],[i_0_177]) ).
cnf(i_0_282,plain,
subclass(X1,X1),
inference(rename_variables,[],[i_0_237]) ).
cnf(i_0_284,plain,
member(esk2_0,unordered_pair(esk2_0,X1)),
inference(equality_inference,[],[280]) ).
cnf(i_0_285,plain,
~ inductive(unordered_pair(X1,X2)),
inference(scs_inference,[],[i_0_239,i_0_205]) ).
cnf(i_0_286,plain,
( member(null_class,X1)
| ~ inductive(X1) ),
inference(rename_variables,[],[i_0_205]) ).
cnf(i_0_287,plain,
disjoint(esk6_1(universal_class),universal_class),
inference(scs_inference,[],[i_0_268,i_0_239,i_0_205,i_0_201]) ).
cnf(i_0_288,plain,
( X1 = null_class
| disjoint(esk6_1(X1),X1) ),
inference(rename_variables,[],[i_0_201]) ).
cnf(i_0_289,plain,
member(esk6_1(universal_class),universal_class),
inference(scs_inference,[],[i_0_268,i_0_239,i_0_205,i_0_201,i_0_202]) ).
cnf(i_0_290,plain,
( X1 = null_class
| member(esk6_1(X1),X1) ),
inference(rename_variables,[],[i_0_202]) ).
cnf(i_0_291,plain,
member(unordered_pair(X1,X2),unordered_pair(unordered_pair(X1,X2),X3)),
inference(scs_inference,[],[i_0_268,i_0_239,i_0_198,i_0_205,i_0_201,i_0_202,i_0_235]) ).
cnf(i_0_292,plain,
( ~ member(X1,universal_class)
| member(X1,unordered_pair(X1,X2)) ),
inference(rename_variables,[],[i_0_235]) ).
cnf(i_0_293,plain,
member(unordered_pair(X1,X2),unordered_pair(X3,unordered_pair(X1,X2))),
inference(scs_inference,[],[i_0_268,i_0_239,i_0_198,i_0_205,i_0_201,i_0_202,i_0_235,i_0_236]) ).
cnf(i_0_294,plain,
( ~ member(X1,universal_class)
| member(X1,unordered_pair(X2,X1)) ),
inference(rename_variables,[],[i_0_236]) ).
cnf(i_0_295,plain,
member(unordered_pair(X1,X2),power_class(universal_class)),
inference(scs_inference,[],[i_0_268,i_0_239,i_0_210,i_0_198,i_0_205,i_0_201,i_0_202,i_0_235,i_0_236,i_0_179]) ).
cnf(i_0_296,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_210]) ).
cnf(i_0_297,plain,
( ~ member(X1,universal_class)
| member(X1,power_class(X2))
| ~ subclass(X1,X2) ),
inference(rename_variables,[],[i_0_179]) ).
cnf(i_0_298,plain,
~ subclass(universal_class,compose(X1,X2)),
inference(scs_inference,[],[i_0_268,i_0_239,i_0_249,i_0_210,i_0_198,i_0_205,i_0_201,i_0_202,i_0_235,i_0_236,i_0_179,i_0_183]) ).
cnf(i_0_299,plain,
member(unordered_pair(X1,X2),universal_class),
inference(rename_variables,[],[i_0_198]) ).
cnf(i_0_300,plain,
( ~ member(X1,X2)
| member(X1,X3)
| ~ subclass(X2,X3) ),
inference(rename_variables,[],[i_0_183]) ).
cnf(i_0_301,plain,
unordered_pair(X1,X2) != null_class,
inference(scs_inference,[],[i_0_209,i_0_268,i_0_239,i_0_249,i_0_210,i_0_198,i_0_299,i_0_205,i_0_201,i_0_202,i_0_235,i_0_236,i_0_179,i_0_183,i_0_225]) ).
cnf(i_0_302,plain,
universal_class != compose(X1,X2),
inference(scs_inference,[],[i_0_209,i_0_268,i_0_239,i_0_249,i_0_210,i_0_198,i_0_299,i_0_205,i_0_201,i_0_202,i_0_235,i_0_236,i_0_179,i_0_183,i_0_225,i_0_226]) ).
cnf(i_0_303,plain,
member(unordered_pair(X1,X2),universal_class),
inference(rename_variables,[],[i_0_198]) ).
cnf(i_0_304,plain,
( unordered_pair(X1,X2) != X3
| member(unordered_pair(X1,X2),unordered_pair(X3,X4)) ),
inference(scs_inference,[],[i_0_209,i_0_268,i_0_239,i_0_249,i_0_210,i_0_198,i_0_299,i_0_303,i_0_205,i_0_201,i_0_202,i_0_235,i_0_236,i_0_179,i_0_183,i_0_225,i_0_226,i_0_177]) ).
cnf(i_0_305,plain,
( ~ member(X1,universal_class)
| member(X1,unordered_pair(X2,X3))
| X1 != X2 ),
inference(rename_variables,[],[i_0_177]) ).
cnf(i_0_306,plain,
member(unordered_pair(X1,X2),universal_class),
inference(rename_variables,[],[i_0_198]) ).
cnf(i_0_307,plain,
subclass(null_class,X1),
inference(rename_variables,[],[i_0_257]) ).
cnf(i_0_308,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_210]) ).
cnf(i_0_310,plain,
member(unordered_pair(X1,X2),unordered_pair(unordered_pair(X1,X2),X3)),
inference(equality_inference,[],[304]) ).
cnf(i_0_311,plain,
disjoint(esk6_1(unordered_pair(X1,X2)),unordered_pair(X1,X2)),
inference(scs_inference,[],[i_0_301,i_0_201]) ).
cnf(i_0_312,plain,
( X1 = null_class
| disjoint(esk6_1(X1),X1) ),
inference(rename_variables,[],[i_0_201]) ).
cnf(i_0_313,plain,
member(esk6_1(unordered_pair(X1,X2)),unordered_pair(X1,X2)),
inference(scs_inference,[],[i_0_301,i_0_201,i_0_202]) ).
cnf(i_0_314,plain,
( X1 = null_class
| member(esk6_1(X1),X1) ),
inference(rename_variables,[],[i_0_202]) ).
cnf(i_0_315,plain,
~ inductive(domain_of(X1)),
inference(scs_inference,[],[i_0_243,i_0_301,i_0_201,i_0_202,i_0_205]) ).
cnf(i_0_316,plain,
( member(null_class,X1)
| ~ inductive(X1) ),
inference(rename_variables,[],[i_0_205]) ).
cnf(i_0_317,plain,
member(esk6_1(universal_class),unordered_pair(esk6_1(universal_class),X1)),
inference(scs_inference,[],[i_0_243,i_0_301,i_0_289,i_0_201,i_0_202,i_0_205,i_0_235]) ).
cnf(i_0_318,plain,
( ~ member(X1,universal_class)
| member(X1,unordered_pair(X1,X2)) ),
inference(rename_variables,[],[i_0_235]) ).
cnf(i_0_319,plain,
member(esk6_1(universal_class),unordered_pair(X1,esk6_1(universal_class))),
inference(scs_inference,[],[i_0_243,i_0_301,i_0_289,i_0_201,i_0_202,i_0_205,i_0_235,i_0_236]) ).
cnf(i_0_320,plain,
( ~ member(X1,universal_class)
| member(X1,unordered_pair(X2,X1)) ),
inference(rename_variables,[],[i_0_236]) ).
cnf(i_0_321,plain,
member(esk6_1(universal_class),power_class(universal_class)),
inference(scs_inference,[],[i_0_243,i_0_301,i_0_210,i_0_289,i_0_201,i_0_202,i_0_205,i_0_235,i_0_236,i_0_179]) ).
cnf(i_0_322,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_210]) ).
cnf(i_0_323,plain,
( ~ member(X1,universal_class)
| member(X1,power_class(X2))
| ~ subclass(X1,X2) ),
inference(rename_variables,[],[i_0_179]) ).
cnf(i_0_324,plain,
~ subclass(power_class(esk2_0),null_class),
inference(scs_inference,[],[i_0_243,i_0_301,i_0_204,i_0_270,i_0_210,i_0_289,i_0_201,i_0_202,i_0_205,i_0_235,i_0_236,i_0_179,i_0_183]) ).
cnf(i_0_325,plain,
~ member(X1,null_class),
inference(rename_variables,[],[i_0_204]) ).
cnf(i_0_326,plain,
( ~ member(X1,X2)
| member(X1,X3)
| ~ subclass(X2,X3) ),
inference(rename_variables,[],[i_0_183]) ).
cnf(i_0_327,plain,
esk2_0 != unordered_pair(X1,X2),
inference(scs_inference,[],[i_0_243,i_0_285,i_0_301,i_0_204,i_0_213,i_0_270,i_0_210,i_0_289,i_0_201,i_0_202,i_0_205,i_0_235,i_0_236,i_0_179,i_0_183,i_0_227]) ).
cnf(i_0_328,plain,
power_class(esk2_0) != null_class,
inference(scs_inference,[],[i_0_243,i_0_285,i_0_301,i_0_204,i_0_325,i_0_213,i_0_270,i_0_210,i_0_289,i_0_201,i_0_202,i_0_205,i_0_235,i_0_236,i_0_179,i_0_183,i_0_227,i_0_226]) ).
cnf(i_0_329,plain,
~ member(X1,null_class),
inference(rename_variables,[],[i_0_204]) ).
cnf(i_0_330,plain,
compose(X1,X2) != universal_class,
inference(scs_inference,[],[i_0_243,i_0_285,i_0_298,i_0_301,i_0_204,i_0_325,i_0_213,i_0_270,i_0_210,i_0_289,i_0_237,i_0_201,i_0_202,i_0_205,i_0_235,i_0_236,i_0_179,i_0_183,i_0_227,i_0_226,i_0_228]) ).
cnf(i_0_331,plain,
subclass(X1,X1),
inference(rename_variables,[],[i_0_237]) ).
cnf(i_0_332,plain,
~ member(esk2_0,cross_product(X1,X2)),
inference(scs_inference,[],[i_0_243,i_0_285,i_0_298,i_0_301,i_0_204,i_0_325,i_0_213,i_0_270,i_0_210,i_0_289,i_0_237,i_0_201,i_0_202,i_0_205,i_0_235,i_0_236,i_0_179,i_0_183,i_0_227,i_0_226,i_0_228,i_0_158]) ).
cnf(i_0_333,plain,
( X1 = unordered_pair(unordered_pair(first(X1),first(X1)),unordered_pair(first(X1),unordered_pair(second(X1),second(X1))))
| ~ member(X1,cross_product(X2,X3)) ),
inference(rename_variables,[],[i_0_158]) ).
cnf(i_0_334,plain,
( esk6_1(unordered_pair(X1,X2)) = X1
| esk6_1(unordered_pair(X1,X2)) = X2 ),
inference(scs_inference,[],[i_0_243,i_0_285,i_0_298,i_0_301,i_0_204,i_0_325,i_0_213,i_0_270,i_0_210,i_0_289,i_0_237,i_0_201,i_0_202,i_0_205,i_0_235,i_0_236,i_0_179,i_0_183,i_0_227,i_0_226,i_0_228,i_0_158,i_0_175]) ).
cnf(i_0_335,plain,
( ~ member(X1,unordered_pair(X2,X3))
| X1 = X2
| X1 = X3 ),
inference(rename_variables,[],[i_0_175]) ).
cnf(i_0_336,plain,
( ~ member(esk6_1(unordered_pair(null_class,X1)),universal_class)
| esk6_1(unordered_pair(null_class,X1)) = X1 ),
inference(scs_inference,[],[i_0_209,i_0_243,i_0_285,i_0_298,i_0_301,i_0_204,i_0_325,i_0_213,i_0_270,i_0_210,i_0_289,i_0_237,i_0_201,i_0_202,i_0_205,i_0_235,i_0_236,i_0_179,i_0_183,i_0_227,i_0_226,i_0_228,i_0_158,i_0_175,i_0_225]) ).
cnf(i_0_337,plain,
( ~ subclass(universal_class,esk6_1(unordered_pair(null_class,X1)))
| esk6_1(unordered_pair(null_class,X1)) = X1 ),
inference(scs_inference,[],[i_0_209,i_0_264,i_0_243,i_0_285,i_0_298,i_0_301,i_0_204,i_0_325,i_0_213,i_0_270,i_0_210,i_0_289,i_0_237,i_0_201,i_0_202,i_0_205,i_0_235,i_0_236,i_0_179,i_0_183,i_0_227,i_0_226,i_0_228,i_0_158,i_0_175,i_0_225,i_0_229]) ).
cnf(i_0_338,plain,
unordered_pair(X1,X2) != null_class,
inference(rename_variables,[],[i_0_301]) ).
cnf(i_0_339,plain,
( member(esk6_1(X1),universal_class)
| X1 = null_class ),
inference(rename_variables,[],[i_0_203]) ).
cnf(i_0_340,plain,
( subclass(esk6_1(unordered_pair(null_class,X1)),null_class)
| esk6_1(unordered_pair(null_class,X1)) = X1 ),
inference(scs_inference,[],[i_0_209,i_0_264,i_0_243,i_0_285,i_0_298,i_0_301,i_0_204,i_0_325,i_0_213,i_0_270,i_0_210,i_0_289,i_0_237,i_0_201,i_0_202,i_0_205,i_0_235,i_0_236,i_0_179,i_0_183,i_0_227,i_0_226,i_0_228,i_0_158,i_0_175,i_0_225,i_0_229,i_0_203,i_0_207]) ).
cnf(i_0_341,plain,
( X1 != X2
| subclass(X1,X2) ),
inference(rename_variables,[],[i_0_207]) ).
cnf(i_0_342,plain,
( null_class = esk6_1(unordered_pair(null_class,X1))
| esk6_1(unordered_pair(null_class,X1)) = X1 ),
inference(scs_inference,[],[i_0_209,i_0_264,i_0_243,i_0_285,i_0_298,i_0_301,i_0_204,i_0_325,i_0_213,i_0_270,i_0_210,i_0_289,i_0_237,i_0_201,i_0_202,i_0_205,i_0_235,i_0_236,i_0_179,i_0_183,i_0_227,i_0_226,i_0_228,i_0_158,i_0_175,i_0_225,i_0_229,i_0_203,i_0_207,i_0_215]) ).
cnf(i_0_343,plain,
( member(X1,universal_class)
| ~ member(X1,unordered_pair(X2,X3)) ),
inference(rename_variables,[],[i_0_171]) ).
cnf(i_0_344,plain,
( esk6_1(unordered_pair(null_class,X1)) = X1
| ~ member(esk6_1(unordered_pair(null_class,X1)),power_class(X2)) ),
inference(scs_inference,[],[i_0_209,i_0_264,i_0_243,i_0_285,i_0_298,i_0_301,i_0_204,i_0_325,i_0_213,i_0_270,i_0_210,i_0_289,i_0_237,i_0_201,i_0_202,i_0_205,i_0_235,i_0_236,i_0_179,i_0_183,i_0_227,i_0_226,i_0_228,i_0_158,i_0_175,i_0_225,i_0_229,i_0_203,i_0_207,i_0_215,i_0_171,i_0_191]) ).
cnf(i_0_345,plain,
( member(X1,universal_class)
| ~ member(X1,power_class(X2)) ),
inference(rename_variables,[],[i_0_191]) ).
cnf(i_0_346,plain,
( esk6_1(unordered_pair(null_class,X1)) = X1
| ~ member(esk6_1(unordered_pair(null_class,X1)),domain_of(X2)) ),
inference(scs_inference,[],[i_0_209,i_0_264,i_0_243,i_0_285,i_0_298,i_0_301,i_0_204,i_0_325,i_0_213,i_0_270,i_0_210,i_0_289,i_0_237,i_0_201,i_0_202,i_0_205,i_0_235,i_0_236,i_0_179,i_0_183,i_0_227,i_0_226,i_0_228,i_0_158,i_0_175,i_0_225,i_0_229,i_0_203,i_0_207,i_0_215,i_0_171,i_0_191,i_0_192]) ).
cnf(i_0_347,plain,
( member(X1,universal_class)
| ~ member(X1,domain_of(X2)) ),
inference(rename_variables,[],[i_0_192]) ).
cnf(i_0_348,plain,
( esk6_1(unordered_pair(null_class,X1)) = X1
| ~ member(unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(esk6_1(unordered_pair(null_class,X1)),esk6_1(unordered_pair(null_class,X1))))),compose(X3,X4)) ),
inference(scs_inference,[],[i_0_209,i_0_264,i_0_243,i_0_285,i_0_298,i_0_301,i_0_204,i_0_325,i_0_213,i_0_270,i_0_210,i_0_289,i_0_237,i_0_201,i_0_202,i_0_205,i_0_235,i_0_236,i_0_179,i_0_183,i_0_227,i_0_226,i_0_228,i_0_158,i_0_175,i_0_225,i_0_229,i_0_203,i_0_207,i_0_215,i_0_171,i_0_191,i_0_192,i_0_133]) ).
cnf(i_0_349,plain,
( member(X1,domain_of(domain_of(flip(cross_product(intersection(X2,cross_product(domain_of(domain_of(flip(cross_product(intersection(X3,cross_product(unordered_pair(X4,X4),universal_class)),universal_class)))),universal_class)),universal_class)))))
| ~ member(unordered_pair(unordered_pair(X4,X4),unordered_pair(X4,unordered_pair(X1,X1))),compose(X2,X3)) ),
inference(rename_variables,[],[i_0_133]) ).
cnf(i_0_350,plain,
( esk6_1(unordered_pair(null_class,X1)) = X1
| ~ member(esk6_1(unordered_pair(null_class,X1)),complement(X2)) ),
inference(scs_inference,[],[i_0_209,i_0_264,i_0_243,i_0_285,i_0_298,i_0_301,i_0_204,i_0_325,i_0_213,i_0_270,i_0_210,i_0_289,i_0_237,i_0_201,i_0_202,i_0_205,i_0_235,i_0_236,i_0_179,i_0_183,i_0_227,i_0_226,i_0_228,i_0_158,i_0_175,i_0_225,i_0_229,i_0_203,i_0_207,i_0_215,i_0_171,i_0_191,i_0_192,i_0_133,i_0_193]) ).
cnf(i_0_351,plain,
( member(X1,universal_class)
| ~ member(X1,complement(X2)) ),
inference(rename_variables,[],[i_0_193]) ).
cnf(i_0_352,plain,
( esk2_0 != esk6_1(unordered_pair(null_class,X1))
| esk6_1(unordered_pair(null_class,X1)) = X1 ),
inference(scs_inference,[],[i_0_209,i_0_264,i_0_243,i_0_285,i_0_267,i_0_298,i_0_301,i_0_204,i_0_325,i_0_213,i_0_270,i_0_210,i_0_289,i_0_237,i_0_201,i_0_202,i_0_205,i_0_235,i_0_236,i_0_179,i_0_183,i_0_227,i_0_226,i_0_228,i_0_158,i_0_175,i_0_225,i_0_229,i_0_203,i_0_207,i_0_215,i_0_171,i_0_191,i_0_192,i_0_133,i_0_193,i_0_216]) ).
cnf(i_0_353,plain,
( ~ member(X1,universal_class)
| member(X1,unordered_pair(X2,X3))
| X1 != X3 ),
inference(rename_variables,[],[i_0_178]) ).
cnf(i_0_354,plain,
( function(X1)
| esk7_0 != X1
| esk6_1(unordered_pair(null_class,X2)) = X2 ),
inference(scs_inference,[],[i_0_209,i_0_264,i_0_243,i_0_285,i_0_267,i_0_298,i_0_301,i_0_204,i_0_325,i_0_213,i_0_270,i_0_210,i_0_198,i_0_289,i_0_199,i_0_237,i_0_212,i_0_211,i_0_201,i_0_202,i_0_205,i_0_235,i_0_236,i_0_179,i_0_183,i_0_227,i_0_226,i_0_228,i_0_158,i_0_175,i_0_225,i_0_229,i_0_203,i_0_207,i_0_215,i_0_171,i_0_191,i_0_192,i_0_133,i_0_193,i_0_216,i_0_230]) ).
cnf(i_0_355,plain,
( function(esk7_0)
| esk6_1(unordered_pair(null_class,X1)) = X1 ),
inference(equality_inference,[],[354]) ).
cnf(i_0_356,plain,
~ member(esk2_0,identity_relation),
inference(scs_inference,[],[i_0_327,i_0_160]) ).
cnf(i_0_357,plain,
esk2_0 != unordered_pair(X1,X2),
inference(rename_variables,[],[i_0_327]) ).
cnf(i_0_358,plain,
( X1 = unordered_pair(unordered_pair(esk4_1(X1),esk4_1(X1)),unordered_pair(esk4_1(X1),unordered_pair(esk4_1(X1),esk4_1(X1))))
| ~ member(X1,identity_relation) ),
inference(rename_variables,[],[i_0_160]) ).
cnf(i_0_359,plain,
disjoint(esk6_1(power_class(esk2_0)),power_class(esk2_0)),
inference(scs_inference,[],[i_0_328,i_0_327,i_0_160,i_0_201]) ).
cnf(i_0_360,plain,
( X1 = null_class
| disjoint(esk6_1(X1),X1) ),
inference(rename_variables,[],[i_0_201]) ).
cnf(i_0_361,plain,
~ inductive(complement(X1)),
inference(scs_inference,[],[i_0_245,i_0_328,i_0_327,i_0_160,i_0_201,i_0_205]) ).
cnf(i_0_362,plain,
( member(null_class,X1)
| ~ inductive(X1) ),
inference(rename_variables,[],[i_0_205]) ).
cnf(i_0_363,plain,
member(esk6_1(power_class(esk2_0)),power_class(esk2_0)),
inference(scs_inference,[],[i_0_245,i_0_328,i_0_327,i_0_160,i_0_201,i_0_205,i_0_202]) ).
cnf(i_0_364,plain,
( X1 = null_class
| member(esk6_1(X1),X1) ),
inference(rename_variables,[],[i_0_202]) ).
cnf(i_0_365,plain,
~ member(unordered_pair(X1,X2),esk6_1(unordered_pair(unordered_pair(X1,X2),X3))),
inference(scs_inference,[],[i_0_245,i_0_328,i_0_291,i_0_311,i_0_327,i_0_160,i_0_201,i_0_205,i_0_202,i_0_174]) ).
cnf(i_0_366,plain,
member(unordered_pair(X1,X2),unordered_pair(unordered_pair(X1,X2),X3)),
inference(rename_variables,[],[i_0_291]) ).
cnf(i_0_367,plain,
disjoint(esk6_1(unordered_pair(X1,X2)),unordered_pair(X1,X2)),
inference(rename_variables,[],[i_0_311]) ).
cnf(i_0_368,plain,
( ~ member(X1,X2)
| ~ disjoint(X3,X2)
| ~ member(X1,X3) ),
inference(rename_variables,[],[i_0_174]) ).
cnf(i_0_369,plain,
member(esk2_0,power_class(universal_class)),
inference(scs_inference,[],[i_0_245,i_0_328,i_0_291,i_0_210,i_0_311,i_0_327,i_0_211,i_0_160,i_0_201,i_0_205,i_0_202,i_0_174,i_0_179]) ).
cnf(i_0_370,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_210]) ).
cnf(i_0_371,plain,
( ~ member(X1,universal_class)
| member(X1,power_class(X2))
| ~ subclass(X1,X2) ),
inference(rename_variables,[],[i_0_179]) ).
cnf(i_0_372,plain,
~ subclass(power_class(universal_class),compose(X1,X2)),
inference(scs_inference,[],[i_0_245,i_0_328,i_0_249,i_0_295,i_0_291,i_0_210,i_0_311,i_0_327,i_0_211,i_0_160,i_0_201,i_0_205,i_0_202,i_0_174,i_0_179,i_0_183]) ).
cnf(i_0_373,plain,
member(unordered_pair(X1,X2),power_class(universal_class)),
inference(rename_variables,[],[i_0_295]) ).
cnf(i_0_374,plain,
( ~ member(X1,X2)
| member(X1,X3)
| ~ subclass(X2,X3) ),
inference(rename_variables,[],[i_0_183]) ).
cnf(i_0_375,plain,
esk2_0 != domain_of(X1),
inference(scs_inference,[],[i_0_245,i_0_315,i_0_328,i_0_249,i_0_295,i_0_213,i_0_291,i_0_210,i_0_311,i_0_327,i_0_211,i_0_160,i_0_201,i_0_205,i_0_202,i_0_174,i_0_179,i_0_183,i_0_227]) ).
cnf(i_0_376,plain,
power_class(universal_class) != compose(X1,X2),
inference(scs_inference,[],[i_0_245,i_0_315,i_0_328,i_0_249,i_0_295,i_0_373,i_0_213,i_0_291,i_0_210,i_0_311,i_0_327,i_0_211,i_0_160,i_0_201,i_0_205,i_0_202,i_0_174,i_0_179,i_0_183,i_0_227,i_0_226]) ).
cnf(i_0_377,plain,
member(unordered_pair(X1,X2),power_class(universal_class)),
inference(rename_variables,[],[i_0_295]) ).
cnf(i_0_378,plain,
null_class != power_class(esk2_0),
inference(scs_inference,[],[i_0_245,i_0_315,i_0_324,i_0_328,i_0_249,i_0_295,i_0_373,i_0_213,i_0_291,i_0_210,i_0_311,i_0_327,i_0_257,i_0_211,i_0_160,i_0_201,i_0_205,i_0_202,i_0_174,i_0_179,i_0_183,i_0_227,i_0_226,i_0_228]) ).
cnf(i_0_379,plain,
subclass(null_class,X1),
inference(rename_variables,[],[i_0_257]) ).
cnf(i_0_380,plain,
subclass(esk6_1(power_class(esk2_0)),esk2_0),
inference(scs_inference,[],[i_0_245,i_0_315,i_0_324,i_0_328,i_0_249,i_0_295,i_0_373,i_0_213,i_0_291,i_0_210,i_0_311,i_0_327,i_0_257,i_0_211,i_0_160,i_0_201,i_0_205,i_0_202,i_0_174,i_0_179,i_0_183,i_0_227,i_0_226,i_0_228,i_0_190]) ).
cnf(i_0_381,plain,
( ~ member(X1,power_class(X2))
| subclass(X1,X2) ),
inference(rename_variables,[],[i_0_190]) ).
cnf(i_0_382,plain,
( unordered_pair(X1,X2) != X3
| member(unordered_pair(X1,X2),unordered_pair(X4,X3)) ),
inference(scs_inference,[],[i_0_245,i_0_315,i_0_324,i_0_328,i_0_249,i_0_295,i_0_373,i_0_213,i_0_198,i_0_291,i_0_210,i_0_311,i_0_327,i_0_257,i_0_211,i_0_160,i_0_201,i_0_205,i_0_202,i_0_174,i_0_179,i_0_183,i_0_227,i_0_226,i_0_228,i_0_190,i_0_178]) ).
cnf(i_0_383,plain,
( ~ member(X1,universal_class)
| member(X1,unordered_pair(X2,X3))
| X1 != X3 ),
inference(rename_variables,[],[i_0_178]) ).
cnf(i_0_384,plain,
member(unordered_pair(X1,X2),universal_class),
inference(rename_variables,[],[i_0_198]) ).
cnf(i_0_386,plain,
member(unordered_pair(X1,X2),unordered_pair(X3,unordered_pair(X1,X2))),
inference(equality_inference,[],[382]) ).
cnf(i_0_387,plain,
~ inductive(power_class(X1)),
inference(scs_inference,[],[i_0_241,i_0_205]) ).
cnf(i_0_388,plain,
( member(null_class,X1)
| ~ inductive(X1) ),
inference(rename_variables,[],[i_0_205]) ).
cnf(i_0_389,plain,
~ member(esk2_0,esk6_1(power_class(esk2_0))),
inference(scs_inference,[],[i_0_241,i_0_270,i_0_359,i_0_205,i_0_174]) ).
cnf(i_0_390,plain,
( ~ member(X1,X2)
| ~ disjoint(X3,X2)
| ~ member(X1,X3) ),
inference(rename_variables,[],[i_0_174]) ).
cnf(i_0_391,plain,
~ subclass(unordered_pair(X1,unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(null_class,null_class)))),compose(X3,X4)),
inference(scs_inference,[],[i_0_241,i_0_249,i_0_293,i_0_270,i_0_359,i_0_205,i_0_174,i_0_183]) ).
cnf(i_0_392,plain,
member(unordered_pair(X1,X2),unordered_pair(X3,unordered_pair(X1,X2))),
inference(rename_variables,[],[i_0_293]) ).
cnf(i_0_393,plain,
( ~ member(X1,X2)
| member(X1,X3)
| ~ subclass(X2,X3) ),
inference(rename_variables,[],[i_0_183]) ).
cnf(i_0_394,plain,
esk2_0 != complement(X1),
inference(scs_inference,[],[i_0_241,i_0_361,i_0_249,i_0_213,i_0_293,i_0_270,i_0_359,i_0_205,i_0_174,i_0_183,i_0_227]) ).
cnf(i_0_395,plain,
universal_class != esk6_1(unordered_pair(unordered_pair(X1,X2),X3)),
inference(scs_inference,[],[i_0_241,i_0_361,i_0_249,i_0_198,i_0_213,i_0_293,i_0_270,i_0_365,i_0_359,i_0_205,i_0_174,i_0_183,i_0_227,i_0_226]) ).
cnf(i_0_396,plain,
~ member(unordered_pair(X1,X2),esk6_1(unordered_pair(unordered_pair(X1,X2),X3))),
inference(rename_variables,[],[i_0_365]) ).
cnf(i_0_397,plain,
compose(X1,X2) != power_class(universal_class),
inference(scs_inference,[],[i_0_241,i_0_361,i_0_372,i_0_249,i_0_198,i_0_213,i_0_293,i_0_270,i_0_365,i_0_359,i_0_237,i_0_205,i_0_174,i_0_183,i_0_227,i_0_226,i_0_228]) ).
cnf(i_0_398,plain,
subclass(X1,X1),
inference(rename_variables,[],[i_0_237]) ).
cnf(i_0_399,plain,
( esk6_1(universal_class) != X1
| member(esk6_1(universal_class),unordered_pair(X2,X1)) ),
inference(scs_inference,[],[i_0_241,i_0_361,i_0_372,i_0_249,i_0_198,i_0_289,i_0_213,i_0_293,i_0_270,i_0_365,i_0_359,i_0_237,i_0_205,i_0_174,i_0_183,i_0_227,i_0_226,i_0_228,i_0_178]) ).
cnf(i_0_400,plain,
( ~ member(X1,universal_class)
| member(X1,unordered_pair(X2,X3))
| X1 != X3 ),
inference(rename_variables,[],[i_0_178]) ).
cnf(i_0_401,plain,
( ~ subclass(esk2_0,esk6_1(power_class(esk2_0)))
| esk6_1(power_class(esk2_0)) = esk2_0 ),
inference(scs_inference,[],[i_0_241,i_0_361,i_0_372,i_0_249,i_0_198,i_0_289,i_0_213,i_0_293,i_0_270,i_0_365,i_0_359,i_0_380,i_0_237,i_0_205,i_0_174,i_0_183,i_0_227,i_0_226,i_0_228,i_0_178,i_0_189]) ).
cnf(i_0_402,plain,
( ~ subclass(X1,X2)
| ~ subclass(X2,X1)
| X1 = X2 ),
inference(rename_variables,[],[i_0_189]) ).
cnf(i_0_403,plain,
( member(unordered_pair(unordered_pair(esk2_0,esk2_0),unordered_pair(esk2_0,unordered_pair(union(esk2_0,unordered_pair(esk2_0,esk2_0)),union(esk2_0,unordered_pair(esk2_0,esk2_0))))),successor_relation)
| ~ member(union(esk2_0,unordered_pair(esk2_0,esk2_0)),universal_class) ),
inference(scs_inference,[],[i_0_241,i_0_361,i_0_372,i_0_249,i_0_198,i_0_289,i_0_213,i_0_211,i_0_293,i_0_270,i_0_365,i_0_359,i_0_380,i_0_237,i_0_205,i_0_174,i_0_183,i_0_227,i_0_226,i_0_228,i_0_178,i_0_189,i_0_233]) ).
cnf(i_0_404,plain,
( ~ member(X1,universal_class)
| member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(union(X1,unordered_pair(X1,X1)),union(X1,unordered_pair(X1,X1))))),successor_relation)
| ~ member(union(X1,unordered_pair(X1,X1)),universal_class) ),
inference(rename_variables,[],[i_0_233]) ).
cnf(i_0_405,plain,
( esk6_1(universal_class) != X1
| function(X2)
| esk7_0 != X2
| esk6_1(universal_class) = X1 ),
inference(scs_inference,[],[i_0_264,i_0_241,i_0_361,i_0_372,i_0_249,i_0_198,i_0_289,i_0_213,i_0_211,i_0_293,i_0_270,i_0_365,i_0_359,i_0_380,i_0_237,i_0_212,i_0_205,i_0_174,i_0_183,i_0_227,i_0_226,i_0_228,i_0_178,i_0_175,i_0_229,i_0_230]) ).
cnf(i_0_406,plain,
member(esk6_1(universal_class),unordered_pair(X1,esk6_1(universal_class))),
inference(equality_inference,[],[399]) ).
cnf(i_0_407,plain,
~ inductive(null_class),
inference(scs_inference,[],[i_0_204,i_0_205]) ).
cnf(i_0_408,plain,
~ member(X1,null_class),
inference(rename_variables,[],[i_0_204]) ).
cnf(i_0_409,plain,
( member(null_class,X1)
| ~ inductive(X1) ),
inference(rename_variables,[],[i_0_205]) ).
cnf(i_0_410,plain,
~ member(unordered_pair(X1,X2),esk6_1(universal_class)),
inference(scs_inference,[],[i_0_204,i_0_198,i_0_287,i_0_205,i_0_174]) ).
cnf(i_0_411,plain,
( ~ member(X1,X2)
| ~ disjoint(X3,X2)
| ~ member(X1,X3) ),
inference(rename_variables,[],[i_0_174]) ).
cnf(i_0_412,plain,
~ subclass(unordered_pair(X1,X2),null_class),
inference(scs_inference,[],[i_0_204,i_0_408,i_0_198,i_0_313,i_0_287,i_0_205,i_0_174,i_0_183]) ).
cnf(i_0_413,plain,
~ member(X1,null_class),
inference(rename_variables,[],[i_0_204]) ).
cnf(i_0_414,plain,
( ~ member(X1,X2)
| member(X1,X3)
| ~ subclass(X2,X3) ),
inference(rename_variables,[],[i_0_183]) ).
cnf(i_0_415,plain,
esk2_0 != power_class(X1),
inference(scs_inference,[],[i_0_387,i_0_204,i_0_408,i_0_198,i_0_213,i_0_313,i_0_287,i_0_205,i_0_174,i_0_183,i_0_227]) ).
cnf(i_0_416,plain,
esk6_1(unordered_pair(X1,X2)) != null_class,
inference(scs_inference,[],[i_0_239,i_0_387,i_0_204,i_0_408,i_0_198,i_0_213,i_0_313,i_0_287,i_0_205,i_0_174,i_0_183,i_0_227,i_0_225]) ).
cnf(i_0_417,plain,
~ member(null_class,unordered_pair(X1,X2)),
inference(rename_variables,[],[i_0_239]) ).
cnf(i_0_418,plain,
universal_class != identity_relation,
inference(scs_inference,[],[i_0_239,i_0_387,i_0_204,i_0_408,i_0_198,i_0_211,i_0_213,i_0_313,i_0_287,i_0_356,i_0_205,i_0_174,i_0_183,i_0_227,i_0_225,i_0_226]) ).
cnf(i_0_419,plain,
null_class != power_class(universal_class),
inference(scs_inference,[],[i_0_239,i_0_372,i_0_387,i_0_204,i_0_408,i_0_198,i_0_211,i_0_213,i_0_313,i_0_287,i_0_356,i_0_257,i_0_205,i_0_174,i_0_183,i_0_227,i_0_225,i_0_226,i_0_228]) ).
cnf(i_0_420,plain,
subclass(null_class,X1),
inference(rename_variables,[],[i_0_257]) ).
cnf(i_0_421,plain,
~ member(esk6_1(unordered_pair(null_class,null_class)),power_class(X1)),
inference(scs_inference,[],[i_0_239,i_0_372,i_0_387,i_0_204,i_0_408,i_0_198,i_0_211,i_0_213,i_0_313,i_0_287,i_0_356,i_0_257,i_0_205,i_0_174,i_0_183,i_0_227,i_0_225,i_0_226,i_0_228,i_0_344]) ).
cnf(i_0_422,plain,
( esk6_1(unordered_pair(null_class,X1)) = X1
| ~ member(esk6_1(unordered_pair(null_class,X1)),power_class(X2)) ),
inference(rename_variables,[],[i_0_344]) ).
cnf(i_0_423,plain,
~ member(esk6_1(unordered_pair(null_class,null_class)),domain_of(X1)),
inference(scs_inference,[],[i_0_239,i_0_372,i_0_387,i_0_204,i_0_408,i_0_198,i_0_211,i_0_213,i_0_313,i_0_287,i_0_356,i_0_257,i_0_205,i_0_174,i_0_183,i_0_227,i_0_225,i_0_226,i_0_228,i_0_344,i_0_346]) ).
cnf(i_0_424,plain,
( esk6_1(unordered_pair(null_class,X1)) = X1
| ~ member(esk6_1(unordered_pair(null_class,X1)),domain_of(X2)) ),
inference(rename_variables,[],[i_0_346]) ).
cnf(i_0_425,plain,
~ member(esk6_1(unordered_pair(null_class,null_class)),complement(X1)),
inference(scs_inference,[],[i_0_239,i_0_372,i_0_387,i_0_204,i_0_408,i_0_198,i_0_211,i_0_213,i_0_313,i_0_287,i_0_356,i_0_257,i_0_205,i_0_174,i_0_183,i_0_227,i_0_225,i_0_226,i_0_228,i_0_344,i_0_346,i_0_350]) ).
cnf(i_0_426,plain,
( esk6_1(unordered_pair(null_class,X1)) = X1
| ~ member(esk6_1(unordered_pair(null_class,X1)),complement(X2)) ),
inference(rename_variables,[],[i_0_350]) ).
cnf(i_0_427,plain,
~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(esk6_1(unordered_pair(null_class,null_class)),esk6_1(unordered_pair(null_class,null_class))))),compose(X2,X3)),
inference(scs_inference,[],[i_0_239,i_0_372,i_0_387,i_0_204,i_0_408,i_0_198,i_0_211,i_0_213,i_0_313,i_0_287,i_0_356,i_0_257,i_0_205,i_0_174,i_0_183,i_0_227,i_0_225,i_0_226,i_0_228,i_0_344,i_0_346,i_0_350,i_0_348]) ).
cnf(i_0_428,plain,
( esk6_1(unordered_pair(null_class,X1)) = X1
| ~ member(unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(esk6_1(unordered_pair(null_class,X1)),esk6_1(unordered_pair(null_class,X1))))),compose(X3,X4)) ),
inference(rename_variables,[],[i_0_348]) ).
cnf(i_0_429,plain,
$false,
inference(scs_inference,[],[i_0_239,i_0_372,i_0_387,i_0_204,i_0_408,i_0_198,i_0_211,i_0_213,i_0_313,i_0_287,i_0_356,i_0_257,i_0_205,i_0_174,i_0_183,i_0_227,i_0_225,i_0_226,i_0_228,i_0_344,i_0_346,i_0_350,i_0_348,i_0_334]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SET065+1 : TPTP v9.2.1. Bugfixed v5.4.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.15/0.32 % Computer : n022.cluster.edu
% 0.15/0.32 % Model : x86_64 x86_64
% 0.15/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.32 % Memory : 8042.1875MB
% 0.15/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.32 % CPULimit : 300
% 0.15/0.33 % WCLimit : 300
% 0.15/0.33 % DateTime : Tue May 5 02:08:21 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.34 % start to proof: theBenchmark
% 0.40/1.61 % Version : CSE_E---1.7
% 0.40/1.61 % Problem : theBenchmark.p
% 0.40/1.61 % SZS status Theorem for theBenchmark.p
% 0.40/1.61 % SZS output start CNFRefutation
% See solution above
% 0.84/2.10 % Total time : 1.271s
%------------------------------------------------------------------------------