%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SET121-7 : TPTP v9.2.1. Bugfixed v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : 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:07:23 PM UTC 2026
% Result : Unsatisfiable 261.11s 196.70s
% Output : CNFRefutation 273.81s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named c_0_167)
% Comments :
%------------------------------------------------------------------------------
cnf(image,axiom,
range_of(restrict(X1,X2,universal_class)) = image(X1,X2),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',image) ).
cnf(range_of,axiom,
domain_of(inverse(X1)) = range_of(X1),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',range_of) ).
cnf(restriction1,axiom,
intersection(X1,cross_product(X2,X3)) = restrict(X1,X2,X3),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',restriction1) ).
cnf(apply,axiom,
sum_class(image(X1,singleton(X2))) = apply(X1,X2),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',apply) ).
cnf(singleton_set,axiom,
unordered_pair(X1,X1) = singleton(X1),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',singleton_set) ).
cnf(sum_class_definition,axiom,
domain_of(restrict(element_relation,universal_class,X1)) = sum_class(X1),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',sum_class_definition) ).
cnf(ordered_pair,axiom,
unordered_pair(singleton(X1),unordered_pair(X1,singleton(X2))) = ordered_pair(X1,X2),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',ordered_pair) ).
cnf(power_class_definition,axiom,
complement(image(element_relation,complement(X1))) = power_class(X1),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',power_class_definition) ).
cnf(inverse,axiom,
domain_of(flip(cross_product(X1,universal_class))) = inverse(X1),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',inverse) ).
cnf(successor,axiom,
union(X1,singleton(X1)) = successor(X1),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',successor) ).
cnf(homomorphism6,axiom,
( homomorphism(X3,X1,X2)
| ~ operation(X1)
| ~ operation(X2)
| ~ compatible(X3,X1,X2)
| apply(X2,ordered_pair(apply(X3,not_homomorphism1(X3,X1,X2)),apply(X3,not_homomorphism2(X3,X1,X2)))) != apply(X3,apply(X1,ordered_pair(not_homomorphism1(X3,X1,X2),not_homomorphism2(X3,X1,X2)))) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',homomorphism6) ).
cnf(homomorphism4,axiom,
( apply(X3,ordered_pair(apply(X1,X4),apply(X1,X5))) = apply(X1,apply(X2,ordered_pair(X4,X5)))
| ~ homomorphism(X1,X2,X3)
| ~ member(ordered_pair(X4,X5),domain_of(X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',homomorphism4) ).
cnf(compose3,axiom,
( member(ordered_pair(X4,X1),compose(X2,X3))
| ~ member(X1,image(X2,image(X3,singleton(X4))))
| ~ member(ordered_pair(X4,X1),cross_product(universal_class,universal_class)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',compose3) ).
cnf(compose2,axiom,
( member(X2,image(X3,image(X4,singleton(X1))))
| ~ member(ordered_pair(X1,X2),compose(X3,X4)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',compose2) ).
cnf(choice2,axiom,
( X1 = null_class
| member(apply(choice,X1),X1)
| ~ member(X1,universal_class) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',choice2) ).
cnf(existence_of_1st_and_2nd_1,axiom,
( member(ordered_pair(first(ordered_pair(X1,X2)),second(ordered_pair(X1,X2))),cross_product(universal_class,universal_class))
| ~ member(ordered_pair(X1,X2),cross_product(universal_class,universal_class)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_of_1st_and_2nd_1) ).
cnf(flip3,axiom,
( member(ordered_pair(ordered_pair(X2,X1),X3),flip(X4))
| ~ member(ordered_pair(ordered_pair(X1,X2),X3),X4)
| ~ member(ordered_pair(ordered_pair(X2,X1),X3),cross_product(cross_product(universal_class,universal_class),universal_class)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',flip3) ).
cnf(rotate3,axiom,
( member(ordered_pair(ordered_pair(X3,X1),X2),rotate(X4))
| ~ member(ordered_pair(ordered_pair(X1,X2),X3),X4)
| ~ member(ordered_pair(ordered_pair(X3,X1),X2),cross_product(cross_product(universal_class,universal_class),universal_class)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',rotate3) ).
cnf(flip2,axiom,
( member(ordered_pair(ordered_pair(X2,X1),X3),X4)
| ~ member(ordered_pair(ordered_pair(X1,X2),X3),flip(X4)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',flip2) ).
cnf(rotate2,axiom,
( member(ordered_pair(ordered_pair(X2,X3),X1),X4)
| ~ member(ordered_pair(ordered_pair(X1,X2),X3),rotate(X4)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',rotate2) ).
cnf(power_class2,axiom,
( member(power_class(X1),universal_class)
| ~ member(X1,universal_class) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',power_class2) ).
cnf(homomorphism5,axiom,
( member(ordered_pair(not_homomorphism1(X3,X1,X2),not_homomorphism2(X3,X1,X2)),domain_of(X1))
| homomorphism(X3,X1,X2)
| ~ operation(X1)
| ~ operation(X2)
| ~ compatible(X3,X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',homomorphism5) ).
cnf(inductive3,axiom,
( inductive(X1)
| ~ member(null_class,X1)
| ~ subclass(image(successor_relation,X1),X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',inductive3) ).
cnf(cantor_class,axiom,
intersection(domain_of(X1),diagonalise(compose(inverse(element_relation),X1))) = cantor(X1),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',cantor_class) ).
cnf(diagonalisation,axiom,
complement(domain_of(intersection(X1,identity_relation))) = diagonalise(X1),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',diagonalisation) ).
cnf(number_of_elements_in_class,axiom,
( member(not_subclass_element(intersection(complement(singleton(not_subclass_element(X1,null_class))),X1),null_class),intersection(complement(singleton(not_subclass_element(X1,null_class))),X1))
| singleton(not_subclass_element(X1,null_class)) = X1
| X1 = null_class ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',number_of_elements_in_class) ).
cnf(replacement,axiom,
( member(image(X1,X2),universal_class)
| ~ function(X1)
| ~ member(X2,universal_class) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',replacement) ).
cnf(inductive2,axiom,
( subclass(image(successor_relation,X1),X1)
| ~ inductive(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',inductive2) ).
cnf(corollary_2_to_number_of_elements_in_class,axiom,
( member(not_subclass_element(intersection(complement(singleton(not_subclass_element(X1,null_class))),X1),null_class),X1)
| singleton(not_subclass_element(X1,null_class)) = X1
| X1 = null_class ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',corollary_2_to_number_of_elements_in_class) ).
cnf(subset_relation,axiom,
intersection(cross_product(universal_class,universal_class),intersection(cross_product(universal_class,universal_class),complement(compose(complement(element_relation),inverse(element_relation))))) = subset_relation,
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',subset_relation) ).
cnf(successor_relation3,axiom,
( member(ordered_pair(X1,X2),successor_relation)
| successor(X1) != X2
| ~ member(ordered_pair(X1,X2),cross_product(universal_class,universal_class)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',successor_relation3) ).
cnf(union,axiom,
complement(intersection(complement(X1),complement(X2))) = union(X1,X2),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',union) ).
cnf(corollary_1_to_number_of_elements_in_class,axiom,
( singleton(not_subclass_element(X1,null_class)) = X1
| X1 = null_class
| not_subclass_element(intersection(complement(singleton(not_subclass_element(X1,null_class))),X1),null_class) != not_subclass_element(X1,null_class) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',corollary_1_to_number_of_elements_in_class) ).
cnf(element_relation3,axiom,
( member(ordered_pair(X1,X2),element_relation)
| ~ member(ordered_pair(X1,X2),cross_product(universal_class,universal_class))
| ~ member(X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',element_relation3) ).
cnf(unique_1st_and_2nd_in_pair_of_sets2,axiom,
( second(ordered_pair(X1,X2)) = X2
| ~ member(ordered_pair(X1,X2),cross_product(universal_class,universal_class)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unique_1st_and_2nd_in_pair_of_sets2) ).
cnf(unique_1st_and_2nd_in_pair_of_sets1,axiom,
( first(ordered_pair(X1,X2)) = X1
| ~ member(ordered_pair(X1,X2),cross_product(universal_class,universal_class)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unique_1st_and_2nd_in_pair_of_sets1) ).
cnf(successor_relation2,axiom,
( successor(X1) = X2
| ~ member(ordered_pair(X1,X2),successor_relation) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',successor_relation2) ).
cnf(operation4,axiom,
( operation(X1)
| ~ function(X1)
| cross_product(domain_of(domain_of(X1)),domain_of(domain_of(X1))) != domain_of(X1)
| ~ subclass(range_of(X1),domain_of(domain_of(X1))) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',operation4) ).
cnf(compatible4,axiom,
( compatible(X1,X2,X3)
| ~ function(X1)
| domain_of(domain_of(X2)) != domain_of(X1)
| ~ subclass(range_of(X1),domain_of(domain_of(X3))) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',compatible4) ).
cnf(corollary_1_to_unordered_pair,axiom,
( member(X1,unordered_pair(X1,X2))
| ~ member(ordered_pair(X1,X2),cross_product(X3,X4)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',corollary_1_to_unordered_pair) ).
cnf(corollary_2_to_unordered_pair,axiom,
( member(X2,unordered_pair(X1,X2))
| ~ member(ordered_pair(X1,X2),cross_product(X3,X4)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',corollary_2_to_unordered_pair) ).
cnf(right_cancellation,axiom,
( X1 = X3
| unordered_pair(X1,X2) != unordered_pair(X3,X2)
| ~ member(ordered_pair(X1,X3),cross_product(universal_class,universal_class)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',right_cancellation) ).
cnf(left_cancellation,axiom,
( X2 = X3
| unordered_pair(X1,X2) != unordered_pair(X1,X3)
| ~ member(ordered_pair(X2,X3),cross_product(universal_class,universal_class)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',left_cancellation) ).
cnf(function3,axiom,
( function(X1)
| ~ subclass(X1,cross_product(universal_class,universal_class))
| ~ subclass(compose(X1,inverse(X1)),identity_relation) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',function3) ).
cnf(prove_corollary_1_to_OP_determines_components2_2,negated_conjecture,
first(ordered_pair(x,y)) != ordered_pair(x,y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_corollary_1_to_OP_determines_components2_2) ).
cnf(corollary_to_unordered_pair_axiom3,axiom,
( ~ member(ordered_pair(X1,X2),cross_product(X3,X4))
| unordered_pair(X1,X2) != null_class ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',corollary_to_unordered_pair_axiom3) ).
cnf(cartesian_product1,axiom,
( member(X1,X3)
| ~ member(ordered_pair(X1,X2),cross_product(X3,X4)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',cartesian_product1) ).
cnf(cartesian_product2,axiom,
( member(X2,X4)
| ~ member(ordered_pair(X1,X2),cross_product(X3,X4)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',cartesian_product2) ).
cnf(unique_1st_and_2nd_in_pair_of_non_sets2,axiom,
( member(ordered_pair(first(X1),second(X1)),cross_product(universal_class,universal_class))
| second(X1) = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unique_1st_and_2nd_in_pair_of_non_sets2) ).
cnf(existence_of_1st_and_2nd_3,axiom,
( member(ordered_pair(first(X1),second(X1)),cross_product(universal_class,universal_class))
| second(X1) = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_of_1st_and_2nd_3) ).
cnf(unique_1st_and_2nd_in_pair_of_non_sets1,axiom,
( member(ordered_pair(first(X1),second(X1)),cross_product(universal_class,universal_class))
| first(X1) = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unique_1st_and_2nd_in_pair_of_non_sets1) ).
cnf(existence_of_1st_and_2nd_2,axiom,
( member(ordered_pair(first(X1),second(X1)),cross_product(universal_class,universal_class))
| first(X1) = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_of_1st_and_2nd_2) ).
cnf(corollary_1_to_cartesian_product,axiom,
( member(X1,universal_class)
| ~ member(ordered_pair(X1,X2),cross_product(X3,X4)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',corollary_1_to_cartesian_product) ).
cnf(corollary_2_to_cartesian_product,axiom,
( member(X2,universal_class)
| ~ member(ordered_pair(X1,X2),cross_product(X3,X4)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',corollary_2_to_cartesian_product) ).
cnf(single_valued_class2,axiom,
( single_valued_class(X1)
| ~ subclass(compose(X1,inverse(X1)),identity_relation) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',single_valued_class2) ).
cnf(element_relation2,axiom,
( member(X1,X2)
| ~ member(ordered_pair(X1,X2),element_relation) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',element_relation2) ).
cnf(ordered_pair_determines_components1,axiom,
( X1 = X3
| ordered_pair(X1,X2) != ordered_pair(X3,X4)
| ~ member(X1,universal_class) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ordered_pair_determines_components1) ).
cnf(ordered_pair_determines_components2,axiom,
( X2 = X4
| ordered_pair(X1,X2) != ordered_pair(X3,X4)
| ~ member(X2,universal_class) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ordered_pair_determines_components2) ).
cnf(corollary_2_to_ordered_pair_determines_components1,axiom,
( member(X1,universal_class)
| second(ordered_pair(X1,X2)) = ordered_pair(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',corollary_2_to_ordered_pair_determines_components1) ).
cnf(corollary_1_to_ordered_pair_determines_components1,axiom,
( member(X1,universal_class)
| first(ordered_pair(X1,X2)) = ordered_pair(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',corollary_1_to_ordered_pair_determines_components1) ).
cnf(compatible3,axiom,
( subclass(range_of(X1),domain_of(domain_of(X3)))
| ~ compatible(X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',compatible3) ).
cnf(corollary_1_to_ordered_pairs_are_sets,axiom,
( member(X1,universal_class)
| ordered_pair(first(X1),second(X1)) != X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',corollary_1_to_ordered_pairs_are_sets) ).
cnf(unordered_pair_member_of_ordered_pair,axiom,
member(unordered_pair(X1,singleton(X2)),ordered_pair(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unordered_pair_member_of_ordered_pair) ).
cnf(cartesian_product3,axiom,
( member(ordered_pair(X1,X3),cross_product(X2,X4))
| ~ member(X1,X2)
| ~ member(X3,X4) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',cartesian_product3) ).
cnf(property_2_of_ordered_pair,axiom,
( unordered_pair(null_class,singleton(singleton(X1))) = ordered_pair(X2,X1)
| member(X2,universal_class)
| ~ member(X1,universal_class) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',property_2_of_ordered_pair) ).
cnf(unordered_pairs_and_singletons,axiom,
unordered_pair(X1,X2) = union(singleton(X1),singleton(X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unordered_pairs_and_singletons) ).
cnf(singleton_member_of_ordered_pair,axiom,
member(singleton(X1),ordered_pair(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',singleton_member_of_ordered_pair) ).
cnf(cartesian_product4,axiom,
( ordered_pair(first(X1),second(X1)) = X1
| ~ member(X1,cross_product(X2,X3)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',cartesian_product4) ).
cnf(operation3,axiom,
( subclass(range_of(X1),domain_of(domain_of(X1)))
| ~ operation(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',operation3) ).
cnf(function2,axiom,
( subclass(compose(X1,inverse(X1)),identity_relation)
| ~ function(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',function2) ).
cnf(single_valued_class1,axiom,
( subclass(compose(X1,inverse(X1)),identity_relation)
| ~ single_valued_class(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',single_valued_class1) ).
cnf(ordered_pair_is_set,axiom,
member(ordered_pair(X1,X2),universal_class),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ordered_pair_is_set) ).
cnf(unique_1st_and_2nd_in_pair_of_non_sets4,axiom,
( ordered_pair(first(X1),second(X1)) = X1
| second(X1) = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unique_1st_and_2nd_in_pair_of_non_sets4) ).
cnf(existence_of_1st_and_2nd_5,axiom,
( ordered_pair(first(X1),second(X1)) = X1
| second(X1) = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_of_1st_and_2nd_5) ).
cnf(unique_1st_and_2nd_in_pair_of_non_sets3,axiom,
( ordered_pair(first(X1),second(X1)) = X1
| first(X1) = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unique_1st_and_2nd_in_pair_of_non_sets3) ).
cnf(existence_of_1st_and_2nd_4,axiom,
( ordered_pair(first(X1),second(X1)) = X1
| first(X1) = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_of_1st_and_2nd_4) ).
cnf(property_1_of_ordered_pair,axiom,
( unordered_pair(singleton(X1),unordered_pair(X1,null_class)) = ordered_pair(X1,X2)
| member(X2,universal_class) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',property_1_of_ordered_pair) ).
cnf(one_to_one3,axiom,
( one_to_one(X1)
| ~ function(inverse(X1))
| ~ function(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',one_to_one3) ).
cnf(sum_class2,axiom,
( member(sum_class(X1),universal_class)
| ~ member(X1,universal_class) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',sum_class2) ).
cnf(property_3_of_ordered_pair,axiom,
( unordered_pair(null_class,singleton(null_class)) = ordered_pair(X1,X2)
| member(X1,universal_class)
| member(X2,universal_class) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',property_3_of_ordered_pair) ).
cnf(domain1,axiom,
( restrict(X1,singleton(X2),universal_class) != null_class
| ~ member(X2,domain_of(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',domain1) ).
cnf(member_exists2,axiom,
( singleton(member_of(singleton(X1))) = singleton(X1)
| ~ member(X1,universal_class) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',member_exists2) ).
cnf(domain2,axiom,
( restrict(X2,singleton(X1),universal_class) = null_class
| member(X1,domain_of(X2))
| ~ member(X1,universal_class) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',domain2) ).
cnf(one_to_one2,axiom,
( function(inverse(X1))
| ~ one_to_one(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',one_to_one2) ).
cnf(corollary_1_to_singletons_are_sets,axiom,
member(singleton(X1),unordered_pair(X2,singleton(X1))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',corollary_1_to_singletons_are_sets) ).
cnf(identity_relation,axiom,
intersection(inverse(subset_relation),subset_relation) = identity_relation,
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',identity_relation) ).
cnf(member_exists1,axiom,
( member(member_of(singleton(X1)),universal_class)
| ~ member(X1,universal_class) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',member_exists1) ).
cnf(two_subsets_of_singleton,axiom,
( X1 = null_class
| singleton(X2) = X1
| ~ subclass(X1,singleton(X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',two_subsets_of_singleton) ).
cnf(restriction2,axiom,
intersection(cross_product(X1,X2),X3) = restrict(X3,X1,X2),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',restriction2) ).
cnf(property_of_singletons1,axiom,
( member_of(X1) = X2
| singleton(member_of(X1)) != X1
| ~ member(X2,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',property_of_singletons1) ).
cnf(singleton_in_unordered_pair3,axiom,
( X3 = X1
| X3 = X2
| unordered_pair(X1,X2) != singleton(X3)
| ~ member(X3,universal_class) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',singleton_in_unordered_pair3) ).
cnf(singleton_identified_by_element1,axiom,
( X1 = X2
| singleton(X1) != singleton(X2)
| ~ member(X1,universal_class) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',singleton_identified_by_element1) ).
cnf(singleton_identified_by_element2,axiom,
( X1 = X2
| singleton(X1) != singleton(X2)
| ~ member(X2,universal_class) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',singleton_identified_by_element2) ).
cnf(singleton_in_unordered_pair1,axiom,
subclass(singleton(X1),unordered_pair(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',singleton_in_unordered_pair1) ).
cnf(singleton_in_unordered_pair2,axiom,
subclass(singleton(X1),unordered_pair(X2,X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',singleton_in_unordered_pair2) ).
cnf(only_member_in_singleton,axiom,
( X1 = X2
| ~ member(X1,singleton(X2)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',only_member_in_singleton) ).
cnf(property_of_singletons2,axiom,
( subclass(singleton(X1),X2)
| ~ member(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',property_of_singletons2) ).
cnf(set_in_its_singleton,axiom,
( member(X1,singleton(X1))
| ~ member(X1,universal_class) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',set_in_its_singleton) ).
cnf(corollary_2_to_singletons_are_sets,axiom,
( member(X1,universal_class)
| singleton(member_of(X1)) != X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',corollary_2_to_singletons_are_sets) ).
cnf(member_of_singleton_is_unique,axiom,
( member_of(singleton(X1)) = X1
| ~ member(X1,universal_class) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',member_of_singleton_is_unique) ).
cnf(corollary_to_set_in_its_singleton,axiom,
( ~ member(X1,universal_class)
| singleton(X1) != null_class ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',corollary_to_set_in_its_singleton) ).
cnf(unordered_pair_equals_singleton2,axiom,
( member(X1,universal_class)
| unordered_pair(X1,X2) = singleton(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unordered_pair_equals_singleton2) ).
cnf(unordered_pair_equals_singleton1,axiom,
( member(X1,universal_class)
| unordered_pair(X2,X1) = singleton(X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unordered_pair_equals_singleton1) ).
cnf(singletons_are_sets,axiom,
member(singleton(X1),universal_class),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',singletons_are_sets) ).
cnf(member_of_non_singleton_unique2,axiom,
( singleton(member_of1(X1)) = X1
| member_of(X1) = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',member_of_non_singleton_unique2) ).
cnf(member_exists4,axiom,
( singleton(member_of(X1)) = X1
| member_of(X1) = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',member_exists4) ).
cnf(null_class_in_its_singleton,axiom,
member(null_class,singleton(null_class)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',null_class_in_its_singleton) ).
cnf(singleton_is_null_class,axiom,
( member(X1,universal_class)
| singleton(X1) = null_class ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',singleton_is_null_class) ).
cnf(homomorphism3,axiom,
( compatible(X1,X2,X3)
| ~ homomorphism(X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',homomorphism3) ).
cnf(equality4,axiom,
( X1 = X2
| ~ member(not_subclass_element(X1,X2),X2)
| ~ member(not_subclass_element(X2,X1),X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',equality4) ).
cnf(equality3,axiom,
( X2 = X1
| member(not_subclass_element(X2,X1),X2)
| ~ member(not_subclass_element(X1,X2),X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',equality3) ).
cnf(equality2,axiom,
( X1 = X2
| member(not_subclass_element(X2,X1),X2)
| ~ member(not_subclass_element(X1,X2),X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',equality2) ).
cnf(compatible2,axiom,
( domain_of(domain_of(X2)) = domain_of(X1)
| ~ compatible(X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',compatible2) ).
cnf(homomorphism1,axiom,
( operation(X2)
| ~ homomorphism(X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',homomorphism1) ).
cnf(homomorphism2,axiom,
( operation(X3)
| ~ homomorphism(X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',homomorphism2) ).
cnf(compatible1,axiom,
( function(X1)
| ~ compatible(X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',compatible1) ).
cnf(unordered_pair_is_subset,axiom,
( subclass(unordered_pair(X1,X3),X2)
| ~ member(X1,X2)
| ~ member(X3,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',unordered_pair_is_subset) ).
cnf(intersection3,axiom,
( member(X1,intersection(X2,X3))
| ~ member(X1,X2)
| ~ member(X1,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',intersection3) ).
cnf(equality1,axiom,
( X1 = X2
| member(not_subclass_element(X1,X2),X1)
| member(not_subclass_element(X2,X1),X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',equality1) ).
cnf(flip1,axiom,
subclass(flip(X1),cross_product(cross_product(universal_class,universal_class),universal_class)),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',flip1) ).
cnf(rotate1,axiom,
subclass(rotate(X1),cross_product(cross_product(universal_class,universal_class),universal_class)),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',rotate1) ).
cnf(special_classes_lemma,axiom,
~ member(X1,intersection(complement(X2),X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',special_classes_lemma) ).
cnf(not_subclass_members2,axiom,
( subclass(X1,X2)
| ~ member(not_subclass_element(X1,X2),X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',not_subclass_members2) ).
cnf(intersection1,axiom,
( member(X1,X2)
| ~ member(X1,intersection(X2,X3)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',intersection1) ).
cnf(intersection2,axiom,
( member(X1,X3)
| ~ member(X1,intersection(X2,X3)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',intersection2) ).
cnf(unordered_pair_member,axiom,
( X1 = X2
| X1 = X3
| ~ member(X1,unordered_pair(X2,X3)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',unordered_pair_member) ).
cnf(corollary_12to_ordered_pairs_are_sets,axiom,
( member(X1,universal_class)
| ~ member(X1,cross_product(universal_class,universal_class)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',corollary_12to_ordered_pairs_are_sets) ).
cnf(operation2,axiom,
( cross_product(domain_of(domain_of(X1)),domain_of(domain_of(X1))) = domain_of(X1)
| ~ operation(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',operation2) ).
cnf(unordered_pair2,axiom,
( member(X1,unordered_pair(X1,X2))
| ~ member(X1,universal_class) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',unordered_pair2) ).
cnf(unordered_pair3,axiom,
( member(X1,unordered_pair(X2,X1))
| ~ member(X1,universal_class) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',unordered_pair3) ).
cnf(compose1,axiom,
subclass(compose(X1,X2),cross_product(universal_class,universal_class)),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',compose1) ).
cnf(subclass_members,axiom,
( member(X3,X2)
| ~ subclass(X1,X2)
| ~ member(X3,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',subclass_members) ).
cnf(transitivity_of_subclass,axiom,
( subclass(X1,X3)
| ~ subclass(X1,X2)
| ~ subclass(X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',transitivity_of_subclass) ).
cnf(complement2,axiom,
( member(X1,complement(X2))
| member(X1,X2)
| ~ member(X1,universal_class) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',complement2) ).
cnf(complement1,axiom,
( ~ member(X1,complement(X2))
| ~ member(X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',complement1) ).
cnf(not_subclass_members1,axiom,
( member(not_subclass_element(X1,X2),X1)
| subclass(X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',not_subclass_members1) ).
cnf(subclass_implies_equal,axiom,
( X1 = X2
| ~ subclass(X1,X2)
| ~ subclass(X2,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',subclass_implies_equal) ).
cnf(corollary_to_unordered_pair_axiom1,axiom,
( ~ member(X1,universal_class)
| unordered_pair(X1,X2) != null_class ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',corollary_to_unordered_pair_axiom1) ).
cnf(corollary_to_unordered_pair_axiom2,axiom,
( ~ member(X1,universal_class)
| unordered_pair(X2,X1) != null_class ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',corollary_to_unordered_pair_axiom2) ).
cnf(function1,axiom,
( subclass(X1,cross_product(universal_class,universal_class))
| ~ function(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',function1) ).
cnf(null_unordered_pair,axiom,
( unordered_pair(X1,X2) = null_class
| member(X1,universal_class)
| member(X2,universal_class) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',null_unordered_pair) ).
cnf(null_class_is_unique,axiom,
( X1 = null_class
| member(not_subclass_element(X1,null_class),X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',null_class_is_unique) ).
cnf(unordered_pairs_in_universal,axiom,
member(unordered_pair(X1,X2),universal_class),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',unordered_pairs_in_universal) ).
cnf(successor_relation1,axiom,
subclass(successor_relation,cross_product(universal_class,universal_class)),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',successor_relation1) ).
cnf(element_relation1,axiom,
subclass(element_relation,cross_product(universal_class,universal_class)),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',element_relation1) ).
cnf(commutativity_of_unordered_pair,axiom,
unordered_pair(X1,X2) = unordered_pair(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_of_unordered_pair) ).
cnf(member_of_non_singleton_unique1,axiom,
( member(member_of1(X1),universal_class)
| member_of(X1) = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',member_of_non_singleton_unique1) ).
cnf(member_exists3,axiom,
( member(member_of(X1),universal_class)
| member_of(X1) = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',member_exists3) ).
cnf(regularity1,axiom,
( X1 = null_class
| member(regular(X1),X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',regularity1) ).
cnf(regularity2,axiom,
( X1 = null_class
| intersection(X1,regular(X1)) = null_class ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',regularity2) ).
cnf(corollary_of_null_class_is_subclass,axiom,
( X1 = null_class
| ~ subclass(X1,null_class) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',corollary_of_null_class_is_subclass) ).
cnf(existence_of_null_class,axiom,
~ member(X1,null_class),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',existence_of_null_class) ).
cnf(inductive1,axiom,
( member(null_class,X1)
| ~ inductive(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',inductive1) ).
cnf(omega_is_inductive2,axiom,
( subclass(omega,X1)
| ~ inductive(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',omega_is_inductive2) ).
cnf(equal_implies_subclass1,axiom,
( subclass(X1,X2)
| X1 != X2 ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',equal_implies_subclass1) ).
cnf(equal_implies_subclass2,axiom,
( subclass(X2,X1)
| X1 != X2 ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',equal_implies_subclass2) ).
cnf(prove_corollary_1_to_OP_determines_components2_1,negated_conjecture,
~ member(y,universal_class),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_corollary_1_to_OP_determines_components2_1) ).
cnf(subclass_is_reflexive,axiom,
subclass(X1,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',subclass_is_reflexive) ).
cnf(null_class_is_subclass,axiom,
subclass(null_class,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',null_class_is_subclass) ).
cnf(class_elements_are_sets,axiom,
subclass(X1,universal_class),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',class_elements_are_sets) ).
cnf(operation1,axiom,
( function(X1)
| ~ operation(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',operation1) ).
cnf(one_to_one1,axiom,
( function(X1)
| ~ one_to_one(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',one_to_one1) ).
cnf(omega_in_universal,axiom,
member(omega,universal_class),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',omega_in_universal) ).
cnf(null_class_is_a_set,axiom,
member(null_class,universal_class),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',null_class_is_a_set) ).
cnf(choice1,axiom,
function(choice),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',choice1) ).
cnf(omega_is_inductive1,axiom,
inductive(omega),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',omega_is_inductive1) ).
cnf(i_0_166,axiom,
range_of(restrict(X1,X2,universal_class)) = image(X1,X2),
image ).
cnf(i_0_167,axiom,
domain_of(inverse(X1)) = range_of(X1),
range_of ).
cnf(i_0_168,axiom,
intersection(X1,cross_product(X2,X3)) = restrict(X1,X2,X3),
restriction1 ).
cnf(i_0_169,axiom,
sum_class(image(X1,singleton(X2))) = apply(X1,X2),
apply ).
cnf(i_0_170,axiom,
unordered_pair(X1,X1) = singleton(X1),
singleton_set ).
cnf(i_0_171,axiom,
domain_of(restrict(element_relation,universal_class,X1)) = sum_class(X1),
sum_class_definition ).
cnf(i_0_172,axiom,
unordered_pair(singleton(X1),unordered_pair(X1,singleton(X2))) = ordered_pair(X1,X2),
ordered_pair ).
cnf(i_0_173,axiom,
complement(image(element_relation,complement(X1))) = power_class(X1),
power_class_definition ).
cnf(i_0_174,plain,
domain_of(inverse(intersection(X1,cross_product(X2,universal_class)))) = image(X1,X2),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_166,c_0_167]),c_0_168]) ).
cnf(i_0_175,axiom,
domain_of(flip(cross_product(X1,universal_class))) = inverse(X1),
inverse ).
cnf(i_0_176,axiom,
union(X1,singleton(X1)) = successor(X1),
successor ).
cnf(i_0_177,axiom,
( homomorphism(X3,X1,X2)
| ~ operation(X1)
| ~ operation(X2)
| ~ compatible(X3,X1,X2)
| apply(X2,ordered_pair(apply(X3,not_homomorphism1(X3,X1,X2)),apply(X3,not_homomorphism2(X3,X1,X2)))) != apply(X3,apply(X1,ordered_pair(not_homomorphism1(X3,X1,X2),not_homomorphism2(X3,X1,X2)))) ),
homomorphism6 ).
cnf(i_0_178,plain,
sum_class(image(X1,unordered_pair(X2,X2))) = apply(X1,X2),
inference(rw,[status(thm)],[i_0_169,c_0_170]) ).
cnf(i_0_179,plain,
domain_of(intersection(element_relation,cross_product(universal_class,X1))) = sum_class(X1),
inference(rw,[status(thm)],[i_0_171,c_0_168]) ).
cnf(i_0_180,plain,
unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))) = ordered_pair(X1,X2),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_172,c_0_170]),c_0_170]) ).
cnf(i_0_181,axiom,
( apply(X3,ordered_pair(apply(X1,X4),apply(X1,X5))) = apply(X1,apply(X2,ordered_pair(X4,X5)))
| ~ homomorphism(X1,X2,X3)
| ~ member(ordered_pair(X4,X5),domain_of(X2)) ),
homomorphism4 ).
cnf(i_0_182,axiom,
( member(ordered_pair(X4,X1),compose(X2,X3))
| ~ member(X1,image(X2,image(X3,singleton(X4))))
| ~ member(ordered_pair(X4,X1),cross_product(universal_class,universal_class)) ),
compose3 ).
cnf(i_0_183,axiom,
( member(X2,image(X3,image(X4,singleton(X1))))
| ~ member(ordered_pair(X1,X2),compose(X3,X4)) ),
compose2 ).
cnf(i_0_184,axiom,
( X1 = null_class
| member(apply(choice,X1),X1)
| ~ member(X1,universal_class) ),
choice2 ).
cnf(i_0_185,axiom,
( member(ordered_pair(first(ordered_pair(X1,X2)),second(ordered_pair(X1,X2))),cross_product(universal_class,universal_class))
| ~ member(ordered_pair(X1,X2),cross_product(universal_class,universal_class)) ),
existence_of_1st_and_2nd_1 ).
cnf(i_0_186,axiom,
( member(ordered_pair(ordered_pair(X2,X1),X3),flip(X4))
| ~ member(ordered_pair(ordered_pair(X1,X2),X3),X4)
| ~ member(ordered_pair(ordered_pair(X2,X1),X3),cross_product(cross_product(universal_class,universal_class),universal_class)) ),
flip3 ).
cnf(i_0_187,axiom,
( member(ordered_pair(ordered_pair(X3,X1),X2),rotate(X4))
| ~ member(ordered_pair(ordered_pair(X1,X2),X3),X4)
| ~ member(ordered_pair(ordered_pair(X3,X1),X2),cross_product(cross_product(universal_class,universal_class),universal_class)) ),
rotate3 ).
cnf(i_0_188,axiom,
( member(ordered_pair(ordered_pair(X2,X1),X3),X4)
| ~ member(ordered_pair(ordered_pair(X1,X2),X3),flip(X4)) ),
flip2 ).
cnf(i_0_189,axiom,
( member(ordered_pair(ordered_pair(X2,X3),X1),X4)
| ~ member(ordered_pair(ordered_pair(X1,X2),X3),rotate(X4)) ),
rotate2 ).
cnf(i_0_190,axiom,
( member(power_class(X1),universal_class)
| ~ member(X1,universal_class) ),
power_class2 ).
cnf(i_0_191,plain,
complement(domain_of(domain_of(flip(cross_product(intersection(element_relation,cross_product(complement(X1),universal_class)),universal_class))))) = power_class(X1),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_173,c_0_174]),c_0_175]) ).
cnf(i_0_192,axiom,
( member(ordered_pair(not_homomorphism1(X3,X1,X2),not_homomorphism2(X3,X1,X2)),domain_of(X1))
| homomorphism(X3,X1,X2)
| ~ operation(X1)
| ~ operation(X2)
| ~ compatible(X3,X1,X2) ),
homomorphism5 ).
cnf(i_0_193,axiom,
( inductive(X1)
| ~ member(null_class,X1)
| ~ subclass(image(successor_relation,X1),X1) ),
inductive3 ).
cnf(i_0_194,axiom,
intersection(domain_of(X1),diagonalise(compose(inverse(element_relation),X1))) = cantor(X1),
cantor_class ).
cnf(i_0_195,axiom,
complement(domain_of(intersection(X1,identity_relation))) = diagonalise(X1),
diagonalisation ).
cnf(i_0_196,axiom,
( member(not_subclass_element(intersection(complement(singleton(not_subclass_element(X1,null_class))),X1),null_class),intersection(complement(singleton(not_subclass_element(X1,null_class))),X1))
| singleton(not_subclass_element(X1,null_class)) = X1
| X1 = null_class ),
number_of_elements_in_class ).
cnf(i_0_197,axiom,
( member(image(X1,X2),universal_class)
| ~ function(X1)
| ~ member(X2,universal_class) ),
replacement ).
cnf(i_0_198,axiom,
( subclass(image(successor_relation,X1),X1)
| ~ inductive(X1) ),
inductive2 ).
cnf(i_0_199,axiom,
( member(not_subclass_element(intersection(complement(singleton(not_subclass_element(X1,null_class))),X1),null_class),X1)
| singleton(not_subclass_element(X1,null_class)) = X1
| X1 = null_class ),
corollary_2_to_number_of_elements_in_class ).
cnf(i_0_200,axiom,
intersection(cross_product(universal_class,universal_class),intersection(cross_product(universal_class,universal_class),complement(compose(complement(element_relation),inverse(element_relation))))) = subset_relation,
subset_relation ).
cnf(i_0_201,axiom,
( member(ordered_pair(X1,X2),successor_relation)
| successor(X1) != X2
| ~ member(ordered_pair(X1,X2),cross_product(universal_class,universal_class)) ),
successor_relation3 ).
cnf(i_0_202,plain,
union(X1,unordered_pair(X1,X1)) = successor(X1),
inference(rw,[status(thm)],[i_0_176,c_0_170]) ).
cnf(i_0_203,axiom,
complement(intersection(complement(X1),complement(X2))) = union(X1,X2),
union ).
cnf(i_0_204,axiom,
( singleton(not_subclass_element(X1,null_class)) = X1
| X1 = null_class
| not_subclass_element(intersection(complement(singleton(not_subclass_element(X1,null_class))),X1),null_class) != not_subclass_element(X1,null_class) ),
corollary_1_to_number_of_elements_in_class ).
cnf(i_0_205,axiom,
( member(ordered_pair(X1,X2),element_relation)
| ~ member(ordered_pair(X1,X2),cross_product(universal_class,universal_class))
| ~ member(X1,X2) ),
element_relation3 ).
cnf(i_0_206,axiom,
( second(ordered_pair(X1,X2)) = X2
| ~ member(ordered_pair(X1,X2),cross_product(universal_class,universal_class)) ),
unique_1st_and_2nd_in_pair_of_sets2 ).
cnf(i_0_207,axiom,
( first(ordered_pair(X1,X2)) = X1
| ~ member(ordered_pair(X1,X2),cross_product(universal_class,universal_class)) ),
unique_1st_and_2nd_in_pair_of_sets1 ).
cnf(i_0_208,axiom,
( successor(X1) = X2
| ~ member(ordered_pair(X1,X2),successor_relation) ),
successor_relation2 ).
cnf(i_0_209,axiom,
( operation(X1)
| ~ function(X1)
| cross_product(domain_of(domain_of(X1)),domain_of(domain_of(X1))) != domain_of(X1)
| ~ subclass(range_of(X1),domain_of(domain_of(X1))) ),
operation4 ).
cnf(i_0_210,axiom,
( compatible(X1,X2,X3)
| ~ function(X1)
| domain_of(domain_of(X2)) != domain_of(X1)
| ~ subclass(range_of(X1),domain_of(domain_of(X3))) ),
compatible4 ).
cnf(i_0_211,axiom,
( member(X1,unordered_pair(X1,X2))
| ~ member(ordered_pair(X1,X2),cross_product(X3,X4)) ),
corollary_1_to_unordered_pair ).
cnf(i_0_212,axiom,
( member(X2,unordered_pair(X1,X2))
| ~ member(ordered_pair(X1,X2),cross_product(X3,X4)) ),
corollary_2_to_unordered_pair ).
cnf(i_0_213,axiom,
( X1 = X3
| unordered_pair(X1,X2) != unordered_pair(X3,X2)
| ~ member(ordered_pair(X1,X3),cross_product(universal_class,universal_class)) ),
right_cancellation ).
cnf(i_0_214,axiom,
( X2 = X3
| unordered_pair(X1,X2) != unordered_pair(X1,X3)
| ~ member(ordered_pair(X2,X3),cross_product(universal_class,universal_class)) ),
left_cancellation ).
cnf(i_0_215,axiom,
( function(X1)
| ~ subclass(X1,cross_product(universal_class,universal_class))
| ~ subclass(compose(X1,inverse(X1)),identity_relation) ),
function3 ).
cnf(i_0_216,negated_conjecture,
first(ordered_pair(x,y)) != ordered_pair(x,y),
prove_corollary_1_to_OP_determines_components2_2 ).
cnf(i_0_217,axiom,
( ~ member(ordered_pair(X1,X2),cross_product(X3,X4))
| unordered_pair(X1,X2) != null_class ),
corollary_to_unordered_pair_axiom3 ).
cnf(i_0_218,axiom,
( member(X1,X3)
| ~ member(ordered_pair(X1,X2),cross_product(X3,X4)) ),
cartesian_product1 ).
cnf(i_0_219,axiom,
( member(X2,X4)
| ~ member(ordered_pair(X1,X2),cross_product(X3,X4)) ),
cartesian_product2 ).
cnf(i_0_220,axiom,
( member(ordered_pair(first(X1),second(X1)),cross_product(universal_class,universal_class))
| second(X1) = X1 ),
unique_1st_and_2nd_in_pair_of_non_sets2 ).
cnf(i_0_221,axiom,
( member(ordered_pair(first(X1),second(X1)),cross_product(universal_class,universal_class))
| second(X1) = X1 ),
existence_of_1st_and_2nd_3 ).
cnf(i_0_222,axiom,
( member(ordered_pair(first(X1),second(X1)),cross_product(universal_class,universal_class))
| first(X1) = X1 ),
unique_1st_and_2nd_in_pair_of_non_sets1 ).
cnf(i_0_223,axiom,
( member(ordered_pair(first(X1),second(X1)),cross_product(universal_class,universal_class))
| first(X1) = X1 ),
existence_of_1st_and_2nd_2 ).
cnf(i_0_224,axiom,
( member(X1,universal_class)
| ~ member(ordered_pair(X1,X2),cross_product(X3,X4)) ),
corollary_1_to_cartesian_product ).
cnf(i_0_225,axiom,
( member(X2,universal_class)
| ~ member(ordered_pair(X1,X2),cross_product(X3,X4)) ),
corollary_2_to_cartesian_product ).
cnf(i_0_226,axiom,
( single_valued_class(X1)
| ~ subclass(compose(X1,inverse(X1)),identity_relation) ),
single_valued_class2 ).
cnf(i_0_227,axiom,
( member(X1,X2)
| ~ member(ordered_pair(X1,X2),element_relation) ),
element_relation2 ).
cnf(i_0_228,axiom,
( X1 = X3
| ordered_pair(X1,X2) != ordered_pair(X3,X4)
| ~ member(X1,universal_class) ),
ordered_pair_determines_components1 ).
cnf(i_0_229,axiom,
( X2 = X4
| ordered_pair(X1,X2) != ordered_pair(X3,X4)
| ~ member(X2,universal_class) ),
ordered_pair_determines_components2 ).
cnf(i_0_230,axiom,
( member(X1,universal_class)
| second(ordered_pair(X1,X2)) = ordered_pair(X1,X2) ),
corollary_2_to_ordered_pair_determines_components1 ).
cnf(i_0_231,axiom,
( member(X1,universal_class)
| first(ordered_pair(X1,X2)) = ordered_pair(X1,X2) ),
corollary_1_to_ordered_pair_determines_components1 ).
cnf(i_0_232,axiom,
( subclass(range_of(X1),domain_of(domain_of(X3)))
| ~ compatible(X1,X2,X3) ),
compatible3 ).
cnf(i_0_233,axiom,
( member(X1,universal_class)
| ordered_pair(first(X1),second(X1)) != X1 ),
corollary_1_to_ordered_pairs_are_sets ).
cnf(i_0_234,axiom,
member(unordered_pair(X1,singleton(X2)),ordered_pair(X1,X2)),
unordered_pair_member_of_ordered_pair ).
cnf(i_0_235,axiom,
( member(ordered_pair(X1,X3),cross_product(X2,X4))
| ~ member(X1,X2)
| ~ member(X3,X4) ),
cartesian_product3 ).
cnf(i_0_236,axiom,
( unordered_pair(null_class,singleton(singleton(X1))) = ordered_pair(X2,X1)
| member(X2,universal_class)
| ~ member(X1,universal_class) ),
property_2_of_ordered_pair ).
cnf(i_0_237,axiom,
unordered_pair(X1,X2) = union(singleton(X1),singleton(X2)),
unordered_pairs_and_singletons ).
cnf(i_0_238,axiom,
member(singleton(X1),ordered_pair(X1,X2)),
singleton_member_of_ordered_pair ).
cnf(i_0_239,axiom,
( ordered_pair(first(X1),second(X1)) = X1
| ~ member(X1,cross_product(X2,X3)) ),
cartesian_product4 ).
cnf(i_0_240,axiom,
( subclass(range_of(X1),domain_of(domain_of(X1)))
| ~ operation(X1) ),
operation3 ).
cnf(i_0_241,axiom,
( subclass(compose(X1,inverse(X1)),identity_relation)
| ~ function(X1) ),
function2 ).
cnf(i_0_242,axiom,
( subclass(compose(X1,inverse(X1)),identity_relation)
| ~ single_valued_class(X1) ),
single_valued_class1 ).
cnf(i_0_243,axiom,
member(ordered_pair(X1,X2),universal_class),
ordered_pair_is_set ).
cnf(i_0_244,axiom,
( ordered_pair(first(X1),second(X1)) = X1
| second(X1) = X1 ),
unique_1st_and_2nd_in_pair_of_non_sets4 ).
cnf(i_0_245,axiom,
( ordered_pair(first(X1),second(X1)) = X1
| second(X1) = X1 ),
existence_of_1st_and_2nd_5 ).
cnf(i_0_246,axiom,
( ordered_pair(first(X1),second(X1)) = X1
| first(X1) = X1 ),
unique_1st_and_2nd_in_pair_of_non_sets3 ).
cnf(i_0_247,axiom,
( ordered_pair(first(X1),second(X1)) = X1
| first(X1) = X1 ),
existence_of_1st_and_2nd_4 ).
cnf(i_0_248,axiom,
( unordered_pair(singleton(X1),unordered_pair(X1,null_class)) = ordered_pair(X1,X2)
| member(X2,universal_class) ),
property_1_of_ordered_pair ).
cnf(i_0_249,axiom,
( one_to_one(X1)
| ~ function(inverse(X1))
| ~ function(X1) ),
one_to_one3 ).
cnf(i_0_250,axiom,
( member(sum_class(X1),universal_class)
| ~ member(X1,universal_class) ),
sum_class2 ).
cnf(i_0_251,axiom,
( unordered_pair(null_class,singleton(null_class)) = ordered_pair(X1,X2)
| member(X1,universal_class)
| member(X2,universal_class) ),
property_3_of_ordered_pair ).
cnf(i_0_252,axiom,
( restrict(X1,singleton(X2),universal_class) != null_class
| ~ member(X2,domain_of(X1)) ),
domain1 ).
cnf(i_0_253,axiom,
( singleton(member_of(singleton(X1))) = singleton(X1)
| ~ member(X1,universal_class) ),
member_exists2 ).
cnf(i_0_254,axiom,
( restrict(X2,singleton(X1),universal_class) = null_class
| member(X1,domain_of(X2))
| ~ member(X1,universal_class) ),
domain2 ).
cnf(i_0_255,axiom,
( function(inverse(X1))
| ~ one_to_one(X1) ),
one_to_one2 ).
cnf(i_0_256,axiom,
member(singleton(X1),unordered_pair(X2,singleton(X1))),
corollary_1_to_singletons_are_sets ).
cnf(i_0_257,axiom,
intersection(inverse(subset_relation),subset_relation) = identity_relation,
identity_relation ).
cnf(i_0_258,axiom,
( member(member_of(singleton(X1)),universal_class)
| ~ member(X1,universal_class) ),
member_exists1 ).
cnf(i_0_259,axiom,
( X1 = null_class
| singleton(X2) = X1
| ~ subclass(X1,singleton(X2)) ),
two_subsets_of_singleton ).
cnf(i_0_260,axiom,
intersection(cross_product(X1,X2),X3) = restrict(X3,X1,X2),
restriction2 ).
cnf(i_0_261,axiom,
( member_of(X1) = X2
| singleton(member_of(X1)) != X1
| ~ member(X2,X1) ),
property_of_singletons1 ).
cnf(i_0_262,axiom,
( X3 = X1
| X3 = X2
| unordered_pair(X1,X2) != singleton(X3)
| ~ member(X3,universal_class) ),
singleton_in_unordered_pair3 ).
cnf(i_0_263,axiom,
( X1 = X2
| singleton(X1) != singleton(X2)
| ~ member(X1,universal_class) ),
singleton_identified_by_element1 ).
cnf(i_0_264,axiom,
( X1 = X2
| singleton(X1) != singleton(X2)
| ~ member(X2,universal_class) ),
singleton_identified_by_element2 ).
cnf(i_0_265,axiom,
subclass(singleton(X1),unordered_pair(X1,X2)),
singleton_in_unordered_pair1 ).
cnf(i_0_266,axiom,
subclass(singleton(X1),unordered_pair(X2,X1)),
singleton_in_unordered_pair2 ).
cnf(i_0_267,axiom,
( X1 = X2
| ~ member(X1,singleton(X2)) ),
only_member_in_singleton ).
cnf(i_0_268,axiom,
( subclass(singleton(X1),X2)
| ~ member(X1,X2) ),
property_of_singletons2 ).
cnf(i_0_269,axiom,
( member(X1,singleton(X1))
| ~ member(X1,universal_class) ),
set_in_its_singleton ).
cnf(i_0_270,axiom,
( member(X1,universal_class)
| singleton(member_of(X1)) != X1 ),
corollary_2_to_singletons_are_sets ).
cnf(i_0_271,axiom,
( member_of(singleton(X1)) = X1
| ~ member(X1,universal_class) ),
member_of_singleton_is_unique ).
cnf(i_0_272,axiom,
( ~ member(X1,universal_class)
| singleton(X1) != null_class ),
corollary_to_set_in_its_singleton ).
cnf(i_0_273,axiom,
( member(X1,universal_class)
| unordered_pair(X1,X2) = singleton(X2) ),
unordered_pair_equals_singleton2 ).
cnf(i_0_274,axiom,
( member(X1,universal_class)
| unordered_pair(X2,X1) = singleton(X2) ),
unordered_pair_equals_singleton1 ).
cnf(i_0_275,axiom,
member(singleton(X1),universal_class),
singletons_are_sets ).
cnf(i_0_276,axiom,
( singleton(member_of1(X1)) = X1
| member_of(X1) = X1 ),
member_of_non_singleton_unique2 ).
cnf(i_0_277,axiom,
( singleton(member_of(X1)) = X1
| member_of(X1) = X1 ),
member_exists4 ).
cnf(i_0_278,axiom,
member(null_class,singleton(null_class)),
null_class_in_its_singleton ).
cnf(i_0_279,axiom,
( member(X1,universal_class)
| singleton(X1) = null_class ),
singleton_is_null_class ).
cnf(i_0_280,plain,
( homomorphism(X3,X1,X2)
| domain_of(intersection(element_relation,cross_product(universal_class,domain_of(domain_of(flip(cross_product(intersection(X2,cross_product(unordered_pair(unordered_pair(unordered_pair(domain_of(intersection(element_relation,cross_product(universal_class,domain_of(domain_of(flip(cross_product(intersection(X3,cross_product(unordered_pair(not_homomorphism1(X3,X1,X2),not_homomorphism1(X3,X1,X2)),universal_class)),universal_class))))))),domain_of(intersection(element_relation,cross_product(universal_class,domain_of(domain_of(flip(cross_product(intersection(X3,cross_product(unordered_pair(not_homomorphism1(X3,X1,X2),not_homomorphism1(X3,X1,X2)),universal_class)),universal_class)))))))),unordered_pair(domain_of(intersection(element_relation,cross_product(universal_class,domain_of(domain_of(flip(cross_product(intersection(X3,cross_product(unordered_pair(not_homomorphism1(X3,X1,X2),not_homomorphism1(X3,X1,X2)),universal_class)),universal_class))))))),unordered_pair(domain_of(intersection(element_relation,cross_product(universal_class,domain_of(domain_of(flip(cross_product(intersection(X3,cross_product(unordered_pair(not_homomorphism2(X3,X1,X2),not_homomorphism2(X3,X1,X2)),universal_class)),universal_class))))))),domain_of(intersection(element_relation,cross_product(universal_class,domain_of(domain_of(flip(cross_product(intersection(X3,cross_product(unordered_pair(not_homomorphism2(X3,X1,X2),not_homomorphism2(X3,X1,X2)),universal_class)),universal_class)))))))))),unordered_pair(unordered_pair(domain_of(intersection(element_relation,cross_product(universal_class,domain_of(domain_of(flip(cross_product(intersection(X3,cross_product(unordered_pair(not_homomorphism1(X3,X1,X2),not_homomorphism1(X3,X1,X2)),universal_class)),universal_class))))))),domain_of(intersection(element_relation,cross_product(universal_class,domain_of(domain_of(flip(cross_product(intersection(X3,cross_product(unordered_pair(not_homomorphism1(X3,X1,X2),not_homomorphism1(X3,X1,X2)),universal_class)),universal_class)))))))),unordered_pair(domain_of(intersection(element_relation,cross_product(universal_class,domain_of(domain_of(flip(cross_product(intersection(X3,cross_product(unordered_pair(not_homomorphism1(X3,X1,X2),not_homomorphism1(X3,X1,X2)),universal_class)),universal_class))))))),unordered_pair(domain_of(intersection(element_relation,cross_product(universal_class,domain_of(domain_of(flip(cross_product(intersection(X3,cross_product(unordered_pair(not_homomorphism2(X3,X1,X2),not_homomorphism2(X3,X1,X2)),universal_class)),universal_class))))))),domain_of(intersection(element_relation,cross_product(universal_class,domain_of(domain_of(flip(cross_product(intersection(X3,cross_product(unordered_pair(not_homomorphism2(X3,X1,X2),not_homomorphism2(X3,X1,X2)),universal_class)),universal_class))))))))))),universal_class)),universal_class))))))) != domain_of(intersection(element_relation,cross_product(universal_class,domain_of(domain_of(flip(cross_product(intersection(X3,cross_product(unordered_pair(domain_of(intersection(element_relation,cross_product(universal_class,domain_of(domain_of(flip(cross_product(intersection(X1,cross_product(unordered_pair(unordered_pair(unordered_pair(not_homomorphism1(X3,X1,X2),not_homomorphism1(X3,X1,X2)),unordered_pair(not_homomorphism1(X3,X1,X2),unordered_pair(not_homomorphism2(X3,X1,X2),not_homomorphism2(X3,X1,X2)))),unordered_pair(unordered_pair(not_homomorphism1(X3,X1,X2),not_homomorphism1(X3,X1,X2)),unordered_pair(not_homomorphism1(X3,X1,X2),unordered_pair(not_homomorphism2(X3,X1,X2),not_homomorphism2(X3,X1,X2))))),universal_class)),universal_class))))))),domain_of(intersection(element_relation,cross_product(universal_class,domain_of(domain_of(flip(cross_product(intersection(X1,cross_product(unordered_pair(unordered_pair(unordered_pair(not_homomorphism1(X3,X1,X2),not_homomorphism1(X3,X1,X2)),unordered_pair(not_homomorphism1(X3,X1,X2),unordered_pair(not_homomorphism2(X3,X1,X2),not_homomorphism2(X3,X1,X2)))),unordered_pair(unordered_pair(not_homomorphism1(X3,X1,X2),not_homomorphism1(X3,X1,X2)),unordered_pair(not_homomorphism1(X3,X1,X2),unordered_pair(not_homomorphism2(X3,X1,X2),not_homomorphism2(X3,X1,X2))))),universal_class)),universal_class)))))))),universal_class)),universal_class)))))))
| ~ operation(X2)
| ~ operation(X1)
| ~ compatible(X3,X1,X2) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[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_177,c_0_178]),c_0_178]),c_0_178]),c_0_178]),c_0_178]),c_0_174]),c_0_174]),c_0_174]),c_0_174]),c_0_174]),c_0_174]),c_0_174]),c_0_174]),c_0_175]),c_0_175]),c_0_175]),c_0_175]),c_0_175]),c_0_175]),c_0_175]),c_0_175]),c_0_179]),c_0_179]),c_0_179]),c_0_179]),c_0_179]),c_0_179]),c_0_179]),c_0_179]),c_0_180]),c_0_180]),c_0_180]),c_0_180]),c_0_180]),c_0_180]),
[final] ).
cnf(i_0_281,plain,
( domain_of(intersection(element_relation,cross_product(universal_class,domain_of(domain_of(flip(cross_product(intersection(X3,cross_product(unordered_pair(unordered_pair(unordered_pair(domain_of(intersection(element_relation,cross_product(universal_class,domain_of(domain_of(flip(cross_product(intersection(X1,cross_product(unordered_pair(X4,X4),universal_class)),universal_class))))))),domain_of(intersection(element_relation,cross_product(universal_class,domain_of(domain_of(flip(cross_product(intersection(X1,cross_product(unordered_pair(X4,X4),universal_class)),universal_class)))))))),unordered_pair(domain_of(intersection(element_relation,cross_product(universal_class,domain_of(domain_of(flip(cross_product(intersection(X1,cross_product(unordered_pair(X4,X4),universal_class)),universal_class))))))),unordered_pair(domain_of(intersection(element_relation,cross_product(universal_class,domain_of(domain_of(flip(cross_product(intersection(X1,cross_product(unordered_pair(X5,X5),universal_class)),universal_class))))))),domain_of(intersection(element_relation,cross_product(universal_class,domain_of(domain_of(flip(cross_product(intersection(X1,cross_product(unordered_pair(X5,X5),universal_class)),universal_class)))))))))),unordered_pair(unordered_pair(domain_of(intersection(element_relation,cross_product(universal_class,domain_of(domain_of(flip(cross_product(intersection(X1,cross_product(unordered_pair(X4,X4),universal_class)),universal_class))))))),domain_of(intersection(element_relation,cross_product(universal_class,domain_of(domain_of(flip(cross_product(intersection(X1,cross_product(unordered_pair(X4,X4),universal_class)),universal_class)))))))),unordered_pair(domain_of(intersection(element_relation,cross_product(universal_class,domain_of(domain_of(flip(cross_product(intersection(X1,cross_product(unordered_pair(X4,X4),universal_class)),universal_class))))))),unordered_pair(domain_of(intersection(element_relation,cross_product(universal_class,domain_of(domain_of(flip(cross_product(intersection(X1,cross_product(unordered_pair(X5,X5),universal_class)),universal_class))))))),domain_of(intersection(element_relation,cross_product(universal_class,domain_of(domain_of(flip(cross_product(intersection(X1,cross_product(unordered_pair(X5,X5),universal_class)),universal_class))))))))))),universal_class)),universal_class))))))) = domain_of(intersection(element_relation,cross_product(universal_class,domain_of(domain_of(flip(cross_product(intersection(X1,cross_product(unordered_pair(domain_of(intersection(element_relation,cross_product(universal_class,domain_of(domain_of(flip(cross_product(intersection(X2,cross_product(unordered_pair(unordered_pair(unordered_pair(X4,X4),unordered_pair(X4,unordered_pair(X5,X5))),unordered_pair(unordered_pair(X4,X4),unordered_pair(X4,unordered_pair(X5,X5)))),universal_class)),universal_class))))))),domain_of(intersection(element_relation,cross_product(universal_class,domain_of(domain_of(flip(cross_product(intersection(X2,cross_product(unordered_pair(unordered_pair(unordered_pair(X4,X4),unordered_pair(X4,unordered_pair(X5,X5))),unordered_pair(unordered_pair(X4,X4),unordered_pair(X4,unordered_pair(X5,X5)))),universal_class)),universal_class)))))))),universal_class)),universal_class)))))))
| ~ homomorphism(X1,X2,X3)
| ~ member(unordered_pair(unordered_pair(X4,X4),unordered_pair(X4,unordered_pair(X5,X5))),domain_of(X2)) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[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_181,c_0_178]),c_0_178]),c_0_178]),c_0_178]),c_0_178]),c_0_174]),c_0_174]),c_0_174]),c_0_174]),c_0_174]),c_0_174]),c_0_174]),c_0_174]),c_0_175]),c_0_175]),c_0_175]),c_0_175]),c_0_175]),c_0_175]),c_0_175]),c_0_175]),c_0_179]),c_0_179]),c_0_179]),c_0_179]),c_0_179]),c_0_179]),c_0_179]),c_0_179]),c_0_180]),c_0_180]),c_0_180]),c_0_180]),c_0_180]),c_0_180]),c_0_180]),
[final] ).
cnf(i_0_282,plain,
( member(unordered_pair(unordered_pair(X4,X4),unordered_pair(X4,unordered_pair(X1,X1))),compose(X2,X3))
| ~ member(unordered_pair(unordered_pair(X4,X4),unordered_pair(X4,unordered_pair(X1,X1))),cross_product(universal_class,universal_class))
| ~ 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))))) ),
inference(rw,[status(thm)],[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_182,c_0_170]),c_0_174]),c_0_174]),c_0_175]),c_0_175]),c_0_180]),c_0_180]),
[final] ).
cnf(i_0_283,plain,
( 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)))))
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),compose(X3,X4)) ),
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_183,c_0_170]),c_0_174]),c_0_174]),c_0_175]),c_0_175]),c_0_180]),
[final] ).
cnf(i_0_284,plain,
( X1 = null_class
| member(domain_of(intersection(element_relation,cross_product(universal_class,domain_of(domain_of(flip(cross_product(intersection(choice,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)],[inference(rw,[status(thm)],[i_0_184,c_0_178]),c_0_174]),c_0_175]),c_0_179]),
[final] ).
cnf(i_0_285,plain,
( member(unordered_pair(unordered_pair(first(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2)))),first(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))))),unordered_pair(first(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2)))),unordered_pair(second(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2)))),second(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))))))),cross_product(universal_class,universal_class))
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),cross_product(universal_class,universal_class)) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_185,c_0_180]),c_0_180]),c_0_180]),c_0_180]),
[final] ).
cnf(i_0_286,plain,
( 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))
| ~ 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))),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_186,c_0_180]),c_0_180]),c_0_180]),c_0_180]),c_0_180]),c_0_180]),
[final] ).
cnf(i_0_287,plain,
( 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))
| ~ 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))),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_187,c_0_180]),c_0_180]),c_0_180]),c_0_180]),c_0_180]),c_0_180]),
[final] ).
cnf(i_0_288,plain,
( 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))),flip(X4)) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_188,c_0_180]),c_0_180]),c_0_180]),c_0_180]),
[final] ).
cnf(i_0_289,plain,
( 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))),rotate(X4)) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_189,c_0_180]),c_0_180]),c_0_180]),c_0_180]),
[final] ).
cnf(i_0_290,plain,
( member(complement(domain_of(domain_of(flip(cross_product(intersection(element_relation,cross_product(complement(X1),universal_class)),universal_class))))),universal_class)
| ~ member(X1,universal_class) ),
inference(rw,[status(thm)],[i_0_190,c_0_191]),
[final] ).
cnf(i_0_291,plain,
( homomorphism(X3,X1,X2)
| member(unordered_pair(unordered_pair(not_homomorphism1(X3,X1,X2),not_homomorphism1(X3,X1,X2)),unordered_pair(not_homomorphism1(X3,X1,X2),unordered_pair(not_homomorphism2(X3,X1,X2),not_homomorphism2(X3,X1,X2)))),domain_of(X1))
| ~ operation(X2)
| ~ operation(X1)
| ~ compatible(X3,X1,X2) ),
inference(rw,[status(thm)],[i_0_192,c_0_180]),
[final] ).
cnf(i_0_292,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_193,c_0_174]),c_0_175]),
[final] ).
cnf(i_0_293,plain,
intersection(domain_of(X1),complement(domain_of(intersection(compose(domain_of(flip(cross_product(element_relation,universal_class))),X1),identity_relation)))) = cantor(X1),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_194,c_0_195]),c_0_175]),
[final] ).
cnf(i_0_294,plain,
( X1 = null_class
| unordered_pair(not_subclass_element(X1,null_class),not_subclass_element(X1,null_class)) = X1
| member(not_subclass_element(intersection(complement(unordered_pair(not_subclass_element(X1,null_class),not_subclass_element(X1,null_class))),X1),null_class),intersection(complement(unordered_pair(not_subclass_element(X1,null_class),not_subclass_element(X1,null_class))),X1)) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_196,c_0_170]),c_0_170]),c_0_170]),
[final] ).
cnf(i_0_295,plain,
( member(domain_of(domain_of(flip(cross_product(intersection(X1,cross_product(X2,universal_class)),universal_class)))),universal_class)
| ~ function(X1)
| ~ member(X2,universal_class) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_197,c_0_174]),c_0_175]),
[final] ).
cnf(i_0_296,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_198,c_0_174]),c_0_175]),
[final] ).
cnf(i_0_297,plain,
( X1 = null_class
| unordered_pair(not_subclass_element(X1,null_class),not_subclass_element(X1,null_class)) = X1
| member(not_subclass_element(intersection(complement(unordered_pair(not_subclass_element(X1,null_class),not_subclass_element(X1,null_class))),X1),null_class),X1) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_199,c_0_170]),c_0_170]),
[final] ).
cnf(i_0_298,plain,
intersection(cross_product(universal_class,universal_class),intersection(cross_product(universal_class,universal_class),complement(compose(complement(element_relation),domain_of(flip(cross_product(element_relation,universal_class))))))) = subset_relation,
inference(rw,[status(thm)],[i_0_200,c_0_175]),
[final] ).
cnf(i_0_299,plain,
( member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),successor_relation)
| complement(intersection(complement(X1),complement(unordered_pair(X1,X1)))) != X2
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),cross_product(universal_class,universal_class)) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_201,c_0_202]),c_0_203]),c_0_180]),c_0_180]),
[final] ).
cnf(i_0_300,plain,
( X1 = null_class
| unordered_pair(not_subclass_element(X1,null_class),not_subclass_element(X1,null_class)) = X1
| not_subclass_element(intersection(complement(unordered_pair(not_subclass_element(X1,null_class),not_subclass_element(X1,null_class))),X1),null_class) != not_subclass_element(X1,null_class) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_204,c_0_170]),c_0_170]),
[final] ).
cnf(i_0_301,plain,
( member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),element_relation)
| ~ member(X1,X2)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),cross_product(universal_class,universal_class)) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_205,c_0_180]),c_0_180]),
[final] ).
cnf(i_0_302,plain,
( second(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2)))) = X2
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),cross_product(universal_class,universal_class)) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_206,c_0_180]),c_0_180]),
[final] ).
cnf(i_0_303,plain,
( first(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2)))) = X1
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),cross_product(universal_class,universal_class)) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_207,c_0_180]),c_0_180]),
[final] ).
cnf(i_0_304,plain,
( complement(intersection(complement(X1),complement(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)],[inference(rw,[status(thm)],[i_0_208,c_0_202]),c_0_203]),c_0_180]),
[final] ).
cnf(i_0_305,plain,
( operation(X1)
| cross_product(domain_of(domain_of(X1)),domain_of(domain_of(X1))) != domain_of(X1)
| ~ function(X1)
| ~ subclass(domain_of(domain_of(flip(cross_product(X1,universal_class)))),domain_of(domain_of(X1))) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_209,c_0_167]),c_0_175]),
[final] ).
cnf(i_0_306,plain,
( compatible(X1,X2,X3)
| domain_of(domain_of(X2)) != domain_of(X1)
| ~ function(X1)
| ~ subclass(domain_of(domain_of(flip(cross_product(X1,universal_class)))),domain_of(domain_of(X3))) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_210,c_0_167]),c_0_175]),
[final] ).
cnf(i_0_307,plain,
( member(X1,unordered_pair(X1,X2))
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),cross_product(X3,X4)) ),
inference(rw,[status(thm)],[i_0_211,c_0_180]),
[final] ).
cnf(i_0_308,plain,
( member(X2,unordered_pair(X1,X2))
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),cross_product(X3,X4)) ),
inference(rw,[status(thm)],[i_0_212,c_0_180]),
[final] ).
cnf(i_0_309,plain,
( X1 = X3
| unordered_pair(X1,X2) != unordered_pair(X3,X2)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X3,X3))),cross_product(universal_class,universal_class)) ),
inference(rw,[status(thm)],[i_0_213,c_0_180]),
[final] ).
cnf(i_0_310,plain,
( X2 = X3
| unordered_pair(X1,X2) != unordered_pair(X1,X3)
| ~ member(unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X3,X3))),cross_product(universal_class,universal_class)) ),
inference(rw,[status(thm)],[i_0_214,c_0_180]),
[final] ).
cnf(i_0_311,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_215,c_0_175]),
[final] ).
cnf(i_0_312,negated_conjecture,
first(unordered_pair(unordered_pair(x,x),unordered_pair(x,unordered_pair(y,y)))) != unordered_pair(unordered_pair(x,x),unordered_pair(x,unordered_pair(y,y))),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_216,c_0_180]),c_0_180]),
[final] ).
cnf(i_0_313,plain,
( unordered_pair(X1,X2) != null_class
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),cross_product(X3,X4)) ),
inference(rw,[status(thm)],[i_0_217,c_0_180]),
[final] ).
cnf(i_0_314,plain,
( member(X1,X3)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),cross_product(X3,X4)) ),
inference(rw,[status(thm)],[i_0_218,c_0_180]),
[final] ).
cnf(i_0_315,plain,
( member(X2,X4)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),cross_product(X3,X4)) ),
inference(rw,[status(thm)],[i_0_219,c_0_180]),
[final] ).
cnf(i_0_316,plain,
( second(X1) = X1
| member(unordered_pair(unordered_pair(first(X1),first(X1)),unordered_pair(first(X1),unordered_pair(second(X1),second(X1)))),cross_product(universal_class,universal_class)) ),
inference(rw,[status(thm)],[i_0_220,c_0_180]),
[final] ).
cnf(i_0_317,plain,
( second(X1) = X1
| member(unordered_pair(unordered_pair(first(X1),first(X1)),unordered_pair(first(X1),unordered_pair(second(X1),second(X1)))),cross_product(universal_class,universal_class)) ),
inference(rw,[status(thm)],[i_0_221,c_0_180]),
[final] ).
cnf(i_0_318,plain,
( first(X1) = X1
| member(unordered_pair(unordered_pair(first(X1),first(X1)),unordered_pair(first(X1),unordered_pair(second(X1),second(X1)))),cross_product(universal_class,universal_class)) ),
inference(rw,[status(thm)],[i_0_222,c_0_180]),
[final] ).
cnf(i_0_319,plain,
( first(X1) = X1
| member(unordered_pair(unordered_pair(first(X1),first(X1)),unordered_pair(first(X1),unordered_pair(second(X1),second(X1)))),cross_product(universal_class,universal_class)) ),
inference(rw,[status(thm)],[i_0_223,c_0_180]),
[final] ).
cnf(i_0_320,plain,
( member(X1,universal_class)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),cross_product(X3,X4)) ),
inference(rw,[status(thm)],[i_0_224,c_0_180]),
[final] ).
cnf(i_0_321,plain,
( member(X2,universal_class)
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),cross_product(X3,X4)) ),
inference(rw,[status(thm)],[i_0_225,c_0_180]),
[final] ).
cnf(i_0_322,plain,
( single_valued_class(X1)
| ~ subclass(compose(X1,domain_of(flip(cross_product(X1,universal_class)))),identity_relation) ),
inference(rw,[status(thm)],[i_0_226,c_0_175]),
[final] ).
cnf(i_0_323,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_227,c_0_180]),
[final] ).
cnf(i_0_324,plain,
( X1 = X3
| unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))) != unordered_pair(unordered_pair(X3,X3),unordered_pair(X3,unordered_pair(X4,X4)))
| ~ member(X1,universal_class) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_228,c_0_180]),c_0_180]),
[final] ).
cnf(i_0_325,plain,
( X2 = X4
| unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))) != unordered_pair(unordered_pair(X3,X3),unordered_pair(X3,unordered_pair(X4,X4)))
| ~ member(X2,universal_class) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_229,c_0_180]),c_0_180]),
[final] ).
cnf(i_0_326,plain,
( second(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)))
| member(X1,universal_class) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_230,c_0_180]),c_0_180]),
[final] ).
cnf(i_0_327,plain,
( first(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)))
| member(X1,universal_class) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_231,c_0_180]),c_0_180]),
[final] ).
cnf(i_0_328,plain,
( subclass(domain_of(domain_of(flip(cross_product(X1,universal_class)))),domain_of(domain_of(X3)))
| ~ compatible(X1,X2,X3) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_232,c_0_167]),c_0_175]),
[final] ).
cnf(i_0_329,plain,
( member(X1,universal_class)
| unordered_pair(unordered_pair(first(X1),first(X1)),unordered_pair(first(X1),unordered_pair(second(X1),second(X1)))) != X1 ),
inference(rw,[status(thm)],[i_0_233,c_0_180]),
[final] ).
cnf(i_0_330,plain,
member(unordered_pair(X1,unordered_pair(X2,X2)),unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2)))),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_234,c_0_170]),c_0_180]),
[final] ).
cnf(i_0_331,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_235,c_0_180]),
[final] ).
cnf(i_0_332,plain,
( unordered_pair(null_class,unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,X1))) = unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X1,X1)))
| member(X2,universal_class)
| ~ member(X1,universal_class) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_236,c_0_170]),c_0_170]),c_0_180]),
[final] ).
cnf(i_0_333,plain,
unordered_pair(X1,X2) = complement(intersection(complement(unordered_pair(X1,X1)),complement(unordered_pair(X2,X2)))),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_237,c_0_170]),c_0_170]),c_0_203]),
[final] ).
cnf(i_0_334,plain,
member(unordered_pair(X1,X1),unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2)))),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_238,c_0_170]),c_0_180]),
[final] ).
cnf(i_0_335,plain,
( unordered_pair(unordered_pair(first(X1),first(X1)),unordered_pair(first(X1),unordered_pair(second(X1),second(X1)))) = X1
| ~ member(X1,cross_product(X2,X3)) ),
inference(rw,[status(thm)],[i_0_239,c_0_180]),
[final] ).
cnf(i_0_336,plain,
( subclass(domain_of(domain_of(flip(cross_product(X1,universal_class)))),domain_of(domain_of(X1)))
| ~ operation(X1) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_240,c_0_167]),c_0_175]),
[final] ).
cnf(i_0_337,plain,
( subclass(compose(X1,domain_of(flip(cross_product(X1,universal_class)))),identity_relation)
| ~ function(X1) ),
inference(rw,[status(thm)],[i_0_241,c_0_175]),
[final] ).
cnf(i_0_338,plain,
( subclass(compose(X1,domain_of(flip(cross_product(X1,universal_class)))),identity_relation)
| ~ single_valued_class(X1) ),
inference(rw,[status(thm)],[i_0_242,c_0_175]),
[final] ).
cnf(i_0_339,plain,
member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),universal_class),
inference(rw,[status(thm)],[i_0_243,c_0_180]),
[final] ).
cnf(i_0_340,plain,
( second(X1) = X1
| unordered_pair(unordered_pair(first(X1),first(X1)),unordered_pair(first(X1),unordered_pair(second(X1),second(X1)))) = X1 ),
inference(rw,[status(thm)],[i_0_244,c_0_180]),
[final] ).
cnf(i_0_341,plain,
( second(X1) = X1
| unordered_pair(unordered_pair(first(X1),first(X1)),unordered_pair(first(X1),unordered_pair(second(X1),second(X1)))) = X1 ),
inference(rw,[status(thm)],[i_0_245,c_0_180]),
[final] ).
cnf(i_0_342,plain,
( first(X1) = X1
| unordered_pair(unordered_pair(first(X1),first(X1)),unordered_pair(first(X1),unordered_pair(second(X1),second(X1)))) = X1 ),
inference(rw,[status(thm)],[i_0_246,c_0_180]),
[final] ).
cnf(i_0_343,plain,
( first(X1) = X1
| unordered_pair(unordered_pair(first(X1),first(X1)),unordered_pair(first(X1),unordered_pair(second(X1),second(X1)))) = X1 ),
inference(rw,[status(thm)],[i_0_247,c_0_180]),
[final] ).
cnf(i_0_344,plain,
( unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,null_class)) = unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2)))
| member(X2,universal_class) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_248,c_0_170]),c_0_180]),
[final] ).
cnf(i_0_345,plain,
( one_to_one(X1)
| ~ function(X1)
| ~ function(domain_of(flip(cross_product(X1,universal_class)))) ),
inference(rw,[status(thm)],[i_0_249,c_0_175]),
[final] ).
cnf(i_0_346,plain,
( member(domain_of(intersection(element_relation,cross_product(universal_class,X1))),universal_class)
| ~ member(X1,universal_class) ),
inference(rw,[status(thm)],[i_0_250,c_0_179]),
[final] ).
cnf(i_0_347,plain,
( unordered_pair(null_class,unordered_pair(null_class,null_class)) = unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2)))
| member(X2,universal_class)
| member(X1,universal_class) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_251,c_0_170]),c_0_180]),
[final] ).
cnf(i_0_348,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_252,c_0_170]),c_0_168]),
[final] ).
cnf(i_0_349,plain,
( unordered_pair(member_of(unordered_pair(X1,X1)),member_of(unordered_pair(X1,X1))) = unordered_pair(X1,X1)
| ~ member(X1,universal_class) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_253,c_0_170]),c_0_170]),c_0_170]),
[final] ).
cnf(i_0_350,axiom,
( compatible(X1,X2,X3)
| ~ homomorphism(X1,X2,X3) ),
homomorphism3,
[final] ).
cnf(i_0_351,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_254,c_0_170]),c_0_168]),
[final] ).
cnf(i_0_352,axiom,
( X1 = X2
| ~ member(not_subclass_element(X1,X2),X2)
| ~ member(not_subclass_element(X2,X1),X1) ),
equality4,
[final] ).
cnf(i_0_353,plain,
( function(domain_of(flip(cross_product(X1,universal_class))))
| ~ one_to_one(X1) ),
inference(rw,[status(thm)],[i_0_255,c_0_175]),
[final] ).
cnf(i_0_354,plain,
member(unordered_pair(X1,X1),unordered_pair(X2,unordered_pair(X1,X1))),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_256,c_0_170]),c_0_170]),
[final] ).
cnf(i_0_355,plain,
intersection(domain_of(flip(cross_product(subset_relation,universal_class))),subset_relation) = identity_relation,
inference(rw,[status(thm)],[i_0_257,c_0_175]),
[final] ).
cnf(i_0_356,axiom,
( X2 = X1
| member(not_subclass_element(X2,X1),X2)
| ~ member(not_subclass_element(X1,X2),X2) ),
equality3,
[final] ).
cnf(i_0_357,axiom,
( X1 = X2
| member(not_subclass_element(X2,X1),X2)
| ~ member(not_subclass_element(X1,X2),X2) ),
equality2,
[final] ).
cnf(i_0_358,axiom,
( domain_of(domain_of(X2)) = domain_of(X1)
| ~ compatible(X1,X2,X3) ),
compatible2,
[final] ).
cnf(i_0_359,plain,
( member(member_of(unordered_pair(X1,X1)),universal_class)
| ~ member(X1,universal_class) ),
inference(rw,[status(thm)],[i_0_258,c_0_170]),
[final] ).
cnf(i_0_360,axiom,
( operation(X2)
| ~ homomorphism(X1,X2,X3) ),
homomorphism1,
[final] ).
cnf(i_0_361,axiom,
( operation(X3)
| ~ homomorphism(X1,X2,X3) ),
homomorphism2,
[final] ).
cnf(i_0_362,axiom,
( function(X1)
| ~ compatible(X1,X2,X3) ),
compatible1,
[final] ).
cnf(i_0_363,axiom,
( subclass(unordered_pair(X1,X3),X2)
| ~ member(X1,X2)
| ~ member(X3,X2) ),
unordered_pair_is_subset,
[final] ).
cnf(i_0_364,axiom,
( member(X1,intersection(X2,X3))
| ~ member(X1,X2)
| ~ member(X1,X3) ),
intersection3,
[final] ).
cnf(i_0_365,axiom,
( X1 = X2
| member(not_subclass_element(X1,X2),X1)
| member(not_subclass_element(X2,X1),X2) ),
equality1,
[final] ).
cnf(i_0_366,axiom,
subclass(flip(X1),cross_product(cross_product(universal_class,universal_class),universal_class)),
flip1,
[final] ).
cnf(i_0_367,axiom,
subclass(rotate(X1),cross_product(cross_product(universal_class,universal_class),universal_class)),
rotate1,
[final] ).
cnf(i_0_368,axiom,
~ member(X1,intersection(complement(X2),X2)),
special_classes_lemma,
[final] ).
cnf(i_0_369,plain,
( X1 = null_class
| unordered_pair(X2,X2) = X1
| ~ subclass(X1,unordered_pair(X2,X2)) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_259,c_0_170]),c_0_170]),
[final] ).
cnf(i_0_370,plain,
intersection(cross_product(X1,X2),X3) = intersection(X3,cross_product(X1,X2)),
inference(rw,[status(thm)],[i_0_260,c_0_168]),
[final] ).
cnf(i_0_371,axiom,
( subclass(X1,X2)
| ~ member(not_subclass_element(X1,X2),X2) ),
not_subclass_members2,
[final] ).
cnf(i_0_372,axiom,
( member(X1,X2)
| ~ member(X1,intersection(X2,X3)) ),
intersection1,
[final] ).
cnf(i_0_373,axiom,
( member(X1,X3)
| ~ member(X1,intersection(X2,X3)) ),
intersection2,
[final] ).
cnf(i_0_374,plain,
( member_of(X1) = X2
| unordered_pair(member_of(X1),member_of(X1)) != X1
| ~ member(X2,X1) ),
inference(rw,[status(thm)],[i_0_261,c_0_170]),
[final] ).
cnf(i_0_375,plain,
( X2 = X3
| X1 = X3
| unordered_pair(X1,X2) != unordered_pair(X3,X3)
| ~ member(X3,universal_class) ),
inference(rw,[status(thm)],[i_0_262,c_0_170]),
[final] ).
cnf(i_0_376,axiom,
( X1 = X2
| X1 = X3
| ~ member(X1,unordered_pair(X2,X3)) ),
unordered_pair_member,
[final] ).
cnf(i_0_377,plain,
( X1 = X2
| unordered_pair(X1,X1) != unordered_pair(X2,X2)
| ~ member(X1,universal_class) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_263,c_0_170]),c_0_170]),
[final] ).
cnf(i_0_378,plain,
( X1 = X2
| unordered_pair(X1,X1) != unordered_pair(X2,X2)
| ~ member(X2,universal_class) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_264,c_0_170]),c_0_170]),
[final] ).
cnf(i_0_379,axiom,
( member(X1,universal_class)
| ~ member(X1,cross_product(universal_class,universal_class)) ),
corollary_12to_ordered_pairs_are_sets,
[final] ).
cnf(i_0_380,plain,
subclass(unordered_pair(X1,X1),unordered_pair(X1,X2)),
inference(rw,[status(thm)],[i_0_265,c_0_170]),
[final] ).
cnf(i_0_381,plain,
subclass(unordered_pair(X1,X1),unordered_pair(X2,X1)),
inference(rw,[status(thm)],[i_0_266,c_0_170]),
[final] ).
cnf(i_0_382,plain,
( X1 = X2
| ~ member(X1,unordered_pair(X2,X2)) ),
inference(rw,[status(thm)],[i_0_267,c_0_170]),
[final] ).
cnf(i_0_383,plain,
( subclass(unordered_pair(X1,X1),X2)
| ~ member(X1,X2) ),
inference(rw,[status(thm)],[i_0_268,c_0_170]),
[final] ).
cnf(i_0_384,axiom,
( cross_product(domain_of(domain_of(X1)),domain_of(domain_of(X1))) = domain_of(X1)
| ~ operation(X1) ),
operation2,
[final] ).
cnf(i_0_385,plain,
( member(X1,unordered_pair(X1,X1))
| ~ member(X1,universal_class) ),
inference(rw,[status(thm)],[i_0_269,c_0_170]),
[final] ).
cnf(i_0_386,axiom,
( member(X1,unordered_pair(X1,X2))
| ~ member(X1,universal_class) ),
unordered_pair2,
[final] ).
cnf(i_0_387,axiom,
( member(X1,unordered_pair(X2,X1))
| ~ member(X1,universal_class) ),
unordered_pair3,
[final] ).
cnf(i_0_388,axiom,
subclass(compose(X1,X2),cross_product(universal_class,universal_class)),
compose1,
[final] ).
cnf(i_0_389,axiom,
( member(X3,X2)
| ~ subclass(X1,X2)
| ~ member(X3,X1) ),
subclass_members,
[final] ).
cnf(i_0_390,axiom,
( subclass(X1,X3)
| ~ subclass(X1,X2)
| ~ subclass(X2,X3) ),
transitivity_of_subclass,
[final] ).
cnf(i_0_391,plain,
( member(X1,universal_class)
| unordered_pair(member_of(X1),member_of(X1)) != X1 ),
inference(rw,[status(thm)],[i_0_270,c_0_170]),
[final] ).
cnf(i_0_392,axiom,
( member(X1,complement(X2))
| member(X1,X2)
| ~ member(X1,universal_class) ),
complement2,
[final] ).
cnf(i_0_393,axiom,
( ~ member(X1,complement(X2))
| ~ member(X1,X2) ),
complement1,
[final] ).
cnf(i_0_394,axiom,
( member(not_subclass_element(X1,X2),X1)
| subclass(X1,X2) ),
not_subclass_members1,
[final] ).
cnf(i_0_395,plain,
( member_of(unordered_pair(X1,X1)) = X1
| ~ member(X1,universal_class) ),
inference(rw,[status(thm)],[i_0_271,c_0_170]),
[final] ).
cnf(i_0_396,axiom,
( X1 = X2
| ~ subclass(X1,X2)
| ~ subclass(X2,X1) ),
subclass_implies_equal,
[final] ).
cnf(i_0_397,plain,
( unordered_pair(X1,X1) != null_class
| ~ member(X1,universal_class) ),
inference(rw,[status(thm)],[i_0_272,c_0_170]),
[final] ).
cnf(i_0_398,axiom,
( ~ member(X1,universal_class)
| unordered_pair(X1,X2) != null_class ),
corollary_to_unordered_pair_axiom1,
[final] ).
cnf(i_0_399,axiom,
( ~ member(X1,universal_class)
| unordered_pair(X2,X1) != null_class ),
corollary_to_unordered_pair_axiom2,
[final] ).
cnf(i_0_400,axiom,
( subclass(X1,cross_product(universal_class,universal_class))
| ~ function(X1) ),
function1,
[final] ).
cnf(i_0_401,plain,
( unordered_pair(X1,X2) = unordered_pair(X2,X2)
| member(X1,universal_class) ),
inference(rw,[status(thm)],[i_0_273,c_0_170]),
[final] ).
cnf(i_0_402,plain,
( unordered_pair(X2,X1) = unordered_pair(X2,X2)
| member(X1,universal_class) ),
inference(rw,[status(thm)],[i_0_274,c_0_170]),
[final] ).
cnf(i_0_403,axiom,
( unordered_pair(X1,X2) = null_class
| member(X1,universal_class)
| member(X2,universal_class) ),
null_unordered_pair,
[final] ).
cnf(i_0_404,axiom,
( X1 = null_class
| member(not_subclass_element(X1,null_class),X1) ),
null_class_is_unique,
[final] ).
cnf(i_0_405,plain,
member(unordered_pair(X1,X1),universal_class),
inference(rw,[status(thm)],[i_0_275,c_0_170]),
[final] ).
cnf(i_0_406,axiom,
member(unordered_pair(X1,X2),universal_class),
unordered_pairs_in_universal,
[final] ).
cnf(i_0_407,plain,
( member_of(X1) = X1
| unordered_pair(member_of1(X1),member_of1(X1)) = X1 ),
inference(rw,[status(thm)],[i_0_276,c_0_170]),
[final] ).
cnf(i_0_408,plain,
( member_of(X1) = X1
| unordered_pair(member_of(X1),member_of(X1)) = X1 ),
inference(rw,[status(thm)],[i_0_277,c_0_170]),
[final] ).
cnf(i_0_409,plain,
member(null_class,unordered_pair(null_class,null_class)),
inference(rw,[status(thm)],[i_0_278,c_0_170]),
[final] ).
cnf(i_0_410,axiom,
subclass(successor_relation,cross_product(universal_class,universal_class)),
successor_relation1,
[final] ).
cnf(i_0_411,axiom,
subclass(element_relation,cross_product(universal_class,universal_class)),
element_relation1,
[final] ).
cnf(i_0_412,axiom,
unordered_pair(X1,X2) = unordered_pair(X2,X1),
commutativity_of_unordered_pair,
[final] ).
cnf(i_0_413,plain,
( unordered_pair(X1,X1) = null_class
| member(X1,universal_class) ),
inference(rw,[status(thm)],[i_0_279,c_0_170]),
[final] ).
cnf(i_0_414,axiom,
( member(member_of1(X1),universal_class)
| member_of(X1) = X1 ),
member_of_non_singleton_unique1,
[final] ).
cnf(i_0_415,axiom,
( member(member_of(X1),universal_class)
| member_of(X1) = X1 ),
member_exists3,
[final] ).
cnf(i_0_416,axiom,
( X1 = null_class
| member(regular(X1),X1) ),
regularity1,
[final] ).
cnf(i_0_417,axiom,
( X1 = null_class
| intersection(X1,regular(X1)) = null_class ),
regularity2,
[final] ).
cnf(i_0_418,axiom,
( X1 = null_class
| ~ subclass(X1,null_class) ),
corollary_of_null_class_is_subclass,
[final] ).
cnf(i_0_419,axiom,
~ member(X1,null_class),
existence_of_null_class,
[final] ).
cnf(i_0_420,axiom,
( member(null_class,X1)
| ~ inductive(X1) ),
inductive1,
[final] ).
cnf(i_0_421,axiom,
( subclass(omega,X1)
| ~ inductive(X1) ),
omega_is_inductive2,
[final] ).
cnf(i_0_422,axiom,
( subclass(X1,X2)
| X1 != X2 ),
equal_implies_subclass1,
[final] ).
cnf(i_0_423,axiom,
( subclass(X2,X1)
| X1 != X2 ),
equal_implies_subclass2,
[final] ).
cnf(i_0_424,negated_conjecture,
~ member(y,universal_class),
prove_corollary_1_to_OP_determines_components2_1,
[final] ).
cnf(i_0_425,axiom,
subclass(X1,X1),
subclass_is_reflexive,
[final] ).
cnf(i_0_426,axiom,
subclass(null_class,X1),
null_class_is_subclass,
[final] ).
cnf(i_0_427,axiom,
subclass(X1,universal_class),
class_elements_are_sets,
[final] ).
cnf(i_0_428,axiom,
( function(X1)
| ~ operation(X1) ),
operation1,
[final] ).
cnf(i_0_429,axiom,
( function(X1)
| ~ one_to_one(X1) ),
one_to_one1,
[final] ).
cnf(i_0_430,axiom,
member(omega,universal_class),
omega_in_universal,
[final] ).
cnf(i_0_431,axiom,
member(null_class,universal_class),
null_class_is_a_set,
[final] ).
cnf(i_0_432,axiom,
function(choice),
choice1,
[final] ).
cnf(i_0_433,axiom,
inductive(omega),
omega_is_inductive1,
[final] ).
cnf(i_0_434,axiom,
X1 = X1 ).
cnf(i_0_435,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_436,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_437,axiom,
( X1 != X2
| domain_of(X1) = domain_of(X2) ) ).
cnf(i_0_438,axiom,
( X1 != X2
| second(X1) = second(X2) ) ).
cnf(i_0_439,axiom,
( X1 != X2
| complement(X1) = complement(X2) ) ).
cnf(i_0_440,axiom,
( X1 != X2
| cantor(X1) = cantor(X2) ) ).
cnf(i_0_441,axiom,
( X1 != X2
| not_subclass_element(X1,X3) = not_subclass_element(X2,X3) ) ).
cnf(i_0_442,axiom,
( X1 != X2
| not_subclass_element(X3,X1) = not_subclass_element(X3,X2) ) ).
cnf(i_0_443,axiom,
( X1 != X2
| member_of(X1) = member_of(X2) ) ).
cnf(i_0_444,axiom,
( X1 != X2
| intersection(X1,X3) = intersection(X2,X3) ) ).
cnf(i_0_445,axiom,
( X1 != X2
| intersection(X3,X1) = intersection(X3,X2) ) ).
cnf(i_0_446,axiom,
( X1 != X2
| cross_product(X1,X3) = cross_product(X2,X3) ) ).
cnf(i_0_447,axiom,
( X1 != X2
| cross_product(X3,X1) = cross_product(X3,X2) ) ).
cnf(i_0_448,axiom,
( X1 != X2
| unordered_pair(X1,X3) = unordered_pair(X2,X3) ) ).
cnf(i_0_449,axiom,
( X1 != X2
| unordered_pair(X3,X1) = unordered_pair(X3,X2) ) ).
cnf(i_0_450,axiom,
( X1 != X2
| first(X1) = first(X2) ) ).
cnf(i_0_451,axiom,
( X1 != X2
| ~ homomorphism(X1,X3,X4)
| homomorphism(X2,X3,X4) ) ).
cnf(i_0_452,axiom,
( X1 != X2
| ~ homomorphism(X3,X1,X4)
| homomorphism(X3,X2,X4) ) ).
cnf(i_0_453,axiom,
( X1 != X2
| ~ homomorphism(X3,X4,X1)
| homomorphism(X3,X4,X2) ) ).
cnf(i_0_454,axiom,
( X1 != X2
| ~ operation(X1)
| operation(X2) ) ).
cnf(i_0_455,axiom,
( X1 != X2
| ~ compatible(X1,X3,X4)
| compatible(X2,X3,X4) ) ).
cnf(i_0_456,axiom,
( X1 != X2
| ~ compatible(X3,X1,X4)
| compatible(X3,X2,X4) ) ).
cnf(i_0_457,axiom,
( X1 != X2
| ~ compatible(X3,X4,X1)
| compatible(X3,X4,X2) ) ).
cnf(i_0_458,axiom,
( X1 != X2
| ~ member(X1,X3)
| member(X2,X3) ) ).
cnf(i_0_459,axiom,
( X1 != X2
| ~ member(X3,X1)
| member(X3,X2) ) ).
cnf(i_0_460,axiom,
( X1 != X2
| ~ inductive(X1)
| inductive(X2) ) ).
cnf(i_0_461,axiom,
( X1 != X2
| ~ subclass(X1,X3)
| subclass(X2,X3) ) ).
cnf(i_0_462,axiom,
( X1 != X2
| ~ subclass(X3,X1)
| subclass(X3,X2) ) ).
cnf(i_0_463,axiom,
( X1 != X2
| ~ function(X1)
| function(X2) ) ).
cnf(i_0_464,axiom,
( X1 != X2
| ~ single_valued_class(X1)
| single_valued_class(X2) ) ).
cnf(i_0_465,axiom,
( X1 != X2
| ~ one_to_one(X1)
| one_to_one(X2) ) ).
cnf(i_0_2506,plain,
~ member(X1,intersection(X2,intersection(null_class,X3))),
inference(rename_variables,[],[i_0_1273]) ).
cnf(i_0_893,plain,
~ subclass(unordered_pair(X1,unordered_pair(X2,X3)),intersection(complement(X4),X4)),
inference(scs_inference,[],[i_0_705,i_0_492,i_0_390]) ).
cnf(i_0_899,plain,
~ subclass(unordered_pair(X1,unordered_pair(X2,X3)),null_class),
inference(scs_inference,[],[i_0_705,i_0_426,i_0_390]) ).
cnf(i_0_930,plain,
~ subclass(unordered_pair(unordered_pair(X1,y),X2),intersection(complement(X3),X3)),
inference(rename_variables,[],[i_0_702]) ).
cnf(i_0_933,plain,
~ subclass(unordered_pair(unordered_pair(X1,y),X2),null_class),
inference(rename_variables,[],[i_0_708]) ).
cnf(i_0_971,plain,
null_class != complement(intersection(cross_product(X1,X2),complement(cross_product(X1,X2)))),
inference(scs_inference,[],[i_0_799,i_0_961,i_0_425,i_0_651,i_0_458,i_0_461]) ).
cnf(i_0_939,plain,
~ subclass(unordered_pair(X1,unordered_pair(X2,X3)),intersection(complement(X4),X4)),
inference(rename_variables,[],[i_0_893]) ).
cnf(i_0_942,plain,
~ subclass(unordered_pair(X1,unordered_pair(X2,X3)),null_class),
inference(rename_variables,[],[i_0_899]) ).
cnf(i_0_1839,plain,
~ subclass(unordered_pair(X1,unordered_pair(X2,X3)),null_class),
inference(rename_variables,[],[i_0_899]) ).
cnf(i_0_2069,plain,
~ subclass(unordered_pair(X1,unordered_pair(X2,X3)),intersection(complement(X4),X4)),
inference(rename_variables,[],[i_0_893]) ).
cnf(i_0_771,plain,
~ subclass(unordered_pair(x,X1),intersection(cross_product(X2,X3),complement(cross_product(X2,X3)))),
inference(scs_inference,[],[i_0_510,i_0_763,i_0_584,i_0_745,i_0_539,i_0_422,i_0_435,i_0_390,i_0_389]) ).
cnf(i_0_787,plain,
~ subclass(unordered_pair(X1,x),intersection(cross_product(X2,X3),complement(cross_product(X2,X3)))),
inference(scs_inference,[],[i_0_510,i_0_705,i_0_779,i_0_486,i_0_541,i_0_422,i_0_435,i_0_390,i_0_389]) ).
cnf(i_0_897,plain,
~ subclass(unordered_pair(x,X1),intersection(cross_product(X2,X3),complement(cross_product(X2,X3)))),
inference(rename_variables,[],[i_0_771]) ).
cnf(i_0_918,plain,
~ subclass(unordered_pair(x,X1),intersection(cross_product(X2,X3),complement(cross_product(X2,X3)))),
inference(rename_variables,[],[i_0_771]) ).
cnf(i_0_1206,plain,
member(null_class,omega),
inference(scs_inference,[],[i_0_312,i_0_1058,i_0_682,i_0_634,i_0_513,i_0_433,i_0_419,i_0_1183,i_0_406,i_0_424,i_0_432,i_0_438,i_0_440,i_0_441,i_0_442,i_0_443,i_0_444,i_0_445,i_0_447,i_0_448,i_0_449,i_0_450,i_0_372,i_0_373,i_0_382,i_0_400,i_0_398,i_0_399,i_0_413,i_0_379,i_0_395,i_0_359,i_0_417,i_0_391,i_0_337,i_0_346,i_0_323,i_0_314,i_0_315,i_0_320,i_0_321,i_0_296,i_0_349,i_0_344,i_0_326,i_0_288,i_0_289,i_0_418,i_0_393,i_0_383,i_0_329,i_0_327,i_0_404,i_0_416,i_0_394,i_0_439,i_0_446,i_0_420]) ).
cnf(i_0_1214,plain,
~ member(null_class,unordered_pair(universal_class,universal_class)),
inference(scs_inference,[],[i_0_312,i_0_519,i_0_1058,i_0_682,i_0_634,i_0_513,i_0_433,i_0_419,i_0_1183,i_0_406,i_0_424,i_0_432,i_0_438,i_0_440,i_0_441,i_0_442,i_0_443,i_0_444,i_0_445,i_0_447,i_0_448,i_0_449,i_0_450,i_0_372,i_0_373,i_0_382,i_0_400,i_0_398,i_0_399,i_0_413,i_0_379,i_0_395,i_0_359,i_0_417,i_0_391,i_0_337,i_0_346,i_0_323,i_0_314,i_0_315,i_0_320,i_0_321,i_0_296,i_0_349,i_0_344,i_0_326,i_0_288,i_0_289,i_0_418,i_0_393,i_0_383,i_0_329,i_0_327,i_0_404,i_0_416,i_0_394,i_0_439,i_0_446,i_0_420,i_0_437,i_0_423,i_0_422,i_0_435,i_0_376]) ).
cnf(i_0_1216,plain,
unordered_pair(null_class,null_class) != unordered_pair(universal_class,universal_class),
inference(scs_inference,[],[i_0_312,i_0_519,i_0_1058,i_0_682,i_0_634,i_0_513,i_0_433,i_0_419,i_0_1183,i_0_406,i_0_431,i_0_424,i_0_432,i_0_438,i_0_440,i_0_441,i_0_442,i_0_443,i_0_444,i_0_445,i_0_447,i_0_448,i_0_449,i_0_450,i_0_372,i_0_373,i_0_382,i_0_400,i_0_398,i_0_399,i_0_413,i_0_379,i_0_395,i_0_359,i_0_417,i_0_391,i_0_337,i_0_346,i_0_323,i_0_314,i_0_315,i_0_320,i_0_321,i_0_296,i_0_349,i_0_344,i_0_326,i_0_288,i_0_289,i_0_418,i_0_393,i_0_383,i_0_329,i_0_327,i_0_404,i_0_416,i_0_394,i_0_439,i_0_446,i_0_420,i_0_437,i_0_423,i_0_422,i_0_435,i_0_376,i_0_377]) ).
cnf(i_0_1237,plain,
member(not_subclass_element(omega,intersection(complement(X1),X1)),omega),
inference(scs_inference,[],[i_0_312,i_0_519,i_0_566,i_0_1058,i_0_682,i_0_634,i_0_513,i_0_488,i_0_961,i_0_433,i_0_419,i_0_1183,i_0_406,i_0_1219,i_0_1223,i_0_431,i_0_368,i_0_424,i_0_432,i_0_438,i_0_440,i_0_441,i_0_442,i_0_443,i_0_444,i_0_445,i_0_447,i_0_448,i_0_449,i_0_450,i_0_372,i_0_373,i_0_382,i_0_400,i_0_398,i_0_399,i_0_413,i_0_379,i_0_395,i_0_359,i_0_417,i_0_391,i_0_337,i_0_346,i_0_323,i_0_314,i_0_315,i_0_320,i_0_321,i_0_296,i_0_349,i_0_344,i_0_326,i_0_288,i_0_289,i_0_418,i_0_393,i_0_383,i_0_329,i_0_327,i_0_404,i_0_416,i_0_394,i_0_439,i_0_446,i_0_420,i_0_437,i_0_423,i_0_422,i_0_435,i_0_376,i_0_377,i_0_378,i_0_351,i_0_331,i_0_295,i_0_347,i_0_324,i_0_325,i_0_332,i_0_365]) ).
cnf(i_0_1244,plain,
omega != domain_of(complement(cross_product(unordered_pair(null_class,null_class),universal_class))),
inference(scs_inference,[],[i_0_312,i_0_519,i_0_566,i_0_1058,i_0_682,i_0_631,i_0_634,i_0_513,i_0_579,i_0_488,i_0_961,i_0_433,i_0_419,i_0_1183,i_0_406,i_0_1219,i_0_1223,i_0_431,i_0_368,i_0_424,i_0_432,i_0_438,i_0_440,i_0_441,i_0_442,i_0_443,i_0_444,i_0_445,i_0_447,i_0_448,i_0_449,i_0_450,i_0_372,i_0_373,i_0_382,i_0_400,i_0_398,i_0_399,i_0_413,i_0_379,i_0_395,i_0_359,i_0_417,i_0_391,i_0_337,i_0_346,i_0_323,i_0_314,i_0_315,i_0_320,i_0_321,i_0_296,i_0_349,i_0_344,i_0_326,i_0_288,i_0_289,i_0_418,i_0_393,i_0_383,i_0_329,i_0_327,i_0_404,i_0_416,i_0_394,i_0_439,i_0_446,i_0_420,i_0_437,i_0_423,i_0_422,i_0_435,i_0_376,i_0_377,i_0_378,i_0_351,i_0_331,i_0_295,i_0_347,i_0_324,i_0_325,i_0_332,i_0_365,i_0_363,i_0_364,i_0_460]) ).
cnf(i_0_1251,plain,
~ member(y,X1),
inference(scs_inference,[],[i_0_312,i_0_519,i_0_566,i_0_380,i_0_1058,i_0_682,i_0_631,i_0_634,i_0_513,i_0_579,i_0_488,i_0_961,i_0_427,i_0_1249,i_0_628,i_0_433,i_0_419,i_0_1183,i_0_406,i_0_1219,i_0_1223,i_0_431,i_0_368,i_0_424,i_0_432,i_0_438,i_0_440,i_0_441,i_0_442,i_0_443,i_0_444,i_0_445,i_0_447,i_0_448,i_0_449,i_0_450,i_0_372,i_0_373,i_0_382,i_0_400,i_0_398,i_0_399,i_0_413,i_0_379,i_0_395,i_0_359,i_0_417,i_0_391,i_0_337,i_0_346,i_0_323,i_0_314,i_0_315,i_0_320,i_0_321,i_0_296,i_0_349,i_0_344,i_0_326,i_0_288,i_0_289,i_0_418,i_0_393,i_0_383,i_0_329,i_0_327,i_0_404,i_0_416,i_0_394,i_0_439,i_0_446,i_0_420,i_0_437,i_0_423,i_0_422,i_0_435,i_0_376,i_0_377,i_0_378,i_0_351,i_0_331,i_0_295,i_0_347,i_0_324,i_0_325,i_0_332,i_0_365,i_0_363,i_0_364,i_0_460,i_0_396,i_0_390,i_0_389]) ).
cnf(i_0_915,plain,
~ subclass(unordered_pair(X1,x),intersection(cross_product(X2,X3),complement(cross_product(X2,X3)))),
inference(rename_variables,[],[i_0_787]) ).
cnf(i_0_1348,plain,
~ member(y,X1),
inference(rename_variables,[],[i_0_1251]) ).
cnf(i_0_1405,plain,
~ member(null_class,intersection(unordered_pair(universal_class,universal_class),X1)),
inference(scs_inference,[],[i_0_1214,i_0_1271,i_0_1400,i_0_1162,i_0_1146,i_0_431,i_0_395,i_0_359,i_0_417,i_0_346,i_0_323,i_0_349,i_0_288,i_0_289,i_0_372]) ).
cnf(i_0_1407,plain,
~ member(null_class,intersection(X1,unordered_pair(universal_class,universal_class))),
inference(scs_inference,[],[i_0_1214,i_0_1271,i_0_1400,i_0_1162,i_0_1146,i_0_431,i_0_395,i_0_359,i_0_417,i_0_346,i_0_323,i_0_349,i_0_288,i_0_289,i_0_372,i_0_373]) ).
cnf(i_0_1459,plain,
~ member(y,X1),
inference(rename_variables,[],[i_0_1251]) ).
cnf(i_0_1613,plain,
~ member(y,X1),
inference(rename_variables,[],[i_0_1251]) ).
cnf(i_0_2075,plain,
~ member(y,X1),
inference(rename_variables,[],[i_0_1251]) ).
cnf(i_0_2202,plain,
~ member(y,X1),
inference(rename_variables,[],[i_0_1251]) ).
cnf(i_0_2299,plain,
~ member(y,X1),
inference(rename_variables,[],[i_0_1251]) ).
cnf(i_0_2526,plain,
~ member(y,X1),
inference(rename_variables,[],[i_0_1251]) ).
cnf(i_0_2760,plain,
~ member(y,X1),
inference(rename_variables,[],[i_0_1251]) ).
cnf(i_0_1259,plain,
intersection(complement(X1),X1) != complement(null_class),
inference(scs_inference,[],[i_0_312,i_0_519,i_0_944,i_0_566,i_0_380,i_0_1246,i_0_1058,i_0_682,i_0_631,i_0_634,i_0_849,i_0_513,i_0_579,i_0_488,i_0_577,i_0_1254,i_0_961,i_0_427,i_0_1249,i_0_559,i_0_628,i_0_433,i_0_419,i_0_1183,i_0_406,i_0_1219,i_0_1223,i_0_431,i_0_368,i_0_424,i_0_432,i_0_438,i_0_440,i_0_441,i_0_442,i_0_443,i_0_444,i_0_445,i_0_447,i_0_448,i_0_449,i_0_450,i_0_372,i_0_373,i_0_382,i_0_400,i_0_398,i_0_399,i_0_413,i_0_379,i_0_395,i_0_359,i_0_417,i_0_391,i_0_337,i_0_346,i_0_323,i_0_314,i_0_315,i_0_320,i_0_321,i_0_296,i_0_349,i_0_344,i_0_326,i_0_288,i_0_289,i_0_418,i_0_393,i_0_383,i_0_329,i_0_327,i_0_404,i_0_416,i_0_394,i_0_439,i_0_446,i_0_420,i_0_437,i_0_423,i_0_422,i_0_435,i_0_376,i_0_377,i_0_378,i_0_351,i_0_331,i_0_295,i_0_347,i_0_324,i_0_325,i_0_332,i_0_365,i_0_363,i_0_364,i_0_460,i_0_396,i_0_390,i_0_389,i_0_458,i_0_462,i_0_459,i_0_436]) ).
cnf(i_0_1262,plain,
unordered_pair(omega,omega) != unordered_pair(null_class,null_class),
inference(scs_inference,[],[i_0_312,i_0_519,i_0_944,i_0_566,i_0_582,i_0_380,i_0_1246,i_0_1058,i_0_682,i_0_631,i_0_634,i_0_849,i_0_513,i_0_579,i_0_488,i_0_577,i_0_1254,i_0_961,i_0_427,i_0_1249,i_0_559,i_0_628,i_0_433,i_0_419,i_0_1183,i_0_406,i_0_1219,i_0_1223,i_0_431,i_0_368,i_0_424,i_0_432,i_0_438,i_0_440,i_0_441,i_0_442,i_0_443,i_0_444,i_0_445,i_0_447,i_0_448,i_0_449,i_0_450,i_0_372,i_0_373,i_0_382,i_0_400,i_0_398,i_0_399,i_0_413,i_0_379,i_0_395,i_0_359,i_0_417,i_0_391,i_0_337,i_0_346,i_0_323,i_0_314,i_0_315,i_0_320,i_0_321,i_0_296,i_0_349,i_0_344,i_0_326,i_0_288,i_0_289,i_0_418,i_0_393,i_0_383,i_0_329,i_0_327,i_0_404,i_0_416,i_0_394,i_0_439,i_0_446,i_0_420,i_0_437,i_0_423,i_0_422,i_0_435,i_0_376,i_0_377,i_0_378,i_0_351,i_0_331,i_0_295,i_0_347,i_0_324,i_0_325,i_0_332,i_0_365,i_0_363,i_0_364,i_0_460,i_0_396,i_0_390,i_0_389,i_0_458,i_0_462,i_0_459,i_0_436,i_0_461,i_0_375]) ).
cnf(i_0_1305,plain,
~ subclass(unordered_pair(unordered_pair(X1,X2),X3),null_class),
inference(scs_inference,[],[i_0_1251,i_0_1262,i_0_1136,i_0_1294,i_0_1144,i_0_1154,i_0_1248,i_0_430,i_0_372,i_0_373,i_0_382,i_0_395,i_0_359,i_0_417,i_0_346,i_0_323,i_0_314,i_0_315,i_0_349,i_0_288,i_0_289,i_0_398,i_0_399,i_0_371,i_0_418]) ).
cnf(i_0_1307,plain,
~ member(null_class,complement(omega)),
inference(scs_inference,[],[i_0_1251,i_0_1206,i_0_1262,i_0_1136,i_0_1294,i_0_1144,i_0_1154,i_0_1248,i_0_430,i_0_372,i_0_373,i_0_382,i_0_395,i_0_359,i_0_417,i_0_346,i_0_323,i_0_314,i_0_315,i_0_349,i_0_288,i_0_289,i_0_398,i_0_399,i_0_371,i_0_418,i_0_393]) ).
cnf(i_0_1309,plain,
subclass(unordered_pair(null_class,null_class),omega),
inference(scs_inference,[],[i_0_1251,i_0_1206,i_0_1262,i_0_1136,i_0_1294,i_0_1144,i_0_1154,i_0_1248,i_0_430,i_0_372,i_0_373,i_0_382,i_0_395,i_0_359,i_0_417,i_0_346,i_0_323,i_0_314,i_0_315,i_0_349,i_0_288,i_0_289,i_0_398,i_0_399,i_0_371,i_0_418,i_0_393,i_0_383]) ).
cnf(i_0_1313,plain,
member(regular(unordered_pair(unordered_pair(X1,X2),X3)),unordered_pair(unordered_pair(X1,X2),X3)),
inference(scs_inference,[],[i_0_1251,i_0_1206,i_0_1262,i_0_1136,i_0_1294,i_0_1144,i_0_1154,i_0_1248,i_0_430,i_0_372,i_0_373,i_0_382,i_0_395,i_0_359,i_0_417,i_0_346,i_0_323,i_0_314,i_0_315,i_0_349,i_0_288,i_0_289,i_0_398,i_0_399,i_0_371,i_0_418,i_0_393,i_0_383,i_0_404,i_0_416]) ).
cnf(i_0_1315,plain,
second(unordered_pair(y,y)) = second(null_class),
inference(scs_inference,[],[i_0_1251,i_0_1206,i_0_1262,i_0_1148,i_0_1136,i_0_1294,i_0_1144,i_0_1154,i_0_1248,i_0_430,i_0_372,i_0_373,i_0_382,i_0_395,i_0_359,i_0_417,i_0_346,i_0_323,i_0_314,i_0_315,i_0_349,i_0_288,i_0_289,i_0_398,i_0_399,i_0_371,i_0_418,i_0_393,i_0_383,i_0_404,i_0_416,i_0_438]) ).
cnf(i_0_1316,plain,
cantor(unordered_pair(y,y)) = cantor(null_class),
inference(scs_inference,[],[i_0_1251,i_0_1206,i_0_1262,i_0_1148,i_0_1136,i_0_1294,i_0_1144,i_0_1154,i_0_1248,i_0_430,i_0_372,i_0_373,i_0_382,i_0_395,i_0_359,i_0_417,i_0_346,i_0_323,i_0_314,i_0_315,i_0_349,i_0_288,i_0_289,i_0_398,i_0_399,i_0_371,i_0_418,i_0_393,i_0_383,i_0_404,i_0_416,i_0_438,i_0_440]) ).
cnf(i_0_1317,plain,
not_subclass_element(unordered_pair(y,y),X1) = not_subclass_element(null_class,X1),
inference(scs_inference,[],[i_0_1251,i_0_1206,i_0_1262,i_0_1148,i_0_1136,i_0_1294,i_0_1144,i_0_1154,i_0_1248,i_0_430,i_0_372,i_0_373,i_0_382,i_0_395,i_0_359,i_0_417,i_0_346,i_0_323,i_0_314,i_0_315,i_0_349,i_0_288,i_0_289,i_0_398,i_0_399,i_0_371,i_0_418,i_0_393,i_0_383,i_0_404,i_0_416,i_0_438,i_0_440,i_0_441]) ).
cnf(i_0_1318,plain,
not_subclass_element(X1,unordered_pair(y,y)) = not_subclass_element(X1,null_class),
inference(scs_inference,[],[i_0_1251,i_0_1206,i_0_1262,i_0_1148,i_0_1136,i_0_1294,i_0_1144,i_0_1154,i_0_1248,i_0_430,i_0_372,i_0_373,i_0_382,i_0_395,i_0_359,i_0_417,i_0_346,i_0_323,i_0_314,i_0_315,i_0_349,i_0_288,i_0_289,i_0_398,i_0_399,i_0_371,i_0_418,i_0_393,i_0_383,i_0_404,i_0_416,i_0_438,i_0_440,i_0_441,i_0_442]) ).
cnf(i_0_1319,plain,
member_of(unordered_pair(y,y)) = member_of(null_class),
inference(scs_inference,[],[i_0_1251,i_0_1206,i_0_1262,i_0_1148,i_0_1136,i_0_1294,i_0_1144,i_0_1154,i_0_1248,i_0_430,i_0_372,i_0_373,i_0_382,i_0_395,i_0_359,i_0_417,i_0_346,i_0_323,i_0_314,i_0_315,i_0_349,i_0_288,i_0_289,i_0_398,i_0_399,i_0_371,i_0_418,i_0_393,i_0_383,i_0_404,i_0_416,i_0_438,i_0_440,i_0_441,i_0_442,i_0_443]) ).
cnf(i_0_1320,plain,
intersection(unordered_pair(y,y),X1) = intersection(null_class,X1),
inference(scs_inference,[],[i_0_1251,i_0_1206,i_0_1262,i_0_1148,i_0_1136,i_0_1294,i_0_1144,i_0_1154,i_0_1248,i_0_430,i_0_372,i_0_373,i_0_382,i_0_395,i_0_359,i_0_417,i_0_346,i_0_323,i_0_314,i_0_315,i_0_349,i_0_288,i_0_289,i_0_398,i_0_399,i_0_371,i_0_418,i_0_393,i_0_383,i_0_404,i_0_416,i_0_438,i_0_440,i_0_441,i_0_442,i_0_443,i_0_444]) ).
cnf(i_0_1321,plain,
intersection(X1,unordered_pair(y,y)) = intersection(X1,null_class),
inference(scs_inference,[],[i_0_1251,i_0_1206,i_0_1262,i_0_1148,i_0_1136,i_0_1294,i_0_1144,i_0_1154,i_0_1248,i_0_430,i_0_372,i_0_373,i_0_382,i_0_395,i_0_359,i_0_417,i_0_346,i_0_323,i_0_314,i_0_315,i_0_349,i_0_288,i_0_289,i_0_398,i_0_399,i_0_371,i_0_418,i_0_393,i_0_383,i_0_404,i_0_416,i_0_438,i_0_440,i_0_441,i_0_442,i_0_443,i_0_444,i_0_445]) ).
cnf(i_0_1322,plain,
cross_product(X1,unordered_pair(y,y)) = cross_product(X1,null_class),
inference(scs_inference,[],[i_0_1251,i_0_1206,i_0_1262,i_0_1148,i_0_1136,i_0_1294,i_0_1144,i_0_1154,i_0_1248,i_0_430,i_0_372,i_0_373,i_0_382,i_0_395,i_0_359,i_0_417,i_0_346,i_0_323,i_0_314,i_0_315,i_0_349,i_0_288,i_0_289,i_0_398,i_0_399,i_0_371,i_0_418,i_0_393,i_0_383,i_0_404,i_0_416,i_0_438,i_0_440,i_0_441,i_0_442,i_0_443,i_0_444,i_0_445,i_0_447]) ).
cnf(i_0_1323,plain,
unordered_pair(unordered_pair(y,y),X1) = unordered_pair(null_class,X1),
inference(scs_inference,[],[i_0_1251,i_0_1206,i_0_1262,i_0_1148,i_0_1136,i_0_1294,i_0_1144,i_0_1154,i_0_1248,i_0_430,i_0_372,i_0_373,i_0_382,i_0_395,i_0_359,i_0_417,i_0_346,i_0_323,i_0_314,i_0_315,i_0_349,i_0_288,i_0_289,i_0_398,i_0_399,i_0_371,i_0_418,i_0_393,i_0_383,i_0_404,i_0_416,i_0_438,i_0_440,i_0_441,i_0_442,i_0_443,i_0_444,i_0_445,i_0_447,i_0_448]) ).
cnf(i_0_1324,plain,
unordered_pair(X1,unordered_pair(y,y)) = unordered_pair(X1,null_class),
inference(scs_inference,[],[i_0_1251,i_0_1206,i_0_1262,i_0_1148,i_0_1136,i_0_1294,i_0_1144,i_0_1154,i_0_1248,i_0_430,i_0_372,i_0_373,i_0_382,i_0_395,i_0_359,i_0_417,i_0_346,i_0_323,i_0_314,i_0_315,i_0_349,i_0_288,i_0_289,i_0_398,i_0_399,i_0_371,i_0_418,i_0_393,i_0_383,i_0_404,i_0_416,i_0_438,i_0_440,i_0_441,i_0_442,i_0_443,i_0_444,i_0_445,i_0_447,i_0_448,i_0_449]) ).
cnf(i_0_1325,plain,
first(unordered_pair(y,y)) = first(null_class),
inference(scs_inference,[],[i_0_1251,i_0_1206,i_0_1262,i_0_1148,i_0_1136,i_0_1294,i_0_1144,i_0_1154,i_0_1248,i_0_430,i_0_372,i_0_373,i_0_382,i_0_395,i_0_359,i_0_417,i_0_346,i_0_323,i_0_314,i_0_315,i_0_349,i_0_288,i_0_289,i_0_398,i_0_399,i_0_371,i_0_418,i_0_393,i_0_383,i_0_404,i_0_416,i_0_438,i_0_440,i_0_441,i_0_442,i_0_443,i_0_444,i_0_445,i_0_447,i_0_448,i_0_449,i_0_450]) ).
cnf(i_0_1328,plain,
complement(unordered_pair(y,y)) = complement(null_class),
inference(scs_inference,[],[i_0_1251,i_0_1206,i_0_1262,i_0_1148,i_0_1136,i_0_1294,i_0_1144,i_0_1154,i_0_1245,i_0_1248,i_0_430,i_0_372,i_0_373,i_0_382,i_0_395,i_0_359,i_0_417,i_0_346,i_0_323,i_0_314,i_0_315,i_0_349,i_0_288,i_0_289,i_0_398,i_0_399,i_0_371,i_0_418,i_0_393,i_0_383,i_0_404,i_0_416,i_0_438,i_0_440,i_0_441,i_0_442,i_0_443,i_0_444,i_0_445,i_0_447,i_0_448,i_0_449,i_0_450,i_0_394,i_0_439]) ).
cnf(i_0_1329,plain,
cross_product(unordered_pair(y,y),X1) = cross_product(null_class,X1),
inference(scs_inference,[],[i_0_1251,i_0_1206,i_0_1262,i_0_1148,i_0_1136,i_0_1294,i_0_1144,i_0_1154,i_0_1245,i_0_1248,i_0_430,i_0_372,i_0_373,i_0_382,i_0_395,i_0_359,i_0_417,i_0_346,i_0_323,i_0_314,i_0_315,i_0_349,i_0_288,i_0_289,i_0_398,i_0_399,i_0_371,i_0_418,i_0_393,i_0_383,i_0_404,i_0_416,i_0_438,i_0_440,i_0_441,i_0_442,i_0_443,i_0_444,i_0_445,i_0_447,i_0_448,i_0_449,i_0_450,i_0_394,i_0_439,i_0_446]) ).
cnf(i_0_1330,plain,
domain_of(unordered_pair(y,y)) = domain_of(null_class),
inference(scs_inference,[],[i_0_1251,i_0_1206,i_0_1262,i_0_1148,i_0_1136,i_0_1294,i_0_1144,i_0_1154,i_0_1245,i_0_1248,i_0_430,i_0_372,i_0_373,i_0_382,i_0_395,i_0_359,i_0_417,i_0_346,i_0_323,i_0_314,i_0_315,i_0_349,i_0_288,i_0_289,i_0_398,i_0_399,i_0_371,i_0_418,i_0_393,i_0_383,i_0_404,i_0_416,i_0_438,i_0_440,i_0_441,i_0_442,i_0_443,i_0_444,i_0_445,i_0_447,i_0_448,i_0_449,i_0_450,i_0_394,i_0_439,i_0_446,i_0_437]) ).
cnf(i_0_1331,plain,
null_class != omega,
inference(scs_inference,[],[i_0_1251,i_0_1188,i_0_1206,i_0_1262,i_0_1148,i_0_1136,i_0_1294,i_0_1144,i_0_1154,i_0_1245,i_0_1248,i_0_430,i_0_372,i_0_373,i_0_382,i_0_395,i_0_359,i_0_417,i_0_346,i_0_323,i_0_314,i_0_315,i_0_349,i_0_288,i_0_289,i_0_398,i_0_399,i_0_371,i_0_418,i_0_393,i_0_383,i_0_404,i_0_416,i_0_438,i_0_440,i_0_441,i_0_442,i_0_443,i_0_444,i_0_445,i_0_447,i_0_448,i_0_449,i_0_450,i_0_394,i_0_439,i_0_446,i_0_437,i_0_423]) ).
cnf(i_0_1335,plain,
unordered_pair(null_class,null_class) != unordered_pair(omega,omega),
inference(scs_inference,[],[i_0_1251,i_0_1188,i_0_1206,i_0_1262,i_0_1148,i_0_1136,i_0_1294,i_0_1144,i_0_1154,i_0_1245,i_0_1248,i_0_430,i_0_372,i_0_373,i_0_382,i_0_395,i_0_359,i_0_417,i_0_346,i_0_323,i_0_314,i_0_315,i_0_349,i_0_288,i_0_289,i_0_398,i_0_399,i_0_371,i_0_418,i_0_393,i_0_383,i_0_404,i_0_416,i_0_438,i_0_440,i_0_441,i_0_442,i_0_443,i_0_444,i_0_445,i_0_447,i_0_448,i_0_449,i_0_450,i_0_394,i_0_439,i_0_446,i_0_437,i_0_423,i_0_422,i_0_435]) ).
cnf(i_0_1356,plain,
intersection(complement(X1),X1) != complement(null_class),
inference(rename_variables,[],[i_0_1259]) ).
cnf(i_0_1361,plain,
member(null_class,intersection(omega,omega)),
inference(scs_inference,[],[i_0_1251,i_0_1188,i_0_1206,i_0_1262,i_0_1148,i_0_1136,i_0_1294,i_0_1138,i_0_1216,i_0_1198,i_0_1259,i_0_1144,i_0_1154,i_0_1245,i_0_1248,i_0_430,i_0_406,i_0_1337,i_0_1340,i_0_1345,i_0_372,i_0_373,i_0_382,i_0_395,i_0_359,i_0_417,i_0_346,i_0_323,i_0_314,i_0_315,i_0_349,i_0_288,i_0_289,i_0_398,i_0_399,i_0_371,i_0_418,i_0_393,i_0_383,i_0_404,i_0_416,i_0_438,i_0_440,i_0_441,i_0_442,i_0_443,i_0_444,i_0_445,i_0_447,i_0_448,i_0_449,i_0_450,i_0_394,i_0_439,i_0_446,i_0_437,i_0_423,i_0_422,i_0_435,i_0_377,i_0_378,i_0_331,i_0_324,i_0_332,i_0_376,i_0_325,i_0_365,i_0_363,i_0_364]) ).
cnf(i_0_1363,plain,
~ inductive(unordered_pair(y,y)),
inference(scs_inference,[],[i_0_1251,i_0_1188,i_0_1206,i_0_1262,i_0_1148,i_0_1136,i_0_1294,i_0_1138,i_0_1216,i_0_1198,i_0_1259,i_0_1144,i_0_1154,i_0_1245,i_0_1248,i_0_498,i_0_430,i_0_406,i_0_1337,i_0_1340,i_0_1345,i_0_372,i_0_373,i_0_382,i_0_395,i_0_359,i_0_417,i_0_346,i_0_323,i_0_314,i_0_315,i_0_349,i_0_288,i_0_289,i_0_398,i_0_399,i_0_371,i_0_418,i_0_393,i_0_383,i_0_404,i_0_416,i_0_438,i_0_440,i_0_441,i_0_442,i_0_443,i_0_444,i_0_445,i_0_447,i_0_448,i_0_449,i_0_450,i_0_394,i_0_439,i_0_446,i_0_437,i_0_423,i_0_422,i_0_435,i_0_377,i_0_378,i_0_331,i_0_324,i_0_332,i_0_376,i_0_325,i_0_365,i_0_363,i_0_364,i_0_460]) ).
cnf(i_0_1364,plain,
~ subclass(universal_class,domain_of(complement(cross_product(unordered_pair(x,x),universal_class)))),
inference(scs_inference,[],[i_0_1251,i_0_1188,i_0_1206,i_0_1262,i_0_1148,i_0_1136,i_0_1294,i_0_1138,i_0_1216,i_0_1198,i_0_1259,i_0_1144,i_0_1154,i_0_573,i_0_1245,i_0_1248,i_0_498,i_0_427,i_0_430,i_0_406,i_0_1337,i_0_1340,i_0_1345,i_0_372,i_0_373,i_0_382,i_0_395,i_0_359,i_0_417,i_0_346,i_0_323,i_0_314,i_0_315,i_0_349,i_0_288,i_0_289,i_0_398,i_0_399,i_0_371,i_0_418,i_0_393,i_0_383,i_0_404,i_0_416,i_0_438,i_0_440,i_0_441,i_0_442,i_0_443,i_0_444,i_0_445,i_0_447,i_0_448,i_0_449,i_0_450,i_0_394,i_0_439,i_0_446,i_0_437,i_0_423,i_0_422,i_0_435,i_0_377,i_0_378,i_0_331,i_0_324,i_0_332,i_0_376,i_0_325,i_0_365,i_0_363,i_0_364,i_0_460,i_0_396]) ).
cnf(i_0_1369,plain,
member(intersection(complement(X1),X1),omega),
inference(scs_inference,[],[i_0_1251,i_0_1188,i_0_1206,i_0_1262,i_0_1148,i_0_1136,i_0_1294,i_0_1138,i_0_1216,i_0_1198,i_0_1259,i_0_1144,i_0_1154,i_0_573,i_0_1160,i_0_1245,i_0_1248,i_0_622,i_0_498,i_0_427,i_0_559,i_0_430,i_0_406,i_0_1337,i_0_1340,i_0_1345,i_0_372,i_0_373,i_0_382,i_0_395,i_0_359,i_0_417,i_0_346,i_0_323,i_0_314,i_0_315,i_0_349,i_0_288,i_0_289,i_0_398,i_0_399,i_0_371,i_0_418,i_0_393,i_0_383,i_0_404,i_0_416,i_0_438,i_0_440,i_0_441,i_0_442,i_0_443,i_0_444,i_0_445,i_0_447,i_0_448,i_0_449,i_0_450,i_0_394,i_0_439,i_0_446,i_0_437,i_0_423,i_0_422,i_0_435,i_0_377,i_0_378,i_0_331,i_0_324,i_0_332,i_0_376,i_0_325,i_0_365,i_0_363,i_0_364,i_0_460,i_0_396,i_0_390,i_0_458]) ).
cnf(i_0_1372,plain,
omega != intersection(null_class,X1),
inference(scs_inference,[],[i_0_1251,i_0_1188,i_0_1206,i_0_1262,i_0_1148,i_0_1136,i_0_1294,i_0_1297,i_0_1138,i_0_1216,i_0_1198,i_0_1259,i_0_1144,i_0_1154,i_0_573,i_0_1192,i_0_1160,i_0_1245,i_0_1248,i_0_622,i_0_498,i_0_800,i_0_427,i_0_559,i_0_430,i_0_406,i_0_1337,i_0_1340,i_0_1345,i_0_372,i_0_373,i_0_382,i_0_395,i_0_359,i_0_417,i_0_346,i_0_323,i_0_314,i_0_315,i_0_349,i_0_288,i_0_289,i_0_398,i_0_399,i_0_371,i_0_418,i_0_393,i_0_383,i_0_404,i_0_416,i_0_438,i_0_440,i_0_441,i_0_442,i_0_443,i_0_444,i_0_445,i_0_447,i_0_448,i_0_449,i_0_450,i_0_394,i_0_439,i_0_446,i_0_437,i_0_423,i_0_422,i_0_435,i_0_377,i_0_378,i_0_331,i_0_324,i_0_332,i_0_376,i_0_325,i_0_365,i_0_363,i_0_364,i_0_460,i_0_396,i_0_390,i_0_458,i_0_462,i_0_459]) ).
cnf(i_0_1374,plain,
unordered_pair(y,y) = intersection(complement(X1),X1),
inference(scs_inference,[],[i_0_1251,i_0_1188,i_0_1206,i_0_1262,i_0_1148,i_0_1136,i_0_1294,i_0_1297,i_0_1138,i_0_1216,i_0_1198,i_0_1259,i_0_1144,i_0_1154,i_0_573,i_0_1192,i_0_1160,i_0_1245,i_0_1248,i_0_622,i_0_498,i_0_800,i_0_427,i_0_559,i_0_430,i_0_406,i_0_1337,i_0_1340,i_0_1345,i_0_372,i_0_373,i_0_382,i_0_395,i_0_359,i_0_417,i_0_346,i_0_323,i_0_314,i_0_315,i_0_349,i_0_288,i_0_289,i_0_398,i_0_399,i_0_371,i_0_418,i_0_393,i_0_383,i_0_404,i_0_416,i_0_438,i_0_440,i_0_441,i_0_442,i_0_443,i_0_444,i_0_445,i_0_447,i_0_448,i_0_449,i_0_450,i_0_394,i_0_439,i_0_446,i_0_437,i_0_423,i_0_422,i_0_435,i_0_377,i_0_378,i_0_331,i_0_324,i_0_332,i_0_376,i_0_325,i_0_365,i_0_363,i_0_364,i_0_460,i_0_396,i_0_390,i_0_458,i_0_462,i_0_459,i_0_436]) ).
cnf(i_0_1409,plain,
~ member(null_class,unordered_pair(omega,omega)),
inference(scs_inference,[],[i_0_1331,i_0_1214,i_0_1271,i_0_1400,i_0_1162,i_0_1146,i_0_431,i_0_395,i_0_359,i_0_417,i_0_346,i_0_323,i_0_349,i_0_288,i_0_289,i_0_372,i_0_373,i_0_382]) ).
cnf(i_0_1423,plain,
~ member(regular(omega),complement(omega)),
inference(scs_inference,[],[i_0_1331,i_0_1200,i_0_1214,i_0_1271,i_0_1400,i_0_1299,i_0_1364,i_0_1162,i_0_1146,i_0_431,i_0_395,i_0_359,i_0_417,i_0_346,i_0_323,i_0_349,i_0_288,i_0_289,i_0_372,i_0_373,i_0_382,i_0_314,i_0_315,i_0_398,i_0_399,i_0_371,i_0_418,i_0_393]) ).
cnf(i_0_1425,plain,
subclass(unordered_pair(regular(omega),regular(omega)),omega),
inference(scs_inference,[],[i_0_1331,i_0_1200,i_0_1214,i_0_1271,i_0_1400,i_0_1299,i_0_1364,i_0_1162,i_0_1146,i_0_431,i_0_395,i_0_359,i_0_417,i_0_346,i_0_323,i_0_349,i_0_288,i_0_289,i_0_372,i_0_373,i_0_382,i_0_314,i_0_315,i_0_398,i_0_399,i_0_371,i_0_418,i_0_393,i_0_383]) ).
cnf(i_0_1433,plain,
second(not_subclass_element(unordered_pair(y,y),X1)) = second(not_subclass_element(null_class,X1)),
inference(scs_inference,[],[i_0_1331,i_0_1200,i_0_1214,i_0_1317,i_0_1271,i_0_1400,i_0_1299,i_0_1364,i_0_1162,i_0_1146,i_0_431,i_0_395,i_0_359,i_0_417,i_0_346,i_0_323,i_0_349,i_0_288,i_0_289,i_0_372,i_0_373,i_0_382,i_0_314,i_0_315,i_0_398,i_0_399,i_0_371,i_0_418,i_0_393,i_0_383,i_0_404,i_0_416,i_0_394,i_0_438]) ).
cnf(i_0_1434,plain,
cantor(not_subclass_element(unordered_pair(y,y),X1)) = cantor(not_subclass_element(null_class,X1)),
inference(scs_inference,[],[i_0_1331,i_0_1200,i_0_1214,i_0_1317,i_0_1271,i_0_1400,i_0_1299,i_0_1364,i_0_1162,i_0_1146,i_0_431,i_0_395,i_0_359,i_0_417,i_0_346,i_0_323,i_0_349,i_0_288,i_0_289,i_0_372,i_0_373,i_0_382,i_0_314,i_0_315,i_0_398,i_0_399,i_0_371,i_0_418,i_0_393,i_0_383,i_0_404,i_0_416,i_0_394,i_0_438,i_0_440]) ).
cnf(i_0_1443,plain,
first(not_subclass_element(unordered_pair(y,y),X1)) = first(not_subclass_element(null_class,X1)),
inference(scs_inference,[],[i_0_1331,i_0_1200,i_0_1214,i_0_1317,i_0_1271,i_0_1400,i_0_1299,i_0_1364,i_0_1162,i_0_1146,i_0_431,i_0_395,i_0_359,i_0_417,i_0_346,i_0_323,i_0_349,i_0_288,i_0_289,i_0_372,i_0_373,i_0_382,i_0_314,i_0_315,i_0_398,i_0_399,i_0_371,i_0_418,i_0_393,i_0_383,i_0_404,i_0_416,i_0_394,i_0_438,i_0_440,i_0_441,i_0_442,i_0_443,i_0_444,i_0_445,i_0_447,i_0_448,i_0_449,i_0_450]) ).
cnf(i_0_1447,plain,
null_class != unordered_pair(unordered_pair(X1,X2),X3),
inference(scs_inference,[],[i_0_1331,i_0_1200,i_0_1214,i_0_1317,i_0_1271,i_0_1400,i_0_1305,i_0_1299,i_0_1364,i_0_1162,i_0_1146,i_0_431,i_0_395,i_0_359,i_0_417,i_0_346,i_0_323,i_0_349,i_0_288,i_0_289,i_0_372,i_0_373,i_0_382,i_0_314,i_0_315,i_0_398,i_0_399,i_0_371,i_0_418,i_0_393,i_0_383,i_0_404,i_0_416,i_0_394,i_0_438,i_0_440,i_0_441,i_0_442,i_0_443,i_0_444,i_0_445,i_0_447,i_0_448,i_0_449,i_0_450,i_0_439,i_0_446,i_0_437,i_0_423]) ).
cnf(i_0_1451,plain,
intersection(null_class,X1) != omega,
inference(scs_inference,[],[i_0_1331,i_0_1372,i_0_1200,i_0_1214,i_0_1317,i_0_1271,i_0_1400,i_0_1305,i_0_1299,i_0_1364,i_0_1162,i_0_1146,i_0_932,i_0_431,i_0_395,i_0_359,i_0_417,i_0_346,i_0_323,i_0_349,i_0_288,i_0_289,i_0_372,i_0_373,i_0_382,i_0_314,i_0_315,i_0_398,i_0_399,i_0_371,i_0_418,i_0_393,i_0_383,i_0_404,i_0_416,i_0_394,i_0_438,i_0_440,i_0_441,i_0_442,i_0_443,i_0_444,i_0_445,i_0_447,i_0_448,i_0_449,i_0_450,i_0_439,i_0_446,i_0_437,i_0_423,i_0_422,i_0_435]) ).
cnf(i_0_1452,plain,
unordered_pair(omega,omega) != unordered_pair(intersection(null_class,X1),intersection(null_class,X1)),
inference(scs_inference,[],[i_0_1331,i_0_1372,i_0_1200,i_0_1214,i_0_1317,i_0_1271,i_0_1400,i_0_1305,i_0_1299,i_0_1364,i_0_1162,i_0_1146,i_0_932,i_0_430,i_0_431,i_0_395,i_0_359,i_0_417,i_0_346,i_0_323,i_0_349,i_0_288,i_0_289,i_0_372,i_0_373,i_0_382,i_0_314,i_0_315,i_0_398,i_0_399,i_0_371,i_0_418,i_0_393,i_0_383,i_0_404,i_0_416,i_0_394,i_0_438,i_0_440,i_0_441,i_0_442,i_0_443,i_0_444,i_0_445,i_0_447,i_0_448,i_0_449,i_0_450,i_0_439,i_0_446,i_0_437,i_0_423,i_0_422,i_0_435,i_0_377]) ).
cnf(i_0_1467,plain,
member(not_subclass_element(omega,intersection(null_class,intersection(null_class,X1))),omega),
inference(scs_inference,[],[i_0_1331,i_0_1335,i_0_1372,i_0_1200,i_0_1214,i_0_1317,i_0_1271,i_0_1400,i_0_1273,i_0_1305,i_0_1299,i_0_1364,i_0_1162,i_0_1146,i_0_932,i_0_1251,i_0_430,i_0_431,i_0_395,i_0_359,i_0_417,i_0_346,i_0_323,i_0_349,i_0_288,i_0_289,i_0_372,i_0_373,i_0_382,i_0_314,i_0_315,i_0_398,i_0_399,i_0_371,i_0_418,i_0_393,i_0_383,i_0_404,i_0_416,i_0_394,i_0_438,i_0_440,i_0_441,i_0_442,i_0_443,i_0_444,i_0_445,i_0_447,i_0_448,i_0_449,i_0_450,i_0_439,i_0_446,i_0_437,i_0_423,i_0_422,i_0_435,i_0_377,i_0_331,i_0_324,i_0_332,i_0_378,i_0_325,i_0_376,i_0_365]) ).
cnf(i_0_1469,plain,
omega != intersection(null_class,X1),
inference(rename_variables,[],[i_0_1372]) ).
cnf(i_0_1471,plain,
subclass(unordered_pair(null_class,null_class),intersection(omega,omega)),
inference(scs_inference,[],[i_0_1331,i_0_1335,i_0_1372,i_0_1200,i_0_1214,i_0_1361,i_0_1317,i_0_1271,i_0_1400,i_0_1273,i_0_1305,i_0_1299,i_0_1364,i_0_1162,i_0_1146,i_0_932,i_0_1251,i_0_430,i_0_431,i_0_395,i_0_359,i_0_417,i_0_346,i_0_323,i_0_349,i_0_288,i_0_289,i_0_372,i_0_373,i_0_382,i_0_314,i_0_315,i_0_398,i_0_399,i_0_371,i_0_418,i_0_393,i_0_383,i_0_404,i_0_416,i_0_394,i_0_438,i_0_440,i_0_441,i_0_442,i_0_443,i_0_444,i_0_445,i_0_447,i_0_448,i_0_449,i_0_450,i_0_439,i_0_446,i_0_437,i_0_423,i_0_422,i_0_435,i_0_377,i_0_331,i_0_324,i_0_332,i_0_378,i_0_325,i_0_376,i_0_365,i_0_363]) ).
cnf(i_0_1473,plain,
member(regular(omega),intersection(omega,omega)),
inference(scs_inference,[],[i_0_1331,i_0_1335,i_0_1372,i_0_1200,i_0_1214,i_0_1361,i_0_1317,i_0_1271,i_0_1400,i_0_1273,i_0_1305,i_0_1299,i_0_1364,i_0_1162,i_0_1146,i_0_932,i_0_1251,i_0_430,i_0_431,i_0_395,i_0_359,i_0_417,i_0_346,i_0_323,i_0_349,i_0_288,i_0_289,i_0_372,i_0_373,i_0_382,i_0_314,i_0_315,i_0_398,i_0_399,i_0_371,i_0_418,i_0_393,i_0_383,i_0_404,i_0_416,i_0_394,i_0_438,i_0_440,i_0_441,i_0_442,i_0_443,i_0_444,i_0_445,i_0_447,i_0_448,i_0_449,i_0_450,i_0_439,i_0_446,i_0_437,i_0_423,i_0_422,i_0_435,i_0_377,i_0_331,i_0_324,i_0_332,i_0_378,i_0_325,i_0_376,i_0_365,i_0_363,i_0_364]) ).
cnf(i_0_1479,plain,
~ inductive(member_of(unordered_pair(unordered_pair(y,y),unordered_pair(y,y)))),
inference(scs_inference,[],[i_0_1331,i_0_1335,i_0_1363,i_0_1372,i_0_1200,i_0_1214,i_0_1361,i_0_1317,i_0_1271,i_0_1400,i_0_1273,i_0_1305,i_0_1152,i_0_1299,i_0_1364,i_0_1162,i_0_1352,i_0_1146,i_0_932,i_0_380,i_0_1251,i_0_430,i_0_431,i_0_395,i_0_359,i_0_417,i_0_346,i_0_323,i_0_349,i_0_288,i_0_289,i_0_372,i_0_373,i_0_382,i_0_314,i_0_315,i_0_398,i_0_399,i_0_371,i_0_418,i_0_393,i_0_383,i_0_404,i_0_416,i_0_394,i_0_438,i_0_440,i_0_441,i_0_442,i_0_443,i_0_444,i_0_445,i_0_447,i_0_448,i_0_449,i_0_450,i_0_439,i_0_446,i_0_437,i_0_423,i_0_422,i_0_435,i_0_377,i_0_331,i_0_324,i_0_332,i_0_378,i_0_325,i_0_376,i_0_365,i_0_363,i_0_364,i_0_396,i_0_460]) ).
cnf(i_0_1481,plain,
~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(y,y))),choice),
inference(scs_inference,[],[i_0_1331,i_0_1335,i_0_1363,i_0_1372,i_0_1200,i_0_1214,i_0_1361,i_0_1317,i_0_1271,i_0_1400,i_0_1273,i_0_1305,i_0_1152,i_0_1172,i_0_1299,i_0_1364,i_0_1162,i_0_1352,i_0_1142,i_0_1146,i_0_932,i_0_380,i_0_1251,i_0_430,i_0_431,i_0_395,i_0_359,i_0_417,i_0_346,i_0_323,i_0_349,i_0_288,i_0_289,i_0_372,i_0_373,i_0_382,i_0_314,i_0_315,i_0_398,i_0_399,i_0_371,i_0_418,i_0_393,i_0_383,i_0_404,i_0_416,i_0_394,i_0_438,i_0_440,i_0_441,i_0_442,i_0_443,i_0_444,i_0_445,i_0_447,i_0_448,i_0_449,i_0_450,i_0_439,i_0_446,i_0_437,i_0_423,i_0_422,i_0_435,i_0_377,i_0_331,i_0_324,i_0_332,i_0_378,i_0_325,i_0_376,i_0_365,i_0_363,i_0_364,i_0_396,i_0_460,i_0_389]) ).
cnf(i_0_1487,plain,
member(intersection(complement(unordered_pair(y,y)),null_class),omega),
inference(scs_inference,[],[i_0_1331,i_0_1335,i_0_1363,i_0_1372,i_0_1200,i_0_1214,i_0_1361,i_0_1317,i_0_1321,i_0_1271,i_0_1400,i_0_1273,i_0_1305,i_0_1369,i_0_1152,i_0_1172,i_0_1299,i_0_1364,i_0_1162,i_0_1352,i_0_1142,i_0_1146,i_0_932,i_0_1245,i_0_484,i_0_380,i_0_1251,i_0_430,i_0_431,i_0_395,i_0_359,i_0_417,i_0_346,i_0_323,i_0_349,i_0_288,i_0_289,i_0_372,i_0_373,i_0_382,i_0_314,i_0_315,i_0_398,i_0_399,i_0_371,i_0_418,i_0_393,i_0_383,i_0_404,i_0_416,i_0_394,i_0_438,i_0_440,i_0_441,i_0_442,i_0_443,i_0_444,i_0_445,i_0_447,i_0_448,i_0_449,i_0_450,i_0_439,i_0_446,i_0_437,i_0_423,i_0_422,i_0_435,i_0_377,i_0_331,i_0_324,i_0_332,i_0_378,i_0_325,i_0_376,i_0_365,i_0_363,i_0_364,i_0_396,i_0_460,i_0_389,i_0_390,i_0_458]) ).
cnf(i_0_1488,plain,
intersection(X1,unordered_pair(y,y)) = intersection(X1,null_class),
inference(rename_variables,[],[i_0_1321]) ).
cnf(i_0_1489,plain,
member(intersection(complement(X1),X1),omega),
inference(rename_variables,[],[i_0_1369]) ).
cnf(i_0_1490,plain,
subclass(unordered_pair(y,unordered_pair(y,y)),unordered_pair(null_class,unordered_pair(y,y))),
inference(scs_inference,[],[i_0_1331,i_0_1335,i_0_1363,i_0_1372,i_0_1200,i_0_1214,i_0_1361,i_0_1317,i_0_1321,i_0_1323,i_0_1271,i_0_1400,i_0_1273,i_0_1305,i_0_1369,i_0_1152,i_0_1172,i_0_1299,i_0_1364,i_0_1162,i_0_1352,i_0_1142,i_0_1146,i_0_537,i_0_932,i_0_1245,i_0_484,i_0_380,i_0_1251,i_0_430,i_0_431,i_0_395,i_0_359,i_0_417,i_0_346,i_0_323,i_0_349,i_0_288,i_0_289,i_0_372,i_0_373,i_0_382,i_0_314,i_0_315,i_0_398,i_0_399,i_0_371,i_0_418,i_0_393,i_0_383,i_0_404,i_0_416,i_0_394,i_0_438,i_0_440,i_0_441,i_0_442,i_0_443,i_0_444,i_0_445,i_0_447,i_0_448,i_0_449,i_0_450,i_0_439,i_0_446,i_0_437,i_0_423,i_0_422,i_0_435,i_0_377,i_0_331,i_0_324,i_0_332,i_0_378,i_0_325,i_0_376,i_0_365,i_0_363,i_0_364,i_0_396,i_0_460,i_0_389,i_0_390,i_0_458,i_0_462]) ).
cnf(i_0_1491,plain,
unordered_pair(unordered_pair(y,y),X1) = unordered_pair(null_class,X1),
inference(rename_variables,[],[i_0_1323]) ).
cnf(i_0_1494,plain,
unordered_pair(unordered_pair(y,y),X1) = unordered_pair(null_class,X1),
inference(rename_variables,[],[i_0_1323]) ).
cnf(i_0_1495,plain,
member(regular(unordered_pair(unordered_pair(X1,X2),X3)),unordered_pair(unordered_pair(X1,X2),X3)),
inference(rename_variables,[],[i_0_1313]) ).
cnf(i_0_1499,plain,
intersection(X1,unordered_pair(y,y)) = intersection(X1,null_class),
inference(rename_variables,[],[i_0_1321]) ).
cnf(i_0_1618,plain,
not_subclass_element(X1,unordered_pair(y,y)) = not_subclass_element(X1,null_class),
inference(rename_variables,[],[i_0_1318]) ).
cnf(i_0_1722,plain,
intersection(unordered_pair(y,y),X1) = intersection(null_class,X1),
inference(rename_variables,[],[i_0_1320]) ).
cnf(i_0_1724,plain,
unordered_pair(X1,unordered_pair(y,y)) = unordered_pair(X1,null_class),
inference(rename_variables,[],[i_0_1324]) ).
cnf(i_0_1726,plain,
cross_product(X1,unordered_pair(y,y)) = cross_product(X1,null_class),
inference(rename_variables,[],[i_0_1322]) ).
cnf(i_0_1730,plain,
unordered_pair(X1,unordered_pair(y,y)) = unordered_pair(X1,null_class),
inference(rename_variables,[],[i_0_1324]) ).
cnf(i_0_1849,plain,
cross_product(unordered_pair(y,y),X1) = cross_product(null_class,X1),
inference(rename_variables,[],[i_0_1329]) ).
cnf(i_0_1960,plain,
unordered_pair(y,y) = intersection(complement(X1),X1),
inference(rename_variables,[],[i_0_1374]) ).
cnf(i_0_2405,plain,
~ subclass(unordered_pair(unordered_pair(X1,X2),X3),null_class),
inference(rename_variables,[],[i_0_1305]) ).
cnf(i_0_1493,plain,
member(regular(unordered_pair(unordered_pair(y,y),X1)),unordered_pair(null_class,X1)),
inference(scs_inference,[],[i_0_1331,i_0_1335,i_0_1363,i_0_1372,i_0_1200,i_0_1214,i_0_1361,i_0_1317,i_0_1321,i_0_1323,i_0_1491,i_0_1271,i_0_1400,i_0_1273,i_0_1305,i_0_1369,i_0_1152,i_0_1172,i_0_1313,i_0_1299,i_0_1364,i_0_1162,i_0_1352,i_0_1142,i_0_1146,i_0_537,i_0_932,i_0_1245,i_0_484,i_0_380,i_0_1251,i_0_430,i_0_431,i_0_395,i_0_359,i_0_417,i_0_346,i_0_323,i_0_349,i_0_288,i_0_289,i_0_372,i_0_373,i_0_382,i_0_314,i_0_315,i_0_398,i_0_399,i_0_371,i_0_418,i_0_393,i_0_383,i_0_404,i_0_416,i_0_394,i_0_438,i_0_440,i_0_441,i_0_442,i_0_443,i_0_444,i_0_445,i_0_447,i_0_448,i_0_449,i_0_450,i_0_439,i_0_446,i_0_437,i_0_423,i_0_422,i_0_435,i_0_377,i_0_331,i_0_324,i_0_332,i_0_378,i_0_325,i_0_376,i_0_365,i_0_363,i_0_364,i_0_396,i_0_460,i_0_389,i_0_390,i_0_458,i_0_462,i_0_459]) ).
cnf(i_0_1528,plain,
~ member(null_class,intersection(unordered_pair(omega,omega),X1)),
inference(scs_inference,[],[i_0_1409,i_0_1166,i_0_1523,i_0_568,i_0_477,i_0_395,i_0_359,i_0_417,i_0_346,i_0_323,i_0_288,i_0_289,i_0_372]) ).
cnf(i_0_1530,plain,
~ member(null_class,intersection(X1,unordered_pair(omega,omega))),
inference(scs_inference,[],[i_0_1409,i_0_1166,i_0_1523,i_0_568,i_0_477,i_0_395,i_0_359,i_0_417,i_0_346,i_0_323,i_0_288,i_0_289,i_0_372,i_0_373]) ).
cnf(i_0_1536,plain,
unordered_pair(member_of(unordered_pair(x,x)),member_of(unordered_pair(x,x))) = unordered_pair(x,x),
inference(scs_inference,[],[i_0_1409,i_0_1166,i_0_1523,i_0_568,i_0_477,i_0_395,i_0_359,i_0_417,i_0_346,i_0_323,i_0_288,i_0_289,i_0_372,i_0_373,i_0_314,i_0_315,i_0_349]) ).
cnf(i_0_1538,plain,
~ member(intersection(null_class,X1),unordered_pair(omega,omega)),
inference(scs_inference,[],[i_0_1409,i_0_1451,i_0_1166,i_0_1523,i_0_568,i_0_477,i_0_395,i_0_359,i_0_417,i_0_346,i_0_323,i_0_288,i_0_289,i_0_372,i_0_373,i_0_314,i_0_315,i_0_349,i_0_382]) ).
cnf(i_0_1548,plain,
~ member(regular(omega),complement(intersection(omega,omega))),
inference(scs_inference,[],[i_0_1409,i_0_1473,i_0_1451,i_0_1166,i_0_1523,i_0_1484,i_0_1415,i_0_1431,i_0_568,i_0_477,i_0_395,i_0_359,i_0_417,i_0_346,i_0_323,i_0_288,i_0_289,i_0_372,i_0_373,i_0_314,i_0_315,i_0_349,i_0_382,i_0_398,i_0_399,i_0_371,i_0_418,i_0_393]) ).
cnf(i_0_1550,plain,
subclass(unordered_pair(regular(omega),regular(omega)),intersection(omega,omega)),
inference(scs_inference,[],[i_0_1409,i_0_1473,i_0_1451,i_0_1166,i_0_1523,i_0_1484,i_0_1415,i_0_1431,i_0_568,i_0_477,i_0_395,i_0_359,i_0_417,i_0_346,i_0_323,i_0_288,i_0_289,i_0_372,i_0_373,i_0_314,i_0_315,i_0_349,i_0_382,i_0_398,i_0_399,i_0_371,i_0_418,i_0_393,i_0_383]) ).
cnf(i_0_1558,plain,
second(not_subclass_element(X1,unordered_pair(y,y))) = second(not_subclass_element(X1,null_class)),
inference(scs_inference,[],[i_0_1409,i_0_1473,i_0_1451,i_0_1318,i_0_1166,i_0_1523,i_0_1484,i_0_1449,i_0_1415,i_0_1431,i_0_568,i_0_477,i_0_395,i_0_359,i_0_417,i_0_346,i_0_323,i_0_288,i_0_289,i_0_372,i_0_373,i_0_314,i_0_315,i_0_349,i_0_382,i_0_398,i_0_399,i_0_371,i_0_418,i_0_393,i_0_383,i_0_404,i_0_416,i_0_394,i_0_438]) ).
cnf(i_0_1559,plain,
cantor(not_subclass_element(X1,unordered_pair(y,y))) = cantor(not_subclass_element(X1,null_class)),
inference(scs_inference,[],[i_0_1409,i_0_1473,i_0_1451,i_0_1318,i_0_1166,i_0_1523,i_0_1484,i_0_1449,i_0_1415,i_0_1431,i_0_568,i_0_477,i_0_395,i_0_359,i_0_417,i_0_346,i_0_323,i_0_288,i_0_289,i_0_372,i_0_373,i_0_314,i_0_315,i_0_349,i_0_382,i_0_398,i_0_399,i_0_371,i_0_418,i_0_393,i_0_383,i_0_404,i_0_416,i_0_394,i_0_438,i_0_440]) ).
cnf(i_0_1568,plain,
first(not_subclass_element(X1,unordered_pair(y,y))) = first(not_subclass_element(X1,null_class)),
inference(scs_inference,[],[i_0_1409,i_0_1473,i_0_1451,i_0_1318,i_0_1166,i_0_1523,i_0_1484,i_0_1449,i_0_1415,i_0_1431,i_0_568,i_0_477,i_0_395,i_0_359,i_0_417,i_0_346,i_0_323,i_0_288,i_0_289,i_0_372,i_0_373,i_0_314,i_0_315,i_0_349,i_0_382,i_0_398,i_0_399,i_0_371,i_0_418,i_0_393,i_0_383,i_0_404,i_0_416,i_0_394,i_0_438,i_0_440,i_0_441,i_0_442,i_0_443,i_0_444,i_0_445,i_0_447,i_0_448,i_0_449,i_0_450]) ).
cnf(i_0_1576,plain,
unordered_pair(intersection(null_class,X1),intersection(null_class,X1)) != unordered_pair(omega,omega),
inference(scs_inference,[],[i_0_1409,i_0_1473,i_0_1451,i_0_1318,i_0_1452,i_0_1166,i_0_1523,i_0_1421,i_0_1484,i_0_1449,i_0_1415,i_0_1431,i_0_568,i_0_477,i_0_395,i_0_359,i_0_417,i_0_346,i_0_323,i_0_288,i_0_289,i_0_372,i_0_373,i_0_314,i_0_315,i_0_349,i_0_382,i_0_398,i_0_399,i_0_371,i_0_418,i_0_393,i_0_383,i_0_404,i_0_416,i_0_394,i_0_438,i_0_440,i_0_441,i_0_442,i_0_443,i_0_444,i_0_445,i_0_447,i_0_448,i_0_449,i_0_450,i_0_439,i_0_446,i_0_437,i_0_423,i_0_422,i_0_435]) ).
cnf(i_0_1586,plain,
null_class != unordered_pair(unordered_pair(X1,X2),X3),
inference(rename_variables,[],[i_0_1447]) ).
cnf(i_0_1594,plain,
member(not_subclass_element(omega,intersection(null_class,null_class)),omega),
inference(scs_inference,[],[i_0_1409,i_0_1473,i_0_1451,i_0_1318,i_0_1452,i_0_1447,i_0_1166,i_0_1523,i_0_1421,i_0_1484,i_0_1449,i_0_1415,i_0_1431,i_0_1158,i_0_1138,i_0_568,i_0_477,i_0_406,i_0_1580,i_0_1583,i_0_1587,i_0_395,i_0_359,i_0_417,i_0_346,i_0_323,i_0_288,i_0_289,i_0_372,i_0_373,i_0_314,i_0_315,i_0_349,i_0_382,i_0_398,i_0_399,i_0_371,i_0_418,i_0_393,i_0_383,i_0_404,i_0_416,i_0_394,i_0_438,i_0_440,i_0_441,i_0_442,i_0_443,i_0_444,i_0_445,i_0_447,i_0_448,i_0_449,i_0_450,i_0_439,i_0_446,i_0_437,i_0_423,i_0_422,i_0_435,i_0_331,i_0_324,i_0_377,i_0_378,i_0_325,i_0_376,i_0_365]) ).
cnf(i_0_1595,plain,
intersection(null_class,X1) != omega,
inference(rename_variables,[],[i_0_1451]) ).
cnf(i_0_1860,plain,
~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(y,y))),choice),
inference(rename_variables,[],[i_0_1481]) ).
cnf(i_0_1863,plain,
~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(y,y))),choice),
inference(rename_variables,[],[i_0_1481]) ).
cnf(i_0_1600,plain,
member(regular(omega),intersection(intersection(omega,omega),intersection(omega,omega))),
inference(scs_inference,[],[i_0_1409,i_0_1473,i_0_1451,i_0_1318,i_0_1452,i_0_1447,i_0_1166,i_0_1523,i_0_1493,i_0_1421,i_0_1484,i_0_1449,i_0_1415,i_0_1431,i_0_1158,i_0_1138,i_0_568,i_0_477,i_0_406,i_0_1580,i_0_1583,i_0_1587,i_0_395,i_0_359,i_0_417,i_0_346,i_0_323,i_0_288,i_0_289,i_0_372,i_0_373,i_0_314,i_0_315,i_0_349,i_0_382,i_0_398,i_0_399,i_0_371,i_0_418,i_0_393,i_0_383,i_0_404,i_0_416,i_0_394,i_0_438,i_0_440,i_0_441,i_0_442,i_0_443,i_0_444,i_0_445,i_0_447,i_0_448,i_0_449,i_0_450,i_0_439,i_0_446,i_0_437,i_0_423,i_0_422,i_0_435,i_0_331,i_0_324,i_0_377,i_0_378,i_0_325,i_0_376,i_0_365,i_0_363,i_0_364]) ).
cnf(i_0_1605,plain,
~ inductive(intersection(omega,regular(omega))),
inference(scs_inference,[],[i_0_1409,i_0_1473,i_0_1451,i_0_1318,i_0_1452,i_0_1447,i_0_1156,i_0_1166,i_0_1523,i_0_1493,i_0_1421,i_0_636,i_0_1484,i_0_1449,i_0_1415,i_0_1431,i_0_1158,i_0_1138,i_0_568,i_0_498,i_0_427,i_0_477,i_0_406,i_0_1580,i_0_1583,i_0_1587,i_0_395,i_0_359,i_0_417,i_0_346,i_0_323,i_0_288,i_0_289,i_0_372,i_0_373,i_0_314,i_0_315,i_0_349,i_0_382,i_0_398,i_0_399,i_0_371,i_0_418,i_0_393,i_0_383,i_0_404,i_0_416,i_0_394,i_0_438,i_0_440,i_0_441,i_0_442,i_0_443,i_0_444,i_0_445,i_0_447,i_0_448,i_0_449,i_0_450,i_0_439,i_0_446,i_0_437,i_0_423,i_0_422,i_0_435,i_0_331,i_0_324,i_0_377,i_0_378,i_0_325,i_0_376,i_0_365,i_0_363,i_0_364,i_0_396,i_0_460]) ).
cnf(i_0_1606,plain,
~ member(unordered_pair(unordered_pair(y,y),unordered_pair(y,unordered_pair(X1,X1))),choice),
inference(scs_inference,[],[i_0_1409,i_0_1473,i_0_1451,i_0_1318,i_0_1452,i_0_1447,i_0_1156,i_0_1170,i_0_1166,i_0_1523,i_0_1493,i_0_1421,i_0_636,i_0_1484,i_0_1449,i_0_1415,i_0_1431,i_0_1158,i_0_1138,i_0_1142,i_0_568,i_0_498,i_0_427,i_0_477,i_0_406,i_0_1580,i_0_1583,i_0_1587,i_0_395,i_0_359,i_0_417,i_0_346,i_0_323,i_0_288,i_0_289,i_0_372,i_0_373,i_0_314,i_0_315,i_0_349,i_0_382,i_0_398,i_0_399,i_0_371,i_0_418,i_0_393,i_0_383,i_0_404,i_0_416,i_0_394,i_0_438,i_0_440,i_0_441,i_0_442,i_0_443,i_0_444,i_0_445,i_0_447,i_0_448,i_0_449,i_0_450,i_0_439,i_0_446,i_0_437,i_0_423,i_0_422,i_0_435,i_0_331,i_0_324,i_0_377,i_0_378,i_0_325,i_0_376,i_0_365,i_0_363,i_0_364,i_0_396,i_0_460,i_0_389]) ).
cnf(c_0_1386,axiom,
~ member(X1,intersection(complement(X2),X2)),
i_0_368 ).
cnf(c_0_1387,plain,
unordered_pair(y,y) = intersection(complement(X1),X1),
i_0_1374 ).
cnf(c_0_1388,negated_conjecture,
first(unordered_pair(unordered_pair(x,x),unordered_pair(x,unordered_pair(y,y)))) != unordered_pair(unordered_pair(x,x),unordered_pair(x,unordered_pair(y,y))),
i_0_312 ).
cnf(c_0_1389,plain,
unordered_pair(X1,unordered_pair(y,y)) = unordered_pair(X1,null_class),
i_0_1324 ).
cnf(c_0_1390,plain,
~ member(y,X1),
i_0_1251 ).
cnf(c_0_1391,plain,
( unordered_pair(X1,X2) = unordered_pair(X2,X2)
| member(X1,universal_class) ),
i_0_401 ).
cnf(c_0_1392,plain,
~ member(X1,unordered_pair(y,y)),
inference(rw,[status(thm)],[c_0_1386,c_0_1387]) ).
cnf(c_0_1393,axiom,
( X1 = null_class
| member(regular(X1),X1) ),
i_0_416 ).
cnf(c_0_1394,negated_conjecture,
first(unordered_pair(unordered_pair(x,x),unordered_pair(x,null_class))) != unordered_pair(unordered_pair(x,x),unordered_pair(x,null_class)),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_1388,c_0_1389]),c_0_1389]) ).
cnf(c_0_1395,axiom,
unordered_pair(X1,X2) = unordered_pair(X2,X1),
i_0_412 ).
cnf(c_0_1396,plain,
( first(X1) = X1
| member(unordered_pair(unordered_pair(first(X1),first(X1)),unordered_pair(first(X1),unordered_pair(second(X1),second(X1)))),cross_product(universal_class,universal_class)) ),
i_0_318 ).
cnf(c_0_1397,plain,
unordered_pair(y,X1) = unordered_pair(X1,X1),
inference(spm,[status(thm)],[c_0_1390,c_0_1391]) ).
cnf(c_0_1398,plain,
( first(X1) = X1
| unordered_pair(unordered_pair(first(X1),first(X1)),unordered_pair(first(X1),unordered_pair(second(X1),second(X1)))) = X1 ),
i_0_342 ).
cnf(c_0_1399,plain,
( member(X1,universal_class)
| ~ member(unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(X1,X1))),cross_product(X3,X4)) ),
i_0_321 ).
cnf(c_0_1400,plain,
unordered_pair(y,y) = null_class,
inference(spm,[status(thm)],[c_0_1392,c_0_1393]) ).
cnf(c_0_1401,negated_conjecture,
first(unordered_pair(unordered_pair(null_class,x),unordered_pair(x,x))) != unordered_pair(unordered_pair(null_class,x),unordered_pair(x,x)),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_1394,c_0_1395]),c_0_1395]),c_0_1395]),c_0_1395]) ).
cnf(c_0_1402,plain,
( first(X1) = X1
| member(unordered_pair(unordered_pair(y,first(X1)),unordered_pair(first(X1),unordered_pair(y,second(X1)))),cross_product(universal_class,universal_class)) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_1396,c_0_1397]),c_0_1397]) ).
cnf(c_0_1403,plain,
( unordered_pair(unordered_pair(y,first(X1)),unordered_pair(first(X1),unordered_pair(y,second(X1)))) = X1
| first(X1) = X1 ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_1398,c_0_1397]),c_0_1397]) ).
cnf(c_0_1404,plain,
~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,null_class)),cross_product(X2,X3)),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1399,c_0_1400]),c_0_1390]) ).
cnf(c_0_1405,negated_conjecture,
first(unordered_pair(unordered_pair(null_class,x),unordered_pair(y,x))) != unordered_pair(unordered_pair(null_class,x),unordered_pair(y,x)),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_1401,c_0_1397]),c_0_1397]) ).
cnf(c_0_1406,plain,
( first(X1) = X1
| member(X1,cross_product(universal_class,universal_class)) ),
inference(spm,[status(thm)],[c_0_1402,c_0_1403]) ).
cnf(c_0_1407,plain,
~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(null_class,X1)),cross_product(X2,X3)),
inference(spm,[status(thm)],[c_0_1404,c_0_1395]) ).
cnf(c_0_1408,negated_conjecture,
member(unordered_pair(unordered_pair(null_class,x),unordered_pair(y,x)),cross_product(universal_class,universal_class)),
inference(spm,[status(thm)],[c_0_1405,c_0_1406]) ).
cnf(c_0_1409,plain,
~ member(unordered_pair(unordered_pair(null_class,X1),unordered_pair(y,X1)),cross_product(X2,X3)),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_1407,c_0_1397]),c_0_1395]) ).
cnf(c_0_1410,negated_conjecture,
$false,
inference(sr,[status(thm)],[c_0_1408,c_0_1409]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.06 % Problem : SET121-7 : TPTP v9.2.1. Bugfixed v7.3.0.
% 0.00/0.06 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.07/0.24 % Computer : n024.cluster.edu
% 0.07/0.24 % Model : x86_64 x86_64
% 0.07/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.24 % Memory : 8042.1875MB
% 0.07/0.24 % OS : Linux 3.10.0-693.el7.x86_64
% 0.07/0.24 % CPULimit : 300
% 0.07/0.24 % WCLimit : 300
% 0.07/0.24 % DateTime : Mon May 4 21:10:57 EDT 2026
% 0.07/0.24 % CPUTime :
% 0.07/0.25 % start to proof: theBenchmark
% 261.11/196.70 % Version : CSE_E---1.7
% 261.11/196.70 % Problem : theBenchmark.p
% 261.11/196.70 % SZS status Unsatisfiable for theBenchmark.p
% 261.11/196.70 % SZS output start CNFRefutation
% See solution above
% 273.81/209.42 % Total time : 195.558s
%------------------------------------------------------------------------------