%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : RNG025-7 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n010.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 : Fri Sep 25 02:37:31 PM UTC 2026
% Result : Unsatisfiable 67.76s 10.07s
% Output : CNFRefutation 67.76s
% Verified :
% SZS Type : Refutation
% Derivation depth : 45
% Number of leaves : 18
% Syntax : Number of clauses : 147 ( 147 unt; 0 nHn; 5 RR)
% Number of literals : 147 ( 146 equ; 2 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 3 con; 0-3 aty)
% Number of variables : 368 ( 8 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t21,axiom,
add(multiply(multiply(X1,X2),X3),additive_inverse(multiply(X1,multiply(X2,X3)))) = associator(X1,X2,X3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t8,axiom,
multiply(X1,additive_inverse(X2)) = additive_inverse(multiply(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t45,plain,
additive_inverse(multiply(X1,X2)) = multiply(X1,additive_inverse(X2)),
inference(orient,[status(thm)],[t8]) ).
cnf(t125236,plain,
add(multiply(multiply(X1,X2),X3),multiply(X1,additive_inverse(multiply(X2,X3)))) = associator(X1,X2,X3),
inference(step,[status(thm)],[t21,t45]) ).
cnf(t125237,plain,
add(multiply(multiply(X1,X2),X3),multiply(X1,multiply(X2,additive_inverse(X3)))) = associator(X1,X2,X3),
inference(step,[status(thm)],[t125236,t45]) ).
cnf(t142,plain,
add(multiply(multiply(X1,X2),X3),multiply(X1,multiply(X2,additive_inverse(X3)))) = associator(X1,X2,X3),
inference(orient,[status(thm)],[t125237]) ).
cnf(t9,axiom,
multiply(additive_inverse(X1),X2) = additive_inverse(multiply(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t125230,plain,
multiply(additive_inverse(X1),X2) = multiply(X1,additive_inverse(X2)),
inference(step,[status(thm)],[t9,t45]) ).
cnf(t70,plain,
multiply(additive_inverse(X1),X2) = multiply(X1,additive_inverse(X2)),
inference(orient,[status(thm)],[t125230]) ).
cnf(t150,plain,
associator(additive_inverse(X1),X2,X3) = add(multiply(multiply(X1,additive_inverse(X2)),X3),multiply(additive_inverse(X1),multiply(X2,additive_inverse(X3)))),
inference(cp,[status(thm)],[t142,t70]) ).
cnf(t126156,plain,
associator(additive_inverse(X1),X2,X3) = add(multiply(multiply(X1,additive_inverse(X2)),X3),multiply(X1,additive_inverse(multiply(X2,additive_inverse(X3))))),
inference(step,[status(thm)],[t150,t70]) ).
cnf(t126157,plain,
associator(additive_inverse(X1),X2,X3) = add(multiply(multiply(X1,additive_inverse(X2)),X3),multiply(X1,multiply(X2,additive_inverse(additive_inverse(X3))))),
inference(step,[status(thm)],[t126156,t45]) ).
cnf(t2,axiom,
additive_inverse(additive_inverse(X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t24,plain,
additive_inverse(additive_inverse(X1)) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t126158,plain,
associator(additive_inverse(X1),X2,X3) = add(multiply(multiply(X1,additive_inverse(X2)),X3),multiply(X1,multiply(X2,X3))),
inference(step,[status(thm)],[t126157,t24]) ).
cnf(t18,axiom,
add(multiply(X1,X2),additive_inverse(multiply(X3,X2))) = multiply(add(X1,additive_inverse(X3)),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t125229,plain,
add(multiply(X1,X2),multiply(X3,additive_inverse(X2))) = multiply(add(X1,additive_inverse(X3)),X2),
inference(step,[status(thm)],[t18,t45]) ).
cnf(t60,plain,
add(multiply(X1,X2),multiply(X3,additive_inverse(X2))) = multiply(add(X1,additive_inverse(X3)),X2),
inference(orient,[status(thm)],[t125229]) ).
cnf(t77,plain,
multiply(add(additive_inverse(X1),additive_inverse(X2)),X3) = add(multiply(X1,additive_inverse(X3)),multiply(X2,additive_inverse(X3))),
inference(cp,[status(thm)],[t60,t70]) ).
cnf(t16,axiom,
add(multiply(X1,X2),multiply(X3,X2)) = multiply(add(X1,X3),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t52,plain,
add(multiply(X1,X2),multiply(X3,X2)) = multiply(add(X1,X3),X2),
inference(orient,[status(thm)],[t16]) ).
cnf(t125288,plain,
multiply(add(additive_inverse(X1),additive_inverse(X2)),X3) = multiply(add(X1,X2),additive_inverse(X3)),
inference(step,[status(thm)],[t77,t52]) ).
cnf(t348,plain,
multiply(add(additive_inverse(X1),additive_inverse(X2)),X3) = multiply(add(X1,X2),additive_inverse(X3)),
inference(orient,[status(thm)],[t125288]) ).
cnf(t4,axiom,
multiply(additive_identity,X1) = additive_identity,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t91,plain,
multiply(additive_identity,X1) = additive_identity,
inference(orient,[status(thm)],[t4]) ).
cnf(t92,plain,
multiply(additive_identity,additive_inverse(X1)) = additive_inverse(additive_identity),
inference(cp,[status(thm)],[t45,t91]) ).
cnf(t125238,plain,
additive_identity = additive_inverse(additive_identity),
inference(step,[status(thm)],[t92,t91]) ).
cnf(t165,plain,
additive_inverse(additive_identity) = additive_identity,
inference(orient,[status(thm)],[t125238]) ).
cnf(t351,plain,
multiply(add(additive_identity,X1),additive_inverse(X2)) = multiply(add(additive_identity,additive_inverse(X1)),X2),
inference(cp,[status(thm)],[t348,t165]) ).
cnf(t7,axiom,
add(X1,X2) = add(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t94,plain,
add(X1,X2) = add(X2,X1),
inference(orient,[status(thm)],[t7]) ).
cnf(t125289,plain,
multiply(add(X1,additive_identity),additive_inverse(X2)) = multiply(add(additive_identity,additive_inverse(X1)),X2),
inference(step,[status(thm)],[t351,t94]) ).
cnf(t0,axiom,
add(X1,additive_identity) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t22,plain,
add(X1,additive_identity) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t125290,plain,
multiply(X1,additive_inverse(X2)) = multiply(add(additive_identity,additive_inverse(X1)),X2),
inference(step,[status(thm)],[t125289,t22]) ).
cnf(t365,plain,
multiply(add(additive_identity,additive_inverse(X1)),X2) = multiply(X1,additive_inverse(X2)),
inference(orient,[status(thm)],[t125290]) ).
cnf(t375,plain,
associator(add(additive_identity,additive_inverse(X1)),X2,X3) = add(multiply(multiply(X1,additive_inverse(X2)),X3),multiply(add(additive_identity,additive_inverse(X1)),multiply(X2,additive_inverse(X3)))),
inference(cp,[status(thm)],[t142,t365]) ).
cnf(t72,plain,
multiply(multiply(X1,X2),additive_inverse(X3)) = multiply(multiply(X1,additive_inverse(X2)),X3),
inference(cp,[status(thm)],[t70,t45]) ).
cnf(t234,plain,
multiply(multiply(X1,additive_inverse(X2)),X3) = multiply(multiply(X1,X2),additive_inverse(X3)),
inference(orient,[status(thm)],[t72]) ).
cnf(t125291,plain,
associator(add(additive_identity,additive_inverse(X1)),X2,X3) = add(multiply(multiply(X1,X2),additive_inverse(X3)),multiply(add(additive_identity,additive_inverse(X1)),multiply(X2,additive_inverse(X3)))),
inference(step,[status(thm)],[t375,t234]) ).
cnf(t125292,plain,
associator(add(additive_identity,additive_inverse(X1)),X2,X3) = add(multiply(multiply(X1,X2),additive_inverse(X3)),multiply(X1,additive_inverse(multiply(X2,additive_inverse(X3))))),
inference(step,[status(thm)],[t125291,t365]) ).
cnf(t125293,plain,
associator(add(additive_identity,additive_inverse(X1)),X2,X3) = add(multiply(multiply(X1,X2),additive_inverse(X3)),multiply(X1,multiply(X2,additive_inverse(additive_inverse(X3))))),
inference(step,[status(thm)],[t125292,t45]) ).
cnf(t125294,plain,
associator(add(additive_identity,additive_inverse(X1)),X2,X3) = associator(X1,X2,additive_inverse(X3)),
inference(step,[status(thm)],[t125293,t142]) ).
cnf(t378,plain,
associator(add(additive_identity,additive_inverse(X1)),X2,X3) = associator(X1,X2,additive_inverse(X3)),
inference(orient,[status(thm)],[t125294]) ).
cnf(t380,plain,
associator(additive_inverse(X1),X2,additive_inverse(X3)) = associator(add(additive_identity,X1),X2,X3),
inference(cp,[status(thm)],[t378,t24]) ).
cnf(t125295,plain,
associator(additive_inverse(X1),X2,additive_inverse(X3)) = associator(add(X1,additive_identity),X2,X3),
inference(step,[status(thm)],[t380,t94]) ).
cnf(t125296,plain,
associator(additive_inverse(X1),X2,additive_inverse(X3)) = associator(X1,X2,X3),
inference(step,[status(thm)],[t125295,t22]) ).
cnf(t435,plain,
associator(additive_inverse(X1),X2,additive_inverse(X3)) = associator(X1,X2,X3),
inference(orient,[status(thm)],[t125296]) ).
cnf(t437,plain,
associator(additive_inverse(X1),X2,X3) = associator(X1,X2,additive_inverse(X3)),
inference(cp,[status(thm)],[t435,t24]) ).
cnf(t441,plain,
associator(additive_inverse(X1),X2,X3) = associator(X1,X2,additive_inverse(X3)),
inference(orient,[status(thm)],[t437]) ).
cnf(t126159,plain,
associator(X1,X2,additive_inverse(X3)) = add(multiply(multiply(X1,additive_inverse(X2)),X3),multiply(X1,multiply(X2,X3))),
inference(step,[status(thm)],[t126158,t441]) ).
cnf(t126160,plain,
associator(X1,X2,additive_inverse(X3)) = add(multiply(X1,multiply(X2,X3)),multiply(multiply(X1,additive_inverse(X2)),X3)),
inference(step,[status(thm)],[t126159,t94]) ).
cnf(t126161,plain,
associator(X1,X2,additive_inverse(X3)) = add(multiply(X1,multiply(X2,X3)),multiply(multiply(X1,X2),additive_inverse(X3))),
inference(step,[status(thm)],[t126160,t234]) ).
cnf(t56604,plain,
add(multiply(X1,multiply(X2,X3)),multiply(multiply(X1,X2),additive_inverse(X3))) = associator(X1,X2,additive_inverse(X3)),
inference(orient,[status(thm)],[t126161]) ).
cnf(t15,axiom,
add(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,add(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t35,plain,
add(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,add(X2,X3)),
inference(orient,[status(thm)],[t15]) ).
cnf(t13,axiom,
multiply(multiply(X1,X2),X2) = multiply(X1,multiply(X2,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t28,plain,
multiply(multiply(X1,X2),X2) = multiply(X1,multiply(X2,X2)),
inference(orient,[status(thm)],[t13]) ).
cnf(t37,plain,
multiply(multiply(X1,X2),add(X2,X3)) = add(multiply(X1,multiply(X2,X2)),multiply(multiply(X1,X2),X3)),
inference(cp,[status(thm)],[t35,t28]) ).
cnf(t2961,plain,
add(multiply(X1,multiply(X2,X2)),multiply(multiply(X1,X2),X3)) = multiply(multiply(X1,X2),add(X2,X3)),
inference(orient,[status(thm)],[t37]) ).
cnf(t55,plain,
multiply(add(multiply(X1,X2),X3),X2) = add(multiply(X1,multiply(X2,X2)),multiply(X3,X2)),
inference(cp,[status(thm)],[t52,t28]) ).
cnf(t125395,plain,
multiply(add(X3,multiply(X1,X2)),X2) = add(multiply(X1,multiply(X2,X2)),multiply(X3,X2)),
inference(step,[status(thm)],[t55,t94]) ).
cnf(t125396,plain,
multiply(add(X3,multiply(X1,X2)),X2) = add(multiply(X3,X2),multiply(X1,multiply(X2,X2))),
inference(step,[status(thm)],[t125395,t94]) ).
cnf(t2060,plain,
add(multiply(X1,X2),multiply(X3,multiply(X2,X2))) = multiply(add(X1,multiply(X3,X2)),X2),
inference(orient,[status(thm)],[t125396]) ).
cnf(t12,axiom,
multiply(multiply(X1,X1),X2) = multiply(X1,multiply(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t31,plain,
multiply(multiply(X1,X1),X2) = multiply(X1,multiply(X1,X2)),
inference(orient,[status(thm)],[t12]) ).
cnf(t2085,plain,
multiply(add(multiply(X1,X1),multiply(X2,X3)),X3) = add(multiply(X1,multiply(X1,X3)),multiply(X2,multiply(X3,X3))),
inference(cp,[status(thm)],[t2060,t31]) ).
cnf(t114450,plain,
add(multiply(X1,multiply(X1,X2)),multiply(X3,multiply(X2,X2))) = multiply(add(multiply(X1,X1),multiply(X3,X2)),X2),
inference(orient,[status(thm)],[t2085]) ).
cnf(t114452,plain,
multiply(add(multiply(X1,X1),multiply(X1,X2)),X2) = multiply(X1,add(multiply(X1,X2),multiply(X2,X2))),
inference(cp,[status(thm)],[t114450,t35]) ).
cnf(t126667,plain,
multiply(multiply(X1,add(X1,X2)),X2) = multiply(X1,add(multiply(X1,X2),multiply(X2,X2))),
inference(step,[status(thm)],[t114452,t35]) ).
cnf(t126668,plain,
multiply(multiply(X1,add(X1,X2)),X2) = multiply(X1,multiply(add(X1,X2),X2)),
inference(step,[status(thm)],[t126667,t52]) ).
cnf(t114997,plain,
multiply(multiply(X1,add(X1,X2)),X2) = multiply(X1,multiply(add(X1,X2),X2)),
inference(orient,[status(thm)],[t126668]) ).
cnf(t19,axiom,
add(additive_inverse(multiply(X1,X2)),additive_inverse(multiply(X1,X3))) = multiply(additive_inverse(X1),add(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t125231,plain,
add(multiply(X1,additive_inverse(X2)),additive_inverse(multiply(X1,X3))) = multiply(additive_inverse(X1),add(X2,X3)),
inference(step,[status(thm)],[t19,t45]) ).
cnf(t17,axiom,
add(multiply(X1,X2),additive_inverse(multiply(X1,X3))) = multiply(X1,add(X2,additive_inverse(X3))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t40,plain,
add(multiply(X1,X2),additive_inverse(multiply(X1,X3))) = multiply(X1,add(X2,additive_inverse(X3))),
inference(orient,[status(thm)],[t17]) ).
cnf(t125232,plain,
multiply(X1,add(additive_inverse(X2),additive_inverse(X3))) = multiply(additive_inverse(X1),add(X2,X3)),
inference(step,[status(thm)],[t125231,t40]) ).
cnf(t125233,plain,
multiply(X1,add(additive_inverse(X2),additive_inverse(X3))) = multiply(X1,additive_inverse(add(X2,X3))),
inference(step,[status(thm)],[t125232,t70]) ).
cnf(t78,plain,
multiply(X1,add(additive_inverse(X2),additive_inverse(X3))) = multiply(X1,additive_inverse(add(X2,X3))),
inference(orient,[status(thm)],[t125233]) ).
cnf(t86,plain,
multiply(X1,add(add(additive_inverse(X2),additive_inverse(X3)),Y3)) = add(multiply(X1,additive_inverse(add(X2,X3))),multiply(X1,Y3)),
inference(cp,[status(thm)],[t35,t78]) ).
cnf(t125430,plain,
multiply(X1,add(Y3,add(additive_inverse(X2),additive_inverse(X3)))) = add(multiply(X1,additive_inverse(add(X2,X3))),multiply(X1,Y3)),
inference(step,[status(thm)],[t86,t94]) ).
cnf(t125431,plain,
multiply(X1,add(Y3,add(additive_inverse(X2),additive_inverse(X3)))) = multiply(X1,add(additive_inverse(add(X2,X3)),Y3)),
inference(step,[status(thm)],[t125430,t35]) ).
cnf(t125432,plain,
multiply(X1,add(Y3,add(additive_inverse(X2),additive_inverse(X3)))) = multiply(X1,add(Y3,additive_inverse(add(X2,X3)))),
inference(step,[status(thm)],[t125431,t94]) ).
cnf(t2436,plain,
multiply(X1,add(X2,add(additive_inverse(X3),additive_inverse(Y3)))) = multiply(X1,add(X2,additive_inverse(add(X3,Y3)))),
inference(orient,[status(thm)],[t125432]) ).
cnf(t11,axiom,
add(add(X1,X2),X3) = add(X1,add(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t125234,plain,
add(X3,add(X1,X2)) = add(X1,add(X2,X3)),
inference(step,[status(thm)],[t11,t94]) ).
cnf(t101,plain,
add(X1,add(X2,X3)) = add(X2,add(X3,X1)),
inference(orient,[status(thm)],[t125234]) ).
cnf(t5,axiom,
add(X1,additive_inverse(X1)) = additive_identity,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t119,plain,
add(X1,additive_inverse(X1)) = additive_identity,
inference(orient,[status(thm)],[t5]) ).
cnf(t122,plain,
add(X1,add(additive_inverse(X1),X2)) = add(X2,additive_identity),
inference(cp,[status(thm)],[t101,t119]) ).
cnf(t125270,plain,
add(X1,add(X2,additive_inverse(X1))) = add(X2,additive_identity),
inference(step,[status(thm)],[t122,t94]) ).
cnf(t125271,plain,
add(X1,add(X2,additive_inverse(X1))) = X2,
inference(step,[status(thm)],[t125270,t22]) ).
cnf(t182,plain,
add(X1,add(X2,additive_inverse(X1))) = X2,
inference(orient,[status(thm)],[t125271]) ).
cnf(t2448,plain,
multiply(X1,add(X2,additive_inverse(add(X3,X2)))) = multiply(X1,additive_inverse(X3)),
inference(cp,[status(thm)],[t2436,t182]) ).
cnf(t125433,plain,
multiply(X1,add(X2,additive_inverse(add(X2,X3)))) = multiply(X1,additive_inverse(X3)),
inference(step,[status(thm)],[t2448,t94]) ).
cnf(t2486,plain,
multiply(X1,add(X2,additive_inverse(add(X2,X3)))) = multiply(X1,additive_inverse(X3)),
inference(orient,[status(thm)],[t125433]) ).
cnf(t115047,plain,
multiply(X1,multiply(add(X1,additive_inverse(add(X1,X2))),additive_inverse(add(X1,X2)))) = multiply(multiply(X1,additive_inverse(X2)),additive_inverse(add(X1,X2))),
inference(cp,[status(thm)],[t114997,t2486]) ).
cnf(t357,plain,
multiply(add(X1,add(additive_inverse(X2),additive_inverse(X3))),Y3) = add(multiply(X1,Y3),multiply(add(X2,X3),additive_inverse(Y3))),
inference(cp,[status(thm)],[t52,t348]) ).
cnf(t125439,plain,
multiply(add(X1,add(additive_inverse(X2),additive_inverse(X3))),Y3) = multiply(add(X1,additive_inverse(add(X2,X3))),Y3),
inference(step,[status(thm)],[t357,t60]) ).
cnf(t2719,plain,
multiply(add(X1,add(additive_inverse(X2),additive_inverse(X3))),Y3) = multiply(add(X1,additive_inverse(add(X2,X3))),Y3),
inference(orient,[status(thm)],[t125439]) ).
cnf(t2727,plain,
multiply(add(X1,additive_inverse(add(X2,X1))),X3) = multiply(additive_inverse(X2),X3),
inference(cp,[status(thm)],[t2719,t182]) ).
cnf(t125440,plain,
multiply(add(X1,additive_inverse(add(X1,X2))),X3) = multiply(additive_inverse(X2),X3),
inference(step,[status(thm)],[t2727,t94]) ).
cnf(t125441,plain,
multiply(add(X1,additive_inverse(add(X1,X2))),X3) = multiply(X2,additive_inverse(X3)),
inference(step,[status(thm)],[t125440,t70]) ).
cnf(t2760,plain,
multiply(add(X1,additive_inverse(add(X1,X2))),X3) = multiply(X2,additive_inverse(X3)),
inference(orient,[status(thm)],[t125441]) ).
cnf(t126694,plain,
multiply(X1,multiply(X2,additive_inverse(additive_inverse(add(X1,X2))))) = multiply(multiply(X1,additive_inverse(X2)),additive_inverse(add(X1,X2))),
inference(step,[status(thm)],[t115047,t2760]) ).
cnf(t126695,plain,
multiply(X1,multiply(X2,add(X1,X2))) = multiply(multiply(X1,additive_inverse(X2)),additive_inverse(add(X1,X2))),
inference(step,[status(thm)],[t126694,t24]) ).
cnf(t126696,plain,
multiply(X1,multiply(X2,add(X1,X2))) = multiply(multiply(X1,X2),additive_inverse(additive_inverse(add(X1,X2)))),
inference(step,[status(thm)],[t126695,t234]) ).
cnf(t126697,plain,
multiply(X1,multiply(X2,add(X1,X2))) = multiply(multiply(X1,X2),add(X1,X2)),
inference(step,[status(thm)],[t126696,t24]) ).
cnf(t117312,plain,
multiply(multiply(X1,X2),add(X1,X2)) = multiply(X1,multiply(X2,add(X1,X2))),
inference(orient,[status(thm)],[t126697]) ).
cnf(t117334,plain,
multiply(additive_inverse(X1),multiply(additive_inverse(X2),add(additive_inverse(X1),additive_inverse(X2)))) = multiply(multiply(additive_inverse(X1),additive_inverse(X2)),additive_inverse(add(X1,X2))),
inference(cp,[status(thm)],[t117312,t78]) ).
cnf(t126752,plain,
multiply(X1,additive_inverse(multiply(additive_inverse(X2),add(additive_inverse(X1),additive_inverse(X2))))) = multiply(multiply(additive_inverse(X1),additive_inverse(X2)),additive_inverse(add(X1,X2))),
inference(step,[status(thm)],[t117334,t70]) ).
cnf(t126753,plain,
multiply(X1,multiply(additive_inverse(X2),additive_inverse(add(additive_inverse(X1),additive_inverse(X2))))) = multiply(multiply(additive_inverse(X1),additive_inverse(X2)),additive_inverse(add(X1,X2))),
inference(step,[status(thm)],[t126752,t45]) ).
cnf(t10,axiom,
multiply(additive_inverse(X1),additive_inverse(X2)) = multiply(X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t25,plain,
multiply(additive_inverse(X1),additive_inverse(X2)) = multiply(X1,X2),
inference(orient,[status(thm)],[t10]) ).
cnf(t126754,plain,
multiply(X1,multiply(X2,add(additive_inverse(X1),additive_inverse(X2)))) = multiply(multiply(additive_inverse(X1),additive_inverse(X2)),additive_inverse(add(X1,X2))),
inference(step,[status(thm)],[t126753,t25]) ).
cnf(t126755,plain,
multiply(X1,multiply(X2,additive_inverse(add(X1,X2)))) = multiply(multiply(additive_inverse(X1),additive_inverse(X2)),additive_inverse(add(X1,X2))),
inference(step,[status(thm)],[t126754,t78]) ).
cnf(t126756,plain,
multiply(X1,multiply(X2,additive_inverse(add(X1,X2)))) = multiply(multiply(additive_inverse(X1),X2),additive_inverse(additive_inverse(add(X1,X2)))),
inference(step,[status(thm)],[t126755,t234]) ).
cnf(t126757,plain,
multiply(X1,multiply(X2,additive_inverse(add(X1,X2)))) = multiply(multiply(X1,additive_inverse(X2)),additive_inverse(additive_inverse(add(X1,X2)))),
inference(step,[status(thm)],[t126756,t70]) ).
cnf(t126758,plain,
multiply(X1,multiply(X2,additive_inverse(add(X1,X2)))) = multiply(multiply(X1,X2),additive_inverse(additive_inverse(additive_inverse(add(X1,X2))))),
inference(step,[status(thm)],[t126757,t234]) ).
cnf(t126759,plain,
multiply(X1,multiply(X2,additive_inverse(add(X1,X2)))) = multiply(multiply(X1,X2),additive_inverse(add(X1,X2))),
inference(step,[status(thm)],[t126758,t24]) ).
cnf(t123751,plain,
multiply(multiply(X1,X2),additive_inverse(add(X1,X2))) = multiply(X1,multiply(X2,additive_inverse(add(X1,X2)))),
inference(orient,[status(thm)],[t126759]) ).
cnf(t124050,plain,
multiply(multiply(X1,X2),add(X2,additive_inverse(add(X1,X2)))) = add(multiply(X1,multiply(X2,X2)),multiply(X1,multiply(X2,additive_inverse(add(X1,X2))))),
inference(cp,[status(thm)],[t2961,t123751]) ).
cnf(t2506,plain,
multiply(X1,additive_inverse(X2)) = multiply(X1,add(X3,additive_inverse(add(X2,X3)))),
inference(cp,[status(thm)],[t2486,t94]) ).
cnf(t2537,plain,
multiply(X1,add(X2,additive_inverse(add(X3,X2)))) = multiply(X1,additive_inverse(X3)),
inference(orient,[status(thm)],[t2506]) ).
cnf(t126760,plain,
multiply(multiply(X1,X2),additive_inverse(X1)) = add(multiply(X1,multiply(X2,X2)),multiply(X1,multiply(X2,additive_inverse(add(X1,X2))))),
inference(step,[status(thm)],[t124050,t2537]) ).
cnf(t126761,plain,
multiply(multiply(X1,X2),additive_inverse(X1)) = multiply(X1,add(multiply(X2,X2),multiply(X2,additive_inverse(add(X1,X2))))),
inference(step,[status(thm)],[t126760,t35]) ).
cnf(t126762,plain,
multiply(multiply(X1,X2),additive_inverse(X1)) = multiply(X1,multiply(X2,add(X2,additive_inverse(add(X1,X2))))),
inference(step,[status(thm)],[t126761,t35]) ).
cnf(t126763,plain,
multiply(multiply(X1,X2),additive_inverse(X1)) = multiply(X1,multiply(X2,additive_inverse(X1))),
inference(step,[status(thm)],[t126762,t2537]) ).
cnf(t124185,plain,
multiply(multiply(X1,X2),additive_inverse(X1)) = multiply(X1,multiply(X2,additive_inverse(X1))),
inference(orient,[status(thm)],[t126763]) ).
cnf(t124397,plain,
associator(X1,X2,additive_inverse(X1)) = add(multiply(X1,multiply(X2,X1)),multiply(X1,multiply(X2,additive_inverse(X1)))),
inference(cp,[status(thm)],[t56604,t124185]) ).
cnf(t69,plain,
multiply(add(X1,additive_inverse(X2)),multiply(X3,Y3)) = add(multiply(X1,multiply(X3,Y3)),multiply(X2,multiply(X3,additive_inverse(Y3)))),
inference(cp,[status(thm)],[t60,t45]) ).
cnf(t16704,plain,
add(multiply(X1,multiply(X2,X3)),multiply(Y3,multiply(X2,additive_inverse(X3)))) = multiply(add(X1,additive_inverse(Y3)),multiply(X2,X3)),
inference(orient,[status(thm)],[t69]) ).
cnf(t126764,plain,
associator(X1,X2,additive_inverse(X1)) = multiply(add(X1,additive_inverse(X1)),multiply(X2,X1)),
inference(step,[status(thm)],[t124397,t16704]) ).
cnf(t126765,plain,
associator(X1,X2,additive_inverse(X1)) = multiply(additive_identity,multiply(X2,X1)),
inference(step,[status(thm)],[t126764,t119]) ).
cnf(t126766,plain,
associator(X1,X2,additive_inverse(X1)) = additive_identity,
inference(step,[status(thm)],[t126765,t91]) ).
cnf(t124597,plain,
associator(X1,X2,additive_inverse(X1)) = additive_identity,
inference(orient,[status(thm)],[t126766]) ).
cnf(t2804,plain,
associator(X1,add(X2,additive_inverse(add(X2,X3))),Y3) = add(multiply(multiply(X1,add(X2,additive_inverse(add(X2,X3)))),Y3),multiply(X1,multiply(X3,additive_inverse(additive_inverse(Y3))))),
inference(cp,[status(thm)],[t142,t2760]) ).
cnf(t125448,plain,
associator(X1,add(X2,additive_inverse(add(X2,X3))),Y3) = add(multiply(multiply(X1,additive_inverse(X3)),Y3),multiply(X1,multiply(X3,additive_inverse(additive_inverse(Y3))))),
inference(step,[status(thm)],[t2804,t2486]) ).
cnf(t125449,plain,
associator(X1,add(X2,additive_inverse(add(X2,X3))),Y3) = add(multiply(multiply(X1,X3),additive_inverse(Y3)),multiply(X1,multiply(X3,additive_inverse(additive_inverse(Y3))))),
inference(step,[status(thm)],[t125448,t234]) ).
cnf(t125450,plain,
associator(X1,add(X2,additive_inverse(add(X2,X3))),Y3) = associator(X1,X3,additive_inverse(Y3)),
inference(step,[status(thm)],[t125449,t142]) ).
cnf(t2900,plain,
associator(X1,add(X2,additive_inverse(add(X2,X3))),Y3) = associator(X1,X3,additive_inverse(Y3)),
inference(orient,[status(thm)],[t125450]) ).
cnf(t124621,plain,
additive_identity = associator(X1,X2,additive_inverse(additive_inverse(X1))),
inference(cp,[status(thm)],[t124597,t2900]) ).
cnf(t126769,plain,
additive_identity = associator(X1,X2,X1),
inference(step,[status(thm)],[t124621,t24]) ).
cnf(t125208,plain,
associator(X1,X2,X1) = additive_identity,
inference(orient,[status(thm)],[t126769]) ).
cnf(goal_0,negated_conjecture,
associator(x,y,x) != additive_identity,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
additive_identity != additive_identity,
inference(rw,[status(thm)],[goal_0,t125208]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : RNG025-7 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.11/0.38 % Computer : n010.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Thu Sep 24 07:49:09 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 67.76/10.07 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 67.76/10.07 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------