%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : RNG029-3 : TPTP v9.3.1. Bugfixed v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n007.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:26 AM UTC 2026
% Result : Unsatisfiable 57.76s 7.77s
% Output : CNFRefutation 57.76s
% Verified :
% SZS Type : Refutation
% Derivation depth : 43
% Number of leaves : 19
% Syntax : Number of formulae : 156 ( 146 unt; 0 def)
% Number of atoms : 166 ( 165 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 45 ( 35 ~; 10 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 4 con; 0-3 aty)
% Number of variables : 357 ( 1 sgn 41 !; 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_multiplicative_zero,axiom,
! [VAR_0] : multiply(VAR_0,additive_identity) = additive_identity,
file('theBenchmark.p',right_multiplicative_zero) ).
cnf(c_3,plain,
multiply(A,additive_identity) = additive_identity,
inference(clausify,[status(thm)],[right_multiplicative_zero]) ).
fof(add_inverse,axiom,
! [VAR_0] : add(additive_inverse(VAR_0),VAR_0) = additive_identity,
file('theBenchmark.p',add_inverse) ).
cnf(c_4,plain,
add(additive_inverse(A),A) = additive_identity,
inference(clausify,[status(thm)],[add_inverse]) ).
fof(sum_of_inverses,axiom,
! [VAR_0,VAR_1] : additive_inverse(add(VAR_0,VAR_1)) = add(additive_inverse(VAR_0),additive_inverse(VAR_1)),
file('theBenchmark.p',sum_of_inverses) ).
cnf(c_5,plain,
additive_inverse(add(A,B)) = add(additive_inverse(A),additive_inverse(B)),
inference(clausify,[status(thm)],[sum_of_inverses]) ).
fof(additive_inverse_additive_inverse,axiom,
! [VAR_0] : additive_inverse(additive_inverse(VAR_0)) = VAR_0,
file('theBenchmark.p',additive_inverse_additive_inverse) ).
cnf(c_6,plain,
additive_inverse(additive_inverse(A)) = A,
inference(clausify,[status(thm)],[additive_inverse_additive_inverse]) ).
fof(multiply_over_add1,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',multiply_over_add1) ).
cnf(c_7,plain,
multiply(A,add(B,C)) = add(multiply(A,B),multiply(A,C)),
inference(clausify,[status(thm)],[multiply_over_add1]) ).
cnf(c_8,plain,
add(multiply(A,B),multiply(A,C)) = multiply(A,add(B,C)),
inference(copy,[status(thm)],[c_7]) ).
fof(right_alternative,axiom,
! [VAR_0,VAR_1] : multiply(multiply(VAR_0,VAR_1),VAR_1) = multiply(VAR_0,multiply(VAR_1,VAR_1)),
file('theBenchmark.p',right_alternative) ).
cnf(c_11,plain,
multiply(multiply(A,B),B) = multiply(A,multiply(B,B)),
inference(clausify,[status(thm)],[right_alternative]) ).
fof(inverse_product1,axiom,
! [VAR_0,VAR_1] : multiply(additive_inverse(VAR_0),VAR_1) = additive_inverse(multiply(VAR_0,VAR_1)),
file('theBenchmark.p',inverse_product1) ).
cnf(c_13,plain,
multiply(additive_inverse(A),B) = additive_inverse(multiply(A,B)),
inference(clausify,[status(thm)],[inverse_product1]) ).
cnf(c_14,plain,
additive_inverse(multiply(A,B)) = multiply(additive_inverse(A),B),
inference(copy,[status(thm)],[c_13]) ).
fof(inverse_product2,axiom,
! [VAR_0,VAR_1] : multiply(VAR_0,additive_inverse(VAR_1)) = additive_inverse(multiply(VAR_0,VAR_1)),
file('theBenchmark.p',inverse_product2) ).
cnf(c_15,plain,
multiply(A,additive_inverse(B)) = additive_inverse(multiply(A,B)),
inference(clausify,[status(thm)],[inverse_product2]) ).
cnf(c_11625,plain,
multiply(A,additive_inverse(B)) = multiply(additive_inverse(A),B),
inference(paramod,[status(thm)],[c_14,c_15]) ).
cnf(c_16,plain,
multiply(additive_inverse(A),B) = multiply(A,additive_inverse(B)),
inference(copy,[status(thm)],[c_11625]) ).
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_18,plain,
add(A,B) = add(B,A),
inference(clausify,[status(thm)],[commutativity_for_addition]) ).
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_19,plain,
add(A,add(B,C)) = add(add(A,B),C),
inference(clausify,[status(thm)],[associativity_for_addition]) ).
cnf(c_20,plain,
add(add(A,B),C) = add(A,add(B,C)),
inference(copy,[status(thm)],[c_19]) ).
fof(left_cancellation_for_addition,axiom,
! [VAR_0,VAR_1,VAR_2] :
( VAR_0 = VAR_2
| add(VAR_0,VAR_1) != add(VAR_2,VAR_1) ),
file('theBenchmark.p',left_cancellation_for_addition) ).
cnf(c_21,plain,
( A = C
| add(A,B) != add(C,B) ),
inference(clausify,[status(thm)],[left_cancellation_for_addition]) ).
fof(right_cancellation_for_addition,axiom,
! [VAR_0,VAR_1,VAR_2] :
( VAR_1 = VAR_2
| add(VAR_0,VAR_1) != add(VAR_0,VAR_2) ),
file('theBenchmark.p',right_cancellation_for_addition) ).
cnf(c_22,plain,
( B = C
| add(A,B) != add(A,C) ),
inference(clausify,[status(thm)],[right_cancellation_for_addition]) ).
fof(right_moufang,axiom,
! [VAR_0,VAR_1,VAR_2] : multiply(VAR_0,multiply(VAR_1,multiply(VAR_2,VAR_1))) = multiply(multiply(multiply(VAR_0,VAR_1),VAR_2),VAR_1),
file('theBenchmark.p',right_moufang) ).
cnf(c_23,plain,
multiply(A,multiply(B,multiply(C,B))) = multiply(multiply(multiply(A,B),C),B),
inference(clausify,[status(thm)],[right_moufang]) ).
cnf(c_24,plain,
multiply(multiply(multiply(A,B),C),B) = multiply(A,multiply(B,multiply(C,B))),
inference(copy,[status(thm)],[c_23]) ).
fof(left_moufang,axiom,
! [VAR_0,VAR_1,VAR_2] : multiply(multiply(VAR_0,multiply(VAR_1,VAR_0)),VAR_2) = multiply(VAR_0,multiply(VAR_1,multiply(VAR_0,VAR_2))),
file('theBenchmark.p',left_moufang) ).
cnf(c_25,plain,
multiply(multiply(A,multiply(B,A)),C) = multiply(A,multiply(B,multiply(A,C))),
inference(clausify,[status(thm)],[left_moufang]) ).
fof(associator,axiom,
! [VAR_0,VAR_1,VAR_2] : associator(VAR_0,VAR_1,VAR_2) = add(multiply(multiply(VAR_0,VAR_1),VAR_2),additive_inverse(multiply(VAR_0,multiply(VAR_1,VAR_2)))),
file('theBenchmark.p',associator) ).
cnf(c_26,plain,
associator(A,B,C) = add(multiply(multiply(A,B),C),additive_inverse(multiply(A,multiply(B,C)))),
inference(clausify,[status(thm)],[associator]) ).
cnf(c_11626,plain,
associator(A,B,C) = add(multiply(multiply(A,B),C),multiply(additive_inverse(A),multiply(B,C))),
inference(paramod,[status(thm)],[c_14,c_26]) ).
cnf(c_11627,plain,
associator(A,B,C) = add(multiply(multiply(A,B),C),multiply(A,additive_inverse(multiply(B,C)))),
inference(paramod,[status(thm)],[c_16,c_11626]) ).
cnf(c_11628,plain,
associator(A,B,C) = add(multiply(multiply(A,B),C),multiply(A,multiply(additive_inverse(B),C))),
inference(paramod,[status(thm)],[c_14,c_11627]) ).
cnf(c_11629,plain,
associator(A,B,C) = add(multiply(multiply(A,B),C),multiply(A,multiply(B,additive_inverse(C)))),
inference(paramod,[status(thm)],[c_16,c_11628]) ).
cnf(c_27,plain,
associator(A,B,C) = add(multiply(A,multiply(B,additive_inverse(C))),multiply(multiply(A,B),C)),
inference(paramod,[status(thm)],[c_18,c_11629]) ).
fof(associator_skew_symmetry1,axiom,
! [VAR_0,VAR_1,VAR_2] : associator(VAR_0,VAR_1,VAR_2) = additive_inverse(associator(VAR_1,VAR_0,VAR_2)),
file('theBenchmark.p',associator_skew_symmetry1) ).
cnf(c_29,plain,
associator(A,B,C) = additive_inverse(associator(B,A,C)),
inference(clausify,[status(thm)],[associator_skew_symmetry1]) ).
cnf(c_11630,plain,
add(multiply(A,multiply(B,additive_inverse(C))),multiply(multiply(A,B),C)) = additive_inverse(associator(B,A,C)),
inference(paramod,[status(thm)],[c_27,c_29]) ).
cnf(c_11631,plain,
add(multiply(A,multiply(B,additive_inverse(C))),multiply(multiply(A,B),C)) = additive_inverse(add(multiply(B,multiply(A,additive_inverse(C))),multiply(multiply(B,A),C))),
inference(paramod,[status(thm)],[c_27,c_11630]) ).
cnf(c_11632,plain,
add(multiply(A,multiply(B,additive_inverse(C))),multiply(multiply(A,B),C)) = add(additive_inverse(multiply(B,multiply(A,additive_inverse(C)))),additive_inverse(multiply(multiply(B,A),C))),
inference(paramod,[status(thm)],[c_5,c_11631]) ).
cnf(c_11633,plain,
add(multiply(A,multiply(B,additive_inverse(C))),multiply(multiply(A,B),C)) = add(multiply(additive_inverse(B),multiply(A,additive_inverse(C))),additive_inverse(multiply(multiply(B,A),C))),
inference(paramod,[status(thm)],[c_14,c_11632]) ).
cnf(c_11634,plain,
add(multiply(A,multiply(B,additive_inverse(C))),multiply(multiply(A,B),C)) = add(multiply(B,additive_inverse(multiply(A,additive_inverse(C)))),additive_inverse(multiply(multiply(B,A),C))),
inference(paramod,[status(thm)],[c_16,c_11633]) ).
cnf(c_11635,plain,
add(multiply(A,multiply(B,additive_inverse(C))),multiply(multiply(A,B),C)) = add(multiply(B,multiply(additive_inverse(A),additive_inverse(C))),additive_inverse(multiply(multiply(B,A),C))),
inference(paramod,[status(thm)],[c_14,c_11634]) ).
cnf(c_11636,plain,
add(multiply(A,multiply(B,additive_inverse(C))),multiply(multiply(A,B),C)) = add(multiply(B,multiply(A,additive_inverse(additive_inverse(C)))),additive_inverse(multiply(multiply(B,A),C))),
inference(paramod,[status(thm)],[c_16,c_11635]) ).
cnf(c_11637,plain,
add(multiply(A,multiply(B,additive_inverse(C))),multiply(multiply(A,B),C)) = add(multiply(B,multiply(A,C)),additive_inverse(multiply(multiply(B,A),C))),
inference(paramod,[status(thm)],[c_6,c_11636]) ).
cnf(c_11638,plain,
add(multiply(A,multiply(B,additive_inverse(C))),multiply(multiply(A,B),C)) = add(multiply(B,multiply(A,C)),multiply(additive_inverse(multiply(B,A)),C)),
inference(paramod,[status(thm)],[c_14,c_11637]) ).
cnf(c_11639,plain,
add(multiply(A,multiply(B,additive_inverse(C))),multiply(multiply(A,B),C)) = add(multiply(B,multiply(A,C)),multiply(multiply(additive_inverse(B),A),C)),
inference(paramod,[status(thm)],[c_14,c_11638]) ).
cnf(c_30,plain,
add(multiply(A,multiply(B,additive_inverse(C))),multiply(multiply(A,B),C)) = add(multiply(B,multiply(A,C)),multiply(multiply(B,additive_inverse(A)),C)),
inference(paramod,[status(thm)],[c_16,c_11639]) ).
fof(associator_skew_symmetry2,axiom,
! [VAR_0,VAR_1,VAR_2] : associator(VAR_0,VAR_1,VAR_2) = additive_inverse(associator(VAR_2,VAR_1,VAR_0)),
file('theBenchmark.p',associator_skew_symmetry2) ).
cnf(c_31,plain,
associator(A,B,C) = additive_inverse(associator(C,B,A)),
inference(clausify,[status(thm)],[associator_skew_symmetry2]) ).
cnf(c_11640,plain,
add(multiply(A,multiply(B,additive_inverse(C))),multiply(multiply(A,B),C)) = additive_inverse(associator(C,B,A)),
inference(paramod,[status(thm)],[c_27,c_31]) ).
cnf(c_11641,plain,
add(multiply(A,multiply(B,additive_inverse(C))),multiply(multiply(A,B),C)) = additive_inverse(add(multiply(C,multiply(B,additive_inverse(A))),multiply(multiply(C,B),A))),
inference(paramod,[status(thm)],[c_27,c_11640]) ).
cnf(c_11642,plain,
add(multiply(A,multiply(B,additive_inverse(C))),multiply(multiply(A,B),C)) = add(additive_inverse(multiply(C,multiply(B,additive_inverse(A)))),additive_inverse(multiply(multiply(C,B),A))),
inference(paramod,[status(thm)],[c_5,c_11641]) ).
cnf(c_11643,plain,
add(multiply(A,multiply(B,additive_inverse(C))),multiply(multiply(A,B),C)) = add(multiply(additive_inverse(C),multiply(B,additive_inverse(A))),additive_inverse(multiply(multiply(C,B),A))),
inference(paramod,[status(thm)],[c_14,c_11642]) ).
cnf(c_11644,plain,
add(multiply(A,multiply(B,additive_inverse(C))),multiply(multiply(A,B),C)) = add(multiply(C,additive_inverse(multiply(B,additive_inverse(A)))),additive_inverse(multiply(multiply(C,B),A))),
inference(paramod,[status(thm)],[c_16,c_11643]) ).
cnf(c_11645,plain,
add(multiply(A,multiply(B,additive_inverse(C))),multiply(multiply(A,B),C)) = add(multiply(C,multiply(additive_inverse(B),additive_inverse(A))),additive_inverse(multiply(multiply(C,B),A))),
inference(paramod,[status(thm)],[c_14,c_11644]) ).
cnf(c_11646,plain,
add(multiply(A,multiply(B,additive_inverse(C))),multiply(multiply(A,B),C)) = add(multiply(C,multiply(B,additive_inverse(additive_inverse(A)))),additive_inverse(multiply(multiply(C,B),A))),
inference(paramod,[status(thm)],[c_16,c_11645]) ).
cnf(c_11647,plain,
add(multiply(A,multiply(B,additive_inverse(C))),multiply(multiply(A,B),C)) = add(multiply(C,multiply(B,A)),additive_inverse(multiply(multiply(C,B),A))),
inference(paramod,[status(thm)],[c_6,c_11646]) ).
cnf(c_11648,plain,
add(multiply(A,multiply(B,additive_inverse(C))),multiply(multiply(A,B),C)) = add(multiply(C,multiply(B,A)),multiply(additive_inverse(multiply(C,B)),A)),
inference(paramod,[status(thm)],[c_14,c_11647]) ).
cnf(c_11649,plain,
add(multiply(A,multiply(B,additive_inverse(C))),multiply(multiply(A,B),C)) = add(multiply(C,multiply(B,A)),multiply(multiply(additive_inverse(C),B),A)),
inference(paramod,[status(thm)],[c_14,c_11648]) ).
cnf(c_32,plain,
add(multiply(A,multiply(B,additive_inverse(C))),multiply(multiply(A,B),C)) = add(multiply(C,multiply(B,A)),multiply(multiply(C,additive_inverse(B)),A)),
inference(paramod,[status(thm)],[c_16,c_11649]) ).
fof(prove_middle_law,axiom,
multiply(multiply(cx,cy),multiply(cz,cx)) != multiply(cx,multiply(multiply(cy,cz),cx)),
file('theBenchmark.p',prove_middle_law) ).
cnf(c_33,plain,
multiply(multiply(cx,cy),multiply(cz,cx)) != multiply(cx,multiply(multiply(cy,cz),cx)),
inference(clausify,[status(thm)],[prove_middle_law]) ).
cnf(c_34,plain,
additive_inverse(multiply(A,B)) = multiply(A,additive_inverse(B)),
inference(paramod,[status(thm)],[c_16,c_14]) ).
cnf(c_35,plain,
add(A,additive_inverse(A)) = additive_identity,
inference(paramod,[status(thm)],[c_18,c_4]) ).
cnf(c_53,plain,
add(A,additive_identity) = A,
inference(paramod,[status(thm)],[c_18,c_1]) ).
cnf(c_59,plain,
( multiply(A,B) = D
| multiply(A,add(B,C)) != add(D,multiply(A,C)) ),
inference(paramod,[status(thm)],[c_8,c_21]) ).
cnf(c_11650,plain,
multiply(additive_inverse(multiply(A,multiply(B,A))),C) = multiply(A,multiply(B,multiply(A,additive_inverse(C)))),
inference(paramod,[status(thm)],[c_25,c_16]) ).
cnf(c_11651,plain,
multiply(multiply(A,additive_inverse(multiply(B,A))),C) = multiply(A,multiply(B,multiply(A,additive_inverse(C)))),
inference(paramod,[status(thm)],[c_34,c_11650]) ).
cnf(c_88,plain,
multiply(multiply(A,multiply(B,additive_inverse(A))),C) = multiply(A,multiply(B,multiply(A,additive_inverse(C)))),
inference(paramod,[status(thm)],[c_34,c_11651]) ).
cnf(c_11652,plain,
add(multiply(A,multiply(multiply(B,additive_inverse(A)),additive_inverse(C))),multiply(multiply(A,multiply(B,additive_inverse(A))),C)) = add(multiply(multiply(B,additive_inverse(A)),multiply(A,C)),multiply(multiply(B,multiply(additive_inverse(A),additive_inverse(A))),C)),
inference(paramod,[status(thm)],[c_11,c_30]) ).
cnf(c_11653,plain,
add(multiply(A,multiply(multiply(B,additive_inverse(A)),additive_inverse(C))),multiply(A,multiply(B,multiply(A,additive_inverse(C))))) = add(multiply(multiply(B,additive_inverse(A)),multiply(A,C)),multiply(multiply(B,multiply(additive_inverse(A),additive_inverse(A))),C)),
inference(paramod,[status(thm)],[c_88,c_11652]) ).
cnf(c_11654,plain,
add(multiply(A,multiply(B,multiply(A,additive_inverse(C)))),multiply(A,multiply(multiply(B,additive_inverse(A)),additive_inverse(C)))) = add(multiply(multiply(B,additive_inverse(A)),multiply(A,C)),multiply(multiply(B,multiply(additive_inverse(A),additive_inverse(A))),C)),
inference(paramod,[status(thm)],[c_18,c_11653]) ).
cnf(c_11655,plain,
multiply(A,add(multiply(B,multiply(A,additive_inverse(C))),multiply(multiply(B,additive_inverse(A)),additive_inverse(C)))) = add(multiply(multiply(B,additive_inverse(A)),multiply(A,C)),multiply(multiply(B,multiply(additive_inverse(A),additive_inverse(A))),C)),
inference(paramod,[status(thm)],[c_8,c_11654]) ).
cnf(c_11656,plain,
multiply(A,add(multiply(B,multiply(A,additive_inverse(C))),multiply(multiply(B,additive_inverse(A)),additive_inverse(C)))) = add(multiply(multiply(B,additive_inverse(A)),multiply(A,C)),multiply(multiply(B,multiply(A,additive_inverse(additive_inverse(A)))),C)),
inference(paramod,[status(thm)],[c_16,c_11655]) ).
cnf(c_11657,plain,
multiply(A,add(multiply(B,multiply(A,additive_inverse(C))),multiply(multiply(B,additive_inverse(A)),additive_inverse(C)))) = add(multiply(multiply(B,additive_inverse(A)),multiply(A,C)),multiply(multiply(B,multiply(A,A)),C)),
inference(paramod,[status(thm)],[c_6,c_11656]) ).
cnf(c_110,plain,
add(multiply(multiply(A,additive_inverse(B)),multiply(B,C)),multiply(multiply(A,multiply(B,B)),C)) = multiply(B,add(multiply(A,multiply(B,additive_inverse(C))),multiply(multiply(A,additive_inverse(B)),additive_inverse(C)))),
inference(copy,[status(thm)],[c_11657]) ).
cnf(c_11658,plain,
add(multiply(A,multiply(B,C)),multiply(multiply(A,B),additive_inverse(C))) = add(multiply(additive_inverse(C),multiply(B,A)),multiply(multiply(additive_inverse(C),additive_inverse(B)),A)),
inference(paramod,[status(thm)],[c_6,c_32]) ).
cnf(c_11659,plain,
add(multiply(A,multiply(B,C)),multiply(multiply(A,B),additive_inverse(C))) = add(multiply(C,additive_inverse(multiply(B,A))),multiply(multiply(additive_inverse(C),additive_inverse(B)),A)),
inference(paramod,[status(thm)],[c_16,c_11658]) ).
cnf(c_11660,plain,
add(multiply(A,multiply(B,C)),multiply(multiply(A,B),additive_inverse(C))) = add(multiply(C,multiply(B,additive_inverse(A))),multiply(multiply(additive_inverse(C),additive_inverse(B)),A)),
inference(paramod,[status(thm)],[c_34,c_11659]) ).
cnf(c_11661,plain,
add(multiply(A,multiply(B,C)),multiply(multiply(A,B),additive_inverse(C))) = add(multiply(C,multiply(B,additive_inverse(A))),multiply(multiply(C,additive_inverse(additive_inverse(B))),A)),
inference(paramod,[status(thm)],[c_16,c_11660]) ).
cnf(c_11662,plain,
add(multiply(A,multiply(B,C)),multiply(multiply(A,B),additive_inverse(C))) = add(multiply(C,multiply(B,additive_inverse(A))),multiply(multiply(C,B),A)),
inference(paramod,[status(thm)],[c_6,c_11661]) ).
cnf(c_124,plain,
add(multiply(A,multiply(B,additive_inverse(C))),multiply(multiply(A,B),C)) = add(multiply(C,multiply(B,A)),multiply(multiply(C,B),additive_inverse(A))),
inference(copy,[status(thm)],[c_11662]) ).
cnf(c_11663,plain,
add(multiply(A,multiply(B,multiply(additive_inverse(C),additive_inverse(C)))),multiply(multiply(A,multiply(B,additive_inverse(C))),C)) = add(multiply(C,multiply(multiply(B,additive_inverse(C)),A)),multiply(multiply(C,additive_inverse(multiply(B,additive_inverse(C)))),A)),
inference(paramod,[status(thm)],[c_11,c_32]) ).
cnf(c_11664,plain,
add(multiply(A,multiply(B,multiply(C,additive_inverse(additive_inverse(C))))),multiply(multiply(A,multiply(B,additive_inverse(C))),C)) = add(multiply(C,multiply(multiply(B,additive_inverse(C)),A)),multiply(multiply(C,additive_inverse(multiply(B,additive_inverse(C)))),A)),
inference(paramod,[status(thm)],[c_16,c_11663]) ).
cnf(c_11665,plain,
add(multiply(A,multiply(B,multiply(C,C))),multiply(multiply(A,multiply(B,additive_inverse(C))),C)) = add(multiply(C,multiply(multiply(B,additive_inverse(C)),A)),multiply(multiply(C,additive_inverse(multiply(B,additive_inverse(C)))),A)),
inference(paramod,[status(thm)],[c_6,c_11664]) ).
cnf(c_11666,plain,
add(multiply(A,multiply(B,multiply(C,C))),multiply(multiply(A,multiply(B,additive_inverse(C))),C)) = add(multiply(C,multiply(multiply(B,additive_inverse(C)),A)),multiply(multiply(C,multiply(B,additive_inverse(additive_inverse(C)))),A)),
inference(paramod,[status(thm)],[c_34,c_11665]) ).
cnf(c_11667,plain,
add(multiply(A,multiply(B,multiply(C,C))),multiply(multiply(A,multiply(B,additive_inverse(C))),C)) = add(multiply(C,multiply(multiply(B,additive_inverse(C)),A)),multiply(multiply(C,multiply(B,C)),A)),
inference(paramod,[status(thm)],[c_6,c_11666]) ).
cnf(c_11668,plain,
add(multiply(A,multiply(B,multiply(C,C))),multiply(multiply(A,multiply(B,additive_inverse(C))),C)) = add(multiply(C,multiply(multiply(B,additive_inverse(C)),A)),multiply(C,multiply(B,multiply(C,A)))),
inference(paramod,[status(thm)],[c_25,c_11667]) ).
cnf(c_11669,plain,
add(multiply(A,multiply(B,multiply(C,C))),multiply(multiply(A,multiply(B,additive_inverse(C))),C)) = add(multiply(C,multiply(B,multiply(C,A))),multiply(C,multiply(multiply(B,additive_inverse(C)),A))),
inference(paramod,[status(thm)],[c_18,c_11668]) ).
cnf(c_127,plain,
add(multiply(A,multiply(B,multiply(C,C))),multiply(multiply(A,multiply(B,additive_inverse(C))),C)) = multiply(C,add(multiply(B,multiply(C,A)),multiply(multiply(B,additive_inverse(C)),A))),
inference(paramod,[status(thm)],[c_8,c_11669]) ).
cnf(c_11670,plain,
add(multiply(A,multiply(multiply(B,A),additive_inverse(C))),multiply(multiply(A,multiply(B,A)),C)) = add(multiply(C,multiply(B,multiply(A,A))),multiply(multiply(C,additive_inverse(multiply(B,A))),A)),
inference(paramod,[status(thm)],[c_11,c_32]) ).
cnf(c_11671,plain,
add(multiply(A,multiply(multiply(B,A),additive_inverse(C))),multiply(A,multiply(B,multiply(A,C)))) = add(multiply(C,multiply(B,multiply(A,A))),multiply(multiply(C,additive_inverse(multiply(B,A))),A)),
inference(paramod,[status(thm)],[c_25,c_11670]) ).
cnf(c_11672,plain,
add(multiply(A,multiply(B,multiply(A,C))),multiply(A,multiply(multiply(B,A),additive_inverse(C)))) = add(multiply(C,multiply(B,multiply(A,A))),multiply(multiply(C,additive_inverse(multiply(B,A))),A)),
inference(paramod,[status(thm)],[c_18,c_11671]) ).
cnf(c_11673,plain,
multiply(A,add(multiply(B,multiply(A,C)),multiply(multiply(B,A),additive_inverse(C)))) = add(multiply(C,multiply(B,multiply(A,A))),multiply(multiply(C,additive_inverse(multiply(B,A))),A)),
inference(paramod,[status(thm)],[c_8,c_11672]) ).
cnf(c_11674,plain,
multiply(A,add(multiply(B,multiply(A,C)),multiply(multiply(B,A),additive_inverse(C)))) = add(multiply(C,multiply(B,multiply(A,A))),multiply(multiply(C,multiply(B,additive_inverse(A))),A)),
inference(paramod,[status(thm)],[c_34,c_11673]) ).
cnf(c_11675,plain,
multiply(A,add(multiply(B,multiply(A,C)),multiply(multiply(B,A),additive_inverse(C)))) = multiply(A,add(multiply(B,multiply(A,C)),multiply(multiply(B,additive_inverse(A)),C))),
inference(paramod,[status(thm)],[c_127,c_11674]) ).
cnf(c_129,plain,
multiply(A,add(multiply(B,multiply(A,C)),multiply(multiply(B,additive_inverse(A)),C))) = multiply(A,add(multiply(B,multiply(A,C)),multiply(multiply(B,A),additive_inverse(C)))),
inference(copy,[status(thm)],[c_11675]) ).
cnf(c_11676,plain,
add(multiply(A,multiply(B,additive_inverse(multiply(C,additive_inverse(B))))),multiply(multiply(A,B),multiply(C,additive_inverse(B)))) = add(multiply(multiply(C,additive_inverse(B)),multiply(B,A)),multiply(multiply(C,multiply(additive_inverse(B),additive_inverse(B))),A)),
inference(paramod,[status(thm)],[c_11,c_32]) ).
cnf(c_11677,plain,
add(multiply(A,multiply(B,multiply(C,additive_inverse(additive_inverse(B))))),multiply(multiply(A,B),multiply(C,additive_inverse(B)))) = add(multiply(multiply(C,additive_inverse(B)),multiply(B,A)),multiply(multiply(C,multiply(additive_inverse(B),additive_inverse(B))),A)),
inference(paramod,[status(thm)],[c_34,c_11676]) ).
cnf(c_11678,plain,
add(multiply(A,multiply(B,multiply(C,B))),multiply(multiply(A,B),multiply(C,additive_inverse(B)))) = add(multiply(multiply(C,additive_inverse(B)),multiply(B,A)),multiply(multiply(C,multiply(additive_inverse(B),additive_inverse(B))),A)),
inference(paramod,[status(thm)],[c_6,c_11677]) ).
cnf(c_11679,plain,
add(multiply(A,multiply(B,multiply(C,B))),multiply(multiply(A,B),multiply(C,additive_inverse(B)))) = add(multiply(multiply(C,additive_inverse(B)),multiply(B,A)),multiply(multiply(C,multiply(B,additive_inverse(additive_inverse(B)))),A)),
inference(paramod,[status(thm)],[c_16,c_11678]) ).
cnf(c_11680,plain,
add(multiply(A,multiply(B,multiply(C,B))),multiply(multiply(A,B),multiply(C,additive_inverse(B)))) = add(multiply(multiply(C,additive_inverse(B)),multiply(B,A)),multiply(multiply(C,multiply(B,B)),A)),
inference(paramod,[status(thm)],[c_6,c_11679]) ).
cnf(c_11681,plain,
add(multiply(A,multiply(B,multiply(C,B))),multiply(multiply(A,B),multiply(C,additive_inverse(B)))) = multiply(B,add(multiply(C,multiply(B,additive_inverse(A))),multiply(multiply(C,additive_inverse(B)),additive_inverse(A)))),
inference(paramod,[status(thm)],[c_110,c_11680]) ).
cnf(c_11682,plain,
add(multiply(A,multiply(B,multiply(C,B))),multiply(multiply(A,B),multiply(C,additive_inverse(B)))) = multiply(B,add(multiply(C,multiply(B,additive_inverse(A))),multiply(multiply(C,B),additive_inverse(additive_inverse(A))))),
inference(paramod,[status(thm)],[c_129,c_11681]) ).
cnf(c_130,plain,
add(multiply(A,multiply(B,multiply(C,B))),multiply(multiply(A,B),multiply(C,additive_inverse(B)))) = multiply(B,add(multiply(C,multiply(B,additive_inverse(A))),multiply(multiply(C,B),A))),
inference(paramod,[status(thm)],[c_6,c_11682]) ).
cnf(c_11683,plain,
add(multiply(multiply(A,B),multiply(C,additive_inverse(B))),multiply(A,multiply(B,multiply(C,B)))) = add(multiply(B,multiply(C,multiply(A,B))),multiply(multiply(B,additive_inverse(C)),multiply(A,B))),
inference(paramod,[status(thm)],[c_24,c_32]) ).
cnf(c_11684,plain,
add(multiply(A,multiply(B,multiply(C,B))),multiply(multiply(A,B),multiply(C,additive_inverse(B)))) = add(multiply(B,multiply(C,multiply(A,B))),multiply(multiply(B,additive_inverse(C)),multiply(A,B))),
inference(paramod,[status(thm)],[c_18,c_11683]) ).
cnf(c_11685,plain,
multiply(B,add(multiply(C,multiply(B,additive_inverse(A))),multiply(multiply(C,B),A))) = add(multiply(B,multiply(C,multiply(A,B))),multiply(multiply(B,additive_inverse(C)),multiply(A,B))),
inference(paramod,[status(thm)],[c_130,c_11684]) ).
cnf(c_139,plain,
add(multiply(A,multiply(B,multiply(C,A))),multiply(multiply(A,additive_inverse(B)),multiply(C,A))) = multiply(A,add(multiply(B,multiply(A,additive_inverse(C))),multiply(multiply(B,A),C))),
inference(copy,[status(thm)],[c_11685]) ).
cnf(c_145,plain,
add(multiply(A,multiply(B,additive_inverse(C))),multiply(multiply(A,B),C)) = add(multiply(C,multiply(A,additive_inverse(B))),multiply(multiply(C,A),B)),
inference(paramod,[status(thm)],[c_32,c_30]) ).
cnf(c_148,plain,
add(A,multiply(multiply(cx,cy),multiply(cz,cx))) != add(A,multiply(cx,multiply(multiply(cy,cz),cx))),
inference(resolve,[status(thm)],[c_22,c_33]) ).
cnf(c_151,plain,
multiply(multiply(A,additive_inverse(B)),C) = multiply(multiply(A,B),additive_inverse(C)),
inference(paramod,[status(thm)],[c_34,c_16]) ).
cnf(c_11686,plain,
add(multiply(A,multiply(B,multiply(C,A))),multiply(multiply(A,B),additive_inverse(multiply(C,A)))) = multiply(A,add(multiply(B,multiply(A,additive_inverse(C))),multiply(multiply(B,A),C))),
inference(paramod,[status(thm)],[c_151,c_139]) ).
cnf(c_157,plain,
add(multiply(A,multiply(B,multiply(C,A))),multiply(multiply(A,B),multiply(C,additive_inverse(A)))) = multiply(A,add(multiply(B,multiply(A,additive_inverse(C))),multiply(multiply(B,A),C))),
inference(paramod,[status(thm)],[c_34,c_11686]) ).
cnf(c_11687,plain,
add(add(A,B),additive_inverse(B)) = add(A,additive_identity),
inference(paramod,[status(thm)],[c_35,c_20]) ).
cnf(c_11688,plain,
add(additive_inverse(B),add(A,B)) = add(A,additive_identity),
inference(paramod,[status(thm)],[c_18,c_11687]) ).
cnf(c_182,plain,
add(additive_inverse(A),add(B,A)) = B,
inference(paramod,[status(thm)],[c_53,c_11688]) ).
cnf(c_241,plain,
add(multiply(cx,A),multiply(multiply(cx,cy),multiply(cz,cx))) != multiply(cx,add(A,multiply(multiply(cy,cz),cx))),
inference(paramod,[status(thm)],[c_8,c_148]) ).
cnf(c_252,plain,
add(multiply(cx,A),multiply(multiply(cx,cy),multiply(cz,cx))) != multiply(cx,add(multiply(multiply(cy,cz),cx),A)),
inference(paramod,[status(thm)],[c_18,c_241]) ).
cnf(c_11689,plain,
( additive_identity = B
| A != add(A,B) ),
inference(paramod,[status(thm)],[c_53,c_22]) ).
cnf(c_264,plain,
( additive_identity = B
| add(A,B) != A ),
inference(copy,[status(thm)],[c_11689]) ).
cnf(c_11690,plain,
add(multiply(cx,additive_inverse(multiply(multiply(cy,cz),cx))),multiply(multiply(cx,cy),multiply(cz,cx))) != multiply(cx,additive_identity),
inference(paramod,[status(thm)],[c_35,c_252]) ).
cnf(c_11691,plain,
add(multiply(cx,multiply(multiply(cy,cz),additive_inverse(cx))),multiply(multiply(cx,cy),multiply(cz,cx))) != multiply(cx,additive_identity),
inference(paramod,[status(thm)],[c_34,c_11690]) ).
cnf(c_308,plain,
add(multiply(cx,multiply(multiply(cy,cz),additive_inverse(cx))),multiply(multiply(cx,cy),multiply(cz,cx))) != additive_identity,
inference(paramod,[status(thm)],[c_3,c_11691]) ).
cnf(c_11692,plain,
( additive_identity = add(A,B)
| A != additive_inverse(B) ),
inference(paramod,[status(thm)],[c_182,c_264]) ).
cnf(c_11693,plain,
( additive_identity = add(A,B)
| additive_inverse(B) != A ),
inference(copy,[status(thm)],[c_11692]) ).
cnf(c_600,plain,
( add(B,A) = additive_identity
| additive_inverse(A) != B ),
inference(copy,[status(thm)],[c_11693]) ).
cnf(c_11694,plain,
additive_inverse(multiply(multiply(cx,cy),multiply(cz,cx))) != multiply(cx,multiply(multiply(cy,cz),additive_inverse(cx))),
inference(resolve,[status(thm)],[c_600,c_308]) ).
cnf(c_11695,plain,
multiply(multiply(cx,cy),additive_inverse(multiply(cz,cx))) != multiply(cx,multiply(multiply(cy,cz),additive_inverse(cx))),
inference(paramod,[status(thm)],[c_34,c_11694]) ).
cnf(c_616,plain,
multiply(multiply(cx,cy),multiply(cz,additive_inverse(cx))) != multiply(cx,multiply(multiply(cy,cz),additive_inverse(cx))),
inference(paramod,[status(thm)],[c_34,c_11695]) ).
cnf(c_11696,plain,
multiply(cx,multiply(multiply(cy,cz),additive_inverse(cx))) != multiply(multiply(cx,cy),multiply(cz,additive_inverse(cx))),
inference(copy,[status(thm)],[c_616]) ).
cnf(c_11697,plain,
multiply(cx,add(multiply(multiply(cy,cz),additive_inverse(cx)),A)) != add(multiply(multiply(cx,cy),multiply(cz,additive_inverse(cx))),multiply(cx,A)),
inference(resolve,[status(thm)],[c_59,c_11696]) ).
cnf(c_1298,plain,
add(multiply(multiply(cx,cy),multiply(cz,additive_inverse(cx))),multiply(cx,A)) != multiply(cx,add(multiply(multiply(cy,cz),additive_inverse(cx)),A)),
inference(copy,[status(thm)],[c_11697]) ).
cnf(c_1448,plain,
add(multiply(multiply(cx,cy),multiply(cz,additive_inverse(cx))),multiply(cx,A)) != multiply(cx,add(A,multiply(multiply(cy,cz),additive_inverse(cx)))),
inference(paramod,[status(thm)],[c_18,c_1298]) ).
cnf(c_11698,plain,
add(multiply(multiply(cx,cy),multiply(cz,additive_inverse(cx))),multiply(cx,multiply(cy,multiply(cz,additive_inverse(additive_inverse(cx)))))) != multiply(cx,add(multiply(additive_inverse(cx),multiply(cz,cy)),multiply(multiply(additive_inverse(cx),cz),additive_inverse(cy)))),
inference(paramod,[status(thm)],[c_124,c_1448]) ).
cnf(c_11699,plain,
add(multiply(multiply(cx,cy),multiply(cz,additive_inverse(cx))),multiply(cx,multiply(cy,multiply(cz,cx)))) != multiply(cx,add(multiply(additive_inverse(cx),multiply(cz,cy)),multiply(multiply(additive_inverse(cx),cz),additive_inverse(cy)))),
inference(paramod,[status(thm)],[c_6,c_11698]) ).
cnf(c_11700,plain,
add(multiply(cx,multiply(cy,multiply(cz,cx))),multiply(multiply(cx,cy),multiply(cz,additive_inverse(cx)))) != multiply(cx,add(multiply(additive_inverse(cx),multiply(cz,cy)),multiply(multiply(additive_inverse(cx),cz),additive_inverse(cy)))),
inference(paramod,[status(thm)],[c_18,c_11699]) ).
cnf(c_11701,plain,
multiply(cx,add(multiply(cy,multiply(cx,additive_inverse(cz))),multiply(multiply(cy,cx),cz))) != multiply(cx,add(multiply(additive_inverse(cx),multiply(cz,cy)),multiply(multiply(additive_inverse(cx),cz),additive_inverse(cy)))),
inference(paramod,[status(thm)],[c_157,c_11700]) ).
cnf(c_11702,plain,
multiply(cx,add(multiply(cy,multiply(cx,additive_inverse(cz))),multiply(multiply(cy,cx),cz))) != multiply(cx,add(multiply(cx,additive_inverse(multiply(cz,cy))),multiply(multiply(additive_inverse(cx),cz),additive_inverse(cy)))),
inference(paramod,[status(thm)],[c_16,c_11701]) ).
cnf(c_11703,plain,
multiply(cx,add(multiply(cy,multiply(cx,additive_inverse(cz))),multiply(multiply(cy,cx),cz))) != multiply(cx,add(multiply(cx,multiply(cz,additive_inverse(cy))),multiply(multiply(additive_inverse(cx),cz),additive_inverse(cy)))),
inference(paramod,[status(thm)],[c_34,c_11702]) ).
cnf(c_11704,plain,
multiply(cx,add(multiply(cy,multiply(cx,additive_inverse(cz))),multiply(multiply(cy,cx),cz))) != multiply(cx,add(multiply(cx,multiply(cz,additive_inverse(cy))),multiply(multiply(cx,additive_inverse(cz)),additive_inverse(cy)))),
inference(paramod,[status(thm)],[c_16,c_11703]) ).
cnf(c_11705,plain,
multiply(cx,add(multiply(cy,multiply(cx,additive_inverse(cz))),multiply(multiply(cy,cx),cz))) != multiply(cx,add(multiply(cx,multiply(cz,additive_inverse(cy))),multiply(multiply(cx,cz),additive_inverse(additive_inverse(cy))))),
inference(paramod,[status(thm)],[c_151,c_11704]) ).
cnf(c_10724,plain,
multiply(cx,add(multiply(cy,multiply(cx,additive_inverse(cz))),multiply(multiply(cy,cx),cz))) != multiply(cx,add(multiply(cx,multiply(cz,additive_inverse(cy))),multiply(multiply(cx,cz),cy))),
inference(paramod,[status(thm)],[c_6,c_11705]) ).
cnf(c_11706,plain,
add(multiply(A,multiply(B,multiply(C,additive_inverse(D)))),multiply(A,multiply(multiply(B,C),D))) = multiply(A,add(multiply(D,multiply(B,additive_inverse(C))),multiply(multiply(D,B),C))),
inference(paramod,[status(thm)],[c_145,c_8]) ).
cnf(c_11623,plain,
multiply(A,add(multiply(B,multiply(C,additive_inverse(D))),multiply(multiply(B,C),D))) = multiply(A,add(multiply(D,multiply(B,additive_inverse(C))),multiply(multiply(D,B),C))),
inference(paramod,[status(thm)],[c_8,c_11706]) ).
cnf(c_11707,plain,
multiply(cx,add(multiply(cx,multiply(cz,additive_inverse(cy))),multiply(multiply(cx,cz),cy))) != multiply(cx,add(multiply(cy,multiply(cx,additive_inverse(cz))),multiply(multiply(cy,cx),cz))),
inference(copy,[status(thm)],[c_10724]) ).
cnf(c_11624,plain,
$false,
inference(resolve,[status(thm)],[c_11623,c_11707]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : RNG029-3 : TPTP v9.3.1. Bugfixed v2.4.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n007.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sat Sep 26 05:46:53 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.35 % Process 2931096 was started by sandbox2 on n007,
% 0.08/0.35 % Sat Sep 26 05:46:53 2026
% 0.08/0.35 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.08/0.36
% 0.08/0.36 % From the command line: assign(max_seconds, 300).
% 57.76/7.77
% 57.76/7.77 % Assigning unary symbol additive_inverse kb_weight 0 and highest precedence (9).
% 57.76/7.77
% 57.76/7.77 % given #500 (F,wt=61): 8025 add(multiply(A,cx),multiply(multiply(cx,cy),multiply(cz,cx))) != multiply(add(multiply(cx,multiply(cy,cz)),A),cx). [para(96(a,1),245(a,1)),flip(a)].
% 57.76/7.77
% 57.76/7.77 % SZS status Unsatisfiable for theBenchmark
% 57.76/7.77
% 57.76/7.77 % Proof 1 at 6.20 (+ 1.17) seconds.
% 57.76/7.77 % Length of proof is 54.
% 57.76/7.77 % Level of proof is 11.
% 57.76/7.77 % Maximum clause weight is 93.000.
% 57.76/7.77 % Given clauses 586.
% 57.76/7.77
% 57.76/7.77 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------