%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SET024-4 : TPTP v9.2.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n027.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 05:06:55 PM UTC 2026
% Result : Unsatisfiable 0.36s 1.61s
% Output : CNFRefutation 0.36s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named c_0_143)
% Comments :
%------------------------------------------------------------------------------
cnf(ordered_pair,axiom,
ordered_pair(X1,X2) = non_ordered_pair(singleton_set(X1),non_ordered_pair(X1,X2)),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',ordered_pair) ).
cnf(singleton_set,axiom,
singleton_set(X1) = non_ordered_pair(X1,X1),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',singleton_set) ).
cnf(successor,axiom,
successor(X1) = union(X1,singleton_set(X1)),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',successor) ).
cnf(homomorphism7,axiom,
( homomorphism(X1,X2,X3,X4,X5)
| ~ closed(X2,X3)
| ~ closed(X4,X5)
| ~ maps(X1,X2,X4)
| apply(X1,apply_to_two_arguments(X3,f32(X1,X2,X3,X4,X5),f33(X1,X2,X3,X4,X5))) != apply_to_two_arguments(X5,apply(X1,f32(X1,X2,X3,X4,X5)),apply(X1,f33(X1,X2,X3,X4,X5))) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',homomorphism7) ).
cnf(apply_to_two_arguments,axiom,
apply_to_two_arguments(X1,X2,X3) = apply(X1,ordered_pair(X2,X3)),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',apply_to_two_arguments) ).
cnf(homomorphism4,axiom,
( apply(X1,apply_to_two_arguments(X3,X6,X7)) = apply_to_two_arguments(X5,apply(X1,X6),apply(X1,X7))
| ~ homomorphism(X1,X2,X3,X4,X5)
| ~ member(X6,X2)
| ~ member(X7,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',homomorphism4) ).
cnf(flip_range5,axiom,
( member(ordered_pair(f12(X1,X2),ordered_pair(f14(X1,X2),f13(X1,X2))),X2)
| ~ member(X1,flip_range_of(X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',flip_range5) ).
cnf(rotate_right5,axiom,
( member(ordered_pair(f10(X1,X2),ordered_pair(f11(X1,X2),f9(X1,X2))),X2)
| ~ member(X1,rotate_right(X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',rotate_right5) ).
cnf(compose6,axiom,
( member(ordered_pair(f31(X1,X2,X3),f30(X1,X2,X3)),X3)
| ~ member(X1,compose(X2,X3)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',compose6) ).
cnf(compose5,axiom,
( member(ordered_pair(f29(X1,X2,X3),f31(X1,X2,X3)),X2)
| ~ member(X1,compose(X2,X3)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',compose5) ).
cnf(flip_range6,axiom,
( member(X1,flip_range_of(X2))
| ~ little_set(X1)
| ~ little_set(X3)
| ~ little_set(X4)
| ~ little_set(X5)
| X1 != ordered_pair(X3,ordered_pair(X4,X5))
| ~ member(ordered_pair(X3,ordered_pair(X5,X4)),X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',flip_range6) ).
cnf(rotate_right6,axiom,
( member(X1,rotate_right(X2))
| ~ little_set(X1)
| ~ little_set(X3)
| ~ little_set(X4)
| ~ little_set(X5)
| X1 != ordered_pair(X3,ordered_pair(X4,X5))
| ~ member(ordered_pair(X4,ordered_pair(X5,X3)),X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',rotate_right6) ).
cnf(flip_range4,axiom,
( X1 = ordered_pair(f12(X1,X2),ordered_pair(f13(X1,X2),f14(X1,X2)))
| ~ member(X1,flip_range_of(X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',flip_range4) ).
cnf(rotate_right4,axiom,
( X1 = ordered_pair(f9(X1,X2),ordered_pair(f10(X1,X2),f11(X1,X2)))
| ~ member(X1,rotate_right(X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',rotate_right4) ).
cnf(compose4,axiom,
( X1 = ordered_pair(f29(X1,X2,X3),f30(X1,X2,X3))
| ~ member(X1,compose(X2,X3)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',compose4) ).
cnf(compose7,axiom,
( member(X1,compose(X2,X3))
| ~ little_set(X1)
| ~ little_set(X4)
| ~ little_set(X5)
| ~ little_set(X6)
| X1 != ordered_pair(X4,X5)
| ~ member(ordered_pair(X4,X6),X2)
| ~ member(ordered_pair(X6,X5),X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',compose7) ).
cnf(single_valued_set1,axiom,
( X3 = X4
| ~ single_valued_set(X1)
| ~ little_set(X2)
| ~ little_set(X3)
| ~ little_set(X4)
| ~ member(ordered_pair(X2,X3),X1)
| ~ member(ordered_pair(X2,X4),X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',single_valued_set1) ).
cnf(converse3,axiom,
( member(X1,converse(X2))
| ~ little_set(X1)
| ~ ordered_pair_predicate(X1)
| ~ member(ordered_pair(second(X1),first(X1)),X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',converse3) ).
cnf(infinity3,axiom,
( member(successor(X1),infinity)
| ~ member(X1,infinity) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',infinity3) ).
cnf(union,axiom,
union(X1,X2) = complement(intersection(complement(X1),complement(X2))),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',union) ).
cnf(second3,axiom,
( X2 = ordered_pair(f6(X1,X2),f7(X1,X2))
| ~ member(X1,second(X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',second3) ).
cnf(first3,axiom,
( X2 = ordered_pair(f4(X1,X2),f5(X1,X2))
| ~ member(X1,first(X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',first3) ).
cnf(converse2,axiom,
( member(ordered_pair(second(X1),first(X1)),X2)
| ~ member(X1,converse(X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',converse2) ).
cnf(single_valued_set6,axiom,
( single_valued_set(X1)
| member(ordered_pair(f19(X1),f21(X1)),X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',single_valued_set6) ).
cnf(single_valued_set5,axiom,
( single_valued_set(X1)
| member(ordered_pair(f19(X1),f20(X1)),X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',single_valued_set5) ).
cnf(choice3,axiom,
( X1 = empty_set
| member(ordered_pair(X1,f26(X1)),f25)
| ~ little_set(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',choice3) ).
cnf(second5,axiom,
( member(X1,second(X2))
| ~ little_set(X3)
| ~ little_set(X4)
| X2 != ordered_pair(X3,X4)
| ~ member(X1,X4) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',second5) ).
cnf(first5,axiom,
( member(X1,first(X2))
| ~ little_set(X3)
| ~ little_set(X4)
| X2 != ordered_pair(X3,X4)
| ~ member(X1,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',first5) ).
cnf(ordered_pair_predicate4,axiom,
( ordered_pair_predicate(X1)
| ~ little_set(X2)
| ~ little_set(X3)
| X1 != ordered_pair(X2,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',ordered_pair_predicate4) ).
cnf(ordered_pair_predicate3,axiom,
( X1 = ordered_pair(f2(X1),f3(X1))
| ~ ordered_pair_predicate(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',ordered_pair_predicate3) ).
cnf(prove_membership_of_singleton_set,negated_conjecture,
~ member(a,singleton_set(a)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_membership_of_singleton_set) ).
cnf(homomorphism6,axiom,
( homomorphism(X1,X2,X3,X4,X5)
| member(f33(X1,X2,X3,X4,X5),X2)
| ~ closed(X2,X3)
| ~ closed(X4,X5)
| ~ maps(X1,X2,X4) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',homomorphism6) ).
cnf(homomorphism5,axiom,
( homomorphism(X1,X2,X3,X4,X5)
| member(f32(X1,X2,X3,X4,X5),X2)
| ~ closed(X2,X3)
| ~ closed(X4,X5)
| ~ maps(X1,X2,X4) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',homomorphism5) ).
cnf(homomorphism3,axiom,
( maps(X1,X2,X4)
| ~ homomorphism(X1,X2,X3,X4,X5) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',homomorphism3) ).
cnf(homomorphism1,axiom,
( closed(X2,X3)
| ~ homomorphism(X1,X2,X3,X4,X5) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',homomorphism1) ).
cnf(homomorphism2,axiom,
( closed(X4,X5)
| ~ homomorphism(X1,X2,X3,X4,X5) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',homomorphism2) ).
cnf(image_and_substitution3,axiom,
( member(first(f22(X1,X2,X3)),X2)
| ~ member(X1,image(X2,X3)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',image_and_substitution3) ).
cnf(apply4,axiom,
( member(X1,second(f28(X1,X2,X3)))
| ~ member(X1,apply(X2,X3)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',apply4) ).
cnf(apply2,axiom,
( member(f28(X1,X2,X3),X2)
| ~ member(X1,apply(X2,X3)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',apply2) ).
cnf(image_and_substitution2,axiom,
( member(f22(X1,X2,X3),X3)
| ~ member(X1,image(X2,X3)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',image_and_substitution2) ).
cnf(image_and_substitution4,axiom,
( second(f22(X1,X2,X3)) = X1
| ~ member(X1,image(X2,X3)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',image_and_substitution4) ).
cnf(apply3,axiom,
( first(f28(X1,X2,X3)) = X3
| ~ member(X1,apply(X2,X3)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',apply3) ).
cnf(apply1,axiom,
( ordered_pair_predicate(f28(X1,X2,X3))
| ~ member(X1,apply(X2,X3)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',apply1) ).
cnf(image_and_substitution1,axiom,
( ordered_pair_predicate(f22(X1,X2,X3))
| ~ member(X1,image(X2,X3)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',image_and_substitution1) ).
cnf(compose3,axiom,
( little_set(f31(X1,X2,X3))
| ~ member(X1,compose(X2,X3)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',compose3) ).
cnf(compose2,axiom,
( little_set(f30(X1,X2,X3))
| ~ member(X1,compose(X2,X3)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',compose2) ).
cnf(compose1,axiom,
( little_set(f29(X1,X2,X3))
| ~ member(X1,compose(X2,X3)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',compose1) ).
cnf(closed4,axiom,
( closed(X1,X2)
| ~ little_set(X1)
| ~ little_set(X2)
| ~ maps(X2,cross_product(X1,X1),X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',closed4) ).
cnf(extensionality3,axiom,
( X1 = X2
| ~ member(f1(X1,X2),X1)
| ~ member(f1(X1,X2),X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',extensionality3) ).
cnf(cross_product4,axiom,
( member(X1,cross_product(X2,X3))
| ~ little_set(X1)
| ~ ordered_pair_predicate(X1)
| ~ member(first(X1),X2)
| ~ member(second(X1),X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',cross_product4) ).
cnf(image_and_substitution5,axiom,
( member(X1,image(X2,X3))
| ~ little_set(X1)
| ~ ordered_pair_predicate(X4)
| ~ member(X4,X3)
| ~ member(first(X4),X2)
| second(X4) != X1 ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',image_and_substitution5) ).
cnf(apply5,axiom,
( member(X1,apply(X2,X3))
| ~ ordered_pair_predicate(X4)
| ~ member(X4,X2)
| first(X4) != X3
| ~ member(X1,second(X4)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',apply5) ).
cnf(maps3,axiom,
( subset(range_of(X1),X3)
| ~ maps(X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',maps3) ).
cnf(closed3,axiom,
( maps(X2,cross_product(X1,X1),X1)
| ~ closed(X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',closed3) ).
cnf(maps4,axiom,
( maps(X1,X2,X3)
| ~ function(X1)
| domain_of(X1) != X2
| ~ subset(range_of(X1),X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',maps4) ).
cnf(maps2,axiom,
( domain_of(X1) = X2
| ~ maps(X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',maps2) ).
cnf(maps1,axiom,
( function(X1)
| ~ maps(X1,X2,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',maps1) ).
cnf(intersection3,axiom,
( member(X1,intersection(X2,X3))
| ~ member(X1,X2)
| ~ member(X1,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',intersection3) ).
cnf(cross_product3,axiom,
( member(second(X1),X3)
| ~ member(X1,cross_product(X2,X3)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',cross_product3) ).
cnf(cross_product2,axiom,
( member(first(X1),X2)
| ~ member(X1,cross_product(X2,X3)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',cross_product2) ).
cnf(extensionality2,axiom,
( member(f1(X1,X2),X1)
| member(f1(X1,X2),X2)
| X1 = X2 ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',extensionality2) ).
cnf(subset3,axiom,
( subset(X1,X2)
| ~ member(f17(X1,X2),X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',subset3) ).
cnf(intersection1,axiom,
( member(X1,X2)
| ~ member(X1,intersection(X2,X3)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',intersection1) ).
cnf(intersection2,axiom,
( member(X1,X3)
| ~ member(X1,intersection(X2,X3)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',intersection2) ).
cnf(range_of2,axiom,
( member(f27(X1,X2),X2)
| ~ member(X1,range_of(X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',range_of2) ).
cnf(sigma1,axiom,
( member(f16(X1,X2),X2)
| ~ member(X1,sigma(X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',sigma1) ).
cnf(domain2,axiom,
( member(f8(X1,X2),X2)
| ~ member(X1,domain_of(X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',domain2) ).
cnf(sigma2,axiom,
( member(X1,f16(X1,X2))
| ~ member(X1,sigma(X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',sigma2) ).
cnf(second4,axiom,
( member(X1,f7(X1,X2))
| ~ member(X1,second(X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',second4) ).
cnf(first4,axiom,
( member(X1,f4(X1,X2))
| ~ member(X1,first(X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',first4) ).
cnf(element_relation3,axiom,
( member(X1,estin)
| ~ little_set(X1)
| ~ ordered_pair_predicate(X1)
| ~ member(first(X1),second(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',element_relation3) ).
cnf(disjoint1,axiom,
( ~ disjoint(X1,X2)
| ~ member(X3,X1)
| ~ member(X3,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',disjoint1) ).
cnf(non_ordered_pair1,axiom,
( X1 = X2
| X1 = X3
| ~ member(X1,non_ordered_pair(X2,X3)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',non_ordered_pair1) ).
cnf(cross_product1,axiom,
( ordered_pair_predicate(X1)
| ~ member(X1,cross_product(X2,X3)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',cross_product1) ).
cnf(range_of4,axiom,
( member(X1,range_of(X2))
| ~ little_set(X1)
| ~ ordered_pair_predicate(X3)
| ~ member(X3,X2)
| X1 != second(X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',range_of4) ).
cnf(domain4,axiom,
( member(X1,domain_of(X2))
| ~ little_set(X1)
| ~ ordered_pair_predicate(X3)
| ~ member(X3,X2)
| X1 != first(X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',domain4) ).
cnf(sigma3,axiom,
( member(X1,sigma(X2))
| ~ member(X3,X2)
| ~ member(X1,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',sigma3) ).
cnf(range_of3,axiom,
( X1 = second(f27(X1,X2))
| ~ member(X1,range_of(X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',range_of3) ).
cnf(domain3,axiom,
( X1 = first(f8(X1,X2))
| ~ member(X1,domain_of(X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',domain3) ).
cnf(range_of1,axiom,
( ordered_pair_predicate(f27(X1,X2))
| ~ member(X1,range_of(X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',range_of1) ).
cnf(domain1,axiom,
( ordered_pair_predicate(f8(X1,X2))
| ~ member(X1,domain_of(X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',domain1) ).
cnf(flip_range3,axiom,
( little_set(f14(X1,X2))
| ~ member(X1,flip_range_of(X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',flip_range3) ).
cnf(flip_range2,axiom,
( little_set(f13(X1,X2))
| ~ member(X1,flip_range_of(X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',flip_range2) ).
cnf(flip_range1,axiom,
( little_set(f12(X1,X2))
| ~ member(X1,flip_range_of(X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',flip_range1) ).
cnf(rotate_right3,axiom,
( little_set(f11(X1,X2))
| ~ member(X1,rotate_right(X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',rotate_right3) ).
cnf(rotate_right2,axiom,
( little_set(f10(X1,X2))
| ~ member(X1,rotate_right(X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',rotate_right2) ).
cnf(rotate_right1,axiom,
( little_set(f9(X1,X2))
| ~ member(X1,rotate_right(X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',rotate_right1) ).
cnf(second2,axiom,
( little_set(f7(X1,X2))
| ~ member(X1,second(X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',second2) ).
cnf(second1,axiom,
( little_set(f6(X1,X2))
| ~ member(X1,second(X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',second1) ).
cnf(first2,axiom,
( little_set(f5(X1,X2))
| ~ member(X1,first(X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',first2) ).
cnf(first1,axiom,
( little_set(f4(X1,X2))
| ~ member(X1,first(X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',first1) ).
cnf(subset1,axiom,
( member(X3,X2)
| ~ subset(X1,X2)
| ~ member(X3,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',subset1) ).
cnf(complement1,axiom,
( ~ member(X1,complement(X2))
| ~ member(X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',complement1) ).
cnf(disjoint2,axiom,
( disjoint(X1,X2)
| member(f23(X1,X2),X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',disjoint2) ).
cnf(disjoint3,axiom,
( disjoint(X1,X2)
| member(f23(X1,X2),X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',disjoint3) ).
cnf(subset2,axiom,
( subset(X1,X2)
| member(f17(X1,X2),X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',subset2) ).
cnf(non_ordered_pair2,axiom,
( member(X1,non_ordered_pair(X2,X3))
| ~ little_set(X1)
| X1 != X2 ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',non_ordered_pair2) ).
cnf(non_ordered_pair3,axiom,
( member(X1,non_ordered_pair(X2,X3))
| ~ little_set(X1)
| X1 != X3 ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',non_ordered_pair3) ).
cnf(powerset2,axiom,
( member(X1,powerset(X2))
| ~ little_set(X1)
| ~ subset(X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',powerset2) ).
cnf(element_relation2,axiom,
( member(first(X1),second(X1))
| ~ member(X1,estin) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',element_relation2) ).
cnf(powerset1,axiom,
( subset(X1,X2)
| ~ member(X1,powerset(X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',powerset1) ).
cnf(image_and_substitution6,axiom,
( little_set(image(X1,X2))
| ~ little_set(X1)
| ~ function(X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',image_and_substitution6) ).
cnf(complement2,axiom,
( member(X1,complement(X2))
| member(X1,X2)
| ~ little_set(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',complement2) ).
cnf(identity_relation3,axiom,
( member(X1,identity_relation)
| ~ little_set(X1)
| ~ ordered_pair_predicate(X1)
| first(X1) != second(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',identity_relation3) ).
cnf(proper_subset3,axiom,
( proper_subset(X1,X2)
| X1 = X2
| ~ subset(X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',proper_subset3) ).
cnf(proper_subset1,axiom,
( subset(X1,X2)
| ~ proper_subset(X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',proper_subset1) ).
cnf(converse1,axiom,
( ordered_pair_predicate(X1)
| ~ member(X1,converse(X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',converse1) ).
cnf(relation1,axiom,
( ordered_pair_predicate(X2)
| ~ relation(X1)
| ~ member(X2,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',relation1) ).
cnf(extensionality1,axiom,
( little_set(f1(X1,X2))
| X1 = X2 ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',extensionality1) ).
cnf(non_ordered_pair4,axiom,
little_set(non_ordered_pair(X1,X2)),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',non_ordered_pair4) ).
cnf(choice2,axiom,
( X1 = empty_set
| member(f26(X1),X1)
| ~ little_set(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',choice2) ).
cnf(identity_relation2,axiom,
( first(X1) = second(X1)
| ~ member(X1,identity_relation) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',identity_relation2) ).
cnf(one_to_one_function3,axiom,
( one_to_one_function(X1)
| ~ function(X1)
| ~ function(converse(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',one_to_one_function3) ).
cnf(closed1,axiom,
( little_set(X1)
| ~ closed(X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',closed1) ).
cnf(a2,axiom,
( little_set(X1)
| ~ member(X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',a2) ).
cnf(closed2,axiom,
( little_set(X2)
| ~ closed(X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',closed2) ).
cnf(proper_subset2,axiom,
( ~ proper_subset(X1,X2)
| X1 != X2 ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',proper_subset2) ).
cnf(relation2,axiom,
( relation(X1)
| member(f18(X1),X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',relation2) ).
cnf(identity_relation1,axiom,
( ordered_pair_predicate(X1)
| ~ member(X1,identity_relation) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',identity_relation1) ).
cnf(element_relation1,axiom,
( ordered_pair_predicate(X1)
| ~ member(X1,estin) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',element_relation1) ).
cnf(regularity2,axiom,
( X1 = empty_set
| disjoint(f24(X1),X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',regularity2) ).
cnf(regularity1,axiom,
( X1 = empty_set
| member(f24(X1),X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',regularity1) ).
cnf(relation3,axiom,
( relation(X1)
| ~ ordered_pair_predicate(f18(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',relation3) ).
cnf(empty_set,axiom,
~ member(X1,empty_set),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',empty_set) ).
cnf(universal_set,axiom,
( member(X1,universal_set)
| ~ little_set(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',universal_set) ).
cnf(function3,axiom,
( function(X1)
| ~ relation(X1)
| ~ single_valued_set(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',function3) ).
cnf(one_to_one_function2,axiom,
( function(converse(X1))
| ~ one_to_one_function(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',one_to_one_function2) ).
cnf(powerset3,axiom,
( little_set(powerset(X1))
| ~ little_set(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',powerset3) ).
cnf(sigma4,axiom,
( little_set(sigma(X1))
| ~ little_set(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',sigma4) ).
cnf(ordered_pair_predicate2,axiom,
( little_set(f3(X1))
| ~ ordered_pair_predicate(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',ordered_pair_predicate2) ).
cnf(ordered_pair_predicate1,axiom,
( little_set(f2(X1))
| ~ ordered_pair_predicate(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',ordered_pair_predicate1) ).
cnf(single_valued_set7,axiom,
( single_valued_set(X1)
| f20(X1) != f21(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',single_valued_set7) ).
cnf(single_valued_set4,axiom,
( single_valued_set(X1)
| little_set(f21(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',single_valued_set4) ).
cnf(single_valued_set3,axiom,
( single_valued_set(X1)
| little_set(f20(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',single_valued_set3) ).
cnf(single_valued_set2,axiom,
( single_valued_set(X1)
| little_set(f19(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',single_valued_set2) ).
cnf(one_to_one_function1,axiom,
( function(X1)
| ~ one_to_one_function(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',one_to_one_function1) ).
cnf(function2,axiom,
( single_valued_set(X1)
| ~ function(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',function2) ).
cnf(function1,axiom,
( relation(X1)
| ~ function(X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',function1) ).
cnf(infinity2,axiom,
member(empty_set,infinity),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',infinity2) ).
cnf(choice1,axiom,
function(f25),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',choice1) ).
cnf(a_little_set,hypothesis,
little_set(a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_little_set) ).
cnf(infinity1,axiom,
little_set(infinity),
file('/export/starexec/sandbox/benchmark/Axioms/SET003-0.ax',infinity1) ).
cnf(i_0_142,axiom,
ordered_pair(X1,X2) = non_ordered_pair(singleton_set(X1),non_ordered_pair(X1,X2)),
ordered_pair ).
cnf(i_0_143,axiom,
singleton_set(X1) = non_ordered_pair(X1,X1),
singleton_set ).
cnf(i_0_144,axiom,
successor(X1) = union(X1,singleton_set(X1)),
successor ).
cnf(i_0_145,axiom,
( homomorphism(X1,X2,X3,X4,X5)
| ~ closed(X2,X3)
| ~ closed(X4,X5)
| ~ maps(X1,X2,X4)
| apply(X1,apply_to_two_arguments(X3,f32(X1,X2,X3,X4,X5),f33(X1,X2,X3,X4,X5))) != apply_to_two_arguments(X5,apply(X1,f32(X1,X2,X3,X4,X5)),apply(X1,f33(X1,X2,X3,X4,X5))) ),
homomorphism7 ).
cnf(i_0_146,axiom,
apply_to_two_arguments(X1,X2,X3) = apply(X1,ordered_pair(X2,X3)),
apply_to_two_arguments ).
cnf(i_0_147,plain,
ordered_pair(X1,X2) = non_ordered_pair(non_ordered_pair(X1,X1),non_ordered_pair(X1,X2)),
inference(rw,[status(thm)],[i_0_142,c_0_143]) ).
cnf(i_0_148,axiom,
( apply(X1,apply_to_two_arguments(X3,X6,X7)) = apply_to_two_arguments(X5,apply(X1,X6),apply(X1,X7))
| ~ homomorphism(X1,X2,X3,X4,X5)
| ~ member(X6,X2)
| ~ member(X7,X2) ),
homomorphism4 ).
cnf(i_0_149,axiom,
( member(ordered_pair(f12(X1,X2),ordered_pair(f14(X1,X2),f13(X1,X2))),X2)
| ~ member(X1,flip_range_of(X2)) ),
flip_range5 ).
cnf(i_0_150,axiom,
( member(ordered_pair(f10(X1,X2),ordered_pair(f11(X1,X2),f9(X1,X2))),X2)
| ~ member(X1,rotate_right(X2)) ),
rotate_right5 ).
cnf(i_0_151,axiom,
( member(ordered_pair(f31(X1,X2,X3),f30(X1,X2,X3)),X3)
| ~ member(X1,compose(X2,X3)) ),
compose6 ).
cnf(i_0_152,axiom,
( member(ordered_pair(f29(X1,X2,X3),f31(X1,X2,X3)),X2)
| ~ member(X1,compose(X2,X3)) ),
compose5 ).
cnf(i_0_153,axiom,
( member(X1,flip_range_of(X2))
| ~ little_set(X1)
| ~ little_set(X3)
| ~ little_set(X4)
| ~ little_set(X5)
| X1 != ordered_pair(X3,ordered_pair(X4,X5))
| ~ member(ordered_pair(X3,ordered_pair(X5,X4)),X2) ),
flip_range6 ).
cnf(i_0_154,axiom,
( member(X1,rotate_right(X2))
| ~ little_set(X1)
| ~ little_set(X3)
| ~ little_set(X4)
| ~ little_set(X5)
| X1 != ordered_pair(X3,ordered_pair(X4,X5))
| ~ member(ordered_pair(X4,ordered_pair(X5,X3)),X2) ),
rotate_right6 ).
cnf(i_0_155,axiom,
( X1 = ordered_pair(f12(X1,X2),ordered_pair(f13(X1,X2),f14(X1,X2)))
| ~ member(X1,flip_range_of(X2)) ),
flip_range4 ).
cnf(i_0_156,axiom,
( X1 = ordered_pair(f9(X1,X2),ordered_pair(f10(X1,X2),f11(X1,X2)))
| ~ member(X1,rotate_right(X2)) ),
rotate_right4 ).
cnf(i_0_157,axiom,
( X1 = ordered_pair(f29(X1,X2,X3),f30(X1,X2,X3))
| ~ member(X1,compose(X2,X3)) ),
compose4 ).
cnf(i_0_158,axiom,
( member(X1,compose(X2,X3))
| ~ little_set(X1)
| ~ little_set(X4)
| ~ little_set(X5)
| ~ little_set(X6)
| X1 != ordered_pair(X4,X5)
| ~ member(ordered_pair(X4,X6),X2)
| ~ member(ordered_pair(X6,X5),X3) ),
compose7 ).
cnf(i_0_159,axiom,
( X3 = X4
| ~ single_valued_set(X1)
| ~ little_set(X2)
| ~ little_set(X3)
| ~ little_set(X4)
| ~ member(ordered_pair(X2,X3),X1)
| ~ member(ordered_pair(X2,X4),X1) ),
single_valued_set1 ).
cnf(i_0_160,axiom,
( member(X1,converse(X2))
| ~ little_set(X1)
| ~ ordered_pair_predicate(X1)
| ~ member(ordered_pair(second(X1),first(X1)),X2) ),
converse3 ).
cnf(i_0_161,axiom,
( member(successor(X1),infinity)
| ~ member(X1,infinity) ),
infinity3 ).
cnf(i_0_162,plain,
successor(X1) = union(X1,non_ordered_pair(X1,X1)),
inference(rw,[status(thm)],[i_0_144,c_0_143]) ).
cnf(i_0_163,axiom,
union(X1,X2) = complement(intersection(complement(X1),complement(X2))),
union ).
cnf(i_0_164,axiom,
( X2 = ordered_pair(f6(X1,X2),f7(X1,X2))
| ~ member(X1,second(X2)) ),
second3 ).
cnf(i_0_165,axiom,
( X2 = ordered_pair(f4(X1,X2),f5(X1,X2))
| ~ member(X1,first(X2)) ),
first3 ).
cnf(i_0_166,axiom,
( member(ordered_pair(second(X1),first(X1)),X2)
| ~ member(X1,converse(X2)) ),
converse2 ).
cnf(i_0_167,axiom,
( single_valued_set(X1)
| member(ordered_pair(f19(X1),f21(X1)),X1) ),
single_valued_set6 ).
cnf(i_0_168,axiom,
( single_valued_set(X1)
| member(ordered_pair(f19(X1),f20(X1)),X1) ),
single_valued_set5 ).
cnf(i_0_169,axiom,
( X1 = empty_set
| member(ordered_pair(X1,f26(X1)),f25)
| ~ little_set(X1) ),
choice3 ).
cnf(i_0_170,axiom,
( member(X1,second(X2))
| ~ little_set(X3)
| ~ little_set(X4)
| X2 != ordered_pair(X3,X4)
| ~ member(X1,X4) ),
second5 ).
cnf(i_0_171,axiom,
( member(X1,first(X2))
| ~ little_set(X3)
| ~ little_set(X4)
| X2 != ordered_pair(X3,X4)
| ~ member(X1,X3) ),
first5 ).
cnf(i_0_172,axiom,
( ordered_pair_predicate(X1)
| ~ little_set(X2)
| ~ little_set(X3)
| X1 != ordered_pair(X2,X3) ),
ordered_pair_predicate4 ).
cnf(i_0_173,axiom,
( X1 = ordered_pair(f2(X1),f3(X1))
| ~ ordered_pair_predicate(X1) ),
ordered_pair_predicate3 ).
cnf(i_0_174,negated_conjecture,
~ member(a,singleton_set(a)),
prove_membership_of_singleton_set ).
cnf(i_0_175,plain,
( homomorphism(X1,X2,X3,X4,X5)
| apply(X1,apply(X3,non_ordered_pair(non_ordered_pair(f32(X1,X2,X3,X4,X5),f32(X1,X2,X3,X4,X5)),non_ordered_pair(f32(X1,X2,X3,X4,X5),f33(X1,X2,X3,X4,X5))))) != apply(X5,non_ordered_pair(non_ordered_pair(apply(X1,f32(X1,X2,X3,X4,X5)),apply(X1,f32(X1,X2,X3,X4,X5))),non_ordered_pair(apply(X1,f32(X1,X2,X3,X4,X5)),apply(X1,f33(X1,X2,X3,X4,X5)))))
| ~ closed(X4,X5)
| ~ closed(X2,X3)
| ~ maps(X1,X2,X4) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_145,c_0_146]),c_0_146]),c_0_147]),c_0_147]),
[final] ).
cnf(i_0_176,axiom,
( homomorphism(X1,X2,X3,X4,X5)
| member(f33(X1,X2,X3,X4,X5),X2)
| ~ closed(X2,X3)
| ~ closed(X4,X5)
| ~ maps(X1,X2,X4) ),
homomorphism6,
[final] ).
cnf(i_0_177,axiom,
( homomorphism(X1,X2,X3,X4,X5)
| member(f32(X1,X2,X3,X4,X5),X2)
| ~ closed(X2,X3)
| ~ closed(X4,X5)
| ~ maps(X1,X2,X4) ),
homomorphism5,
[final] ).
cnf(i_0_178,plain,
( apply(X1,apply(X3,non_ordered_pair(non_ordered_pair(X6,X6),non_ordered_pair(X6,X7)))) = apply(X5,non_ordered_pair(non_ordered_pair(apply(X1,X6),apply(X1,X6)),non_ordered_pair(apply(X1,X6),apply(X1,X7))))
| ~ member(X7,X2)
| ~ member(X6,X2)
| ~ homomorphism(X1,X2,X3,X4,X5) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_148,c_0_146]),c_0_146]),c_0_147]),c_0_147]),
[final] ).
cnf(i_0_179,plain,
( member(non_ordered_pair(non_ordered_pair(f12(X1,X2),f12(X1,X2)),non_ordered_pair(f12(X1,X2),non_ordered_pair(non_ordered_pair(f14(X1,X2),f14(X1,X2)),non_ordered_pair(f14(X1,X2),f13(X1,X2))))),X2)
| ~ member(X1,flip_range_of(X2)) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_149,c_0_147]),c_0_147]),
[final] ).
cnf(i_0_180,plain,
( member(non_ordered_pair(non_ordered_pair(f10(X1,X2),f10(X1,X2)),non_ordered_pair(f10(X1,X2),non_ordered_pair(non_ordered_pair(f11(X1,X2),f11(X1,X2)),non_ordered_pair(f11(X1,X2),f9(X1,X2))))),X2)
| ~ member(X1,rotate_right(X2)) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_150,c_0_147]),c_0_147]),
[final] ).
cnf(i_0_181,axiom,
( maps(X1,X2,X4)
| ~ homomorphism(X1,X2,X3,X4,X5) ),
homomorphism3,
[final] ).
cnf(i_0_182,plain,
( member(non_ordered_pair(non_ordered_pair(f31(X1,X2,X3),f31(X1,X2,X3)),non_ordered_pair(f31(X1,X2,X3),f30(X1,X2,X3))),X3)
| ~ member(X1,compose(X2,X3)) ),
inference(rw,[status(thm)],[i_0_151,c_0_147]),
[final] ).
cnf(i_0_183,plain,
( member(non_ordered_pair(non_ordered_pair(f29(X1,X2,X3),f29(X1,X2,X3)),non_ordered_pair(f29(X1,X2,X3),f31(X1,X2,X3))),X2)
| ~ member(X1,compose(X2,X3)) ),
inference(rw,[status(thm)],[i_0_152,c_0_147]),
[final] ).
cnf(i_0_184,axiom,
( closed(X2,X3)
| ~ homomorphism(X1,X2,X3,X4,X5) ),
homomorphism1,
[final] ).
cnf(i_0_185,axiom,
( closed(X4,X5)
| ~ homomorphism(X1,X2,X3,X4,X5) ),
homomorphism2,
[final] ).
cnf(i_0_186,plain,
( member(X1,flip_range_of(X2))
| X1 != non_ordered_pair(non_ordered_pair(X3,X3),non_ordered_pair(X3,non_ordered_pair(non_ordered_pair(X4,X4),non_ordered_pair(X4,X5))))
| ~ little_set(X5)
| ~ little_set(X4)
| ~ little_set(X3)
| ~ little_set(X1)
| ~ member(non_ordered_pair(non_ordered_pair(X3,X3),non_ordered_pair(X3,non_ordered_pair(non_ordered_pair(X5,X5),non_ordered_pair(X5,X4)))),X2) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_153,c_0_147]),c_0_147]),c_0_147]),c_0_147]),
[final] ).
cnf(i_0_187,plain,
( member(X1,rotate_right(X2))
| X1 != non_ordered_pair(non_ordered_pair(X3,X3),non_ordered_pair(X3,non_ordered_pair(non_ordered_pair(X4,X4),non_ordered_pair(X4,X5))))
| ~ little_set(X5)
| ~ little_set(X4)
| ~ little_set(X3)
| ~ little_set(X1)
| ~ member(non_ordered_pair(non_ordered_pair(X4,X4),non_ordered_pair(X4,non_ordered_pair(non_ordered_pair(X5,X5),non_ordered_pair(X5,X3)))),X2) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_154,c_0_147]),c_0_147]),c_0_147]),c_0_147]),
[final] ).
cnf(i_0_188,plain,
( X1 = non_ordered_pair(non_ordered_pair(f12(X1,X2),f12(X1,X2)),non_ordered_pair(f12(X1,X2),non_ordered_pair(non_ordered_pair(f13(X1,X2),f13(X1,X2)),non_ordered_pair(f13(X1,X2),f14(X1,X2)))))
| ~ member(X1,flip_range_of(X2)) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_155,c_0_147]),c_0_147]),
[final] ).
cnf(i_0_189,plain,
( X1 = non_ordered_pair(non_ordered_pair(f9(X1,X2),f9(X1,X2)),non_ordered_pair(f9(X1,X2),non_ordered_pair(non_ordered_pair(f10(X1,X2),f10(X1,X2)),non_ordered_pair(f10(X1,X2),f11(X1,X2)))))
| ~ member(X1,rotate_right(X2)) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_156,c_0_147]),c_0_147]),
[final] ).
cnf(i_0_190,plain,
( X1 = non_ordered_pair(non_ordered_pair(f29(X1,X2,X3),f29(X1,X2,X3)),non_ordered_pair(f29(X1,X2,X3),f30(X1,X2,X3)))
| ~ member(X1,compose(X2,X3)) ),
inference(rw,[status(thm)],[i_0_157,c_0_147]),
[final] ).
cnf(i_0_191,plain,
( member(X1,compose(X2,X3))
| X1 != non_ordered_pair(non_ordered_pair(X4,X4),non_ordered_pair(X4,X5))
| ~ little_set(X6)
| ~ little_set(X5)
| ~ little_set(X4)
| ~ little_set(X1)
| ~ member(non_ordered_pair(non_ordered_pair(X6,X6),non_ordered_pair(X6,X5)),X3)
| ~ member(non_ordered_pair(non_ordered_pair(X4,X4),non_ordered_pair(X4,X6)),X2) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_158,c_0_147]),c_0_147]),c_0_147]),
[final] ).
cnf(i_0_192,plain,
( X3 = X4
| ~ little_set(X4)
| ~ little_set(X3)
| ~ little_set(X2)
| ~ single_valued_set(X1)
| ~ member(non_ordered_pair(non_ordered_pair(X2,X2),non_ordered_pair(X2,X4)),X1)
| ~ member(non_ordered_pair(non_ordered_pair(X2,X2),non_ordered_pair(X2,X3)),X1) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_159,c_0_147]),c_0_147]),
[final] ).
cnf(i_0_193,plain,
( member(X1,converse(X2))
| ~ little_set(X1)
| ~ ordered_pair_predicate(X1)
| ~ member(non_ordered_pair(non_ordered_pair(second(X1),second(X1)),non_ordered_pair(second(X1),first(X1))),X2) ),
inference(rw,[status(thm)],[i_0_160,c_0_147]),
[final] ).
cnf(i_0_194,plain,
( member(complement(intersection(complement(X1),complement(non_ordered_pair(X1,X1)))),infinity)
| ~ member(X1,infinity) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_161,c_0_162]),c_0_163]),
[final] ).
cnf(i_0_195,plain,
( X2 = non_ordered_pair(non_ordered_pair(f6(X1,X2),f6(X1,X2)),non_ordered_pair(f6(X1,X2),f7(X1,X2)))
| ~ member(X1,second(X2)) ),
inference(rw,[status(thm)],[i_0_164,c_0_147]),
[final] ).
cnf(i_0_196,plain,
( X2 = non_ordered_pair(non_ordered_pair(f4(X1,X2),f4(X1,X2)),non_ordered_pair(f4(X1,X2),f5(X1,X2)))
| ~ member(X1,first(X2)) ),
inference(rw,[status(thm)],[i_0_165,c_0_147]),
[final] ).
cnf(i_0_197,axiom,
( member(first(f22(X1,X2,X3)),X2)
| ~ member(X1,image(X2,X3)) ),
image_and_substitution3,
[final] ).
cnf(i_0_198,axiom,
( member(X1,second(f28(X1,X2,X3)))
| ~ member(X1,apply(X2,X3)) ),
apply4,
[final] ).
cnf(i_0_199,plain,
( member(non_ordered_pair(non_ordered_pair(second(X1),second(X1)),non_ordered_pair(second(X1),first(X1))),X2)
| ~ member(X1,converse(X2)) ),
inference(rw,[status(thm)],[i_0_166,c_0_147]),
[final] ).
cnf(i_0_200,plain,
( single_valued_set(X1)
| member(non_ordered_pair(non_ordered_pair(f19(X1),f19(X1)),non_ordered_pair(f19(X1),f21(X1))),X1) ),
inference(rw,[status(thm)],[i_0_167,c_0_147]),
[final] ).
cnf(i_0_201,plain,
( single_valued_set(X1)
| member(non_ordered_pair(non_ordered_pair(f19(X1),f19(X1)),non_ordered_pair(f19(X1),f20(X1))),X1) ),
inference(rw,[status(thm)],[i_0_168,c_0_147]),
[final] ).
cnf(i_0_202,axiom,
( member(f28(X1,X2,X3),X2)
| ~ member(X1,apply(X2,X3)) ),
apply2,
[final] ).
cnf(i_0_203,axiom,
( member(f22(X1,X2,X3),X3)
| ~ member(X1,image(X2,X3)) ),
image_and_substitution2,
[final] ).
cnf(i_0_204,plain,
( X1 = empty_set
| member(non_ordered_pair(non_ordered_pair(X1,X1),non_ordered_pair(X1,f26(X1))),f25)
| ~ little_set(X1) ),
inference(rw,[status(thm)],[i_0_169,c_0_147]),
[final] ).
cnf(i_0_205,axiom,
( second(f22(X1,X2,X3)) = X1
| ~ member(X1,image(X2,X3)) ),
image_and_substitution4,
[final] ).
cnf(i_0_206,axiom,
( first(f28(X1,X2,X3)) = X3
| ~ member(X1,apply(X2,X3)) ),
apply3,
[final] ).
cnf(i_0_207,axiom,
( ordered_pair_predicate(f28(X1,X2,X3))
| ~ member(X1,apply(X2,X3)) ),
apply1,
[final] ).
cnf(i_0_208,axiom,
( ordered_pair_predicate(f22(X1,X2,X3))
| ~ member(X1,image(X2,X3)) ),
image_and_substitution1,
[final] ).
cnf(i_0_209,axiom,
( little_set(f31(X1,X2,X3))
| ~ member(X1,compose(X2,X3)) ),
compose3,
[final] ).
cnf(i_0_210,axiom,
( little_set(f30(X1,X2,X3))
| ~ member(X1,compose(X2,X3)) ),
compose2,
[final] ).
cnf(i_0_211,axiom,
( little_set(f29(X1,X2,X3))
| ~ member(X1,compose(X2,X3)) ),
compose1,
[final] ).
cnf(i_0_212,plain,
( member(X1,second(X2))
| X2 != non_ordered_pair(non_ordered_pair(X3,X3),non_ordered_pair(X3,X4))
| ~ little_set(X4)
| ~ little_set(X3)
| ~ member(X1,X4) ),
inference(rw,[status(thm)],[i_0_170,c_0_147]),
[final] ).
cnf(i_0_213,plain,
( member(X1,first(X2))
| X2 != non_ordered_pair(non_ordered_pair(X3,X3),non_ordered_pair(X3,X4))
| ~ little_set(X4)
| ~ little_set(X3)
| ~ member(X1,X3) ),
inference(rw,[status(thm)],[i_0_171,c_0_147]),
[final] ).
cnf(i_0_214,axiom,
( closed(X1,X2)
| ~ little_set(X1)
| ~ little_set(X2)
| ~ maps(X2,cross_product(X1,X1),X1) ),
closed4,
[final] ).
cnf(i_0_215,axiom,
( X1 = X2
| ~ member(f1(X1,X2),X1)
| ~ member(f1(X1,X2),X2) ),
extensionality3,
[final] ).
cnf(i_0_216,plain,
( ordered_pair_predicate(X1)
| X1 != non_ordered_pair(non_ordered_pair(X2,X2),non_ordered_pair(X2,X3))
| ~ little_set(X3)
| ~ little_set(X2) ),
inference(rw,[status(thm)],[i_0_172,c_0_147]),
[final] ).
cnf(i_0_217,plain,
( X1 = non_ordered_pair(non_ordered_pair(f2(X1),f2(X1)),non_ordered_pair(f2(X1),f3(X1)))
| ~ ordered_pair_predicate(X1) ),
inference(rw,[status(thm)],[i_0_173,c_0_147]),
[final] ).
cnf(i_0_218,axiom,
( member(X1,cross_product(X2,X3))
| ~ little_set(X1)
| ~ ordered_pair_predicate(X1)
| ~ member(first(X1),X2)
| ~ member(second(X1),X3) ),
cross_product4,
[final] ).
cnf(i_0_219,axiom,
( member(X1,image(X2,X3))
| ~ little_set(X1)
| ~ ordered_pair_predicate(X4)
| ~ member(X4,X3)
| ~ member(first(X4),X2)
| second(X4) != X1 ),
image_and_substitution5,
[final] ).
cnf(i_0_220,axiom,
( member(X1,apply(X2,X3))
| ~ ordered_pair_predicate(X4)
| ~ member(X4,X2)
| first(X4) != X3
| ~ member(X1,second(X4)) ),
apply5,
[final] ).
cnf(i_0_221,axiom,
( subset(range_of(X1),X3)
| ~ maps(X1,X2,X3) ),
maps3,
[final] ).
cnf(i_0_222,axiom,
( maps(X2,cross_product(X1,X1),X1)
| ~ closed(X1,X2) ),
closed3,
[final] ).
cnf(i_0_223,axiom,
( maps(X1,X2,X3)
| ~ function(X1)
| domain_of(X1) != X2
| ~ subset(range_of(X1),X3) ),
maps4,
[final] ).
cnf(i_0_224,axiom,
( domain_of(X1) = X2
| ~ maps(X1,X2,X3) ),
maps2,
[final] ).
cnf(i_0_225,axiom,
( function(X1)
| ~ maps(X1,X2,X3) ),
maps1,
[final] ).
cnf(i_0_226,axiom,
( member(X1,intersection(X2,X3))
| ~ member(X1,X2)
| ~ member(X1,X3) ),
intersection3,
[final] ).
cnf(i_0_227,axiom,
( member(second(X1),X3)
| ~ member(X1,cross_product(X2,X3)) ),
cross_product3,
[final] ).
cnf(i_0_228,axiom,
( member(first(X1),X2)
| ~ member(X1,cross_product(X2,X3)) ),
cross_product2,
[final] ).
cnf(i_0_229,axiom,
( member(f1(X1,X2),X1)
| member(f1(X1,X2),X2)
| X1 = X2 ),
extensionality2,
[final] ).
cnf(i_0_230,axiom,
( subset(X1,X2)
| ~ member(f17(X1,X2),X2) ),
subset3,
[final] ).
cnf(i_0_231,axiom,
( member(X1,X2)
| ~ member(X1,intersection(X2,X3)) ),
intersection1,
[final] ).
cnf(i_0_232,axiom,
( member(X1,X3)
| ~ member(X1,intersection(X2,X3)) ),
intersection2,
[final] ).
cnf(i_0_233,axiom,
( member(f27(X1,X2),X2)
| ~ member(X1,range_of(X2)) ),
range_of2,
[final] ).
cnf(i_0_234,axiom,
( member(f16(X1,X2),X2)
| ~ member(X1,sigma(X2)) ),
sigma1,
[final] ).
cnf(i_0_235,axiom,
( member(f8(X1,X2),X2)
| ~ member(X1,domain_of(X2)) ),
domain2,
[final] ).
cnf(i_0_236,axiom,
( member(X1,f16(X1,X2))
| ~ member(X1,sigma(X2)) ),
sigma2,
[final] ).
cnf(i_0_237,axiom,
( member(X1,f7(X1,X2))
| ~ member(X1,second(X2)) ),
second4,
[final] ).
cnf(i_0_238,axiom,
( member(X1,f4(X1,X2))
| ~ member(X1,first(X2)) ),
first4,
[final] ).
cnf(i_0_239,axiom,
( member(X1,estin)
| ~ little_set(X1)
| ~ ordered_pair_predicate(X1)
| ~ member(first(X1),second(X1)) ),
element_relation3,
[final] ).
cnf(i_0_240,axiom,
( ~ disjoint(X1,X2)
| ~ member(X3,X1)
| ~ member(X3,X2) ),
disjoint1,
[final] ).
cnf(i_0_241,axiom,
( X1 = X2
| X1 = X3
| ~ member(X1,non_ordered_pair(X2,X3)) ),
non_ordered_pair1,
[final] ).
cnf(i_0_242,axiom,
( ordered_pair_predicate(X1)
| ~ member(X1,cross_product(X2,X3)) ),
cross_product1,
[final] ).
cnf(i_0_243,axiom,
( member(X1,range_of(X2))
| ~ little_set(X1)
| ~ ordered_pair_predicate(X3)
| ~ member(X3,X2)
| X1 != second(X3) ),
range_of4,
[final] ).
cnf(i_0_244,axiom,
( member(X1,domain_of(X2))
| ~ little_set(X1)
| ~ ordered_pair_predicate(X3)
| ~ member(X3,X2)
| X1 != first(X3) ),
domain4,
[final] ).
cnf(i_0_245,axiom,
( member(X1,sigma(X2))
| ~ member(X3,X2)
| ~ member(X1,X3) ),
sigma3,
[final] ).
cnf(i_0_246,axiom,
( X1 = second(f27(X1,X2))
| ~ member(X1,range_of(X2)) ),
range_of3,
[final] ).
cnf(i_0_247,axiom,
( X1 = first(f8(X1,X2))
| ~ member(X1,domain_of(X2)) ),
domain3,
[final] ).
cnf(i_0_248,axiom,
( ordered_pair_predicate(f27(X1,X2))
| ~ member(X1,range_of(X2)) ),
range_of1,
[final] ).
cnf(i_0_249,axiom,
( ordered_pair_predicate(f8(X1,X2))
| ~ member(X1,domain_of(X2)) ),
domain1,
[final] ).
cnf(i_0_250,axiom,
( little_set(f14(X1,X2))
| ~ member(X1,flip_range_of(X2)) ),
flip_range3,
[final] ).
cnf(i_0_251,axiom,
( little_set(f13(X1,X2))
| ~ member(X1,flip_range_of(X2)) ),
flip_range2,
[final] ).
cnf(i_0_252,axiom,
( little_set(f12(X1,X2))
| ~ member(X1,flip_range_of(X2)) ),
flip_range1,
[final] ).
cnf(i_0_253,axiom,
( little_set(f11(X1,X2))
| ~ member(X1,rotate_right(X2)) ),
rotate_right3,
[final] ).
cnf(i_0_254,axiom,
( little_set(f10(X1,X2))
| ~ member(X1,rotate_right(X2)) ),
rotate_right2,
[final] ).
cnf(i_0_255,axiom,
( little_set(f9(X1,X2))
| ~ member(X1,rotate_right(X2)) ),
rotate_right1,
[final] ).
cnf(i_0_256,axiom,
( little_set(f7(X1,X2))
| ~ member(X1,second(X2)) ),
second2,
[final] ).
cnf(i_0_257,axiom,
( little_set(f6(X1,X2))
| ~ member(X1,second(X2)) ),
second1,
[final] ).
cnf(i_0_258,axiom,
( little_set(f5(X1,X2))
| ~ member(X1,first(X2)) ),
first2,
[final] ).
cnf(i_0_259,axiom,
( little_set(f4(X1,X2))
| ~ member(X1,first(X2)) ),
first1,
[final] ).
cnf(i_0_260,axiom,
( member(X3,X2)
| ~ subset(X1,X2)
| ~ member(X3,X1) ),
subset1,
[final] ).
cnf(i_0_261,axiom,
( ~ member(X1,complement(X2))
| ~ member(X1,X2) ),
complement1,
[final] ).
cnf(i_0_262,axiom,
( disjoint(X1,X2)
| member(f23(X1,X2),X1) ),
disjoint2,
[final] ).
cnf(i_0_263,axiom,
( disjoint(X1,X2)
| member(f23(X1,X2),X2) ),
disjoint3,
[final] ).
cnf(i_0_264,axiom,
( subset(X1,X2)
| member(f17(X1,X2),X1) ),
subset2,
[final] ).
cnf(i_0_265,negated_conjecture,
~ member(a,non_ordered_pair(a,a)),
inference(rw,[status(thm)],[i_0_174,c_0_143]),
[final] ).
cnf(i_0_266,axiom,
( member(X1,non_ordered_pair(X2,X3))
| ~ little_set(X1)
| X1 != X2 ),
non_ordered_pair2,
[final] ).
cnf(i_0_267,axiom,
( member(X1,non_ordered_pair(X2,X3))
| ~ little_set(X1)
| X1 != X3 ),
non_ordered_pair3,
[final] ).
cnf(i_0_268,axiom,
( member(X1,powerset(X2))
| ~ little_set(X1)
| ~ subset(X1,X2) ),
powerset2,
[final] ).
cnf(i_0_269,axiom,
( member(first(X1),second(X1))
| ~ member(X1,estin) ),
element_relation2,
[final] ).
cnf(i_0_270,axiom,
( subset(X1,X2)
| ~ member(X1,powerset(X2)) ),
powerset1,
[final] ).
cnf(i_0_271,axiom,
( little_set(image(X1,X2))
| ~ little_set(X1)
| ~ function(X2) ),
image_and_substitution6,
[final] ).
cnf(i_0_272,axiom,
( member(X1,complement(X2))
| member(X1,X2)
| ~ little_set(X1) ),
complement2,
[final] ).
cnf(i_0_273,axiom,
( member(X1,identity_relation)
| ~ little_set(X1)
| ~ ordered_pair_predicate(X1)
| first(X1) != second(X1) ),
identity_relation3,
[final] ).
cnf(i_0_274,axiom,
( proper_subset(X1,X2)
| X1 = X2
| ~ subset(X1,X2) ),
proper_subset3,
[final] ).
cnf(i_0_275,axiom,
( subset(X1,X2)
| ~ proper_subset(X1,X2) ),
proper_subset1,
[final] ).
cnf(i_0_276,axiom,
( ordered_pair_predicate(X1)
| ~ member(X1,converse(X2)) ),
converse1,
[final] ).
cnf(i_0_277,axiom,
( ordered_pair_predicate(X2)
| ~ relation(X1)
| ~ member(X2,X1) ),
relation1,
[final] ).
cnf(i_0_278,axiom,
( little_set(f1(X1,X2))
| X1 = X2 ),
extensionality1,
[final] ).
cnf(i_0_279,axiom,
little_set(non_ordered_pair(X1,X2)),
non_ordered_pair4,
[final] ).
cnf(i_0_280,axiom,
( X1 = empty_set
| member(f26(X1),X1)
| ~ little_set(X1) ),
choice2,
[final] ).
cnf(i_0_281,axiom,
( first(X1) = second(X1)
| ~ member(X1,identity_relation) ),
identity_relation2,
[final] ).
cnf(i_0_282,axiom,
( one_to_one_function(X1)
| ~ function(X1)
| ~ function(converse(X1)) ),
one_to_one_function3,
[final] ).
cnf(i_0_283,axiom,
( little_set(X1)
| ~ closed(X1,X2) ),
closed1,
[final] ).
cnf(i_0_284,axiom,
( little_set(X1)
| ~ member(X1,X2) ),
a2,
[final] ).
cnf(i_0_285,axiom,
( little_set(X2)
| ~ closed(X1,X2) ),
closed2,
[final] ).
cnf(i_0_286,axiom,
( ~ proper_subset(X1,X2)
| X1 != X2 ),
proper_subset2,
[final] ).
cnf(i_0_287,axiom,
( relation(X1)
| member(f18(X1),X1) ),
relation2,
[final] ).
cnf(i_0_288,axiom,
( ordered_pair_predicate(X1)
| ~ member(X1,identity_relation) ),
identity_relation1,
[final] ).
cnf(i_0_289,axiom,
( ordered_pair_predicate(X1)
| ~ member(X1,estin) ),
element_relation1,
[final] ).
cnf(i_0_290,axiom,
( X1 = empty_set
| disjoint(f24(X1),X1) ),
regularity2,
[final] ).
cnf(i_0_291,axiom,
( X1 = empty_set
| member(f24(X1),X1) ),
regularity1,
[final] ).
cnf(i_0_292,axiom,
( relation(X1)
| ~ ordered_pair_predicate(f18(X1)) ),
relation3,
[final] ).
cnf(i_0_293,axiom,
~ member(X1,empty_set),
empty_set,
[final] ).
cnf(i_0_294,axiom,
( member(X1,universal_set)
| ~ little_set(X1) ),
universal_set,
[final] ).
cnf(i_0_295,axiom,
( function(X1)
| ~ relation(X1)
| ~ single_valued_set(X1) ),
function3,
[final] ).
cnf(i_0_296,axiom,
( function(converse(X1))
| ~ one_to_one_function(X1) ),
one_to_one_function2,
[final] ).
cnf(i_0_297,axiom,
( little_set(powerset(X1))
| ~ little_set(X1) ),
powerset3,
[final] ).
cnf(i_0_298,axiom,
( little_set(sigma(X1))
| ~ little_set(X1) ),
sigma4,
[final] ).
cnf(i_0_299,axiom,
( little_set(f3(X1))
| ~ ordered_pair_predicate(X1) ),
ordered_pair_predicate2,
[final] ).
cnf(i_0_300,axiom,
( little_set(f2(X1))
| ~ ordered_pair_predicate(X1) ),
ordered_pair_predicate1,
[final] ).
cnf(i_0_301,axiom,
( single_valued_set(X1)
| f20(X1) != f21(X1) ),
single_valued_set7,
[final] ).
cnf(i_0_302,axiom,
( single_valued_set(X1)
| little_set(f21(X1)) ),
single_valued_set4,
[final] ).
cnf(i_0_303,axiom,
( single_valued_set(X1)
| little_set(f20(X1)) ),
single_valued_set3,
[final] ).
cnf(i_0_304,axiom,
( single_valued_set(X1)
| little_set(f19(X1)) ),
single_valued_set2,
[final] ).
cnf(i_0_305,axiom,
( function(X1)
| ~ one_to_one_function(X1) ),
one_to_one_function1,
[final] ).
cnf(i_0_306,axiom,
( single_valued_set(X1)
| ~ function(X1) ),
function2,
[final] ).
cnf(i_0_307,axiom,
( relation(X1)
| ~ function(X1) ),
function1,
[final] ).
cnf(i_0_308,axiom,
member(empty_set,infinity),
infinity2,
[final] ).
cnf(i_0_309,axiom,
function(f25),
choice1,
[final] ).
cnf(i_0_310,hypothesis,
little_set(a),
a_little_set,
[final] ).
cnf(i_0_311,axiom,
little_set(infinity),
infinity1,
[final] ).
cnf(i_0_312,axiom,
X1 = X1 ).
cnf(i_0_313,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_314,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_315,axiom,
( X1 != X2
| apply(X1,X3) = apply(X2,X3) ) ).
cnf(i_0_316,axiom,
( X1 != X2
| apply(X3,X1) = apply(X3,X2) ) ).
cnf(i_0_317,axiom,
( X1 != X2
| second(X1) = second(X2) ) ).
cnf(i_0_318,axiom,
( X1 != X2
| first(X1) = first(X2) ) ).
cnf(i_0_319,axiom,
( X1 != X2
| non_ordered_pair(X1,X3) = non_ordered_pair(X2,X3) ) ).
cnf(i_0_320,axiom,
( X1 != X2
| non_ordered_pair(X3,X1) = non_ordered_pair(X3,X2) ) ).
cnf(i_0_321,axiom,
( X1 != X2
| f21(X1) = f21(X2) ) ).
cnf(i_0_322,axiom,
( X1 != X2
| f20(X1) = f20(X2) ) ).
cnf(i_0_323,axiom,
( X1 != X2
| domain_of(X1) = domain_of(X2) ) ).
cnf(i_0_324,axiom,
( X1 != X2
| ~ homomorphism(X1,X3,X4,X5,X6)
| homomorphism(X2,X3,X4,X5,X6) ) ).
cnf(i_0_325,axiom,
( X1 != X2
| ~ homomorphism(X3,X1,X4,X5,X6)
| homomorphism(X3,X2,X4,X5,X6) ) ).
cnf(i_0_326,axiom,
( X1 != X2
| ~ homomorphism(X3,X4,X1,X5,X6)
| homomorphism(X3,X4,X2,X5,X6) ) ).
cnf(i_0_327,axiom,
( X1 != X2
| ~ homomorphism(X3,X4,X5,X1,X6)
| homomorphism(X3,X4,X5,X2,X6) ) ).
cnf(i_0_328,axiom,
( X1 != X2
| ~ homomorphism(X3,X4,X5,X6,X1)
| homomorphism(X3,X4,X5,X6,X2) ) ).
cnf(i_0_329,axiom,
( X1 != X2
| ~ disjoint(X1,X3)
| disjoint(X2,X3) ) ).
cnf(i_0_330,axiom,
( X1 != X2
| ~ disjoint(X3,X1)
| disjoint(X3,X2) ) ).
cnf(i_0_331,axiom,
( X1 != X2
| ~ proper_subset(X1,X3)
| proper_subset(X2,X3) ) ).
cnf(i_0_332,axiom,
( X1 != X2
| ~ proper_subset(X3,X1)
| proper_subset(X3,X2) ) ).
cnf(i_0_333,axiom,
( X1 != X2
| ~ relation(X1)
| relation(X2) ) ).
cnf(i_0_334,axiom,
( X1 != X2
| ~ one_to_one_function(X1)
| one_to_one_function(X2) ) ).
cnf(i_0_335,axiom,
( X1 != X2
| ~ closed(X1,X3)
| closed(X2,X3) ) ).
cnf(i_0_336,axiom,
( X1 != X2
| ~ closed(X3,X1)
| closed(X3,X2) ) ).
cnf(i_0_337,axiom,
( X1 != X2
| ~ maps(X1,X3,X4)
| maps(X2,X3,X4) ) ).
cnf(i_0_338,axiom,
( X1 != X2
| ~ maps(X3,X1,X4)
| maps(X3,X2,X4) ) ).
cnf(i_0_339,axiom,
( X1 != X2
| ~ maps(X3,X4,X1)
| maps(X3,X4,X2) ) ).
cnf(i_0_340,axiom,
( X1 != X2
| ~ member(X1,X3)
| member(X2,X3) ) ).
cnf(i_0_341,axiom,
( X1 != X2
| ~ member(X3,X1)
| member(X3,X2) ) ).
cnf(i_0_342,axiom,
( X1 != X2
| ~ little_set(X1)
| little_set(X2) ) ).
cnf(i_0_343,axiom,
( X1 != X2
| ~ single_valued_set(X1)
| single_valued_set(X2) ) ).
cnf(i_0_344,axiom,
( X1 != X2
| ~ ordered_pair_predicate(X1)
| ordered_pair_predicate(X2) ) ).
cnf(i_0_345,axiom,
( X1 != X2
| ~ subset(X1,X3)
| subset(X2,X3) ) ).
cnf(i_0_346,axiom,
( X1 != X2
| ~ subset(X3,X1)
| subset(X3,X2) ) ).
cnf(i_0_347,axiom,
( X1 != X2
| ~ function(X1)
| function(X2) ) ).
cnf(i_0_312_001,axiom,
X1 = X1 ).
cnf(i_0_313_002,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_314_003,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_315_004,axiom,
( X1 != X2
| apply(X1,X3) = apply(X2,X3) ) ).
cnf(i_0_316_005,axiom,
( X1 != X2
| apply(X3,X1) = apply(X3,X2) ) ).
cnf(i_0_317_006,axiom,
( X1 != X2
| second(X1) = second(X2) ) ).
cnf(i_0_318_007,axiom,
( X1 != X2
| first(X1) = first(X2) ) ).
cnf(i_0_319_008,axiom,
( X1 != X2
| non_ordered_pair(X1,X3) = non_ordered_pair(X2,X3) ) ).
cnf(i_0_320_009,axiom,
( X1 != X2
| non_ordered_pair(X3,X1) = non_ordered_pair(X3,X2) ) ).
cnf(i_0_321_010,axiom,
( X1 != X2
| f21(X1) = f21(X2) ) ).
cnf(i_0_322_011,axiom,
( X1 != X2
| f20(X1) = f20(X2) ) ).
cnf(i_0_323_012,axiom,
( X1 != X2
| domain_of(X1) = domain_of(X2) ) ).
cnf(i_0_324_013,axiom,
( X1 != X2
| ~ homomorphism(X1,X3,X4,X5,X6)
| homomorphism(X2,X3,X4,X5,X6) ) ).
cnf(i_0_325_014,axiom,
( X1 != X2
| ~ homomorphism(X3,X1,X4,X5,X6)
| homomorphism(X3,X2,X4,X5,X6) ) ).
cnf(i_0_326_015,axiom,
( X1 != X2
| ~ homomorphism(X3,X4,X1,X5,X6)
| homomorphism(X3,X4,X2,X5,X6) ) ).
cnf(i_0_327_016,axiom,
( X1 != X2
| ~ homomorphism(X3,X4,X5,X1,X6)
| homomorphism(X3,X4,X5,X2,X6) ) ).
cnf(i_0_328_017,axiom,
( X1 != X2
| ~ homomorphism(X3,X4,X5,X6,X1)
| homomorphism(X3,X4,X5,X6,X2) ) ).
cnf(i_0_329_018,axiom,
( X1 != X2
| ~ disjoint(X1,X3)
| disjoint(X2,X3) ) ).
cnf(i_0_330_019,axiom,
( X1 != X2
| ~ disjoint(X3,X1)
| disjoint(X3,X2) ) ).
cnf(i_0_331_020,axiom,
( X1 != X2
| ~ proper_subset(X1,X3)
| proper_subset(X2,X3) ) ).
cnf(i_0_332_021,axiom,
( X1 != X2
| ~ proper_subset(X3,X1)
| proper_subset(X3,X2) ) ).
cnf(i_0_333_022,axiom,
( X1 != X2
| ~ relation(X1)
| relation(X2) ) ).
cnf(i_0_334_023,axiom,
( X1 != X2
| ~ one_to_one_function(X1)
| one_to_one_function(X2) ) ).
cnf(i_0_335_024,axiom,
( X1 != X2
| ~ closed(X1,X3)
| closed(X2,X3) ) ).
cnf(i_0_336_025,axiom,
( X1 != X2
| ~ closed(X3,X1)
| closed(X3,X2) ) ).
cnf(i_0_337_026,axiom,
( X1 != X2
| ~ maps(X1,X3,X4)
| maps(X2,X3,X4) ) ).
cnf(i_0_338_027,axiom,
( X1 != X2
| ~ maps(X3,X1,X4)
| maps(X3,X2,X4) ) ).
cnf(i_0_339_028,axiom,
( X1 != X2
| ~ maps(X3,X4,X1)
| maps(X3,X4,X2) ) ).
cnf(i_0_340_029,axiom,
( X1 != X2
| ~ member(X1,X3)
| member(X2,X3) ) ).
cnf(i_0_341_030,axiom,
( X1 != X2
| ~ member(X3,X1)
| member(X3,X2) ) ).
cnf(i_0_342_031,axiom,
( X1 != X2
| ~ little_set(X1)
| little_set(X2) ) ).
cnf(i_0_343_032,axiom,
( X1 != X2
| ~ single_valued_set(X1)
| single_valued_set(X2) ) ).
cnf(i_0_344_033,axiom,
( X1 != X2
| ~ ordered_pair_predicate(X1)
| ordered_pair_predicate(X2) ) ).
cnf(i_0_345_034,axiom,
( X1 != X2
| ~ subset(X1,X3)
| subset(X2,X3) ) ).
cnf(i_0_346_035,axiom,
( X1 != X2
| ~ subset(X3,X1)
| subset(X3,X2) ) ).
cnf(i_0_347_036,axiom,
( X1 != X2
| ~ function(X1)
| function(X2) ) ).
cnf(i_0_348,plain,
( ~ little_set(X1)
| ~ little_set(X2)
| ~ little_set(X3)
| ~ little_set(non_ordered_pair(non_ordered_pair(X3,X3),non_ordered_pair(X3,non_ordered_pair(non_ordered_pair(X2,X2),non_ordered_pair(X2,X1)))))
| member(non_ordered_pair(non_ordered_pair(X3,X3),non_ordered_pair(X3,non_ordered_pair(non_ordered_pair(X2,X2),non_ordered_pair(X2,X1)))),flip_range_of(X4))
| ~ member(non_ordered_pair(non_ordered_pair(X3,X3),non_ordered_pair(X3,non_ordered_pair(non_ordered_pair(X1,X1),non_ordered_pair(X1,X2)))),X4) ),
inference(equality_inference,[],[186]) ).
cnf(i_0_349,plain,
( ~ little_set(X1)
| ~ little_set(X2)
| ~ little_set(X3)
| ~ little_set(non_ordered_pair(non_ordered_pair(X3,X3),non_ordered_pair(X3,non_ordered_pair(non_ordered_pair(X2,X2),non_ordered_pair(X2,X1)))))
| member(non_ordered_pair(non_ordered_pair(X3,X3),non_ordered_pair(X3,non_ordered_pair(non_ordered_pair(X2,X2),non_ordered_pair(X2,X1)))),rotate_right(X4))
| ~ member(non_ordered_pair(non_ordered_pair(X2,X2),non_ordered_pair(X2,non_ordered_pair(non_ordered_pair(X1,X1),non_ordered_pair(X1,X3)))),X4) ),
inference(equality_inference,[],[187]) ).
cnf(i_0_350,plain,
( ~ little_set(X1)
| ~ little_set(X2)
| ~ little_set(non_ordered_pair(non_ordered_pair(X2,X2),non_ordered_pair(X2,X1)))
| ~ little_set(X3)
| member(non_ordered_pair(non_ordered_pair(X2,X2),non_ordered_pair(X2,X1)),compose(X4,X5))
| ~ member(non_ordered_pair(non_ordered_pair(X3,X3),non_ordered_pair(X3,X1)),X5)
| ~ member(non_ordered_pair(non_ordered_pair(X2,X2),non_ordered_pair(X2,X3)),X4) ),
inference(equality_inference,[],[191]) ).
cnf(i_0_351,plain,
( ~ little_set(X1)
| ~ little_set(X2)
| ~ member(X3,X1)
| member(X3,second(non_ordered_pair(non_ordered_pair(X2,X2),non_ordered_pair(X2,X1)))) ),
inference(equality_inference,[],[212]) ).
cnf(i_0_352,plain,
( ~ little_set(X1)
| ~ little_set(X2)
| ~ member(X3,X2)
| member(X3,first(non_ordered_pair(non_ordered_pair(X2,X2),non_ordered_pair(X2,X1)))) ),
inference(equality_inference,[],[213]) ).
cnf(i_0_353,plain,
( ~ little_set(X1)
| ~ little_set(X2)
| ordered_pair_predicate(non_ordered_pair(non_ordered_pair(X2,X2),non_ordered_pair(X2,X1))) ),
inference(equality_inference,[],[216]) ).
cnf(i_0_354,plain,
( ~ little_set(second(X1))
| ~ member(X1,X2)
| ~ ordered_pair_predicate(X1)
| ~ member(first(X1),X3)
| member(second(X1),image(X3,X2)) ),
inference(equality_inference,[],[219]) ).
cnf(i_0_355,plain,
( ~ member(X1,X2)
| ~ ordered_pair_predicate(X1)
| ~ member(X3,second(X1))
| member(X3,apply(X2,first(X1))) ),
inference(equality_inference,[],[220]) ).
cnf(i_0_356,plain,
( ~ function(X1)
| maps(X1,domain_of(X1),X2)
| ~ subset(range_of(X1),X2) ),
inference(equality_inference,[],[223]) ).
cnf(i_0_357,plain,
( ~ little_set(second(X1))
| ~ member(X1,X2)
| ~ ordered_pair_predicate(X1)
| member(second(X1),range_of(X2)) ),
inference(equality_inference,[],[243]) ).
cnf(i_0_358,plain,
( ~ little_set(first(X1))
| ~ member(X1,X2)
| ~ ordered_pair_predicate(X1)
| member(first(X1),domain_of(X2)) ),
inference(equality_inference,[],[244]) ).
cnf(i_0_359,plain,
( ~ little_set(X1)
| member(X1,non_ordered_pair(X1,X2)) ),
inference(equality_inference,[],[266]) ).
cnf(i_0_360,plain,
( ~ little_set(X1)
| member(X1,non_ordered_pair(X2,X1)) ),
inference(equality_inference,[],[267]) ).
cnf(i_0_361,plain,
~ proper_subset(X1,X1),
inference(equality_inference,[],[286]) ).
cnf(i_0_362,plain,
$false,
inference(scs_inference,[],[i_0_310,i_0_265,i_0_359]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SET024-4 : TPTP v9.2.1. Released v1.0.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.15/0.33 % Computer : n027.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % WCLimit : 300
% 0.15/0.33 % DateTime : Tue May 5 02:05:20 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.34 % start to proof: theBenchmark
% 0.36/1.61 % Version : CSE_E---1.7
% 0.36/1.61 % Problem : theBenchmark.p
% 0.36/1.61 % SZS status Unsatisfiable for theBenchmark.p
% 0.36/1.61 % SZS output start CNFRefutation
% See solution above
% 0.36/1.64 % Total time : 1.272s
%------------------------------------------------------------------------------