% benchmark parameters -n2 -N6 -p

%--------------------------------------------------------------------------
% File     : BOO032-1 : TPTP v2.3.0. Released v2.2.0.
% Domain   : Boolean Algebra
% Problem  : Independence of a system of Boolean algebra
% Version  : [MP96] (equality) axioms : Especial.
% English  : This is part of a proof that a self-dual 3-basis for Boolean 
%            algebra is independent.

% Refs     : [McC98] McCune (1998), Email to G. Sutcliffe
%          : [MP96]  McCune & Padmanabhan (1996), Automated Deduction in Eq
% Source   : [McC98]
% Names    : DUAL-BA-9 [MP96]

% Status   : satisfiable
% Rating   : 1.00 v2.2.1
% Syntax   : Number of clauses    :   14 (   0 non-Horn;  14 unit;   1 RR)
%            Number of literals   :   14 (  14 equality)
%            Maximal clause size  :    1 (   1 average)
%            Number of predicates :    1 (   0 propositional; 2-2 arity)
%            Number of functors   :    4 (   1 constant; 0-2 arity)
%            Number of variables  :   29 (  10 singleton)
%            Maximal term depth   :    4 (   2 average)

% Comments : The smallest model has 5 elements.
%          : tptp2X -f otter:hypothesis:[set(tptp_eq),set(auto),clear(print_given)] -t rm_equality:stfp BOO032-1.p 
%--------------------------------------------------------------------------
set(prolog_style_variables).
set(tptp_eq).
set(auto).
clear(print_given).

list(usable).

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

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

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

% property3, axiom.
 equal(multiply(add(X, inverse(X)), Y), Y).

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

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

% property3_dual, axiom.
 equal(add(multiply(X, inverse(X)), Y), Y).

% majority1, axiom.
 equal(add(multiply(add(X, Y), X), multiply(X, Y)), X).

% majority2, axiom.
 equal(add(multiply(add(X, X), Y), multiply(X, X)), X).

% majority3, axiom.
 equal(add(multiply(add(X, Y), Y), multiply(X, Y)), Y).

% majority1_dual, axiom.
 equal(multiply(add(multiply(X, Y), X), add(X, Y)), X).

% majority2_dual, axiom.
 equal(multiply(add(multiply(X, X), Y), add(X, X)), X).

% majority3_dual, axiom.
 equal(multiply(add(multiply(X, Y), Y), add(X, Y)), Y).

end_of_list.

list(sos).

% prove_inverse_involution, conjecture.
-equal(inverse(inverse(a)), a).

end_of_list.

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