%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : BOO007-1 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n011.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 41.06s 6.31s
% Output : CNFRefutation 41.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 22
% Syntax : Number of formulae : 220 ( 133 unt; 0 def)
% Number of atoms : 398 ( 51 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 363 ( 185 ~; 178 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 3 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 12 ( 12 usr; 9 con; 0-2 aty)
% Number of variables : 386 ( 10 sgn 65 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(closure_of_addition,axiom,
! [VAR_0,VAR_1] : sum(VAR_0,VAR_1,add(VAR_0,VAR_1)),
file('theBenchmark.p',closure_of_addition) ).
cnf(c_1,plain,
sum(A,B,add(A,B)),
inference(clausify,[status(thm)],[closure_of_addition]) ).
fof(closure_of_multiplication,axiom,
! [VAR_0,VAR_1] : product(VAR_0,VAR_1,multiply(VAR_0,VAR_1)),
file('theBenchmark.p',closure_of_multiplication) ).
cnf(c_2,plain,
product(A,B,multiply(A,B)),
inference(clausify,[status(thm)],[closure_of_multiplication]) ).
fof(commutativity_of_addition,axiom,
! [VAR_0,VAR_1,VAR_2] :
( sum(VAR_1,VAR_0,VAR_2)
| ~ sum(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',commutativity_of_addition) ).
cnf(c_3,plain,
( sum(B,A,C)
| ~ sum(A,B,C) ),
inference(clausify,[status(thm)],[commutativity_of_addition]) ).
fof(commutativity_of_multiplication,axiom,
! [VAR_0,VAR_1,VAR_2] :
( product(VAR_1,VAR_0,VAR_2)
| ~ product(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',commutativity_of_multiplication) ).
cnf(c_4,plain,
( product(B,A,C)
| ~ product(A,B,C) ),
inference(clausify,[status(thm)],[commutativity_of_multiplication]) ).
fof(additive_identity1,axiom,
! [VAR_0] : sum(additive_identity,VAR_0,VAR_0),
file('theBenchmark.p',additive_identity1) ).
cnf(c_5,plain,
sum(additive_identity,A,A),
inference(clausify,[status(thm)],[additive_identity1]) ).
fof(additive_identity2,axiom,
! [VAR_0] : sum(VAR_0,additive_identity,VAR_0),
file('theBenchmark.p',additive_identity2) ).
cnf(c_6,plain,
sum(A,additive_identity,A),
inference(clausify,[status(thm)],[additive_identity2]) ).
fof(multiplicative_identity1,axiom,
! [VAR_0] : product(multiplicative_identity,VAR_0,VAR_0),
file('theBenchmark.p',multiplicative_identity1) ).
cnf(c_7,plain,
product(multiplicative_identity,A,A),
inference(clausify,[status(thm)],[multiplicative_identity1]) ).
fof(multiplicative_identity2,axiom,
! [VAR_0] : product(VAR_0,multiplicative_identity,VAR_0),
file('theBenchmark.p',multiplicative_identity2) ).
cnf(c_8,plain,
product(A,multiplicative_identity,A),
inference(clausify,[status(thm)],[multiplicative_identity2]) ).
fof(distributivity1,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( sum(VAR_2,VAR_4,VAR_6)
| ~ product(VAR_0,VAR_5,VAR_6)
| ~ sum(VAR_1,VAR_3,VAR_5)
| ~ product(VAR_0,VAR_3,VAR_4)
| ~ product(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',distributivity1) ).
cnf(c_9,plain,
( sum(C,E,V6)
| ~ product(A,F,V6)
| ~ sum(B,D,F)
| ~ product(A,D,E)
| ~ product(A,B,C) ),
inference(clausify,[status(thm)],[distributivity1]) ).
fof(distributivity3,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( sum(VAR_2,VAR_4,VAR_6)
| ~ product(VAR_5,VAR_1,VAR_6)
| ~ sum(VAR_0,VAR_3,VAR_5)
| ~ product(VAR_3,VAR_1,VAR_4)
| ~ product(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',distributivity3) ).
cnf(c_11,plain,
( sum(C,E,V6)
| ~ product(F,B,V6)
| ~ sum(A,D,F)
| ~ product(D,B,E)
| ~ product(A,B,C) ),
inference(clausify,[status(thm)],[distributivity3]) ).
fof(distributivity4,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( product(VAR_5,VAR_1,VAR_6)
| ~ sum(VAR_2,VAR_4,VAR_6)
| ~ sum(VAR_0,VAR_3,VAR_5)
| ~ product(VAR_3,VAR_1,VAR_4)
| ~ product(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',distributivity4) ).
cnf(c_12,plain,
( product(F,B,V6)
| ~ sum(C,E,V6)
| ~ sum(A,D,F)
| ~ product(D,B,E)
| ~ product(A,B,C) ),
inference(clausify,[status(thm)],[distributivity4]) ).
fof(distributivity5,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( product(VAR_2,VAR_4,VAR_6)
| ~ sum(VAR_0,VAR_5,VAR_6)
| ~ product(VAR_1,VAR_3,VAR_5)
| ~ sum(VAR_0,VAR_3,VAR_4)
| ~ sum(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',distributivity5) ).
cnf(c_13,plain,
( product(C,E,V6)
| ~ sum(A,F,V6)
| ~ product(B,D,F)
| ~ sum(A,D,E)
| ~ sum(A,B,C) ),
inference(clausify,[status(thm)],[distributivity5]) ).
fof(distributivity6,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( sum(VAR_0,VAR_5,VAR_6)
| ~ product(VAR_2,VAR_4,VAR_6)
| ~ product(VAR_1,VAR_3,VAR_5)
| ~ sum(VAR_0,VAR_3,VAR_4)
| ~ sum(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',distributivity6) ).
cnf(c_14,plain,
( sum(A,F,V6)
| ~ product(C,E,V6)
| ~ product(B,D,F)
| ~ sum(A,D,E)
| ~ sum(A,B,C) ),
inference(clausify,[status(thm)],[distributivity6]) ).
fof(distributivity7,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( product(VAR_2,VAR_4,VAR_6)
| ~ sum(VAR_5,VAR_1,VAR_6)
| ~ product(VAR_0,VAR_3,VAR_5)
| ~ sum(VAR_3,VAR_1,VAR_4)
| ~ sum(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',distributivity7) ).
cnf(c_15,plain,
( product(C,E,V6)
| ~ sum(F,B,V6)
| ~ product(A,D,F)
| ~ sum(D,B,E)
| ~ sum(A,B,C) ),
inference(clausify,[status(thm)],[distributivity7]) ).
fof(additive_inverse1,axiom,
! [VAR_0] : sum(inverse(VAR_0),VAR_0,multiplicative_identity),
file('theBenchmark.p',additive_inverse1) ).
cnf(c_17,plain,
sum(inverse(A),A,multiplicative_identity),
inference(clausify,[status(thm)],[additive_inverse1]) ).
fof(addition_is_well_defined,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( VAR_2 = VAR_3
| ~ sum(VAR_0,VAR_1,VAR_3)
| ~ sum(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',addition_is_well_defined) ).
cnf(c_21,plain,
( C = D
| ~ sum(A,B,D)
| ~ sum(A,B,C) ),
inference(clausify,[status(thm)],[addition_is_well_defined]) ).
fof(multiplication_is_well_defined,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] :
( VAR_2 = VAR_3
| ~ product(VAR_0,VAR_1,VAR_3)
| ~ product(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',multiplication_is_well_defined) ).
cnf(c_22,plain,
( C = D
| ~ product(A,B,D)
| ~ product(A,B,C) ),
inference(clausify,[status(thm)],[multiplication_is_well_defined]) ).
fof(y_times_z,axiom,
product(y,z,y_times_z),
file('theBenchmark.p',y_times_z) ).
cnf(c_23,plain,
product(y,z,y_times_z),
inference(clausify,[status(thm)],[y_times_z]) ).
fof(x_times__y_times_z,axiom,
product(x,y_times_z,x_times__y_times_z),
file('theBenchmark.p',x_times__y_times_z) ).
cnf(c_24,plain,
product(x,y_times_z,x_times__y_times_z),
inference(clausify,[status(thm)],[x_times__y_times_z]) ).
fof(x_times_y,axiom,
product(x,y,x_times_y),
file('theBenchmark.p',x_times_y) ).
cnf(c_25,plain,
product(x,y,x_times_y),
inference(clausify,[status(thm)],[x_times_y]) ).
fof(x_times_y__times_z,axiom,
product(x_times_y,z,x_times_y__times_z),
file('theBenchmark.p',x_times_y__times_z) ).
cnf(c_26,plain,
product(x_times_y,z,x_times_y__times_z),
inference(clausify,[status(thm)],[x_times_y__times_z]) ).
fof(prove_equality,axiom,
x_times__y_times_z != x_times_y__times_z,
file('theBenchmark.p',prove_equality) ).
cnf(c_27,plain,
x_times__y_times_z != x_times_y__times_z,
inference(clausify,[status(thm)],[prove_equality]) ).
cnf(c_28,plain,
x_times_y__times_z != x_times__y_times_z,
inference(copy,[status(thm)],[c_27]) ).
cnf(c_35,plain,
( sum(C,E,C)
| ~ sum(A,D,A)
| ~ product(D,B,E)
| ~ product(A,B,C) ),
inference(factor,[status(thm)],[c_11]) ).
cnf(c_37,plain,
( product(D,B,E)
| ~ sum(C,C,E)
| ~ sum(A,A,D)
| ~ product(A,B,C) ),
inference(factor,[status(thm)],[c_12]) ).
cnf(c_57,plain,
sum(A,B,add(B,A)),
inference(resolve,[status(thm)],[c_3,c_1]) ).
cnf(c_58,plain,
product(A,B,multiply(B,A)),
inference(resolve,[status(thm)],[c_4,c_2]) ).
cnf(c_8866,plain,
( sum(A,C,E)
| ~ product(A,D,E)
| ~ sum(multiplicative_identity,B,D)
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_9,c_8]) ).
cnf(c_8867,plain,
( sum(B,B,C)
| ~ product(B,A,C)
| ~ sum(multiplicative_identity,multiplicative_identity,A) ),
inference(resolve,[status(thm)],[c_8866,c_8]) ).
cnf(c_8868,plain,
( sum(A,A,B)
| ~ product(A,add(multiplicative_identity,multiplicative_identity),B) ),
inference(resolve,[status(thm)],[c_8867,c_1]) ).
cnf(c_59,plain,
sum(A,A,multiply(A,add(multiplicative_identity,multiplicative_identity))),
inference(resolve,[status(thm)],[c_8868,c_2]) ).
cnf(c_8869,plain,
( sum(A,C,E)
| ~ product(A,D,E)
| ~ sum(multiplicative_identity,B,D)
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_9,c_8]) ).
cnf(c_8870,plain,
( sum(C,multiply(C,A),D)
| ~ product(C,B,D)
| ~ sum(multiplicative_identity,A,B) ),
inference(resolve,[status(thm)],[c_8869,c_2]) ).
cnf(c_8871,plain,
( sum(A,multiply(A,B),C)
| ~ product(A,add(multiplicative_identity,B),C) ),
inference(resolve,[status(thm)],[c_8870,c_1]) ).
cnf(c_65,plain,
sum(A,multiply(A,B),multiply(A,add(multiplicative_identity,B))),
inference(resolve,[status(thm)],[c_8871,c_2]) ).
cnf(c_8872,plain,
( product(A,C,E)
| ~ sum(A,D,E)
| ~ product(additive_identity,B,D)
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_13,c_6]) ).
cnf(c_8873,plain,
( product(C,add(C,A),D)
| ~ sum(C,B,D)
| ~ product(additive_identity,A,B) ),
inference(resolve,[status(thm)],[c_8872,c_1]) ).
cnf(c_8874,plain,
( product(A,add(A,multiplicative_identity),B)
| ~ sum(A,additive_identity,B) ),
inference(resolve,[status(thm)],[c_8873,c_8]) ).
cnf(c_177,plain,
product(A,add(A,multiplicative_identity),A),
inference(resolve,[status(thm)],[c_8874,c_6]) ).
cnf(c_8875,plain,
( product(A,C,E)
| ~ sum(A,D,E)
| ~ product(additive_identity,B,D)
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_13,c_6]) ).
cnf(c_8876,plain,
( product(C,add(C,A),D)
| ~ sum(C,B,D)
| ~ product(additive_identity,A,B) ),
inference(resolve,[status(thm)],[c_8875,c_1]) ).
cnf(c_8877,plain,
( product(A,add(A,B),C)
| ~ sum(A,multiply(additive_identity,B),C) ),
inference(resolve,[status(thm)],[c_8876,c_2]) ).
cnf(c_180,plain,
product(A,add(A,B),add(A,multiply(additive_identity,B))),
inference(resolve,[status(thm)],[c_8877,c_1]) ).
cnf(c_8878,plain,
( product(multiplicative_identity,C,E)
| ~ sum(D,B,E)
| ~ product(inverse(B),A,D)
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_15,c_17]) ).
cnf(c_8879,plain,
( product(multiplicative_identity,add(B,A),D)
| ~ sum(C,A,D)
| ~ product(inverse(A),B,C) ),
inference(resolve,[status(thm)],[c_8878,c_1]) ).
cnf(c_8880,plain,
( product(multiplicative_identity,add(multiplicative_identity,A),B)
| ~ sum(inverse(A),A,B) ),
inference(resolve,[status(thm)],[c_8879,c_8]) ).
cnf(c_279,plain,
product(multiplicative_identity,add(multiplicative_identity,A),multiplicative_identity),
inference(resolve,[status(thm)],[c_8880,c_17]) ).
cnf(c_8881,plain,
( A = B
| ~ sum(additive_identity,A,B) ),
inference(resolve,[status(thm)],[c_21,c_5]) ).
cnf(c_8882,plain,
A = add(additive_identity,A),
inference(resolve,[status(thm)],[c_8881,c_1]) ).
cnf(c_870,plain,
add(additive_identity,A) = A,
inference(copy,[status(thm)],[c_8882]) ).
cnf(c_8883,plain,
( A = B
| ~ product(A,multiplicative_identity,B) ),
inference(resolve,[status(thm)],[c_22,c_8]) ).
cnf(c_8884,plain,
A = multiply(A,multiplicative_identity),
inference(resolve,[status(thm)],[c_8883,c_2]) ).
cnf(c_874,plain,
multiply(A,multiplicative_identity) = A,
inference(copy,[status(thm)],[c_8884]) ).
cnf(c_8885,plain,
( A = B
| ~ product(multiplicative_identity,A,B) ),
inference(resolve,[status(thm)],[c_22,c_7]) ).
cnf(c_8886,plain,
A = multiply(multiplicative_identity,A),
inference(resolve,[status(thm)],[c_8885,c_2]) ).
cnf(c_875,plain,
multiply(multiplicative_identity,A) = A,
inference(copy,[status(thm)],[c_8886]) ).
cnf(c_8887,plain,
( multiply(A,B) = C
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_22,c_2]) ).
cnf(c_876,plain,
multiply(y,z) = y_times_z,
inference(resolve,[status(thm)],[c_8887,c_23]) ).
cnf(c_935,plain,
product(z,y,y_times_z),
inference(resolve,[status(thm)],[c_4,c_23]) ).
cnf(c_8888,plain,
( multiply(A,B) = C
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_22,c_2]) ).
cnf(c_936,plain,
multiply(x,y_times_z) = x_times__y_times_z,
inference(resolve,[status(thm)],[c_8888,c_24]) ).
cnf(c_995,plain,
product(y_times_z,x,x_times__y_times_z),
inference(resolve,[status(thm)],[c_4,c_24]) ).
cnf(c_1059,plain,
product(y,x,x_times_y),
inference(resolve,[status(thm)],[c_4,c_25]) ).
cnf(c_8889,plain,
( multiply(A,B) = C
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_22,c_2]) ).
cnf(c_1060,plain,
multiply(x_times_y,z) = x_times_y__times_z,
inference(resolve,[status(thm)],[c_8889,c_26]) ).
cnf(c_1123,plain,
product(z,x_times_y,x_times_y__times_z),
inference(resolve,[status(thm)],[c_4,c_26]) ).
cnf(c_8890,plain,
( x_times_y__times_z = A
| ~ product(x_times_y,z,A) ),
inference(resolve,[status(thm)],[c_22,c_26]) ).
cnf(c_1127,plain,
~ product(x_times_y,z,x_times__y_times_z),
inference(resolve,[status(thm)],[c_8890,c_28]) ).
cnf(c_8891,plain,
( add(A,B) = C
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_21,c_1]) ).
cnf(c_1148,plain,
add(A,B) = add(B,A),
inference(resolve,[status(thm)],[c_8891,c_57]) ).
cnf(c_8892,plain,
( sum(x_times_y__times_z,B,D)
| ~ product(z,C,D)
| ~ sum(x_times_y,A,C)
| ~ product(z,A,B) ),
inference(resolve,[status(thm)],[c_9,c_1123]) ).
cnf(c_8893,plain,
( sum(x_times_y__times_z,y_times_z,B)
| ~ product(z,A,B)
| ~ sum(x_times_y,y,A) ),
inference(resolve,[status(thm)],[c_8892,c_935]) ).
cnf(c_8894,plain,
( sum(x_times_y__times_z,y_times_z,A)
| ~ product(z,add(y,x_times_y),A) ),
inference(resolve,[status(thm)],[c_8893,c_57]) ).
cnf(c_8895,plain,
sum(x_times_y__times_z,y_times_z,multiply(z,add(y,x_times_y))),
inference(resolve,[status(thm)],[c_8894,c_2]) ).
cnf(c_1648,plain,
sum(x_times_y__times_z,y_times_z,multiply(z,add(x_times_y,y))),
inference(paramod,[status(thm)],[c_1148,c_8895]) ).
cnf(c_8896,plain,
( multiply(A,B) = C
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_22,c_2]) ).
cnf(c_1692,plain,
multiply(A,B) = multiply(B,A),
inference(resolve,[status(thm)],[c_8896,c_58]) ).
cnf(c_8897,plain,
( add(B,A) = C
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_21,c_57]) ).
cnf(c_8898,plain,
add(multiply(A,B),A) = multiply(A,add(multiplicative_identity,B)),
inference(resolve,[status(thm)],[c_8897,c_65]) ).
cnf(c_8899,plain,
add(A,multiply(A,B)) = multiply(A,add(multiplicative_identity,B)),
inference(paramod,[status(thm)],[c_1148,c_8898]) ).
cnf(c_2854,plain,
multiply(A,add(multiplicative_identity,B)) = add(A,multiply(A,B)),
inference(copy,[status(thm)],[c_8899]) ).
cnf(c_8900,plain,
( multiply(B,A) = C
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_22,c_58]) ).
cnf(c_8901,plain,
multiply(add(A,multiplicative_identity),A) = A,
inference(resolve,[status(thm)],[c_8900,c_177]) ).
cnf(c_3160,plain,
multiply(A,add(A,multiplicative_identity)) = A,
inference(paramod,[status(thm)],[c_1692,c_8901]) ).
cnf(c_8902,plain,
( A = B
| ~ product(multiplicative_identity,A,B) ),
inference(resolve,[status(thm)],[c_22,c_7]) ).
cnf(c_3161,plain,
add(multiplicative_identity,multiplicative_identity) = multiplicative_identity,
inference(resolve,[status(thm)],[c_8902,c_177]) ).
cnf(c_8903,plain,
( sum(multiply(B,D),C,F)
| ~ product(E,B,F)
| ~ sum(D,A,E)
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_11,c_58]) ).
cnf(c_8904,plain,
( sum(multiply(D,A),multiply(D,B),E)
| ~ product(C,D,E)
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_8903,c_58]) ).
cnf(c_8905,plain,
( sum(multiply(B,A),multiply(B,A),C)
| ~ product(multiply(A,add(multiplicative_identity,multiplicative_identity)),B,C) ),
inference(resolve,[status(thm)],[c_8904,c_59]) ).
cnf(c_8906,plain,
sum(multiply(add(multiply(A,add(multiplicative_identity,multiplicative_identity)),multiplicative_identity),A),multiply(add(multiply(A,add(multiplicative_identity,multiplicative_identity)),multiplicative_identity),A),multiply(A,add(multiplicative_identity,multiplicative_identity))),
inference(resolve,[status(thm)],[c_8905,c_177]) ).
cnf(c_8907,plain,
sum(multiply(add(multiply(A,multiplicative_identity),multiplicative_identity),A),multiply(add(multiply(A,add(multiplicative_identity,multiplicative_identity)),multiplicative_identity),A),multiply(A,add(multiplicative_identity,multiplicative_identity))),
inference(paramod,[status(thm)],[c_3161,c_8906]) ).
cnf(c_8908,plain,
sum(multiply(add(A,multiplicative_identity),A),multiply(add(multiply(A,add(multiplicative_identity,multiplicative_identity)),multiplicative_identity),A),multiply(A,add(multiplicative_identity,multiplicative_identity))),
inference(paramod,[status(thm)],[c_874,c_8907]) ).
cnf(c_8909,plain,
sum(multiply(A,add(A,multiplicative_identity)),multiply(add(multiply(A,add(multiplicative_identity,multiplicative_identity)),multiplicative_identity),A),multiply(A,add(multiplicative_identity,multiplicative_identity))),
inference(paramod,[status(thm)],[c_1692,c_8908]) ).
cnf(c_8910,plain,
sum(A,multiply(add(multiply(A,add(multiplicative_identity,multiplicative_identity)),multiplicative_identity),A),multiply(A,add(multiplicative_identity,multiplicative_identity))),
inference(paramod,[status(thm)],[c_3160,c_8909]) ).
cnf(c_8911,plain,
sum(A,multiply(add(multiply(A,multiplicative_identity),multiplicative_identity),A),multiply(A,add(multiplicative_identity,multiplicative_identity))),
inference(paramod,[status(thm)],[c_3161,c_8910]) ).
cnf(c_8912,plain,
sum(A,multiply(add(A,multiplicative_identity),A),multiply(A,add(multiplicative_identity,multiplicative_identity))),
inference(paramod,[status(thm)],[c_874,c_8911]) ).
cnf(c_8913,plain,
sum(A,multiply(A,add(A,multiplicative_identity)),multiply(A,add(multiplicative_identity,multiplicative_identity))),
inference(paramod,[status(thm)],[c_1692,c_8912]) ).
cnf(c_8914,plain,
sum(A,A,multiply(A,add(multiplicative_identity,multiplicative_identity))),
inference(paramod,[status(thm)],[c_3160,c_8913]) ).
cnf(c_8915,plain,
sum(A,A,multiply(A,multiplicative_identity)),
inference(paramod,[status(thm)],[c_3161,c_8914]) ).
cnf(c_3224,plain,
sum(A,A,A),
inference(paramod,[status(thm)],[c_874,c_8915]) ).
cnf(c_8916,plain,
( sum(A,C,E)
| ~ product(A,D,E)
| ~ sum(add(A,multiplicative_identity),B,D)
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_9,c_177]) ).
cnf(c_8917,plain,
( sum(y,x_times_y,B)
| ~ product(y,A,B)
| ~ sum(add(y,multiplicative_identity),x,A) ),
inference(resolve,[status(thm)],[c_8916,c_1059]) ).
cnf(c_8918,plain,
( sum(y,x_times_y,A)
| ~ product(y,add(x,add(y,multiplicative_identity)),A) ),
inference(resolve,[status(thm)],[c_8917,c_57]) ).
cnf(c_8919,plain,
sum(y,x_times_y,multiply(add(x,add(y,multiplicative_identity)),y)),
inference(resolve,[status(thm)],[c_8918,c_58]) ).
cnf(c_8920,plain,
sum(y,x_times_y,multiply(add(x,add(multiplicative_identity,y)),y)),
inference(paramod,[status(thm)],[c_1148,c_8919]) ).
cnf(c_3306,plain,
sum(y,x_times_y,multiply(y,add(x,add(multiplicative_identity,y)))),
inference(paramod,[status(thm)],[c_1692,c_8920]) ).
cnf(c_8921,plain,
( sum(A,C,E)
| ~ product(A,D,E)
| ~ sum(add(A,multiplicative_identity),B,D)
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_9,c_177]) ).
cnf(c_8922,plain,
( sum(z,y_times_z,B)
| ~ product(z,A,B)
| ~ sum(add(z,multiplicative_identity),y,A) ),
inference(resolve,[status(thm)],[c_8921,c_935]) ).
cnf(c_8923,plain,
( sum(z,y_times_z,A)
| ~ product(z,add(y,add(z,multiplicative_identity)),A) ),
inference(resolve,[status(thm)],[c_8922,c_57]) ).
cnf(c_8924,plain,
sum(z,y_times_z,multiply(add(y,add(z,multiplicative_identity)),z)),
inference(resolve,[status(thm)],[c_8923,c_58]) ).
cnf(c_8925,plain,
sum(z,y_times_z,multiply(add(y,add(multiplicative_identity,z)),z)),
inference(paramod,[status(thm)],[c_1148,c_8924]) ).
cnf(c_3308,plain,
sum(z,y_times_z,multiply(z,add(y,add(multiplicative_identity,z)))),
inference(paramod,[status(thm)],[c_1692,c_8925]) ).
cnf(c_8926,plain,
( sum(A,C,E)
| ~ product(A,D,E)
| ~ sum(add(A,multiplicative_identity),B,D)
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_9,c_177]) ).
cnf(c_8927,plain,
( sum(x,x_times_y,B)
| ~ product(x,A,B)
| ~ sum(add(x,multiplicative_identity),y,A) ),
inference(resolve,[status(thm)],[c_8926,c_25]) ).
cnf(c_8928,plain,
( sum(x,x_times_y,A)
| ~ product(x,add(y,add(x,multiplicative_identity)),A) ),
inference(resolve,[status(thm)],[c_8927,c_57]) ).
cnf(c_8929,plain,
sum(x,x_times_y,multiply(add(y,add(x,multiplicative_identity)),x)),
inference(resolve,[status(thm)],[c_8928,c_58]) ).
cnf(c_8930,plain,
sum(x,x_times_y,multiply(add(y,add(multiplicative_identity,x)),x)),
inference(paramod,[status(thm)],[c_1148,c_8929]) ).
cnf(c_3314,plain,
sum(x,x_times_y,multiply(x,add(y,add(multiplicative_identity,x)))),
inference(paramod,[status(thm)],[c_1692,c_8930]) ).
cnf(c_8931,plain,
( sum(A,C,E)
| ~ product(A,D,E)
| ~ sum(add(A,multiplicative_identity),B,D)
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_9,c_177]) ).
cnf(c_8932,plain,
( sum(y,y_times_z,B)
| ~ product(y,A,B)
| ~ sum(add(y,multiplicative_identity),z,A) ),
inference(resolve,[status(thm)],[c_8931,c_23]) ).
cnf(c_8933,plain,
( sum(y,y_times_z,A)
| ~ product(y,add(z,add(y,multiplicative_identity)),A) ),
inference(resolve,[status(thm)],[c_8932,c_57]) ).
cnf(c_8934,plain,
sum(y,y_times_z,multiply(add(z,add(y,multiplicative_identity)),y)),
inference(resolve,[status(thm)],[c_8933,c_58]) ).
cnf(c_8935,plain,
sum(y,y_times_z,multiply(add(z,add(multiplicative_identity,y)),y)),
inference(paramod,[status(thm)],[c_1148,c_8934]) ).
cnf(c_3316,plain,
sum(y,y_times_z,multiply(y,add(z,add(multiplicative_identity,y)))),
inference(paramod,[status(thm)],[c_1692,c_8935]) ).
cnf(c_8936,plain,
( multiply(B,A) = C
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_22,c_58]) ).
cnf(c_8937,plain,
multiply(add(multiplicative_identity,A),multiplicative_identity) = multiplicative_identity,
inference(resolve,[status(thm)],[c_8936,c_279]) ).
cnf(c_8938,plain,
multiply(multiplicative_identity,add(multiplicative_identity,A)) = multiplicative_identity,
inference(paramod,[status(thm)],[c_1692,c_8937]) ).
cnf(c_8939,plain,
add(multiplicative_identity,multiply(multiplicative_identity,A)) = multiplicative_identity,
inference(paramod,[status(thm)],[c_2854,c_8938]) ).
cnf(c_3991,plain,
add(multiplicative_identity,A) = multiplicative_identity,
inference(paramod,[status(thm)],[c_875,c_8939]) ).
cnf(c_8940,plain,
sum(y,y_times_z,multiply(y,add(z,multiplicative_identity))),
inference(paramod,[status(thm)],[c_3991,c_3316]) ).
cnf(c_8941,plain,
sum(y,y_times_z,multiply(y,add(multiplicative_identity,z))),
inference(paramod,[status(thm)],[c_1148,c_8940]) ).
cnf(c_8942,plain,
sum(y,y_times_z,multiply(y,multiplicative_identity)),
inference(paramod,[status(thm)],[c_3991,c_8941]) ).
cnf(c_8943,plain,
sum(y,y_times_z,multiply(multiplicative_identity,y)),
inference(paramod,[status(thm)],[c_1692,c_8942]) ).
cnf(c_4045,plain,
sum(y,y_times_z,y),
inference(paramod,[status(thm)],[c_875,c_8943]) ).
cnf(c_8944,plain,
sum(x,x_times_y,multiply(x,add(y,multiplicative_identity))),
inference(paramod,[status(thm)],[c_3991,c_3314]) ).
cnf(c_8945,plain,
sum(x,x_times_y,multiply(x,add(multiplicative_identity,y))),
inference(paramod,[status(thm)],[c_1148,c_8944]) ).
cnf(c_8946,plain,
sum(x,x_times_y,multiply(x,multiplicative_identity)),
inference(paramod,[status(thm)],[c_3991,c_8945]) ).
cnf(c_8947,plain,
sum(x,x_times_y,multiply(multiplicative_identity,x)),
inference(paramod,[status(thm)],[c_1692,c_8946]) ).
cnf(c_4047,plain,
sum(x,x_times_y,x),
inference(paramod,[status(thm)],[c_875,c_8947]) ).
cnf(c_8948,plain,
sum(z,y_times_z,multiply(z,add(y,multiplicative_identity))),
inference(paramod,[status(thm)],[c_3991,c_3308]) ).
cnf(c_8949,plain,
sum(z,y_times_z,multiply(z,add(multiplicative_identity,y))),
inference(paramod,[status(thm)],[c_1148,c_8948]) ).
cnf(c_8950,plain,
sum(z,y_times_z,multiply(z,multiplicative_identity)),
inference(paramod,[status(thm)],[c_3991,c_8949]) ).
cnf(c_8951,plain,
sum(z,y_times_z,multiply(multiplicative_identity,z)),
inference(paramod,[status(thm)],[c_1692,c_8950]) ).
cnf(c_4049,plain,
sum(z,y_times_z,z),
inference(paramod,[status(thm)],[c_875,c_8951]) ).
cnf(c_8952,plain,
sum(y,x_times_y,multiply(y,add(x,multiplicative_identity))),
inference(paramod,[status(thm)],[c_3991,c_3306]) ).
cnf(c_8953,plain,
sum(y,x_times_y,multiply(y,add(multiplicative_identity,x))),
inference(paramod,[status(thm)],[c_1148,c_8952]) ).
cnf(c_8954,plain,
sum(y,x_times_y,multiply(y,multiplicative_identity)),
inference(paramod,[status(thm)],[c_3991,c_8953]) ).
cnf(c_8955,plain,
sum(y,x_times_y,multiply(multiplicative_identity,y)),
inference(paramod,[status(thm)],[c_1692,c_8954]) ).
cnf(c_4051,plain,
sum(y,x_times_y,y),
inference(paramod,[status(thm)],[c_875,c_8955]) ).
cnf(c_8956,plain,
multiply(A,multiplicative_identity) = add(A,multiply(A,B)),
inference(paramod,[status(thm)],[c_3991,c_2854]) ).
cnf(c_8957,plain,
A = add(A,multiply(A,B)),
inference(paramod,[status(thm)],[c_874,c_8956]) ).
cnf(c_4204,plain,
add(A,multiply(A,B)) = A,
inference(copy,[status(thm)],[c_8957]) ).
cnf(c_8958,plain,
( sum(x_times_y,B,x_times_y)
| ~ sum(y,A,y)
| ~ product(A,x,B) ),
inference(resolve,[status(thm)],[c_35,c_1059]) ).
cnf(c_8959,plain,
( sum(x_times_y,x_times__y_times_z,x_times_y)
| ~ sum(y,y_times_z,y) ),
inference(resolve,[status(thm)],[c_8958,c_995]) ).
cnf(c_4289,plain,
sum(x_times_y,x_times__y_times_z,x_times_y),
inference(resolve,[status(thm)],[c_8959,c_4045]) ).
cnf(c_8960,plain,
( add(B,A) = C
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_21,c_57]) ).
cnf(c_4932,plain,
add(x_times_y,y) = y,
inference(resolve,[status(thm)],[c_8960,c_4051]) ).
cnf(c_8961,plain,
sum(x_times_y__times_z,y_times_z,multiply(z,y)),
inference(paramod,[status(thm)],[c_4932,c_1648]) ).
cnf(c_8962,plain,
sum(x_times_y__times_z,y_times_z,multiply(y,z)),
inference(paramod,[status(thm)],[c_1692,c_8961]) ).
cnf(c_5005,plain,
sum(x_times_y__times_z,y_times_z,y_times_z),
inference(paramod,[status(thm)],[c_876,c_8962]) ).
cnf(c_8963,plain,
( sum(A,E,F)
| ~ product(add(D,A),C,F)
| ~ product(D,B,E)
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_14,c_57]) ).
cnf(c_8964,plain,
( sum(x_times_y__times_z,B,C)
| ~ product(add(A,x_times_y__times_z),y_times_z,C)
| ~ product(A,y_times_z,B) ),
inference(resolve,[status(thm)],[c_8963,c_5005]) ).
cnf(c_8965,plain,
( sum(x_times_y__times_z,x_times__y_times_z,A)
| ~ product(add(x,x_times_y__times_z),y_times_z,A) ),
inference(resolve,[status(thm)],[c_8964,c_24]) ).
cnf(c_6196,plain,
sum(x_times_y__times_z,x_times__y_times_z,multiply(y_times_z,add(x,x_times_y__times_z))),
inference(resolve,[status(thm)],[c_8965,c_58]) ).
cnf(c_8966,plain,
( product(B,add(A,C),D)
| ~ sum(add(A,multiply(additive_identity,C)),add(A,multiply(additive_identity,C)),D)
| ~ sum(A,A,B) ),
inference(resolve,[status(thm)],[c_37,c_180]) ).
cnf(c_8967,plain,
( product(additive_identity,add(additive_identity,A),B)
| ~ sum(add(additive_identity,multiply(additive_identity,A)),add(additive_identity,multiply(additive_identity,A)),B) ),
inference(resolve,[status(thm)],[c_8966,c_6]) ).
cnf(c_8968,plain,
product(additive_identity,add(additive_identity,A),add(additive_identity,multiply(additive_identity,A))),
inference(resolve,[status(thm)],[c_8967,c_3224]) ).
cnf(c_8969,plain,
product(additive_identity,A,add(additive_identity,multiply(additive_identity,A))),
inference(paramod,[status(thm)],[c_870,c_8968]) ).
cnf(c_6752,plain,
product(additive_identity,A,additive_identity),
inference(paramod,[status(thm)],[c_4204,c_8969]) ).
cnf(c_8970,plain,
( sum(z,C,D)
| ~ product(z,B,D)
| ~ product(y_times_z,A,C)
| ~ sum(z,A,B) ),
inference(resolve,[status(thm)],[c_14,c_4049]) ).
cnf(c_8971,plain,
( sum(z,B,C)
| ~ product(z,add(z,A),C)
| ~ product(y_times_z,A,B) ),
inference(resolve,[status(thm)],[c_8970,c_1]) ).
cnf(c_8972,plain,
( sum(z,x_times__y_times_z,A)
| ~ product(z,add(z,x),A) ),
inference(resolve,[status(thm)],[c_8971,c_995]) ).
cnf(c_7039,plain,
sum(z,x_times__y_times_z,add(z,multiply(additive_identity,x))),
inference(resolve,[status(thm)],[c_8972,c_180]) ).
cnf(c_8973,plain,
( sum(x,C,D)
| ~ product(x,B,D)
| ~ product(x_times_y,A,C)
| ~ sum(x,A,B) ),
inference(resolve,[status(thm)],[c_14,c_4047]) ).
cnf(c_8974,plain,
( sum(x,B,C)
| ~ product(x,add(x,A),C)
| ~ product(x_times_y,A,B) ),
inference(resolve,[status(thm)],[c_8973,c_1]) ).
cnf(c_8975,plain,
( sum(x,x_times_y__times_z,A)
| ~ product(x,add(x,z),A) ),
inference(resolve,[status(thm)],[c_8974,c_26]) ).
cnf(c_7051,plain,
sum(x,x_times_y__times_z,add(x,multiply(additive_identity,z))),
inference(resolve,[status(thm)],[c_8975,c_180]) ).
cnf(c_8976,plain,
( multiply(A,B) = C
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_22,c_2]) ).
cnf(c_7338,plain,
multiply(additive_identity,A) = additive_identity,
inference(resolve,[status(thm)],[c_8976,c_6752]) ).
cnf(c_8977,plain,
sum(x,x_times_y__times_z,add(x,additive_identity)),
inference(paramod,[status(thm)],[c_7338,c_7051]) ).
cnf(c_8978,plain,
sum(x,x_times_y__times_z,add(additive_identity,x)),
inference(paramod,[status(thm)],[c_1148,c_8977]) ).
cnf(c_7525,plain,
sum(x,x_times_y__times_z,x),
inference(paramod,[status(thm)],[c_870,c_8978]) ).
cnf(c_8979,plain,
sum(z,x_times__y_times_z,add(z,additive_identity)),
inference(paramod,[status(thm)],[c_7338,c_7039]) ).
cnf(c_8980,plain,
sum(z,x_times__y_times_z,add(additive_identity,z)),
inference(paramod,[status(thm)],[c_1148,c_8979]) ).
cnf(c_7531,plain,
sum(z,x_times__y_times_z,z),
inference(paramod,[status(thm)],[c_870,c_8980]) ).
cnf(c_8981,plain,
( add(B,A) = C
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_21,c_57]) ).
cnf(c_8982,plain,
add(x_times_y__times_z,x) = x,
inference(resolve,[status(thm)],[c_8981,c_7525]) ).
cnf(c_8650,plain,
add(x,x_times_y__times_z) = x,
inference(paramod,[status(thm)],[c_1148,c_8982]) ).
cnf(c_8983,plain,
sum(x_times_y__times_z,x_times__y_times_z,multiply(y_times_z,x)),
inference(paramod,[status(thm)],[c_8650,c_6196]) ).
cnf(c_8984,plain,
sum(x_times_y__times_z,x_times__y_times_z,multiply(x,y_times_z)),
inference(paramod,[status(thm)],[c_1692,c_8983]) ).
cnf(c_8763,plain,
sum(x_times_y__times_z,x_times__y_times_z,x_times__y_times_z),
inference(paramod,[status(thm)],[c_936,c_8984]) ).
cnf(c_8985,plain,
( product(x_times_y,B,D)
| ~ sum(C,x_times__y_times_z,D)
| ~ product(x_times_y,A,C)
| ~ sum(A,x_times__y_times_z,B) ),
inference(resolve,[status(thm)],[c_15,c_4289]) ).
cnf(c_8986,plain,
( product(x_times_y,z,B)
| ~ sum(A,x_times__y_times_z,B)
| ~ product(x_times_y,z,A) ),
inference(resolve,[status(thm)],[c_8985,c_7531]) ).
cnf(c_8987,plain,
( product(x_times_y,z,A)
| ~ sum(multiply(z,x_times_y),x_times__y_times_z,A) ),
inference(resolve,[status(thm)],[c_8986,c_58]) ).
cnf(c_8988,plain,
~ sum(multiply(z,x_times_y),x_times__y_times_z,x_times__y_times_z),
inference(resolve,[status(thm)],[c_8987,c_1127]) ).
cnf(c_8989,plain,
~ sum(multiply(x_times_y,z),x_times__y_times_z,x_times__y_times_z),
inference(paramod,[status(thm)],[c_1692,c_8988]) ).
cnf(c_8990,plain,
~ sum(x_times_y__times_z,x_times__y_times_z,x_times__y_times_z),
inference(paramod,[status(thm)],[c_1060,c_8989]) ).
cnf(c_8865,plain,
$false,
inference(resolve,[status(thm)],[c_8763,c_8990]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : BOO007-1 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n011.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sat Sep 26 22:33:59 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.36 % Process 1711998 was started by sandbox on n011,
% 0.10/0.36 % Sat Sep 26 22:33:59 2026
% 0.10/0.36 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.10/0.36
% 0.10/0.36 % From the command line: assign(max_seconds, 300).
% 41.06/6.31
% 41.06/6.31 % Assigning unary symbol inverse kb_weight 0 and highest precedence (15).
% 41.06/6.31
% 41.06/6.31 % SZS status Unsatisfiable for theBenchmark
% 41.06/6.31
% 41.06/6.31 % Proof 1 at 4.70 (+ 1.18) seconds.
% 41.06/6.31 % Length of proof is 73.
% 41.06/6.31 % Level of proof is 11.
% 41.06/6.31 % Maximum clause weight is 32.000.
% 41.06/6.31 % Given clauses 217.
% 41.06/6.31
% 41.06/6.31 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------