%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : NUM044-1 : TPTP v9.2.1. Bugfixed v2.1.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 : n014.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 04:52:46 PM UTC 2026
% Result : Unsatisfiable 191.57s 138.33s
% Output : CNFRefutation 197.17s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named c_0_159)
% 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(single_valued_term_defn1,axiom,
first(not_subclass_element(compose(X1,inverse(X1)),identity_relation)) = single_valued1(X1),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-1.ax',single_valued_term_defn1) ).
cnf(inverse,axiom,
domain_of(flip(cross_product(X1,universal_class))) = inverse(X1),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',inverse) ).
cnf(single_valued_term_defn2,axiom,
second(not_subclass_element(compose(X1,inverse(X1)),identity_relation)) = single_valued2(X1),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-1.ax',single_valued_term_defn2) ).
cnf(domain,axiom,
first(not_subclass_element(restrict(X1,X2,singleton(X3)),null_class)) = domain(X1,X2,X3),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',domain) ).
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(successor,axiom,
union(X1,singleton(X1)) = successor(X1),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',successor) ).
cnf(segment,axiom,
segment(X1,X2,X3) = domain_of(restrict(X1,X2,singleton(X3))),
file('/export/starexec/sandbox/benchmark/Axioms/NUM004-0.ax',segment) ).
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(application_function_defn4,axiom,
( member(ordered_pair(X1,ordered_pair(X2,apply(X1,X2))),application_function)
| ~ member(ordered_pair(X1,ordered_pair(X2,X3)),cross_product(universal_class,cross_product(universal_class,universal_class)))
| ~ member(X2,domain_of(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-1.ax',application_function_defn4) ).
cnf(single_valued_term_defn3,axiom,
domain(X1,image(inverse(X1),singleton(single_valued1(X1))),single_valued2(X1)) = single_valued3(X1),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-1.ax',single_valued_term_defn3) ).
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(ordinal_addition,axiom,
apply(recursion(X1,successor_relation,union_of_range_map),X2) = ordinal_add(X1,X2),
file('/export/starexec/sandbox/benchmark/Axioms/NUM004-0.ax',ordinal_addition) ).
cnf(ordinal_multiplication,axiom,
recursion(null_class,apply(add_relation,X1),union_of_range_map) = ordinal_multiply(X1,X2),
file('/export/starexec/sandbox/benchmark/Axioms/NUM004-0.ax',ordinal_multiplication) ).
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(application_function_defn3,axiom,
( apply(X1,X2) = X3
| ~ member(ordered_pair(X1,ordered_pair(X2,X3)),application_function) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-1.ax',application_function_defn3) ).
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(connected2,axiom,
( connected(X2,X1)
| ~ subclass(cross_product(X1,X1),union(identity_relation,symmetrization_of(X2))) ),
file('/export/starexec/sandbox/benchmark/Axioms/NUM004-0.ax',connected2) ).
cnf(symmetrization,axiom,
union(X1,inverse(X1)) = symmetrization_of(X1),
file('/export/starexec/sandbox/benchmark/Axioms/NUM004-0.ax',symmetrization) ).
cnf(union,axiom,
complement(intersection(complement(X1),complement(X2))) = union(X1,X2),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',union) ).
cnf(definition_of_composition_function3,axiom,
( member(ordered_pair(X1,ordered_pair(X2,compose(X1,X2))),composition_function)
| ~ member(ordered_pair(X1,X2),cross_product(universal_class,universal_class)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-1.ax',definition_of_composition_function3) ).
cnf(connected1,axiom,
( subclass(cross_product(X2,X2),union(identity_relation,symmetrization_of(X1)))
| ~ connected(X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/NUM004-0.ax',connected1) ).
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(application_function_defn2,axiom,
( member(X2,domain_of(X1))
| ~ member(ordered_pair(X1,ordered_pair(X2,X3)),application_function) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-1.ax',application_function_defn2) ).
cnf(definition_of_composition_function2,axiom,
( compose(X1,X2) = X3
| ~ member(ordered_pair(X1,ordered_pair(X2,X3)),composition_function) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-1.ax',definition_of_composition_function2) ).
cnf(kind_1_ordinals,axiom,
union(singleton(null_class),image(successor_relation,ordinal_numbers)) = kind_1_ordinals,
file('/export/starexec/sandbox/benchmark/Axioms/NUM004-0.ax',kind_1_ordinals) ).
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(union_of_range_map3,axiom,
( member(ordered_pair(X1,X2),union_of_range_map)
| ~ member(ordered_pair(X1,X2),cross_product(universal_class,universal_class))
| sum_class(range_of(X1)) != X2 ),
file('/export/starexec/sandbox/benchmark/Axioms/NUM004-0.ax',union_of_range_map3) ).
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(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(union_of_range_map2,axiom,
( sum_class(range_of(X1)) = X2
| ~ member(ordered_pair(X1,X2),union_of_range_map) ),
file('/export/starexec/sandbox/benchmark/Axioms/NUM004-0.ax',union_of_range_map2) ).
cnf(inductive2,axiom,
( subclass(image(successor_relation,X1),X1)
| ~ inductive(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',inductive2) ).
cnf(well_ordering5,axiom,
( ~ well_ordering(X1,X2)
| ~ subclass(X3,X2)
| ~ member(X4,X3)
| ~ member(ordered_pair(X4,least(X1,X3)),X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/NUM004-0.ax',well_ordering5) ).
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(compose_class_definition3,axiom,
( member(ordered_pair(X1,X2),compose_class(X3))
| ~ member(ordered_pair(X1,X2),cross_product(universal_class,universal_class))
| compose(X3,X1) != X2 ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-1.ax',compose_class_definition3) ).
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(transitive2,axiom,
( transitive(X1,X2)
| ~ subclass(compose(restrict(X1,X2,X2),restrict(X1,X2,X2)),restrict(X1,X2,X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/NUM004-0.ax',transitive2) ).
cnf(well_ordering4,axiom,
( segment(X1,X3,least(X1,X3)) = null_class
| ~ well_ordering(X1,X2)
| ~ subclass(X3,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/NUM004-0.ax',well_ordering4) ).
cnf(well_ordering8,axiom,
( well_ordering(X2,X3)
| ~ member(X1,not_well_ordering(X2,X3))
| segment(X2,not_well_ordering(X2,X3),X1) != null_class
| ~ connected(X2,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/NUM004-0.ax',well_ordering8) ).
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(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(asymmetric2,axiom,
( asymmetric(X1,X2)
| restrict(intersection(X1,inverse(X1)),X2,X2) != null_class ),
file('/export/starexec/sandbox/benchmark/Axioms/NUM004-0.ax',asymmetric2) ).
cnf(transitive1,axiom,
( subclass(compose(restrict(X1,X2,X2),restrict(X1,X2,X2)),restrict(X1,X2,X2))
| ~ transitive(X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/NUM004-0.ax',transitive1) ).
cnf(maps4,axiom,
( maps(X1,domain_of(X1),X2)
| ~ function(X1)
| ~ subclass(range_of(X1),X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-1.ax',maps4) ).
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(rest_of3,axiom,
( restrict(X3,X1,universal_class) = X2
| ~ member(ordered_pair(X1,X2),rest_of(X3)) ),
file('/export/starexec/sandbox/benchmark/Axioms/NUM004-0.ax',rest_of3) ).
cnf(rest_of2,axiom,
( member(X1,domain_of(X3))
| ~ member(ordered_pair(X1,X2),rest_of(X3)) ),
file('/export/starexec/sandbox/benchmark/Axioms/NUM004-0.ax',rest_of2) ).
cnf(compose_class_definition2,axiom,
( compose(X3,X1) = X2
| ~ member(ordered_pair(X1,X2),compose_class(X3)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-1.ax',compose_class_definition2) ).
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(rest_relation2,axiom,
( rest_of(X1) = X2
| ~ member(ordered_pair(X1,X2),rest_relation) ),
file('/export/starexec/sandbox/benchmark/Axioms/NUM004-0.ax',rest_relation2) ).
cnf(definition_of_domain_relation2,axiom,
( domain_of(X1) = X2
| ~ member(ordered_pair(X1,X2),domain_relation) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-1.ax',definition_of_domain_relation2) ).
cnf(rest_relation3,axiom,
( member(ordered_pair(X1,rest_of(X1)),rest_relation)
| ~ member(X1,universal_class) ),
file('/export/starexec/sandbox/benchmark/Axioms/NUM004-0.ax',rest_relation3) ).
cnf(definition_of_domain_relation3,axiom,
( member(ordered_pair(X1,domain_of(X1)),domain_relation)
| ~ member(X1,universal_class) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-1.ax',definition_of_domain_relation3) ).
cnf(section3,axiom,
( section(X3,X1,X2)
| ~ subclass(X1,X2)
| ~ subclass(domain_of(restrict(X3,X2,X1)),X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/NUM004-0.ax',section3) ).
cnf(rest_of4,axiom,
( member(ordered_pair(X1,X3),rest_of(X2))
| ~ member(X1,domain_of(X2))
| restrict(X2,X1,universal_class) != X3 ),
file('/export/starexec/sandbox/benchmark/Axioms/NUM004-0.ax',rest_of4) ).
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(maps3,axiom,
( subclass(range_of(X1),X3)
| ~ maps(X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-1.ax',maps3) ).
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(asymmetric1,axiom,
( restrict(intersection(X1,inverse(X1)),X2,X2) = null_class
| ~ asymmetric(X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/NUM004-0.ax',asymmetric1) ).
cnf(ordinal_numbers3,axiom,
( member(X1,ordinal_numbers)
| ~ well_ordering(element_relation,X1)
| ~ subclass(sum_class(X1),X1)
| ~ member(X1,universal_class) ),
file('/export/starexec/sandbox/benchmark/Axioms/NUM004-0.ax',ordinal_numbers3) ).
cnf(ordinal_numbers4,axiom,
( member(X1,ordinal_numbers)
| X1 = ordinal_numbers
| ~ well_ordering(element_relation,X1)
| ~ subclass(sum_class(X1),X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/NUM004-0.ax',ordinal_numbers4) ).
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(section2,axiom,
( subclass(domain_of(restrict(X1,X3,X2)),X2)
| ~ section(X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/NUM004-0.ax',section2) ).
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(ordinal_numbers2,axiom,
( subclass(sum_class(X1),X1)
| ~ member(X1,ordinal_numbers) ),
file('/export/starexec/sandbox/benchmark/Axioms/NUM004-0.ax',ordinal_numbers2) ).
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(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(irreflexive2,axiom,
( irreflexive(X1,X2)
| ~ subclass(restrict(X1,X2,X2),complement(identity_relation)) ),
file('/export/starexec/sandbox/benchmark/Axioms/NUM004-0.ax',irreflexive2) ).
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(irreflexive1,axiom,
( subclass(restrict(X1,X2,X2),complement(identity_relation))
| ~ irreflexive(X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/NUM004-0.ax',irreflexive1) ).
cnf(identity_relation,axiom,
intersection(inverse(subset_relation),subset_relation) = identity_relation,
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',identity_relation) ).
cnf(prove_irreflexive_class_property6_2,negated_conjecture,
restrict(intersection(x,identity_relation),y,y) != null_class,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_irreflexive_class_property6_2) ).
cnf(restriction2,axiom,
intersection(cross_product(X1,X2),X3) = restrict(X3,X1,X2),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',restriction2) ).
cnf(homomorphism3,axiom,
( compatible(X1,X2,X3)
| ~ homomorphism(X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',homomorphism3) ).
cnf(well_ordering3,axiom,
( member(least(X1,X3),X3)
| ~ well_ordering(X1,X2)
| ~ subclass(X3,X2)
| ~ member(X4,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/NUM004-0.ax',well_ordering3) ).
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(section1,axiom,
( subclass(X2,X3)
| ~ section(X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/NUM004-0.ax',section1) ).
cnf(recursion_equation_functions5,axiom,
( member(X2,recursion_equation_functions(X1))
| ~ function(X1)
| ~ function(X2)
| ~ member(domain_of(X2),ordinal_numbers)
| compose(X1,rest_of(X2)) != X2 ),
file('/export/starexec/sandbox/benchmark/Axioms/NUM004-0.ax',recursion_equation_functions5) ).
cnf(maps2,axiom,
( domain_of(X1) = X2
| ~ maps(X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-1.ax',maps2) ).
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(maps1,axiom,
( function(X1)
| ~ maps(X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-1.ax',maps1) ).
cnf(compatible1,axiom,
( function(X1)
| ~ compatible(X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',compatible1) ).
cnf(well_ordering2,axiom,
( X3 = null_class
| member(least(X1,X3),X3)
| ~ well_ordering(X1,X2)
| ~ subclass(X3,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/NUM004-0.ax',well_ordering2) ).
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(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(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(well_ordering7,axiom,
( subclass(not_well_ordering(X1,X2),X2)
| well_ordering(X1,X2)
| ~ connected(X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/NUM004-0.ax',well_ordering7) ).
cnf(compose_can_define_singleton,axiom,
intersection(complement(compose(element_relation,complement(identity_relation))),element_relation) = singleton_relation,
file('/export/starexec/sandbox/benchmark/Axioms/SET004-1.ax',compose_can_define_singleton) ).
cnf(application_function_defn1,axiom,
subclass(application_function,cross_product(universal_class,cross_product(universal_class,universal_class))),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-1.ax',application_function_defn1) ).
cnf(definition_of_composition_function1,axiom,
subclass(composition_function,cross_product(universal_class,cross_product(universal_class,universal_class))),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-1.ax',definition_of_composition_function1) ).
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(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(well_ordering6,axiom,
( well_ordering(X1,X2)
| ~ connected(X1,X2)
| not_well_ordering(X1,X2) != null_class ),
file('/export/starexec/sandbox/benchmark/Axioms/NUM004-0.ax',well_ordering6) ).
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(recursion_equation_functions4,axiom,
( compose(X2,rest_of(X1)) = X1
| ~ member(X1,recursion_equation_functions(X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/NUM004-0.ax',recursion_equation_functions4) ).
cnf(recursion_equation_functions3,axiom,
( member(domain_of(X1),ordinal_numbers)
| ~ member(X1,recursion_equation_functions(X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/NUM004-0.ax',recursion_equation_functions3) ).
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(function1,axiom,
( subclass(X1,cross_product(universal_class,universal_class))
| ~ function(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',function1) ).
cnf(rest_of1,axiom,
subclass(rest_of(X1),cross_product(universal_class,universal_class)),
file('/export/starexec/sandbox/benchmark/Axioms/NUM004-0.ax',rest_of1) ).
cnf(compose_class_definition1,axiom,
subclass(compose_class(X1),cross_product(universal_class,universal_class)),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-1.ax',compose_class_definition1) ).
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(well_ordering1,axiom,
( connected(X1,X2)
| ~ well_ordering(X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/NUM004-0.ax',well_ordering1) ).
cnf(recursion_equation_functions2,axiom,
( function(X1)
| ~ member(X1,recursion_equation_functions(X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/NUM004-0.ax',recursion_equation_functions2) ).
cnf(recursion_equation_functions1,axiom,
( function(X2)
| ~ member(X1,recursion_equation_functions(X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/NUM004-0.ax',recursion_equation_functions1) ).
cnf(ordinal_numbers1,axiom,
( well_ordering(element_relation,X1)
| ~ member(X1,ordinal_numbers) ),
file('/export/starexec/sandbox/benchmark/Axioms/NUM004-0.ax',ordinal_numbers1) ).
cnf(union_of_range_map1,axiom,
subclass(union_of_range_map,cross_product(universal_class,universal_class)),
file('/export/starexec/sandbox/benchmark/Axioms/NUM004-0.ax',union_of_range_map1) ).
cnf(rest_relation1,axiom,
subclass(rest_relation,cross_product(universal_class,universal_class)),
file('/export/starexec/sandbox/benchmark/Axioms/NUM004-0.ax',rest_relation1) ).
cnf(definition_of_domain_relation1,axiom,
subclass(domain_relation,cross_product(universal_class,universal_class)),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-1.ax',definition_of_domain_relation1) ).
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(integer_function1,axiom,
( integer_of(X1) = X1
| ~ member(X1,omega) ),
file('/export/starexec/sandbox/benchmark/Axioms/NUM004-0.ax',integer_function1) ).
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(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(integer_function2,axiom,
( member(X1,omega)
| integer_of(X1) = null_class ),
file('/export/starexec/sandbox/benchmark/Axioms/NUM004-0.ax',integer_function2) ).
cnf(limit_ordinals,axiom,
intersection(complement(kind_1_ordinals),ordinal_numbers) = limit_ordinals,
file('/export/starexec/sandbox/benchmark/Axioms/NUM004-0.ax',limit_ordinals) ).
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(prove_irreflexive_class_property6_1,negated_conjecture,
irreflexive(x,y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_irreflexive_class_property6_1) ).
cnf(omega_in_universal,axiom,
member(omega,universal_class),
file('/export/starexec/sandbox/benchmark/Axioms/SET004-0.ax',omega_in_universal) ).
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_158,axiom,
range_of(restrict(X1,X2,universal_class)) = image(X1,X2),
image ).
cnf(i_0_159,axiom,
domain_of(inverse(X1)) = range_of(X1),
range_of ).
cnf(i_0_160,axiom,
intersection(X1,cross_product(X2,X3)) = restrict(X1,X2,X3),
restriction1 ).
cnf(i_0_161,axiom,
sum_class(image(X1,singleton(X2))) = apply(X1,X2),
apply ).
cnf(i_0_162,axiom,
unordered_pair(X1,X1) = singleton(X1),
singleton_set ).
cnf(i_0_163,axiom,
domain_of(restrict(element_relation,universal_class,X1)) = sum_class(X1),
sum_class_definition ).
cnf(i_0_164,axiom,
unordered_pair(singleton(X1),unordered_pair(X1,singleton(X2))) = ordered_pair(X1,X2),
ordered_pair ).
cnf(i_0_165,axiom,
first(not_subclass_element(compose(X1,inverse(X1)),identity_relation)) = single_valued1(X1),
single_valued_term_defn1 ).
cnf(i_0_166,axiom,
domain_of(flip(cross_product(X1,universal_class))) = inverse(X1),
inverse ).
cnf(i_0_167,axiom,
second(not_subclass_element(compose(X1,inverse(X1)),identity_relation)) = single_valued2(X1),
single_valued_term_defn2 ).
cnf(i_0_168,axiom,
first(not_subclass_element(restrict(X1,X2,singleton(X3)),null_class)) = domain(X1,X2,X3),
domain ).
cnf(i_0_169,axiom,
complement(image(element_relation,complement(X1))) = power_class(X1),
power_class_definition ).
cnf(i_0_170,plain,
domain_of(inverse(intersection(X1,cross_product(X2,universal_class)))) = image(X1,X2),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_158,c_0_159]),c_0_160]) ).
cnf(i_0_171,axiom,
union(X1,singleton(X1)) = successor(X1),
successor ).
cnf(i_0_172,axiom,
segment(X1,X2,X3) = domain_of(restrict(X1,X2,singleton(X3))),
segment ).
cnf(i_0_173,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_174,plain,
sum_class(image(X1,unordered_pair(X2,X2))) = apply(X1,X2),
inference(rw,[status(thm)],[i_0_161,c_0_162]) ).
cnf(i_0_175,plain,
domain_of(intersection(element_relation,cross_product(universal_class,X1))) = sum_class(X1),
inference(rw,[status(thm)],[i_0_163,c_0_160]) ).
cnf(i_0_176,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_164,c_0_162]),c_0_162]) ).
cnf(i_0_177,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_178,axiom,
( member(ordered_pair(X1,ordered_pair(X2,apply(X1,X2))),application_function)
| ~ member(ordered_pair(X1,ordered_pair(X2,X3)),cross_product(universal_class,cross_product(universal_class,universal_class)))
| ~ member(X2,domain_of(X1)) ),
application_function_defn4 ).
cnf(i_0_179,axiom,
domain(X1,image(inverse(X1),singleton(single_valued1(X1))),single_valued2(X1)) = single_valued3(X1),
single_valued_term_defn3 ).
cnf(i_0_180,plain,
first(not_subclass_element(compose(X1,domain_of(flip(cross_product(X1,universal_class)))),identity_relation)) = single_valued1(X1),
inference(rw,[status(thm)],[i_0_165,c_0_166]) ).
cnf(i_0_181,plain,
second(not_subclass_element(compose(X1,domain_of(flip(cross_product(X1,universal_class)))),identity_relation)) = single_valued2(X1),
inference(rw,[status(thm)],[i_0_167,c_0_166]) ).
cnf(i_0_182,plain,
first(not_subclass_element(intersection(X1,cross_product(X2,unordered_pair(X3,X3))),null_class)) = domain(X1,X2,X3),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_168,c_0_162]),c_0_160]) ).
cnf(i_0_183,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_184,axiom,
( member(X2,image(X3,image(X4,singleton(X1))))
| ~ member(ordered_pair(X1,X2),compose(X3,X4)) ),
compose2 ).
cnf(i_0_185,axiom,
apply(recursion(X1,successor_relation,union_of_range_map),X2) = ordinal_add(X1,X2),
ordinal_addition ).
cnf(i_0_186,axiom,
recursion(null_class,apply(add_relation,X1),union_of_range_map) = ordinal_multiply(X1,X2),
ordinal_multiplication ).
cnf(i_0_187,axiom,
( X1 = null_class
| member(apply(choice,X1),X1)
| ~ member(X1,universal_class) ),
choice2 ).
cnf(i_0_188,axiom,
( apply(X1,X2) = X3
| ~ member(ordered_pair(X1,ordered_pair(X2,X3)),application_function) ),
application_function_defn3 ).
cnf(i_0_189,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_190,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_191,axiom,
( connected(X2,X1)
| ~ subclass(cross_product(X1,X1),union(identity_relation,symmetrization_of(X2))) ),
connected2 ).
cnf(i_0_192,axiom,
union(X1,inverse(X1)) = symmetrization_of(X1),
symmetrization ).
cnf(i_0_193,axiom,
complement(intersection(complement(X1),complement(X2))) = union(X1,X2),
union ).
cnf(i_0_194,axiom,
( member(ordered_pair(X1,ordered_pair(X2,compose(X1,X2))),composition_function)
| ~ member(ordered_pair(X1,X2),cross_product(universal_class,universal_class)) ),
definition_of_composition_function3 ).
cnf(i_0_195,axiom,
( subclass(cross_product(X2,X2),union(identity_relation,symmetrization_of(X1)))
| ~ connected(X1,X2) ),
connected1 ).
cnf(i_0_196,axiom,
( member(ordered_pair(ordered_pair(X2,X1),X3),X4)
| ~ member(ordered_pair(ordered_pair(X1,X2),X3),flip(X4)) ),
flip2 ).
cnf(i_0_197,axiom,
( member(ordered_pair(ordered_pair(X2,X3),X1),X4)
| ~ member(ordered_pair(ordered_pair(X1,X2),X3),rotate(X4)) ),
rotate2 ).
cnf(i_0_198,axiom,
( member(X2,domain_of(X1))
| ~ member(ordered_pair(X1,ordered_pair(X2,X3)),application_function) ),
application_function_defn2 ).
cnf(i_0_199,axiom,
( compose(X1,X2) = X3
| ~ member(ordered_pair(X1,ordered_pair(X2,X3)),composition_function) ),
definition_of_composition_function2 ).
cnf(i_0_200,axiom,
union(singleton(null_class),image(successor_relation,ordinal_numbers)) = kind_1_ordinals,
kind_1_ordinals ).
cnf(i_0_201,axiom,
( member(power_class(X1),universal_class)
| ~ member(X1,universal_class) ),
power_class2 ).
cnf(i_0_202,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_169,c_0_170]),c_0_166]) ).
cnf(i_0_203,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_204,axiom,
( member(ordered_pair(X1,X2),union_of_range_map)
| ~ member(ordered_pair(X1,X2),cross_product(universal_class,universal_class))
| sum_class(range_of(X1)) != X2 ),
union_of_range_map3 ).
cnf(i_0_205,axiom,
( inductive(X1)
| ~ member(null_class,X1)
| ~ subclass(image(successor_relation,X1),X1) ),
inductive3 ).
cnf(i_0_206,axiom,
intersection(domain_of(X1),diagonalise(compose(inverse(element_relation),X1))) = cantor(X1),
cantor_class ).
cnf(i_0_207,axiom,
complement(domain_of(intersection(X1,identity_relation))) = diagonalise(X1),
diagonalisation ).
cnf(i_0_208,axiom,
( member(image(X1,X2),universal_class)
| ~ function(X1)
| ~ member(X2,universal_class) ),
replacement ).
cnf(i_0_209,axiom,
( sum_class(range_of(X1)) = X2
| ~ member(ordered_pair(X1,X2),union_of_range_map) ),
union_of_range_map2 ).
cnf(i_0_210,axiom,
( subclass(image(successor_relation,X1),X1)
| ~ inductive(X1) ),
inductive2 ).
cnf(i_0_211,axiom,
( ~ well_ordering(X1,X2)
| ~ subclass(X3,X2)
| ~ member(X4,X3)
| ~ member(ordered_pair(X4,least(X1,X3)),X1) ),
well_ordering5 ).
cnf(i_0_212,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_213,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_214,plain,
union(X1,unordered_pair(X1,X1)) = successor(X1),
inference(rw,[status(thm)],[i_0_171,c_0_162]) ).
cnf(i_0_215,axiom,
( member(ordered_pair(X1,X2),compose_class(X3))
| ~ member(ordered_pair(X1,X2),cross_product(universal_class,universal_class))
| compose(X3,X1) != X2 ),
compose_class_definition3 ).
cnf(i_0_216,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_217,axiom,
( transitive(X1,X2)
| ~ subclass(compose(restrict(X1,X2,X2),restrict(X1,X2,X2)),restrict(X1,X2,X2)) ),
transitive2 ).
cnf(i_0_218,axiom,
( segment(X1,X3,least(X1,X3)) = null_class
| ~ well_ordering(X1,X2)
| ~ subclass(X3,X2) ),
well_ordering4 ).
cnf(i_0_219,plain,
segment(X1,X2,X3) = domain_of(intersection(X1,cross_product(X2,unordered_pair(X3,X3)))),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_172,c_0_162]),c_0_160]) ).
cnf(i_0_220,axiom,
( well_ordering(X2,X3)
| ~ member(X1,not_well_ordering(X2,X3))
| segment(X2,not_well_ordering(X2,X3),X1) != null_class
| ~ connected(X2,X3) ),
well_ordering8 ).
cnf(i_0_221,axiom,
( successor(X1) = X2
| ~ member(ordered_pair(X1,X2),successor_relation) ),
successor_relation2 ).
cnf(i_0_222,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_223,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_224,axiom,
( function(X1)
| ~ subclass(X1,cross_product(universal_class,universal_class))
| ~ subclass(compose(X1,inverse(X1)),identity_relation) ),
function3 ).
cnf(i_0_225,axiom,
( asymmetric(X1,X2)
| restrict(intersection(X1,inverse(X1)),X2,X2) != null_class ),
asymmetric2 ).
cnf(i_0_226,axiom,
( subclass(compose(restrict(X1,X2,X2),restrict(X1,X2,X2)),restrict(X1,X2,X2))
| ~ transitive(X1,X2) ),
transitive1 ).
cnf(i_0_227,axiom,
( maps(X1,domain_of(X1),X2)
| ~ function(X1)
| ~ subclass(range_of(X1),X2) ),
maps4 ).
cnf(i_0_228,axiom,
( member(X1,X3)
| ~ member(ordered_pair(X1,X2),cross_product(X3,X4)) ),
cartesian_product1 ).
cnf(i_0_229,axiom,
( member(X2,X4)
| ~ member(ordered_pair(X1,X2),cross_product(X3,X4)) ),
cartesian_product2 ).
cnf(i_0_230,axiom,
( restrict(X3,X1,universal_class) = X2
| ~ member(ordered_pair(X1,X2),rest_of(X3)) ),
rest_of3 ).
cnf(i_0_231,axiom,
( member(X1,domain_of(X3))
| ~ member(ordered_pair(X1,X2),rest_of(X3)) ),
rest_of2 ).
cnf(i_0_232,axiom,
( compose(X3,X1) = X2
| ~ member(ordered_pair(X1,X2),compose_class(X3)) ),
compose_class_definition2 ).
cnf(i_0_233,axiom,
( single_valued_class(X1)
| ~ subclass(compose(X1,inverse(X1)),identity_relation) ),
single_valued_class2 ).
cnf(i_0_234,axiom,
( member(X1,X2)
| ~ member(ordered_pair(X1,X2),element_relation) ),
element_relation2 ).
cnf(i_0_235,axiom,
( rest_of(X1) = X2
| ~ member(ordered_pair(X1,X2),rest_relation) ),
rest_relation2 ).
cnf(i_0_236,axiom,
( domain_of(X1) = X2
| ~ member(ordered_pair(X1,X2),domain_relation) ),
definition_of_domain_relation2 ).
cnf(i_0_237,axiom,
( member(ordered_pair(X1,rest_of(X1)),rest_relation)
| ~ member(X1,universal_class) ),
rest_relation3 ).
cnf(i_0_238,axiom,
( member(ordered_pair(X1,domain_of(X1)),domain_relation)
| ~ member(X1,universal_class) ),
definition_of_domain_relation3 ).
cnf(i_0_239,axiom,
( section(X3,X1,X2)
| ~ subclass(X1,X2)
| ~ subclass(domain_of(restrict(X3,X2,X1)),X1) ),
section3 ).
cnf(i_0_240,axiom,
( member(ordered_pair(X1,X3),rest_of(X2))
| ~ member(X1,domain_of(X2))
| restrict(X2,X1,universal_class) != X3 ),
rest_of4 ).
cnf(i_0_241,axiom,
( subclass(range_of(X1),domain_of(domain_of(X3)))
| ~ compatible(X1,X2,X3) ),
compatible3 ).
cnf(i_0_242,axiom,
( subclass(range_of(X1),X3)
| ~ maps(X1,X2,X3) ),
maps3 ).
cnf(i_0_243,axiom,
( member(ordered_pair(X1,X3),cross_product(X2,X4))
| ~ member(X1,X2)
| ~ member(X3,X4) ),
cartesian_product3 ).
cnf(i_0_244,axiom,
( restrict(intersection(X1,inverse(X1)),X2,X2) = null_class
| ~ asymmetric(X1,X2) ),
asymmetric1 ).
cnf(i_0_245,axiom,
( member(X1,ordinal_numbers)
| ~ well_ordering(element_relation,X1)
| ~ subclass(sum_class(X1),X1)
| ~ member(X1,universal_class) ),
ordinal_numbers3 ).
cnf(i_0_246,axiom,
( member(X1,ordinal_numbers)
| X1 = ordinal_numbers
| ~ well_ordering(element_relation,X1)
| ~ subclass(sum_class(X1),X1) ),
ordinal_numbers4 ).
cnf(i_0_247,axiom,
( ordered_pair(first(X1),second(X1)) = X1
| ~ member(X1,cross_product(X2,X3)) ),
cartesian_product4 ).
cnf(i_0_248,axiom,
( subclass(range_of(X1),domain_of(domain_of(X1)))
| ~ operation(X1) ),
operation3 ).
cnf(i_0_249,axiom,
( subclass(compose(X1,inverse(X1)),identity_relation)
| ~ function(X1) ),
function2 ).
cnf(i_0_250,axiom,
( subclass(compose(X1,inverse(X1)),identity_relation)
| ~ single_valued_class(X1) ),
single_valued_class1 ).
cnf(i_0_251,axiom,
( subclass(domain_of(restrict(X1,X3,X2)),X2)
| ~ section(X1,X2,X3) ),
section2 ).
cnf(i_0_252,axiom,
( one_to_one(X1)
| ~ function(inverse(X1))
| ~ function(X1) ),
one_to_one3 ).
cnf(i_0_253,axiom,
( subclass(sum_class(X1),X1)
| ~ member(X1,ordinal_numbers) ),
ordinal_numbers2 ).
cnf(i_0_254,axiom,
( member(sum_class(X1),universal_class)
| ~ member(X1,universal_class) ),
sum_class2 ).
cnf(i_0_255,axiom,
( restrict(X1,singleton(X2),universal_class) != null_class
| ~ member(X2,domain_of(X1)) ),
domain1 ).
cnf(i_0_256,axiom,
( irreflexive(X1,X2)
| ~ subclass(restrict(X1,X2,X2),complement(identity_relation)) ),
irreflexive2 ).
cnf(i_0_257,axiom,
( restrict(X2,singleton(X1),universal_class) = null_class
| member(X1,domain_of(X2))
| ~ member(X1,universal_class) ),
domain2 ).
cnf(i_0_258,axiom,
( function(inverse(X1))
| ~ one_to_one(X1) ),
one_to_one2 ).
cnf(i_0_259,axiom,
( subclass(restrict(X1,X2,X2),complement(identity_relation))
| ~ irreflexive(X1,X2) ),
irreflexive1 ).
cnf(i_0_260,axiom,
intersection(inverse(subset_relation),subset_relation) = identity_relation,
identity_relation ).
cnf(i_0_261,negated_conjecture,
restrict(intersection(x,identity_relation),y,y) != null_class,
prove_irreflexive_class_property6_2 ).
cnf(i_0_262,axiom,
intersection(cross_product(X1,X2),X3) = restrict(X3,X1,X2),
restriction2 ).
cnf(i_0_263,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_173,c_0_174]),c_0_174]),c_0_174]),c_0_174]),c_0_174]),c_0_170]),c_0_170]),c_0_170]),c_0_170]),c_0_170]),c_0_170]),c_0_170]),c_0_170]),c_0_166]),c_0_166]),c_0_166]),c_0_166]),c_0_166]),c_0_166]),c_0_166]),c_0_166]),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_176]),c_0_176]),c_0_176]),c_0_176]),c_0_176]),c_0_176]),
[final] ).
cnf(i_0_264,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_177,c_0_174]),c_0_174]),c_0_174]),c_0_174]),c_0_174]),c_0_170]),c_0_170]),c_0_170]),c_0_170]),c_0_170]),c_0_170]),c_0_170]),c_0_170]),c_0_166]),c_0_166]),c_0_166]),c_0_166]),c_0_166]),c_0_166]),c_0_166]),c_0_166]),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_176]),c_0_176]),c_0_176]),c_0_176]),c_0_176]),c_0_176]),c_0_176]),
[final] ).
cnf(i_0_265,plain,
( member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(domain_of(intersection(element_relation,cross_product(universal_class,domain_of(domain_of(flip(cross_product(intersection(X1,cross_product(unordered_pair(X2,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(X2,X2),universal_class)),universal_class)))))))))),unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(domain_of(intersection(element_relation,cross_product(universal_class,domain_of(domain_of(flip(cross_product(intersection(X1,cross_product(unordered_pair(X2,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(X2,X2),universal_class)),universal_class))))))))))))),application_function)
| ~ member(X2,domain_of(X1))
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,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)))))),cross_product(universal_class,cross_product(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)],[inference(rw,[status(thm)],[i_0_178,c_0_174]),c_0_170]),c_0_166]),c_0_175]),c_0_176]),c_0_176]),c_0_176]),c_0_176]),
[final] ).
cnf(i_0_266,plain,
first(not_subclass_element(intersection(X1,cross_product(domain_of(domain_of(flip(cross_product(intersection(domain_of(flip(cross_product(X1,universal_class))),cross_product(unordered_pair(first(not_subclass_element(compose(X1,domain_of(flip(cross_product(X1,universal_class)))),identity_relation)),first(not_subclass_element(compose(X1,domain_of(flip(cross_product(X1,universal_class)))),identity_relation))),universal_class)),universal_class)))),unordered_pair(second(not_subclass_element(compose(X1,domain_of(flip(cross_product(X1,universal_class)))),identity_relation)),second(not_subclass_element(compose(X1,domain_of(flip(cross_product(X1,universal_class)))),identity_relation))))),null_class)) = single_valued3(X1),
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_179,c_0_162]),c_0_170]),c_0_166]),c_0_166]),c_0_180]),c_0_180]),c_0_181]),c_0_182]),
[final] ).
cnf(i_0_267,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_183,c_0_162]),c_0_170]),c_0_170]),c_0_166]),c_0_166]),c_0_176]),c_0_176]),
[final] ).
cnf(i_0_268,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_184,c_0_162]),c_0_170]),c_0_170]),c_0_166]),c_0_166]),c_0_176]),
[final] ).
cnf(i_0_269,plain,
domain_of(intersection(element_relation,cross_product(universal_class,domain_of(domain_of(flip(cross_product(intersection(recursion(X1,successor_relation,union_of_range_map),cross_product(unordered_pair(X2,X2),universal_class)),universal_class))))))) = ordinal_add(X1,X2),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_185,c_0_174]),c_0_170]),c_0_166]),c_0_175]),
[final] ).
cnf(i_0_270,plain,
recursion(null_class,domain_of(intersection(element_relation,cross_product(universal_class,domain_of(domain_of(flip(cross_product(intersection(add_relation,cross_product(unordered_pair(X1,X1),universal_class)),universal_class))))))),union_of_range_map) = ordinal_multiply(X1,X2),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_186,c_0_174]),c_0_170]),c_0_166]),c_0_175]),
[final] ).
cnf(i_0_271,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_187,c_0_174]),c_0_170]),c_0_166]),c_0_175]),
[final] ).
cnf(i_0_272,plain,
( domain_of(intersection(element_relation,cross_product(universal_class,domain_of(domain_of(flip(cross_product(intersection(X1,cross_product(unordered_pair(X2,X2),universal_class)),universal_class))))))) = X3
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,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)))))),application_function) ),
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_188,c_0_174]),c_0_170]),c_0_166]),c_0_175]),c_0_176]),c_0_176]),
[final] ).
cnf(i_0_273,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_189,c_0_176]),c_0_176]),c_0_176]),c_0_176]),c_0_176]),c_0_176]),
[final] ).
cnf(i_0_274,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_190,c_0_176]),c_0_176]),c_0_176]),c_0_176]),c_0_176]),c_0_176]),
[final] ).
cnf(i_0_275,plain,
( connected(X2,X1)
| ~ subclass(cross_product(X1,X1),complement(intersection(complement(identity_relation),complement(complement(intersection(complement(X2),complement(domain_of(flip(cross_product(X2,universal_class)))))))))) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_191,c_0_192]),c_0_166]),c_0_193]),c_0_193]),
[final] ).
cnf(i_0_276,plain,
( member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(compose(X1,X2),compose(X1,X2)))),unordered_pair(unordered_pair(X2,X2),unordered_pair(X2,unordered_pair(compose(X1,X2),compose(X1,X2))))))),composition_function)
| ~ 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)],[i_0_194,c_0_176]),c_0_176]),c_0_176]),
[final] ).
cnf(i_0_277,plain,
( subclass(cross_product(X2,X2),complement(intersection(complement(identity_relation),complement(complement(intersection(complement(X1),complement(domain_of(flip(cross_product(X1,universal_class))))))))))
| ~ connected(X1,X2) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_195,c_0_192]),c_0_166]),c_0_193]),c_0_193]),
[final] ).
cnf(i_0_278,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_196,c_0_176]),c_0_176]),c_0_176]),c_0_176]),
[final] ).
cnf(i_0_279,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_197,c_0_176]),c_0_176]),c_0_176]),c_0_176]),
[final] ).
cnf(i_0_280,plain,
( member(X2,domain_of(X1))
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,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)))))),application_function) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_198,c_0_176]),c_0_176]),
[final] ).
cnf(i_0_281,plain,
( compose(X1,X2) = X3
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,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)))))),composition_function) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_199,c_0_176]),c_0_176]),
[final] ).
cnf(i_0_282,plain,
complement(intersection(complement(unordered_pair(null_class,null_class)),complement(domain_of(domain_of(flip(cross_product(intersection(successor_relation,cross_product(ordinal_numbers,universal_class)),universal_class))))))) = kind_1_ordinals,
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_200,c_0_162]),c_0_170]),c_0_166]),c_0_193]),
[final] ).
cnf(i_0_283,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_201,c_0_202]),
[final] ).
cnf(i_0_284,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_203,c_0_176]),
[final] ).
cnf(i_0_285,plain,
( member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),union_of_range_map)
| domain_of(intersection(element_relation,cross_product(universal_class,domain_of(domain_of(flip(cross_product(X1,universal_class))))))) != 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)],[inference(rw,[status(thm)],[i_0_204,c_0_159]),c_0_166]),c_0_175]),c_0_176]),c_0_176]),
[final] ).
cnf(i_0_286,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_205,c_0_170]),c_0_166]),
[final] ).
cnf(i_0_287,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_206,c_0_207]),c_0_166]),
[final] ).
cnf(i_0_288,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_208,c_0_170]),c_0_166]),
[final] ).
cnf(i_0_289,plain,
( domain_of(intersection(element_relation,cross_product(universal_class,domain_of(domain_of(flip(cross_product(X1,universal_class))))))) = X2
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),union_of_range_map) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_209,c_0_159]),c_0_166]),c_0_175]),c_0_176]),
[final] ).
cnf(i_0_290,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_210,c_0_170]),c_0_166]),
[final] ).
cnf(i_0_291,plain,
( ~ subclass(X3,X2)
| ~ member(X4,X3)
| ~ well_ordering(X1,X2)
| ~ member(unordered_pair(unordered_pair(X4,X4),unordered_pair(X4,unordered_pair(least(X1,X3),least(X1,X3)))),X1) ),
inference(rw,[status(thm)],[i_0_211,c_0_176]),
[final] ).
cnf(i_0_292,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_212,c_0_166]),
[final] ).
cnf(i_0_293,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_213,c_0_214]),c_0_193]),c_0_176]),c_0_176]),
[final] ).
cnf(i_0_294,plain,
( member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),compose_class(X3))
| compose(X3,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_215,c_0_176]),c_0_176]),
[final] ).
cnf(i_0_295,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_216,c_0_176]),c_0_176]),
[final] ).
cnf(i_0_296,plain,
( transitive(X1,X2)
| ~ subclass(compose(intersection(X1,cross_product(X2,X2)),intersection(X1,cross_product(X2,X2))),intersection(X1,cross_product(X2,X2))) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_217,c_0_160]),c_0_160]),c_0_160]),
[final] ).
cnf(i_0_297,plain,
( domain_of(intersection(X1,cross_product(X3,unordered_pair(least(X1,X3),least(X1,X3))))) = null_class
| ~ subclass(X3,X2)
| ~ well_ordering(X1,X2) ),
inference(rw,[status(thm)],[i_0_218,c_0_219]),
[final] ).
cnf(i_0_298,plain,
( well_ordering(X2,X3)
| domain_of(intersection(X2,cross_product(not_well_ordering(X2,X3),unordered_pair(X1,X1)))) != null_class
| ~ connected(X2,X3)
| ~ member(X1,not_well_ordering(X2,X3)) ),
inference(rw,[status(thm)],[i_0_220,c_0_219]),
[final] ).
cnf(i_0_299,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_221,c_0_214]),c_0_193]),c_0_176]),
[final] ).
cnf(i_0_300,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_222,c_0_159]),c_0_166]),
[final] ).
cnf(i_0_301,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_223,c_0_159]),c_0_166]),
[final] ).
cnf(i_0_302,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_224,c_0_166]),
[final] ).
cnf(i_0_303,plain,
( asymmetric(X1,X2)
| intersection(intersection(X1,domain_of(flip(cross_product(X1,universal_class)))),cross_product(X2,X2)) != null_class ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_225,c_0_160]),c_0_166]),
[final] ).
cnf(i_0_304,plain,
( subclass(compose(intersection(X1,cross_product(X2,X2)),intersection(X1,cross_product(X2,X2))),intersection(X1,cross_product(X2,X2)))
| ~ transitive(X1,X2) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_226,c_0_160]),c_0_160]),c_0_160]),
[final] ).
cnf(i_0_305,plain,
( maps(X1,domain_of(X1),X2)
| ~ function(X1)
| ~ subclass(domain_of(domain_of(flip(cross_product(X1,universal_class)))),X2) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_227,c_0_159]),c_0_166]),
[final] ).
cnf(i_0_306,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_228,c_0_176]),
[final] ).
cnf(i_0_307,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_229,c_0_176]),
[final] ).
cnf(i_0_308,plain,
( intersection(X3,cross_product(X1,universal_class)) = X2
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),rest_of(X3)) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_230,c_0_160]),c_0_176]),
[final] ).
cnf(i_0_309,plain,
( member(X1,domain_of(X3))
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),rest_of(X3)) ),
inference(rw,[status(thm)],[i_0_231,c_0_176]),
[final] ).
cnf(i_0_310,plain,
( compose(X3,X1) = X2
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),compose_class(X3)) ),
inference(rw,[status(thm)],[i_0_232,c_0_176]),
[final] ).
cnf(i_0_311,plain,
( single_valued_class(X1)
| ~ subclass(compose(X1,domain_of(flip(cross_product(X1,universal_class)))),identity_relation) ),
inference(rw,[status(thm)],[i_0_233,c_0_166]),
[final] ).
cnf(i_0_312,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_234,c_0_176]),
[final] ).
cnf(i_0_313,plain,
( rest_of(X1) = X2
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),rest_relation) ),
inference(rw,[status(thm)],[i_0_235,c_0_176]),
[final] ).
cnf(i_0_314,plain,
( domain_of(X1) = X2
| ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X2,X2))),domain_relation) ),
inference(rw,[status(thm)],[i_0_236,c_0_176]),
[final] ).
cnf(i_0_315,plain,
( member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(rest_of(X1),rest_of(X1)))),rest_relation)
| ~ member(X1,universal_class) ),
inference(rw,[status(thm)],[i_0_237,c_0_176]),
[final] ).
cnf(i_0_316,plain,
( member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(domain_of(X1),domain_of(X1)))),domain_relation)
| ~ member(X1,universal_class) ),
inference(rw,[status(thm)],[i_0_238,c_0_176]),
[final] ).
cnf(i_0_317,plain,
( section(X3,X1,X2)
| ~ subclass(X1,X2)
| ~ subclass(domain_of(intersection(X3,cross_product(X2,X1))),X1) ),
inference(rw,[status(thm)],[i_0_239,c_0_160]),
[final] ).
cnf(i_0_318,plain,
( member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(X3,X3))),rest_of(X2))
| intersection(X2,cross_product(X1,universal_class)) != X3
| ~ member(X1,domain_of(X2)) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_240,c_0_160]),c_0_176]),
[final] ).
cnf(i_0_319,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_241,c_0_159]),c_0_166]),
[final] ).
cnf(i_0_320,plain,
( subclass(domain_of(domain_of(flip(cross_product(X1,universal_class)))),X3)
| ~ maps(X1,X2,X3) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_242,c_0_159]),c_0_166]),
[final] ).
cnf(i_0_321,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_243,c_0_176]),
[final] ).
cnf(i_0_322,plain,
( intersection(intersection(X1,domain_of(flip(cross_product(X1,universal_class)))),cross_product(X2,X2)) = null_class
| ~ asymmetric(X1,X2) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_244,c_0_160]),c_0_166]),
[final] ).
cnf(i_0_323,plain,
( member(X1,ordinal_numbers)
| ~ member(X1,universal_class)
| ~ well_ordering(element_relation,X1)
| ~ subclass(domain_of(intersection(element_relation,cross_product(universal_class,X1))),X1) ),
inference(rw,[status(thm)],[i_0_245,c_0_175]),
[final] ).
cnf(i_0_324,plain,
( X1 = ordinal_numbers
| member(X1,ordinal_numbers)
| ~ well_ordering(element_relation,X1)
| ~ subclass(domain_of(intersection(element_relation,cross_product(universal_class,X1))),X1) ),
inference(rw,[status(thm)],[i_0_246,c_0_175]),
[final] ).
cnf(i_0_325,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_247,c_0_176]),
[final] ).
cnf(i_0_326,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_248,c_0_159]),c_0_166]),
[final] ).
cnf(i_0_327,plain,
( subclass(compose(X1,domain_of(flip(cross_product(X1,universal_class)))),identity_relation)
| ~ function(X1) ),
inference(rw,[status(thm)],[i_0_249,c_0_166]),
[final] ).
cnf(i_0_328,plain,
( subclass(compose(X1,domain_of(flip(cross_product(X1,universal_class)))),identity_relation)
| ~ single_valued_class(X1) ),
inference(rw,[status(thm)],[i_0_250,c_0_166]),
[final] ).
cnf(i_0_329,plain,
( subclass(domain_of(intersection(X1,cross_product(X3,X2))),X2)
| ~ section(X1,X2,X3) ),
inference(rw,[status(thm)],[i_0_251,c_0_160]),
[final] ).
cnf(i_0_330,plain,
( one_to_one(X1)
| ~ function(X1)
| ~ function(domain_of(flip(cross_product(X1,universal_class)))) ),
inference(rw,[status(thm)],[i_0_252,c_0_166]),
[final] ).
cnf(i_0_331,plain,
( subclass(domain_of(intersection(element_relation,cross_product(universal_class,X1))),X1)
| ~ member(X1,ordinal_numbers) ),
inference(rw,[status(thm)],[i_0_253,c_0_175]),
[final] ).
cnf(i_0_332,plain,
( member(domain_of(intersection(element_relation,cross_product(universal_class,X1))),universal_class)
| ~ member(X1,universal_class) ),
inference(rw,[status(thm)],[i_0_254,c_0_175]),
[final] ).
cnf(i_0_333,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_255,c_0_162]),c_0_160]),
[final] ).
cnf(i_0_334,plain,
( irreflexive(X1,X2)
| ~ subclass(intersection(X1,cross_product(X2,X2)),complement(identity_relation)) ),
inference(rw,[status(thm)],[i_0_256,c_0_160]),
[final] ).
cnf(i_0_335,axiom,
( compatible(X1,X2,X3)
| ~ homomorphism(X1,X2,X3) ),
homomorphism3,
[final] ).
cnf(i_0_336,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_257,c_0_162]),c_0_160]),
[final] ).
cnf(i_0_337,plain,
( function(domain_of(flip(cross_product(X1,universal_class))))
| ~ one_to_one(X1) ),
inference(rw,[status(thm)],[i_0_258,c_0_166]),
[final] ).
cnf(i_0_338,plain,
( subclass(intersection(X1,cross_product(X2,X2)),complement(identity_relation))
| ~ irreflexive(X1,X2) ),
inference(rw,[status(thm)],[i_0_259,c_0_160]),
[final] ).
cnf(i_0_339,plain,
intersection(domain_of(flip(cross_product(subset_relation,universal_class))),subset_relation) = identity_relation,
inference(rw,[status(thm)],[i_0_260,c_0_166]),
[final] ).
cnf(i_0_340,axiom,
( member(least(X1,X3),X3)
| ~ well_ordering(X1,X2)
| ~ subclass(X3,X2)
| ~ member(X4,X3) ),
well_ordering3,
[final] ).
cnf(i_0_341,axiom,
( domain_of(domain_of(X2)) = domain_of(X1)
| ~ compatible(X1,X2,X3) ),
compatible2,
[final] ).
cnf(i_0_342,axiom,
( subclass(X2,X3)
| ~ section(X1,X2,X3) ),
section1,
[final] ).
cnf(i_0_343,axiom,
( member(X2,recursion_equation_functions(X1))
| ~ function(X1)
| ~ function(X2)
| ~ member(domain_of(X2),ordinal_numbers)
| compose(X1,rest_of(X2)) != X2 ),
recursion_equation_functions5,
[final] ).
cnf(i_0_344,axiom,
( domain_of(X1) = X2
| ~ maps(X1,X2,X3) ),
maps2,
[final] ).
cnf(i_0_345,axiom,
( operation(X2)
| ~ homomorphism(X1,X2,X3) ),
homomorphism1,
[final] ).
cnf(i_0_346,axiom,
( operation(X3)
| ~ homomorphism(X1,X2,X3) ),
homomorphism2,
[final] ).
cnf(i_0_347,axiom,
( function(X1)
| ~ maps(X1,X2,X3) ),
maps1,
[final] ).
cnf(i_0_348,axiom,
( function(X1)
| ~ compatible(X1,X2,X3) ),
compatible1,
[final] ).
cnf(i_0_349,axiom,
( X3 = null_class
| member(least(X1,X3),X3)
| ~ well_ordering(X1,X2)
| ~ subclass(X3,X2) ),
well_ordering2,
[final] ).
cnf(i_0_350,axiom,
( member(X1,intersection(X2,X3))
| ~ member(X1,X2)
| ~ member(X1,X3) ),
intersection3,
[final] ).
cnf(i_0_351,negated_conjecture,
intersection(intersection(x,identity_relation),cross_product(y,y)) != null_class,
inference(rw,[status(thm)],[i_0_261,c_0_160]),
[final] ).
cnf(i_0_352,axiom,
subclass(flip(X1),cross_product(cross_product(universal_class,universal_class),universal_class)),
flip1,
[final] ).
cnf(i_0_353,axiom,
subclass(rotate(X1),cross_product(cross_product(universal_class,universal_class),universal_class)),
rotate1,
[final] ).
cnf(i_0_354,plain,
intersection(cross_product(X1,X2),X3) = intersection(X3,cross_product(X1,X2)),
inference(rw,[status(thm)],[i_0_262,c_0_160]),
[final] ).
cnf(i_0_355,axiom,
( subclass(X1,X2)
| ~ member(not_subclass_element(X1,X2),X2) ),
not_subclass_members2,
[final] ).
cnf(i_0_356,axiom,
( member(X1,X2)
| ~ member(X1,intersection(X2,X3)) ),
intersection1,
[final] ).
cnf(i_0_357,axiom,
( member(X1,X3)
| ~ member(X1,intersection(X2,X3)) ),
intersection2,
[final] ).
cnf(i_0_358,axiom,
( subclass(not_well_ordering(X1,X2),X2)
| well_ordering(X1,X2)
| ~ connected(X1,X2) ),
well_ordering7,
[final] ).
cnf(i_0_359,axiom,
intersection(complement(compose(element_relation,complement(identity_relation))),element_relation) = singleton_relation,
compose_can_define_singleton,
[final] ).
cnf(i_0_360,axiom,
subclass(application_function,cross_product(universal_class,cross_product(universal_class,universal_class))),
application_function_defn1,
[final] ).
cnf(i_0_361,axiom,
subclass(composition_function,cross_product(universal_class,cross_product(universal_class,universal_class))),
definition_of_composition_function1,
[final] ).
cnf(i_0_362,axiom,
( X1 = X2
| X1 = X3
| ~ member(X1,unordered_pair(X2,X3)) ),
unordered_pair_member,
[final] ).
cnf(i_0_363,axiom,
( cross_product(domain_of(domain_of(X1)),domain_of(domain_of(X1))) = domain_of(X1)
| ~ operation(X1) ),
operation2,
[final] ).
cnf(i_0_364,axiom,
( member(X1,unordered_pair(X1,X2))
| ~ member(X1,universal_class) ),
unordered_pair2,
[final] ).
cnf(i_0_365,axiom,
( member(X1,unordered_pair(X2,X1))
| ~ member(X1,universal_class) ),
unordered_pair3,
[final] ).
cnf(i_0_366,axiom,
subclass(compose(X1,X2),cross_product(universal_class,universal_class)),
compose1,
[final] ).
cnf(i_0_367,axiom,
( member(X3,X2)
| ~ subclass(X1,X2)
| ~ member(X3,X1) ),
subclass_members,
[final] ).
cnf(i_0_368,axiom,
( well_ordering(X1,X2)
| ~ connected(X1,X2)
| not_well_ordering(X1,X2) != null_class ),
well_ordering6,
[final] ).
cnf(i_0_369,axiom,
( member(X1,complement(X2))
| member(X1,X2)
| ~ member(X1,universal_class) ),
complement2,
[final] ).
cnf(i_0_370,axiom,
( ~ member(X1,complement(X2))
| ~ member(X1,X2) ),
complement1,
[final] ).
cnf(i_0_371,axiom,
( member(not_subclass_element(X1,X2),X1)
| subclass(X1,X2) ),
not_subclass_members1,
[final] ).
cnf(i_0_372,axiom,
( compose(X2,rest_of(X1)) = X1
| ~ member(X1,recursion_equation_functions(X2)) ),
recursion_equation_functions4,
[final] ).
cnf(i_0_373,axiom,
( member(domain_of(X1),ordinal_numbers)
| ~ member(X1,recursion_equation_functions(X2)) ),
recursion_equation_functions3,
[final] ).
cnf(i_0_374,axiom,
( X1 = X2
| ~ subclass(X1,X2)
| ~ subclass(X2,X1) ),
subclass_implies_equal,
[final] ).
cnf(i_0_375,axiom,
( subclass(X1,cross_product(universal_class,universal_class))
| ~ function(X1) ),
function1,
[final] ).
cnf(i_0_376,axiom,
subclass(rest_of(X1),cross_product(universal_class,universal_class)),
rest_of1,
[final] ).
cnf(i_0_377,axiom,
subclass(compose_class(X1),cross_product(universal_class,universal_class)),
compose_class_definition1,
[final] ).
cnf(i_0_378,axiom,
member(unordered_pair(X1,X2),universal_class),
unordered_pairs_in_universal,
[final] ).
cnf(i_0_379,axiom,
( connected(X1,X2)
| ~ well_ordering(X1,X2) ),
well_ordering1,
[final] ).
cnf(i_0_380,axiom,
( function(X1)
| ~ member(X1,recursion_equation_functions(X2)) ),
recursion_equation_functions2,
[final] ).
cnf(i_0_381,axiom,
( function(X2)
| ~ member(X1,recursion_equation_functions(X2)) ),
recursion_equation_functions1,
[final] ).
cnf(i_0_382,axiom,
( well_ordering(element_relation,X1)
| ~ member(X1,ordinal_numbers) ),
ordinal_numbers1,
[final] ).
cnf(i_0_383,axiom,
subclass(union_of_range_map,cross_product(universal_class,universal_class)),
union_of_range_map1,
[final] ).
cnf(i_0_384,axiom,
subclass(rest_relation,cross_product(universal_class,universal_class)),
rest_relation1,
[final] ).
cnf(i_0_385,axiom,
subclass(domain_relation,cross_product(universal_class,universal_class)),
definition_of_domain_relation1,
[final] ).
cnf(i_0_386,axiom,
subclass(successor_relation,cross_product(universal_class,universal_class)),
successor_relation1,
[final] ).
cnf(i_0_387,axiom,
subclass(element_relation,cross_product(universal_class,universal_class)),
element_relation1,
[final] ).
cnf(i_0_388,axiom,
( integer_of(X1) = X1
| ~ member(X1,omega) ),
integer_function1,
[final] ).
cnf(i_0_389,axiom,
( X1 = null_class
| member(regular(X1),X1) ),
regularity1,
[final] ).
cnf(i_0_390,axiom,
( X1 = null_class
| intersection(X1,regular(X1)) = null_class ),
regularity2,
[final] ).
cnf(i_0_391,axiom,
( member(null_class,X1)
| ~ inductive(X1) ),
inductive1,
[final] ).
cnf(i_0_392,axiom,
( subclass(omega,X1)
| ~ inductive(X1) ),
omega_is_inductive2,
[final] ).
cnf(i_0_393,axiom,
( subclass(X1,X2)
| X1 != X2 ),
equal_implies_subclass1,
[final] ).
cnf(i_0_394,axiom,
( subclass(X2,X1)
| X1 != X2 ),
equal_implies_subclass2,
[final] ).
cnf(i_0_395,axiom,
( member(X1,omega)
| integer_of(X1) = null_class ),
integer_function2,
[final] ).
cnf(i_0_396,axiom,
intersection(complement(kind_1_ordinals),ordinal_numbers) = limit_ordinals,
limit_ordinals,
[final] ).
cnf(i_0_397,axiom,
subclass(X1,universal_class),
class_elements_are_sets,
[final] ).
cnf(i_0_398,axiom,
( function(X1)
| ~ operation(X1) ),
operation1,
[final] ).
cnf(i_0_399,axiom,
( function(X1)
| ~ one_to_one(X1) ),
one_to_one1,
[final] ).
cnf(i_0_400,negated_conjecture,
irreflexive(x,y),
prove_irreflexive_class_property6_1,
[final] ).
cnf(i_0_401,axiom,
member(omega,universal_class),
omega_in_universal,
[final] ).
cnf(i_0_402,axiom,
function(choice),
choice1,
[final] ).
cnf(i_0_403,axiom,
inductive(omega),
omega_is_inductive1,
[final] ).
cnf(i_0_404,axiom,
X1 = X1 ).
cnf(i_0_405,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_406,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_407,axiom,
( X1 != X2
| domain_of(X1) = domain_of(X2) ) ).
cnf(i_0_408,axiom,
( X1 != X2
| compose(X1,X3) = compose(X2,X3) ) ).
cnf(i_0_409,axiom,
( X1 != X2
| compose(X3,X1) = compose(X3,X2) ) ).
cnf(i_0_410,axiom,
( X1 != X2
| single_valued3(X1) = single_valued3(X2) ) ).
cnf(i_0_411,axiom,
( X1 != X2
| recursion(X1,X3,X4) = recursion(X2,X3,X4) ) ).
cnf(i_0_412,axiom,
( X1 != X2
| recursion(X3,X1,X4) = recursion(X3,X2,X4) ) ).
cnf(i_0_413,axiom,
( X1 != X2
| recursion(X3,X4,X1) = recursion(X3,X4,X2) ) ).
cnf(i_0_414,axiom,
( X1 != X2
| ordinal_add(X1,X3) = ordinal_add(X2,X3) ) ).
cnf(i_0_415,axiom,
( X1 != X2
| ordinal_add(X3,X1) = ordinal_add(X3,X2) ) ).
cnf(i_0_416,axiom,
( X1 != X2
| ordinal_multiply(X1,X3) = ordinal_multiply(X2,X3) ) ).
cnf(i_0_417,axiom,
( X1 != X2
| ordinal_multiply(X3,X1) = ordinal_multiply(X3,X2) ) ).
cnf(i_0_418,axiom,
( X1 != X2
| complement(X1) = complement(X2) ) ).
cnf(i_0_419,axiom,
( X1 != X2
| cantor(X1) = cantor(X2) ) ).
cnf(i_0_420,axiom,
( X1 != X2
| intersection(X1,X3) = intersection(X2,X3) ) ).
cnf(i_0_421,axiom,
( X1 != X2
| intersection(X3,X1) = intersection(X3,X2) ) ).
cnf(i_0_422,axiom,
( X1 != X2
| not_well_ordering(X1,X3) = not_well_ordering(X2,X3) ) ).
cnf(i_0_423,axiom,
( X1 != X2
| not_well_ordering(X3,X1) = not_well_ordering(X3,X2) ) ).
cnf(i_0_424,axiom,
( X1 != X2
| rest_of(X1) = rest_of(X2) ) ).
cnf(i_0_425,axiom,
( X1 != X2
| integer_of(X1) = integer_of(X2) ) ).
cnf(i_0_426,axiom,
( X1 != X2
| cross_product(X1,X3) = cross_product(X2,X3) ) ).
cnf(i_0_427,axiom,
( X1 != X2
| cross_product(X3,X1) = cross_product(X3,X2) ) ).
cnf(i_0_428,axiom,
( X1 != X2
| unordered_pair(X1,X3) = unordered_pair(X2,X3) ) ).
cnf(i_0_429,axiom,
( X1 != X2
| unordered_pair(X3,X1) = unordered_pair(X3,X2) ) ).
cnf(i_0_430,axiom,
( X1 != X2
| first(X1) = first(X2) ) ).
cnf(i_0_431,axiom,
( X1 != X2
| ~ homomorphism(X1,X3,X4)
| homomorphism(X2,X3,X4) ) ).
cnf(i_0_432,axiom,
( X1 != X2
| ~ homomorphism(X3,X1,X4)
| homomorphism(X3,X2,X4) ) ).
cnf(i_0_433,axiom,
( X1 != X2
| ~ homomorphism(X3,X4,X1)
| homomorphism(X3,X4,X2) ) ).
cnf(i_0_434,axiom,
( X1 != X2
| ~ transitive(X1,X3)
| transitive(X2,X3) ) ).
cnf(i_0_435,axiom,
( X1 != X2
| ~ transitive(X3,X1)
| transitive(X3,X2) ) ).
cnf(i_0_436,axiom,
( X1 != X2
| ~ asymmetric(X1,X3)
| asymmetric(X2,X3) ) ).
cnf(i_0_437,axiom,
( X1 != X2
| ~ asymmetric(X3,X1)
| asymmetric(X3,X2) ) ).
cnf(i_0_438,axiom,
( X1 != X2
| ~ maps(X1,X3,X4)
| maps(X2,X3,X4) ) ).
cnf(i_0_439,axiom,
( X1 != X2
| ~ maps(X3,X1,X4)
| maps(X3,X2,X4) ) ).
cnf(i_0_440,axiom,
( X1 != X2
| ~ maps(X3,X4,X1)
| maps(X3,X4,X2) ) ).
cnf(i_0_441,axiom,
( X1 != X2
| ~ single_valued_class(X1)
| single_valued_class(X2) ) ).
cnf(i_0_442,axiom,
( X1 != X2
| ~ section(X1,X3,X4)
| section(X2,X3,X4) ) ).
cnf(i_0_443,axiom,
( X1 != X2
| ~ section(X3,X1,X4)
| section(X3,X2,X4) ) ).
cnf(i_0_444,axiom,
( X1 != X2
| ~ section(X3,X4,X1)
| section(X3,X4,X2) ) ).
cnf(i_0_445,axiom,
( X1 != X2
| ~ one_to_one(X1)
| one_to_one(X2) ) ).
cnf(i_0_446,axiom,
( X1 != X2
| ~ irreflexive(X1,X3)
| irreflexive(X2,X3) ) ).
cnf(i_0_447,axiom,
( X1 != X2
| ~ irreflexive(X3,X1)
| irreflexive(X3,X2) ) ).
cnf(i_0_448,axiom,
( X1 != X2
| ~ operation(X1)
| operation(X2) ) ).
cnf(i_0_449,axiom,
( X1 != X2
| ~ compatible(X1,X3,X4)
| compatible(X2,X3,X4) ) ).
cnf(i_0_450,axiom,
( X1 != X2
| ~ compatible(X3,X1,X4)
| compatible(X3,X2,X4) ) ).
cnf(i_0_451,axiom,
( X1 != X2
| ~ compatible(X3,X4,X1)
| compatible(X3,X4,X2) ) ).
cnf(i_0_452,axiom,
( X1 != X2
| ~ member(X1,X3)
| member(X2,X3) ) ).
cnf(i_0_453,axiom,
( X1 != X2
| ~ member(X3,X1)
| member(X3,X2) ) ).
cnf(i_0_454,axiom,
( X1 != X2
| ~ connected(X1,X3)
| connected(X2,X3) ) ).
cnf(i_0_455,axiom,
( X1 != X2
| ~ connected(X3,X1)
| connected(X3,X2) ) ).
cnf(i_0_456,axiom,
( X1 != X2
| ~ subclass(X1,X3)
| subclass(X2,X3) ) ).
cnf(i_0_457,axiom,
( X1 != X2
| ~ subclass(X3,X1)
| subclass(X3,X2) ) ).
cnf(i_0_458,axiom,
( X1 != X2
| ~ inductive(X1)
| inductive(X2) ) ).
cnf(i_0_459,axiom,
( X1 != X2
| ~ function(X1)
| function(X2) ) ).
cnf(i_0_460,axiom,
( X1 != X2
| ~ well_ordering(X1,X3)
| well_ordering(X2,X3) ) ).
cnf(i_0_461,axiom,
( X1 != X2
| ~ well_ordering(X3,X1)
| well_ordering(X3,X2) ) ).
cnf(i_0_4081,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4083,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4084,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4086,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4087,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4089,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4090,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4092,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4093,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4095,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4096,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4098,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4099,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4101,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4102,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4104,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4105,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4107,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4108,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4110,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4111,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4113,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4114,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4116,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4117,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4119,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4120,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4122,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4123,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4125,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4126,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4128,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4129,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4131,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4132,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4134,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4135,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4137,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4138,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4140,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4141,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4143,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4144,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4146,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4147,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4149,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4150,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4152,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4153,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4155,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4156,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4158,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4159,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4161,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4162,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4164,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4165,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4167,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4168,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4170,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4171,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4173,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4174,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4176,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4177,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4179,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4180,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4182,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4183,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4185,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4186,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4188,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4189,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4191,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4192,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4194,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4195,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4197,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4198,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4200,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4201,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4203,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4204,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4206,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4207,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4209,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4210,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4212,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4213,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4215,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4216,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4218,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4219,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4221,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4222,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4224,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4225,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4227,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4228,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4230,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4231,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4233,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4234,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4236,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4237,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4239,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4240,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4242,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4243,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4245,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4246,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4248,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4249,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4251,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4252,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4254,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4255,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4257,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4258,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4260,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4261,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4263,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4264,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4266,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4267,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4269,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4270,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4272,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4273,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4275,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4276,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4278,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4279,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4281,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4282,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4284,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4285,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4287,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4288,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4290,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4291,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4293,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4294,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4296,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4297,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4299,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4300,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4302,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4303,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4305,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4306,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4308,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4309,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4311,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4312,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4314,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4315,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4317,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4318,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4320,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4321,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4323,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4324,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4326,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4327,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4329,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4330,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4332,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4333,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4335,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4336,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4338,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4339,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4341,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4342,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4344,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4345,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4347,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4348,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4350,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4351,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4353,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4354,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4356,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4357,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4359,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4360,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4362,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4363,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4365,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4366,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4368,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4369,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4371,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4372,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4374,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4375,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4377,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4378,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4380,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4381,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4383,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4384,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4386,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4387,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4389,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4390,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4392,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4393,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4395,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4396,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4398,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4399,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4401,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4402,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4404,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4405,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4407,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4408,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4410,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4411,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4413,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4414,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4416,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4417,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4419,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4420,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4422,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4423,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4425,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4426,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4428,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4429,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4431,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4432,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4434,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4435,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4437,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4438,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4440,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4441,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4443,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4444,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4446,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4447,plain,
subclass(X1,universal_class),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4511,plain,
intersection(cross_product(X1,X2),X3) = intersection(X3,cross_product(X1,X2)),
inference(rename_variables,[],[i_0_354]) ).
cnf(i_0_4520,plain,
member(unordered_pair(X1,X2),universal_class),
inference(rename_variables,[],[i_0_378]) ).
cnf(i_0_4603,plain,
intersection(cross_product(X1,X2),X3) = intersection(X3,cross_product(X1,X2)),
inference(rename_variables,[],[i_0_354]) ).
cnf(i_0_4608,plain,
member(unordered_pair(X1,X2),universal_class),
inference(rename_variables,[],[i_0_378]) ).
cnf(i_0_4671,plain,
intersection(cross_product(X1,X2),X3) = intersection(X3,cross_product(X1,X2)),
inference(rename_variables,[],[i_0_354]) ).
cnf(i_0_4937,plain,
member(unordered_pair(X1,X2),universal_class),
inference(rename_variables,[],[i_0_378]) ).
cnf(i_0_5007,plain,
member(unordered_pair(X1,X2),universal_class),
inference(rename_variables,[],[i_0_378]) ).
cnf(i_0_5075,plain,
member(unordered_pair(X1,X2),universal_class),
inference(rename_variables,[],[i_0_378]) ).
cnf(i_0_5209,plain,
subclass(compose_class(X1),cross_product(universal_class,universal_class)),
inference(rename_variables,[],[i_0_377]) ).
cnf(i_0_5329,plain,
member(unordered_pair(X1,X2),universal_class),
inference(rename_variables,[],[i_0_378]) ).
cnf(i_0_479,plain,
maps(choice,domain_of(choice),domain_of(domain_of(flip(cross_product(choice,universal_class))))),
inference(scs_inference,[],[i_0_467,i_0_401,i_0_402,i_0_354,i_0_292,i_0_405,i_0_393,i_0_394,i_0_364,i_0_365,i_0_406,i_0_305]) ).
cnf(i_0_480,plain,
subclass(X1,X1),
inference(rename_variables,[],[i_0_467]) ).
cnf(i_0_484,plain,
subclass(X1,X1),
inference(rename_variables,[],[i_0_467]) ).
cnf(i_0_488,plain,
subclass(X1,X1),
inference(rename_variables,[],[i_0_467]) ).
cnf(i_0_495,plain,
subclass(X1,X1),
inference(rename_variables,[],[i_0_467]) ).
cnf(i_0_498,plain,
subclass(X1,X1),
inference(rename_variables,[],[i_0_467]) ).
cnf(i_0_499,plain,
subclass(X1,X1),
inference(rename_variables,[],[i_0_467]) ).
cnf(i_0_505,plain,
member(unordered_pair(X1,X2),unordered_pair(unordered_pair(X1,X2),X3)),
inference(scs_inference,[],[i_0_478,i_0_378,i_0_393,i_0_394,i_0_364]) ).
cnf(i_0_507,plain,
member(unordered_pair(X1,X2),unordered_pair(X3,unordered_pair(X1,X2))),
inference(scs_inference,[],[i_0_478,i_0_378,i_0_393,i_0_394,i_0_364,i_0_365]) ).
cnf(i_0_510,plain,
maps(choice,domain_of(choice),universal_class),
inference(scs_inference,[],[i_0_478,i_0_397,i_0_402,i_0_378,i_0_393,i_0_394,i_0_364,i_0_365,i_0_405,i_0_305]) ).
cnf(i_0_515,plain,
subclass(X1,X1),
inference(rename_variables,[],[i_0_467]) ).
cnf(i_0_530,plain,
subclass(X1,X1),
inference(rename_variables,[],[i_0_467]) ).
cnf(i_0_534,plain,
subclass(X1,X1),
inference(rename_variables,[],[i_0_467]) ).
cnf(i_0_544,plain,
subclass(X1,X1),
inference(rename_variables,[],[i_0_467]) ).
cnf(i_0_567,plain,
subclass(X1,X1),
inference(rename_variables,[],[i_0_467]) ).
cnf(i_0_579,plain,
subclass(X1,X1),
inference(rename_variables,[],[i_0_467]) ).
cnf(i_0_583,plain,
subclass(X1,X1),
inference(rename_variables,[],[i_0_467]) ).
cnf(i_0_589,plain,
subclass(X1,X1),
inference(rename_variables,[],[i_0_467]) ).
cnf(i_0_593,plain,
subclass(X1,X1),
inference(rename_variables,[],[i_0_467]) ).
cnf(i_0_599,plain,
subclass(X1,X1),
inference(rename_variables,[],[i_0_467]) ).
cnf(i_0_603,plain,
subclass(X1,X1),
inference(rename_variables,[],[i_0_467]) ).
cnf(i_0_615,plain,
subclass(X1,X1),
inference(rename_variables,[],[i_0_467]) ).
cnf(i_0_623,plain,
subclass(X1,X1),
inference(rename_variables,[],[i_0_467]) ).
cnf(i_0_627,plain,
subclass(X1,X1),
inference(rename_variables,[],[i_0_467]) ).
cnf(i_0_633,plain,
subclass(X1,X1),
inference(rename_variables,[],[i_0_467]) ).
cnf(i_0_637,plain,
subclass(X1,X1),
inference(rename_variables,[],[i_0_467]) ).
cnf(i_0_642,plain,
subclass(X1,X1),
inference(rename_variables,[],[i_0_467]) ).
cnf(i_0_648,plain,
subclass(X1,X1),
inference(rename_variables,[],[i_0_467]) ).
cnf(i_0_652,plain,
subclass(X1,X1),
inference(rename_variables,[],[i_0_467]) ).
cnf(i_0_657,plain,
subclass(X1,X1),
inference(rename_variables,[],[i_0_467]) ).
cnf(i_0_665,plain,
subclass(X1,X1),
inference(rename_variables,[],[i_0_467]) ).
cnf(i_0_668,plain,
subclass(X1,X1),
inference(rename_variables,[],[i_0_467]) ).
cnf(i_0_671,plain,
subclass(X1,X1),
inference(rename_variables,[],[i_0_467]) ).
cnf(i_0_3680,plain,
subclass(X1,X1),
inference(rename_variables,[],[i_0_467]) ).
cnf(i_0_4021,plain,
subclass(X1,X1),
inference(rename_variables,[],[i_0_467]) ).
cnf(i_0_4449,plain,
compose(limit_ordinals,X1) = compose(intersection(complement(kind_1_ordinals),ordinal_numbers),X1),
inference(scs_inference,[],[i_0_540,i_0_408]) ).
cnf(i_0_4450,plain,
compose(X1,limit_ordinals) = compose(X1,intersection(complement(kind_1_ordinals),ordinal_numbers)),
inference(scs_inference,[],[i_0_540,i_0_408,i_0_409]) ).
cnf(i_0_4459,plain,
complement(limit_ordinals) = complement(intersection(complement(kind_1_ordinals),ordinal_numbers)),
inference(scs_inference,[],[i_0_540,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_415,i_0_416,i_0_417,i_0_418]) ).
cnf(i_0_4460,plain,
cantor(limit_ordinals) = cantor(intersection(complement(kind_1_ordinals),ordinal_numbers)),
inference(scs_inference,[],[i_0_540,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_415,i_0_416,i_0_417,i_0_418,i_0_419]) ).
cnf(i_0_4465,plain,
rest_of(limit_ordinals) = rest_of(intersection(complement(kind_1_ordinals),ordinal_numbers)),
inference(scs_inference,[],[i_0_540,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_415,i_0_416,i_0_417,i_0_418,i_0_419,i_0_420,i_0_421,i_0_422,i_0_423,i_0_424]) ).
cnf(i_0_4466,plain,
integer_of(limit_ordinals) = integer_of(intersection(complement(kind_1_ordinals),ordinal_numbers)),
inference(scs_inference,[],[i_0_540,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_415,i_0_416,i_0_417,i_0_418,i_0_419,i_0_420,i_0_421,i_0_422,i_0_423,i_0_424,i_0_425]) ).
cnf(i_0_4471,plain,
first(limit_ordinals) = first(intersection(complement(kind_1_ordinals),ordinal_numbers)),
inference(scs_inference,[],[i_0_540,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_415,i_0_416,i_0_417,i_0_418,i_0_419,i_0_420,i_0_421,i_0_422,i_0_423,i_0_424,i_0_425,i_0_426,i_0_427,i_0_428,i_0_429,i_0_430]) ).
cnf(i_0_4472,plain,
member(null_class,omega),
inference(scs_inference,[],[i_0_540,i_0_403,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_415,i_0_416,i_0_417,i_0_418,i_0_419,i_0_420,i_0_421,i_0_422,i_0_423,i_0_424,i_0_425,i_0_426,i_0_427,i_0_428,i_0_429,i_0_430,i_0_391]) ).
cnf(i_0_4474,plain,
subclass(choice,cross_product(universal_class,universal_class)),
inference(scs_inference,[],[i_0_540,i_0_403,i_0_402,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_415,i_0_416,i_0_417,i_0_418,i_0_419,i_0_420,i_0_421,i_0_422,i_0_423,i_0_424,i_0_425,i_0_426,i_0_427,i_0_428,i_0_429,i_0_430,i_0_391,i_0_375]) ).
cnf(i_0_4478,plain,
subclass(intersection(x,cross_product(y,y)),complement(identity_relation)),
inference(scs_inference,[],[i_0_351,i_0_400,i_0_540,i_0_403,i_0_402,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_415,i_0_416,i_0_417,i_0_418,i_0_419,i_0_420,i_0_421,i_0_422,i_0_423,i_0_424,i_0_425,i_0_426,i_0_427,i_0_428,i_0_429,i_0_430,i_0_391,i_0_375,i_0_390,i_0_338]) ).
cnf(i_0_4480,plain,
subclass(compose(choice,domain_of(flip(cross_product(choice,universal_class)))),identity_relation),
inference(scs_inference,[],[i_0_351,i_0_400,i_0_540,i_0_403,i_0_402,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_415,i_0_416,i_0_417,i_0_418,i_0_419,i_0_420,i_0_421,i_0_422,i_0_423,i_0_424,i_0_425,i_0_426,i_0_427,i_0_428,i_0_429,i_0_430,i_0_391,i_0_375,i_0_390,i_0_338,i_0_327]) ).
cnf(i_0_4501,plain,
subclass(X1,X1),
inference(rename_variables,[],[i_0_467]) ).
cnf(i_0_4513,plain,
intersection(X1,cross_product(X2,X3)) = intersection(cross_product(X2,X3),X1),
inference(rename_variables,[],[i_0_469]) ).
cnf(i_0_4515,plain,
intersection(X1,cross_product(X2,X3)) = intersection(cross_product(X2,X3),X1),
inference(rename_variables,[],[i_0_469]) ).
cnf(i_0_4517,plain,
subclass(X1,X1),
inference(rename_variables,[],[i_0_467]) ).
cnf(i_0_4519,plain,
subclass(intersection(cross_product(X1,X2),X3),intersection(X3,cross_product(X1,X2))),
inference(rename_variables,[],[i_0_470]) ).
cnf(i_0_4605,plain,
intersection(X1,cross_product(X2,X3)) = intersection(cross_product(X2,X3),X1),
inference(rename_variables,[],[i_0_469]) ).
cnf(i_0_4607,plain,
subclass(X1,X1),
inference(rename_variables,[],[i_0_467]) ).
cnf(i_0_4666,plain,
subclass(X1,X1),
inference(rename_variables,[],[i_0_467]) ).
cnf(i_0_4673,plain,
subclass(X1,X1),
inference(rename_variables,[],[i_0_467]) ).
cnf(i_0_4940,plain,
subclass(X1,X1),
inference(rename_variables,[],[i_0_467]) ).
cnf(i_0_4943,plain,
subclass(X1,X1),
inference(rename_variables,[],[i_0_467]) ).
cnf(i_0_5006,plain,
subclass(intersection(cross_product(X1,X2),X3),intersection(X3,cross_product(X1,X2))),
inference(rename_variables,[],[i_0_470]) ).
cnf(i_0_5067,plain,
subclass(X1,X1),
inference(rename_variables,[],[i_0_467]) ).
cnf(i_0_5072,plain,
subclass(X1,X1),
inference(rename_variables,[],[i_0_467]) ).
cnf(i_0_5074,plain,
subclass(X1,X1),
inference(rename_variables,[],[i_0_467]) ).
cnf(i_0_5200,plain,
subclass(X1,X1),
inference(rename_variables,[],[i_0_467]) ).
cnf(i_0_5211,plain,
intersection(X1,cross_product(X2,X3)) = intersection(cross_product(X2,X3),X1),
inference(rename_variables,[],[i_0_469]) ).
cnf(i_0_5332,plain,
subclass(X1,X1),
inference(rename_variables,[],[i_0_467]) ).
cnf(i_0_5337,plain,
subclass(X1,X1),
inference(rename_variables,[],[i_0_467]) ).
cnf(i_0_5457,plain,
subclass(X1,X1),
inference(rename_variables,[],[i_0_467]) ).
cnf(i_0_5462,plain,
subclass(X1,X1),
inference(rename_variables,[],[i_0_467]) ).
cnf(i_0_5464,plain,
subclass(intersection(X1,cross_product(X2,X3)),intersection(cross_product(X2,X3),X1)),
inference(rename_variables,[],[i_0_472]) ).
cnf(i_0_5534,plain,
subclass(X1,X1),
inference(rename_variables,[],[i_0_467]) ).
cnf(i_0_482,plain,
section(X1,universal_class,universal_class),
inference(scs_inference,[],[i_0_467,i_0_480,i_0_397,i_0_401,i_0_402,i_0_354,i_0_292,i_0_405,i_0_393,i_0_394,i_0_364,i_0_365,i_0_406,i_0_305,i_0_317]) ).
cnf(i_0_486,plain,
~ well_ordering(universal_class,universal_class),
inference(scs_inference,[],[i_0_467,i_0_480,i_0_484,i_0_397,i_0_401,i_0_402,i_0_378,i_0_354,i_0_292,i_0_405,i_0_393,i_0_394,i_0_364,i_0_365,i_0_406,i_0_305,i_0_317,i_0_291]) ).
cnf(i_0_521,plain,
function(choice),
inference(equality_inference,[],[513]) ).
cnf(i_0_4490,plain,
~ member(unordered_pair(X1,X2),complement(unordered_pair(unordered_pair(X1,X2),X3))),
inference(scs_inference,[],[i_0_351,i_0_400,i_0_505,i_0_540,i_0_403,i_0_401,i_0_402,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_415,i_0_416,i_0_417,i_0_418,i_0_419,i_0_420,i_0_421,i_0_422,i_0_423,i_0_424,i_0_425,i_0_426,i_0_427,i_0_428,i_0_429,i_0_430,i_0_391,i_0_375,i_0_390,i_0_338,i_0_327,i_0_332,i_0_290,i_0_315,i_0_316,i_0_370]) ).
cnf(i_0_4494,plain,
~ member(unordered_pair(X1,X2),intersection(complement(unordered_pair(unordered_pair(X1,X2),X3)),X4)),
inference(scs_inference,[],[i_0_351,i_0_400,i_0_505,i_0_540,i_0_403,i_0_401,i_0_402,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_415,i_0_416,i_0_417,i_0_418,i_0_419,i_0_420,i_0_421,i_0_422,i_0_423,i_0_424,i_0_425,i_0_426,i_0_427,i_0_428,i_0_429,i_0_430,i_0_391,i_0_375,i_0_390,i_0_338,i_0_327,i_0_332,i_0_290,i_0_315,i_0_316,i_0_370,i_0_389,i_0_356]) ).
cnf(i_0_4496,plain,
~ member(unordered_pair(X1,X2),intersection(X3,complement(unordered_pair(unordered_pair(X1,X2),X4)))),
inference(scs_inference,[],[i_0_351,i_0_400,i_0_505,i_0_540,i_0_403,i_0_401,i_0_402,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_415,i_0_416,i_0_417,i_0_418,i_0_419,i_0_420,i_0_421,i_0_422,i_0_423,i_0_424,i_0_425,i_0_426,i_0_427,i_0_428,i_0_429,i_0_430,i_0_391,i_0_375,i_0_390,i_0_338,i_0_327,i_0_332,i_0_290,i_0_315,i_0_316,i_0_370,i_0_389,i_0_356,i_0_357]) ).
cnf(i_0_4498,plain,
domain_of(limit_ordinals) = domain_of(intersection(complement(kind_1_ordinals),ordinal_numbers)),
inference(scs_inference,[],[i_0_351,i_0_400,i_0_505,i_0_540,i_0_403,i_0_401,i_0_402,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_415,i_0_416,i_0_417,i_0_418,i_0_419,i_0_420,i_0_421,i_0_422,i_0_423,i_0_424,i_0_425,i_0_426,i_0_427,i_0_428,i_0_429,i_0_430,i_0_391,i_0_375,i_0_390,i_0_338,i_0_327,i_0_332,i_0_290,i_0_315,i_0_316,i_0_370,i_0_389,i_0_356,i_0_357,i_0_407]) ).
cnf(i_0_4499,plain,
null_class != intersection(intersection(x,identity_relation),cross_product(y,y)),
inference(scs_inference,[],[i_0_351,i_0_400,i_0_505,i_0_540,i_0_403,i_0_401,i_0_402,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_415,i_0_416,i_0_417,i_0_418,i_0_419,i_0_420,i_0_421,i_0_422,i_0_423,i_0_424,i_0_425,i_0_426,i_0_427,i_0_428,i_0_429,i_0_430,i_0_391,i_0_375,i_0_390,i_0_338,i_0_327,i_0_332,i_0_290,i_0_315,i_0_316,i_0_370,i_0_389,i_0_356,i_0_357,i_0_407,i_0_405]) ).
cnf(i_0_4514,plain,
intersection(cross_product(y,y),intersection(x,identity_relation)) != null_class,
inference(scs_inference,[],[i_0_351,i_0_400,i_0_505,i_0_540,i_0_469,i_0_4513,i_0_354,i_0_403,i_0_401,i_0_402,i_0_467,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_415,i_0_416,i_0_417,i_0_418,i_0_419,i_0_420,i_0_421,i_0_422,i_0_423,i_0_424,i_0_425,i_0_426,i_0_427,i_0_428,i_0_429,i_0_430,i_0_391,i_0_375,i_0_390,i_0_338,i_0_327,i_0_332,i_0_290,i_0_315,i_0_316,i_0_370,i_0_389,i_0_356,i_0_357,i_0_407,i_0_405,i_0_457,i_0_350,i_0_362,i_0_321,i_0_288,i_0_452,i_0_453,i_0_406]) ).
cnf(i_0_4518,plain,
~ well_ordering(universal_class,intersection(intersection(x,identity_relation),cross_product(y,y))),
inference(scs_inference,[],[i_0_351,i_0_400,i_0_470,i_0_505,i_0_540,i_0_469,i_0_4513,i_0_354,i_0_403,i_0_401,i_0_402,i_0_378,i_0_467,i_0_4501,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_415,i_0_416,i_0_417,i_0_418,i_0_419,i_0_420,i_0_421,i_0_422,i_0_423,i_0_424,i_0_425,i_0_426,i_0_427,i_0_428,i_0_429,i_0_430,i_0_391,i_0_375,i_0_390,i_0_338,i_0_327,i_0_332,i_0_290,i_0_315,i_0_316,i_0_370,i_0_389,i_0_356,i_0_357,i_0_407,i_0_405,i_0_457,i_0_350,i_0_362,i_0_321,i_0_288,i_0_452,i_0_453,i_0_406,i_0_456,i_0_291]) ).
cnf(i_0_4595,plain,
compose(X1,limit_ordinals) = compose(X1,intersection(complement(kind_1_ordinals),ordinal_numbers)),
inference(rename_variables,[],[i_0_4450]) ).
cnf(i_0_4876,plain,
member(unordered_pair(X1,X2),unordered_pair(X3,unordered_pair(X1,X2))),
inference(rename_variables,[],[i_0_507]) ).
cnf(i_0_5138,plain,
~ member(unordered_pair(X1,X2),complement(unordered_pair(unordered_pair(X1,X2),X3))),
inference(rename_variables,[],[i_0_4490]) ).
cnf(i_0_5648,plain,
~ member(unordered_pair(X1,X2),intersection(complement(unordered_pair(unordered_pair(X1,X2),X3)),X4)),
inference(rename_variables,[],[i_0_4494]) ).
cnf(i_0_618,plain,
~ well_ordering(universal_class,universal_class),
inference(equality_inference,[],[606]) ).
cnf(i_0_619,plain,
inductive(omega),
inference(equality_inference,[],[617]) ).
cnf(i_0_644,plain,
~ well_ordering(universal_class,universal_class),
inference(equality_inference,[],[639]) ).
cnf(i_0_4522,plain,
member(unordered_pair(X1,X2),complement(complement(unordered_pair(unordered_pair(X1,X2),X3)))),
inference(scs_inference,[],[i_0_351,i_0_400,i_0_470,i_0_505,i_0_540,i_0_469,i_0_4513,i_0_354,i_0_403,i_0_401,i_0_402,i_0_378,i_0_467,i_0_4501,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_415,i_0_416,i_0_417,i_0_418,i_0_419,i_0_420,i_0_421,i_0_422,i_0_423,i_0_424,i_0_425,i_0_426,i_0_427,i_0_428,i_0_429,i_0_430,i_0_391,i_0_375,i_0_390,i_0_338,i_0_327,i_0_332,i_0_290,i_0_315,i_0_316,i_0_370,i_0_389,i_0_356,i_0_357,i_0_407,i_0_405,i_0_457,i_0_350,i_0_362,i_0_321,i_0_288,i_0_452,i_0_453,i_0_406,i_0_456,i_0_291,i_0_607]) ).
cnf(i_0_4556,plain,
~ member(null_class,complement(omega)),
inference(scs_inference,[],[i_0_4472,i_0_4504,i_0_4510,i_0_4514,i_0_4482,i_0_4496,i_0_4530,i_0_390,i_0_607,i_0_332,i_0_312,i_0_306,i_0_307,i_0_278,i_0_389,i_0_370]) ).
cnf(i_0_4586,plain,
null_class != intersection(cross_product(y,y),intersection(x,identity_relation)),
inference(scs_inference,[],[i_0_4472,i_0_4504,i_0_4510,i_0_4514,i_0_4452,i_0_4482,i_0_4496,i_0_4530,i_0_390,i_0_607,i_0_332,i_0_312,i_0_306,i_0_307,i_0_278,i_0_389,i_0_370,i_0_356,i_0_357,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_415,i_0_416,i_0_417,i_0_418,i_0_419,i_0_420,i_0_421,i_0_422,i_0_423,i_0_424,i_0_425,i_0_426,i_0_427,i_0_428,i_0_429,i_0_430,i_0_407,i_0_405]) ).
cnf(i_0_4587,plain,
member(null_class,intersection(omega,omega)),
inference(scs_inference,[],[i_0_4472,i_0_4504,i_0_4510,i_0_4514,i_0_4452,i_0_4482,i_0_4496,i_0_4530,i_0_390,i_0_607,i_0_332,i_0_312,i_0_306,i_0_307,i_0_278,i_0_389,i_0_370,i_0_356,i_0_357,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_415,i_0_416,i_0_417,i_0_418,i_0_419,i_0_420,i_0_421,i_0_422,i_0_423,i_0_424,i_0_425,i_0_426,i_0_427,i_0_428,i_0_429,i_0_430,i_0_407,i_0_405,i_0_350]) ).
cnf(i_0_4598,plain,
omega != complement(omega),
inference(scs_inference,[],[i_0_4472,i_0_4504,i_0_4510,i_0_4514,i_0_4499,i_0_4452,i_0_4450,i_0_4469,i_0_4500,i_0_4482,i_0_4502,i_0_4496,i_0_4530,i_0_390,i_0_607,i_0_332,i_0_312,i_0_306,i_0_307,i_0_278,i_0_389,i_0_370,i_0_356,i_0_357,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_415,i_0_416,i_0_417,i_0_418,i_0_419,i_0_420,i_0_421,i_0_422,i_0_423,i_0_424,i_0_425,i_0_426,i_0_427,i_0_428,i_0_429,i_0_430,i_0_407,i_0_405,i_0_350,i_0_362,i_0_321,i_0_457,i_0_452,i_0_453]) ).
cnf(i_0_4602,plain,
~ well_ordering(universal_class,intersection(cross_product(y,y),intersection(x,identity_relation))),
inference(scs_inference,[],[i_0_4472,i_0_4504,i_0_4510,i_0_4514,i_0_4518,i_0_4499,i_0_4452,i_0_4453,i_0_4450,i_0_4469,i_0_4500,i_0_4482,i_0_4502,i_0_4496,i_0_4530,i_0_354,i_0_390,i_0_607,i_0_332,i_0_312,i_0_306,i_0_307,i_0_278,i_0_389,i_0_370,i_0_356,i_0_357,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_415,i_0_416,i_0_417,i_0_418,i_0_419,i_0_420,i_0_421,i_0_422,i_0_423,i_0_424,i_0_425,i_0_426,i_0_427,i_0_428,i_0_429,i_0_430,i_0_407,i_0_405,i_0_350,i_0_362,i_0_321,i_0_457,i_0_452,i_0_453,i_0_406,i_0_461]) ).
cnf(i_0_4604,plain,
subclass(intersection(cross_product(y,y),x),complement(identity_relation)),
inference(scs_inference,[],[i_0_4472,i_0_4504,i_0_4510,i_0_4478,i_0_4514,i_0_4518,i_0_4499,i_0_4452,i_0_4453,i_0_4450,i_0_4469,i_0_4500,i_0_4482,i_0_4502,i_0_4496,i_0_4530,i_0_469,i_0_354,i_0_390,i_0_607,i_0_332,i_0_312,i_0_306,i_0_307,i_0_278,i_0_389,i_0_370,i_0_356,i_0_357,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_415,i_0_416,i_0_417,i_0_418,i_0_419,i_0_420,i_0_421,i_0_422,i_0_423,i_0_424,i_0_425,i_0_426,i_0_427,i_0_428,i_0_429,i_0_430,i_0_407,i_0_405,i_0_350,i_0_362,i_0_321,i_0_457,i_0_452,i_0_453,i_0_406,i_0_461,i_0_456]) ).
cnf(i_0_4606,plain,
~ well_ordering(universal_class,omega),
inference(scs_inference,[],[i_0_4472,i_0_4504,i_0_4510,i_0_4478,i_0_4514,i_0_4518,i_0_4499,i_0_4452,i_0_4453,i_0_4450,i_0_4469,i_0_4500,i_0_4482,i_0_4502,i_0_4496,i_0_4530,i_0_469,i_0_354,i_0_378,i_0_467,i_0_390,i_0_607,i_0_332,i_0_312,i_0_306,i_0_307,i_0_278,i_0_389,i_0_370,i_0_356,i_0_357,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_415,i_0_416,i_0_417,i_0_418,i_0_419,i_0_420,i_0_421,i_0_422,i_0_423,i_0_424,i_0_425,i_0_426,i_0_427,i_0_428,i_0_429,i_0_430,i_0_407,i_0_405,i_0_350,i_0_362,i_0_321,i_0_457,i_0_452,i_0_453,i_0_406,i_0_461,i_0_456,i_0_291]) ).
cnf(i_0_4669,plain,
member(unordered_pair(X1,X2),complement(complement(unordered_pair(unordered_pair(X1,X2),X3)))),
inference(rename_variables,[],[i_0_4522]) ).
cnf(i_0_4628,plain,
~ member(null_class,complement(intersection(omega,omega))),
inference(scs_inference,[],[i_0_4556,i_0_4587,i_0_4548,i_0_378,i_0_332,i_0_306,i_0_307,i_0_312,i_0_278,i_0_607,i_0_370]) ).
cnf(i_0_4630,plain,
~ member(null_class,intersection(complement(omega),X1)),
inference(scs_inference,[],[i_0_4556,i_0_4587,i_0_4548,i_0_378,i_0_332,i_0_306,i_0_307,i_0_312,i_0_278,i_0_607,i_0_370,i_0_356]) ).
cnf(i_0_4632,plain,
~ member(null_class,intersection(X1,complement(omega))),
inference(scs_inference,[],[i_0_4556,i_0_4587,i_0_4548,i_0_378,i_0_332,i_0_306,i_0_307,i_0_312,i_0_278,i_0_607,i_0_370,i_0_356,i_0_357]) ).
cnf(i_0_4658,plain,
complement(omega) != omega,
inference(scs_inference,[],[i_0_4556,i_0_4587,i_0_4598,i_0_4454,i_0_4548,i_0_378,i_0_332,i_0_306,i_0_307,i_0_312,i_0_278,i_0_607,i_0_370,i_0_356,i_0_357,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_415,i_0_416,i_0_417,i_0_418,i_0_419,i_0_420,i_0_421,i_0_422,i_0_423,i_0_424,i_0_425,i_0_426,i_0_427,i_0_428,i_0_429,i_0_430,i_0_407,i_0_405]) ).
cnf(i_0_4659,plain,
member(null_class,intersection(intersection(omega,omega),intersection(omega,omega))),
inference(scs_inference,[],[i_0_4556,i_0_4587,i_0_4598,i_0_4454,i_0_4548,i_0_378,i_0_332,i_0_306,i_0_307,i_0_312,i_0_278,i_0_607,i_0_370,i_0_356,i_0_357,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_415,i_0_416,i_0_417,i_0_418,i_0_419,i_0_420,i_0_421,i_0_422,i_0_423,i_0_424,i_0_425,i_0_426,i_0_427,i_0_428,i_0_429,i_0_430,i_0_407,i_0_405,i_0_350]) ).
cnf(i_0_4663,plain,
~ member(omega,unordered_pair(complement(omega),complement(omega))),
inference(scs_inference,[],[i_0_4556,i_0_4587,i_0_4598,i_0_4454,i_0_4548,i_0_378,i_0_332,i_0_306,i_0_307,i_0_312,i_0_278,i_0_607,i_0_370,i_0_356,i_0_357,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_415,i_0_416,i_0_417,i_0_418,i_0_419,i_0_420,i_0_421,i_0_422,i_0_423,i_0_424,i_0_425,i_0_426,i_0_427,i_0_428,i_0_429,i_0_430,i_0_407,i_0_405,i_0_350,i_0_321,i_0_362]) ).
cnf(i_0_4674,plain,
member(omega,complement(unordered_pair(complement(omega),complement(omega)))),
inference(scs_inference,[],[i_0_4556,i_0_4587,i_0_4598,i_0_4454,i_0_4470,i_0_4554,i_0_4522,i_0_4548,i_0_354,i_0_378,i_0_467,i_0_4666,i_0_332,i_0_306,i_0_307,i_0_312,i_0_278,i_0_607,i_0_370,i_0_356,i_0_357,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_415,i_0_416,i_0_417,i_0_418,i_0_419,i_0_420,i_0_421,i_0_422,i_0_423,i_0_424,i_0_425,i_0_426,i_0_427,i_0_428,i_0_429,i_0_430,i_0_407,i_0_405,i_0_350,i_0_321,i_0_362,i_0_457,i_0_452,i_0_453,i_0_456,i_0_554]) ).
cnf(i_0_4685,plain,
irreflexive(x,y),
inference(equality_inference,[],[4678]) ).
cnf(i_0_4686,plain,
subclass(intersection(x,cross_product(y,y)),complement(identity_relation)),
inference(equality_inference,[],[4682]) ).
cnf(i_0_4702,plain,
~ member(null_class,complement(intersection(intersection(omega,omega),intersection(omega,omega)))),
inference(scs_inference,[],[i_0_4630,i_0_4659,i_0_4620,i_0_4616,i_0_4624,i_0_279,i_0_306,i_0_307,i_0_312,i_0_607,i_0_332,i_0_278,i_0_370]) ).
cnf(i_0_4704,plain,
~ member(null_class,intersection(intersection(complement(omega),X1),X2)),
inference(scs_inference,[],[i_0_4630,i_0_4659,i_0_4620,i_0_4616,i_0_4624,i_0_279,i_0_306,i_0_307,i_0_312,i_0_607,i_0_332,i_0_278,i_0_370,i_0_356]) ).
cnf(i_0_4706,plain,
~ member(null_class,intersection(X1,intersection(complement(omega),X2))),
inference(scs_inference,[],[i_0_4630,i_0_4659,i_0_4620,i_0_4616,i_0_4624,i_0_279,i_0_306,i_0_307,i_0_312,i_0_607,i_0_332,i_0_278,i_0_370,i_0_356,i_0_357]) ).
cnf(i_0_4736,plain,
~ member(complement(omega),unordered_pair(omega,omega)),
inference(scs_inference,[],[i_0_4658,i_0_4630,i_0_4659,i_0_4449,i_0_4620,i_0_4616,i_0_4624,i_0_279,i_0_306,i_0_307,i_0_312,i_0_607,i_0_332,i_0_278,i_0_370,i_0_356,i_0_357,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_415,i_0_416,i_0_417,i_0_418,i_0_419,i_0_420,i_0_421,i_0_422,i_0_423,i_0_424,i_0_425,i_0_426,i_0_427,i_0_428,i_0_429,i_0_430,i_0_407,i_0_350,i_0_321,i_0_362]) ).
cnf(i_0_4757,plain,
irreflexive(x,y),
inference(equality_inference,[],[4751]) ).
cnf(i_0_4758,plain,
subclass(intersection(x,cross_product(y,y)),complement(identity_relation)),
inference(equality_inference,[],[4754]) ).
cnf(i_0_4776,plain,
~ member(complement(omega),intersection(unordered_pair(omega,omega),X1)),
inference(scs_inference,[],[i_0_4736,i_0_4591,i_0_4618,i_0_4692,i_0_4761,i_0_279,i_0_306,i_0_307,i_0_312,i_0_607,i_0_278,i_0_370,i_0_356]) ).
cnf(i_0_4778,plain,
~ member(complement(omega),intersection(X1,unordered_pair(omega,omega))),
inference(scs_inference,[],[i_0_4736,i_0_4591,i_0_4618,i_0_4692,i_0_4761,i_0_279,i_0_306,i_0_307,i_0_312,i_0_607,i_0_278,i_0_370,i_0_356,i_0_357]) ).
cnf(i_0_4816,plain,
cross_product(omega,omega) != cross_product(complement(omega),X1),
inference(scs_inference,[],[i_0_4736,i_0_4628,i_0_4746,i_0_4740,i_0_4811,i_0_4814,i_0_4591,i_0_4674,i_0_4618,i_0_4692,i_0_4761,i_0_4747,i_0_4476,i_0_4738,i_0_279,i_0_306,i_0_307,i_0_312,i_0_607,i_0_278,i_0_370,i_0_356,i_0_357,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_415,i_0_416,i_0_417,i_0_418,i_0_419,i_0_420,i_0_421,i_0_422,i_0_423,i_0_424,i_0_425,i_0_426,i_0_427,i_0_428,i_0_429,i_0_430,i_0_407,i_0_350,i_0_321,i_0_362,i_0_457,i_0_452,i_0_456,i_0_448,i_0_453]) ).
cnf(i_0_4839,plain,
~ member(complement(omega),intersection(intersection(unordered_pair(omega,omega),X1),X2)),
inference(scs_inference,[],[i_0_4776,i_0_4492,i_0_4774,i_0_4622,i_0_4765,i_0_4676,i_0_279,i_0_306,i_0_307,i_0_312,i_0_607,i_0_278,i_0_370,i_0_356]) ).
cnf(i_0_4841,plain,
~ member(complement(omega),intersection(X1,intersection(unordered_pair(omega,omega),X2))),
inference(scs_inference,[],[i_0_4776,i_0_4492,i_0_4774,i_0_4622,i_0_4765,i_0_4676,i_0_279,i_0_306,i_0_307,i_0_312,i_0_607,i_0_278,i_0_370,i_0_356,i_0_357]) ).
cnf(i_0_4867,plain,
cross_product(complement(omega),X1) != cross_product(omega,omega),
inference(scs_inference,[],[i_0_4776,i_0_4816,i_0_4455,i_0_4492,i_0_4774,i_0_4622,i_0_4765,i_0_4676,i_0_279,i_0_306,i_0_307,i_0_312,i_0_607,i_0_278,i_0_370,i_0_356,i_0_357,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_415,i_0_416,i_0_417,i_0_418,i_0_419,i_0_420,i_0_421,i_0_422,i_0_423,i_0_424,i_0_425,i_0_426,i_0_427,i_0_428,i_0_429,i_0_430,i_0_407,i_0_405]) ).
cnf(i_0_5005,plain,
~ well_ordering(universal_class,intersection(cross_product(omega,omega),cross_product(omega,omega))),
inference(scs_inference,[],[i_0_4934,i_0_4942,i_0_4997,i_0_4457,i_0_4670,i_0_4932,i_0_4804,i_0_4786,i_0_4998,i_0_4826,i_0_4524,i_0_4887,i_0_4760,i_0_4586,i_0_476,i_0_470,i_0_4763,i_0_378,i_0_279,i_0_306,i_0_307,i_0_312,i_0_607,i_0_278,i_0_370,i_0_356,i_0_357,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_415,i_0_416,i_0_417,i_0_418,i_0_419,i_0_422,i_0_423,i_0_424,i_0_425,i_0_430,i_0_420,i_0_421,i_0_426,i_0_427,i_0_428,i_0_429,i_0_407,i_0_350,i_0_321,i_0_362,i_0_457,i_0_452,i_0_456,i_0_291]) ).
cnf(i_0_5073,plain,
~ well_ordering(universal_class,cross_product(unordered_pair(X1,omega),unordered_pair(X1,omega))),
inference(scs_inference,[],[i_0_4458,i_0_5064,i_0_4992,i_0_4962,i_0_4788,i_0_5009,i_0_4987,i_0_4667,i_0_4526,i_0_4546,i_0_4834,i_0_4700,i_0_4502,i_0_378,i_0_467,i_0_5067,i_0_5072,i_0_279,i_0_306,i_0_307,i_0_312,i_0_607,i_0_278,i_0_370,i_0_356,i_0_357,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_415,i_0_416,i_0_417,i_0_418,i_0_419,i_0_422,i_0_423,i_0_424,i_0_425,i_0_430,i_0_420,i_0_421,i_0_426,i_0_427,i_0_428,i_0_429,i_0_407,i_0_350,i_0_321,i_0_362,i_0_406,i_0_457,i_0_452,i_0_456,i_0_291]) ).
cnf(i_0_5456,plain,
subclass(rest_of(limit_ordinals),rest_of(intersection(complement(kind_1_ordinals),ordinal_numbers))),
inference(scs_inference,[],[i_0_4465,i_0_5358,i_0_5362,i_0_4784,i_0_4785,i_0_5294,i_0_5352,i_0_5156,i_0_467,i_0_279,i_0_306,i_0_307,i_0_312,i_0_607,i_0_278,i_0_370,i_0_356,i_0_357,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_415,i_0_416,i_0_417,i_0_418,i_0_419,i_0_422,i_0_423,i_0_424,i_0_425,i_0_430,i_0_428,i_0_420,i_0_421,i_0_426,i_0_427,i_0_429,i_0_407,i_0_350,i_0_406,i_0_457]) ).
cnf(i_0_5512,plain,
first(first(limit_ordinals)) = first(first(intersection(complement(kind_1_ordinals),ordinal_numbers))),
inference(scs_inference,[],[i_0_4471,i_0_5364,i_0_4769,i_0_5296,i_0_5409,i_0_5220,i_0_279,i_0_306,i_0_307,i_0_312,i_0_607,i_0_278,i_0_370,i_0_356,i_0_357,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_415,i_0_416,i_0_417,i_0_418,i_0_419,i_0_422,i_0_423,i_0_424,i_0_425,i_0_430]) ).
cnf(i_0_5522,plain,
complement(intersection(complement(kind_1_ordinals),ordinal_numbers)) = complement(limit_ordinals),
inference(scs_inference,[],[i_0_5336,i_0_4471,i_0_5331,i_0_5364,i_0_4769,i_0_5296,i_0_5409,i_0_5220,i_0_279,i_0_306,i_0_307,i_0_312,i_0_607,i_0_278,i_0_370,i_0_356,i_0_357,i_0_408,i_0_409,i_0_410,i_0_411,i_0_412,i_0_413,i_0_414,i_0_415,i_0_416,i_0_417,i_0_418,i_0_419,i_0_422,i_0_423,i_0_424,i_0_425,i_0_430,i_0_428,i_0_420,i_0_421,i_0_426,i_0_427,i_0_429,i_0_407,i_0_350,i_0_374]) ).
cnf(i_0_5541,plain,
maps(choice,domain_of(choice),universal_class),
inference(equality_inference,[],[5537]) ).
cnf(i_0_5542,plain,
domain_of(choice) = domain_of(choice),
inference(equality_inference,[],[5538]) ).
cnf(i_0_5600,plain,
maps(choice,domain_of(choice),universal_class),
inference(equality_inference,[],[5596]) ).
cnf(c_0_4598,axiom,
( member(X1,X2)
| ~ subclass(X3,X2)
| ~ member(X1,X3) ),
i_0_367 ).
cnf(c_0_4599,axiom,
subclass(X1,universal_class),
i_0_397 ).
cnf(c_0_4600,axiom,
( ~ member(X1,complement(X2))
| ~ member(X1,X2) ),
i_0_370 ).
cnf(c_0_4601,axiom,
( X1 = null_class
| member(regular(X1),X1) ),
i_0_389 ).
cnf(c_0_4602,plain,
( member(X1,universal_class)
| ~ member(X1,X2) ),
inference(spm,[status(thm)],[c_0_4598,c_0_4599]) ).
cnf(c_0_4603,plain,
( complement(X1) = null_class
| ~ member(regular(complement(X1)),X1) ),
inference(spm,[status(thm)],[c_0_4600,c_0_4601]) ).
cnf(c_0_4604,plain,
( X1 = null_class
| member(regular(X1),universal_class) ),
inference(spm,[status(thm)],[c_0_4602,c_0_4601]) ).
cnf(c_0_4605,plain,
null_class = complement(universal_class),
inference(spm,[status(thm)],[c_0_4603,c_0_4604]) ).
cnf(c_0_4606,axiom,
( member(X1,X2)
| ~ member(X1,intersection(X2,X3)) ),
i_0_356 ).
cnf(c_0_4607,plain,
( X1 = complement(universal_class)
| member(regular(X1),X1) ),
inference(rw,[status(thm)],[c_0_4601,c_0_4605]) ).
cnf(c_0_4608,plain,
( intersection(X1,X2) = complement(universal_class)
| member(regular(intersection(X1,X2)),X1) ),
inference(spm,[status(thm)],[c_0_4606,c_0_4607]) ).
cnf(c_0_4609,plain,
subclass(intersection(x,cross_product(y,y)),complement(identity_relation)),
i_0_4478 ).
cnf(c_0_4610,plain,
( intersection(X1,cross_product(unordered_pair(X2,X2),universal_class)) != null_class
| ~ member(X2,domain_of(X1)) ),
i_0_333 ).
cnf(c_0_4611,plain,
( intersection(complement(X1),X2) = complement(universal_class)
| ~ member(regular(intersection(complement(X1),X2)),X1) ),
inference(spm,[status(thm)],[c_0_4600,c_0_4608]) ).
cnf(c_0_4612,plain,
( X1 = complement(universal_class)
| member(regular(X1),universal_class) ),
inference(rw,[status(thm)],[c_0_4604,c_0_4605]) ).
cnf(c_0_4613,plain,
( member(X1,complement(identity_relation))
| ~ member(X1,intersection(x,cross_product(y,y))) ),
inference(spm,[status(thm)],[c_0_4598,c_0_4609]) ).
cnf(c_0_4614,plain,
( intersection(X1,cross_product(unordered_pair(X2,X2),universal_class)) != complement(universal_class)
| ~ member(X2,domain_of(X1)) ),
inference(rw,[status(thm)],[c_0_4610,c_0_4605]) ).
cnf(c_0_4615,plain,
intersection(complement(universal_class),X1) = complement(universal_class),
inference(spm,[status(thm)],[c_0_4611,c_0_4612]) ).
cnf(c_0_4616,plain,
( intersection(intersection(x,cross_product(y,y)),X1) = complement(universal_class)
| member(regular(intersection(intersection(x,cross_product(y,y)),X1)),complement(identity_relation)) ),
inference(spm,[status(thm)],[c_0_4613,c_0_4608]) ).
cnf(c_0_4617,axiom,
( member(X1,X2)
| ~ member(X1,intersection(X3,X2)) ),
i_0_357 ).
cnf(c_0_4618,plain,
~ member(X1,domain_of(complement(universal_class))),
inference(spm,[status(thm)],[c_0_4614,c_0_4615]) ).
cnf(c_0_4619,plain,
( intersection(intersection(x,cross_product(y,y)),X1) = complement(universal_class)
| ~ member(regular(intersection(intersection(x,cross_product(y,y)),X1)),identity_relation) ),
inference(spm,[status(thm)],[c_0_4600,c_0_4616]) ).
cnf(c_0_4620,plain,
( intersection(X1,X2) = complement(universal_class)
| member(regular(intersection(X1,X2)),X2) ),
inference(spm,[status(thm)],[c_0_4617,c_0_4607]) ).
cnf(c_0_4621,plain,
domain_of(complement(universal_class)) = complement(universal_class),
inference(spm,[status(thm)],[c_0_4618,c_0_4607]) ).
cnf(c_0_4622,axiom,
( member(X1,intersection(X2,X3))
| ~ member(X1,X2)
| ~ member(X1,X3) ),
i_0_350 ).
cnf(c_0_4623,plain,
intersection(intersection(x,cross_product(y,y)),identity_relation) = complement(universal_class),
inference(spm,[status(thm)],[c_0_4619,c_0_4620]) ).
cnf(c_0_4624,plain,
~ member(X1,complement(universal_class)),
inference(rw,[status(thm)],[c_0_4618,c_0_4621]) ).
cnf(c_0_4625,plain,
( ~ member(X1,intersection(x,cross_product(y,y)))
| ~ member(X1,identity_relation) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_4622,c_0_4623]),c_0_4624]) ).
cnf(c_0_4626,plain,
( ~ member(X1,cross_product(y,y))
| ~ member(X1,identity_relation)
| ~ member(X1,x) ),
inference(spm,[status(thm)],[c_0_4625,c_0_4622]) ).
cnf(c_0_4627,plain,
( intersection(X1,cross_product(y,y)) = complement(universal_class)
| ~ member(regular(intersection(X1,cross_product(y,y))),identity_relation)
| ~ member(regular(intersection(X1,cross_product(y,y))),x) ),
inference(spm,[status(thm)],[c_0_4626,c_0_4620]) ).
cnf(c_0_4628,plain,
( intersection(intersection(X1,X2),X3) = complement(universal_class)
| member(regular(intersection(intersection(X1,X2),X3)),X1) ),
inference(spm,[status(thm)],[c_0_4606,c_0_4608]) ).
cnf(c_0_4629,plain,
null_class != intersection(cross_product(y,y),intersection(x,identity_relation)),
i_0_4586 ).
cnf(c_0_4630,plain,
( intersection(intersection(x,X1),cross_product(y,y)) = complement(universal_class)
| ~ member(regular(intersection(intersection(x,X1),cross_product(y,y))),identity_relation) ),
inference(spm,[status(thm)],[c_0_4627,c_0_4628]) ).
cnf(c_0_4631,plain,
( intersection(intersection(X1,X2),X3) = complement(universal_class)
| member(regular(intersection(intersection(X1,X2),X3)),X2) ),
inference(spm,[status(thm)],[c_0_4617,c_0_4608]) ).
cnf(c_0_4632,plain,
intersection(X1,cross_product(X2,X3)) = intersection(cross_product(X2,X3),X1),
i_0_4513 ).
cnf(c_0_4633,plain,
intersection(cross_product(y,y),intersection(x,identity_relation)) != complement(universal_class),
inference(rw,[status(thm)],[c_0_4629,c_0_4605]) ).
cnf(c_0_4634,plain,
$false,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_4630,c_0_4631]),c_0_4632]),c_0_4633]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : NUM044-1 : TPTP v9.2.1. Bugfixed v2.1.0.
% 0.00/0.11 % 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.14/0.32 % Computer : n014.cluster.edu
% 0.14/0.32 % Model : x86_64 x86_64
% 0.14/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.32 % Memory : 8042.1875MB
% 0.14/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.32 % CPULimit : 300
% 0.14/0.32 % WCLimit : 300
% 0.14/0.32 % DateTime : Tue May 5 00:08:36 EDT 2026
% 0.14/0.32 % CPUTime :
% 0.14/0.33 % start to proof: theBenchmark
% 191.57/138.33 % Version : CSE_E---1.7
% 191.57/138.33 % Problem : theBenchmark.p
% 191.57/138.33 % SZS status Unsatisfiable for theBenchmark.p
% 191.57/138.33 % SZS output start CNFRefutation
% See solution above
% 197.17/143.94 % Total time : 137.849s
%------------------------------------------------------------------------------