%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : BOO008-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n009.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 120.67s 15.77s
% Output : CNFRefutation 120.67s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 23
% Syntax : Number of formulae : 246 ( 138 unt; 0 def)
% Number of atoms : 472 ( 49 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 458 ( 232 ~; 226 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 3 avg)
% Maximal term depth : 4 ( 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 : 493 ( 12 sgn 72 !; 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(distributivity2,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( product(VAR_0,VAR_5,VAR_6)
| ~ sum(VAR_2,VAR_4,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',distributivity2) ).
cnf(c_10,plain,
( product(A,F,V6)
| ~ sum(C,E,V6)
| ~ sum(B,D,F)
| ~ product(A,D,E)
| ~ product(A,B,C) ),
inference(clausify,[status(thm)],[distributivity2]) ).
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(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(distributivity8,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6] :
( sum(VAR_5,VAR_1,VAR_6)
| ~ product(VAR_2,VAR_4,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',distributivity8) ).
cnf(c_16,plain,
( sum(F,B,V6)
| ~ product(C,E,V6)
| ~ product(A,D,F)
| ~ sum(D,B,E)
| ~ sum(A,B,C) ),
inference(clausify,[status(thm)],[distributivity8]) ).
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_plus_z,axiom,
sum(y,z,y_plus_z),
file('theBenchmark.p',y_plus_z) ).
cnf(c_23,plain,
sum(y,z,y_plus_z),
inference(clausify,[status(thm)],[y_plus_z]) ).
fof(x_plus__y_plus_z,axiom,
sum(x,y_plus_z,x__plus_y_plus_z),
file('theBenchmark.p',x_plus__y_plus_z) ).
cnf(c_24,plain,
sum(x,y_plus_z,x__plus_y_plus_z),
inference(clausify,[status(thm)],[x_plus__y_plus_z]) ).
fof(x_plus_y,axiom,
sum(x,y,x_plus_y),
file('theBenchmark.p',x_plus_y) ).
cnf(c_25,plain,
sum(x,y,x_plus_y),
inference(clausify,[status(thm)],[x_plus_y]) ).
fof(x_plus_y__plus_z,axiom,
sum(x_plus_y,z,x_plus_y__plus_z),
file('theBenchmark.p',x_plus_y__plus_z) ).
cnf(c_26,plain,
sum(x_plus_y,z,x_plus_y__plus_z),
inference(clausify,[status(thm)],[x_plus_y__plus_z]) ).
fof(prove_equality,axiom,
x__plus_y_plus_z != x_plus_y__plus_z,
file('theBenchmark.p',prove_equality) ).
cnf(c_27,plain,
x__plus_y_plus_z != x_plus_y__plus_z,
inference(clausify,[status(thm)],[prove_equality]) ).
cnf(c_28,plain,
x_plus_y__plus_z != x__plus_y_plus_z,
inference(copy,[status(thm)],[c_27]) ).
cnf(c_29,plain,
sum(A,B,add(B,A)),
inference(resolve,[status(thm)],[c_3,c_1]) ).
cnf(c_30,plain,
product(A,B,multiply(B,A)),
inference(resolve,[status(thm)],[c_4,c_2]) ).
cnf(c_12957,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_12958,plain,
( sum(C,multiply(C,A),D)
| ~ product(C,B,D)
| ~ sum(multiplicative_identity,A,B) ),
inference(resolve,[status(thm)],[c_12957,c_2]) ).
cnf(c_12959,plain,
( sum(A,multiply(A,additive_identity),B)
| ~ product(A,multiplicative_identity,B) ),
inference(resolve,[status(thm)],[c_12958,c_6]) ).
cnf(c_34,plain,
sum(A,multiply(A,additive_identity),A),
inference(resolve,[status(thm)],[c_12959,c_8]) ).
cnf(c_12960,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_12961,plain,
( sum(C,multiply(C,A),D)
| ~ product(C,B,D)
| ~ sum(multiplicative_identity,A,B) ),
inference(resolve,[status(thm)],[c_12960,c_2]) ).
cnf(c_12962,plain,
( sum(A,multiply(A,B),C)
| ~ product(A,add(multiplicative_identity,B),C) ),
inference(resolve,[status(thm)],[c_12961,c_1]) ).
cnf(c_37,plain,
sum(A,multiply(A,B),multiply(A,add(multiplicative_identity,B))),
inference(resolve,[status(thm)],[c_12962,c_2]) ).
cnf(c_12963,plain,
( sum(multiply(A,D),C,F)
| ~ product(A,E,F)
| ~ sum(D,B,E)
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_9,c_2]) ).
cnf(c_12964,plain,
( sum(multiply(C,A),C,D)
| ~ product(C,B,D)
| ~ sum(A,multiplicative_identity,B) ),
inference(resolve,[status(thm)],[c_12963,c_8]) ).
cnf(c_12965,plain,
( sum(multiply(A,B),A,C)
| ~ product(A,add(B,multiplicative_identity),C) ),
inference(resolve,[status(thm)],[c_12964,c_1]) ).
cnf(c_52,plain,
sum(multiply(A,B),A,multiply(A,add(B,multiplicative_identity))),
inference(resolve,[status(thm)],[c_12965,c_2]) ).
cnf(c_12966,plain,
( product(E,B,F)
| ~ sum(multiply(D,B),C,F)
| ~ sum(D,A,E)
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_12,c_2]) ).
cnf(c_12967,plain,
( product(C,D,E)
| ~ sum(multiply(A,D),multiply(B,D),E)
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_12966,c_2]) ).
cnf(c_12968,plain,
( product(A,B,C)
| ~ sum(multiply(A,B),multiply(additive_identity,B),C) ),
inference(resolve,[status(thm)],[c_12967,c_6]) ).
cnf(c_144,plain,
product(A,B,add(multiply(A,B),multiply(additive_identity,B))),
inference(resolve,[status(thm)],[c_12968,c_1]) ).
cnf(c_12969,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_12970,plain,
( product(C,add(C,A),D)
| ~ sum(C,B,D)
| ~ product(additive_identity,A,B) ),
inference(resolve,[status(thm)],[c_12969,c_1]) ).
cnf(c_12971,plain,
( product(A,add(A,multiplicative_identity),B)
| ~ sum(A,additive_identity,B) ),
inference(resolve,[status(thm)],[c_12970,c_8]) ).
cnf(c_149,plain,
product(A,add(A,multiplicative_identity),A),
inference(resolve,[status(thm)],[c_12971,c_6]) ).
cnf(c_12972,plain,
( product(B,C,E)
| ~ sum(D,B,E)
| ~ product(additive_identity,A,D)
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_15,c_5]) ).
cnf(c_12973,plain,
( product(B,B,C)
| ~ sum(A,B,C)
| ~ product(additive_identity,additive_identity,A) ),
inference(resolve,[status(thm)],[c_12972,c_5]) ).
cnf(c_12974,plain,
( product(A,A,B)
| ~ sum(multiply(additive_identity,additive_identity),A,B) ),
inference(resolve,[status(thm)],[c_12973,c_2]) ).
cnf(c_196,plain,
product(A,A,add(multiply(additive_identity,additive_identity),A)),
inference(resolve,[status(thm)],[c_12974,c_1]) ).
cnf(c_12975,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_12976,plain,
( product(multiplicative_identity,add(B,A),D)
| ~ sum(C,A,D)
| ~ product(inverse(A),B,C) ),
inference(resolve,[status(thm)],[c_12975,c_1]) ).
cnf(c_12977,plain,
( product(multiplicative_identity,add(multiplicative_identity,A),B)
| ~ sum(inverse(A),A,B) ),
inference(resolve,[status(thm)],[c_12976,c_8]) ).
cnf(c_251,plain,
product(multiplicative_identity,add(multiplicative_identity,A),multiplicative_identity),
inference(resolve,[status(thm)],[c_12977,c_17]) ).
cnf(c_12978,plain,
( A = B
| ~ sum(additive_identity,A,B) ),
inference(resolve,[status(thm)],[c_21,c_5]) ).
cnf(c_12979,plain,
A = add(additive_identity,A),
inference(resolve,[status(thm)],[c_12978,c_1]) ).
cnf(c_842,plain,
add(additive_identity,A) = A,
inference(copy,[status(thm)],[c_12979]) ).
cnf(c_12980,plain,
( A = B
| ~ product(A,multiplicative_identity,B) ),
inference(resolve,[status(thm)],[c_22,c_8]) ).
cnf(c_12981,plain,
A = multiply(A,multiplicative_identity),
inference(resolve,[status(thm)],[c_12980,c_2]) ).
cnf(c_846,plain,
multiply(A,multiplicative_identity) = A,
inference(copy,[status(thm)],[c_12981]) ).
cnf(c_12982,plain,
( A = B
| ~ product(multiplicative_identity,A,B) ),
inference(resolve,[status(thm)],[c_22,c_7]) ).
cnf(c_12983,plain,
A = multiply(multiplicative_identity,A),
inference(resolve,[status(thm)],[c_12982,c_2]) ).
cnf(c_847,plain,
multiply(multiplicative_identity,A) = A,
inference(copy,[status(thm)],[c_12983]) ).
cnf(c_12984,plain,
( add(A,B) = C
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_21,c_1]) ).
cnf(c_848,plain,
add(y,z) = y_plus_z,
inference(resolve,[status(thm)],[c_12984,c_23]) ).
cnf(c_907,plain,
sum(z,y,y_plus_z),
inference(resolve,[status(thm)],[c_3,c_23]) ).
cnf(c_967,plain,
sum(y_plus_z,x,x__plus_y_plus_z),
inference(resolve,[status(thm)],[c_3,c_24]) ).
cnf(c_1031,plain,
sum(y,x,x_plus_y),
inference(resolve,[status(thm)],[c_3,c_25]) ).
cnf(c_12985,plain,
( add(A,B) = C
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_21,c_1]) ).
cnf(c_1032,plain,
add(x_plus_y,z) = x_plus_y__plus_z,
inference(resolve,[status(thm)],[c_12985,c_26]) ).
cnf(c_1095,plain,
sum(z,x_plus_y,x_plus_y__plus_z),
inference(resolve,[status(thm)],[c_3,c_26]) ).
cnf(c_12986,plain,
( x_plus_y__plus_z = A
| ~ sum(x_plus_y,z,A) ),
inference(resolve,[status(thm)],[c_21,c_26]) ).
cnf(c_1103,plain,
~ sum(x_plus_y,z,x__plus_y_plus_z),
inference(resolve,[status(thm)],[c_12986,c_28]) ).
cnf(c_12987,plain,
( add(A,B) = C
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_21,c_1]) ).
cnf(c_1110,plain,
add(A,B) = add(B,A),
inference(resolve,[status(thm)],[c_12987,c_29]) ).
cnf(c_12988,plain,
( multiply(A,B) = C
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_22,c_2]) ).
cnf(c_1459,plain,
multiply(A,B) = multiply(B,A),
inference(resolve,[status(thm)],[c_12988,c_30]) ).
cnf(c_1800,plain,
~ sum(z,x_plus_y,x__plus_y_plus_z),
inference(resolve,[status(thm)],[c_3,c_1103]) ).
cnf(c_12989,plain,
( A = B
| ~ sum(additive_identity,A,B) ),
inference(resolve,[status(thm)],[c_21,c_5]) ).
cnf(c_1919,plain,
multiply(additive_identity,additive_identity) = additive_identity,
inference(resolve,[status(thm)],[c_12989,c_34]) ).
cnf(c_12990,plain,
product(A,A,add(additive_identity,A)),
inference(paramod,[status(thm)],[c_1919,c_196]) ).
cnf(c_2062,plain,
product(A,A,A),
inference(paramod,[status(thm)],[c_842,c_12990]) ).
cnf(c_12991,plain,
( multiply(B,A) = C
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_22,c_30]) ).
cnf(c_2079,plain,
multiply(A,A) = A,
inference(resolve,[status(thm)],[c_12991,c_2062]) ).
cnf(c_12992,plain,
( product(A,E,F)
| ~ sum(multiply(D,A),C,F)
| ~ sum(D,B,E)
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_10,c_30]) ).
cnf(c_12993,plain,
( product(B,C,D)
| ~ sum(multiply(A,B),B,D)
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_12992,c_2062]) ).
cnf(c_12994,plain,
( product(x,x_plus_y,A)
| ~ sum(multiply(y,x),x,A) ),
inference(resolve,[status(thm)],[c_12993,c_1031]) ).
cnf(c_12995,plain,
product(x,x_plus_y,add(x,multiply(y,x))),
inference(resolve,[status(thm)],[c_12994,c_29]) ).
cnf(c_2148,plain,
product(x,x_plus_y,add(x,multiply(x,y))),
inference(paramod,[status(thm)],[c_1459,c_12995]) ).
cnf(c_12996,plain,
( product(A,E,F)
| ~ sum(multiply(D,A),C,F)
| ~ sum(D,B,E)
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_10,c_30]) ).
cnf(c_12997,plain,
( product(B,C,D)
| ~ sum(multiply(A,B),B,D)
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_12996,c_2062]) ).
cnf(c_12998,plain,
( product(y,y_plus_z,A)
| ~ sum(multiply(z,y),y,A) ),
inference(resolve,[status(thm)],[c_12997,c_907]) ).
cnf(c_12999,plain,
product(y,y_plus_z,add(y,multiply(z,y))),
inference(resolve,[status(thm)],[c_12998,c_29]) ).
cnf(c_2150,plain,
product(y,y_plus_z,add(y,multiply(y,z))),
inference(paramod,[status(thm)],[c_1459,c_12999]) ).
cnf(c_13000,plain,
( add(B,A) = C
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_21,c_29]) ).
cnf(c_13001,plain,
add(multiply(A,B),A) = multiply(A,add(multiplicative_identity,B)),
inference(resolve,[status(thm)],[c_13000,c_37]) ).
cnf(c_13002,plain,
add(A,multiply(A,B)) = multiply(A,add(multiplicative_identity,B)),
inference(paramod,[status(thm)],[c_1110,c_13001]) ).
cnf(c_2169,plain,
multiply(A,add(multiplicative_identity,B)) = add(A,multiply(A,B)),
inference(copy,[status(thm)],[c_13002]) ).
cnf(c_13003,plain,
( add(B,A) = C
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_21,c_29]) ).
cnf(c_13004,plain,
add(A,multiply(A,B)) = multiply(A,add(B,multiplicative_identity)),
inference(resolve,[status(thm)],[c_13003,c_52]) ).
cnf(c_2428,plain,
multiply(A,add(B,multiplicative_identity)) = add(A,multiply(A,B)),
inference(copy,[status(thm)],[c_13004]) ).
cnf(c_13005,plain,
( multiply(B,A) = C
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_22,c_30]) ).
cnf(c_13006,plain,
multiply(add(A,multiplicative_identity),A) = A,
inference(resolve,[status(thm)],[c_13005,c_149]) ).
cnf(c_13007,plain,
multiply(A,add(A,multiplicative_identity)) = A,
inference(paramod,[status(thm)],[c_1459,c_13006]) ).
cnf(c_13008,plain,
add(A,multiply(A,A)) = A,
inference(paramod,[status(thm)],[c_2428,c_13007]) ).
cnf(c_2465,plain,
add(A,A) = A,
inference(paramod,[status(thm)],[c_2079,c_13008]) ).
cnf(c_13009,plain,
( sum(B,C,E)
| ~ product(D,add(B,multiplicative_identity),E)
| ~ sum(B,A,D)
| ~ product(A,add(B,multiplicative_identity),C) ),
inference(resolve,[status(thm)],[c_11,c_149]) ).
cnf(c_13010,plain,
( sum(A,A,C)
| ~ product(B,add(A,multiplicative_identity),C)
| ~ sum(A,A,B) ),
inference(resolve,[status(thm)],[c_13009,c_149]) ).
cnf(c_13011,plain,
( sum(A,A,B)
| ~ product(add(A,A),add(A,multiplicative_identity),B) ),
inference(resolve,[status(thm)],[c_13010,c_29]) ).
cnf(c_13012,plain,
sum(A,A,multiply(add(A,multiplicative_identity),add(A,A))),
inference(resolve,[status(thm)],[c_13011,c_30]) ).
cnf(c_13013,plain,
sum(A,A,multiply(add(A,multiplicative_identity),A)),
inference(paramod,[status(thm)],[c_2465,c_13012]) ).
cnf(c_13014,plain,
sum(A,A,multiply(A,add(A,multiplicative_identity))),
inference(paramod,[status(thm)],[c_1459,c_13013]) ).
cnf(c_13015,plain,
sum(A,A,add(A,multiply(A,A))),
inference(paramod,[status(thm)],[c_2428,c_13014]) ).
cnf(c_13016,plain,
sum(A,A,add(A,A)),
inference(paramod,[status(thm)],[c_2079,c_13015]) ).
cnf(c_2567,plain,
sum(A,A,A),
inference(paramod,[status(thm)],[c_2465,c_13016]) ).
cnf(c_13017,plain,
( multiply(B,A) = C
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_22,c_30]) ).
cnf(c_13018,plain,
multiply(add(multiplicative_identity,A),multiplicative_identity) = multiplicative_identity,
inference(resolve,[status(thm)],[c_13017,c_251]) ).
cnf(c_13019,plain,
multiply(multiplicative_identity,add(multiplicative_identity,A)) = multiplicative_identity,
inference(paramod,[status(thm)],[c_1459,c_13018]) ).
cnf(c_13020,plain,
add(multiplicative_identity,multiply(multiplicative_identity,A)) = multiplicative_identity,
inference(paramod,[status(thm)],[c_2169,c_13019]) ).
cnf(c_3061,plain,
add(multiplicative_identity,A) = multiplicative_identity,
inference(paramod,[status(thm)],[c_847,c_13020]) ).
cnf(c_13021,plain,
( sum(E,B,F)
| ~ product(add(B,D),C,F)
| ~ product(D,A,E)
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_16,c_29]) ).
cnf(c_13022,plain,
( sum(C,D,E)
| ~ product(add(D,A),add(B,D),E)
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_13021,c_1]) ).
cnf(c_13023,plain,
( sum(multiplicative_identity,A,C)
| ~ product(add(A,multiplicative_identity),add(add(multiplicative_identity,B),A),C) ),
inference(resolve,[status(thm)],[c_13022,c_251]) ).
cnf(c_13024,plain,
sum(multiplicative_identity,A,multiply(add(add(multiplicative_identity,B),A),add(A,multiplicative_identity))),
inference(resolve,[status(thm)],[c_13023,c_30]) ).
cnf(c_13025,plain,
sum(multiplicative_identity,A,multiply(add(multiplicative_identity,A),add(A,multiplicative_identity))),
inference(paramod,[status(thm)],[c_3061,c_13024]) ).
cnf(c_13026,plain,
sum(multiplicative_identity,A,multiply(multiplicative_identity,add(A,multiplicative_identity))),
inference(paramod,[status(thm)],[c_3061,c_13025]) ).
cnf(c_13027,plain,
sum(multiplicative_identity,A,add(multiplicative_identity,multiply(multiplicative_identity,A))),
inference(paramod,[status(thm)],[c_2428,c_13026]) ).
cnf(c_13028,plain,
sum(multiplicative_identity,A,add(multiplicative_identity,A)),
inference(paramod,[status(thm)],[c_847,c_13027]) ).
cnf(c_3063,plain,
sum(multiplicative_identity,A,multiplicative_identity),
inference(paramod,[status(thm)],[c_3061,c_13028]) ).
cnf(c_13029,plain,
multiply(A,multiplicative_identity) = add(A,multiply(A,B)),
inference(paramod,[status(thm)],[c_3061,c_2169]) ).
cnf(c_13030,plain,
A = add(A,multiply(A,B)),
inference(paramod,[status(thm)],[c_846,c_13029]) ).
cnf(c_3119,plain,
add(A,multiply(A,B)) = A,
inference(copy,[status(thm)],[c_13030]) ).
cnf(c_3139,plain,
product(y,y_plus_z,y),
inference(paramod,[status(thm)],[c_3119,c_2150]) ).
cnf(c_3141,plain,
product(x,x_plus_y,x),
inference(paramod,[status(thm)],[c_3119,c_2148]) ).
cnf(c_13031,plain,
( product(x_plus_y,B,D)
| ~ sum(C,x,D)
| ~ product(y,A,C)
| ~ sum(A,x,B) ),
inference(resolve,[status(thm)],[c_15,c_1031]) ).
cnf(c_13032,plain,
( product(x_plus_y,x__plus_y_plus_z,B)
| ~ sum(A,x,B)
| ~ product(y,y_plus_z,A) ),
inference(resolve,[status(thm)],[c_13031,c_967]) ).
cnf(c_13033,plain,
( product(x_plus_y,x__plus_y_plus_z,A)
| ~ sum(y,x,A) ),
inference(resolve,[status(thm)],[c_13032,c_3139]) ).
cnf(c_3220,plain,
product(x_plus_y,x__plus_y_plus_z,x_plus_y),
inference(resolve,[status(thm)],[c_13033,c_1031]) ).
cnf(c_13034,plain,
( product(A,E,F)
| ~ sum(multiply(D,A),C,F)
| ~ sum(D,B,E)
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_10,c_30]) ).
cnf(c_13035,plain,
( product(x,B,C)
| ~ sum(multiply(A,x),x,C)
| ~ sum(A,x_plus_y,B) ),
inference(resolve,[status(thm)],[c_13034,c_3141]) ).
cnf(c_13036,plain,
( product(x,x_plus_y__plus_z,A)
| ~ sum(multiply(z,x),x,A) ),
inference(resolve,[status(thm)],[c_13035,c_1095]) ).
cnf(c_13037,plain,
product(x,x_plus_y__plus_z,add(x,multiply(z,x))),
inference(resolve,[status(thm)],[c_13036,c_29]) ).
cnf(c_13038,plain,
product(x,x_plus_y__plus_z,add(x,multiply(x,z))),
inference(paramod,[status(thm)],[c_1459,c_13037]) ).
cnf(c_3641,plain,
product(x,x_plus_y__plus_z,x),
inference(paramod,[status(thm)],[c_3119,c_13038]) ).
cnf(c_13039,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_30]) ).
cnf(c_13040,plain,
( sum(multiply(x__plus_y_plus_z,A),x_plus_y,C)
| ~ product(B,x__plus_y_plus_z,C)
| ~ sum(A,x_plus_y,B) ),
inference(resolve,[status(thm)],[c_13039,c_3220]) ).
cnf(c_13041,plain,
( sum(multiply(x__plus_y_plus_z,multiplicative_identity),x_plus_y,A)
| ~ product(multiplicative_identity,x__plus_y_plus_z,A) ),
inference(resolve,[status(thm)],[c_13040,c_3063]) ).
cnf(c_13042,plain,
sum(multiply(x__plus_y_plus_z,multiplicative_identity),x_plus_y,multiply(x__plus_y_plus_z,multiplicative_identity)),
inference(resolve,[status(thm)],[c_13041,c_30]) ).
cnf(c_13043,plain,
sum(multiply(multiplicative_identity,x__plus_y_plus_z),x_plus_y,multiply(x__plus_y_plus_z,multiplicative_identity)),
inference(paramod,[status(thm)],[c_1459,c_13042]) ).
cnf(c_13044,plain,
sum(x__plus_y_plus_z,x_plus_y,multiply(x__plus_y_plus_z,multiplicative_identity)),
inference(paramod,[status(thm)],[c_847,c_13043]) ).
cnf(c_13045,plain,
sum(x__plus_y_plus_z,x_plus_y,multiply(multiplicative_identity,x__plus_y_plus_z)),
inference(paramod,[status(thm)],[c_1459,c_13044]) ).
cnf(c_4297,plain,
sum(x__plus_y_plus_z,x_plus_y,x__plus_y_plus_z),
inference(paramod,[status(thm)],[c_847,c_13045]) ).
cnf(c_13046,plain,
( product(B,C,E)
| ~ sum(D,B,E)
| ~ product(B,A,D)
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_15,c_2567]) ).
cnf(c_13047,plain,
( product(additive_identity,A,C)
| ~ sum(B,additive_identity,C)
| ~ product(additive_identity,A,B) ),
inference(resolve,[status(thm)],[c_13046,c_6]) ).
cnf(c_13048,plain,
( product(additive_identity,A,B)
| ~ sum(add(multiply(additive_identity,A),multiply(additive_identity,A)),additive_identity,B) ),
inference(resolve,[status(thm)],[c_13047,c_144]) ).
cnf(c_13049,plain,
product(additive_identity,A,add(additive_identity,add(multiply(additive_identity,A),multiply(additive_identity,A)))),
inference(resolve,[status(thm)],[c_13048,c_29]) ).
cnf(c_13050,plain,
product(additive_identity,A,add(additive_identity,multiply(additive_identity,A))),
inference(paramod,[status(thm)],[c_2465,c_13049]) ).
cnf(c_5174,plain,
product(additive_identity,A,additive_identity),
inference(paramod,[status(thm)],[c_3119,c_13050]) ).
cnf(c_13051,plain,
( product(x_plus_y,B,D)
| ~ sum(C,y,D)
| ~ product(x,A,C)
| ~ sum(A,y,B) ),
inference(resolve,[status(thm)],[c_15,c_25]) ).
cnf(c_13052,plain,
( product(x_plus_y,y,B)
| ~ sum(A,y,B)
| ~ product(x,additive_identity,A) ),
inference(resolve,[status(thm)],[c_13051,c_5]) ).
cnf(c_13053,plain,
( product(x_plus_y,y,A)
| ~ sum(add(multiply(x,additive_identity),multiply(additive_identity,additive_identity)),y,A) ),
inference(resolve,[status(thm)],[c_13052,c_144]) ).
cnf(c_13054,plain,
product(x_plus_y,y,add(y,add(multiply(x,additive_identity),multiply(additive_identity,additive_identity)))),
inference(resolve,[status(thm)],[c_13053,c_29]) ).
cnf(c_13055,plain,
product(x_plus_y,y,add(y,add(multiply(additive_identity,x),multiply(additive_identity,additive_identity)))),
inference(paramod,[status(thm)],[c_1459,c_13054]) ).
cnf(c_13056,plain,
product(x_plus_y,y,add(y,add(multiply(additive_identity,x),additive_identity))),
inference(paramod,[status(thm)],[c_2079,c_13055]) ).
cnf(c_13057,plain,
product(x_plus_y,y,add(y,add(additive_identity,multiply(additive_identity,x)))),
inference(paramod,[status(thm)],[c_1110,c_13056]) ).
cnf(c_13058,plain,
product(x_plus_y,y,add(y,additive_identity)),
inference(paramod,[status(thm)],[c_3119,c_13057]) ).
cnf(c_13059,plain,
product(x_plus_y,y,add(additive_identity,y)),
inference(paramod,[status(thm)],[c_1110,c_13058]) ).
cnf(c_5206,plain,
product(x_plus_y,y,y),
inference(paramod,[status(thm)],[c_842,c_13059]) ).
cnf(c_13060,plain,
( product(x__plus_y_plus_z,B,D)
| ~ sum(C,y_plus_z,D)
| ~ product(x,A,C)
| ~ sum(A,y_plus_z,B) ),
inference(resolve,[status(thm)],[c_15,c_24]) ).
cnf(c_13061,plain,
( product(x__plus_y_plus_z,y_plus_z,B)
| ~ sum(A,y_plus_z,B)
| ~ product(x,additive_identity,A) ),
inference(resolve,[status(thm)],[c_13060,c_5]) ).
cnf(c_13062,plain,
( product(x__plus_y_plus_z,y_plus_z,A)
| ~ sum(add(multiply(x,additive_identity),multiply(additive_identity,additive_identity)),y_plus_z,A) ),
inference(resolve,[status(thm)],[c_13061,c_144]) ).
cnf(c_13063,plain,
product(x__plus_y_plus_z,y_plus_z,add(y_plus_z,add(multiply(x,additive_identity),multiply(additive_identity,additive_identity)))),
inference(resolve,[status(thm)],[c_13062,c_29]) ).
cnf(c_13064,plain,
product(x__plus_y_plus_z,y_plus_z,add(y_plus_z,add(multiply(additive_identity,x),multiply(additive_identity,additive_identity)))),
inference(paramod,[status(thm)],[c_1459,c_13063]) ).
cnf(c_13065,plain,
product(x__plus_y_plus_z,y_plus_z,add(y_plus_z,add(multiply(additive_identity,x),additive_identity))),
inference(paramod,[status(thm)],[c_2079,c_13064]) ).
cnf(c_13066,plain,
product(x__plus_y_plus_z,y_plus_z,add(y_plus_z,add(additive_identity,multiply(additive_identity,x)))),
inference(paramod,[status(thm)],[c_1110,c_13065]) ).
cnf(c_13067,plain,
product(x__plus_y_plus_z,y_plus_z,add(y_plus_z,additive_identity)),
inference(paramod,[status(thm)],[c_3119,c_13066]) ).
cnf(c_13068,plain,
product(x__plus_y_plus_z,y_plus_z,add(additive_identity,y_plus_z)),
inference(paramod,[status(thm)],[c_1110,c_13067]) ).
cnf(c_5212,plain,
product(x__plus_y_plus_z,y_plus_z,y_plus_z),
inference(paramod,[status(thm)],[c_842,c_13068]) ).
cnf(c_13069,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_30]) ).
cnf(c_13070,plain,
( sum(multiply(x_plus_y__plus_z,A),x,C)
| ~ product(B,x_plus_y__plus_z,C)
| ~ sum(A,x,B) ),
inference(resolve,[status(thm)],[c_13069,c_3641]) ).
cnf(c_13071,plain,
( sum(multiply(x_plus_y__plus_z,multiplicative_identity),x,A)
| ~ product(multiplicative_identity,x_plus_y__plus_z,A) ),
inference(resolve,[status(thm)],[c_13070,c_3063]) ).
cnf(c_13072,plain,
sum(multiply(x_plus_y__plus_z,multiplicative_identity),x,multiply(x_plus_y__plus_z,multiplicative_identity)),
inference(resolve,[status(thm)],[c_13071,c_30]) ).
cnf(c_13073,plain,
sum(multiply(multiplicative_identity,x_plus_y__plus_z),x,multiply(x_plus_y__plus_z,multiplicative_identity)),
inference(paramod,[status(thm)],[c_1459,c_13072]) ).
cnf(c_13074,plain,
sum(x_plus_y__plus_z,x,multiply(x_plus_y__plus_z,multiplicative_identity)),
inference(paramod,[status(thm)],[c_847,c_13073]) ).
cnf(c_13075,plain,
sum(x_plus_y__plus_z,x,multiply(multiplicative_identity,x_plus_y__plus_z)),
inference(paramod,[status(thm)],[c_1459,c_13074]) ).
cnf(c_6957,plain,
sum(x_plus_y__plus_z,x,x_plus_y__plus_z),
inference(paramod,[status(thm)],[c_847,c_13075]) ).
cnf(c_13076,plain,
( product(add(B,D),C,F)
| ~ sum(E,B,F)
| ~ product(D,A,E)
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_15,c_29]) ).
cnf(c_13077,plain,
( product(add(z,A),y_plus_z,C)
| ~ sum(B,z,C)
| ~ product(A,y,B) ),
inference(resolve,[status(thm)],[c_13076,c_23]) ).
cnf(c_13078,plain,
( product(add(z,additive_identity),y_plus_z,A)
| ~ sum(additive_identity,z,A) ),
inference(resolve,[status(thm)],[c_13077,c_5174]) ).
cnf(c_13079,plain,
product(add(z,additive_identity),y_plus_z,add(z,additive_identity)),
inference(resolve,[status(thm)],[c_13078,c_29]) ).
cnf(c_13080,plain,
product(add(additive_identity,z),y_plus_z,add(z,additive_identity)),
inference(paramod,[status(thm)],[c_1110,c_13079]) ).
cnf(c_13081,plain,
product(z,y_plus_z,add(z,additive_identity)),
inference(paramod,[status(thm)],[c_842,c_13080]) ).
cnf(c_13082,plain,
product(z,y_plus_z,add(additive_identity,z)),
inference(paramod,[status(thm)],[c_1110,c_13081]) ).
cnf(c_8391,plain,
product(z,y_plus_z,z),
inference(paramod,[status(thm)],[c_842,c_13082]) ).
cnf(c_13083,plain,
( product(add(B,D),C,F)
| ~ sum(E,B,F)
| ~ product(D,A,E)
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_15,c_29]) ).
cnf(c_13084,plain,
( product(add(D,A),add(D,B),E)
| ~ sum(C,D,E)
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_13083,c_29]) ).
cnf(c_13085,plain,
( product(add(A,x_plus_y),add(A,y),B)
| ~ sum(y,A,B) ),
inference(resolve,[status(thm)],[c_13084,c_5206]) ).
cnf(c_13086,plain,
product(add(z,x_plus_y),add(z,y),y_plus_z),
inference(resolve,[status(thm)],[c_13085,c_23]) ).
cnf(c_13087,plain,
product(add(x_plus_y,z),add(z,y),y_plus_z),
inference(paramod,[status(thm)],[c_1110,c_13086]) ).
cnf(c_13088,plain,
product(x_plus_y__plus_z,add(z,y),y_plus_z),
inference(paramod,[status(thm)],[c_1032,c_13087]) ).
cnf(c_13089,plain,
product(x_plus_y__plus_z,add(y,z),y_plus_z),
inference(paramod,[status(thm)],[c_1110,c_13088]) ).
cnf(c_8504,plain,
product(x_plus_y__plus_z,y_plus_z,y_plus_z),
inference(paramod,[status(thm)],[c_848,c_13089]) ).
cnf(c_13090,plain,
( sum(multiply(D,A),C,F)
| ~ product(A,E,F)
| ~ sum(D,B,E)
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_9,c_30]) ).
cnf(c_13091,plain,
( sum(multiply(A,x__plus_y_plus_z),y_plus_z,C)
| ~ product(x__plus_y_plus_z,B,C)
| ~ sum(A,y_plus_z,B) ),
inference(resolve,[status(thm)],[c_13090,c_5212]) ).
cnf(c_13092,plain,
( sum(multiply(multiplicative_identity,x__plus_y_plus_z),y_plus_z,A)
| ~ product(x__plus_y_plus_z,multiplicative_identity,A) ),
inference(resolve,[status(thm)],[c_13091,c_3063]) ).
cnf(c_13093,plain,
sum(multiply(multiplicative_identity,x__plus_y_plus_z),y_plus_z,multiply(multiplicative_identity,x__plus_y_plus_z)),
inference(resolve,[status(thm)],[c_13092,c_30]) ).
cnf(c_13094,plain,
sum(x__plus_y_plus_z,y_plus_z,multiply(multiplicative_identity,x__plus_y_plus_z)),
inference(paramod,[status(thm)],[c_847,c_13093]) ).
cnf(c_8605,plain,
sum(x__plus_y_plus_z,y_plus_z,x__plus_y_plus_z),
inference(paramod,[status(thm)],[c_847,c_13094]) ).
cnf(c_13095,plain,
( product(x_plus_y__plus_z,B,D)
| ~ sum(C,x,D)
| ~ product(x_plus_y__plus_z,A,C)
| ~ sum(A,x,B) ),
inference(resolve,[status(thm)],[c_15,c_6957]) ).
cnf(c_13096,plain,
( product(x_plus_y__plus_z,x__plus_y_plus_z,B)
| ~ sum(A,x,B)
| ~ product(x_plus_y__plus_z,y_plus_z,A) ),
inference(resolve,[status(thm)],[c_13095,c_967]) ).
cnf(c_13097,plain,
( product(x_plus_y__plus_z,x__plus_y_plus_z,A)
| ~ sum(y_plus_z,x,A) ),
inference(resolve,[status(thm)],[c_13096,c_8504]) ).
cnf(c_10655,plain,
product(x_plus_y__plus_z,x__plus_y_plus_z,x__plus_y_plus_z),
inference(resolve,[status(thm)],[c_13097,c_967]) ).
cnf(c_13098,plain,
( product(A,E,F)
| ~ sum(multiply(D,A),C,F)
| ~ sum(D,B,E)
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_10,c_30]) ).
cnf(c_13099,plain,
( product(z,B,C)
| ~ sum(multiply(A,z),z,C)
| ~ sum(A,y_plus_z,B) ),
inference(resolve,[status(thm)],[c_13098,c_8391]) ).
cnf(c_13100,plain,
( product(z,x__plus_y_plus_z,A)
| ~ sum(multiply(x__plus_y_plus_z,z),z,A) ),
inference(resolve,[status(thm)],[c_13099,c_8605]) ).
cnf(c_13101,plain,
product(z,x__plus_y_plus_z,add(z,multiply(x__plus_y_plus_z,z))),
inference(resolve,[status(thm)],[c_13100,c_29]) ).
cnf(c_13102,plain,
product(z,x__plus_y_plus_z,add(z,multiply(z,x__plus_y_plus_z))),
inference(paramod,[status(thm)],[c_1459,c_13101]) ).
cnf(c_12198,plain,
product(z,x__plus_y_plus_z,z),
inference(paramod,[status(thm)],[c_3119,c_13102]) ).
cnf(c_13103,plain,
( sum(C,x_plus_y,D)
| ~ product(x_plus_y__plus_z,B,D)
| ~ product(z,A,C)
| ~ sum(A,x_plus_y,B) ),
inference(resolve,[status(thm)],[c_16,c_1095]) ).
cnf(c_13104,plain,
( sum(A,x_plus_y,B)
| ~ product(x_plus_y__plus_z,x__plus_y_plus_z,B)
| ~ product(z,x__plus_y_plus_z,A) ),
inference(resolve,[status(thm)],[c_13103,c_4297]) ).
cnf(c_13105,plain,
( sum(A,x_plus_y,x__plus_y_plus_z)
| ~ product(z,x__plus_y_plus_z,A) ),
inference(resolve,[status(thm)],[c_13104,c_10655]) ).
cnf(c_12955,plain,
~ product(z,x__plus_y_plus_z,z),
inference(resolve,[status(thm)],[c_13105,c_1800]) ).
cnf(c_12956,plain,
$false,
inference(resolve,[status(thm)],[c_12955,c_12198]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : BOO008-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.43 % Computer : n009.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.44 % CPULimit : 300
% 0.17/0.44 % WCLimit : 300
% 0.17/0.44 % DateTime : Sat Sep 26 22:33:44 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.17/0.44 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.17/0.44 % Process 1294084 was started by sandbox2 on n009,
% 0.17/0.44 % Sat Sep 26 22:33:44 2026
% 0.17/0.44 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.17/0.45
% 0.17/0.45 % From the command line: assign(max_seconds, 300).
% 120.67/15.77
% 120.67/15.77 % SZS status Unsatisfiable for theBenchmark
% 120.67/15.77
% 120.67/15.77 % Proof 1 at 11.41 (+ 3.82) seconds.
% 120.67/15.77 % Length of proof is 74.
% 120.67/15.77 % Level of proof is 11.
% 120.67/15.77 % Maximum clause weight is 20.000.
% 120.67/15.77 % Given clauses 206.
% 120.67/15.77
% 120.67/15.77 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------