%------------------------------------------------------------------------------
% File     : ALG001-1 : TPTP v3.2.0. Released v1.0.0.
% Domain   : General Algebra
% Problem  : The composition of homomorphisms is a homomorphism
% Version  : [BL+86] axioms : Augmented.
% English  : 

% Refs     : [BL+86] Boyer et al. (1986), Set Theory in First-Order Logic: 
% Source   : [BL+86]
% Names    : Problem 221-223 [BL+86]

% Status   : Unsatisfiable
% Rating   : 1.00 v2.0.0
% Syntax   : Number of clauses    :  172 (  20 non-Horn;  20 unit; 139 RR)
%            Number of literals   :  431 (  61 equality)
%            Maximal clause size  :    8 (   2 average)
%            Number of predicates :   14 (   0 propositional; 1-5 arity)
%            Number of functors   :   67 (  14 constant; 0-5 arity)
%            Number of variables  :  389 (  36 singleton)
%            Maximal term depth   :    4 (   1 average)

% Comments : Augmented with previous lemmas.
%          : tptp2X -f otter:none:[set(auto),clear(print_given)] -t stdfof+add_equality:r ALG001-1.p 
%------------------------------------------------------------------------------
set(prolog_style_variables).
set(tptp_eq).
set(auto).
clear(print_given).

list(usable).

% reflexivity, axiom.
 equal(A, A).

% a2, axiom.
-member(X, Y) |
 little_set(X).

% extensionality1, axiom.
 little_set(f1(X, Y)) |
 equal(X, Y).

% extensionality2, axiom.
 member(f1(X, Y), X) |
 member(f1(X, Y), Y) |
 equal(X, Y).

% extensionality3, axiom.
-member(f1(X, Y), X) |
-member(f1(X, Y), Y) |
 equal(X, Y).

% non_ordered_pair1, axiom.
-member(U, non_ordered_pair(X, Y)) |
 equal(U, X) |
 equal(U, Y).

% non_ordered_pair2, axiom.
 member(U, non_ordered_pair(X, Y)) |
-little_set(U) |
-equal(U, X).

% non_ordered_pair3, axiom.
 member(U, non_ordered_pair(X, Y)) |
-little_set(U) |
-equal(U, Y).

% non_ordered_pair4, axiom.
 little_set(non_ordered_pair(X, Y)).

% singleton_set, axiom.
 equal(singleton_set(X), non_ordered_pair(X, X)).

% ordered_pair, axiom.
 equal(ordered_pair(X, Y), non_ordered_pair(singleton_set(X), non_ordered_pair(X, Y))).

% ordered_pair_predicate1, axiom.
-ordered_pair_predicate(X) |
 little_set(f2(X)).

% ordered_pair_predicate2, axiom.
-ordered_pair_predicate(X) |
 little_set(f3(X)).

% ordered_pair_predicate3, axiom.
-ordered_pair_predicate(X) |
 equal(X, ordered_pair(f2(X), f3(X))).

% ordered_pair_predicate4, axiom.
 ordered_pair_predicate(X) |
-little_set(Y) |
-little_set(Z) |
-equal(X, ordered_pair(Y, Z)).

% first1, axiom.
-member(Z, first(X)) |
 little_set(f4(Z, X)).

% first2, axiom.
-member(Z, first(X)) |
 little_set(f5(Z, X)).

% first3, axiom.
-member(Z, first(X)) |
 equal(X, ordered_pair(f4(Z, X), f5(Z, X))).

% first4, axiom.
-member(Z, first(X)) |
 member(Z, f4(Z, X)).

% first5, axiom.
 member(Z, first(X)) |
-little_set(U) |
-little_set(V) |
-equal(X, ordered_pair(U, V)) |
-member(Z, U).

% second1, axiom.
-member(Z, second(X)) |
 little_set(f6(Z, X)).

% second2, axiom.
-member(Z, second(X)) |
 little_set(f7(Z, X)).

% second3, axiom.
-member(Z, second(X)) |
 equal(X, ordered_pair(f6(Z, X), f7(Z, X))).

