%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SET024-6 : TPTP v9.2.1. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 05:06:55 PM UTC 2026
% Result : Unsatisfiable 0.27s 1.61s
% Output : CNFRefutation 0.27s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named c_0_91)
% Comments :
%------------------------------------------------------------------------------
cnf(image,axiom,
range_of(restrict(X1,X2,universal_class)) = image(X1,X2),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',image) ).
cnf(range_of,axiom,
domain_of(inverse(X1)) = range_of(X1),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',range_of) ).
cnf(restriction1,axiom,
intersection(X1,cross_product(X2,X3)) = restrict(X1,X2,X3),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',restriction1) ).
cnf(apply,axiom,
sum_class(image(X1,singleton(X2))) = apply(X1,X2),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',apply) ).
cnf(singleton_set,axiom,
unordered_pair(X1,X1) = singleton(X1),
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/benchmark/Axioms/SET004-0.ax',ordered_pair) ).
cnf(power_class_definition,axiom,
complement(image(element_relation,complement(X1))) = power_class(X1),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',power_class_definition) ).
cnf(inverse,axiom,
domain_of(flip(cross_product(X1,universal_class))) = inverse(X1),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',inverse) ).
cnf(successor,axiom,
union(X1,singleton(X1)) = successor(X1),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',successor) ).
cnf(homomorphism6,axiom,
( homomorphism(X3,X1,X2)
| ~ operation(X1)
| ~ operation(X2)
| ~ compatible(X3,X1,X2)
| apply(X2,ordered_pair(apply(X3,not_homomorphism1(X3,X1,X2)),apply(X3,not_homomorphism2(X3,X1,X2)))) != apply(X3,apply(X1,ordered_pair(not_homomorphism1(X3,X1,X2),not_homomorphism2(X3,X1,X2)))) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/Axioms/SET004-0.ax',homomorphism4) ).
cnf(compose3,axiom,
( member(ordered_pair(X4,X1),compose(X2,X3))
| ~ member(X1,image(X2,image(X3,singleton(X4))))
| ~ member(ordered_pair(X4,X1),cross_product(universal_class,universal_class)) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/Axioms/SET004-0.ax',compose2) ).
cnf(choice2,axiom,
( X1 = null_class
| member(apply(choice,X1),X1)
| ~ member(X1,universal_class) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',choice2) ).
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/sandbox2/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/sandbox2/benchmark/Axioms/SET004-0.ax',rotate3) ).
cnf(flip2,axiom,
( member(ordered_pair(ordered_pair(X2,X1),X3),X4)
| ~ member(ordered_pair(ordered_pair(X1,X2),X3),flip(X4)) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/Axioms/SET004-0.ax',rotate2) ).
cnf(power_class2,axiom,
( member(power_class(X1),universal_class)
| ~ member(X1,universal_class) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/Axioms/SET004-0.ax',homomorphism5) ).
cnf(inductive3,axiom,
( inductive(X1)
| ~ member(null_class,X1)
| ~ subclass(image(successor_relation,X1),X1) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/Axioms/SET004-0.ax',cantor_class) ).
cnf(diagonalisation,axiom,
complement(domain_of(intersection(X1,identity_relation))) = diagonalise(X1),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',diagonalisation) ).
cnf(replacement,axiom,
( member(image(X1,X2),universal_class)
| ~ function(X1)
| ~ member(X2,universal_class) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',replacement) ).
cnf(inductive2,axiom,
( subclass(image(successor_relation,X1),X1)
| ~ inductive(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',inductive2) ).
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/sandbox2/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/sandbox2/benchmark/Axioms/SET004-0.ax',successor_relation3) ).
cnf(union,axiom,
complement(intersection(complement(X1),complement(X2))) = union(X1,X2),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',union) ).
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/sandbox2/benchmark/Axioms/SET004-0.ax',element_relation3) ).
cnf(successor_relation2,axiom,
( successor(X1) = X2
| ~ member(ordered_pair(X1,X2),successor_relation) ),
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/benchmark/Axioms/SET004-0.ax',function3) ).
cnf(cartesian_product1,axiom,
( member(X1,X3)
| ~ member(ordered_pair(X1,X2),cross_product(X3,X4)) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/Axioms/SET004-0.ax',cartesian_product2) ).
cnf(single_valued_class2,axiom,
( single_valued_class(X1)
| ~ subclass(compose(X1,inverse(X1)),identity_relation) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/Axioms/SET004-0.ax',element_relation2) ).
cnf(compatible3,axiom,
( subclass(range_of(X1),domain_of(domain_of(X3)))
| ~ compatible(X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',compatible3) ).
cnf(cartesian_product3,axiom,
( member(ordered_pair(X1,X3),cross_product(X2,X4))
| ~ member(X1,X2)
| ~ member(X3,X4) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',cartesian_product3) ).
cnf(cartesian_product4,axiom,
( ordered_pair(first(X1),second(X1)) = X1
| ~ member(X1,cross_product(X2,X3)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',cartesian_product4) ).
cnf(operation3,axiom,
( subclass(range_of(X1),domain_of(domain_of(X1)))
| ~ operation(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',operation3) ).
cnf(function2,axiom,
( subclass(compose(X1,inverse(X1)),identity_relation)
| ~ function(X1) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/Axioms/SET004-0.ax',single_valued_class1) ).
cnf(one_to_one3,axiom,
( one_to_one(X1)
| ~ function(inverse(X1))
| ~ function(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',one_to_one3) ).
cnf(sum_class2,axiom,
( member(sum_class(X1),universal_class)
| ~ member(X1,universal_class) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/Axioms/SET004-0.ax',domain1) ).
cnf(domain2,axiom,
( restrict(X2,singleton(X1),universal_class) = null_class
| member(X1,domain_of(X2))
| ~ member(X1,universal_class) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',domain2) ).
cnf(one_to_one2,axiom,
( function(inverse(X1))
| ~ one_to_one(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',one_to_one2) ).
cnf(identity_relation,axiom,
intersection(inverse(subset_relation),subset_relation) = identity_relation,
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',identity_relation) ).
cnf(restriction2,axiom,
intersection(cross_product(X1,X2),X3) = restrict(X3,X1,X2),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',restriction2) ).
cnf(prove_set_in_its_singleton_2,negated_conjecture,
~ member(x,singleton(x)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_set_in_its_singleton_2) ).
cnf(homomorphism3,axiom,
( compatible(X1,X2,X3)
| ~ homomorphism(X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',homomorphism3) ).
cnf(compatible2,axiom,
( domain_of(domain_of(X2)) = domain_of(X1)
| ~ compatible(X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',compatible2) ).
cnf(homomorphism1,axiom,
( operation(X2)
| ~ homomorphism(X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',homomorphism1) ).
cnf(homomorphism2,axiom,
( operation(X3)
| ~ homomorphism(X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',homomorphism2) ).
cnf(compatible1,axiom,
( function(X1)
| ~ compatible(X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',compatible1) ).
cnf(intersection3,axiom,
( member(X1,intersection(X2,X3))
| ~ member(X1,X2)
| ~ member(X1,X3) ),
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/benchmark/Axioms/SET004-0.ax',rotate1) ).
cnf(not_subclass_members2,axiom,
( subclass(X1,X2)
| ~ member(not_subclass_element(X1,X2),X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',not_subclass_members2) ).
cnf(intersection1,axiom,
( member(X1,X2)
| ~ member(X1,intersection(X2,X3)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',intersection1) ).
cnf(intersection2,axiom,
( member(X1,X3)
| ~ member(X1,intersection(X2,X3)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',intersection2) ).
cnf(unordered_pair_member,axiom,
( X1 = X2
| X1 = X3
| ~ member(X1,unordered_pair(X2,X3)) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/Axioms/SET004-0.ax',operation2) ).
cnf(unordered_pair2,axiom,
( member(X1,unordered_pair(X1,X2))
| ~ member(X1,universal_class) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',unordered_pair2) ).
cnf(unordered_pair3,axiom,
( member(X1,unordered_pair(X2,X1))
| ~ member(X1,universal_class) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',unordered_pair3) ).
cnf(compose1,axiom,
subclass(compose(X1,X2),cross_product(universal_class,universal_class)),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',compose1) ).
cnf(subclass_members,axiom,
( member(X3,X2)
| ~ subclass(X1,X2)
| ~ member(X3,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',subclass_members) ).
cnf(complement2,axiom,
( member(X1,complement(X2))
| member(X1,X2)
| ~ member(X1,universal_class) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',complement2) ).
cnf(complement1,axiom,
( ~ member(X1,complement(X2))
| ~ member(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',complement1) ).
cnf(not_subclass_members1,axiom,
( member(not_subclass_element(X1,X2),X1)
| subclass(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',not_subclass_members1) ).
cnf(subclass_implies_equal,axiom,
( X1 = X2
| ~ subclass(X1,X2)
| ~ subclass(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',subclass_implies_equal) ).
cnf(function1,axiom,
( subclass(X1,cross_product(universal_class,universal_class))
| ~ function(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',function1) ).
cnf(unordered_pairs_in_universal,axiom,
member(unordered_pair(X1,X2),universal_class),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',unordered_pairs_in_universal) ).
cnf(successor_relation1,axiom,
subclass(successor_relation,cross_product(universal_class,universal_class)),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',successor_relation1) ).
cnf(element_relation1,axiom,
subclass(element_relation,cross_product(universal_class,universal_class)),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',element_relation1) ).
cnf(regularity1,axiom,
( X1 = null_class
| member(regular(X1),X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',regularity1) ).
cnf(regularity2,axiom,
( X1 = null_class
| intersection(X1,regular(X1)) = null_class ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',regularity2) ).
cnf(inductive1,axiom,
( member(null_class,X1)
| ~ inductive(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',inductive1) ).
cnf(omega_is_inductive2,axiom,
( subclass(omega,X1)
| ~ inductive(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',omega_is_inductive2) ).
cnf(equal_implies_subclass1,axiom,
( subclass(X1,X2)
| X1 != X2 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',equal_implies_subclass1) ).
cnf(equal_implies_subclass2,axiom,
( subclass(X2,X1)
| X1 != X2 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',equal_implies_subclass2) ).
cnf(class_elements_are_sets,axiom,
subclass(X1,universal_class),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',class_elements_are_sets) ).
cnf(operation1,axiom,
( function(X1)
| ~ operation(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',operation1) ).
cnf(one_to_one1,axiom,
( function(X1)
| ~ one_to_one(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',one_to_one1) ).
cnf(prove_set_in_its_singleton_1,negated_conjecture,
member(x,universal_class),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_set_in_its_singleton_1) ).
cnf(omega_in_universal,axiom,
member(omega,universal_class),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',omega_in_universal) ).
cnf(choice1,axiom,
function(choice),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',choice1) ).
cnf(omega_is_inductive1,axiom,
inductive(omega),
file('/export/starexec/sandbox2/benchmark/Axioms/SET004-0.ax',omega_is_inductive1) ).
cnf(i_0_90,axiom,
range_of(restrict(X1,X2,universal_class)) = image(X1,X2),
image ).
cnf(i_0_91,axiom,
domain_of(inverse(X1)) = range_of(X1),
range_of ).
cnf(i_0_92,axiom,
intersection(X1,cross_product(X2,X3)) = restrict(X1,X2,X3),
restriction1 ).
cnf(i_0_93,axiom,
sum_class(image(X1,singleton(X2))) = apply(X1,X2),
apply ).
cnf(i_0_94,axiom,
unordered_pair(X1,X1) = singleton(X1),
singleton_set ).
cnf(i_0_95,axiom,
domain_of(restrict(element_relation,universal_class,X1)) = sum_class(X1),
sum_class_definition ).
cnf(i_0_96,axiom,
unordered_pair(singleton(X1),unordered_pair(X1,singleton(X2))) = ordered_pair(X1,X2),
ordered_pair ).
cnf(i_0_97,axiom,
complement(image(element_relation,complement(X1))) = power_class(X1),
power_class_definition ).
cnf(i_0_98,plain,
domain_of(inverse(intersection(X1,cross_product(X2,universal_class)))) = image(X1,X2),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_90,c_0_91]),c_0_92]) ).
cnf(i_0_99,axiom,
domain_of(flip(cross_product(X1,universal_class))) = inverse(X1),
inverse ).
cnf(i_0_100,axiom,
union(X1,singleton(X1)) = successor(X1),
successor ).
cnf(i_0_101,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_102,plain,
sum_class(image(X1,unordered_pair(X2,X2))) = apply(X1,X2),
inference(rw,[status(thm)],[i_0_93,c_0_94]) ).
cnf(i_0_103,plain,
domain_of(intersection(element_relation,cross_product(universal_class,X1))) = sum_class(X1),
inference(rw,[status(thm)],[i_0_95,c_0_92]) ).
cnf(i_0_104,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_96,c_0_94]),c_0_94]) ).
cnf(i_0_105,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_106,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_107,axiom,
( member(X2,image(X3,image(X4,singleton(X1))))
| ~ member(ordered_pair(X1,X2),compose(X3,X4)) ),
compose2 ).
cnf(i_0_108,axiom,
( X1 = null_class
| member(apply(choice,X1),X1)
| ~ member(X1,universal_class) ),
choice2 ).
cnf(i_0_109,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_110,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_111,axiom,
( member(ordered_pair(ordered_pair(X2,X1),X3),X4)
| ~ member(ordered_pair(ordered_pair(X1,X2),X3),flip(X4)) ),
flip2 ).
cnf(i_0_112,axiom,
( member(ordered_pair(ordered_pair(X2,X3),X1),X4)
| ~ member(ordered_pair(ordered_pair(X1,X2),X3),rotate(X4)) ),
rotate2 ).
cnf(i_0_113,axiom,
( member(power_class(X1),universal_class)
| ~ member(X1,universal_class) ),
power_class2 ).
cnf(i_0_114,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_97,c_0_98]),c_0_99]) ).
cnf(i_0_115,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_116,axiom,
( inductive(X1)
| ~ member(null_class,X1)
| ~ subclass(image(successor_relation,X1),X1) ),
inductive3 ).
cnf(i_0_117,axiom,
intersection(domain_of(X1),diagonalise(compose(inverse(element_relation),X1))) = cantor(X1),
cantor_class ).
cnf(i_0_118,axiom,
complement(domain_of(intersection(X1,identity_relation))) = diagonalise(X1),
diagonalisation ).
cnf(i_0_119,axiom,
( member(image(X1,X2),universal_class)
| ~ function(X1)
| ~ member(X2,universal_class) ),
replacement ).
cnf(i_0_120,axiom,
( subclass(image(successor_relation,X1),X1)
| ~ inductive(X1) ),
inductive2 ).
cnf(i_0_121,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_122,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_123,plain,
union(X1,unordered_pair(X1,X1)) = successor(X1),
inference(rw,[status(thm)],[i_0_100,c_0_94]) ).
cnf(i_0_124,axiom,
complement(intersection(complement(X1),complement(X2))) = union(X1,X2),
union ).
cnf(i_0_125,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_126,axiom,
( successor(X1) = X2
| ~ member(ordered_pair(X1,X2),successor_relation) ),
successor_relation2 ).
cnf(i_0_127,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_128,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_129,axiom,
( function(X1)
| ~ subclass(X1,cross_product(universal_class,universal_class))
| ~ subclass(compose(X1,inverse(X1)),identity_relation) ),
function3 ).
cnf(i_0_130,axiom,
( member(X1,X3)
| ~ member(ordered_pair(X1,X2),cross_product(X3,X4)) ),
cartesian_product1 ).
cnf(i_0_131,axiom,
( member(X2,X4)
| ~ member(ordered_pair(X1,X2),cross_product(X3,X4)) ),
cartesian_product2 ).
cnf(i_0_132,axiom,
( single_valued_class(X1)
| ~ subclass(compose(X1,inverse(X1)),identity_relation) ),
single_valued_class2 ).
cnf(i_0_133,axiom,
( member(X1,X2)
| ~ member(ordered_pair(X1,X2),element_relation) ),
element_relation2 ).
cnf(i_0_134,axiom,
( subclass(range_of(X1),domain_of(domain_of(X3)))
| ~ compatible(X1,X2,X3) ),
compatible3 ).
cnf(i_0_135,axiom,
( member(ordered_pair(X1,X3),cross_product(X2,X4))
| ~ member(X1,X2)
| ~ member(X3,X4) ),
cartesian_product3 ).
cnf(i_0_136,axiom,
( ordered_pair(first(X1),second(X1)) = X1
| ~ member(X1,cross_product(X2,X3)) ),
cartesian_product4 ).
cnf(i_0_137,axiom,
( subclass(range_of(X1),domain_of(domain_of(X1)))
| ~ operation(X1) ),
operation3 ).
cnf(i_0_138,axiom,
( subclass(compose(X1,inverse(X1)),identity_relation)
| ~ function(X1) ),
function2 ).
cnf(i_0_139,axiom,
( subclass(compose(X1,inverse(X1)),identity_relation)
| ~ single_valued_class(X1) ),
single_valued_class1 ).
cnf(i_0_140,axiom,
( one_to_one(X1)
| ~ function(inverse(X1))
| ~ function(X1) ),
one_to_one3 ).
cnf(i_0_141,axiom,
( member(sum_class(X1),universal_class)
| ~ member(X1,universal_class) ),
sum_class2 ).
cnf(i_0_142,axiom,
( restrict(X1,singleton(X2),universal_class) != null_class
| ~ member(X2,domain_of(X1)) ),
domain1 ).
cnf(i_0_143,axiom,
( restrict(X2,singleton(X1),universal_class) = null_class
| member(X1,domain_of(X2))
| ~ member(X1,universal_class) ),
domain2 ).
cnf(i_0_144,axiom,
( function(inverse(X1))
| ~ one_to_one(X1) ),
one_to_one2 ).
cnf(i_0_145,axiom,
intersection(inverse(subset_relation),subset_relation) = identity_relation,
identity_relation ).
cnf(i_0_146,axiom,
intersection(cross_product(X1,X2),X3) = restrict(X3,X1,X2),
restriction2 ).
cnf(i_0_147,negated_conjecture,
~ member(x,singleton(x)),
prove_set_in_its_singleton_2 ).
cnf(i_0_148,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_101,c_0_102]),c_0_102]),c_0_102]),c_0_102]),c_0_102]),c_0_98]),c_0_98]),c_0_98]),c_0_98]),c_0_98]),c_0_98]),c_0_98]),c_0_98]),c_0_99]),c_0_99]),c_0_99]),c_0_99]),c_0_99]),c_0_99]),c_0_99]),c_0_99]),c_0_103]),c_0_103]),c_0_103]),c_0_103]),c_0_103]),c_0_103]),c_0_103]),c_0_103]),c_0_104]),c_0_104]),c_0_104]),c_0_104]),c_0_104]),c_0_104]),
[final] ).
cnf(i_0_149,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_105,c_0_102]),c_0_102]),c_0_102]),c_0_102]),c_0_102]),c_0_98]),c_0_98]),c_0_98]),c_0_98]),c_0_98]),c_0_98]),c_0_98]),c_0_98]),c_0_99]),c_0_99]),c_0_99]),c_0_99]),c_0_99]),c_0_99]),c_0_99]),c_0_99]),c_0_103]),c_0_103]),c_0_103]),c_0_103]),c_0_103]),c_0_103]),c_0_103]),c_0_103]),c_0_104]),c_0_104]),c_0_104]),c_0_104]),c_0_104]),c_0_104]),c_0_104]),
[final] ).
cnf(i_0_150,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_106,c_0_94]),c_0_98]),c_0_98]),c_0_99]),c_0_99]),c_0_104]),c_0_104]),
[final] ).
cnf(i_0_151,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_107,c_0_94]),c_0_98]),c_0_98]),c_0_99]),c_0_99]),c_0_104]),
[final] ).
cnf(i_0_152,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_108,c_0_102]),c_0_98]),c_0_99]),c_0_103]),
[final] ).
cnf(i_0_153,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_109,c_0_104]),c_0_104]),c_0_104]),c_0_104]),c_0_104]),c_0_104]),
[final] ).
cnf(i_0_154,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_110,c_0_104]),c_0_104]),c_0_104]),c_0_104]),c_0_104]),c_0_104]),
[final] ).
cnf(i_0_155,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_111,c_0_104]),c_0_104]),c_0_104]),c_0_104]),
[final] ).
cnf(i_0_156,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_112,c_0_104]),c_0_104]),c_0_104]),c_0_104]),
[final] ).
cnf(i_0_157,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_113,c_0_114]),
[final] ).
cnf(i_0_158,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_115,c_0_104]),
[final] ).
cnf(i_0_159,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_116,c_0_98]),c_0_99]),
[final] ).
cnf(i_0_160,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_117,c_0_118]),c_0_99]),
[final] ).
cnf(i_0_161,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_119,c_0_98]),c_0_99]),
[final] ).
cnf(i_0_162,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_120,c_0_98]),c_0_99]),
[final] ).
cnf(i_0_163,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_121,c_0_99]),
[final] ).
cnf(i_0_164,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_122,c_0_123]),c_0_124]),c_0_104]),c_0_104]),
[final] ).
cnf(i_0_165,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_125,c_0_104]),c_0_104]),
[final] ).
cnf(i_0_166,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_126,c_0_123]),c_0_124]),c_0_104]),
[final] ).
cnf(i_0_167,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_127,c_0_91]),c_0_99]),
[final] ).
cnf(i_0_168,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_128,c_0_91]),c_0_99]),
[final] ).
cnf(i_0_169,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_129,c_0_99]),
[final] ).
cnf(i_0_170,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_130,c_0_104]),
[final] ).
cnf(i_0_171,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_131,c_0_104]),
[final] ).
cnf(i_0_172,plain,
( single_valued_class(X1)
| ~ subclass(compose(X1,domain_of(flip(cross_product(X1,universal_class)))),identity_relation) ),
inference(rw,[status(thm)],[i_0_132,c_0_99]),
[final] ).
cnf(i_0_173,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_133,c_0_104]),
[final] ).
cnf(i_0_174,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_134,c_0_91]),c_0_99]),
[final] ).
cnf(i_0_175,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_135,c_0_104]),
[final] ).
cnf(i_0_176,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_136,c_0_104]),
[final] ).
cnf(i_0_177,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_137,c_0_91]),c_0_99]),
[final] ).
cnf(i_0_178,plain,
( subclass(compose(X1,domain_of(flip(cross_product(X1,universal_class)))),identity_relation)
| ~ function(X1) ),
inference(rw,[status(thm)],[i_0_138,c_0_99]),
[final] ).
cnf(i_0_179,plain,
( subclass(compose(X1,domain_of(flip(cross_product(X1,universal_class)))),identity_relation)
| ~ single_valued_class(X1) ),
inference(rw,[status(thm)],[i_0_139,c_0_99]),
[final] ).
cnf(i_0_180,plain,
( one_to_one(X1)
| ~ function(X1)
| ~ function(domain_of(flip(cross_product(X1,universal_class)))) ),
inference(rw,[status(thm)],[i_0_140,c_0_99]),
[final] ).
cnf(i_0_181,plain,
( member(domain_of(intersection(element_relation,cross_product(universal_class,X1))),universal_class)
| ~ member(X1,universal_class) ),
inference(rw,[status(thm)],[i_0_141,c_0_103]),
[final] ).
cnf(i_0_182,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_142,c_0_94]),c_0_92]),
[final] ).
cnf(i_0_183,axiom,
( compatible(X1,X2,X3)
| ~ homomorphism(X1,X2,X3) ),
homomorphism3,
[final] ).
cnf(i_0_184,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_143,c_0_94]),c_0_92]),
[final] ).
cnf(i_0_185,plain,
( function(domain_of(flip(cross_product(X1,universal_class))))
| ~ one_to_one(X1) ),
inference(rw,[status(thm)],[i_0_144,c_0_99]),
[final] ).
cnf(i_0_186,plain,
intersection(domain_of(flip(cross_product(subset_relation,universal_class))),subset_relation) = identity_relation,
inference(rw,[status(thm)],[i_0_145,c_0_99]),
[final] ).
cnf(i_0_187,axiom,
( domain_of(domain_of(X2)) = domain_of(X1)
| ~ compatible(X1,X2,X3) ),
compatible2,
[final] ).
cnf(i_0_188,axiom,
( operation(X2)
| ~ homomorphism(X1,X2,X3) ),
homomorphism1,
[final] ).
cnf(i_0_189,axiom,
( operation(X3)
| ~ homomorphism(X1,X2,X3) ),
homomorphism2,
[final] ).
cnf(i_0_190,axiom,
( function(X1)
| ~ compatible(X1,X2,X3) ),
compatible1,
[final] ).
cnf(i_0_191,axiom,
( member(X1,intersection(X2,X3))
| ~ member(X1,X2)
| ~ member(X1,X3) ),
intersection3,
[final] ).
cnf(i_0_192,axiom,
subclass(flip(X1),cross_product(cross_product(universal_class,universal_class),universal_class)),
flip1,
[final] ).
cnf(i_0_193,axiom,
subclass(rotate(X1),cross_product(cross_product(universal_class,universal_class),universal_class)),
rotate1,
[final] ).
cnf(i_0_194,plain,
intersection(cross_product(X1,X2),X3) = intersection(X3,cross_product(X1,X2)),
inference(rw,[status(thm)],[i_0_146,c_0_92]),
[final] ).
cnf(i_0_195,axiom,
( subclass(X1,X2)
| ~ member(not_subclass_element(X1,X2),X2) ),
not_subclass_members2,
[final] ).
cnf(i_0_196,axiom,
( member(X1,X2)
| ~ member(X1,intersection(X2,X3)) ),
intersection1,
[final] ).
cnf(i_0_197,axiom,
( member(X1,X3)
| ~ member(X1,intersection(X2,X3)) ),
intersection2,
[final] ).
cnf(i_0_198,axiom,
( X1 = X2
| X1 = X3
| ~ member(X1,unordered_pair(X2,X3)) ),
unordered_pair_member,
[final] ).
cnf(i_0_199,axiom,
( cross_product(domain_of(domain_of(X1)),domain_of(domain_of(X1))) = domain_of(X1)
| ~ operation(X1) ),
operation2,
[final] ).
cnf(i_0_200,axiom,
( member(X1,unordered_pair(X1,X2))
| ~ member(X1,universal_class) ),
unordered_pair2,
[final] ).
cnf(i_0_201,axiom,
( member(X1,unordered_pair(X2,X1))
| ~ member(X1,universal_class) ),
unordered_pair3,
[final] ).
cnf(i_0_202,axiom,
subclass(compose(X1,X2),cross_product(universal_class,universal_class)),
compose1,
[final] ).
cnf(i_0_203,axiom,
( member(X3,X2)
| ~ subclass(X1,X2)
| ~ member(X3,X1) ),
subclass_members,
[final] ).
cnf(i_0_204,axiom,
( member(X1,complement(X2))
| member(X1,X2)
| ~ member(X1,universal_class) ),
complement2,
[final] ).
cnf(i_0_205,axiom,
( ~ member(X1,complement(X2))
| ~ member(X1,X2) ),
complement1,
[final] ).
cnf(i_0_206,axiom,
( member(not_subclass_element(X1,X2),X1)
| subclass(X1,X2) ),
not_subclass_members1,
[final] ).
cnf(i_0_207,negated_conjecture,
~ member(x,unordered_pair(x,x)),
inference(rw,[status(thm)],[i_0_147,c_0_94]),
[final] ).
cnf(i_0_208,axiom,
( X1 = X2
| ~ subclass(X1,X2)
| ~ subclass(X2,X1) ),
subclass_implies_equal,
[final] ).
cnf(i_0_209,axiom,
( subclass(X1,cross_product(universal_class,universal_class))
| ~ function(X1) ),
function1,
[final] ).
cnf(i_0_210,axiom,
member(unordered_pair(X1,X2),universal_class),
unordered_pairs_in_universal,
[final] ).
cnf(i_0_211,axiom,
subclass(successor_relation,cross_product(universal_class,universal_class)),
successor_relation1,
[final] ).
cnf(i_0_212,axiom,
subclass(element_relation,cross_product(universal_class,universal_class)),
element_relation1,
[final] ).
cnf(i_0_213,axiom,
( X1 = null_class
| member(regular(X1),X1) ),
regularity1,
[final] ).
cnf(i_0_214,axiom,
( X1 = null_class
| intersection(X1,regular(X1)) = null_class ),
regularity2,
[final] ).
cnf(i_0_215,axiom,
( member(null_class,X1)
| ~ inductive(X1) ),
inductive1,
[final] ).
cnf(i_0_216,axiom,
( subclass(omega,X1)
| ~ inductive(X1) ),
omega_is_inductive2,
[final] ).
cnf(i_0_217,axiom,
( subclass(X1,X2)
| X1 != X2 ),
equal_implies_subclass1,
[final] ).
cnf(i_0_218,axiom,
( subclass(X2,X1)
| X1 != X2 ),
equal_implies_subclass2,
[final] ).
cnf(i_0_219,axiom,
subclass(X1,universal_class),
class_elements_are_sets,
[final] ).
cnf(i_0_220,axiom,
( function(X1)
| ~ operation(X1) ),
operation1,
[final] ).
cnf(i_0_221,axiom,
( function(X1)
| ~ one_to_one(X1) ),
one_to_one1,
[final] ).
cnf(i_0_222,negated_conjecture,
member(x,universal_class),
prove_set_in_its_singleton_1,
[final] ).
cnf(i_0_223,axiom,
member(omega,universal_class),
omega_in_universal,
[final] ).
cnf(i_0_224,axiom,
function(choice),
choice1,
[final] ).
cnf(i_0_225,axiom,
inductive(omega),
omega_is_inductive1,
[final] ).
cnf(i_0_226,axiom,
X1 = X1 ).
cnf(i_0_227,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_228,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_229,axiom,
( X1 != X2
| domain_of(X1) = domain_of(X2) ) ).
cnf(i_0_230,axiom,
( X1 != X2
| complement(X1) = complement(X2) ) ).
cnf(i_0_231,axiom,
( X1 != X2
| cantor(X1) = cantor(X2) ) ).
cnf(i_0_232,axiom,
( X1 != X2
| intersection(X1,X3) = intersection(X2,X3) ) ).
cnf(i_0_233,axiom,
( X1 != X2
| intersection(X3,X1) = intersection(X3,X2) ) ).
cnf(i_0_234,axiom,
( X1 != X2
| cross_product(X1,X3) = cross_product(X2,X3) ) ).
cnf(i_0_235,axiom,
( X1 != X2
| cross_product(X3,X1) = cross_product(X3,X2) ) ).
cnf(i_0_236,axiom,
( X1 != X2
| unordered_pair(X1,X3) = unordered_pair(X2,X3) ) ).
cnf(i_0_237,axiom,
( X1 != X2
| unordered_pair(X3,X1) = unordered_pair(X3,X2) ) ).
cnf(i_0_238,axiom,
( X1 != X2
| ~ homomorphism(X1,X3,X4)
| homomorphism(X2,X3,X4) ) ).
cnf(i_0_239,axiom,
( X1 != X2
| ~ homomorphism(X3,X1,X4)
| homomorphism(X3,X2,X4) ) ).
cnf(i_0_240,axiom,
( X1 != X2
| ~ homomorphism(X3,X4,X1)
| homomorphism(X3,X4,X2) ) ).
cnf(i_0_241,axiom,
( X1 != X2
| ~ operation(X1)
| operation(X2) ) ).
cnf(i_0_242,axiom,
( X1 != X2
| ~ compatible(X1,X3,X4)
| compatible(X2,X3,X4) ) ).
cnf(i_0_243,axiom,
( X1 != X2
| ~ compatible(X3,X1,X4)
| compatible(X3,X2,X4) ) ).
cnf(i_0_244,axiom,
( X1 != X2
| ~ compatible(X3,X4,X1)
| compatible(X3,X4,X2) ) ).
cnf(i_0_245,axiom,
( X1 != X2
| ~ member(X1,X3)
| member(X2,X3) ) ).
cnf(i_0_246,axiom,
( X1 != X2
| ~ member(X3,X1)
| member(X3,X2) ) ).
cnf(i_0_247,axiom,
( X1 != X2
| ~ inductive(X1)
| inductive(X2) ) ).
cnf(i_0_248,axiom,
( X1 != X2
| ~ subclass(X1,X3)
| subclass(X2,X3) ) ).
cnf(i_0_249,axiom,
( X1 != X2
| ~ subclass(X3,X1)
| subclass(X3,X2) ) ).
cnf(i_0_250,axiom,
( X1 != X2
| ~ function(X1)
| function(X2) ) ).
cnf(i_0_251,axiom,
( X1 != X2
| ~ single_valued_class(X1)
| single_valued_class(X2) ) ).
cnf(i_0_252,axiom,
( X1 != X2
| ~ one_to_one(X1)
| one_to_one(X2) ) ).
cnf(i_0_226_001,axiom,
X1 = X1 ).
cnf(i_0_227_002,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_228_003,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_229_004,axiom,
( X1 != X2
| domain_of(X1) = domain_of(X2) ) ).
cnf(i_0_230_005,axiom,
( X1 != X2
| complement(X1) = complement(X2) ) ).
cnf(i_0_231_006,axiom,
( X1 != X2
| cantor(X1) = cantor(X2) ) ).
cnf(i_0_232_007,axiom,
( X1 != X2
| intersection(X1,X3) = intersection(X2,X3) ) ).
cnf(i_0_233_008,axiom,
( X1 != X2
| intersection(X3,X1) = intersection(X3,X2) ) ).
cnf(i_0_234_009,axiom,
( X1 != X2
| cross_product(X1,X3) = cross_product(X2,X3) ) ).
cnf(i_0_235_010,axiom,
( X1 != X2
| cross_product(X3,X1) = cross_product(X3,X2) ) ).
cnf(i_0_236_011,axiom,
( X1 != X2
| unordered_pair(X1,X3) = unordered_pair(X2,X3) ) ).
cnf(i_0_237_012,axiom,
( X1 != X2
| unordered_pair(X3,X1) = unordered_pair(X3,X2) ) ).
cnf(i_0_238_013,axiom,
( X1 != X2
| ~ homomorphism(X1,X3,X4)
| homomorphism(X2,X3,X4) ) ).
cnf(i_0_239_014,axiom,
( X1 != X2
| ~ homomorphism(X3,X1,X4)
| homomorphism(X3,X2,X4) ) ).
cnf(i_0_240_015,axiom,
( X1 != X2
| ~ homomorphism(X3,X4,X1)
| homomorphism(X3,X4,X2) ) ).
cnf(i_0_241_016,axiom,
( X1 != X2
| ~ operation(X1)
| operation(X2) ) ).
cnf(i_0_242_017,axiom,
( X1 != X2
| ~ compatible(X1,X3,X4)
| compatible(X2,X3,X4) ) ).
cnf(i_0_243_018,axiom,
( X1 != X2
| ~ compatible(X3,X1,X4)
| compatible(X3,X2,X4) ) ).
cnf(i_0_244_019,axiom,
( X1 != X2
| ~ compatible(X3,X4,X1)
| compatible(X3,X4,X2) ) ).
cnf(i_0_245_020,axiom,
( X1 != X2
| ~ member(X1,X3)
| member(X2,X3) ) ).
cnf(i_0_246_021,axiom,
( X1 != X2
| ~ member(X3,X1)
| member(X3,X2) ) ).
cnf(i_0_247_022,axiom,
( X1 != X2
| ~ inductive(X1)
| inductive(X2) ) ).
cnf(i_0_248_023,axiom,
( X1 != X2
| ~ subclass(X1,X3)
| subclass(X2,X3) ) ).
cnf(i_0_249_024,axiom,
( X1 != X2
| ~ subclass(X3,X1)
| subclass(X3,X2) ) ).
cnf(i_0_250_025,axiom,
( X1 != X2
| ~ function(X1)
| function(X2) ) ).
cnf(i_0_251_026,axiom,
( X1 != X2
| ~ single_valued_class(X1)
| single_valued_class(X2) ) ).
cnf(i_0_252_027,axiom,
( X1 != X2
| ~ one_to_one(X1)
| one_to_one(X2) ) ).
cnf(i_0_253,plain,
( ~ member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(complement(intersection(complement(X1),complement(unordered_pair(X1,X1)))),complement(intersection(complement(X1),complement(unordered_pair(X1,X1))))))),cross_product(universal_class,universal_class))
| member(unordered_pair(unordered_pair(X1,X1),unordered_pair(X1,unordered_pair(complement(intersection(complement(X1),complement(unordered_pair(X1,X1)))),complement(intersection(complement(X1),complement(unordered_pair(X1,X1))))))),successor_relation) ),
inference(equality_inference,[],[164]) ).
cnf(i_0_254,plain,
( ~ function(domain_of(X1))
| compatible(domain_of(X1),X1,X2)
| ~ subclass(domain_of(domain_of(flip(cross_product(domain_of(X1),universal_class)))),domain_of(domain_of(X2))) ),
inference(equality_inference,[],[168]) ).
cnf(i_0_255,plain,
subclass(X1,X1),
inference(equality_inference,[],[217]) ).
cnf(i_0_256,plain,
subclass(X1,X1),
inference(equality_inference,[],[218]) ).
cnf(i_0_257,plain,
$false,
inference(scs_inference,[],[i_0_207,i_0_222,i_0_200]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : SET024-6 : TPTP v9.2.1. Bugfixed v2.1.0.
% 0.00/0.11 % Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.14/0.32 % Computer : n011.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 02:04:47 EDT 2026
% 0.14/0.32 % CPUTime :
% 0.14/0.33 % start to proof: theBenchmark
% 0.27/1.61 % Version : CSE_E---1.7
% 0.27/1.61 % Problem : theBenchmark.p
% 0.27/1.61 % SZS status Unsatisfiable for theBenchmark.p
% 0.27/1.61 % SZS output start CNFRefutation
% See solution above
% 0.27/1.63 % Total time : 1.270s
%------------------------------------------------------------------------------