%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : NUM042-1 : TPTP v9.3.1. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n011.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:51:41 AM UTC 2026
% Result : Unsatisfiable 165.17s 165.49s
% Output : Proof 165.55s
% 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(compose_class_definition1,axiom,
subclass(compose_class(X),cross_product(universal_class,universal_class)),
file('SET004-1.ax',compose_class_definition1) ).
cnf(compose_class_definition2,axiom,
( compose(X,Y) = Z
| ~ member(ordered_pair(Y,Z),compose_class(X)) ),
file('SET004-1.ax',compose_class_definition2) ).
cnf(compose_class_definition3,axiom,
( member(ordered_pair(Y,Z),compose_class(X))
| compose(X,Y) != Z
| ~ member(ordered_pair(Y,Z),cross_product(universal_class,universal_class)) ),
file('SET004-1.ax',compose_class_definition3) ).
cnf(definition_of_composition_function1,axiom,
subclass(composition_function,cross_product(universal_class,cross_product(universal_class,universal_class))),
file('SET004-1.ax',definition_of_composition_function1) ).
cnf(definition_of_composition_function2,axiom,
( compose(X,Y) = Z
| ~ member(ordered_pair(X,ordered_pair(Y,Z)),composition_function) ),
file('SET004-1.ax',definition_of_composition_function2) ).
cnf(definition_of_composition_function3,axiom,
( member(ordered_pair(X,ordered_pair(Y,compose(X,Y))),composition_function)
| ~ member(ordered_pair(X,Y),cross_product(universal_class,universal_class)) ),
file('SET004-1.ax',definition_of_composition_function3) ).
cnf(definition_of_domain_relation1,axiom,
subclass(domain_relation,cross_product(universal_class,universal_class)),
file('SET004-1.ax',definition_of_domain_relation1) ).
cnf(definition_of_domain_relation2,axiom,
( domain_of(X) = Y
| ~ member(ordered_pair(X,Y),domain_relation) ),
file('SET004-1.ax',definition_of_domain_relation2) ).
cnf(definition_of_domain_relation3,axiom,
( member(ordered_pair(X,domain_of(X)),domain_relation)
| ~ member(X,universal_class) ),
file('SET004-1.ax',definition_of_domain_relation3) ).
cnf(single_valued_term_defn1,axiom,
first(not_subclass_element(compose(X,inverse(X)),identity_relation)) = single_valued1(X),
file('SET004-1.ax',single_valued_term_defn1) ).
cnf(single_valued_term_defn2,axiom,
second(not_subclass_element(compose(X,inverse(X)),identity_relation)) = single_valued2(X),
file('SET004-1.ax',single_valued_term_defn2) ).
cnf(single_valued_term_defn3,axiom,
domain(X,image(inverse(X),singleton(single_valued1(X))),single_valued2(X)) = single_valued3(X),
file('SET004-1.ax',single_valued_term_defn3) ).
cnf(compose_can_define_singleton,axiom,
intersection(complement(compose(element_relation,complement(identity_relation))),element_relation) = singleton_relation,
file('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('SET004-1.ax',application_function_defn1) ).
cnf(application_function_defn2,axiom,
( member(Y,domain_of(X))
| ~ member(ordered_pair(X,ordered_pair(Y,Z)),application_function) ),
file('SET004-1.ax',application_function_defn2) ).
cnf(application_function_defn3,axiom,
( apply(X,Y) = Z
| ~ member(ordered_pair(X,ordered_pair(Y,Z)),application_function) ),
file('SET004-1.ax',application_function_defn3) ).
cnf(application_function_defn4,axiom,
( member(ordered_pair(X,ordered_pair(Y,apply(X,Y))),application_function)
| ~ member(Y,domain_of(X))
| ~ member(ordered_pair(X,ordered_pair(Y,Z)),cross_product(universal_class,cross_product(universal_class,universal_class))) ),
file('SET004-1.ax',application_function_defn4) ).
cnf(maps1,axiom,
( function(Xf)
| ~ maps(Xf,X,Y) ),
file('SET004-1.ax',maps1) ).
cnf(maps2,axiom,
( domain_of(Xf) = X
| ~ maps(Xf,X,Y) ),
file('SET004-1.ax',maps2) ).
cnf(maps3,axiom,
( subclass(range_of(Xf),Y)
| ~ maps(Xf,X,Y) ),
file('SET004-1.ax',maps3) ).
cnf(maps4,axiom,
( maps(Xf,domain_of(Xf),Y)
| ~ subclass(range_of(Xf),Y)
| ~ function(Xf) ),
file('SET004-1.ax',maps4) ).
cnf(symmetrization,axiom,
union(X,inverse(X)) = symmetrization_of(X),
file('NUM004-0.ax',symmetrization) ).
cnf(irreflexive1,axiom,
( subclass(restrict(X,Y,Y),complement(identity_relation))
| ~ irreflexive(X,Y) ),
file('NUM004-0.ax',irreflexive1) ).
cnf(irreflexive2,axiom,
( irreflexive(X,Y)
| ~ subclass(restrict(X,Y,Y),complement(identity_relation)) ),
file('NUM004-0.ax',irreflexive2) ).
cnf(connected1,axiom,
( subclass(cross_product(Y,Y),union(identity_relation,symmetrization_of(X)))
| ~ connected(X,Y) ),
file('NUM004-0.ax',connected1) ).
cnf(connected2,axiom,
( connected(X,Y)
| ~ subclass(cross_product(Y,Y),union(identity_relation,symmetrization_of(X))) ),
file('NUM004-0.ax',connected2) ).
cnf(transitive1,axiom,
( subclass(compose(restrict(Xr,Y,Y),restrict(Xr,Y,Y)),restrict(Xr,Y,Y))
| ~ transitive(Xr,Y) ),
file('NUM004-0.ax',transitive1) ).
cnf(transitive2,axiom,
( transitive(Xr,Y)
| ~ subclass(compose(restrict(Xr,Y,Y),restrict(Xr,Y,Y)),restrict(Xr,Y,Y)) ),
file('NUM004-0.ax',transitive2) ).
cnf(asymmetric1,axiom,
( restrict(intersection(Xr,inverse(Xr)),Y,Y) = null_class
| ~ asymmetric(Xr,Y) ),
file('NUM004-0.ax',asymmetric1) ).
cnf(asymmetric2,axiom,
( asymmetric(Xr,Y)
| restrict(intersection(Xr,inverse(Xr)),Y,Y) != null_class ),
file('NUM004-0.ax',asymmetric2) ).
cnf(segment,axiom,
segment(Xr,Y,Z) = domain_of(restrict(Xr,Y,singleton(Z))),
file('NUM004-0.ax',segment) ).
cnf(well_ordering1,axiom,
( connected(X,Y)
| ~ well_ordering(X,Y) ),
file('NUM004-0.ax',well_ordering1) ).
cnf(well_ordering2,axiom,
( member(least(Xr,U),U)
| U = null_class
| ~ subclass(U,Y)
| ~ well_ordering(Xr,Y) ),
file('NUM004-0.ax',well_ordering2) ).
cnf(well_ordering3,axiom,
( member(least(Xr,U),U)
| ~ member(V,U)
| ~ subclass(U,Y)
| ~ well_ordering(Xr,Y) ),
file('NUM004-0.ax',well_ordering3) ).
cnf(well_ordering4,axiom,
( segment(Xr,U,least(Xr,U)) = null_class
| ~ subclass(U,Y)
| ~ well_ordering(Xr,Y) ),
file('NUM004-0.ax',well_ordering4) ).
cnf(well_ordering5,axiom,
( ~ member(ordered_pair(V,least(Xr,U)),Xr)
| ~ member(V,U)
| ~ subclass(U,Y)
| ~ well_ordering(Xr,Y) ),
file('NUM004-0.ax',well_ordering5) ).
cnf(well_ordering6,axiom,
( well_ordering(Xr,Y)
| not_well_ordering(Xr,Y) != null_class
| ~ connected(Xr,Y) ),
file('NUM004-0.ax',well_ordering6) ).
cnf(well_ordering7,axiom,
( well_ordering(Xr,Y)
| subclass(not_well_ordering(Xr,Y),Y)
| ~ connected(Xr,Y) ),
file('NUM004-0.ax',well_ordering7) ).
cnf(well_ordering8,axiom,
( well_ordering(Xr,Y)
| ~ connected(Xr,Y)
| segment(Xr,not_well_ordering(Xr,Y),V) != null_class
| ~ member(V,not_well_ordering(Xr,Y)) ),
file('NUM004-0.ax',well_ordering8) ).
cnf(section1,axiom,
( subclass(Y,Z)
| ~ section(Xr,Y,Z) ),
file('NUM004-0.ax',section1) ).
cnf(section2,axiom,
( subclass(domain_of(restrict(Xr,Z,Y)),Y)
| ~ section(Xr,Y,Z) ),
file('NUM004-0.ax',section2) ).
cnf(section3,axiom,
( section(Xr,Y,Z)
| ~ subclass(domain_of(restrict(Xr,Z,Y)),Y)
| ~ subclass(Y,Z) ),
file('NUM004-0.ax',section3) ).
cnf(ordinal_numbers1,axiom,
( well_ordering(element_relation,X)
| ~ member(X,ordinal_numbers) ),
file('NUM004-0.ax',ordinal_numbers1) ).
cnf(ordinal_numbers2,axiom,
( subclass(sum_class(X),X)
| ~ member(X,ordinal_numbers) ),
file('NUM004-0.ax',ordinal_numbers2) ).
cnf(ordinal_numbers3,axiom,
( member(X,ordinal_numbers)
| ~ member(X,universal_class)
| ~ subclass(sum_class(X),X)
| ~ well_ordering(element_relation,X) ),
file('NUM004-0.ax',ordinal_numbers3) ).
cnf(ordinal_numbers4,axiom,
( X = ordinal_numbers
| member(X,ordinal_numbers)
| ~ subclass(sum_class(X),X)
| ~ well_ordering(element_relation,X) ),
file('NUM004-0.ax',ordinal_numbers4) ).
cnf(kind_1_ordinals,axiom,
union(singleton(null_class),image(successor_relation,ordinal_numbers)) = kind_1_ordinals,
file('NUM004-0.ax',kind_1_ordinals) ).
cnf(limit_ordinals,axiom,
intersection(complement(kind_1_ordinals),ordinal_numbers) = limit_ordinals,
file('NUM004-0.ax',limit_ordinals) ).
cnf(rest_of1,axiom,
subclass(rest_of(X),cross_product(universal_class,universal_class)),
file('NUM004-0.ax',rest_of1) ).
cnf(rest_of2,axiom,
( member(U,domain_of(X))
| ~ member(ordered_pair(U,V),rest_of(X)) ),
file('NUM004-0.ax',rest_of2) ).
cnf(rest_of3,axiom,
( restrict(X,U,universal_class) = V
| ~ member(ordered_pair(U,V),rest_of(X)) ),
file('NUM004-0.ax',rest_of3) ).
cnf(rest_of4,axiom,
( member(ordered_pair(U,V),rest_of(X))
| restrict(X,U,universal_class) != V
| ~ member(U,domain_of(X)) ),
file('NUM004-0.ax',rest_of4) ).
cnf(rest_relation1,axiom,
subclass(rest_relation,cross_product(universal_class,universal_class)),
file('NUM004-0.ax',rest_relation1) ).
cnf(rest_relation2,axiom,
( rest_of(X) = Y
| ~ member(ordered_pair(X,Y),rest_relation) ),
file('NUM004-0.ax',rest_relation2) ).
cnf(rest_relation3,axiom,
( member(ordered_pair(X,rest_of(X)),rest_relation)
| ~ member(X,universal_class) ),
file('NUM004-0.ax',rest_relation3) ).
cnf(recursion_equation_functions1,axiom,
( function(Z)
| ~ member(X,recursion_equation_functions(Z)) ),
file('NUM004-0.ax',recursion_equation_functions1) ).
cnf(recursion_equation_functions2,axiom,
( function(X)
| ~ member(X,recursion_equation_functions(Z)) ),
file('NUM004-0.ax',recursion_equation_functions2) ).
cnf(recursion_equation_functions3,axiom,
( member(domain_of(X),ordinal_numbers)
| ~ member(X,recursion_equation_functions(Z)) ),
file('NUM004-0.ax',recursion_equation_functions3) ).
cnf(recursion_equation_functions4,axiom,
( compose(Z,rest_of(X)) = X
| ~ member(X,recursion_equation_functions(Z)) ),
file('NUM004-0.ax',recursion_equation_functions4) ).
cnf(recursion_equation_functions5,axiom,
( member(X,recursion_equation_functions(Z))
| compose(Z,rest_of(X)) != X
| ~ member(domain_of(X),ordinal_numbers)
| ~ function(X)
| ~ function(Z) ),
file('NUM004-0.ax',recursion_equation_functions5) ).
cnf(union_of_range_map1,axiom,
subclass(union_of_range_map,cross_product(universal_class,universal_class)),
file('NUM004-0.ax',union_of_range_map1) ).
cnf(union_of_range_map2,axiom,
( sum_class(range_of(X)) = Y
| ~ member(ordered_pair(X,Y),union_of_range_map) ),
file('NUM004-0.ax',union_of_range_map2) ).
cnf(union_of_range_map3,axiom,
( member(ordered_pair(X,Y),union_of_range_map)
| sum_class(range_of(X)) != Y
| ~ member(ordered_pair(X,Y),cross_product(universal_class,universal_class)) ),
file('NUM004-0.ax',union_of_range_map3) ).
cnf(ordinal_addition,axiom,
apply(recursion(X,successor_relation,union_of_range_map),Y) = ordinal_add(X,Y),
file('NUM004-0.ax',ordinal_addition) ).
cnf(ordinal_multiplication,axiom,
recursion(null_class,apply(add_relation,X),union_of_range_map) = ordinal_multiply(X,Y),
file('NUM004-0.ax',ordinal_multiplication) ).
cnf(integer_function1,axiom,
( integer_of(X) = X
| ~ member(X,omega) ),
file('NUM004-0.ax',integer_function1) ).
cnf(integer_function2,axiom,
( integer_of(X) = null_class
| member(X,omega) ),
file('NUM004-0.ax',integer_function2) ).
cnf(prove_irreflexive_class_property4_1,negated_conjecture,
subclass(x,complement(identity_relation)),
file('theBenchmark.p',prove_irreflexive_class_property4_1) ).
cnf(prove_irreflexive_class_property4_2,negated_conjecture,
~ irreflexive(x,domain_of(symmetrization_of(x))),
file('theBenchmark.p',prove_irreflexive_class_property4_2) ).
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,
( compose_class(Eq_x_0) = compose_class(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_35,axiom,
( single_valued1(Eq_x_0) = single_valued1(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_36,axiom,
( single_valued2(Eq_x_0) = single_valued2(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_37,axiom,
( single_valued3(Eq_x_0) = single_valued3(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_38,axiom,
( symmetrization_of(Eq_x_0) = symmetrization_of(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_39,axiom,
( segment(Eq_x_0,Eq_x_1,Eq_x_2) = segment(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_40,axiom,
( least(Eq_x_0,Eq_x_1) = least(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_41,axiom,
( not_well_ordering(Eq_x_0,Eq_x_1) = not_well_ordering(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_42,axiom,
( rest_of(Eq_x_0) = rest_of(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_43,axiom,
( recursion_equation_functions(Eq_x_0) = recursion_equation_functions(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_44,axiom,
( recursion(Eq_x_0,Eq_x_1,Eq_x_2) = recursion(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_45,axiom,
( ordinal_add(Eq_x_0,Eq_x_1) = ordinal_add(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_46,axiom,
( ordinal_multiply(Eq_x_0,Eq_x_1) = ordinal_multiply(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_47,axiom,
( integer_of(Eq_x_0) = integer_of(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_48,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_49,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_50,axiom,
( inductive(Eq_y_0)
| ~ inductive(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_51,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_52,axiom,
( function(Eq_y_0)
| ~ function(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_53,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_54,axiom,
( operation(Eq_y_0)
| ~ operation(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_55,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_56,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(equality_57,axiom,
( maps(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ maps(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_58,axiom,
( irreflexive(Eq_y_0,Eq_y_1)
| ~ irreflexive(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_59,axiom,
( connected(Eq_y_0,Eq_y_1)
| ~ connected(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_60,axiom,
( transitive(Eq_y_0,Eq_y_1)
| ~ transitive(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_61,axiom,
( asymmetric(Eq_y_0,Eq_y_1)
| ~ asymmetric(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_62,axiom,
( well_ordering(Eq_y_0,Eq_y_1)
| ~ well_ordering(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_63,axiom,
( section(Eq_y_0,Eq_y_1,Eq_y_2)
| ~ section(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 : NUM042-1 : 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/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n011.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sat Sep 19 17:36:54 UTC 2026
% 0.10/0.36 % CPUTime :
% 165.17/165.49 % SZS status Unsatisfiable for theBenchmark
% 165.17/165.49 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------