%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : RNG009-7 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : 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 08:26:20 AM UTC 2026
% Result : Unsatisfiable 104.29s 24.68s
% Output : CNFRefutation 104.29s
% Verified :
% SZS Type : Refutation
% Derivation depth : 86
% Number of leaves : 11
% Syntax : Number of formulae : 211 ( 211 unt; 0 def)
% Number of atoms : 211 ( 210 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 12 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 4 con; 0-2 aty)
% Number of variables : 434 ( 12 sgn 18 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(left_additive_identity,axiom,
! [VAR_0] : add(additive_identity,VAR_0) = VAR_0,
file('theBenchmark.p',left_additive_identity) ).
cnf(c_1,plain,
add(additive_identity,A) = A,
inference(clausify,[status(thm)],[left_additive_identity]) ).
fof(right_additive_identity,axiom,
! [VAR_0] : add(VAR_0,additive_identity) = VAR_0,
file('theBenchmark.p',right_additive_identity) ).
cnf(c_2,plain,
add(A,additive_identity) = A,
inference(clausify,[status(thm)],[right_additive_identity]) ).
fof(right_additive_inverse,axiom,
! [VAR_0] : add(VAR_0,additive_inverse(VAR_0)) = additive_identity,
file('theBenchmark.p',right_additive_inverse) ).
cnf(c_4,plain,
add(A,additive_inverse(A)) = additive_identity,
inference(clausify,[status(thm)],[right_additive_inverse]) ).
fof(associativity_for_addition,axiom,
! [VAR_0,VAR_1,VAR_2] : add(VAR_0,add(VAR_1,VAR_2)) = add(add(VAR_0,VAR_1),VAR_2),
file('theBenchmark.p',associativity_for_addition) ).
cnf(c_5,plain,
add(A,add(B,C)) = add(add(A,B),C),
inference(clausify,[status(thm)],[associativity_for_addition]) ).
cnf(c_6,plain,
add(add(A,B),C) = add(A,add(B,C)),
inference(copy,[status(thm)],[c_5]) ).
fof(commutativity_for_addition,axiom,
! [VAR_0,VAR_1] : add(VAR_0,VAR_1) = add(VAR_1,VAR_0),
file('theBenchmark.p',commutativity_for_addition) ).
cnf(c_7,plain,
add(A,B) = add(B,A),
inference(clausify,[status(thm)],[commutativity_for_addition]) ).
fof(associativity_for_multiplication,axiom,
! [VAR_0,VAR_1,VAR_2] : multiply(VAR_0,multiply(VAR_1,VAR_2)) = multiply(multiply(VAR_0,VAR_1),VAR_2),
file('theBenchmark.p',associativity_for_multiplication) ).
cnf(c_8,plain,
multiply(A,multiply(B,C)) = multiply(multiply(A,B),C),
inference(clausify,[status(thm)],[associativity_for_multiplication]) ).
cnf(c_9,plain,
multiply(multiply(A,B),C) = multiply(A,multiply(B,C)),
inference(copy,[status(thm)],[c_8]) ).
fof(distribute1,axiom,
! [VAR_0,VAR_1,VAR_2] : multiply(VAR_0,add(VAR_1,VAR_2)) = add(multiply(VAR_0,VAR_1),multiply(VAR_0,VAR_2)),
file('theBenchmark.p',distribute1) ).
cnf(c_10,plain,
multiply(A,add(B,C)) = add(multiply(A,B),multiply(A,C)),
inference(clausify,[status(thm)],[distribute1]) ).
cnf(c_11,plain,
add(multiply(A,B),multiply(A,C)) = multiply(A,add(B,C)),
inference(copy,[status(thm)],[c_10]) ).
fof(distribute2,axiom,
! [VAR_0,VAR_1,VAR_2] : multiply(add(VAR_0,VAR_1),VAR_2) = add(multiply(VAR_0,VAR_2),multiply(VAR_1,VAR_2)),
file('theBenchmark.p',distribute2) ).
cnf(c_12,plain,
multiply(add(A,B),C) = add(multiply(A,C),multiply(B,C)),
inference(clausify,[status(thm)],[distribute2]) ).
cnf(c_13,plain,
add(multiply(A,B),multiply(C,B)) = multiply(add(A,C),B),
inference(copy,[status(thm)],[c_12]) ).
fof(x_cubed_is_x,axiom,
! [VAR_0] : multiply(VAR_0,multiply(VAR_0,VAR_0)) = VAR_0,
file('theBenchmark.p',x_cubed_is_x) ).
cnf(c_14,plain,
multiply(A,multiply(A,A)) = A,
inference(clausify,[status(thm)],[x_cubed_is_x]) ).
fof(a_times_b_is_c,axiom,
multiply(a,b) = c,
file('theBenchmark.p',a_times_b_is_c) ).
cnf(c_15,plain,
multiply(a,b) = c,
inference(clausify,[status(thm)],[a_times_b_is_c]) ).
cnf(c_16,plain,
c = multiply(a,b),
inference(copy,[status(thm)],[c_15]) ).
fof(prove_commutativity,axiom,
multiply(b,a) != c,
file('theBenchmark.p',prove_commutativity) ).
cnf(c_17,plain,
multiply(b,a) != c,
inference(clausify,[status(thm)],[prove_commutativity]) ).
cnf(c_18,plain,
multiply(b,a) != multiply(a,b),
inference(paramod,[status(thm)],[c_16,c_17]) ).
cnf(c_9516,plain,
add(additive_identity,A) = add(B,add(additive_inverse(B),A)),
inference(paramod,[status(thm)],[c_4,c_6]) ).
cnf(c_9517,plain,
A = add(B,add(additive_inverse(B),A)),
inference(paramod,[status(thm)],[c_1,c_9516]) ).
cnf(c_21,plain,
add(A,add(additive_inverse(A),B)) = B,
inference(copy,[status(thm)],[c_9517]) ).
cnf(c_9518,plain,
add(add(A,B),additive_inverse(B)) = add(A,additive_identity),
inference(paramod,[status(thm)],[c_4,c_6]) ).
cnf(c_9519,plain,
add(additive_inverse(B),add(A,B)) = add(A,additive_identity),
inference(paramod,[status(thm)],[c_7,c_9518]) ).
cnf(c_22,plain,
add(additive_inverse(A),add(B,A)) = B,
inference(paramod,[status(thm)],[c_2,c_9519]) ).
cnf(c_9520,plain,
add(add(A,B),C) = add(B,add(A,C)),
inference(paramod,[status(thm)],[c_7,c_6]) ).
cnf(c_23,plain,
add(A,add(B,C)) = add(B,add(A,C)),
inference(paramod,[status(thm)],[c_6,c_9520]) ).
cnf(c_9521,plain,
add(multiply(add(A,B),C),D) = add(multiply(A,C),add(multiply(B,C),D)),
inference(paramod,[status(thm)],[c_13,c_6]) ).
cnf(c_25,plain,
add(multiply(A,B),add(multiply(C,B),D)) = add(multiply(add(A,C),B),D),
inference(copy,[status(thm)],[c_9521]) ).
cnf(c_26,plain,
add(multiply(A,multiply(B,C)),multiply(D,C)) = multiply(add(multiply(A,B),D),C),
inference(paramod,[status(thm)],[c_9,c_13]) ).
cnf(c_27,plain,
add(multiply(A,B),multiply(C,multiply(D,B))) = multiply(add(A,multiply(C,D)),B),
inference(paramod,[status(thm)],[c_9,c_13]) ).
cnf(c_9522,plain,
multiply(A,B) = multiply(A,multiply(B,multiply(multiply(A,B),multiply(A,B)))),
inference(paramod,[status(thm)],[c_14,c_9]) ).
cnf(c_9523,plain,
multiply(A,B) = multiply(A,multiply(B,multiply(A,multiply(B,multiply(A,B))))),
inference(paramod,[status(thm)],[c_9,c_9522]) ).
cnf(c_30,plain,
multiply(A,multiply(B,multiply(A,multiply(B,multiply(A,B))))) = multiply(A,B),
inference(copy,[status(thm)],[c_9523]) ).
cnf(c_9524,plain,
add(A,multiply(A,B)) = multiply(A,add(multiply(A,A),B)),
inference(paramod,[status(thm)],[c_14,c_11]) ).
cnf(c_31,plain,
multiply(A,add(multiply(A,A),B)) = add(A,multiply(A,B)),
inference(copy,[status(thm)],[c_9524]) ).
cnf(c_9525,plain,
add(A,multiply(B,multiply(A,A))) = multiply(add(A,B),multiply(A,A)),
inference(paramod,[status(thm)],[c_14,c_13]) ).
cnf(c_33,plain,
multiply(add(A,B),multiply(A,A)) = add(A,multiply(B,multiply(A,A))),
inference(copy,[status(thm)],[c_9525]) ).
cnf(c_9526,plain,
add(A,additive_identity) = additive_inverse(additive_inverse(A)),
inference(paramod,[status(thm)],[c_4,c_21]) ).
cnf(c_9527,plain,
A = additive_inverse(additive_inverse(A)),
inference(paramod,[status(thm)],[c_2,c_9526]) ).
cnf(c_38,plain,
additive_inverse(additive_inverse(A)) = A,
inference(copy,[status(thm)],[c_9527]) ).
cnf(c_9528,plain,
add(add(A,B),add(additive_inverse(B),C)) = add(A,C),
inference(paramod,[status(thm)],[c_21,c_6]) ).
cnf(c_9529,plain,
add(additive_inverse(B),add(add(A,B),C)) = add(A,C),
inference(paramod,[status(thm)],[c_23,c_9528]) ).
cnf(c_39,plain,
add(additive_inverse(A),add(B,add(A,C))) = add(B,C),
inference(paramod,[status(thm)],[c_6,c_9529]) ).
cnf(c_40,plain,
add(A,add(B,additive_inverse(A))) = B,
inference(paramod,[status(thm)],[c_7,c_21]) ).
cnf(c_43,plain,
add(additive_inverse(multiply(A,B)),multiply(A,add(C,B))) = multiply(A,C),
inference(paramod,[status(thm)],[c_11,c_22]) ).
cnf(c_9530,plain,
add(additive_inverse(add(A,B)),A) = additive_inverse(B),
inference(paramod,[status(thm)],[c_22,c_22]) ).
cnf(c_46,plain,
add(A,additive_inverse(add(A,B))) = additive_inverse(B),
inference(paramod,[status(thm)],[c_7,c_9530]) ).
cnf(c_56,plain,
add(multiply(A,B),additive_inverse(multiply(A,add(B,C)))) = additive_inverse(multiply(A,C)),
inference(paramod,[status(thm)],[c_11,c_46]) ).
cnf(c_9531,plain,
add(A,multiply(B,add(C,D))) = add(multiply(B,C),add(A,multiply(B,D))),
inference(paramod,[status(thm)],[c_11,c_23]) ).
cnf(c_60,plain,
add(multiply(A,B),add(C,multiply(A,D))) = add(C,multiply(A,add(B,D))),
inference(copy,[status(thm)],[c_9531]) ).
cnf(c_9532,plain,
add(multiply(add(A,B),C),additive_inverse(multiply(A,C))) = multiply(B,C),
inference(paramod,[status(thm)],[c_25,c_40]) ).
cnf(c_124,plain,
add(additive_inverse(multiply(A,B)),multiply(add(A,C),B)) = multiply(C,B),
inference(paramod,[status(thm)],[c_7,c_9532]) ).
cnf(c_9533,plain,
add(A,multiply(B,A)) = multiply(add(multiply(A,A),B),A),
inference(paramod,[status(thm)],[c_14,c_26]) ).
cnf(c_141,plain,
multiply(add(multiply(A,A),B),A) = add(A,multiply(B,A)),
inference(copy,[status(thm)],[c_9533]) ).
cnf(c_9534,plain,
multiply(A,multiply(A,A)) = add(A,multiply(A,additive_identity)),
inference(paramod,[status(thm)],[c_2,c_31]) ).
cnf(c_9535,plain,
A = add(A,multiply(A,additive_identity)),
inference(paramod,[status(thm)],[c_14,c_9534]) ).
cnf(c_172,plain,
add(A,multiply(A,additive_identity)) = A,
inference(copy,[status(thm)],[c_9535]) ).
cnf(c_9536,plain,
multiply(A,additive_identity) = add(A,multiply(A,additive_inverse(multiply(A,A)))),
inference(paramod,[status(thm)],[c_4,c_31]) ).
cnf(c_173,plain,
add(A,multiply(A,additive_inverse(multiply(A,A)))) = multiply(A,additive_identity),
inference(copy,[status(thm)],[c_9536]) ).
cnf(c_9537,plain,
additive_identity = multiply(additive_identity,additive_identity),
inference(paramod,[status(thm)],[c_172,c_1]) ).
cnf(c_197,plain,
multiply(additive_identity,additive_identity) = additive_identity,
inference(copy,[status(thm)],[c_9537]) ).
cnf(c_9538,plain,
add(additive_inverse(A),add(B,A)) = add(B,multiply(A,additive_identity)),
inference(paramod,[status(thm)],[c_172,c_39]) ).
cnf(c_9539,plain,
B = add(B,multiply(A,additive_identity)),
inference(paramod,[status(thm)],[c_22,c_9538]) ).
cnf(c_205,plain,
add(A,multiply(B,additive_identity)) = A,
inference(copy,[status(thm)],[c_9539]) ).
cnf(c_9540,plain,
add(additive_identity,multiply(A,additive_identity)) = multiply(add(additive_identity,A),additive_identity),
inference(paramod,[status(thm)],[c_197,c_13]) ).
cnf(c_9541,plain,
additive_identity = multiply(add(additive_identity,A),additive_identity),
inference(paramod,[status(thm)],[c_205,c_9540]) ).
cnf(c_9542,plain,
additive_identity = multiply(A,additive_identity),
inference(paramod,[status(thm)],[c_1,c_9541]) ).
cnf(c_209,plain,
multiply(A,additive_identity) = additive_identity,
inference(copy,[status(thm)],[c_9542]) ).
cnf(c_210,plain,
add(A,multiply(A,additive_inverse(multiply(A,A)))) = additive_identity,
inference(paramod,[status(thm)],[c_209,c_173]) ).
cnf(c_212,plain,
add(multiply(A,B),multiply(C,multiply(D,multiply(E,B)))) = multiply(add(A,multiply(C,multiply(D,E))),B),
inference(paramod,[status(thm)],[c_9,c_27]) ).
cnf(c_9543,plain,
multiply(additive_identity,A) = multiply(B,multiply(additive_identity,A)),
inference(paramod,[status(thm)],[c_209,c_9]) ).
cnf(c_249,plain,
multiply(A,multiply(additive_identity,B)) = multiply(additive_identity,B),
inference(copy,[status(thm)],[c_9543]) ).
cnf(c_9544,plain,
add(multiply(A,B),multiply(multiply(A,additive_inverse(multiply(A,A))),B)) = multiply(additive_identity,B),
inference(paramod,[status(thm)],[c_210,c_13]) ).
cnf(c_9545,plain,
add(multiply(A,B),multiply(A,multiply(additive_inverse(multiply(A,A)),B))) = multiply(additive_identity,B),
inference(paramod,[status(thm)],[c_9,c_9544]) ).
cnf(c_255,plain,
multiply(A,add(B,multiply(additive_inverse(multiply(A,A)),B))) = multiply(additive_identity,B),
inference(paramod,[status(thm)],[c_11,c_9545]) ).
cnf(c_9546,plain,
multiply(A,multiply(A,A)) = add(A,multiply(additive_identity,multiply(A,A))),
inference(paramod,[status(thm)],[c_2,c_33]) ).
cnf(c_9547,plain,
A = add(A,multiply(additive_identity,multiply(A,A))),
inference(paramod,[status(thm)],[c_14,c_9546]) ).
cnf(c_316,plain,
add(A,multiply(additive_identity,multiply(A,A))) = A,
inference(copy,[status(thm)],[c_9547]) ).
cnf(c_9548,plain,
add(A,additive_inverse(A)) = multiply(additive_identity,multiply(additive_inverse(A),additive_inverse(A))),
inference(paramod,[status(thm)],[c_316,c_21]) ).
cnf(c_9549,plain,
additive_identity = multiply(additive_identity,multiply(additive_inverse(A),additive_inverse(A))),
inference(paramod,[status(thm)],[c_4,c_9548]) ).
cnf(c_361,plain,
multiply(additive_identity,multiply(additive_inverse(A),additive_inverse(A))) = additive_identity,
inference(copy,[status(thm)],[c_9549]) ).
cnf(c_9550,plain,
multiply(additive_identity,multiply(A,additive_inverse(additive_inverse(A)))) = additive_identity,
inference(paramod,[status(thm)],[c_38,c_361]) ).
cnf(c_373,plain,
multiply(additive_identity,multiply(A,A)) = additive_identity,
inference(paramod,[status(thm)],[c_38,c_9550]) ).
cnf(c_9551,plain,
multiply(additive_identity,multiply(additive_identity,A)) = additive_identity,
inference(paramod,[status(thm)],[c_249,c_373]) ).
cnf(c_383,plain,
multiply(additive_identity,A) = additive_identity,
inference(paramod,[status(thm)],[c_249,c_9551]) ).
cnf(c_385,plain,
multiply(A,add(B,multiply(additive_inverse(multiply(A,A)),B))) = additive_identity,
inference(paramod,[status(thm)],[c_383,c_255]) ).
cnf(c_9552,plain,
add(additive_inverse(multiply(A,add(B,C))),multiply(A,B)) = multiply(A,additive_inverse(C)),
inference(paramod,[status(thm)],[c_22,c_43]) ).
cnf(c_9553,plain,
add(multiply(A,B),additive_inverse(multiply(A,add(B,C)))) = multiply(A,additive_inverse(C)),
inference(paramod,[status(thm)],[c_7,c_9552]) ).
cnf(c_423,plain,
additive_inverse(multiply(A,B)) = multiply(A,additive_inverse(B)),
inference(paramod,[status(thm)],[c_56,c_9553]) ).
cnf(c_9554,plain,
multiply(A,add(B,multiply(multiply(A,additive_inverse(A)),B))) = additive_identity,
inference(paramod,[status(thm)],[c_423,c_385]) ).
cnf(c_439,plain,
multiply(A,add(B,multiply(A,multiply(additive_inverse(A),B)))) = additive_identity,
inference(paramod,[status(thm)],[c_9,c_9554]) ).
cnf(c_459,plain,
add(multiply(A,additive_inverse(B)),multiply(add(A,C),B)) = multiply(C,B),
inference(paramod,[status(thm)],[c_423,c_124]) ).
cnf(c_9555,plain,
multiply(additive_identity,A) = multiply(B,multiply(add(C,multiply(B,multiply(additive_inverse(B),C))),A)),
inference(paramod,[status(thm)],[c_439,c_9]) ).
cnf(c_9556,plain,
additive_identity = multiply(B,multiply(add(C,multiply(B,multiply(additive_inverse(B),C))),A)),
inference(paramod,[status(thm)],[c_383,c_9555]) ).
cnf(c_524,plain,
multiply(A,multiply(add(B,multiply(A,multiply(additive_inverse(A),B))),C)) = additive_identity,
inference(copy,[status(thm)],[c_9556]) ).
cnf(c_9557,plain,
multiply(A,add(add(B,multiply(additive_inverse(A),multiply(additive_inverse(additive_inverse(A)),B))),multiply(A,additive_identity))) = additive_identity,
inference(paramod,[status(thm)],[c_439,c_439]) ).
cnf(c_9558,plain,
multiply(A,add(add(B,multiply(additive_inverse(A),multiply(A,B))),multiply(A,additive_identity))) = additive_identity,
inference(paramod,[status(thm)],[c_38,c_9557]) ).
cnf(c_9559,plain,
multiply(A,add(add(B,multiply(additive_inverse(A),multiply(A,B))),additive_identity)) = additive_identity,
inference(paramod,[status(thm)],[c_209,c_9558]) ).
cnf(c_9560,plain,
multiply(A,add(additive_identity,add(B,multiply(additive_inverse(A),multiply(A,B))))) = additive_identity,
inference(paramod,[status(thm)],[c_7,c_9559]) ).
cnf(c_543,plain,
multiply(A,add(B,multiply(additive_inverse(A),multiply(A,B)))) = additive_identity,
inference(paramod,[status(thm)],[c_1,c_9560]) ).
cnf(c_592,plain,
multiply(additive_inverse(A),add(B,multiply(A,multiply(additive_inverse(A),B)))) = additive_identity,
inference(paramod,[status(thm)],[c_38,c_543]) ).
cnf(c_9561,plain,
multiply(additive_inverse(A),add(multiply(B,multiply(additive_inverse(A),multiply(B,multiply(additive_inverse(A),B)))),multiply(A,multiply(additive_inverse(A),B)))) = additive_identity,
inference(paramod,[status(thm)],[c_30,c_592]) ).
cnf(c_9562,plain,
multiply(additive_inverse(A),add(multiply(A,multiply(additive_inverse(A),B)),multiply(B,multiply(additive_inverse(A),multiply(B,multiply(additive_inverse(A),B)))))) = additive_identity,
inference(paramod,[status(thm)],[c_7,c_9561]) ).
cnf(c_878,plain,
multiply(additive_inverse(A),multiply(add(A,multiply(B,multiply(additive_inverse(A),B))),multiply(additive_inverse(A),B))) = additive_identity,
inference(paramod,[status(thm)],[c_212,c_9562]) ).
cnf(c_9563,plain,
add(multiply(A,additive_inverse(B)),multiply(additive_identity,B)) = multiply(additive_inverse(A),B),
inference(paramod,[status(thm)],[c_4,c_459]) ).
cnf(c_9564,plain,
add(multiply(A,additive_inverse(B)),additive_identity) = multiply(additive_inverse(A),B),
inference(paramod,[status(thm)],[c_383,c_9563]) ).
cnf(c_9565,plain,
add(additive_identity,multiply(A,additive_inverse(B))) = multiply(additive_inverse(A),B),
inference(paramod,[status(thm)],[c_7,c_9564]) ).
cnf(c_9566,plain,
multiply(A,additive_inverse(B)) = multiply(additive_inverse(A),B),
inference(paramod,[status(thm)],[c_1,c_9565]) ).
cnf(c_940,plain,
multiply(additive_inverse(A),B) = multiply(A,additive_inverse(B)),
inference(copy,[status(thm)],[c_9566]) ).
cnf(c_9567,plain,
multiply(additive_inverse(A),multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),multiply(additive_inverse(A),B))) = additive_identity,
inference(paramod,[status(thm)],[c_940,c_878]) ).
cnf(c_9568,plain,
multiply(additive_inverse(A),multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),multiply(A,additive_inverse(B)))) = additive_identity,
inference(paramod,[status(thm)],[c_940,c_9567]) ).
cnf(c_9569,plain,
multiply(A,additive_inverse(multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),multiply(A,additive_inverse(B))))) = additive_identity,
inference(paramod,[status(thm)],[c_940,c_9568]) ).
cnf(c_9570,plain,
multiply(A,multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),additive_inverse(multiply(A,additive_inverse(B))))) = additive_identity,
inference(paramod,[status(thm)],[c_423,c_9569]) ).
cnf(c_9571,plain,
multiply(A,multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),multiply(A,additive_inverse(additive_inverse(B))))) = additive_identity,
inference(paramod,[status(thm)],[c_423,c_9570]) ).
cnf(c_1011,plain,
multiply(A,multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),multiply(A,B))) = additive_identity,
inference(paramod,[status(thm)],[c_38,c_9571]) ).
cnf(c_1045,plain,
multiply(A,multiply(add(B,multiply(A,multiply(A,additive_inverse(B)))),C)) = additive_identity,
inference(paramod,[status(thm)],[c_940,c_524]) ).
cnf(c_9572,plain,
multiply(add(A,multiply(B,multiply(B,additive_inverse(A)))),multiply(B,multiply(add(A,multiply(B,multiply(B,additive_inverse(A)))),additive_identity))) = multiply(add(A,multiply(B,multiply(B,additive_inverse(A)))),B),
inference(paramod,[status(thm)],[c_1045,c_30]) ).
cnf(c_9573,plain,
multiply(add(A,multiply(B,multiply(B,additive_inverse(A)))),multiply(B,additive_identity)) = multiply(add(A,multiply(B,multiply(B,additive_inverse(A)))),B),
inference(paramod,[status(thm)],[c_209,c_9572]) ).
cnf(c_9574,plain,
multiply(add(A,multiply(B,multiply(B,additive_inverse(A)))),additive_identity) = multiply(add(A,multiply(B,multiply(B,additive_inverse(A)))),B),
inference(paramod,[status(thm)],[c_209,c_9573]) ).
cnf(c_9575,plain,
additive_identity = multiply(add(A,multiply(B,multiply(B,additive_inverse(A)))),B),
inference(paramod,[status(thm)],[c_209,c_9574]) ).
cnf(c_1083,plain,
multiply(add(A,multiply(B,multiply(B,additive_inverse(A)))),B) = additive_identity,
inference(copy,[status(thm)],[c_9575]) ).
cnf(c_9576,plain,
add(multiply(A,B),multiply(multiply(B,multiply(B,additive_inverse(A))),B)) = additive_identity,
inference(paramod,[status(thm)],[c_1083,c_13]) ).
cnf(c_9577,plain,
add(multiply(A,B),multiply(B,multiply(multiply(B,additive_inverse(A)),B))) = additive_identity,
inference(paramod,[status(thm)],[c_9,c_9576]) ).
cnf(c_9578,plain,
add(multiply(A,B),multiply(B,multiply(B,multiply(additive_inverse(A),B)))) = additive_identity,
inference(paramod,[status(thm)],[c_9,c_9577]) ).
cnf(c_1312,plain,
add(multiply(A,B),multiply(B,multiply(B,multiply(A,additive_inverse(B))))) = additive_identity,
inference(paramod,[status(thm)],[c_940,c_9578]) ).
cnf(c_9579,plain,
add(additive_inverse(multiply(A,multiply(A,multiply(B,additive_inverse(A))))),additive_identity) = multiply(B,A),
inference(paramod,[status(thm)],[c_1312,c_22]) ).
cnf(c_9580,plain,
add(multiply(A,additive_inverse(multiply(A,multiply(B,additive_inverse(A))))),additive_identity) = multiply(B,A),
inference(paramod,[status(thm)],[c_423,c_9579]) ).
cnf(c_9581,plain,
add(multiply(A,multiply(A,additive_inverse(multiply(B,additive_inverse(A))))),additive_identity) = multiply(B,A),
inference(paramod,[status(thm)],[c_423,c_9580]) ).
cnf(c_9582,plain,
add(multiply(A,multiply(A,multiply(B,additive_inverse(additive_inverse(A))))),additive_identity) = multiply(B,A),
inference(paramod,[status(thm)],[c_423,c_9581]) ).
cnf(c_9583,plain,
add(multiply(A,multiply(A,multiply(B,A))),additive_identity) = multiply(B,A),
inference(paramod,[status(thm)],[c_38,c_9582]) ).
cnf(c_9584,plain,
add(additive_identity,multiply(A,multiply(A,multiply(B,A)))) = multiply(B,A),
inference(paramod,[status(thm)],[c_7,c_9583]) ).
cnf(c_1847,plain,
multiply(A,multiply(A,multiply(B,A))) = multiply(B,A),
inference(paramod,[status(thm)],[c_1,c_9584]) ).
cnf(c_9585,plain,
multiply(multiply(A,B),C) = multiply(B,multiply(multiply(B,multiply(A,B)),C)),
inference(paramod,[status(thm)],[c_1847,c_9]) ).
cnf(c_9586,plain,
multiply(A,multiply(B,C)) = multiply(B,multiply(multiply(B,multiply(A,B)),C)),
inference(paramod,[status(thm)],[c_9,c_9585]) ).
cnf(c_9587,plain,
multiply(A,multiply(B,C)) = multiply(B,multiply(B,multiply(multiply(A,B),C))),
inference(paramod,[status(thm)],[c_9,c_9586]) ).
cnf(c_9588,plain,
multiply(A,multiply(B,C)) = multiply(B,multiply(B,multiply(A,multiply(B,C)))),
inference(paramod,[status(thm)],[c_9,c_9587]) ).
cnf(c_1883,plain,
multiply(A,multiply(A,multiply(B,multiply(A,C)))) = multiply(B,multiply(A,C)),
inference(copy,[status(thm)],[c_9588]) ).
cnf(c_9589,plain,
additive_inverse(multiply(A,B)) = multiply(B,additive_inverse(multiply(B,multiply(A,B)))),
inference(paramod,[status(thm)],[c_1847,c_423]) ).
cnf(c_9590,plain,
multiply(A,additive_inverse(B)) = multiply(B,additive_inverse(multiply(B,multiply(A,B)))),
inference(paramod,[status(thm)],[c_423,c_9589]) ).
cnf(c_9591,plain,
multiply(A,additive_inverse(B)) = multiply(B,multiply(B,additive_inverse(multiply(A,B)))),
inference(paramod,[status(thm)],[c_423,c_9590]) ).
cnf(c_9592,plain,
multiply(A,additive_inverse(B)) = multiply(B,multiply(B,multiply(A,additive_inverse(B)))),
inference(paramod,[status(thm)],[c_423,c_9591]) ).
cnf(c_1903,plain,
multiply(A,multiply(A,multiply(B,additive_inverse(A)))) = multiply(B,additive_inverse(A)),
inference(copy,[status(thm)],[c_9592]) ).
cnf(c_9593,plain,
add(multiply(A,B),multiply(C,additive_inverse(A))) = multiply(A,add(B,multiply(A,multiply(C,additive_inverse(A))))),
inference(paramod,[status(thm)],[c_1903,c_11]) ).
cnf(c_1953,plain,
multiply(A,add(B,multiply(A,multiply(C,additive_inverse(A))))) = add(multiply(A,B),multiply(C,additive_inverse(A))),
inference(copy,[status(thm)],[c_9593]) ).
cnf(c_9594,plain,
multiply(A,multiply(A,B)) = multiply(B,multiply(A,multiply(B,multiply(A,B)))),
inference(paramod,[status(thm)],[c_30,c_1883]) ).
cnf(c_4831,plain,
multiply(A,multiply(B,multiply(A,multiply(B,A)))) = multiply(B,multiply(B,A)),
inference(copy,[status(thm)],[c_9594]) ).
cnf(c_9595,plain,
multiply(A,multiply(multiply(B,C),multiply(A,multiply(B,multiply(C,A))))) = multiply(multiply(B,C),multiply(multiply(B,C),A)),
inference(paramod,[status(thm)],[c_9,c_4831]) ).
cnf(c_9596,plain,
multiply(A,multiply(B,multiply(C,multiply(A,multiply(B,multiply(C,A)))))) = multiply(multiply(B,C),multiply(multiply(B,C),A)),
inference(paramod,[status(thm)],[c_9,c_9595]) ).
cnf(c_9597,plain,
multiply(A,multiply(B,multiply(C,multiply(A,multiply(B,multiply(C,A)))))) = multiply(multiply(B,C),multiply(B,multiply(C,A))),
inference(paramod,[status(thm)],[c_9,c_9596]) ).
cnf(c_6671,plain,
multiply(A,multiply(B,multiply(C,multiply(A,multiply(B,multiply(C,A)))))) = multiply(B,multiply(C,multiply(B,multiply(C,A)))),
inference(paramod,[status(thm)],[c_9,c_9597]) ).
cnf(c_9598,plain,
add(additive_identity,multiply(A,multiply(add(B,multiply(C,multiply(B,additive_inverse(C)))),multiply(B,C)))) = multiply(add(B,A),multiply(add(B,multiply(C,multiply(B,additive_inverse(C)))),multiply(B,C))),
inference(paramod,[status(thm)],[c_1011,c_13]) ).
cnf(c_9599,plain,
multiply(A,multiply(add(B,multiply(C,multiply(B,additive_inverse(C)))),multiply(B,C))) = multiply(add(B,A),multiply(add(B,multiply(C,multiply(B,additive_inverse(C)))),multiply(B,C))),
inference(paramod,[status(thm)],[c_1,c_9598]) ).
cnf(c_8601,plain,
multiply(add(A,B),multiply(add(A,multiply(C,multiply(A,additive_inverse(C)))),multiply(A,C))) = multiply(B,multiply(add(A,multiply(C,multiply(A,additive_inverse(C)))),multiply(A,C))),
inference(copy,[status(thm)],[c_9599]) ).
cnf(c_9600,plain,
multiply(add(multiply(multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),multiply(A,B)),multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),multiply(A,B))),A),multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),multiply(A,B))) = add(multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),multiply(A,B)),additive_identity),
inference(paramod,[status(thm)],[c_1011,c_141]) ).
cnf(c_9601,plain,
multiply(add(multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),multiply(multiply(A,B),multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),multiply(A,B)))),A),multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),multiply(A,B))) = add(multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),multiply(A,B)),additive_identity),
inference(paramod,[status(thm)],[c_9,c_9600]) ).
cnf(c_9602,plain,
multiply(add(multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),multiply(A,multiply(B,multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),multiply(A,B))))),A),multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),multiply(A,B))) = add(multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),multiply(A,B)),additive_identity),
inference(paramod,[status(thm)],[c_9,c_9601]) ).
cnf(c_9603,plain,
multiply(add(A,multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),multiply(A,multiply(B,multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),multiply(A,B)))))),multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),multiply(A,B))) = add(multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),multiply(A,B)),additive_identity),
inference(paramod,[status(thm)],[c_7,c_9602]) ).
cnf(c_9604,plain,
multiply(multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),multiply(A,multiply(B,multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),multiply(A,B))))),multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),multiply(A,B))) = add(multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),multiply(A,B)),additive_identity),
inference(paramod,[status(thm)],[c_8601,c_9603]) ).
cnf(c_9605,plain,
multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),multiply(multiply(A,multiply(B,multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),multiply(A,B)))),multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),multiply(A,B)))) = add(multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),multiply(A,B)),additive_identity),
inference(paramod,[status(thm)],[c_9,c_9604]) ).
cnf(c_9606,plain,
multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),multiply(A,multiply(multiply(B,multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),multiply(A,B))),multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),multiply(A,B))))) = add(multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),multiply(A,B)),additive_identity),
inference(paramod,[status(thm)],[c_9,c_9605]) ).
cnf(c_9607,plain,
multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),multiply(A,multiply(B,multiply(multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),multiply(A,B)),multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),multiply(A,B)))))) = add(multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),multiply(A,B)),additive_identity),
inference(paramod,[status(thm)],[c_9,c_9606]) ).
cnf(c_9608,plain,
multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),multiply(A,multiply(B,multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),multiply(multiply(A,B),multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),multiply(A,B))))))) = add(multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),multiply(A,B)),additive_identity),
inference(paramod,[status(thm)],[c_9,c_9607]) ).
cnf(c_9609,plain,
multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),multiply(A,multiply(B,multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),multiply(A,multiply(B,multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),multiply(A,B)))))))) = add(multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),multiply(A,B)),additive_identity),
inference(paramod,[status(thm)],[c_9,c_9608]) ).
cnf(c_9610,plain,
multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),multiply(A,multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),multiply(A,multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),multiply(A,B)))))) = add(multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),multiply(A,B)),additive_identity),
inference(paramod,[status(thm)],[c_6671,c_9609]) ).
cnf(c_9611,plain,
multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),multiply(A,multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),additive_identity))) = add(multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),multiply(A,B)),additive_identity),
inference(paramod,[status(thm)],[c_1011,c_9610]) ).
cnf(c_9612,plain,
multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),multiply(A,additive_identity)) = add(multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),multiply(A,B)),additive_identity),
inference(paramod,[status(thm)],[c_209,c_9611]) ).
cnf(c_9613,plain,
multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),additive_identity) = add(multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),multiply(A,B)),additive_identity),
inference(paramod,[status(thm)],[c_209,c_9612]) ).
cnf(c_9614,plain,
additive_identity = add(multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),multiply(A,B)),additive_identity),
inference(paramod,[status(thm)],[c_209,c_9613]) ).
cnf(c_9615,plain,
additive_identity = add(additive_identity,multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),multiply(A,B))),
inference(paramod,[status(thm)],[c_7,c_9614]) ).
cnf(c_9616,plain,
additive_identity = multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),multiply(A,B)),
inference(paramod,[status(thm)],[c_1,c_9615]) ).
cnf(c_8618,plain,
multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),multiply(A,B)) = additive_identity,
inference(copy,[status(thm)],[c_9616]) ).
cnf(c_9617,plain,
add(multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),C),additive_identity) = multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),add(C,multiply(A,B))),
inference(paramod,[status(thm)],[c_8618,c_11]) ).
cnf(c_9618,plain,
add(additive_identity,multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),C)) = multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),add(C,multiply(A,B))),
inference(paramod,[status(thm)],[c_7,c_9617]) ).
cnf(c_9619,plain,
multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),C) = multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),add(C,multiply(A,B))),
inference(paramod,[status(thm)],[c_1,c_9618]) ).
cnf(c_8720,plain,
multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),add(C,multiply(A,B))) = multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),C),
inference(copy,[status(thm)],[c_9619]) ).
cnf(c_9620,plain,
multiply(add(add(multiply(additive_inverse(A),additive_inverse(A)),B),multiply(A,add(additive_inverse(A),multiply(B,additive_inverse(A))))),multiply(add(multiply(additive_inverse(A),additive_inverse(A)),B),A)) = additive_identity,
inference(paramod,[status(thm)],[c_141,c_8618]) ).
cnf(c_9621,plain,
multiply(add(add(multiply(A,additive_inverse(additive_inverse(A))),B),multiply(A,add(additive_inverse(A),multiply(B,additive_inverse(A))))),multiply(add(multiply(additive_inverse(A),additive_inverse(A)),B),A)) = additive_identity,
inference(paramod,[status(thm)],[c_940,c_9620]) ).
cnf(c_9622,plain,
multiply(add(add(multiply(A,A),B),multiply(A,add(additive_inverse(A),multiply(B,additive_inverse(A))))),multiply(add(multiply(additive_inverse(A),additive_inverse(A)),B),A)) = additive_identity,
inference(paramod,[status(thm)],[c_38,c_9621]) ).
cnf(c_9623,plain,
multiply(add(multiply(A,A),add(B,multiply(A,add(additive_inverse(A),multiply(B,additive_inverse(A)))))),multiply(add(multiply(additive_inverse(A),additive_inverse(A)),B),A)) = additive_identity,
inference(paramod,[status(thm)],[c_6,c_9622]) ).
cnf(c_9624,plain,
multiply(add(B,multiply(A,add(A,add(additive_inverse(A),multiply(B,additive_inverse(A)))))),multiply(add(multiply(additive_inverse(A),additive_inverse(A)),B),A)) = additive_identity,
inference(paramod,[status(thm)],[c_60,c_9623]) ).
cnf(c_9625,plain,
multiply(add(B,multiply(A,multiply(B,additive_inverse(A)))),multiply(add(multiply(additive_inverse(A),additive_inverse(A)),B),A)) = additive_identity,
inference(paramod,[status(thm)],[c_21,c_9624]) ).
cnf(c_9626,plain,
multiply(add(B,multiply(A,multiply(B,additive_inverse(A)))),multiply(add(multiply(A,additive_inverse(additive_inverse(A))),B),A)) = additive_identity,
inference(paramod,[status(thm)],[c_940,c_9625]) ).
cnf(c_9627,plain,
multiply(add(B,multiply(A,multiply(B,additive_inverse(A)))),multiply(add(multiply(A,A),B),A)) = additive_identity,
inference(paramod,[status(thm)],[c_38,c_9626]) ).
cnf(c_9628,plain,
multiply(add(B,multiply(A,multiply(B,additive_inverse(A)))),add(A,multiply(B,A))) = additive_identity,
inference(paramod,[status(thm)],[c_141,c_9627]) ).
cnf(c_8740,plain,
multiply(add(A,multiply(B,multiply(A,additive_inverse(B)))),B) = additive_identity,
inference(paramod,[status(thm)],[c_8720,c_9628]) ).
cnf(c_9629,plain,
multiply(add(A,multiply(add(B,multiply(additive_inverse(A),multiply(B,additive_inverse(additive_inverse(A))))),additive_identity)),add(B,multiply(additive_inverse(A),multiply(B,additive_inverse(additive_inverse(A)))))) = additive_identity,
inference(paramod,[status(thm)],[c_8740,c_1083]) ).
cnf(c_9630,plain,
multiply(add(A,multiply(add(B,multiply(additive_inverse(A),multiply(B,A))),additive_identity)),add(B,multiply(additive_inverse(A),multiply(B,additive_inverse(additive_inverse(A)))))) = additive_identity,
inference(paramod,[status(thm)],[c_38,c_9629]) ).
cnf(c_9631,plain,
multiply(add(A,multiply(add(B,multiply(A,additive_inverse(multiply(B,A)))),additive_identity)),add(B,multiply(additive_inverse(A),multiply(B,additive_inverse(additive_inverse(A)))))) = additive_identity,
inference(paramod,[status(thm)],[c_940,c_9630]) ).
cnf(c_9632,plain,
multiply(add(A,multiply(add(B,multiply(A,multiply(B,additive_inverse(A)))),additive_identity)),add(B,multiply(additive_inverse(A),multiply(B,additive_inverse(additive_inverse(A)))))) = additive_identity,
inference(paramod,[status(thm)],[c_423,c_9631]) ).
cnf(c_9633,plain,
multiply(add(A,additive_identity),add(B,multiply(additive_inverse(A),multiply(B,additive_inverse(additive_inverse(A)))))) = additive_identity,
inference(paramod,[status(thm)],[c_209,c_9632]) ).
cnf(c_9634,plain,
multiply(A,add(B,multiply(additive_inverse(A),multiply(B,additive_inverse(additive_inverse(A)))))) = additive_identity,
inference(paramod,[status(thm)],[c_2,c_9633]) ).
cnf(c_9635,plain,
multiply(A,add(B,multiply(additive_inverse(A),multiply(B,A)))) = additive_identity,
inference(paramod,[status(thm)],[c_38,c_9634]) ).
cnf(c_9636,plain,
multiply(A,add(B,multiply(A,additive_inverse(multiply(B,A))))) = additive_identity,
inference(paramod,[status(thm)],[c_940,c_9635]) ).
cnf(c_9637,plain,
multiply(A,add(B,multiply(A,multiply(B,additive_inverse(A))))) = additive_identity,
inference(paramod,[status(thm)],[c_423,c_9636]) ).
cnf(c_8856,plain,
add(multiply(A,B),multiply(B,additive_inverse(A))) = additive_identity,
inference(paramod,[status(thm)],[c_1953,c_9637]) ).
cnf(c_9638,plain,
add(additive_inverse(multiply(A,additive_inverse(B))),additive_identity) = multiply(B,A),
inference(paramod,[status(thm)],[c_8856,c_22]) ).
cnf(c_9639,plain,
add(multiply(A,additive_inverse(additive_inverse(B))),additive_identity) = multiply(B,A),
inference(paramod,[status(thm)],[c_423,c_9638]) ).
cnf(c_9640,plain,
add(multiply(A,B),additive_identity) = multiply(B,A),
inference(paramod,[status(thm)],[c_38,c_9639]) ).
cnf(c_9641,plain,
add(additive_identity,multiply(A,B)) = multiply(B,A),
inference(paramod,[status(thm)],[c_7,c_9640]) ).
cnf(c_9514,plain,
multiply(A,B) = multiply(B,A),
inference(paramod,[status(thm)],[c_1,c_9641]) ).
cnf(c_9515,plain,
$false,
inference(resolve,[status(thm)],[c_9514,c_18]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : RNG009-7 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.37 % Computer : n011.cluster.edu
% 0.08/0.37 % Model : x86_64 x86_64
% 0.08/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.37 % Memory : 8046.5625MB
% 0.08/0.37 % OS : Linux 6.8.0-71-generic
% 0.08/0.37 % CPULimit : 300
% 0.08/0.37 % WCLimit : 300
% 0.08/0.37 % DateTime : Sat Sep 26 05:45:00 UTC 2026
% 0.08/0.37 % CPUTime :
% 0.08/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.37 % Process 3914646 was started by sandbox on n011,
% 0.08/0.37 % Sat Sep 26 05:45:00 2026
% 0.08/0.37 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.08/0.37
% 0.08/0.37 % From the command line: assign(max_seconds, 300).
% 104.29/24.68
% 104.29/24.68 % Assigning unary symbol additive_inverse kb_weight 0 and highest precedence (8).
% 104.29/24.68
% 104.29/24.68 % SZS status Unsatisfiable for theBenchmark
% 104.29/24.68
% 104.29/24.68 % Proof 1 at 2.82 (+ 0.47) seconds.
% 104.29/24.68 % Length of proof is 74.
% 104.29/24.68 % Level of proof is 23.
% 104.29/24.68 % Maximum clause weight is 31.000.
% 104.29/24.68 % Given clauses 166.
% 104.29/24.68
% 104.29/24.68 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------