%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : RNG008-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 : n017.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 08:26:18 AM UTC 2026
% Result : Unsatisfiable 53.76s 7.24s
% Output : CNFRefutation 53.76s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 17
% Syntax : Number of formulae : 182 ( 95 unt; 0 def)
% Number of atoms : 345 ( 47 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 338 ( 175 ~; 163 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 3 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 7 ( 7 usr; 4 con; 0-2 aty)
% Number of variables : 480 ( 8 sgn 56 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(additive_identity1,axiom,
! [VAR_0] : sum(additive_identity,VAR_0,VAR_0),
file('theBenchmark.p',additive_identity1) ).
cnf(c_1,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_2,plain,
sum(A,additive_identity,A),
inference(clausify,[status(thm)],[additive_identity2]) ).
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_3,plain,
product(A,B,multiply(A,B)),
inference(clausify,[status(thm)],[closure_of_multiplication]) ).
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_4,plain,
sum(A,B,add(A,B)),
inference(clausify,[status(thm)],[closure_of_addition]) ).
fof(left_inverse,axiom,
! [VAR_0] : sum(additive_inverse(VAR_0),VAR_0,additive_identity),
file('theBenchmark.p',left_inverse) ).
cnf(c_5,plain,
sum(additive_inverse(A),A,additive_identity),
inference(clausify,[status(thm)],[left_inverse]) ).
fof(right_inverse,axiom,
! [VAR_0] : sum(VAR_0,additive_inverse(VAR_0),additive_identity),
file('theBenchmark.p',right_inverse) ).
cnf(c_6,plain,
sum(A,additive_inverse(A),additive_identity),
inference(clausify,[status(thm)],[right_inverse]) ).
fof(associativity_of_addition1,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( sum(VAR_0,VAR_4,VAR_5)
| ~ sum(VAR_2,VAR_3,VAR_5)
| ~ sum(VAR_1,VAR_3,VAR_4)
| ~ sum(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',associativity_of_addition1) ).
cnf(c_7,plain,
( sum(A,E,F)
| ~ sum(C,D,F)
| ~ sum(B,D,E)
| ~ sum(A,B,C) ),
inference(clausify,[status(thm)],[associativity_of_addition1]) ).
fof(associativity_of_addition2,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5] :
( sum(VAR_2,VAR_3,VAR_5)
| ~ sum(VAR_0,VAR_4,VAR_5)
| ~ sum(VAR_1,VAR_3,VAR_4)
| ~ sum(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',associativity_of_addition2) ).
cnf(c_8,plain,
( sum(C,D,F)
| ~ sum(A,E,F)
| ~ sum(B,D,E)
| ~ sum(A,B,C) ),
inference(clausify,[status(thm)],[associativity_of_addition2]) ).
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_9,plain,
( sum(B,A,C)
| ~ sum(A,B,C) ),
inference(clausify,[status(thm)],[commutativity_of_addition]) ).
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_12,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_13,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_14,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_15,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(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_16,plain,
( C = D
| ~ sum(A,B,D)
| ~ sum(A,B,C) ),
inference(clausify,[status(thm)],[addition_is_well_defined]) ).
fof(x_squared_is_x,axiom,
! [VAR_0] : product(VAR_0,VAR_0,VAR_0),
file('theBenchmark.p',x_squared_is_x) ).
cnf(c_18,plain,
product(A,A,A),
inference(clausify,[status(thm)],[x_squared_is_x]) ).
fof(a_times_b_is_c,axiom,
product(a,b,c),
file('theBenchmark.p',a_times_b_is_c) ).
cnf(c_19,plain,
product(a,b,c),
inference(clausify,[status(thm)],[a_times_b_is_c]) ).
fof(prove_b_times_a_is_c,axiom,
~ product(b,a,c),
file('theBenchmark.p',prove_b_times_a_is_c) ).
cnf(c_20,plain,
~ product(b,a,c),
inference(clausify,[status(thm)],[prove_b_times_a_is_c]) ).
cnf(c_14131,plain,
( sum(A,C,D)
| ~ sum(additive_identity,B,D)
| ~ sum(additive_inverse(A),B,C) ),
inference(resolve,[status(thm)],[c_7,c_6]) ).
cnf(c_14132,plain,
( sum(A,additive_identity,B)
| ~ sum(additive_identity,additive_inverse(additive_inverse(A)),B) ),
inference(resolve,[status(thm)],[c_14131,c_6]) ).
cnf(c_22,plain,
sum(A,additive_identity,additive_inverse(additive_inverse(A))),
inference(resolve,[status(thm)],[c_14132,c_1]) ).
cnf(c_14133,plain,
( sum(A,C,D)
| ~ sum(additive_identity,B,D)
| ~ sum(additive_inverse(A),B,C) ),
inference(resolve,[status(thm)],[c_7,c_6]) ).
cnf(c_14134,plain,
( sum(C,add(additive_inverse(C),A),B)
| ~ sum(additive_identity,A,B) ),
inference(resolve,[status(thm)],[c_14133,c_4]) ).
cnf(c_27,plain,
sum(A,add(additive_inverse(A),B),B),
inference(resolve,[status(thm)],[c_14134,c_1]) ).
cnf(c_14135,plain,
( sum(additive_inverse(A),C,D)
| ~ sum(additive_identity,B,D)
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_7,c_5]) ).
cnf(c_14136,plain,
( sum(additive_inverse(C),add(C,A),B)
| ~ sum(additive_identity,A,B) ),
inference(resolve,[status(thm)],[c_14135,c_4]) ).
cnf(c_36,plain,
sum(additive_inverse(A),add(A,B),B),
inference(resolve,[status(thm)],[c_14136,c_1]) ).
cnf(c_14137,plain,
( sum(D,C,E)
| ~ sum(add(D,A),B,E)
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_7,c_4]) ).
cnf(c_14138,plain,
( sum(A,add(B,C),D)
| ~ sum(add(A,B),C,D) ),
inference(resolve,[status(thm)],[c_14137,c_4]) ).
cnf(c_45,plain,
sum(A,add(B,C),add(add(A,B),C)),
inference(resolve,[status(thm)],[c_14138,c_4]) ).
cnf(c_14139,plain,
( sum(add(D,A),B,E)
| ~ sum(D,C,E)
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_8,c_4]) ).
cnf(c_14140,plain,
( sum(add(A,additive_inverse(C)),C,B)
| ~ sum(A,additive_identity,B) ),
inference(resolve,[status(thm)],[c_14139,c_5]) ).
cnf(c_75,plain,
sum(add(A,additive_inverse(B)),B,A),
inference(resolve,[status(thm)],[c_14140,c_2]) ).
cnf(c_14141,plain,
( sum(add(D,A),B,E)
| ~ sum(D,C,E)
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_8,c_4]) ).
cnf(c_14142,plain,
( sum(add(A,B),C,D)
| ~ sum(A,add(B,C),D) ),
inference(resolve,[status(thm)],[c_14141,c_4]) ).
cnf(c_77,plain,
sum(add(A,B),C,add(A,add(B,C))),
inference(resolve,[status(thm)],[c_14142,c_4]) ).
cnf(c_92,plain,
sum(A,B,add(B,A)),
inference(resolve,[status(thm)],[c_9,c_4]) ).
cnf(c_14143,plain,
( product(A,E,F)
| ~ sum(multiply(A,D),C,F)
| ~ sum(D,B,E)
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_13,c_3]) ).
cnf(c_14144,plain,
( product(D,C,E)
| ~ sum(multiply(D,A),multiply(D,B),E)
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_14143,c_3]) ).
cnf(c_14145,plain,
( product(A,add(B,C),D)
| ~ sum(multiply(A,B),multiply(A,C),D) ),
inference(resolve,[status(thm)],[c_14144,c_4]) ).
cnf(c_102,plain,
product(A,add(B,C),add(multiply(A,B),multiply(A,C))),
inference(resolve,[status(thm)],[c_14145,c_4]) ).
cnf(c_14146,plain,
( additive_identity = B
| ~ sum(A,additive_inverse(A),B) ),
inference(resolve,[status(thm)],[c_16,c_6]) ).
cnf(c_14147,plain,
additive_identity = add(A,additive_inverse(A)),
inference(resolve,[status(thm)],[c_14146,c_4]) ).
cnf(c_115,plain,
add(A,additive_inverse(A)) = additive_identity,
inference(copy,[status(thm)],[c_14147]) ).
cnf(c_14148,plain,
( additive_identity = B
| ~ sum(A,additive_inverse(A),B) ),
inference(resolve,[status(thm)],[c_16,c_6]) ).
cnf(c_14149,plain,
additive_identity = additive_inverse(additive_identity),
inference(resolve,[status(thm)],[c_14148,c_1]) ).
cnf(c_116,plain,
additive_inverse(additive_identity) = additive_identity,
inference(copy,[status(thm)],[c_14149]) ).
cnf(c_14150,plain,
( add(A,B) = C
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_16,c_4]) ).
cnf(c_118,plain,
add(A,additive_identity) = A,
inference(resolve,[status(thm)],[c_14150,c_2]) ).
cnf(c_14151,plain,
( add(A,B) = C
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_16,c_4]) ).
cnf(c_119,plain,
add(additive_identity,A) = A,
inference(resolve,[status(thm)],[c_14151,c_1]) ).
cnf(c_14152,plain,
( sum(B,C,E)
| ~ product(D,B,E)
| ~ sum(B,A,D)
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_14,c_18]) ).
cnf(c_14153,plain,
( sum(A,multiply(B,A),D)
| ~ product(C,A,D)
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_14152,c_3]) ).
cnf(c_14154,plain,
( sum(A,multiply(additive_identity,A),B)
| ~ product(A,A,B) ),
inference(resolve,[status(thm)],[c_14153,c_2]) ).
cnf(c_130,plain,
sum(A,multiply(additive_identity,A),A),
inference(resolve,[status(thm)],[c_14154,c_18]) ).
cnf(c_14155,plain,
( sum(multiply(D,B),C,F)
| ~ product(E,B,F)
| ~ sum(D,A,E)
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_14,c_3]) ).
cnf(c_14156,plain,
( sum(multiply(A,B),B,D)
| ~ product(C,B,D)
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_14155,c_18]) ).
cnf(c_14157,plain,
( sum(multiply(additive_identity,A),A,B)
| ~ product(A,A,B) ),
inference(resolve,[status(thm)],[c_14156,c_1]) ).
cnf(c_131,plain,
sum(multiply(additive_identity,A),A,A),
inference(resolve,[status(thm)],[c_14157,c_18]) ).
cnf(c_14158,plain,
( sum(B,C,E)
| ~ product(D,B,E)
| ~ sum(B,A,D)
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_14,c_18]) ).
cnf(c_14159,plain,
( sum(A,multiply(B,A),D)
| ~ product(C,A,D)
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_14158,c_3]) ).
cnf(c_14160,plain,
( sum(A,multiply(additive_inverse(A),A),B)
| ~ product(additive_identity,A,B) ),
inference(resolve,[status(thm)],[c_14159,c_6]) ).
cnf(c_139,plain,
sum(A,multiply(additive_inverse(A),A),multiply(additive_identity,A)),
inference(resolve,[status(thm)],[c_14160,c_3]) ).
cnf(c_14161,plain,
( sum(A,C,E)
| ~ product(A,D,E)
| ~ sum(A,B,D)
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_12,c_18]) ).
cnf(c_14162,plain,
( sum(A,multiply(A,B),D)
| ~ product(A,C,D)
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_14161,c_3]) ).
cnf(c_14163,plain,
( sum(A,multiply(A,additive_identity),B)
| ~ product(A,A,B) ),
inference(resolve,[status(thm)],[c_14162,c_2]) ).
cnf(c_151,plain,
sum(A,multiply(A,additive_identity),A),
inference(resolve,[status(thm)],[c_14163,c_18]) ).
cnf(c_14164,plain,
( sum(A,C,E)
| ~ product(A,D,E)
| ~ sum(A,B,D)
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_12,c_18]) ).
cnf(c_14165,plain,
( sum(A,multiply(A,B),D)
| ~ product(A,C,D)
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_14164,c_3]) ).
cnf(c_14166,plain,
( sum(A,multiply(A,additive_inverse(A)),B)
| ~ product(A,additive_identity,B) ),
inference(resolve,[status(thm)],[c_14165,c_6]) ).
cnf(c_160,plain,
sum(A,multiply(A,additive_inverse(A)),multiply(A,additive_identity)),
inference(resolve,[status(thm)],[c_14166,c_3]) ).
cnf(c_14167,plain,
( product(E,B,F)
| ~ sum(multiply(D,B),C,F)
| ~ sum(D,A,E)
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_15,c_3]) ).
cnf(c_14168,plain,
( product(C,D,E)
| ~ sum(multiply(A,D),multiply(B,D),E)
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_14167,c_3]) ).
cnf(c_14169,plain,
( product(B,A,C)
| ~ sum(multiply(additive_identity,A),multiply(B,A),C) ),
inference(resolve,[status(thm)],[c_14168,c_1]) ).
cnf(c_217,plain,
~ sum(multiply(additive_identity,a),multiply(b,a),c),
inference(resolve,[status(thm)],[c_14169,c_20]) ).
cnf(c_14170,plain,
( add(A,B) = C
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_16,c_4]) ).
cnf(c_14171,plain,
add(A,additive_identity) = additive_inverse(additive_inverse(A)),
inference(resolve,[status(thm)],[c_14170,c_22]) ).
cnf(c_14172,plain,
A = additive_inverse(additive_inverse(A)),
inference(paramod,[status(thm)],[c_118,c_14171]) ).
cnf(c_222,plain,
additive_inverse(additive_inverse(A)) = A,
inference(copy,[status(thm)],[c_14172]) ).
cnf(c_14173,plain,
( add(A,B) = C
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_16,c_4]) ).
cnf(c_516,plain,
add(additive_inverse(A),add(A,B)) = B,
inference(resolve,[status(thm)],[c_14173,c_36]) ).
cnf(c_537,plain,
sum(add(A,B),additive_inverse(A),B),
inference(resolve,[status(thm)],[c_9,c_36]) ).
cnf(c_14174,plain,
( B = C
| ~ sum(additive_inverse(A),add(A,B),C) ),
inference(resolve,[status(thm)],[c_16,c_36]) ).
cnf(c_14175,plain,
A = add(add(B,A),additive_inverse(B)),
inference(resolve,[status(thm)],[c_14174,c_92]) ).
cnf(c_637,plain,
add(add(A,B),additive_inverse(A)) = B,
inference(copy,[status(thm)],[c_14175]) ).
cnf(c_14176,plain,
( add(A,B) = C
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_16,c_4]) ).
cnf(c_639,plain,
add(A,B) = add(B,A),
inference(resolve,[status(thm)],[c_14176,c_92]) ).
cnf(c_14177,plain,
( sum(A,C,D)
| ~ sum(additive_identity,B,D)
| ~ sum(additive_inverse(A),B,C) ),
inference(resolve,[status(thm)],[c_7,c_6]) ).
cnf(c_14178,plain,
( sum(C,add(A,additive_inverse(C)),B)
| ~ sum(additive_identity,A,B) ),
inference(resolve,[status(thm)],[c_14177,c_92]) ).
cnf(c_14179,plain,
sum(A,add(B,additive_inverse(A)),add(B,additive_identity)),
inference(resolve,[status(thm)],[c_14178,c_92]) ).
cnf(c_723,plain,
sum(A,add(B,additive_inverse(A)),B),
inference(paramod,[status(thm)],[c_118,c_14179]) ).
cnf(c_14180,plain,
( sum(additive_inverse(A),C,D)
| ~ sum(additive_identity,B,D)
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_7,c_5]) ).
cnf(c_14181,plain,
( sum(additive_inverse(C),add(A,C),B)
| ~ sum(additive_identity,A,B) ),
inference(resolve,[status(thm)],[c_14180,c_92]) ).
cnf(c_14182,plain,
sum(additive_inverse(A),add(B,A),add(B,additive_identity)),
inference(resolve,[status(thm)],[c_14181,c_92]) ).
cnf(c_724,plain,
sum(additive_inverse(A),add(B,A),B),
inference(paramod,[status(thm)],[c_118,c_14182]) ).
cnf(c_14183,plain,
( sum(add(A,D),B,E)
| ~ sum(D,C,E)
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_8,c_92]) ).
cnf(c_14184,plain,
( sum(add(B,A),multiply(additive_identity,B),C)
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_14183,c_130]) ).
cnf(c_14185,plain,
sum(add(A,additive_inverse(A)),multiply(additive_identity,A),additive_identity),
inference(resolve,[status(thm)],[c_14184,c_5]) ).
cnf(c_1009,plain,
sum(additive_identity,multiply(additive_identity,A),additive_identity),
inference(paramod,[status(thm)],[c_115,c_14185]) ).
cnf(c_14186,plain,
( sum(multiply(additive_identity,A),C,D)
| ~ sum(A,B,D)
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_7,c_131]) ).
cnf(c_14187,plain,
( sum(multiply(additive_identity,A),C,B)
| ~ sum(A,add(additive_inverse(A),B),C) ),
inference(resolve,[status(thm)],[c_14186,c_27]) ).
cnf(c_14188,plain,
~ sum(a,add(additive_inverse(a),c),multiply(b,a)),
inference(resolve,[status(thm)],[c_14187,c_217]) ).
cnf(c_1275,plain,
~ sum(a,add(c,additive_inverse(a)),multiply(b,a)),
inference(paramod,[status(thm)],[c_639,c_14188]) ).
cnf(c_14189,plain,
( sum(add(A,D),B,E)
| ~ sum(D,C,E)
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_8,c_92]) ).
cnf(c_14190,plain,
( sum(add(B,A),multiply(B,additive_identity),C)
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_14189,c_151]) ).
cnf(c_14191,plain,
sum(add(A,additive_inverse(A)),multiply(A,additive_identity),additive_identity),
inference(resolve,[status(thm)],[c_14190,c_5]) ).
cnf(c_1313,plain,
sum(additive_identity,multiply(A,additive_identity),additive_identity),
inference(paramod,[status(thm)],[c_115,c_14191]) ).
cnf(c_14192,plain,
( add(A,B) = C
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_16,c_4]) ).
cnf(c_14193,plain,
add(A,add(B,C)) = add(add(A,B),C),
inference(resolve,[status(thm)],[c_14192,c_45]) ).
cnf(c_2183,plain,
add(add(A,B),C) = add(A,add(B,C)),
inference(copy,[status(thm)],[c_14193]) ).
cnf(c_14194,plain,
( add(add(A,B),C) = D
| ~ sum(A,add(B,C),D) ),
inference(resolve,[status(thm)],[c_16,c_45]) ).
cnf(c_14195,plain,
add(add(A,B),C) = add(add(B,C),A),
inference(resolve,[status(thm)],[c_14194,c_92]) ).
cnf(c_14196,plain,
add(A,add(B,C)) = add(add(B,C),A),
inference(paramod,[status(thm)],[c_2183,c_14195]) ).
cnf(c_14197,plain,
add(A,add(B,C)) = add(B,add(C,A)),
inference(paramod,[status(thm)],[c_2183,c_14196]) ).
cnf(c_2184,plain,
add(A,add(B,C)) = add(C,add(A,B)),
inference(copy,[status(thm)],[c_14197]) ).
cnf(c_2329,plain,
add(A,add(B,additive_inverse(A))) = B,
inference(paramod,[status(thm)],[c_2183,c_637]) ).
cnf(c_14198,plain,
( sum(A,B,D)
| ~ sum(additive_identity,C,D)
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_8,c_1]) ).
cnf(c_14199,plain,
( sum(B,A,C)
| ~ sum(additive_identity,add(A,B),C) ),
inference(resolve,[status(thm)],[c_14198,c_92]) ).
cnf(c_14200,plain,
~ sum(additive_identity,add(add(c,additive_inverse(a)),a),multiply(b,a)),
inference(resolve,[status(thm)],[c_14199,c_1275]) ).
cnf(c_14201,plain,
~ sum(additive_identity,add(a,add(c,additive_inverse(a))),multiply(b,a)),
inference(paramod,[status(thm)],[c_639,c_14200]) ).
cnf(c_2422,plain,
~ sum(additive_identity,c,multiply(b,a)),
inference(paramod,[status(thm)],[c_2329,c_14201]) ).
cnf(c_14202,plain,
( sum(B,C,E)
| ~ sum(additive_inverse(A),D,E)
| ~ sum(add(A,B),C,D) ),
inference(resolve,[status(thm)],[c_8,c_36]) ).
cnf(c_14203,plain,
( sum(B,C,D)
| ~ sum(add(A,B),C,add(A,D)) ),
inference(resolve,[status(thm)],[c_14202,c_36]) ).
cnf(c_14204,plain,
~ sum(add(A,additive_identity),c,add(A,multiply(b,a))),
inference(resolve,[status(thm)],[c_14203,c_2422]) ).
cnf(c_2452,plain,
~ sum(A,c,add(A,multiply(b,a))),
inference(paramod,[status(thm)],[c_118,c_14204]) ).
cnf(c_14205,plain,
( add(B,A) = C
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_16,c_92]) ).
cnf(c_14206,plain,
add(multiply(additive_identity,A),additive_identity) = additive_identity,
inference(resolve,[status(thm)],[c_14205,c_1009]) ).
cnf(c_14207,plain,
add(additive_identity,multiply(additive_identity,A)) = additive_identity,
inference(paramod,[status(thm)],[c_639,c_14206]) ).
cnf(c_2615,plain,
multiply(additive_identity,A) = additive_identity,
inference(paramod,[status(thm)],[c_119,c_14207]) ).
cnf(c_2757,plain,
sum(A,multiply(additive_inverse(A),A),additive_identity),
inference(paramod,[status(thm)],[c_2615,c_139]) ).
cnf(c_14208,plain,
( add(B,A) = C
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_16,c_92]) ).
cnf(c_14209,plain,
add(multiply(A,additive_identity),additive_identity) = additive_identity,
inference(resolve,[status(thm)],[c_14208,c_1313]) ).
cnf(c_14210,plain,
add(additive_identity,multiply(A,additive_identity)) = additive_identity,
inference(paramod,[status(thm)],[c_639,c_14209]) ).
cnf(c_2994,plain,
multiply(A,additive_identity) = additive_identity,
inference(paramod,[status(thm)],[c_119,c_14210]) ).
cnf(c_3032,plain,
sum(A,multiply(A,additive_inverse(A)),additive_identity),
inference(paramod,[status(thm)],[c_2994,c_160]) ).
cnf(c_14211,plain,
( sum(A,C,E)
| ~ product(A,D,E)
| ~ sum(A,B,D)
| ~ product(A,B,C) ),
inference(resolve,[status(thm)],[c_12,c_18]) ).
cnf(c_14212,plain,
( sum(a,c,B)
| ~ product(a,A,B)
| ~ sum(a,b,A) ),
inference(resolve,[status(thm)],[c_14211,c_19]) ).
cnf(c_14213,plain,
( sum(a,c,A)
| ~ product(a,add(b,a),A) ),
inference(resolve,[status(thm)],[c_14212,c_92]) ).
cnf(c_14214,plain,
~ product(a,add(b,a),add(a,multiply(b,a))),
inference(resolve,[status(thm)],[c_14213,c_2452]) ).
cnf(c_4715,plain,
~ product(a,add(a,b),add(a,multiply(b,a))),
inference(paramod,[status(thm)],[c_639,c_14214]) ).
cnf(c_14215,plain,
( sum(D,B,E)
| ~ sum(add(A,D),C,E)
| ~ sum(additive_inverse(A),B,C) ),
inference(resolve,[status(thm)],[c_8,c_537]) ).
cnf(c_14216,plain,
( sum(B,multiply(additive_inverse(additive_inverse(A)),additive_inverse(A)),C)
| ~ sum(add(A,B),additive_identity,C) ),
inference(resolve,[status(thm)],[c_14215,c_2757]) ).
cnf(c_14217,plain,
sum(additive_inverse(additive_identity),multiply(additive_inverse(additive_inverse(A)),additive_inverse(A)),A),
inference(resolve,[status(thm)],[c_14216,c_75]) ).
cnf(c_14218,plain,
sum(additive_identity,multiply(additive_inverse(additive_inverse(A)),additive_inverse(A)),A),
inference(paramod,[status(thm)],[c_116,c_14217]) ).
cnf(c_6088,plain,
sum(additive_identity,multiply(A,additive_inverse(A)),A),
inference(paramod,[status(thm)],[c_222,c_14218]) ).
cnf(c_14219,plain,
( product(F,add(B,C),V6)
| ~ sum(add(multiply(E,B),multiply(E,C)),D,V6)
| ~ sum(E,A,F)
| ~ product(A,add(B,C),D) ),
inference(resolve,[status(thm)],[c_15,c_102]) ).
cnf(c_14220,plain,
( product(D,add(B,C),E)
| ~ sum(add(multiply(A,B),multiply(A,C)),add(B,C),E)
| ~ sum(A,add(B,C),D) ),
inference(resolve,[status(thm)],[c_14219,c_18]) ).
cnf(c_14221,plain,
( product(B,add(B,additive_inverse(A)),C)
| ~ sum(add(multiply(A,B),multiply(A,additive_inverse(A))),add(B,additive_inverse(A)),C) ),
inference(resolve,[status(thm)],[c_14220,c_723]) ).
cnf(c_14222,plain,
product(A,add(A,additive_inverse(B)),add(multiply(B,A),add(multiply(B,additive_inverse(B)),add(A,additive_inverse(B))))),
inference(resolve,[status(thm)],[c_14221,c_77]) ).
cnf(c_9455,plain,
product(A,add(A,additive_inverse(B)),add(multiply(B,A),add(additive_inverse(B),add(multiply(B,additive_inverse(B)),A)))),
inference(paramod,[status(thm)],[c_2184,c_14222]) ).
cnf(c_14223,plain,
( add(B,A) = C
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_16,c_92]) ).
cnf(c_14224,plain,
add(multiply(A,additive_inverse(A)),additive_identity) = A,
inference(resolve,[status(thm)],[c_14223,c_6088]) ).
cnf(c_14225,plain,
add(additive_identity,multiply(A,additive_inverse(A))) = A,
inference(paramod,[status(thm)],[c_639,c_14224]) ).
cnf(c_12857,plain,
multiply(A,additive_inverse(A)) = A,
inference(paramod,[status(thm)],[c_119,c_14225]) ).
cnf(c_14226,plain,
( sum(additive_inverse(B),D,E)
| ~ sum(A,C,E)
| ~ sum(add(A,B),C,D) ),
inference(resolve,[status(thm)],[c_7,c_724]) ).
cnf(c_14227,plain,
( sum(additive_inverse(B),additive_identity,C)
| ~ sum(A,multiply(add(A,B),additive_inverse(add(A,B))),C) ),
inference(resolve,[status(thm)],[c_14226,c_3032]) ).
cnf(c_14228,plain,
sum(additive_inverse(A),additive_identity,add(additive_identity,A)),
inference(resolve,[status(thm)],[c_14227,c_6088]) ).
cnf(c_12898,plain,
sum(additive_inverse(A),additive_identity,A),
inference(paramod,[status(thm)],[c_119,c_14228]) ).
cnf(c_14229,plain,
product(A,add(A,additive_inverse(B)),add(multiply(B,A),add(additive_inverse(B),add(B,A)))),
inference(paramod,[status(thm)],[c_12857,c_9455]) ).
cnf(c_14230,plain,
product(A,add(A,additive_inverse(B)),add(multiply(B,A),A)),
inference(paramod,[status(thm)],[c_516,c_14229]) ).
cnf(c_13058,plain,
product(A,add(A,additive_inverse(B)),add(A,multiply(B,A))),
inference(paramod,[status(thm)],[c_639,c_14230]) ).
cnf(c_14231,plain,
( add(B,A) = C
| ~ sum(A,B,C) ),
inference(resolve,[status(thm)],[c_16,c_92]) ).
cnf(c_14232,plain,
add(additive_identity,additive_inverse(A)) = A,
inference(resolve,[status(thm)],[c_14231,c_12898]) ).
cnf(c_13965,plain,
additive_inverse(A) = A,
inference(paramod,[status(thm)],[c_119,c_14232]) ).
cnf(c_14129,plain,
product(A,add(A,B),add(A,multiply(B,A))),
inference(paramod,[status(thm)],[c_13965,c_13058]) ).
cnf(c_14130,plain,
$false,
inference(resolve,[status(thm)],[c_14129,c_4715]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : RNG008-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n017.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 26 05:40:04 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.36 % Process 4170528 was started by sandbox2 on n017,
% 0.09/0.36 % Sat Sep 26 05:40:04 2026
% 0.09/0.36 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.13/0.36
% 0.13/0.36 % From the command line: assign(max_seconds, 300).
% 53.76/7.24
% 53.76/7.24 % SZS status Unsatisfiable for theBenchmark
% 53.76/7.24
% 53.76/7.24 % Proof 1 at 5.40 (+ 1.36) seconds.
% 53.76/7.24 % Length of proof is 63.
% 53.76/7.24 % Level of proof is 9.
% 53.76/7.24 % Maximum clause weight is 20.000.
% 53.76/7.24 % Given clauses 155.
% 53.76/7.24
% 53.76/7.24 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------