% second4, axiom.
-member(Z, second(X)) |
 member(Z, f7(Z, X)).

% second5, axiom.
 member(Z, second(X)) |
-little_set(U) |
-little_set(V) |
-equal(X, ordered_pair(U, V)) |
-member(Z, V).

% element_relation1, axiom.
-member(Z, estin) |
 ordered_pair_predicate(Z).

% element_relation2, axiom.
-member(Z, estin) |
 member(first(Z), second(Z)).

% element_relation3, axiom.
 member(Z, estin) |
-little_set(Z) |
-ordered_pair_predicate(Z) |
-member(first(Z), second(Z)).

% intersection1, axiom.
-member(Z, intersection(X, Y)) |
 member(Z, X).

% intersection2, axiom.
-member(Z, intersection(X, Y)) |
 member(Z, Y).

% intersection3, axiom.
 member(Z, intersection(X, Y)) |
-member(Z, X) |
-member(Z, Y).

% complement1, axiom.
-member(Z, complement(X)) |
-member(Z, X).

% complement2, axiom.
 member(Z, complement(X)) |
-little_set(Z) |
 member(Z, X).

% union, axiom.
 equal(union(X, Y), complement(intersection(complement(X), complement(Y)))).

% domain1, axiom.
-member(Z, domain_of(X)) |
 ordered_pair_predicate(f8(Z, X)).

% domain2, axiom.
-member(Z, domain_of(X)) |
 member(f8(Z, X), X).

% domain3, axiom.
-member(Z, domain_of(X)) |
 equal(Z, first(f8(Z, X))).

% domain4, axiom.
 member(Z, domain_of(X)) |
-little_set(Z) |
-ordered_pair_predicate(Xp) |
-member(Xp, X) |
-equal(Z, first(Xp)).

% cross_product1, axiom.
-member(Z, cross_product(X, Y)) |
 ordered_pair_predicate(Z).

% cross_product2, axiom.
-member(Z, cross_product(X, Y)) |
 member(first(Z), X).

% cross_product3, axiom.
-member(Z, cross_product(X, Y)) |
 member(second(Z), Y).

% cross_product4, axiom.
 member(Z, cross_product(X, Y)) |
-little_set(Z) |
-ordered_pair_predicate(Z) |
-member(first(Z), X) |
-member(second(Z), Y).

% converse1, axiom.
-member(Z, converse(X)) |
 ordered_pair_predicate(Z).

% converse2, axiom.
-member(Z, converse(X)) |
 member(ordered_pair(second(Z), first(Z)), X).

% converse3, axiom.
 member(Z, converse(X)) |
-little_set(Z) |
-ordered_pair_predicate(Z) |
-member(ordered_pair(second(Z), first(Z)), X).

% rotate_right1, axiom.
-member(Z, rotate_right(X)) |
 little_set(f9(Z, X)).

% rotate_right2, axiom.
-member(Z, rotate_right(X)) |
 little_set(f10(Z, X)).

% rotate_right3, axiom.
-member(Z, rotate_right(X)) |
 little_set(f11(Z, X)).

% rotate_right4, axiom.
-member(Z, rotate_right(X)) |
 equal(Z, ordered_pair(f9(Z, X), ordered_pair(f10(Z, X), f11(Z, X)))).

% rotate_right5, axiom.
-member(Z, rotate_right(X)) |
 member(ordered_pair(f10(Z, X), ordered_pair(f11(Z, X), f9(Z, X))), X).

% rotate_right6, axiom.
 member(Z, rotate_right(X)) |
-little_set(Z) |
-little_set(U) |
-little_set(V) |
-little_set(W) |
-equal(Z, ordered_pair(U, ordered_pair(V, W))) |
-member(ordered_pair(V, ordered_pair(W, U)), X).

% flip_range1, axiom.
-member(Z, flip_range_of(X)) |
 little_set(f12(Z, X)).

% flip_range2, axiom.
-member(Z, flip_range_of(X)) |
 little_set(f13(Z, X)).

% flip_range3, axiom.
-member(Z, flip_range_of(X)) |
 little_set(f14(Z, X)).

