%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SET021-3 : TPTP v9.3.1. Released v1.0.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 : 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:55:57 AM UTC 2026
% Result : Unsatisfiable 150.32s 160.69s
% Output : Proof 150.92s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(a2,axiom,
( little_set(X)
| ~ member(X,Y) ),
file('SET003-0.ax',a2) ).
cnf(extensionality1,axiom,
( X = Y
| little_set(f1(X,Y)) ),
file('SET003-0.ax',extensionality1) ).
cnf(extensionality2,axiom,
( X = Y
| member(f1(X,Y),Y)
| member(f1(X,Y),X) ),
file('SET003-0.ax',extensionality2) ).
cnf(extensionality3,axiom,
( X = Y
| ~ member(f1(X,Y),Y)
| ~ member(f1(X,Y),X) ),
file('SET003-0.ax',extensionality3) ).
cnf(non_ordered_pair1,axiom,
( U = Y
| U = X
| ~ member(U,non_ordered_pair(X,Y)) ),
file('SET003-0.ax',non_ordered_pair1) ).
cnf(non_ordered_pair2,axiom,
( U != X
| ~ little_set(U)
| member(U,non_ordered_pair(X,Y)) ),
file('SET003-0.ax',non_ordered_pair2) ).
cnf(non_ordered_pair3,axiom,
( U != Y
| ~ little_set(U)
| member(U,non_ordered_pair(X,Y)) ),
file('SET003-0.ax',non_ordered_pair3) ).
cnf(non_ordered_pair4,axiom,
little_set(non_ordered_pair(X,Y)),
file('SET003-0.ax',non_ordered_pair4) ).
cnf(singleton_set,axiom,
singleton_set(X) = non_ordered_pair(X,X),
file('SET003-0.ax',singleton_set) ).
cnf(ordered_pair,axiom,
ordered_pair(X,Y) = non_ordered_pair(singleton_set(X),non_ordered_pair(X,Y)),
file('SET003-0.ax',ordered_pair) ).
cnf(ordered_pair_predicate1,axiom,
( little_set(f2(X))
| ~ ordered_pair_predicate(X) ),
file('SET003-0.ax',ordered_pair_predicate1) ).
cnf(ordered_pair_predicate2,axiom,
( little_set(f3(X))
| ~ ordered_pair_predicate(X) ),
file('SET003-0.ax',ordered_pair_predicate2) ).
cnf(ordered_pair_predicate3,axiom,
( X = ordered_pair(f2(X),f3(X))
| ~ ordered_pair_predicate(X) ),
file('SET003-0.ax',ordered_pair_predicate3) ).
cnf(ordered_pair_predicate4,axiom,
( X != ordered_pair(Y,Z)
| ~ little_set(Z)
| ~ little_set(Y)
| ordered_pair_predicate(X) ),
file('SET003-0.ax',ordered_pair_predicate4) ).
cnf(first1,axiom,
( little_set(f4(Z,X))
| ~ member(Z,first(X)) ),
file('SET003-0.ax',first1) ).
cnf(first2,axiom,
( little_set(f5(Z,X))
| ~ member(Z,first(X)) ),
file('SET003-0.ax',first2) ).
cnf(first3,axiom,
( X = ordered_pair(f4(Z,X),f5(Z,X))
| ~ member(Z,first(X)) ),
file('SET003-0.ax',first3) ).
cnf(first4,axiom,
( member(Z,f4(Z,X))
| ~ member(Z,first(X)) ),
file('SET003-0.ax',first4) ).
cnf(first5,axiom,
( ~ member(Z,U)
| X != ordered_pair(U,V)
| ~ little_set(V)
| ~ little_set(U)
| member(Z,first(X)) ),
file('SET003-0.ax',first5) ).
cnf(second1,axiom,
( little_set(f6(Z,X))
| ~ member(Z,second(X)) ),
file('SET003-0.ax',second1) ).
cnf(second2,axiom,
( little_set(f7(Z,X))
| ~ member(Z,second(X)) ),
file('SET003-0.ax',second2) ).
cnf(second3,axiom,
( X = ordered_pair(f6(Z,X),f7(Z,X))
| ~ member(Z,second(X)) ),
file('SET003-0.ax',second3) ).
cnf(second4,axiom,
( member(Z,f7(Z,X))
| ~ member(Z,second(X)) ),
file('SET003-0.ax',second4) ).
cnf(second5,axiom,
( ~ member(Z,V)
| X != ordered_pair(U,V)
| ~ little_set(V)
| ~ little_set(U)
| member(Z,second(X)) ),
file('SET003-0.ax',second5) ).
cnf(element_relation1,axiom,
( ordered_pair_predicate(Z)
| ~ member(Z,estin) ),
file('SET003-0.ax',element_relation1) ).
cnf(element_relation2,axiom,
( member(first(Z),second(Z))
| ~ member(Z,estin) ),
file('SET003-0.ax',element_relation2) ).
cnf(element_relation3,axiom,
( ~ member(first(Z),second(Z))
| ~ ordered_pair_predicate(Z)
| ~ little_set(Z)
| member(Z,estin) ),
file('SET003-0.ax',element_relation3) ).
cnf(intersection1,axiom,
( member(Z,X)
| ~ member(Z,intersection(X,Y)) ),
file('SET003-0.ax',intersection1) ).
cnf(intersection2,axiom,
( member(Z,Y)
| ~ member(Z,intersection(X,Y)) ),
file('SET003-0.ax',intersection2) ).
cnf(intersection3,axiom,
( ~ member(Z,Y)
| ~ member(Z,X)
| member(Z,intersection(X,Y)) ),
file('SET003-0.ax',intersection3) ).
cnf(complement1,axiom,
( ~ member(Z,X)
| ~ member(Z,complement(X)) ),
file('SET003-0.ax',complement1) ).
cnf(complement2,axiom,
( member(Z,X)
| ~ little_set(Z)
| member(Z,complement(X)) ),
file('SET003-0.ax',complement2) ).
cnf(union,axiom,
union(X,Y) = complement(intersection(complement(X),complement(Y))),
file('SET003-0.ax',union) ).
cnf(domain1,axiom,
( ordered_pair_predicate(f8(Z,X))
| ~ member(Z,domain_of(X)) ),
file('SET003-0.ax',domain1) ).
cnf(domain2,axiom,
( member(f8(Z,X),X)
| ~ member(Z,domain_of(X)) ),
file('SET003-0.ax',domain2) ).
cnf(domain3,axiom,
( Z = first(f8(Z,X))
| ~ member(Z,domain_of(X)) ),
file('SET003-0.ax',domain3) ).
cnf(domain4,axiom,
( Z != first(Xp)
| ~ member(Xp,X)
| ~ ordered_pair_predicate(Xp)
| ~ little_set(Z)
| member(Z,domain_of(X)) ),
file('SET003-0.ax',domain4) ).
cnf(cross_product1,axiom,
( ordered_pair_predicate(Z)
| ~ member(Z,cross_product(X,Y)) ),
file('SET003-0.ax',cross_product1) ).
cnf(cross_product2,axiom,
( member(first(Z),X)
| ~ member(Z,cross_product(X,Y)) ),
file('SET003-0.ax',cross_product2) ).
cnf(cross_product3,axiom,
( member(second(Z),Y)
| ~ member(Z,cross_product(X,Y)) ),
file('SET003-0.ax',cross_product3) ).
cnf(cross_product4,axiom,
( ~ member(second(Z),Y)
| ~ member(first(Z),X)
| ~ ordered_pair_predicate(Z)
| ~ little_set(Z)
| member(Z,cross_product(X,Y)) ),
file('SET003-0.ax',cross_product4) ).
cnf(converse1,axiom,
( ordered_pair_predicate(Z)
| ~ member(Z,converse(X)) ),
file('SET003-0.ax',converse1) ).
cnf(converse2,axiom,
( member(ordered_pair(second(Z),first(Z)),X)
| ~ member(Z,converse(X)) ),
file('SET003-0.ax',converse2) ).
cnf(converse3,axiom,
( ~ member(ordered_pair(second(Z),first(Z)),X)
| ~ ordered_pair_predicate(Z)
| ~ little_set(Z)
| member(Z,converse(X)) ),
file('SET003-0.ax',converse3) ).
cnf(rotate_right1,axiom,
( little_set(f9(Z,X))
| ~ member(Z,rotate_right(X)) ),
file('SET003-0.ax',rotate_right1) ).
cnf(rotate_right2,axiom,
( little_set(f10(Z,X))
| ~ member(Z,rotate_right(X)) ),
file('SET003-0.ax',rotate_right2) ).
cnf(rotate_right3,axiom,
( little_set(f11(Z,X))
| ~ member(Z,rotate_right(X)) ),
file('SET003-0.ax',rotate_right3) ).
cnf(rotate_right4,axiom,
( Z = ordered_pair(f9(Z,X),ordered_pair(f10(Z,X),f11(Z,X)))
| ~ member(Z,rotate_right(X)) ),
file('SET003-0.ax',rotate_right4) ).
cnf(rotate_right5,axiom,
( member(ordered_pair(f10(Z,X),ordered_pair(f11(Z,X),f9(Z,X))),X)
| ~ member(Z,rotate_right(X)) ),
file('SET003-0.ax',rotate_right5) ).
cnf(rotate_right6,axiom,
( ~ member(ordered_pair(V,ordered_pair(W,U)),X)
| Z != ordered_pair(U,ordered_pair(V,W))
| ~ little_set(W)
| ~ little_set(V)
| ~ little_set(U)
| ~ little_set(Z)
| member(Z,rotate_right(X)) ),
file('SET003-0.ax',rotate_right6) ).
cnf(flip_range1,axiom,
( little_set(f12(Z,X))
| ~ member(Z,flip_range_of(X)) ),
file('SET003-0.ax',flip_range1) ).
cnf(flip_range2,axiom,
( little_set(f13(Z,X))
| ~ member(Z,flip_range_of(X)) ),
file('SET003-0.ax',flip_range2) ).
cnf(flip_range3,axiom,
( little_set(f14(Z,X))
| ~ member(Z,flip_range_of(X)) ),
file('SET003-0.ax',flip_range3) ).
cnf(flip_range4,axiom,
( Z = ordered_pair(f12(Z,X),ordered_pair(f13(Z,X),f14(Z,X)))
| ~ member(Z,flip_range_of(X)) ),
file('SET003-0.ax',flip_range4) ).
cnf(flip_range5,axiom,
( member(ordered_pair(f12(Z,X),ordered_pair(f14(Z,X),f13(Z,X))),X)
| ~ member(Z,flip_range_of(X)) ),
file('SET003-0.ax',flip_range5) ).
cnf(flip_range6,axiom,
( ~ member(ordered_pair(U,ordered_pair(W,V)),X)
| Z != ordered_pair(U,ordered_pair(V,W))
| ~ little_set(W)
| ~ little_set(V)
| ~ little_set(U)
| ~ little_set(Z)
| member(Z,flip_range_of(X)) ),
file('SET003-0.ax',flip_range6) ).
cnf(successor,axiom,
successor(X) = union(X,singleton_set(X)),
file('SET003-0.ax',successor) ).
cnf(empty_set,axiom,
~ member(Z,empty_set),
file('SET003-0.ax',empty_set) ).
cnf(universal_set,axiom,
( ~ little_set(Z)
| member(Z,universal_set) ),
file('SET003-0.ax',universal_set) ).
cnf(infinity1,axiom,
little_set(infinity),
file('SET003-0.ax',infinity1) ).
cnf(infinity2,axiom,
member(empty_set,infinity),
file('SET003-0.ax',infinity2) ).
cnf(infinity3,axiom,
( member(successor(X),infinity)
| ~ member(X,infinity) ),
file('SET003-0.ax',infinity3) ).
cnf(sigma1,axiom,
( member(f16(Z,X),X)
| ~ member(Z,sigma(X)) ),
file('SET003-0.ax',sigma1) ).
cnf(sigma2,axiom,
( member(Z,f16(Z,X))
| ~ member(Z,sigma(X)) ),
file('SET003-0.ax',sigma2) ).
cnf(sigma3,axiom,
( ~ member(Z,Y)
| ~ member(Y,X)
| member(Z,sigma(X)) ),
file('SET003-0.ax',sigma3) ).
cnf(sigma4,axiom,
( little_set(sigma(U))
| ~ little_set(U) ),
file('SET003-0.ax',sigma4) ).
cnf(subset1,axiom,
( member(U,Y)
| ~ member(U,X)
| ~ subset(X,Y) ),
file('SET003-0.ax',subset1) ).
cnf(subset2,axiom,
( member(f17(X,Y),X)
| subset(X,Y) ),
file('SET003-0.ax',subset2) ).
cnf(subset3,axiom,
( ~ member(f17(X,Y),Y)
| subset(X,Y) ),
file('SET003-0.ax',subset3) ).
cnf(proper_subset1,axiom,
( subset(X,Y)
| ~ proper_subset(X,Y) ),
file('SET003-0.ax',proper_subset1) ).
cnf(proper_subset2,axiom,
( X != Y
| ~ proper_subset(X,Y) ),
file('SET003-0.ax',proper_subset2) ).
cnf(proper_subset3,axiom,
( X = Y
| ~ subset(X,Y)
| proper_subset(X,Y) ),
file('SET003-0.ax',proper_subset3) ).
cnf(powerset1,axiom,
( subset(Z,X)
| ~ member(Z,powerset(X)) ),
file('SET003-0.ax',powerset1) ).
cnf(powerset2,axiom,
( ~ subset(Z,X)
| ~ little_set(Z)
| member(Z,powerset(X)) ),
file('SET003-0.ax',powerset2) ).
cnf(powerset3,axiom,
( little_set(powerset(U))
| ~ little_set(U) ),
file('SET003-0.ax',powerset3) ).
cnf(relation1,axiom,
( ordered_pair_predicate(X)
| ~ member(X,Z)
| ~ relation(Z) ),
file('SET003-0.ax',relation1) ).
cnf(relation2,axiom,
( member(f18(Z),Z)
| relation(Z) ),
file('SET003-0.ax',relation2) ).
cnf(relation3,axiom,
( ~ ordered_pair_predicate(f18(Z))
| relation(Z) ),
file('SET003-0.ax',relation3) ).
cnf(single_valued_set1,axiom,
( V = W
| ~ member(ordered_pair(U,W),X)
| ~ member(ordered_pair(U,V),X)
| ~ little_set(W)
| ~ little_set(V)
| ~ little_set(U)
| ~ single_valued_set(X) ),
file('SET003-0.ax',single_valued_set1) ).
cnf(single_valued_set2,axiom,
( little_set(f19(X))
| single_valued_set(X) ),
file('SET003-0.ax',single_valued_set2) ).
cnf(single_valued_set3,axiom,
( little_set(f20(X))
| single_valued_set(X) ),
file('SET003-0.ax',single_valued_set3) ).
cnf(single_valued_set4,axiom,
( little_set(f21(X))
| single_valued_set(X) ),
file('SET003-0.ax',single_valued_set4) ).
cnf(single_valued_set5,axiom,
( member(ordered_pair(f19(X),f20(X)),X)
| single_valued_set(X) ),
file('SET003-0.ax',single_valued_set5) ).
cnf(single_valued_set6,axiom,
( member(ordered_pair(f19(X),f21(X)),X)
| single_valued_set(X) ),
file('SET003-0.ax',single_valued_set6) ).
cnf(single_valued_set7,axiom,
( f20(X) != f21(X)
| single_valued_set(X) ),
file('SET003-0.ax',single_valued_set7) ).
cnf(function1,axiom,
( relation(Xf)
| ~ function(Xf) ),
file('SET003-0.ax',function1) ).
cnf(function2,axiom,
( single_valued_set(Xf)
| ~ function(Xf) ),
file('SET003-0.ax',function2) ).
cnf(function3,axiom,
( ~ single_valued_set(Xf)
| ~ relation(Xf)
| function(Xf) ),
file('SET003-0.ax',function3) ).
cnf(image_and_substitution1,axiom,
( ordered_pair_predicate(f22(Z,X,Xf))
| ~ member(Z,image(X,Xf)) ),
file('SET003-0.ax',image_and_substitution1) ).
cnf(image_and_substitution2,axiom,
( member(f22(Z,X,Xf),Xf)
| ~ member(Z,image(X,Xf)) ),
file('SET003-0.ax',image_and_substitution2) ).
cnf(image_and_substitution3,axiom,
( member(first(f22(Z,X,Xf)),X)
| ~ member(Z,image(X,Xf)) ),
file('SET003-0.ax',image_and_substitution3) ).
cnf(image_and_substitution4,axiom,
( second(f22(Z,X,Xf)) = Z
| ~ member(Z,image(X,Xf)) ),
file('SET003-0.ax',image_and_substitution4) ).
cnf(image_and_substitution5,axiom,
( second(Y) != Z
| ~ member(first(Y),X)
| ~ member(Y,Xf)
| ~ ordered_pair_predicate(Y)
| ~ little_set(Z)
| member(Z,image(X,Xf)) ),
file('SET003-0.ax',image_and_substitution5) ).
cnf(image_and_substitution6,axiom,
( little_set(image(X,Xf))
| ~ function(Xf)
| ~ little_set(X) ),
file('SET003-0.ax',image_and_substitution6) ).
cnf(disjoint1,axiom,
( ~ member(U,Y)
| ~ member(U,X)
| ~ disjoint(X,Y) ),
file('SET003-0.ax',disjoint1) ).
cnf(disjoint2,axiom,
( member(f23(X,Y),X)
| disjoint(X,Y) ),
file('SET003-0.ax',disjoint2) ).
cnf(disjoint3,axiom,
( member(f23(X,Y),Y)
| disjoint(X,Y) ),
file('SET003-0.ax',disjoint3) ).
cnf(regularity1,axiom,
( member(f24(X),X)
| X = empty_set ),
file('SET003-0.ax',regularity1) ).
cnf(regularity2,axiom,
( disjoint(f24(X),X)
| X = empty_set ),
file('SET003-0.ax',regularity2) ).
cnf(choice1,axiom,
function(f25),
file('SET003-0.ax',choice1) ).
cnf(choice2,axiom,
( member(f26(X),X)
| X = empty_set
| ~ little_set(X) ),
file('SET003-0.ax',choice2) ).
cnf(choice3,axiom,
( member(ordered_pair(X,f26(X)),f25)
| X = empty_set
| ~ little_set(X) ),
file('SET003-0.ax',choice3) ).
cnf(range_of1,axiom,
( ordered_pair_predicate(f27(Z,X))
| ~ member(Z,range_of(X)) ),
file('SET003-0.ax',range_of1) ).
cnf(range_of2,axiom,
( member(f27(Z,X),X)
| ~ member(Z,range_of(X)) ),
file('SET003-0.ax',range_of2) ).
cnf(range_of3,axiom,
( Z = second(f27(Z,X))
| ~ member(Z,range_of(X)) ),
file('SET003-0.ax',range_of3) ).
cnf(range_of4,axiom,
( Z != second(Xp)
| ~ member(Xp,X)
| ~ ordered_pair_predicate(Xp)
| ~ little_set(Z)
| member(Z,range_of(X)) ),
file('SET003-0.ax',range_of4) ).
cnf(identity_relation1,axiom,
( ordered_pair_predicate(Z)
| ~ member(Z,identity_relation) ),
file('SET003-0.ax',identity_relation1) ).
cnf(identity_relation2,axiom,
( first(Z) = second(Z)
| ~ member(Z,identity_relation) ),
file('SET003-0.ax',identity_relation2) ).
cnf(identity_relation3,axiom,
( first(Z) != second(Z)
| ~ ordered_pair_predicate(Z)
| ~ little_set(Z)
| member(Z,identity_relation) ),
file('SET003-0.ax',identity_relation3) ).
cnf(restrict,axiom,
restrict(X,Y) = intersection(X,cross_product(Y,universal_set)),
file('SET003-0.ax',restrict) ).
cnf(one_to_one_function1,axiom,
( function(Xf)
| ~ one_to_one_function(Xf) ),
file('SET003-0.ax',one_to_one_function1) ).
cnf(one_to_one_function2,axiom,
( function(converse(Xf))
| ~ one_to_one_function(Xf) ),
file('SET003-0.ax',one_to_one_function2) ).
cnf(one_to_one_function3,axiom,
( ~ function(converse(Xf))
| ~ function(Xf)
| one_to_one_function(Xf) ),
file('SET003-0.ax',one_to_one_function3) ).
cnf(apply1,axiom,
( ordered_pair_predicate(f28(Z,Xf,Y))
| ~ member(Z,apply(Xf,Y)) ),
file('SET003-0.ax',apply1) ).
cnf(apply2,axiom,
( member(f28(Z,Xf,Y),Xf)
| ~ member(Z,apply(Xf,Y)) ),
file('SET003-0.ax',apply2) ).
cnf(apply3,axiom,
( first(f28(Z,Xf,Y)) = Y
| ~ member(Z,apply(Xf,Y)) ),
file('SET003-0.ax',apply3) ).
cnf(apply4,axiom,
( member(Z,second(f28(Z,Xf,Y)))
| ~ member(Z,apply(Xf,Y)) ),
file('SET003-0.ax',apply4) ).
cnf(apply5,axiom,
( ~ member(Z,second(W))
| first(W) != Y
| ~ member(W,Xf)
| ~ ordered_pair_predicate(W)
| member(Z,apply(Xf,Y)) ),
file('SET003-0.ax',apply5) ).
cnf(apply_to_two_arguments,axiom,
apply_to_two_arguments(Xf,X,Y) = apply(Xf,ordered_pair(X,Y)),
file('SET003-0.ax',apply_to_two_arguments) ).
cnf(maps1,axiom,
( function(Xf)
| ~ maps(Xf,X,Y) ),
file('SET003-0.ax',maps1) ).
cnf(maps2,axiom,
( domain_of(Xf) = X
| ~ maps(Xf,X,Y) ),
file('SET003-0.ax',maps2) ).
cnf(maps3,axiom,
( subset(range_of(Xf),Y)
| ~ maps(Xf,X,Y) ),
file('SET003-0.ax',maps3) ).
cnf(maps4,axiom,
( ~ subset(range_of(Xf),Y)
| domain_of(Xf) != X
| ~ function(Xf)
| maps(Xf,X,Y) ),
file('SET003-0.ax',maps4) ).
cnf(closed1,axiom,
( little_set(Xs)
| ~ closed(Xs,Xf) ),
file('SET003-0.ax',closed1) ).
cnf(closed2,axiom,
( little_set(Xf)
| ~ closed(Xs,Xf) ),
file('SET003-0.ax',closed2) ).
cnf(closed3,axiom,
( maps(Xf,cross_product(Xs,Xs),Xs)
| ~ closed(Xs,Xf) ),
file('SET003-0.ax',closed3) ).
cnf(closed4,axiom,
( ~ maps(Xf,cross_product(Xs,Xs),Xs)
| ~ little_set(Xf)
| ~ little_set(Xs)
| closed(Xs,Xf) ),
file('SET003-0.ax',closed4) ).
cnf(compose1,axiom,
( little_set(f29(Z,Xf,Xg))
| ~ member(Z,compose(Xf,Xg)) ),
file('SET003-0.ax',compose1) ).
cnf(compose2,axiom,
( little_set(f30(Z,Xf,Xg))
| ~ member(Z,compose(Xf,Xg)) ),
file('SET003-0.ax',compose2) ).
cnf(compose3,axiom,
( little_set(f31(Z,Xf,Xg))
| ~ member(Z,compose(Xf,Xg)) ),
file('SET003-0.ax',compose3) ).
cnf(compose4,axiom,
( Z = ordered_pair(f29(Z,Xf,Xg),f30(Z,Xf,Xg))
| ~ member(Z,compose(Xf,Xg)) ),
file('SET003-0.ax',compose4) ).
cnf(compose5,axiom,
( member(ordered_pair(f29(Z,Xf,Xg),f31(Z,Xf,Xg)),Xf)
| ~ member(Z,compose(Xf,Xg)) ),
file('SET003-0.ax',compose5) ).
cnf(compose6,axiom,
( member(ordered_pair(f31(Z,Xf,Xg),f30(Z,Xf,Xg)),Xg)
| ~ member(Z,compose(Xf,Xg)) ),
file('SET003-0.ax',compose6) ).
cnf(compose7,axiom,
( ~ member(ordered_pair(W,Y),Xg)
| ~ member(ordered_pair(X,W),Xf)
| Z != ordered_pair(X,Y)
| ~ little_set(W)
| ~ little_set(Y)
| ~ little_set(X)
| ~ little_set(Z)
| member(Z,compose(Xf,Xg)) ),
file('SET003-0.ax',compose7) ).
cnf(homomorphism1,axiom,
( closed(Xs1,Xf1)
| ~ homomorphism(Xh,Xs1,Xf1,Xs2,Xf2) ),
file('SET003-0.ax',homomorphism1) ).
cnf(homomorphism2,axiom,
( closed(Xs2,Xf2)
| ~ homomorphism(Xh,Xs1,Xf1,Xs2,Xf2) ),
file('SET003-0.ax',homomorphism2) ).
cnf(homomorphism3,axiom,
( maps(Xh,Xs1,Xs2)
| ~ homomorphism(Xh,Xs1,Xf1,Xs2,Xf2) ),
file('SET003-0.ax',homomorphism3) ).
cnf(homomorphism4,axiom,
( apply(Xh,apply_to_two_arguments(Xf1,X,Y)) = apply_to_two_arguments(Xf2,apply(Xh,X),apply(Xh,Y))
| ~ member(Y,Xs1)
| ~ member(X,Xs1)
| ~ homomorphism(Xh,Xs1,Xf1,Xs2,Xf2) ),
file('SET003-0.ax',homomorphism4) ).
cnf(homomorphism5,axiom,
( member(f32(Xh,Xs1,Xf1,Xs2,Xf2),Xs1)
| ~ maps(Xh,Xs1,Xs2)
| ~ closed(Xs2,Xf2)
| ~ closed(Xs1,Xf1)
| homomorphism(Xh,Xs1,Xf1,Xs2,Xf2) ),
file('SET003-0.ax',homomorphism5) ).
cnf(homomorphism6,axiom,
( member(f33(Xh,Xs1,Xf1,Xs2,Xf2),Xs1)
| ~ maps(Xh,Xs1,Xs2)
| ~ closed(Xs2,Xf2)
| ~ closed(Xs1,Xf1)
| homomorphism(Xh,Xs1,Xf1,Xs2,Xf2) ),
file('SET003-0.ax',homomorphism6) ).
cnf(homomorphism7,axiom,
( apply(Xh,apply_to_two_arguments(Xf1,f32(Xh,Xs1,Xf1,Xs2,Xf2),f33(Xh,Xs1,Xf1,Xs2,Xf2))) != apply_to_two_arguments(Xf2,apply(Xh,f32(Xh,Xs1,Xf1,Xs2,Xf2)),apply(Xh,f33(Xh,Xs1,Xf1,Xs2,Xf2)))
| ~ maps(Xh,Xs1,Xs2)
| ~ closed(Xs2,Xf2)
| ~ closed(Xs1,Xf1)
| homomorphism(Xh,Xs1,Xf1,Xs2,Xf2) ),
file('SET003-0.ax',homomorphism7) ).
cnf(first_components_are_equal,axiom,
( X = U
| ordered_pair(X,Y) != ordered_pair(U,V)
| ~ little_set(U)
| ~ little_set(X) ),
file('theBenchmark.p',first_components_are_equal) ).
cnf(left_cancellation,axiom,
( X = Y
| non_ordered_pair(Z,X) != non_ordered_pair(Z,Y)
| ~ little_set(Y)
| ~ little_set(X) ),
file('theBenchmark.p',left_cancellation) ).
cnf(second_components_are_equal,axiom,
( Y = V
| ordered_pair(X,Y) != ordered_pair(U,V)
| ~ little_set(V)
| ~ little_set(U)
| ~ little_set(Y)
| ~ little_set(X) ),
file('theBenchmark.p',second_components_are_equal) ).
cnf(two_sets_equal,axiom,
( X = Y
| ~ subset(Y,X)
| ~ subset(X,Y) ),
file('theBenchmark.p',two_sets_equal) ).
cnf(property_of_first,axiom,
( first(ordered_pair(X,Y)) = X
| ~ little_set(Y)
| ~ little_set(X) ),
file('theBenchmark.p',property_of_first) ).
cnf(a_little_set,hypothesis,
little_set(a),
file('theBenchmark.p',a_little_set) ).
cnf(b_little_set,hypothesis,
little_set(b),
file('theBenchmark.p',b_little_set) ).
cnf(prove_second_is_second,negated_conjecture,
second(ordered_pair(a,b)) != b,
file('theBenchmark.p',prove_second_is_second) ).
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,
( f1(Eq_x_0,Eq_x_1) = f1(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,
( non_ordered_pair(Eq_x_0,Eq_x_1) = non_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_6,axiom,
( singleton_set(Eq_x_0) = singleton_set(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,
( f2(Eq_x_0) = f2(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_9,axiom,
( f3(Eq_x_0) = f3(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_10,axiom,
( first(Eq_x_0) = first(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_11,axiom,
( f4(Eq_x_0,Eq_x_1) = f4(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,
( f5(Eq_x_0,Eq_x_1) = f5(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_13,axiom,
( second(Eq_x_0) = second(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_14,axiom,
( f6(Eq_x_0,Eq_x_1) = f6(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,
( f7(Eq_x_0,Eq_x_1) = f7(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_16,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_17,axiom,
( complement(Eq_x_0) = complement(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_18,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_19,axiom,
( domain_of(Eq_x_0) = domain_of(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_20,axiom,
( f8(Eq_x_0,Eq_x_1) = f8(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_21,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_22,axiom,
( converse(Eq_x_0) = converse(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_23,axiom,
( rotate_right(Eq_x_0) = rotate_right(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_24,axiom,
( f9(Eq_x_0,Eq_x_1) = f9(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_25,axiom,
( f10(Eq_x_0,Eq_x_1) = f10(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_26,axiom,
( f11(Eq_x_0,Eq_x_1) = f11(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_27,axiom,
( flip_range_of(Eq_x_0) = flip_range_of(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_28,axiom,
( f12(Eq_x_0,Eq_x_1) = f12(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_29,axiom,
( f13(Eq_x_0,Eq_x_1) = f13(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,
( f14(Eq_x_0,Eq_x_1) = f14(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_31,axiom,
( successor(Eq_x_0) = successor(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_32,axiom,
( sigma(Eq_x_0) = sigma(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_33,axiom,
( f16(Eq_x_0,Eq_x_1) = f16(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_34,axiom,
( f17(Eq_x_0,Eq_x_1) = f17(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_35,axiom,
( powerset(Eq_x_0) = powerset(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_36,axiom,
( f18(Eq_x_0) = f18(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_37,axiom,
( f19(Eq_x_0) = f19(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_38,axiom,
( f20(Eq_x_0) = f20(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_39,axiom,
( f21(Eq_x_0) = f21(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_40,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_41,axiom,
( f22(Eq_x_0,Eq_x_1,Eq_x_2) = f22(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_42,axiom,
( f23(Eq_x_0,Eq_x_1) = f23(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_43,axiom,
( f24(Eq_x_0) = f24(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_44,axiom,
( f26(Eq_x_0) = f26(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_45,axiom,
( range_of(Eq_x_0) = range_of(Eq_y_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_46,axiom,
( f27(Eq_x_0,Eq_x_1) = f27(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,
( restrict(Eq_x_0,Eq_x_1) = restrict(Eq_y_0,Eq_y_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_48,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_49,axiom,
( f28(Eq_x_0,Eq_x_1,Eq_x_2) = f28(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_50,axiom,
( apply_to_two_arguments(Eq_x_0,Eq_x_1,Eq_x_2) = apply_to_two_arguments(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_51,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_52,axiom,
( f29(Eq_x_0,Eq_x_1,Eq_x_2) = f29(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_53,axiom,
( f30(Eq_x_0,Eq_x_1,Eq_x_2) = f30(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_54,axiom,
( f31(Eq_x_0,Eq_x_1,Eq_x_2) = f31(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_55,axiom,
( f32(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3,Eq_x_4) = f32(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3,Eq_y_4)
| Eq_x_4 != Eq_y_4
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_56,axiom,
( f33(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3,Eq_x_4) = f33(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3,Eq_y_4)
| Eq_x_4 != Eq_y_4
| Eq_x_3 != Eq_y_3
| Eq_x_2 != Eq_y_2
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_functions]) ).
cnf(equality_57,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_58,axiom,
( little_set(Eq_y_0)
| ~ little_set(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_59,axiom,
( ordered_pair_predicate(Eq_y_0)
| ~ ordered_pair_predicate(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_60,axiom,
( subset(Eq_y_0,Eq_y_1)
| ~ subset(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,
( proper_subset(Eq_y_0,Eq_y_1)
| ~ proper_subset(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,
( relation(Eq_y_0)
| ~ relation(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_63,axiom,
( single_valued_set(Eq_y_0)
| ~ single_valued_set(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_64,axiom,
( function(Eq_y_0)
| ~ function(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_65,axiom,
( disjoint(Eq_y_0,Eq_y_1)
| ~ disjoint(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_66,axiom,
( one_to_one_function(Eq_y_0)
| ~ one_to_one_function(Eq_x_0)
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_67,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_68,axiom,
( closed(Eq_y_0,Eq_y_1)
| ~ closed(Eq_x_0,Eq_x_1)
| Eq_x_1 != Eq_y_1
| Eq_x_0 != Eq_y_0 ),
theory(equality,[substitution_predicates]) ).
cnf(equality_69,axiom,
( homomorphism(Eq_y_0,Eq_y_1,Eq_y_2,Eq_y_3,Eq_y_4)
| ~ homomorphism(Eq_x_0,Eq_x_1,Eq_x_2,Eq_x_3,Eq_x_4)
| Eq_x_4 != Eq_y_4
| Eq_x_3 != Eq_y_3
| 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 : SET021-3 : TPTP v9.3.1. Released v1.0.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.12/10.40 % Computer : n013.cluster.edu
% 0.12/10.40 % Model : x86_64 x86_64
% 0.12/10.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/10.40 % Memory : 8046.5625MB
% 0.12/10.40 % OS : Linux 6.8.0-71-generic
% 0.12/10.40 % CPULimit : 300
% 0.12/10.40 % WCLimit : 300
% 0.12/10.40 % DateTime : Sat Sep 19 21:29:04 UTC 2026
% 0.12/10.40 % CPUTime :
% 150.32/160.69 % SZS status Unsatisfiable for theBenchmark
% 150.32/160.69 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------