Prover9---2026-6A.UNS-CRf.s

%------------------------------------------------------------------------------
% File     : Prover9---2026-6A
% Problem  : RNG027-9 : TPTP v9.3.1. Released v1.0.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p

% Computer : n026.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8046.5625MB
% OS       : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Sun Sep 27 08:26:25 AM UTC 2026

% Result   : Unsatisfiable 107.37s 14.94s
% Output   : CNFRefutation 107.37s
% Verified : 
% SZS Type : Refutation
%            Derivation depth      :  154
%            Number of leaves      :   12
% Syntax   : Number of formulae    :  239 ( 239 unt;   0 def)
%            Number of atoms       :  239 ( 238 equ)
%            Maximal formula atoms :    1 (   1 avg)
%            Number of connectives :  127 ( 127   ~;   0   |;   0   &)
%                                         (   0 <=>;   0  =>;   0  <=;   0 <~>)
%            Maximal formula depth :    4 (   2 avg)
%            Maximal term depth    :   12 (   2 avg)
%            Number of predicates  :    2 (   0 usr;   1 prp; 0-2 aty)
%            Number of functors    :    8 (   8 usr;   4 con; 0-3 aty)
%            Number of variables   :  304 (   0 sgn  23   !;   0   ?)

% Comments : 
%------------------------------------------------------------------------------
fof(left_additive_identity,axiom,
    ! [VAR_0] : add(additive_identity,VAR_0) = VAR_0,
    file('theBenchmark.p',left_additive_identity) ).

cnf(c_1,plain,
    add(additive_identity,A) = A,
    inference(clausify,[status(thm)],[left_additive_identity]) ).

fof(right_additive_inverse,axiom,
    ! [VAR_0] : add(VAR_0,additive_inverse(VAR_0)) = additive_identity,
    file('theBenchmark.p',right_additive_inverse) ).

cnf(c_6,plain,
    add(A,additive_inverse(A)) = additive_identity,
    inference(clausify,[status(thm)],[right_additive_inverse]) ).

fof(additive_inverse_additive_inverse,axiom,
    ! [VAR_0] : additive_inverse(additive_inverse(VAR_0)) = VAR_0,
    file('theBenchmark.p',additive_inverse_additive_inverse) ).

cnf(c_7,plain,
    additive_inverse(additive_inverse(A)) = A,
    inference(clausify,[status(thm)],[additive_inverse_additive_inverse]) ).

fof(distribute1,axiom,
    ! [VAR_0,VAR_1,VAR_2] : multiply(VAR_0,add(VAR_1,VAR_2)) = add(multiply(VAR_0,VAR_1),multiply(VAR_0,VAR_2)),
    file('theBenchmark.p',distribute1) ).

cnf(c_8,plain,
    multiply(A,add(B,C)) = add(multiply(A,B),multiply(A,C)),
    inference(clausify,[status(thm)],[distribute1]) ).

fof(distribute2,axiom,
    ! [VAR_0,VAR_1,VAR_2] : multiply(add(VAR_0,VAR_1),VAR_2) = add(multiply(VAR_0,VAR_2),multiply(VAR_1,VAR_2)),
    file('theBenchmark.p',distribute2) ).

cnf(c_9,plain,
    multiply(add(A,B),C) = add(multiply(A,C),multiply(B,C)),
    inference(clausify,[status(thm)],[distribute2]) ).

fof(commutativity_for_addition,axiom,
    ! [VAR_0,VAR_1] : add(VAR_0,VAR_1) = add(VAR_1,VAR_0),
    file('theBenchmark.p',commutativity_for_addition) ).

cnf(c_10,plain,
    add(A,B) = add(B,A),
    inference(clausify,[status(thm)],[commutativity_for_addition]) ).

fof(associativity_for_addition,axiom,
    ! [VAR_0,VAR_1,VAR_2] : add(VAR_0,add(VAR_1,VAR_2)) = add(add(VAR_0,VAR_1),VAR_2),
    file('theBenchmark.p',associativity_for_addition) ).

cnf(c_11,plain,
    add(A,add(B,C)) = add(add(A,B),C),
    inference(clausify,[status(thm)],[associativity_for_addition]) ).

cnf(c_12,plain,
    add(add(A,B),C) = add(A,add(B,C)),
    inference(copy,[status(thm)],[c_11]) ).

fof(right_alternative,axiom,
    ! [VAR_0,VAR_1] : multiply(multiply(VAR_0,VAR_1),VAR_1) = multiply(VAR_0,multiply(VAR_1,VAR_1)),
    file('theBenchmark.p',right_alternative) ).

cnf(c_13,plain,
    multiply(multiply(A,B),B) = multiply(A,multiply(B,B)),
    inference(clausify,[status(thm)],[right_alternative]) ).

fof(left_alternative,axiom,
    ! [VAR_0,VAR_1] : multiply(multiply(VAR_0,VAR_0),VAR_1) = multiply(VAR_0,multiply(VAR_0,VAR_1)),
    file('theBenchmark.p',left_alternative) ).

cnf(c_14,plain,
    multiply(multiply(A,A),B) = multiply(A,multiply(A,B)),
    inference(clausify,[status(thm)],[left_alternative]) ).

fof(associator,axiom,
    ! [VAR_0,VAR_1,VAR_2] : associator(VAR_0,VAR_1,VAR_2) = add(multiply(multiply(VAR_0,VAR_1),VAR_2),additive_inverse(multiply(VAR_0,multiply(VAR_1,VAR_2)))),
    file('theBenchmark.p',associator) ).

cnf(c_15,plain,
    associator(A,B,C) = add(multiply(multiply(A,B),C),additive_inverse(multiply(A,multiply(B,C)))),
    inference(clausify,[status(thm)],[associator]) ).

cnf(c_16,plain,
    associator(A,B,C) = add(additive_inverse(multiply(A,multiply(B,C))),multiply(multiply(A,B),C)),
    inference(paramod,[status(thm)],[c_10,c_15]) ).

fof(inverse_product1,axiom,
    ! [VAR_0,VAR_1] : multiply(additive_inverse(VAR_0),VAR_1) = additive_inverse(multiply(VAR_0,VAR_1)),
    file('theBenchmark.p',inverse_product1) ).

cnf(c_19,plain,
    multiply(additive_inverse(A),B) = additive_inverse(multiply(A,B)),
    inference(clausify,[status(thm)],[inverse_product1]) ).

fof(prove_right_moufang,axiom,
    associator(x,multiply(x,y),z) != multiply(associator(x,y,z),x),
    file('theBenchmark.p',prove_right_moufang) ).

cnf(c_26,plain,
    associator(x,multiply(x,y),z) != multiply(associator(x,y,z),x),
    inference(clausify,[status(thm)],[prove_right_moufang]) ).

cnf(c_11441,plain,
    add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)) != multiply(associator(x,y,z),x),
    inference(paramod,[status(thm)],[c_16,c_26]) ).

cnf(c_11442,plain,
    add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)) != multiply(add(additive_inverse(multiply(x,multiply(y,z))),multiply(multiply(x,y),z)),x),
    inference(paramod,[status(thm)],[c_16,c_11441]) ).

cnf(c_11443,plain,
    add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)) != add(multiply(additive_inverse(multiply(x,multiply(y,z))),x),multiply(multiply(multiply(x,y),z),x)),
    inference(paramod,[status(thm)],[c_9,c_11442]) ).

cnf(c_11444,plain,
    add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)) != add(additive_inverse(multiply(multiply(x,multiply(y,z)),x)),multiply(multiply(multiply(x,y),z),x)),
    inference(paramod,[status(thm)],[c_19,c_11443]) ).

cnf(c_27,plain,
    add(additive_inverse(multiply(multiply(x,multiply(y,z)),x)),multiply(multiply(multiply(x,y),z),x)) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(copy,[status(thm)],[c_11444]) ).

cnf(c_11445,plain,
    add(additive_identity,A) = add(B,add(additive_inverse(B),A)),
    inference(paramod,[status(thm)],[c_6,c_12]) ).

cnf(c_11446,plain,
    A = add(B,add(additive_inverse(B),A)),
    inference(paramod,[status(thm)],[c_1,c_11445]) ).

cnf(c_31,plain,
    add(A,add(additive_inverse(A),B)) = B,
    inference(copy,[status(thm)],[c_11446]) ).

cnf(c_11447,plain,
    add(add(A,B),C) = add(B,add(A,C)),
    inference(paramod,[status(thm)],[c_10,c_12]) ).

cnf(c_33,plain,
    add(A,add(B,C)) = add(B,add(A,C)),
    inference(paramod,[status(thm)],[c_12,c_11447]) ).

cnf(c_11448,plain,
    multiply(A,multiply(add(B,C),add(B,C))) = add(multiply(multiply(A,add(B,C)),B),multiply(multiply(A,add(B,C)),C)),
    inference(paramod,[status(thm)],[c_13,c_8]) ).

cnf(c_11449,plain,
    multiply(A,add(multiply(add(B,C),B),multiply(add(B,C),C))) = add(multiply(multiply(A,add(B,C)),B),multiply(multiply(A,add(B,C)),C)),
    inference(paramod,[status(thm)],[c_8,c_11448]) ).

cnf(c_11450,plain,
    multiply(A,add(add(multiply(B,B),multiply(C,B)),multiply(add(B,C),C))) = add(multiply(multiply(A,add(B,C)),B),multiply(multiply(A,add(B,C)),C)),
    inference(paramod,[status(thm)],[c_9,c_11449]) ).

cnf(c_11451,plain,
    multiply(A,add(add(multiply(B,B),multiply(C,B)),add(multiply(B,C),multiply(C,C)))) = add(multiply(multiply(A,add(B,C)),B),multiply(multiply(A,add(B,C)),C)),
    inference(paramod,[status(thm)],[c_9,c_11450]) ).

cnf(c_11452,plain,
    multiply(A,add(multiply(B,B),add(multiply(C,B),add(multiply(B,C),multiply(C,C))))) = add(multiply(multiply(A,add(B,C)),B),multiply(multiply(A,add(B,C)),C)),
    inference(paramod,[status(thm)],[c_12,c_11451]) ).

cnf(c_11453,plain,
    add(multiply(A,multiply(B,B)),multiply(A,add(multiply(C,B),add(multiply(B,C),multiply(C,C))))) = add(multiply(multiply(A,add(B,C)),B),multiply(multiply(A,add(B,C)),C)),
    inference(paramod,[status(thm)],[c_8,c_11452]) ).

cnf(c_11454,plain,
    add(multiply(A,multiply(B,B)),add(multiply(A,multiply(C,B)),multiply(A,add(multiply(B,C),multiply(C,C))))) = add(multiply(multiply(A,add(B,C)),B),multiply(multiply(A,add(B,C)),C)),
    inference(paramod,[status(thm)],[c_8,c_11453]) ).

cnf(c_11455,plain,
    add(multiply(A,multiply(B,B)),add(multiply(A,multiply(C,B)),add(multiply(A,multiply(B,C)),multiply(A,multiply(C,C))))) = add(multiply(multiply(A,add(B,C)),B),multiply(multiply(A,add(B,C)),C)),
    inference(paramod,[status(thm)],[c_8,c_11454]) ).

