%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : BOO026-1 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n020.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 06:55:08 AM UTC 2026
% Result : Unsatisfiable 2.56s 0.74s
% Output : CNFRefutation 2.56s
% Verified :
% SZS Type : Refutation
% Derivation depth : 70
% Number of leaves : 9
% Syntax : Number of formulae : 304 ( 304 unt; 0 def)
% Number of atoms : 304 ( 303 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 4 ( 4 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 4 con; 0-2 aty)
% Number of variables : 307 ( 10 sgn 16 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(multiply_add_property,axiom,
! [VAR_0,VAR_1,VAR_2] : multiply(VAR_0,add(VAR_1,VAR_2)) = add(multiply(VAR_1,VAR_0),multiply(VAR_2,VAR_0)),
file('theBenchmark.p',multiply_add_property) ).
cnf(c_1,plain,
multiply(A,add(B,C)) = add(multiply(B,A),multiply(C,A)),
inference(clausify,[status(thm)],[multiply_add_property]) ).
fof(additive_inverse,axiom,
! [VAR_0] : add(VAR_0,inverse(VAR_0)) = n1,
file('theBenchmark.p',additive_inverse) ).
cnf(c_2,plain,
add(A,inverse(A)) = n1,
inference(clausify,[status(thm)],[additive_inverse]) ).
fof(add_multiply_property,axiom,
! [VAR_0,VAR_1,VAR_2] : add(VAR_0,multiply(VAR_1,VAR_2)) = multiply(add(VAR_1,VAR_0),add(VAR_2,VAR_0)),
file('theBenchmark.p',add_multiply_property) ).
cnf(c_3,plain,
add(A,multiply(B,C)) = multiply(add(B,A),add(C,A)),
inference(clausify,[status(thm)],[add_multiply_property]) ).
cnf(c_4,plain,
multiply(add(A,B),add(C,B)) = add(B,multiply(A,C)),
inference(copy,[status(thm)],[c_3]) ).
fof(multiplicative_inverse,axiom,
! [VAR_0] : multiply(VAR_0,inverse(VAR_0)) = n0,
file('theBenchmark.p',multiplicative_inverse) ).
cnf(c_5,plain,
multiply(A,inverse(A)) = n0,
inference(clausify,[status(thm)],[multiplicative_inverse]) ).
fof(pixley1,axiom,
! [VAR_0,VAR_1] : add(multiply(VAR_0,inverse(VAR_0)),add(multiply(VAR_0,VAR_1),multiply(inverse(VAR_0),VAR_1))) = VAR_1,
file('theBenchmark.p',pixley1) ).
cnf(c_6,plain,
add(multiply(A,inverse(A)),add(multiply(A,B),multiply(inverse(A),B))) = B,
inference(clausify,[status(thm)],[pixley1]) ).
cnf(c_7,plain,
add(n0,add(multiply(A,B),multiply(inverse(A),B))) = B,
inference(paramod,[status(thm)],[c_5,c_6]) ).
fof(pixley2,axiom,
! [VAR_0,VAR_1] : add(multiply(VAR_0,inverse(VAR_1)),add(multiply(VAR_0,VAR_1),multiply(inverse(VAR_1),VAR_1))) = VAR_0,
file('theBenchmark.p',pixley2) ).
cnf(c_8,plain,
add(multiply(A,inverse(B)),add(multiply(A,B),multiply(inverse(B),B))) = A,
inference(clausify,[status(thm)],[pixley2]) ).
fof(pixley1_dual,axiom,
! [VAR_0,VAR_1] : multiply(add(VAR_0,inverse(VAR_0)),multiply(add(VAR_0,VAR_1),add(inverse(VAR_0),VAR_1))) = VAR_1,
file('theBenchmark.p',pixley1_dual) ).
cnf(c_10,plain,
multiply(add(A,inverse(A)),multiply(add(A,B),add(inverse(A),B))) = B,
inference(clausify,[status(thm)],[pixley1_dual]) ).
cnf(c_787,plain,
multiply(n1,multiply(add(A,B),add(inverse(A),B))) = B,
inference(paramod,[status(thm)],[c_2,c_10]) ).
cnf(c_788,plain,
multiply(n1,add(B,multiply(A,inverse(A)))) = B,
inference(paramod,[status(thm)],[c_4,c_787]) ).
cnf(c_11,plain,
multiply(n1,add(A,n0)) = A,
inference(paramod,[status(thm)],[c_5,c_788]) ).
fof(pixley2_dual,axiom,
! [VAR_0,VAR_1] : multiply(add(VAR_0,inverse(VAR_1)),multiply(add(VAR_0,VAR_1),add(inverse(VAR_1),VAR_1))) = VAR_0,
file('theBenchmark.p',pixley2_dual) ).
cnf(c_12,plain,
multiply(add(A,inverse(B)),multiply(add(A,B),add(inverse(B),B))) = A,
inference(clausify,[status(thm)],[pixley2_dual]) ).
cnf(c_13,plain,
multiply(add(A,inverse(B)),add(B,multiply(A,inverse(B)))) = A,
inference(paramod,[status(thm)],[c_4,c_12]) ).
fof(prove_multiply_add,axiom,
multiply(add(a,b),b) != b,
file('theBenchmark.p',prove_multiply_add) ).
cnf(c_16,plain,
multiply(add(a,b),b) != b,
inference(clausify,[status(thm)],[prove_multiply_add]) ).
cnf(c_17,plain,
multiply(A,n1) = add(multiply(B,A),multiply(inverse(B),A)),
inference(paramod,[status(thm)],[c_2,c_1]) ).
cnf(c_789,plain,
add(A,multiply(B,C)) = add(multiply(C,add(B,A)),multiply(A,add(B,A))),
inference(paramod,[status(thm)],[c_4,c_1]) ).
cnf(c_18,plain,
add(multiply(A,add(B,C)),multiply(C,add(B,C))) = add(C,multiply(B,A)),
inference(copy,[status(thm)],[c_789]) ).
cnf(c_790,plain,
multiply(add(A,B),add(add(C,D),B)) = add(B,add(multiply(C,A),multiply(D,A))),
inference(paramod,[status(thm)],[c_1,c_4]) ).
cnf(c_19,plain,
add(A,multiply(B,add(C,D))) = add(A,add(multiply(C,B),multiply(D,B))),
inference(paramod,[status(thm)],[c_4,c_790]) ).
cnf(c_20,plain,
multiply(n1,add(A,inverse(B))) = add(inverse(B),multiply(B,A)),
inference(paramod,[status(thm)],[c_2,c_4]) ).
cnf(c_21,plain,
multiply(add(A,inverse(B)),n1) = add(inverse(B),multiply(A,B)),
inference(paramod,[status(thm)],[c_2,c_4]) ).
cnf(c_22,plain,
multiply(inverse(A),add(A,B)) = add(n0,multiply(B,inverse(A))),
inference(paramod,[status(thm)],[c_5,c_1]) ).
cnf(c_23,plain,
multiply(inverse(A),add(B,A)) = add(multiply(B,inverse(A)),n0),
inference(paramod,[status(thm)],[c_5,c_1]) ).
cnf(c_24,plain,
multiply(A,B) = add(multiply(n0,A),multiply(add(multiply(C,B),multiply(inverse(C),B)),A)),
inference(paramod,[status(thm)],[c_7,c_1]) ).
cnf(c_791,plain,
add(n0,multiply(A,add(B,inverse(B)))) = A,
inference(paramod,[status(thm)],[c_1,c_7]) ).
cnf(c_25,plain,
add(n0,multiply(A,n1)) = A,
inference(paramod,[status(thm)],[c_2,c_791]) ).
cnf(c_27,plain,
add(multiply(A,inverse(B)),multiply(B,add(A,inverse(B)))) = A,
inference(paramod,[status(thm)],[c_1,c_8]) ).
cnf(c_792,plain,
A = add(multiply(A,n1),multiply(n0,n1)),
inference(paramod,[status(thm)],[c_11,c_1]) ).
cnf(c_29,plain,
add(multiply(A,n1),multiply(n0,n1)) = A,
inference(copy,[status(thm)],[c_792]) ).
cnf(c_30,plain,
multiply(add(A,n0),add(n1,B)) = add(A,multiply(B,add(A,n0))),
inference(paramod,[status(thm)],[c_11,c_1]) ).
cnf(c_37,plain,
multiply(add(A,B),n1) = add(add(multiply(A,C),multiply(B,C)),multiply(inverse(C),add(A,B))),
inference(paramod,[status(thm)],[c_1,c_17]) ).
cnf(c_793,plain,
multiply(inverse(A),n1) = add(n0,multiply(inverse(A),inverse(A))),
inference(paramod,[status(thm)],[c_5,c_17]) ).
cnf(c_39,plain,
add(n0,multiply(inverse(A),inverse(A))) = multiply(inverse(A),n1),
inference(copy,[status(thm)],[c_793]) ).
cnf(c_45,plain,
add(add(multiply(A,B),multiply(C,B)),multiply(C,add(A,C))) = add(C,multiply(A,B)),
inference(paramod,[status(thm)],[c_1,c_18]) ).
cnf(c_48,plain,
add(add(A,multiply(B,C)),multiply(A,add(C,A))) = add(A,multiply(C,add(B,A))),
inference(paramod,[status(thm)],[c_4,c_18]) ).
cnf(c_50,plain,
add(n0,add(inverse(A),multiply(B,A))) = add(B,inverse(A)),
inference(paramod,[status(thm)],[c_18,c_7]) ).
cnf(c_794,plain,
add(A,multiply(n0,add(A,n0))) = add(n0,multiply(A,n1)),
inference(paramod,[status(thm)],[c_11,c_18]) ).
cnf(c_51,plain,
add(A,multiply(n0,add(A,n0))) = A,
inference(paramod,[status(thm)],[c_25,c_794]) ).
cnf(c_57,plain,
multiply(A,B) = add(multiply(n0,A),multiply(multiply(B,n1),A)),
inference(paramod,[status(thm)],[c_25,c_1]) ).
cnf(c_58,plain,
multiply(A,add(B,multiply(A,n1))) = add(multiply(A,n1),multiply(n0,B)),
inference(paramod,[status(thm)],[c_25,c_4]) ).
cnf(c_59,plain,
multiply(add(A,multiply(B,n1)),B) = add(multiply(B,n1),multiply(A,n0)),
inference(paramod,[status(thm)],[c_25,c_4]) ).
cnf(c_795,plain,
add(multiply(A,B),multiply(multiply(B,n1),add(n0,multiply(B,n1)))) = add(multiply(B,n1),multiply(n0,A)),
inference(paramod,[status(thm)],[c_25,c_18]) ).
cnf(c_796,plain,
add(multiply(A,B),multiply(multiply(B,n1),B)) = add(multiply(B,n1),multiply(n0,A)),
inference(paramod,[status(thm)],[c_25,c_795]) ).
cnf(c_60,plain,
add(multiply(A,n1),multiply(n0,B)) = add(multiply(B,A),multiply(multiply(A,n1),A)),
inference(copy,[status(thm)],[c_796]) ).
cnf(c_797,plain,
multiply(A,add(B,multiply(n0,n1))) = add(multiply(n0,n1),multiply(multiply(A,n1),B)),
inference(paramod,[status(thm)],[c_29,c_4]) ).
cnf(c_62,plain,
add(multiply(n0,n1),multiply(multiply(A,n1),B)) = multiply(A,add(B,multiply(n0,n1))),
inference(copy,[status(thm)],[c_797]) ).
cnf(c_798,plain,
multiply(add(n0,multiply(A,n1)),add(n1,multiply(A,n1))) = A,
inference(paramod,[status(thm)],[c_29,c_4]) ).
cnf(c_64,plain,
multiply(A,add(n1,multiply(A,n1))) = A,
inference(paramod,[status(thm)],[c_25,c_798]) ).
cnf(c_799,plain,
add(multiply(n1,add(n0,multiply(A,n1))),multiply(multiply(A,n1),add(n0,multiply(A,n1)))) = A,
inference(paramod,[status(thm)],[c_29,c_18]) ).
cnf(c_800,plain,
add(multiply(n1,A),multiply(multiply(A,n1),add(n0,multiply(A,n1)))) = A,
inference(paramod,[status(thm)],[c_25,c_799]) ).
cnf(c_67,plain,
add(multiply(n1,A),multiply(multiply(A,n1),A)) = A,
inference(paramod,[status(thm)],[c_25,c_800]) ).
cnf(c_70,plain,
multiply(A,add(B,multiply(n0,add(A,n0)))) = add(multiply(n0,add(A,n0)),multiply(A,B)),
inference(paramod,[status(thm)],[c_51,c_4]) ).
cnf(c_77,plain,
add(multiply(add(n1,multiply(A,n1)),add(A,B)),multiply(B,add(A,B))) = add(B,A),
inference(paramod,[status(thm)],[c_64,c_18]) ).
cnf(c_801,plain,
multiply(n1,n1) = add(inverse(A),multiply(A,A)),
inference(paramod,[status(thm)],[c_2,c_20]) ).
cnf(c_83,plain,
add(inverse(A),multiply(A,A)) = multiply(n1,n1),
inference(copy,[status(thm)],[c_801]) ).
cnf(c_85,plain,
multiply(n1,add(inverse(A),inverse(A))) = add(inverse(A),n0),
inference(paramod,[status(thm)],[c_5,c_20]) ).
cnf(c_88,plain,
multiply(n1,add(add(inverse(n0),n0),inverse(n0))) = inverse(n0),
inference(paramod,[status(thm)],[c_20,c_51]) ).
cnf(c_802,plain,
add(inverse(A),multiply(A,A)) = add(multiply(B,n1),multiply(inverse(B),n1)),
inference(paramod,[status(thm)],[c_17,c_83]) ).
cnf(c_803,plain,
multiply(n1,n1) = add(multiply(B,n1),multiply(inverse(B),n1)),
inference(paramod,[status(thm)],[c_83,c_802]) ).
cnf(c_95,plain,
add(multiply(A,n1),multiply(inverse(A),n1)) = multiply(n1,n1),
inference(copy,[status(thm)],[c_803]) ).
cnf(c_99,plain,
multiply(inverse(A),add(A,A)) = add(n0,n0),
inference(paramod,[status(thm)],[c_5,c_22]) ).
cnf(c_804,plain,
add(multiply(n0,A),multiply(add(multiply(B,n1),multiply(inverse(B),n1)),A)) = add(multiply(C,A),multiply(inverse(C),A)),
inference(paramod,[status(thm)],[c_24,c_17]) ).
cnf(c_805,plain,
add(multiply(n0,A),multiply(multiply(n1,n1),A)) = add(multiply(C,A),multiply(inverse(C),A)),
inference(paramod,[status(thm)],[c_95,c_804]) ).
cnf(c_115,plain,
add(multiply(A,B),multiply(inverse(A),B)) = add(multiply(n0,B),multiply(multiply(n1,n1),B)),
inference(copy,[status(thm)],[c_805]) ).
cnf(c_806,plain,
add(multiply(n0,n1),multiply(multiply(n1,n1),n1)) = multiply(n1,n1),
inference(paramod,[status(thm)],[c_115,c_95]) ).
cnf(c_117,plain,
multiply(n1,add(n1,multiply(n0,n1))) = multiply(n1,n1),
inference(paramod,[status(thm)],[c_62,c_806]) ).
cnf(c_137,plain,
add(multiply(inverse(n1),inverse(n1)),add(inverse(n1),n0)) = inverse(n1),
inference(paramod,[status(thm)],[c_85,c_27]) ).
cnf(c_807,plain,
add(inverse(add(n1,n0)),add(n1,multiply(n0,add(n1,n0)))) = multiply(n1,n1),
inference(paramod,[status(thm)],[c_30,c_83]) ).
cnf(c_143,plain,
add(inverse(add(n1,n0)),n1) = multiply(n1,n1),
inference(paramod,[status(thm)],[c_51,c_807]) ).
cnf(c_808,plain,
multiply(inverse(n1),multiply(n1,n1)) = add(multiply(inverse(add(n1,n0)),inverse(n1)),n0),
inference(paramod,[status(thm)],[c_143,c_23]) ).
cnf(c_148,plain,
add(multiply(inverse(add(n1,n0)),inverse(n1)),n0) = multiply(inverse(n1),multiply(n1,n1)),
inference(copy,[status(thm)],[c_808]) ).
cnf(c_809,plain,
add(multiply(n0,n1),multiply(multiply(add(n1,multiply(n0,n1)),n1),n1)) = multiply(n1,n1),
inference(paramod,[status(thm)],[c_57,c_117]) ).
cnf(c_810,plain,
multiply(add(n1,multiply(n0,n1)),add(n1,multiply(n0,n1))) = multiply(n1,n1),
inference(paramod,[status(thm)],[c_62,c_809]) ).
cnf(c_168,plain,
add(multiply(n0,n1),multiply(n1,n1)) = multiply(n1,n1),
inference(paramod,[status(thm)],[c_4,c_810]) ).
cnf(c_170,plain,
multiply(n1,add(n0,n1)) = multiply(n1,n1),
inference(paramod,[status(thm)],[c_168,c_1]) ).
cnf(c_196,plain,
add(add(multiply(n0,A),multiply(n1,A)),multiply(n1,n1)) = add(n1,multiply(n0,A)),
inference(paramod,[status(thm)],[c_170,c_45]) ).
cnf(c_199,plain,
multiply(A,A) = add(multiply(A,n1),multiply(n0,n0)),
inference(paramod,[status(thm)],[c_25,c_58]) ).
cnf(c_201,plain,
multiply(A,add(add(multiply(A,n1),n0),multiply(A,n1))) = multiply(A,n1),
inference(paramod,[status(thm)],[c_58,c_51]) ).
cnf(c_202,plain,
multiply(A,add(add(n1,multiply(n0,n1)),multiply(A,n1))) = add(multiply(A,n1),n0),
inference(paramod,[status(thm)],[c_64,c_58]) ).
cnf(c_213,plain,
multiply(A,add(A,B)) = add(add(multiply(A,n1),multiply(n0,n0)),multiply(B,A)),
inference(paramod,[status(thm)],[c_199,c_1]) ).
cnf(c_811,plain,
multiply(add(A,inverse(B)),add(A,inverse(B))) = add(add(inverse(B),multiply(A,B)),multiply(n0,n0)),
inference(paramod,[status(thm)],[c_21,c_199]) ).
cnf(c_223,plain,
add(inverse(A),multiply(B,B)) = add(add(inverse(A),multiply(B,A)),multiply(n0,n0)),
inference(paramod,[status(thm)],[c_4,c_811]) ).
cnf(c_812,plain,
multiply(A,add(n0,multiply(A,n1))) = add(multiply(A,n1),add(multiply(n0,n1),multiply(n0,n0))),
inference(paramod,[status(thm)],[c_199,c_58]) ).
cnf(c_230,plain,
multiply(A,A) = add(multiply(A,n1),add(multiply(n0,n1),multiply(n0,n0))),
inference(paramod,[status(thm)],[c_25,c_812]) ).
cnf(c_813,plain,
add(add(n0,multiply(A,n1)),multiply(n0,add(n1,n0))) = add(n0,A),
inference(paramod,[status(thm)],[c_11,c_48]) ).
cnf(c_814,plain,
add(A,multiply(n0,add(n1,n0))) = add(n0,A),
inference(paramod,[status(thm)],[c_25,c_813]) ).
cnf(c_248,plain,
add(n0,A) = add(A,multiply(n0,add(n1,n0))),
inference(copy,[status(thm)],[c_814]) ).
cnf(c_815,plain,
add(multiply(A,A),multiply(multiply(A,n1),add(n0,multiply(A,n1)))) = add(multiply(A,n1),multiply(n0,add(n0,multiply(A,n1)))),
inference(paramod,[status(thm)],[c_199,c_48]) ).
cnf(c_816,plain,
add(multiply(A,A),multiply(multiply(A,n1),A)) = add(multiply(A,n1),multiply(n0,add(n0,multiply(A,n1)))),
inference(paramod,[status(thm)],[c_25,c_815]) ).
cnf(c_252,plain,
add(multiply(A,A),multiply(multiply(A,n1),A)) = add(multiply(A,n1),multiply(n0,A)),
inference(paramod,[status(thm)],[c_25,c_816]) ).
cnf(c_817,plain,
multiply(add(A,n0),add(B,n0)) = add(multiply(A,B),multiply(n0,add(n1,n0))),
inference(paramod,[status(thm)],[c_248,c_4]) ).
cnf(c_818,plain,
add(n0,multiply(A,B)) = add(multiply(A,B),multiply(n0,add(n1,n0))),
inference(paramod,[status(thm)],[c_4,c_817]) ).
cnf(c_261,plain,
add(multiply(A,B),multiply(n0,add(n1,n0))) = add(n0,multiply(A,B)),
inference(copy,[status(thm)],[c_818]) ).
cnf(c_819,plain,
multiply(n1,add(n0,multiply(n0,add(n1,n0)))) = n0,
inference(paramod,[status(thm)],[c_248,c_11]) ).
cnf(c_262,plain,
add(multiply(n0,add(n1,n0)),multiply(n1,n0)) = n0,
inference(paramod,[status(thm)],[c_70,c_819]) ).
cnf(c_267,plain,
add(n0,n1) = n1,
inference(paramod,[status(thm)],[c_248,c_51]) ).
cnf(c_820,plain,
multiply(inverse(A),add(A,A)) = add(n0,multiply(n0,add(n1,n0))),
inference(paramod,[status(thm)],[c_248,c_99]) ).
cnf(c_821,plain,
add(n0,n0) = add(n0,multiply(n0,add(n1,n0))),
inference(paramod,[status(thm)],[c_99,c_820]) ).
cnf(c_275,plain,
add(n0,multiply(n0,add(n1,n0))) = add(n0,n0),
inference(copy,[status(thm)],[c_821]) ).
cnf(c_822,plain,
multiply(A,add(add(n1,n0),multiply(A,n1))) = add(n0,multiply(A,n1)),
inference(paramod,[status(thm)],[c_248,c_58]) ).
cnf(c_286,plain,
multiply(A,add(add(n1,n0),multiply(A,n1))) = A,
inference(paramod,[status(thm)],[c_25,c_822]) ).
cnf(c_288,plain,
add(add(n0,multiply(n1,n0)),multiply(n0,add(n0,n0))) = add(n0,n0),
inference(paramod,[status(thm)],[c_248,c_48]) ).
cnf(c_290,plain,
multiply(A,n1) = add(multiply(n0,A),multiply(n1,A)),
inference(paramod,[status(thm)],[c_267,c_1]) ).
cnf(c_291,plain,
multiply(n1,add(A,n1)) = add(n1,multiply(n0,A)),
inference(paramod,[status(thm)],[c_267,c_4]) ).
cnf(c_823,plain,
multiply(n1,n1) = add(add(multiply(n0,A),multiply(n1,A)),multiply(inverse(A),add(n0,n1))),
inference(paramod,[status(thm)],[c_267,c_37]) ).
cnf(c_824,plain,
multiply(n1,n1) = add(add(multiply(n0,A),multiply(n1,A)),multiply(inverse(A),n1)),
inference(paramod,[status(thm)],[c_267,c_823]) ).
cnf(c_296,plain,
add(add(multiply(n0,A),multiply(n1,A)),multiply(inverse(A),n1)) = multiply(n1,n1),
inference(copy,[status(thm)],[c_824]) ).
cnf(c_309,plain,
multiply(n1,add(n1,inverse(A))) = add(inverse(A),add(multiply(n0,A),multiply(n1,A))),
inference(paramod,[status(thm)],[c_290,c_20]) ).
cnf(c_825,plain,
multiply(n1,A) = add(add(multiply(n0,n0),multiply(n1,n0)),multiply(multiply(A,n1),n1)),
inference(paramod,[status(thm)],[c_290,c_57]) ).
cnf(c_316,plain,
add(add(multiply(n0,n0),multiply(n1,n0)),multiply(multiply(A,n1),n1)) = multiply(n1,A),
inference(copy,[status(thm)],[c_825]) ).
cnf(c_826,plain,
add(add(multiply(n0,n0),multiply(n1,n0)),multiply(n1,n1)) = multiply(n1,n1),
inference(paramod,[status(thm)],[c_290,c_168]) ).
cnf(c_827,plain,
add(n1,multiply(n0,n0)) = multiply(n1,n1),
inference(paramod,[status(thm)],[c_196,c_826]) ).
cnf(c_319,plain,
multiply(n1,n1) = add(n1,multiply(n0,n0)),
inference(copy,[status(thm)],[c_827]) ).
cnf(c_828,plain,
multiply(n0,n1) = add(add(multiply(n0,n1),multiply(n0,n0)),multiply(n1,n0)),
inference(paramod,[status(thm)],[c_199,c_290]) ).
cnf(c_324,plain,
add(add(multiply(n0,n1),multiply(n0,n0)),multiply(n1,n0)) = multiply(n0,n1),
inference(copy,[status(thm)],[c_828]) ).
cnf(c_337,plain,
add(add(multiply(n0,A),multiply(n1,A)),multiply(inverse(A),n1)) = add(n1,multiply(n0,n0)),
inference(paramod,[status(thm)],[c_319,c_296]) ).
cnf(c_342,plain,
add(multiply(inverse(add(n1,n0)),inverse(n1)),n0) = multiply(inverse(n1),add(n1,multiply(n0,n0))),
inference(paramod,[status(thm)],[c_319,c_148]) ).
cnf(c_349,plain,
multiply(n1,add(n1,multiply(n0,n1))) = add(n1,multiply(n0,n0)),
inference(paramod,[status(thm)],[c_319,c_117]) ).
cnf(c_361,plain,
multiply(n1,add(n1,add(n1,multiply(n0,n0)))) = n1,
inference(paramod,[status(thm)],[c_319,c_64]) ).
cnf(c_829,plain,
multiply(n1,add(n1,n1)) = add(n1,add(multiply(n0,n0),multiply(n1,n0))),
inference(paramod,[status(thm)],[c_290,c_291]) ).
cnf(c_830,plain,
add(n1,multiply(n0,n1)) = add(n1,add(multiply(n0,n0),multiply(n1,n0))),
inference(paramod,[status(thm)],[c_291,c_829]) ).
cnf(c_367,plain,
add(n1,add(multiply(n0,n0),multiply(n1,n0))) = add(n1,multiply(n0,n1)),
inference(copy,[status(thm)],[c_830]) ).
cnf(c_377,plain,
add(add(multiply(n1,n0),multiply(n0,n0)),multiply(n1,n0)) = n0,
inference(paramod,[status(thm)],[c_1,c_262]) ).
cnf(c_831,plain,
add(multiply(n0,add(n1,n0)),add(multiply(n0,n1),multiply(multiply(n0,n1),n1))) = n0,
inference(paramod,[status(thm)],[c_57,c_262]) ).
cnf(c_832,plain,
add(multiply(n0,add(n1,n0)),multiply(n0,add(n1,multiply(n0,n1)))) = n0,
inference(paramod,[status(thm)],[c_62,c_831]) ).
cnf(c_379,plain,
add(multiply(n0,add(n1,n0)),n0) = n0,
inference(paramod,[status(thm)],[c_64,c_832]) ).
cnf(c_384,plain,
multiply(n1,n0) = multiply(n0,add(n1,n0)),
inference(paramod,[status(thm)],[c_379,c_11]) ).
cnf(c_385,plain,
add(multiply(n0,add(n1,n0)),multiply(n0,n0)) = multiply(n0,add(n1,n0)),
inference(paramod,[status(thm)],[c_379,c_51]) ).
cnf(c_833,plain,
add(add(multiply(n0,add(n1,n0)),multiply(n0,n0)),multiply(n1,n0)) = n0,
inference(paramod,[status(thm)],[c_384,c_377]) ).
cnf(c_834,plain,
add(multiply(n0,add(n1,n0)),multiply(n1,n0)) = n0,
inference(paramod,[status(thm)],[c_385,c_833]) ).
cnf(c_835,plain,
add(multiply(n0,add(n1,n0)),multiply(n0,add(n1,n0))) = n0,
inference(paramod,[status(thm)],[c_384,c_834]) ).
cnf(c_836,plain,
add(n0,multiply(n0,add(n1,n0))) = n0,
inference(paramod,[status(thm)],[c_261,c_835]) ).
cnf(c_389,plain,
add(n0,n0) = n0,
inference(paramod,[status(thm)],[c_275,c_836]) ).
cnf(c_837,plain,
add(n1,add(multiply(n0,n0),multiply(n0,add(n1,n0)))) = add(n1,multiply(n0,n1)),
inference(paramod,[status(thm)],[c_384,c_367]) ).
cnf(c_838,plain,
add(n1,add(n0,multiply(n0,n0))) = add(n1,multiply(n0,n1)),
inference(paramod,[status(thm)],[c_261,c_837]) ).
cnf(c_390,plain,
add(n1,multiply(n0,n1)) = add(n1,add(n0,multiply(n0,n0))),
inference(copy,[status(thm)],[c_838]) ).
cnf(c_391,plain,
add(add(multiply(n0,n1),multiply(n0,n0)),multiply(n0,add(n1,n0))) = multiply(n0,n1),
inference(paramod,[status(thm)],[c_384,c_324]) ).
cnf(c_839,plain,
add(add(multiply(n0,n0),multiply(n0,add(n1,n0))),multiply(multiply(A,n1),n1)) = multiply(n1,A),
inference(paramod,[status(thm)],[c_384,c_316]) ).
cnf(c_392,plain,
add(add(n0,multiply(n0,n0)),multiply(multiply(A,n1),n1)) = multiply(n1,A),
inference(paramod,[status(thm)],[c_261,c_839]) ).
cnf(c_840,plain,
add(add(n0,multiply(n0,add(n1,n0))),multiply(n0,add(n0,n0))) = add(n0,n0),
inference(paramod,[status(thm)],[c_384,c_288]) ).
cnf(c_841,plain,
add(add(n0,n0),multiply(n0,add(n0,n0))) = add(n0,n0),
inference(paramod,[status(thm)],[c_275,c_840]) ).
cnf(c_842,plain,
add(n0,multiply(n0,add(n0,n0))) = add(n0,n0),
inference(paramod,[status(thm)],[c_389,c_841]) ).
cnf(c_843,plain,
add(n0,multiply(n0,n0)) = add(n0,n0),
inference(paramod,[status(thm)],[c_389,c_842]) ).
cnf(c_394,plain,
add(n0,multiply(n0,n0)) = n0,
inference(paramod,[status(thm)],[c_389,c_843]) ).
cnf(c_844,plain,
multiply(n1,add(n1,add(n0,multiply(n0,n0)))) = add(n1,multiply(n0,n0)),
inference(paramod,[status(thm)],[c_390,c_349]) ).
cnf(c_845,plain,
multiply(n1,add(n1,n0)) = add(n1,multiply(n0,n0)),
inference(paramod,[status(thm)],[c_394,c_844]) ).
cnf(c_846,plain,
n1 = add(n1,multiply(n0,n0)),
inference(paramod,[status(thm)],[c_11,c_845]) ).
cnf(c_409,plain,
add(n1,multiply(n0,n0)) = n1,
inference(copy,[status(thm)],[c_846]) ).
cnf(c_847,plain,
multiply(A,add(add(n1,add(n0,multiply(n0,n0))),multiply(A,n1))) = add(multiply(A,n1),n0),
inference(paramod,[status(thm)],[c_390,c_202]) ).
cnf(c_848,plain,
multiply(A,add(add(n1,n0),multiply(A,n1))) = add(multiply(A,n1),n0),
inference(paramod,[status(thm)],[c_394,c_847]) ).
cnf(c_849,plain,
A = add(multiply(A,n1),n0),
inference(paramod,[status(thm)],[c_286,c_848]) ).
cnf(c_412,plain,
add(multiply(A,n1),n0) = A,
inference(copy,[status(thm)],[c_849]) ).
cnf(c_850,plain,
add(n0,multiply(multiply(A,n1),n1)) = multiply(n1,A),
inference(paramod,[status(thm)],[c_394,c_392]) ).
cnf(c_851,plain,
multiply(A,n1) = multiply(n1,A),
inference(paramod,[status(thm)],[c_25,c_850]) ).
cnf(c_414,plain,
multiply(n1,A) = multiply(A,n1),
inference(copy,[status(thm)],[c_851]) ).
cnf(c_415,plain,
add(n1,multiply(n0,n1)) = add(n1,n0),
inference(paramod,[status(thm)],[c_394,c_390]) ).
cnf(c_852,plain,
multiply(n1,add(n1,n1)) = n1,
inference(paramod,[status(thm)],[c_409,c_361]) ).
cnf(c_853,plain,
add(n1,multiply(n0,n1)) = n1,
inference(paramod,[status(thm)],[c_291,c_852]) ).
cnf(c_420,plain,
add(n1,n0) = n1,
inference(paramod,[status(thm)],[c_415,c_853]) ).
cnf(c_854,plain,
add(multiply(inverse(n1),inverse(n1)),n0) = multiply(inverse(n1),add(n1,multiply(n0,n0))),
inference(paramod,[status(thm)],[c_420,c_342]) ).
cnf(c_855,plain,
add(multiply(inverse(n1),inverse(n1)),n0) = multiply(inverse(n1),n1),
inference(paramod,[status(thm)],[c_409,c_854]) ).
cnf(c_856,plain,
add(multiply(inverse(n1),inverse(n1)),n0) = multiply(n1,inverse(n1)),
inference(paramod,[status(thm)],[c_414,c_855]) ).
cnf(c_433,plain,
add(multiply(inverse(n1),inverse(n1)),n0) = n0,
inference(paramod,[status(thm)],[c_5,c_856]) ).
cnf(c_857,plain,
add(add(multiply(n0,A),multiply(n1,A)),multiply(n1,inverse(A))) = add(n1,multiply(n0,n0)),
inference(paramod,[status(thm)],[c_414,c_337]) ).
cnf(c_436,plain,
add(add(multiply(n0,A),multiply(n1,A)),multiply(n1,inverse(A))) = n1,
inference(paramod,[status(thm)],[c_409,c_857]) ).
cnf(c_442,plain,
multiply(A,add(A,multiply(A,n1))) = multiply(A,n1),
inference(paramod,[status(thm)],[c_412,c_201]) ).
cnf(c_462,plain,
add(n0,multiply(inverse(A),inverse(A))) = multiply(n1,inverse(A)),
inference(paramod,[status(thm)],[c_414,c_39]) ).
cnf(c_467,plain,
add(add(multiply(n0,n1),multiply(n0,n0)),multiply(n0,n1)) = multiply(n0,n1),
inference(paramod,[status(thm)],[c_420,c_391]) ).
cnf(c_858,plain,
add(multiply(n0,n1),multiply(n0,n0)) = multiply(n0,add(n1,n0)),
inference(paramod,[status(thm)],[c_420,c_385]) ).
cnf(c_468,plain,
add(multiply(n0,n1),multiply(n0,n0)) = multiply(n0,n1),
inference(paramod,[status(thm)],[c_420,c_858]) ).
cnf(c_490,plain,
add(multiply(A,B),multiply(n0,n1)) = add(n0,multiply(A,B)),
inference(paramod,[status(thm)],[c_420,c_261]) ).
cnf(c_496,plain,
add(n0,A) = add(A,multiply(n0,n1)),
inference(paramod,[status(thm)],[c_420,c_248]) ).
cnf(c_859,plain,
add(multiply(n0,n1),multiply(n0,n1)) = multiply(n0,n1),
inference(paramod,[status(thm)],[c_468,c_467]) ).
cnf(c_860,plain,
add(n0,multiply(n0,n1)) = multiply(n0,n1),
inference(paramod,[status(thm)],[c_490,c_859]) ).
cnf(c_861,plain,
n0 = multiply(n0,n1),
inference(paramod,[status(thm)],[c_25,c_860]) ).
cnf(c_498,plain,
multiply(n0,n1) = n0,
inference(copy,[status(thm)],[c_861]) ).
cnf(c_862,plain,
multiply(A,A) = add(multiply(A,n1),add(n0,multiply(n0,n0))),
inference(paramod,[status(thm)],[c_498,c_230]) ).
cnf(c_863,plain,
multiply(A,A) = add(multiply(A,n1),n0),
inference(paramod,[status(thm)],[c_394,c_862]) ).
cnf(c_499,plain,
multiply(A,A) = A,
inference(paramod,[status(thm)],[c_412,c_863]) ).
cnf(c_505,plain,
add(n0,A) = add(A,n0),
inference(paramod,[status(thm)],[c_498,c_496]) ).
cnf(c_864,plain,
add(n0,inverse(A)) = multiply(n1,inverse(A)),
inference(paramod,[status(thm)],[c_499,c_462]) ).
cnf(c_523,plain,
multiply(n1,inverse(A)) = add(n0,inverse(A)),
inference(copy,[status(thm)],[c_864]) ).
cnf(c_865,plain,
add(inverse(n1),n0) = n0,
inference(paramod,[status(thm)],[c_499,c_433]) ).
cnf(c_527,plain,
add(n0,inverse(n1)) = n0,
inference(paramod,[status(thm)],[c_505,c_865]) ).
cnf(c_533,plain,
add(A,multiply(multiply(A,n1),A)) = add(multiply(A,n1),multiply(n0,A)),
inference(paramod,[status(thm)],[c_499,c_252]) ).
cnf(c_866,plain,
add(inverse(A),B) = add(add(inverse(A),multiply(B,A)),multiply(n0,n0)),
inference(paramod,[status(thm)],[c_499,c_223]) ).
cnf(c_867,plain,
add(inverse(A),B) = add(add(inverse(A),multiply(B,A)),n0),
inference(paramod,[status(thm)],[c_499,c_866]) ).
cnf(c_868,plain,
add(inverse(A),B) = add(n0,add(inverse(A),multiply(B,A))),
inference(paramod,[status(thm)],[c_505,c_867]) ).
cnf(c_536,plain,
add(n0,add(inverse(A),multiply(B,A))) = add(inverse(A),B),
inference(copy,[status(thm)],[c_868]) ).
cnf(c_869,plain,
multiply(A,add(A,B)) = add(add(multiply(A,n1),n0),multiply(B,A)),
inference(paramod,[status(thm)],[c_499,c_213]) ).
cnf(c_870,plain,
multiply(A,add(A,B)) = add(add(n0,multiply(A,n1)),multiply(B,A)),
inference(paramod,[status(thm)],[c_505,c_869]) ).
cnf(c_539,plain,
multiply(A,add(A,B)) = add(A,multiply(B,A)),
inference(paramod,[status(thm)],[c_25,c_870]) ).
cnf(c_871,plain,
add(inverse(n1),add(inverse(n1),n0)) = inverse(n1),
inference(paramod,[status(thm)],[c_499,c_137]) ).
cnf(c_872,plain,
add(inverse(n1),add(n0,inverse(n1))) = inverse(n1),
inference(paramod,[status(thm)],[c_505,c_871]) ).
cnf(c_873,plain,
add(inverse(n1),n0) = inverse(n1),
inference(paramod,[status(thm)],[c_527,c_872]) ).
cnf(c_874,plain,
add(n0,inverse(n1)) = inverse(n1),
inference(paramod,[status(thm)],[c_505,c_873]) ).
cnf(c_875,plain,
n0 = inverse(n1),
inference(paramod,[status(thm)],[c_527,c_874]) ).
cnf(c_540,plain,
inverse(n1) = n0,
inference(copy,[status(thm)],[c_875]) ).
cnf(c_876,plain,
multiply(n1,add(add(n0,inverse(n0)),inverse(n0))) = inverse(n0),
inference(paramod,[status(thm)],[c_505,c_88]) ).
cnf(c_877,plain,
multiply(n1,add(n1,inverse(n0))) = inverse(n0),
inference(paramod,[status(thm)],[c_2,c_876]) ).
cnf(c_878,plain,
add(inverse(n0),add(multiply(n0,n0),multiply(n1,n0))) = inverse(n0),
inference(paramod,[status(thm)],[c_309,c_877]) ).
cnf(c_879,plain,
add(inverse(n0),add(n0,multiply(n1,n0))) = inverse(n0),
inference(paramod,[status(thm)],[c_499,c_878]) ).
cnf(c_880,plain,
add(inverse(n0),add(n0,multiply(n0,n1))) = inverse(n0),
inference(paramod,[status(thm)],[c_414,c_879]) ).
cnf(c_881,plain,
add(inverse(n0),add(n0,n0)) = inverse(n0),
inference(paramod,[status(thm)],[c_498,c_880]) ).
cnf(c_882,plain,
add(inverse(n0),n0) = inverse(n0),
inference(paramod,[status(thm)],[c_389,c_881]) ).
cnf(c_883,plain,
add(n0,inverse(n0)) = inverse(n0),
inference(paramod,[status(thm)],[c_505,c_882]) ).
cnf(c_884,plain,
n1 = inverse(n0),
inference(paramod,[status(thm)],[c_2,c_883]) ).
cnf(c_551,plain,
inverse(n0) = n1,
inference(copy,[status(thm)],[c_884]) ).
cnf(c_552,plain,
multiply(n1,add(inverse(A),inverse(A))) = add(n0,inverse(A)),
inference(paramod,[status(thm)],[c_505,c_85]) ).
cnf(c_566,plain,
add(add(multiply(n0,A),multiply(n1,A)),add(n0,inverse(A))) = n1,
inference(paramod,[status(thm)],[c_523,c_436]) ).
cnf(c_574,plain,
add(inverse(A),B) = add(B,inverse(A)),
inference(paramod,[status(thm)],[c_536,c_50]) ).
cnf(c_885,plain,
multiply(A,add(A,multiply(A,n1))) = add(multiply(A,n1),multiply(n0,A)),
inference(paramod,[status(thm)],[c_539,c_533]) ).
cnf(c_886,plain,
multiply(A,n1) = add(multiply(A,n1),multiply(n0,A)),
inference(paramod,[status(thm)],[c_442,c_885]) ).
cnf(c_576,plain,
add(multiply(A,n1),multiply(n0,A)) = multiply(A,n1),
inference(copy,[status(thm)],[c_886]) ).
cnf(c_588,plain,
multiply(n1,add(n1,inverse(A))) = add(add(multiply(n0,A),multiply(n1,A)),inverse(A)),
inference(paramod,[status(thm)],[c_574,c_309]) ).
cnf(c_887,plain,
multiply(n0,add(n1,A)) = add(n0,multiply(A,inverse(n1))),
inference(paramod,[status(thm)],[c_540,c_22]) ).
cnf(c_591,plain,
multiply(n0,add(n1,A)) = add(n0,multiply(A,n0)),
inference(paramod,[status(thm)],[c_540,c_887]) ).
cnf(c_888,plain,
multiply(add(multiply(n1,A),multiply(multiply(A,n1),A)),n0) = add(multiply(n0,n1),multiply(multiply(A,n1),n0)),
inference(paramod,[status(thm)],[c_60,c_59]) ).
cnf(c_889,plain,
multiply(A,n0) = add(multiply(n0,n1),multiply(multiply(A,n1),n0)),
inference(paramod,[status(thm)],[c_67,c_888]) ).
cnf(c_890,plain,
multiply(A,n0) = add(n0,multiply(multiply(A,n1),n0)),
inference(paramod,[status(thm)],[c_498,c_889]) ).
cnf(c_891,plain,
multiply(A,n0) = multiply(n0,add(n0,multiply(A,n1))),
inference(paramod,[status(thm)],[c_539,c_890]) ).
cnf(c_892,plain,
multiply(A,n0) = multiply(n0,A),
inference(paramod,[status(thm)],[c_25,c_891]) ).
cnf(c_599,plain,
multiply(n0,A) = multiply(A,n0),
inference(copy,[status(thm)],[c_892]) ).
cnf(c_893,plain,
multiply(n1,add(n0,A)) = add(n0,multiply(A,inverse(n0))),
inference(paramod,[status(thm)],[c_551,c_22]) ).
cnf(c_894,plain,
multiply(n1,add(n0,A)) = add(n0,multiply(A,n1)),
inference(paramod,[status(thm)],[c_551,c_893]) ).
cnf(c_611,plain,
multiply(n1,add(n0,A)) = A,
inference(paramod,[status(thm)],[c_25,c_894]) ).
cnf(c_619,plain,
add(A,multiply(B,n0)) = add(A,add(multiply(n0,B),multiply(n0,B))),
inference(paramod,[status(thm)],[c_389,c_19]) ).
cnf(c_895,plain,
add(A,B) = add(B,multiply(A,A)),
inference(paramod,[status(thm)],[c_499,c_4]) ).
cnf(c_626,plain,
add(A,B) = add(B,A),
inference(paramod,[status(thm)],[c_499,c_895]) ).
cnf(c_896,plain,
multiply(add(inverse(A),inverse(A)),add(A,inverse(A))) = inverse(A),
inference(paramod,[status(thm)],[c_499,c_13]) ).
cnf(c_897,plain,
multiply(add(inverse(A),inverse(A)),n1) = inverse(A),
inference(paramod,[status(thm)],[c_2,c_896]) ).
cnf(c_898,plain,
multiply(n1,add(inverse(A),inverse(A))) = inverse(A),
inference(paramod,[status(thm)],[c_414,c_897]) ).
cnf(c_627,plain,
add(n0,inverse(A)) = inverse(A),
inference(paramod,[status(thm)],[c_552,c_898]) ).
cnf(c_899,plain,
multiply(multiply(A,n1),A) = add(multiply(n0,multiply(A,n1)),multiply(A,n1)),
inference(paramod,[status(thm)],[c_499,c_57]) ).
cnf(c_632,plain,
multiply(multiply(A,n1),A) = add(multiply(A,n1),multiply(n0,multiply(A,n1))),
inference(paramod,[status(thm)],[c_626,c_899]) ).
cnf(c_900,plain,
add(multiply(A,n1),multiply(n0,A)) = add(A,multiply(multiply(A,n1),A)),
inference(paramod,[status(thm)],[c_499,c_60]) ).
cnf(c_901,plain,
multiply(A,n1) = add(A,multiply(multiply(A,n1),A)),
inference(paramod,[status(thm)],[c_576,c_900]) ).
cnf(c_902,plain,
multiply(A,n1) = add(A,add(multiply(A,n1),multiply(n0,multiply(A,n1)))),
inference(paramod,[status(thm)],[c_632,c_901]) ).
cnf(c_638,plain,
add(A,add(multiply(A,n1),multiply(n0,multiply(A,n1)))) = multiply(A,n1),
inference(copy,[status(thm)],[c_902]) ).
cnf(c_657,plain,
add(add(multiply(n0,A),multiply(n1,A)),inverse(A)) = n1,
inference(paramod,[status(thm)],[c_627,c_566]) ).
cnf(c_663,plain,
multiply(n1,inverse(A)) = inverse(A),
inference(paramod,[status(thm)],[c_627,c_523]) ).
cnf(c_668,plain,
multiply(n1,add(n1,inverse(A))) = n1,
inference(paramod,[status(thm)],[c_657,c_588]) ).
cnf(c_903,plain,
add(multiply(add(n1,multiply(inverse(A),n1)),add(inverse(A),A)),multiply(A,add(inverse(A),A))) = n1,
inference(paramod,[status(thm)],[c_2,c_77]) ).
cnf(c_904,plain,
add(multiply(add(n1,multiply(n1,inverse(A))),add(inverse(A),A)),multiply(A,add(inverse(A),A))) = n1,
inference(paramod,[status(thm)],[c_414,c_903]) ).
cnf(c_905,plain,
add(multiply(add(n1,inverse(A)),add(inverse(A),A)),multiply(A,add(inverse(A),A))) = n1,
inference(paramod,[status(thm)],[c_663,c_904]) ).
cnf(c_906,plain,
add(multiply(add(n1,inverse(A)),add(A,inverse(A))),multiply(A,add(inverse(A),A))) = n1,
inference(paramod,[status(thm)],[c_626,c_905]) ).
cnf(c_907,plain,
add(multiply(add(n1,inverse(A)),n1),multiply(A,add(inverse(A),A))) = n1,
inference(paramod,[status(thm)],[c_2,c_906]) ).
cnf(c_908,plain,
add(multiply(n1,add(n1,inverse(A))),multiply(A,add(inverse(A),A))) = n1,
inference(paramod,[status(thm)],[c_414,c_907]) ).
cnf(c_909,plain,
add(n1,multiply(A,add(inverse(A),A))) = n1,
inference(paramod,[status(thm)],[c_668,c_908]) ).
cnf(c_910,plain,
add(n1,multiply(A,add(A,inverse(A)))) = n1,
inference(paramod,[status(thm)],[c_626,c_909]) ).
cnf(c_675,plain,
add(n1,multiply(A,n1)) = n1,
inference(paramod,[status(thm)],[c_2,c_910]) ).
cnf(c_911,plain,
add(A,B) = add(A,multiply(B,add(n1,multiply(B,n1)))),
inference(paramod,[status(thm)],[c_77,c_18]) ).
cnf(c_912,plain,
add(A,B) = add(A,multiply(B,n1)),
inference(paramod,[status(thm)],[c_675,c_911]) ).
cnf(c_677,plain,
add(A,multiply(B,n1)) = add(A,B),
inference(copy,[status(thm)],[c_912]) ).
cnf(c_913,plain,
add(multiply(add(n1,multiply(n0,n1)),add(n0,multiply(A,n1))),multiply(multiply(A,n1),A)) = add(multiply(A,n1),n0),
inference(paramod,[status(thm)],[c_25,c_77]) ).
cnf(c_914,plain,
add(multiply(add(n1,n0),add(n0,multiply(A,n1))),multiply(multiply(A,n1),A)) = add(multiply(A,n1),n0),
inference(paramod,[status(thm)],[c_498,c_913]) ).
cnf(c_915,plain,
add(multiply(add(n0,n1),add(n0,multiply(A,n1))),multiply(multiply(A,n1),A)) = add(multiply(A,n1),n0),
inference(paramod,[status(thm)],[c_626,c_914]) ).
cnf(c_916,plain,
add(multiply(n1,add(n0,multiply(A,n1))),multiply(multiply(A,n1),A)) = add(multiply(A,n1),n0),
inference(paramod,[status(thm)],[c_267,c_915]) ).
cnf(c_917,plain,
add(multiply(n1,add(n0,A)),multiply(multiply(A,n1),A)) = add(multiply(A,n1),n0),
inference(paramod,[status(thm)],[c_677,c_916]) ).
cnf(c_918,plain,
add(A,multiply(multiply(A,n1),A)) = add(multiply(A,n1),n0),
inference(paramod,[status(thm)],[c_611,c_917]) ).
cnf(c_919,plain,
add(A,add(multiply(A,n1),multiply(n0,multiply(A,n1)))) = add(multiply(A,n1),n0),
inference(paramod,[status(thm)],[c_632,c_918]) ).
cnf(c_920,plain,
multiply(A,n1) = add(multiply(A,n1),n0),
inference(paramod,[status(thm)],[c_638,c_919]) ).
cnf(c_921,plain,
multiply(A,n1) = add(n0,multiply(A,n1)),
inference(paramod,[status(thm)],[c_626,c_920]) ).
cnf(c_679,plain,
multiply(A,n1) = add(n0,A),
inference(paramod,[status(thm)],[c_677,c_921]) ).
cnf(c_689,plain,
add(n1,add(n0,A)) = n1,
inference(paramod,[status(thm)],[c_679,c_675]) ).
cnf(c_922,plain,
multiply(A,add(A,add(n0,A))) = multiply(A,n1),
inference(paramod,[status(thm)],[c_679,c_442]) ).
cnf(c_694,plain,
multiply(A,add(A,add(n0,A))) = add(n0,A),
inference(paramod,[status(thm)],[c_679,c_922]) ).
cnf(c_923,plain,
multiply(add(A,add(n0,B)),B) = add(multiply(B,n1),multiply(A,n0)),
inference(paramod,[status(thm)],[c_679,c_59]) ).
cnf(c_697,plain,
multiply(add(A,add(n0,B)),B) = add(add(n0,B),multiply(A,n0)),
inference(paramod,[status(thm)],[c_679,c_923]) ).
cnf(c_700,plain,
add(A,add(n0,B)) = add(A,B),
inference(paramod,[status(thm)],[c_679,c_677]) ).
cnf(c_716,plain,
multiply(n1,A) = add(n0,A),
inference(paramod,[status(thm)],[c_679,c_414]) ).
cnf(c_924,plain,
add(n0,add(n0,A)) = A,
inference(paramod,[status(thm)],[c_716,c_611]) ).
cnf(c_736,plain,
add(n0,A) = A,
inference(paramod,[status(thm)],[c_700,c_924]) ).
cnf(c_925,plain,
add(n0,add(A,n0)) = A,
inference(paramod,[status(thm)],[c_716,c_11]) ).
cnf(c_742,plain,
add(A,n0) = A,
inference(paramod,[status(thm)],[c_736,c_925]) ).
cnf(c_926,plain,
multiply(add(A,B),B) = add(add(n0,B),multiply(A,n0)),
inference(paramod,[status(thm)],[c_736,c_697]) ).
cnf(c_743,plain,
multiply(add(A,B),B) = add(B,multiply(A,n0)),
inference(paramod,[status(thm)],[c_736,c_926]) ).
cnf(c_927,plain,
multiply(A,add(A,A)) = add(n0,A),
inference(paramod,[status(thm)],[c_736,c_694]) ).
cnf(c_928,plain,
add(A,multiply(A,A)) = add(n0,A),
inference(paramod,[status(thm)],[c_539,c_927]) ).
cnf(c_929,plain,
add(A,A) = add(n0,A),
inference(paramod,[status(thm)],[c_499,c_928]) ).
cnf(c_744,plain,
add(A,A) = A,
inference(paramod,[status(thm)],[c_736,c_929]) ).
cnf(c_745,plain,
add(n1,A) = n1,
inference(paramod,[status(thm)],[c_736,c_689]) ).
cnf(c_769,plain,
multiply(A,n1) = A,
inference(paramod,[status(thm)],[c_736,c_679]) ).
cnf(c_930,plain,
multiply(n0,n1) = add(n0,multiply(A,n0)),
inference(paramod,[status(thm)],[c_745,c_591]) ).
cnf(c_931,plain,
n0 = add(n0,multiply(A,n0)),
inference(paramod,[status(thm)],[c_769,c_930]) ).
cnf(c_932,plain,
n0 = multiply(A,n0),
inference(paramod,[status(thm)],[c_736,c_931]) ).
cnf(c_772,plain,
multiply(A,n0) = n0,
inference(copy,[status(thm)],[c_932]) ).
cnf(c_933,plain,
add(b,multiply(a,n0)) != b,
inference(paramod,[status(thm)],[c_743,c_16]) ).
cnf(c_783,plain,
add(b,multiply(n0,a)) != b,
inference(paramod,[status(thm)],[c_599,c_933]) ).
cnf(c_934,plain,
add(A,n0) = add(A,add(multiply(n0,B),multiply(n0,B))),
inference(paramod,[status(thm)],[c_772,c_619]) ).
cnf(c_935,plain,
A = add(A,add(multiply(n0,B),multiply(n0,B))),
inference(paramod,[status(thm)],[c_742,c_934]) ).
cnf(c_936,plain,
A = add(A,multiply(n0,B)),
inference(paramod,[status(thm)],[c_744,c_935]) ).
cnf(c_785,plain,
add(A,multiply(n0,B)) = A,
inference(copy,[status(thm)],[c_936]) ).
cnf(c_786,plain,
$false,
inference(resolve,[status(thm)],[c_785,c_783]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : BOO026-1 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n020.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sat Sep 26 22:38:04 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.38 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.38 % Process 2694037 was started by sandbox2 on n020,
% 0.10/0.38 % Sat Sep 26 22:38:04 2026
% 0.10/0.38 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.10/0.38
% 0.10/0.38 % From the command line: assign(max_seconds, 300).
% 2.56/0.74
% 2.56/0.74 % SZS status Unsatisfiable for theBenchmark
% 2.56/0.74
% 2.56/0.74 % Proof 1 at 0.24 (+ 0.09) seconds.
% 2.56/0.74 % Length of proof is 145.
% 2.56/0.74 % Level of proof is 29.
% 2.56/0.74 % Maximum clause weight is 30.000.
% 2.56/0.74 % Given clauses 87.
% 2.56/0.74
% 2.56/0.74 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------