% flip_range4, axiom.
-member(Z, flip_range_of(X)) |
 equal(Z, ordered_pair(f12(Z, X), ordered_pair(f13(Z, X), f14(Z, X)))).

% flip_range5, axiom.
-member(Z, flip_range_of(X)) |
 member(ordered_pair(f12(Z, X), ordered_pair(f14(Z, X), f13(Z, X))), X).

% flip_range6, axiom.
 member(Z, flip_range_of(X)) |
-little_set(Z) |
-little_set(U) |
-little_set(V) |
-little_set(W) |
-equal(Z, ordered_pair(U, ordered_pair(V, W))) |
-member(ordered_pair(U, ordered_pair(W, V)), X).

% successor, axiom.
 equal(successor(X), union(X, singleton_set(X))).

% empty_set, axiom.
-member(Z, empty_set).

% universal_set, axiom.
 member(Z, universal_set) |
-little_set(Z).

% infinity1, axiom.
 little_set(infinity).

% infinity2, axiom.
 member(empty_set, infinity).

% infinity3, axiom.
-member(X, infinity) |
 member(successor(X), infinity).

% sigma1, axiom.
-member(Z, sigma(X)) |
 member(f16(Z, X), X).

% sigma2, axiom.
-member(Z, sigma(X)) |
 member(Z, f16(Z, X)).

% sigma3, axiom.
 member(Z, sigma(X)) |
-member(Y, X) |
-member(Z, Y).

% sigma4, axiom.
-little_set(U) |
 little_set(sigma(U)).

% subset1, axiom.
-subset(X, Y) |
-member(U, X) |
 member(U, Y).

% subset2, axiom.
 subset(X, Y) |
 member(f17(X, Y), X).

% subset3, axiom.
 subset(X, Y) |
-member(f17(X, Y), Y).

% proper_subset1, axiom.
-proper_subset(X, Y) |
 subset(X, Y).

% proper_subset2, axiom.
-proper_subset(X, Y) |
-equal(X, Y).

% proper_subset3, axiom.
 proper_subset(X, Y) |
-subset(X, Y) |
 equal(X, Y).

% powerset1, axiom.
-member(Z, powerset(X)) |
 subset(Z, X).

% powerset2, axiom.
 member(Z, powerset(X)) |
-little_set(Z) |
-subset(Z, X).

% powerset3, axiom.
-little_set(U) |
 little_set(powerset(U)).

% relation1, axiom.
-relation(Z) |
-member(X, Z) |
 ordered_pair_predicate(X).

% relation2, axiom.
 relation(Z) |
 member(f18(Z), Z).

% relation3, axiom.
 relation(Z) |
-ordered_pair_predicate(f18(Z)).

% single_valued_set1, axiom.
-single_valued_set(X) |
-little_set(U) |
-little_set(V) |
-little_set(W) |
-member(ordered_pair(U, V), X) |
-member(ordered_pair(U, W), X) |
 equal(V, W).

% single_valued_set2, axiom.
 single_valued_set(X) |
 little_set(f19(X)).

% single_valued_set3, axiom.
 single_valued_set(X) |
 little_set(f20(X)).

% single_valued_set4, axiom.
 single_valued_set(X) |
 little_set(f21(X)).

% single_valued_set5, axiom.
 single_valued_set(X) |
 member(ordered_pair(f19(X), f20(X)), X).

% single_valued_set6, axiom.
 single_valued_set(X) |
 member(ordered_pair(f19(X), f21(X)), X).

% single_valued_set7, axiom.
 single_valued_set(X) |
-equal(f20(X), f21(X)).

% function1, axiom.
-function(Xf) |
 relation(Xf).

% function2, axiom.
-function(Xf) |
 single_valued_set(Xf).

% function3, axiom.
 function(Xf) |
-relation(Xf) |
-single_valued_set(Xf).

% image_and_substitution1, axiom.
-member(Z, image(X, Xf)) |
 ordered_pair_predicate(f22(Z, X, Xf)).

% image_and_substitution2, axiom.
-member(Z, image(X, Xf)) |
 member(f22(Z, X, Xf), Xf).