cnf(c_11456,plain,
    add(multiply(A,multiply(B,B)),add(multiply(A,multiply(C,B)),add(multiply(A,multiply(B,C)),multiply(A,multiply(C,C))))) = add(multiply(add(multiply(A,B),multiply(A,C)),B),multiply(multiply(A,add(B,C)),C)),
    inference(paramod,[status(thm)],[c_8,c_11455]) ).

cnf(c_11457,plain,
    add(multiply(A,multiply(B,B)),add(multiply(A,multiply(C,B)),add(multiply(A,multiply(B,C)),multiply(A,multiply(C,C))))) = add(add(multiply(multiply(A,B),B),multiply(multiply(A,C),B)),multiply(multiply(A,add(B,C)),C)),
    inference(paramod,[status(thm)],[c_9,c_11456]) ).

cnf(c_11458,plain,
    add(multiply(A,multiply(B,B)),add(multiply(A,multiply(C,B)),add(multiply(A,multiply(B,C)),multiply(A,multiply(C,C))))) = add(add(multiply(A,multiply(B,B)),multiply(multiply(A,C),B)),multiply(multiply(A,add(B,C)),C)),
    inference(paramod,[status(thm)],[c_13,c_11457]) ).

cnf(c_11459,plain,
    add(multiply(A,multiply(B,B)),add(multiply(A,multiply(C,B)),add(multiply(A,multiply(B,C)),multiply(A,multiply(C,C))))) = add(add(multiply(A,multiply(B,B)),multiply(multiply(A,C),B)),multiply(add(multiply(A,B),multiply(A,C)),C)),
    inference(paramod,[status(thm)],[c_8,c_11458]) ).

cnf(c_11460,plain,
    add(multiply(A,multiply(B,B)),add(multiply(A,multiply(C,B)),add(multiply(A,multiply(B,C)),multiply(A,multiply(C,C))))) = add(add(multiply(A,multiply(B,B)),multiply(multiply(A,C),B)),add(multiply(multiply(A,B),C),multiply(multiply(A,C),C))),
    inference(paramod,[status(thm)],[c_9,c_11459]) ).

cnf(c_11461,plain,
    add(multiply(A,multiply(B,B)),add(multiply(A,multiply(C,B)),add(multiply(A,multiply(B,C)),multiply(A,multiply(C,C))))) = add(add(multiply(A,multiply(B,B)),multiply(multiply(A,C),B)),add(multiply(multiply(A,B),C),multiply(A,multiply(C,C)))),
    inference(paramod,[status(thm)],[c_13,c_11460]) ).

cnf(c_11462,plain,
    add(multiply(A,multiply(B,B)),add(multiply(A,multiply(C,B)),add(multiply(A,multiply(B,C)),multiply(A,multiply(C,C))))) = add(multiply(A,multiply(B,B)),add(multiply(multiply(A,C),B),add(multiply(multiply(A,B),C),multiply(A,multiply(C,C))))),
    inference(paramod,[status(thm)],[c_12,c_11461]) ).

cnf(c_34,plain,
    add(multiply(A,multiply(B,B)),add(multiply(multiply(A,C),B),add(multiply(multiply(A,B),C),multiply(A,multiply(C,C))))) = add(multiply(A,multiply(B,B)),add(multiply(A,multiply(C,B)),add(multiply(A,multiply(B,C)),multiply(A,multiply(C,C))))),
    inference(copy,[status(thm)],[c_11462]) ).

cnf(c_11463,plain,
    multiply(add(multiply(add(A,B),A),multiply(add(A,B),B)),C) = multiply(add(A,B),multiply(add(A,B),C)),
    inference(paramod,[status(thm)],[c_8,c_14]) ).

cnf(c_11464,plain,
    multiply(add(add(multiply(A,A),multiply(B,A)),multiply(add(A,B),B)),C) = multiply(add(A,B),multiply(add(A,B),C)),
    inference(paramod,[status(thm)],[c_9,c_11463]) ).

cnf(c_11465,plain,
    multiply(add(add(multiply(A,A),multiply(B,A)),add(multiply(A,B),multiply(B,B))),C) = multiply(add(A,B),multiply(add(A,B),C)),
    inference(paramod,[status(thm)],[c_9,c_11464]) ).

cnf(c_11466,plain,
    multiply(add(multiply(A,A),add(multiply(B,A),add(multiply(A,B),multiply(B,B)))),C) = multiply(add(A,B),multiply(add(A,B),C)),
    inference(paramod,[status(thm)],[c_12,c_11465]) ).

cnf(c_11467,plain,
    add(multiply(multiply(A,A),C),multiply(add(multiply(B,A),add(multiply(A,B),multiply(B,B))),C)) = multiply(add(A,B),multiply(add(A,B),C)),
    inference(paramod,[status(thm)],[c_9,c_11466]) ).

cnf(c_11468,plain,
    add(multiply(A,multiply(A,C)),multiply(add(multiply(B,A),add(multiply(A,B),multiply(B,B))),C)) = multiply(add(A,B),multiply(add(A,B),C)),
    inference(paramod,[status(thm)],[c_14,c_11467]) ).

cnf(c_11469,plain,
    add(multiply(A,multiply(A,C)),add(multiply(multiply(B,A),C),multiply(add(multiply(A,B),multiply(B,B)),C))) = multiply(add(A,B),multiply(add(A,B),C)),
    inference(paramod,[status(thm)],[c_9,c_11468]) ).

cnf(c_11470,plain,
    add(multiply(A,multiply(A,C)),add(multiply(multiply(B,A),C),add(multiply(multiply(A,B),C),multiply(multiply(B,B),C)))) = multiply(add(A,B),multiply(add(A,B),C)),
    inference(paramod,[status(thm)],[c_9,c_11469]) ).

cnf(c_11471,plain,
    add(multiply(A,multiply(A,C)),add(multiply(multiply(B,A),C),add(multiply(multiply(A,B),C),multiply(B,multiply(B,C))))) = multiply(add(A,B),multiply(add(A,B),C)),
    inference(paramod,[status(thm)],[c_14,c_11470]) ).

cnf(c_11472,plain,
    add(multiply(A,multiply(A,C)),add(multiply(multiply(B,A),C),add(multiply(B,multiply(B,C)),multiply(multiply(A,B),C)))) = multiply(add(A,B),multiply(add(A,B),C)),
    inference(paramod,[status(thm)],[c_10,c_11471]) ).

cnf(c_11473,plain,
    add(multiply(A,multiply(A,C)),add(multiply(B,multiply(B,C)),add(multiply(multiply(B,A),C),multiply(multiply(A,B),C)))) = multiply(add(A,B),multiply(add(A,B),C)),
    inference(paramod,[status(thm)],[c_33,c_11472]) ).

cnf(c_11474,plain,
    add(multiply(A,multiply(A,C)),add(multiply(B,multiply(B,C)),add(multiply(multiply(B,A),C),multiply(multiply(A,B),C)))) = multiply(add(A,B),add(multiply(A,C),multiply(B,C))),
    inference(paramod,[status(thm)],[c_9,c_11473]) ).

cnf(c_11475,plain,
    add(multiply(A,multiply(A,C)),add(multiply(B,multiply(B,C)),add(multiply(multiply(B,A),C),multiply(multiply(A,B),C)))) = add(multiply(add(A,B),multiply(A,C)),multiply(add(A,B),multiply(B,C))),
    inference(paramod,[status(thm)],[c_8,c_11474]) ).

cnf(c_11476,plain,
    add(multiply(A,multiply(A,C)),add(multiply(B,multiply(B,C)),add(multiply(multiply(B,A),C),multiply(multiply(A,B),C)))) = add(add(multiply(A,multiply(A,C)),multiply(B,multiply(A,C))),multiply(add(A,B),multiply(B,C))),
    inference(paramod,[status(thm)],[c_9,c_11475]) ).

cnf(c_11477,plain,
    add(multiply(A,multiply(A,C)),add(multiply(B,multiply(B,C)),add(multiply(multiply(B,A),C),multiply(multiply(A,B),C)))) = add(add(multiply(A,multiply(A,C)),multiply(B,multiply(A,C))),add(multiply(A,multiply(B,C)),multiply(B,multiply(B,C)))),
    inference(paramod,[status(thm)],[c_9,c_11476]) ).

cnf(c_36,plain,
    add(multiply(A,multiply(A,B)),add(multiply(C,multiply(C,B)),add(multiply(multiply(C,A),B),multiply(multiply(A,C),B)))) = add(multiply(A,multiply(A,B)),add(multiply(C,multiply(A,B)),add(multiply(A,multiply(C,B)),multiply(C,multiply(C,B))))),
    inference(paramod,[status(thm)],[c_12,c_11477]) ).

cnf(c_51,plain,
    add(A,add(B,additive_inverse(A))) = B,
    inference(paramod,[status(thm)],[c_10,c_31]) ).

cnf(c_54,plain,
    add(additive_inverse(A),add(B,A)) = B,
    inference(paramod,[status(thm)],[c_7,c_51]) ).

cnf(c_11478,plain,
    add(A,B) = add(additive_inverse(C),add(add(A,C),B)),
    inference(paramod,[status(thm)],[c_54,c_12]) ).

cnf(c_11479,plain,
    add(A,B) = add(additive_inverse(C),add(A,add(C,B))),
    inference(paramod,[status(thm)],[c_12,c_11478]) ).

cnf(c_58,plain,
    add(additive_inverse(A),add(B,add(A,C))) = add(B,C),
    inference(copy,[status(thm)],[c_11479]) ).

cnf(c_59,plain,
    add(additive_inverse(A),add(B,add(C,A))) = add(B,C),
    inference(paramod,[status(thm)],[c_12,c_54]) ).

cnf(c_11480,plain,
    add(additive_inverse(add(A,B)),A) = additive_inverse(B),
    inference(paramod,[status(thm)],[c_54,c_54]) ).

cnf(c_62,plain,
    add(A,additive_inverse(add(A,B))) = additive_inverse(B),
    inference(paramod,[status(thm)],[c_10,c_11480]) ).

cnf(c_11481,plain,
    add(additive_inverse(A),additive_inverse(B)) = additive_inverse(add(B,A)),
    inference(paramod,[status(thm)],[c_54,c_62]) ).

cnf(c_73,plain,
    additive_inverse(add(A,B)) = add(additive_inverse(B),additive_inverse(A)),
    inference(copy,[status(thm)],[c_11481]) ).

cnf(c_11482,plain,
    add(multiply(A,multiply(B,B)),add(multiply(A,multiply(C,B)),add(multiply(A,multiply(B,C)),multiply(A,multiply(C,C))))) = add(multiply(multiply(A,C),B),add(multiply(A,multiply(B,B)),add(multiply(multiply(A,B),C),multiply(A,multiply(C,C))))),
    inference(paramod,[status(thm)],[c_34,c_33]) ).

cnf(c_99,plain,
    add(multiply(multiply(A,B),C),add(multiply(A,multiply(C,C)),add(multiply(multiply(A,C),B),multiply(A,multiply(B,B))))) = add(multiply(A,multiply(C,C)),add(multiply(A,multiply(B,C)),add(multiply(A,multiply(C,B)),multiply(A,multiply(B,B))))),
    inference(copy,[status(thm)],[c_11482]) ).

cnf(c_105,plain,
    add(additive_inverse(A),add(B,add(C,add(D,A)))) = add(B,add(C,D)),
    inference(paramod,[status(thm)],[c_12,c_59]) ).

