%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : RNG009-5 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n008.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:26 PM UTC 2026
% Result : Unsatisfiable 50.39s 7.07s
% Output : CNFRefutation 11.43s
% Verified :
% SZS Type : Refutation
% Derivation depth : 202
% Number of leaves : 9
% Syntax : Number of clauses : 533 ( 533 unt; 0 nHn; 8 RR)
% Number of literals : 533 ( 532 equ; 2 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 3 con; 0-2 aty)
% Number of variables : 1237 ( 12 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t7,axiom,
add(multiply(X1,X2),multiply(X3,X2)) = multiply(add(X1,X3),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t27,plain,
add(multiply(X1,X2),multiply(X3,X2)) = multiply(add(X1,X3),X2),
inference(orient,[status(thm)],[t7]) ).
cnf(t6,axiom,
add(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,add(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t33,plain,
add(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,add(X2,X3)),
inference(orient,[status(thm)],[t6]) ).
cnf(t5,axiom,
multiply(multiply(X1,X2),X3) = multiply(X1,multiply(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t40,plain,
multiply(multiply(X1,X2),X3) = multiply(X1,multiply(X2,X3)),
inference(orient,[status(thm)],[t5]) ).
cnf(t44,plain,
multiply(add(multiply(X1,X2),X3),Y3) = add(multiply(X1,multiply(X2,Y3)),multiply(X3,Y3)),
inference(cp,[status(thm)],[t27,t40]) ).
cnf(t2,axiom,
add(X1,X2) = add(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t10,plain,
add(X1,X2) = add(X2,X1),
inference(orient,[status(thm)],[t2]) ).
cnf(t123785,plain,
multiply(add(X3,multiply(X1,X2)),Y3) = add(multiply(X1,multiply(X2,Y3)),multiply(X3,Y3)),
inference(step,[status(thm)],[t44,t10]) ).
cnf(t123786,plain,
multiply(add(X3,multiply(X1,X2)),Y3) = add(multiply(X3,Y3),multiply(X1,multiply(X2,Y3))),
inference(step,[status(thm)],[t123785,t10]) ).
cnf(t627,plain,
add(multiply(X1,X2),multiply(X3,multiply(Y3,X2))) = multiply(add(X1,multiply(X3,Y3)),X2),
inference(orient,[status(thm)],[t123786]) ).
cnf(t628,plain,
multiply(add(X1,multiply(X1,X2)),X3) = multiply(X1,add(X3,multiply(X2,X3))),
inference(cp,[status(thm)],[t627,t33]) ).
cnf(t2243,plain,
multiply(add(X1,multiply(X1,X2)),X3) = multiply(X1,add(X3,multiply(X2,X3))),
inference(orient,[status(thm)],[t628]) ).
cnf(t3,axiom,
multiply(X1,multiply(X1,X1)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t9,plain,
multiply(X1,multiply(X1,X1)) = X1,
inference(orient,[status(thm)],[t3]) ).
cnf(t649,plain,
multiply(add(X1,multiply(X2,X2)),X2) = add(multiply(X1,X2),X2),
inference(cp,[status(thm)],[t627,t9]) ).
cnf(t123787,plain,
multiply(add(X1,multiply(X2,X2)),X2) = add(X2,multiply(X1,X2)),
inference(step,[status(thm)],[t649,t10]) ).
cnf(t684,plain,
multiply(add(X1,multiply(X2,X2)),X2) = add(X2,multiply(X1,X2)),
inference(orient,[status(thm)],[t123787]) ).
cnf(t695,plain,
multiply(add(add(X1,multiply(X2,X2)),X3),X2) = add(add(X2,multiply(X1,X2)),multiply(X3,X2)),
inference(cp,[status(thm)],[t27,t684]) ).
cnf(t123837,plain,
multiply(add(X3,add(X1,multiply(X2,X2))),X2) = add(add(X2,multiply(X1,X2)),multiply(X3,X2)),
inference(step,[status(thm)],[t695,t10]) ).
cnf(t4,axiom,
add(add(X1,X2),X3) = add(X1,add(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t123729,plain,
add(X3,add(X1,X2)) = add(X1,add(X2,X3)),
inference(step,[status(thm)],[t4,t10]) ).
cnf(t12,plain,
add(X1,add(X2,X3)) = add(X2,add(X3,X1)),
inference(orient,[status(thm)],[t123729]) ).
cnf(t123838,plain,
multiply(add(X1,add(multiply(X2,X2),X3)),X2) = add(add(X2,multiply(X1,X2)),multiply(X3,X2)),
inference(step,[status(thm)],[t123837,t12]) ).
cnf(t123839,plain,
multiply(add(X1,add(X3,multiply(X2,X2))),X2) = add(add(X2,multiply(X1,X2)),multiply(X3,X2)),
inference(step,[status(thm)],[t123838,t10]) ).
cnf(t123840,plain,
multiply(add(X1,add(X3,multiply(X2,X2))),X2) = add(multiply(X3,X2),add(X2,multiply(X1,X2))),
inference(step,[status(thm)],[t123839,t10]) ).
cnf(t123841,plain,
multiply(add(X1,add(X3,multiply(X2,X2))),X2) = add(multiply(X1,X2),add(multiply(X3,X2),X2)),
inference(step,[status(thm)],[t123840,t12]) ).
cnf(t123842,plain,
multiply(add(X1,add(X3,multiply(X2,X2))),X2) = add(X2,add(multiply(X1,X2),multiply(X3,X2))),
inference(step,[status(thm)],[t123841,t12]) ).
cnf(t123843,plain,
multiply(add(X1,add(X3,multiply(X2,X2))),X2) = add(X2,multiply(add(X1,X3),X2)),
inference(step,[status(thm)],[t123842,t27]) ).
cnf(t1505,plain,
multiply(add(X1,add(X2,multiply(X3,X3))),X3) = add(X3,multiply(add(X1,X2),X3)),
inference(orient,[status(thm)],[t123843]) ).
cnf(t1515,plain,
add(X1,multiply(add(X2,multiply(X1,X3)),X1)) = multiply(add(X2,multiply(X1,add(X3,X1))),X1),
inference(cp,[status(thm)],[t1505,t33]) ).
cnf(t123853,plain,
add(X1,multiply(add(X2,multiply(X1,X3)),X1)) = multiply(add(X2,multiply(X1,add(X1,X3))),X1),
inference(step,[status(thm)],[t1515,t10]) ).
cnf(t1930,plain,
add(X1,multiply(add(X2,multiply(X1,X3)),X1)) = multiply(add(X2,multiply(X1,add(X1,X3))),X1),
inference(orient,[status(thm)],[t123853]) ).
cnf(t1942,plain,
multiply(add(multiply(X1,X2),multiply(X3,add(X3,X2))),X3) = add(X3,multiply(multiply(add(X1,X3),X2),X3)),
inference(cp,[status(thm)],[t1930,t27]) ).
cnf(t124034,plain,
multiply(add(multiply(X1,X2),multiply(X3,add(X2,X3))),X3) = add(X3,multiply(multiply(add(X1,X3),X2),X3)),
inference(step,[status(thm)],[t1942,t10]) ).
cnf(t124035,plain,
multiply(add(multiply(X1,X2),multiply(X3,add(X2,X3))),X3) = add(X3,multiply(add(X1,X3),multiply(X2,X3))),
inference(step,[status(thm)],[t124034,t40]) ).
cnf(t12943,plain,
multiply(add(multiply(X1,X2),multiply(X3,add(X2,X3))),X3) = add(X3,multiply(add(X1,X3),multiply(X2,X3))),
inference(orient,[status(thm)],[t124035]) ).
cnf(t1,axiom,
add(X1,additive_inverse(X1)) = additive_identity,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t24,plain,
add(X1,additive_inverse(X1)) = additive_identity,
inference(orient,[status(thm)],[t1]) ).
cnf(t13082,plain,
add(additive_inverse(X1),multiply(add(X2,additive_inverse(X1)),multiply(X1,additive_inverse(X1)))) = multiply(add(multiply(X2,X1),multiply(additive_inverse(X1),additive_identity)),additive_inverse(X1)),
inference(cp,[status(thm)],[t12943,t24]) ).
cnf(t42,plain,
multiply(X1,multiply(multiply(X1,X1),X2)) = multiply(X1,X2),
inference(cp,[status(thm)],[t40,t9]) ).
cnf(t123732,plain,
multiply(X1,multiply(X1,multiply(X1,X2))) = multiply(X1,X2),
inference(step,[status(thm)],[t42,t40]) ).
cnf(t51,plain,
multiply(X1,multiply(X1,multiply(X1,X2))) = multiply(X1,X2),
inference(orient,[status(thm)],[t123732]) ).
cnf(t34,plain,
multiply(X1,add(X2,X2)) = multiply(add(X1,X1),X2),
inference(cp,[status(thm)],[t33,t27]) ).
cnf(t149,plain,
multiply(X1,add(X2,X2)) = multiply(add(X1,X1),X2),
inference(orient,[status(thm)],[t34]) ).
cnf(t0,axiom,
add(X1,additive_identity) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t8,plain,
add(X1,additive_identity) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t168,plain,
multiply(additive_identity,add(X1,X1)) = multiply(additive_identity,X1),
inference(cp,[status(thm)],[t149,t8]) ).
cnf(t181,plain,
multiply(additive_identity,add(X1,X1)) = multiply(additive_identity,X1),
inference(orient,[status(thm)],[t168]) ).
cnf(t187,plain,
multiply(additive_identity,add(add(X1,X1),X2)) = add(multiply(additive_identity,X1),multiply(additive_identity,X2)),
inference(cp,[status(thm)],[t33,t181]) ).
cnf(t123743,plain,
multiply(additive_identity,add(X2,add(X1,X1))) = add(multiply(additive_identity,X1),multiply(additive_identity,X2)),
inference(step,[status(thm)],[t187,t10]) ).
cnf(t123744,plain,
multiply(additive_identity,add(X1,add(X2,X1))) = add(multiply(additive_identity,X1),multiply(additive_identity,X2)),
inference(step,[status(thm)],[t123743,t12]) ).
cnf(t123745,plain,
multiply(additive_identity,add(X1,add(X1,X2))) = add(multiply(additive_identity,X1),multiply(additive_identity,X2)),
inference(step,[status(thm)],[t123744,t12]) ).
cnf(t123746,plain,
multiply(additive_identity,add(X1,add(X1,X2))) = multiply(additive_identity,add(X1,X2)),
inference(step,[status(thm)],[t123745,t33]) ).
cnf(t210,plain,
multiply(additive_identity,add(X1,add(X1,X2))) = multiply(additive_identity,add(X1,X2)),
inference(orient,[status(thm)],[t123746]) ).
cnf(t25,plain,
add(X1,add(additive_inverse(X1),X2)) = add(X2,additive_identity),
inference(cp,[status(thm)],[t12,t24]) ).
cnf(t123730,plain,
add(X1,add(X2,additive_inverse(X1))) = add(X2,additive_identity),
inference(step,[status(thm)],[t25,t10]) ).
cnf(t123731,plain,
add(X1,add(X2,additive_inverse(X1))) = X2,
inference(step,[status(thm)],[t123730,t8]) ).
cnf(t46,plain,
add(X1,add(X2,additive_inverse(X1))) = X2,
inference(orient,[status(thm)],[t123731]) ).
cnf(t211,plain,
multiply(additive_identity,add(X1,additive_inverse(X1))) = multiply(additive_identity,X1),
inference(cp,[status(thm)],[t210,t46]) ).
cnf(t123747,plain,
multiply(additive_identity,additive_identity) = multiply(additive_identity,X1),
inference(step,[status(thm)],[t211,t24]) ).
cnf(t233,plain,
multiply(additive_identity,additive_identity) = multiply(additive_identity,X1),
inference(orient,[status(thm)],[t123747]) ).
cnf(t263,plain,
multiply(additive_identity,X1) = multiply(additive_identity,multiply(additive_identity,additive_identity)),
inference(cp,[status(thm)],[t51,t233]) ).
cnf(t123750,plain,
multiply(additive_identity,X1) = additive_identity,
inference(step,[status(thm)],[t263,t9]) ).
cnf(t275,plain,
multiply(additive_identity,X1) = additive_identity,
inference(orient,[status(thm)],[t123750]) ).
cnf(t668,plain,
multiply(add(X1,multiply(X2,additive_identity)),X3) = add(multiply(X1,X3),multiply(X2,additive_identity)),
inference(cp,[status(thm)],[t627,t275]) ).
cnf(t708,plain,
add(multiply(X1,X2),multiply(X3,additive_identity)) = multiply(add(X1,multiply(X3,additive_identity)),X2),
inference(orient,[status(thm)],[t668]) ).
cnf(t124036,plain,
add(additive_inverse(X1),multiply(add(X2,additive_inverse(X1)),multiply(X1,additive_inverse(X1)))) = multiply(multiply(add(X2,multiply(additive_inverse(X1),additive_identity)),X1),additive_inverse(X1)),
inference(step,[status(thm)],[t13082,t708]) ).
cnf(t124037,plain,
add(additive_inverse(X1),multiply(add(X2,additive_inverse(X1)),multiply(X1,additive_inverse(X1)))) = multiply(add(X2,multiply(additive_inverse(X1),additive_identity)),multiply(X1,additive_inverse(X1))),
inference(step,[status(thm)],[t124036,t40]) ).
cnf(t709,plain,
multiply(add(X1,multiply(X2,additive_identity)),additive_identity) = multiply(add(X1,X2),additive_identity),
inference(cp,[status(thm)],[t708,t27]) ).
cnf(t749,plain,
multiply(add(X1,multiply(X2,additive_identity)),additive_identity) = multiply(add(X1,X2),additive_identity),
inference(orient,[status(thm)],[t709]) ).
cnf(t36,plain,
multiply(X1,add(multiply(X1,X1),X2)) = add(X1,multiply(X1,X2)),
inference(cp,[status(thm)],[t33,t9]) ).
cnf(t123733,plain,
multiply(X1,add(X2,multiply(X1,X1))) = add(X1,multiply(X1,X2)),
inference(step,[status(thm)],[t36,t10]) ).
cnf(t59,plain,
multiply(X1,add(X2,multiply(X1,X1))) = add(X1,multiply(X1,X2)),
inference(orient,[status(thm)],[t123733]) ).
cnf(t61,plain,
add(X1,multiply(X1,multiply(X2,X1))) = multiply(X1,multiply(add(X2,X1),X1)),
inference(cp,[status(thm)],[t59,t27]) ).
cnf(t123738,plain,
add(X1,multiply(X1,multiply(X2,X1))) = multiply(X1,multiply(add(X1,X2),X1)),
inference(step,[status(thm)],[t61,t10]) ).
cnf(t100,plain,
add(X1,multiply(X1,multiply(X2,X1))) = multiply(X1,multiply(add(X1,X2),X1)),
inference(orient,[status(thm)],[t123738]) ).
cnf(t277,plain,
multiply(X1,multiply(add(X1,additive_identity),X1)) = add(X1,multiply(X1,additive_identity)),
inference(cp,[status(thm)],[t100,t275]) ).
cnf(t123751,plain,
multiply(X1,multiply(X1,X1)) = add(X1,multiply(X1,additive_identity)),
inference(step,[status(thm)],[t277,t8]) ).
cnf(t123752,plain,
X1 = add(X1,multiply(X1,additive_identity)),
inference(step,[status(thm)],[t123751,t9]) ).
cnf(t279,plain,
add(X1,multiply(X1,additive_identity)) = X1,
inference(orient,[status(thm)],[t123752]) ).
cnf(t281,plain,
add(X1,add(multiply(X1,additive_identity),X2)) = add(X2,X1),
inference(cp,[status(thm)],[t12,t279]) ).
cnf(t123755,plain,
add(X1,add(X2,multiply(X1,additive_identity))) = add(X2,X1),
inference(step,[status(thm)],[t281,t10]) ).
cnf(t123756,plain,
add(X1,add(X2,multiply(X1,additive_identity))) = add(X1,X2),
inference(step,[status(thm)],[t123755,t10]) ).
cnf(t293,plain,
add(X1,add(X2,multiply(X1,additive_identity))) = add(X1,X2),
inference(orient,[status(thm)],[t123756]) ).
cnf(t295,plain,
add(X1,multiply(X2,additive_identity)) = add(X1,multiply(add(X2,X1),additive_identity)),
inference(cp,[status(thm)],[t293,t27]) ).
cnf(t123757,plain,
add(X1,multiply(X2,additive_identity)) = add(X1,multiply(add(X1,X2),additive_identity)),
inference(step,[status(thm)],[t295,t10]) ).
cnf(t301,plain,
add(X1,multiply(add(X1,X2),additive_identity)) = add(X1,multiply(X2,additive_identity)),
inference(orient,[status(thm)],[t123757]) ).
cnf(t309,plain,
add(X1,multiply(additive_inverse(X1),additive_identity)) = add(X1,multiply(additive_identity,additive_identity)),
inference(cp,[status(thm)],[t301,t24]) ).
cnf(t123758,plain,
add(X1,multiply(additive_inverse(X1),additive_identity)) = add(X1,additive_identity),
inference(step,[status(thm)],[t309,t275]) ).
cnf(t123759,plain,
add(X1,multiply(additive_inverse(X1),additive_identity)) = X1,
inference(step,[status(thm)],[t123758,t8]) ).
cnf(t317,plain,
add(X1,multiply(additive_inverse(X1),additive_identity)) = X1,
inference(orient,[status(thm)],[t123759]) ).
cnf(t752,plain,
multiply(add(X1,additive_inverse(X1)),additive_identity) = multiply(X1,additive_identity),
inference(cp,[status(thm)],[t749,t317]) ).
cnf(t123789,plain,
multiply(additive_identity,additive_identity) = multiply(X1,additive_identity),
inference(step,[status(thm)],[t752,t24]) ).
cnf(t123790,plain,
additive_identity = multiply(X1,additive_identity),
inference(step,[status(thm)],[t123789,t275]) ).
cnf(t787,plain,
multiply(X1,additive_identity) = additive_identity,
inference(orient,[status(thm)],[t123790]) ).
cnf(t124038,plain,
add(additive_inverse(X1),multiply(add(X2,additive_inverse(X1)),multiply(X1,additive_inverse(X1)))) = multiply(add(X2,additive_identity),multiply(X1,additive_inverse(X1))),
inference(step,[status(thm)],[t124037,t787]) ).
cnf(t124039,plain,
add(additive_inverse(X1),multiply(add(X2,additive_inverse(X1)),multiply(X1,additive_inverse(X1)))) = multiply(X2,multiply(X1,additive_inverse(X1))),
inference(step,[status(thm)],[t124038,t8]) ).
cnf(t13194,plain,
add(additive_inverse(X1),multiply(add(X2,additive_inverse(X1)),multiply(X1,additive_inverse(X1)))) = multiply(X2,multiply(X1,additive_inverse(X1))),
inference(orient,[status(thm)],[t124039]) ).
cnf(t13196,plain,
multiply(X1,multiply(X1,additive_inverse(X1))) = add(additive_inverse(X1),multiply(additive_identity,multiply(X1,additive_inverse(X1)))),
inference(cp,[status(thm)],[t13194,t24]) ).
cnf(t124040,plain,
multiply(X1,multiply(X1,additive_inverse(X1))) = add(additive_inverse(X1),additive_identity),
inference(step,[status(thm)],[t13196,t275]) ).
cnf(t124041,plain,
multiply(X1,multiply(X1,additive_inverse(X1))) = additive_inverse(X1),
inference(step,[status(thm)],[t124040,t8]) ).
cnf(t13224,plain,
multiply(X1,multiply(X1,additive_inverse(X1))) = additive_inverse(X1),
inference(orient,[status(thm)],[t124041]) ).
cnf(t13300,plain,
multiply(X1,add(X2,multiply(multiply(X1,additive_inverse(X1)),X2))) = multiply(add(X1,additive_inverse(X1)),X2),
inference(cp,[status(thm)],[t2243,t13224]) ).
cnf(t124065,plain,
multiply(X1,add(X2,multiply(X1,multiply(additive_inverse(X1),X2)))) = multiply(add(X1,additive_inverse(X1)),X2),
inference(step,[status(thm)],[t13300,t40]) ).
cnf(t124066,plain,
multiply(X1,add(X2,multiply(X1,multiply(additive_inverse(X1),X2)))) = multiply(additive_identity,X2),
inference(step,[status(thm)],[t124065,t24]) ).
cnf(t124067,plain,
multiply(X1,add(X2,multiply(X1,multiply(additive_inverse(X1),X2)))) = additive_identity,
inference(step,[status(thm)],[t124066,t275]) ).
cnf(t14342,plain,
multiply(X1,add(X2,multiply(X1,multiply(additive_inverse(X1),X2)))) = additive_identity,
inference(orient,[status(thm)],[t124067]) ).
cnf(t14404,plain,
multiply(X1,add(add(X2,multiply(X1,multiply(additive_inverse(X1),X2))),X3)) = add(additive_identity,multiply(X1,X3)),
inference(cp,[status(thm)],[t33,t14342]) ).
cnf(t124229,plain,
multiply(X1,add(X3,add(X2,multiply(X1,multiply(additive_inverse(X1),X2))))) = add(additive_identity,multiply(X1,X3)),
inference(step,[status(thm)],[t14404,t10]) ).
cnf(t124230,plain,
multiply(X1,add(X2,add(multiply(X1,multiply(additive_inverse(X1),X2)),X3))) = add(additive_identity,multiply(X1,X3)),
inference(step,[status(thm)],[t124229,t12]) ).
cnf(t124231,plain,
multiply(X1,add(X2,add(X3,multiply(X1,multiply(additive_inverse(X1),X2))))) = add(additive_identity,multiply(X1,X3)),
inference(step,[status(thm)],[t124230,t10]) ).
cnf(t276,plain,
multiply(add(additive_identity,X1),X2) = add(additive_identity,multiply(X1,X2)),
inference(cp,[status(thm)],[t27,t275]) ).
cnf(t123753,plain,
multiply(add(X1,additive_identity),X2) = add(additive_identity,multiply(X1,X2)),
inference(step,[status(thm)],[t276,t10]) ).
cnf(t123754,plain,
multiply(X1,X2) = add(additive_identity,multiply(X1,X2)),
inference(step,[status(thm)],[t123753,t8]) ).
cnf(t283,plain,
add(additive_identity,multiply(X1,X2)) = multiply(X1,X2),
inference(orient,[status(thm)],[t123754]) ).
cnf(t124232,plain,
multiply(X1,add(X2,add(X3,multiply(X1,multiply(additive_inverse(X1),X2))))) = multiply(X1,X3),
inference(step,[status(thm)],[t124231,t283]) ).
cnf(t25418,plain,
multiply(X1,add(X2,add(X3,multiply(X1,multiply(additive_inverse(X1),X2))))) = multiply(X1,X3),
inference(orient,[status(thm)],[t124232]) ).
cnf(t29,plain,
multiply(add(X1,X2),multiply(X1,X1)) = add(X1,multiply(X2,multiply(X1,X1))),
inference(cp,[status(thm)],[t27,t9]) ).
cnf(t80,plain,
add(X1,multiply(X2,multiply(X1,X1))) = multiply(add(X1,X2),multiply(X1,X1)),
inference(orient,[status(thm)],[t29]) ).
cnf(t83,plain,
multiply(add(X1,multiply(X2,X3)),multiply(X1,X1)) = add(X1,multiply(X2,multiply(X3,multiply(X1,X1)))),
inference(cp,[status(thm)],[t80,t40]) ).
cnf(t1184,plain,
add(X1,multiply(X2,multiply(X3,multiply(X1,X1)))) = multiply(add(X1,multiply(X2,X3)),multiply(X1,X1)),
inference(orient,[status(thm)],[t83]) ).
cnf(t66,plain,
multiply(X1,add(add(X2,multiply(X1,X1)),X3)) = add(add(X1,multiply(X1,X2)),multiply(X1,X3)),
inference(cp,[status(thm)],[t33,t59]) ).
cnf(t123815,plain,
multiply(X1,add(X3,add(X2,multiply(X1,X1)))) = add(add(X1,multiply(X1,X2)),multiply(X1,X3)),
inference(step,[status(thm)],[t66,t10]) ).
cnf(t123816,plain,
multiply(X1,add(X2,add(multiply(X1,X1),X3))) = add(add(X1,multiply(X1,X2)),multiply(X1,X3)),
inference(step,[status(thm)],[t123815,t12]) ).
cnf(t123817,plain,
multiply(X1,add(X2,add(X3,multiply(X1,X1)))) = add(add(X1,multiply(X1,X2)),multiply(X1,X3)),
inference(step,[status(thm)],[t123816,t10]) ).
cnf(t123818,plain,
multiply(X1,add(X2,add(X3,multiply(X1,X1)))) = add(multiply(X1,X3),add(X1,multiply(X1,X2))),
inference(step,[status(thm)],[t123817,t10]) ).
cnf(t123819,plain,
multiply(X1,add(X2,add(X3,multiply(X1,X1)))) = add(multiply(X1,X2),add(multiply(X1,X3),X1)),
inference(step,[status(thm)],[t123818,t12]) ).
cnf(t123820,plain,
multiply(X1,add(X2,add(X3,multiply(X1,X1)))) = add(X1,add(multiply(X1,X2),multiply(X1,X3))),
inference(step,[status(thm)],[t123819,t12]) ).
cnf(t123821,plain,
multiply(X1,add(X2,add(X3,multiply(X1,X1)))) = add(X1,multiply(X1,add(X2,X3))),
inference(step,[status(thm)],[t123820,t33]) ).
cnf(t1153,plain,
multiply(X1,add(X2,add(X3,multiply(X1,X1)))) = add(X1,multiply(X1,add(X2,X3))),
inference(orient,[status(thm)],[t123821]) ).
cnf(t1160,plain,
add(X1,multiply(X1,add(X2,multiply(X3,X1)))) = multiply(X1,add(X2,multiply(add(X3,X1),X1))),
inference(cp,[status(thm)],[t1153,t27]) ).
cnf(t123849,plain,
add(X1,multiply(X1,add(X2,multiply(X3,X1)))) = multiply(X1,add(X2,multiply(add(X1,X3),X1))),
inference(step,[status(thm)],[t1160,t10]) ).
cnf(t1725,plain,
add(X1,multiply(X1,add(X2,multiply(X3,X1)))) = multiply(X1,add(X2,multiply(add(X1,X3),X1))),
inference(orient,[status(thm)],[t123849]) ).
cnf(t1737,plain,
multiply(X1,add(multiply(X2,X3),multiply(add(X1,X2),X1))) = add(X1,multiply(X1,multiply(X2,add(X3,X1)))),
inference(cp,[status(thm)],[t1725,t33]) ).
cnf(t123949,plain,
multiply(X1,add(multiply(X2,X3),multiply(add(X1,X2),X1))) = add(X1,multiply(X1,multiply(X2,add(X1,X3)))),
inference(step,[status(thm)],[t1737,t10]) ).
cnf(t6917,plain,
multiply(X1,add(multiply(X2,X3),multiply(add(X1,X2),X1))) = add(X1,multiply(X1,multiply(X2,add(X1,X3)))),
inference(orient,[status(thm)],[t123949]) ).
cnf(t7020,plain,
add(X1,multiply(X1,multiply(additive_inverse(X1),add(X1,X2)))) = multiply(X1,add(multiply(additive_inverse(X1),X2),multiply(additive_identity,X1))),
inference(cp,[status(thm)],[t6917,t24]) ).
cnf(t123950,plain,
add(X1,multiply(X1,multiply(additive_inverse(X1),add(X1,X2)))) = multiply(X1,add(multiply(additive_identity,X1),multiply(additive_inverse(X1),X2))),
inference(step,[status(thm)],[t7020,t10]) ).
cnf(t123951,plain,
add(X1,multiply(X1,multiply(additive_inverse(X1),add(X1,X2)))) = multiply(X1,add(additive_identity,multiply(additive_inverse(X1),X2))),
inference(step,[status(thm)],[t123950,t275]) ).
cnf(t123952,plain,
add(X1,multiply(X1,multiply(additive_inverse(X1),add(X1,X2)))) = multiply(X1,multiply(additive_inverse(X1),X2)),
inference(step,[status(thm)],[t123951,t283]) ).
cnf(t7086,plain,
add(X1,multiply(X1,multiply(additive_inverse(X1),add(X1,X2)))) = multiply(X1,multiply(additive_inverse(X1),X2)),
inference(orient,[status(thm)],[t123952]) ).
cnf(t7110,plain,
multiply(X1,multiply(additive_inverse(X1),additive_inverse(X1))) = add(X1,multiply(X1,multiply(additive_inverse(X1),additive_identity))),
inference(cp,[status(thm)],[t7086,t24]) ).
cnf(t123953,plain,
multiply(X1,multiply(additive_inverse(X1),additive_inverse(X1))) = add(X1,multiply(X1,additive_identity)),
inference(step,[status(thm)],[t7110,t787]) ).
cnf(t123954,plain,
multiply(X1,multiply(additive_inverse(X1),additive_inverse(X1))) = add(X1,additive_identity),
inference(step,[status(thm)],[t123953,t787]) ).
cnf(t123955,plain,
multiply(X1,multiply(additive_inverse(X1),additive_inverse(X1))) = X1,
inference(step,[status(thm)],[t123954,t8]) ).
cnf(t7143,plain,
multiply(X1,multiply(additive_inverse(X1),additive_inverse(X1))) = X1,
inference(orient,[status(thm)],[t123955]) ).
cnf(t7182,plain,
multiply(add(additive_inverse(X1),multiply(X2,X1)),multiply(additive_inverse(X1),additive_inverse(X1))) = add(additive_inverse(X1),multiply(X2,X1)),
inference(cp,[status(thm)],[t1184,t7143]) ).
cnf(t11340,plain,
multiply(add(additive_inverse(X1),multiply(X2,X1)),multiply(additive_inverse(X1),additive_inverse(X1))) = add(additive_inverse(X1),multiply(X2,X1)),
inference(orient,[status(thm)],[t7182]) ).
cnf(t13227,plain,
multiply(X1,multiply(multiply(X1,additive_inverse(X1)),X2)) = multiply(additive_inverse(X1),X2),
inference(cp,[status(thm)],[t40,t13224]) ).
cnf(t124045,plain,
multiply(X1,multiply(X1,multiply(additive_inverse(X1),X2))) = multiply(additive_inverse(X1),X2),
inference(step,[status(thm)],[t13227,t40]) ).
cnf(t13392,plain,
multiply(X1,multiply(X1,multiply(additive_inverse(X1),X2))) = multiply(additive_inverse(X1),X2),
inference(orient,[status(thm)],[t124045]) ).
cnf(t7146,plain,
multiply(X1,multiply(multiply(additive_inverse(X1),additive_inverse(X1)),X2)) = multiply(X1,X2),
inference(cp,[status(thm)],[t40,t7143]) ).
cnf(t123956,plain,
multiply(X1,multiply(additive_inverse(X1),multiply(additive_inverse(X1),X2))) = multiply(X1,X2),
inference(step,[status(thm)],[t7146,t40]) ).
cnf(t7203,plain,
multiply(X1,multiply(additive_inverse(X1),multiply(additive_inverse(X1),X2))) = multiply(X1,X2),
inference(orient,[status(thm)],[t123956]) ).
cnf(t41,plain,
multiply(X1,multiply(X2,multiply(multiply(X1,X2),multiply(X1,X2)))) = multiply(X1,X2),
inference(cp,[status(thm)],[t40,t9]) ).
cnf(t123791,plain,
multiply(X1,multiply(X2,multiply(X1,multiply(X2,multiply(X1,X2))))) = multiply(X1,X2),
inference(step,[status(thm)],[t41,t40]) ).
cnf(t790,plain,
multiply(X1,multiply(X2,multiply(X1,multiply(X2,multiply(X1,X2))))) = multiply(X1,X2),
inference(orient,[status(thm)],[t123791]) ).
cnf(t7222,plain,
multiply(X1,multiply(X2,multiply(additive_inverse(X1),multiply(X2,multiply(additive_inverse(X1),X2))))) = multiply(X1,multiply(additive_inverse(X1),multiply(additive_inverse(X1),X2))),
inference(cp,[status(thm)],[t7203,t790]) ).
cnf(t123991,plain,
multiply(X1,multiply(X2,multiply(additive_inverse(X1),multiply(X2,multiply(additive_inverse(X1),X2))))) = multiply(X1,X2),
inference(step,[status(thm)],[t7222,t7203]) ).
cnf(t9922,plain,
multiply(X1,multiply(X2,multiply(additive_inverse(X1),multiply(X2,multiply(additive_inverse(X1),X2))))) = multiply(X1,X2),
inference(orient,[status(thm)],[t123991]) ).
cnf(t13393,plain,
multiply(additive_inverse(X1),multiply(X1,multiply(additive_inverse(X1),X1))) = multiply(X1,X1),
inference(cp,[status(thm)],[t13392,t9922]) ).
cnf(t52,plain,
multiply(multiply(X1,X2),X3) = multiply(X1,multiply(X2,multiply(multiply(X1,X2),multiply(multiply(X1,X2),X3)))),
inference(cp,[status(thm)],[t51,t40]) ).
cnf(t123916,plain,
multiply(X1,multiply(X2,X3)) = multiply(X1,multiply(X2,multiply(multiply(X1,X2),multiply(multiply(X1,X2),X3)))),
inference(step,[status(thm)],[t52,t40]) ).
cnf(t123917,plain,
multiply(X1,multiply(X2,X3)) = multiply(X1,multiply(X2,multiply(X1,multiply(X2,multiply(multiply(X1,X2),X3))))),
inference(step,[status(thm)],[t123916,t40]) ).
cnf(t123918,plain,
multiply(X1,multiply(X2,X3)) = multiply(X1,multiply(X2,multiply(X1,multiply(X2,multiply(X1,multiply(X2,X3)))))),
inference(step,[status(thm)],[t123917,t40]) ).
cnf(t3958,plain,
multiply(X1,multiply(X2,multiply(X1,multiply(X2,multiply(X1,multiply(X2,X3)))))) = multiply(X1,multiply(X2,X3)),
inference(orient,[status(thm)],[t123918]) ).
cnf(t7286,plain,
multiply(X1,multiply(additive_inverse(X1),multiply(additive_inverse(X1),X2))) = multiply(X1,multiply(additive_inverse(X1),multiply(X1,multiply(additive_inverse(X1),multiply(X1,X2))))),
inference(cp,[status(thm)],[t3958,t7203]) ).
cnf(t123992,plain,
multiply(X1,X2) = multiply(X1,multiply(additive_inverse(X1),multiply(X1,multiply(additive_inverse(X1),multiply(X1,X2))))),
inference(step,[status(thm)],[t7286,t7203]) ).
cnf(t10068,plain,
multiply(X1,multiply(additive_inverse(X1),multiply(X1,multiply(additive_inverse(X1),multiply(X1,X2))))) = multiply(X1,X2),
inference(orient,[status(thm)],[t123992]) ).
cnf(t13282,plain,
multiply(X1,multiply(X1,additive_inverse(X1))) = multiply(X1,multiply(additive_inverse(X1),multiply(X1,multiply(additive_inverse(X1),additive_inverse(X1))))),
inference(cp,[status(thm)],[t10068,t13224]) ).
cnf(t124042,plain,
additive_inverse(X1) = multiply(X1,multiply(additive_inverse(X1),multiply(X1,multiply(additive_inverse(X1),additive_inverse(X1))))),
inference(step,[status(thm)],[t13282,t13224]) ).
cnf(t124043,plain,
additive_inverse(X1) = multiply(X1,multiply(additive_inverse(X1),X1)),
inference(step,[status(thm)],[t124042,t7143]) ).
cnf(t13304,plain,
multiply(X1,multiply(additive_inverse(X1),X1)) = additive_inverse(X1),
inference(orient,[status(thm)],[t124043]) ).
cnf(t124048,plain,
multiply(additive_inverse(X1),additive_inverse(X1)) = multiply(X1,X1),
inference(step,[status(thm)],[t13393,t13304]) ).
cnf(t13614,plain,
multiply(additive_inverse(X1),additive_inverse(X1)) = multiply(X1,X1),
inference(orient,[status(thm)],[t124048]) ).
cnf(t124051,plain,
multiply(add(additive_inverse(X1),multiply(X2,X1)),multiply(X1,X1)) = add(additive_inverse(X1),multiply(X2,X1)),
inference(step,[status(thm)],[t11340,t13614]) ).
cnf(t664,plain,
multiply(add(X1,multiply(X2,X3)),multiply(X3,X3)) = add(multiply(X1,multiply(X3,X3)),multiply(X2,X3)),
inference(cp,[status(thm)],[t627,t9]) ).
cnf(t123830,plain,
multiply(add(X1,multiply(X2,X3)),multiply(X3,X3)) = add(multiply(X2,X3),multiply(X1,multiply(X3,X3))),
inference(step,[status(thm)],[t664,t10]) ).
cnf(t123831,plain,
multiply(add(X1,multiply(X2,X3)),multiply(X3,X3)) = multiply(add(X2,multiply(X1,X3)),X3),
inference(step,[status(thm)],[t123830,t627]) ).
cnf(t1395,plain,
multiply(add(X1,multiply(X2,X3)),multiply(X3,X3)) = multiply(add(X2,multiply(X1,X3)),X3),
inference(orient,[status(thm)],[t123831]) ).
cnf(t124052,plain,
multiply(add(X2,multiply(additive_inverse(X1),X1)),X1) = add(additive_inverse(X1),multiply(X2,X1)),
inference(step,[status(thm)],[t124051,t1395]) ).
cnf(t13395,plain,
multiply(additive_inverse(X1),X1) = multiply(X1,additive_inverse(X1)),
inference(cp,[status(thm)],[t13392,t13304]) ).
cnf(t13520,plain,
multiply(additive_inverse(X1),X1) = multiply(X1,additive_inverse(X1)),
inference(orient,[status(thm)],[t13395]) ).
cnf(t124053,plain,
multiply(add(X2,multiply(X1,additive_inverse(X1))),X1) = add(additive_inverse(X1),multiply(X2,X1)),
inference(step,[status(thm)],[t124052,t13520]) ).
cnf(t13712,plain,
multiply(add(X2,multiply(X1,additive_inverse(X1))),X1) = add(additive_inverse(X1),multiply(X2,X1)),
inference(rw,[status(thm)],[t124053]) ).
cnf(t15458,plain,
multiply(add(X1,multiply(X2,additive_inverse(X2))),X2) = add(additive_inverse(X2),multiply(X1,X2)),
inference(orient,[status(thm)],[t13712]) ).
cnf(t15526,plain,
multiply(add(X1,multiply(X2,add(X2,additive_inverse(X2)))),X2) = add(X2,add(additive_inverse(X2),multiply(X1,X2))),
inference(cp,[status(thm)],[t1930,t15458]) ).
cnf(t124092,plain,
multiply(add(X1,multiply(X2,additive_identity)),X2) = add(X2,add(additive_inverse(X2),multiply(X1,X2))),
inference(step,[status(thm)],[t15526,t24]) ).
cnf(t124093,plain,
multiply(add(X1,additive_identity),X2) = add(X2,add(additive_inverse(X2),multiply(X1,X2))),
inference(step,[status(thm)],[t124092,t787]) ).
cnf(t124094,plain,
multiply(X1,X2) = add(X2,add(additive_inverse(X2),multiply(X1,X2))),
inference(step,[status(thm)],[t124093,t8]) ).
cnf(t15563,plain,
add(X1,add(additive_inverse(X1),multiply(X2,X1))) = multiply(X2,X1),
inference(orient,[status(thm)],[t124094]) ).
cnf(t15626,plain,
multiply(multiply(X1,X2),X3) = add(X3,add(additive_inverse(X3),multiply(X1,multiply(X2,X3)))),
inference(cp,[status(thm)],[t15563,t40]) ).
cnf(t124122,plain,
multiply(X1,multiply(X2,X3)) = add(X3,add(additive_inverse(X3),multiply(X1,multiply(X2,X3)))),
inference(step,[status(thm)],[t15626,t40]) ).
cnf(t17238,plain,
add(X1,add(additive_inverse(X1),multiply(X2,multiply(X3,X1)))) = multiply(X2,multiply(X3,X1)),
inference(orient,[status(thm)],[t124122]) ).
cnf(t25420,plain,
multiply(X1,additive_inverse(X2)) = multiply(X1,multiply(X1,multiply(additive_inverse(X1),X2))),
inference(cp,[status(thm)],[t25418,t17238]) ).
cnf(t124233,plain,
multiply(X1,additive_inverse(X2)) = multiply(additive_inverse(X1),X2),
inference(step,[status(thm)],[t25420,t13392]) ).
cnf(t25628,plain,
multiply(additive_inverse(X1),X2) = multiply(X1,additive_inverse(X2)),
inference(orient,[status(thm)],[t124233]) ).
cnf(t25671,plain,
multiply(add(additive_inverse(X1),X2),X3) = add(multiply(X1,additive_inverse(X3)),multiply(X2,X3)),
inference(cp,[status(thm)],[t27,t25628]) ).
cnf(t124361,plain,
multiply(add(X2,additive_inverse(X1)),X3) = add(multiply(X1,additive_inverse(X3)),multiply(X2,X3)),
inference(step,[status(thm)],[t25671,t10]) ).
cnf(t124362,plain,
multiply(add(X2,additive_inverse(X1)),X3) = add(multiply(X2,X3),multiply(X1,additive_inverse(X3))),
inference(step,[status(thm)],[t124361,t10]) ).
cnf(t27718,plain,
add(multiply(X1,X2),multiply(X3,additive_inverse(X2))) = multiply(add(X1,additive_inverse(X3)),X2),
inference(orient,[status(thm)],[t124362]) ).
cnf(t27758,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)],[t27718,t25628]) ).
cnf(t124365,plain,
multiply(add(additive_inverse(X1),additive_inverse(X2)),X3) = multiply(add(X1,X2),additive_inverse(X3)),
inference(step,[status(thm)],[t27758,t27]) ).
cnf(t27900,plain,
multiply(add(additive_inverse(X1),additive_inverse(X2)),X3) = multiply(add(X1,X2),additive_inverse(X3)),
inference(orient,[status(thm)],[t124365]) ).
cnf(t27931,plain,
multiply(add(X1,X2),additive_inverse(multiply(add(additive_inverse(X1),additive_inverse(X2)),add(additive_inverse(X1),additive_inverse(X2))))) = add(additive_inverse(X1),additive_inverse(X2)),
inference(cp,[status(thm)],[t27900,t9]) ).
cnf(t25668,plain,
multiply(additive_inverse(X1),multiply(X2,X3)) = multiply(multiply(X1,additive_inverse(X2)),X3),
inference(cp,[status(thm)],[t40,t25628]) ).
cnf(t124323,plain,
multiply(X1,additive_inverse(multiply(X2,X3))) = multiply(multiply(X1,additive_inverse(X2)),X3),
inference(step,[status(thm)],[t25668,t25628]) ).
cnf(t124324,plain,
multiply(X1,additive_inverse(multiply(X2,X3))) = multiply(X1,multiply(additive_inverse(X2),X3)),
inference(step,[status(thm)],[t124323,t40]) ).
cnf(t124325,plain,
multiply(X1,additive_inverse(multiply(X2,X3))) = multiply(X1,multiply(X2,additive_inverse(X3))),
inference(step,[status(thm)],[t124324,t25628]) ).
cnf(t25894,plain,
multiply(X1,additive_inverse(multiply(X2,X3))) = multiply(X1,multiply(X2,additive_inverse(X3))),
inference(orient,[status(thm)],[t124325]) ).
cnf(t124366,plain,
multiply(add(X1,X2),multiply(add(additive_inverse(X1),additive_inverse(X2)),additive_inverse(add(additive_inverse(X1),additive_inverse(X2))))) = add(additive_inverse(X1),additive_inverse(X2)),
inference(step,[status(thm)],[t27931,t25894]) ).
cnf(t124367,plain,
multiply(add(X1,X2),multiply(add(X1,X2),additive_inverse(additive_inverse(add(additive_inverse(X1),additive_inverse(X2)))))) = add(additive_inverse(X1),additive_inverse(X2)),
inference(step,[status(thm)],[t124366,t27900]) ).
cnf(t14428,plain,
multiply(X1,multiply(additive_inverse(X1),multiply(additive_inverse(X1),multiply(additive_inverse(additive_inverse(X1)),X1)))) = add(X1,multiply(X1,additive_identity)),
inference(cp,[status(thm)],[t7086,t14342]) ).
cnf(t124068,plain,
multiply(X1,multiply(additive_inverse(additive_inverse(X1)),X1)) = add(X1,multiply(X1,additive_identity)),
inference(step,[status(thm)],[t14428,t7203]) ).
cnf(t124069,plain,
multiply(X1,multiply(additive_inverse(additive_inverse(X1)),X1)) = X1,
inference(step,[status(thm)],[t124068,t279]) ).
cnf(t14466,plain,
multiply(X1,multiply(additive_inverse(additive_inverse(X1)),X1)) = X1,
inference(orient,[status(thm)],[t124069]) ).
cnf(t14470,plain,
multiply(X1,multiply(multiply(additive_inverse(additive_inverse(X1)),X1),X2)) = multiply(X1,X2),
inference(cp,[status(thm)],[t40,t14466]) ).
cnf(t124079,plain,
multiply(X1,multiply(additive_inverse(additive_inverse(X1)),multiply(X1,X2))) = multiply(X1,X2),
inference(step,[status(thm)],[t14470,t40]) ).
cnf(t14619,plain,
multiply(X1,multiply(additive_inverse(additive_inverse(X1)),multiply(X1,X2))) = multiply(X1,X2),
inference(orient,[status(thm)],[t124079]) ).
cnf(t13410,plain,
multiply(additive_inverse(X1),multiply(additive_inverse(X1),additive_inverse(additive_inverse(X1)))) = multiply(X1,multiply(X1,additive_inverse(additive_inverse(X1)))),
inference(cp,[status(thm)],[t13392,t13224]) ).
cnf(t124059,plain,
additive_inverse(additive_inverse(X1)) = multiply(X1,multiply(X1,additive_inverse(additive_inverse(X1)))),
inference(step,[status(thm)],[t13410,t13224]) ).
cnf(t13782,plain,
multiply(X1,multiply(X1,additive_inverse(additive_inverse(X1)))) = additive_inverse(additive_inverse(X1)),
inference(orient,[status(thm)],[t124059]) ).
cnf(t14627,plain,
multiply(X1,multiply(X1,additive_inverse(additive_inverse(X1)))) = multiply(X1,multiply(additive_inverse(additive_inverse(X1)),additive_inverse(additive_inverse(X1)))),
inference(cp,[status(thm)],[t14619,t13782]) ).
cnf(t124080,plain,
additive_inverse(additive_inverse(X1)) = multiply(X1,multiply(additive_inverse(additive_inverse(X1)),additive_inverse(additive_inverse(X1)))),
inference(step,[status(thm)],[t14627,t13782]) ).
cnf(t7210,plain,
multiply(X1,multiply(additive_inverse(additive_inverse(X1)),additive_inverse(additive_inverse(X1)))) = multiply(X1,multiply(additive_inverse(X1),additive_inverse(X1))),
inference(cp,[status(thm)],[t7203,t7143]) ).
cnf(t123957,plain,
multiply(X1,multiply(additive_inverse(additive_inverse(X1)),additive_inverse(additive_inverse(X1)))) = X1,
inference(step,[status(thm)],[t7210,t7143]) ).
cnf(t7292,plain,
multiply(X1,multiply(additive_inverse(additive_inverse(X1)),additive_inverse(additive_inverse(X1)))) = X1,
inference(orient,[status(thm)],[t123957]) ).
cnf(t124081,plain,
additive_inverse(additive_inverse(X1)) = X1,
inference(step,[status(thm)],[t124080,t7292]) ).
cnf(t14771,plain,
additive_inverse(additive_inverse(X1)) = X1,
inference(orient,[status(thm)],[t124081]) ).
cnf(t124368,plain,
multiply(add(X1,X2),multiply(add(X1,X2),add(additive_inverse(X1),additive_inverse(X2)))) = add(additive_inverse(X1),additive_inverse(X2)),
inference(step,[status(thm)],[t124367,t14771]) ).
cnf(t25669,plain,
multiply(additive_inverse(X1),add(X2,X3)) = add(multiply(X1,additive_inverse(X2)),multiply(additive_inverse(X1),X3)),
inference(cp,[status(thm)],[t33,t25628]) ).
cnf(t124329,plain,
multiply(X1,additive_inverse(add(X2,X3))) = add(multiply(X1,additive_inverse(X2)),multiply(additive_inverse(X1),X3)),
inference(step,[status(thm)],[t25669,t25628]) ).
cnf(t124330,plain,
multiply(X1,additive_inverse(add(X2,X3))) = add(multiply(X1,additive_inverse(X2)),multiply(X1,additive_inverse(X3))),
inference(step,[status(thm)],[t124329,t25628]) ).
cnf(t124331,plain,
multiply(X1,additive_inverse(add(X2,X3))) = multiply(X1,add(additive_inverse(X2),additive_inverse(X3))),
inference(step,[status(thm)],[t124330,t33]) ).
cnf(t26092,plain,
multiply(X1,add(additive_inverse(X2),additive_inverse(X3))) = multiply(X1,additive_inverse(add(X2,X3))),
inference(orient,[status(thm)],[t124331]) ).
cnf(t124369,plain,
multiply(add(X1,X2),multiply(add(X1,X2),additive_inverse(add(X1,X2)))) = add(additive_inverse(X1),additive_inverse(X2)),
inference(step,[status(thm)],[t124368,t26092]) ).
cnf(t124370,plain,
additive_inverse(add(X1,X2)) = add(additive_inverse(X1),additive_inverse(X2)),
inference(step,[status(thm)],[t124369,t13224]) ).
cnf(t28152,plain,
add(additive_inverse(X1),additive_inverse(X2)) = additive_inverse(add(X1,X2)),
inference(orient,[status(thm)],[t124370]) ).
cnf(t28162,plain,
additive_inverse(add(additive_inverse(X1),X2)) = add(X1,additive_inverse(X2)),
inference(cp,[status(thm)],[t28152,t14771]) ).
cnf(t124375,plain,
additive_inverse(add(X2,additive_inverse(X1))) = add(X1,additive_inverse(X2)),
inference(step,[status(thm)],[t28162,t10]) ).
cnf(t28228,plain,
additive_inverse(add(X1,additive_inverse(X2))) = add(X2,additive_inverse(X1)),
inference(orient,[status(thm)],[t124375]) ).
cnf(t28235,plain,
additive_inverse(add(add(X1,additive_inverse(X2)),X3)) = add(add(X2,additive_inverse(X1)),additive_inverse(X3)),
inference(cp,[status(thm)],[t28152,t28228]) ).
cnf(t124387,plain,
additive_inverse(add(X3,add(X1,additive_inverse(X2)))) = add(add(X2,additive_inverse(X1)),additive_inverse(X3)),
inference(step,[status(thm)],[t28235,t10]) ).
cnf(t124388,plain,
additive_inverse(add(X1,add(additive_inverse(X2),X3))) = add(add(X2,additive_inverse(X1)),additive_inverse(X3)),
inference(step,[status(thm)],[t124387,t12]) ).
cnf(t124389,plain,
additive_inverse(add(X1,add(X3,additive_inverse(X2)))) = add(add(X2,additive_inverse(X1)),additive_inverse(X3)),
inference(step,[status(thm)],[t124388,t10]) ).
cnf(t124390,plain,
additive_inverse(add(X1,add(X3,additive_inverse(X2)))) = add(additive_inverse(X3),add(X2,additive_inverse(X1))),
inference(step,[status(thm)],[t124389,t10]) ).
cnf(t124391,plain,
additive_inverse(add(X1,add(X3,additive_inverse(X2)))) = add(additive_inverse(X1),add(additive_inverse(X3),X2)),
inference(step,[status(thm)],[t124390,t12]) ).
cnf(t124392,plain,
additive_inverse(add(X1,add(X3,additive_inverse(X2)))) = add(X2,add(additive_inverse(X1),additive_inverse(X3))),
inference(step,[status(thm)],[t124391,t12]) ).
cnf(t124393,plain,
additive_inverse(add(X1,add(X3,additive_inverse(X2)))) = add(X2,additive_inverse(add(X1,X3))),
inference(step,[status(thm)],[t124392,t28152]) ).
cnf(t29034,plain,
additive_inverse(add(X1,add(X2,additive_inverse(X3)))) = add(X3,additive_inverse(add(X1,X2))),
inference(orient,[status(thm)],[t124393]) ).
cnf(t29035,plain,
add(X1,additive_inverse(add(X1,X2))) = additive_inverse(X2),
inference(cp,[status(thm)],[t29034,t46]) ).
cnf(t29121,plain,
add(X1,additive_inverse(add(X1,X2))) = additive_inverse(X2),
inference(orient,[status(thm)],[t29035]) ).
cnf(t654,plain,
multiply(add(X1,multiply(multiply(X2,X3),Y3)),Y4) = add(multiply(X1,Y4),multiply(X2,multiply(X3,multiply(Y3,Y4)))),
inference(cp,[status(thm)],[t627,t40]) ).
cnf(t123919,plain,
multiply(add(X1,multiply(X2,multiply(X3,Y3))),Y4) = add(multiply(X1,Y4),multiply(X2,multiply(X3,multiply(Y3,Y4)))),
inference(step,[status(thm)],[t654,t40]) ).
cnf(t4415,plain,
add(multiply(X1,X2),multiply(X3,multiply(Y3,multiply(Y4,X2)))) = multiply(add(X1,multiply(X3,multiply(Y3,Y4))),X2),
inference(orient,[status(thm)],[t123919]) ).
cnf(t14346,plain,
additive_identity = multiply(X1,multiply(add(X2,multiply(X1,multiply(additive_inverse(X1),X2))),X3)),
inference(cp,[status(thm)],[t14342,t4415]) ).
cnf(t18821,plain,
multiply(X1,multiply(add(X2,multiply(X1,multiply(additive_inverse(X1),X2))),X3)) = additive_identity,
inference(orient,[status(thm)],[t14346]) ).
cnf(t18984,plain,
multiply(add(X1,multiply(X2,multiply(additive_inverse(X2),X1))),X2) = multiply(add(X1,multiply(X2,multiply(additive_inverse(X2),X1))),additive_identity),
inference(cp,[status(thm)],[t790,t18821]) ).
cnf(t124151,plain,
multiply(add(X1,multiply(X2,multiply(additive_inverse(X2),X1))),X2) = additive_identity,
inference(step,[status(thm)],[t18984,t787]) ).
cnf(t19012,plain,
multiply(add(X1,multiply(X2,multiply(additive_inverse(X2),X1))),X2) = additive_identity,
inference(orient,[status(thm)],[t124151]) ).
cnf(t124298,plain,
multiply(add(X1,multiply(X2,multiply(X2,additive_inverse(X1)))),X2) = additive_identity,
inference(step,[status(thm)],[t19012,t25628]) ).
cnf(t25881,plain,
multiply(add(X1,multiply(X2,multiply(X2,additive_inverse(X1)))),X2) = additive_identity,
inference(rw,[status(thm)],[t124298]) ).
cnf(t27027,plain,
multiply(add(X1,multiply(X2,multiply(X2,additive_inverse(X1)))),X2) = additive_identity,
inference(orient,[status(thm)],[t25881]) ).
cnf(t27078,plain,
multiply(add(add(X1,multiply(X2,multiply(X2,additive_inverse(X1)))),X3),X2) = add(additive_identity,multiply(X3,X2)),
inference(cp,[status(thm)],[t27,t27027]) ).
cnf(t124533,plain,
multiply(add(X3,add(X1,multiply(X2,multiply(X2,additive_inverse(X1))))),X2) = add(additive_identity,multiply(X3,X2)),
inference(step,[status(thm)],[t27078,t10]) ).
cnf(t124534,plain,
multiply(add(X1,add(multiply(X2,multiply(X2,additive_inverse(X1))),X3)),X2) = add(additive_identity,multiply(X3,X2)),
inference(step,[status(thm)],[t124533,t12]) ).
cnf(t124535,plain,
multiply(add(X1,add(X3,multiply(X2,multiply(X2,additive_inverse(X1))))),X2) = add(additive_identity,multiply(X3,X2)),
inference(step,[status(thm)],[t124534,t10]) ).
cnf(t124536,plain,
multiply(add(X1,add(X3,multiply(X2,multiply(X2,additive_inverse(X1))))),X2) = multiply(X3,X2),
inference(step,[status(thm)],[t124535,t283]) ).
cnf(t40198,plain,
multiply(add(X1,add(X2,multiply(X3,multiply(X3,additive_inverse(X1))))),X3) = multiply(X2,X3),
inference(orient,[status(thm)],[t124536]) ).
cnf(t28167,plain,
additive_inverse(X1) = add(X2,additive_inverse(add(X1,X2))),
inference(cp,[status(thm)],[t46,t28152]) ).
cnf(t28295,plain,
add(X1,additive_inverse(add(X2,X1))) = additive_inverse(X2),
inference(orient,[status(thm)],[t28167]) ).
cnf(t28333,plain,
additive_inverse(multiply(X1,X2)) = add(multiply(X3,X2),additive_inverse(multiply(add(X1,X3),X2))),
inference(cp,[status(thm)],[t28295,t27]) ).
cnf(t31754,plain,
add(multiply(X1,X2),additive_inverse(multiply(add(X3,X1),X2))) = additive_inverse(multiply(X3,X2)),
inference(orient,[status(thm)],[t28333]) ).
cnf(t31967,plain,
additive_inverse(multiply(X1,X2)) = add(multiply(additive_inverse(X1),X2),additive_inverse(multiply(additive_identity,X2))),
inference(cp,[status(thm)],[t31754,t24]) ).
cnf(t124428,plain,
additive_inverse(multiply(X1,X2)) = add(multiply(X1,additive_inverse(X2)),additive_inverse(multiply(additive_identity,X2))),
inference(step,[status(thm)],[t31967,t25628]) ).
cnf(t124429,plain,
additive_inverse(multiply(X1,X2)) = add(multiply(X1,additive_inverse(X2)),additive_inverse(additive_identity)),
inference(step,[status(thm)],[t124428,t275]) ).
cnf(t11438,plain,
multiply(add(additive_inverse(X1),multiply(X2,X1)),multiply(additive_inverse(X1),additive_inverse(X1))) = add(additive_identity,add(additive_inverse(X1),multiply(X2,X1))),
inference(cp,[status(thm)],[t283,t11340]) ).
cnf(t124003,plain,
add(additive_inverse(X1),multiply(X2,X1)) = add(additive_identity,add(additive_inverse(X1),multiply(X2,X1))),
inference(step,[status(thm)],[t11438,t11340]) ).
cnf(t11503,plain,
add(additive_identity,add(additive_inverse(X1),multiply(X2,X1))) = add(additive_inverse(X1),multiply(X2,X1)),
inference(orient,[status(thm)],[t124003]) ).
cnf(t11543,plain,
add(additive_inverse(additive_identity),multiply(X1,additive_identity)) = add(additive_identity,add(additive_inverse(additive_identity),additive_identity)),
inference(cp,[status(thm)],[t11503,t787]) ).
cnf(t124004,plain,
add(additive_inverse(additive_identity),additive_identity) = add(additive_identity,add(additive_inverse(additive_identity),additive_identity)),
inference(step,[status(thm)],[t11543,t787]) ).
cnf(t124005,plain,
additive_inverse(additive_identity) = add(additive_identity,add(additive_inverse(additive_identity),additive_identity)),
inference(step,[status(thm)],[t124004,t8]) ).
cnf(t124006,plain,
additive_inverse(additive_identity) = add(additive_identity,add(additive_identity,additive_inverse(additive_identity))),
inference(step,[status(thm)],[t124005,t12]) ).
cnf(t124007,plain,
additive_inverse(additive_identity) = additive_identity,
inference(step,[status(thm)],[t124006,t46]) ).
cnf(t11615,plain,
additive_inverse(additive_identity) = additive_identity,
inference(orient,[status(thm)],[t124007]) ).
cnf(t124430,plain,
additive_inverse(multiply(X1,X2)) = add(multiply(X1,additive_inverse(X2)),additive_identity),
inference(step,[status(thm)],[t124429,t11615]) ).
cnf(t124431,plain,
additive_inverse(multiply(X1,X2)) = multiply(X1,additive_inverse(X2)),
inference(step,[status(thm)],[t124430,t8]) ).
cnf(t32022,plain,
additive_inverse(multiply(X1,X2)) = multiply(X1,additive_inverse(X2)),
inference(orient,[status(thm)],[t124431]) ).
cnf(t32107,plain,
add(multiply(X1,X2),additive_inverse(X3)) = additive_inverse(add(X3,multiply(X1,additive_inverse(X2)))),
inference(cp,[status(thm)],[t28228,t32022]) ).
cnf(t124450,plain,
add(additive_inverse(X3),multiply(X1,X2)) = additive_inverse(add(X3,multiply(X1,additive_inverse(X2)))),
inference(step,[status(thm)],[t32107,t10]) ).
cnf(t32559,plain,
additive_inverse(add(X1,multiply(X2,additive_inverse(X3)))) = add(additive_inverse(X1),multiply(X2,X3)),
inference(orient,[status(thm)],[t124450]) ).
cnf(t32614,plain,
additive_inverse(multiply(X1,additive_inverse(X2))) = add(X3,add(additive_inverse(X3),multiply(X1,X2))),
inference(cp,[status(thm)],[t29121,t32559]) ).
cnf(t124451,plain,
multiply(X1,additive_inverse(additive_inverse(X2))) = add(X3,add(additive_inverse(X3),multiply(X1,X2))),
inference(step,[status(thm)],[t32614,t32022]) ).
cnf(t124452,plain,
multiply(X1,X2) = add(X3,add(additive_inverse(X3),multiply(X1,X2))),
inference(step,[status(thm)],[t124451,t14771]) ).
cnf(t32673,plain,
add(X1,add(additive_inverse(X1),multiply(X2,X3))) = multiply(X2,X3),
inference(orient,[status(thm)],[t124452]) ).
cnf(t40200,plain,
multiply(additive_inverse(X1),X2) = multiply(multiply(X2,multiply(X2,additive_inverse(X1))),X2),
inference(cp,[status(thm)],[t40198,t32673]) ).
cnf(t124537,plain,
multiply(X1,additive_inverse(X2)) = multiply(multiply(X2,multiply(X2,additive_inverse(X1))),X2),
inference(step,[status(thm)],[t40200,t25628]) ).
cnf(t124538,plain,
multiply(X1,additive_inverse(X2)) = multiply(X2,multiply(multiply(X2,additive_inverse(X1)),X2)),
inference(step,[status(thm)],[t124537,t40]) ).
cnf(t124539,plain,
multiply(X1,additive_inverse(X2)) = multiply(X2,multiply(X2,multiply(additive_inverse(X1),X2))),
inference(step,[status(thm)],[t124538,t40]) ).
cnf(t124540,plain,
multiply(X1,additive_inverse(X2)) = multiply(X2,multiply(X2,multiply(X1,additive_inverse(X2)))),
inference(step,[status(thm)],[t124539,t25628]) ).
cnf(t40394,plain,
multiply(X1,multiply(X1,multiply(X2,additive_inverse(X1)))) = multiply(X2,additive_inverse(X1)),
inference(orient,[status(thm)],[t124540]) ).
cnf(t40396,plain,
multiply(X1,additive_inverse(additive_inverse(X2))) = multiply(X2,additive_inverse(multiply(additive_inverse(X2),multiply(X1,additive_inverse(additive_inverse(X2)))))),
inference(cp,[status(thm)],[t40394,t25628]) ).
cnf(t124541,plain,
multiply(X1,X2) = multiply(X2,additive_inverse(multiply(additive_inverse(X2),multiply(X1,additive_inverse(additive_inverse(X2)))))),
inference(step,[status(thm)],[t40396,t14771]) ).
cnf(t124542,plain,
multiply(X1,X2) = multiply(X2,multiply(additive_inverse(X2),additive_inverse(multiply(X1,additive_inverse(additive_inverse(X2)))))),
inference(step,[status(thm)],[t124541,t25894]) ).
cnf(t124543,plain,
multiply(X1,X2) = multiply(X2,multiply(X2,additive_inverse(additive_inverse(multiply(X1,additive_inverse(additive_inverse(X2))))))),
inference(step,[status(thm)],[t124542,t25628]) ).
cnf(t124544,plain,
multiply(X1,X2) = multiply(X2,multiply(X2,multiply(X1,additive_inverse(additive_inverse(X2))))),
inference(step,[status(thm)],[t124543,t14771]) ).
cnf(t124545,plain,
multiply(X1,X2) = multiply(X2,multiply(X2,multiply(X1,X2))),
inference(step,[status(thm)],[t124544,t14771]) ).
cnf(t40546,plain,
multiply(X1,multiply(X1,multiply(X2,X1))) = multiply(X2,X1),
inference(orient,[status(thm)],[t124545]) ).
cnf(t65,plain,
multiply(X1,multiply(add(X2,multiply(X1,X1)),X3)) = multiply(add(X1,multiply(X1,X2)),X3),
inference(cp,[status(thm)],[t40,t59]) ).
cnf(t839,plain,
multiply(X1,multiply(add(X2,multiply(X1,X1)),X3)) = multiply(add(X1,multiply(X1,X2)),X3),
inference(orient,[status(thm)],[t65]) ).
cnf(t40551,plain,
multiply(add(X1,multiply(X2,X2)),X2) = multiply(X2,multiply(add(X2,multiply(X2,X1)),X2)),
inference(cp,[status(thm)],[t40546,t839]) ).
cnf(t124546,plain,
add(X2,multiply(X1,X2)) = multiply(X2,multiply(add(X2,multiply(X2,X1)),X2)),
inference(step,[status(thm)],[t40551,t684]) ).
cnf(t124547,plain,
add(X2,multiply(X1,X2)) = multiply(X2,multiply(X2,add(X2,multiply(X1,X2)))),
inference(step,[status(thm)],[t124546,t2243]) ).
cnf(t40722,plain,
multiply(X1,multiply(X1,add(X1,multiply(X2,X1)))) = add(X1,multiply(X2,X1)),
inference(orient,[status(thm)],[t124547]) ).
cnf(t40832,plain,
multiply(X1,multiply(multiply(X1,add(X1,multiply(X2,X1))),X3)) = multiply(add(X1,multiply(X2,X1)),X3),
inference(cp,[status(thm)],[t40,t40722]) ).
cnf(t124940,plain,
multiply(X1,multiply(X1,multiply(add(X1,multiply(X2,X1)),X3))) = multiply(add(X1,multiply(X2,X1)),X3),
inference(step,[status(thm)],[t40832,t40]) ).
cnf(t72767,plain,
multiply(X1,multiply(X1,multiply(add(X1,multiply(X2,X1)),X3))) = multiply(add(X1,multiply(X2,X1)),X3),
inference(orient,[status(thm)],[t124940]) ).
cnf(t19132,plain,
multiply(add(X1,multiply(X2,add(X2,multiply(additive_inverse(X2),X1)))),X2) = add(X2,additive_identity),
inference(cp,[status(thm)],[t1930,t19012]) ).
cnf(t124200,plain,
multiply(add(X1,multiply(X2,add(X2,multiply(additive_inverse(X2),X1)))),X2) = X2,
inference(step,[status(thm)],[t19132,t8]) ).
cnf(t22338,plain,
multiply(add(X1,multiply(X2,add(X2,multiply(additive_inverse(X2),X1)))),X2) = X2,
inference(orient,[status(thm)],[t124200]) ).
cnf(t124314,plain,
multiply(add(X1,multiply(X2,add(X2,multiply(X2,additive_inverse(X1))))),X2) = X2,
inference(step,[status(thm)],[t22338,t25628]) ).
cnf(t25889,plain,
multiply(add(X1,multiply(X2,add(X2,multiply(X2,additive_inverse(X1))))),X2) = X2,
inference(rw,[status(thm)],[t124314]) ).
cnf(t36304,plain,
multiply(add(X1,multiply(X2,add(X2,multiply(X2,additive_inverse(X1))))),X2) = X2,
inference(orient,[status(thm)],[t25889]) ).
cnf(t32094,plain,
additive_inverse(add(multiply(X1,X2),X3)) = add(multiply(X1,additive_inverse(X2)),additive_inverse(X3)),
inference(cp,[status(thm)],[t28152,t32022]) ).
cnf(t124448,plain,
additive_inverse(add(X3,multiply(X1,X2))) = add(multiply(X1,additive_inverse(X2)),additive_inverse(X3)),
inference(step,[status(thm)],[t32094,t10]) ).
cnf(t124449,plain,
additive_inverse(add(X3,multiply(X1,X2))) = add(additive_inverse(X3),multiply(X1,additive_inverse(X2))),
inference(step,[status(thm)],[t124448,t10]) ).
cnf(t32462,plain,
add(additive_inverse(X1),multiply(X2,additive_inverse(X3))) = additive_inverse(add(X1,multiply(X2,X3))),
inference(orient,[status(thm)],[t124449]) ).
cnf(t32475,plain,
additive_inverse(add(additive_inverse(X1),multiply(X2,X3))) = add(X1,multiply(X2,additive_inverse(X3))),
inference(cp,[status(thm)],[t32462,t14771]) ).
cnf(t32749,plain,
additive_inverse(add(additive_inverse(X1),multiply(X2,X3))) = add(X1,multiply(X2,additive_inverse(X3))),
inference(orient,[status(thm)],[t32475]) ).
cnf(t32840,plain,
multiply(add(additive_inverse(X1),multiply(X2,X3)),additive_inverse(Y3)) = multiply(add(X1,multiply(X2,additive_inverse(X3))),Y3),
inference(cp,[status(thm)],[t25628,t32749]) ).
cnf(t35074,plain,
multiply(add(additive_inverse(X1),multiply(X2,X3)),additive_inverse(Y3)) = multiply(add(X1,multiply(X2,additive_inverse(X3))),Y3),
inference(orient,[status(thm)],[t32840]) ).
cnf(t36305,plain,
additive_inverse(X1) = multiply(add(X2,multiply(additive_inverse(X1),additive_inverse(add(additive_inverse(X1),multiply(additive_inverse(X1),additive_inverse(additive_inverse(X2))))))),X1),
inference(cp,[status(thm)],[t36304,t35074]) ).
cnf(t124524,plain,
additive_inverse(X1) = multiply(add(X2,multiply(X1,additive_inverse(additive_inverse(add(additive_inverse(X1),multiply(additive_inverse(X1),additive_inverse(additive_inverse(X2)))))))),X1),
inference(step,[status(thm)],[t36305,t25628]) ).
cnf(t124525,plain,
additive_inverse(X1) = multiply(add(X2,multiply(X1,add(additive_inverse(X1),multiply(additive_inverse(X1),additive_inverse(additive_inverse(X2)))))),X1),
inference(step,[status(thm)],[t124524,t14771]) ).
cnf(t124526,plain,
additive_inverse(X1) = multiply(add(X2,multiply(X1,additive_inverse(add(X1,multiply(additive_inverse(X1),additive_inverse(X2)))))),X1),
inference(step,[status(thm)],[t124525,t32462]) ).
cnf(t124527,plain,
additive_inverse(X1) = multiply(add(X2,multiply(X1,add(additive_inverse(X1),multiply(additive_inverse(X1),X2)))),X1),
inference(step,[status(thm)],[t124526,t32559]) ).
cnf(t124528,plain,
additive_inverse(X1) = multiply(add(X2,multiply(X1,add(additive_inverse(X1),multiply(X1,additive_inverse(X2))))),X1),
inference(step,[status(thm)],[t124527,t25628]) ).
cnf(t124529,plain,
additive_inverse(X1) = multiply(add(X2,multiply(X1,additive_inverse(add(X1,multiply(X1,X2))))),X1),
inference(step,[status(thm)],[t124528,t32462]) ).
cnf(t39610,plain,
multiply(add(X1,multiply(X2,additive_inverse(add(X2,multiply(X2,X1))))),X2) = additive_inverse(X2),
inference(orient,[status(thm)],[t124529]) ).
cnf(t94617,plain,
add(X1,multiply(X2,multiply(X3,multiply(X1,X1)))) = multiply(add(X1,multiply(X2,X3)),multiply(X1,X1)),
inference(rw,[status(thm)],[t1184]) ).
cnf(t32128,plain,
add(multiply(X1,X2),additive_inverse(add(X3,Y3))) = additive_inverse(add(X3,add(Y3,multiply(X1,additive_inverse(X2))))),
inference(cp,[status(thm)],[t29034,t32022]) ).
cnf(t34397,plain,
additive_inverse(add(X1,add(X2,multiply(X3,additive_inverse(Y3))))) = add(multiply(X3,Y3),additive_inverse(add(X1,X2))),
inference(orient,[status(thm)],[t32128]) ).
cnf(t34407,plain,
add(multiply(X1,X2),additive_inverse(add(X3,multiply(Y3,X2)))) = additive_inverse(add(X3,multiply(add(Y3,additive_inverse(X1)),X2))),
inference(cp,[status(thm)],[t34397,t27718]) ).
cnf(t28237,plain,
multiply(add(X1,additive_inverse(X2)),additive_inverse(X3)) = multiply(add(X2,additive_inverse(X1)),X3),
inference(cp,[status(thm)],[t25628,t28228]) ).
cnf(t28474,plain,
multiply(add(X1,additive_inverse(X2)),additive_inverse(X3)) = multiply(add(X2,additive_inverse(X1)),X3),
inference(orient,[status(thm)],[t28237]) ).
cnf(t32479,plain,
additive_inverse(add(X1,multiply(add(X2,additive_inverse(X3)),Y3))) = add(additive_inverse(X1),multiply(add(X3,additive_inverse(X2)),Y3)),
inference(cp,[status(thm)],[t32462,t28474]) ).
cnf(t39281,plain,
additive_inverse(add(X1,multiply(add(X2,additive_inverse(X3)),Y3))) = add(additive_inverse(X1),multiply(add(X3,additive_inverse(X2)),Y3)),
inference(orient,[status(thm)],[t32479]) ).
cnf(t124794,plain,
add(multiply(X1,X2),additive_inverse(add(X3,multiply(Y3,X2)))) = add(additive_inverse(X3),multiply(add(X1,additive_inverse(Y3)),X2)),
inference(step,[status(thm)],[t34407,t39281]) ).
cnf(t60246,plain,
add(multiply(X1,X2),additive_inverse(add(X3,multiply(Y3,X2)))) = add(additive_inverse(X3),multiply(add(X1,additive_inverse(Y3)),X2)),
inference(orient,[status(thm)],[t124794]) ).
cnf(t60248,plain,
add(additive_inverse(multiply(X1,X2)),multiply(add(X1,additive_inverse(X3)),X2)) = additive_inverse(multiply(X3,X2)),
inference(cp,[status(thm)],[t60246,t29121]) ).
cnf(t124795,plain,
add(multiply(X1,additive_inverse(X2)),multiply(add(X1,additive_inverse(X3)),X2)) = additive_inverse(multiply(X3,X2)),
inference(step,[status(thm)],[t60248,t32022]) ).
cnf(t124796,plain,
add(multiply(X1,additive_inverse(X2)),multiply(add(X1,additive_inverse(X3)),X2)) = multiply(X3,additive_inverse(X2)),
inference(step,[status(thm)],[t124795,t32022]) ).
cnf(t60690,plain,
add(multiply(X1,additive_inverse(X2)),multiply(add(X1,additive_inverse(X3)),X2)) = multiply(X3,additive_inverse(X2)),
inference(orient,[status(thm)],[t124796]) ).
cnf(t40610,plain,
multiply(multiply(X1,X2),X3) = multiply(X3,multiply(X3,multiply(X1,multiply(X2,X3)))),
inference(cp,[status(thm)],[t40546,t40]) ).
cnf(t124550,plain,
multiply(X1,multiply(X2,X3)) = multiply(X3,multiply(X3,multiply(X1,multiply(X2,X3)))),
inference(step,[status(thm)],[t40610,t40]) ).
cnf(t41201,plain,
multiply(X1,multiply(X1,multiply(X2,multiply(X3,X1)))) = multiply(X2,multiply(X3,X1)),
inference(orient,[status(thm)],[t124550]) ).
cnf(t40630,plain,
multiply(X1,multiply(multiply(X1,multiply(X2,X1)),X3)) = multiply(multiply(X2,X1),X3),
inference(cp,[status(thm)],[t40,t40546]) ).
cnf(t124551,plain,
multiply(X1,multiply(X1,multiply(multiply(X2,X1),X3))) = multiply(multiply(X2,X1),X3),
inference(step,[status(thm)],[t40630,t40]) ).
cnf(t124552,plain,
multiply(X1,multiply(X1,multiply(X2,multiply(X1,X3)))) = multiply(multiply(X2,X1),X3),
inference(step,[status(thm)],[t124551,t40]) ).
cnf(t124553,plain,
multiply(X1,multiply(X1,multiply(X2,multiply(X1,X3)))) = multiply(X2,multiply(X1,X3)),
inference(step,[status(thm)],[t124552,t40]) ).
cnf(t41428,plain,
multiply(X1,multiply(X1,multiply(X2,multiply(X1,X3)))) = multiply(X2,multiply(X1,X3)),
inference(orient,[status(thm)],[t124553]) ).
cnf(t41432,plain,
multiply(X1,multiply(X2,multiply(X1,multiply(X2,X1)))) = multiply(X2,multiply(X2,X1)),
inference(cp,[status(thm)],[t41428,t790]) ).
cnf(t41654,plain,
multiply(X1,multiply(X2,multiply(X1,multiply(X2,X1)))) = multiply(X2,multiply(X2,X1)),
inference(orient,[status(thm)],[t41432]) ).
cnf(t41809,plain,
multiply(X1,multiply(X1,multiply(X2,multiply(X1,multiply(X2,X1))))) = multiply(multiply(X2,multiply(X1,multiply(X2,X1))),multiply(X1,multiply(multiply(X2,multiply(X1,multiply(X2,X1))),multiply(X2,multiply(X2,X1))))),
inference(cp,[status(thm)],[t41654,t41654]) ).
cnf(t124861,plain,
multiply(X2,multiply(X1,multiply(X2,X1))) = multiply(multiply(X2,multiply(X1,multiply(X2,X1))),multiply(X1,multiply(multiply(X2,multiply(X1,multiply(X2,X1))),multiply(X2,multiply(X2,X1))))),
inference(step,[status(thm)],[t41809,t41428]) ).
cnf(t124862,plain,
multiply(X2,multiply(X1,multiply(X2,X1))) = multiply(X2,multiply(multiply(X1,multiply(X2,X1)),multiply(X1,multiply(multiply(X2,multiply(X1,multiply(X2,X1))),multiply(X2,multiply(X2,X1)))))),
inference(step,[status(thm)],[t124861,t40]) ).
cnf(t124863,plain,
multiply(X2,multiply(X1,multiply(X2,X1))) = multiply(X2,multiply(X1,multiply(multiply(X2,X1),multiply(X1,multiply(multiply(X2,multiply(X1,multiply(X2,X1))),multiply(X2,multiply(X2,X1))))))),
inference(step,[status(thm)],[t124862,t40]) ).
cnf(t124864,plain,
multiply(X2,multiply(X1,multiply(X2,X1))) = multiply(X2,multiply(X1,multiply(X2,multiply(X1,multiply(X1,multiply(multiply(X2,multiply(X1,multiply(X2,X1))),multiply(X2,multiply(X2,X1)))))))),
inference(step,[status(thm)],[t124863,t40]) ).
cnf(t124865,plain,
multiply(X2,multiply(X1,multiply(X2,X1))) = multiply(X2,multiply(X1,multiply(X2,multiply(X1,multiply(X1,multiply(X2,multiply(multiply(X1,multiply(X2,X1)),multiply(X2,multiply(X2,X1))))))))),
inference(step,[status(thm)],[t124864,t40]) ).
cnf(t124866,plain,
multiply(X2,multiply(X1,multiply(X2,X1))) = multiply(X2,multiply(X1,multiply(X2,multiply(X1,multiply(X1,multiply(X2,multiply(X1,multiply(multiply(X2,X1),multiply(X2,multiply(X2,X1)))))))))),
inference(step,[status(thm)],[t124865,t40]) ).
cnf(t124867,plain,
multiply(X2,multiply(X1,multiply(X2,X1))) = multiply(X2,multiply(X1,multiply(X2,multiply(X2,multiply(X1,multiply(multiply(X2,X1),multiply(X2,multiply(X2,X1)))))))),
inference(step,[status(thm)],[t124866,t41428]) ).
cnf(t124868,plain,
multiply(X2,multiply(X1,multiply(X2,X1))) = multiply(X2,multiply(X1,multiply(X2,multiply(X2,multiply(X1,multiply(X2,multiply(X1,multiply(X2,multiply(X2,X1))))))))),
inference(step,[status(thm)],[t124867,t40]) ).
cnf(t124869,plain,
multiply(X2,multiply(X1,multiply(X2,X1))) = multiply(X2,multiply(X1,multiply(X1,multiply(X2,multiply(X1,multiply(X2,multiply(X2,X1))))))),
inference(step,[status(thm)],[t124868,t41428]) ).
cnf(t124870,plain,
multiply(X2,multiply(X1,multiply(X2,X1))) = multiply(X2,multiply(X2,multiply(X1,multiply(X2,multiply(X2,X1))))),
inference(step,[status(thm)],[t124869,t41428]) ).
cnf(t124871,plain,
multiply(X2,multiply(X1,multiply(X2,X1))) = multiply(X1,multiply(X2,multiply(X2,X1))),
inference(step,[status(thm)],[t124870,t41428]) ).
cnf(t66083,plain,
multiply(X1,multiply(X2,multiply(X1,X2))) = multiply(X2,multiply(X1,multiply(X1,X2))),
inference(orient,[status(thm)],[t124871]) ).
cnf(t66570,plain,
multiply(X1,multiply(X1,X2)) = multiply(X2,multiply(X1,multiply(X2,multiply(X1,X2)))),
inference(cp,[status(thm)],[t41201,t66083]) ).
cnf(t66979,plain,
multiply(X1,multiply(X2,multiply(X1,multiply(X2,X1)))) = multiply(X2,multiply(X2,X1)),
inference(orient,[status(thm)],[t66570]) ).
cnf(t67239,plain,
multiply(add(X1,multiply(X2,multiply(X3,X2))),multiply(X3,X2)) = add(multiply(X1,multiply(X3,X2)),multiply(X3,multiply(X3,X2))),
inference(cp,[status(thm)],[t4415,t66979]) ).
cnf(t642,plain,
multiply(add(multiply(X1,X2),multiply(X3,Y3)),Y4) = add(multiply(X1,multiply(X2,Y4)),multiply(X3,multiply(Y3,Y4))),
inference(cp,[status(thm)],[t627,t40]) ).
cnf(t4069,plain,
add(multiply(X1,multiply(X2,X3)),multiply(Y3,multiply(Y4,X3))) = multiply(add(multiply(X1,X2),multiply(Y3,Y4)),X3),
inference(orient,[status(thm)],[t642]) ).
cnf(t125065,plain,
multiply(add(X1,multiply(X2,multiply(X3,X2))),multiply(X3,X2)) = multiply(add(multiply(X1,X3),multiply(X3,X3)),X2),
inference(step,[status(thm)],[t67239,t4069]) ).
cnf(t125066,plain,
multiply(add(X1,multiply(X2,multiply(X3,X2))),multiply(X3,X2)) = multiply(multiply(add(X1,X3),X3),X2),
inference(step,[status(thm)],[t125065,t27]) ).
cnf(t125067,plain,
multiply(add(X1,multiply(X2,multiply(X3,X2))),multiply(X3,X2)) = multiply(add(X1,X3),multiply(X3,X2)),
inference(step,[status(thm)],[t125066,t40]) ).
cnf(t87798,plain,
multiply(add(X1,multiply(X2,multiply(X3,X2))),multiply(X3,X2)) = multiply(add(X1,X3),multiply(X3,X2)),
inference(orient,[status(thm)],[t125067]) ).
cnf(t87812,plain,
multiply(add(X1,X2),multiply(X2,X1)) = multiply(multiply(X1,multiply(add(X1,X2),X1)),multiply(X2,X1)),
inference(cp,[status(thm)],[t87798,t100]) ).
cnf(t125110,plain,
multiply(add(X1,X2),multiply(X2,X1)) = multiply(X1,multiply(multiply(add(X1,X2),X1),multiply(X2,X1))),
inference(step,[status(thm)],[t87812,t40]) ).
cnf(t125111,plain,
multiply(add(X1,X2),multiply(X2,X1)) = multiply(X1,multiply(add(X1,X2),multiply(X1,multiply(X2,X1)))),
inference(step,[status(thm)],[t125110,t40]) ).
cnf(t55,plain,
multiply(X1,add(multiply(X1,multiply(X1,X2)),X3)) = add(multiply(X1,X2),multiply(X1,X3)),
inference(cp,[status(thm)],[t33,t51]) ).
cnf(t123769,plain,
multiply(X1,add(X3,multiply(X1,multiply(X1,X2)))) = add(multiply(X1,X2),multiply(X1,X3)),
inference(step,[status(thm)],[t55,t10]) ).
cnf(t123770,plain,
multiply(X1,add(X3,multiply(X1,multiply(X1,X2)))) = multiply(X1,add(X2,X3)),
inference(step,[status(thm)],[t123769,t33]) ).
cnf(t387,plain,
multiply(X1,add(X2,multiply(X1,multiply(X1,X3)))) = multiply(X1,add(X3,X2)),
inference(orient,[status(thm)],[t123770]) ).
cnf(t411,plain,
multiply(X1,multiply(add(X2,multiply(X1,multiply(X1,X3))),Y3)) = multiply(multiply(X1,add(X3,X2)),Y3),
inference(cp,[status(thm)],[t40,t387]) ).
cnf(t123868,plain,
multiply(X1,multiply(add(X2,multiply(X1,multiply(X1,X3))),Y3)) = multiply(X1,multiply(add(X3,X2),Y3)),
inference(step,[status(thm)],[t411,t40]) ).
cnf(t123869,plain,
multiply(X1,multiply(add(X2,multiply(X1,multiply(X1,X3))),Y3)) = multiply(X1,multiply(add(X2,X3),Y3)),
inference(step,[status(thm)],[t123868,t10]) ).
cnf(t2525,plain,
multiply(X1,multiply(add(X2,multiply(X1,multiply(X1,X3))),Y3)) = multiply(X1,multiply(add(X2,X3),Y3)),
inference(orient,[status(thm)],[t123869]) ).
cnf(t40552,plain,
multiply(add(X1,multiply(X2,multiply(X2,X3))),X2) = multiply(X2,multiply(X2,multiply(add(X1,X3),X2))),
inference(cp,[status(thm)],[t40546,t2525]) ).
cnf(t124548,plain,
multiply(add(X1,multiply(X2,multiply(X2,X3))),X2) = multiply(add(X1,X3),X2),
inference(step,[status(thm)],[t40552,t40546]) ).
cnf(t40933,plain,
multiply(add(X1,multiply(X2,multiply(X2,X3))),X2) = multiply(add(X1,X3),X2),
inference(orient,[status(thm)],[t124548]) ).
cnf(t40953,plain,
multiply(add(multiply(X1,X2),multiply(X3,X2)),Y3) = multiply(multiply(add(X1,multiply(Y3,multiply(Y3,X3))),X2),Y3),
inference(cp,[status(thm)],[t40933,t4415]) ).
cnf(t124944,plain,
multiply(multiply(add(X1,X3),X2),Y3) = multiply(multiply(add(X1,multiply(Y3,multiply(Y3,X3))),X2),Y3),
inference(step,[status(thm)],[t40953,t27]) ).
cnf(t124945,plain,
multiply(add(X1,X3),multiply(X2,Y3)) = multiply(multiply(add(X1,multiply(Y3,multiply(Y3,X3))),X2),Y3),
inference(step,[status(thm)],[t124944,t40]) ).
cnf(t124946,plain,
multiply(add(X1,X3),multiply(X2,Y3)) = multiply(add(X1,multiply(Y3,multiply(Y3,X3))),multiply(X2,Y3)),
inference(step,[status(thm)],[t124945,t40]) ).
cnf(t73622,plain,
multiply(add(X1,multiply(X2,multiply(X2,X3))),multiply(Y3,X2)) = multiply(add(X1,X3),multiply(Y3,X2)),
inference(orient,[status(thm)],[t124946]) ).
cnf(t40720,plain,
multiply(X1,add(X2,multiply(multiply(X1,multiply(X3,X1)),X2))) = multiply(add(X1,multiply(X3,X1)),X2),
inference(cp,[status(thm)],[t2243,t40546]) ).
cnf(t124912,plain,
multiply(X1,add(X2,multiply(X1,multiply(multiply(X3,X1),X2)))) = multiply(add(X1,multiply(X3,X1)),X2),
inference(step,[status(thm)],[t40720,t40]) ).
cnf(t124913,plain,
multiply(X1,add(X2,multiply(X1,multiply(X3,multiply(X1,X2))))) = multiply(add(X1,multiply(X3,X1)),X2),
inference(step,[status(thm)],[t124912,t40]) ).
cnf(t69765,plain,
multiply(X1,add(X2,multiply(X1,multiply(X3,multiply(X1,X2))))) = multiply(add(X1,multiply(X3,X1)),X2),
inference(orient,[status(thm)],[t124913]) ).
cnf(t69907,plain,
multiply(add(X1,multiply(X2,X1)),multiply(X2,X1)) = multiply(X1,add(multiply(X2,X1),multiply(X1,multiply(X1,multiply(X2,multiply(X2,X1)))))),
inference(cp,[status(thm)],[t69765,t66083]) ).
cnf(t124918,plain,
multiply(add(X1,multiply(X2,X1)),multiply(X2,X1)) = multiply(X1,add(multiply(X2,multiply(X2,X1)),multiply(X2,X1))),
inference(step,[status(thm)],[t69907,t387]) ).
cnf(t124919,plain,
multiply(add(X1,multiply(X2,X1)),multiply(X2,X1)) = multiply(X1,multiply(X2,add(multiply(X2,X1),X1))),
inference(step,[status(thm)],[t124918,t33]) ).
cnf(t124920,plain,
multiply(add(X1,multiply(X2,X1)),multiply(X2,X1)) = multiply(X1,multiply(X2,add(X1,multiply(X2,X1)))),
inference(step,[status(thm)],[t124919,t10]) ).
cnf(t70784,plain,
multiply(add(X1,multiply(X2,X1)),multiply(X2,X1)) = multiply(X1,multiply(X2,add(X1,multiply(X2,X1)))),
inference(orient,[status(thm)],[t124920]) ).
cnf(t70975,plain,
multiply(multiply(X1,multiply(X2,X1)),multiply(X2,add(multiply(X1,multiply(X2,X1)),multiply(X2,multiply(X1,multiply(X2,X1)))))) = multiply(add(multiply(X1,multiply(X2,X1)),multiply(X1,multiply(X2,multiply(X2,X1)))),multiply(X2,multiply(X1,multiply(X2,X1)))),
inference(cp,[status(thm)],[t70784,t66083]) ).
cnf(t124931,plain,
multiply(X1,multiply(multiply(X2,X1),multiply(X2,add(multiply(X1,multiply(X2,X1)),multiply(X2,multiply(X1,multiply(X2,X1))))))) = multiply(add(multiply(X1,multiply(X2,X1)),multiply(X1,multiply(X2,multiply(X2,X1)))),multiply(X2,multiply(X1,multiply(X2,X1)))),
inference(step,[status(thm)],[t70975,t40]) ).
cnf(t124932,plain,
multiply(X1,multiply(X2,multiply(X1,multiply(X2,add(multiply(X1,multiply(X2,X1)),multiply(X2,multiply(X1,multiply(X2,X1)))))))) = multiply(add(multiply(X1,multiply(X2,X1)),multiply(X1,multiply(X2,multiply(X2,X1)))),multiply(X2,multiply(X1,multiply(X2,X1)))),
inference(step,[status(thm)],[t124931,t40]) ).
cnf(t124933,plain,
multiply(X1,multiply(X2,multiply(X1,multiply(X2,multiply(add(X1,multiply(X2,X1)),multiply(X2,X1)))))) = multiply(add(multiply(X1,multiply(X2,X1)),multiply(X1,multiply(X2,multiply(X2,X1)))),multiply(X2,multiply(X1,multiply(X2,X1)))),
inference(step,[status(thm)],[t124932,t627]) ).
cnf(t124934,plain,
multiply(X1,multiply(X2,multiply(X1,multiply(X2,multiply(X1,multiply(X2,add(X1,multiply(X2,X1)))))))) = multiply(add(multiply(X1,multiply(X2,X1)),multiply(X1,multiply(X2,multiply(X2,X1)))),multiply(X2,multiply(X1,multiply(X2,X1)))),
inference(step,[status(thm)],[t124933,t70784]) ).
cnf(t124935,plain,
multiply(X1,multiply(X2,add(X1,multiply(X2,X1)))) = multiply(add(multiply(X1,multiply(X2,X1)),multiply(X1,multiply(X2,multiply(X2,X1)))),multiply(X2,multiply(X1,multiply(X2,X1)))),
inference(step,[status(thm)],[t124934,t3958]) ).
cnf(t124936,plain,
multiply(X1,multiply(X2,add(X1,multiply(X2,X1)))) = multiply(multiply(add(X1,multiply(X1,X2)),multiply(X2,X1)),multiply(X2,multiply(X1,multiply(X2,X1)))),
inference(step,[status(thm)],[t124935,t627]) ).
cnf(t124937,plain,
multiply(X1,multiply(X2,add(X1,multiply(X2,X1)))) = multiply(add(X1,multiply(X1,X2)),multiply(multiply(X2,X1),multiply(X2,multiply(X1,multiply(X2,X1))))),
inference(step,[status(thm)],[t124936,t40]) ).
cnf(t124938,plain,
multiply(X1,multiply(X2,add(X1,multiply(X2,X1)))) = multiply(add(X1,multiply(X1,X2)),multiply(X2,multiply(X1,multiply(X2,multiply(X1,multiply(X2,X1)))))),
inference(step,[status(thm)],[t124937,t40]) ).
cnf(t124939,plain,
multiply(X1,multiply(X2,add(X1,multiply(X2,X1)))) = multiply(add(X1,multiply(X1,X2)),multiply(X2,X1)),
inference(step,[status(thm)],[t124938,t790]) ).
cnf(t71761,plain,
multiply(add(X1,multiply(X1,X2)),multiply(X2,X1)) = multiply(X1,multiply(X2,add(X1,multiply(X2,X1)))),
inference(orient,[status(thm)],[t124939]) ).
cnf(t73626,plain,
multiply(add(X1,X2),multiply(multiply(X1,X2),X1)) = multiply(X1,multiply(multiply(X1,X2),add(X1,multiply(multiply(X1,X2),X1)))),
inference(cp,[status(thm)],[t73622,t71761]) ).
cnf(t124948,plain,
multiply(add(X1,X2),multiply(X1,multiply(X2,X1))) = multiply(X1,multiply(multiply(X1,X2),add(X1,multiply(multiply(X1,X2),X1)))),
inference(step,[status(thm)],[t73626,t40]) ).
cnf(t124949,plain,
multiply(add(X1,X2),multiply(X1,multiply(X2,X1))) = multiply(X1,multiply(X1,multiply(X2,add(X1,multiply(multiply(X1,X2),X1))))),
inference(step,[status(thm)],[t124948,t40]) ).
cnf(t124950,plain,
multiply(add(X1,X2),multiply(X1,multiply(X2,X1))) = multiply(X1,multiply(X1,multiply(X2,add(X1,multiply(X1,multiply(X2,X1)))))),
inference(step,[status(thm)],[t124949,t40]) ).
cnf(t124951,plain,
multiply(add(X1,X2),multiply(X1,multiply(X2,X1))) = multiply(X1,multiply(X1,multiply(X2,multiply(X1,multiply(add(X1,X2),X1))))),
inference(step,[status(thm)],[t124950,t100]) ).
cnf(t124952,plain,
multiply(add(X1,X2),multiply(X1,multiply(X2,X1))) = multiply(X2,multiply(X1,multiply(add(X1,X2),X1))),
inference(step,[status(thm)],[t124951,t41428]) ).
cnf(t74218,plain,
multiply(add(X1,X2),multiply(X1,multiply(X2,X1))) = multiply(X2,multiply(X1,multiply(add(X1,X2),X1))),
inference(orient,[status(thm)],[t124952]) ).
cnf(t125112,plain,
multiply(add(X1,X2),multiply(X2,X1)) = multiply(X1,multiply(X2,multiply(X1,multiply(add(X1,X2),X1)))),
inference(step,[status(thm)],[t125111,t74218]) ).
cnf(t93028,plain,
multiply(X1,multiply(X2,multiply(X1,multiply(add(X1,X2),X1)))) = multiply(add(X1,X2),multiply(X2,X1)),
inference(orient,[status(thm)],[t125112]) ).
cnf(t93145,plain,
multiply(add(X1,additive_inverse(add(X1,X2))),multiply(additive_inverse(add(X1,X2)),X1)) = multiply(X1,multiply(additive_inverse(add(X1,X2)),multiply(X1,multiply(additive_inverse(X2),X1)))),
inference(cp,[status(thm)],[t93028,t29121]) ).
cnf(t93413,plain,
multiply(add(X1,X2),multiply(X1,X2)) = multiply(X1,multiply(add(X1,X2),X2)),
inference(orient,[status(thm)],[t93145]) ).
cnf(t93799,plain,
multiply(X1,additive_inverse(multiply(X2,additive_inverse(X1)))) = add(multiply(X2,additive_inverse(multiply(X2,additive_inverse(X1)))),multiply(X2,multiply(add(X2,additive_inverse(X1)),additive_inverse(X1)))),
inference(cp,[status(thm)],[t60690,t93413]) ).
cnf(t125119,plain,
multiply(X1,multiply(X2,additive_inverse(additive_inverse(X1)))) = add(multiply(X2,additive_inverse(multiply(X2,additive_inverse(X1)))),multiply(X2,multiply(add(X2,additive_inverse(X1)),additive_inverse(X1)))),
inference(step,[status(thm)],[t93799,t25894]) ).
cnf(t125120,plain,
multiply(X1,multiply(X2,X1)) = add(multiply(X2,additive_inverse(multiply(X2,additive_inverse(X1)))),multiply(X2,multiply(add(X2,additive_inverse(X1)),additive_inverse(X1)))),
inference(step,[status(thm)],[t125119,t14771]) ).
cnf(t125121,plain,
multiply(X1,multiply(X2,X1)) = multiply(X2,add(additive_inverse(multiply(X2,additive_inverse(X1))),multiply(add(X2,additive_inverse(X1)),additive_inverse(X1)))),
inference(step,[status(thm)],[t125120,t33]) ).
cnf(t125122,plain,
multiply(X1,multiply(X2,X1)) = multiply(X2,additive_inverse(add(multiply(X2,additive_inverse(X1)),multiply(add(X2,additive_inverse(X1)),X1)))),
inference(step,[status(thm)],[t125121,t32462]) ).
cnf(t125123,plain,
multiply(X1,multiply(X2,X1)) = multiply(X2,add(additive_inverse(multiply(X2,additive_inverse(X1))),multiply(add(X1,additive_inverse(X2)),X1))),
inference(step,[status(thm)],[t125122,t39281]) ).
cnf(t125124,plain,
multiply(X1,multiply(X2,X1)) = multiply(X2,add(multiply(X2,additive_inverse(additive_inverse(X1))),multiply(add(X1,additive_inverse(X2)),X1))),
inference(step,[status(thm)],[t125123,t32022]) ).
cnf(t125125,plain,
multiply(X1,multiply(X2,X1)) = multiply(X2,add(multiply(X2,X1),multiply(add(X1,additive_inverse(X2)),X1))),
inference(step,[status(thm)],[t125124,t14771]) ).
cnf(t125126,plain,
multiply(X1,multiply(X2,X1)) = multiply(X2,multiply(add(X2,add(X1,additive_inverse(X2))),X1)),
inference(step,[status(thm)],[t125125,t27]) ).
cnf(t125127,plain,
multiply(X1,multiply(X2,X1)) = multiply(X2,multiply(X1,X1)),
inference(step,[status(thm)],[t125126,t46]) ).
cnf(t93918,plain,
multiply(X1,multiply(X2,X1)) = multiply(X2,multiply(X1,X1)),
inference(orient,[status(thm)],[t125127]) ).
cnf(t125299,plain,
add(X1,multiply(X2,multiply(X1,multiply(X3,X1)))) = multiply(add(X1,multiply(X2,X3)),multiply(X1,X1)),
inference(step,[status(thm)],[t94617,t93918]) ).
cnf(t125300,plain,
add(X1,multiply(X2,multiply(X1,multiply(X3,X1)))) = multiply(X1,multiply(add(X1,multiply(X2,X3)),X1)),
inference(step,[status(thm)],[t125299,t93918]) ).
cnf(t113340,plain,
add(X1,multiply(X2,multiply(X1,multiply(X3,X1)))) = multiply(X1,multiply(add(X1,multiply(X2,X3)),X1)),
inference(orient,[status(thm)],[t125300]) ).
cnf(t113800,plain,
additive_inverse(X1) = multiply(add(multiply(X1,multiply(X2,X1)),multiply(X1,additive_inverse(multiply(X1,multiply(add(X1,multiply(X1,X2)),X1))))),X1),
inference(cp,[status(thm)],[t39610,t113340]) ).
cnf(t125360,plain,
additive_inverse(X1) = multiply(multiply(X1,add(multiply(X2,X1),additive_inverse(multiply(X1,multiply(add(X1,multiply(X1,X2)),X1))))),X1),
inference(step,[status(thm)],[t113800,t33]) ).
cnf(t25992,plain,
multiply(X1,add(additive_inverse(multiply(X2,X3)),Y3)) = add(multiply(X1,multiply(X2,additive_inverse(X3))),multiply(X1,Y3)),
inference(cp,[status(thm)],[t33,t25894]) ).
cnf(t124419,plain,
multiply(X1,add(Y3,additive_inverse(multiply(X2,X3)))) = add(multiply(X1,multiply(X2,additive_inverse(X3))),multiply(X1,Y3)),
inference(step,[status(thm)],[t25992,t10]) ).
cnf(t124420,plain,
multiply(X1,add(Y3,additive_inverse(multiply(X2,X3)))) = multiply(X1,add(multiply(X2,additive_inverse(X3)),Y3)),
inference(step,[status(thm)],[t124419,t33]) ).
cnf(t124421,plain,
multiply(X1,add(Y3,additive_inverse(multiply(X2,X3)))) = multiply(X1,add(Y3,multiply(X2,additive_inverse(X3)))),
inference(step,[status(thm)],[t124420,t10]) ).
cnf(t30884,plain,
multiply(X1,add(X2,additive_inverse(multiply(X3,Y3)))) = multiply(X1,add(X2,multiply(X3,additive_inverse(Y3)))),
inference(orient,[status(thm)],[t124421]) ).
cnf(t125361,plain,
additive_inverse(X1) = multiply(multiply(X1,add(multiply(X2,X1),multiply(X1,additive_inverse(multiply(add(X1,multiply(X1,X2)),X1))))),X1),
inference(step,[status(thm)],[t125360,t30884]) ).
cnf(t125362,plain,
additive_inverse(X1) = multiply(X1,multiply(add(multiply(X2,X1),multiply(X1,additive_inverse(multiply(add(X1,multiply(X1,X2)),X1)))),X1)),
inference(step,[status(thm)],[t125361,t40]) ).
cnf(t393,plain,
multiply(X1,add(X2,multiply(X1,X3))) = multiply(X1,multiply(X1,add(X3,multiply(X1,X2)))),
inference(cp,[status(thm)],[t387,t33]) ).
cnf(t946,plain,
multiply(X1,multiply(X1,add(X2,multiply(X1,X3)))) = multiply(X1,add(X3,multiply(X1,X2))),
inference(orient,[status(thm)],[t393]) ).
cnf(t955,plain,
multiply(X1,add(multiply(X2,X3),multiply(X1,multiply(Y3,X3)))) = multiply(X1,multiply(X1,multiply(add(Y3,multiply(X1,X2)),X3))),
inference(cp,[status(thm)],[t946,t627]) ).
cnf(t123925,plain,
multiply(X1,multiply(add(X2,multiply(X1,Y3)),X3)) = multiply(X1,multiply(X1,multiply(add(Y3,multiply(X1,X2)),X3))),
inference(step,[status(thm)],[t955,t627]) ).
cnf(t4817,plain,
multiply(X1,multiply(X1,multiply(add(X2,multiply(X1,X3)),Y3))) = multiply(X1,multiply(add(X3,multiply(X1,X2)),Y3)),
inference(orient,[status(thm)],[t123925]) ).
cnf(t40548,plain,
multiply(add(X1,multiply(X2,X3)),X2) = multiply(X2,multiply(add(X3,multiply(X2,X1)),X2)),
inference(cp,[status(thm)],[t40546,t4817]) ).
cnf(t42027,plain,
multiply(X1,multiply(add(X2,multiply(X1,X3)),X1)) = multiply(add(X3,multiply(X1,X2)),X1),
inference(orient,[status(thm)],[t40548]) ).
cnf(t125363,plain,
additive_inverse(X1) = multiply(add(additive_inverse(multiply(add(X1,multiply(X1,X2)),X1)),multiply(X1,multiply(X2,X1))),X1),
inference(step,[status(thm)],[t125362,t42027]) ).
cnf(t94125,plain,
multiply(X1,X2) = multiply(X2,multiply(X1,multiply(X2,X2))),
inference(cp,[status(thm)],[t40546,t93918]) ).
cnf(t94620,plain,
multiply(X1,multiply(X2,multiply(X1,X1))) = multiply(X2,X1),
inference(orient,[status(thm)],[t94125]) ).
cnf(t94775,plain,
multiply(add(X1,multiply(X2,multiply(X3,X2))),X2) = add(multiply(X1,X2),multiply(X3,X2)),
inference(cp,[status(thm)],[t4415,t94620]) ).
cnf(t125161,plain,
multiply(add(X1,multiply(X2,multiply(X3,X2))),X2) = multiply(add(X1,X3),X2),
inference(step,[status(thm)],[t94775,t27]) ).
cnf(t97581,plain,
multiply(add(X1,multiply(X2,multiply(X3,X2))),X2) = multiply(add(X1,X3),X2),
inference(orient,[status(thm)],[t125161]) ).
cnf(t125364,plain,
additive_inverse(X1) = multiply(add(additive_inverse(multiply(add(X1,multiply(X1,X2)),X1)),X2),X1),
inference(step,[status(thm)],[t125363,t97581]) ).
cnf(t125365,plain,
additive_inverse(X1) = multiply(add(X2,additive_inverse(multiply(add(X1,multiply(X1,X2)),X1))),X1),
inference(step,[status(thm)],[t125364,t10]) ).
cnf(t125366,plain,
additive_inverse(X1) = multiply(add(X2,multiply(add(X1,multiply(X1,X2)),additive_inverse(X1))),X1),
inference(step,[status(thm)],[t125365,t32022]) ).
cnf(t13522,plain,
multiply(additive_inverse(X1),add(X1,X2)) = add(multiply(X1,additive_inverse(X1)),multiply(additive_inverse(X1),X2)),
inference(cp,[status(thm)],[t33,t13520]) ).
cnf(t16858,plain,
add(multiply(X1,additive_inverse(X1)),multiply(additive_inverse(X1),X2)) = multiply(additive_inverse(X1),add(X1,X2)),
inference(orient,[status(thm)],[t13522]) ).
cnf(t16859,plain,
multiply(additive_inverse(X1),add(X1,multiply(X2,additive_inverse(X1)))) = multiply(add(X1,multiply(additive_inverse(X1),X2)),additive_inverse(X1)),
inference(cp,[status(thm)],[t16858,t627]) ).
cnf(t23977,plain,
multiply(add(X1,multiply(additive_inverse(X1),X2)),additive_inverse(X1)) = multiply(additive_inverse(X1),add(X1,multiply(X2,additive_inverse(X1)))),
inference(orient,[status(thm)],[t16859]) ).
cnf(t24041,plain,
multiply(additive_inverse(additive_inverse(X1)),add(additive_inverse(X1),multiply(X2,additive_inverse(additive_inverse(X1))))) = multiply(add(additive_inverse(X1),multiply(X1,X2)),additive_inverse(additive_inverse(X1))),
inference(cp,[status(thm)],[t23977,t14771]) ).
cnf(t124216,plain,
multiply(X1,add(additive_inverse(X1),multiply(X2,additive_inverse(additive_inverse(X1))))) = multiply(add(additive_inverse(X1),multiply(X1,X2)),additive_inverse(additive_inverse(X1))),
inference(step,[status(thm)],[t24041,t14771]) ).
cnf(t124217,plain,
multiply(X1,add(additive_inverse(X1),multiply(X2,X1))) = multiply(add(additive_inverse(X1),multiply(X1,X2)),additive_inverse(additive_inverse(X1))),
inference(step,[status(thm)],[t124216,t14771]) ).
cnf(t124218,plain,
multiply(X1,add(additive_inverse(X1),multiply(X2,X1))) = multiply(add(additive_inverse(X1),multiply(X1,X2)),X1),
inference(step,[status(thm)],[t124217,t14771]) ).
cnf(t24127,plain,
multiply(add(additive_inverse(X1),multiply(X1,X2)),X1) = multiply(X1,add(additive_inverse(X1),multiply(X2,X1))),
inference(orient,[status(thm)],[t124218]) ).
cnf(t32513,plain,
multiply(X1,add(additive_inverse(X1),multiply(additive_inverse(X2),X1))) = multiply(additive_inverse(add(X1,multiply(X1,X2))),X1),
inference(cp,[status(thm)],[t24127,t32462]) ).
cnf(t124457,plain,
multiply(X1,add(additive_inverse(X1),multiply(X2,additive_inverse(X1)))) = multiply(additive_inverse(add(X1,multiply(X1,X2))),X1),
inference(step,[status(thm)],[t32513,t25628]) ).
cnf(t124458,plain,
multiply(X1,additive_inverse(add(X1,multiply(X2,X1)))) = multiply(additive_inverse(add(X1,multiply(X1,X2))),X1),
inference(step,[status(thm)],[t124457,t32462]) ).
cnf(t124459,plain,
multiply(X1,additive_inverse(add(X1,multiply(X2,X1)))) = multiply(add(X1,multiply(X1,X2)),additive_inverse(X1)),
inference(step,[status(thm)],[t124458,t25628]) ).
cnf(t32978,plain,
multiply(add(X1,multiply(X1,X2)),additive_inverse(X1)) = multiply(X1,additive_inverse(add(X1,multiply(X2,X1)))),
inference(orient,[status(thm)],[t124459]) ).
cnf(t125367,plain,
additive_inverse(X1) = multiply(add(X2,multiply(X1,additive_inverse(add(X1,multiply(X2,X1))))),X1),
inference(step,[status(thm)],[t125366,t32978]) ).
cnf(t121104,plain,
multiply(add(X1,multiply(X2,additive_inverse(add(X2,multiply(X1,X2))))),X2) = additive_inverse(X2),
inference(orient,[status(thm)],[t125367]) ).
cnf(t121572,plain,
multiply(add(X1,multiply(add(X2,multiply(X1,additive_inverse(add(X1,multiply(X2,X1))))),X1)),X3) = multiply(X1,multiply(X1,multiply(add(X1,additive_inverse(X1)),X3))),
inference(cp,[status(thm)],[t72767,t121104]) ).
cnf(t122493,plain,
multiply(add(X1,multiply(X1,multiply(X2,additive_inverse(X2)))),multiply(X2,X3)) = additive_identity,
inference(orient,[status(thm)],[t121572]) ).
cnf(t94022,plain,
multiply(additive_inverse(X1),multiply(X2,X2)) = multiply(X2,multiply(X1,additive_inverse(X2))),
inference(cp,[status(thm)],[t93918,t25628]) ).
cnf(t125194,plain,
multiply(X1,additive_inverse(multiply(X2,X2))) = multiply(X2,multiply(X1,additive_inverse(X2))),
inference(step,[status(thm)],[t94022,t25628]) ).
cnf(t125195,plain,
multiply(X1,multiply(X2,additive_inverse(X2))) = multiply(X2,multiply(X1,additive_inverse(X2))),
inference(step,[status(thm)],[t125194,t25894]) ).
cnf(t100527,plain,
multiply(X1,multiply(X2,additive_inverse(X2))) = multiply(X2,multiply(X1,additive_inverse(X2))),
inference(orient,[status(thm)],[t125195]) ).
cnf(t100970,plain,
multiply(X1,multiply(X1,multiply(X2,additive_inverse(X1)))) = multiply(multiply(X2,additive_inverse(X1)),multiply(X1,multiply(multiply(X2,additive_inverse(X1)),multiply(X2,multiply(X1,additive_inverse(X1)))))),
inference(cp,[status(thm)],[t66979,t100527]) ).
cnf(t125196,plain,
multiply(X2,additive_inverse(X1)) = multiply(multiply(X2,additive_inverse(X1)),multiply(X1,multiply(multiply(X2,additive_inverse(X1)),multiply(X2,multiply(X1,additive_inverse(X1)))))),
inference(step,[status(thm)],[t100970,t40394]) ).
cnf(t125197,plain,
multiply(X2,additive_inverse(X1)) = multiply(X2,multiply(additive_inverse(X1),multiply(X1,multiply(multiply(X2,additive_inverse(X1)),multiply(X2,multiply(X1,additive_inverse(X1))))))),
inference(step,[status(thm)],[t125196,t40]) ).
cnf(t125198,plain,
multiply(X2,additive_inverse(X1)) = multiply(X2,multiply(X1,additive_inverse(multiply(X1,multiply(multiply(X2,additive_inverse(X1)),multiply(X2,multiply(X1,additive_inverse(X1)))))))),
inference(step,[status(thm)],[t125197,t25628]) ).
cnf(t125199,plain,
multiply(X2,additive_inverse(X1)) = multiply(X2,multiply(X1,multiply(X1,additive_inverse(multiply(multiply(X2,additive_inverse(X1)),multiply(X2,multiply(X1,additive_inverse(X1)))))))),
inference(step,[status(thm)],[t125198,t25894]) ).
cnf(t125200,plain,
multiply(X2,additive_inverse(X1)) = multiply(X2,multiply(X1,multiply(X1,multiply(multiply(X2,additive_inverse(X1)),additive_inverse(multiply(X2,multiply(X1,additive_inverse(X1)))))))),
inference(step,[status(thm)],[t125199,t25894]) ).
cnf(t125201,plain,
multiply(X2,additive_inverse(X1)) = multiply(X2,multiply(X1,multiply(X1,multiply(X2,multiply(additive_inverse(X1),additive_inverse(multiply(X2,multiply(X1,additive_inverse(X1))))))))),
inference(step,[status(thm)],[t125200,t40]) ).
cnf(t125202,plain,
multiply(X2,additive_inverse(X1)) = multiply(X2,multiply(X1,multiply(X1,multiply(X2,multiply(X1,additive_inverse(additive_inverse(multiply(X2,multiply(X1,additive_inverse(X1)))))))))),
inference(step,[status(thm)],[t125201,t25628]) ).
cnf(t125203,plain,
multiply(X2,additive_inverse(X1)) = multiply(X2,multiply(X2,multiply(X1,additive_inverse(additive_inverse(multiply(X2,multiply(X1,additive_inverse(X1)))))))),
inference(step,[status(thm)],[t125202,t41428]) ).
cnf(t125204,plain,
multiply(X2,additive_inverse(X1)) = multiply(X2,multiply(X2,multiply(X1,multiply(X2,multiply(X1,additive_inverse(X1)))))),
inference(step,[status(thm)],[t125203,t14771]) ).
cnf(t125205,plain,
multiply(X2,additive_inverse(X1)) = multiply(X1,multiply(X2,multiply(X1,additive_inverse(X1)))),
inference(step,[status(thm)],[t125204,t41428]) ).
cnf(t101074,plain,
multiply(X1,multiply(X2,multiply(X1,additive_inverse(X1)))) = multiply(X2,additive_inverse(X1)),
inference(orient,[status(thm)],[t125205]) ).
cnf(t122497,plain,
additive_identity = multiply(X1,additive_inverse(add(X2,multiply(X2,multiply(X1,additive_inverse(X1)))))),
inference(cp,[status(thm)],[t122493,t101074]) ).
cnf(t32585,plain,
add(additive_inverse(X1),multiply(multiply(X2,X3),Y3)) = additive_inverse(add(X1,multiply(X2,multiply(X3,additive_inverse(Y3))))),
inference(cp,[status(thm)],[t32559,t40]) ).
cnf(t124473,plain,
add(additive_inverse(X1),multiply(X2,multiply(X3,Y3))) = additive_inverse(add(X1,multiply(X2,multiply(X3,additive_inverse(Y3))))),
inference(step,[status(thm)],[t32585,t40]) ).
cnf(t34815,plain,
additive_inverse(add(X1,multiply(X2,multiply(X3,additive_inverse(Y3))))) = add(additive_inverse(X1),multiply(X2,multiply(X3,Y3))),
inference(orient,[status(thm)],[t124473]) ).
cnf(t125380,plain,
additive_identity = multiply(X1,add(additive_inverse(X2),multiply(X2,multiply(X1,X1)))),
inference(step,[status(thm)],[t122497,t34815]) ).
cnf(t125381,plain,
additive_identity = multiply(X1,add(additive_inverse(X2),multiply(X1,multiply(X2,X1)))),
inference(step,[status(thm)],[t125380,t93918]) ).
cnf(t40631,plain,
multiply(X1,add(multiply(X1,multiply(X2,X1)),X3)) = add(multiply(X2,X1),multiply(X1,X3)),
inference(cp,[status(thm)],[t33,t40546]) ).
cnf(t124555,plain,
multiply(X1,add(X3,multiply(X1,multiply(X2,X1)))) = add(multiply(X2,X1),multiply(X1,X3)),
inference(step,[status(thm)],[t40631,t10]) ).
cnf(t124556,plain,
multiply(X1,add(X3,multiply(X1,multiply(X2,X1)))) = add(multiply(X1,X3),multiply(X2,X1)),
inference(step,[status(thm)],[t124555,t10]) ).
cnf(t42299,plain,
multiply(X1,add(X2,multiply(X1,multiply(X3,X1)))) = add(multiply(X1,X2),multiply(X3,X1)),
inference(orient,[status(thm)],[t124556]) ).
cnf(t125382,plain,
additive_identity = add(multiply(X1,additive_inverse(X2)),multiply(X2,X1)),
inference(step,[status(thm)],[t125381,t42299]) ).
cnf(t125383,plain,
additive_identity = add(multiply(X2,X1),multiply(X1,additive_inverse(X2))),
inference(step,[status(thm)],[t125382,t10]) ).
cnf(t123004,plain,
add(multiply(X1,X2),multiply(X2,additive_inverse(X1))) = additive_identity,
inference(orient,[status(thm)],[t125383]) ).
cnf(t123287,plain,
additive_inverse(multiply(X1,additive_inverse(X2))) = add(multiply(X2,X1),additive_inverse(additive_identity)),
inference(cp,[status(thm)],[t29121,t123004]) ).
cnf(t125384,plain,
multiply(X1,additive_inverse(additive_inverse(X2))) = add(multiply(X2,X1),additive_inverse(additive_identity)),
inference(step,[status(thm)],[t123287,t32022]) ).
cnf(t125385,plain,
multiply(X1,X2) = add(multiply(X2,X1),additive_inverse(additive_identity)),
inference(step,[status(thm)],[t125384,t14771]) ).
cnf(t125386,plain,
multiply(X1,X2) = add(additive_inverse(additive_identity),multiply(X2,X1)),
inference(step,[status(thm)],[t125385,t10]) ).
cnf(t125387,plain,
multiply(X1,X2) = add(additive_identity,multiply(X2,X1)),
inference(step,[status(thm)],[t125386,t11615]) ).
cnf(t125388,plain,
multiply(X1,X2) = multiply(X2,X1),
inference(step,[status(thm)],[t125387,t283]) ).
cnf(t123353,plain,
multiply(X1,X2) = multiply(X2,X1),
inference(orient,[status(thm)],[t125388]) ).
cnf(goal_0,negated_conjecture,
multiply(b,a) != multiply(a,b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
multiply(b,a) != multiply(b,a),
inference(rw,[status(thm)],[goal_0,t123353]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : RNG009-5 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.12/0.38 % Computer : n008.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Thu Sep 24 07:44:40 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.38 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 50.39/7.07 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 50.39/7.07 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------