%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SET080-7 : TPTP v9.3.1. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n013.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 08:56:14 AM UTC 2026
% Result : Unsatisfiable 0.14s 0.41s
% Output : Proof 0.14s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(subclass_members,axiom,
( member(U,Y)
| ~ member(U,X)
| ~ subclass(X,Y) ),
file('SET004-0.ax',subclass_members) ).
cnf(not_subclass_members1,axiom,
( subclass(X,Y)
| member(not_subclass_element(X,Y),X) ),
file('SET004-0.ax',not_subclass_members1) ).
cnf(not_subclass_members2,axiom,
( subclass(X,Y)
| ~ member(not_subclass_element(X,Y),Y) ),
file('SET004-0.ax',not_subclass_members2) ).
cnf(class_elements_are_sets,axiom,
subclass(X,universal_class),
file('SET004-0.ax',class_elements_are_sets) ).
cnf(equal_implies_subclass1,axiom,
( subclass(X,Y)
| X != Y ),
file('SET004-0.ax',equal_implies_subclass1) ).
cnf(equal_implies_subclass2,axiom,
( subclass(Y,X)
| X != Y ),
file('SET004-0.ax',equal_implies_subclass2) ).
cnf(subclass_implies_equal,axiom,
( X = Y
| ~ subclass(Y,X)
| ~ subclass(X,Y) ),
file('SET004-0.ax',subclass_implies_equal) ).
cnf(unordered_pair_member,axiom,
( U = Y
| U = X
| ~ member(U,unordered_pair(X,Y)) ),
file('SET004-0.ax',unordered_pair_member) ).
cnf(unordered_pair2,axiom,
( member(X,unordered_pair(X,Y))
| ~ member(X,universal_class) ),
file('SET004-0.ax',unordered_pair2) ).
cnf(unordered_pair3,axiom,
( member(Y,unordered_pair(X,Y))
| ~ member(Y,universal_class) ),
file('SET004-0.ax',unordered_pair3) ).
cnf(unordered_pairs_in_universal,axiom,
member(unordered_pair(X,Y),universal_class),
file('SET004-0.ax',unordered_pairs_in_universal) ).
cnf(singleton_set,axiom,
unordered_pair(X,X) = singleton(X),
file('SET004-0.ax',singleton_set) ).
cnf(ordered_pair,axiom,
unordered_pair(singleton(X),unordered_pair(X,singleton(Y))) = ordered_pair(X,Y),
file('SET004-0.ax',ordered_pair) ).
cnf(cartesian_product1,axiom,
( member(U,X)
| ~ member(ordered_pair(U,V),cross_product(X,Y)) ),
file('SET004-0.ax',cartesian_product1) ).
cnf(cartesian_product2,axiom,
( member(V,Y)
| ~ member(ordered_pair(U,V),cross_product(X,Y)) ),
file('SET004-0.ax',cartesian_product2) ).
cnf(cartesian_product3,axiom,
( member(ordered_pair(U,V),cross_product(X,Y))
| ~ member(V,Y)
| ~ member(U,X) ),
file('SET004-0.ax',cartesian_product3) ).
cnf(cartesian_product4,axiom,
( ordered_pair(first(Z),second(Z)) = Z
| ~ member(Z,cross_product(X,Y)) ),
file('SET004-0.ax',cartesian_product4) ).
cnf(element_relation1,axiom,
subclass(element_relation,cross_product(universal_class,universal_class)),
file('SET004-0.ax',element_relation1) ).
cnf(element_relation2,axiom,
( member(X,Y)
| ~ member(ordered_pair(X,Y),element_relation) ),
file('SET004-0.ax',element_relation2) ).
cnf(element_relation3,axiom,
( member(ordered_pair(X,Y),element_relation)
| ~ member(X,Y)
| ~ member(ordered_pair(X,Y),cross_product(universal_class,universal_class)) ),
file('SET004-0.ax',element_relation3) ).
cnf(intersection1,axiom,
( member(Z,X)
| ~ member(Z,intersection(X,Y)) ),
file('SET004-0.ax',intersection1) ).
cnf(intersection2,axiom,
( member(Z,Y)
| ~ member(Z,intersection(X,Y)) ),
file('SET004-0.ax',intersection2) ).
cnf(intersection3,axiom,
( member(Z,intersection(X,Y))
| ~ member(Z,Y)
| ~ member(Z,X) ),
file('SET004-0.ax',intersection3) ).
cnf(complement1,axiom,
( ~ member(Z,X)
| ~ member(Z,complement(X)) ),
file('SET004-0.ax',complement1) ).
cnf(complement2,axiom,
( member(Z,X)
| member(Z,complement(X))
| ~ member(Z,universal_class) ),
file('SET004-0.ax',complement2) ).
cnf(union,axiom,
complement(intersection(complement(X),complement(Y))) = union(X,Y),
file('SET004-0.ax',union) ).
cnf(symmetric_difference,axiom,
intersection(complement(intersection(X,Y)),complement(intersection(complement(X),complement(Y)))) = symmetric_difference(X,Y),
file('SET004-0.ax',symmetric_difference) ).
cnf(restriction1,axiom,
intersection(Xr,cross_product(X,Y)) = restrict(Xr,X,Y),
file('SET004-0.ax',restriction1) ).
cnf(restriction2,axiom,
intersection(cross_product(X,Y),Xr) = restrict(Xr,X,Y),
file('SET004-0.ax',restriction2) ).
cnf(domain1,axiom,
( ~ member(Z,domain_of(X))
| restrict(X,singleton(Z),universal_class) != null_class ),
file('SET004-0.ax',domain1) ).
cnf(domain2,axiom,
( member(Z,domain_of(X))
| restrict(X,singleton(Z),universal_class) = null_class
| ~ member(Z,universal_class) ),
file('SET004-0.ax',domain2) ).
cnf(rotate1,axiom,
subclass(rotate(X),cross_product(cross_product(universal_class,universal_class),universal_class)),
file('SET004-0.ax',rotate1) ).
cnf(rotate2,axiom,
( member(ordered_pair(ordered_pair(V,W),U),X)
| ~ member(ordered_pair(ordered_pair(U,V),W),rotate(X)) ),
file('SET004-0.ax',rotate2) ).
cnf(rotate3,axiom,
( member(ordered_pair(ordered_pair(U,V),W),rotate(X))
| ~ member(ordered_pair(ordered_pair(U,V),W),cross_product(cross_product(universal_class,universal_class),universal_class))
| ~ member(ordered_pair(ordered_pair(V,W),U),X) ),
file('SET004-0.ax',rotate3) ).
cnf(flip1,axiom,
subclass(flip(X),cross_product(cross_product(universal_class,universal_class),universal_class)),
file('SET004-0.ax',flip1) ).
cnf(flip2,axiom,
( member(ordered_pair(ordered_pair(V,U),W),X)
| ~ member(ordered_pair(ordered_pair(U,V),W),flip(X)) ),
file('SET004-0.ax',flip2) ).
cnf(flip3,axiom,
( member(ordered_pair(ordered_pair(U,V),W),flip(X))
| ~ member(ordered_pair(ordered_pair(U,V),W),cross_product(cross_product(universal_class,universal_class),universal_class))
| ~ member(ordered_pair(ordered_pair(V,U),W),X) ),
file('SET004-0.ax',flip3) ).
cnf(inverse,axiom,
domain_of(flip(cross_product(Y,universal_class))) = inverse(Y),
file('SET004-0.ax',inverse) ).
cnf(range_of,axiom,
domain_of(inverse(Z)) = range_of(Z),
file('SET004-0.ax',range_of) ).
cnf(domain,axiom,
first(not_subclass_element(restrict(Z,X,singleton(Y)),null_class)) = domain(Z,X,Y),
file('SET004-0.ax',domain) ).
cnf(range,axiom,
second(not_subclass_element(restrict(Z,singleton(X),Y),null_class)) = range(Z,X,Y),
file('SET004-0.ax',range) ).
cnf(image,axiom,
range_of(restrict(Xr,X,universal_class)) = image(Xr,X),
file('SET004-0.ax',image) ).
cnf(successor,axiom,
union(X,singleton(X)) = successor(X),
file('SET004-0.ax',successor) ).
cnf(successor_relation1,axiom,
subclass(successor_relation,cross_product(universal_class,universal_class)),
file('SET004-0.ax',successor_relation1) ).
cnf(successor_relation2,axiom,
( successor(X) = Y
| ~ member(ordered_pair(X,Y),successor_relation) ),
file('SET004-0.ax',successor_relation2) ).
cnf(successor_relation3,axiom,
( member(ordered_pair(X,Y),successor_relation)
| ~ member(ordered_pair(X,Y),cross_product(universal_class,universal_class))
| successor(X) != Y ),
file('SET004-0.ax',successor_relation3) ).
cnf(inductive1,axiom,
( member(null_class,X)
| ~ inductive(X) ),
file('SET004-0.ax',inductive1) ).
cnf(inductive2,axiom,
( subclass(image(successor_relation,X),X)
| ~ inductive(X) ),
file('SET004-0.ax',inductive2) ).
cnf(inductive3,axiom,
( inductive(X)
| ~ subclass(image(successor_relation,X),X)
| ~ member(null_class,X) ),
file('SET004-0.ax',inductive3) ).
cnf(omega_is_inductive1,axiom,
inductive(omega),
file('SET004-0.ax',omega_is_inductive1) ).
cnf(omega_is_inductive2,axiom,
( subclass(omega,Y)
| ~ inductive(Y) ),
file('SET004-0.ax',omega_is_inductive2) ).
cnf(omega_in_universal,axiom,
member(omega,universal_class),
file('SET004-0.ax',omega_in_universal) ).
cnf(sum_class_definition,axiom,
domain_of(restrict(element_relation,universal_class,X)) = sum_class(X),
file('SET004-0.ax',sum_class_definition) ).
cnf(sum_class2,axiom,
( member(sum_class(X),universal_class)
| ~ member(X,universal_class) ),
file('SET004-0.ax',sum_class2) ).
cnf(power_class_definition,axiom,
complement(image(element_relation,complement(X))) = power_class(X),
file('SET004-0.ax',power_class_definition) ).
cnf(power_class2,axiom,
( member(power_class(U),universal_class)
| ~ member(U,universal_class) ),
file('SET004-0.ax',power_class2) ).
cnf(compose1,axiom,
subclass(compose(Yr,Xr),cross_product(universal_class,universal_class)),
file('SET004-0.ax',compose1) ).
cnf(compose2,axiom,
( member(Z,image(Yr,image(Xr,singleton(Y))))
| ~ member(ordered_pair(Y,Z),compose(Yr,Xr)) ),
file('SET004-0.ax',compose2) ).
cnf(compose3,axiom,
( member(ordered_pair(Y,Z),compose(Yr,Xr))
| ~ member(ordered_pair(Y,Z),cross_product(universal_class,universal_class))
| ~ member(Z,image(Yr,image(Xr,singleton(Y)))) ),
file('SET004-0.ax',compose3) ).
cnf(single_valued_class1,axiom,
( subclass(compose(X,inverse(X)),identity_relation)
| ~ single_valued_class(X) ),
file('SET004-0.ax',single_valued_class1) ).
cnf(single_valued_class2,axiom,
( single_valued_class(X)
| ~ subclass(compose(X,inverse(X)),identity_relation) ),
file('SET004-0.ax',single_valued_class2) ).
cnf(function1,axiom,
( subclass(Xf,cross_product(universal_class,universal_class))
| ~ function(Xf) ),
file('SET004-0.ax',function1) ).
cnf(function2,axiom,
( subclass(compose(Xf,inverse(Xf)),identity_relation)
| ~ function(Xf) ),
file('SET004-0.ax',function2) ).
cnf(function3,axiom,
( function(Xf)
| ~ subclass(compose(Xf,inverse(Xf)),identity_relation)
| ~ subclass(Xf,cross_product(universal_class,universal_class)) ),
file('SET004-0.ax',function3) ).
cnf(replacement,axiom,
( member(image(Xf,X),universal_class)
| ~ member(X,universal_class)
| ~ function(Xf) ),
file('SET004-0.ax',replacement) ).
cnf(regularity1,axiom,
( member(regular(X),X)
| X = null_class ),
file('SET004-0.ax',regularity1) ).
cnf(regularity2,axiom,
( intersection(X,regular(X)) = null_class
| X = null_class ),
file('SET004-0.ax',regularity2) ).
cnf(apply,axiom,
sum_class(image(Xf,singleton(Y))) = apply(Xf,Y),
file('SET004-0.ax',apply) ).
cnf(choice1,axiom,
function(choice),
file('SET004-0.ax',choice1) ).
cnf(choice2,axiom,
( member(apply(choice,Y),Y)
| Y = null_class
| ~ member(Y,universal_class) ),
file('SET004-0.ax',choice2) ).
cnf(one_to_one1,axiom,
( function(Xf)
| ~ one_to_one(Xf) ),
file('SET004-0.ax',one_to_one1) ).
cnf(one_to_one2,axiom,
( function(inverse(Xf))
| ~ one_to_one(Xf) ),
file('SET004-0.ax',one_to_one2) ).
cnf(one_to_one3,axiom,
( one_to_one(Xf)
| ~ function(Xf)
| ~ function(inverse(Xf)) ),
file('SET004-0.ax',one_to_one3) ).
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('SET004-0.ax',subset_relation) ).
cnf(identity_relation,axiom,
intersection(inverse(subset_relation),subset_relation) = identity_relation,
file('SET004-0.ax',identity_relation) ).
cnf(diagonalisation,axiom,
complement(domain_of(intersection(Xr,identity_relation))) = diagonalise(Xr),
file('SET004-0.ax',diagonalisation) ).
cnf(cantor_class,axiom,
intersection(domain_of(X),diagonalise(compose(inverse(element_relation),X))) = cantor(X),
file('SET004-0.ax',cantor_class) ).
cnf(operation1,axiom,
( function(Xf)
| ~ operation(Xf) ),
file('SET004-0.ax',operation1) ).
cnf(operation2,axiom,
( cross_product(domain_of(domain_of(Xf)),domain_of(domain_of(Xf))) = domain_of(Xf)
| ~ operation(Xf) ),
file('SET004-0.ax',operation2) ).
cnf(operation3,axiom,
( subclass(range_of(Xf),domain_of(domain_of(Xf)))
| ~ operation(Xf) ),
file('SET004-0.ax',operation3) ).
cnf(operation4,axiom,
( operation(Xf)
| ~ subclass(range_of(Xf),domain_of(domain_of(Xf)))
| cross_product(domain_of(domain_of(Xf)),domain_of(domain_of(Xf))) != domain_of(Xf)
| ~ function(Xf) ),
file('SET004-0.ax',operation4) ).
cnf(compatible1,axiom,
( function(Xh)
| ~ compatible(Xh,Xf1,Xf2) ),
file('SET004-0.ax',compatible1) ).
cnf(compatible2,axiom,
( domain_of(domain_of(Xf1)) = domain_of(Xh)
| ~ compatible(Xh,Xf1,Xf2) ),
file('SET004-0.ax',compatible2) ).
cnf(compatible3,axiom,
( subclass(range_of(Xh),domain_of(domain_of(Xf2)))
| ~ compatible(Xh,Xf1,Xf2) ),
file('SET004-0.ax',compatible3) ).
cnf(compatible4,axiom,
( compatible(Xh,Xf1,Xf2)
| ~ subclass(range_of(Xh),domain_of(domain_of(Xf2)))
| domain_of(domain_of(Xf1)) != domain_of(Xh)
| ~ function(Xh) ),
file('SET004-0.ax',compatible4) ).
cnf(homomorphism1,axiom,
( operation(Xf1)
| ~ homomorphism(Xh,Xf1,Xf2) ),
file('SET004-0.ax',homomorphism1) ).
cnf(homomorphism2,axiom,
( operation(Xf2)
| ~ homomorphism(Xh,Xf1,Xf2) ),
file('SET004-0.ax',homomorphism2) ).
cnf(homomorphism3,axiom,
( compatible(Xh,Xf1,Xf2)
| ~ homomorphism(Xh,Xf1,Xf2) ),
file('SET004-0.ax',homomorphism3) ).
cnf(homomorphism4,axiom,
( apply(Xf2,ordered_pair(apply(Xh,X),apply(Xh,Y))) = apply(Xh,apply(Xf1,ordered_pair(X,Y)))
| ~ member(ordered_pair(X,Y),domain_of(Xf1))
| ~ homomorphism(Xh,Xf1,Xf2) ),
file('SET004-0.ax',homomorphism4) ).
cnf(homomorphism5,axiom,
( homomorphism(Xh,Xf1,Xf2)
| member(ordered_pair(not_homomorphism1(Xh,Xf1,Xf2),not_homomorphism2(Xh,Xf1,Xf2)),domain_of(Xf1))
| ~ compatible(Xh,Xf1,Xf2)
| ~ operation(Xf2)
| ~ operation(Xf1) ),
file('SET004-0.ax',homomorphism5) ).
cnf(homomorphism6,axiom,
( homomorphism(Xh,Xf1,Xf2)
| apply(Xf2,ordered_pair(apply(Xh,not_homomorphism1(Xh,Xf1,Xf2)),apply(Xh,not_homomorphism2(Xh,Xf1,Xf2)))) != apply(Xh,apply(Xf1,ordered_pair(not_homomorphism1(Xh,Xf1,Xf2),not_homomorphism2(Xh,Xf1,Xf2))))
| ~ compatible(Xh,Xf1,Xf2)
| ~ operation(Xf2)
| ~ operation(Xf1) ),
file('SET004-0.ax',homomorphism6) ).
cnf(corollary_1_to_unordered_pair,axiom,
( member(X,unordered_pair(X,Y))
| ~ member(ordered_pair(X,Y),cross_product(U,V)) ),
file('theBenchmark.p',corollary_1_to_unordered_pair) ).
cnf(corollary_2_to_unordered_pair,axiom,
( member(Y,unordered_pair(X,Y))
| ~ member(ordered_pair(X,Y),cross_product(U,V)) ),
file('theBenchmark.p',corollary_2_to_unordered_pair) ).
cnf(corollary_1_to_cartesian_product,axiom,
( member(U,universal_class)
| ~ member(ordered_pair(U,V),cross_product(X,Y)) ),
file('theBenchmark.p',corollary_1_to_cartesian_product) ).
cnf(corollary_2_to_cartesian_product,axiom,
( member(V,universal_class)
| ~ member(ordered_pair(U,V),cross_product(X,Y)) ),
file('theBenchmark.p',corollary_2_to_cartesian_product) ).
cnf(subclass_is_reflexive,axiom,
subclass(X,X),
file('theBenchmark.p',subclass_is_reflexive) ).
cnf(transitivity_of_subclass,axiom,
( subclass(X,Z)
| ~ subclass(Y,Z)
| ~ subclass(X,Y) ),
file('theBenchmark.p',transitivity_of_subclass) ).
cnf(equality1,axiom,
( member(not_subclass_element(Y,X),Y)
| member(not_subclass_element(X,Y),X)
| X = Y ),
file('theBenchmark.p',equality1) ).
cnf(equality2,axiom,
( member(not_subclass_element(Y,X),Y)
| X = Y
| ~ member(not_subclass_element(X,Y),Y) ),
file('theBenchmark.p',equality2) ).
cnf(equality3,axiom,
( member(not_subclass_element(X,Y),X)
| X = Y
| ~ member(not_subclass_element(Y,X),X) ),
file('theBenchmark.p',equality3) ).
cnf(equality4,axiom,
( X = Y
| ~ member(not_subclass_element(Y,X),X)
| ~ member(not_subclass_element(X,Y),Y) ),
file('theBenchmark.p',equality4) ).
cnf(special_classes_lemma,axiom,
~ member(Y,intersection(complement(X),X)),
file('theBenchmark.p',special_classes_lemma) ).
cnf(existence_of_null_class,axiom,
~ member(Z,null_class),
file('theBenchmark.p',existence_of_null_class) ).
cnf(null_class_is_subclass,axiom,
subclass(null_class,X),
file('theBenchmark.p',null_class_is_subclass) ).
cnf(corollary_of_null_class_is_subclass,axiom,
( X = null_class
| ~ subclass(X,null_class) ),
file('theBenchmark.p',corollary_of_null_class_is_subclass) ).
cnf(null_class_is_unique,axiom,
( member(not_subclass_element(Z,null_class),Z)
| Z = null_class ),
file('theBenchmark.p',null_class_is_unique) ).
cnf(null_class_is_a_set,axiom,
member(null_class,universal_class),
file('theBenchmark.p',null_class_is_a_set) ).
cnf(commutativity_of_unordered_pair,axiom,
unordered_pair(X,Y) = unordered_pair(Y,X),
file('theBenchmark.p',commutativity_of_unordered_pair) ).
cnf(singleton_in_unordered_pair1,axiom,
subclass(singleton(X),unordered_pair(X,Y)),
file('theBenchmark.p',singleton_in_unordered_pair1) ).
cnf(singleton_in_unordered_pair2,axiom,
subclass(singleton(Y),unordered_pair(X,Y)),
file('theBenchmark.p',singleton_in_unordered_pair2) ).
cnf(unordered_pair_equals_singleton1,axiom,
( unordered_pair(X,Y) = singleton(X)
| member(Y,universal_class) ),
file('theBenchmark.p',unordered_pair_equals_singleton1) ).
cnf(unordered_pair_equals_singleton2,axiom,
( unordered_pair(X,Y) = singleton(Y)
| member(X,universal_class) ),
file('theBenchmark.p',unordered_pair_equals_singleton2) ).
cnf(null_unordered_pair,axiom,
( member(Y,universal_class)
| member(X,universal_class)
| unordered_pair(X,Y) = null_class ),
file('theBenchmark.p',null_unordered_pair) ).
cnf(left_cancellation,axiom,
( Y = Z
| ~ member(ordered_pair(Y,Z),cross_product(universal_class,universal_class))
| unordered_pair(X,Y) != unordered_pair(X,Z) ),
file('theBenchmark.p',left_cancellation) ).
cnf(right_cancellation,axiom,
( X = Y
| ~ member(ordered_pair(X,Y),cross_product(universal_class,universal_class))
| unordered_pair(X,Z) != unordered_pair(Y,Z) ),
file('theBenchmark.p',right_cancellation) ).
cnf(corollary_to_unordered_pair_axiom1,axiom,
( unordered_pair(X,Y) != null_class
| ~ member(X,universal_class) ),
file('theBenchmark.p',corollary_to_unordered_pair_axiom1) ).
cnf(corollary_to_unordered_pair_axiom2,axiom,
( unordered_pair(X,Y) != null_class
| ~ member(Y,universal_class) ),
file('theBenchmark.p',corollary_to_unordered_pair_axiom2) ).
cnf(corollary_to_unordered_pair_axiom3,axiom,
( unordered_pair(X,Y) != null_class
| ~ member(ordered_pair(X,Y),cross_product(U,V)) ),
file('theBenchmark.p',corollary_to_unordered_pair_axiom3) ).
cnf(unordered_pair_is_subset,axiom,
( subclass(unordered_pair(X,Y),Z)
| ~ member(Y,Z)
| ~ member(X,Z) ),
file('theBenchmark.p',unordered_pair_is_subset) ).
cnf(singletons_are_sets,axiom,
member(singleton(X),universal_class),
file('theBenchmark.p',singletons_are_sets) ).
cnf(corollary_1_to_singletons_are_sets,axiom,
member(singleton(Y),unordered_pair(X,singleton(Y))),
file('theBenchmark.p',corollary_1_to_singletons_are_sets) ).
cnf(set_in_its_singleton,axiom,
( member(X,singleton(X))
| ~ member(X,universal_class) ),
file('theBenchmark.p',set_in_its_singleton) ).
cnf(corollary_to_set_in_its_singleton,axiom,
( singleton(X) != null_class
| ~ member(X,universal_class) ),
file('theBenchmark.p',corollary_to_set_in_its_singleton) ).
cnf(prove_null_class_in_its_singleton_1,negated_conjecture,
~ member(null_class,singleton(null_class)),
file('theBenchmark.p',prove_null_class_in_its_singleton_1) ).
cnf(equality_1,axiom,
Eq_x_0 = Eq_x_0,
theory(equality,[reflexivity]) ).
cnf(equality_2,axiom,
( Eq_x_1 = Eq_x_0
| Eq_x_0 != Eq_x_1 ),
theory(equality,[symmetry]) ).
cnf(equality_3,axiom,
( Eq_x_0 = Eq_x_2
| Eq_x_1 != Eq_x_2
| Eq_x_0 != Eq_x_1 ),
theory(equality,[transitivity]) ).
cnf(equality_4,axiom,
( not_subclass_element(Eq_x_0,Eq_x_1) = not_subclass_element(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_5,axiom,
( unordered_pair(Eq_x_0,Eq_x_1) = unordered_pair(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_6,axiom,
( singleton(Eq_x_0) = singleton(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_7,axiom,
( ordered_pair(Eq_x_0,Eq_x_1) = ordered_pair(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_8,axiom,
( cross_product(Eq_x_0,Eq_x_1) = cross_product(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_9,axiom,
( first(Eq_x_0) = first(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_10,axiom,
( second(Eq_x_0) = second(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_11,axiom,
( intersection(Eq_x_0,Eq_x_1) = intersection(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_12,axiom,
( complement(Eq_x_0) = complement(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_13,axiom,
( union(Eq_x_0,Eq_x_1) = union(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_14,axiom,
( symmetric_difference(Eq_x_0,Eq_x_1) = symmetric_difference(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_15,axiom,
( restrict(Eq_x_0,Eq_x_1,Eq_x_2) = restrict(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_16,axiom,
( domain_of(Eq_x_0) = domain_of(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_17,axiom,
( rotate(Eq_x_0) = rotate(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_18,axiom,
( flip(Eq_x_0) = flip(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_19,axiom,
( inverse(Eq_x_0) = inverse(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_20,axiom,
( range_of(Eq_x_0) = range_of(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_21,axiom,
( domain(Eq_x_0,Eq_x_1,Eq_x_2) = domain(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_22,axiom,
( range(Eq_x_0,Eq_x_1,Eq_x_2) = range(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_23,axiom,
( image(Eq_x_0,Eq_x_1) = image(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_24,axiom,
( successor(Eq_x_0) = successor(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_25,axiom,
( sum_class(Eq_x_0) = sum_class(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_26,axiom,
( power_class(Eq_x_0) = power_class(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_27,axiom,
( compose(Eq_x_0,Eq_x_1) = compose(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_28,axiom,
( regular(Eq_x_0) = regular(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_29,axiom,
( apply(Eq_x_0,Eq_x_1) = apply(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_30,axiom,
( diagonalise(Eq_x_0) = diagonalise(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_31,axiom,
( cantor(Eq_x_0) = cantor(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_32,axiom,
( not_homomorphism1(Eq_x_0,Eq_x_1,Eq_x_2) = not_homomorphism1(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_33,axiom,
( not_homomorphism2(Eq_x_0,Eq_x_1,Eq_x_2) = not_homomorphism2(Eq_y_0,Eq_y_1,Eq_y_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_34,axiom,
( subclass(Eq_y_0,Eq_y_1)
| ~ subclass(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_35,axiom,
( member(Eq_y_0,Eq_y_1)
| ~ member(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_36,axiom,
( inductive(Eq_y_0)
| ~ inductive(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_37,axiom,
( single_valued_class(Eq_y_0)
| ~ single_valued_class(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_38,axiom,
( function(Eq_y_0)
| ~ function(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_39,axiom,
( one_to_one(Eq_y_0)
| ~ one_to_one(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_40,axiom,
( operation(Eq_y_0)
| ~ operation(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_41,axiom,
( compatible(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ compatible(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_42,axiom,
( homomorphism(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ homomorphism(Eq_x_0,Eq_x_1,Eq_x_2)
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET080-7 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.03 This is a CNF_UNS_RFO_SEQ_NHN problem
% 0.00/0.04 % Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.35 % Computer : n013.cluster.edu
% 0.11/0.35 % Model : x86_64 x86_64
% 0.11/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.35 % Memory : 8046.5625MB
% 0.11/0.35 % OS : Linux 6.8.0-71-generic
% 0.11/0.35 % CPULimit : 300
% 0.11/0.35 % WCLimit : 300
% 0.11/0.35 % DateTime : Sat Sep 19 21:37:35 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.14/0.41 % SZS status Unsatisfiable for theBenchmark
% 0.14/0.41 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------