% image_and_substitution3, axiom.
-member(Z, image(X, Xf)) |
 member(first(f22(Z, X, Xf)), X).

% image_and_substitution4, axiom.
-member(Z, image(X, Xf)) |
 equal(second(f22(Z, X, Xf)), Z).

% image_and_substitution5, axiom.
 member(Z, image(X, Xf)) |
-little_set(Z) |
-ordered_pair_predicate(Y) |
-member(Y, Xf) |
-member(first(Y), X) |
-equal(second(Y), Z).

% image_and_substitution6, axiom.
-little_set(X) |
-function(Xf) |
 little_set(image(X, Xf)).

% disjoint1, axiom.
-disjoint(X, Y) |
-member(U, X) |
-member(U, Y).

% disjoint2, axiom.
 disjoint(X, Y) |
 member(f23(X, Y), X).

% disjoint3, axiom.
 disjoint(X, Y) |
 member(f23(X, Y), Y).

% regularity1, axiom.
 equal(X, empty_set) |
 member(f24(X), X).

% regularity2, axiom.
 equal(X, empty_set) |
 disjoint(f24(X), X).

% choice1, axiom.
 function(f25).

% choice2, axiom.
-little_set(X) |
 equal(X, empty_set) |
 member(f26(X), X).

% choice3, axiom.
-little_set(X) |
 equal(X, empty_set) |
 member(ordered_pair(X, f26(X)), f25).

% range_of1, axiom.
-member(Z, range_of(X)) |
 ordered_pair_predicate(f27(Z, X)).

% range_of2, axiom.
-member(Z, range_of(X)) |
 member(f27(Z, X), X).

% range_of3, axiom.
-member(Z, range_of(X)) |
 equal(Z, second(f27(Z, X))).

% range_of4, axiom.
 member(Z, range_of(X)) |
-little_set(Z) |
-ordered_pair_predicate(Xp) |
-member(Xp, X) |
-equal(Z, second(Xp)).

% identity_relation1, axiom.
-member(Z, identity_relation) |
 ordered_pair_predicate(Z).

% identity_relation2, axiom.
-member(Z, identity_relation) |
 equal(first(Z), second(Z)).

% identity_relation3, axiom.
 member(Z, identity_relation) |
-little_set(Z) |
-ordered_pair_predicate(Z) |
-equal(first(Z), second(Z)).

% restrict, axiom.
 equal(restrict(X, Y), intersection(X, cross_product(Y, universal_set))).

% one_to_one_function1, axiom.
-one_to_one_function(Xf) |
 function(Xf).

% one_to_one_function2, axiom.
-one_to_one_function(Xf) |
 function(converse(Xf)).

% one_to_one_function3, axiom.
 one_to_one_function(Xf) |
-function(Xf) |
-function(converse(Xf)).

% apply1, axiom.
-member(Z, apply(Xf, Y)) |
 ordered_pair_predicate(f28(Z, Xf, Y)).

% apply2, axiom.
-member(Z, apply(Xf, Y)) |
 member(f28(Z, Xf, Y), Xf).

% apply3, axiom.
-member(Z, apply(Xf, Y)) |
 equal(first(f28(Z, Xf, Y)), Y).

% apply4, axiom.
-member(Z, apply(Xf, Y)) |
 member(Z, second(f28(Z, Xf, Y))).

% apply5, axiom.
 member(Z, apply(Xf, Y)) |
-ordered_pair_predicate(W) |
-member(W, Xf) |
-equal(first(W), Y) |
-member(Z, second(W)).

% apply_to_two_arguments, axiom.
 equal(apply_to_two_arguments(Xf, X, Y), apply(Xf, ordered_pair(X, Y))).

% maps1, axiom.
-maps(Xf, X, Y) |
 function(Xf).

% maps2, axiom.
-maps(Xf, X, Y) |
 equal(domain_of(Xf), X).

% maps3, axiom.
-maps(Xf, X, Y) |
 subset(range_of(Xf), Y).

% maps4, axiom.
 maps(Xf, X, Y) |
-function(Xf) |
-equal(domain_of(Xf), X) |
-subset(range_of(Xf), Y).

