% benchmark parameters -n2 -N6 -p

%--------------------------------------------------------------------------
% File     : RNG025-8 : TPTP v2.3.0. Released v1.0.0.
% Domain   : Ring Theory (Alternative)
% Problem  : Middle or Flexible Law
% Version  : [Ste87] (equality) axioms : Reduced & Augmented > Complete.
%            Theorem formulation : Linearized.
% English  : 

% Refs     : [Ste87] Stevens (1987), Some Experiments in Nonassociative Rin
% Source   : [TPTP]
% Names    : 

% Status   : satisfiable
% Rating   : 0.67 v2.2.1, 0.75 v2.2.0, 0.67 v2.1.0, 1.00 v2.0.0
% Syntax   : Number of clauses    :   19 (   0 non-Horn;  19 unit;   1 RR)
%            Number of literals   :   19 (  19 equality)
%            Maximal clause size  :    1 (   1 average)
%            Number of predicates :    1 (   0 propositional; 2-2 arity)
%            Number of functors   :    9 (   4 constant; 0-3 arity)
%            Number of variables  :   37 (   2 singleton)
%            Maximal term depth   :    4 (   2 average)

% Comments : 
%          : tptp2X -f otter:hypothesis:[set(tptp_eq),set(auto),clear(print_given)] -t rm_equality:stfp RNG025-8.p 
%--------------------------------------------------------------------------
set(prolog_style_variables).
set(tptp_eq).
set(auto).
clear(print_given).

list(usable).

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

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

% associativity_for_addition, axiom.
 equal(add(X, add(Y, Z)), add(add(X, Y), Z)).

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

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

% left_multiplicative_zero, axiom.
 equal(multiply(additive_identity, X), additive_identity).

% right_multiplicative_zero, axiom.
 equal(multiply(X, additive_identity), additive_identity).

% left_additive_inverse, axiom.
 equal(add(additive_inverse(X), X), additive_identity).

% right_additive_inverse, axiom.
 equal(add(X, additive_inverse(X)), additive_identity).

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

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

% additive_inverse_additive_inverse, axiom.
 equal(additive_inverse(additive_inverse(X)), X).

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

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

% linearised_associator1, axiom.
 equal(associator(X, Y, add(U, V)), add(associator(X, Y, U), associator(X, Y, V))).

% linearised_associator2, axiom.
 equal(associator(X, add(U, V), Y), add(associator(X, U, Y), associator(X, V, Y))).

% linearised_associator3, axiom.
 equal(associator(add(U, V), X, Y), add(associator(U, X, Y), associator(V, X, Y))).

% commutator, axiom.
 equal(commutator(X, Y), add(multiply(Y, X), additive_inverse(multiply(X, Y)))).

end_of_list.

list(sos).

% prove_flexible_law, conjecture.
-equal(add(associator(a, b, c), associator(a, c, b)), additive_identity).

end_of_list.

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