%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : RNG025-6 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n016.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:30 PM UTC 2026
% Result : Unsatisfiable 209.42s 27.39s
% Output : CNFRefutation 209.42s
% Verified :
% SZS Type : Refutation
% Derivation depth : 84
% Number of leaves : 16
% Syntax : Number of clauses : 248 ( 248 unt; 0 nHn; 10 RR)
% Number of literals : 248 ( 247 equ; 3 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 4 con; 0-3 aty)
% Number of variables : 569 ( 11 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t15,axiom,
sFlat0 = associator(x,y,x),
introduced(definition) ).
cnf(t74,plain,
associator(x,y,x) = sFlat0,
inference(orient,[status(thm)],[t15]) ).
cnf(t8,axiom,
add(add(X1,X2),X3) = add(X1,add(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t37,plain,
add(add(X1,X2),X3) = add(X1,add(X2,X3)),
inference(orient,[status(thm)],[t8]) ).
cnf(t14,axiom,
add(multiply(multiply(X1,X2),X3),additive_inverse(multiply(X1,multiply(X2,X3)))) = associator(X1,X2,X3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t57,plain,
add(multiply(multiply(X1,X2),X3),additive_inverse(multiply(X1,multiply(X2,X3)))) = associator(X1,X2,X3),
inference(orient,[status(thm)],[t14]) ).
cnf(t73,plain,
add(multiply(multiply(X1,X2),X3),add(additive_inverse(multiply(X1,multiply(X2,X3))),Y3)) = add(associator(X1,X2,X3),Y3),
inference(cp,[status(thm)],[t37,t57]) ).
cnf(t12,axiom,
add(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,add(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t24,plain,
add(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,add(X2,X3)),
inference(orient,[status(thm)],[t12]) ).
cnf(t39,plain,
add(multiply(X1,X2),add(multiply(X1,X3),Y3)) = add(multiply(X1,add(X2,X3)),Y3),
inference(cp,[status(thm)],[t37,t24]) ).
cnf(t1166,plain,
add(multiply(X1,X2),add(multiply(X1,X3),Y3)) = add(multiply(X1,add(X2,X3)),Y3),
inference(orient,[status(thm)],[t39]) ).
cnf(t5,axiom,
add(X1,additive_inverse(X1)) = additive_identity,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t42,plain,
add(X1,additive_inverse(X1)) = additive_identity,
inference(orient,[status(thm)],[t5]) ).
cnf(t1197,plain,
add(multiply(X1,add(X2,X3)),additive_inverse(multiply(X1,X3))) = add(multiply(X1,X2),additive_identity),
inference(cp,[status(thm)],[t1166,t42]) ).
cnf(t7,axiom,
add(X1,X2) = add(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t36,plain,
add(X1,X2) = add(X2,X1),
inference(orient,[status(thm)],[t7]) ).
cnf(t130933,plain,
add(additive_inverse(multiply(X1,X3)),multiply(X1,add(X2,X3))) = add(multiply(X1,X2),additive_identity),
inference(step,[status(thm)],[t1197,t36]) ).
cnf(t0,axiom,
add(X1,additive_identity) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t16,plain,
add(X1,additive_identity) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t130934,plain,
add(additive_inverse(multiply(X1,X3)),multiply(X1,add(X2,X3))) = multiply(X1,X2),
inference(step,[status(thm)],[t130933,t16]) ).
cnf(t2785,plain,
add(additive_inverse(multiply(X1,X2)),multiply(X1,add(X3,X2))) = multiply(X1,X3),
inference(orient,[status(thm)],[t130934]) ).
cnf(t2848,plain,
multiply(X1,X2) = add(additive_inverse(multiply(X1,additive_inverse(X2))),multiply(X1,additive_identity)),
inference(cp,[status(thm)],[t2785,t42]) ).
cnf(t130935,plain,
multiply(X1,X2) = add(multiply(X1,additive_identity),additive_inverse(multiply(X1,additive_inverse(X2)))),
inference(step,[status(thm)],[t2848,t36]) ).
cnf(t3,axiom,
multiply(X1,additive_identity) = additive_identity,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t27,plain,
multiply(X1,additive_identity) = additive_identity,
inference(orient,[status(thm)],[t3]) ).
cnf(t130936,plain,
multiply(X1,X2) = add(additive_identity,additive_inverse(multiply(X1,additive_inverse(X2)))),
inference(step,[status(thm)],[t130935,t27]) ).
cnf(t1,axiom,
add(additive_identity,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t17,plain,
add(additive_identity,X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t130937,plain,
multiply(X1,X2) = additive_inverse(multiply(X1,additive_inverse(X2))),
inference(step,[status(thm)],[t130936,t17]) ).
cnf(t2888,plain,
additive_inverse(multiply(X1,additive_inverse(X2))) = multiply(X1,X2),
inference(orient,[status(thm)],[t130937]) ).
cnf(t2,axiom,
additive_inverse(additive_inverse(X1)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t18,plain,
additive_inverse(additive_inverse(X1)) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t2904,plain,
multiply(X1,additive_inverse(X2)) = additive_inverse(multiply(X1,X2)),
inference(cp,[status(thm)],[t2888,t18]) ).
cnf(t3035,plain,
additive_inverse(multiply(X1,X2)) = multiply(X1,additive_inverse(X2)),
inference(orient,[status(thm)],[t2904]) ).
cnf(t131932,plain,
add(multiply(multiply(X1,X2),X3),add(multiply(X1,additive_inverse(multiply(X2,X3))),Y3)) = add(associator(X1,X2,X3),Y3),
inference(step,[status(thm)],[t73,t3035]) ).
cnf(t131933,plain,
add(multiply(multiply(X1,X2),X3),add(multiply(X1,multiply(X2,additive_inverse(X3))),Y3)) = add(associator(X1,X2,X3),Y3),
inference(step,[status(thm)],[t131932,t3035]) ).
cnf(t119562,plain,
add(multiply(multiply(X1,X2),X3),add(multiply(X1,multiply(X2,additive_inverse(X3))),Y3)) = add(associator(X1,X2,X3),Y3),
inference(orient,[status(thm)],[t131933]) ).
cnf(t45,plain,
add(X1,add(additive_inverse(X1),X2)) = add(additive_identity,X2),
inference(cp,[status(thm)],[t37,t42]) ).
cnf(t130880,plain,
add(X1,add(additive_inverse(X1),X2)) = X2,
inference(step,[status(thm)],[t45,t17]) ).
cnf(t116,plain,
add(X1,add(additive_inverse(X1),X2)) = X2,
inference(orient,[status(thm)],[t130880]) ).
cnf(t118,plain,
X1 = add(X2,add(X1,additive_inverse(X2))),
inference(cp,[status(thm)],[t116,t36]) ).
cnf(t123,plain,
add(X1,add(X2,additive_inverse(X1))) = X2,
inference(orient,[status(thm)],[t118]) ).
cnf(t11,axiom,
add(multiply(X1,X2),additive_inverse(multiply(X2,X1))) = commutator(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t46,plain,
add(multiply(X1,X2),additive_inverse(multiply(X2,X1))) = commutator(X2,X1),
inference(orient,[status(thm)],[t11]) ).
cnf(t127,plain,
multiply(X1,X2) = add(multiply(X2,X1),commutator(X2,X1)),
inference(cp,[status(thm)],[t123,t46]) ).
cnf(t224,plain,
add(multiply(X1,X2),commutator(X1,X2)) = multiply(X2,X1),
inference(orient,[status(thm)],[t127]) ).
cnf(t130938,plain,
add(multiply(X1,X2),multiply(X2,additive_inverse(X1))) = commutator(X2,X1),
inference(step,[status(thm)],[t46,t3035]) ).
cnf(t3072,plain,
add(multiply(X1,X2),multiply(X2,additive_inverse(X1))) = commutator(X2,X1),
inference(rw,[status(thm)],[t130938]) ).
cnf(t4112,plain,
add(multiply(X1,X2),multiply(X2,additive_inverse(X1))) = commutator(X2,X1),
inference(orient,[status(thm)],[t3072]) ).
cnf(t10,axiom,
multiply(multiply(X1,X2),X2) = multiply(X1,multiply(X2,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t19,plain,
multiply(multiply(X1,X2),X2) = multiply(X1,multiply(X2,X2)),
inference(orient,[status(thm)],[t10]) ).
cnf(t25,plain,
multiply(multiply(X1,X2),add(X2,X3)) = add(multiply(X1,multiply(X2,X2)),multiply(multiply(X1,X2),X3)),
inference(cp,[status(thm)],[t24,t19]) ).
cnf(t2919,plain,
add(multiply(X1,multiply(X2,X2)),multiply(multiply(X1,X2),X3)) = multiply(multiply(X1,X2),add(X2,X3)),
inference(orient,[status(thm)],[t25]) ).
cnf(t13,axiom,
add(multiply(X1,X2),multiply(X3,X2)) = multiply(add(X1,X3),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t29,plain,
add(multiply(X1,X2),multiply(X3,X2)) = multiply(add(X1,X3),X2),
inference(orient,[status(thm)],[t13]) ).
cnf(t31,plain,
multiply(add(multiply(X1,X2),X3),X2) = add(multiply(X1,multiply(X2,X2)),multiply(X3,X2)),
inference(cp,[status(thm)],[t29,t19]) ).
cnf(t857,plain,
add(multiply(X1,multiply(X2,X2)),multiply(X3,X2)) = multiply(add(multiply(X1,X2),X3),X2),
inference(orient,[status(thm)],[t31]) ).
cnf(t9,axiom,
multiply(multiply(X1,X1),X2) = multiply(X1,multiply(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t21,plain,
multiply(multiply(X1,X1),X2) = multiply(X1,multiply(X1,X2)),
inference(orient,[status(thm)],[t9]) ).
cnf(t880,plain,
multiply(add(multiply(X1,X2),multiply(X3,X3)),X2) = add(multiply(X1,multiply(X2,X2)),multiply(X3,multiply(X3,X2))),
inference(cp,[status(thm)],[t857,t21]) ).
cnf(t114191,plain,
add(multiply(X1,multiply(X2,X2)),multiply(X3,multiply(X3,X2))) = multiply(add(multiply(X1,X2),multiply(X3,X3)),X2),
inference(orient,[status(thm)],[t880]) ).
cnf(t114192,plain,
multiply(add(multiply(X1,X2),multiply(X1,X1)),X2) = multiply(X1,add(multiply(X2,X2),multiply(X1,X2))),
inference(cp,[status(thm)],[t114191,t24]) ).
cnf(t131893,plain,
multiply(multiply(X1,add(X2,X1)),X2) = multiply(X1,add(multiply(X2,X2),multiply(X1,X2))),
inference(step,[status(thm)],[t114192,t24]) ).
cnf(t131894,plain,
multiply(multiply(X1,add(X2,X1)),X2) = multiply(X1,multiply(add(X2,X1),X2)),
inference(step,[status(thm)],[t131893,t29]) ).
cnf(t114891,plain,
multiply(multiply(X1,add(X2,X1)),X2) = multiply(X1,multiply(add(X2,X1),X2)),
inference(orient,[status(thm)],[t131894]) ).
cnf(t115087,plain,
multiply(multiply(X1,add(X2,X1)),additive_inverse(X2)) = additive_inverse(multiply(X1,multiply(add(X2,X1),X2))),
inference(cp,[status(thm)],[t3035,t114891]) ).
cnf(t131930,plain,
multiply(multiply(X1,add(X2,X1)),additive_inverse(X2)) = multiply(X1,additive_inverse(multiply(add(X2,X1),X2))),
inference(step,[status(thm)],[t115087,t3035]) ).
cnf(t131931,plain,
multiply(multiply(X1,add(X2,X1)),additive_inverse(X2)) = multiply(X1,multiply(add(X2,X1),additive_inverse(X2))),
inference(step,[status(thm)],[t131930,t3035]) ).
cnf(t119160,plain,
multiply(multiply(X1,add(X2,X1)),additive_inverse(X2)) = multiply(X1,multiply(add(X2,X1),additive_inverse(X2))),
inference(orient,[status(thm)],[t131931]) ).
cnf(t119379,plain,
multiply(multiply(X1,add(X2,X1)),add(add(X2,X1),additive_inverse(X2))) = add(multiply(X1,multiply(add(X2,X1),add(X2,X1))),multiply(X1,multiply(add(X2,X1),additive_inverse(X2)))),
inference(cp,[status(thm)],[t2919,t119160]) ).
cnf(t131979,plain,
multiply(multiply(X1,add(X2,X1)),add(X2,add(X1,additive_inverse(X2)))) = add(multiply(X1,multiply(add(X2,X1),add(X2,X1))),multiply(X1,multiply(add(X2,X1),additive_inverse(X2)))),
inference(step,[status(thm)],[t119379,t37]) ).
cnf(t131980,plain,
multiply(multiply(X1,add(X2,X1)),X1) = add(multiply(X1,multiply(add(X2,X1),add(X2,X1))),multiply(X1,multiply(add(X2,X1),additive_inverse(X2)))),
inference(step,[status(thm)],[t131979,t123]) ).
cnf(t131981,plain,
multiply(multiply(X1,add(X2,X1)),X1) = multiply(X1,add(multiply(add(X2,X1),add(X2,X1)),multiply(add(X2,X1),additive_inverse(X2)))),
inference(step,[status(thm)],[t131980,t24]) ).
cnf(t131982,plain,
multiply(multiply(X1,add(X2,X1)),X1) = multiply(X1,multiply(add(X2,X1),add(add(X2,X1),additive_inverse(X2)))),
inference(step,[status(thm)],[t131981,t24]) ).
cnf(t131983,plain,
multiply(multiply(X1,add(X2,X1)),X1) = multiply(X1,multiply(add(X2,X1),add(X2,add(X1,additive_inverse(X2))))),
inference(step,[status(thm)],[t131982,t37]) ).
cnf(t131984,plain,
multiply(multiply(X1,add(X2,X1)),X1) = multiply(X1,multiply(add(X2,X1),X1)),
inference(step,[status(thm)],[t131983,t123]) ).
cnf(t128438,plain,
multiply(multiply(X1,add(X2,X1)),X1) = multiply(X1,multiply(add(X2,X1),X1)),
inference(orient,[status(thm)],[t131984]) ).
cnf(t128711,plain,
commutator(X1,multiply(X1,add(X2,X1))) = add(multiply(X1,multiply(add(X2,X1),X1)),multiply(X1,additive_inverse(multiply(X1,add(X2,X1))))),
inference(cp,[status(thm)],[t4112,t128438]) ).
cnf(t56,plain,
add(multiply(X1,X2),add(additive_inverse(multiply(X2,X1)),X3)) = add(commutator(X2,X1),X3),
inference(cp,[status(thm)],[t37,t46]) ).
cnf(t2693,plain,
add(multiply(X1,X2),add(additive_inverse(multiply(X2,X1)),X3)) = add(commutator(X2,X1),X3),
inference(orient,[status(thm)],[t56]) ).
cnf(t130945,plain,
add(multiply(X1,X2),add(multiply(X2,additive_inverse(X1)),X3)) = add(commutator(X2,X1),X3),
inference(step,[status(thm)],[t2693,t3035]) ).
cnf(t3076,plain,
add(multiply(X1,X2),add(multiply(X2,additive_inverse(X1)),X3)) = add(commutator(X2,X1),X3),
inference(rw,[status(thm)],[t130945]) ).
cnf(t54224,plain,
add(multiply(X1,X2),add(multiply(X2,additive_inverse(X1)),X3)) = add(commutator(X2,X1),X3),
inference(orient,[status(thm)],[t3076]) ).
cnf(t1185,plain,
add(multiply(X1,add(X2,X3)),additive_inverse(multiply(X3,X1))) = add(multiply(X1,X2),commutator(X3,X1)),
inference(cp,[status(thm)],[t1166,t46]) ).
cnf(t131145,plain,
add(additive_inverse(multiply(X3,X1)),multiply(X1,add(X2,X3))) = add(multiply(X1,X2),commutator(X3,X1)),
inference(step,[status(thm)],[t1185,t36]) ).
cnf(t131146,plain,
add(multiply(X3,additive_inverse(X1)),multiply(X1,add(X2,X3))) = add(multiply(X1,X2),commutator(X3,X1)),
inference(step,[status(thm)],[t131145,t3035]) ).
cnf(t25032,plain,
add(multiply(X1,additive_inverse(X2)),multiply(X2,add(X3,X1))) = add(multiply(X2,X3),commutator(X1,X2)),
inference(orient,[status(thm)],[t131146]) ).
cnf(t43,plain,
additive_identity = add(X1,add(X2,additive_inverse(add(X1,X2)))),
inference(cp,[status(thm)],[t42,t37]) ).
cnf(t128,plain,
add(X1,add(X2,additive_inverse(add(X1,X2)))) = additive_identity,
inference(orient,[status(thm)],[t43]) ).
cnf(t139,plain,
add(X1,additive_inverse(add(additive_inverse(X2),X1))) = add(X2,additive_identity),
inference(cp,[status(thm)],[t116,t128]) ).
cnf(t130881,plain,
add(X1,additive_inverse(add(additive_inverse(X2),X1))) = X2,
inference(step,[status(thm)],[t139,t16]) ).
cnf(t140,plain,
add(X1,additive_inverse(add(additive_inverse(X2),X1))) = X2,
inference(orient,[status(thm)],[t130881]) ).
cnf(t146,plain,
additive_inverse(X1) = add(X2,additive_inverse(add(X1,X2))),
inference(cp,[status(thm)],[t140,t18]) ).
cnf(t148,plain,
add(X1,additive_inverse(add(X2,X1))) = additive_inverse(X2),
inference(orient,[status(thm)],[t146]) ).
cnf(t158,plain,
additive_inverse(add(X1,additive_inverse(X2))) = add(X2,additive_inverse(X1)),
inference(cp,[status(thm)],[t116,t148]) ).
cnf(t159,plain,
additive_inverse(add(X1,additive_inverse(X2))) = add(X2,additive_inverse(X1)),
inference(orient,[status(thm)],[t158]) ).
cnf(t161,plain,
add(X1,additive_inverse(add(X2,X3))) = additive_inverse(add(X2,add(X3,additive_inverse(X1)))),
inference(cp,[status(thm)],[t159,t37]) ).
cnf(t734,plain,
additive_inverse(add(X1,add(X2,additive_inverse(X3)))) = add(X3,additive_inverse(add(X1,X2))),
inference(orient,[status(thm)],[t161]) ).
cnf(t735,plain,
add(X1,additive_inverse(add(X1,X2))) = additive_inverse(X2),
inference(cp,[status(thm)],[t734,t123]) ).
cnf(t751,plain,
add(X1,additive_inverse(add(X1,X2))) = additive_inverse(X2),
inference(orient,[status(thm)],[t735]) ).
cnf(t25176,plain,
add(multiply(X1,X2),commutator(additive_inverse(add(X2,X3)),X1)) = add(multiply(additive_inverse(add(X2,X3)),additive_inverse(X1)),multiply(X1,additive_inverse(X3))),
inference(cp,[status(thm)],[t25032,t751]) ).
cnf(t2908,plain,
commutator(X1,additive_inverse(X2)) = add(multiply(additive_inverse(X2),X1),multiply(X1,X2)),
inference(cp,[status(thm)],[t46,t2888]) ).
cnf(t130949,plain,
commutator(X1,additive_inverse(X2)) = add(multiply(X1,X2),multiply(additive_inverse(X2),X1)),
inference(step,[status(thm)],[t2908,t36]) ).
cnf(t3383,plain,
add(multiply(X1,X2),multiply(additive_inverse(X2),X1)) = commutator(X1,additive_inverse(X2)),
inference(orient,[status(thm)],[t130949]) ).
cnf(t40,plain,
add(multiply(X1,X2),add(multiply(X3,X2),Y3)) = add(multiply(add(X1,X3),X2),Y3),
inference(cp,[status(thm)],[t37,t29]) ).
cnf(t1220,plain,
add(multiply(X1,X2),add(multiply(X3,X2),Y3)) = add(multiply(add(X1,X3),X2),Y3),
inference(orient,[status(thm)],[t40]) ).
cnf(t1248,plain,
add(multiply(add(X1,X2),X3),additive_inverse(multiply(X2,X3))) = add(multiply(X1,X3),additive_identity),
inference(cp,[status(thm)],[t1220,t42]) ).
cnf(t131000,plain,
add(additive_inverse(multiply(X2,X3)),multiply(add(X1,X2),X3)) = add(multiply(X1,X3),additive_identity),
inference(step,[status(thm)],[t1248,t36]) ).
cnf(t131001,plain,
add(multiply(X2,additive_inverse(X3)),multiply(add(X1,X2),X3)) = add(multiply(X1,X3),additive_identity),
inference(step,[status(thm)],[t131000,t3035]) ).
cnf(t131002,plain,
add(multiply(X2,additive_inverse(X3)),multiply(add(X1,X2),X3)) = multiply(X1,X3),
inference(step,[status(thm)],[t131001,t16]) ).
cnf(t4422,plain,
add(multiply(X1,additive_inverse(X2)),multiply(add(X3,X1),X2)) = multiply(X3,X2),
inference(orient,[status(thm)],[t131002]) ).
cnf(t4482,plain,
multiply(X1,X2) = add(multiply(additive_inverse(X1),additive_inverse(X2)),multiply(additive_identity,X2)),
inference(cp,[status(thm)],[t4422,t42]) ).
cnf(t131003,plain,
multiply(X1,X2) = add(multiply(additive_identity,X2),multiply(additive_inverse(X1),additive_inverse(X2))),
inference(step,[status(thm)],[t4482,t36]) ).
cnf(t4,axiom,
multiply(additive_identity,X1) = additive_identity,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t35,plain,
multiply(additive_identity,X1) = additive_identity,
inference(orient,[status(thm)],[t4]) ).
cnf(t131004,plain,
multiply(X1,X2) = add(additive_identity,multiply(additive_inverse(X1),additive_inverse(X2))),
inference(step,[status(thm)],[t131003,t35]) ).
cnf(t131005,plain,
multiply(X1,X2) = multiply(additive_inverse(X1),additive_inverse(X2)),
inference(step,[status(thm)],[t131004,t17]) ).
cnf(t4526,plain,
multiply(additive_inverse(X1),additive_inverse(X2)) = multiply(X1,X2),
inference(orient,[status(thm)],[t131005]) ).
cnf(t4571,plain,
commutator(additive_inverse(X1),additive_inverse(additive_inverse(X2))) = add(multiply(X1,X2),multiply(additive_inverse(additive_inverse(X2)),additive_inverse(X1))),
inference(cp,[status(thm)],[t3383,t4526]) ).
cnf(t131014,plain,
commutator(additive_inverse(X1),X2) = add(multiply(X1,X2),multiply(additive_inverse(additive_inverse(X2)),additive_inverse(X1))),
inference(step,[status(thm)],[t4571,t18]) ).
cnf(t131015,plain,
commutator(additive_inverse(X1),X2) = add(multiply(X1,X2),multiply(additive_inverse(X2),X1)),
inference(step,[status(thm)],[t131014,t4526]) ).
cnf(t131016,plain,
commutator(additive_inverse(X1),X2) = commutator(X1,additive_inverse(X2)),
inference(step,[status(thm)],[t131015,t3383]) ).
cnf(t4664,plain,
commutator(additive_inverse(X1),X2) = commutator(X1,additive_inverse(X2)),
inference(orient,[status(thm)],[t131016]) ).
cnf(t4539,plain,
multiply(additive_inverse(X1),X2) = multiply(X1,additive_inverse(X2)),
inference(cp,[status(thm)],[t4526,t18]) ).
cnf(t4603,plain,
multiply(additive_inverse(X1),X2) = multiply(X1,additive_inverse(X2)),
inference(orient,[status(thm)],[t4539]) ).
cnf(t131012,plain,
add(multiply(X1,X2),multiply(X2,additive_inverse(X1))) = commutator(X1,additive_inverse(X2)),
inference(step,[status(thm)],[t3383,t4603]) ).
cnf(t131013,plain,
commutator(X2,X1) = commutator(X1,additive_inverse(X2)),
inference(step,[status(thm)],[t131012,t4112]) ).
cnf(t4663,plain,
commutator(X2,X1) = commutator(X1,additive_inverse(X2)),
inference(rw,[status(thm)],[t131013]) ).
cnf(t4685,plain,
commutator(X1,additive_inverse(X2)) = commutator(X2,X1),
inference(orient,[status(thm)],[t4663]) ).
cnf(t131018,plain,
commutator(additive_inverse(X1),X2) = commutator(X2,X1),
inference(step,[status(thm)],[t4664,t4685]) ).
cnf(t4686,plain,
commutator(additive_inverse(X1),X2) = commutator(X2,X1),
inference(orient,[status(thm)],[t131018]) ).
cnf(t131352,plain,
add(multiply(X1,X2),commutator(X1,add(X2,X3))) = add(multiply(additive_inverse(add(X2,X3)),additive_inverse(X1)),multiply(X1,additive_inverse(X3))),
inference(step,[status(thm)],[t25176,t4686]) ).
cnf(t2913,plain,
add(multiply(X1,additive_inverse(X2)),additive_inverse(X3)) = additive_inverse(add(X3,multiply(X1,X2))),
inference(cp,[status(thm)],[t159,t2888]) ).
cnf(t3297,plain,
add(multiply(X1,additive_inverse(X2)),additive_inverse(X3)) = additive_inverse(add(X3,multiply(X1,X2))),
inference(orient,[status(thm)],[t2913]) ).
cnf(t3321,plain,
additive_inverse(add(multiply(X1,X2),multiply(X3,Y3))) = add(multiply(X3,additive_inverse(Y3)),multiply(X1,additive_inverse(X2))),
inference(cp,[status(thm)],[t3297,t3035]) ).
cnf(t41238,plain,
add(multiply(X1,additive_inverse(X2)),multiply(X3,additive_inverse(Y3))) = additive_inverse(add(multiply(X3,Y3),multiply(X1,X2))),
inference(orient,[status(thm)],[t3321]) ).
cnf(t131353,plain,
add(multiply(X1,X2),commutator(X1,add(X2,X3))) = additive_inverse(add(multiply(X1,X3),multiply(additive_inverse(add(X2,X3)),X1))),
inference(step,[status(thm)],[t131352,t41238]) ).
cnf(t131354,plain,
add(multiply(X1,X2),commutator(X1,add(X2,X3))) = additive_inverse(add(multiply(X1,X3),multiply(add(X2,X3),additive_inverse(X1)))),
inference(step,[status(thm)],[t131353,t4603]) ).
cnf(t163,plain,
add(additive_inverse(X1),additive_inverse(X2)) = additive_inverse(add(X2,X1)),
inference(cp,[status(thm)],[t159,t18]) ).
cnf(t173,plain,
add(additive_inverse(X1),additive_inverse(X2)) = additive_inverse(add(X2,X1)),
inference(orient,[status(thm)],[t163]) ).
cnf(t2906,plain,
additive_inverse(add(X1,multiply(X2,additive_inverse(X3)))) = add(multiply(X2,X3),additive_inverse(X1)),
inference(cp,[status(thm)],[t173,t2888]) ).
cnf(t3216,plain,
additive_inverse(add(X1,multiply(X2,additive_inverse(X3)))) = add(multiply(X2,X3),additive_inverse(X1)),
inference(orient,[status(thm)],[t2906]) ).
cnf(t131355,plain,
add(multiply(X1,X2),commutator(X1,add(X2,X3))) = add(multiply(add(X2,X3),X1),additive_inverse(multiply(X1,X3))),
inference(step,[status(thm)],[t131354,t3216]) ).
cnf(t131356,plain,
add(multiply(X1,X2),commutator(X1,add(X2,X3))) = add(additive_inverse(multiply(X1,X3)),multiply(add(X2,X3),X1)),
inference(step,[status(thm)],[t131355,t36]) ).
cnf(t131357,plain,
add(multiply(X1,X2),commutator(X1,add(X2,X3))) = add(multiply(X1,additive_inverse(X3)),multiply(add(X2,X3),X1)),
inference(step,[status(thm)],[t131356,t3035]) ).
cnf(t1239,plain,
add(multiply(add(X1,X2),X3),additive_inverse(multiply(X3,X2))) = add(multiply(X1,X3),commutator(X3,X2)),
inference(cp,[status(thm)],[t1220,t46]) ).
cnf(t131148,plain,
add(additive_inverse(multiply(X3,X2)),multiply(add(X1,X2),X3)) = add(multiply(X1,X3),commutator(X3,X2)),
inference(step,[status(thm)],[t1239,t36]) ).
cnf(t131149,plain,
add(multiply(X3,additive_inverse(X2)),multiply(add(X1,X2),X3)) = add(multiply(X1,X3),commutator(X3,X2)),
inference(step,[status(thm)],[t131148,t3035]) ).
cnf(t25490,plain,
add(multiply(X1,additive_inverse(X2)),multiply(add(X3,X2),X1)) = add(multiply(X3,X1),commutator(X1,X2)),
inference(orient,[status(thm)],[t131149]) ).
cnf(t131358,plain,
add(multiply(X1,X2),commutator(X1,add(X2,X3))) = add(multiply(X2,X1),commutator(X1,X3)),
inference(step,[status(thm)],[t131357,t25490]) ).
cnf(t44530,plain,
add(multiply(X1,X2),commutator(X1,add(X2,X3))) = add(multiply(X2,X1),commutator(X1,X3)),
inference(orient,[status(thm)],[t131358]) ).
cnf(t44714,plain,
add(multiply(X1,X2),commutator(X2,additive_inverse(add(X1,X3)))) = add(multiply(X2,X1),commutator(X2,additive_inverse(X3))),
inference(cp,[status(thm)],[t44530,t751]) ).
cnf(t131362,plain,
add(multiply(X1,X2),commutator(add(X1,X3),X2)) = add(multiply(X2,X1),commutator(X2,additive_inverse(X3))),
inference(step,[status(thm)],[t44714,t4685]) ).
cnf(t131363,plain,
add(multiply(X1,X2),commutator(add(X1,X3),X2)) = add(multiply(X2,X1),commutator(X3,X2)),
inference(step,[status(thm)],[t131362,t4685]) ).
cnf(t44964,plain,
add(multiply(X1,X2),commutator(add(X1,X3),X2)) = add(multiply(X2,X1),commutator(X3,X2)),
inference(orient,[status(thm)],[t131363]) ).
cnf(t54364,plain,
add(commutator(X1,X2),commutator(add(X1,X3),additive_inverse(X2))) = add(multiply(X2,X1),add(multiply(additive_inverse(X2),X1),commutator(X3,additive_inverse(X2)))),
inference(cp,[status(thm)],[t54224,t44964]) ).
cnf(t131447,plain,
add(commutator(X1,X2),commutator(X2,add(X1,X3))) = add(multiply(X2,X1),add(multiply(additive_inverse(X2),X1),commutator(X3,additive_inverse(X2)))),
inference(step,[status(thm)],[t54364,t4685]) ).
cnf(t131448,plain,
add(commutator(X1,X2),commutator(X2,add(X1,X3))) = add(multiply(add(X2,additive_inverse(X2)),X1),commutator(X3,additive_inverse(X2))),
inference(step,[status(thm)],[t131447,t1220]) ).
cnf(t131449,plain,
add(commutator(X1,X2),commutator(X2,add(X1,X3))) = add(multiply(additive_identity,X1),commutator(X3,additive_inverse(X2))),
inference(step,[status(thm)],[t131448,t42]) ).
cnf(t131450,plain,
add(commutator(X1,X2),commutator(X2,add(X1,X3))) = add(additive_identity,commutator(X3,additive_inverse(X2))),
inference(step,[status(thm)],[t131449,t35]) ).
cnf(t131451,plain,
add(commutator(X1,X2),commutator(X2,add(X1,X3))) = commutator(X3,additive_inverse(X2)),
inference(step,[status(thm)],[t131450,t17]) ).
cnf(t131452,plain,
add(commutator(X1,X2),commutator(X2,add(X1,X3))) = commutator(X2,X3),
inference(step,[status(thm)],[t131451,t4685]) ).
cnf(t54568,plain,
add(commutator(X1,X2),commutator(X2,add(X1,X3))) = commutator(X2,X3),
inference(orient,[status(thm)],[t131452]) ).
cnf(t54672,plain,
commutator(X1,add(additive_inverse(X2),X3)) = add(commutator(X2,X1),commutator(X1,X3)),
inference(cp,[status(thm)],[t54568,t116]) ).
cnf(t56963,plain,
add(commutator(X1,X2),commutator(X2,X3)) = commutator(X2,add(additive_inverse(X1),X3)),
inference(orient,[status(thm)],[t54672]) ).
cnf(t162,plain,
add(multiply(X1,X2),additive_inverse(multiply(X2,X1))) = additive_inverse(commutator(X1,X2)),
inference(cp,[status(thm)],[t159,t46]) ).
cnf(t130882,plain,
commutator(X2,X1) = additive_inverse(commutator(X1,X2)),
inference(step,[status(thm)],[t162,t46]) ).
cnf(t165,plain,
additive_inverse(commutator(X1,X2)) = commutator(X2,X1),
inference(orient,[status(thm)],[t130882]) ).
cnf(t58,plain,
associator(X1,X1,X1) = commutator(X1,multiply(X1,X1)),
inference(cp,[status(thm)],[t57,t46]) ).
cnf(t59,plain,
associator(X1,X2,X2) = add(multiply(X1,multiply(X2,X2)),additive_inverse(multiply(X1,multiply(X2,X2)))),
inference(cp,[status(thm)],[t57,t19]) ).
cnf(t130863,plain,
associator(X1,X2,X2) = additive_identity,
inference(step,[status(thm)],[t59,t42]) ).
cnf(t79,plain,
associator(X1,X2,X2) = additive_identity,
inference(orient,[status(thm)],[t130863]) ).
cnf(t130878,plain,
additive_identity = commutator(X1,multiply(X1,X1)),
inference(step,[status(thm)],[t58,t79]) ).
cnf(t84,plain,
commutator(X1,multiply(X1,X1)) = additive_identity,
inference(orient,[status(thm)],[t130878]) ).
cnf(t166,plain,
commutator(multiply(X1,X1),X1) = additive_inverse(additive_identity),
inference(cp,[status(thm)],[t165,t84]) ).
cnf(t44,plain,
additive_identity = additive_inverse(additive_identity),
inference(cp,[status(thm)],[t42,t17]) ).
cnf(t75,plain,
additive_inverse(additive_identity) = additive_identity,
inference(orient,[status(thm)],[t44]) ).
cnf(t130883,plain,
commutator(multiply(X1,X1),X1) = additive_identity,
inference(step,[status(thm)],[t166,t75]) ).
cnf(t171,plain,
commutator(multiply(X1,X1),X1) = additive_identity,
inference(orient,[status(thm)],[t130883]) ).
cnf(t57008,plain,
commutator(X1,add(additive_inverse(multiply(X1,X1)),X2)) = add(additive_identity,commutator(X1,X2)),
inference(cp,[status(thm)],[t56963,t171]) ).
cnf(t131481,plain,
commutator(X1,add(multiply(X1,additive_inverse(X1)),X2)) = add(additive_identity,commutator(X1,X2)),
inference(step,[status(thm)],[t57008,t3035]) ).
cnf(t131482,plain,
commutator(X1,add(multiply(X1,additive_inverse(X1)),X2)) = commutator(X1,X2),
inference(step,[status(thm)],[t131481,t17]) ).
cnf(t57326,plain,
commutator(X1,add(multiply(X1,additive_inverse(X1)),X2)) = commutator(X1,X2),
inference(orient,[status(thm)],[t131482]) ).
cnf(t57342,plain,
commutator(X1,multiply(X1,add(X2,X1))) = commutator(X1,add(multiply(X1,X2),commutator(X1,X1))),
inference(cp,[status(thm)],[t57326,t25032]) ).
cnf(t47,plain,
commutator(X1,X1) = additive_identity,
inference(cp,[status(thm)],[t46,t42]) ).
cnf(t76,plain,
commutator(X1,X1) = additive_identity,
inference(orient,[status(thm)],[t47]) ).
cnf(t131511,plain,
commutator(X1,multiply(X1,add(X2,X1))) = commutator(X1,add(multiply(X1,X2),additive_identity)),
inference(step,[status(thm)],[t57342,t76]) ).
cnf(t131512,plain,
commutator(X1,multiply(X1,add(X2,X1))) = commutator(X1,multiply(X1,X2)),
inference(step,[status(thm)],[t131511,t16]) ).
cnf(t58190,plain,
commutator(X1,multiply(X1,add(X2,X1))) = commutator(X1,multiply(X1,X2)),
inference(orient,[status(thm)],[t131512]) ).
cnf(t131985,plain,
commutator(X1,multiply(X1,X2)) = add(multiply(X1,multiply(add(X2,X1),X1)),multiply(X1,additive_inverse(multiply(X1,add(X2,X1))))),
inference(step,[status(thm)],[t128711,t58190]) ).
cnf(t131986,plain,
commutator(X1,multiply(X1,X2)) = multiply(X1,add(multiply(add(X2,X1),X1),additive_inverse(multiply(X1,add(X2,X1))))),
inference(step,[status(thm)],[t131985,t24]) ).
cnf(t131987,plain,
commutator(X1,multiply(X1,X2)) = multiply(X1,add(multiply(add(X2,X1),X1),multiply(X1,additive_inverse(add(X2,X1))))),
inference(step,[status(thm)],[t131986,t3035]) ).
cnf(t131988,plain,
commutator(X1,multiply(X1,X2)) = multiply(X1,commutator(X1,add(X2,X1))),
inference(step,[status(thm)],[t131987,t4112]) ).
cnf(t1186,plain,
add(multiply(X1,add(X2,X3)),multiply(Y3,X3)) = add(multiply(X1,X2),multiply(add(X1,Y3),X3)),
inference(cp,[status(thm)],[t1166,t29]) ).
cnf(t7607,plain,
add(multiply(X1,add(X2,X3)),multiply(Y3,X3)) = add(multiply(X1,X2),multiply(add(X1,Y3),X3)),
inference(orient,[status(thm)],[t1186]) ).
cnf(t7608,plain,
add(multiply(X1,X2),multiply(add(X1,add(X2,additive_inverse(X1))),additive_inverse(X1))) = commutator(add(X2,additive_inverse(X1)),X1),
inference(cp,[status(thm)],[t7607,t4112]) ).
cnf(t131052,plain,
add(multiply(X1,X2),multiply(X2,additive_inverse(X1))) = commutator(add(X2,additive_inverse(X1)),X1),
inference(step,[status(thm)],[t7608,t123]) ).
cnf(t131053,plain,
commutator(X2,X1) = commutator(add(X2,additive_inverse(X1)),X1),
inference(step,[status(thm)],[t131052,t4112]) ).
cnf(t4696,plain,
commutator(add(X1,additive_inverse(X2)),X3) = commutator(X3,add(X2,additive_inverse(X1))),
inference(cp,[status(thm)],[t4685,t159]) ).
cnf(t5748,plain,
commutator(add(X1,additive_inverse(X2)),X3) = commutator(X3,add(X2,additive_inverse(X1))),
inference(orient,[status(thm)],[t4696]) ).
cnf(t131054,plain,
commutator(X2,X1) = commutator(X1,add(X1,additive_inverse(X2))),
inference(step,[status(thm)],[t131053,t5748]) ).
cnf(t7888,plain,
commutator(X1,add(X1,additive_inverse(X2))) = commutator(X2,X1),
inference(orient,[status(thm)],[t131054]) ).
cnf(t7890,plain,
commutator(X1,additive_inverse(X2)) = commutator(add(additive_inverse(X2),additive_inverse(X1)),X2),
inference(cp,[status(thm)],[t7888,t4686]) ).
cnf(t131055,plain,
commutator(X2,X1) = commutator(add(additive_inverse(X2),additive_inverse(X1)),X2),
inference(step,[status(thm)],[t7890,t4685]) ).
cnf(t131056,plain,
commutator(X2,X1) = commutator(additive_inverse(add(X1,X2)),X2),
inference(step,[status(thm)],[t131055,t173]) ).
cnf(t131057,plain,
commutator(X2,X1) = commutator(X2,add(X1,X2)),
inference(step,[status(thm)],[t131056,t4686]) ).
cnf(t7929,plain,
commutator(X1,add(X2,X1)) = commutator(X1,X2),
inference(orient,[status(thm)],[t131057]) ).
cnf(t131989,plain,
commutator(X1,multiply(X1,X2)) = multiply(X1,commutator(X1,X2)),
inference(step,[status(thm)],[t131988,t7929]) ).
cnf(t128895,plain,
commutator(X1,multiply(X1,X2)) = multiply(X1,commutator(X1,X2)),
inference(orient,[status(thm)],[t131989]) ).
cnf(t129070,plain,
multiply(multiply(X1,X2),X1) = add(multiply(X1,multiply(X1,X2)),multiply(X1,commutator(X1,X2))),
inference(cp,[status(thm)],[t224,t128895]) ).
cnf(t131994,plain,
multiply(multiply(X1,X2),X1) = multiply(X1,add(multiply(X1,X2),commutator(X1,X2))),
inference(step,[status(thm)],[t129070,t24]) ).
cnf(t131995,plain,
multiply(multiply(X1,X2),X1) = multiply(X1,multiply(X2,X1)),
inference(step,[status(thm)],[t131994,t224]) ).
cnf(t129402,plain,
multiply(multiply(X1,X2),X1) = multiply(X1,multiply(X2,X1)),
inference(orient,[status(thm)],[t131995]) ).
cnf(t129752,plain,
add(associator(X1,X2,X1),X3) = add(multiply(X1,multiply(X2,X1)),add(multiply(X1,multiply(X2,additive_inverse(X1))),X3)),
inference(cp,[status(thm)],[t119562,t129402]) ).
cnf(t131999,plain,
add(associator(X1,X2,X1),X3) = add(multiply(X1,add(multiply(X2,X1),multiply(X2,additive_inverse(X1)))),X3),
inference(step,[status(thm)],[t129752,t1166]) ).
cnf(t4558,plain,
multiply(add(additive_inverse(X1),X2),additive_inverse(X3)) = add(multiply(X1,X3),multiply(X2,additive_inverse(X3))),
inference(cp,[status(thm)],[t29,t4526]) ).
cnf(t5436,plain,
add(multiply(X1,X2),multiply(X3,additive_inverse(X2))) = multiply(add(additive_inverse(X1),X3),additive_inverse(X2)),
inference(orient,[status(thm)],[t4558]) ).
cnf(t757,plain,
add(add(X1,X2),additive_inverse(add(X3,X1))) = additive_inverse(add(X3,additive_inverse(X2))),
inference(cp,[status(thm)],[t734,t751]) ).
cnf(t130906,plain,
add(X1,add(X2,additive_inverse(add(X3,X1)))) = additive_inverse(add(X3,additive_inverse(X2))),
inference(step,[status(thm)],[t757,t37]) ).
cnf(t151,plain,
additive_inverse(add(X1,X2)) = add(X3,additive_inverse(add(X1,add(X2,X3)))),
inference(cp,[status(thm)],[t148,t37]) ).
cnf(t717,plain,
add(X1,additive_inverse(add(X2,add(X3,X1)))) = additive_inverse(add(X2,X3)),
inference(orient,[status(thm)],[t151]) ).
cnf(t38,plain,
add(X1,add(X2,X3)) = add(X3,add(X1,X2)),
inference(cp,[status(thm)],[t37,t36]) ).
cnf(t108,plain,
add(X1,add(X2,X3)) = add(X3,add(X1,X2)),
inference(orient,[status(thm)],[t38]) ).
cnf(t721,plain,
additive_inverse(add(X1,X2)) = add(X3,additive_inverse(add(X2,add(X3,X1)))),
inference(cp,[status(thm)],[t717,t108]) ).
cnf(t814,plain,
add(X1,additive_inverse(add(X2,add(X1,X3)))) = additive_inverse(add(X3,X2)),
inference(orient,[status(thm)],[t721]) ).
cnf(t816,plain,
additive_inverse(add(additive_inverse(X1),X2)) = add(X3,add(X1,additive_inverse(add(X2,X3)))),
inference(cp,[status(thm)],[t814,t734]) ).
cnf(t1329,plain,
add(X1,add(X2,additive_inverse(add(X3,X1)))) = additive_inverse(add(additive_inverse(X2),X3)),
inference(orient,[status(thm)],[t816]) ).
cnf(t130907,plain,
additive_inverse(add(additive_inverse(X2),X3)) = additive_inverse(add(X3,additive_inverse(X2))),
inference(step,[status(thm)],[t130906,t1329]) ).
cnf(t130908,plain,
additive_inverse(add(additive_inverse(X2),X3)) = add(X2,additive_inverse(X3)),
inference(step,[status(thm)],[t130907,t159]) ).
cnf(t1425,plain,
additive_inverse(add(additive_inverse(X1),X2)) = add(X1,additive_inverse(X2)),
inference(orient,[status(thm)],[t130908]) ).
cnf(t4614,plain,
multiply(add(additive_inverse(X1),X2),additive_inverse(X3)) = multiply(add(X1,additive_inverse(X2)),X3),
inference(cp,[status(thm)],[t4603,t1425]) ).
cnf(t10705,plain,
multiply(add(additive_inverse(X1),X2),additive_inverse(X3)) = multiply(add(X1,additive_inverse(X2)),X3),
inference(orient,[status(thm)],[t4614]) ).
cnf(t131074,plain,
add(multiply(X1,X2),multiply(X3,additive_inverse(X2))) = multiply(add(X1,additive_inverse(X3)),X2),
inference(step,[status(thm)],[t5436,t10705]) ).
cnf(t10706,plain,
add(multiply(X1,X2),multiply(X3,additive_inverse(X2))) = multiply(add(X1,additive_inverse(X3)),X2),
inference(orient,[status(thm)],[t131074]) ).
cnf(t132000,plain,
add(associator(X1,X2,X1),X3) = add(multiply(X1,multiply(add(X2,additive_inverse(X2)),X1)),X3),
inference(step,[status(thm)],[t131999,t10706]) ).
cnf(t132001,plain,
add(associator(X1,X2,X1),X3) = add(multiply(X1,multiply(additive_identity,X1)),X3),
inference(step,[status(thm)],[t132000,t42]) ).
cnf(t132002,plain,
add(associator(X1,X2,X1),X3) = add(multiply(X1,additive_identity),X3),
inference(step,[status(thm)],[t132001,t35]) ).
cnf(t132003,plain,
add(associator(X1,X2,X1),X3) = add(additive_identity,X3),
inference(step,[status(thm)],[t132002,t27]) ).
cnf(t132004,plain,
add(associator(X1,X2,X1),X3) = X3,
inference(step,[status(thm)],[t132003,t17]) ).
cnf(t129842,plain,
add(associator(X1,X2,X1),X3) = X3,
inference(orient,[status(thm)],[t132004]) ).
cnf(t129868,plain,
X1 = add(sFlat0,X1),
inference(cp,[status(thm)],[t129842,t74]) ).
cnf(t130353,plain,
add(sFlat0,X1) = X1,
inference(orient,[status(thm)],[t129868]) ).
cnf(t130367,plain,
additive_identity = sFlat0,
inference(cp,[status(thm)],[t130353,t16]) ).
cnf(t130689,plain,
additive_identity = sFlat0,
inference(orient,[status(thm)],[t130367]) ).
cnf(goal_0,negated_conjecture,
associator(x,y,x) != additive_identity,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
sFlat0 != additive_identity,
inference(rw,[status(thm)],[goal_0,t74]) ).
cnf(g0_1,plain,
sFlat0 != sFlat0,
inference(rw,[status(thm)],[g0_0,t130689]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : RNG025-6 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.38 % Computer : n016.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Thu Sep 24 07:53:43 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 209.42/27.39 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 209.42/27.39 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------