%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SET027-3 : TPTP v9.2.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n018.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:56 PM UTC 2026
% Result : Unsatisfiable 231.86s 184.03s
% Output : CNFRefutation 245.34s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named c_0_155)
% Comments :
%------------------------------------------------------------------------------
cnf(ordered_pair,axiom,
ordered_pair(X1,X2) = non_ordered_pair(singleton_set(X1),non_ordered_pair(X1,X2)),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',ordered_pair) ).
cnf(singleton_set,axiom,
singleton_set(X1) = non_ordered_pair(X1,X1),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',singleton_set) ).
cnf(successor,axiom,
successor(X1) = union(X1,singleton_set(X1)),
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/benchmark/Axioms/SET003-0.ax',converse3) ).
cnf(infinity3,axiom,
( member(successor(X1),infinity)
| ~ member(X1,infinity) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',infinity3) ).
cnf(union,axiom,
union(X1,X2) = complement(intersection(complement(X1),complement(X2))),
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/benchmark/Axioms/SET003-0.ax',first3) ).
cnf(converse2,axiom,
( member(ordered_pair(second(X1),first(X1)),X2)
| ~ member(X1,converse(X2)) ),
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/benchmark/Axioms/SET003-0.ax',single_valued_set5) ).
cnf(second_components_are_equal,axiom,
( X2 = X4
| ~ little_set(X1)
| ~ little_set(X2)
| ~ little_set(X3)
| ~ little_set(X4)
| ordered_pair(X1,X2) != ordered_pair(X3,X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',second_components_are_equal) ).
cnf(first_components_are_equal,axiom,
( X1 = X2
| ~ little_set(X1)
| ~ little_set(X2)
| ordered_pair(X1,X3) != ordered_pair(X2,X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',first_components_are_equal) ).
cnf(choice3,axiom,
( X1 = empty_set
| member(ordered_pair(X1,f26(X1)),f25)
| ~ little_set(X1) ),
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/benchmark/Axioms/SET003-0.ax',first5) ).
cnf(property_of_second,axiom,
( second(ordered_pair(X1,X2)) = X2
| ~ little_set(X1)
| ~ little_set(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',property_of_second) ).
cnf(property_of_first,axiom,
( first(ordered_pair(X1,X2)) = X1
| ~ little_set(X1)
| ~ little_set(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',property_of_first) ).
cnf(ordered_pairs_are_small1,axiom,
little_set(ordered_pair(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ordered_pairs_are_small1) ).
cnf(ordered_pair_predicate4,axiom,
( ordered_pair_predicate(X1)
| ~ little_set(X2)
| ~ little_set(X3)
| X1 != ordered_pair(X2,X3) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/Axioms/SET003-0.ax',ordered_pair_predicate3) ).
cnf(property_of_singleton_sets,axiom,
( member(X1,singleton_set(X1))
| ~ little_set(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',property_of_singleton_sets) ).
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/sandbox2/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/sandbox2/benchmark/Axioms/SET003-0.ax',homomorphism5) ).
cnf(homomorphism3,axiom,
( maps(X1,X2,X4)
| ~ homomorphism(X1,X2,X3,X4,X5) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',homomorphism3) ).
cnf(homomorphism1,axiom,
( closed(X2,X3)
| ~ homomorphism(X1,X2,X3,X4,X5) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',homomorphism1) ).
cnf(homomorphism2,axiom,
( closed(X4,X5)
| ~ homomorphism(X1,X2,X3,X4,X5) ),
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/benchmark/Axioms/SET003-0.ax',apply4) ).
cnf(apply2,axiom,
( member(f28(X1,X2,X3),X2)
| ~ member(X1,apply(X2,X3)) ),
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/benchmark/Axioms/SET003-0.ax',apply3) ).
cnf(apply1,axiom,
( ordered_pair_predicate(f28(X1,X2,X3))
| ~ member(X1,apply(X2,X3)) ),
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/benchmark/Axioms/SET003-0.ax',compose3) ).
cnf(compose2,axiom,
( little_set(f30(X1,X2,X3))
| ~ member(X1,compose(X2,X3)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',compose2) ).
cnf(compose1,axiom,
( little_set(f29(X1,X2,X3))
| ~ member(X1,compose(X2,X3)) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/Axioms/SET003-0.ax',closed4) ).
cnf(extensionality3,axiom,
( X1 = X2
| ~ member(f1(X1,X2),X1)
| ~ member(f1(X1,X2),X2) ),
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/benchmark/Axioms/SET003-0.ax',apply5) ).
cnf(maps3,axiom,
( subset(range_of(X1),X3)
| ~ maps(X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',maps3) ).
cnf(closed3,axiom,
( maps(X2,cross_product(X1,X1),X1)
| ~ closed(X1,X2) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/Axioms/SET003-0.ax',maps4) ).
cnf(maps2,axiom,
( domain_of(X1) = X2
| ~ maps(X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',maps2) ).
cnf(maps1,axiom,
( function(X1)
| ~ maps(X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',maps1) ).
cnf(intersection3,axiom,
( member(X1,intersection(X2,X3))
| ~ member(X1,X2)
| ~ member(X1,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',intersection3) ).
cnf(cross_product3,axiom,
( member(second(X1),X3)
| ~ member(X1,cross_product(X2,X3)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',cross_product3) ).
cnf(cross_product2,axiom,
( member(first(X1),X2)
| ~ member(X1,cross_product(X2,X3)) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/Axioms/SET003-0.ax',extensionality2) ).
cnf(subset3,axiom,
( subset(X1,X2)
| ~ member(f17(X1,X2),X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',subset3) ).
cnf(intersection1,axiom,
( member(X1,X2)
| ~ member(X1,intersection(X2,X3)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',intersection1) ).
cnf(intersection2,axiom,
( member(X1,X3)
| ~ member(X1,intersection(X2,X3)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',intersection2) ).
cnf(range_of2,axiom,
( member(f27(X1,X2),X2)
| ~ member(X1,range_of(X2)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',range_of2) ).
cnf(sigma1,axiom,
( member(f16(X1,X2),X2)
| ~ member(X1,sigma(X2)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',sigma1) ).
cnf(domain2,axiom,
( member(f8(X1,X2),X2)
| ~ member(X1,domain_of(X2)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',domain2) ).
cnf(sigma2,axiom,
( member(X1,f16(X1,X2))
| ~ member(X1,sigma(X2)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',sigma2) ).
cnf(second4,axiom,
( member(X1,f7(X1,X2))
| ~ member(X1,second(X2)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',second4) ).
cnf(first4,axiom,
( member(X1,f4(X1,X2))
| ~ member(X1,first(X2)) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/Axioms/SET003-0.ax',element_relation3) ).
cnf(disjoint1,axiom,
( ~ disjoint(X1,X2)
| ~ member(X3,X1)
| ~ member(X3,X2) ),
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/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/sandbox2/benchmark/Axioms/SET003-0.ax',domain4) ).
cnf(sigma3,axiom,
( member(X1,sigma(X2))
| ~ member(X3,X2)
| ~ member(X1,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',sigma3) ).
cnf(range_of3,axiom,
( X1 = second(f27(X1,X2))
| ~ member(X1,range_of(X2)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',range_of3) ).
cnf(domain3,axiom,
( X1 = first(f8(X1,X2))
| ~ member(X1,domain_of(X2)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',domain3) ).
cnf(range_of1,axiom,
( ordered_pair_predicate(f27(X1,X2))
| ~ member(X1,range_of(X2)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',range_of1) ).
cnf(domain1,axiom,
( ordered_pair_predicate(f8(X1,X2))
| ~ member(X1,domain_of(X2)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',domain1) ).
cnf(flip_range3,axiom,
( little_set(f14(X1,X2))
| ~ member(X1,flip_range_of(X2)) ),
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/benchmark/Axioms/SET003-0.ax',flip_range1) ).
cnf(rotate_right3,axiom,
( little_set(f11(X1,X2))
| ~ member(X1,rotate_right(X2)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',rotate_right3) ).
cnf(rotate_right2,axiom,
( little_set(f10(X1,X2))
| ~ member(X1,rotate_right(X2)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',rotate_right2) ).
cnf(rotate_right1,axiom,
( little_set(f9(X1,X2))
| ~ member(X1,rotate_right(X2)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',rotate_right1) ).
cnf(second2,axiom,
( little_set(f7(X1,X2))
| ~ member(X1,second(X2)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',second2) ).
cnf(second1,axiom,
( little_set(f6(X1,X2))
| ~ member(X1,second(X2)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',second1) ).
cnf(first2,axiom,
( little_set(f5(X1,X2))
| ~ member(X1,first(X2)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',first2) ).
cnf(first1,axiom,
( little_set(f4(X1,X2))
| ~ member(X1,first(X2)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',first1) ).
cnf(left_cancellation,axiom,
( X1 = X2
| ~ little_set(X1)
| ~ little_set(X2)
| non_ordered_pair(X3,X1) != non_ordered_pair(X3,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',left_cancellation) ).
cnf(subset1,axiom,
( member(X3,X2)
| ~ subset(X1,X2)
| ~ member(X3,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',subset1) ).
cnf(complement1,axiom,
( ~ member(X1,complement(X2))
| ~ member(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',complement1) ).
cnf(disjoint2,axiom,
( disjoint(X1,X2)
| member(f23(X1,X2),X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',disjoint2) ).
cnf(disjoint3,axiom,
( disjoint(X1,X2)
| member(f23(X1,X2),X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',disjoint3) ).
cnf(subset2,axiom,
( subset(X1,X2)
| member(f17(X1,X2),X1) ),
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/benchmark/Axioms/SET003-0.ax',non_ordered_pair3) ).
cnf(powerset2,axiom,
( member(X1,powerset(X2))
| ~ little_set(X1)
| ~ subset(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',powerset2) ).
cnf(two_sets_equal,axiom,
( X1 = X2
| ~ subset(X1,X2)
| ~ subset(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',two_sets_equal) ).
cnf(element_relation2,axiom,
( member(first(X1),second(X1))
| ~ member(X1,estin) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',element_relation2) ).
cnf(powerset1,axiom,
( subset(X1,X2)
| ~ member(X1,powerset(X2)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',powerset1) ).
cnf(image_and_substitution6,axiom,
( little_set(image(X1,X2))
| ~ little_set(X1)
| ~ function(X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',image_and_substitution6) ).
cnf(complement2,axiom,
( member(X1,complement(X2))
| member(X1,X2)
| ~ little_set(X1) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/Axioms/SET003-0.ax',identity_relation3) ).
cnf(proper_subset3,axiom,
( proper_subset(X1,X2)
| X1 = X2
| ~ subset(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',proper_subset3) ).
cnf(proper_subset1,axiom,
( subset(X1,X2)
| ~ proper_subset(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',proper_subset1) ).
cnf(converse1,axiom,
( ordered_pair_predicate(X1)
| ~ member(X1,converse(X2)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',converse1) ).
cnf(relation1,axiom,
( ordered_pair_predicate(X2)
| ~ relation(X1)
| ~ member(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',relation1) ).
cnf(extensionality1,axiom,
( little_set(f1(X1,X2))
| X1 = X2 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',extensionality1) ).
cnf(non_ordered_pair4,axiom,
little_set(non_ordered_pair(X1,X2)),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',non_ordered_pair4) ).
cnf(choice2,axiom,
( X1 = empty_set
| member(f26(X1),X1)
| ~ little_set(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',choice2) ).
cnf(identity_relation2,axiom,
( first(X1) = second(X1)
| ~ member(X1,identity_relation) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/Axioms/SET003-0.ax',one_to_one_function3) ).
cnf(closed1,axiom,
( little_set(X1)
| ~ closed(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',closed1) ).
cnf(a2,axiom,
( little_set(X1)
| ~ member(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',a2) ).
cnf(closed2,axiom,
( little_set(X2)
| ~ closed(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',closed2) ).
cnf(proper_subset2,axiom,
( ~ proper_subset(X1,X2)
| X1 != X2 ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',proper_subset2) ).
cnf(relation2,axiom,
( relation(X1)
| member(f18(X1),X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',relation2) ).
cnf(identity_relation1,axiom,
( ordered_pair_predicate(X1)
| ~ member(X1,identity_relation) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',identity_relation1) ).
cnf(element_relation1,axiom,
( ordered_pair_predicate(X1)
| ~ member(X1,estin) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',element_relation1) ).
cnf(regularity2,axiom,
( X1 = empty_set
| disjoint(f24(X1),X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',regularity2) ).
cnf(regularity1,axiom,
( X1 = empty_set
| member(f24(X1),X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',regularity1) ).
cnf(relation3,axiom,
( relation(X1)
| ~ ordered_pair_predicate(f18(X1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',relation3) ).
cnf(empty_set,axiom,
~ member(X1,empty_set),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',empty_set) ).
cnf(universal_set,axiom,
( member(X1,universal_set)
| ~ little_set(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',universal_set) ).
cnf(function3,axiom,
( function(X1)
| ~ relation(X1)
| ~ single_valued_set(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',function3) ).
cnf(prove_a_subset_c,negated_conjecture,
~ subset(a,c),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_a_subset_c) ).
cnf(one_to_one_function2,axiom,
( function(converse(X1))
| ~ one_to_one_function(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',one_to_one_function2) ).
cnf(powerset3,axiom,
( little_set(powerset(X1))
| ~ little_set(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',powerset3) ).
cnf(sigma4,axiom,
( little_set(sigma(X1))
| ~ little_set(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',sigma4) ).
cnf(second_component_is_small,axiom,
( little_set(second(X1))
| ~ ordered_pair_predicate(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',second_component_is_small) ).
cnf(first_component_is_small,axiom,
( little_set(first(X1))
| ~ ordered_pair_predicate(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',first_component_is_small) ).
cnf(ordered_pair_predicate2,axiom,
( little_set(f3(X1))
| ~ ordered_pair_predicate(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',ordered_pair_predicate2) ).
cnf(ordered_pair_predicate1,axiom,
( little_set(f2(X1))
| ~ ordered_pair_predicate(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',ordered_pair_predicate1) ).
cnf(single_valued_set7,axiom,
( single_valued_set(X1)
| f20(X1) != f21(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',single_valued_set7) ).
cnf(single_valued_set4,axiom,
( single_valued_set(X1)
| little_set(f21(X1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',single_valued_set4) ).
cnf(single_valued_set3,axiom,
( single_valued_set(X1)
| little_set(f20(X1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',single_valued_set3) ).
cnf(single_valued_set2,axiom,
( single_valued_set(X1)
| little_set(f19(X1)) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',single_valued_set2) ).
cnf(one_to_one_function1,axiom,
( function(X1)
| ~ one_to_one_function(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',one_to_one_function1) ).
cnf(function2,axiom,
( single_valued_set(X1)
| ~ function(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',function2) ).
cnf(function1,axiom,
( relation(X1)
| ~ function(X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',function1) ).
cnf(ordered_pairs_are_small2,axiom,
( little_set(X1)
| ~ ordered_pair_predicate(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ordered_pairs_are_small2) ).
cnf(b_subset_c,hypothesis,
subset(b,c),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',b_subset_c) ).
cnf(a_subset_b,hypothesis,
subset(a,b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a_subset_b) ).
cnf(infinity2,axiom,
member(empty_set,infinity),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',infinity2) ).
cnf(choice1,axiom,
function(f25),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',choice1) ).
cnf(infinity1,axiom,
little_set(infinity),
file('/export/starexec/sandbox2/benchmark/Axioms/SET003-0.ax',infinity1) ).
cnf(i_0_154,axiom,
ordered_pair(X1,X2) = non_ordered_pair(singleton_set(X1),non_ordered_pair(X1,X2)),
ordered_pair ).
cnf(i_0_155,axiom,
singleton_set(X1) = non_ordered_pair(X1,X1),
singleton_set ).
cnf(i_0_156,axiom,
successor(X1) = union(X1,singleton_set(X1)),
successor ).
cnf(i_0_157,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_158,axiom,
apply_to_two_arguments(X1,X2,X3) = apply(X1,ordered_pair(X2,X3)),
apply_to_two_arguments ).
cnf(i_0_159,plain,
ordered_pair(X1,X2) = non_ordered_pair(non_ordered_pair(X1,X1),non_ordered_pair(X1,X2)),
inference(rw,[status(thm)],[i_0_154,c_0_155]) ).
cnf(i_0_160,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_161,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_162,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_163,axiom,
( member(ordered_pair(f31(X1,X2,X3),f30(X1,X2,X3)),X3)
| ~ member(X1,compose(X2,X3)) ),
compose6 ).
cnf(i_0_164,axiom,
( member(ordered_pair(f29(X1,X2,X3),f31(X1,X2,X3)),X2)
| ~ member(X1,compose(X2,X3)) ),
compose5 ).
cnf(i_0_165,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_166,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_167,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_168,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_169,axiom,
( X1 = ordered_pair(f29(X1,X2,X3),f30(X1,X2,X3))
| ~ member(X1,compose(X2,X3)) ),
compose4 ).
cnf(i_0_170,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_171,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_172,axiom,
( member(X1,converse(X2))
| ~ little_set(X1)
| ~ ordered_pair_predicate(X1)
| ~ member(ordered_pair(second(X1),first(X1)),X2) ),
converse3 ).
cnf(i_0_173,axiom,
( member(successor(X1),infinity)
| ~ member(X1,infinity) ),
infinity3 ).
cnf(i_0_174,plain,
successor(X1) = union(X1,non_ordered_pair(X1,X1)),
inference(rw,[status(thm)],[i_0_156,c_0_155]) ).
cnf(i_0_175,axiom,
union(X1,X2) = complement(intersection(complement(X1),complement(X2))),
union ).
cnf(i_0_176,axiom,
( X2 = ordered_pair(f6(X1,X2),f7(X1,X2))
| ~ member(X1,second(X2)) ),
second3 ).
cnf(i_0_177,axiom,
( X2 = ordered_pair(f4(X1,X2),f5(X1,X2))
| ~ member(X1,first(X2)) ),
first3 ).
cnf(i_0_178,axiom,
( member(ordered_pair(second(X1),first(X1)),X2)
| ~ member(X1,converse(X2)) ),
converse2 ).
cnf(i_0_179,axiom,
( single_valued_set(X1)
| member(ordered_pair(f19(X1),f21(X1)),X1) ),
single_valued_set6 ).
cnf(i_0_180,axiom,
( single_valued_set(X1)
| member(ordered_pair(f19(X1),f20(X1)),X1) ),
single_valued_set5 ).
cnf(i_0_181,axiom,
( X2 = X4
| ~ little_set(X1)
| ~ little_set(X2)
| ~ little_set(X3)
| ~ little_set(X4)
| ordered_pair(X1,X2) != ordered_pair(X3,X4) ),
second_components_are_equal ).
cnf(i_0_182,axiom,
( X1 = X2
| ~ little_set(X1)
| ~ little_set(X2)
| ordered_pair(X1,X3) != ordered_pair(X2,X4) ),
first_components_are_equal ).
cnf(i_0_183,axiom,
( X1 = empty_set
| member(ordered_pair(X1,f26(X1)),f25)
| ~ little_set(X1) ),
choice3 ).
cnf(i_0_184,axiom,
( member(X1,second(X2))
| ~ little_set(X3)
| ~ little_set(X4)
| X2 != ordered_pair(X3,X4)
| ~ member(X1,X4) ),
second5 ).
cnf(i_0_185,axiom,
( member(X1,first(X2))
| ~ little_set(X3)
| ~ little_set(X4)
| X2 != ordered_pair(X3,X4)
| ~ member(X1,X3) ),
first5 ).
cnf(i_0_186,axiom,
( second(ordered_pair(X1,X2)) = X2
| ~ little_set(X1)
| ~ little_set(X2) ),
property_of_second ).
cnf(i_0_187,axiom,
( first(ordered_pair(X1,X2)) = X1
| ~ little_set(X1)
| ~ little_set(X2) ),
property_of_first ).
cnf(i_0_188,axiom,
little_set(ordered_pair(X1,X2)),
ordered_pairs_are_small1 ).
cnf(i_0_189,axiom,
( ordered_pair_predicate(X1)
| ~ little_set(X2)
| ~ little_set(X3)
| X1 != ordered_pair(X2,X3) ),
ordered_pair_predicate4 ).
cnf(i_0_190,axiom,
( X1 = ordered_pair(f2(X1),f3(X1))
| ~ ordered_pair_predicate(X1) ),
ordered_pair_predicate3 ).
cnf(i_0_191,axiom,
( member(X1,singleton_set(X1))
| ~ little_set(X1) ),
property_of_singleton_sets ).
cnf(i_0_192,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_157,c_0_158]),c_0_158]),c_0_159]),c_0_159]),
[final] ).
cnf(i_0_193,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_194,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_195,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_160,c_0_158]),c_0_158]),c_0_159]),c_0_159]),
[final] ).
cnf(i_0_196,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_161,c_0_159]),c_0_159]),
[final] ).
cnf(i_0_197,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_162,c_0_159]),c_0_159]),
[final] ).
cnf(i_0_198,axiom,
( maps(X1,X2,X4)
| ~ homomorphism(X1,X2,X3,X4,X5) ),
homomorphism3,
[final] ).
cnf(i_0_199,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_163,c_0_159]),
[final] ).
cnf(i_0_200,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_164,c_0_159]),
[final] ).
cnf(i_0_201,axiom,
( closed(X2,X3)
| ~ homomorphism(X1,X2,X3,X4,X5) ),
homomorphism1,
[final] ).
cnf(i_0_202,axiom,
( closed(X4,X5)
| ~ homomorphism(X1,X2,X3,X4,X5) ),
homomorphism2,
[final] ).
cnf(i_0_203,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_165,c_0_159]),c_0_159]),c_0_159]),c_0_159]),
[final] ).
cnf(i_0_204,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_166,c_0_159]),c_0_159]),c_0_159]),c_0_159]),
[final] ).
cnf(i_0_205,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_167,c_0_159]),c_0_159]),
[final] ).
cnf(i_0_206,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_168,c_0_159]),c_0_159]),
[final] ).
cnf(i_0_207,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_169,c_0_159]),
[final] ).
cnf(i_0_208,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_170,c_0_159]),c_0_159]),c_0_159]),
[final] ).
cnf(i_0_209,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_171,c_0_159]),c_0_159]),
[final] ).
cnf(i_0_210,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_172,c_0_159]),
[final] ).
cnf(i_0_211,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_173,c_0_174]),c_0_175]),
[final] ).
cnf(i_0_212,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_176,c_0_159]),
[final] ).
cnf(i_0_213,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_177,c_0_159]),
[final] ).
cnf(i_0_214,axiom,
( member(first(f22(X1,X2,X3)),X2)
| ~ member(X1,image(X2,X3)) ),
image_and_substitution3,
[final] ).
cnf(i_0_215,axiom,
( member(X1,second(f28(X1,X2,X3)))
| ~ member(X1,apply(X2,X3)) ),
apply4,
[final] ).
cnf(i_0_216,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_178,c_0_159]),
[final] ).
cnf(i_0_217,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_179,c_0_159]),
[final] ).
cnf(i_0_218,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_180,c_0_159]),
[final] ).
cnf(i_0_219,plain,
( X2 = X4
| non_ordered_pair(non_ordered_pair(X1,X1),non_ordered_pair(X1,X2)) != non_ordered_pair(non_ordered_pair(X3,X3),non_ordered_pair(X3,X4))
| ~ little_set(X4)
| ~ little_set(X3)
| ~ little_set(X2)
| ~ little_set(X1) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_181,c_0_159]),c_0_159]),
[final] ).
cnf(i_0_220,plain,
( X1 = X2
| non_ordered_pair(non_ordered_pair(X1,X1),non_ordered_pair(X1,X3)) != non_ordered_pair(non_ordered_pair(X2,X2),non_ordered_pair(X2,X4))
| ~ little_set(X2)
| ~ little_set(X1) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[i_0_182,c_0_159]),c_0_159]),
[final] ).
cnf(i_0_221,axiom,
( member(f28(X1,X2,X3),X2)
| ~ member(X1,apply(X2,X3)) ),
apply2,
[final] ).
cnf(i_0_222,axiom,
( member(f22(X1,X2,X3),X3)
| ~ member(X1,image(X2,X3)) ),
image_and_substitution2,
[final] ).
cnf(i_0_223,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_183,c_0_159]),
[final] ).
cnf(i_0_224,axiom,
( second(f22(X1,X2,X3)) = X1
| ~ member(X1,image(X2,X3)) ),
image_and_substitution4,
[final] ).
cnf(i_0_225,axiom,
( first(f28(X1,X2,X3)) = X3
| ~ member(X1,apply(X2,X3)) ),
apply3,
[final] ).
cnf(i_0_226,axiom,
( ordered_pair_predicate(f28(X1,X2,X3))
| ~ member(X1,apply(X2,X3)) ),
apply1,
[final] ).
cnf(i_0_227,axiom,
( ordered_pair_predicate(f22(X1,X2,X3))
| ~ member(X1,image(X2,X3)) ),
image_and_substitution1,
[final] ).
cnf(i_0_228,axiom,
( little_set(f31(X1,X2,X3))
| ~ member(X1,compose(X2,X3)) ),
compose3,
[final] ).
cnf(i_0_229,axiom,
( little_set(f30(X1,X2,X3))
| ~ member(X1,compose(X2,X3)) ),
compose2,
[final] ).
cnf(i_0_230,axiom,
( little_set(f29(X1,X2,X3))
| ~ member(X1,compose(X2,X3)) ),
compose1,
[final] ).
cnf(i_0_231,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_184,c_0_159]),
[final] ).
cnf(i_0_232,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_185,c_0_159]),
[final] ).
cnf(i_0_233,axiom,
( closed(X1,X2)
| ~ little_set(X1)
| ~ little_set(X2)
| ~ maps(X2,cross_product(X1,X1),X1) ),
closed4,
[final] ).
cnf(i_0_234,plain,
( second(non_ordered_pair(non_ordered_pair(X1,X1),non_ordered_pair(X1,X2))) = X2
| ~ little_set(X2)
| ~ little_set(X1) ),
inference(rw,[status(thm)],[i_0_186,c_0_159]),
[final] ).
cnf(i_0_235,plain,
( first(non_ordered_pair(non_ordered_pair(X1,X1),non_ordered_pair(X1,X2))) = X1
| ~ little_set(X2)
| ~ little_set(X1) ),
inference(rw,[status(thm)],[i_0_187,c_0_159]),
[final] ).
cnf(i_0_236,plain,
little_set(non_ordered_pair(non_ordered_pair(X1,X1),non_ordered_pair(X1,X2))),
inference(rw,[status(thm)],[i_0_188,c_0_159]),
[final] ).
cnf(i_0_237,axiom,
( X1 = X2
| ~ member(f1(X1,X2),X1)
| ~ member(f1(X1,X2),X2) ),
extensionality3,
[final] ).
cnf(i_0_238,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_189,c_0_159]),
[final] ).
cnf(i_0_239,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_190,c_0_159]),
[final] ).
cnf(i_0_240,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_241,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_242,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_243,axiom,
( subset(range_of(X1),X3)
| ~ maps(X1,X2,X3) ),
maps3,
[final] ).
cnf(i_0_244,axiom,
( maps(X2,cross_product(X1,X1),X1)
| ~ closed(X1,X2) ),
closed3,
[final] ).
cnf(i_0_245,axiom,
( maps(X1,X2,X3)
| ~ function(X1)
| domain_of(X1) != X2
| ~ subset(range_of(X1),X3) ),
maps4,
[final] ).
cnf(i_0_246,axiom,
( domain_of(X1) = X2
| ~ maps(X1,X2,X3) ),
maps2,
[final] ).
cnf(i_0_247,axiom,
( function(X1)
| ~ maps(X1,X2,X3) ),
maps1,
[final] ).
cnf(i_0_248,axiom,
( member(X1,intersection(X2,X3))
| ~ member(X1,X2)
| ~ member(X1,X3) ),
intersection3,
[final] ).
cnf(i_0_249,axiom,
( member(second(X1),X3)
| ~ member(X1,cross_product(X2,X3)) ),
cross_product3,
[final] ).
cnf(i_0_250,axiom,
( member(first(X1),X2)
| ~ member(X1,cross_product(X2,X3)) ),
cross_product2,
[final] ).
cnf(i_0_251,axiom,
( member(f1(X1,X2),X1)
| member(f1(X1,X2),X2)
| X1 = X2 ),
extensionality2,
[final] ).
cnf(i_0_252,axiom,
( subset(X1,X2)
| ~ member(f17(X1,X2),X2) ),
subset3,
[final] ).
cnf(i_0_253,axiom,
( member(X1,X2)
| ~ member(X1,intersection(X2,X3)) ),
intersection1,
[final] ).
cnf(i_0_254,axiom,
( member(X1,X3)
| ~ member(X1,intersection(X2,X3)) ),
intersection2,
[final] ).
cnf(i_0_255,axiom,
( member(f27(X1,X2),X2)
| ~ member(X1,range_of(X2)) ),
range_of2,
[final] ).
cnf(i_0_256,axiom,
( member(f16(X1,X2),X2)
| ~ member(X1,sigma(X2)) ),
sigma1,
[final] ).
cnf(i_0_257,axiom,
( member(f8(X1,X2),X2)
| ~ member(X1,domain_of(X2)) ),
domain2,
[final] ).
cnf(i_0_258,axiom,
( member(X1,f16(X1,X2))
| ~ member(X1,sigma(X2)) ),
sigma2,
[final] ).
cnf(i_0_259,axiom,
( member(X1,f7(X1,X2))
| ~ member(X1,second(X2)) ),
second4,
[final] ).
cnf(i_0_260,axiom,
( member(X1,f4(X1,X2))
| ~ member(X1,first(X2)) ),
first4,
[final] ).
cnf(i_0_261,axiom,
( member(X1,estin)
| ~ little_set(X1)
| ~ ordered_pair_predicate(X1)
| ~ member(first(X1),second(X1)) ),
element_relation3,
[final] ).
cnf(i_0_262,axiom,
( ~ disjoint(X1,X2)
| ~ member(X3,X1)
| ~ member(X3,X2) ),
disjoint1,
[final] ).
cnf(i_0_263,axiom,
( X1 = X2
| X1 = X3
| ~ member(X1,non_ordered_pair(X2,X3)) ),
non_ordered_pair1,
[final] ).
cnf(i_0_264,axiom,
( ordered_pair_predicate(X1)
| ~ member(X1,cross_product(X2,X3)) ),
cross_product1,
[final] ).
cnf(i_0_265,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_266,axiom,
( member(X1,domain_of(X2))
| ~ little_set(X1)
| ~ ordered_pair_predicate(X3)
| ~ member(X3,X2)
| X1 != first(X3) ),
domain4,
[final] ).
cnf(i_0_267,axiom,
( member(X1,sigma(X2))
| ~ member(X3,X2)
| ~ member(X1,X3) ),
sigma3,
[final] ).
cnf(i_0_268,axiom,
( X1 = second(f27(X1,X2))
| ~ member(X1,range_of(X2)) ),
range_of3,
[final] ).
cnf(i_0_269,axiom,
( X1 = first(f8(X1,X2))
| ~ member(X1,domain_of(X2)) ),
domain3,
[final] ).
cnf(i_0_270,axiom,
( ordered_pair_predicate(f27(X1,X2))
| ~ member(X1,range_of(X2)) ),
range_of1,
[final] ).
cnf(i_0_271,axiom,
( ordered_pair_predicate(f8(X1,X2))
| ~ member(X1,domain_of(X2)) ),
domain1,
[final] ).
cnf(i_0_272,axiom,
( little_set(f14(X1,X2))
| ~ member(X1,flip_range_of(X2)) ),
flip_range3,
[final] ).
cnf(i_0_273,axiom,
( little_set(f13(X1,X2))
| ~ member(X1,flip_range_of(X2)) ),
flip_range2,
[final] ).
cnf(i_0_274,axiom,
( little_set(f12(X1,X2))
| ~ member(X1,flip_range_of(X2)) ),
flip_range1,
[final] ).
cnf(i_0_275,axiom,
( little_set(f11(X1,X2))
| ~ member(X1,rotate_right(X2)) ),
rotate_right3,
[final] ).
cnf(i_0_276,axiom,
( little_set(f10(X1,X2))
| ~ member(X1,rotate_right(X2)) ),
rotate_right2,
[final] ).
cnf(i_0_277,axiom,
( little_set(f9(X1,X2))
| ~ member(X1,rotate_right(X2)) ),
rotate_right1,
[final] ).
cnf(i_0_278,axiom,
( little_set(f7(X1,X2))
| ~ member(X1,second(X2)) ),
second2,
[final] ).
cnf(i_0_279,axiom,
( little_set(f6(X1,X2))
| ~ member(X1,second(X2)) ),
second1,
[final] ).
cnf(i_0_280,axiom,
( little_set(f5(X1,X2))
| ~ member(X1,first(X2)) ),
first2,
[final] ).
cnf(i_0_281,axiom,
( little_set(f4(X1,X2))
| ~ member(X1,first(X2)) ),
first1,
[final] ).
cnf(i_0_282,axiom,
( X1 = X2
| ~ little_set(X1)
| ~ little_set(X2)
| non_ordered_pair(X3,X1) != non_ordered_pair(X3,X2) ),
left_cancellation,
[final] ).
cnf(i_0_283,axiom,
( member(X3,X2)
| ~ subset(X1,X2)
| ~ member(X3,X1) ),
subset1,
[final] ).
cnf(i_0_284,axiom,
( ~ member(X1,complement(X2))
| ~ member(X1,X2) ),
complement1,
[final] ).
cnf(i_0_285,axiom,
( disjoint(X1,X2)
| member(f23(X1,X2),X1) ),
disjoint2,
[final] ).
cnf(i_0_286,axiom,
( disjoint(X1,X2)
| member(f23(X1,X2),X2) ),
disjoint3,
[final] ).
cnf(i_0_287,axiom,
( subset(X1,X2)
| member(f17(X1,X2),X1) ),
subset2,
[final] ).
cnf(i_0_288,axiom,
( member(X1,non_ordered_pair(X2,X3))
| ~ little_set(X1)
| X1 != X2 ),
non_ordered_pair2,
[final] ).
cnf(i_0_289,axiom,
( member(X1,non_ordered_pair(X2,X3))
| ~ little_set(X1)
| X1 != X3 ),
non_ordered_pair3,
[final] ).
cnf(i_0_290,axiom,
( member(X1,powerset(X2))
| ~ little_set(X1)
| ~ subset(X1,X2) ),
powerset2,
[final] ).
cnf(i_0_291,axiom,
( X1 = X2
| ~ subset(X1,X2)
| ~ subset(X2,X1) ),
two_sets_equal,
[final] ).
cnf(i_0_292,plain,
( member(X1,non_ordered_pair(X1,X1))
| ~ little_set(X1) ),
inference(rw,[status(thm)],[i_0_191,c_0_155]),
[final] ).
cnf(i_0_293,axiom,
( member(first(X1),second(X1))
| ~ member(X1,estin) ),
element_relation2,
[final] ).
cnf(i_0_294,axiom,
( subset(X1,X2)
| ~ member(X1,powerset(X2)) ),
powerset1,
[final] ).
cnf(i_0_295,axiom,
( little_set(image(X1,X2))
| ~ little_set(X1)
| ~ function(X2) ),
image_and_substitution6,
[final] ).
cnf(i_0_296,axiom,
( member(X1,complement(X2))
| member(X1,X2)
| ~ little_set(X1) ),
complement2,
[final] ).
cnf(i_0_297,axiom,
( member(X1,identity_relation)
| ~ little_set(X1)
| ~ ordered_pair_predicate(X1)
| first(X1) != second(X1) ),
identity_relation3,
[final] ).
cnf(i_0_298,axiom,
( proper_subset(X1,X2)
| X1 = X2
| ~ subset(X1,X2) ),
proper_subset3,
[final] ).
cnf(i_0_299,axiom,
( subset(X1,X2)
| ~ proper_subset(X1,X2) ),
proper_subset1,
[final] ).
cnf(i_0_300,axiom,
( ordered_pair_predicate(X1)
| ~ member(X1,converse(X2)) ),
converse1,
[final] ).
cnf(i_0_301,axiom,
( ordered_pair_predicate(X2)
| ~ relation(X1)
| ~ member(X2,X1) ),
relation1,
[final] ).
cnf(i_0_302,axiom,
( little_set(f1(X1,X2))
| X1 = X2 ),
extensionality1,
[final] ).
cnf(i_0_303,axiom,
little_set(non_ordered_pair(X1,X2)),
non_ordered_pair4,
[final] ).
cnf(i_0_304,axiom,
( X1 = empty_set
| member(f26(X1),X1)
| ~ little_set(X1) ),
choice2,
[final] ).
cnf(i_0_305,axiom,
( first(X1) = second(X1)
| ~ member(X1,identity_relation) ),
identity_relation2,
[final] ).
cnf(i_0_306,axiom,
( one_to_one_function(X1)
| ~ function(X1)
| ~ function(converse(X1)) ),
one_to_one_function3,
[final] ).
cnf(i_0_307,axiom,
( little_set(X1)
| ~ closed(X1,X2) ),
closed1,
[final] ).
cnf(i_0_308,axiom,
( little_set(X1)
| ~ member(X1,X2) ),
a2,
[final] ).
cnf(i_0_309,axiom,
( little_set(X2)
| ~ closed(X1,X2) ),
closed2,
[final] ).
cnf(i_0_310,axiom,
( ~ proper_subset(X1,X2)
| X1 != X2 ),
proper_subset2,
[final] ).
cnf(i_0_311,axiom,
( relation(X1)
| member(f18(X1),X1) ),
relation2,
[final] ).
cnf(i_0_312,axiom,
( ordered_pair_predicate(X1)
| ~ member(X1,identity_relation) ),
identity_relation1,
[final] ).
cnf(i_0_313,axiom,
( ordered_pair_predicate(X1)
| ~ member(X1,estin) ),
element_relation1,
[final] ).
cnf(i_0_314,axiom,
( X1 = empty_set
| disjoint(f24(X1),X1) ),
regularity2,
[final] ).
cnf(i_0_315,axiom,
( X1 = empty_set
| member(f24(X1),X1) ),
regularity1,
[final] ).
cnf(i_0_316,axiom,
( relation(X1)
| ~ ordered_pair_predicate(f18(X1)) ),
relation3,
[final] ).
cnf(i_0_317,axiom,
~ member(X1,empty_set),
empty_set,
[final] ).
cnf(i_0_318,axiom,
( member(X1,universal_set)
| ~ little_set(X1) ),
universal_set,
[final] ).
cnf(i_0_319,axiom,
( function(X1)
| ~ relation(X1)
| ~ single_valued_set(X1) ),
function3,
[final] ).
cnf(i_0_320,negated_conjecture,
~ subset(a,c),
prove_a_subset_c,
[final] ).
cnf(i_0_321,axiom,
( function(converse(X1))
| ~ one_to_one_function(X1) ),
one_to_one_function2,
[final] ).
cnf(i_0_322,axiom,
( little_set(powerset(X1))
| ~ little_set(X1) ),
powerset3,
[final] ).
cnf(i_0_323,axiom,
( little_set(sigma(X1))
| ~ little_set(X1) ),
sigma4,
[final] ).
cnf(i_0_324,axiom,
( little_set(second(X1))
| ~ ordered_pair_predicate(X1) ),
second_component_is_small,
[final] ).
cnf(i_0_325,axiom,
( little_set(first(X1))
| ~ ordered_pair_predicate(X1) ),
first_component_is_small,
[final] ).
cnf(i_0_326,axiom,
( little_set(f3(X1))
| ~ ordered_pair_predicate(X1) ),
ordered_pair_predicate2,
[final] ).
cnf(i_0_327,axiom,
( little_set(f2(X1))
| ~ ordered_pair_predicate(X1) ),
ordered_pair_predicate1,
[final] ).
cnf(i_0_328,axiom,
( single_valued_set(X1)
| f20(X1) != f21(X1) ),
single_valued_set7,
[final] ).
cnf(i_0_329,axiom,
( single_valued_set(X1)
| little_set(f21(X1)) ),
single_valued_set4,
[final] ).
cnf(i_0_330,axiom,
( single_valued_set(X1)
| little_set(f20(X1)) ),
single_valued_set3,
[final] ).
cnf(i_0_331,axiom,
( single_valued_set(X1)
| little_set(f19(X1)) ),
single_valued_set2,
[final] ).
cnf(i_0_332,axiom,
( function(X1)
| ~ one_to_one_function(X1) ),
one_to_one_function1,
[final] ).
cnf(i_0_333,axiom,
( single_valued_set(X1)
| ~ function(X1) ),
function2,
[final] ).
cnf(i_0_334,axiom,
( relation(X1)
| ~ function(X1) ),
function1,
[final] ).
cnf(i_0_335,axiom,
( little_set(X1)
| ~ ordered_pair_predicate(X1) ),
ordered_pairs_are_small2,
[final] ).
cnf(i_0_336,hypothesis,
subset(b,c),
b_subset_c,
[final] ).
cnf(i_0_337,hypothesis,
subset(a,b),
a_subset_b,
[final] ).
cnf(i_0_338,axiom,
member(empty_set,infinity),
infinity2,
[final] ).
cnf(i_0_339,axiom,
function(f25),
choice1,
[final] ).
cnf(i_0_340,axiom,
little_set(infinity),
infinity1,
[final] ).
cnf(i_0_341,axiom,
X1 = X1 ).
cnf(i_0_342,axiom,
( X1 = X2
| X2 != X1 ) ).
cnf(i_0_343,axiom,
( X1 = X2
| X1 != X3
| X3 != X2 ) ).
cnf(i_0_344,axiom,
( X1 != X2
| apply(X1,X3) = apply(X2,X3) ) ).
cnf(i_0_345,axiom,
( X1 != X2
| apply(X3,X1) = apply(X3,X2) ) ).
cnf(i_0_346,axiom,
( X1 != X2
| second(X1) = second(X2) ) ).
cnf(i_0_347,axiom,
( X1 != X2
| first(X1) = first(X2) ) ).
cnf(i_0_348,axiom,
( X1 != X2
| non_ordered_pair(X1,X3) = non_ordered_pair(X2,X3) ) ).
cnf(i_0_349,axiom,
( X1 != X2
| non_ordered_pair(X3,X1) = non_ordered_pair(X3,X2) ) ).
cnf(i_0_350,axiom,
( X1 != X2
| f21(X1) = f21(X2) ) ).
cnf(i_0_351,axiom,
( X1 != X2
| f20(X1) = f20(X2) ) ).
cnf(i_0_352,axiom,
( X1 != X2
| domain_of(X1) = domain_of(X2) ) ).
cnf(i_0_353,axiom,
( X1 != X2
| ~ homomorphism(X1,X3,X4,X5,X6)
| homomorphism(X2,X3,X4,X5,X6) ) ).
cnf(i_0_354,axiom,
( X1 != X2
| ~ homomorphism(X3,X1,X4,X5,X6)
| homomorphism(X3,X2,X4,X5,X6) ) ).
cnf(i_0_355,axiom,
( X1 != X2
| ~ homomorphism(X3,X4,X1,X5,X6)
| homomorphism(X3,X4,X2,X5,X6) ) ).
cnf(i_0_356,axiom,
( X1 != X2
| ~ homomorphism(X3,X4,X5,X1,X6)
| homomorphism(X3,X4,X5,X2,X6) ) ).
cnf(i_0_357,axiom,
( X1 != X2
| ~ homomorphism(X3,X4,X5,X6,X1)
| homomorphism(X3,X4,X5,X6,X2) ) ).
cnf(i_0_358,axiom,
( X1 != X2
| ~ disjoint(X1,X3)
| disjoint(X2,X3) ) ).
cnf(i_0_359,axiom,
( X1 != X2
| ~ disjoint(X3,X1)
| disjoint(X3,X2) ) ).
cnf(i_0_360,axiom,
( X1 != X2
| ~ proper_subset(X1,X3)
| proper_subset(X2,X3) ) ).
cnf(i_0_361,axiom,
( X1 != X2
| ~ proper_subset(X3,X1)
| proper_subset(X3,X2) ) ).
cnf(i_0_362,axiom,
( X1 != X2
| ~ relation(X1)
| relation(X2) ) ).
cnf(i_0_363,axiom,
( X1 != X2
| ~ one_to_one_function(X1)
| one_to_one_function(X2) ) ).
cnf(i_0_364,axiom,
( X1 != X2
| ~ closed(X1,X3)
| closed(X2,X3) ) ).
cnf(i_0_365,axiom,
( X1 != X2
| ~ closed(X3,X1)
| closed(X3,X2) ) ).
cnf(i_0_366,axiom,
( X1 != X2
| ~ maps(X1,X3,X4)
| maps(X2,X3,X4) ) ).
cnf(i_0_367,axiom,
( X1 != X2
| ~ maps(X3,X1,X4)
| maps(X3,X2,X4) ) ).
cnf(i_0_368,axiom,
( X1 != X2
| ~ maps(X3,X4,X1)
| maps(X3,X4,X2) ) ).
cnf(i_0_369,axiom,
( X1 != X2
| ~ member(X1,X3)
| member(X2,X3) ) ).
cnf(i_0_370,axiom,
( X1 != X2
| ~ member(X3,X1)
| member(X3,X2) ) ).
cnf(i_0_371,axiom,
( X1 != X2
| ~ little_set(X1)
| little_set(X2) ) ).
cnf(i_0_372,axiom,
( X1 != X2
| ~ single_valued_set(X1)
| single_valued_set(X2) ) ).
cnf(i_0_373,axiom,
( X1 != X2
| ~ ordered_pair_predicate(X1)
| ordered_pair_predicate(X2) ) ).
cnf(i_0_374,axiom,
( X1 != X2
| ~ subset(X1,X3)
| subset(X2,X3) ) ).
cnf(i_0_375,axiom,
( X1 != X2
| ~ subset(X3,X1)
| subset(X3,X2) ) ).
cnf(i_0_376,axiom,
( X1 != X2
| ~ function(X1)
| function(X2) ) ).
cnf(i_0_393,plain,
~ proper_subset(X1,X1),
inference(equality_inference,[],[310]) ).
cnf(i_0_394,plain,
subset(empty_set,X1),
inference(scs_inference,[],[i_0_317,i_0_287]) ).
cnf(i_0_395,plain,
~ member(X1,empty_set),
inference(rename_variables,[],[i_0_317]) ).
cnf(i_0_398,plain,
~ member(X1,empty_set),
inference(rename_variables,[],[i_0_317]) ).
cnf(i_0_401,plain,
~ member(X1,empty_set),
inference(rename_variables,[],[i_0_317]) ).
cnf(i_0_404,plain,
~ member(X1,empty_set),
inference(rename_variables,[],[i_0_317]) ).
cnf(i_0_407,plain,
~ member(X1,empty_set),
inference(rename_variables,[],[i_0_317]) ).
cnf(i_0_410,plain,
~ member(X1,empty_set),
inference(rename_variables,[],[i_0_317]) ).
cnf(i_0_413,plain,
~ member(X1,empty_set),
inference(rename_variables,[],[i_0_317]) ).
cnf(i_0_416,plain,
~ member(X1,empty_set),
inference(rename_variables,[],[i_0_317]) ).
cnf(i_0_421,plain,
~ member(X1,empty_set),
inference(rename_variables,[],[i_0_317]) ).
cnf(i_0_424,plain,
~ member(X1,empty_set),
inference(rename_variables,[],[i_0_317]) ).
cnf(i_0_427,plain,
~ member(X1,empty_set),
inference(rename_variables,[],[i_0_317]) ).
cnf(i_0_430,plain,
~ member(X1,empty_set),
inference(rename_variables,[],[i_0_317]) ).
cnf(i_0_433,plain,
~ member(X1,empty_set),
inference(rename_variables,[],[i_0_317]) ).
cnf(i_0_447,plain,
~ member(X1,empty_set),
inference(rename_variables,[],[i_0_317]) ).
cnf(i_0_450,plain,
~ member(X1,empty_set),
inference(rename_variables,[],[i_0_317]) ).
cnf(i_0_1029,plain,
~ member(X1,empty_set),
inference(rename_variables,[],[i_0_317]) ).
cnf(i_0_4655,plain,
little_set(non_ordered_pair(X1,X2)),
inference(rename_variables,[],[i_0_303]) ).
cnf(i_0_4658,plain,
little_set(non_ordered_pair(X1,X2)),
inference(rename_variables,[],[i_0_303]) ).
cnf(i_0_4817,plain,
little_set(non_ordered_pair(X1,X2)),
inference(rename_variables,[],[i_0_303]) ).
cnf(i_0_4821,plain,
little_set(non_ordered_pair(X1,X2)),
inference(rename_variables,[],[i_0_303]) ).
cnf(i_0_5036,plain,
little_set(non_ordered_pair(X1,X2)),
inference(rename_variables,[],[i_0_303]) ).
cnf(i_0_5153,plain,
little_set(non_ordered_pair(X1,X2)),
inference(rename_variables,[],[i_0_303]) ).
cnf(i_0_5272,plain,
little_set(non_ordered_pair(X1,X2)),
inference(rename_variables,[],[i_0_303]) ).
cnf(i_0_397,plain,
~ member(X1,flip_range_of(empty_set)),
inference(scs_inference,[],[i_0_317,i_0_395,i_0_287,i_0_196]) ).
cnf(i_0_400,plain,
~ member(X1,rotate_right(empty_set)),
inference(scs_inference,[],[i_0_317,i_0_395,i_0_398,i_0_287,i_0_196,i_0_197]) ).
cnf(i_0_403,plain,
~ member(X1,compose(X2,empty_set)),
inference(scs_inference,[],[i_0_317,i_0_395,i_0_398,i_0_401,i_0_287,i_0_196,i_0_197,i_0_199]) ).
cnf(i_0_406,plain,
~ member(X1,compose(empty_set,X2)),
inference(scs_inference,[],[i_0_317,i_0_395,i_0_398,i_0_401,i_0_404,i_0_287,i_0_196,i_0_197,i_0_199,i_0_200]) ).
cnf(i_0_409,plain,
~ member(X1,image(empty_set,X2)),
inference(scs_inference,[],[i_0_317,i_0_395,i_0_398,i_0_401,i_0_404,i_0_407,i_0_287,i_0_196,i_0_197,i_0_199,i_0_200,i_0_214]) ).
cnf(i_0_412,plain,
~ member(X1,converse(empty_set)),
inference(scs_inference,[],[i_0_317,i_0_395,i_0_398,i_0_401,i_0_404,i_0_407,i_0_410,i_0_287,i_0_196,i_0_197,i_0_199,i_0_200,i_0_214,i_0_216]) ).
cnf(i_0_415,plain,
single_valued_set(empty_set),
inference(scs_inference,[],[i_0_317,i_0_395,i_0_398,i_0_401,i_0_404,i_0_407,i_0_410,i_0_413,i_0_287,i_0_196,i_0_197,i_0_199,i_0_200,i_0_214,i_0_216,i_0_217]) ).
cnf(i_0_418,plain,
single_valued_set(compose(X1,empty_set)),
inference(scs_inference,[],[i_0_317,i_0_395,i_0_398,i_0_401,i_0_404,i_0_407,i_0_410,i_0_413,i_0_287,i_0_196,i_0_197,i_0_199,i_0_200,i_0_214,i_0_216,i_0_217,i_0_218]) ).
cnf(i_0_420,plain,
~ member(X1,cross_product(X2,empty_set)),
inference(scs_inference,[],[i_0_317,i_0_395,i_0_398,i_0_401,i_0_404,i_0_407,i_0_410,i_0_413,i_0_416,i_0_287,i_0_196,i_0_197,i_0_199,i_0_200,i_0_214,i_0_216,i_0_217,i_0_218,i_0_249]) ).
cnf(i_0_423,plain,
~ member(X1,cross_product(empty_set,X2)),
inference(scs_inference,[],[i_0_317,i_0_395,i_0_398,i_0_401,i_0_404,i_0_407,i_0_410,i_0_413,i_0_416,i_0_421,i_0_287,i_0_196,i_0_197,i_0_199,i_0_200,i_0_214,i_0_216,i_0_217,i_0_218,i_0_249,i_0_250]) ).
cnf(i_0_426,plain,
disjoint(empty_set,X1),
inference(scs_inference,[],[i_0_317,i_0_395,i_0_398,i_0_401,i_0_404,i_0_407,i_0_410,i_0_413,i_0_416,i_0_421,i_0_424,i_0_287,i_0_196,i_0_197,i_0_199,i_0_200,i_0_214,i_0_216,i_0_217,i_0_218,i_0_249,i_0_250,i_0_285]) ).
cnf(i_0_429,plain,
disjoint(X1,empty_set),
inference(scs_inference,[],[i_0_317,i_0_395,i_0_398,i_0_401,i_0_404,i_0_407,i_0_410,i_0_413,i_0_416,i_0_421,i_0_424,i_0_427,i_0_287,i_0_196,i_0_197,i_0_199,i_0_200,i_0_214,i_0_216,i_0_217,i_0_218,i_0_249,i_0_250,i_0_285,i_0_286]) ).
cnf(i_0_432,plain,
relation(empty_set),
inference(scs_inference,[],[i_0_317,i_0_395,i_0_398,i_0_401,i_0_404,i_0_407,i_0_410,i_0_413,i_0_416,i_0_421,i_0_424,i_0_427,i_0_430,i_0_287,i_0_196,i_0_197,i_0_199,i_0_200,i_0_214,i_0_216,i_0_217,i_0_218,i_0_249,i_0_250,i_0_285,i_0_286,i_0_311]) ).
cnf(i_0_435,plain,
flip_range_of(empty_set) = empty_set,
inference(scs_inference,[],[i_0_317,i_0_395,i_0_398,i_0_401,i_0_404,i_0_407,i_0_410,i_0_413,i_0_416,i_0_421,i_0_424,i_0_427,i_0_430,i_0_287,i_0_196,i_0_197,i_0_199,i_0_200,i_0_214,i_0_216,i_0_217,i_0_218,i_0_249,i_0_250,i_0_285,i_0_286,i_0_311,i_0_315]) ).
cnf(i_0_437,plain,
empty_set = flip_range_of(empty_set),
inference(scs_inference,[],[i_0_317,i_0_395,i_0_398,i_0_401,i_0_404,i_0_407,i_0_410,i_0_413,i_0_416,i_0_421,i_0_424,i_0_427,i_0_430,i_0_287,i_0_196,i_0_197,i_0_199,i_0_200,i_0_214,i_0_216,i_0_217,i_0_218,i_0_249,i_0_250,i_0_285,i_0_286,i_0_311,i_0_315,i_0_342]) ).
cnf(i_0_438,plain,
~ proper_subset(flip_range_of(empty_set),empty_set),
inference(scs_inference,[],[i_0_317,i_0_395,i_0_398,i_0_401,i_0_404,i_0_407,i_0_410,i_0_413,i_0_416,i_0_421,i_0_424,i_0_427,i_0_430,i_0_287,i_0_196,i_0_197,i_0_199,i_0_200,i_0_214,i_0_216,i_0_217,i_0_218,i_0_249,i_0_250,i_0_285,i_0_286,i_0_311,i_0_315,i_0_342,i_0_310]) ).
cnf(i_0_440,plain,
single_valued_set(f25),
inference(scs_inference,[],[i_0_317,i_0_395,i_0_398,i_0_401,i_0_404,i_0_407,i_0_410,i_0_413,i_0_416,i_0_421,i_0_424,i_0_427,i_0_430,i_0_339,i_0_287,i_0_196,i_0_197,i_0_199,i_0_200,i_0_214,i_0_216,i_0_217,i_0_218,i_0_249,i_0_250,i_0_285,i_0_286,i_0_311,i_0_315,i_0_342,i_0_310,i_0_333]) ).
cnf(i_0_442,plain,
relation(f25),
inference(scs_inference,[],[i_0_317,i_0_395,i_0_398,i_0_401,i_0_404,i_0_407,i_0_410,i_0_413,i_0_416,i_0_421,i_0_424,i_0_427,i_0_430,i_0_339,i_0_287,i_0_196,i_0_197,i_0_199,i_0_200,i_0_214,i_0_216,i_0_217,i_0_218,i_0_249,i_0_250,i_0_285,i_0_286,i_0_311,i_0_315,i_0_342,i_0_310,i_0_333,i_0_334]) ).
cnf(i_0_444,plain,
b != a,
inference(scs_inference,[],[i_0_320,i_0_317,i_0_395,i_0_398,i_0_401,i_0_404,i_0_407,i_0_410,i_0_413,i_0_416,i_0_421,i_0_424,i_0_427,i_0_430,i_0_336,i_0_339,i_0_287,i_0_196,i_0_197,i_0_199,i_0_200,i_0_214,i_0_216,i_0_217,i_0_218,i_0_249,i_0_250,i_0_285,i_0_286,i_0_311,i_0_315,i_0_342,i_0_310,i_0_333,i_0_334,i_0_374]) ).
cnf(i_0_445,plain,
b != c,
inference(scs_inference,[],[i_0_320,i_0_317,i_0_395,i_0_398,i_0_401,i_0_404,i_0_407,i_0_410,i_0_413,i_0_416,i_0_421,i_0_424,i_0_427,i_0_430,i_0_336,i_0_337,i_0_339,i_0_287,i_0_196,i_0_197,i_0_199,i_0_200,i_0_214,i_0_216,i_0_217,i_0_218,i_0_249,i_0_250,i_0_285,i_0_286,i_0_311,i_0_315,i_0_342,i_0_310,i_0_333,i_0_334,i_0_374,i_0_375]) ).
cnf(i_0_446,plain,
rotate_right(empty_set) = empty_set,
inference(scs_inference,[],[i_0_320,i_0_317,i_0_395,i_0_398,i_0_401,i_0_404,i_0_407,i_0_410,i_0_413,i_0_416,i_0_421,i_0_424,i_0_427,i_0_430,i_0_433,i_0_336,i_0_337,i_0_339,i_0_287,i_0_196,i_0_197,i_0_199,i_0_200,i_0_214,i_0_216,i_0_217,i_0_218,i_0_249,i_0_250,i_0_285,i_0_286,i_0_311,i_0_315,i_0_342,i_0_310,i_0_333,i_0_334,i_0_374,i_0_375,i_0_251]) ).
cnf(i_0_449,plain,
~ subset(infinity,empty_set),
inference(scs_inference,[],[i_0_320,i_0_317,i_0_395,i_0_398,i_0_401,i_0_404,i_0_407,i_0_410,i_0_413,i_0_416,i_0_421,i_0_424,i_0_427,i_0_430,i_0_433,i_0_447,i_0_336,i_0_337,i_0_338,i_0_339,i_0_287,i_0_196,i_0_197,i_0_199,i_0_200,i_0_214,i_0_216,i_0_217,i_0_218,i_0_249,i_0_250,i_0_285,i_0_286,i_0_311,i_0_315,i_0_342,i_0_310,i_0_333,i_0_334,i_0_374,i_0_375,i_0_251,i_0_283]) ).
cnf(i_0_452,plain,
~ subset(c,b),
inference(scs_inference,[],[i_0_320,i_0_317,i_0_395,i_0_398,i_0_401,i_0_404,i_0_407,i_0_410,i_0_413,i_0_416,i_0_421,i_0_424,i_0_427,i_0_430,i_0_433,i_0_447,i_0_336,i_0_337,i_0_338,i_0_339,i_0_287,i_0_196,i_0_197,i_0_199,i_0_200,i_0_214,i_0_216,i_0_217,i_0_218,i_0_249,i_0_250,i_0_285,i_0_286,i_0_311,i_0_315,i_0_342,i_0_310,i_0_333,i_0_334,i_0_374,i_0_375,i_0_251,i_0_283,i_0_291]) ).
cnf(i_0_454,plain,
proper_subset(b,c),
inference(scs_inference,[],[i_0_320,i_0_317,i_0_395,i_0_398,i_0_401,i_0_404,i_0_407,i_0_410,i_0_413,i_0_416,i_0_421,i_0_424,i_0_427,i_0_430,i_0_433,i_0_447,i_0_336,i_0_337,i_0_338,i_0_339,i_0_287,i_0_196,i_0_197,i_0_199,i_0_200,i_0_214,i_0_216,i_0_217,i_0_218,i_0_249,i_0_250,i_0_285,i_0_286,i_0_311,i_0_315,i_0_342,i_0_310,i_0_333,i_0_334,i_0_374,i_0_375,i_0_251,i_0_283,i_0_291,i_0_298]) ).
cnf(i_0_456,plain,
~ proper_subset(empty_set,flip_range_of(empty_set)),
inference(scs_inference,[],[i_0_320,i_0_317,i_0_395,i_0_398,i_0_401,i_0_404,i_0_407,i_0_410,i_0_413,i_0_416,i_0_421,i_0_424,i_0_427,i_0_430,i_0_433,i_0_447,i_0_336,i_0_337,i_0_393,i_0_338,i_0_339,i_0_287,i_0_196,i_0_197,i_0_199,i_0_200,i_0_214,i_0_216,i_0_217,i_0_218,i_0_249,i_0_250,i_0_285,i_0_286,i_0_311,i_0_315,i_0_342,i_0_310,i_0_333,i_0_334,i_0_374,i_0_375,i_0_251,i_0_283,i_0_291,i_0_298,i_0_361]) ).
cnf(i_0_457,plain,
~ proper_subset(X1,X1),
inference(rename_variables,[],[i_0_393]) ).
cnf(i_0_458,plain,
infinity != compose(empty_set,X1),
inference(scs_inference,[],[i_0_320,i_0_317,i_0_395,i_0_398,i_0_401,i_0_404,i_0_407,i_0_410,i_0_413,i_0_416,i_0_421,i_0_424,i_0_427,i_0_430,i_0_433,i_0_447,i_0_336,i_0_337,i_0_393,i_0_338,i_0_339,i_0_287,i_0_196,i_0_197,i_0_199,i_0_200,i_0_214,i_0_216,i_0_217,i_0_218,i_0_249,i_0_250,i_0_285,i_0_286,i_0_311,i_0_315,i_0_342,i_0_310,i_0_333,i_0_334,i_0_374,i_0_375,i_0_251,i_0_283,i_0_291,i_0_298,i_0_361,i_0_370]) ).
cnf(i_0_459,plain,
function(empty_set),
inference(scs_inference,[],[i_0_320,i_0_317,i_0_395,i_0_398,i_0_401,i_0_404,i_0_407,i_0_410,i_0_413,i_0_416,i_0_421,i_0_424,i_0_427,i_0_430,i_0_433,i_0_447,i_0_336,i_0_337,i_0_393,i_0_338,i_0_339,i_0_287,i_0_196,i_0_197,i_0_199,i_0_200,i_0_214,i_0_216,i_0_217,i_0_218,i_0_249,i_0_250,i_0_285,i_0_286,i_0_311,i_0_315,i_0_342,i_0_310,i_0_333,i_0_334,i_0_374,i_0_375,i_0_251,i_0_283,i_0_291,i_0_298,i_0_361,i_0_370,i_0_319]) ).
cnf(i_0_461,plain,
relation(flip_range_of(empty_set)),
inference(scs_inference,[],[i_0_320,i_0_317,i_0_395,i_0_398,i_0_401,i_0_404,i_0_407,i_0_410,i_0_413,i_0_416,i_0_421,i_0_424,i_0_427,i_0_430,i_0_433,i_0_447,i_0_336,i_0_337,i_0_393,i_0_338,i_0_339,i_0_287,i_0_196,i_0_197,i_0_199,i_0_200,i_0_214,i_0_216,i_0_217,i_0_218,i_0_249,i_0_250,i_0_285,i_0_286,i_0_311,i_0_315,i_0_342,i_0_310,i_0_333,i_0_334,i_0_374,i_0_375,i_0_251,i_0_283,i_0_291,i_0_298,i_0_361,i_0_370,i_0_319,i_0_362]) ).
cnf(i_0_462,plain,
single_valued_set(flip_range_of(empty_set)),
inference(scs_inference,[],[i_0_320,i_0_317,i_0_395,i_0_398,i_0_401,i_0_404,i_0_407,i_0_410,i_0_413,i_0_416,i_0_421,i_0_424,i_0_427,i_0_430,i_0_433,i_0_447,i_0_336,i_0_337,i_0_393,i_0_338,i_0_339,i_0_287,i_0_196,i_0_197,i_0_199,i_0_200,i_0_214,i_0_216,i_0_217,i_0_218,i_0_249,i_0_250,i_0_285,i_0_286,i_0_311,i_0_315,i_0_342,i_0_310,i_0_333,i_0_334,i_0_374,i_0_375,i_0_251,i_0_283,i_0_291,i_0_298,i_0_361,i_0_370,i_0_319,i_0_362,i_0_372]) ).
cnf(i_0_463,plain,
function(flip_range_of(empty_set)),
inference(scs_inference,[],[i_0_320,i_0_317,i_0_395,i_0_398,i_0_401,i_0_404,i_0_407,i_0_410,i_0_413,i_0_416,i_0_421,i_0_424,i_0_427,i_0_430,i_0_433,i_0_447,i_0_336,i_0_337,i_0_393,i_0_338,i_0_339,i_0_287,i_0_196,i_0_197,i_0_199,i_0_200,i_0_214,i_0_216,i_0_217,i_0_218,i_0_249,i_0_250,i_0_285,i_0_286,i_0_311,i_0_315,i_0_342,i_0_310,i_0_333,i_0_334,i_0_374,i_0_375,i_0_251,i_0_283,i_0_291,i_0_298,i_0_361,i_0_370,i_0_319,i_0_362,i_0_372,i_0_376]) ).
cnf(i_0_528,plain,
subset(empty_set,X1),
inference(rename_variables,[],[i_0_394]) ).
cnf(i_0_537,plain,
subset(empty_set,X1),
inference(rename_variables,[],[i_0_394]) ).
cnf(i_0_607,plain,
subset(empty_set,X1),
inference(rename_variables,[],[i_0_394]) ).
cnf(i_0_470,plain,
subset(compose(X1,empty_set),X2),
inference(scs_inference,[],[i_0_403,i_0_287]) ).
cnf(i_0_471,plain,
~ member(X1,compose(X2,empty_set)),
inference(rename_variables,[],[i_0_403]) ).
cnf(i_0_474,plain,
~ member(X1,compose(X2,empty_set)),
inference(rename_variables,[],[i_0_403]) ).
cnf(i_0_477,plain,
~ member(X1,compose(X2,empty_set)),
inference(rename_variables,[],[i_0_403]) ).
cnf(i_0_480,plain,
~ member(X1,compose(X2,empty_set)),
inference(rename_variables,[],[i_0_403]) ).
cnf(i_0_483,plain,
~ member(X1,compose(empty_set,X2)),
inference(rename_variables,[],[i_0_406]) ).
cnf(i_0_486,plain,
~ member(X1,compose(X2,empty_set)),
inference(rename_variables,[],[i_0_403]) ).
cnf(i_0_489,plain,
~ member(X1,compose(X2,empty_set)),
inference(rename_variables,[],[i_0_403]) ).
cnf(i_0_492,plain,
~ member(X1,compose(X2,empty_set)),
inference(rename_variables,[],[i_0_403]) ).
cnf(i_0_495,plain,
~ member(X1,compose(X2,empty_set)),
inference(rename_variables,[],[i_0_403]) ).
cnf(i_0_500,plain,
~ member(X1,compose(X2,empty_set)),
inference(rename_variables,[],[i_0_403]) ).
cnf(i_0_503,plain,
~ member(X1,compose(X2,empty_set)),
inference(rename_variables,[],[i_0_403]) ).
cnf(i_0_506,plain,
~ member(X1,compose(X2,empty_set)),
inference(rename_variables,[],[i_0_403]) ).
cnf(i_0_509,plain,
~ member(X1,image(empty_set,X2)),
inference(rename_variables,[],[i_0_409]) ).
cnf(i_0_512,plain,
~ member(X1,compose(X2,empty_set)),
inference(rename_variables,[],[i_0_403]) ).
cnf(i_0_515,plain,
~ member(X1,compose(X2,empty_set)),
inference(rename_variables,[],[i_0_403]) ).
cnf(i_0_519,plain,
~ member(X1,compose(empty_set,X2)),
inference(rename_variables,[],[i_0_406]) ).
cnf(i_0_520,plain,
~ member(X1,compose(X2,empty_set)),
inference(rename_variables,[],[i_0_403]) ).
cnf(i_0_523,plain,
~ member(X1,compose(X2,empty_set)),
inference(rename_variables,[],[i_0_403]) ).
cnf(i_0_532,plain,
~ member(X1,image(empty_set,X2)),
inference(rename_variables,[],[i_0_409]) ).
cnf(i_0_540,plain,
~ member(X1,image(empty_set,X2)),
inference(rename_variables,[],[i_0_409]) ).
cnf(i_0_550,plain,
subset(cross_product(X1,empty_set),X2),
inference(scs_inference,[],[i_0_420,i_0_287]) ).
cnf(i_0_551,plain,
~ member(X1,cross_product(X2,empty_set)),
inference(rename_variables,[],[i_0_420]) ).
cnf(i_0_554,plain,
~ member(X1,cross_product(X2,empty_set)),
inference(rename_variables,[],[i_0_420]) ).
cnf(i_0_557,plain,
~ member(X1,cross_product(X2,empty_set)),
inference(rename_variables,[],[i_0_420]) ).
cnf(i_0_560,plain,
~ member(X1,cross_product(X2,empty_set)),
inference(rename_variables,[],[i_0_420]) ).
cnf(i_0_563,plain,
~ member(X1,cross_product(X2,empty_set)),
inference(rename_variables,[],[i_0_420]) ).
cnf(i_0_566,plain,
~ member(X1,cross_product(X2,empty_set)),
inference(rename_variables,[],[i_0_420]) ).
cnf(i_0_569,plain,
~ member(X1,cross_product(X2,empty_set)),
inference(rename_variables,[],[i_0_420]) ).
cnf(i_0_572,plain,
~ member(X1,cross_product(X2,empty_set)),
inference(rename_variables,[],[i_0_420]) ).
cnf(i_0_575,plain,
~ member(X1,cross_product(X2,empty_set)),
inference(rename_variables,[],[i_0_420]) ).
cnf(i_0_578,plain,
~ member(X1,cross_product(X2,empty_set)),
inference(rename_variables,[],[i_0_420]) ).
cnf(i_0_581,plain,
~ member(X1,cross_product(X2,empty_set)),
inference(rename_variables,[],[i_0_420]) ).
cnf(i_0_584,plain,
~ member(X1,cross_product(X2,empty_set)),
inference(rename_variables,[],[i_0_420]) ).
cnf(i_0_587,plain,
~ member(X1,cross_product(X2,empty_set)),
inference(rename_variables,[],[i_0_420]) ).
cnf(i_0_590,plain,
~ member(X1,cross_product(X2,empty_set)),
inference(rename_variables,[],[i_0_420]) ).
cnf(i_0_593,plain,
~ member(X1,cross_product(empty_set,X2)),
inference(rename_variables,[],[i_0_423]) ).
cnf(i_0_600,plain,
~ member(X1,cross_product(empty_set,X2)),
inference(rename_variables,[],[i_0_423]) ).
cnf(i_0_601,plain,
~ member(X1,cross_product(X2,empty_set)),
inference(rename_variables,[],[i_0_420]) ).
cnf(i_0_604,plain,
~ member(X1,cross_product(X2,empty_set)),
inference(rename_variables,[],[i_0_420]) ).
cnf(i_0_621,plain,
~ member(X1,cross_product(empty_set,X2)),
inference(rename_variables,[],[i_0_423]) ).
cnf(i_0_628,plain,
~ member(X1,cross_product(X2,empty_set)),
inference(rename_variables,[],[i_0_420]) ).
cnf(i_0_789,plain,
infinity != compose(empty_set,X1),
inference(rename_variables,[],[i_0_458]) ).
cnf(i_0_849,plain,
~ member(X1,rotate_right(empty_set)),
inference(rename_variables,[],[i_0_400]) ).
cnf(i_0_853,plain,
~ member(X1,flip_range_of(empty_set)),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_880,plain,
~ member(X1,converse(empty_set)),
inference(rename_variables,[],[i_0_412]) ).
cnf(i_0_885,plain,
~ member(X1,converse(empty_set)),
inference(rename_variables,[],[i_0_412]) ).
cnf(i_0_892,plain,
subset(compose(empty_set,X1),X2),
inference(scs_inference,[],[i_0_406,i_0_287]) ).
cnf(i_0_893,plain,
~ member(X1,compose(empty_set,X2)),
inference(rename_variables,[],[i_0_406]) ).
cnf(i_0_896,plain,
~ member(X1,compose(empty_set,X2)),
inference(rename_variables,[],[i_0_406]) ).
cnf(i_0_899,plain,
~ member(X1,compose(empty_set,X2)),
inference(rename_variables,[],[i_0_406]) ).
cnf(i_0_902,plain,
~ member(X1,image(empty_set,X2)),
inference(rename_variables,[],[i_0_409]) ).
cnf(i_0_905,plain,
~ member(X1,image(empty_set,X2)),
inference(rename_variables,[],[i_0_409]) ).
cnf(i_0_910,plain,
~ member(X1,compose(empty_set,X2)),
inference(rename_variables,[],[i_0_406]) ).
cnf(i_0_913,plain,
~ member(X1,compose(empty_set,X2)),
inference(rename_variables,[],[i_0_406]) ).
cnf(i_0_916,plain,
~ member(X1,compose(empty_set,X2)),
inference(rename_variables,[],[i_0_406]) ).
cnf(i_0_919,plain,
~ member(X1,compose(empty_set,X2)),
inference(rename_variables,[],[i_0_406]) ).
cnf(i_0_922,plain,
~ member(X1,compose(empty_set,X2)),
inference(rename_variables,[],[i_0_406]) ).
cnf(i_0_925,plain,
~ member(X1,compose(empty_set,X2)),
inference(rename_variables,[],[i_0_406]) ).
cnf(i_0_928,plain,
~ member(X1,compose(empty_set,X2)),
inference(rename_variables,[],[i_0_406]) ).
cnf(i_0_931,plain,
~ member(X1,compose(empty_set,X2)),
inference(rename_variables,[],[i_0_406]) ).
cnf(i_0_937,plain,
~ member(X1,converse(empty_set)),
inference(rename_variables,[],[i_0_412]) ).
cnf(i_0_943,plain,
~ member(X1,image(empty_set,X2)),
inference(rename_variables,[],[i_0_409]) ).
cnf(i_0_944,plain,
~ member(X1,compose(X2,empty_set)),
inference(rename_variables,[],[i_0_403]) ).
cnf(i_0_973,plain,
~ member(X1,compose(X2,empty_set)),
inference(rename_variables,[],[i_0_403]) ).
cnf(i_0_993,plain,
~ member(X1,rotate_right(empty_set)),
inference(rename_variables,[],[i_0_400]) ).
cnf(i_0_1059,plain,
subset(cross_product(empty_set,X1),X2),
inference(scs_inference,[],[i_0_423,i_0_287]) ).
cnf(i_0_1060,plain,
~ member(X1,cross_product(empty_set,X2)),
inference(rename_variables,[],[i_0_423]) ).
cnf(i_0_1063,plain,
~ member(X1,cross_product(empty_set,X2)),
inference(rename_variables,[],[i_0_423]) ).
cnf(i_0_1066,plain,
~ member(X1,cross_product(empty_set,X2)),
inference(rename_variables,[],[i_0_423]) ).
cnf(i_0_1071,plain,
~ member(X1,cross_product(empty_set,X2)),
inference(rename_variables,[],[i_0_423]) ).
cnf(i_0_1074,plain,
~ member(X1,cross_product(empty_set,X2)),
inference(rename_variables,[],[i_0_423]) ).
cnf(i_0_1077,plain,
~ member(X1,cross_product(empty_set,X2)),
inference(rename_variables,[],[i_0_423]) ).
cnf(i_0_1080,plain,
~ member(X1,cross_product(empty_set,X2)),
inference(rename_variables,[],[i_0_423]) ).
cnf(i_0_1083,plain,
~ member(X1,cross_product(empty_set,X2)),
inference(rename_variables,[],[i_0_423]) ).
cnf(i_0_1086,plain,
~ member(X1,cross_product(empty_set,X2)),
inference(rename_variables,[],[i_0_423]) ).
cnf(i_0_1089,plain,
~ member(X1,cross_product(empty_set,X2)),
inference(rename_variables,[],[i_0_423]) ).
cnf(i_0_1092,plain,
~ member(X1,cross_product(empty_set,X2)),
inference(rename_variables,[],[i_0_423]) ).
cnf(i_0_1095,plain,
~ member(X1,cross_product(empty_set,X2)),
inference(rename_variables,[],[i_0_423]) ).
cnf(i_0_1112,plain,
~ member(X1,cross_product(X2,empty_set)),
inference(rename_variables,[],[i_0_420]) ).
cnf(i_0_1139,plain,
~ member(X1,flip_range_of(empty_set)),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_1142,plain,
~ member(X1,flip_range_of(empty_set)),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_1145,plain,
~ member(X1,flip_range_of(empty_set)),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_1151,plain,
~ member(X1,flip_range_of(empty_set)),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_1154,plain,
~ member(X1,flip_range_of(empty_set)),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_1157,plain,
~ member(X1,flip_range_of(empty_set)),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_1160,plain,
~ member(X1,flip_range_of(empty_set)),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_1163,plain,
~ member(X1,flip_range_of(empty_set)),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_1166,plain,
~ member(X1,flip_range_of(empty_set)),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_1169,plain,
~ member(X1,flip_range_of(empty_set)),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_1172,plain,
~ member(X1,flip_range_of(empty_set)),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_1189,plain,
~ member(X1,compose(empty_set,X2)),
inference(rename_variables,[],[i_0_406]) ).
cnf(i_0_1190,plain,
~ member(X1,flip_range_of(empty_set)),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_1213,plain,
~ member(X1,flip_range_of(empty_set)),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_1218,plain,
~ member(X1,image(empty_set,X2)),
inference(rename_variables,[],[i_0_409]) ).
cnf(i_0_1221,plain,
~ member(X1,image(empty_set,X2)),
inference(rename_variables,[],[i_0_409]) ).
cnf(i_0_1224,plain,
~ member(X1,image(empty_set,X2)),
inference(rename_variables,[],[i_0_409]) ).
cnf(i_0_1227,plain,
~ member(X1,image(empty_set,X2)),
inference(rename_variables,[],[i_0_409]) ).
cnf(i_0_1230,plain,
~ member(X1,image(empty_set,X2)),
inference(rename_variables,[],[i_0_409]) ).
cnf(i_0_1233,plain,
~ member(X1,image(empty_set,X2)),
inference(rename_variables,[],[i_0_409]) ).
cnf(i_0_1239,plain,
~ member(X1,image(empty_set,X2)),
inference(rename_variables,[],[i_0_409]) ).
cnf(i_0_1242,plain,
~ member(X1,image(empty_set,X2)),
inference(rename_variables,[],[i_0_409]) ).
cnf(i_0_1245,plain,
~ member(X1,image(empty_set,X2)),
inference(rename_variables,[],[i_0_409]) ).
cnf(i_0_1248,plain,
~ member(X1,image(empty_set,X2)),
inference(rename_variables,[],[i_0_409]) ).
cnf(i_0_1251,plain,
~ member(X1,image(empty_set,X2)),
inference(rename_variables,[],[i_0_409]) ).
cnf(i_0_1269,plain,
~ member(X1,compose(X2,empty_set)),
inference(rename_variables,[],[i_0_403]) ).
cnf(i_0_1295,plain,
~ member(X1,compose(X2,empty_set)),
inference(rename_variables,[],[i_0_403]) ).
cnf(i_0_1383,plain,
~ member(X1,rotate_right(empty_set)),
inference(rename_variables,[],[i_0_400]) ).
cnf(i_0_1386,plain,
~ member(X1,rotate_right(empty_set)),
inference(rename_variables,[],[i_0_400]) ).
cnf(i_0_1389,plain,
~ member(X1,rotate_right(empty_set)),
inference(rename_variables,[],[i_0_400]) ).
cnf(i_0_1392,plain,
~ member(X1,rotate_right(empty_set)),
inference(rename_variables,[],[i_0_400]) ).
cnf(i_0_1395,plain,
~ member(X1,rotate_right(empty_set)),
inference(rename_variables,[],[i_0_400]) ).
cnf(i_0_1398,plain,
~ member(X1,rotate_right(empty_set)),
inference(rename_variables,[],[i_0_400]) ).
cnf(i_0_1401,plain,
~ member(X1,rotate_right(empty_set)),
inference(rename_variables,[],[i_0_400]) ).
cnf(i_0_1404,plain,
~ member(X1,rotate_right(empty_set)),
inference(rename_variables,[],[i_0_400]) ).
cnf(i_0_1407,plain,
~ member(X1,rotate_right(empty_set)),
inference(rename_variables,[],[i_0_400]) ).
cnf(i_0_1410,plain,
~ member(X1,rotate_right(empty_set)),
inference(rename_variables,[],[i_0_400]) ).
cnf(i_0_1413,plain,
~ member(X1,rotate_right(empty_set)),
inference(rename_variables,[],[i_0_400]) ).
cnf(i_0_1416,plain,
~ member(X1,converse(empty_set)),
inference(rename_variables,[],[i_0_412]) ).
cnf(i_0_1419,plain,
~ member(X1,converse(empty_set)),
inference(rename_variables,[],[i_0_412]) ).
cnf(i_0_1433,plain,
~ member(X1,flip_range_of(empty_set)),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_1434,plain,
~ member(X1,cross_product(X2,empty_set)),
inference(rename_variables,[],[i_0_420]) ).
cnf(i_0_1456,plain,
~ member(X1,cross_product(X2,empty_set)),
inference(rename_variables,[],[i_0_420]) ).
cnf(i_0_1513,plain,
~ member(X1,compose(X2,empty_set)),
inference(rename_variables,[],[i_0_403]) ).
cnf(i_0_1514,plain,
~ member(X1,cross_product(empty_set,X2)),
inference(rename_variables,[],[i_0_423]) ).
cnf(i_0_1536,plain,
~ member(X1,cross_product(empty_set,X2)),
inference(rename_variables,[],[i_0_423]) ).
cnf(i_0_1595,plain,
~ member(X1,image(empty_set,X2)),
inference(rename_variables,[],[i_0_409]) ).
cnf(i_0_1596,plain,
~ member(X1,compose(empty_set,X2)),
inference(rename_variables,[],[i_0_406]) ).
cnf(i_0_1627,plain,
~ member(X1,converse(empty_set)),
inference(rename_variables,[],[i_0_412]) ).
cnf(i_0_1630,plain,
~ member(X1,converse(empty_set)),
inference(rename_variables,[],[i_0_412]) ).
cnf(i_0_1633,plain,
~ member(X1,converse(empty_set)),
inference(rename_variables,[],[i_0_412]) ).
cnf(i_0_1636,plain,
~ member(X1,converse(empty_set)),
inference(rename_variables,[],[i_0_412]) ).
cnf(i_0_1639,plain,
~ member(X1,converse(empty_set)),
inference(rename_variables,[],[i_0_412]) ).
cnf(i_0_1642,plain,
~ member(X1,converse(empty_set)),
inference(rename_variables,[],[i_0_412]) ).
cnf(i_0_1645,plain,
~ member(X1,converse(empty_set)),
inference(rename_variables,[],[i_0_412]) ).
cnf(i_0_1648,plain,
~ member(X1,converse(empty_set)),
inference(rename_variables,[],[i_0_412]) ).
cnf(i_0_1651,plain,
~ member(X1,converse(empty_set)),
inference(rename_variables,[],[i_0_412]) ).
cnf(i_0_1654,plain,
~ member(X1,converse(empty_set)),
inference(rename_variables,[],[i_0_412]) ).
cnf(i_0_1657,plain,
~ member(X1,converse(empty_set)),
inference(rename_variables,[],[i_0_412]) ).
cnf(i_0_1752,plain,
~ member(X1,cross_product(empty_set,X2)),
inference(rename_variables,[],[i_0_423]) ).
cnf(i_0_1837,plain,
~ member(X1,compose(X2,empty_set)),
inference(rename_variables,[],[i_0_403]) ).
cnf(i_0_1915,plain,
~ member(X1,compose(empty_set,X2)),
inference(rename_variables,[],[i_0_406]) ).
cnf(i_0_1916,plain,
~ member(X1,cross_product(X2,empty_set)),
inference(rename_variables,[],[i_0_420]) ).
cnf(i_0_1935,plain,
~ member(X1,cross_product(X2,empty_set)),
inference(rename_variables,[],[i_0_420]) ).
cnf(i_0_1992,plain,
~ member(X1,image(empty_set,X2)),
inference(rename_variables,[],[i_0_409]) ).
cnf(i_0_1993,plain,
~ member(X1,flip_range_of(empty_set)),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_2013,plain,
~ member(X1,flip_range_of(empty_set)),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_2153,plain,
~ member(X1,flip_range_of(empty_set)),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_2233,plain,
~ member(X1,cross_product(X2,empty_set)),
inference(rename_variables,[],[i_0_420]) ).
cnf(i_0_2260,plain,
single_valued_set(compose(X1,empty_set)),
inference(rename_variables,[],[i_0_418]) ).
cnf(i_0_2261,plain,
~ member(X1,image(empty_set,X2)),
inference(rename_variables,[],[i_0_409]) ).
cnf(i_0_2317,plain,
~ member(X1,cross_product(empty_set,X2)),
inference(rename_variables,[],[i_0_423]) ).
cnf(i_0_2338,plain,
~ member(X1,cross_product(empty_set,X2)),
inference(rename_variables,[],[i_0_423]) ).
cnf(i_0_2397,plain,
~ member(X1,compose(X2,empty_set)),
inference(rename_variables,[],[i_0_403]) ).
cnf(i_0_2472,plain,
~ member(X1,compose(empty_set,X2)),
inference(rename_variables,[],[i_0_406]) ).
cnf(i_0_2490,plain,
~ member(X1,compose(empty_set,X2)),
inference(rename_variables,[],[i_0_406]) ).
cnf(i_0_2547,plain,
~ member(X1,cross_product(X2,empty_set)),
inference(rename_variables,[],[i_0_420]) ).
cnf(i_0_2548,plain,
~ member(X1,image(empty_set,X2)),
inference(rename_variables,[],[i_0_409]) ).
cnf(i_0_2567,plain,
~ member(X1,image(empty_set,X2)),
inference(rename_variables,[],[i_0_409]) ).
cnf(i_0_2624,plain,
~ member(X1,flip_range_of(empty_set)),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_2625,plain,
~ member(X1,rotate_right(empty_set)),
inference(rename_variables,[],[i_0_400]) ).
cnf(i_0_2643,plain,
~ member(X1,rotate_right(empty_set)),
inference(rename_variables,[],[i_0_400]) ).
cnf(i_0_2781,plain,
~ member(X1,cross_product(empty_set,X2)),
inference(rename_variables,[],[i_0_423]) ).
cnf(i_0_2861,plain,
~ member(X1,compose(empty_set,X2)),
inference(rename_variables,[],[i_0_406]) ).
cnf(i_0_2939,plain,
~ member(X1,image(empty_set,X2)),
inference(rename_variables,[],[i_0_409]) ).
cnf(i_0_3013,plain,
~ member(X1,compose(X2,empty_set)),
inference(rename_variables,[],[i_0_403]) ).
cnf(i_0_3030,plain,
~ member(X1,compose(X2,empty_set)),
inference(rename_variables,[],[i_0_403]) ).
cnf(i_0_3085,plain,
~ member(X1,rotate_right(empty_set)),
inference(rename_variables,[],[i_0_400]) ).
cnf(i_0_3153,plain,
~ member(X1,converse(empty_set)),
inference(rename_variables,[],[i_0_412]) ).
cnf(i_0_3164,plain,
~ member(X1,converse(empty_set)),
inference(rename_variables,[],[i_0_412]) ).
cnf(i_0_3183,plain,
~ member(X1,converse(empty_set)),
inference(rename_variables,[],[i_0_412]) ).
cnf(i_0_3187,plain,
single_valued_set(compose(X1,empty_set)),
inference(rename_variables,[],[i_0_418]) ).
cnf(i_0_3188,plain,
~ member(X1,image(empty_set,X2)),
inference(rename_variables,[],[i_0_409]) ).
cnf(i_0_3246,plain,
~ member(X1,cross_product(X2,empty_set)),
inference(rename_variables,[],[i_0_420]) ).
cnf(i_0_3271,plain,
~ member(X1,cross_product(X2,empty_set)),
inference(rename_variables,[],[i_0_420]) ).
cnf(i_0_3332,plain,
~ member(X1,flip_range_of(empty_set)),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_3333,plain,
~ member(X1,cross_product(empty_set,X2)),
inference(rename_variables,[],[i_0_423]) ).
cnf(i_0_3352,plain,
~ member(X1,cross_product(empty_set,X2)),
inference(rename_variables,[],[i_0_423]) ).
cnf(i_0_3433,plain,
single_valued_set(compose(X1,empty_set)),
inference(rename_variables,[],[i_0_418]) ).
cnf(i_0_3434,plain,
~ member(X1,image(empty_set,X2)),
inference(rename_variables,[],[i_0_409]) ).
cnf(i_0_3492,plain,
~ member(X1,converse(empty_set)),
inference(rename_variables,[],[i_0_412]) ).
cnf(i_0_3569,plain,
~ member(X1,image(empty_set,X2)),
inference(rename_variables,[],[i_0_409]) ).
cnf(i_0_3643,plain,
~ member(X1,flip_range_of(empty_set)),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_3720,plain,
~ member(X1,compose(empty_set,X2)),
inference(rename_variables,[],[i_0_406]) ).
cnf(i_0_3796,plain,
~ member(X1,cross_product(empty_set,X2)),
inference(rename_variables,[],[i_0_423]) ).
cnf(i_0_3797,plain,
~ member(X1,compose(X2,empty_set)),
inference(rename_variables,[],[i_0_403]) ).
cnf(i_0_3951,plain,
~ member(X1,converse(empty_set)),
inference(rename_variables,[],[i_0_412]) ).
cnf(i_0_4099,plain,
~ member(X1,cross_product(X2,empty_set)),
inference(rename_variables,[],[i_0_420]) ).
cnf(i_0_4100,plain,
~ member(X1,rotate_right(empty_set)),
inference(rename_variables,[],[i_0_400]) ).
cnf(i_0_4118,plain,
~ member(X1,rotate_right(empty_set)),
inference(rename_variables,[],[i_0_400]) ).
cnf(i_0_4198,plain,
single_valued_set(compose(X1,empty_set)),
inference(rename_variables,[],[i_0_418]) ).
cnf(i_0_4199,plain,
~ member(X1,image(empty_set,X2)),
inference(rename_variables,[],[i_0_409]) ).
cnf(i_0_4407,plain,
~ member(X1,image(empty_set,X2)),
inference(rename_variables,[],[i_0_409]) ).
cnf(i_0_4485,plain,
~ member(X1,flip_range_of(empty_set)),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_4486,plain,
~ member(X1,compose(X2,empty_set)),
inference(rename_variables,[],[i_0_403]) ).
cnf(i_0_4505,plain,
~ member(X1,compose(X2,empty_set)),
inference(rename_variables,[],[i_0_403]) ).
cnf(i_0_4507,plain,
single_valued_set(compose(X1,empty_set)),
inference(rename_variables,[],[i_0_418]) ).
cnf(i_0_4563,plain,
~ member(X1,cross_product(empty_set,X2)),
inference(rename_variables,[],[i_0_423]) ).
cnf(i_0_4564,plain,
~ member(X1,compose(empty_set,X2)),
inference(rename_variables,[],[i_0_406]) ).
cnf(i_0_4581,plain,
~ member(X1,compose(empty_set,X2)),
inference(rename_variables,[],[i_0_406]) ).
cnf(i_0_4839,plain,
~ member(X1,flip_range_of(empty_set)),
inference(rename_variables,[],[i_0_397]) ).
cnf(i_0_473,plain,
~ member(X1,flip_range_of(compose(X2,empty_set))),
inference(scs_inference,[],[i_0_403,i_0_471,i_0_287,i_0_196]) ).
cnf(i_0_476,plain,
~ member(X1,rotate_right(compose(X2,empty_set))),
inference(scs_inference,[],[i_0_403,i_0_471,i_0_474,i_0_287,i_0_196,i_0_197]) ).
cnf(i_0_479,plain,
~ member(X1,compose(X2,compose(X3,empty_set))),
inference(scs_inference,[],[i_0_403,i_0_471,i_0_474,i_0_477,i_0_287,i_0_196,i_0_197,i_0_199]) ).
cnf(i_0_482,plain,
single_valued_set(compose(empty_set,X1)),
inference(scs_inference,[],[i_0_403,i_0_471,i_0_474,i_0_477,i_0_406,i_0_287,i_0_196,i_0_197,i_0_199,i_0_217]) ).
cnf(i_0_485,plain,
disjoint(compose(X1,empty_set),X2),
inference(scs_inference,[],[i_0_403,i_0_471,i_0_474,i_0_477,i_0_480,i_0_406,i_0_287,i_0_196,i_0_197,i_0_199,i_0_217,i_0_285]) ).
cnf(i_0_488,plain,
disjoint(X1,compose(X2,empty_set)),
inference(scs_inference,[],[i_0_403,i_0_471,i_0_474,i_0_477,i_0_480,i_0_486,i_0_406,i_0_287,i_0_196,i_0_197,i_0_199,i_0_217,i_0_285,i_0_286]) ).
cnf(i_0_491,plain,
relation(compose(X1,empty_set)),
inference(scs_inference,[],[i_0_403,i_0_471,i_0_474,i_0_477,i_0_480,i_0_486,i_0_489,i_0_406,i_0_287,i_0_196,i_0_197,i_0_199,i_0_217,i_0_285,i_0_286,i_0_311]) ).
cnf(i_0_494,plain,
compose(X1,empty_set) = empty_set,
inference(scs_inference,[],[i_0_403,i_0_471,i_0_474,i_0_477,i_0_480,i_0_486,i_0_489,i_0_492,i_0_406,i_0_287,i_0_196,i_0_197,i_0_199,i_0_217,i_0_285,i_0_286,i_0_311,i_0_315]) ).
cnf(i_0_497,plain,
~ proper_subset(rotate_right(empty_set),empty_set),
inference(scs_inference,[],[i_0_403,i_0_471,i_0_474,i_0_477,i_0_480,i_0_486,i_0_489,i_0_492,i_0_406,i_0_446,i_0_287,i_0_196,i_0_197,i_0_199,i_0_217,i_0_285,i_0_286,i_0_311,i_0_315,i_0_310]) ).
cnf(i_0_499,plain,
~ member(X1,compose(compose(X2,empty_set),X3)),
inference(scs_inference,[],[i_0_403,i_0_471,i_0_474,i_0_477,i_0_480,i_0_486,i_0_489,i_0_492,i_0_495,i_0_406,i_0_446,i_0_287,i_0_196,i_0_197,i_0_199,i_0_217,i_0_285,i_0_286,i_0_311,i_0_315,i_0_310,i_0_200]) ).
cnf(i_0_502,plain,
~ member(X1,image(compose(X2,empty_set),X3)),
inference(scs_inference,[],[i_0_403,i_0_471,i_0_474,i_0_477,i_0_480,i_0_486,i_0_489,i_0_492,i_0_495,i_0_500,i_0_406,i_0_446,i_0_287,i_0_196,i_0_197,i_0_199,i_0_217,i_0_285,i_0_286,i_0_311,i_0_315,i_0_310,i_0_200,i_0_214]) ).
cnf(i_0_505,plain,
~ member(X1,converse(compose(X2,empty_set))),
inference(scs_inference,[],[i_0_403,i_0_471,i_0_474,i_0_477,i_0_480,i_0_486,i_0_489,i_0_492,i_0_495,i_0_500,i_0_503,i_0_406,i_0_446,i_0_287,i_0_196,i_0_197,i_0_199,i_0_217,i_0_285,i_0_286,i_0_311,i_0_315,i_0_310,i_0_200,i_0_214,i_0_216]) ).
cnf(i_0_508,plain,
single_valued_set(image(empty_set,X1)),
inference(scs_inference,[],[i_0_403,i_0_471,i_0_474,i_0_477,i_0_480,i_0_486,i_0_489,i_0_492,i_0_495,i_0_500,i_0_503,i_0_406,i_0_409,i_0_446,i_0_287,i_0_196,i_0_197,i_0_199,i_0_217,i_0_285,i_0_286,i_0_311,i_0_315,i_0_310,i_0_200,i_0_214,i_0_216,i_0_218]) ).
cnf(i_0_511,plain,
~ member(X1,cross_product(X2,compose(X3,empty_set))),
inference(scs_inference,[],[i_0_403,i_0_471,i_0_474,i_0_477,i_0_480,i_0_486,i_0_489,i_0_492,i_0_495,i_0_500,i_0_503,i_0_506,i_0_406,i_0_409,i_0_446,i_0_287,i_0_196,i_0_197,i_0_199,i_0_217,i_0_285,i_0_286,i_0_311,i_0_315,i_0_310,i_0_200,i_0_214,i_0_216,i_0_218,i_0_249]) ).
cnf(i_0_514,plain,
~ member(X1,cross_product(compose(X2,empty_set),X3)),
inference(scs_inference,[],[i_0_403,i_0_471,i_0_474,i_0_477,i_0_480,i_0_486,i_0_489,i_0_492,i_0_495,i_0_500,i_0_503,i_0_506,i_0_512,i_0_406,i_0_409,i_0_446,i_0_287,i_0_196,i_0_197,i_0_199,i_0_217,i_0_285,i_0_286,i_0_311,i_0_315,i_0_310,i_0_200,i_0_214,i_0_216,i_0_218,i_0_249,i_0_250]) ).
cnf(i_0_517,plain,
empty_set = rotate_right(empty_set),
inference(scs_inference,[],[i_0_403,i_0_471,i_0_474,i_0_477,i_0_480,i_0_486,i_0_489,i_0_492,i_0_495,i_0_500,i_0_503,i_0_506,i_0_512,i_0_406,i_0_409,i_0_446,i_0_287,i_0_196,i_0_197,i_0_199,i_0_217,i_0_285,i_0_286,i_0_311,i_0_315,i_0_310,i_0_200,i_0_214,i_0_216,i_0_218,i_0_249,i_0_250,i_0_342]) ).
cnf(i_0_518,plain,
compose(empty_set,X1) = compose(X2,empty_set),
inference(scs_inference,[],[i_0_403,i_0_471,i_0_474,i_0_477,i_0_480,i_0_486,i_0_489,i_0_492,i_0_495,i_0_500,i_0_503,i_0_506,i_0_512,i_0_515,i_0_406,i_0_483,i_0_409,i_0_446,i_0_287,i_0_196,i_0_197,i_0_199,i_0_217,i_0_285,i_0_286,i_0_311,i_0_315,i_0_310,i_0_200,i_0_214,i_0_216,i_0_218,i_0_249,i_0_250,i_0_342,i_0_251]) ).
cnf(i_0_522,plain,
~ subset(infinity,compose(X1,empty_set)),
inference(scs_inference,[],[i_0_403,i_0_471,i_0_474,i_0_477,i_0_480,i_0_486,i_0_489,i_0_492,i_0_495,i_0_500,i_0_503,i_0_506,i_0_512,i_0_515,i_0_520,i_0_406,i_0_483,i_0_409,i_0_446,i_0_338,i_0_287,i_0_196,i_0_197,i_0_199,i_0_217,i_0_285,i_0_286,i_0_311,i_0_315,i_0_310,i_0_200,i_0_214,i_0_216,i_0_218,i_0_249,i_0_250,i_0_342,i_0_251,i_0_283]) ).
cnf(i_0_525,plain,
function(compose(X1,empty_set)),
inference(scs_inference,[],[i_0_403,i_0_471,i_0_474,i_0_477,i_0_480,i_0_486,i_0_489,i_0_492,i_0_495,i_0_500,i_0_503,i_0_506,i_0_512,i_0_515,i_0_520,i_0_406,i_0_483,i_0_409,i_0_418,i_0_446,i_0_338,i_0_287,i_0_196,i_0_197,i_0_199,i_0_217,i_0_285,i_0_286,i_0_311,i_0_315,i_0_310,i_0_200,i_0_214,i_0_216,i_0_218,i_0_249,i_0_250,i_0_342,i_0_251,i_0_283,i_0_319]) ).
cnf(i_0_527,plain,
empty_set != a,
inference(scs_inference,[],[i_0_320,i_0_394,i_0_403,i_0_471,i_0_474,i_0_477,i_0_480,i_0_486,i_0_489,i_0_492,i_0_495,i_0_500,i_0_503,i_0_506,i_0_512,i_0_515,i_0_520,i_0_406,i_0_483,i_0_409,i_0_418,i_0_446,i_0_338,i_0_287,i_0_196,i_0_197,i_0_199,i_0_217,i_0_285,i_0_286,i_0_311,i_0_315,i_0_310,i_0_200,i_0_214,i_0_216,i_0_218,i_0_249,i_0_250,i_0_342,i_0_251,i_0_283,i_0_319,i_0_374]) ).
cnf(i_0_529,plain,
~ subset(infinity,flip_range_of(empty_set)),
inference(scs_inference,[],[i_0_320,i_0_394,i_0_403,i_0_471,i_0_474,i_0_477,i_0_480,i_0_486,i_0_489,i_0_492,i_0_495,i_0_500,i_0_503,i_0_506,i_0_512,i_0_515,i_0_520,i_0_406,i_0_483,i_0_409,i_0_418,i_0_435,i_0_446,i_0_449,i_0_338,i_0_287,i_0_196,i_0_197,i_0_199,i_0_217,i_0_285,i_0_286,i_0_311,i_0_315,i_0_310,i_0_200,i_0_214,i_0_216,i_0_218,i_0_249,i_0_250,i_0_342,i_0_251,i_0_283,i_0_319,i_0_374,i_0_375]) ).
cnf(i_0_530,plain,
compose(empty_set,X1) = empty_set,
inference(scs_inference,[],[i_0_320,i_0_394,i_0_403,i_0_471,i_0_474,i_0_477,i_0_480,i_0_486,i_0_489,i_0_492,i_0_495,i_0_500,i_0_503,i_0_506,i_0_512,i_0_515,i_0_520,i_0_406,i_0_483,i_0_409,i_0_418,i_0_435,i_0_446,i_0_449,i_0_338,i_0_287,i_0_196,i_0_197,i_0_199,i_0_217,i_0_285,i_0_286,i_0_311,i_0_315,i_0_310,i_0_200,i_0_214,i_0_216,i_0_218,i_0_249,i_0_250,i_0_342,i_0_251,i_0_283,i_0_319,i_0_374,i_0_375,i_0_343]) ).
cnf(i_0_531,plain,
infinity != image(empty_set,X1),
inference(scs_inference,[],[i_0_320,i_0_394,i_0_403,i_0_471,i_0_474,i_0_477,i_0_480,i_0_486,i_0_489,i_0_492,i_0_495,i_0_500,i_0_503,i_0_506,i_0_512,i_0_515,i_0_520,i_0_406,i_0_483,i_0_409,i_0_509,i_0_418,i_0_435,i_0_446,i_0_449,i_0_338,i_0_287,i_0_196,i_0_197,i_0_199,i_0_217,i_0_285,i_0_286,i_0_311,i_0_315,i_0_310,i_0_200,i_0_214,i_0_216,i_0_218,i_0_249,i_0_250,i_0_342,i_0_251,i_0_283,i_0_319,i_0_374,i_0_375,i_0_343,i_0_370]) ).
cnf(i_0_533,plain,
~ proper_subset(rotate_right(empty_set),flip_range_of(empty_set)),
inference(scs_inference,[],[i_0_320,i_0_394,i_0_403,i_0_471,i_0_474,i_0_477,i_0_480,i_0_486,i_0_489,i_0_492,i_0_495,i_0_500,i_0_503,i_0_506,i_0_512,i_0_515,i_0_520,i_0_406,i_0_483,i_0_409,i_0_509,i_0_418,i_0_435,i_0_446,i_0_449,i_0_338,i_0_287,i_0_196,i_0_197,i_0_199,i_0_217,i_0_285,i_0_286,i_0_311,i_0_315,i_0_310,i_0_200,i_0_214,i_0_216,i_0_218,i_0_249,i_0_250,i_0_342,i_0_251,i_0_283,i_0_319,i_0_374,i_0_375,i_0_343,i_0_370,i_0_361]) ).
cnf(i_0_536,plain,
proper_subset(empty_set,a),
inference(scs_inference,[],[i_0_320,i_0_394,i_0_528,i_0_403,i_0_471,i_0_474,i_0_477,i_0_480,i_0_486,i_0_489,i_0_492,i_0_495,i_0_500,i_0_503,i_0_506,i_0_512,i_0_515,i_0_520,i_0_406,i_0_483,i_0_409,i_0_509,i_0_418,i_0_435,i_0_446,i_0_449,i_0_337,i_0_338,i_0_287,i_0_196,i_0_197,i_0_199,i_0_217,i_0_285,i_0_286,i_0_311,i_0_315,i_0_310,i_0_200,i_0_214,i_0_216,i_0_218,i_0_249,i_0_250,i_0_342,i_0_251,i_0_283,i_0_319,i_0_374,i_0_375,i_0_343,i_0_370,i_0_361,i_0_291,i_0_298]) ).
cnf(i_0_553,plain,
disjoint(cross_product(X1,empty_set),X2),
inference(scs_inference,[],[i_0_420,i_0_551,i_0_287,i_0_285]) ).
cnf(i_0_556,plain,
disjoint(X1,cross_product(X2,empty_set)),
inference(scs_inference,[],[i_0_420,i_0_551,i_0_554,i_0_287,i_0_285,i_0_286]) ).
cnf(i_0_559,plain,
cross_product(X1,empty_set) = empty_set,
inference(scs_inference,[],[i_0_420,i_0_551,i_0_554,i_0_557,i_0_287,i_0_285,i_0_286,i_0_315]) ).
cnf(i_0_562,plain,
~ member(X1,flip_range_of(cross_product(X2,empty_set))),
inference(scs_inference,[],[i_0_420,i_0_551,i_0_554,i_0_557,i_0_560,i_0_287,i_0_285,i_0_286,i_0_315,i_0_196]) ).
cnf(i_0_565,plain,
~ member(X1,rotate_right(cross_product(X2,empty_set))),
inference(scs_inference,[],[i_0_420,i_0_551,i_0_554,i_0_557,i_0_560,i_0_563,i_0_287,i_0_285,i_0_286,i_0_315,i_0_196,i_0_197]) ).
cnf(i_0_568,plain,
~ member(X1,compose(X2,cross_product(X3,empty_set))),
inference(scs_inference,[],[i_0_420,i_0_551,i_0_554,i_0_557,i_0_560,i_0_563,i_0_566,i_0_287,i_0_285,i_0_286,i_0_315,i_0_196,i_0_197,i_0_199]) ).
cnf(i_0_571,plain,
relation(cross_product(X1,empty_set)),
inference(scs_inference,[],[i_0_420,i_0_551,i_0_554,i_0_557,i_0_560,i_0_563,i_0_566,i_0_569,i_0_287,i_0_285,i_0_286,i_0_315,i_0_196,i_0_197,i_0_199,i_0_311]) ).
cnf(i_0_574,plain,
~ member(X1,compose(cross_product(X2,empty_set),X3)),
inference(scs_inference,[],[i_0_420,i_0_551,i_0_554,i_0_557,i_0_560,i_0_563,i_0_566,i_0_569,i_0_572,i_0_287,i_0_285,i_0_286,i_0_315,i_0_196,i_0_197,i_0_199,i_0_311,i_0_200]) ).
cnf(i_0_577,plain,
~ member(X1,image(cross_product(X2,empty_set),X3)),
inference(scs_inference,[],[i_0_420,i_0_551,i_0_554,i_0_557,i_0_560,i_0_563,i_0_566,i_0_569,i_0_572,i_0_575,i_0_287,i_0_285,i_0_286,i_0_315,i_0_196,i_0_197,i_0_199,i_0_311,i_0_200,i_0_214]) ).
cnf(i_0_580,plain,
~ member(X1,converse(cross_product(X2,empty_set))),
inference(scs_inference,[],[i_0_420,i_0_551,i_0_554,i_0_557,i_0_560,i_0_563,i_0_566,i_0_569,i_0_572,i_0_575,i_0_578,i_0_287,i_0_285,i_0_286,i_0_315,i_0_196,i_0_197,i_0_199,i_0_311,i_0_200,i_0_214,i_0_216]) ).
cnf(i_0_583,plain,
single_valued_set(cross_product(X1,empty_set)),
inference(scs_inference,[],[i_0_420,i_0_551,i_0_554,i_0_557,i_0_560,i_0_563,i_0_566,i_0_569,i_0_572,i_0_575,i_0_578,i_0_581,i_0_287,i_0_285,i_0_286,i_0_315,i_0_196,i_0_197,i_0_199,i_0_311,i_0_200,i_0_214,i_0_216,i_0_217]) ).
cnf(i_0_586,plain,
~ member(X1,cross_product(X2,cross_product(X3,empty_set))),
inference(scs_inference,[],[i_0_420,i_0_551,i_0_554,i_0_557,i_0_560,i_0_563,i_0_566,i_0_569,i_0_572,i_0_575,i_0_578,i_0_581,i_0_584,i_0_287,i_0_285,i_0_286,i_0_315,i_0_196,i_0_197,i_0_199,i_0_311,i_0_200,i_0_214,i_0_216,i_0_217,i_0_249]) ).
cnf(i_0_589,plain,
~ member(X1,cross_product(cross_product(X2,empty_set),X3)),
inference(scs_inference,[],[i_0_420,i_0_551,i_0_554,i_0_557,i_0_560,i_0_563,i_0_566,i_0_569,i_0_572,i_0_575,i_0_578,i_0_581,i_0_584,i_0_587,i_0_287,i_0_285,i_0_286,i_0_315,i_0_196,i_0_197,i_0_199,i_0_311,i_0_200,i_0_214,i_0_216,i_0_217,i_0_249,i_0_250]) ).
cnf(i_0_592,plain,
single_valued_set(cross_product(empty_set,X1)),
inference(scs_inference,[],[i_0_420,i_0_551,i_0_554,i_0_557,i_0_560,i_0_563,i_0_566,i_0_569,i_0_572,i_0_575,i_0_578,i_0_581,i_0_584,i_0_587,i_0_423,i_0_287,i_0_285,i_0_286,i_0_315,i_0_196,i_0_197,i_0_199,i_0_311,i_0_200,i_0_214,i_0_216,i_0_217,i_0_249,i_0_250,i_0_218]) ).
cnf(i_0_608,plain,
subset(compose(X1,empty_set),X2),
inference(rename_variables,[],[i_0_470]) ).
cnf(i_0_613,plain,
subset(compose(X1,empty_set),X2),
inference(rename_variables,[],[i_0_470]) ).
cnf(i_0_624,plain,
subset(compose(X1,empty_set),X2),
inference(rename_variables,[],[i_0_470]) ).
cnf(i_0_689,plain,
subset(compose(X1,empty_set),X2),
inference(rename_variables,[],[i_0_470]) ).
cnf(i_0_690,plain,
subset(cross_product(X1,empty_set),X2),
inference(rename_variables,[],[i_0_550]) ).
cnf(i_0_701,plain,
subset(cross_product(X1,empty_set),X2),
inference(rename_variables,[],[i_0_550]) ).
cnf(i_0_713,plain,
subset(cross_product(X1,empty_set),X2),
inference(rename_variables,[],[i_0_550]) ).
cnf(i_0_773,plain,
subset(cross_product(X1,empty_set),X2),
inference(rename_variables,[],[i_0_550]) ).
cnf(i_0_895,plain,
disjoint(compose(empty_set,X1),X2),
inference(scs_inference,[],[i_0_406,i_0_893,i_0_287,i_0_285]) ).
cnf(i_0_898,plain,
disjoint(X1,compose(empty_set,X2)),
inference(scs_inference,[],[i_0_406,i_0_893,i_0_896,i_0_287,i_0_285,i_0_286]) ).
cnf(i_0_901,plain,
image(empty_set,X1) = empty_set,
inference(scs_inference,[],[i_0_406,i_0_893,i_0_896,i_0_409,i_0_287,i_0_285,i_0_286,i_0_315]) ).
cnf(i_0_904,plain,
relation(image(empty_set,X1)),
inference(scs_inference,[],[i_0_406,i_0_893,i_0_896,i_0_409,i_0_902,i_0_287,i_0_285,i_0_286,i_0_315,i_0_311]) ).
cnf(i_0_1034,plain,
subset(compose(empty_set,X1),X2),
inference(rename_variables,[],[i_0_892]) ).
cnf(i_0_1040,plain,
subset(compose(empty_set,X1),X2),
inference(rename_variables,[],[i_0_892]) ).
cnf(i_0_1052,plain,
subset(compose(empty_set,X1),X2),
inference(rename_variables,[],[i_0_892]) ).
cnf(i_0_1062,plain,
disjoint(cross_product(empty_set,X1),X2),
inference(scs_inference,[],[i_0_423,i_0_1060,i_0_287,i_0_285]) ).
cnf(i_0_1065,plain,
disjoint(X1,cross_product(empty_set,X2)),
inference(scs_inference,[],[i_0_423,i_0_1060,i_0_1063,i_0_287,i_0_285,i_0_286]) ).
cnf(i_0_1108,plain,
subset(compose(empty_set,X1),X2),
inference(rename_variables,[],[i_0_892]) ).
cnf(i_0_1186,plain,
subset(cross_product(empty_set,X1),X2),
inference(rename_variables,[],[i_0_1059]) ).
cnf(i_0_1200,plain,
subset(cross_product(empty_set,X1),X2),
inference(rename_variables,[],[i_0_1059]) ).
cnf(i_0_1211,plain,
subset(cross_product(empty_set,X1),X2),
inference(rename_variables,[],[i_0_1059]) ).
cnf(i_0_1264,plain,
subset(cross_product(empty_set,X1),X2),
inference(rename_variables,[],[i_0_1059]) ).
cnf(i_0_546,plain,
relation(f25),
inference(equality_inference,[],[542]) ).
cnf(i_0_547,plain,
little_set(non_ordered_pair(X1,X2)),
inference(equality_inference,[],[543]) ).
cnf(i_0_548,plain,
single_valued_set(f25),
inference(equality_inference,[],[544]) ).
cnf(i_0_549,plain,
function(f25),
inference(equality_inference,[],[545]) ).
cnf(i_0_595,plain,
~ proper_subset(compose(empty_set,X1),compose(X2,empty_set)),
inference(scs_inference,[],[i_0_420,i_0_551,i_0_554,i_0_557,i_0_560,i_0_563,i_0_566,i_0_569,i_0_572,i_0_575,i_0_578,i_0_581,i_0_584,i_0_587,i_0_423,i_0_518,i_0_287,i_0_285,i_0_286,i_0_315,i_0_196,i_0_197,i_0_199,i_0_311,i_0_200,i_0_214,i_0_216,i_0_217,i_0_249,i_0_250,i_0_218,i_0_310]) ).
cnf(i_0_597,plain,
compose(X1,empty_set) = compose(empty_set,X2),
inference(scs_inference,[],[i_0_420,i_0_551,i_0_554,i_0_557,i_0_560,i_0_563,i_0_566,i_0_569,i_0_572,i_0_575,i_0_578,i_0_581,i_0_584,i_0_587,i_0_423,i_0_518,i_0_287,i_0_285,i_0_286,i_0_315,i_0_196,i_0_197,i_0_199,i_0_311,i_0_200,i_0_214,i_0_216,i_0_217,i_0_249,i_0_250,i_0_218,i_0_310,i_0_342]) ).
cnf(i_0_598,plain,
~ proper_subset(compose(X1,empty_set),flip_range_of(empty_set)),
inference(scs_inference,[],[i_0_456,i_0_420,i_0_551,i_0_554,i_0_557,i_0_560,i_0_563,i_0_566,i_0_569,i_0_572,i_0_575,i_0_578,i_0_581,i_0_584,i_0_587,i_0_423,i_0_518,i_0_494,i_0_287,i_0_285,i_0_286,i_0_315,i_0_196,i_0_197,i_0_199,i_0_311,i_0_200,i_0_214,i_0_216,i_0_217,i_0_249,i_0_250,i_0_218,i_0_310,i_0_342,i_0_360]) ).
cnf(i_0_599,plain,
cross_product(empty_set,X1) = cross_product(X2,empty_set),
inference(scs_inference,[],[i_0_456,i_0_420,i_0_551,i_0_554,i_0_557,i_0_560,i_0_563,i_0_566,i_0_569,i_0_572,i_0_575,i_0_578,i_0_581,i_0_584,i_0_587,i_0_590,i_0_423,i_0_593,i_0_518,i_0_494,i_0_287,i_0_285,i_0_286,i_0_315,i_0_196,i_0_197,i_0_199,i_0_311,i_0_200,i_0_214,i_0_216,i_0_217,i_0_249,i_0_250,i_0_218,i_0_310,i_0_342,i_0_360,i_0_251]) ).
cnf(i_0_603,plain,
~ subset(infinity,cross_product(X1,empty_set)),
inference(scs_inference,[],[i_0_456,i_0_420,i_0_551,i_0_554,i_0_557,i_0_560,i_0_563,i_0_566,i_0_569,i_0_572,i_0_575,i_0_578,i_0_581,i_0_584,i_0_587,i_0_590,i_0_601,i_0_423,i_0_593,i_0_518,i_0_494,i_0_338,i_0_287,i_0_285,i_0_286,i_0_315,i_0_196,i_0_197,i_0_199,i_0_311,i_0_200,i_0_214,i_0_216,i_0_217,i_0_249,i_0_250,i_0_218,i_0_310,i_0_342,i_0_360,i_0_251,i_0_283]) ).
cnf(i_0_606,plain,
empty_set = compose(X1,empty_set),
inference(scs_inference,[],[i_0_470,i_0_394,i_0_456,i_0_420,i_0_551,i_0_554,i_0_557,i_0_560,i_0_563,i_0_566,i_0_569,i_0_572,i_0_575,i_0_578,i_0_581,i_0_584,i_0_587,i_0_590,i_0_601,i_0_423,i_0_593,i_0_518,i_0_494,i_0_338,i_0_287,i_0_285,i_0_286,i_0_315,i_0_196,i_0_197,i_0_199,i_0_311,i_0_200,i_0_214,i_0_216,i_0_217,i_0_249,i_0_250,i_0_218,i_0_310,i_0_342,i_0_360,i_0_251,i_0_283,i_0_291]) ).
cnf(i_0_610,plain,
function(cross_product(X1,empty_set)),
inference(scs_inference,[],[i_0_470,i_0_394,i_0_456,i_0_420,i_0_551,i_0_554,i_0_557,i_0_560,i_0_563,i_0_566,i_0_569,i_0_572,i_0_575,i_0_578,i_0_581,i_0_584,i_0_587,i_0_590,i_0_601,i_0_423,i_0_593,i_0_518,i_0_494,i_0_338,i_0_287,i_0_285,i_0_286,i_0_315,i_0_196,i_0_197,i_0_199,i_0_311,i_0_200,i_0_214,i_0_216,i_0_217,i_0_249,i_0_250,i_0_218,i_0_310,i_0_342,i_0_360,i_0_251,i_0_283,i_0_291,i_0_319]) ).
cnf(i_0_612,plain,
compose(X1,empty_set) != a,
inference(scs_inference,[],[i_0_320,i_0_470,i_0_608,i_0_394,i_0_456,i_0_420,i_0_551,i_0_554,i_0_557,i_0_560,i_0_563,i_0_566,i_0_569,i_0_572,i_0_575,i_0_578,i_0_581,i_0_584,i_0_587,i_0_590,i_0_601,i_0_423,i_0_593,i_0_518,i_0_494,i_0_338,i_0_287,i_0_285,i_0_286,i_0_315,i_0_196,i_0_197,i_0_199,i_0_311,i_0_200,i_0_214,i_0_216,i_0_217,i_0_249,i_0_250,i_0_218,i_0_310,i_0_342,i_0_360,i_0_251,i_0_283,i_0_291,i_0_319,i_0_374]) ).
cnf(i_0_614,plain,
compose(X1,empty_set) = flip_range_of(empty_set),
inference(scs_inference,[],[i_0_320,i_0_470,i_0_608,i_0_394,i_0_456,i_0_420,i_0_551,i_0_554,i_0_557,i_0_560,i_0_563,i_0_566,i_0_569,i_0_572,i_0_575,i_0_578,i_0_581,i_0_584,i_0_587,i_0_590,i_0_601,i_0_423,i_0_593,i_0_518,i_0_437,i_0_494,i_0_338,i_0_287,i_0_285,i_0_286,i_0_315,i_0_196,i_0_197,i_0_199,i_0_311,i_0_200,i_0_214,i_0_216,i_0_217,i_0_249,i_0_250,i_0_218,i_0_310,i_0_342,i_0_360,i_0_251,i_0_283,i_0_291,i_0_319,i_0_374,i_0_343]) ).
cnf(i_0_615,plain,
~ subset(infinity,compose(empty_set,X1)),
inference(scs_inference,[],[i_0_320,i_0_470,i_0_608,i_0_394,i_0_456,i_0_420,i_0_551,i_0_554,i_0_557,i_0_560,i_0_563,i_0_566,i_0_569,i_0_572,i_0_575,i_0_578,i_0_581,i_0_584,i_0_587,i_0_590,i_0_601,i_0_423,i_0_593,i_0_518,i_0_437,i_0_494,i_0_522,i_0_338,i_0_287,i_0_285,i_0_286,i_0_315,i_0_196,i_0_197,i_0_199,i_0_311,i_0_200,i_0_214,i_0_216,i_0_217,i_0_249,i_0_250,i_0_218,i_0_310,i_0_342,i_0_360,i_0_251,i_0_283,i_0_291,i_0_319,i_0_374,i_0_343,i_0_375]) ).
cnf(i_0_616,plain,
~ subset(infinity,compose(X1,empty_set)),
inference(rename_variables,[],[i_0_522]) ).
cnf(i_0_617,plain,
infinity != image(compose(X1,empty_set),X2),
inference(scs_inference,[],[i_0_320,i_0_470,i_0_608,i_0_394,i_0_456,i_0_420,i_0_551,i_0_554,i_0_557,i_0_560,i_0_563,i_0_566,i_0_569,i_0_572,i_0_575,i_0_578,i_0_581,i_0_584,i_0_587,i_0_590,i_0_601,i_0_423,i_0_593,i_0_502,i_0_518,i_0_437,i_0_494,i_0_522,i_0_338,i_0_287,i_0_285,i_0_286,i_0_315,i_0_196,i_0_197,i_0_199,i_0_311,i_0_200,i_0_214,i_0_216,i_0_217,i_0_249,i_0_250,i_0_218,i_0_310,i_0_342,i_0_360,i_0_251,i_0_283,i_0_291,i_0_319,i_0_374,i_0_343,i_0_375,i_0_370]) ).
cnf(i_0_618,plain,
~ member(X1,image(compose(X2,empty_set),X3)),
inference(rename_variables,[],[i_0_502]) ).
cnf(i_0_619,plain,
~ proper_subset(flip_range_of(empty_set),compose(X1,empty_set)),
inference(scs_inference,[],[i_0_320,i_0_470,i_0_608,i_0_394,i_0_456,i_0_420,i_0_551,i_0_554,i_0_557,i_0_560,i_0_563,i_0_566,i_0_569,i_0_572,i_0_575,i_0_578,i_0_581,i_0_584,i_0_587,i_0_590,i_0_601,i_0_423,i_0_593,i_0_502,i_0_518,i_0_437,i_0_494,i_0_522,i_0_438,i_0_338,i_0_287,i_0_285,i_0_286,i_0_315,i_0_196,i_0_197,i_0_199,i_0_311,i_0_200,i_0_214,i_0_216,i_0_217,i_0_249,i_0_250,i_0_218,i_0_310,i_0_342,i_0_360,i_0_251,i_0_283,i_0_291,i_0_319,i_0_374,i_0_343,i_0_375,i_0_370,i_0_361]) ).
cnf(i_0_623,plain,
proper_subset(compose(X1,empty_set),a),
inference(scs_inference,[],[i_0_320,i_0_470,i_0_608,i_0_613,i_0_394,i_0_456,i_0_420,i_0_551,i_0_554,i_0_557,i_0_560,i_0_563,i_0_566,i_0_569,i_0_572,i_0_575,i_0_578,i_0_581,i_0_584,i_0_587,i_0_590,i_0_601,i_0_423,i_0_593,i_0_600,i_0_502,i_0_518,i_0_437,i_0_494,i_0_522,i_0_438,i_0_338,i_0_287,i_0_285,i_0_286,i_0_315,i_0_196,i_0_197,i_0_199,i_0_311,i_0_200,i_0_214,i_0_216,i_0_217,i_0_249,i_0_250,i_0_218,i_0_310,i_0_342,i_0_360,i_0_251,i_0_283,i_0_291,i_0_319,i_0_374,i_0_343,i_0_375,i_0_370,i_0_361,i_0_304,i_0_298]) ).
cnf(i_0_633,plain,
subset(compose(X1,compose(X2,empty_set)),X3),
inference(scs_inference,[],[i_0_479,i_0_287]) ).
cnf(i_0_634,plain,
~ member(X1,compose(X2,compose(X3,empty_set))),
inference(rename_variables,[],[i_0_479]) ).
cnf(i_0_637,plain,
~ member(X1,compose(X2,compose(X3,empty_set))),
inference(rename_variables,[],[i_0_479]) ).
cnf(i_0_640,plain,
~ member(X1,compose(X2,compose(X3,empty_set))),
inference(rename_variables,[],[i_0_479]) ).
cnf(i_0_643,plain,
~ member(X1,compose(X2,compose(X3,empty_set))),
inference(rename_variables,[],[i_0_479]) ).
cnf(i_0_646,plain,
~ member(X1,compose(X2,compose(X3,empty_set))),
inference(rename_variables,[],[i_0_479]) ).
cnf(i_0_649,plain,
~ member(X1,compose(X2,compose(X3,empty_set))),
inference(rename_variables,[],[i_0_479]) ).
cnf(i_0_652,plain,
~ member(X1,compose(X2,compose(X3,empty_set))),
inference(rename_variables,[],[i_0_479]) ).
cnf(i_0_655,plain,
~ member(X1,compose(X2,compose(X3,empty_set))),
inference(rename_variables,[],[i_0_479]) ).
cnf(i_0_658,plain,
~ member(X1,compose(X2,compose(X3,empty_set))),
inference(rename_variables,[],[i_0_479]) ).
cnf(i_0_663,plain,
~ member(X1,compose(X2,compose(X3,empty_set))),
inference(rename_variables,[],[i_0_479]) ).
cnf(i_0_666,plain,
~ member(X1,compose(X2,compose(X3,empty_set))),
inference(rename_variables,[],[i_0_479]) ).
cnf(i_0_669,plain,
~ member(X1,compose(X2,compose(X3,empty_set))),
inference(rename_variables,[],[i_0_479]) ).
cnf(i_0_672,plain,
~ member(X1,compose(X2,compose(X3,empty_set))),
inference(rename_variables,[],[i_0_479]) ).
cnf(i_0_675,plain,
~ member(X1,compose(X2,compose(X3,empty_set))),
inference(rename_variables,[],[i_0_479]) ).
cnf(i_0_678,plain,
~ member(X1,compose(compose(X2,empty_set),X3)),
inference(rename_variables,[],[i_0_499]) ).
cnf(i_0_682,plain,
~ member(X1,compose(compose(X2,empty_set),X3)),
inference(rename_variables,[],[i_0_499]) ).
cnf(i_0_683,plain,
~ member(X1,compose(X2,compose(X3,empty_set))),
inference(rename_variables,[],[i_0_479]) ).
cnf(i_0_686,plain,
~ member(X1,compose(X2,compose(X3,empty_set))),
inference(rename_variables,[],[i_0_479]) ).
cnf(i_0_694,plain,
single_valued_set(compose(empty_set,X1)),
inference(rename_variables,[],[i_0_482]) ).
cnf(i_0_697,plain,
relation(compose(X1,empty_set)),
inference(rename_variables,[],[i_0_491]) ).
cnf(i_0_699,plain,
function(compose(X1,empty_set)),
inference(rename_variables,[],[i_0_525]) ).
cnf(i_0_707,plain,
~ member(X1,flip_range_of(compose(X2,empty_set))),
inference(rename_variables,[],[i_0_473]) ).
cnf(i_0_710,plain,
~ member(X1,compose(compose(X2,empty_set),X3)),
inference(rename_variables,[],[i_0_499]) ).
cnf(i_0_715,plain,
~ member(X1,compose(X2,compose(X3,empty_set))),
inference(rename_variables,[],[i_0_479]) ).
cnf(i_0_717,plain,
subset(cross_product(X1,compose(X2,empty_set)),X3),
inference(scs_inference,[],[i_0_511,i_0_287]) ).
cnf(i_0_718,plain,
~ member(X1,cross_product(X2,compose(X3,empty_set))),
inference(rename_variables,[],[i_0_511]) ).
cnf(i_0_721,plain,
~ member(X1,cross_product(X2,compose(X3,empty_set))),
inference(rename_variables,[],[i_0_511]) ).
cnf(i_0_724,plain,
~ member(X1,cross_product(X2,compose(X3,empty_set))),
inference(rename_variables,[],[i_0_511]) ).
cnf(i_0_727,plain,
~ member(X1,cross_product(X2,compose(X3,empty_set))),
inference(rename_variables,[],[i_0_511]) ).
cnf(i_0_730,plain,
~ member(X1,cross_product(X2,compose(X3,empty_set))),
inference(rename_variables,[],[i_0_511]) ).
cnf(i_0_735,plain,
~ member(X1,cross_product(X2,compose(X3,empty_set))),
inference(rename_variables,[],[i_0_511]) ).
cnf(i_0_738,plain,
~ member(X1,cross_product(X2,compose(X3,empty_set))),
inference(rename_variables,[],[i_0_511]) ).
cnf(i_0_741,plain,
~ member(X1,cross_product(X2,compose(X3,empty_set))),
inference(rename_variables,[],[i_0_511]) ).
cnf(i_0_744,plain,
~ member(X1,cross_product(X2,compose(X3,empty_set))),
inference(rename_variables,[],[i_0_511]) ).
cnf(i_0_747,plain,
~ member(X1,cross_product(X2,compose(X3,empty_set))),
inference(rename_variables,[],[i_0_511]) ).
cnf(i_0_750,plain,
~ member(X1,cross_product(X2,compose(X3,empty_set))),
inference(rename_variables,[],[i_0_511]) ).
cnf(i_0_753,plain,
~ member(X1,cross_product(X2,compose(X3,empty_set))),
inference(rename_variables,[],[i_0_511]) ).
cnf(i_0_756,plain,
~ member(X1,cross_product(X2,compose(X3,empty_set))),
inference(rename_variables,[],[i_0_511]) ).
cnf(i_0_759,plain,
~ member(X1,cross_product(X2,compose(X3,empty_set))),
inference(rename_variables,[],[i_0_511]) ).
cnf(i_0_762,plain,
~ member(X1,cross_product(compose(X2,empty_set),X3)),
inference(rename_variables,[],[i_0_514]) ).
cnf(i_0_766,plain,
~ member(X1,cross_product(compose(X2,empty_set),X3)),
inference(rename_variables,[],[i_0_514]) ).
cnf(i_0_767,plain,
~ member(X1,cross_product(X2,compose(X3,empty_set))),
inference(rename_variables,[],[i_0_511]) ).
cnf(i_0_770,plain,
~ member(X1,cross_product(X2,compose(X3,empty_set))),
inference(rename_variables,[],[i_0_511]) ).
cnf(i_0_777,plain,
single_valued_set(cross_product(empty_set,X1)),
inference(rename_variables,[],[i_0_592]) ).
cnf(i_0_781,plain,
relation(cross_product(X1,empty_set)),
inference(rename_variables,[],[i_0_571]) ).
cnf(i_0_783,plain,
function(compose(X1,empty_set)),
inference(rename_variables,[],[i_0_525]) ).
cnf(i_0_795,plain,
~ member(X1,rotate_right(compose(X2,empty_set))),
inference(rename_variables,[],[i_0_476]) ).
cnf(i_0_797,plain,
~ member(X1,cross_product(compose(X2,empty_set),X3)),
inference(rename_variables,[],[i_0_514]) ).
cnf(i_0_802,plain,
~ member(X1,cross_product(X2,compose(X3,empty_set))),
inference(rename_variables,[],[i_0_511]) ).
cnf(i_0_804,plain,
subset(converse(compose(X1,empty_set)),X2),
inference(scs_inference,[],[i_0_505,i_0_287]) ).
cnf(i_0_805,plain,
~ member(X1,converse(compose(X2,empty_set))),
inference(rename_variables,[],[i_0_505]) ).
cnf(i_0_808,plain,
~ member(X1,converse(compose(X2,empty_set))),
inference(rename_variables,[],[i_0_505]) ).
cnf(i_0_811,plain,
~ member(X1,converse(compose(X2,empty_set))),
inference(rename_variables,[],[i_0_505]) ).
cnf(i_0_814,plain,
~ member(X1,converse(compose(X2,empty_set))),
inference(rename_variables,[],[i_0_505]) ).
cnf(i_0_817,plain,
~ member(X1,converse(compose(X2,empty_set))),
inference(rename_variables,[],[i_0_505]) ).
cnf(i_0_822,plain,
~ member(X1,converse(compose(X2,empty_set))),
inference(rename_variables,[],[i_0_505]) ).
cnf(i_0_825,plain,
~ member(X1,converse(compose(X2,empty_set))),
inference(rename_variables,[],[i_0_505]) ).
cnf(i_0_828,plain,
~ member(X1,converse(compose(X2,empty_set))),
inference(rename_variables,[],[i_0_505]) ).
cnf(i_0_831,plain,
~ member(X1,converse(compose(X2,empty_set))),
inference(rename_variables,[],[i_0_505]) ).
cnf(i_0_834,plain,
~ member(X1,converse(compose(X2,empty_set))),
inference(rename_variables,[],[i_0_505]) ).
cnf(i_0_837,plain,
~ member(X1,converse(compose(X2,empty_set))),
inference(rename_variables,[],[i_0_505]) ).
cnf(i_0_840,plain,
~ member(X1,converse(compose(X2,empty_set))),
inference(rename_variables,[],[i_0_505]) ).
cnf(i_0_843,plain,
~ member(X1,converse(compose(X2,empty_set))),
inference(rename_variables,[],[i_0_505]) ).
cnf(i_0_846,plain,
~ member(X1,converse(compose(X2,empty_set))),
inference(rename_variables,[],[i_0_505]) ).
cnf(i_0_854,plain,
~ member(X1,converse(compose(X2,empty_set))),
inference(rename_variables,[],[i_0_505]) ).
cnf(i_0_857,plain,
~ member(X1,converse(compose(X2,empty_set))),
inference(rename_variables,[],[i_0_505]) ).
cnf(i_0_890,plain,
~ member(X1,converse(compose(X2,empty_set))),
inference(rename_variables,[],[i_0_505]) ).
cnf(i_0_934,plain,
~ member(X1,rotate_right(compose(X2,empty_set))),
inference(rename_variables,[],[i_0_476]) ).
cnf(i_0_964,plain,
~ member(X1,image(cross_product(X2,empty_set),X3)),
inference(rename_variables,[],[i_0_577]) ).
cnf(i_0_966,plain,
~ member(X1,rotate_right(compose(X2,empty_set))),
inference(rename_variables,[],[i_0_476]) ).
cnf(i_0_978,plain,
subset(cross_product(compose(X1,empty_set),X2),X3),
inference(scs_inference,[],[i_0_514,i_0_287]) ).
cnf(i_0_979,plain,
~ member(X1,cross_product(compose(X2,empty_set),X3)),
inference(rename_variables,[],[i_0_514]) ).
cnf(i_0_982,plain,
~ member(X1,cross_product(compose(X2,empty_set),X3)),
inference(rename_variables,[],[i_0_514]) ).
cnf(i_0_985,plain,
~ member(X1,cross_product(compose(X2,empty_set),X3)),
inference(rename_variables,[],[i_0_514]) ).
cnf(i_0_988,plain,
~ member(X1,cross_product(compose(X2,empty_set),X3)),
inference(rename_variables,[],[i_0_514]) ).
cnf(i_0_996,plain,
~ member(X1,cross_product(compose(X2,empty_set),X3)),
inference(rename_variables,[],[i_0_514]) ).
cnf(i_0_999,plain,
~ member(X1,cross_product(compose(X2,empty_set),X3)),
inference(rename_variables,[],[i_0_514]) ).
cnf(i_0_1002,plain,
~ member(X1,cross_product(compose(X2,empty_set),X3)),
inference(rename_variables,[],[i_0_514]) ).
cnf(i_0_1005,plain,
~ member(X1,cross_product(compose(X2,empty_set),X3)),
inference(rename_variables,[],[i_0_514]) ).
cnf(i_0_1008,plain,
~ member(X1,cross_product(compose(X2,empty_set),X3)),
inference(rename_variables,[],[i_0_514]) ).
cnf(i_0_1011,plain,
~ member(X1,cross_product(compose(X2,empty_set),X3)),
inference(rename_variables,[],[i_0_514]) ).
cnf(i_0_1014,plain,
~ member(X1,cross_product(compose(X2,empty_set),X3)),
inference(rename_variables,[],[i_0_514]) ).
cnf(i_0_1017,plain,
~ member(X1,cross_product(compose(X2,empty_set),X3)),
inference(rename_variables,[],[i_0_514]) ).
cnf(i_0_1020,plain,
~ member(X1,compose(X2,cross_product(X3,empty_set))),
inference(rename_variables,[],[i_0_568]) ).
cnf(i_0_1023,plain,
~ member(X1,compose(cross_product(X2,empty_set),X3)),
inference(rename_variables,[],[i_0_574]) ).
cnf(i_0_1030,plain,
~ member(X1,cross_product(X2,compose(X3,empty_set))),
inference(rename_variables,[],[i_0_511]) ).
cnf(i_0_1045,plain,
~ subset(infinity,compose(X1,empty_set)),
inference(rename_variables,[],[i_0_522]) ).
cnf(i_0_1047,plain,
~ member(X1,flip_range_of(cross_product(X2,empty_set))),
inference(rename_variables,[],[i_0_562]) ).
cnf(i_0_1049,plain,
~ member(X1,compose(X2,cross_product(X3,empty_set))),
inference(rename_variables,[],[i_0_568]) ).
cnf(i_0_1055,plain,
~ member(X1,cross_product(X2,compose(X3,empty_set))),
inference(rename_variables,[],[i_0_511]) ).
cnf(i_0_1068,plain,
~ proper_subset(image(empty_set,X1),empty_set),
inference(scs_inference,[],[i_0_423,i_0_1060,i_0_1063,i_0_901,i_0_287,i_0_285,i_0_286,i_0_310]) ).
cnf(i_0_1070,plain,
cross_product(empty_set,X1) = empty_set,
inference(scs_inference,[],[i_0_423,i_0_1060,i_0_1063,i_0_1066,i_0_901,i_0_287,i_0_285,i_0_286,i_0_310,i_0_315]) ).
cnf(i_0_1073,plain,
~ member(X1,flip_range_of(cross_product(empty_set,X2))),
inference(scs_inference,[],[i_0_423,i_0_1060,i_0_1063,i_0_1066,i_0_1071,i_0_901,i_0_287,i_0_285,i_0_286,i_0_310,i_0_315,i_0_196]) ).
cnf(i_0_1076,plain,
~ member(X1,rotate_right(cross_product(empty_set,X2))),
inference(scs_inference,[],[i_0_423,i_0_1060,i_0_1063,i_0_1066,i_0_1071,i_0_1074,i_0_901,i_0_287,i_0_285,i_0_286,i_0_310,i_0_315,i_0_196,i_0_197]) ).
cnf(i_0_1079,plain,
~ member(X1,compose(X2,cross_product(empty_set,X3))),
inference(scs_inference,[],[i_0_423,i_0_1060,i_0_1063,i_0_1066,i_0_1071,i_0_1074,i_0_1077,i_0_901,i_0_287,i_0_285,i_0_286,i_0_310,i_0_315,i_0_196,i_0_197,i_0_199]) ).
cnf(i_0_1082,plain,
~ member(X1,compose(cross_product(empty_set,X2),X3)),
inference(scs_inference,[],[i_0_423,i_0_1060,i_0_1063,i_0_1066,i_0_1071,i_0_1074,i_0_1077,i_0_1080,i_0_901,i_0_287,i_0_285,i_0_286,i_0_310,i_0_315,i_0_196,i_0_197,i_0_199,i_0_200]) ).
cnf(i_0_1085,plain,
~ member(X1,image(cross_product(empty_set,X2),X3)),
inference(scs_inference,[],[i_0_423,i_0_1060,i_0_1063,i_0_1066,i_0_1071,i_0_1074,i_0_1077,i_0_1080,i_0_1083,i_0_901,i_0_287,i_0_285,i_0_286,i_0_310,i_0_315,i_0_196,i_0_197,i_0_199,i_0_200,i_0_214]) ).
cnf(i_0_1088,plain,
~ member(X1,converse(cross_product(empty_set,X2))),
inference(scs_inference,[],[i_0_423,i_0_1060,i_0_1063,i_0_1066,i_0_1071,i_0_1074,i_0_1077,i_0_1080,i_0_1083,i_0_1086,i_0_901,i_0_287,i_0_285,i_0_286,i_0_310,i_0_315,i_0_196,i_0_197,i_0_199,i_0_200,i_0_214,i_0_216]) ).
cnf(i_0_1091,plain,
~ member(X1,cross_product(X2,cross_product(empty_set,X3))),
inference(scs_inference,[],[i_0_423,i_0_1060,i_0_1063,i_0_1066,i_0_1071,i_0_1074,i_0_1077,i_0_1080,i_0_1083,i_0_1086,i_0_1089,i_0_901,i_0_287,i_0_285,i_0_286,i_0_310,i_0_315,i_0_196,i_0_197,i_0_199,i_0_200,i_0_214,i_0_216,i_0_249]) ).
cnf(i_0_1094,plain,
~ member(X1,cross_product(cross_product(empty_set,X2),X3)),
inference(scs_inference,[],[i_0_423,i_0_1060,i_0_1063,i_0_1066,i_0_1071,i_0_1074,i_0_1077,i_0_1080,i_0_1083,i_0_1086,i_0_1089,i_0_1092,i_0_901,i_0_287,i_0_285,i_0_286,i_0_310,i_0_315,i_0_196,i_0_197,i_0_199,i_0_200,i_0_214,i_0_216,i_0_249,i_0_250]) ).
cnf(i_0_1097,plain,
relation(cross_product(X1,cross_product(X2,empty_set))),
inference(scs_inference,[],[i_0_423,i_0_1060,i_0_1063,i_0_1066,i_0_1071,i_0_1074,i_0_1077,i_0_1080,i_0_1083,i_0_1086,i_0_1089,i_0_1092,i_0_586,i_0_901,i_0_287,i_0_285,i_0_286,i_0_310,i_0_315,i_0_196,i_0_197,i_0_199,i_0_200,i_0_214,i_0_216,i_0_249,i_0_250,i_0_311]) ).
cnf(i_0_1098,plain,
~ member(X1,cross_product(X2,cross_product(X3,empty_set))),
inference(rename_variables,[],[i_0_586]) ).
cnf(i_0_1101,plain,
~ member(X1,cross_product(X2,cross_product(X3,empty_set))),
inference(rename_variables,[],[i_0_586]) ).
cnf(i_0_1104,plain,
~ member(X1,cross_product(cross_product(X2,empty_set),X3)),
inference(rename_variables,[],[i_0_589]) ).
cnf(i_0_1113,plain,
~ member(X1,converse(compose(X2,empty_set))),
inference(rename_variables,[],[i_0_505]) ).
cnf(i_0_1116,plain,
single_valued_set(cross_product(empty_set,X1)),
inference(rename_variables,[],[i_0_592]) ).
cnf(i_0_1127,plain,
~ member(X1,rotate_right(cross_product(X2,empty_set))),
inference(rename_variables,[],[i_0_565]) ).
cnf(i_0_1129,plain,
~ member(X1,cross_product(X2,cross_product(X3,empty_set))),
inference(rename_variables,[],[i_0_586]) ).
cnf(i_0_1134,plain,
~ member(X1,converse(compose(X2,empty_set))),
inference(rename_variables,[],[i_0_505]) ).
cnf(i_0_1148,plain,
~ member(X1,converse(cross_product(X2,empty_set))),
inference(rename_variables,[],[i_0_580]) ).
cnf(i_0_1175,plain,
~ member(X1,converse(cross_product(X2,empty_set))),
inference(rename_variables,[],[i_0_580]) ).
cnf(i_0_1178,plain,
~ member(X1,converse(cross_product(X2,empty_set))),
inference(rename_variables,[],[i_0_580]) ).
cnf(c_0_344,axiom,
( member(X1,X2)
| ~ subset(X3,X2)
| ~ member(X1,X3) ),
i_0_283 ).
cnf(c_0_345,hypothesis,
subset(b,c),
i_0_336 ).
cnf(c_0_346,axiom,
( subset(X1,X2)
| ~ member(f17(X1,X2),X2) ),
i_0_252 ).
cnf(c_0_347,hypothesis,
( member(X1,c)
| ~ member(X1,b) ),
inference(spm,[status(thm)],[c_0_344,c_0_345]) ).
cnf(c_0_348,hypothesis,
subset(a,b),
i_0_337 ).
cnf(c_0_349,hypothesis,
( subset(X1,c)
| ~ member(f17(X1,c),b) ),
inference(spm,[status(thm)],[c_0_346,c_0_347]) ).
cnf(c_0_350,hypothesis,
( member(X1,b)
| ~ member(X1,a) ),
inference(spm,[status(thm)],[c_0_344,c_0_348]) ).
cnf(c_0_351,hypothesis,
( subset(X1,c)
| ~ member(f17(X1,c),a) ),
inference(spm,[status(thm)],[c_0_349,c_0_350]) ).
cnf(c_0_352,axiom,
( subset(X1,X2)
| member(f17(X1,X2),X1) ),
i_0_287 ).
cnf(c_0_353,negated_conjecture,
~ subset(a,c),
i_0_320 ).
cnf(c_0_354,hypothesis,
$false,
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_351,c_0_352]),c_0_353]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SET027-3 : TPTP v9.2.1. Released v1.0.0.
% 0.00/0.12 % Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.16/0.33 % Computer : n018.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % WCLimit : 300
% 0.16/0.33 % DateTime : Tue May 5 02:04:47 EDT 2026
% 0.16/0.33 % CPUTime :
% 0.16/0.34 % start to proof: theBenchmark
% 231.86/184.03 % Version : CSE_E---1.7
% 231.86/184.03 % Problem : theBenchmark.p
% 231.86/184.03 % SZS status Unsatisfiable for theBenchmark.p
% 231.86/184.03 % SZS output start CNFRefutation
% See solution above
% 245.34/197.52 % Total time : 183.682s
%------------------------------------------------------------------------------