%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : BOO008-2 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n003.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:02 AM UTC 2026
% Result : Unsatisfiable 36.03s 5.07s
% Output : CNFRefutation 36.03s
% Verified :
% SZS Type : Refutation
% Derivation depth : 58
% Number of leaves : 13
% Syntax : Number of formulae : 272 ( 272 unt; 0 def)
% Number of atoms : 272 ( 271 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 : 5 ( 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 : 575 ( 47 sgn 22 !; 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(multiply(VAR_0,VAR_1),VAR_2) = multiply(add(VAR_0,VAR_2),add(VAR_1,VAR_2)),
file('theBenchmark.p',distributivity1) ).
cnf(c_3,plain,
add(multiply(A,B),C) = multiply(add(A,C),add(B,C)),
inference(clausify,[status(thm)],[distributivity1]) ).
cnf(c_4,plain,
multiply(add(A,B),add(C,B)) = add(multiply(A,C),B),
inference(copy,[status(thm)],[c_3]) ).
fof(distributivity2,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',distributivity2) ).
cnf(c_5,plain,
add(A,multiply(B,C)) = multiply(add(A,B),add(A,C)),
inference(clausify,[status(thm)],[distributivity2]) ).
cnf(c_6,plain,
multiply(add(A,B),add(A,C)) = add(A,multiply(B,C)),
inference(copy,[status(thm)],[c_5]) ).
fof(distributivity3,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',distributivity3) ).
cnf(c_7,plain,
multiply(add(A,B),C) = add(multiply(A,C),multiply(B,C)),
inference(clausify,[status(thm)],[distributivity3]) ).
cnf(c_8,plain,
add(multiply(A,B),multiply(C,B)) = multiply(add(A,C),B),
inference(copy,[status(thm)],[c_7]) ).
fof(distributivity4,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',distributivity4) ).
cnf(c_9,plain,
multiply(A,add(B,C)) = add(multiply(A,B),multiply(A,C)),
inference(clausify,[status(thm)],[distributivity4]) ).
cnf(c_10,plain,
add(multiply(A,B),multiply(A,C)) = multiply(A,add(B,C)),
inference(copy,[status(thm)],[c_9]) ).
fof(additive_inverse1,axiom,
! [VAR_0] : add(VAR_0,inverse(VAR_0)) = multiplicative_identity,
file('theBenchmark.p',additive_inverse1) ).
cnf(c_11,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_13,plain,
multiply(A,inverse(A)) = additive_identity,
inference(clausify,[status(thm)],[multiplicative_inverse1]) ).
fof(multiplicative_id1,axiom,
! [VAR_0] : multiply(VAR_0,multiplicative_identity) = VAR_0,
file('theBenchmark.p',multiplicative_id1) ).
cnf(c_15,plain,
multiply(A,multiplicative_identity) = A,
inference(clausify,[status(thm)],[multiplicative_id1]) ).
fof(multiplicative_id2,axiom,
! [VAR_0] : multiply(multiplicative_identity,VAR_0) = VAR_0,
file('theBenchmark.p',multiplicative_id2) ).
cnf(c_16,plain,
multiply(multiplicative_identity,A) = A,
inference(clausify,[status(thm)],[multiplicative_id2]) ).
fof(additive_id1,axiom,
! [VAR_0] : add(VAR_0,additive_identity) = VAR_0,
file('theBenchmark.p',additive_id1) ).
cnf(c_17,plain,
add(A,additive_identity) = A,
inference(clausify,[status(thm)],[additive_id1]) ).
fof(additive_id2,axiom,
! [VAR_0] : add(additive_identity,VAR_0) = VAR_0,
file('theBenchmark.p',additive_id2) ).
cnf(c_18,plain,
add(additive_identity,A) = A,
inference(clausify,[status(thm)],[additive_id2]) ).
fof(prove_associativity,axiom,
add(a,add(b,c)) != add(add(a,b),c),
file('theBenchmark.p',prove_associativity) ).
cnf(c_19,plain,
add(a,add(b,c)) != add(add(a,b),c),
inference(clausify,[status(thm)],[prove_associativity]) ).
cnf(c_8976,plain,
add(a,add(b,c)) != add(c,add(a,b)),
inference(paramod,[status(thm)],[c_1,c_19]) ).
cnf(c_20,plain,
add(c,add(a,b)) != add(a,add(b,c)),
inference(copy,[status(thm)],[c_8976]) ).
cnf(c_21,plain,
multiply(add(A,B),add(C,A)) = add(multiply(B,C),A),
inference(paramod,[status(thm)],[c_1,c_4]) ).
cnf(c_22,plain,
multiply(add(A,B),add(B,C)) = add(multiply(A,C),B),
inference(paramod,[status(thm)],[c_1,c_4]) ).
cnf(c_8977,plain,
add(A,multiply(B,B)) = add(multiply(A,A),B),
inference(paramod,[status(thm)],[c_6,c_4]) ).
cnf(c_23,plain,
add(multiply(A,A),B) = add(A,multiply(B,B)),
inference(copy,[status(thm)],[c_8977]) ).
cnf(c_24,plain,
add(multiply(A,B),multiply(C,A)) = multiply(add(B,C),A),
inference(paramod,[status(thm)],[c_2,c_8]) ).
cnf(c_25,plain,
add(multiply(A,B),multiply(B,C)) = multiply(add(A,C),B),
inference(paramod,[status(thm)],[c_2,c_8]) ).
cnf(c_26,plain,
multiply(multiply(add(A,B),C),add(D,multiply(B,C))) = add(multiply(multiply(A,C),D),multiply(B,C)),
inference(paramod,[status(thm)],[c_8,c_4]) ).
cnf(c_28,plain,
add(add(multiply(A,B),C),multiply(D,add(B,C))) = multiply(add(add(A,C),D),add(B,C)),
inference(paramod,[status(thm)],[c_4,c_8]) ).
cnf(c_32,plain,
add(add(A,multiply(B,C)),multiply(D,add(A,C))) = multiply(add(add(A,B),D),add(A,C)),
inference(paramod,[status(thm)],[c_6,c_8]) ).
cnf(c_8978,plain,
multiply(A,add(B,B)) = multiply(add(A,A),B),
inference(paramod,[status(thm)],[c_10,c_8]) ).
cnf(c_42,plain,
multiply(add(A,A),B) = multiply(A,add(B,B)),
inference(copy,[status(thm)],[c_8978]) ).
cnf(c_8979,plain,
multiply(multiplicative_identity,add(A,inverse(B))) = add(multiply(B,A),inverse(B)),
inference(paramod,[status(thm)],[c_11,c_4]) ).
cnf(c_8980,plain,
add(A,inverse(B)) = add(multiply(B,A),inverse(B)),
inference(paramod,[status(thm)],[c_16,c_8979]) ).
cnf(c_8981,plain,
add(A,inverse(B)) = add(inverse(B),multiply(B,A)),
inference(paramod,[status(thm)],[c_1,c_8980]) ).
cnf(c_43,plain,
add(inverse(A),multiply(A,B)) = add(B,inverse(A)),
inference(copy,[status(thm)],[c_8981]) ).
cnf(c_8982,plain,
multiply(add(A,B),multiplicative_identity) = add(A,multiply(B,inverse(A))),
inference(paramod,[status(thm)],[c_11,c_6]) ).
cnf(c_8983,plain,
multiply(multiplicative_identity,add(A,B)) = add(A,multiply(B,inverse(A))),
inference(paramod,[status(thm)],[c_2,c_8982]) ).
cnf(c_8984,plain,
add(A,B) = add(A,multiply(B,inverse(A))),
inference(paramod,[status(thm)],[c_16,c_8983]) ).
cnf(c_46,plain,
add(A,multiply(B,inverse(A))) = add(A,B),
inference(copy,[status(thm)],[c_8984]) ).
cnf(c_8985,plain,
add(additive_identity,multiply(A,inverse(B))) = multiply(add(B,A),inverse(B)),
inference(paramod,[status(thm)],[c_13,c_8]) ).
cnf(c_8986,plain,
multiply(A,inverse(B)) = multiply(add(B,A),inverse(B)),
inference(paramod,[status(thm)],[c_18,c_8985]) ).
cnf(c_8987,plain,
multiply(A,inverse(B)) = multiply(inverse(B),add(B,A)),
inference(paramod,[status(thm)],[c_2,c_8986]) ).
cnf(c_47,plain,
multiply(inverse(A),add(A,B)) = multiply(B,inverse(A)),
inference(copy,[status(thm)],[c_8987]) ).
cnf(c_8988,plain,
add(multiply(A,inverse(B)),additive_identity) = multiply(add(A,B),inverse(B)),
inference(paramod,[status(thm)],[c_13,c_8]) ).
cnf(c_8989,plain,
add(additive_identity,multiply(A,inverse(B))) = multiply(add(A,B),inverse(B)),
inference(paramod,[status(thm)],[c_1,c_8988]) ).
cnf(c_8990,plain,
multiply(A,inverse(B)) = multiply(add(A,B),inverse(B)),
inference(paramod,[status(thm)],[c_18,c_8989]) ).
cnf(c_8991,plain,
multiply(A,inverse(B)) = multiply(inverse(B),add(A,B)),
inference(paramod,[status(thm)],[c_2,c_8990]) ).
cnf(c_48,plain,
multiply(inverse(A),add(B,A)) = multiply(B,inverse(A)),
inference(copy,[status(thm)],[c_8991]) ).
cnf(c_8992,plain,
add(multiply(A,B),additive_identity) = multiply(A,add(B,inverse(A))),
inference(paramod,[status(thm)],[c_13,c_10]) ).
cnf(c_8993,plain,
add(additive_identity,multiply(A,B)) = multiply(A,add(B,inverse(A))),
inference(paramod,[status(thm)],[c_1,c_8992]) ).
cnf(c_8994,plain,
multiply(A,B) = multiply(A,add(B,inverse(A))),
inference(paramod,[status(thm)],[c_18,c_8993]) ).
cnf(c_50,plain,
multiply(A,add(B,inverse(A))) = multiply(A,B),
inference(copy,[status(thm)],[c_8994]) ).
cnf(c_8995,plain,
add(A,multiply(A,B)) = multiply(A,add(multiplicative_identity,B)),
inference(paramod,[status(thm)],[c_15,c_10]) ).
cnf(c_51,plain,
multiply(A,add(multiplicative_identity,B)) = add(A,multiply(A,B)),
inference(copy,[status(thm)],[c_8995]) ).
cnf(c_8996,plain,
add(multiply(A,B),A) = multiply(A,add(B,multiplicative_identity)),
inference(paramod,[status(thm)],[c_15,c_10]) ).
cnf(c_8997,plain,
add(A,multiply(A,B)) = multiply(A,add(B,multiplicative_identity)),
inference(paramod,[status(thm)],[c_1,c_8996]) ).
cnf(c_52,plain,
multiply(A,add(B,multiplicative_identity)) = add(A,multiply(A,B)),
inference(copy,[status(thm)],[c_8997]) ).
cnf(c_8998,plain,
add(A,multiply(B,A)) = multiply(add(multiplicative_identity,B),A),
inference(paramod,[status(thm)],[c_16,c_8]) ).
cnf(c_53,plain,
multiply(add(multiplicative_identity,A),B) = add(B,multiply(A,B)),
inference(copy,[status(thm)],[c_8998]) ).
cnf(c_8999,plain,
add(multiply(A,B),B) = multiply(add(A,multiplicative_identity),B),
inference(paramod,[status(thm)],[c_16,c_8]) ).
cnf(c_9000,plain,
add(B,multiply(A,B)) = multiply(add(A,multiplicative_identity),B),
inference(paramod,[status(thm)],[c_1,c_8999]) ).
cnf(c_54,plain,
multiply(add(A,multiplicative_identity),B) = add(B,multiply(A,B)),
inference(copy,[status(thm)],[c_9000]) ).
cnf(c_56,plain,
multiply(A,add(A,B)) = add(A,multiply(additive_identity,B)),
inference(paramod,[status(thm)],[c_17,c_6]) ).
cnf(c_9001,plain,
multiply(add(A,B),A) = add(A,multiply(B,additive_identity)),
inference(paramod,[status(thm)],[c_17,c_6]) ).
cnf(c_57,plain,
multiply(A,add(A,B)) = add(A,multiply(B,additive_identity)),
inference(paramod,[status(thm)],[c_2,c_9001]) ).
cnf(c_60,plain,
inverse(additive_identity) = multiplicative_identity,
inference(paramod,[status(thm)],[c_18,c_11]) ).
cnf(c_9002,plain,
add(multiplicative_identity,A) = add(multiplicative_identity,multiply(A,A)),
inference(paramod,[status(thm)],[c_15,c_23]) ).
cnf(c_84,plain,
add(multiplicative_identity,multiply(A,A)) = add(multiplicative_identity,A),
inference(copy,[status(thm)],[c_9002]) ).
cnf(c_147,plain,
multiply(A,add(A,B)) = add(multiply(additive_identity,B),A),
inference(paramod,[status(thm)],[c_18,c_22]) ).
cnf(c_170,plain,
multiply(A,add(multiplicative_identity,multiplicative_identity)) = add(A,A),
inference(paramod,[status(thm)],[c_42,c_15]) ).
cnf(c_9003,plain,
add(multiplicative_identity,multiply(multiplicative_identity,multiplicative_identity)) = multiply(multiplicative_identity,add(multiplicative_identity,multiplicative_identity)),
inference(paramod,[status(thm)],[c_170,c_84]) ).
cnf(c_9004,plain,
add(multiplicative_identity,multiplicative_identity) = multiply(multiplicative_identity,add(multiplicative_identity,multiplicative_identity)),
inference(paramod,[status(thm)],[c_15,c_9003]) ).
cnf(c_9005,plain,
add(multiplicative_identity,multiplicative_identity) = add(multiplicative_identity,multiply(additive_identity,multiplicative_identity)),
inference(paramod,[status(thm)],[c_56,c_9004]) ).
cnf(c_9006,plain,
add(multiplicative_identity,multiplicative_identity) = add(multiplicative_identity,additive_identity),
inference(paramod,[status(thm)],[c_15,c_9005]) ).
cnf(c_9007,plain,
add(multiplicative_identity,multiplicative_identity) = add(additive_identity,multiplicative_identity),
inference(paramod,[status(thm)],[c_1,c_9006]) ).
cnf(c_197,plain,
add(multiplicative_identity,multiplicative_identity) = multiplicative_identity,
inference(paramod,[status(thm)],[c_18,c_9007]) ).
cnf(c_9008,plain,
multiply(multiply(A,add(multiplicative_identity,multiplicative_identity)),add(A,B)) = add(multiply(A,B),A),
inference(paramod,[status(thm)],[c_170,c_22]) ).
cnf(c_9009,plain,
multiply(multiply(A,multiplicative_identity),add(A,B)) = add(multiply(A,B),A),
inference(paramod,[status(thm)],[c_197,c_9008]) ).
cnf(c_9010,plain,
multiply(A,add(A,B)) = add(multiply(A,B),A),
inference(paramod,[status(thm)],[c_15,c_9009]) ).
cnf(c_199,plain,
multiply(A,add(A,B)) = add(A,multiply(A,B)),
inference(paramod,[status(thm)],[c_1,c_9010]) ).
cnf(c_9011,plain,
multiply(add(A,B),multiply(B,add(multiplicative_identity,multiplicative_identity))) = add(multiply(A,B),B),
inference(paramod,[status(thm)],[c_170,c_22]) ).
cnf(c_9012,plain,
multiply(add(A,B),multiply(B,multiplicative_identity)) = add(multiply(A,B),B),
inference(paramod,[status(thm)],[c_197,c_9011]) ).
cnf(c_9013,plain,
multiply(add(A,B),B) = add(multiply(A,B),B),
inference(paramod,[status(thm)],[c_15,c_9012]) ).
cnf(c_9014,plain,
multiply(B,add(A,B)) = add(multiply(A,B),B),
inference(paramod,[status(thm)],[c_2,c_9013]) ).
cnf(c_200,plain,
multiply(A,add(B,A)) = add(A,multiply(B,A)),
inference(paramod,[status(thm)],[c_1,c_9014]) ).
cnf(c_9015,plain,
add(A,multiply(A,B)) = add(multiply(additive_identity,B),A),
inference(paramod,[status(thm)],[c_199,c_147]) ).
cnf(c_205,plain,
add(multiply(additive_identity,A),B) = add(B,multiply(B,A)),
inference(copy,[status(thm)],[c_9015]) ).
cnf(c_9016,plain,
add(A,multiply(A,B)) = add(A,multiply(B,additive_identity)),
inference(paramod,[status(thm)],[c_199,c_57]) ).
cnf(c_211,plain,
add(A,multiply(B,additive_identity)) = add(A,multiply(A,B)),
inference(copy,[status(thm)],[c_9016]) ).
cnf(c_9017,plain,
multiply(add(multiply(A,B),C),add(B,inverse(A))) = add(multiply(C,inverse(A)),multiply(A,B)),
inference(paramod,[status(thm)],[c_43,c_21]) ).
cnf(c_225,plain,
multiply(add(A,inverse(B)),add(multiply(B,A),C)) = add(multiply(C,inverse(B)),multiply(B,A)),
inference(paramod,[status(thm)],[c_2,c_9017]) ).
cnf(c_9018,plain,
add(multiplicative_identity,multiply(additive_identity,A)) = add(A,inverse(additive_identity)),
inference(paramod,[status(thm)],[c_60,c_43]) ).
cnf(c_227,plain,
add(multiplicative_identity,multiply(additive_identity,A)) = add(A,multiplicative_identity),
inference(paramod,[status(thm)],[c_60,c_9018]) ).
cnf(c_249,plain,
add(multiplicative_identity,multiply(A,additive_identity)) = add(A,multiplicative_identity),
inference(paramod,[status(thm)],[c_2,c_227]) ).
cnf(c_9019,plain,
add(multiply(multiplicative_identity,A),multiply(multiply(additive_identity,B),A)) = multiply(add(B,multiplicative_identity),A),
inference(paramod,[status(thm)],[c_227,c_8]) ).
cnf(c_253,plain,
add(A,multiply(multiply(additive_identity,B),A)) = multiply(add(B,multiplicative_identity),A),
inference(paramod,[status(thm)],[c_16,c_9019]) ).
cnf(c_9020,plain,
add(multiply(A,multiplicative_identity),multiply(A,multiply(B,additive_identity))) = multiply(A,add(B,multiplicative_identity)),
inference(paramod,[status(thm)],[c_249,c_10]) ).
cnf(c_260,plain,
add(A,multiply(A,multiply(B,additive_identity))) = multiply(A,add(B,multiplicative_identity)),
inference(paramod,[status(thm)],[c_15,c_9020]) ).
cnf(c_9021,plain,
add(multiply(inverse(A),B),multiply(C,inverse(A))) = multiply(inverse(A),add(B,add(C,A))),
inference(paramod,[status(thm)],[c_48,c_10]) ).
cnf(c_9022,plain,
multiply(add(B,C),inverse(A)) = multiply(inverse(A),add(B,add(C,A))),
inference(paramod,[status(thm)],[c_24,c_9021]) ).
cnf(c_314,plain,
multiply(inverse(A),add(B,add(C,A))) = multiply(add(B,C),inverse(A)),
inference(copy,[status(thm)],[c_9022]) ).
cnf(c_9023,plain,
multiply(inverse(multiply(additive_identity,A)),add(A,multiplicative_identity)) = multiply(multiplicative_identity,inverse(multiply(additive_identity,A))),
inference(paramod,[status(thm)],[c_227,c_48]) ).
cnf(c_9024,plain,
multiply(add(A,multiplicative_identity),inverse(multiply(additive_identity,A))) = multiply(multiplicative_identity,inverse(multiply(additive_identity,A))),
inference(paramod,[status(thm)],[c_2,c_9023]) ).
cnf(c_320,plain,
multiply(add(A,multiplicative_identity),inverse(multiply(additive_identity,A))) = inverse(multiply(additive_identity,A)),
inference(paramod,[status(thm)],[c_16,c_9024]) ).
cnf(c_325,plain,
multiply(A,add(multiplicative_identity,B)) = add(A,multiply(B,A)),
inference(paramod,[status(thm)],[c_2,c_51]) ).
cnf(c_9025,plain,
add(add(A,B),multiply(add(A,B),B)) = add(multiply(A,multiplicative_identity),B),
inference(paramod,[status(thm)],[c_51,c_4]) ).
cnf(c_9026,plain,
add(add(A,B),multiply(B,add(A,B))) = add(multiply(A,multiplicative_identity),B),
inference(paramod,[status(thm)],[c_2,c_9025]) ).
cnf(c_9027,plain,
add(add(A,B),add(B,multiply(A,B))) = add(multiply(A,multiplicative_identity),B),
inference(paramod,[status(thm)],[c_200,c_9026]) ).
cnf(c_326,plain,
add(add(A,B),add(B,multiply(A,B))) = add(A,B),
inference(paramod,[status(thm)],[c_15,c_9027]) ).
cnf(c_9028,plain,
multiply(multiply(A,B),add(multiplicative_identity,B)) = multiply(add(A,multiply(A,B)),B),
inference(paramod,[status(thm)],[c_51,c_8]) ).
cnf(c_335,plain,
multiply(multiply(A,B),add(multiplicative_identity,B)) = multiply(B,add(A,multiply(A,B))),
inference(paramod,[status(thm)],[c_2,c_9028]) ).
cnf(c_9029,plain,
add(add(A,B),multiply(add(A,B),A)) = add(multiply(B,multiplicative_identity),A),
inference(paramod,[status(thm)],[c_51,c_21]) ).
cnf(c_9030,plain,
add(add(A,B),multiply(A,add(A,B))) = add(multiply(B,multiplicative_identity),A),
inference(paramod,[status(thm)],[c_2,c_9029]) ).
cnf(c_9031,plain,
add(add(A,B),add(A,multiply(A,B))) = add(multiply(B,multiplicative_identity),A),
inference(paramod,[status(thm)],[c_199,c_9030]) ).
cnf(c_341,plain,
add(add(A,B),add(A,multiply(A,B))) = add(B,A),
inference(paramod,[status(thm)],[c_15,c_9031]) ).
cnf(c_9032,plain,
add(multiplicative_identity,add(additive_identity,multiply(additive_identity,A))) = add(add(multiplicative_identity,A),multiplicative_identity),
inference(paramod,[status(thm)],[c_51,c_227]) ).
cnf(c_9033,plain,
add(multiplicative_identity,multiply(additive_identity,A)) = add(add(multiplicative_identity,A),multiplicative_identity),
inference(paramod,[status(thm)],[c_18,c_9032]) ).
cnf(c_9034,plain,
add(A,multiplicative_identity) = add(add(multiplicative_identity,A),multiplicative_identity),
inference(paramod,[status(thm)],[c_227,c_9033]) ).
cnf(c_9035,plain,
add(A,multiplicative_identity) = add(multiplicative_identity,add(multiplicative_identity,A)),
inference(paramod,[status(thm)],[c_1,c_9034]) ).
cnf(c_350,plain,
add(multiplicative_identity,add(multiplicative_identity,A)) = add(A,multiplicative_identity),
inference(copy,[status(thm)],[c_9035]) ).
cnf(c_355,plain,
add(multiply(A,B),add(B,multiply(B,C))) = multiply(add(A,add(multiplicative_identity,C)),B),
inference(paramod,[status(thm)],[c_51,c_25]) ).
cnf(c_9036,plain,
multiply(A,add(multiplicative_identity,add(multiplicative_identity,B))) = add(A,add(A,multiply(A,B))),
inference(paramod,[status(thm)],[c_51,c_51]) ).
cnf(c_9037,plain,
multiply(A,add(B,multiplicative_identity)) = add(A,add(A,multiply(A,B))),
inference(paramod,[status(thm)],[c_350,c_9036]) ).
cnf(c_356,plain,
add(A,add(A,multiply(A,B))) = multiply(A,add(B,multiplicative_identity)),
inference(copy,[status(thm)],[c_9037]) ).
cnf(c_9038,plain,
multiply(multiply(A,B),add(B,multiplicative_identity)) = multiply(add(A,multiply(A,B)),B),
inference(paramod,[status(thm)],[c_52,c_8]) ).
cnf(c_376,plain,
multiply(multiply(A,B),add(B,multiplicative_identity)) = multiply(B,add(A,multiply(A,B))),
inference(paramod,[status(thm)],[c_2,c_9038]) ).
cnf(c_9039,plain,
multiply(multiply(add(A,additive_identity),B),add(B,multiplicative_identity)) = add(multiply(multiply(A,B),multiplicative_identity),multiply(additive_identity,B)),
inference(paramod,[status(thm)],[c_227,c_26]) ).
cnf(c_9040,plain,
multiply(multiply(A,B),add(B,multiplicative_identity)) = add(multiply(multiply(A,B),multiplicative_identity),multiply(additive_identity,B)),
inference(paramod,[status(thm)],[c_17,c_9039]) ).
cnf(c_9041,plain,
multiply(multiply(A,B),add(B,multiplicative_identity)) = add(multiply(multiplicative_identity,multiply(A,B)),multiply(additive_identity,B)),
inference(paramod,[status(thm)],[c_2,c_9040]) ).
cnf(c_9042,plain,
multiply(multiply(A,B),add(B,multiplicative_identity)) = add(multiply(A,B),multiply(additive_identity,B)),
inference(paramod,[status(thm)],[c_16,c_9041]) ).
cnf(c_9043,plain,
multiply(multiply(A,B),add(B,multiplicative_identity)) = multiply(add(A,additive_identity),B),
inference(paramod,[status(thm)],[c_8,c_9042]) ).
cnf(c_421,plain,
multiply(multiply(A,B),add(B,multiplicative_identity)) = multiply(A,B),
inference(paramod,[status(thm)],[c_17,c_9043]) ).
cnf(c_9044,plain,
multiply(A,B) = multiply(B,add(A,multiply(A,B))),
inference(paramod,[status(thm)],[c_421,c_376]) ).
cnf(c_448,plain,
multiply(A,add(B,multiply(B,A))) = multiply(B,A),
inference(copy,[status(thm)],[c_9044]) ).
cnf(c_449,plain,
multiply(multiply(A,B),add(multiplicative_identity,B)) = multiply(A,B),
inference(paramod,[status(thm)],[c_448,c_335]) ).
cnf(c_473,plain,
add(add(A,multiply(B,A)),multiply(A,C)) = multiply(add(add(multiplicative_identity,B),C),A),
inference(paramod,[status(thm)],[c_53,c_25]) ).
cnf(c_9045,plain,
multiply(add(A,multiplicative_identity),add(multiplicative_identity,B)) = add(add(A,multiplicative_identity),add(B,multiply(A,B))),
inference(paramod,[status(thm)],[c_54,c_51]) ).
cnf(c_9046,plain,
add(multiply(A,B),multiplicative_identity) = add(add(A,multiplicative_identity),add(B,multiply(A,B))),
inference(paramod,[status(thm)],[c_22,c_9045]) ).
cnf(c_9047,plain,
add(multiplicative_identity,multiply(A,B)) = add(add(A,multiplicative_identity),add(B,multiply(A,B))),
inference(paramod,[status(thm)],[c_1,c_9046]) ).
cnf(c_502,plain,
add(add(A,multiplicative_identity),add(B,multiply(A,B))) = add(multiplicative_identity,multiply(A,B)),
inference(copy,[status(thm)],[c_9047]) ).
cnf(c_9048,plain,
add(multiply(A,B),add(B,multiply(B,C))) = multiply(add(A,add(B,C)),B),
inference(paramod,[status(thm)],[c_199,c_25]) ).
cnf(c_9049,plain,
multiply(add(A,add(multiplicative_identity,C)),B) = multiply(add(A,add(B,C)),B),
inference(paramod,[status(thm)],[c_355,c_9048]) ).
cnf(c_517,plain,
multiply(add(A,add(multiplicative_identity,B)),C) = multiply(C,add(A,add(C,B))),
inference(paramod,[status(thm)],[c_2,c_9049]) ).
cnf(c_528,plain,
multiply(A,multiply(add(B,multiplicative_identity),A)) = add(A,multiply(A,multiply(B,A))),
inference(paramod,[status(thm)],[c_54,c_199]) ).
cnf(c_9050,plain,
add(add(A,multiply(B,A)),multiply(A,C)) = multiply(A,add(add(B,A),C)),
inference(paramod,[status(thm)],[c_200,c_10]) ).
cnf(c_529,plain,
multiply(add(add(multiplicative_identity,A),B),C) = multiply(C,add(add(A,C),B)),
inference(paramod,[status(thm)],[c_473,c_9050]) ).
cnf(c_9051,plain,
multiply(multiply(A,B),multiply(add(multiplicative_identity,A),B)) = add(multiply(A,B),multiply(B,multiply(A,B))),
inference(paramod,[status(thm)],[c_53,c_200]) ).
cnf(c_9052,plain,
multiply(multiply(A,B),multiply(add(multiplicative_identity,A),B)) = multiply(multiply(A,B),add(multiplicative_identity,B)),
inference(paramod,[status(thm)],[c_325,c_9051]) ).
cnf(c_546,plain,
multiply(multiply(A,B),multiply(add(multiplicative_identity,A),B)) = multiply(A,B),
inference(paramod,[status(thm)],[c_449,c_9052]) ).
cnf(c_9053,plain,
add(inverse(multiply(additive_identity,A)),multiply(inverse(multiply(additive_identity,A)),A)) = multiplicative_identity,
inference(paramod,[status(thm)],[c_205,c_11]) ).
cnf(c_9054,plain,
add(inverse(multiply(additive_identity,A)),multiply(A,inverse(multiply(additive_identity,A)))) = multiplicative_identity,
inference(paramod,[status(thm)],[c_2,c_9053]) ).
cnf(c_9055,plain,
multiply(inverse(multiply(additive_identity,A)),add(multiplicative_identity,A)) = multiplicative_identity,
inference(paramod,[status(thm)],[c_325,c_9054]) ).
cnf(c_561,plain,
multiply(add(multiplicative_identity,A),inverse(multiply(additive_identity,A))) = multiplicative_identity,
inference(paramod,[status(thm)],[c_2,c_9055]) ).
cnf(c_570,plain,
multiply(inverse(multiply(additive_identity,A)),add(B,multiply(B,A))) = multiply(B,inverse(multiply(additive_identity,A))),
inference(paramod,[status(thm)],[c_205,c_47]) ).
cnf(c_9056,plain,
add(multiply(additive_identity,add(multiplicative_identity,A)),B) = add(B,add(B,multiply(B,A))),
inference(paramod,[status(thm)],[c_51,c_205]) ).
cnf(c_9057,plain,
add(add(additive_identity,multiply(additive_identity,A)),B) = add(B,add(B,multiply(B,A))),
inference(paramod,[status(thm)],[c_51,c_9056]) ).
cnf(c_9058,plain,
add(multiply(additive_identity,A),B) = add(B,add(B,multiply(B,A))),
inference(paramod,[status(thm)],[c_18,c_9057]) ).
cnf(c_9059,plain,
add(multiply(additive_identity,A),B) = multiply(B,add(A,multiplicative_identity)),
inference(paramod,[status(thm)],[c_356,c_9058]) ).
cnf(c_578,plain,
multiply(A,add(B,multiplicative_identity)) = add(multiply(additive_identity,B),A),
inference(copy,[status(thm)],[c_9059]) ).
cnf(c_9060,plain,
multiply(A,add(multiply(additive_identity,B),A)) = add(A,multiply(A,multiply(A,B))),
inference(paramod,[status(thm)],[c_205,c_199]) ).
cnf(c_9061,plain,
add(A,multiply(multiply(additive_identity,B),A)) = add(A,multiply(A,multiply(A,B))),
inference(paramod,[status(thm)],[c_200,c_9060]) ).
cnf(c_9062,plain,
multiply(add(B,multiplicative_identity),A) = add(A,multiply(A,multiply(A,B))),
inference(paramod,[status(thm)],[c_253,c_9061]) ).
cnf(c_587,plain,
add(A,multiply(A,multiply(A,B))) = multiply(add(B,multiplicative_identity),A),
inference(copy,[status(thm)],[c_9062]) ).
cnf(c_619,plain,
add(A,multiply(A,multiply(B,additive_identity))) = add(multiply(additive_identity,B),A),
inference(paramod,[status(thm)],[c_578,c_260]) ).
cnf(c_9063,plain,
add(add(A,multiplicative_identity),multiply(B,additive_identity)) = add(add(A,multiplicative_identity),add(B,multiply(A,B))),
inference(paramod,[status(thm)],[c_54,c_211]) ).
cnf(c_719,plain,
add(add(A,multiplicative_identity),multiply(B,additive_identity)) = add(multiplicative_identity,multiply(A,B)),
inference(paramod,[status(thm)],[c_502,c_9063]) ).
cnf(c_9064,plain,
multiply(A,add(A,multiply(A,B))) = add(A,multiply(A,multiply(B,additive_identity))),
inference(paramod,[status(thm)],[c_211,c_199]) ).
cnf(c_9065,plain,
add(A,multiply(A,multiply(A,B))) = add(A,multiply(A,multiply(B,additive_identity))),
inference(paramod,[status(thm)],[c_199,c_9064]) ).
cnf(c_9066,plain,
multiply(add(B,multiplicative_identity),A) = add(A,multiply(A,multiply(B,additive_identity))),
inference(paramod,[status(thm)],[c_587,c_9065]) ).
cnf(c_720,plain,
multiply(add(A,multiplicative_identity),B) = add(multiply(additive_identity,A),B),
inference(paramod,[status(thm)],[c_619,c_9066]) ).
cnf(c_9067,plain,
multiply(A,add(multiply(additive_identity,B),A)) = add(A,multiply(A,multiply(B,A))),
inference(paramod,[status(thm)],[c_720,c_528]) ).
cnf(c_9068,plain,
add(A,multiply(multiply(additive_identity,B),A)) = add(A,multiply(A,multiply(B,A))),
inference(paramod,[status(thm)],[c_200,c_9067]) ).
cnf(c_9069,plain,
multiply(add(B,multiplicative_identity),A) = add(A,multiply(A,multiply(B,A))),
inference(paramod,[status(thm)],[c_253,c_9068]) ).
cnf(c_9070,plain,
add(multiply(additive_identity,B),A) = add(A,multiply(A,multiply(B,A))),
inference(paramod,[status(thm)],[c_720,c_9069]) ).
cnf(c_735,plain,
add(A,multiply(A,multiply(B,A))) = add(multiply(additive_identity,B),A),
inference(copy,[status(thm)],[c_9070]) ).
cnf(c_9071,plain,
add(multiply(additive_identity,A),inverse(multiply(additive_identity,A))) = inverse(multiply(additive_identity,A)),
inference(paramod,[status(thm)],[c_720,c_320]) ).
cnf(c_9072,plain,
multiplicative_identity = inverse(multiply(additive_identity,A)),
inference(paramod,[status(thm)],[c_11,c_9071]) ).
cnf(c_752,plain,
inverse(multiply(additive_identity,A)) = multiplicative_identity,
inference(copy,[status(thm)],[c_9072]) ).
cnf(c_9073,plain,
multiply(multiplicative_identity,add(B,multiply(B,A))) = multiply(B,inverse(multiply(additive_identity,A))),
inference(paramod,[status(thm)],[c_752,c_570]) ).
cnf(c_9074,plain,
add(B,multiply(B,A)) = multiply(B,inverse(multiply(additive_identity,A))),
inference(paramod,[status(thm)],[c_16,c_9073]) ).
cnf(c_9075,plain,
add(B,multiply(B,A)) = multiply(B,multiplicative_identity),
inference(paramod,[status(thm)],[c_752,c_9074]) ).
cnf(c_760,plain,
add(A,multiply(A,B)) = A,
inference(paramod,[status(thm)],[c_15,c_9075]) ).
cnf(c_9076,plain,
multiply(add(multiplicative_identity,A),multiplicative_identity) = multiplicative_identity,
inference(paramod,[status(thm)],[c_752,c_561]) ).
cnf(c_9077,plain,
multiply(multiplicative_identity,add(multiplicative_identity,A)) = multiplicative_identity,
inference(paramod,[status(thm)],[c_2,c_9076]) ).
cnf(c_9078,plain,
add(multiplicative_identity,multiply(multiplicative_identity,A)) = multiplicative_identity,
inference(paramod,[status(thm)],[c_199,c_9077]) ).
cnf(c_761,plain,
add(multiplicative_identity,A) = multiplicative_identity,
inference(paramod,[status(thm)],[c_16,c_9078]) ).
cnf(c_9079,plain,
A = add(multiply(additive_identity,B),A),
inference(paramod,[status(thm)],[c_760,c_735]) ).
cnf(c_762,plain,
add(multiply(additive_identity,A),B) = B,
inference(copy,[status(thm)],[c_9079]) ).
cnf(c_9080,plain,
add(multiply(A,B),B) = multiply(add(A,add(multiplicative_identity,C)),B),
inference(paramod,[status(thm)],[c_760,c_355]) ).
cnf(c_9081,plain,
add(B,multiply(A,B)) = multiply(add(A,add(multiplicative_identity,C)),B),
inference(paramod,[status(thm)],[c_1,c_9080]) ).
cnf(c_9082,plain,
add(B,multiply(A,B)) = multiply(add(A,multiplicative_identity),B),
inference(paramod,[status(thm)],[c_761,c_9081]) ).
cnf(c_9083,plain,
add(B,multiply(A,B)) = add(multiply(additive_identity,A),B),
inference(paramod,[status(thm)],[c_720,c_9082]) ).
cnf(c_787,plain,
add(A,multiply(B,A)) = A,
inference(paramod,[status(thm)],[c_762,c_9083]) ).
cnf(c_9084,plain,
add(add(A,B),A) = add(B,A),
inference(paramod,[status(thm)],[c_760,c_341]) ).
cnf(c_788,plain,
add(A,add(A,B)) = add(B,A),
inference(paramod,[status(thm)],[c_1,c_9084]) ).
cnf(c_790,plain,
add(A,multiply(B,additive_identity)) = A,
inference(paramod,[status(thm)],[c_760,c_211]) ).
cnf(c_792,plain,
multiply(A,add(A,B)) = A,
inference(paramod,[status(thm)],[c_760,c_199]) ).
cnf(c_9085,plain,
add(A,multiplicative_identity) = add(multiplicative_identity,multiply(A,B)),
inference(paramod,[status(thm)],[c_790,c_719]) ).
cnf(c_793,plain,
add(A,multiplicative_identity) = multiplicative_identity,
inference(paramod,[status(thm)],[c_761,c_9085]) ).
cnf(c_9086,plain,
multiply(multiply(A,B),multiply(multiplicative_identity,B)) = multiply(A,B),
inference(paramod,[status(thm)],[c_761,c_546]) ).
cnf(c_9087,plain,
multiply(multiply(A,B),B) = multiply(A,B),
inference(paramod,[status(thm)],[c_16,c_9086]) ).
cnf(c_803,plain,
multiply(A,multiply(B,A)) = multiply(B,A),
inference(paramod,[status(thm)],[c_2,c_9087]) ).
cnf(c_9088,plain,
multiply(add(multiplicative_identity,B),C) = multiply(C,add(add(A,C),B)),
inference(paramod,[status(thm)],[c_761,c_529]) ).
cnf(c_9089,plain,
multiply(multiplicative_identity,C) = multiply(C,add(add(A,C),B)),
inference(paramod,[status(thm)],[c_761,c_9088]) ).
cnf(c_9090,plain,
C = multiply(C,add(add(A,C),B)),
inference(paramod,[status(thm)],[c_16,c_9089]) ).
cnf(c_806,plain,
multiply(A,add(add(B,A),C)) = A,
inference(copy,[status(thm)],[c_9090]) ).
cnf(c_9091,plain,
multiply(add(A,multiplicative_identity),C) = multiply(C,add(A,add(C,B))),
inference(paramod,[status(thm)],[c_761,c_517]) ).
cnf(c_9092,plain,
multiply(multiplicative_identity,C) = multiply(C,add(A,add(C,B))),
inference(paramod,[status(thm)],[c_793,c_9091]) ).
cnf(c_9093,plain,
C = multiply(C,add(A,add(C,B))),
inference(paramod,[status(thm)],[c_16,c_9092]) ).
cnf(c_807,plain,
multiply(A,add(B,add(A,C))) = A,
inference(copy,[status(thm)],[c_9093]) ).
cnf(c_9094,plain,
add(add(A,B),B) = add(A,B),
inference(paramod,[status(thm)],[c_787,c_326]) ).
cnf(c_845,plain,
add(A,add(B,A)) = add(B,A),
inference(paramod,[status(thm)],[c_1,c_9094]) ).
cnf(c_848,plain,
multiply(A,add(B,A)) = A,
inference(paramod,[status(thm)],[c_787,c_200]) ).
cnf(c_9095,plain,
add(add(multiply(A,add(A,B)),B),multiply(C,add(add(A,B),B))) = add(add(A,B),multiply(C,B)),
inference(paramod,[status(thm)],[c_6,c_28]) ).
cnf(c_9096,plain,
add(add(A,B),multiply(C,add(add(A,B),B))) = add(add(A,B),multiply(C,B)),
inference(paramod,[status(thm)],[c_792,c_9095]) ).
cnf(c_9097,plain,
add(add(A,B),multiply(C,add(B,add(A,B)))) = add(add(A,B),multiply(C,B)),
inference(paramod,[status(thm)],[c_1,c_9096]) ).
cnf(c_9098,plain,
add(add(A,B),multiply(C,add(A,B))) = add(add(A,B),multiply(C,B)),
inference(paramod,[status(thm)],[c_845,c_9097]) ).
cnf(c_9099,plain,
add(A,B) = add(add(A,B),multiply(C,B)),
inference(paramod,[status(thm)],[c_787,c_9098]) ).
cnf(c_862,plain,
add(add(A,B),multiply(C,B)) = add(A,B),
inference(copy,[status(thm)],[c_9099]) ).
cnf(c_1044,plain,
multiply(add(A,B),add(C,add(B,A))) = add(multiply(B,C),add(B,A)),
inference(paramod,[status(thm)],[c_788,c_4]) ).
cnf(c_9100,plain,
add(multiply(A,B),multiply(C,multiply(A,B))) = multiply(add(B,C),multiply(A,B)),
inference(paramod,[status(thm)],[c_803,c_8]) ).
cnf(c_9101,plain,
multiply(A,B) = multiply(add(B,C),multiply(A,B)),
inference(paramod,[status(thm)],[c_787,c_9100]) ).
cnf(c_1098,plain,
multiply(add(A,B),multiply(C,A)) = multiply(C,A),
inference(copy,[status(thm)],[c_9101]) ).
cnf(c_9102,plain,
multiply(add(A,B),add(C,add(A,B))) = add(multiply(B,C),add(A,B)),
inference(paramod,[status(thm)],[c_845,c_4]) ).
cnf(c_9103,plain,
add(A,B) = add(multiply(B,C),add(A,B)),
inference(paramod,[status(thm)],[c_848,c_9102]) ).
cnf(c_1115,plain,
add(multiply(A,B),add(C,A)) = add(C,A),
inference(copy,[status(thm)],[c_9103]) ).
cnf(c_9104,plain,
add(multiply(add(A,inverse(B)),C),multiply(B,A)) = multiply(add(C,B),add(A,inverse(B))),
inference(paramod,[status(thm)],[c_50,c_24]) ).
cnf(c_1222,plain,
add(multiply(A,B),multiply(add(B,inverse(A)),C)) = multiply(add(C,A),add(B,inverse(A))),
inference(paramod,[status(thm)],[c_1,c_9104]) ).
cnf(c_9105,plain,
add(add(A,multiply(B,C)),multiply(A,inverse(C))) = multiply(add(add(A,B),inverse(C)),add(A,C)),
inference(paramod,[status(thm)],[c_48,c_32]) ).
cnf(c_9106,plain,
add(multiply(A,inverse(C)),add(A,multiply(B,C))) = multiply(add(add(A,B),inverse(C)),add(A,C)),
inference(paramod,[status(thm)],[c_1,c_9105]) ).
cnf(c_9107,plain,
add(multiply(A,inverse(C)),add(A,multiply(B,C))) = multiply(add(A,C),add(add(A,B),inverse(C))),
inference(paramod,[status(thm)],[c_2,c_9106]) ).
cnf(c_1313,plain,
multiply(add(A,B),add(add(A,C),inverse(B))) = add(multiply(A,inverse(B)),add(A,multiply(C,B))),
inference(copy,[status(thm)],[c_9107]) ).
cnf(c_1345,plain,
add(add(A,B),multiply(C,A)) = add(B,A),
inference(paramod,[status(thm)],[c_1,c_862]) ).
cnf(c_9108,plain,
add(multiply(A,B),multiply(add(B,C),D)) = multiply(add(B,C),add(multiply(A,B),D)),
inference(paramod,[status(thm)],[c_1098,c_10]) ).
cnf(c_1446,plain,
multiply(add(A,B),add(multiply(C,A),D)) = add(multiply(C,A),multiply(add(A,B),D)),
inference(copy,[status(thm)],[c_9108]) ).
cnf(c_9109,plain,
add(multiply(B,A),multiply(add(A,inverse(B)),C)) = add(multiply(C,inverse(B)),multiply(B,A)),
inference(paramod,[status(thm)],[c_1446,c_225]) ).
cnf(c_1463,plain,
multiply(add(A,B),add(C,inverse(B))) = add(multiply(A,inverse(B)),multiply(B,C)),
inference(paramod,[status(thm)],[c_1222,c_9109]) ).
cnf(c_1467,plain,
add(multiply(A,inverse(B)),multiply(B,add(A,C))) = add(multiply(A,inverse(B)),add(A,multiply(C,B))),
inference(paramod,[status(thm)],[c_1463,c_1313]) ).
cnf(c_1504,plain,
add(multiply(A,B),add(A,C)) = add(C,A),
inference(paramod,[status(thm)],[c_1,c_1115]) ).
cnf(c_1537,plain,
add(multiply(A,inverse(B)),multiply(B,add(A,C))) = add(multiply(C,B),A),
inference(paramod,[status(thm)],[c_1504,c_1467]) ).
cnf(c_1538,plain,
multiply(add(A,B),add(C,add(B,A))) = add(A,B),
inference(paramod,[status(thm)],[c_1504,c_1044]) ).
cnf(c_9110,plain,
multiply(add(A,B),add(C,add(B,A))) = add(multiply(multiply(D,B),C),add(B,A)),
inference(paramod,[status(thm)],[c_1345,c_21]) ).
cnf(c_9111,plain,
add(A,B) = add(multiply(multiply(D,B),C),add(B,A)),
inference(paramod,[status(thm)],[c_1538,c_9110]) ).
cnf(c_1608,plain,
add(multiply(multiply(A,B),C),add(B,D)) = add(D,B),
inference(copy,[status(thm)],[c_9111]) ).
cnf(c_9112,plain,
add(multiply(add(A,B),inverse(C)),multiply(C,add(B,A))) = add(multiply(multiply(D,A),C),add(A,B)),
inference(paramod,[status(thm)],[c_1345,c_1537]) ).
cnf(c_7879,plain,
add(multiply(add(A,B),inverse(C)),multiply(C,add(B,A))) = add(B,A),
inference(paramod,[status(thm)],[c_1608,c_9112]) ).
cnf(c_9113,plain,
add(multiply(add(A,add(B,C)),inverse(C)),C) = add(add(B,C),A),
inference(paramod,[status(thm)],[c_806,c_7879]) ).
cnf(c_9114,plain,
add(multiply(inverse(C),add(A,add(B,C))),C) = add(add(B,C),A),
inference(paramod,[status(thm)],[c_2,c_9113]) ).
cnf(c_9115,plain,
add(multiply(add(A,B),inverse(C)),C) = add(add(B,C),A),
inference(paramod,[status(thm)],[c_314,c_9114]) ).
cnf(c_9116,plain,
add(C,multiply(add(A,B),inverse(C))) = add(add(B,C),A),
inference(paramod,[status(thm)],[c_1,c_9115]) ).
cnf(c_9117,plain,
add(C,add(A,B)) = add(add(B,C),A),
inference(paramod,[status(thm)],[c_46,c_9116]) ).
cnf(c_8972,plain,
add(add(A,B),C) = add(B,add(C,A)),
inference(copy,[status(thm)],[c_9117]) ).
cnf(c_9118,plain,
add(multiply(add(add(A,B),C),inverse(A)),A) = add(C,add(A,B)),
inference(paramod,[status(thm)],[c_807,c_7879]) ).
cnf(c_9119,plain,
add(multiply(add(B,add(C,A)),inverse(A)),A) = add(C,add(A,B)),
inference(paramod,[status(thm)],[c_8972,c_9118]) ).
cnf(c_9120,plain,
add(multiply(inverse(A),add(B,add(C,A))),A) = add(C,add(A,B)),
inference(paramod,[status(thm)],[c_2,c_9119]) ).
cnf(c_9121,plain,
add(multiply(add(B,C),inverse(A)),A) = add(C,add(A,B)),
inference(paramod,[status(thm)],[c_314,c_9120]) ).
cnf(c_9122,plain,
add(A,multiply(add(B,C),inverse(A))) = add(C,add(A,B)),
inference(paramod,[status(thm)],[c_1,c_9121]) ).
cnf(c_8974,plain,
add(A,add(B,C)) = add(C,add(A,B)),
inference(paramod,[status(thm)],[c_46,c_9122]) ).
cnf(c_9123,plain,
add(a,add(b,c)) != add(c,add(a,b)),
inference(copy,[status(thm)],[c_20]) ).
cnf(c_8975,plain,
$false,
inference(resolve,[status(thm)],[c_8974,c_9123]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : BOO008-2 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.07 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.43 % Computer : n003.cluster.edu
% 0.17/0.43 % Model : x86_64 x86_64
% 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.43 % Memory : 8046.5625MB
% 0.17/0.43 % OS : Linux 6.8.0-71-generic
% 0.17/0.43 % CPULimit : 300
% 0.17/0.43 % WCLimit : 300
% 0.17/0.43 % DateTime : Sat Sep 26 22:36:24 UTC 2026
% 0.17/0.43 % CPUTime :
% 0.17/0.44 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.17/0.44 % Process 3946892 was started by sandbox on n003,
% 0.17/0.44 % Sat Sep 26 22:36:24 2026
% 0.17/0.44 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.17/0.45
% 0.17/0.45 % From the command line: assign(max_seconds, 300).
% 36.03/5.07
% 36.03/5.07 % Assigning unary symbol inverse kb_weight 0 and highest precedence (9).
% 36.03/5.07
% 36.03/5.07 % SZS status Unsatisfiable for theBenchmark
% 36.03/5.07
% 36.03/5.07 % Proof 1 at 3.71 (+ 0.86) seconds.
% 36.03/5.07 % Length of proof is 111.
% 36.03/5.07 % Level of proof is 22.
% 36.03/5.07 % Maximum clause weight is 51.000.
% 36.03/5.07 % Given clauses 191.
% 36.03/5.07
% 36.03/5.07 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------