%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : RNG027-10 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n019.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:24 AM UTC 2026
% Result : Unsatisfiable 183.37s 38.85s
% Output : CNFRefutation 183.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 78
% Number of leaves : 16
% Syntax : Number of formulae : 163 ( 163 unt; 0 def)
% Number of atoms : 163 ( 162 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 72 ( 72 ~; 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 : 250 ( 0 sgn 33 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(left_additive_identity,axiom,
! [VAR_0] : add(additive_identity,VAR_0) = VAR_0,
file('theBenchmark.p',left_additive_identity) ).
cnf(c_2,plain,
add(additive_identity,A) = A,
inference(clausify,[status(thm)],[left_additive_identity]) ).
fof(add_inverse,axiom,
! [VAR_0] : add(additive_inverse(VAR_0),VAR_0) = additive_identity,
file('theBenchmark.p',add_inverse) ).
cnf(c_5,plain,
add(additive_inverse(A),A) = additive_identity,
inference(clausify,[status(thm)],[add_inverse]) ).
fof(sum_of_inverses,axiom,
! [VAR_0,VAR_1] : additive_inverse(add(VAR_0,VAR_1)) = add(additive_inverse(VAR_0),additive_inverse(VAR_1)),
file('theBenchmark.p',sum_of_inverses) ).
cnf(c_6,plain,
additive_inverse(add(A,B)) = add(additive_inverse(A),additive_inverse(B)),
inference(clausify,[status(thm)],[sum_of_inverses]) ).
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(multiply_over_add1,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',multiply_over_add1) ).
cnf(c_8,plain,
multiply(A,add(B,C)) = add(multiply(A,B),multiply(A,C)),
inference(clausify,[status(thm)],[multiply_over_add1]) ).
fof(multiply_over_add2,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',multiply_over_add2) ).
cnf(c_9,plain,
multiply(add(A,B),C) = add(multiply(A,C),multiply(B,C)),
inference(clausify,[status(thm)],[multiply_over_add2]) ).
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_10,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_11,plain,
multiply(multiply(A,A),B) = multiply(A,multiply(A,B)),
inference(clausify,[status(thm)],[left_alternative]) ).
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_12,plain,
multiply(additive_inverse(A),B) = additive_inverse(multiply(A,B)),
inference(clausify,[status(thm)],[inverse_product1]) ).
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_15,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_16,plain,
add(A,add(B,C)) = add(add(A,B),C),
inference(clausify,[status(thm)],[associativity_for_addition]) ).
cnf(c_17,plain,
add(add(A,B),C) = add(A,add(B,C)),
inference(copy,[status(thm)],[c_16]) ).
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_20,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_21,plain,
associator(A,B,C) = add(additive_inverse(multiply(A,multiply(B,C))),multiply(multiply(A,B),C)),
inference(paramod,[status(thm)],[c_15,c_20]) ).
fof(middle_law,axiom,
! [VAR_0,VAR_1] : multiply(multiply(VAR_0,VAR_1),VAR_0) = multiply(VAR_0,multiply(VAR_1,VAR_0)),
file('theBenchmark.p',middle_law) ).
cnf(c_22,plain,
multiply(multiply(A,B),A) = multiply(A,multiply(B,A)),
inference(clausify,[status(thm)],[middle_law]) ).
fof(associator_skew_symmetry1,axiom,
! [VAR_0,VAR_1,VAR_2] : associator(VAR_0,VAR_1,VAR_2) = additive_inverse(associator(VAR_1,VAR_0,VAR_2)),
file('theBenchmark.p',associator_skew_symmetry1) ).
cnf(c_23,plain,
associator(A,B,C) = additive_inverse(associator(B,A,C)),
inference(clausify,[status(thm)],[associator_skew_symmetry1]) ).
cnf(c_27800,plain,
add(additive_inverse(multiply(A,multiply(B,C))),multiply(multiply(A,B),C)) = additive_inverse(associator(B,A,C)),
inference(paramod,[status(thm)],[c_21,c_23]) ).
cnf(c_27801,plain,
add(additive_inverse(multiply(A,multiply(B,C))),multiply(multiply(A,B),C)) = additive_inverse(add(additive_inverse(multiply(B,multiply(A,C))),multiply(multiply(B,A),C))),
inference(paramod,[status(thm)],[c_21,c_27800]) ).
cnf(c_27802,plain,
add(additive_inverse(multiply(A,multiply(B,C))),multiply(multiply(A,B),C)) = add(additive_inverse(additive_inverse(multiply(B,multiply(A,C)))),additive_inverse(multiply(multiply(B,A),C))),
inference(paramod,[status(thm)],[c_6,c_27801]) ).
cnf(c_24,plain,
add(additive_inverse(multiply(A,multiply(B,C))),multiply(multiply(A,B),C)) = add(multiply(B,multiply(A,C)),additive_inverse(multiply(multiply(B,A),C))),
inference(paramod,[status(thm)],[c_7,c_27802]) ).
fof(associator_skew_symmetry2,axiom,
! [VAR_0,VAR_1,VAR_2] : associator(VAR_0,VAR_1,VAR_2) = additive_inverse(associator(VAR_2,VAR_1,VAR_0)),
file('theBenchmark.p',associator_skew_symmetry2) ).
cnf(c_25,plain,
associator(A,B,C) = additive_inverse(associator(C,B,A)),
inference(clausify,[status(thm)],[associator_skew_symmetry2]) ).
cnf(c_27803,plain,
add(additive_inverse(multiply(A,multiply(B,C))),multiply(multiply(A,B),C)) = additive_inverse(associator(C,B,A)),
inference(paramod,[status(thm)],[c_21,c_25]) ).
cnf(c_27804,plain,
add(additive_inverse(multiply(A,multiply(B,C))),multiply(multiply(A,B),C)) = additive_inverse(add(additive_inverse(multiply(C,multiply(B,A))),multiply(multiply(C,B),A))),
inference(paramod,[status(thm)],[c_21,c_27803]) ).
cnf(c_27805,plain,
add(additive_inverse(multiply(A,multiply(B,C))),multiply(multiply(A,B),C)) = add(additive_inverse(additive_inverse(multiply(C,multiply(B,A)))),additive_inverse(multiply(multiply(C,B),A))),
inference(paramod,[status(thm)],[c_6,c_27804]) ).
cnf(c_26,plain,
add(additive_inverse(multiply(A,multiply(B,C))),multiply(multiply(A,B),C)) = add(multiply(C,multiply(B,A)),additive_inverse(multiply(multiply(C,B),A))),
inference(paramod,[status(thm)],[c_7,c_27805]) ).
fof(prove_right_moufang,axiom,
multiply(cz,multiply(cx,multiply(cy,cx))) != multiply(multiply(multiply(cz,cx),cy),cx),
file('theBenchmark.p',prove_right_moufang) ).
cnf(c_27,plain,
multiply(cz,multiply(cx,multiply(cy,cx))) != multiply(multiply(multiply(cz,cx),cy),cx),
inference(clausify,[status(thm)],[prove_right_moufang]) ).
cnf(c_28,plain,
multiply(multiply(multiply(cz,cx),cy),cx) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(copy,[status(thm)],[c_27]) ).
cnf(c_29,plain,
add(A,additive_inverse(A)) = additive_identity,
inference(paramod,[status(thm)],[c_15,c_5]) ).
cnf(c_27806,plain,
add(add(A,B),C) = add(B,add(A,C)),
inference(paramod,[status(thm)],[c_15,c_17]) ).
cnf(c_40,plain,
add(A,add(B,C)) = add(B,add(A,C)),
inference(paramod,[status(thm)],[c_17,c_27806]) ).
cnf(c_27807,plain,
multiply(multiply(A,multiply(B,A)),A) = multiply(multiply(A,B),multiply(A,A)),
inference(paramod,[status(thm)],[c_22,c_10]) ).
cnf(c_27808,plain,
multiply(A,multiply(multiply(B,A),A)) = multiply(multiply(A,B),multiply(A,A)),
inference(paramod,[status(thm)],[c_22,c_27807]) ).
cnf(c_27809,plain,
multiply(A,multiply(B,multiply(A,A))) = multiply(multiply(A,B),multiply(A,A)),
inference(paramod,[status(thm)],[c_10,c_27808]) ).
cnf(c_53,plain,
multiply(multiply(A,B),multiply(A,A)) = multiply(A,multiply(B,multiply(A,A))),
inference(copy,[status(thm)],[c_27809]) ).
cnf(c_63,plain,
add(additive_inverse(multiply(multiply(A,B),multiply(B,C))),multiply(multiply(A,multiply(B,B)),C)) = add(multiply(B,multiply(multiply(A,B),C)),additive_inverse(multiply(multiply(B,multiply(A,B)),C))),
inference(paramod,[status(thm)],[c_10,c_24]) ).
cnf(c_27810,plain,
add(additive_inverse(multiply(A,multiply(add(B,C),D))),multiply(add(multiply(A,B),multiply(A,C)),D)) = add(multiply(D,multiply(add(B,C),A)),additive_inverse(multiply(multiply(D,add(B,C)),A))),
inference(paramod,[status(thm)],[c_8,c_26]) ).
cnf(c_27811,plain,
add(additive_inverse(multiply(A,add(multiply(B,D),multiply(C,D)))),multiply(add(multiply(A,B),multiply(A,C)),D)) = add(multiply(D,multiply(add(B,C),A)),additive_inverse(multiply(multiply(D,add(B,C)),A))),
inference(paramod,[status(thm)],[c_9,c_27810]) ).
cnf(c_27812,plain,
add(additive_inverse(add(multiply(A,multiply(B,D)),multiply(A,multiply(C,D)))),multiply(add(multiply(A,B),multiply(A,C)),D)) = add(multiply(D,multiply(add(B,C),A)),additive_inverse(multiply(multiply(D,add(B,C)),A))),
inference(paramod,[status(thm)],[c_8,c_27811]) ).
cnf(c_27813,plain,
add(add(additive_inverse(multiply(A,multiply(B,D))),additive_inverse(multiply(A,multiply(C,D)))),multiply(add(multiply(A,B),multiply(A,C)),D)) = add(multiply(D,multiply(add(B,C),A)),additive_inverse(multiply(multiply(D,add(B,C)),A))),
inference(paramod,[status(thm)],[c_6,c_27812]) ).
cnf(c_27814,plain,
add(add(additive_inverse(multiply(A,multiply(B,D))),additive_inverse(multiply(A,multiply(C,D)))),add(multiply(multiply(A,B),D),multiply(multiply(A,C),D))) = add(multiply(D,multiply(add(B,C),A)),additive_inverse(multiply(multiply(D,add(B,C)),A))),
inference(paramod,[status(thm)],[c_9,c_27813]) ).
cnf(c_27815,plain,
add(additive_inverse(multiply(A,multiply(B,D))),add(additive_inverse(multiply(A,multiply(C,D))),add(multiply(multiply(A,B),D),multiply(multiply(A,C),D)))) = add(multiply(D,multiply(add(B,C),A)),additive_inverse(multiply(multiply(D,add(B,C)),A))),
inference(paramod,[status(thm)],[c_17,c_27814]) ).
cnf(c_27816,plain,
add(additive_inverse(multiply(A,multiply(B,D))),add(additive_inverse(multiply(A,multiply(C,D))),add(multiply(multiply(A,B),D),multiply(multiply(A,C),D)))) = add(multiply(D,add(multiply(B,A),multiply(C,A))),additive_inverse(multiply(multiply(D,add(B,C)),A))),
inference(paramod,[status(thm)],[c_9,c_27815]) ).
cnf(c_27817,plain,
add(additive_inverse(multiply(A,multiply(B,D))),add(additive_inverse(multiply(A,multiply(C,D))),add(multiply(multiply(A,B),D),multiply(multiply(A,C),D)))) = add(add(multiply(D,multiply(B,A)),multiply(D,multiply(C,A))),additive_inverse(multiply(multiply(D,add(B,C)),A))),
inference(paramod,[status(thm)],[c_8,c_27816]) ).
cnf(c_27818,plain,
add(additive_inverse(multiply(A,multiply(B,D))),add(additive_inverse(multiply(A,multiply(C,D))),add(multiply(multiply(A,B),D),multiply(multiply(A,C),D)))) = add(add(multiply(D,multiply(B,A)),multiply(D,multiply(C,A))),additive_inverse(multiply(add(multiply(D,B),multiply(D,C)),A))),
inference(paramod,[status(thm)],[c_8,c_27817]) ).
cnf(c_27819,plain,
add(additive_inverse(multiply(A,multiply(B,D))),add(additive_inverse(multiply(A,multiply(C,D))),add(multiply(multiply(A,B),D),multiply(multiply(A,C),D)))) = add(add(multiply(D,multiply(B,A)),multiply(D,multiply(C,A))),additive_inverse(add(multiply(multiply(D,B),A),multiply(multiply(D,C),A)))),
inference(paramod,[status(thm)],[c_9,c_27818]) ).
cnf(c_27820,plain,
add(additive_inverse(multiply(A,multiply(B,D))),add(additive_inverse(multiply(A,multiply(C,D))),add(multiply(multiply(A,B),D),multiply(multiply(A,C),D)))) = add(add(multiply(D,multiply(B,A)),multiply(D,multiply(C,A))),add(additive_inverse(multiply(multiply(D,B),A)),additive_inverse(multiply(multiply(D,C),A)))),
inference(paramod,[status(thm)],[c_6,c_27819]) ).
cnf(c_87,plain,
add(additive_inverse(multiply(A,multiply(B,C))),add(additive_inverse(multiply(A,multiply(D,C))),add(multiply(multiply(A,B),C),multiply(multiply(A,D),C)))) = add(multiply(C,multiply(B,A)),add(multiply(C,multiply(D,A)),add(additive_inverse(multiply(multiply(C,B),A)),additive_inverse(multiply(multiply(C,D),A))))),
inference(paramod,[status(thm)],[c_17,c_27820]) ).
cnf(c_27821,plain,
add(add(multiply(A,multiply(B,C)),additive_inverse(multiply(multiply(A,B),C))),D) = add(additive_inverse(multiply(C,multiply(B,A))),add(multiply(multiply(C,B),A),D)),
inference(paramod,[status(thm)],[c_26,c_17]) ).
cnf(c_27822,plain,
add(multiply(A,multiply(B,C)),add(additive_inverse(multiply(multiply(A,B),C)),D)) = add(additive_inverse(multiply(C,multiply(B,A))),add(multiply(multiply(C,B),A),D)),
inference(paramod,[status(thm)],[c_17,c_27821]) ).
cnf(c_99,plain,
add(additive_inverse(multiply(A,multiply(B,C))),add(multiply(multiply(A,B),C),D)) = add(multiply(C,multiply(B,A)),add(additive_inverse(multiply(multiply(C,B),A)),D)),
inference(copy,[status(thm)],[c_27822]) ).
cnf(c_27823,plain,
add(multiply(A,multiply(B,C)),additive_inverse(multiply(multiply(A,B),C))) = add(multiply(B,multiply(C,A)),additive_inverse(multiply(multiply(B,C),A))),
inference(paramod,[status(thm)],[c_26,c_24]) ).
cnf(c_115,plain,
add(multiply(A,multiply(B,C)),additive_inverse(multiply(multiply(A,B),C))) = add(multiply(C,multiply(A,B)),additive_inverse(multiply(multiply(C,A),B))),
inference(copy,[status(thm)],[c_27823]) ).
cnf(c_27824,plain,
add(additive_identity,A) = add(B,add(additive_inverse(B),A)),
inference(paramod,[status(thm)],[c_29,c_17]) ).
cnf(c_27825,plain,
A = add(B,add(additive_inverse(B),A)),
inference(paramod,[status(thm)],[c_2,c_27824]) ).
cnf(c_120,plain,
add(A,add(additive_inverse(A),B)) = B,
inference(copy,[status(thm)],[c_27825]) ).
cnf(c_144,plain,
add(A,add(B,additive_inverse(A))) = B,
inference(paramod,[status(thm)],[c_15,c_120]) ).
cnf(c_27826,plain,
add(multiply(A,multiply(B,C)),add(multiply(B,multiply(A,C)),additive_inverse(multiply(multiply(B,A),C)))) = multiply(multiply(A,B),C),
inference(paramod,[status(thm)],[c_24,c_120]) ).
cnf(c_149,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_27826]) ).
cnf(c_27827,plain,
add(multiply(A,multiply(B,C)),add(multiply(C,multiply(B,A)),additive_inverse(multiply(multiply(C,B),A)))) = multiply(multiply(A,B),C),
inference(paramod,[status(thm)],[c_26,c_120]) ).
cnf(c_150,plain,
multiply(multiply(A,B),C) = add(multiply(A,multiply(B,C)),add(multiply(C,multiply(B,A)),additive_inverse(multiply(multiply(C,B),A)))),
inference(copy,[status(thm)],[c_27827]) ).
cnf(c_153,plain,
add(additive_inverse(A),add(B,A)) = B,
inference(paramod,[status(thm)],[c_7,c_144]) ).
cnf(c_155,plain,
add(A,add(B,add(C,additive_inverse(A)))) = add(B,C),
inference(paramod,[status(thm)],[c_17,c_144]) ).
cnf(c_27828,plain,
add(A,B) = add(additive_inverse(C),add(add(A,C),B)),
inference(paramod,[status(thm)],[c_153,c_17]) ).
cnf(c_27829,plain,
add(A,B) = add(additive_inverse(C),add(A,add(C,B))),
inference(paramod,[status(thm)],[c_17,c_27828]) ).
cnf(c_190,plain,
add(additive_inverse(A),add(B,add(A,C))) = add(B,C),
inference(copy,[status(thm)],[c_27829]) ).
cnf(c_27830,plain,
add(additive_inverse(multiply(A,multiply(A,multiply(A,B)))),add(additive_inverse(multiply(A,multiply(C,multiply(A,B)))),add(multiply(multiply(A,A),multiply(A,B)),multiply(multiply(A,C),multiply(A,B))))) = add(multiply(A,multiply(B,multiply(A,A))),add(multiply(multiply(A,B),multiply(C,A)),add(additive_inverse(multiply(multiply(multiply(A,B),A),A)),additive_inverse(multiply(multiply(multiply(A,B),C),A))))),
inference(paramod,[status(thm)],[c_53,c_87]) ).
cnf(c_27831,plain,
add(additive_inverse(multiply(A,multiply(A,multiply(A,B)))),add(additive_inverse(multiply(A,multiply(C,multiply(A,B)))),add(multiply(A,multiply(A,multiply(A,B))),multiply(multiply(A,C),multiply(A,B))))) = add(multiply(A,multiply(B,multiply(A,A))),add(multiply(multiply(A,B),multiply(C,A)),add(additive_inverse(multiply(multiply(multiply(A,B),A),A)),additive_inverse(multiply(multiply(multiply(A,B),C),A))))),
inference(paramod,[status(thm)],[c_11,c_27830]) ).
cnf(c_27832,plain,
add(additive_inverse(multiply(A,multiply(C,multiply(A,B)))),multiply(multiply(A,C),multiply(A,B))) = add(multiply(A,multiply(B,multiply(A,A))),add(multiply(multiply(A,B),multiply(C,A)),add(additive_inverse(multiply(multiply(multiply(A,B),A),A)),additive_inverse(multiply(multiply(multiply(A,B),C),A))))),
inference(paramod,[status(thm)],[c_190,c_27831]) ).
cnf(c_27833,plain,
add(additive_inverse(multiply(A,multiply(C,multiply(A,B)))),multiply(multiply(A,C),multiply(A,B))) = add(multiply(A,multiply(B,multiply(A,A))),add(multiply(multiply(A,B),multiply(C,A)),add(additive_inverse(multiply(multiply(A,multiply(B,A)),A)),additive_inverse(multiply(multiply(multiply(A,B),C),A))))),
inference(paramod,[status(thm)],[c_22,c_27832]) ).
cnf(c_27834,plain,
add(additive_inverse(multiply(A,multiply(C,multiply(A,B)))),multiply(multiply(A,C),multiply(A,B))) = add(multiply(A,multiply(B,multiply(A,A))),add(multiply(multiply(A,B),multiply(C,A)),add(additive_inverse(multiply(A,multiply(multiply(B,A),A))),additive_inverse(multiply(multiply(multiply(A,B),C),A))))),
inference(paramod,[status(thm)],[c_22,c_27833]) ).
cnf(c_27835,plain,
add(additive_inverse(multiply(A,multiply(C,multiply(A,B)))),multiply(multiply(A,C),multiply(A,B))) = add(multiply(A,multiply(B,multiply(A,A))),add(multiply(multiply(A,B),multiply(C,A)),add(additive_inverse(multiply(A,multiply(B,multiply(A,A)))),additive_inverse(multiply(multiply(multiply(A,B),C),A))))),
inference(paramod,[status(thm)],[c_10,c_27834]) ).
cnf(c_27836,plain,
add(additive_inverse(multiply(A,multiply(C,multiply(A,B)))),multiply(multiply(A,C),multiply(A,B))) = add(multiply(A,multiply(B,multiply(A,A))),add(additive_inverse(multiply(A,multiply(B,multiply(A,A)))),add(multiply(multiply(A,B),multiply(C,A)),additive_inverse(multiply(multiply(multiply(A,B),C),A))))),
inference(paramod,[status(thm)],[c_40,c_27835]) ).
cnf(c_27837,plain,
add(additive_inverse(multiply(A,multiply(C,multiply(A,B)))),multiply(multiply(A,C),multiply(A,B))) = add(multiply(multiply(A,B),multiply(C,A)),additive_inverse(multiply(multiply(multiply(A,B),C),A))),
inference(paramod,[status(thm)],[c_120,c_27836]) ).
cnf(c_11198,plain,
add(multiply(multiply(A,B),multiply(C,A)),additive_inverse(multiply(multiply(multiply(A,B),C),A))) = add(additive_inverse(multiply(A,multiply(C,multiply(A,B)))),multiply(multiply(A,C),multiply(A,B))),
inference(copy,[status(thm)],[c_27837]) ).
cnf(c_27838,plain,
add(additive_inverse(multiply(multiply(A,B),multiply(B,C))),multiply(multiply(A,multiply(B,B)),C)) = add(multiply(multiply(A,B),multiply(C,B)),additive_inverse(multiply(multiply(multiply(A,B),C),B))),
inference(paramod,[status(thm)],[c_115,c_63]) ).
cnf(c_22217,plain,
add(multiply(multiply(A,B),multiply(C,B)),additive_inverse(multiply(multiply(multiply(A,B),C),B))) = add(additive_inverse(multiply(multiply(A,B),multiply(B,C))),multiply(multiply(A,multiply(B,B)),C)),
inference(copy,[status(thm)],[c_27838]) ).
cnf(c_27839,plain,
multiply(add(multiply(cz,multiply(cx,cy)),add(multiply(cx,multiply(cz,cy)),additive_inverse(multiply(multiply(cx,cz),cy)))),cx) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_149,c_28]) ).
cnf(c_27840,plain,
multiply(add(multiply(cx,multiply(cz,cy)),add(multiply(cz,multiply(cx,cy)),additive_inverse(multiply(multiply(cx,cz),cy)))),cx) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_40,c_27839]) ).
cnf(c_27841,plain,
add(multiply(multiply(cx,multiply(cz,cy)),cx),multiply(add(multiply(cz,multiply(cx,cy)),additive_inverse(multiply(multiply(cx,cz),cy))),cx)) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_9,c_27840]) ).
cnf(c_27842,plain,
add(multiply(cx,multiply(multiply(cz,cy),cx)),multiply(add(multiply(cz,multiply(cx,cy)),additive_inverse(multiply(multiply(cx,cz),cy))),cx)) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_22,c_27841]) ).
cnf(c_27843,plain,
add(multiply(cx,multiply(multiply(cz,cy),cx)),add(multiply(multiply(cz,multiply(cx,cy)),cx),multiply(additive_inverse(multiply(multiply(cx,cz),cy)),cx))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_9,c_27842]) ).
cnf(c_25452,plain,
add(multiply(cx,multiply(multiply(cz,cy),cx)),add(multiply(multiply(cz,multiply(cx,cy)),cx),additive_inverse(multiply(multiply(multiply(cx,cz),cy),cx)))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_12,c_27843]) ).
cnf(c_25466,plain,
add(multiply(multiply(A,B),C),multiply(multiply(B,A),C)) = add(multiply(B,multiply(A,C)),multiply(A,multiply(B,C))),
inference(paramod,[status(thm)],[c_149,c_155]) ).
cnf(c_27844,plain,
add(multiply(cx,multiply(multiply(cz,cy),cx)),add(multiply(multiply(cz,multiply(cx,cy)),cx),additive_inverse(multiply(add(multiply(cx,multiply(cz,cy)),add(multiply(cy,multiply(cz,cx)),additive_inverse(multiply(multiply(cy,cz),cx)))),cx)))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_150,c_25452]) ).
cnf(c_27845,plain,
add(multiply(cx,multiply(multiply(cz,cy),cx)),add(multiply(multiply(cz,multiply(cx,cy)),cx),additive_inverse(multiply(add(multiply(cy,multiply(cz,cx)),add(multiply(cx,multiply(cz,cy)),additive_inverse(multiply(multiply(cy,cz),cx)))),cx)))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_40,c_27844]) ).
cnf(c_27846,plain,
add(multiply(cx,multiply(multiply(cz,cy),cx)),add(multiply(multiply(cz,multiply(cx,cy)),cx),additive_inverse(add(multiply(multiply(cy,multiply(cz,cx)),cx),multiply(add(multiply(cx,multiply(cz,cy)),additive_inverse(multiply(multiply(cy,cz),cx))),cx))))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_9,c_27845]) ).
cnf(c_27847,plain,
add(multiply(cx,multiply(multiply(cz,cy),cx)),add(multiply(multiply(cz,multiply(cx,cy)),cx),additive_inverse(add(multiply(multiply(cy,multiply(cz,cx)),cx),add(multiply(multiply(cx,multiply(cz,cy)),cx),multiply(additive_inverse(multiply(multiply(cy,cz),cx)),cx)))))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_9,c_27846]) ).
cnf(c_27848,plain,
add(multiply(cx,multiply(multiply(cz,cy),cx)),add(multiply(multiply(cz,multiply(cx,cy)),cx),additive_inverse(add(multiply(multiply(cy,multiply(cz,cx)),cx),add(multiply(cx,multiply(multiply(cz,cy),cx)),multiply(additive_inverse(multiply(multiply(cy,cz),cx)),cx)))))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_22,c_27847]) ).
cnf(c_27849,plain,
add(multiply(cx,multiply(multiply(cz,cy),cx)),add(multiply(multiply(cz,multiply(cx,cy)),cx),additive_inverse(add(multiply(multiply(cy,multiply(cz,cx)),cx),add(multiply(cx,multiply(multiply(cz,cy),cx)),additive_inverse(multiply(multiply(multiply(cy,cz),cx),cx))))))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_12,c_27848]) ).
cnf(c_27850,plain,
add(multiply(cx,multiply(multiply(cz,cy),cx)),add(multiply(multiply(cz,multiply(cx,cy)),cx),additive_inverse(add(multiply(multiply(cy,multiply(cz,cx)),cx),add(multiply(cx,multiply(multiply(cz,cy),cx)),additive_inverse(multiply(multiply(cy,cz),multiply(cx,cx)))))))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_10,c_27849]) ).
cnf(c_27851,plain,
add(multiply(cx,multiply(multiply(cz,cy),cx)),add(multiply(multiply(cz,multiply(cx,cy)),cx),additive_inverse(add(multiply(multiply(cy,multiply(cz,cx)),cx),add(additive_inverse(multiply(multiply(cy,cz),multiply(cx,cx))),multiply(cx,multiply(multiply(cz,cy),cx))))))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_15,c_27850]) ).
cnf(c_27852,plain,
add(multiply(cx,multiply(multiply(cz,cy),cx)),add(multiply(multiply(cz,multiply(cx,cy)),cx),additive_inverse(add(additive_inverse(multiply(multiply(cy,cz),multiply(cx,cx))),add(multiply(multiply(cy,multiply(cz,cx)),cx),multiply(cx,multiply(multiply(cz,cy),cx))))))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_40,c_27851]) ).
cnf(c_27853,plain,
add(multiply(cx,multiply(multiply(cz,cy),cx)),add(multiply(multiply(cz,multiply(cx,cy)),cx),add(additive_inverse(additive_inverse(multiply(multiply(cy,cz),multiply(cx,cx)))),additive_inverse(add(multiply(multiply(cy,multiply(cz,cx)),cx),multiply(cx,multiply(multiply(cz,cy),cx))))))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_6,c_27852]) ).
cnf(c_27854,plain,
add(multiply(cx,multiply(multiply(cz,cy),cx)),add(multiply(multiply(cz,multiply(cx,cy)),cx),add(multiply(multiply(cy,cz),multiply(cx,cx)),additive_inverse(add(multiply(multiply(cy,multiply(cz,cx)),cx),multiply(cx,multiply(multiply(cz,cy),cx))))))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_7,c_27853]) ).
cnf(c_27855,plain,
add(multiply(cx,multiply(multiply(cz,cy),cx)),add(multiply(multiply(cz,multiply(cx,cy)),cx),add(multiply(multiply(cy,cz),multiply(cx,cx)),add(additive_inverse(multiply(multiply(cy,multiply(cz,cx)),cx)),additive_inverse(multiply(cx,multiply(multiply(cz,cy),cx))))))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_6,c_27854]) ).
cnf(c_27856,plain,
add(multiply(cx,multiply(multiply(cz,cy),cx)),add(add(multiply(multiply(cy,cz),multiply(cx,cx)),add(additive_inverse(multiply(multiply(cy,multiply(cz,cx)),cx)),additive_inverse(multiply(cx,multiply(multiply(cz,cy),cx))))),multiply(multiply(cz,multiply(cx,cy)),cx))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_15,c_27855]) ).
cnf(c_27857,plain,
add(multiply(cx,multiply(multiply(cz,cy),cx)),add(multiply(multiply(cy,cz),multiply(cx,cx)),add(add(additive_inverse(multiply(multiply(cy,multiply(cz,cx)),cx)),additive_inverse(multiply(cx,multiply(multiply(cz,cy),cx)))),multiply(multiply(cz,multiply(cx,cy)),cx)))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_17,c_27856]) ).
cnf(c_27858,plain,
add(multiply(cx,multiply(multiply(cz,cy),cx)),add(multiply(multiply(cy,cz),multiply(cx,cx)),add(additive_inverse(multiply(multiply(cy,multiply(cz,cx)),cx)),add(additive_inverse(multiply(cx,multiply(multiply(cz,cy),cx))),multiply(multiply(cz,multiply(cx,cy)),cx))))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_17,c_27857]) ).
cnf(c_27859,plain,
add(multiply(multiply(cy,cz),multiply(cx,cx)),add(multiply(cx,multiply(multiply(cz,cy),cx)),add(additive_inverse(multiply(multiply(cy,multiply(cz,cx)),cx)),add(additive_inverse(multiply(cx,multiply(multiply(cz,cy),cx))),multiply(multiply(cz,multiply(cx,cy)),cx))))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_40,c_27858]) ).
cnf(c_27860,plain,
add(multiply(multiply(cy,cz),multiply(cx,cx)),add(additive_inverse(multiply(multiply(cy,multiply(cz,cx)),cx)),add(multiply(cx,multiply(multiply(cz,cy),cx)),add(additive_inverse(multiply(cx,multiply(multiply(cz,cy),cx))),multiply(multiply(cz,multiply(cx,cy)),cx))))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_40,c_27859]) ).
cnf(c_26086,plain,
add(multiply(multiply(cy,cz),multiply(cx,cx)),add(additive_inverse(multiply(multiply(cy,multiply(cz,cx)),cx)),multiply(multiply(cz,multiply(cx,cy)),cx))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_120,c_27860]) ).
cnf(c_27861,plain,
add(multiply(multiply(cy,cz),multiply(cx,cx)),add(additive_inverse(add(multiply(cy,multiply(multiply(cz,cx),cx)),add(multiply(multiply(cz,cx),multiply(cy,cx)),additive_inverse(multiply(multiply(multiply(cz,cx),cy),cx))))),multiply(multiply(cz,multiply(cx,cy)),cx))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_149,c_26086]) ).
cnf(c_27862,plain,
add(multiply(multiply(cy,cz),multiply(cx,cx)),add(additive_inverse(add(multiply(cy,multiply(cz,multiply(cx,cx))),add(multiply(multiply(cz,cx),multiply(cy,cx)),additive_inverse(multiply(multiply(multiply(cz,cx),cy),cx))))),multiply(multiply(cz,multiply(cx,cy)),cx))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_10,c_27861]) ).
cnf(c_27863,plain,
add(multiply(multiply(cy,cz),multiply(cx,cx)),add(additive_inverse(add(multiply(cy,multiply(cz,multiply(cx,cx))),add(additive_inverse(multiply(multiply(cz,cx),multiply(cx,cy))),multiply(multiply(cz,multiply(cx,cx)),cy)))),multiply(multiply(cz,multiply(cx,cy)),cx))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_22217,c_27862]) ).
cnf(c_27864,plain,
add(multiply(multiply(cy,cz),multiply(cx,cx)),add(add(additive_inverse(multiply(cy,multiply(cz,multiply(cx,cx)))),additive_inverse(add(additive_inverse(multiply(multiply(cz,cx),multiply(cx,cy))),multiply(multiply(cz,multiply(cx,cx)),cy)))),multiply(multiply(cz,multiply(cx,cy)),cx))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_6,c_27863]) ).
cnf(c_27865,plain,
add(multiply(multiply(cy,cz),multiply(cx,cx)),add(add(additive_inverse(multiply(cy,multiply(cz,multiply(cx,cx)))),add(additive_inverse(additive_inverse(multiply(multiply(cz,cx),multiply(cx,cy)))),additive_inverse(multiply(multiply(cz,multiply(cx,cx)),cy)))),multiply(multiply(cz,multiply(cx,cy)),cx))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_6,c_27864]) ).
cnf(c_27866,plain,
add(multiply(multiply(cy,cz),multiply(cx,cx)),add(add(additive_inverse(multiply(cy,multiply(cz,multiply(cx,cx)))),add(multiply(multiply(cz,cx),multiply(cx,cy)),additive_inverse(multiply(multiply(cz,multiply(cx,cx)),cy)))),multiply(multiply(cz,multiply(cx,cy)),cx))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_7,c_27865]) ).
cnf(c_27867,plain,
add(multiply(multiply(cy,cz),multiply(cx,cx)),add(additive_inverse(multiply(cy,multiply(cz,multiply(cx,cx)))),add(add(multiply(multiply(cz,cx),multiply(cx,cy)),additive_inverse(multiply(multiply(cz,multiply(cx,cx)),cy))),multiply(multiply(cz,multiply(cx,cy)),cx)))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_17,c_27866]) ).
cnf(c_27868,plain,
add(multiply(multiply(cy,cz),multiply(cx,cx)),add(additive_inverse(multiply(cy,multiply(cz,multiply(cx,cx)))),add(multiply(multiply(cz,cx),multiply(cx,cy)),add(additive_inverse(multiply(multiply(cz,multiply(cx,cx)),cy)),multiply(multiply(cz,multiply(cx,cy)),cx))))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_17,c_27867]) ).
cnf(c_26124,plain,
add(additive_inverse(multiply(cy,multiply(cz,multiply(cx,cx)))),add(multiply(multiply(cy,cz),multiply(cx,cx)),add(multiply(multiply(cz,cx),multiply(cx,cy)),add(additive_inverse(multiply(multiply(cz,multiply(cx,cx)),cy)),multiply(multiply(cz,multiply(cx,cy)),cx))))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_40,c_27868]) ).
cnf(c_27869,plain,
add(multiply(multiply(cx,cx),multiply(cz,cy)),add(additive_inverse(multiply(multiply(multiply(cx,cx),cz),cy)),add(multiply(multiply(cz,cx),multiply(cx,cy)),add(additive_inverse(multiply(multiply(cz,multiply(cx,cx)),cy)),multiply(multiply(cz,multiply(cx,cy)),cx))))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_99,c_26124]) ).
cnf(c_27870,plain,
add(multiply(cx,multiply(cx,multiply(cz,cy))),add(additive_inverse(multiply(multiply(multiply(cx,cx),cz),cy)),add(multiply(multiply(cz,cx),multiply(cx,cy)),add(additive_inverse(multiply(multiply(cz,multiply(cx,cx)),cy)),multiply(multiply(cz,multiply(cx,cy)),cx))))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_11,c_27869]) ).
cnf(c_26541,plain,
add(multiply(cx,multiply(cx,multiply(cz,cy))),add(additive_inverse(multiply(multiply(cx,multiply(cx,cz)),cy)),add(multiply(multiply(cz,cx),multiply(cx,cy)),add(additive_inverse(multiply(multiply(cz,multiply(cx,cx)),cy)),multiply(multiply(cz,multiply(cx,cy)),cx))))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_11,c_27870]) ).
cnf(c_27871,plain,
add(multiply(cx,multiply(cx,multiply(cz,cy))),add(additive_inverse(multiply(multiply(cx,multiply(cx,cz)),cy)),add(multiply(multiply(cz,cx),multiply(cx,cy)),add(additive_inverse(add(multiply(cz,multiply(multiply(cx,cx),cy)),add(multiply(multiply(cx,cx),multiply(cz,cy)),additive_inverse(multiply(multiply(multiply(cx,cx),cz),cy))))),multiply(multiply(cz,multiply(cx,cy)),cx))))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_149,c_26541]) ).
cnf(c_27872,plain,
add(multiply(cx,multiply(cx,multiply(cz,cy))),add(additive_inverse(multiply(multiply(cx,multiply(cx,cz)),cy)),add(multiply(multiply(cz,cx),multiply(cx,cy)),add(additive_inverse(add(multiply(cz,multiply(cx,multiply(cx,cy))),add(multiply(multiply(cx,cx),multiply(cz,cy)),additive_inverse(multiply(multiply(multiply(cx,cx),cz),cy))))),multiply(multiply(cz,multiply(cx,cy)),cx))))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_11,c_27871]) ).
cnf(c_27873,plain,
add(multiply(cx,multiply(cx,multiply(cz,cy))),add(additive_inverse(multiply(multiply(cx,multiply(cx,cz)),cy)),add(multiply(multiply(cz,cx),multiply(cx,cy)),add(additive_inverse(add(multiply(cz,multiply(cx,multiply(cx,cy))),add(multiply(cx,multiply(cx,multiply(cz,cy))),additive_inverse(multiply(multiply(multiply(cx,cx),cz),cy))))),multiply(multiply(cz,multiply(cx,cy)),cx))))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_11,c_27872]) ).
cnf(c_27874,plain,
add(multiply(cx,multiply(cx,multiply(cz,cy))),add(additive_inverse(multiply(multiply(cx,multiply(cx,cz)),cy)),add(multiply(multiply(cz,cx),multiply(cx,cy)),add(additive_inverse(add(multiply(cz,multiply(cx,multiply(cx,cy))),add(multiply(cx,multiply(cx,multiply(cz,cy))),additive_inverse(multiply(multiply(cx,multiply(cx,cz)),cy))))),multiply(multiply(cz,multiply(cx,cy)),cx))))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_11,c_27873]) ).
cnf(c_27875,plain,
add(multiply(cx,multiply(cx,multiply(cz,cy))),add(additive_inverse(multiply(multiply(cx,multiply(cx,cz)),cy)),add(multiply(multiply(cz,cx),multiply(cx,cy)),add(additive_inverse(add(multiply(cx,multiply(cx,multiply(cz,cy))),add(multiply(cz,multiply(cx,multiply(cx,cy))),additive_inverse(multiply(multiply(cx,multiply(cx,cz)),cy))))),multiply(multiply(cz,multiply(cx,cy)),cx))))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_40,c_27874]) ).
cnf(c_27876,plain,
add(multiply(cx,multiply(cx,multiply(cz,cy))),add(additive_inverse(multiply(multiply(cx,multiply(cx,cz)),cy)),add(multiply(multiply(cz,cx),multiply(cx,cy)),add(add(additive_inverse(multiply(cx,multiply(cx,multiply(cz,cy)))),additive_inverse(add(multiply(cz,multiply(cx,multiply(cx,cy))),additive_inverse(multiply(multiply(cx,multiply(cx,cz)),cy))))),multiply(multiply(cz,multiply(cx,cy)),cx))))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_6,c_27875]) ).
cnf(c_27877,plain,
add(multiply(cx,multiply(cx,multiply(cz,cy))),add(additive_inverse(multiply(multiply(cx,multiply(cx,cz)),cy)),add(multiply(multiply(cz,cx),multiply(cx,cy)),add(add(additive_inverse(multiply(cx,multiply(cx,multiply(cz,cy)))),add(additive_inverse(multiply(cz,multiply(cx,multiply(cx,cy)))),additive_inverse(additive_inverse(multiply(multiply(cx,multiply(cx,cz)),cy))))),multiply(multiply(cz,multiply(cx,cy)),cx))))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_6,c_27876]) ).
cnf(c_27878,plain,
add(multiply(cx,multiply(cx,multiply(cz,cy))),add(additive_inverse(multiply(multiply(cx,multiply(cx,cz)),cy)),add(multiply(multiply(cz,cx),multiply(cx,cy)),add(add(additive_inverse(multiply(cx,multiply(cx,multiply(cz,cy)))),add(additive_inverse(multiply(cz,multiply(cx,multiply(cx,cy)))),multiply(multiply(cx,multiply(cx,cz)),cy))),multiply(multiply(cz,multiply(cx,cy)),cx))))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_7,c_27877]) ).
cnf(c_27879,plain,
add(multiply(cx,multiply(cx,multiply(cz,cy))),add(additive_inverse(multiply(multiply(cx,multiply(cx,cz)),cy)),add(multiply(multiply(cz,cx),multiply(cx,cy)),add(additive_inverse(multiply(cx,multiply(cx,multiply(cz,cy)))),add(add(additive_inverse(multiply(cz,multiply(cx,multiply(cx,cy)))),multiply(multiply(cx,multiply(cx,cz)),cy)),multiply(multiply(cz,multiply(cx,cy)),cx)))))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_17,c_27878]) ).
cnf(c_27880,plain,
add(multiply(cx,multiply(cx,multiply(cz,cy))),add(additive_inverse(multiply(multiply(cx,multiply(cx,cz)),cy)),add(multiply(multiply(cz,cx),multiply(cx,cy)),add(additive_inverse(multiply(cx,multiply(cx,multiply(cz,cy)))),add(additive_inverse(multiply(cz,multiply(cx,multiply(cx,cy)))),add(multiply(multiply(cx,multiply(cx,cz)),cy),multiply(multiply(cz,multiply(cx,cy)),cx))))))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_17,c_27879]) ).
cnf(c_27881,plain,
add(multiply(cx,multiply(cx,multiply(cz,cy))),add(additive_inverse(multiply(multiply(cx,multiply(cx,cz)),cy)),add(additive_inverse(multiply(cx,multiply(cx,multiply(cz,cy)))),add(multiply(multiply(cz,cx),multiply(cx,cy)),add(additive_inverse(multiply(cz,multiply(cx,multiply(cx,cy)))),add(multiply(multiply(cx,multiply(cx,cz)),cy),multiply(multiply(cz,multiply(cx,cy)),cx))))))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_40,c_27880]) ).
cnf(c_27882,plain,
add(multiply(cx,multiply(cx,multiply(cz,cy))),add(additive_inverse(multiply(multiply(cx,multiply(cx,cz)),cy)),add(additive_inverse(multiply(cx,multiply(cx,multiply(cz,cy)))),add(additive_inverse(multiply(cz,multiply(cx,multiply(cx,cy)))),add(multiply(multiply(cz,cx),multiply(cx,cy)),add(multiply(multiply(cx,multiply(cx,cz)),cy),multiply(multiply(cz,multiply(cx,cy)),cx))))))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_40,c_27881]) ).
cnf(c_27883,plain,
add(multiply(cx,multiply(cx,multiply(cz,cy))),add(additive_inverse(multiply(multiply(cx,multiply(cx,cz)),cy)),add(additive_inverse(multiply(cx,multiply(cx,multiply(cz,cy)))),add(additive_inverse(multiply(cz,multiply(cx,multiply(cx,cy)))),add(multiply(multiply(cx,multiply(cx,cz)),cy),add(multiply(multiply(cz,cx),multiply(cx,cy)),multiply(multiply(cz,multiply(cx,cy)),cx))))))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_40,c_27882]) ).
cnf(c_27884,plain,
add(multiply(cx,multiply(cx,multiply(cz,cy))),add(additive_inverse(multiply(cx,multiply(cx,multiply(cz,cy)))),add(additive_inverse(multiply(multiply(cx,multiply(cx,cz)),cy)),add(additive_inverse(multiply(cz,multiply(cx,multiply(cx,cy)))),add(multiply(multiply(cx,multiply(cx,cz)),cy),add(multiply(multiply(cz,cx),multiply(cx,cy)),multiply(multiply(cz,multiply(cx,cy)),cx))))))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_40,c_27883]) ).
cnf(c_27885,plain,
add(multiply(cx,multiply(cx,multiply(cz,cy))),add(additive_inverse(multiply(cx,multiply(cx,multiply(cz,cy)))),add(additive_inverse(multiply(cz,multiply(cx,multiply(cx,cy)))),add(additive_inverse(multiply(multiply(cx,multiply(cx,cz)),cy)),add(multiply(multiply(cx,multiply(cx,cz)),cy),add(multiply(multiply(cz,cx),multiply(cx,cy)),multiply(multiply(cz,multiply(cx,cy)),cx))))))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_40,c_27884]) ).
cnf(c_27886,plain,
add(multiply(cx,multiply(cx,multiply(cz,cy))),add(additive_inverse(multiply(cx,multiply(cx,multiply(cz,cy)))),add(additive_inverse(multiply(cz,multiply(cx,multiply(cx,cy)))),add(multiply(multiply(cx,multiply(cx,cz)),cy),add(additive_inverse(multiply(multiply(cx,multiply(cx,cz)),cy)),add(multiply(multiply(cz,cx),multiply(cx,cy)),multiply(multiply(cz,multiply(cx,cy)),cx))))))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_40,c_27885]) ).
cnf(c_27887,plain,
add(multiply(cx,multiply(cx,multiply(cz,cy))),add(additive_inverse(multiply(cx,multiply(cx,multiply(cz,cy)))),add(additive_inverse(multiply(cz,multiply(cx,multiply(cx,cy)))),add(multiply(multiply(cz,cx),multiply(cx,cy)),multiply(multiply(cz,multiply(cx,cy)),cx))))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_120,c_27886]) ).
cnf(c_27581,plain,
add(additive_inverse(multiply(cz,multiply(cx,multiply(cx,cy)))),add(multiply(multiply(cz,cx),multiply(cx,cy)),multiply(multiply(cz,multiply(cx,cy)),cx))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_120,c_27887]) ).
cnf(c_27888,plain,
add(additive_inverse(multiply(cz,multiply(cx,multiply(cx,cy)))),add(multiply(multiply(cz,cx),multiply(cx,cy)),add(multiply(cz,multiply(multiply(cx,cy),cx)),add(multiply(multiply(cx,cy),multiply(cz,cx)),additive_inverse(multiply(multiply(multiply(cx,cy),cz),cx)))))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_149,c_27581]) ).
cnf(c_27889,plain,
add(additive_inverse(multiply(cz,multiply(cx,multiply(cx,cy)))),add(multiply(multiply(cz,cx),multiply(cx,cy)),add(multiply(cz,multiply(cx,multiply(cy,cx))),add(multiply(multiply(cx,cy),multiply(cz,cx)),additive_inverse(multiply(multiply(multiply(cx,cy),cz),cx)))))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_22,c_27888]) ).
cnf(c_27890,plain,
add(additive_inverse(multiply(cz,multiply(cx,multiply(cx,cy)))),add(multiply(multiply(cz,cx),multiply(cx,cy)),add(multiply(cz,multiply(cx,multiply(cy,cx))),add(additive_inverse(multiply(cx,multiply(cz,multiply(cx,cy)))),multiply(multiply(cx,cz),multiply(cx,cy)))))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_11198,c_27889]) ).
cnf(c_27891,plain,
add(additive_inverse(multiply(cz,multiply(cx,multiply(cx,cy)))),add(multiply(multiply(cz,cx),multiply(cx,cy)),add(additive_inverse(multiply(cx,multiply(cz,multiply(cx,cy)))),add(multiply(cz,multiply(cx,multiply(cy,cx))),multiply(multiply(cx,cz),multiply(cx,cy)))))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_40,c_27890]) ).
cnf(c_27892,plain,
add(additive_inverse(multiply(cz,multiply(cx,multiply(cx,cy)))),add(add(additive_inverse(multiply(cx,multiply(cz,multiply(cx,cy)))),add(multiply(cz,multiply(cx,multiply(cy,cx))),multiply(multiply(cx,cz),multiply(cx,cy)))),multiply(multiply(cz,cx),multiply(cx,cy)))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_15,c_27891]) ).
cnf(c_27893,plain,
add(additive_inverse(multiply(cz,multiply(cx,multiply(cx,cy)))),add(additive_inverse(multiply(cx,multiply(cz,multiply(cx,cy)))),add(add(multiply(cz,multiply(cx,multiply(cy,cx))),multiply(multiply(cx,cz),multiply(cx,cy))),multiply(multiply(cz,cx),multiply(cx,cy))))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_17,c_27892]) ).
cnf(c_27894,plain,
add(additive_inverse(multiply(cz,multiply(cx,multiply(cx,cy)))),add(additive_inverse(multiply(cx,multiply(cz,multiply(cx,cy)))),add(multiply(cz,multiply(cx,multiply(cy,cx))),add(multiply(multiply(cx,cz),multiply(cx,cy)),multiply(multiply(cz,cx),multiply(cx,cy)))))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_17,c_27893]) ).
cnf(c_27895,plain,
add(additive_inverse(multiply(cz,multiply(cx,multiply(cx,cy)))),add(additive_inverse(multiply(cx,multiply(cz,multiply(cx,cy)))),add(multiply(cz,multiply(cx,multiply(cy,cx))),add(multiply(cz,multiply(cx,multiply(cx,cy))),multiply(cx,multiply(cz,multiply(cx,cy))))))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_25466,c_27894]) ).
cnf(c_27896,plain,
add(additive_inverse(multiply(cz,multiply(cx,multiply(cx,cy)))),add(additive_inverse(multiply(cx,multiply(cz,multiply(cx,cy)))),add(multiply(cz,multiply(cx,multiply(cy,cx))),add(multiply(cx,multiply(cz,multiply(cx,cy))),multiply(cz,multiply(cx,multiply(cx,cy))))))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_15,c_27895]) ).
cnf(c_27897,plain,
add(additive_inverse(multiply(cz,multiply(cx,multiply(cx,cy)))),add(additive_inverse(multiply(cx,multiply(cz,multiply(cx,cy)))),add(add(multiply(cx,multiply(cz,multiply(cx,cy))),multiply(cz,multiply(cx,multiply(cx,cy)))),multiply(cz,multiply(cx,multiply(cy,cx)))))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_15,c_27896]) ).
cnf(c_27898,plain,
add(additive_inverse(multiply(cz,multiply(cx,multiply(cx,cy)))),add(additive_inverse(multiply(cx,multiply(cz,multiply(cx,cy)))),add(multiply(cx,multiply(cz,multiply(cx,cy))),add(multiply(cz,multiply(cx,multiply(cx,cy))),multiply(cz,multiply(cx,multiply(cy,cx))))))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_17,c_27897]) ).
cnf(c_27899,plain,
add(additive_inverse(multiply(cz,multiply(cx,multiply(cx,cy)))),add(multiply(cx,multiply(cz,multiply(cx,cy))),add(additive_inverse(multiply(cx,multiply(cz,multiply(cx,cy)))),add(multiply(cz,multiply(cx,multiply(cx,cy))),multiply(cz,multiply(cx,multiply(cy,cx))))))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_40,c_27898]) ).
cnf(c_27900,plain,
add(additive_inverse(multiply(cz,multiply(cx,multiply(cx,cy)))),add(multiply(cz,multiply(cx,multiply(cx,cy))),multiply(cz,multiply(cx,multiply(cy,cx))))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_120,c_27899]) ).
cnf(c_27901,plain,
add(multiply(cz,multiply(cx,multiply(cx,cy))),add(additive_inverse(multiply(cz,multiply(cx,multiply(cx,cy)))),multiply(cz,multiply(cx,multiply(cy,cx))))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_40,c_27900]) ).
cnf(c_27902,plain,
multiply(cz,multiply(cx,multiply(cy,cx))) != multiply(cz,multiply(cx,multiply(cy,cx))),
inference(paramod,[status(thm)],[c_120,c_27901]) ).
cnf(c_27799,plain,
$false,
inference(copy,[status(thm)],[c_27902]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : RNG027-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.43 % Computer : n019.cluster.edu
% 0.09/0.43 % Model : x86_64 x86_64
% 0.09/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.43 % Memory : 8046.5625MB
% 0.09/0.43 % OS : Linux 6.8.0-71-generic
% 0.09/0.43 % CPULimit : 300
% 0.09/0.43 % WCLimit : 300
% 0.09/0.43 % DateTime : Sat Sep 26 05:47:33 UTC 2026
% 0.09/0.43 % CPUTime :
% 0.09/0.43 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.43 % Process 540231 was started by sandbox on n019,
% 0.09/0.43 % Sat Sep 26 05:47:33 2026
% 0.09/0.43 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.09/0.43
% 0.09/0.43 % From the command line: assign(max_seconds, 300).
% 183.37/38.85
% 183.37/38.85 % given #500 (T,wt=15): 18720 ifeq(A,add(B,add(A,C)),add(additive_inverse(C),additive_inverse(B)),additive_identity) = additive_identity. [para(153(a,1),7311(a,1,1))].
% 183.37/38.85
% 183.37/38.85 % SZS status Unsatisfiable for theBenchmark
% 183.37/38.85
% 183.37/38.85 % Proof 1 at 21.81 (+ 1.93) seconds.
% 183.37/38.85 % Length of proof is 44.
% 183.37/38.85 % Level of proof is 9.
% 183.37/38.85 % Maximum clause weight is 51.000.
% 183.37/38.85 % Given clauses 610.
% 183.37/38.85
% 183.37/38.85 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------