% closed1, axiom.
-closed(Xs, Xf) |
 little_set(Xs).

% closed2, axiom.
-closed(Xs, Xf) |
 little_set(Xf).

% closed3, axiom.
-closed(Xs, Xf) |
 maps(Xf, cross_product(Xs, Xs), Xs).

% closed4, axiom.
 closed(Xs, Xf) |
-little_set(Xs) |
-little_set(Xf) |
-maps(Xf, cross_product(Xs, Xs), Xs).

% compose1, axiom.
-member(Z, compose(Xf, Xg)) |
 little_set(f29(Z, Xf, Xg)).

% compose2, axiom.
-member(Z, compose(Xf, Xg)) |
 little_set(f30(Z, Xf, Xg)).

% compose3, axiom.
-member(Z, compose(Xf, Xg)) |
 little_set(f31(Z, Xf, Xg)).

% compose4, axiom.
-member(Z, compose(Xf, Xg)) |
 equal(Z, ordered_pair(f29(Z, Xf, Xg), f30(Z, Xf, Xg))).

% compose5, axiom.
-member(Z, compose(Xf, Xg)) |
 member(ordered_pair(f29(Z, Xf, Xg), f31(Z, Xf, Xg)), Xf).

% compose6, axiom.
-member(Z, compose(Xf, Xg)) |
 member(ordered_pair(f31(Z, Xf, Xg), f30(Z, Xf, Xg)), Xg).

% compose7, axiom.
 member(Z, compose(Xf, Xg)) |
-little_set(Z) |
-little_set(X) |
-little_set(Y) |
-little_set(W) |
-equal(Z, ordered_pair(X, Y)) |
-member(ordered_pair(X, W), Xf) |
-member(ordered_pair(W, Y), Xg).

% homomorphism1, axiom.
-homomorphism(Xh, Xs1, Xf1, Xs2, Xf2) |
 closed(Xs1, Xf1).

% homomorphism2, axiom.
-homomorphism(Xh, Xs1, Xf1, Xs2, Xf2) |
 closed(Xs2, Xf2).

% homomorphism3, axiom.
-homomorphism(Xh, Xs1, Xf1, Xs2, Xf2) |
 maps(Xh, Xs1, Xs2).

% homomorphism4, axiom.
-homomorphism(Xh, Xs1, Xf1, Xs2, Xf2) |
-member(X, Xs1) |
-member(Y, Xs1) |
 equal(apply(Xh, apply_to_two_arguments(Xf1, X, Y)), apply_to_two_arguments(Xf2, apply(Xh, X), apply(Xh, Y))).

% homomorphism5, axiom.
 homomorphism(Xh, Xs1, Xf1, Xs2, Xf2) |
-closed(Xs1, Xf1) |
-closed(Xs2, Xf2) |
-maps(Xh, Xs1, Xs2) |
 member(f32(Xh, Xs1, Xf1, Xs2, Xf2), Xs1).

% homomorphism6, axiom.
 homomorphism(Xh, Xs1, Xf1, Xs2, Xf2) |
-closed(Xs1, Xf1) |
-closed(Xs2, Xf2) |
-maps(Xh, Xs1, Xs2) |
 member(f33(Xh, Xs1, Xf1, Xs2, Xf2), Xs1).

% homomorphism7, axiom.
 homomorphism(Xh, Xs1, Xf1, Xs2, Xf2) |
-closed(Xs1, Xf1) |
-closed(Xs2, Xf2) |
-maps(Xh, Xs1, Xs2) |
-equal(apply(Xh, apply_to_two_arguments(Xf1, f32(Xh, Xs1, Xf1, Xs2, Xf2), f33(Xh, Xs1, Xf1, Xs2, Xf2))), apply_to_two_arguments(Xf2, apply(Xh, f32(Xh, Xs1, Xf1, Xs2, Xf2)), apply(Xh, f33(Xh, Xs1, Xf1, Xs2, Xf2)))).

% first_components_are_equal, axiom.
-little_set(X) |
-little_set(U) |
-equal(ordered_pair(X, Y), ordered_pair(U, V)) |
 equal(X, U).

