%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SET055-7 : TPTP v9.3.1. Released v1.0.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 : n015.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:06 AM UTC 2026
% Result : Unsatisfiable 0.10s 0.40s
% Output : Proof 0.10s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(symmetry,axiom,
( equalish(Y,X)
| ~ equalish(X,Y) ),
file('theBenchmark.p',symmetry) ).
cnf(transitivity,axiom,
( equalish(X,Z)
| ~ equalish(Y,Z)
| ~ equalish(X,Y) ),
file('theBenchmark.p',transitivity) ).
cnf(apply_substitution1,axiom,
( equalish(apply(D,F),apply(E,F))
| ~ equalish(D,E) ),
file('theBenchmark.p',apply_substitution1) ).
cnf(apply_substitution2,axiom,
( equalish(apply(I,G),apply(I,H))
| ~ equalish(G,H) ),
file('theBenchmark.p',apply_substitution2) ).
cnf(cantor_substitution1,axiom,
( equalish(cantor(J),cantor(K))
| ~ equalish(J,K) ),
file('theBenchmark.p',cantor_substitution1) ).
cnf(complement_substitution1,axiom,
( equalish(complement(L),complement(M))
| ~ equalish(L,M) ),
file('theBenchmark.p',complement_substitution1) ).
cnf(compose_substitution1,axiom,
( equalish(compose(N,P),compose(O,P))
| ~ equalish(N,O) ),
file('theBenchmark.p',compose_substitution1) ).
cnf(compose_substitution2,axiom,
( equalish(compose(S,Q),compose(S,R))
| ~ equalish(Q,R) ),
file('theBenchmark.p',compose_substitution2) ).
cnf(cross_product_substitution1,axiom,
( equalish(cross_product(T,V),cross_product(U,V))
| ~ equalish(T,U) ),
file('theBenchmark.p',cross_product_substitution1) ).
cnf(cross_product_substitution2,axiom,
( equalish(cross_product(Y,W),cross_product(Y,X))
| ~ equalish(W,X) ),
file('theBenchmark.p',cross_product_substitution2) ).
cnf(diagonalise_substitution1,axiom,
( equalish(diagonalise(Z),diagonalise(A1))
| ~ equalish(Z,A1) ),
file('theBenchmark.p',diagonalise_substitution1) ).
cnf(symmetric_difference_substitution1,axiom,
( equalish(symmetric_difference(B1,D1),symmetric_difference(C1,D1))
| ~ equalish(B1,C1) ),
file('theBenchmark.p',symmetric_difference_substitution1) ).
cnf(symmetric_difference_substitution2,axiom,
( equalish(symmetric_difference(G1,E1),symmetric_difference(G1,F1))
| ~ equalish(E1,F1) ),
file('theBenchmark.p',symmetric_difference_substitution2) ).
cnf(domain_substitution1,axiom,
( equalish(domain(H1,J1,K1),domain(I1,J1,K1))
| ~ equalish(H1,I1) ),
file('theBenchmark.p',domain_substitution1) ).
cnf(domain_substitution2,axiom,
( equalish(domain(N1,L1,O1),domain(N1,M1,O1))
| ~ equalish(L1,M1) ),
file('theBenchmark.p',domain_substitution2) ).
cnf(domain_substitution3,axiom,
( equalish(domain(R1,S1,P1),domain(R1,S1,Q1))
| ~ equalish(P1,Q1) ),
file('theBenchmark.p',domain_substitution3) ).
cnf(domain_of_substitution1,axiom,
( equalish(domain_of(T1),domain_of(U1))
| ~ equalish(T1,U1) ),
file('theBenchmark.p',domain_of_substitution1) ).
cnf(first_substitution1,axiom,
( equalish(first(V1),first(W1))
| ~ equalish(V1,W1) ),
file('theBenchmark.p',first_substitution1) ).
cnf(flip_substitution1,axiom,
( equalish(flip(X1),flip(Y1))
| ~ equalish(X1,Y1) ),
file('theBenchmark.p',flip_substitution1) ).
cnf(image_substitution1,axiom,
( equalish(image(Z1,B2),image(A2,B2))
| ~ equalish(Z1,A2) ),
file('theBenchmark.p',image_substitution1) ).
cnf(image_substitution2,axiom,
( equalish(image(E2,C2),image(E2,D2))
| ~ equalish(C2,D2) ),
file('theBenchmark.p',image_substitution2) ).
cnf(intersection_substitution1,axiom,
( equalish(intersection(F2,H2),intersection(G2,H2))
| ~ equalish(F2,G2) ),
file('theBenchmark.p',intersection_substitution1) ).
cnf(intersection_substitution2,axiom,
( equalish(intersection(K2,I2),intersection(K2,J2))
| ~ equalish(I2,J2) ),
file('theBenchmark.p',intersection_substitution2) ).
cnf(inverse_substitution1,axiom,
( equalish(inverse(L2),inverse(M2))
| ~ equalish(L2,M2) ),
file('theBenchmark.p',inverse_substitution1) ).
cnf(not_homomorphism1_substitution1,axiom,
( equalish(not_homomorphism1(N2,P2,Q2),not_homomorphism1(O2,P2,Q2))
| ~ equalish(N2,O2) ),
file('theBenchmark.p',not_homomorphism1_substitution1) ).
cnf(not_homomorphism1_substitution2,axiom,
( equalish(not_homomorphism1(T2,R2,U2),not_homomorphism1(T2,S2,U2))
| ~ equalish(R2,S2) ),
file('theBenchmark.p',not_homomorphism1_substitution2) ).
cnf(not_homomorphism1_substitution3,axiom,
( equalish(not_homomorphism1(X2,Y2,V2),not_homomorphism1(X2,Y2,W2))
| ~ equalish(V2,W2) ),
file('theBenchmark.p',not_homomorphism1_substitution3) ).
cnf(not_homomorphism2_substitution1,axiom,
( equalish(not_homomorphism2(Z2,B3,C3),not_homomorphism2(A3,B3,C3))
| ~ equalish(Z2,A3) ),
file('theBenchmark.p',not_homomorphism2_substitution1) ).
cnf(not_homomorphism2_substitution2,axiom,
( equalish(not_homomorphism2(F3,D3,G3),not_homomorphism2(F3,E3,G3))
| ~ equalish(D3,E3) ),
file('theBenchmark.p',not_homomorphism2_substitution2) ).
cnf(not_homomorphism2_substitution3,axiom,
( equalish(not_homomorphism2(J3,K3,H3),not_homomorphism2(J3,K3,I3))
| ~ equalish(H3,I3) ),
file('theBenchmark.p',not_homomorphism2_substitution3) ).
cnf(not_subclass_element_substitution1,axiom,
( equalish(not_subclass_element(L3,N3),not_subclass_element(M3,N3))
| ~ equalish(L3,M3) ),
file('theBenchmark.p',not_subclass_element_substitution1) ).
cnf(not_subclass_element_substitution2,axiom,
( equalish(not_subclass_element(Q3,O3),not_subclass_element(Q3,P3))
| ~ equalish(O3,P3) ),
file('theBenchmark.p',not_subclass_element_substitution2) ).
cnf(ordered_pair_substitution1,axiom,
( equalish(ordered_pair(R3,T3),ordered_pair(S3,T3))
| ~ equalish(R3,S3) ),
file('theBenchmark.p',ordered_pair_substitution1) ).
cnf(ordered_pair_substitution2,axiom,
( equalish(ordered_pair(W3,U3),ordered_pair(W3,V3))
| ~ equalish(U3,V3) ),
file('theBenchmark.p',ordered_pair_substitution2) ).
cnf(power_class_substitution1,axiom,
( equalish(power_class(X3),power_class(Y3))
| ~ equalish(X3,Y3) ),
file('theBenchmark.p',power_class_substitution1) ).
cnf(range_substitution1,axiom,
( equalish(range(Z3,B4,C4),range(A4,B4,C4))
| ~ equalish(Z3,A4) ),
file('theBenchmark.p',range_substitution1) ).
cnf(range_substitution2,axiom,
( equalish(range(F4,D4,G4),range(F4,E4,G4))
| ~ equalish(D4,E4) ),
file('theBenchmark.p',range_substitution2) ).
cnf(range_substitution3,axiom,
( equalish(range(J4,K4,H4),range(J4,K4,I4))
| ~ equalish(H4,I4) ),
file('theBenchmark.p',range_substitution3) ).
cnf(range_of_substitution1,axiom,
( equalish(range_of(L4),range_of(M4))
| ~ equalish(L4,M4) ),
file('theBenchmark.p',range_of_substitution1) ).
cnf(regular_substitution1,axiom,
( equalish(regular(N4),regular(O4))
| ~ equalish(N4,O4) ),
file('theBenchmark.p',regular_substitution1) ).
cnf(restrict_substitution1,axiom,
( equalish(restrict(P4,R4,S4),restrict(Q4,R4,S4))
| ~ equalish(P4,Q4) ),
file('theBenchmark.p',restrict_substitution1) ).
cnf(restrict_substitution2,axiom,
( equalish(restrict(V4,T4,W4),restrict(V4,U4,W4))
| ~ equalish(T4,U4) ),
file('theBenchmark.p',restrict_substitution2) ).
cnf(restrict_substitution3,axiom,
( equalish(restrict(Z4,A5,X4),restrict(Z4,A5,Y4))
| ~ equalish(X4,Y4) ),
file('theBenchmark.p',restrict_substitution3) ).
cnf(rotate_substitution1,axiom,
( equalish(rotate(B5),rotate(C5))
| ~ equalish(B5,C5) ),
file('theBenchmark.p',rotate_substitution1) ).
cnf(second_substitution1,axiom,
( equalish(second(D5),second(E5))
| ~ equalish(D5,E5) ),
file('theBenchmark.p',second_substitution1) ).
cnf(singleton_substitution1,axiom,
( equalish(singleton(F5),singleton(G5))
| ~ equalish(F5,G5) ),
file('theBenchmark.p',singleton_substitution1) ).
cnf(successor_substitution1,axiom,
( equalish(successor(H5),successor(I5))
| ~ equalish(H5,I5) ),
file('theBenchmark.p',successor_substitution1) ).
cnf(sum_class_substitution1,axiom,
( equalish(sum_class(J5),sum_class(K5))
| ~ equalish(J5,K5) ),
file('theBenchmark.p',sum_class_substitution1) ).
cnf(union_substitution1,axiom,
( equalish(union(L5,N5),union(M5,N5))
| ~ equalish(L5,M5) ),
file('theBenchmark.p',union_substitution1) ).
cnf(union_substitution2,axiom,
( equalish(union(Q5,O5),union(Q5,P5))
| ~ equalish(O5,P5) ),
file('theBenchmark.p',union_substitution2) ).
cnf(unordered_pair_substitution1,axiom,
( equalish(unordered_pair(R5,T5),unordered_pair(S5,T5))
| ~ equalish(R5,S5) ),
file('theBenchmark.p',unordered_pair_substitution1) ).
cnf(unordered_pair_substitution2,axiom,
( equalish(unordered_pair(W5,U5),unordered_pair(W5,V5))
| ~ equalish(U5,V5) ),
file('theBenchmark.p',unordered_pair_substitution2) ).
cnf(compatible_substitution1,axiom,
( compatible(Y5,Z5,A6)
| ~ compatible(X5,Z5,A6)
| ~ equalish(X5,Y5) ),
file('theBenchmark.p',compatible_substitution1) ).
cnf(compatible_substitution2,axiom,
( compatible(D6,C6,E6)
| ~ compatible(D6,B6,E6)
| ~ equalish(B6,C6) ),
file('theBenchmark.p',compatible_substitution2) ).
cnf(compatible_substitution3,axiom,
( compatible(H6,I6,G6)
| ~ compatible(H6,I6,F6)
| ~ equalish(F6,G6) ),
file('theBenchmark.p',compatible_substitution3) ).
cnf(function_substitution1,axiom,
( function(K6)
| ~ function(J6)
| ~ equalish(J6,K6) ),
file('theBenchmark.p',function_substitution1) ).
cnf(homomorphism_substitution1,axiom,
( homomorphism(M6,N6,O6)
| ~ homomorphism(L6,N6,O6)
| ~ equalish(L6,M6) ),
file('theBenchmark.p',homomorphism_substitution1) ).
cnf(homomorphism_substitution2,axiom,
( homomorphism(R6,Q6,S6)
| ~ homomorphism(R6,P6,S6)
| ~ equalish(P6,Q6) ),
file('theBenchmark.p',homomorphism_substitution2) ).
cnf(homomorphism_substitution3,axiom,
( homomorphism(V6,W6,U6)
| ~ homomorphism(V6,W6,T6)
| ~ equalish(T6,U6) ),
file('theBenchmark.p',homomorphism_substitution3) ).
cnf(inductive_substitution1,axiom,
( inductive(Y6)
| ~ inductive(X6)
| ~ equalish(X6,Y6) ),
file('theBenchmark.p',inductive_substitution1) ).
cnf(member_substitution1,axiom,
( member(A7,B7)
| ~ member(Z6,B7)
| ~ equalish(Z6,A7) ),
file('theBenchmark.p',member_substitution1) ).
cnf(member_substitution2,axiom,
( member(E7,D7)
| ~ member(E7,C7)
| ~ equalish(C7,D7) ),
file('theBenchmark.p',member_substitution2) ).
cnf(one_to_one_substitution1,axiom,
( one_to_one(G7)
| ~ one_to_one(F7)
| ~ equalish(F7,G7) ),
file('theBenchmark.p',one_to_one_substitution1) ).
cnf(operation_substitution1,axiom,
( operation(I7)
| ~ operation(H7)
| ~ equalish(H7,I7) ),
file('theBenchmark.p',operation_substitution1) ).
cnf(single_valued_class_substitution1,axiom,
( single_valued_class(K7)
| ~ single_valued_class(J7)
| ~ equalish(J7,K7) ),
file('theBenchmark.p',single_valued_class_substitution1) ).
cnf(subclass_substitution1,axiom,
( subclass(M7,N7)
| ~ subclass(L7,N7)
| ~ equalish(L7,M7) ),
file('theBenchmark.p',subclass_substitution1) ).
cnf(subclass_substitution2,axiom,
( subclass(Q7,P7)
| ~ subclass(Q7,O7)
| ~ equalish(O7,P7) ),
file('theBenchmark.p',subclass_substitution2) ).
cnf(subclass_members,axiom,
( member(U,Y)
| ~ member(U,X)
| ~ subclass(X,Y) ),
file('theBenchmark.p',subclass_members) ).
cnf(not_subclass_members1,axiom,
( subclass(X,Y)
| member(not_subclass_element(X,Y),X) ),
file('theBenchmark.p',not_subclass_members1) ).
cnf(not_subclass_members2,axiom,
( subclass(X,Y)
| ~ member(not_subclass_element(X,Y),Y) ),
file('theBenchmark.p',not_subclass_members2) ).
cnf(class_elements_are_sets,axiom,
subclass(X,universal_class),
file('theBenchmark.p',class_elements_are_sets) ).
cnf(equal_implies_subclass1,axiom,
( subclass(X,Y)
| ~ equalish(X,Y) ),
file('theBenchmark.p',equal_implies_subclass1) ).
cnf(equal_implies_subclass2,axiom,
( subclass(Y,X)
| ~ equalish(X,Y) ),
file('theBenchmark.p',equal_implies_subclass2) ).
cnf(subclass_implies_equal,axiom,
( equalish(X,Y)
| ~ subclass(Y,X)
| ~ subclass(X,Y) ),
file('theBenchmark.p',subclass_implies_equal) ).
cnf(unordered_pair_member,axiom,
( equalish(U,Y)
| equalish(U,X)
| ~ member(U,unordered_pair(X,Y)) ),
file('theBenchmark.p',unordered_pair_member) ).
cnf(unordered_pair2,axiom,
( member(X,unordered_pair(X,Y))
| ~ member(X,universal_class) ),
file('theBenchmark.p',unordered_pair2) ).
cnf(unordered_pair3,axiom,
( member(Y,unordered_pair(X,Y))
| ~ member(Y,universal_class) ),
file('theBenchmark.p',unordered_pair3) ).
cnf(unordered_pairs_in_universal,axiom,
member(unordered_pair(X,Y),universal_class),
file('theBenchmark.p',unordered_pairs_in_universal) ).
cnf(singleton_set,axiom,
equalish(unordered_pair(X,X),singleton(X)),
file('theBenchmark.p',singleton_set) ).
cnf(ordered_pair,axiom,
equalish(unordered_pair(singleton(X),unordered_pair(X,singleton(Y))),ordered_pair(X,Y)),
file('theBenchmark.p',ordered_pair) ).
cnf(cartesian_product1,axiom,
( member(U,X)
| ~ member(ordered_pair(U,V),cross_product(X,Y)) ),
file('theBenchmark.p',cartesian_product1) ).
cnf(cartesian_product2,axiom,
( member(V,Y)
| ~ member(ordered_pair(U,V),cross_product(X,Y)) ),
file('theBenchmark.p',cartesian_product2) ).
cnf(cartesian_product3,axiom,
( member(ordered_pair(U,V),cross_product(X,Y))
| ~ member(V,Y)
| ~ member(U,X) ),
file('theBenchmark.p',cartesian_product3) ).
cnf(cartesian_product4,axiom,
( equalish(ordered_pair(first(Z),second(Z)),Z)
| ~ member(Z,cross_product(X,Y)) ),
file('theBenchmark.p',cartesian_product4) ).
cnf(element_relation1,axiom,
subclass(element_relation,cross_product(universal_class,universal_class)),
file('theBenchmark.p',element_relation1) ).
cnf(element_relation2,axiom,
( member(X,Y)
| ~ member(ordered_pair(X,Y),element_relation) ),
file('theBenchmark.p',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('theBenchmark.p',element_relation3) ).
cnf(intersection1,axiom,
( member(Z,X)
| ~ member(Z,intersection(X,Y)) ),
file('theBenchmark.p',intersection1) ).
cnf(intersection2,axiom,
( member(Z,Y)
| ~ member(Z,intersection(X,Y)) ),
file('theBenchmark.p',intersection2) ).
cnf(intersection3,axiom,
( member(Z,intersection(X,Y))
| ~ member(Z,Y)
| ~ member(Z,X) ),
file('theBenchmark.p',intersection3) ).
cnf(complement1,axiom,
( ~ member(Z,X)
| ~ member(Z,complement(X)) ),
file('theBenchmark.p',complement1) ).
cnf(complement2,axiom,
( member(Z,X)
| member(Z,complement(X))
| ~ member(Z,universal_class) ),
file('theBenchmark.p',complement2) ).
cnf(union,axiom,
equalish(complement(intersection(complement(X),complement(Y))),union(X,Y)),
file('theBenchmark.p',union) ).
cnf(symmetric_difference,axiom,
equalish(intersection(complement(intersection(X,Y)),complement(intersection(complement(X),complement(Y)))),symmetric_difference(X,Y)),
file('theBenchmark.p',symmetric_difference) ).
cnf(restriction1,axiom,
equalish(intersection(Xr,cross_product(X,Y)),restrict(Xr,X,Y)),
file('theBenchmark.p',restriction1) ).
cnf(restriction2,axiom,
equalish(intersection(cross_product(X,Y),Xr),restrict(Xr,X,Y)),
file('theBenchmark.p',restriction2) ).
cnf(domain1,axiom,
( ~ member(Z,domain_of(X))
| ~ equalish(restrict(X,singleton(Z),universal_class),null_class) ),
file('theBenchmark.p',domain1) ).
cnf(domain2,axiom,
( member(Z,domain_of(X))
| equalish(restrict(X,singleton(Z),universal_class),null_class)
| ~ member(Z,universal_class) ),
file('theBenchmark.p',domain2) ).
cnf(rotate1,axiom,
subclass(rotate(X),cross_product(cross_product(universal_class,universal_class),universal_class)),
file('theBenchmark.p',rotate1) ).
cnf(rotate2,axiom,
( member(ordered_pair(ordered_pair(V,W),U),X)
| ~ member(ordered_pair(ordered_pair(U,V),W),rotate(X)) ),
file('theBenchmark.p',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('theBenchmark.p',rotate3) ).
cnf(flip1,axiom,
subclass(flip(X),cross_product(cross_product(universal_class,universal_class),universal_class)),
file('theBenchmark.p',flip1) ).
cnf(flip2,axiom,
( member(ordered_pair(ordered_pair(V,U),W),X)
| ~ member(ordered_pair(ordered_pair(U,V),W),flip(X)) ),
file('theBenchmark.p',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('theBenchmark.p',flip3) ).
cnf(inverse,axiom,
equalish(domain_of(flip(cross_product(Y,universal_class))),inverse(Y)),
file('theBenchmark.p',inverse) ).
cnf(range_of,axiom,
equalish(domain_of(inverse(Z)),range_of(Z)),
file('theBenchmark.p',range_of) ).
cnf(domain,axiom,
equalish(first(not_subclass_element(restrict(Z,X,singleton(Y)),null_class)),domain(Z,X,Y)),
file('theBenchmark.p',domain) ).
cnf(range,axiom,
equalish(second(not_subclass_element(restrict(Z,singleton(X),Y),null_class)),range(Z,X,Y)),
file('theBenchmark.p',range) ).
cnf(image,axiom,
equalish(range_of(restrict(Xr,X,universal_class)),image(Xr,X)),
file('theBenchmark.p',image) ).
cnf(successor,axiom,
equalish(union(X,singleton(X)),successor(X)),
file('theBenchmark.p',successor) ).
cnf(successor_relation1,axiom,
subclass(successor_relation,cross_product(universal_class,universal_class)),
file('theBenchmark.p',successor_relation1) ).
cnf(successor_relation2,axiom,
( equalish(successor(X),Y)
| ~ member(ordered_pair(X,Y),successor_relation) ),
file('theBenchmark.p',successor_relation2) ).
cnf(successor_relation3,axiom,
( member(ordered_pair(X,Y),successor_relation)
| ~ member(ordered_pair(X,Y),cross_product(universal_class,universal_class))
| ~ equalish(successor(X),Y) ),
file('theBenchmark.p',successor_relation3) ).
cnf(inductive1,axiom,
( member(null_class,X)
| ~ inductive(X) ),
file('theBenchmark.p',inductive1) ).
cnf(inductive2,axiom,
( subclass(image(successor_relation,X),X)
| ~ inductive(X) ),
file('theBenchmark.p',inductive2) ).
cnf(inductive3,axiom,
( inductive(X)
| ~ subclass(image(successor_relation,X),X)
| ~ member(null_class,X) ),
file('theBenchmark.p',inductive3) ).
cnf(omega_is_inductive1,axiom,
inductive(omega),
file('theBenchmark.p',omega_is_inductive1) ).
cnf(omega_is_inductive2,axiom,
( subclass(omega,Y)
| ~ inductive(Y) ),
file('theBenchmark.p',omega_is_inductive2) ).
cnf(omega_in_universal,axiom,
member(omega,universal_class),
file('theBenchmark.p',omega_in_universal) ).
cnf(sum_class_definition,axiom,
equalish(domain_of(restrict(element_relation,universal_class,X)),sum_class(X)),
file('theBenchmark.p',sum_class_definition) ).
cnf(sum_class2,axiom,
( member(sum_class(X),universal_class)
| ~ member(X,universal_class) ),
file('theBenchmark.p',sum_class2) ).
cnf(power_class_definition,axiom,
equalish(complement(image(element_relation,complement(X))),power_class(X)),
file('theBenchmark.p',power_class_definition) ).
cnf(power_class2,axiom,
( member(power_class(U),universal_class)
| ~ member(U,universal_class) ),
file('theBenchmark.p',power_class2) ).
cnf(compose1,axiom,
subclass(compose(Yr,Xr),cross_product(universal_class,universal_class)),
file('theBenchmark.p',compose1) ).
cnf(compose2,axiom,
( member(Z,image(Yr,image(Xr,singleton(Y))))
| ~ member(ordered_pair(Y,Z),compose(Yr,Xr)) ),
file('theBenchmark.p',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('theBenchmark.p',compose3) ).
cnf(single_valued_class1,axiom,
( subclass(compose(X,inverse(X)),identity_relation)
| ~ single_valued_class(X) ),
file('theBenchmark.p',single_valued_class1) ).
cnf(single_valued_class2,axiom,
( single_valued_class(X)
| ~ subclass(compose(X,inverse(X)),identity_relation) ),
file('theBenchmark.p',single_valued_class2) ).
cnf(function1,axiom,
( subclass(Xf,cross_product(universal_class,universal_class))
| ~ function(Xf) ),
file('theBenchmark.p',function1) ).
cnf(function2,axiom,
( subclass(compose(Xf,inverse(Xf)),identity_relation)
| ~ function(Xf) ),
file('theBenchmark.p',function2) ).
cnf(function3,axiom,
( function(Xf)
| ~ subclass(compose(Xf,inverse(Xf)),identity_relation)
| ~ subclass(Xf,cross_product(universal_class,universal_class)) ),
file('theBenchmark.p',function3) ).
cnf(replacement,axiom,
( member(image(Xf,X),universal_class)
| ~ member(X,universal_class)
| ~ function(Xf) ),
file('theBenchmark.p',replacement) ).
cnf(regularity1,axiom,
( member(regular(X),X)
| equalish(X,null_class) ),
file('theBenchmark.p',regularity1) ).
cnf(regularity2,axiom,
( equalish(intersection(X,regular(X)),null_class)
| equalish(X,null_class) ),
file('theBenchmark.p',regularity2) ).
cnf(apply,axiom,
equalish(sum_class(image(Xf,singleton(Y))),apply(Xf,Y)),
file('theBenchmark.p',apply) ).
cnf(choice1,axiom,
function(choice),
file('theBenchmark.p',choice1) ).
cnf(choice2,axiom,
( member(apply(choice,Y),Y)
| equalish(Y,null_class)
| ~ member(Y,universal_class) ),
file('theBenchmark.p',choice2) ).
cnf(one_to_one1,axiom,
( function(Xf)
| ~ one_to_one(Xf) ),
file('theBenchmark.p',one_to_one1) ).
cnf(one_to_one2,axiom,
( function(inverse(Xf))
| ~ one_to_one(Xf) ),
file('theBenchmark.p',one_to_one2) ).
cnf(one_to_one3,axiom,
( one_to_one(Xf)
| ~ function(Xf)
| ~ function(inverse(Xf)) ),
file('theBenchmark.p',one_to_one3) ).
cnf(subset_relation,axiom,
equalish(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('theBenchmark.p',subset_relation) ).
cnf(identity_relation,axiom,
equalish(intersection(inverse(subset_relation),subset_relation),identity_relation),
file('theBenchmark.p',identity_relation) ).
cnf(diagonalisation,axiom,
equalish(complement(domain_of(intersection(Xr,identity_relation))),diagonalise(Xr)),
file('theBenchmark.p',diagonalisation) ).
cnf(cantor_class,axiom,
equalish(intersection(domain_of(X),diagonalise(compose(inverse(element_relation),X))),cantor(X)),
file('theBenchmark.p',cantor_class) ).
cnf(operation1,axiom,
( function(Xf)
| ~ operation(Xf) ),
file('theBenchmark.p',operation1) ).
cnf(operation2,axiom,
( equalish(cross_product(domain_of(domain_of(Xf)),domain_of(domain_of(Xf))),domain_of(Xf))
| ~ operation(Xf) ),
file('theBenchmark.p',operation2) ).
cnf(operation3,axiom,
( subclass(range_of(Xf),domain_of(domain_of(Xf)))
| ~ operation(Xf) ),
file('theBenchmark.p',operation3) ).
cnf(operation4,axiom,
( operation(Xf)
| ~ subclass(range_of(Xf),domain_of(domain_of(Xf)))
| ~ equalish(cross_product(domain_of(domain_of(Xf)),domain_of(domain_of(Xf))),domain_of(Xf))
| ~ function(Xf) ),
file('theBenchmark.p',operation4) ).
cnf(compatible1,axiom,
( function(Xh)
| ~ compatible(Xh,Xf1,Xf2) ),
file('theBenchmark.p',compatible1) ).
cnf(compatible2,axiom,
( equalish(domain_of(domain_of(Xf1)),domain_of(Xh))
| ~ compatible(Xh,Xf1,Xf2) ),
file('theBenchmark.p',compatible2) ).
cnf(compatible3,axiom,
( subclass(range_of(Xh),domain_of(domain_of(Xf2)))
| ~ compatible(Xh,Xf1,Xf2) ),
file('theBenchmark.p',compatible3) ).
cnf(compatible4,axiom,
( compatible(Xh1,Xf1,Xf2)
| ~ subclass(range_of(Xh),domain_of(domain_of(Xf2)))
| ~ equalish(domain_of(domain_of(Xf1)),domain_of(Xh))
| ~ function(Xh) ),
file('theBenchmark.p',compatible4) ).
cnf(homomorphism1,axiom,
( operation(Xf1)
| ~ homomorphism(Xh,Xf1,Xf2) ),
file('theBenchmark.p',homomorphism1) ).
cnf(homomorphism2,axiom,
( operation(Xf2)
| ~ homomorphism(Xh,Xf1,Xf2) ),
file('theBenchmark.p',homomorphism2) ).
cnf(homomorphism3,axiom,
( compatible(Xh,Xf1,Xf2)
| ~ homomorphism(Xh,Xf1,Xf2) ),
file('theBenchmark.p',homomorphism3) ).
cnf(homomorphism4,axiom,
( equalish(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('theBenchmark.p',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('theBenchmark.p',homomorphism5) ).
cnf(homomorphism6,axiom,
( homomorphism(Xh,Xf1,Xf2)
| ~ equalish(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('theBenchmark.p',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(prove_reflexivity,negated_conjecture,
~ equalish(x,x),
file('theBenchmark.p',prove_reflexivity) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET055-7 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.03 This is a CNF_UNS_RFO_NEQ_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.08/0.33 % Computer : n015.cluster.edu
% 0.08/0.33 % Model : x86_64 x86_64
% 0.08/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.33 % Memory : 8046.5625MB
% 0.08/0.33 % OS : Linux 6.8.0-71-generic
% 0.08/0.33 % CPULimit : 300
% 0.08/0.33 % WCLimit : 300
% 0.08/0.33 % DateTime : Sat Sep 19 21:38:18 UTC 2026
% 0.08/0.34 % CPUTime :
% 0.10/0.40 % SZS status Unsatisfiable for theBenchmark
% 0.10/0.40 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------