cnf(c_11483,plain,
    add(additive_inverse(multiply(A,multiply(A,B))),add(multiply(C,multiply(C,B)),add(multiply(A,multiply(C,B)),add(multiply(C,multiply(A,B)),multiply(A,multiply(A,B)))))) = add(multiply(C,multiply(C,B)),add(multiply(multiply(A,C),B),multiply(multiply(C,A),B))),
    inference(paramod,[status(thm)],[c_36,c_58]) ).

cnf(c_11484,plain,
    add(multiply(C,multiply(C,B)),add(multiply(A,multiply(C,B)),multiply(C,multiply(A,B)))) = add(multiply(C,multiply(C,B)),add(multiply(multiply(A,C),B),multiply(multiply(C,A),B))),
    inference(paramod,[status(thm)],[c_105,c_11483]) ).

cnf(c_137,plain,
    add(multiply(A,multiply(A,B)),add(multiply(multiply(C,A),B),multiply(multiply(A,C),B))) = add(multiply(A,multiply(A,B)),add(multiply(C,multiply(A,B)),multiply(A,multiply(C,B)))),
    inference(copy,[status(thm)],[c_11484]) ).

cnf(c_11485,plain,
    add(additive_inverse(multiply(A,multiply(A,B))),add(C,add(multiply(A,multiply(A,B)),add(multiply(D,multiply(A,B)),multiply(A,multiply(D,B)))))) = add(C,add(multiply(multiply(D,A),B),multiply(multiply(A,D),B))),
    inference(paramod,[status(thm)],[c_137,c_58]) ).

cnf(c_11486,plain,
    add(C,add(multiply(D,multiply(A,B)),multiply(A,multiply(D,B)))) = add(C,add(multiply(multiply(D,A),B),multiply(multiply(A,D),B))),
    inference(paramod,[status(thm)],[c_58,c_11485]) ).

cnf(c_682,plain,
    add(A,add(multiply(multiply(B,C),D),multiply(multiply(C,B),D))) = add(A,add(multiply(B,multiply(C,D)),multiply(C,multiply(B,D)))),
    inference(copy,[status(thm)],[c_11486]) ).

cnf(c_11487,plain,
    add(additive_identity,add(multiply(A,multiply(B,C)),multiply(B,multiply(A,C)))) = add(multiply(multiply(A,B),C),multiply(multiply(B,A),C)),
    inference(paramod,[status(thm)],[c_682,c_1]) ).

cnf(c_11488,plain,
    add(multiply(A,multiply(B,C)),multiply(B,multiply(A,C))) = add(multiply(multiply(A,B),C),multiply(multiply(B,A),C)),
    inference(paramod,[status(thm)],[c_1,c_11487]) ).

cnf(c_753,plain,
    add(multiply(multiply(A,B),C),multiply(multiply(B,A),C)) = add(multiply(A,multiply(B,C)),multiply(B,multiply(A,C))),
    inference(copy,[status(thm)],[c_11488]) ).

cnf(c_11489,plain,
    add(additive_inverse(multiply(multiply(A,B),C)),add(multiply(B,multiply(A,C)),multiply(A,multiply(B,C)))) = multiply(multiply(B,A),C),
    inference(paramod,[status(thm)],[c_682,c_54]) ).

cnf(c_11490,plain,
    add(add(multiply(B,multiply(A,C)),multiply(A,multiply(B,C))),additive_inverse(multiply(multiply(A,B),C))) = multiply(multiply(B,A),C),
    inference(paramod,[status(thm)],[c_10,c_11489]) ).

cnf(c_11491,plain,
    add(multiply(B,multiply(A,C)),add(multiply(A,multiply(B,C)),additive_inverse(multiply(multiply(A,B),C)))) = multiply(multiply(B,A),C),
    inference(paramod,[status(thm)],[c_12,c_11490]) ).

cnf(c_763,plain,
    multiply(multiply(A,B),C) = add(multiply(A,multiply(B,C)),add(multiply(B,multiply(A,C)),additive_inverse(multiply(multiply(B,A),C)))),
    inference(copy,[status(thm)],[c_11491]) ).

cnf(c_834,plain,
    add(multiply(A,multiply(B,B)),multiply(multiply(B,A),B)) = add(multiply(A,multiply(B,B)),multiply(B,multiply(A,B))),
    inference(paramod,[status(thm)],[c_13,c_753]) ).

cnf(c_835,plain,
    add(multiply(multiply(A,multiply(B,A)),C),multiply(multiply(B,multiply(A,A)),C)) = add(multiply(A,multiply(multiply(B,A),C)),multiply(multiply(B,A),multiply(A,C))),
    inference(paramod,[status(thm)],[c_13,c_753]) ).

cnf(c_11492,plain,
    add(additive_inverse(multiply(A,multiply(B,B))),add(C,add(multiply(A,multiply(B,B)),multiply(B,multiply(A,B))))) = add(C,multiply(multiply(B,A),B)),
    inference(paramod,[status(thm)],[c_834,c_58]) ).

cnf(c_11493,plain,
    add(C,multiply(B,multiply(A,B))) = add(C,multiply(multiply(B,A),B)),
    inference(paramod,[status(thm)],[c_58,c_11492]) ).

cnf(c_890,plain,
    add(A,multiply(multiply(B,C),B)) = add(A,multiply(B,multiply(C,B))),
    inference(copy,[status(thm)],[c_11493]) ).

cnf(c_11494,plain,
    add(additive_identity,multiply(A,multiply(B,A))) = multiply(multiply(A,B),A),
    inference(paramod,[status(thm)],[c_890,c_1]) ).

cnf(c_11495,plain,
    multiply(A,multiply(B,A)) = multiply(multiply(A,B),A),
    inference(paramod,[status(thm)],[c_1,c_11494]) ).

cnf(c_949,plain,
    multiply(multiply(A,B),A) = multiply(A,multiply(B,A)),
    inference(copy,[status(thm)],[c_11495]) ).

cnf(c_992,plain,
    add(additive_inverse(multiply(x,multiply(multiply(y,z),x))),multiply(multiply(multiply(x,y),z),x)) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_949,c_27]) ).

cnf(c_11496,plain,
    add(additive_inverse(multiply(x,multiply(multiply(y,z),x))),multiply(add(multiply(x,multiply(y,z)),add(multiply(y,multiply(x,z)),additive_inverse(multiply(multiply(y,x),z)))),x)) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_763,c_992]) ).

cnf(c_11497,plain,
    add(additive_inverse(multiply(x,multiply(multiply(y,z),x))),add(multiply(multiply(x,multiply(y,z)),x),multiply(add(multiply(y,multiply(x,z)),additive_inverse(multiply(multiply(y,x),z))),x))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_9,c_11496]) ).

cnf(c_11498,plain,
    add(additive_inverse(multiply(x,multiply(multiply(y,z),x))),add(multiply(x,multiply(multiply(y,z),x)),multiply(add(multiply(y,multiply(x,z)),additive_inverse(multiply(multiply(y,x),z))),x))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_949,c_11497]) ).

cnf(c_11499,plain,
    add(additive_inverse(multiply(x,multiply(multiply(y,z),x))),add(multiply(x,multiply(multiply(y,z),x)),add(multiply(multiply(y,multiply(x,z)),x),multiply(additive_inverse(multiply(multiply(y,x),z)),x)))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_9,c_11498]) ).

cnf(c_11500,plain,
    add(additive_inverse(multiply(x,multiply(multiply(y,z),x))),add(multiply(x,multiply(multiply(y,z),x)),add(multiply(multiply(y,multiply(x,z)),x),additive_inverse(multiply(multiply(multiply(y,x),z),x))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_19,c_11499]) ).

cnf(c_11501,plain,
    add(multiply(x,multiply(multiply(y,z),x)),add(additive_inverse(multiply(x,multiply(multiply(y,z),x))),add(multiply(multiply(y,multiply(x,z)),x),additive_inverse(multiply(multiply(multiply(y,x),z),x))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_33,c_11500]) ).

cnf(c_1605,plain,
    add(multiply(multiply(y,multiply(x,z)),x),additive_inverse(multiply(multiply(multiply(y,x),z),x))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_31,c_11501]) ).

cnf(c_11502,plain,
    add(additive_inverse(add(multiply(A,multiply(B,B)),add(multiply(multiply(A,B),C),multiply(A,multiply(C,C))))),add(multiply(A,multiply(B,B)),add(multiply(A,multiply(C,B)),add(multiply(A,multiply(B,C)),multiply(A,multiply(C,C)))))) = multiply(multiply(A,C),B),
    inference(paramod,[status(thm)],[c_99,c_54]) ).

cnf(c_11503,plain,
    add(add(additive_inverse(add(multiply(multiply(A,B),C),multiply(A,multiply(C,C)))),additive_inverse(multiply(A,multiply(B,B)))),add(multiply(A,multiply(B,B)),add(multiply(A,multiply(C,B)),add(multiply(A,multiply(B,C)),multiply(A,multiply(C,C)))))) = multiply(multiply(A,C),B),
    inference(paramod,[status(thm)],[c_73,c_11502]) ).

cnf(c_11504,plain,
    add(add(add(additive_inverse(multiply(A,multiply(C,C))),additive_inverse(multiply(multiply(A,B),C))),additive_inverse(multiply(A,multiply(B,B)))),add(multiply(A,multiply(B,B)),add(multiply(A,multiply(C,B)),add(multiply(A,multiply(B,C)),multiply(A,multiply(C,C)))))) = multiply(multiply(A,C),B),
    inference(paramod,[status(thm)],[c_73,c_11503]) ).

cnf(c_11505,plain,
    add(add(additive_inverse(multiply(A,multiply(B,B))),add(additive_inverse(multiply(A,multiply(C,C))),additive_inverse(multiply(multiply(A,B),C)))),add(multiply(A,multiply(B,B)),add(multiply(A,multiply(C,B)),add(multiply(A,multiply(B,C)),multiply(A,multiply(C,C)))))) = multiply(multiply(A,C),B),
    inference(paramod,[status(thm)],[c_10,c_11504]) ).

cnf(c_11506,plain,
    add(multiply(A,multiply(B,B)),add(add(additive_inverse(multiply(A,multiply(B,B))),add(additive_inverse(multiply(A,multiply(C,C))),additive_inverse(multiply(multiply(A,B),C)))),add(multiply(A,multiply(C,B)),add(multiply(A,multiply(B,C)),multiply(A,multiply(C,C)))))) = multiply(multiply(A,C),B),
    inference(paramod,[status(thm)],[c_33,c_11505]) ).

cnf(c_11507,plain,
    add(multiply(A,multiply(B,B)),add(additive_inverse(multiply(A,multiply(B,B))),add(add(additive_inverse(multiply(A,multiply(C,C))),additive_inverse(multiply(multiply(A,B),C))),add(multiply(A,multiply(C,B)),add(multiply(A,multiply(B,C)),multiply(A,multiply(C,C))))))) = multiply(multiply(A,C),B),
    inference(paramod,[status(thm)],[c_12,c_11506]) ).

cnf(c_11508,plain,
    add(multiply(A,multiply(B,B)),add(additive_inverse(multiply(A,multiply(B,B))),add(additive_inverse(multiply(A,multiply(C,C))),add(additive_inverse(multiply(multiply(A,B),C)),add(multiply(A,multiply(C,B)),add(multiply(A,multiply(B,C)),multiply(A,multiply(C,C)))))))) = multiply(multiply(A,C),B),
    inference(paramod,[status(thm)],[c_12,c_11507]) ).

cnf(c_11509,plain,
    add(multiply(A,multiply(B,B)),add(additive_inverse(multiply(A,multiply(B,B))),add(additive_inverse(multiply(multiply(A,B),C)),add(multiply(A,multiply(C,B)),multiply(A,multiply(B,C)))))) = multiply(multiply(A,C),B),
    inference(paramod,[status(thm)],[c_105,c_11508]) ).

cnf(c_11510,plain,
    add(additive_inverse(multiply(multiply(A,B),C)),add(multiply(A,multiply(C,B)),multiply(A,multiply(B,C)))) = multiply(multiply(A,C),B),
    inference(paramod,[status(thm)],[c_31,c_11509]) ).

cnf(c_3577,plain,
    multiply(multiply(A,B),C) = add(additive_inverse(multiply(multiply(A,C),B)),add(multiply(A,multiply(B,C)),multiply(A,multiply(C,B)))),
    inference(copy,[status(thm)],[c_11510]) ).

cnf(c_4600,plain,
    multiply(multiply(A,multiply(B,C)),C) = add(additive_inverse(multiply(multiply(A,C),multiply(B,C))),add(multiply(A,multiply(B,multiply(C,C))),multiply(A,multiply(C,multiply(B,C))))),
    inference(paramod,[status(thm)],[c_13,c_3577]) ).

cnf(c_11511,plain,
    associator(A,B,C) = add(additive_inverse(multiply(A,multiply(B,C))),add(additive_inverse(multiply(multiply(A,C),B)),add(multiply(A,multiply(B,C)),multiply(A,multiply(C,B))))),
    inference(paramod,[status(thm)],[c_3577,c_16]) ).

cnf(c_11512,plain,
    add(additive_inverse(multiply(A,multiply(B,C))),multiply(multiply(A,B),C)) = add(additive_inverse(multiply(A,multiply(B,C))),add(additive_inverse(multiply(multiply(A,C),B)),add(multiply(A,multiply(B,C)),multiply(A,multiply(C,B))))),
    inference(paramod,[status(thm)],[c_16,c_11511]) ).

cnf(c_11513,plain,
    add(additive_inverse(multiply(A,multiply(B,C))),multiply(multiply(A,B),C)) = add(additive_inverse(multiply(multiply(A,C),B)),multiply(A,multiply(C,B))),
    inference(paramod,[status(thm)],[c_58,c_11512]) ).

cnf(c_4609,plain,
    add(additive_inverse(multiply(A,multiply(B,C))),multiply(multiply(A,B),C)) = add(multiply(A,multiply(C,B)),additive_inverse(multiply(multiply(A,C),B))),
    inference(paramod,[status(thm)],[c_10,c_11513]) ).

cnf(c_4670,plain,
    multiply(multiply(A,multiply(B,C)),B) = add(additive_inverse(multiply(multiply(A,B),multiply(B,C))),add(multiply(A,multiply(B,multiply(C,B))),multiply(A,multiply(B,multiply(B,C))))),
    inference(paramod,[status(thm)],[c_949,c_3577]) ).

cnf(c_11514,plain,
    add(multiply(multiply(y,multiply(x,z)),x),additive_inverse(multiply(add(additive_inverse(multiply(multiply(y,z),x)),add(multiply(y,multiply(x,z)),multiply(y,multiply(z,x)))),x))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_3577,c_1605]) ).

