%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : BOO008-4 : TPTP v9.3.1. Released v1.1.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/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 06:55:03 AM UTC 2026
% Result : Unsatisfiable 11.17s 1.89s
% Output : CNFRefutation 11.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 70
% Number of leaves : 9
% Syntax : Number of formulae : 342 ( 342 unt; 0 def)
% Number of atoms : 342 ( 341 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 5 ( 5 ~; 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 : 8 ( 8 usr; 5 con; 0-2 aty)
% Number of variables : 685 ( 92 sgn 14 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(commutativity_of_add,axiom,
! [VAR_0,VAR_1] : add(VAR_0,VAR_1) = add(VAR_1,VAR_0),
file('theBenchmark.p',commutativity_of_add) ).
cnf(c_1,plain,
add(A,B) = add(B,A),
inference(clausify,[status(thm)],[commutativity_of_add]) ).
fof(commutativity_of_multiply,axiom,
! [VAR_0,VAR_1] : multiply(VAR_0,VAR_1) = multiply(VAR_1,VAR_0),
file('theBenchmark.p',commutativity_of_multiply) ).
cnf(c_2,plain,
multiply(A,B) = multiply(B,A),
inference(clausify,[status(thm)],[commutativity_of_multiply]) ).
fof(distributivity1,axiom,
! [VAR_0,VAR_1,VAR_2] : add(VAR_0,multiply(VAR_1,VAR_2)) = multiply(add(VAR_0,VAR_1),add(VAR_0,VAR_2)),
file('theBenchmark.p',distributivity1) ).
cnf(c_3,plain,
add(A,multiply(B,C)) = multiply(add(A,B),add(A,C)),
inference(clausify,[status(thm)],[distributivity1]) ).
cnf(c_4,plain,
multiply(add(A,B),add(A,C)) = add(A,multiply(B,C)),
inference(copy,[status(thm)],[c_3]) ).
fof(distributivity2,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',distributivity2) ).
cnf(c_5,plain,
multiply(A,add(B,C)) = add(multiply(A,B),multiply(A,C)),
inference(clausify,[status(thm)],[distributivity2]) ).
cnf(c_6,plain,
add(multiply(A,B),multiply(A,C)) = multiply(A,add(B,C)),
inference(copy,[status(thm)],[c_5]) ).
fof(additive_id1,axiom,
! [VAR_0] : add(VAR_0,additive_identity) = VAR_0,
file('theBenchmark.p',additive_id1) ).
cnf(c_7,plain,
add(A,additive_identity) = A,
inference(clausify,[status(thm)],[additive_id1]) ).
fof(multiplicative_id1,axiom,
! [VAR_0] : multiply(VAR_0,multiplicative_identity) = VAR_0,
file('theBenchmark.p',multiplicative_id1) ).
cnf(c_8,plain,
multiply(A,multiplicative_identity) = A,
inference(clausify,[status(thm)],[multiplicative_id1]) ).
fof(additive_inverse1,axiom,
! [VAR_0] : add(VAR_0,inverse(VAR_0)) = multiplicative_identity,
file('theBenchmark.p',additive_inverse1) ).
cnf(c_9,plain,
add(A,inverse(A)) = multiplicative_identity,
inference(clausify,[status(thm)],[additive_inverse1]) ).
fof(multiplicative_inverse1,axiom,
! [VAR_0] : multiply(VAR_0,inverse(VAR_0)) = additive_identity,
file('theBenchmark.p',multiplicative_inverse1) ).
cnf(c_10,plain,
multiply(A,inverse(A)) = additive_identity,
inference(clausify,[status(thm)],[multiplicative_inverse1]) ).
fof(prove_associativity,axiom,
add(a,add(b,c)) != add(add(a,b),c),
file('theBenchmark.p',prove_associativity) ).
cnf(c_11,plain,
add(a,add(b,c)) != add(add(a,b),c),
inference(clausify,[status(thm)],[prove_associativity]) ).
cnf(c_5467,plain,
add(a,add(b,c)) != add(c,add(a,b)),
inference(paramod,[status(thm)],[c_1,c_11]) ).
cnf(c_12,plain,
add(c,add(a,b)) != add(a,add(b,c)),
inference(copy,[status(thm)],[c_5467]) ).
cnf(c_13,plain,
multiply(add(A,B),add(B,C)) = add(B,multiply(A,C)),
inference(paramod,[status(thm)],[c_1,c_4]) ).
cnf(c_14,plain,
multiply(add(A,B),add(C,A)) = add(A,multiply(B,C)),
inference(paramod,[status(thm)],[c_1,c_4]) ).
cnf(c_15,plain,
add(multiply(A,B),multiply(B,C)) = multiply(B,add(A,C)),
inference(paramod,[status(thm)],[c_2,c_6]) ).
cnf(c_16,plain,
add(multiply(A,B),multiply(C,A)) = multiply(A,add(B,C)),
inference(paramod,[status(thm)],[c_2,c_6]) ).
cnf(c_5468,plain,
A = add(additive_identity,A),
inference(paramod,[status(thm)],[c_7,c_1]) ).
cnf(c_21,plain,
add(additive_identity,A) = A,
inference(copy,[status(thm)],[c_5468]) ).
cnf(c_22,plain,
multiply(A,add(A,B)) = add(A,multiply(additive_identity,B)),
inference(paramod,[status(thm)],[c_7,c_4]) ).
cnf(c_5469,plain,
multiply(add(A,B),A) = add(A,multiply(B,additive_identity)),
inference(paramod,[status(thm)],[c_7,c_4]) ).
cnf(c_23,plain,
multiply(A,add(A,B)) = add(A,multiply(B,additive_identity)),
inference(paramod,[status(thm)],[c_2,c_5469]) ).
cnf(c_5470,plain,
A = multiply(multiplicative_identity,A),
inference(paramod,[status(thm)],[c_8,c_2]) ).
cnf(c_24,plain,
multiply(multiplicative_identity,A) = A,
inference(copy,[status(thm)],[c_5470]) ).
cnf(c_5471,plain,
add(A,multiply(A,B)) = multiply(A,add(multiplicative_identity,B)),
inference(paramod,[status(thm)],[c_8,c_6]) ).
cnf(c_25,plain,
multiply(A,add(multiplicative_identity,B)) = add(A,multiply(A,B)),
inference(copy,[status(thm)],[c_5471]) ).
cnf(c_5472,plain,
add(multiply(A,B),A) = multiply(A,add(B,multiplicative_identity)),
inference(paramod,[status(thm)],[c_8,c_6]) ).
cnf(c_5473,plain,
add(A,multiply(A,B)) = multiply(A,add(B,multiplicative_identity)),
inference(paramod,[status(thm)],[c_1,c_5472]) ).
cnf(c_26,plain,
multiply(A,add(B,multiplicative_identity)) = add(A,multiply(A,B)),
inference(copy,[status(thm)],[c_5473]) ).
cnf(c_5474,plain,
multiply(multiplicative_identity,add(A,B)) = add(A,multiply(inverse(A),B)),
inference(paramod,[status(thm)],[c_9,c_4]) ).
cnf(c_5475,plain,
add(A,B) = add(A,multiply(inverse(A),B)),
inference(paramod,[status(thm)],[c_24,c_5474]) ).
cnf(c_27,plain,
add(A,multiply(inverse(A),B)) = add(A,B),
inference(copy,[status(thm)],[c_5475]) ).
cnf(c_5476,plain,
multiply(add(A,B),multiplicative_identity) = add(A,multiply(B,inverse(A))),
inference(paramod,[status(thm)],[c_9,c_4]) ).
cnf(c_5477,plain,
multiply(multiplicative_identity,add(A,B)) = add(A,multiply(B,inverse(A))),
inference(paramod,[status(thm)],[c_2,c_5476]) ).
cnf(c_5478,plain,
add(A,B) = add(A,multiply(B,inverse(A))),
inference(paramod,[status(thm)],[c_24,c_5477]) ).
cnf(c_28,plain,
add(A,multiply(B,inverse(A))) = add(A,B),
inference(copy,[status(thm)],[c_5478]) ).
cnf(c_32,plain,
add(add(A,multiply(B,C)),multiply(add(B,A),D)) = multiply(add(B,A),add(add(A,C),D)),
inference(paramod,[status(thm)],[c_13,c_6]) ).
cnf(c_5479,plain,
multiply(add(A,B),B) = add(B,multiply(A,additive_identity)),
inference(paramod,[status(thm)],[c_7,c_13]) ).
cnf(c_36,plain,
multiply(A,add(B,A)) = add(A,multiply(B,additive_identity)),
inference(paramod,[status(thm)],[c_2,c_5479]) ).
cnf(c_5480,plain,
multiply(multiplicative_identity,add(inverse(A),B)) = add(inverse(A),multiply(A,B)),
inference(paramod,[status(thm)],[c_9,c_13]) ).
cnf(c_5481,plain,
add(inverse(A),B) = add(inverse(A),multiply(A,B)),
inference(paramod,[status(thm)],[c_24,c_5480]) ).
cnf(c_37,plain,
add(inverse(A),multiply(A,B)) = add(inverse(A),B),
inference(copy,[status(thm)],[c_5481]) ).
cnf(c_39,plain,
inverse(multiplicative_identity) = additive_identity,
inference(paramod,[status(thm)],[c_24,c_10]) ).
cnf(c_40,plain,
multiply(A,add(A,B)) = add(multiply(additive_identity,B),A),
inference(paramod,[status(thm)],[c_22,c_1]) ).
cnf(c_41,plain,
multiply(A,add(B,A)) = add(A,multiply(additive_identity,B)),
inference(paramod,[status(thm)],[c_1,c_22]) ).
cnf(c_5482,plain,
multiply(A,add(A,multiplicative_identity)) = add(A,additive_identity),
inference(paramod,[status(thm)],[c_8,c_22]) ).
cnf(c_50,plain,
multiply(A,add(A,multiplicative_identity)) = A,
inference(paramod,[status(thm)],[c_7,c_5482]) ).
cnf(c_53,plain,
add(multiplicative_identity,multiply(additive_identity,A)) = add(multiplicative_identity,A),
inference(paramod,[status(thm)],[c_22,c_24]) ).
cnf(c_5483,plain,
add(multiply(A,A),multiply(A,multiplicative_identity)) = A,
inference(paramod,[status(thm)],[c_50,c_6]) ).
cnf(c_5484,plain,
add(multiply(A,A),A) = A,
inference(paramod,[status(thm)],[c_8,c_5483]) ).
cnf(c_58,plain,
add(A,multiply(A,A)) = A,
inference(paramod,[status(thm)],[c_1,c_5484]) ).
cnf(c_5485,plain,
multiplicative_identity = add(multiplicative_identity,multiplicative_identity),
inference(paramod,[status(thm)],[c_50,c_24]) ).
cnf(c_59,plain,
add(multiplicative_identity,multiplicative_identity) = multiplicative_identity,
inference(copy,[status(thm)],[c_5485]) ).
cnf(c_5486,plain,
multiply(add(inverse(A),B),multiplicative_identity) = add(inverse(A),multiply(B,A)),
inference(paramod,[status(thm)],[c_9,c_14]) ).
cnf(c_5487,plain,
multiply(multiplicative_identity,add(inverse(A),B)) = add(inverse(A),multiply(B,A)),
inference(paramod,[status(thm)],[c_2,c_5486]) ).
cnf(c_5488,plain,
add(inverse(A),B) = add(inverse(A),multiply(B,A)),
inference(paramod,[status(thm)],[c_24,c_5487]) ).
cnf(c_62,plain,
add(inverse(A),multiply(B,A)) = add(inverse(A),B),
inference(copy,[status(thm)],[c_5488]) ).
cnf(c_5489,plain,
add(multiply(A,multiplicative_identity),multiply(A,multiplicative_identity)) = multiply(A,multiplicative_identity),
inference(paramod,[status(thm)],[c_59,c_6]) ).
cnf(c_5490,plain,
add(A,multiply(A,multiplicative_identity)) = multiply(A,multiplicative_identity),
inference(paramod,[status(thm)],[c_8,c_5489]) ).
cnf(c_5491,plain,
add(A,A) = multiply(A,multiplicative_identity),
inference(paramod,[status(thm)],[c_8,c_5490]) ).
cnf(c_67,plain,
add(A,A) = A,
inference(paramod,[status(thm)],[c_8,c_5491]) ).
cnf(c_5492,plain,
multiply(add(A,multiplicative_identity),multiplicative_identity) = add(multiplicative_identity,multiply(A,multiplicative_identity)),
inference(paramod,[status(thm)],[c_59,c_13]) ).
cnf(c_5493,plain,
multiply(multiplicative_identity,add(A,multiplicative_identity)) = add(multiplicative_identity,multiply(A,multiplicative_identity)),
inference(paramod,[status(thm)],[c_2,c_5492]) ).
cnf(c_5494,plain,
add(multiplicative_identity,multiply(A,additive_identity)) = add(multiplicative_identity,multiply(A,multiplicative_identity)),
inference(paramod,[status(thm)],[c_36,c_5493]) ).
cnf(c_68,plain,
add(multiplicative_identity,multiply(A,additive_identity)) = add(multiplicative_identity,A),
inference(paramod,[status(thm)],[c_8,c_5494]) ).
cnf(c_69,plain,
multiply(A,add(A,B)) = add(A,multiply(A,B)),
inference(paramod,[status(thm)],[c_67,c_4]) ).
cnf(c_5495,plain,
multiply(add(A,B),B) = add(B,multiply(A,B)),
inference(paramod,[status(thm)],[c_67,c_13]) ).
cnf(c_70,plain,
multiply(A,add(B,A)) = add(A,multiply(B,A)),
inference(paramod,[status(thm)],[c_2,c_5495]) ).
cnf(c_5496,plain,
multiply(A,A) = add(A,multiply(additive_identity,A)),
inference(paramod,[status(thm)],[c_67,c_22]) ).
cnf(c_71,plain,
add(A,multiply(additive_identity,A)) = multiply(A,A),
inference(copy,[status(thm)],[c_5496]) ).
cnf(c_5497,plain,
add(A,multiply(A,B)) = add(multiply(additive_identity,B),A),
inference(paramod,[status(thm)],[c_69,c_40]) ).
cnf(c_80,plain,
add(multiply(additive_identity,A),B) = add(B,multiply(B,A)),
inference(copy,[status(thm)],[c_5497]) ).
cnf(c_5498,plain,
add(A,multiply(A,B)) = add(A,multiply(B,additive_identity)),
inference(paramod,[status(thm)],[c_69,c_23]) ).
cnf(c_81,plain,
add(A,multiply(B,additive_identity)) = add(A,multiply(A,B)),
inference(copy,[status(thm)],[c_5498]) ).
cnf(c_5499,plain,
add(A,multiply(A,B)) = add(A,multiply(additive_identity,B)),
inference(paramod,[status(thm)],[c_69,c_22]) ).
cnf(c_82,plain,
add(A,multiply(additive_identity,B)) = add(A,multiply(A,B)),
inference(copy,[status(thm)],[c_5499]) ).
cnf(c_5500,plain,
add(A,multiply(B,A)) = add(A,multiply(additive_identity,B)),
inference(paramod,[status(thm)],[c_70,c_41]) ).
cnf(c_84,plain,
add(A,multiply(additive_identity,B)) = add(A,multiply(B,A)),
inference(copy,[status(thm)],[c_5500]) ).
cnf(c_5501,plain,
multiply(add(A,A),add(A,A)) = A,
inference(paramod,[status(thm)],[c_58,c_4]) ).
cnf(c_5502,plain,
multiply(A,add(A,A)) = A,
inference(paramod,[status(thm)],[c_67,c_5501]) ).
cnf(c_88,plain,
multiply(A,A) = A,
inference(paramod,[status(thm)],[c_67,c_5502]) ).
cnf(c_90,plain,
add(A,multiply(additive_identity,A)) = A,
inference(paramod,[status(thm)],[c_88,c_71]) ).
cnf(c_92,plain,
add(A,multiply(A,additive_identity)) = A,
inference(paramod,[status(thm)],[c_2,c_90]) ).
cnf(c_5503,plain,
multiply(A,add(A,B)) = add(A,multiply(multiply(A,additive_identity),B)),
inference(paramod,[status(thm)],[c_92,c_4]) ).
cnf(c_5504,plain,
add(A,multiply(A,B)) = add(A,multiply(multiply(A,additive_identity),B)),
inference(paramod,[status(thm)],[c_69,c_5503]) ).
cnf(c_97,plain,
add(A,multiply(multiply(A,additive_identity),B)) = add(A,multiply(A,B)),
inference(copy,[status(thm)],[c_5504]) ).
cnf(c_5505,plain,
add(additive_identity,multiply(inverse(A),B)) = multiply(inverse(A),add(A,B)),
inference(paramod,[status(thm)],[c_10,c_15]) ).
cnf(c_5506,plain,
multiply(inverse(A),B) = multiply(inverse(A),add(A,B)),
inference(paramod,[status(thm)],[c_21,c_5505]) ).
cnf(c_106,plain,
multiply(inverse(A),add(A,B)) = multiply(inverse(A),B),
inference(copy,[status(thm)],[c_5506]) ).
cnf(c_5507,plain,
add(multiply(A,multiplicative_identity),multiply(A,multiply(additive_identity,B))) = multiply(A,add(multiplicative_identity,B)),
inference(paramod,[status(thm)],[c_53,c_6]) ).
cnf(c_114,plain,
add(A,multiply(A,multiply(additive_identity,B))) = multiply(A,add(multiplicative_identity,B)),
inference(paramod,[status(thm)],[c_8,c_5507]) ).
cnf(c_5508,plain,
multiply(add(multiplicative_identity,A),add(multiplicative_identity,B)) = add(multiplicative_identity,multiply(multiply(A,additive_identity),B)),
inference(paramod,[status(thm)],[c_68,c_4]) ).
cnf(c_5509,plain,
add(multiplicative_identity,multiply(A,B)) = add(multiplicative_identity,multiply(multiply(A,additive_identity),B)),
inference(paramod,[status(thm)],[c_4,c_5508]) ).
cnf(c_116,plain,
add(multiplicative_identity,multiply(multiply(A,additive_identity),B)) = add(multiplicative_identity,multiply(A,B)),
inference(copy,[status(thm)],[c_5509]) ).
cnf(c_5510,plain,
add(A,multiply(A,B)) = multiply(add(multiplicative_identity,B),A),
inference(paramod,[status(thm)],[c_25,c_2]) ).
cnf(c_120,plain,
multiply(add(multiplicative_identity,A),B) = add(B,multiply(B,A)),
inference(copy,[status(thm)],[c_5510]) ).
cnf(c_5511,plain,
add(A,multiply(A,B)) = multiply(add(B,multiplicative_identity),A),
inference(paramod,[status(thm)],[c_26,c_2]) ).
cnf(c_140,plain,
multiply(add(A,multiplicative_identity),B) = add(B,multiply(B,A)),
inference(copy,[status(thm)],[c_5511]) ).
cnf(c_5512,plain,
add(add(A,B),multiply(add(A,B),B)) = add(B,multiply(A,multiplicative_identity)),
inference(paramod,[status(thm)],[c_26,c_13]) ).
cnf(c_5513,plain,
add(add(A,B),multiply(B,add(A,B))) = add(B,multiply(A,multiplicative_identity)),
inference(paramod,[status(thm)],[c_2,c_5512]) ).
cnf(c_5514,plain,
add(add(A,B),add(B,multiply(A,B))) = add(B,multiply(A,multiplicative_identity)),
inference(paramod,[status(thm)],[c_70,c_5513]) ).
cnf(c_145,plain,
add(add(A,B),add(B,multiply(A,B))) = add(B,A),
inference(paramod,[status(thm)],[c_8,c_5514]) ).
cnf(c_158,plain,
add(inverse(A),add(A,multiply(A,B))) = add(inverse(A),add(multiplicative_identity,B)),
inference(paramod,[status(thm)],[c_25,c_37]) ).
cnf(c_5515,plain,
add(multiply(add(A,B),A),multiply(C,add(A,B))) = add(A,multiply(B,C)),
inference(paramod,[status(thm)],[c_4,c_16]) ).
cnf(c_5516,plain,
add(multiply(A,add(A,B)),multiply(C,add(A,B))) = add(A,multiply(B,C)),
inference(paramod,[status(thm)],[c_2,c_5515]) ).
cnf(c_166,plain,
add(add(A,multiply(A,B)),multiply(C,add(A,B))) = add(A,multiply(B,C)),
inference(paramod,[status(thm)],[c_69,c_5516]) ).
cnf(c_5517,plain,
add(multiply(inverse(A),B),additive_identity) = multiply(inverse(A),add(B,A)),
inference(paramod,[status(thm)],[c_10,c_16]) ).
cnf(c_5518,plain,
add(additive_identity,multiply(inverse(A),B)) = multiply(inverse(A),add(B,A)),
inference(paramod,[status(thm)],[c_1,c_5517]) ).
cnf(c_5519,plain,
multiply(inverse(A),B) = multiply(inverse(A),add(B,A)),
inference(paramod,[status(thm)],[c_21,c_5518]) ).
cnf(c_167,plain,
multiply(inverse(A),add(B,A)) = multiply(inverse(A),B),
inference(copy,[status(thm)],[c_5519]) ).
cnf(c_5520,plain,
add(inverse(inverse(A)),additive_identity) = add(inverse(inverse(A)),A),
inference(paramod,[status(thm)],[c_10,c_62]) ).
cnf(c_5521,plain,
inverse(inverse(A)) = add(inverse(inverse(A)),A),
inference(paramod,[status(thm)],[c_7,c_5520]) ).
cnf(c_5522,plain,
inverse(inverse(A)) = add(A,inverse(inverse(A))),
inference(paramod,[status(thm)],[c_1,c_5521]) ).
cnf(c_182,plain,
add(A,inverse(inverse(A))) = inverse(inverse(A)),
inference(copy,[status(thm)],[c_5522]) ).
cnf(c_5523,plain,
add(inverse(A),add(A,multiply(A,B))) = add(inverse(A),add(A,B)),
inference(paramod,[status(thm)],[c_69,c_37]) ).
cnf(c_197,plain,
add(inverse(A),add(multiplicative_identity,B)) = add(inverse(A),add(A,B)),
inference(paramod,[status(thm)],[c_158,c_5523]) ).
cnf(c_208,plain,
add(multiply(A,B),add(B,multiply(C,B))) = multiply(B,add(A,add(C,B))),
inference(paramod,[status(thm)],[c_70,c_15]) ).
cnf(c_5524,plain,
multiply(add(multiplicative_identity,A),add(B,add(multiplicative_identity,A))) = add(add(multiplicative_identity,A),add(B,multiply(B,A))),
inference(paramod,[status(thm)],[c_25,c_70]) ).
cnf(c_5525,plain,
add(add(multiplicative_identity,A),multiply(B,add(multiplicative_identity,A))) = add(add(multiplicative_identity,A),add(B,multiply(B,A))),
inference(paramod,[status(thm)],[c_70,c_5524]) ).
cnf(c_5526,plain,
add(add(multiplicative_identity,A),multiply(additive_identity,B)) = add(add(multiplicative_identity,A),add(B,multiply(B,A))),
inference(paramod,[status(thm)],[c_84,c_5525]) ).
cnf(c_214,plain,
add(add(multiplicative_identity,A),add(B,multiply(B,A))) = add(add(multiplicative_identity,A),multiply(additive_identity,B)),
inference(copy,[status(thm)],[c_5526]) ).
cnf(c_5527,plain,
multiply(add(A,multiplicative_identity),add(B,add(A,multiplicative_identity))) = add(add(A,multiplicative_identity),add(B,multiply(B,A))),
inference(paramod,[status(thm)],[c_26,c_70]) ).
cnf(c_5528,plain,
add(add(A,multiplicative_identity),multiply(B,add(A,multiplicative_identity))) = add(add(A,multiplicative_identity),add(B,multiply(B,A))),
inference(paramod,[status(thm)],[c_70,c_5527]) ).
cnf(c_5529,plain,
add(add(A,multiplicative_identity),multiply(additive_identity,B)) = add(add(A,multiplicative_identity),add(B,multiply(B,A))),
inference(paramod,[status(thm)],[c_84,c_5528]) ).
cnf(c_216,plain,
add(add(A,multiplicative_identity),add(B,multiply(B,A))) = add(add(A,multiplicative_identity),multiply(additive_identity,B)),
inference(copy,[status(thm)],[c_5529]) ).
cnf(c_218,plain,
add(inverse(A),add(A,multiply(B,A))) = add(inverse(A),add(B,A)),
inference(paramod,[status(thm)],[c_70,c_37]) ).
cnf(c_220,plain,
add(add(A,multiply(B,A)),multiply(C,A)) = multiply(A,add(add(B,A),C)),
inference(paramod,[status(thm)],[c_70,c_16]) ).
cnf(c_234,plain,
multiply(A,add(multiplicative_identity,B)) = add(multiply(additive_identity,B),A),
inference(paramod,[status(thm)],[c_80,c_25]) ).
cnf(c_252,plain,
add(A,multiply(A,multiply(additive_identity,B))) = add(multiply(additive_identity,B),A),
inference(paramod,[status(thm)],[c_234,c_114]) ).
cnf(c_5530,plain,
multiply(multiply(A,additive_identity),add(B,multiply(B,A))) = add(multiply(A,additive_identity),multiply(B,multiply(A,additive_identity))),
inference(paramod,[status(thm)],[c_81,c_70]) ).
cnf(c_5531,plain,
multiply(multiply(A,additive_identity),add(B,multiply(B,A))) = add(multiply(A,additive_identity),multiply(additive_identity,B)),
inference(paramod,[status(thm)],[c_84,c_5530]) ).
cnf(c_265,plain,
multiply(multiply(A,additive_identity),add(B,multiply(B,A))) = multiply(additive_identity,add(A,B)),
inference(paramod,[status(thm)],[c_15,c_5531]) ).
cnf(c_5532,plain,
multiply(A,add(A,multiply(B,A))) = add(A,multiply(A,multiply(additive_identity,B))),
inference(paramod,[status(thm)],[c_84,c_69]) ).
cnf(c_5533,plain,
add(A,multiply(A,multiply(B,A))) = add(A,multiply(A,multiply(additive_identity,B))),
inference(paramod,[status(thm)],[c_69,c_5532]) ).
cnf(c_322,plain,
add(A,multiply(A,multiply(B,A))) = add(multiply(additive_identity,B),A),
inference(paramod,[status(thm)],[c_252,c_5533]) ).
cnf(c_5534,plain,
multiply(inverse(A),A) = multiply(inverse(A),additive_identity),
inference(paramod,[status(thm)],[c_7,c_106]) ).
cnf(c_5535,plain,
multiply(A,inverse(A)) = multiply(inverse(A),additive_identity),
inference(paramod,[status(thm)],[c_2,c_5534]) ).
cnf(c_5536,plain,
additive_identity = multiply(inverse(A),additive_identity),
inference(paramod,[status(thm)],[c_10,c_5535]) ).
cnf(c_346,plain,
multiply(inverse(A),additive_identity) = additive_identity,
inference(copy,[status(thm)],[c_5536]) ).
cnf(c_5537,plain,
add(inverse(add(A,B)),multiply(inverse(A),B)) = add(inverse(add(A,B)),inverse(A)),
inference(paramod,[status(thm)],[c_106,c_62]) ).
cnf(c_5538,plain,
add(multiply(inverse(A),B),inverse(add(A,B))) = add(inverse(add(A,B)),inverse(A)),
inference(paramod,[status(thm)],[c_1,c_5537]) ).
cnf(c_356,plain,
add(multiply(inverse(A),B),inverse(add(A,B))) = add(inverse(A),inverse(add(A,B))),
inference(paramod,[status(thm)],[c_1,c_5538]) ).
cnf(c_5539,plain,
multiply(inverse(A),add(A,multiply(B,A))) = multiply(inverse(A),multiply(additive_identity,B)),
inference(paramod,[status(thm)],[c_84,c_106]) ).
cnf(c_5540,plain,
multiply(inverse(A),multiply(B,A)) = multiply(inverse(A),multiply(additive_identity,B)),
inference(paramod,[status(thm)],[c_106,c_5539]) ).
cnf(c_363,plain,
multiply(inverse(A),multiply(additive_identity,B)) = multiply(inverse(A),multiply(B,A)),
inference(copy,[status(thm)],[c_5540]) ).
cnf(c_5541,plain,
add(add(multiplicative_identity,A),multiply(add(multiplicative_identity,A),B)) = add(multiplicative_identity,multiply(B,A)),
inference(paramod,[status(thm)],[c_120,c_4]) ).
cnf(c_409,plain,
add(add(multiplicative_identity,A),multiply(B,additive_identity)) = add(multiplicative_identity,multiply(B,A)),
inference(paramod,[status(thm)],[c_81,c_5541]) ).
cnf(c_5542,plain,
add(add(A,multiplicative_identity),multiply(add(A,multiplicative_identity),B)) = add(multiplicative_identity,multiply(B,A)),
inference(paramod,[status(thm)],[c_120,c_14]) ).
cnf(c_419,plain,
add(add(A,multiplicative_identity),multiply(B,additive_identity)) = add(multiplicative_identity,multiply(B,A)),
inference(paramod,[status(thm)],[c_81,c_5542]) ).
cnf(c_5543,plain,
multiply(add(multiplicative_identity,A),B) = add(B,multiply(B,multiply(additive_identity,A))),
inference(paramod,[status(thm)],[c_53,c_120]) ).
cnf(c_424,plain,
multiply(add(multiplicative_identity,A),B) = add(multiply(additive_identity,A),B),
inference(paramod,[status(thm)],[c_252,c_5543]) ).
cnf(c_5544,plain,
multiply(add(multiplicative_identity,A),add(add(multiplicative_identity,A),B)) = add(add(multiplicative_identity,A),add(B,multiply(B,A))),
inference(paramod,[status(thm)],[c_120,c_69]) ).
cnf(c_5545,plain,
add(add(multiplicative_identity,A),multiply(add(multiplicative_identity,A),B)) = add(add(multiplicative_identity,A),add(B,multiply(B,A))),
inference(paramod,[status(thm)],[c_69,c_5544]) ).
cnf(c_5546,plain,
add(add(multiplicative_identity,A),add(multiply(additive_identity,A),B)) = add(add(multiplicative_identity,A),add(B,multiply(B,A))),
inference(paramod,[status(thm)],[c_424,c_5545]) ).
cnf(c_428,plain,
add(add(multiplicative_identity,A),add(multiply(additive_identity,A),B)) = add(add(multiplicative_identity,A),multiply(additive_identity,B)),
inference(paramod,[status(thm)],[c_214,c_5546]) ).
cnf(c_5547,plain,
add(add(A,add(multiplicative_identity,B)),multiply(add(A,add(multiplicative_identity,B)),B)) = add(add(multiplicative_identity,B),multiply(A,add(multiplicative_identity,B))),
inference(paramod,[status(thm)],[c_120,c_70]) ).
cnf(c_5548,plain,
add(add(A,add(multiplicative_identity,B)),multiply(B,add(A,add(multiplicative_identity,B)))) = add(add(multiplicative_identity,B),multiply(A,add(multiplicative_identity,B))),
inference(paramod,[status(thm)],[c_2,c_5547]) ).
cnf(c_5549,plain,
add(add(A,add(multiplicative_identity,B)),multiply(additive_identity,B)) = add(add(multiplicative_identity,B),multiply(A,add(multiplicative_identity,B))),
inference(paramod,[status(thm)],[c_84,c_5548]) ).
cnf(c_5550,plain,
add(multiply(additive_identity,B),add(A,add(multiplicative_identity,B))) = add(add(multiplicative_identity,B),multiply(A,add(multiplicative_identity,B))),
inference(paramod,[status(thm)],[c_1,c_5549]) ).
cnf(c_5551,plain,
add(multiply(additive_identity,B),add(A,add(multiplicative_identity,B))) = add(add(multiplicative_identity,B),add(multiply(additive_identity,B),A)),
inference(paramod,[status(thm)],[c_234,c_5550]) ).
cnf(c_429,plain,
add(multiply(additive_identity,A),add(B,add(multiplicative_identity,A))) = add(add(multiplicative_identity,A),multiply(additive_identity,B)),
inference(paramod,[status(thm)],[c_428,c_5551]) ).
cnf(c_5552,plain,
add(add(multiplicative_identity,A),multiply(B,additive_identity)) = add(add(multiplicative_identity,A),add(B,multiply(B,A))),
inference(paramod,[status(thm)],[c_120,c_81]) ).
cnf(c_5553,plain,
add(multiplicative_identity,multiply(B,A)) = add(add(multiplicative_identity,A),add(B,multiply(B,A))),
inference(paramod,[status(thm)],[c_409,c_5552]) ).
cnf(c_5554,plain,
add(multiplicative_identity,multiply(B,A)) = add(add(multiplicative_identity,A),multiply(additive_identity,B)),
inference(paramod,[status(thm)],[c_214,c_5553]) ).
cnf(c_430,plain,
add(add(multiplicative_identity,A),multiply(additive_identity,B)) = add(multiplicative_identity,multiply(B,A)),
inference(copy,[status(thm)],[c_5554]) ).
cnf(c_443,plain,
add(multiply(additive_identity,A),add(B,add(multiplicative_identity,A))) = add(multiplicative_identity,multiply(B,A)),
inference(paramod,[status(thm)],[c_430,c_429]) ).
cnf(c_5555,plain,
multiply(add(A,multiplicative_identity),add(add(A,multiplicative_identity),B)) = add(add(A,multiplicative_identity),add(B,multiply(B,A))),
inference(paramod,[status(thm)],[c_140,c_69]) ).
cnf(c_5556,plain,
add(add(A,multiplicative_identity),multiply(add(A,multiplicative_identity),B)) = add(add(A,multiplicative_identity),add(B,multiply(B,A))),
inference(paramod,[status(thm)],[c_69,c_5555]) ).
cnf(c_5557,plain,
add(add(A,multiplicative_identity),multiply(B,additive_identity)) = add(add(A,multiplicative_identity),add(B,multiply(B,A))),
inference(paramod,[status(thm)],[c_81,c_5556]) ).
cnf(c_5558,plain,
add(multiplicative_identity,multiply(B,A)) = add(add(A,multiplicative_identity),add(B,multiply(B,A))),
inference(paramod,[status(thm)],[c_419,c_5557]) ).
cnf(c_5559,plain,
add(multiplicative_identity,multiply(B,A)) = add(add(A,multiplicative_identity),multiply(additive_identity,B)),
inference(paramod,[status(thm)],[c_216,c_5558]) ).
cnf(c_459,plain,
add(add(A,multiplicative_identity),multiply(additive_identity,B)) = add(multiplicative_identity,multiply(B,A)),
inference(copy,[status(thm)],[c_5559]) ).
cnf(c_5560,plain,
add(multiply(inverse(A),B),multiply(inverse(A),C)) = multiply(inverse(A),add(B,add(C,A))),
inference(paramod,[status(thm)],[c_167,c_6]) ).
cnf(c_5561,plain,
multiply(inverse(A),add(B,C)) = multiply(inverse(A),add(B,add(C,A))),
inference(paramod,[status(thm)],[c_6,c_5560]) ).
cnf(c_471,plain,
multiply(inverse(A),add(B,add(C,A))) = multiply(inverse(A),add(B,C)),
inference(copy,[status(thm)],[c_5561]) ).
cnf(c_5562,plain,
multiply(inverse(multiply(additive_identity,A)),add(multiplicative_identity,A)) = multiply(inverse(multiply(additive_identity,A)),multiplicative_identity),
inference(paramod,[status(thm)],[c_53,c_167]) ).
cnf(c_5563,plain,
multiply(add(multiplicative_identity,A),inverse(multiply(additive_identity,A))) = multiply(inverse(multiply(additive_identity,A)),multiplicative_identity),
inference(paramod,[status(thm)],[c_2,c_5562]) ).
cnf(c_5564,plain,
add(multiply(additive_identity,A),inverse(multiply(additive_identity,A))) = multiply(inverse(multiply(additive_identity,A)),multiplicative_identity),
inference(paramod,[status(thm)],[c_424,c_5563]) ).
cnf(c_5565,plain,
multiplicative_identity = multiply(inverse(multiply(additive_identity,A)),multiplicative_identity),
inference(paramod,[status(thm)],[c_9,c_5564]) ).
cnf(c_5566,plain,
multiplicative_identity = multiply(multiplicative_identity,inverse(multiply(additive_identity,A))),
inference(paramod,[status(thm)],[c_2,c_5565]) ).
cnf(c_5567,plain,
multiplicative_identity = inverse(multiply(additive_identity,A)),
inference(paramod,[status(thm)],[c_24,c_5566]) ).
cnf(c_475,plain,
inverse(multiply(additive_identity,A)) = multiplicative_identity,
inference(copy,[status(thm)],[c_5567]) ).
cnf(c_5568,plain,
add(inverse(add(A,B)),multiply(inverse(B),A)) = add(inverse(add(A,B)),inverse(B)),
inference(paramod,[status(thm)],[c_167,c_62]) ).
cnf(c_5569,plain,
add(multiply(inverse(B),A),inverse(add(A,B))) = add(inverse(add(A,B)),inverse(B)),
inference(paramod,[status(thm)],[c_1,c_5568]) ).
cnf(c_480,plain,
add(multiply(inverse(A),B),inverse(add(B,A))) = add(inverse(A),inverse(add(B,A))),
inference(paramod,[status(thm)],[c_1,c_5569]) ).
cnf(c_5570,plain,
multiply(inverse(multiply(additive_identity,A)),add(B,multiply(B,A))) = multiply(inverse(multiply(additive_identity,A)),B),
inference(paramod,[status(thm)],[c_82,c_167]) ).
cnf(c_5571,plain,
multiply(multiplicative_identity,add(B,multiply(B,A))) = multiply(inverse(multiply(additive_identity,A)),B),
inference(paramod,[status(thm)],[c_475,c_5570]) ).
cnf(c_5572,plain,
add(B,multiply(B,A)) = multiply(inverse(multiply(additive_identity,A)),B),
inference(paramod,[status(thm)],[c_24,c_5571]) ).
cnf(c_5573,plain,
add(B,multiply(B,A)) = multiply(multiplicative_identity,B),
inference(paramod,[status(thm)],[c_475,c_5572]) ).
cnf(c_486,plain,
add(A,multiply(A,B)) = A,
inference(paramod,[status(thm)],[c_24,c_5573]) ).
cnf(c_5574,plain,
multiply(inverse(multiply(additive_identity,A)),add(B,multiply(A,B))) = multiply(inverse(multiply(additive_identity,A)),B),
inference(paramod,[status(thm)],[c_84,c_167]) ).
cnf(c_5575,plain,
multiply(multiplicative_identity,add(B,multiply(A,B))) = multiply(inverse(multiply(additive_identity,A)),B),
inference(paramod,[status(thm)],[c_475,c_5574]) ).
cnf(c_5576,plain,
add(B,multiply(A,B)) = multiply(inverse(multiply(additive_identity,A)),B),
inference(paramod,[status(thm)],[c_24,c_5575]) ).
cnf(c_5577,plain,
add(B,multiply(A,B)) = multiply(multiplicative_identity,B),
inference(paramod,[status(thm)],[c_475,c_5576]) ).
cnf(c_489,plain,
add(A,multiply(B,A)) = A,
inference(paramod,[status(thm)],[c_24,c_5577]) ).
cnf(c_5578,plain,
A = add(multiply(additive_identity,B),A),
inference(paramod,[status(thm)],[c_486,c_322]) ).
cnf(c_512,plain,
add(multiply(additive_identity,A),B) = B,
inference(copy,[status(thm)],[c_5578]) ).
cnf(c_519,plain,
multiply(multiply(A,additive_identity),B) = multiply(additive_identity,add(A,B)),
inference(paramod,[status(thm)],[c_486,c_265]) ).
cnf(c_528,plain,
add(A,multiply(B,add(A,C))) = add(A,multiply(C,B)),
inference(paramod,[status(thm)],[c_486,c_166]) ).
cnf(c_5579,plain,
add(A,multiply(additive_identity,add(A,B))) = add(A,multiply(A,B)),
inference(paramod,[status(thm)],[c_519,c_97]) ).
cnf(c_5580,plain,
add(A,multiply(B,additive_identity)) = add(A,multiply(A,B)),
inference(paramod,[status(thm)],[c_528,c_5579]) ).
cnf(c_533,plain,
add(A,multiply(B,additive_identity)) = A,
inference(paramod,[status(thm)],[c_486,c_5580]) ).
cnf(c_536,plain,
add(A,multiply(additive_identity,B)) = A,
inference(paramod,[status(thm)],[c_486,c_82]) ).
cnf(c_537,plain,
multiply(A,add(A,B)) = A,
inference(paramod,[status(thm)],[c_486,c_69]) ).
cnf(c_5581,plain,
add(A,multiply(C,A)) = multiply(A,add(add(B,A),C)),
inference(paramod,[status(thm)],[c_489,c_220]) ).
cnf(c_5582,plain,
A = multiply(A,add(add(B,A),C)),
inference(paramod,[status(thm)],[c_489,c_5581]) ).
cnf(c_544,plain,
multiply(A,add(add(B,A),C)) = A,
inference(copy,[status(thm)],[c_5582]) ).
cnf(c_5583,plain,
add(inverse(A),A) = add(inverse(A),add(B,A)),
inference(paramod,[status(thm)],[c_489,c_218]) ).
cnf(c_5584,plain,
add(A,inverse(A)) = add(inverse(A),add(B,A)),
inference(paramod,[status(thm)],[c_1,c_5583]) ).
cnf(c_5585,plain,
multiplicative_identity = add(inverse(A),add(B,A)),
inference(paramod,[status(thm)],[c_9,c_5584]) ).
cnf(c_545,plain,
add(inverse(A),add(B,A)) = multiplicative_identity,
inference(copy,[status(thm)],[c_5585]) ).
cnf(c_5586,plain,
add(multiply(A,B),B) = multiply(B,add(A,add(C,B))),
inference(paramod,[status(thm)],[c_489,c_208]) ).
cnf(c_5587,plain,
add(B,multiply(A,B)) = multiply(B,add(A,add(C,B))),
inference(paramod,[status(thm)],[c_1,c_5586]) ).
cnf(c_5588,plain,
B = multiply(B,add(A,add(C,B))),
inference(paramod,[status(thm)],[c_489,c_5587]) ).
cnf(c_546,plain,
multiply(A,add(B,add(C,A))) = A,
inference(copy,[status(thm)],[c_5588]) ).
cnf(c_5589,plain,
add(add(A,B),B) = add(B,A),
inference(paramod,[status(thm)],[c_489,c_145]) ).
cnf(c_547,plain,
add(A,add(B,A)) = add(A,B),
inference(paramod,[status(thm)],[c_1,c_5589]) ).
cnf(c_548,plain,
multiply(A,add(B,A)) = A,
inference(paramod,[status(thm)],[c_489,c_70]) ).
cnf(c_5590,plain,
add(A,multiplicative_identity) = add(multiplicative_identity,multiply(B,A)),
inference(paramod,[status(thm)],[c_536,c_459]) ).
cnf(c_549,plain,
add(multiplicative_identity,multiply(A,B)) = add(B,multiplicative_identity),
inference(copy,[status(thm)],[c_5590]) ).
cnf(c_5591,plain,
add(B,add(multiplicative_identity,A)) = add(multiplicative_identity,multiply(B,A)),
inference(paramod,[status(thm)],[c_512,c_443]) ).
cnf(c_554,plain,
add(A,add(multiplicative_identity,B)) = add(B,multiplicative_identity),
inference(paramod,[status(thm)],[c_549,c_5591]) ).
cnf(c_5592,plain,
add(multiplicative_identity,multiply(additive_identity,add(A,B))) = add(multiplicative_identity,multiply(A,B)),
inference(paramod,[status(thm)],[c_519,c_116]) ).
cnf(c_5593,plain,
multiplicative_identity = add(multiplicative_identity,multiply(A,B)),
inference(paramod,[status(thm)],[c_536,c_5592]) ).
cnf(c_5594,plain,
multiplicative_identity = add(B,multiplicative_identity),
inference(paramod,[status(thm)],[c_549,c_5593]) ).
cnf(c_568,plain,
add(A,multiplicative_identity) = multiplicative_identity,
inference(copy,[status(thm)],[c_5594]) ).
cnf(c_5595,plain,
add(B,multiplicative_identity) = add(inverse(A),add(A,B)),
inference(paramod,[status(thm)],[c_554,c_197]) ).
cnf(c_5596,plain,
multiplicative_identity = add(inverse(A),add(A,B)),
inference(paramod,[status(thm)],[c_568,c_5595]) ).
cnf(c_572,plain,
add(inverse(A),add(A,B)) = multiplicative_identity,
inference(copy,[status(thm)],[c_5596]) ).
cnf(c_5597,plain,
multiplicative_identity = add(multiplicative_identity,A),
inference(paramod,[status(thm)],[c_533,c_68]) ).
cnf(c_580,plain,
add(multiplicative_identity,A) = multiplicative_identity,
inference(copy,[status(thm)],[c_5597]) ).
cnf(c_5598,plain,
multiply(inverse(multiplicative_identity),multiplicative_identity) = multiply(inverse(multiplicative_identity),A),
inference(paramod,[status(thm)],[c_568,c_167]) ).
cnf(c_5599,plain,
multiply(additive_identity,multiplicative_identity) = multiply(inverse(multiplicative_identity),A),
inference(paramod,[status(thm)],[c_39,c_5598]) ).
cnf(c_5600,plain,
additive_identity = multiply(inverse(multiplicative_identity),A),
inference(paramod,[status(thm)],[c_8,c_5599]) ).
cnf(c_5601,plain,
additive_identity = multiply(additive_identity,A),
inference(paramod,[status(thm)],[c_39,c_5600]) ).
cnf(c_594,plain,
multiply(additive_identity,A) = additive_identity,
inference(copy,[status(thm)],[c_5601]) ).
cnf(c_5602,plain,
multiply(inverse(A),additive_identity) = multiply(inverse(A),multiply(B,A)),
inference(paramod,[status(thm)],[c_594,c_363]) ).
cnf(c_5603,plain,
additive_identity = multiply(inverse(A),multiply(B,A)),
inference(paramod,[status(thm)],[c_346,c_5602]) ).
cnf(c_598,plain,
multiply(inverse(A),multiply(B,A)) = additive_identity,
inference(copy,[status(thm)],[c_5603]) ).
cnf(c_5604,plain,
multiply(inverse(add(A,B)),multiplicative_identity) = multiply(inverse(add(A,B)),inverse(B)),
inference(paramod,[status(thm)],[c_545,c_167]) ).
cnf(c_5605,plain,
multiply(multiplicative_identity,inverse(add(A,B))) = multiply(inverse(add(A,B)),inverse(B)),
inference(paramod,[status(thm)],[c_2,c_5604]) ).
cnf(c_5606,plain,
inverse(add(A,B)) = multiply(inverse(add(A,B)),inverse(B)),
inference(paramod,[status(thm)],[c_24,c_5605]) ).
cnf(c_5607,plain,
inverse(add(A,B)) = multiply(inverse(B),inverse(add(A,B))),
inference(paramod,[status(thm)],[c_2,c_5606]) ).
cnf(c_700,plain,
multiply(inverse(A),inverse(add(B,A))) = inverse(add(B,A)),
inference(copy,[status(thm)],[c_5607]) ).
cnf(c_5608,plain,
add(inverse(multiply(A,B)),B) = multiplicative_identity,
inference(paramod,[status(thm)],[c_489,c_545]) ).
cnf(c_702,plain,
add(A,inverse(multiply(B,A))) = multiplicative_identity,
inference(paramod,[status(thm)],[c_1,c_5608]) ).
cnf(c_5609,plain,
multiply(add(inverse(A),B),multiplicative_identity) = add(inverse(A),multiply(B,add(A,C))),
inference(paramod,[status(thm)],[c_572,c_4]) ).
cnf(c_5610,plain,
multiply(multiplicative_identity,add(inverse(A),B)) = add(inverse(A),multiply(B,add(A,C))),
inference(paramod,[status(thm)],[c_2,c_5609]) ).
cnf(c_5611,plain,
add(inverse(A),B) = add(inverse(A),multiply(B,add(A,C))),
inference(paramod,[status(thm)],[c_24,c_5610]) ).
cnf(c_705,plain,
add(inverse(A),multiply(B,add(A,C))) = add(inverse(A),B),
inference(copy,[status(thm)],[c_5611]) ).
cnf(c_5612,plain,
add(additive_identity,multiply(inverse(A),B)) = multiply(inverse(A),add(multiply(C,A),B)),
inference(paramod,[status(thm)],[c_598,c_6]) ).
cnf(c_5613,plain,
multiply(inverse(A),B) = multiply(inverse(A),add(multiply(C,A),B)),
inference(paramod,[status(thm)],[c_21,c_5612]) ).
cnf(c_717,plain,
multiply(inverse(A),add(multiply(B,A),C)) = multiply(inverse(A),C),
inference(copy,[status(thm)],[c_5613]) ).
cnf(c_5614,plain,
multiply(inverse(add(A,B)),A) = additive_identity,
inference(paramod,[status(thm)],[c_537,c_598]) ).
cnf(c_728,plain,
multiply(A,inverse(add(A,B))) = additive_identity,
inference(paramod,[status(thm)],[c_2,c_5614]) ).
cnf(c_5615,plain,
multiply(inverse(add(A,B)),B) = additive_identity,
inference(paramod,[status(thm)],[c_548,c_598]) ).
cnf(c_729,plain,
multiply(A,inverse(add(B,A))) = additive_identity,
inference(paramod,[status(thm)],[c_2,c_5615]) ).
cnf(c_5616,plain,
add(A,additive_identity) = add(A,inverse(inverse(A))),
inference(paramod,[status(thm)],[c_10,c_27]) ).
cnf(c_5617,plain,
A = add(A,inverse(inverse(A))),
inference(paramod,[status(thm)],[c_7,c_5616]) ).
cnf(c_5618,plain,
A = inverse(inverse(A)),
inference(paramod,[status(thm)],[c_182,c_5617]) ).
cnf(c_759,plain,
inverse(inverse(A)) = A,
inference(copy,[status(thm)],[c_5618]) ).
cnf(c_5619,plain,
multiply(inverse(A),multiplicative_identity) = multiply(inverse(A),inverse(multiply(B,A))),
inference(paramod,[status(thm)],[c_702,c_106]) ).
cnf(c_5620,plain,
inverse(A) = multiply(inverse(A),inverse(multiply(B,A))),
inference(paramod,[status(thm)],[c_8,c_5619]) ).
cnf(c_778,plain,
multiply(inverse(A),inverse(multiply(B,A))) = inverse(A),
inference(copy,[status(thm)],[c_5620]) ).
cnf(c_5621,plain,
add(inverse(A),additive_identity) = add(inverse(A),inverse(add(A,B))),
inference(paramod,[status(thm)],[c_728,c_37]) ).
cnf(c_5622,plain,
inverse(A) = add(inverse(A),inverse(add(A,B))),
inference(paramod,[status(thm)],[c_7,c_5621]) ).
cnf(c_790,plain,
add(inverse(A),inverse(add(A,B))) = inverse(A),
inference(copy,[status(thm)],[c_5622]) ).
cnf(c_798,plain,
add(multiply(inverse(A),B),inverse(add(A,B))) = inverse(A),
inference(paramod,[status(thm)],[c_790,c_356]) ).
cnf(c_5623,plain,
add(inverse(A),additive_identity) = add(inverse(A),inverse(add(B,A))),
inference(paramod,[status(thm)],[c_729,c_37]) ).
cnf(c_5624,plain,
inverse(A) = add(inverse(A),inverse(add(B,A))),
inference(paramod,[status(thm)],[c_7,c_5623]) ).
cnf(c_803,plain,
add(inverse(A),inverse(add(B,A))) = inverse(A),
inference(copy,[status(thm)],[c_5624]) ).
cnf(c_814,plain,
add(multiply(inverse(A),B),inverse(add(B,A))) = inverse(A),
inference(paramod,[status(thm)],[c_803,c_480]) ).
cnf(c_828,plain,
multiply(add(A,B),add(add(B,A),C)) = add(add(B,A),multiply(A,C)),
inference(paramod,[status(thm)],[c_547,c_13]) ).
cnf(c_881,plain,
multiply(inverse(add(A,B)),inverse(multiply(inverse(A),B))) = inverse(add(A,B)),
inference(paramod,[status(thm)],[c_106,c_778]) ).
cnf(c_883,plain,
multiply(inverse(add(A,B)),inverse(multiply(inverse(B),A))) = inverse(add(A,B)),
inference(paramod,[status(thm)],[c_167,c_778]) ).
cnf(c_5625,plain,
add(add(A,B),multiply(add(B,A),C)) = multiply(add(B,A),add(add(A,multiplicative_identity),C)),
inference(paramod,[status(thm)],[c_8,c_32]) ).
cnf(c_5626,plain,
add(add(A,B),multiply(add(B,A),C)) = multiply(add(B,A),add(multiplicative_identity,C)),
inference(paramod,[status(thm)],[c_568,c_5625]) ).
cnf(c_5627,plain,
add(add(A,B),multiply(add(B,A),C)) = multiply(add(B,A),multiplicative_identity),
inference(paramod,[status(thm)],[c_580,c_5626]) ).
cnf(c_5628,plain,
add(add(A,B),multiply(add(B,A),C)) = multiply(multiplicative_identity,add(B,A)),
inference(paramod,[status(thm)],[c_2,c_5627]) ).
cnf(c_893,plain,
add(add(A,B),multiply(add(B,A),C)) = add(B,A),
inference(paramod,[status(thm)],[c_24,c_5628]) ).
cnf(c_5629,plain,
add(add(A,B),multiply(add(B,A),C)) = multiply(add(B,A),add(add(A,B),C)),
inference(paramod,[status(thm)],[c_88,c_32]) ).
cnf(c_5630,plain,
add(B,A) = multiply(add(B,A),add(add(A,B),C)),
inference(paramod,[status(thm)],[c_893,c_5629]) ).
cnf(c_5631,plain,
add(B,A) = add(add(A,B),multiply(B,C)),
inference(paramod,[status(thm)],[c_828,c_5630]) ).
cnf(c_901,plain,
add(add(A,B),multiply(B,C)) = add(B,A),
inference(copy,[status(thm)],[c_5631]) ).
cnf(c_937,plain,
multiply(add(A,B),add(add(B,A),C)) = add(A,B),
inference(paramod,[status(thm)],[c_901,c_828]) ).
cnf(c_5632,plain,
multiply(add(A,B),add(add(B,A),C)) = add(add(B,A),multiply(multiply(A,D),C)),
inference(paramod,[status(thm)],[c_901,c_4]) ).
cnf(c_5633,plain,
add(A,B) = add(add(B,A),multiply(multiply(A,D),C)),
inference(paramod,[status(thm)],[c_937,c_5632]) ).
cnf(c_1132,plain,
add(add(A,B),multiply(multiply(B,C),D)) = add(B,A),
inference(copy,[status(thm)],[c_5633]) ).
cnf(c_5634,plain,
add(multiply(inverse(multiply(inverse(A),B)),inverse(add(A,B))),inverse(inverse(A))) = inverse(multiply(inverse(A),B)),
inference(paramod,[status(thm)],[c_798,c_798]) ).
cnf(c_5635,plain,
add(multiply(inverse(add(A,B)),inverse(multiply(inverse(A),B))),inverse(inverse(A))) = inverse(multiply(inverse(A),B)),
inference(paramod,[status(thm)],[c_2,c_5634]) ).
cnf(c_5636,plain,
add(inverse(add(A,B)),inverse(inverse(A))) = inverse(multiply(inverse(A),B)),
inference(paramod,[status(thm)],[c_881,c_5635]) ).
cnf(c_5637,plain,
add(inverse(add(A,B)),A) = inverse(multiply(inverse(A),B)),
inference(paramod,[status(thm)],[c_759,c_5636]) ).
cnf(c_1537,plain,
add(A,inverse(add(A,B))) = inverse(multiply(inverse(A),B)),
inference(paramod,[status(thm)],[c_1,c_5637]) ).
cnf(c_5638,plain,
add(multiply(inverse(multiply(inverse(A),B)),inverse(add(B,A))),inverse(inverse(A))) = inverse(multiply(inverse(A),B)),
inference(paramod,[status(thm)],[c_814,c_798]) ).
cnf(c_5639,plain,
add(multiply(inverse(add(B,A)),inverse(multiply(inverse(A),B))),inverse(inverse(A))) = inverse(multiply(inverse(A),B)),
inference(paramod,[status(thm)],[c_2,c_5638]) ).
cnf(c_5640,plain,
add(inverse(add(B,A)),inverse(inverse(A))) = inverse(multiply(inverse(A),B)),
inference(paramod,[status(thm)],[c_883,c_5639]) ).
cnf(c_5641,plain,
add(inverse(add(B,A)),A) = inverse(multiply(inverse(A),B)),
inference(paramod,[status(thm)],[c_759,c_5640]) ).
cnf(c_1554,plain,
add(A,inverse(add(B,A))) = inverse(multiply(inverse(A),B)),
inference(paramod,[status(thm)],[c_1,c_5641]) ).
cnf(c_5642,plain,
add(multiply(A,add(B,C)),inverse(add(inverse(B),A))) = inverse(multiply(inverse(multiply(A,add(B,C))),inverse(B))),
inference(paramod,[status(thm)],[c_705,c_1554]) ).
cnf(c_5643,plain,
add(inverse(add(inverse(B),A)),multiply(A,add(B,C))) = inverse(multiply(inverse(multiply(A,add(B,C))),inverse(B))),
inference(paramod,[status(thm)],[c_1,c_5642]) ).
cnf(c_2327,plain,
add(inverse(add(inverse(A),B)),multiply(B,add(A,C))) = inverse(multiply(inverse(A),inverse(multiply(B,add(A,C))))),
inference(paramod,[status(thm)],[c_2,c_5643]) ).
cnf(c_5644,plain,
add(inverse(inverse(A)),multiply(inverse(A),B)) = add(inverse(inverse(A)),add(multiply(C,A),B)),
inference(paramod,[status(thm)],[c_717,c_37]) ).
cnf(c_5645,plain,
add(A,multiply(inverse(A),B)) = add(inverse(inverse(A)),add(multiply(C,A),B)),
inference(paramod,[status(thm)],[c_759,c_5644]) ).
cnf(c_5646,plain,
add(A,B) = add(inverse(inverse(A)),add(multiply(C,A),B)),
inference(paramod,[status(thm)],[c_27,c_5645]) ).
cnf(c_5647,plain,
add(A,B) = add(A,add(multiply(C,A),B)),
inference(paramod,[status(thm)],[c_759,c_5646]) ).
cnf(c_2338,plain,
add(A,add(multiply(B,A),C)) = add(A,C),
inference(copy,[status(thm)],[c_5647]) ).
cnf(c_5648,plain,
multiply(inverse(A),inverse(B)) = multiply(inverse(A),inverse(add(B,A))),
inference(paramod,[status(thm)],[c_798,c_717]) ).
cnf(c_5649,plain,
multiply(inverse(A),inverse(B)) = inverse(add(B,A)),
inference(paramod,[status(thm)],[c_700,c_5648]) ).
cnf(c_2365,plain,
inverse(add(A,B)) = multiply(inverse(B),inverse(A)),
inference(copy,[status(thm)],[c_5649]) ).
cnf(c_5650,plain,
add(A,inverse(add(A,add(multiply(B,A),C)))) = inverse(multiply(inverse(A),C)),
inference(paramod,[status(thm)],[c_717,c_1537]) ).
cnf(c_5651,plain,
add(A,inverse(add(A,C))) = inverse(multiply(inverse(A),C)),
inference(paramod,[status(thm)],[c_2338,c_5650]) ).
cnf(c_5652,plain,
add(A,multiply(inverse(C),inverse(A))) = inverse(multiply(inverse(A),C)),
inference(paramod,[status(thm)],[c_2365,c_5651]) ).
cnf(c_5653,plain,
add(A,inverse(C)) = inverse(multiply(inverse(A),C)),
inference(paramod,[status(thm)],[c_28,c_5652]) ).
cnf(c_2366,plain,
inverse(multiply(inverse(A),B)) = add(A,inverse(B)),
inference(copy,[status(thm)],[c_5653]) ).
cnf(c_5654,plain,
add(multiply(inverse(B),inverse(inverse(A))),multiply(B,add(A,C))) = inverse(multiply(inverse(A),inverse(multiply(B,add(A,C))))),
inference(paramod,[status(thm)],[c_2365,c_2327]) ).
cnf(c_5655,plain,
add(multiply(inverse(B),A),multiply(B,add(A,C))) = inverse(multiply(inverse(A),inverse(multiply(B,add(A,C))))),
inference(paramod,[status(thm)],[c_759,c_5654]) ).
cnf(c_5656,plain,
add(multiply(inverse(B),A),multiply(B,add(A,C))) = add(A,inverse(inverse(multiply(B,add(A,C))))),
inference(paramod,[status(thm)],[c_2366,c_5655]) ).
cnf(c_5657,plain,
add(multiply(inverse(B),A),multiply(B,add(A,C))) = add(A,multiply(B,add(A,C))),
inference(paramod,[status(thm)],[c_759,c_5656]) ).
cnf(c_2392,plain,
add(multiply(inverse(A),B),multiply(A,add(B,C))) = add(B,multiply(C,A)),
inference(paramod,[status(thm)],[c_528,c_5657]) ).
cnf(c_5658,plain,
add(multiply(inverse(A),add(B,C)),multiply(A,add(C,B))) = add(add(B,C),multiply(multiply(C,D),A)),
inference(paramod,[status(thm)],[c_901,c_2392]) ).
cnf(c_5659,plain,
add(multiply(A,add(C,B)),multiply(inverse(A),add(B,C))) = add(add(B,C),multiply(multiply(C,D),A)),
inference(paramod,[status(thm)],[c_1,c_5658]) ).
cnf(c_4321,plain,
add(multiply(A,add(B,C)),multiply(inverse(A),add(C,B))) = add(B,C),
inference(paramod,[status(thm)],[c_1132,c_5659]) ).
cnf(c_5660,plain,
add(A,multiply(inverse(A),add(B,add(C,A)))) = add(add(C,A),B),
inference(paramod,[status(thm)],[c_544,c_4321]) ).
cnf(c_5661,plain,
add(A,multiply(inverse(A),add(B,C))) = add(add(C,A),B),
inference(paramod,[status(thm)],[c_471,c_5660]) ).
cnf(c_5662,plain,
add(A,add(B,C)) = add(add(C,A),B),
inference(paramod,[status(thm)],[c_27,c_5661]) ).
cnf(c_5464,plain,
add(add(A,B),C) = add(B,add(C,A)),
inference(copy,[status(thm)],[c_5662]) ).
cnf(c_5663,plain,
add(A,multiply(inverse(A),add(add(B,A),C))) = add(C,add(B,A)),
inference(paramod,[status(thm)],[c_546,c_4321]) ).
cnf(c_5664,plain,
add(A,multiply(inverse(A),add(A,add(C,B)))) = add(C,add(B,A)),
inference(paramod,[status(thm)],[c_5464,c_5663]) ).
cnf(c_5665,plain,
add(A,multiply(inverse(A),add(C,B))) = add(C,add(B,A)),
inference(paramod,[status(thm)],[c_106,c_5664]) ).
cnf(c_5666,plain,
add(A,add(C,B)) = add(C,add(B,A)),
inference(paramod,[status(thm)],[c_27,c_5665]) ).
cnf(c_5465,plain,
add(A,add(B,C)) = add(C,add(A,B)),
inference(copy,[status(thm)],[c_5666]) ).
cnf(c_5667,plain,
add(a,add(b,c)) != add(c,add(a,b)),
inference(copy,[status(thm)],[c_12]) ).
cnf(c_5466,plain,
$false,
inference(resolve,[status(thm)],[c_5465,c_5667]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : BOO008-4 : TPTP v9.3.1. Released v1.1.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n019.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 22:34:48 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.37 % Process 2362474 was started by sandbox2 on n019,
% 0.09/0.37 % Sat Sep 26 22:34:48 2026
% 0.09/0.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.09/0.37
% 0.09/0.37 % From the command line: assign(max_seconds, 300).
% 11.17/1.89
% 11.17/1.89 % Assigning unary symbol inverse kb_weight 0 and highest precedence (9).
% 11.17/1.89
% 11.17/1.89 % SZS status Unsatisfiable for theBenchmark
% 11.17/1.89
% 11.17/1.89 % Proof 1 at 1.13 (+ 0.27) seconds.
% 11.17/1.89 % Length of proof is 132.
% 11.17/1.89 % Level of proof is 27.
% 11.17/1.89 % Maximum clause weight is 52.000.
% 11.17/1.89 % Given clauses 174.
% 11.17/1.89
% 11.17/1.89 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------