% left_cancellation, axiom.
-little_set(X) |
-little_set(Y) |
-equal(non_ordered_pair(Z, X), non_ordered_pair(Z, Y)) |
 equal(X, Y).

% second_components_are_equal, axiom.
-little_set(X) |
-little_set(Y) |
-little_set(U) |
-little_set(V) |
-equal(ordered_pair(X, Y), ordered_pair(U, V)) |
 equal(Y, V).

% two_sets_equal, axiom.
-subset(X, Y) |
-subset(Y, X) |
 equal(X, Y).

% property_of_first, axiom.
-little_set(X) |
-little_set(Y) |
 equal(first(ordered_pair(X, Y)), X).

% property_of_second, axiom.
-little_set(X) |
-little_set(Y) |
 equal(second(ordered_pair(X, Y)), Y).

% first_component_is_small, axiom.
-ordered_pair_predicate(X) |
 little_set(first(X)).

% second_component_is_small, axiom.
-ordered_pair_predicate(X) |
 little_set(second(X)).

% property_of_singleton_sets, axiom.
-little_set(X) |
 member(X, singleton_set(X)).

% ordered_pairs_are_small1, axiom.
 little_set(ordered_pair(X, Y)).

% ordered_pairs_are_small2, axiom.
-ordered_pair_predicate(X) |
 little_set(X).

% containment_is_transitive, axiom.
-subset(X, Y) |
-subset(Y, Z) |
 subset(X, Z).

% image_and_apply1, axiom.
 subset(apply(Xf, Y), sigma(image(singleton_set(Y), Xf))).

% image_and_apply2, axiom.
 subset(image(singleton_set(Y), Xf), apply(Xf, Y)).

% function_values_are_small, axiom.
-function(Y) |
 little_set(apply(Y, X)).

% composition_is_a_relation, axiom.
 relation(compose(Y, X)).

% range_of_composition, axiom.
 subset(range_of(compose(Y, X)), range_of(Y)).

% domain_of_composition, axiom.
-subset(range_of(X), domain_of(Y)) |
 equal(domain_of(X), domain_of(compose(Y, X))).

% composition_is_a_function, axiom.
-function(X) |
-function(Y) |
 function(compose(Y, X)).

% maps_for_composition, axiom.
-maps(Xf, U, V) |
-maps(Xg, V, W) |
 maps(compose(Xg, Xf), U, W).

% apply_for_functions1, axiom.
-little_set(X) |
-little_set(Y) |
-function(Xf) |
-member(ordered_pair(X, Y), Xf) |
 equal(apply(Xf, X), Y).

% apply_for_functions2, axiom.
-function(Xf) |
-member(X, domain_of(Xf)) |
-equal(apply(Xf, X), Y) |
 member(ordered_pair(X, Y), Xf).

% apply_for_functions3, axiom.
-maps(Xf, Xd, Xr) |
-member(X, Xd) |
 member(apply(Xf, X), Xr).

% apply_for_composition1, axiom.
-function(Xf) |
-member(X, domain_of(Xf)) |
 subset(apply(Xg, apply(Xf, X)), apply(compose(Xg, Xf), X)).

% apply_for_composition2, axiom.
-function(Xf) |
 subset(apply(compose(Xg, Xf), X), apply(Xg, apply(Xf, X))).

% apply_for_composition3, axiom.
-function(Xf) |
-member(X, domain_of(Xf)) |
 equal(apply(Xg, apply(Xf, X)), apply(compose(Xg, Xf), X)).

% ordered_pair_in_cross_product, axiom.
-member(X, Xs1) |
-member(Y, Xs2) |
 member(ordered_pair(X, Y), cross_product(Xs1, Xs2)).

% one_homomorphism, hypothesis.
 homomorphism(f60, f62, f63, f64, f65).

% another_homomorphism, hypothesis.
 homomorphism(f61, f64, f65, f66, f67).

% prove_composition_is_a_homomorphism, negated_conjecture.
-homomorphism(compose(f60, f61), f62, f63, f66, f67).

end_of_list.

%------------------------------------------------------------------------------