cnf(c_11515,plain,
    add(add(additive_inverse(multiply(multiply(y,x),multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),multiply(y,multiply(x,multiply(x,z))))),additive_inverse(multiply(add(additive_inverse(multiply(multiply(y,z),x)),add(multiply(y,multiply(x,z)),multiply(y,multiply(z,x)))),x))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_4670,c_11514]) ).

cnf(c_11516,plain,
    add(add(additive_inverse(multiply(multiply(y,x),multiply(x,z))),add(multiply(y,multiply(x,multiply(x,z))),multiply(y,multiply(x,multiply(z,x))))),additive_inverse(multiply(add(additive_inverse(multiply(multiply(y,z),x)),add(multiply(y,multiply(x,z)),multiply(y,multiply(z,x)))),x))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_10,c_11515]) ).

cnf(c_11517,plain,
    add(add(add(multiply(y,multiply(x,multiply(x,z))),multiply(y,multiply(x,multiply(z,x)))),additive_inverse(multiply(multiply(y,x),multiply(x,z)))),additive_inverse(multiply(add(additive_inverse(multiply(multiply(y,z),x)),add(multiply(y,multiply(x,z)),multiply(y,multiply(z,x)))),x))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_10,c_11516]) ).

cnf(c_11518,plain,
    add(add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(y,x),multiply(x,z))))),additive_inverse(multiply(add(additive_inverse(multiply(multiply(y,z),x)),add(multiply(y,multiply(x,z)),multiply(y,multiply(z,x)))),x))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_12,c_11517]) ).

cnf(c_11519,plain,
    add(add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(y,x),multiply(x,z))))),additive_inverse(multiply(add(add(multiply(y,multiply(x,z)),multiply(y,multiply(z,x))),additive_inverse(multiply(multiply(y,z),x))),x))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_10,c_11518]) ).

cnf(c_11520,plain,
    add(add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(y,x),multiply(x,z))))),additive_inverse(multiply(add(multiply(y,multiply(x,z)),add(multiply(y,multiply(z,x)),additive_inverse(multiply(multiply(y,z),x)))),x))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_12,c_11519]) ).

cnf(c_11521,plain,
    add(add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(y,x),multiply(x,z))))),additive_inverse(add(multiply(multiply(y,multiply(x,z)),x),multiply(add(multiply(y,multiply(z,x)),additive_inverse(multiply(multiply(y,z),x))),x)))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_9,c_11520]) ).

cnf(c_11522,plain,
    add(add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(y,x),multiply(x,z))))),additive_inverse(add(add(additive_inverse(multiply(multiply(y,x),multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),multiply(y,multiply(x,multiply(x,z))))),multiply(add(multiply(y,multiply(z,x)),additive_inverse(multiply(multiply(y,z),x))),x)))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_4670,c_11521]) ).

cnf(c_11523,plain,
    add(add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(y,x),multiply(x,z))))),additive_inverse(add(add(additive_inverse(multiply(multiply(y,x),multiply(x,z))),add(multiply(y,multiply(x,multiply(x,z))),multiply(y,multiply(x,multiply(z,x))))),multiply(add(multiply(y,multiply(z,x)),additive_inverse(multiply(multiply(y,z),x))),x)))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_10,c_11522]) ).

cnf(c_11524,plain,
    add(add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(y,x),multiply(x,z))))),additive_inverse(add(add(add(multiply(y,multiply(x,multiply(x,z))),multiply(y,multiply(x,multiply(z,x)))),additive_inverse(multiply(multiply(y,x),multiply(x,z)))),multiply(add(multiply(y,multiply(z,x)),additive_inverse(multiply(multiply(y,z),x))),x)))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_10,c_11523]) ).

cnf(c_11525,plain,
    add(add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(y,x),multiply(x,z))))),additive_inverse(add(add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(y,x),multiply(x,z))))),multiply(add(multiply(y,multiply(z,x)),additive_inverse(multiply(multiply(y,z),x))),x)))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_12,c_11524]) ).

cnf(c_11526,plain,
    add(add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(y,x),multiply(x,z))))),additive_inverse(add(add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(y,x),multiply(x,z))))),add(multiply(multiply(y,multiply(z,x)),x),multiply(additive_inverse(multiply(multiply(y,z),x)),x))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_9,c_11525]) ).

cnf(c_11527,plain,
    add(add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(y,x),multiply(x,z))))),additive_inverse(add(add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(y,x),multiply(x,z))))),add(add(additive_inverse(multiply(multiply(y,x),multiply(z,x))),add(multiply(y,multiply(z,multiply(x,x))),multiply(y,multiply(x,multiply(z,x))))),multiply(additive_inverse(multiply(multiply(y,z),x)),x))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_4600,c_11526]) ).

cnf(c_11528,plain,
    add(add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(y,x),multiply(x,z))))),additive_inverse(add(add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(y,x),multiply(x,z))))),add(add(additive_inverse(multiply(multiply(y,x),multiply(z,x))),add(multiply(y,multiply(x,multiply(z,x))),multiply(y,multiply(z,multiply(x,x))))),multiply(additive_inverse(multiply(multiply(y,z),x)),x))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_10,c_11527]) ).

cnf(c_11529,plain,
    add(add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(y,x),multiply(x,z))))),additive_inverse(add(add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(y,x),multiply(x,z))))),add(add(add(multiply(y,multiply(x,multiply(z,x))),multiply(y,multiply(z,multiply(x,x)))),additive_inverse(multiply(multiply(y,x),multiply(z,x)))),multiply(additive_inverse(multiply(multiply(y,z),x)),x))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_10,c_11528]) ).

cnf(c_11530,plain,
    add(add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(y,x),multiply(x,z))))),additive_inverse(add(add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(y,x),multiply(x,z))))),add(add(multiply(y,multiply(x,multiply(z,x))),add(multiply(y,multiply(z,multiply(x,x))),additive_inverse(multiply(multiply(y,x),multiply(z,x))))),multiply(additive_inverse(multiply(multiply(y,z),x)),x))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_12,c_11529]) ).

cnf(c_11531,plain,
    add(add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(y,x),multiply(x,z))))),additive_inverse(add(add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(y,x),multiply(x,z))))),add(add(multiply(y,multiply(x,multiply(z,x))),add(multiply(y,multiply(z,multiply(x,x))),additive_inverse(multiply(multiply(y,x),multiply(z,x))))),additive_inverse(multiply(multiply(multiply(y,z),x),x)))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_19,c_11530]) ).

cnf(c_11532,plain,
    add(add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(y,x),multiply(x,z))))),additive_inverse(add(add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(y,x),multiply(x,z))))),add(add(multiply(y,multiply(x,multiply(z,x))),add(multiply(y,multiply(z,multiply(x,x))),additive_inverse(multiply(multiply(y,x),multiply(z,x))))),additive_inverse(multiply(multiply(y,z),multiply(x,x))))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_13,c_11531]) ).

cnf(c_11533,plain,
    add(add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(y,x),multiply(x,z))))),additive_inverse(add(add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(y,x),multiply(x,z))))),add(multiply(y,multiply(x,multiply(z,x))),add(add(multiply(y,multiply(z,multiply(x,x))),additive_inverse(multiply(multiply(y,x),multiply(z,x)))),additive_inverse(multiply(multiply(y,z),multiply(x,x)))))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_12,c_11532]) ).

cnf(c_11534,plain,
    add(add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(y,x),multiply(x,z))))),additive_inverse(add(add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(y,x),multiply(x,z))))),add(multiply(y,multiply(x,multiply(z,x))),add(multiply(y,multiply(z,multiply(x,x))),add(additive_inverse(multiply(multiply(y,x),multiply(z,x))),additive_inverse(multiply(multiply(y,z),multiply(x,x))))))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_12,c_11533]) ).

cnf(c_11535,plain,
    add(add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(y,x),multiply(x,z))))),additive_inverse(add(multiply(y,multiply(x,multiply(z,x))),add(add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(y,x),multiply(x,z))))),add(multiply(y,multiply(z,multiply(x,x))),add(additive_inverse(multiply(multiply(y,x),multiply(z,x))),additive_inverse(multiply(multiply(y,z),multiply(x,x))))))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_33,c_11534]) ).

