%------------------------------------------------------------------------------
% File     : BOO003-2 : TPTP v3.2.0. Released v1.0.0.
% Domain   : Boolean Algebra
% Problem  : Multiplication is idempotent (X * X = X)
% Version  : [ANL] (equality) axioms.
% English  : 

% Refs     : 
% Source   : [ANL]
% Names    : prob2_part1.ver2.in [ANL]

% Status   : Unsatisfiable
% Rating   : 0.00 v2.1.0, 0.38 v2.0.0
% Syntax   : Number of clauses    :   16 (   0 non-Horn;  16 unit;   1 RR)
%            Number of literals   :   16 (  16 equality)
%            Maximal clause size  :    1 (   1 average)
%            Number of predicates :    1 (   0 propositional; 2-2 arity)
%            Number of functors   :    6 (   3 constant; 0-2 arity)
%            Number of variables  :   25 (   0 singleton)
%            Maximal term depth   :    3 (   2 average)

% Comments : 
%          : tptp2X -f otter:none:[set(auto),clear(print_given)] -t stdfof+add_equality:r BOO003-2.p 
%------------------------------------------------------------------------------
set(prolog_style_variables).
set(tptp_eq).
set(auto).
clear(print_given).

list(usable).

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

% commutativity_of_add, axiom.
 equal(add(X, Y), add(Y, X)).

% commutativity_of_multiply, axiom.
 equal(multiply(X, Y), multiply(Y, X)).

% distributivity1, axiom.
 equal(add(multiply(X, Y), Z), multiply(add(X, Z), add(Y, Z))).

% distributivity2, axiom.
 equal(add(X, multiply(Y, Z)), multiply(add(X, Y), add(X, Z))).

% distributivity3, axiom.
 equal(multiply(add(X, Y), Z), add(multiply(X, Z), multiply(Y, Z))).

% distributivity4, axiom.
 equal(multiply(X, add(Y, Z)), add(multiply(X, Y), multiply(X, Z))).

% additive_inverse1, axiom.
 equal(add(X, inverse(X)), multiplicative_identity).

% additive_inverse2, axiom.
 equal(add(inverse(X), X), multiplicative_identity).

% multiplicative_inverse1, axiom.
 equal(multiply(X, inverse(X)), additive_identity).

% multiplicative_inverse2, axiom.
 equal(multiply(inverse(X), X), additive_identity).

% multiplicative_id1, axiom.
 equal(multiply(X, multiplicative_identity), X).

% multiplicative_id2, axiom.
 equal(multiply(multiplicative_identity, X), X).

% additive_id1, axiom.
 equal(add(X, additive_identity), X).

% additive_id2, axiom.
 equal(add(additive_identity, X), X).

% prove_a_times_a_is_a, negated_conjecture.
-equal(multiply(a, a), a).

end_of_list.

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