cnf(c_11536,plain,
    add(add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(y,x),multiply(x,z))))),additive_inverse(add(multiply(y,multiply(x,multiply(z,x))),add(multiply(y,multiply(z,multiply(x,x))),add(add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(y,x),multiply(x,z))))),add(additive_inverse(multiply(multiply(y,x),multiply(z,x))),additive_inverse(multiply(multiply(y,z),multiply(x,x))))))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_33,c_11535]) ).

cnf(c_11537,plain,
    add(add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(y,x),multiply(x,z))))),additive_inverse(add(multiply(y,multiply(x,multiply(z,x))),add(multiply(y,multiply(z,multiply(x,x))),add(multiply(y,multiply(x,multiply(x,z))),add(add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(y,x),multiply(x,z)))),add(additive_inverse(multiply(multiply(y,x),multiply(z,x))),additive_inverse(multiply(multiply(y,z),multiply(x,x)))))))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_12,c_11536]) ).

cnf(c_11538,plain,
    add(add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(y,x),multiply(x,z))))),additive_inverse(add(multiply(y,multiply(x,multiply(z,x))),add(multiply(y,multiply(z,multiply(x,x))),add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),add(additive_inverse(multiply(multiply(y,x),multiply(x,z))),add(additive_inverse(multiply(multiply(y,x),multiply(z,x))),additive_inverse(multiply(multiply(y,z),multiply(x,x))))))))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_12,c_11537]) ).

cnf(c_11539,plain,
    add(add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(y,x),multiply(x,z))))),additive_inverse(add(multiply(y,multiply(x,multiply(z,x))),add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(z,multiply(x,x))),add(multiply(y,multiply(x,multiply(z,x))),add(additive_inverse(multiply(multiply(y,x),multiply(x,z))),add(additive_inverse(multiply(multiply(y,x),multiply(z,x))),additive_inverse(multiply(multiply(y,z),multiply(x,x))))))))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_33,c_11538]) ).

cnf(c_11540,plain,
    add(add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(y,x),multiply(x,z))))),additive_inverse(add(multiply(y,multiply(x,multiply(z,x))),add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),add(multiply(y,multiply(z,multiply(x,x))),add(additive_inverse(multiply(multiply(y,x),multiply(x,z))),add(additive_inverse(multiply(multiply(y,x),multiply(z,x))),additive_inverse(multiply(multiply(y,z),multiply(x,x))))))))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_33,c_11539]) ).

cnf(c_11541,plain,
    add(add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(y,x),multiply(x,z))))),additive_inverse(add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),add(multiply(y,multiply(x,multiply(z,x))),add(multiply(y,multiply(z,multiply(x,x))),add(additive_inverse(multiply(multiply(y,x),multiply(x,z))),add(additive_inverse(multiply(multiply(y,x),multiply(z,x))),additive_inverse(multiply(multiply(y,z),multiply(x,x))))))))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_33,c_11540]) ).

cnf(c_11542,plain,
    add(add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(y,x),multiply(x,z))))),add(additive_inverse(add(multiply(y,multiply(x,multiply(z,x))),add(multiply(y,multiply(x,multiply(z,x))),add(multiply(y,multiply(z,multiply(x,x))),add(additive_inverse(multiply(multiply(y,x),multiply(x,z))),add(additive_inverse(multiply(multiply(y,x),multiply(z,x))),additive_inverse(multiply(multiply(y,z),multiply(x,x))))))))),additive_inverse(multiply(y,multiply(x,multiply(x,z)))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_73,c_11541]) ).

cnf(c_11543,plain,
    add(add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(y,x),multiply(x,z))))),add(add(additive_inverse(add(multiply(y,multiply(x,multiply(z,x))),add(multiply(y,multiply(z,multiply(x,x))),add(additive_inverse(multiply(multiply(y,x),multiply(x,z))),add(additive_inverse(multiply(multiply(y,x),multiply(z,x))),additive_inverse(multiply(multiply(y,z),multiply(x,x)))))))),additive_inverse(multiply(y,multiply(x,multiply(z,x))))),additive_inverse(multiply(y,multiply(x,multiply(x,z)))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_73,c_11542]) ).

cnf(c_11544,plain,
    add(add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(y,x),multiply(x,z))))),add(add(add(additive_inverse(add(multiply(y,multiply(z,multiply(x,x))),add(additive_inverse(multiply(multiply(y,x),multiply(x,z))),add(additive_inverse(multiply(multiply(y,x),multiply(z,x))),additive_inverse(multiply(multiply(y,z),multiply(x,x))))))),additive_inverse(multiply(y,multiply(x,multiply(z,x))))),additive_inverse(multiply(y,multiply(x,multiply(z,x))))),additive_inverse(multiply(y,multiply(x,multiply(x,z)))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_73,c_11543]) ).

cnf(c_11545,plain,
    add(add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(y,x),multiply(x,z))))),add(add(add(add(additive_inverse(add(additive_inverse(multiply(multiply(y,x),multiply(x,z))),add(additive_inverse(multiply(multiply(y,x),multiply(z,x))),additive_inverse(multiply(multiply(y,z),multiply(x,x)))))),additive_inverse(multiply(y,multiply(z,multiply(x,x))))),additive_inverse(multiply(y,multiply(x,multiply(z,x))))),additive_inverse(multiply(y,multiply(x,multiply(z,x))))),additive_inverse(multiply(y,multiply(x,multiply(x,z)))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_73,c_11544]) ).

cnf(c_11546,plain,
    add(add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(y,x),multiply(x,z))))),add(add(add(add(add(additive_inverse(add(additive_inverse(multiply(multiply(y,x),multiply(z,x))),additive_inverse(multiply(multiply(y,z),multiply(x,x))))),additive_inverse(additive_inverse(multiply(multiply(y,x),multiply(x,z))))),additive_inverse(multiply(y,multiply(z,multiply(x,x))))),additive_inverse(multiply(y,multiply(x,multiply(z,x))))),additive_inverse(multiply(y,multiply(x,multiply(z,x))))),additive_inverse(multiply(y,multiply(x,multiply(x,z)))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_73,c_11545]) ).

cnf(c_11547,plain,
    add(add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(y,x),multiply(x,z))))),add(add(add(add(add(add(additive_inverse(additive_inverse(multiply(multiply(y,z),multiply(x,x)))),additive_inverse(additive_inverse(multiply(multiply(y,x),multiply(z,x))))),additive_inverse(additive_inverse(multiply(multiply(y,x),multiply(x,z))))),additive_inverse(multiply(y,multiply(z,multiply(x,x))))),additive_inverse(multiply(y,multiply(x,multiply(z,x))))),additive_inverse(multiply(y,multiply(x,multiply(z,x))))),additive_inverse(multiply(y,multiply(x,multiply(x,z)))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_73,c_11546]) ).

cnf(c_11548,plain,
    add(add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(y,x),multiply(x,z))))),add(add(add(add(add(add(multiply(multiply(y,z),multiply(x,x)),additive_inverse(additive_inverse(multiply(multiply(y,x),multiply(z,x))))),additive_inverse(additive_inverse(multiply(multiply(y,x),multiply(x,z))))),additive_inverse(multiply(y,multiply(z,multiply(x,x))))),additive_inverse(multiply(y,multiply(x,multiply(z,x))))),additive_inverse(multiply(y,multiply(x,multiply(z,x))))),additive_inverse(multiply(y,multiply(x,multiply(x,z)))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_7,c_11547]) ).

cnf(c_11549,plain,
    add(add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(y,x),multiply(x,z))))),add(add(add(add(add(add(multiply(multiply(y,z),multiply(x,x)),multiply(multiply(y,x),multiply(z,x))),additive_inverse(additive_inverse(multiply(multiply(y,x),multiply(x,z))))),additive_inverse(multiply(y,multiply(z,multiply(x,x))))),additive_inverse(multiply(y,multiply(x,multiply(z,x))))),additive_inverse(multiply(y,multiply(x,multiply(z,x))))),additive_inverse(multiply(y,multiply(x,multiply(x,z)))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_7,c_11548]) ).

cnf(c_11550,plain,
    add(add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(y,x),multiply(x,z))))),add(add(add(add(add(add(multiply(multiply(y,x),multiply(z,x)),multiply(multiply(y,z),multiply(x,x))),additive_inverse(additive_inverse(multiply(multiply(y,x),multiply(x,z))))),additive_inverse(multiply(y,multiply(z,multiply(x,x))))),additive_inverse(multiply(y,multiply(x,multiply(z,x))))),additive_inverse(multiply(y,multiply(x,multiply(z,x))))),additive_inverse(multiply(y,multiply(x,multiply(x,z)))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_10,c_11549]) ).

cnf(c_11551,plain,
    add(add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(y,x),multiply(x,z))))),add(add(add(add(add(add(multiply(multiply(y,x),multiply(z,x)),multiply(multiply(y,z),multiply(x,x))),multiply(multiply(y,x),multiply(x,z))),additive_inverse(multiply(y,multiply(z,multiply(x,x))))),additive_inverse(multiply(y,multiply(x,multiply(z,x))))),additive_inverse(multiply(y,multiply(x,multiply(z,x))))),additive_inverse(multiply(y,multiply(x,multiply(x,z)))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_7,c_11550]) ).

cnf(c_11552,plain,
    add(add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(y,x),multiply(x,z))))),add(add(add(add(add(multiply(multiply(y,x),multiply(x,z)),add(multiply(multiply(y,x),multiply(z,x)),multiply(multiply(y,z),multiply(x,x)))),additive_inverse(multiply(y,multiply(z,multiply(x,x))))),additive_inverse(multiply(y,multiply(x,multiply(z,x))))),additive_inverse(multiply(y,multiply(x,multiply(z,x))))),additive_inverse(multiply(y,multiply(x,multiply(x,z)))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_10,c_11551]) ).

cnf(c_11553,plain,
    add(add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(y,x),multiply(x,z))))),add(add(add(add(additive_inverse(multiply(y,multiply(z,multiply(x,x)))),add(multiply(multiply(y,x),multiply(x,z)),add(multiply(multiply(y,x),multiply(z,x)),multiply(multiply(y,z),multiply(x,x))))),additive_inverse(multiply(y,multiply(x,multiply(z,x))))),additive_inverse(multiply(y,multiply(x,multiply(z,x))))),additive_inverse(multiply(y,multiply(x,multiply(x,z)))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_10,c_11552]) ).

cnf(c_11554,plain,
    add(add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(y,x),multiply(x,z))))),add(add(add(additive_inverse(multiply(y,multiply(x,multiply(z,x)))),add(additive_inverse(multiply(y,multiply(z,multiply(x,x)))),add(multiply(multiply(y,x),multiply(x,z)),add(multiply(multiply(y,x),multiply(z,x)),multiply(multiply(y,z),multiply(x,x)))))),additive_inverse(multiply(y,multiply(x,multiply(z,x))))),additive_inverse(multiply(y,multiply(x,multiply(x,z)))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_10,c_11553]) ).

cnf(c_11555,plain,
    add(add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(y,x),multiply(x,z))))),add(add(additive_inverse(multiply(y,multiply(x,multiply(z,x)))),add(additive_inverse(multiply(y,multiply(x,multiply(z,x)))),add(additive_inverse(multiply(y,multiply(z,multiply(x,x)))),add(multiply(multiply(y,x),multiply(x,z)),add(multiply(multiply(y,x),multiply(z,x)),multiply(multiply(y,z),multiply(x,x))))))),additive_inverse(multiply(y,multiply(x,multiply(x,z)))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_10,c_11554]) ).

cnf(c_11556,plain,
    add(add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(y,x),multiply(x,z))))),add(additive_inverse(multiply(y,multiply(x,multiply(x,z)))),add(additive_inverse(multiply(y,multiply(x,multiply(z,x)))),add(additive_inverse(multiply(y,multiply(x,multiply(z,x)))),add(additive_inverse(multiply(y,multiply(z,multiply(x,x)))),add(multiply(multiply(y,x),multiply(x,z)),add(multiply(multiply(y,x),multiply(z,x)),multiply(multiply(y,z),multiply(x,x))))))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_10,c_11555]) ).

cnf(c_11557,plain,
    add(additive_inverse(multiply(y,multiply(x,multiply(x,z)))),add(add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(y,x),multiply(x,z))))),add(additive_inverse(multiply(y,multiply(x,multiply(z,x)))),add(additive_inverse(multiply(y,multiply(x,multiply(z,x)))),add(additive_inverse(multiply(y,multiply(z,multiply(x,x)))),add(multiply(multiply(y,x),multiply(x,z)),add(multiply(multiply(y,x),multiply(z,x)),multiply(multiply(y,z),multiply(x,x))))))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_33,c_11556]) ).

cnf(c_11558,plain,
    add(additive_inverse(multiply(y,multiply(x,multiply(x,z)))),add(additive_inverse(multiply(y,multiply(x,multiply(z,x)))),add(add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(y,x),multiply(x,z))))),add(additive_inverse(multiply(y,multiply(x,multiply(z,x)))),add(additive_inverse(multiply(y,multiply(z,multiply(x,x)))),add(multiply(multiply(y,x),multiply(x,z)),add(multiply(multiply(y,x),multiply(z,x)),multiply(multiply(y,z),multiply(x,x))))))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_33,c_11557]) ).

cnf(c_11559,plain,
    add(additive_inverse(multiply(y,multiply(x,multiply(x,z)))),add(additive_inverse(multiply(y,multiply(x,multiply(z,x)))),add(additive_inverse(multiply(y,multiply(x,multiply(z,x)))),add(add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(y,x),multiply(x,z))))),add(additive_inverse(multiply(y,multiply(z,multiply(x,x)))),add(multiply(multiply(y,x),multiply(x,z)),add(multiply(multiply(y,x),multiply(z,x)),multiply(multiply(y,z),multiply(x,x))))))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_33,c_11558]) ).

cnf(c_11560,plain,
    add(additive_inverse(multiply(y,multiply(x,multiply(x,z)))),add(additive_inverse(multiply(y,multiply(x,multiply(z,x)))),add(additive_inverse(multiply(y,multiply(x,multiply(z,x)))),add(additive_inverse(multiply(y,multiply(z,multiply(x,x)))),add(add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(y,x),multiply(x,z))))),add(multiply(multiply(y,x),multiply(x,z)),add(multiply(multiply(y,x),multiply(z,x)),multiply(multiply(y,z),multiply(x,x))))))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_33,c_11559]) ).

cnf(c_11561,plain,
    add(additive_inverse(multiply(y,multiply(x,multiply(x,z)))),add(additive_inverse(multiply(y,multiply(x,multiply(z,x)))),add(additive_inverse(multiply(y,multiply(x,multiply(z,x)))),add(additive_inverse(multiply(y,multiply(z,multiply(x,x)))),add(multiply(multiply(y,x),multiply(x,z)),add(add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(y,x),multiply(x,z))))),add(multiply(multiply(y,x),multiply(z,x)),multiply(multiply(y,z),multiply(x,x))))))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_33,c_11560]) ).

cnf(c_11562,plain,
    add(additive_inverse(multiply(y,multiply(x,multiply(x,z)))),add(additive_inverse(multiply(y,multiply(x,multiply(z,x)))),add(additive_inverse(multiply(y,multiply(x,multiply(z,x)))),add(additive_inverse(multiply(y,multiply(z,multiply(x,x)))),add(multiply(multiply(y,x),multiply(x,z)),add(multiply(y,multiply(x,multiply(x,z))),add(add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(y,x),multiply(x,z)))),add(multiply(multiply(y,x),multiply(z,x)),multiply(multiply(y,z),multiply(x,x)))))))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_12,c_11561]) ).

cnf(c_11563,plain,
    add(additive_inverse(multiply(y,multiply(x,multiply(x,z)))),add(additive_inverse(multiply(y,multiply(x,multiply(z,x)))),add(additive_inverse(multiply(y,multiply(x,multiply(z,x)))),add(additive_inverse(multiply(y,multiply(z,multiply(x,x)))),add(multiply(multiply(y,x),multiply(x,z)),add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),add(additive_inverse(multiply(multiply(y,x),multiply(x,z))),add(multiply(multiply(y,x),multiply(z,x)),multiply(multiply(y,z),multiply(x,x))))))))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_12,c_11562]) ).

cnf(c_11564,plain,
    add(additive_inverse(multiply(y,multiply(x,multiply(x,z)))),add(additive_inverse(multiply(y,multiply(x,multiply(z,x)))),add(additive_inverse(multiply(y,multiply(x,multiply(z,x)))),add(additive_inverse(multiply(y,multiply(z,multiply(x,x)))),add(multiply(y,multiply(x,multiply(x,z))),add(multiply(multiply(y,x),multiply(x,z)),add(multiply(y,multiply(x,multiply(z,x))),add(additive_inverse(multiply(multiply(y,x),multiply(x,z))),add(multiply(multiply(y,x),multiply(z,x)),multiply(multiply(y,z),multiply(x,x))))))))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_33,c_11563]) ).

cnf(c_11565,plain,
    add(additive_inverse(multiply(y,multiply(x,multiply(x,z)))),add(additive_inverse(multiply(y,multiply(x,multiply(z,x)))),add(additive_inverse(multiply(y,multiply(x,multiply(z,x)))),add(additive_inverse(multiply(y,multiply(z,multiply(x,x)))),add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),add(multiply(multiply(y,x),multiply(x,z)),add(additive_inverse(multiply(multiply(y,x),multiply(x,z))),add(multiply(multiply(y,x),multiply(z,x)),multiply(multiply(y,z),multiply(x,x))))))))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_33,c_11564]) ).

cnf(c_11566,plain,
    add(additive_inverse(multiply(y,multiply(x,multiply(x,z)))),add(additive_inverse(multiply(y,multiply(x,multiply(z,x)))),add(additive_inverse(multiply(y,multiply(x,multiply(z,x)))),add(additive_inverse(multiply(y,multiply(z,multiply(x,x)))),add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),add(multiply(multiply(y,x),multiply(z,x)),multiply(multiply(y,z),multiply(x,x))))))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_31,c_11565]) ).

cnf(c_11567,plain,
    add(additive_inverse(multiply(y,multiply(x,multiply(x,z)))),add(additive_inverse(multiply(y,multiply(x,multiply(z,x)))),add(additive_inverse(multiply(y,multiply(x,multiply(z,x)))),add(multiply(y,multiply(x,multiply(x,z))),add(additive_inverse(multiply(y,multiply(z,multiply(x,x)))),add(multiply(y,multiply(x,multiply(z,x))),add(multiply(multiply(y,x),multiply(z,x)),multiply(multiply(y,z),multiply(x,x))))))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_33,c_11566]) ).

cnf(c_11568,plain,
    add(additive_inverse(multiply(y,multiply(x,multiply(x,z)))),add(additive_inverse(multiply(y,multiply(x,multiply(z,x)))),add(additive_inverse(multiply(y,multiply(x,multiply(z,x)))),add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),add(additive_inverse(multiply(y,multiply(z,multiply(x,x)))),add(multiply(multiply(y,x),multiply(z,x)),multiply(multiply(y,z),multiply(x,x))))))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_33,c_11567]) ).

cnf(c_11569,plain,
    add(additive_inverse(multiply(y,multiply(x,multiply(x,z)))),add(additive_inverse(multiply(y,multiply(x,multiply(z,x)))),add(multiply(y,multiply(x,multiply(x,z))),add(additive_inverse(multiply(y,multiply(x,multiply(z,x)))),add(multiply(y,multiply(x,multiply(z,x))),add(additive_inverse(multiply(y,multiply(z,multiply(x,x)))),add(multiply(multiply(y,x),multiply(z,x)),multiply(multiply(y,z),multiply(x,x))))))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_33,c_11568]) ).

cnf(c_11570,plain,
    add(additive_inverse(multiply(y,multiply(x,multiply(x,z)))),add(additive_inverse(multiply(y,multiply(x,multiply(z,x)))),add(multiply(y,multiply(x,multiply(x,z))),add(multiply(y,multiply(x,multiply(z,x))),add(additive_inverse(multiply(y,multiply(x,multiply(z,x)))),add(additive_inverse(multiply(y,multiply(z,multiply(x,x)))),add(multiply(multiply(y,x),multiply(z,x)),multiply(multiply(y,z),multiply(x,x))))))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_33,c_11569]) ).

cnf(c_11571,plain,
    add(additive_inverse(multiply(y,multiply(x,multiply(x,z)))),add(additive_inverse(multiply(y,multiply(x,multiply(z,x)))),add(multiply(y,multiply(x,multiply(x,z))),add(additive_inverse(multiply(y,multiply(z,multiply(x,x)))),add(multiply(multiply(y,x),multiply(z,x)),multiply(multiply(y,z),multiply(x,x))))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_31,c_11570]) ).

cnf(c_11572,plain,
    add(additive_inverse(multiply(y,multiply(x,multiply(x,z)))),add(multiply(y,multiply(x,multiply(x,z))),add(additive_inverse(multiply(y,multiply(x,multiply(z,x)))),add(additive_inverse(multiply(y,multiply(z,multiply(x,x)))),add(multiply(multiply(y,x),multiply(z,x)),multiply(multiply(y,z),multiply(x,x))))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_33,c_11571]) ).

cnf(c_11573,plain,
    add(multiply(y,multiply(x,multiply(x,z))),add(additive_inverse(multiply(y,multiply(x,multiply(x,z)))),add(additive_inverse(multiply(y,multiply(x,multiply(z,x)))),add(additive_inverse(multiply(y,multiply(z,multiply(x,x)))),add(multiply(multiply(y,x),multiply(z,x)),multiply(multiply(y,z),multiply(x,x))))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_33,c_11572]) ).

cnf(c_4773,plain,
    add(additive_inverse(multiply(y,multiply(x,multiply(z,x)))),add(additive_inverse(multiply(y,multiply(z,multiply(x,x)))),add(multiply(multiply(y,x),multiply(z,x)),multiply(multiply(y,z),multiply(x,x))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_31,c_11573]) ).

cnf(c_11574,plain,
    add(additive_inverse(multiply(y,multiply(x,multiply(z,x)))),add(additive_inverse(multiply(y,multiply(z,multiply(x,x)))),add(add(multiply(y,multiply(x,multiply(z,x))),add(multiply(x,multiply(y,multiply(z,x))),additive_inverse(multiply(multiply(x,y),multiply(z,x))))),multiply(multiply(y,z),multiply(x,x))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_763,c_4773]) ).

cnf(c_11575,plain,
    add(additive_inverse(multiply(y,multiply(x,multiply(z,x)))),add(additive_inverse(multiply(y,multiply(z,multiply(x,x)))),add(add(multiply(x,multiply(y,multiply(z,x))),add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(x,y),multiply(z,x))))),multiply(multiply(y,z),multiply(x,x))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_33,c_11574]) ).

cnf(c_11576,plain,
    add(additive_inverse(multiply(y,multiply(x,multiply(z,x)))),add(additive_inverse(multiply(y,multiply(z,multiply(x,x)))),add(multiply(x,multiply(y,multiply(z,x))),add(add(multiply(y,multiply(x,multiply(z,x))),additive_inverse(multiply(multiply(x,y),multiply(z,x)))),multiply(multiply(y,z),multiply(x,x)))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_12,c_11575]) ).

cnf(c_11577,plain,
    add(additive_inverse(multiply(y,multiply(x,multiply(z,x)))),add(additive_inverse(multiply(y,multiply(z,multiply(x,x)))),add(multiply(x,multiply(y,multiply(z,x))),add(multiply(y,multiply(x,multiply(z,x))),add(additive_inverse(multiply(multiply(x,y),multiply(z,x))),multiply(multiply(y,z),multiply(x,x))))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_12,c_11576]) ).

cnf(c_11578,plain,
    add(additive_inverse(multiply(y,multiply(x,multiply(z,x)))),add(multiply(x,multiply(y,multiply(z,x))),add(additive_inverse(multiply(y,multiply(z,multiply(x,x)))),add(multiply(y,multiply(x,multiply(z,x))),add(additive_inverse(multiply(multiply(x,y),multiply(z,x))),multiply(multiply(y,z),multiply(x,x))))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_33,c_11577]) ).

cnf(c_11579,plain,
    add(additive_inverse(multiply(y,multiply(x,multiply(z,x)))),add(multiply(x,multiply(y,multiply(z,x))),add(multiply(y,multiply(x,multiply(z,x))),add(additive_inverse(multiply(y,multiply(z,multiply(x,x)))),add(additive_inverse(multiply(multiply(x,y),multiply(z,x))),multiply(multiply(y,z),multiply(x,x))))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_33,c_11578]) ).

cnf(c_11580,plain,
    add(multiply(x,multiply(y,multiply(z,x))),add(additive_inverse(multiply(y,multiply(x,multiply(z,x)))),add(multiply(y,multiply(x,multiply(z,x))),add(additive_inverse(multiply(y,multiply(z,multiply(x,x)))),add(additive_inverse(multiply(multiply(x,y),multiply(z,x))),multiply(multiply(y,z),multiply(x,x))))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_33,c_11579]) ).

cnf(c_11581,plain,
    add(multiply(x,multiply(y,multiply(z,x))),add(multiply(y,multiply(x,multiply(z,x))),add(additive_inverse(multiply(y,multiply(x,multiply(z,x)))),add(additive_inverse(multiply(y,multiply(z,multiply(x,x)))),add(additive_inverse(multiply(multiply(x,y),multiply(z,x))),multiply(multiply(y,z),multiply(x,x))))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_33,c_11580]) ).

cnf(c_6380,plain,
    add(multiply(x,multiply(y,multiply(z,x))),add(additive_inverse(multiply(y,multiply(z,multiply(x,x)))),add(additive_inverse(multiply(multiply(x,y),multiply(z,x))),multiply(multiply(y,z),multiply(x,x))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_31,c_11581]) ).

cnf(c_11582,plain,
    add(multiply(x,multiply(y,multiply(z,x))),add(additive_inverse(multiply(y,multiply(z,multiply(x,x)))),add(additive_inverse(multiply(multiply(x,y),multiply(z,x))),add(multiply(y,multiply(z,multiply(x,x))),add(multiply(z,multiply(y,multiply(x,x))),additive_inverse(multiply(multiply(z,y),multiply(x,x)))))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_763,c_6380]) ).

cnf(c_11583,plain,
    add(multiply(x,multiply(y,multiply(z,x))),add(additive_inverse(multiply(y,multiply(z,multiply(x,x)))),add(multiply(y,multiply(z,multiply(x,x))),add(additive_inverse(multiply(multiply(x,y),multiply(z,x))),add(multiply(z,multiply(y,multiply(x,x))),additive_inverse(multiply(multiply(z,y),multiply(x,x)))))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_33,c_11582]) ).

cnf(c_11584,plain,
    add(multiply(x,multiply(y,multiply(z,x))),add(additive_inverse(multiply(y,multiply(z,multiply(x,x)))),add(multiply(y,multiply(z,multiply(x,x))),add(multiply(z,multiply(y,multiply(x,x))),add(additive_inverse(multiply(multiply(x,y),multiply(z,x))),additive_inverse(multiply(multiply(z,y),multiply(x,x)))))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_33,c_11583]) ).

cnf(c_11585,plain,
    add(multiply(x,multiply(y,multiply(z,x))),add(multiply(y,multiply(z,multiply(x,x))),add(additive_inverse(multiply(y,multiply(z,multiply(x,x)))),add(multiply(z,multiply(y,multiply(x,x))),add(additive_inverse(multiply(multiply(x,y),multiply(z,x))),additive_inverse(multiply(multiply(z,y),multiply(x,x)))))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_33,c_11584]) ).

cnf(c_7690,plain,
    add(multiply(x,multiply(y,multiply(z,x))),add(multiply(z,multiply(y,multiply(x,x))),add(additive_inverse(multiply(multiply(x,y),multiply(z,x))),additive_inverse(multiply(multiply(z,y),multiply(x,x)))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_31,c_11585]) ).

cnf(c_11586,plain,
    add(multiply(x,multiply(y,multiply(z,x))),add(multiply(z,multiply(y,multiply(x,x))),add(additive_inverse(add(additive_inverse(multiply(multiply(x,multiply(z,x)),y)),add(multiply(x,multiply(y,multiply(z,x))),multiply(x,multiply(multiply(z,x),y))))),additive_inverse(multiply(multiply(z,y),multiply(x,x)))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_3577,c_7690]) ).

cnf(c_11587,plain,
    add(multiply(x,multiply(y,multiply(z,x))),add(multiply(z,multiply(y,multiply(x,x))),add(additive_inverse(add(add(multiply(x,multiply(y,multiply(z,x))),multiply(x,multiply(multiply(z,x),y))),additive_inverse(multiply(multiply(x,multiply(z,x)),y)))),additive_inverse(multiply(multiply(z,y),multiply(x,x)))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_10,c_11586]) ).

cnf(c_11588,plain,
    add(multiply(x,multiply(y,multiply(z,x))),add(multiply(z,multiply(y,multiply(x,x))),add(additive_inverse(add(multiply(x,multiply(y,multiply(z,x))),add(multiply(x,multiply(multiply(z,x),y)),additive_inverse(multiply(multiply(x,multiply(z,x)),y))))),additive_inverse(multiply(multiply(z,y),multiply(x,x)))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_12,c_11587]) ).

cnf(c_11589,plain,
    add(multiply(x,multiply(y,multiply(z,x))),add(multiply(z,multiply(y,multiply(x,x))),add(add(additive_inverse(add(multiply(x,multiply(multiply(z,x),y)),additive_inverse(multiply(multiply(x,multiply(z,x)),y)))),additive_inverse(multiply(x,multiply(y,multiply(z,x))))),additive_inverse(multiply(multiply(z,y),multiply(x,x)))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_73,c_11588]) ).

cnf(c_11590,plain,
    add(multiply(x,multiply(y,multiply(z,x))),add(multiply(z,multiply(y,multiply(x,x))),add(add(add(additive_inverse(additive_inverse(multiply(multiply(x,multiply(z,x)),y))),additive_inverse(multiply(x,multiply(multiply(z,x),y)))),additive_inverse(multiply(x,multiply(y,multiply(z,x))))),additive_inverse(multiply(multiply(z,y),multiply(x,x)))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_73,c_11589]) ).

cnf(c_11591,plain,
    add(multiply(x,multiply(y,multiply(z,x))),add(multiply(z,multiply(y,multiply(x,x))),add(add(add(multiply(multiply(x,multiply(z,x)),y),additive_inverse(multiply(x,multiply(multiply(z,x),y)))),additive_inverse(multiply(x,multiply(y,multiply(z,x))))),additive_inverse(multiply(multiply(z,y),multiply(x,x)))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_7,c_11590]) ).

cnf(c_11592,plain,
    add(multiply(x,multiply(y,multiply(z,x))),add(multiply(z,multiply(y,multiply(x,x))),add(add(add(additive_inverse(multiply(x,multiply(multiply(z,x),y))),multiply(multiply(x,multiply(z,x)),y)),additive_inverse(multiply(x,multiply(y,multiply(z,x))))),additive_inverse(multiply(multiply(z,y),multiply(x,x)))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_10,c_11591]) ).

cnf(c_11593,plain,
    add(multiply(x,multiply(y,multiply(z,x))),add(multiply(z,multiply(y,multiply(x,x))),add(add(additive_inverse(multiply(x,multiply(y,multiply(z,x)))),add(additive_inverse(multiply(x,multiply(multiply(z,x),y))),multiply(multiply(x,multiply(z,x)),y))),additive_inverse(multiply(multiply(z,y),multiply(x,x)))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_10,c_11592]) ).

cnf(c_11594,plain,
    add(multiply(x,multiply(y,multiply(z,x))),add(multiply(z,multiply(y,multiply(x,x))),add(additive_inverse(multiply(x,multiply(y,multiply(z,x)))),add(add(additive_inverse(multiply(x,multiply(multiply(z,x),y))),multiply(multiply(x,multiply(z,x)),y)),additive_inverse(multiply(multiply(z,y),multiply(x,x))))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_12,c_11593]) ).

cnf(c_11595,plain,
    add(multiply(x,multiply(y,multiply(z,x))),add(multiply(z,multiply(y,multiply(x,x))),add(additive_inverse(multiply(x,multiply(y,multiply(z,x)))),add(additive_inverse(multiply(x,multiply(multiply(z,x),y))),add(multiply(multiply(x,multiply(z,x)),y),additive_inverse(multiply(multiply(z,y),multiply(x,x)))))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_12,c_11594]) ).

cnf(c_11596,plain,
    add(multiply(x,multiply(y,multiply(z,x))),add(additive_inverse(multiply(x,multiply(y,multiply(z,x)))),add(multiply(z,multiply(y,multiply(x,x))),add(additive_inverse(multiply(x,multiply(multiply(z,x),y))),add(multiply(multiply(x,multiply(z,x)),y),additive_inverse(multiply(multiply(z,y),multiply(x,x)))))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_33,c_11595]) ).

cnf(c_9290,plain,
    add(multiply(z,multiply(y,multiply(x,x))),add(additive_inverse(multiply(x,multiply(multiply(z,x),y))),add(multiply(multiply(x,multiply(z,x)),y),additive_inverse(multiply(multiply(z,y),multiply(x,x)))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_31,c_11596]) ).

cnf(c_11597,plain,
    add(multiply(z,multiply(y,multiply(x,x))),add(additive_inverse(multiply(x,multiply(multiply(z,x),y))),add(multiply(multiply(x,multiply(z,x)),y),additive_inverse(add(additive_inverse(multiply(multiply(z,multiply(x,x)),y)),add(multiply(z,multiply(y,multiply(x,x))),multiply(z,multiply(multiply(x,x),y)))))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_3577,c_9290]) ).

cnf(c_11598,plain,
    add(multiply(z,multiply(y,multiply(x,x))),add(additive_inverse(multiply(x,multiply(multiply(z,x),y))),add(multiply(multiply(x,multiply(z,x)),y),additive_inverse(add(additive_inverse(multiply(multiply(z,multiply(x,x)),y)),add(multiply(z,multiply(y,multiply(x,x))),multiply(z,multiply(x,multiply(x,y))))))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_14,c_11597]) ).

cnf(c_11599,plain,
    add(multiply(z,multiply(y,multiply(x,x))),add(additive_inverse(multiply(x,multiply(multiply(z,x),y))),add(multiply(multiply(x,multiply(z,x)),y),additive_inverse(add(additive_inverse(multiply(multiply(z,multiply(x,x)),y)),add(multiply(z,multiply(x,multiply(x,y))),multiply(z,multiply(y,multiply(x,x))))))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_10,c_11598]) ).

cnf(c_11600,plain,
    add(multiply(z,multiply(y,multiply(x,x))),add(additive_inverse(multiply(x,multiply(multiply(z,x),y))),add(multiply(multiply(x,multiply(z,x)),y),additive_inverse(add(add(multiply(z,multiply(x,multiply(x,y))),multiply(z,multiply(y,multiply(x,x)))),additive_inverse(multiply(multiply(z,multiply(x,x)),y))))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_10,c_11599]) ).

cnf(c_11601,plain,
    add(multiply(z,multiply(y,multiply(x,x))),add(additive_inverse(multiply(x,multiply(multiply(z,x),y))),add(multiply(multiply(x,multiply(z,x)),y),additive_inverse(add(multiply(z,multiply(x,multiply(x,y))),add(multiply(z,multiply(y,multiply(x,x))),additive_inverse(multiply(multiply(z,multiply(x,x)),y)))))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_12,c_11600]) ).

cnf(c_11602,plain,
    add(multiply(z,multiply(y,multiply(x,x))),add(additive_inverse(multiply(x,multiply(multiply(z,x),y))),add(multiply(multiply(x,multiply(z,x)),y),add(additive_inverse(add(multiply(z,multiply(y,multiply(x,x))),additive_inverse(multiply(multiply(z,multiply(x,x)),y)))),additive_inverse(multiply(z,multiply(x,multiply(x,y)))))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_73,c_11601]) ).

cnf(c_11603,plain,
    add(multiply(z,multiply(y,multiply(x,x))),add(additive_inverse(multiply(x,multiply(multiply(z,x),y))),add(multiply(multiply(x,multiply(z,x)),y),add(add(additive_inverse(additive_inverse(multiply(multiply(z,multiply(x,x)),y))),additive_inverse(multiply(z,multiply(y,multiply(x,x))))),additive_inverse(multiply(z,multiply(x,multiply(x,y)))))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_73,c_11602]) ).

cnf(c_11604,plain,
    add(multiply(z,multiply(y,multiply(x,x))),add(additive_inverse(multiply(x,multiply(multiply(z,x),y))),add(multiply(multiply(x,multiply(z,x)),y),add(add(multiply(multiply(z,multiply(x,x)),y),additive_inverse(multiply(z,multiply(y,multiply(x,x))))),additive_inverse(multiply(z,multiply(x,multiply(x,y)))))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_7,c_11603]) ).

cnf(c_11605,plain,
    add(multiply(z,multiply(y,multiply(x,x))),add(additive_inverse(multiply(x,multiply(multiply(z,x),y))),add(multiply(multiply(x,multiply(z,x)),y),add(add(additive_inverse(multiply(z,multiply(y,multiply(x,x)))),multiply(multiply(z,multiply(x,x)),y)),additive_inverse(multiply(z,multiply(x,multiply(x,y)))))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_10,c_11604]) ).

cnf(c_11606,plain,
    add(multiply(z,multiply(y,multiply(x,x))),add(additive_inverse(multiply(x,multiply(multiply(z,x),y))),add(multiply(multiply(x,multiply(z,x)),y),add(additive_inverse(multiply(z,multiply(x,multiply(x,y)))),add(additive_inverse(multiply(z,multiply(y,multiply(x,x)))),multiply(multiply(z,multiply(x,x)),y)))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_10,c_11605]) ).

cnf(c_11607,plain,
    add(multiply(z,multiply(y,multiply(x,x))),add(additive_inverse(multiply(x,multiply(multiply(z,x),y))),add(additive_inverse(multiply(z,multiply(x,multiply(x,y)))),add(multiply(multiply(x,multiply(z,x)),y),add(additive_inverse(multiply(z,multiply(y,multiply(x,x)))),multiply(multiply(z,multiply(x,x)),y)))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_33,c_11606]) ).

cnf(c_11608,plain,
    add(multiply(z,multiply(y,multiply(x,x))),add(additive_inverse(multiply(x,multiply(multiply(z,x),y))),add(additive_inverse(multiply(z,multiply(x,multiply(x,y)))),add(additive_inverse(multiply(z,multiply(y,multiply(x,x)))),add(multiply(multiply(x,multiply(z,x)),y),multiply(multiply(z,multiply(x,x)),y)))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_33,c_11607]) ).

cnf(c_11609,plain,
    add(multiply(z,multiply(y,multiply(x,x))),add(additive_inverse(multiply(x,multiply(multiply(z,x),y))),add(additive_inverse(multiply(z,multiply(x,multiply(x,y)))),add(additive_inverse(multiply(z,multiply(y,multiply(x,x)))),add(multiply(x,multiply(multiply(z,x),y)),multiply(multiply(z,x),multiply(x,y))))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_835,c_11608]) ).

cnf(c_11610,plain,
    add(multiply(z,multiply(y,multiply(x,x))),add(additive_inverse(multiply(z,multiply(x,multiply(x,y)))),add(additive_inverse(multiply(x,multiply(multiply(z,x),y))),add(additive_inverse(multiply(z,multiply(y,multiply(x,x)))),add(multiply(x,multiply(multiply(z,x),y)),multiply(multiply(z,x),multiply(x,y))))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_33,c_11609]) ).

cnf(c_11611,plain,
    add(multiply(z,multiply(y,multiply(x,x))),add(additive_inverse(multiply(z,multiply(x,multiply(x,y)))),add(additive_inverse(multiply(z,multiply(y,multiply(x,x)))),add(additive_inverse(multiply(x,multiply(multiply(z,x),y))),add(multiply(x,multiply(multiply(z,x),y)),multiply(multiply(z,x),multiply(x,y))))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_33,c_11610]) ).

cnf(c_11612,plain,
    add(multiply(z,multiply(y,multiply(x,x))),add(additive_inverse(multiply(z,multiply(x,multiply(x,y)))),add(additive_inverse(multiply(z,multiply(y,multiply(x,x)))),add(multiply(x,multiply(multiply(z,x),y)),add(additive_inverse(multiply(x,multiply(multiply(z,x),y))),multiply(multiply(z,x),multiply(x,y))))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_33,c_11611]) ).

cnf(c_11613,plain,
    add(multiply(z,multiply(y,multiply(x,x))),add(additive_inverse(multiply(z,multiply(x,multiply(x,y)))),add(additive_inverse(multiply(z,multiply(y,multiply(x,x)))),multiply(multiply(z,x),multiply(x,y))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_31,c_11612]) ).

cnf(c_11614,plain,
    add(additive_inverse(multiply(z,multiply(x,multiply(x,y)))),add(multiply(z,multiply(y,multiply(x,x))),add(additive_inverse(multiply(z,multiply(y,multiply(x,x)))),multiply(multiply(z,x),multiply(x,y))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_33,c_11613]) ).

cnf(c_11436,plain,
    add(additive_inverse(multiply(z,multiply(x,multiply(x,y)))),multiply(multiply(z,x),multiply(x,y))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_31,c_11614]) ).

cnf(c_11615,plain,
    add(additive_inverse(multiply(z,multiply(x,multiply(x,y)))),add(multiply(z,multiply(x,multiply(x,y))),add(multiply(x,multiply(z,multiply(x,y))),additive_inverse(multiply(multiply(x,z),multiply(x,y)))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_763,c_11436]) ).

cnf(c_11616,plain,
    add(additive_inverse(multiply(z,multiply(x,multiply(x,y)))),add(multiply(x,multiply(z,multiply(x,y))),add(multiply(z,multiply(x,multiply(x,y))),additive_inverse(multiply(multiply(x,z),multiply(x,y)))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_33,c_11615]) ).

cnf(c_11617,plain,
    add(multiply(x,multiply(z,multiply(x,y))),add(additive_inverse(multiply(z,multiply(x,multiply(x,y)))),add(multiply(z,multiply(x,multiply(x,y))),additive_inverse(multiply(multiply(x,z),multiply(x,y)))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_33,c_11616]) ).

cnf(c_11618,plain,
    add(multiply(x,multiply(z,multiply(x,y))),add(multiply(z,multiply(x,multiply(x,y))),add(additive_inverse(multiply(z,multiply(x,multiply(x,y)))),additive_inverse(multiply(multiply(x,z),multiply(x,y)))))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_33,c_11617]) ).

cnf(c_11619,plain,
    add(multiply(x,multiply(z,multiply(x,y))),additive_inverse(multiply(multiply(x,z),multiply(x,y)))) != add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)),
    inference(paramod,[status(thm)],[c_31,c_11618]) ).

cnf(c_11439,plain,
    add(additive_inverse(multiply(x,multiply(multiply(x,y),z))),multiply(multiply(x,multiply(x,y)),z)) != add(multiply(x,multiply(z,multiply(x,y))),additive_inverse(multiply(multiply(x,z),multiply(x,y)))),
    inference(copy,[status(thm)],[c_11619]) ).

cnf(c_11440,plain,
    $false,
    inference(resolve,[status(thm)],[c_11439,c_4609]) ).

%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : RNG027-9 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04  % Command  : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36  % Computer : n026.cluster.edu
% 0.09/0.36  % Model    : x86_64 x86_64
% 0.09/0.36  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36  % Memory   : 8046.5625MB
% 0.09/0.36  % OS       : Linux 6.8.0-71-generic
% 0.09/0.36  % CPULimit : 300
% 0.09/0.36  % WCLimit  : 300
% 0.09/0.36  % DateTime : Sat Sep 26 05:50:40 UTC 2026
% 0.09/0.36  % CPUTime  : 
% 0.09/0.37  % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.37  % Process 224018 was started by sandbox on n026,
% 0.09/0.37  % Sat Sep 26 05:50:40 2026
% 0.09/0.37  % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.13/0.37  
% 0.13/0.37  % From the command line: assign(max_seconds, 300).
% 107.37/14.94  
% 107.37/14.94  % SZS status Unsatisfiable for theBenchmark
% 107.37/14.94  
% 107.37/14.94  % Proof 1 at 13.80 (+ 0.64) seconds.
% 107.37/14.94  % Length of proof is 48.
% 107.37/14.94  % Level of proof is 21.
% 107.37/14.94  % Maximum clause weight is 50.000.
% 107.37/14.94  % Given clauses 243.
% 107.37/14.94  
% 107.37/14.94  % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------