%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : BOO031-1 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n003.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 12:59:40 PM UTC 2026
% Result : Unsatisfiable 22.41s 8.43s
% Output : CNFRefutation 22.41s
% Verified :
% SZS Type : Refutation
% Derivation depth : 47
% Number of leaves : 12
% Syntax : Number of clauses : 231 ( 231 unt; 0 nHn; 7 RR)
% Number of literals : 231 ( 230 equ; 2 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 5 con; 0-2 aty)
% Number of variables : 544 ( 76 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t10,axiom,
multiply(add(X1,X2),multiply(add(X2,X3),add(X3,X1))) = add(multiply(X1,X2),add(multiply(X2,X3),multiply(X3,X1))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t180,plain,
add(multiply(X1,X2),add(multiply(X2,X3),multiply(X3,X1))) = multiply(add(X1,X2),multiply(add(X2,X3),add(X3,X1))),
inference(orient,[status(thm)],[t10]) ).
cnf(t8,axiom,
multiply(multiply(X1,X2),X3) = multiply(X1,multiply(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t16,plain,
multiply(multiply(X1,X2),X3) = multiply(X1,multiply(X2,X3)),
inference(orient,[status(thm)],[t8]) ).
cnf(t5,axiom,
multiply(X1,add(X2,add(X1,X3))) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t56,plain,
multiply(X1,add(X2,add(X1,X3))) = X1,
inference(orient,[status(thm)],[t5]) ).
cnf(t2,axiom,
add(multiply(X1,inverse(X1)),X2) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t1,axiom,
multiply(X1,inverse(X1)) = n0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t12,plain,
multiply(X1,inverse(X1)) = n0,
inference(orient,[status(thm)],[t1]) ).
cnf(t10370,plain,
add(n0,X2) = X2,
inference(step,[status(thm)],[t2,t12]) ).
cnf(t19,plain,
add(n0,X1) = X1,
inference(orient,[status(thm)],[t10370]) ).
cnf(t61,plain,
X1 = multiply(X1,add(X1,X2)),
inference(cp,[status(thm)],[t56,t19]) ).
cnf(t80,plain,
multiply(X1,add(X1,X2)) = X1,
inference(orient,[status(thm)],[t61]) ).
cnf(t4,axiom,
add(X1,multiply(X2,multiply(X1,X3))) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t32,plain,
add(X1,multiply(X2,multiply(X1,X3))) = X1,
inference(orient,[status(thm)],[t4]) ).
cnf(t83,plain,
X1 = multiply(X1,X1),
inference(cp,[status(thm)],[t80,t32]) ).
cnf(t85,plain,
multiply(X1,X1) = X1,
inference(orient,[status(thm)],[t83]) ).
cnf(t87,plain,
multiply(X1,multiply(X1,X2)) = multiply(X1,X2),
inference(cp,[status(thm)],[t16,t85]) ).
cnf(t116,plain,
multiply(X1,multiply(X1,X2)) = multiply(X1,X2),
inference(orient,[status(thm)],[t87]) ).
cnf(t204,plain,
multiply(add(X1,X2),multiply(add(X2,multiply(X2,X3)),add(multiply(X2,X3),X1))) = add(multiply(X1,X2),add(multiply(X2,X3),multiply(multiply(X2,X3),X1))),
inference(cp,[status(thm)],[t180,t116]) ).
cnf(t3,axiom,
multiply(add(X1,inverse(X1)),X2) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t0,axiom,
add(X1,inverse(X1)) = n1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t11,plain,
add(X1,inverse(X1)) = n1,
inference(orient,[status(thm)],[t0]) ).
cnf(t10371,plain,
multiply(n1,X2) = X2,
inference(step,[status(thm)],[t3,t11]) ).
cnf(t29,plain,
multiply(n1,X1) = X1,
inference(orient,[status(thm)],[t10371]) ).
cnf(t39,plain,
X1 = add(X1,multiply(X1,X2)),
inference(cp,[status(thm)],[t32,t29]) ).
cnf(t66,plain,
add(X1,multiply(X1,X2)) = X1,
inference(orient,[status(thm)],[t39]) ).
cnf(t10536,plain,
multiply(add(X1,X2),multiply(X2,add(multiply(X2,X3),X1))) = add(multiply(X1,X2),add(multiply(X2,X3),multiply(multiply(X2,X3),X1))),
inference(step,[status(thm)],[t204,t66]) ).
cnf(t9,axiom,
multiply(multiply(add(X1,X2),add(X2,X3)),X2) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t10385,plain,
multiply(add(X1,X2),multiply(add(X2,X3),X2)) = X2,
inference(step,[status(thm)],[t9,t16]) ).
cnf(t148,plain,
multiply(add(X1,X2),multiply(add(X2,X3),X2)) = X2,
inference(orient,[status(thm)],[t10385]) ).
cnf(t150,plain,
X1 = multiply(add(X2,X1),multiply(n1,X1)),
inference(cp,[status(thm)],[t148,t11]) ).
cnf(t10386,plain,
X1 = multiply(add(X2,X1),X1),
inference(step,[status(thm)],[t150,t29]) ).
cnf(t165,plain,
multiply(add(X1,X2),X2) = X2,
inference(orient,[status(thm)],[t10386]) ).
cnf(t65,plain,
X1 = add(X1,multiply(X2,X1)),
inference(cp,[status(thm)],[t32,t56]) ).
cnf(t108,plain,
add(X1,multiply(X2,X1)) = X1,
inference(orient,[status(thm)],[t65]) ).
cnf(t168,plain,
multiply(X1,X2) = multiply(X2,multiply(X1,X2)),
inference(cp,[status(thm)],[t165,t108]) ).
cnf(t176,plain,
multiply(X1,multiply(X2,X1)) = multiply(X2,X1),
inference(orient,[status(thm)],[t168]) ).
cnf(t178,plain,
multiply(multiply(X1,X2),X3) = multiply(X3,multiply(X1,multiply(X2,X3))),
inference(cp,[status(thm)],[t176,t16]) ).
cnf(t10407,plain,
multiply(X1,multiply(X2,X3)) = multiply(X3,multiply(X1,multiply(X2,X3))),
inference(step,[status(thm)],[t178,t16]) ).
cnf(t632,plain,
multiply(X1,multiply(X2,multiply(X3,X1))) = multiply(X2,multiply(X3,X1)),
inference(orient,[status(thm)],[t10407]) ).
cnf(t638,plain,
multiply(X1,multiply(X2,multiply(X2,X3))) = multiply(multiply(X2,X3),multiply(X1,multiply(X2,X3))),
inference(cp,[status(thm)],[t632,t116]) ).
cnf(t10439,plain,
multiply(X1,multiply(X2,X3)) = multiply(multiply(X2,X3),multiply(X1,multiply(X2,X3))),
inference(step,[status(thm)],[t638,t116]) ).
cnf(t10440,plain,
multiply(X1,multiply(X2,X3)) = multiply(X2,multiply(X3,multiply(X1,multiply(X2,X3)))),
inference(step,[status(thm)],[t10439,t16]) ).
cnf(t10441,plain,
multiply(X1,multiply(X2,X3)) = multiply(X2,multiply(X1,multiply(X2,X3))),
inference(step,[status(thm)],[t10440,t632]) ).
cnf(t63,plain,
X1 = multiply(X1,add(X2,X1)),
inference(cp,[status(thm)],[t56,t32]) ).
cnf(t101,plain,
multiply(X1,add(X2,X1)) = X1,
inference(orient,[status(thm)],[t63]) ).
cnf(t106,plain,
multiply(X1,multiply(add(X2,X1),X3)) = multiply(X1,X3),
inference(cp,[status(thm)],[t16,t101]) ).
cnf(t473,plain,
multiply(X1,multiply(add(X2,X1),X3)) = multiply(X1,X3),
inference(orient,[status(thm)],[t106]) ).
cnf(t476,plain,
multiply(multiply(X1,X2),X3) = multiply(multiply(X1,X2),multiply(X1,X3)),
inference(cp,[status(thm)],[t473,t66]) ).
cnf(t10429,plain,
multiply(X1,multiply(X2,X3)) = multiply(multiply(X1,X2),multiply(X1,X3)),
inference(step,[status(thm)],[t476,t16]) ).
cnf(t10430,plain,
multiply(X1,multiply(X2,X3)) = multiply(X1,multiply(X2,multiply(X1,X3))),
inference(step,[status(thm)],[t10429,t16]) ).
cnf(t1003,plain,
multiply(X1,multiply(X2,multiply(X1,X3))) = multiply(X1,multiply(X2,X3)),
inference(orient,[status(thm)],[t10430]) ).
cnf(t10442,plain,
multiply(X1,multiply(X2,X3)) = multiply(X2,multiply(X1,X3)),
inference(step,[status(thm)],[t10441,t1003]) ).
cnf(t1319,plain,
multiply(X1,multiply(X2,X3)) = multiply(X2,multiply(X1,X3)),
inference(orient,[status(thm)],[t10442]) ).
cnf(t10537,plain,
multiply(X2,multiply(add(X1,X2),add(multiply(X2,X3),X1))) = add(multiply(X1,X2),add(multiply(X2,X3),multiply(multiply(X2,X3),X1))),
inference(step,[status(thm)],[t10536,t1319]) ).
cnf(t10538,plain,
multiply(X2,add(multiply(X2,X3),X1)) = add(multiply(X1,X2),add(multiply(X2,X3),multiply(multiply(X2,X3),X1))),
inference(step,[status(thm)],[t10537,t473]) ).
cnf(t10539,plain,
multiply(X2,add(multiply(X2,X3),X1)) = add(multiply(X1,X2),multiply(X2,X3)),
inference(step,[status(thm)],[t10538,t66]) ).
cnf(t4771,plain,
add(multiply(X1,X2),multiply(X2,X3)) = multiply(X2,add(multiply(X2,X3),X1)),
inference(orient,[status(thm)],[t10539]) ).
cnf(t4787,plain,
multiply(X1,add(multiply(X1,multiply(X2,X1)),X3)) = add(multiply(X3,X1),multiply(X2,X1)),
inference(cp,[status(thm)],[t4771,t176]) ).
cnf(t10562,plain,
multiply(X1,add(multiply(X2,X1),X3)) = add(multiply(X3,X1),multiply(X2,X1)),
inference(step,[status(thm)],[t4787,t176]) ).
cnf(t6117,plain,
add(multiply(X1,X2),multiply(X3,X2)) = multiply(X2,add(multiply(X3,X2),X1)),
inference(orient,[status(thm)],[t10562]) ).
cnf(t20,plain,
inverse(n0) = n1,
inference(cp,[status(thm)],[t19,t11]) ).
cnf(t21,plain,
inverse(n0) = n1,
inference(orient,[status(thm)],[t20]) ).
cnf(t22,plain,
n0 = multiply(n0,n1),
inference(cp,[status(thm)],[t12,t21]) ).
cnf(t23,plain,
multiply(n0,n1) = n0,
inference(orient,[status(thm)],[t22]) ).
cnf(t38,plain,
n0 = add(n0,multiply(X1,n0)),
inference(cp,[status(thm)],[t32,t23]) ).
cnf(t10374,plain,
n0 = multiply(X1,n0),
inference(step,[status(thm)],[t38,t19]) ).
cnf(t45,plain,
multiply(X1,n0) = n0,
inference(orient,[status(thm)],[t10374]) ).
cnf(t188,plain,
multiply(add(X1,n0),multiply(add(n0,X2),add(X2,X1))) = add(n0,add(multiply(n0,X2),multiply(X2,X1))),
inference(cp,[status(thm)],[t180,t45]) ).
cnf(t47,plain,
X1 = add(X1,multiply(X2,n0)),
inference(cp,[status(thm)],[t32,t45]) ).
cnf(t10375,plain,
X1 = add(X1,n0),
inference(step,[status(thm)],[t47,t45]) ).
cnf(t49,plain,
add(X1,n0) = X1,
inference(orient,[status(thm)],[t10375]) ).
cnf(t10390,plain,
multiply(X1,multiply(add(n0,X2),add(X2,X1))) = add(n0,add(multiply(n0,X2),multiply(X2,X1))),
inference(step,[status(thm)],[t188,t49]) ).
cnf(t10391,plain,
multiply(X1,multiply(X2,add(X2,X1))) = add(n0,add(multiply(n0,X2),multiply(X2,X1))),
inference(step,[status(thm)],[t10390,t19]) ).
cnf(t10392,plain,
multiply(X1,X2) = add(n0,add(multiply(n0,X2),multiply(X2,X1))),
inference(step,[status(thm)],[t10391,t80]) ).
cnf(t10393,plain,
multiply(X1,X2) = add(multiply(n0,X2),multiply(X2,X1)),
inference(step,[status(thm)],[t10392,t19]) ).
cnf(t37,plain,
n0 = multiply(X1,multiply(n0,X2)),
inference(cp,[status(thm)],[t32,t19]) ).
cnf(t51,plain,
multiply(X1,multiply(n0,X2)) = n0,
inference(orient,[status(thm)],[t37]) ).
cnf(t52,plain,
n0 = multiply(n0,X1),
inference(cp,[status(thm)],[t51,t29]) ).
cnf(t53,plain,
multiply(n0,X1) = n0,
inference(orient,[status(thm)],[t52]) ).
cnf(t10394,plain,
multiply(X1,X2) = add(n0,multiply(X2,X1)),
inference(step,[status(thm)],[t10393,t53]) ).
cnf(t10395,plain,
multiply(X1,X2) = multiply(X2,X1),
inference(step,[status(thm)],[t10394,t19]) ).
cnf(t242,plain,
multiply(X1,X2) = multiply(X2,X1),
inference(orient,[status(thm)],[t10395]) ).
cnf(t4789,plain,
multiply(X1,add(multiply(X1,X2),X3)) = add(multiply(X3,X1),multiply(X2,X1)),
inference(cp,[status(thm)],[t4771,t242]) ).
cnf(t10564,plain,
multiply(X1,add(multiply(X1,X2),X3)) = multiply(X1,add(multiply(X2,X1),X3)),
inference(step,[status(thm)],[t4789,t6117]) ).
cnf(t6322,plain,
multiply(X1,add(multiply(X1,X2),X3)) = multiply(X1,add(multiply(X2,X1),X3)),
inference(orient,[status(thm)],[t10564]) ).
cnf(t203,plain,
multiply(add(X1,multiply(X1,X2)),multiply(add(multiply(X1,X2),X3),add(X3,X1))) = add(multiply(X1,X2),add(multiply(multiply(X1,X2),X3),multiply(X3,X1))),
inference(cp,[status(thm)],[t180,t116]) ).
cnf(t10526,plain,
multiply(X1,multiply(add(multiply(X1,X2),X3),add(X3,X1))) = add(multiply(X1,X2),add(multiply(multiply(X1,X2),X3),multiply(X3,X1))),
inference(step,[status(thm)],[t203,t66]) ).
cnf(t10527,plain,
multiply(X1,multiply(add(multiply(X1,X2),X3),add(X3,X1))) = add(multiply(X1,X2),add(multiply(X1,multiply(X2,X3)),multiply(X3,X1))),
inference(step,[status(thm)],[t10526,t16]) ).
cnf(t6,axiom,
add(add(X1,X2),X3) = add(X1,add(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t13,plain,
add(add(X1,X2),X3) = add(X1,add(X2,X3)),
inference(orient,[status(thm)],[t6]) ).
cnf(t102,plain,
X1 = multiply(X1,add(X2,add(X3,X1))),
inference(cp,[status(thm)],[t101,t13]) ).
cnf(t408,plain,
multiply(X1,add(X2,add(X3,X1))) = X1,
inference(orient,[status(thm)],[t102]) ).
cnf(t412,plain,
multiply(X1,X2) = multiply(multiply(X1,X2),add(X3,X1)),
inference(cp,[status(thm)],[t408,t66]) ).
cnf(t10428,plain,
multiply(X1,X2) = multiply(X1,multiply(X2,add(X3,X1))),
inference(step,[status(thm)],[t412,t16]) ).
cnf(t951,plain,
multiply(X1,multiply(X2,add(X3,X1))) = multiply(X1,X2),
inference(orient,[status(thm)],[t10428]) ).
cnf(t10528,plain,
multiply(X1,add(multiply(X1,X2),X3)) = add(multiply(X1,X2),add(multiply(X1,multiply(X2,X3)),multiply(X3,X1))),
inference(step,[status(thm)],[t10527,t951]) ).
cnf(t112,plain,
add(X1,X2) = add(add(X1,X2),X1),
inference(cp,[status(thm)],[t108,t80]) ).
cnf(t10382,plain,
add(X1,X2) = add(X1,add(X2,X1)),
inference(step,[status(thm)],[t112,t13]) ).
cnf(t130,plain,
add(X1,add(X2,X1)) = add(X1,X2),
inference(orient,[status(thm)],[t10382]) ).
cnf(t133,plain,
add(X1,add(X2,X3)) = add(X1,add(X2,add(X3,X1))),
inference(cp,[status(thm)],[t130,t13]) ).
cnf(t527,plain,
add(X1,add(X2,add(X3,X1))) = add(X1,add(X2,X3)),
inference(orient,[status(thm)],[t133]) ).
cnf(t7,axiom,
add(add(multiply(X1,X2),multiply(X2,X3)),X2) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t10379,plain,
add(multiply(X1,X2),add(multiply(X2,X3),X2)) = X2,
inference(step,[status(thm)],[t7,t13]) ).
cnf(t88,plain,
add(multiply(X1,X2),add(multiply(X2,X3),X2)) = X2,
inference(orient,[status(thm)],[t10379]) ).
cnf(t90,plain,
X1 = add(multiply(X2,X1),add(n0,X1)),
inference(cp,[status(thm)],[t88,t12]) ).
cnf(t10380,plain,
X1 = add(multiply(X2,X1),X1),
inference(step,[status(thm)],[t90,t19]) ).
cnf(t119,plain,
add(multiply(X1,X2),X2) = X2,
inference(orient,[status(thm)],[t10380]) ).
cnf(t122,plain,
add(X1,X2) = add(X2,add(X1,X2)),
inference(cp,[status(thm)],[t119,t101]) ).
cnf(t10384,plain,
add(X1,X2) = add(X2,X1),
inference(step,[status(thm)],[t122,t130]) ).
cnf(t138,plain,
add(X1,X2) = add(X2,X1),
inference(orient,[status(thm)],[t10384]) ).
cnf(t531,plain,
add(X1,add(X2,X3)) = add(X1,add(add(X3,X1),X2)),
inference(cp,[status(thm)],[t527,t138]) ).
cnf(t10437,plain,
add(X1,add(X2,X3)) = add(X1,add(X3,add(X1,X2))),
inference(step,[status(thm)],[t531,t13]) ).
cnf(t134,plain,
add(X1,add(add(X2,X1),X3)) = add(add(X1,X2),X3),
inference(cp,[status(thm)],[t13,t130]) ).
cnf(t10405,plain,
add(X1,add(X2,add(X1,X3))) = add(add(X1,X2),X3),
inference(step,[status(thm)],[t134,t13]) ).
cnf(t10406,plain,
add(X1,add(X2,add(X1,X3))) = add(X1,add(X2,X3)),
inference(step,[status(thm)],[t10405,t13]) ).
cnf(t569,plain,
add(X1,add(X2,add(X1,X3))) = add(X1,add(X2,X3)),
inference(orient,[status(thm)],[t10406]) ).
cnf(t10438,plain,
add(X1,add(X2,X3)) = add(X1,add(X3,X2)),
inference(step,[status(thm)],[t10437,t569]) ).
cnf(t1240,plain,
add(X1,add(X2,X3)) = add(X1,add(X3,X2)),
inference(orient,[status(thm)],[t10438]) ).
cnf(t10529,plain,
multiply(X1,add(multiply(X1,X2),X3)) = add(multiply(X1,X2),add(multiply(X3,X1),multiply(X1,multiply(X2,X3)))),
inference(step,[status(thm)],[t10528,t1240]) ).
cnf(t187,plain,
multiply(add(multiply(multiply(X1,X2),X3),X1),multiply(add(X1,X2),add(X2,multiply(multiply(X1,X2),X3)))) = add(multiply(multiply(multiply(X1,X2),X3),X1),multiply(X1,X2)),
inference(cp,[status(thm)],[t180,t32]) ).
cnf(t2351,plain,
add(multiply(X1,X2),multiply(X2,multiply(X3,X1))) = multiply(X2,X1),
inference(orient,[status(thm)],[t187]) ).
cnf(t10530,plain,
multiply(X1,add(multiply(X1,X2),X3)) = add(multiply(X1,X2),multiply(X1,X3)),
inference(step,[status(thm)],[t10529,t2351]) ).
cnf(t4521,plain,
add(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,add(multiply(X1,X2),X3)),
inference(orient,[status(thm)],[t10530]) ).
cnf(t4528,plain,
multiply(X1,add(multiply(X1,multiply(X2,X1)),X3)) = add(multiply(X2,X1),multiply(X1,X3)),
inference(cp,[status(thm)],[t4521,t176]) ).
cnf(t10548,plain,
multiply(X1,add(multiply(X2,X1),X3)) = add(multiply(X2,X1),multiply(X1,X3)),
inference(step,[status(thm)],[t4528,t176]) ).
cnf(t10549,plain,
multiply(X1,add(multiply(X2,X1),X3)) = multiply(X1,add(multiply(X1,X3),X2)),
inference(step,[status(thm)],[t10548,t4771]) ).
cnf(t5038,plain,
multiply(X1,add(multiply(X2,X1),X3)) = multiply(X1,add(multiply(X1,X3),X2)),
inference(orient,[status(thm)],[t10549]) ).
cnf(t5047,plain,
multiply(X1,add(multiply(X1,X2),X3)) = multiply(X1,add(X2,multiply(X3,X1))),
inference(cp,[status(thm)],[t5038,t138]) ).
cnf(t6701,plain,
multiply(X1,add(multiply(X1,X2),X3)) = multiply(X1,add(X2,multiply(X3,X1))),
inference(orient,[status(thm)],[t5047]) ).
cnf(t10575,plain,
multiply(X1,add(X2,multiply(X3,X1))) = multiply(X1,add(multiply(X2,X1),X3)),
inference(step,[status(thm)],[t6322,t6701]) ).
cnf(t6709,plain,
multiply(X1,add(X2,multiply(X3,X1))) = multiply(X1,add(multiply(X2,X1),X3)),
inference(rw,[status(thm)],[t10575]) ).
cnf(t8169,plain,
multiply(X1,add(multiply(X2,X1),X3)) = multiply(X1,add(X2,multiply(X3,X1))),
inference(orient,[status(thm)],[t6709]) ).
cnf(t10593,plain,
add(multiply(X1,X2),multiply(X3,X2)) = multiply(X2,add(X3,multiply(X1,X2))),
inference(step,[status(thm)],[t6117,t8169]) ).
cnf(t8172,plain,
add(multiply(X1,X2),multiply(X3,X2)) = multiply(X2,add(X3,multiply(X1,X2))),
inference(orient,[status(thm)],[t10593]) ).
cnf(t71,plain,
add(X1,add(multiply(X1,X2),X3)) = add(X1,X3),
inference(cp,[status(thm)],[t13,t66]) ).
cnf(t364,plain,
add(X1,add(multiply(X1,X2),X3)) = add(X1,X3),
inference(orient,[status(thm)],[t71]) ).
cnf(t367,plain,
add(X1,add(X2,multiply(X1,X3))) = add(X1,add(multiply(X1,X3),X2)),
inference(cp,[status(thm)],[t364,t130]) ).
cnf(t10420,plain,
add(X1,add(X2,multiply(X1,X3))) = add(X1,X2),
inference(step,[status(thm)],[t367,t364]) ).
cnf(t740,plain,
add(X1,add(X2,multiply(X1,X3))) = add(X1,X2),
inference(orient,[status(thm)],[t10420]) ).
cnf(t181,plain,
multiply(add(X1,inverse(X1)),multiply(add(inverse(X1),X2),add(X2,X1))) = add(n0,add(multiply(inverse(X1),X2),multiply(X2,X1))),
inference(cp,[status(thm)],[t180,t12]) ).
cnf(t104,plain,
multiply(X1,multiply(X2,X3)) = multiply(multiply(X1,multiply(X2,X3)),X2),
inference(cp,[status(thm)],[t101,t32]) ).
cnf(t10402,plain,
multiply(X1,multiply(X2,X3)) = multiply(X1,multiply(multiply(X2,X3),X2)),
inference(step,[status(thm)],[t104,t16]) ).
cnf(t10403,plain,
multiply(X1,multiply(X2,X3)) = multiply(X1,multiply(X2,multiply(X3,X2))),
inference(step,[status(thm)],[t10402,t16]) ).
cnf(t10404,plain,
multiply(X1,multiply(X2,X3)) = multiply(X1,multiply(X3,X2)),
inference(step,[status(thm)],[t10403,t176]) ).
cnf(t427,plain,
multiply(X1,multiply(X2,X3)) = multiply(X1,multiply(X3,X2)),
inference(orient,[status(thm)],[t10404]) ).
cnf(t10447,plain,
multiply(add(X1,inverse(X1)),multiply(add(X2,X1),add(inverse(X1),X2))) = add(n0,add(multiply(inverse(X1),X2),multiply(X2,X1))),
inference(step,[status(thm)],[t181,t427]) ).
cnf(t10448,plain,
multiply(n1,multiply(add(X2,X1),add(inverse(X1),X2))) = add(n0,add(multiply(inverse(X1),X2),multiply(X2,X1))),
inference(step,[status(thm)],[t10447,t11]) ).
cnf(t10449,plain,
multiply(add(X2,X1),add(inverse(X1),X2)) = add(n0,add(multiply(inverse(X1),X2),multiply(X2,X1))),
inference(step,[status(thm)],[t10448,t29]) ).
cnf(t10450,plain,
multiply(add(X2,X1),add(inverse(X1),X2)) = add(multiply(inverse(X1),X2),multiply(X2,X1)),
inference(step,[status(thm)],[t10449,t19]) ).
cnf(t10451,plain,
multiply(add(X2,X1),add(inverse(X1),X2)) = add(multiply(X2,X1),multiply(inverse(X1),X2)),
inference(step,[status(thm)],[t10450,t138]) ).
cnf(t1634,plain,
add(multiply(X1,X2),multiply(inverse(X2),X1)) = multiply(add(X1,X2),add(inverse(X2),X1)),
inference(orient,[status(thm)],[t10451]) ).
cnf(t1651,plain,
multiply(add(X1,X2),add(inverse(X2),X1)) = add(multiply(X2,X1),multiply(inverse(X2),X1)),
inference(cp,[status(thm)],[t1634,t242]) ).
cnf(t4151,plain,
add(multiply(X1,X2),multiply(inverse(X1),X2)) = multiply(add(X2,X1),add(inverse(X1),X2)),
inference(orient,[status(thm)],[t1651]) ).
cnf(t4247,plain,
add(inverse(X1),multiply(X1,X2)) = add(inverse(X1),multiply(add(X2,X1),add(inverse(X1),X2))),
inference(cp,[status(thm)],[t740,t4151]) ).
cnf(t191,plain,
multiply(add(X1,X2),multiply(add(X2,add(X3,add(X2,Y3))),add(add(X3,add(X2,Y3)),X1))) = add(multiply(X1,X2),add(X2,multiply(add(X3,add(X2,Y3)),X1))),
inference(cp,[status(thm)],[t180,t56]) ).
cnf(t10477,plain,
multiply(add(X1,X2),multiply(add(X2,add(X3,Y3)),add(add(X3,add(X2,Y3)),X1))) = add(multiply(X1,X2),add(X2,multiply(add(X3,add(X2,Y3)),X1))),
inference(step,[status(thm)],[t191,t569]) ).
cnf(t10478,plain,
multiply(add(X1,X2),multiply(add(X2,add(X3,Y3)),add(X3,add(add(X2,Y3),X1)))) = add(multiply(X1,X2),add(X2,multiply(add(X3,add(X2,Y3)),X1))),
inference(step,[status(thm)],[t10477,t13]) ).
cnf(t10479,plain,
multiply(add(X1,X2),multiply(add(X2,add(X3,Y3)),add(X3,add(X2,add(Y3,X1))))) = add(multiply(X1,X2),add(X2,multiply(add(X3,add(X2,Y3)),X1))),
inference(step,[status(thm)],[t10478,t13]) ).
cnf(t143,plain,
add(X1,add(X2,X3)) = add(X2,add(X3,X1)),
inference(cp,[status(thm)],[t138,t13]) ).
cnf(t1546,plain,
add(X1,add(X2,X3)) = add(X2,add(X3,X1)),
inference(orient,[status(thm)],[t143]) ).
cnf(t10480,plain,
multiply(add(X1,X2),multiply(add(X2,add(X3,Y3)),add(X3,add(X2,add(Y3,X1))))) = add(X2,add(multiply(add(X3,add(X2,Y3)),X1),multiply(X1,X2))),
inference(step,[status(thm)],[t10479,t1546]) ).
cnf(t110,plain,
X1 = add(X1,multiply(X2,multiply(X3,X1))),
inference(cp,[status(thm)],[t108,t16]) ).
cnf(t497,plain,
add(X1,multiply(X2,multiply(X3,X1))) = X1,
inference(orient,[status(thm)],[t110]) ).
cnf(t499,plain,
add(X1,X2) = add(add(X1,X2),multiply(X3,X1)),
inference(cp,[status(thm)],[t497,t80]) ).
cnf(t10435,plain,
add(X1,X2) = add(X1,add(X2,multiply(X3,X1))),
inference(step,[status(thm)],[t499,t13]) ).
cnf(t1125,plain,
add(X1,add(X2,multiply(X3,X1))) = add(X1,X2),
inference(orient,[status(thm)],[t10435]) ).
cnf(t10481,plain,
multiply(add(X1,X2),multiply(add(X2,add(X3,Y3)),add(X3,add(X2,add(Y3,X1))))) = add(X2,multiply(add(X3,add(X2,Y3)),X1)),
inference(step,[status(thm)],[t10480,t1125]) ).
cnf(t2731,plain,
multiply(add(X1,X2),multiply(add(X2,add(X3,Y3)),add(X3,add(X2,add(Y3,X1))))) = add(X2,multiply(add(X3,add(X2,Y3)),X1)),
inference(orient,[status(thm)],[t10481]) ).
cnf(t2738,plain,
add(X1,multiply(add(n0,add(X1,X2)),X3)) = multiply(add(X3,X1),multiply(add(X1,X2),add(n0,add(X1,add(X2,X3))))),
inference(cp,[status(thm)],[t2731,t19]) ).
cnf(t10482,plain,
add(X1,multiply(add(X1,X2),X3)) = multiply(add(X3,X1),multiply(add(X1,X2),add(n0,add(X1,add(X2,X3))))),
inference(step,[status(thm)],[t2738,t19]) ).
cnf(t59,plain,
add(X1,X2) = multiply(add(X1,X2),add(X3,add(X1,add(X2,Y3)))),
inference(cp,[status(thm)],[t56,t13]) ).
cnf(t687,plain,
multiply(add(X1,X2),add(X3,add(X1,add(X2,Y3)))) = add(X1,X2),
inference(orient,[status(thm)],[t59]) ).
cnf(t10483,plain,
add(X1,multiply(add(X1,X2),X3)) = multiply(add(X3,X1),add(X1,X2)),
inference(step,[status(thm)],[t10482,t687]) ).
cnf(t2934,plain,
add(X1,multiply(add(X1,X2),X3)) = multiply(add(X3,X1),add(X1,X2)),
inference(orient,[status(thm)],[t10483]) ).
cnf(t2947,plain,
multiply(add(X1,X2),add(X2,X3)) = add(X2,multiply(X1,add(X2,X3))),
inference(cp,[status(thm)],[t2934,t242]) ).
cnf(t3133,plain,
add(X1,multiply(X2,add(X1,X3))) = multiply(add(X2,X1),add(X1,X3)),
inference(orient,[status(thm)],[t2947]) ).
cnf(t10517,plain,
add(inverse(X1),multiply(X1,X2)) = multiply(add(add(X2,X1),inverse(X1)),add(inverse(X1),X2)),
inference(step,[status(thm)],[t4247,t3133]) ).
cnf(t10518,plain,
add(inverse(X1),multiply(X1,X2)) = multiply(add(inverse(X1),X2),add(add(X2,X1),inverse(X1))),
inference(step,[status(thm)],[t10517,t242]) ).
cnf(t10519,plain,
add(inverse(X1),multiply(X1,X2)) = multiply(add(inverse(X1),X2),add(X2,add(X1,inverse(X1)))),
inference(step,[status(thm)],[t10518,t13]) ).
cnf(t10520,plain,
add(inverse(X1),multiply(X1,X2)) = multiply(add(inverse(X1),X2),add(X2,n1)),
inference(step,[status(thm)],[t10519,t11]) ).
cnf(t10521,plain,
add(inverse(X1),multiply(X1,X2)) = multiply(add(X2,n1),add(inverse(X1),X2)),
inference(step,[status(thm)],[t10520,t242]) ).
cnf(t69,plain,
n1 = add(n1,X1),
inference(cp,[status(thm)],[t66,t29]) ).
cnf(t72,plain,
add(n1,X1) = n1,
inference(orient,[status(thm)],[t69]) ).
cnf(t74,plain,
n1 = multiply(n1,add(X1,n1)),
inference(cp,[status(thm)],[t56,t72]) ).
cnf(t10378,plain,
n1 = add(X1,n1),
inference(step,[status(thm)],[t74,t29]) ).
cnf(t79,plain,
add(X1,n1) = n1,
inference(orient,[status(thm)],[t10378]) ).
cnf(t10522,plain,
add(inverse(X1),multiply(X1,X2)) = multiply(n1,add(inverse(X1),X2)),
inference(step,[status(thm)],[t10521,t79]) ).
cnf(t10523,plain,
add(inverse(X1),multiply(X1,X2)) = add(inverse(X1),X2),
inference(step,[status(thm)],[t10522,t29]) ).
cnf(t4282,plain,
add(inverse(X1),multiply(X1,X2)) = add(inverse(X1),X2),
inference(orient,[status(thm)],[t10523]) ).
cnf(t4302,plain,
add(inverse(X1),multiply(X2,multiply(X1,X3))) = add(inverse(X1),multiply(X1,multiply(X2,X3))),
inference(cp,[status(thm)],[t4282,t1003]) ).
cnf(t10604,plain,
add(inverse(X1),multiply(X2,multiply(X1,X3))) = add(inverse(X1),multiply(X2,X3)),
inference(step,[status(thm)],[t4302,t4282]) ).
cnf(t9135,plain,
add(inverse(X1),multiply(X2,multiply(X1,X3))) = add(inverse(X1),multiply(X2,X3)),
inference(orient,[status(thm)],[t10604]) ).
cnf(t5084,plain,
multiply(X1,add(multiply(X1,multiply(inverse(X1),X2)),X2)) = multiply(X1,multiply(add(X2,X1),add(inverse(X1),X2))),
inference(cp,[status(thm)],[t5038,t1634]) ).
cnf(t18,plain,
multiply(X1,multiply(inverse(X1),X2)) = multiply(n0,X2),
inference(cp,[status(thm)],[t16,t12]) ).
cnf(t10389,plain,
multiply(X1,multiply(inverse(X1),X2)) = n0,
inference(step,[status(thm)],[t18,t53]) ).
cnf(t230,plain,
multiply(X1,multiply(inverse(X1),X2)) = n0,
inference(orient,[status(thm)],[t10389]) ).
cnf(t10550,plain,
multiply(X1,add(n0,X2)) = multiply(X1,multiply(add(X2,X1),add(inverse(X1),X2))),
inference(step,[status(thm)],[t5084,t230]) ).
cnf(t10551,plain,
multiply(X1,X2) = multiply(X1,multiply(add(X2,X1),add(inverse(X1),X2))),
inference(step,[status(thm)],[t10550,t19]) ).
cnf(t10552,plain,
multiply(X1,X2) = multiply(X1,add(inverse(X1),X2)),
inference(step,[status(thm)],[t10551,t473]) ).
cnf(t5166,plain,
multiply(X1,add(inverse(X1),X2)) = multiply(X1,X2),
inference(orient,[status(thm)],[t10552]) ).
cnf(t1635,plain,
multiply(add(X1,inverse(X1)),add(inverse(inverse(X1)),X1)) = add(n0,multiply(inverse(inverse(X1)),X1)),
inference(cp,[status(thm)],[t1634,t12]) ).
cnf(t10452,plain,
multiply(n1,add(inverse(inverse(X1)),X1)) = add(n0,multiply(inverse(inverse(X1)),X1)),
inference(step,[status(thm)],[t1635,t11]) ).
cnf(t10453,plain,
add(inverse(inverse(X1)),X1) = add(n0,multiply(inverse(inverse(X1)),X1)),
inference(step,[status(thm)],[t10452,t29]) ).
cnf(t10454,plain,
add(X1,inverse(inverse(X1))) = add(n0,multiply(inverse(inverse(X1)),X1)),
inference(step,[status(thm)],[t10453,t138]) ).
cnf(t10455,plain,
add(X1,inverse(inverse(X1))) = multiply(inverse(inverse(X1)),X1),
inference(step,[status(thm)],[t10454,t19]) ).
cnf(t10456,plain,
add(X1,inverse(inverse(X1))) = multiply(X1,inverse(inverse(X1))),
inference(step,[status(thm)],[t10455,t242]) ).
cnf(t1725,plain,
add(X1,inverse(inverse(X1))) = multiply(X1,inverse(inverse(X1))),
inference(orient,[status(thm)],[t10456]) ).
cnf(t1731,plain,
inverse(inverse(X1)) = multiply(inverse(inverse(X1)),multiply(X1,inverse(inverse(X1)))),
inference(cp,[status(thm)],[t101,t1725]) ).
cnf(t10460,plain,
inverse(inverse(X1)) = multiply(X1,inverse(inverse(X1))),
inference(step,[status(thm)],[t1731,t176]) ).
cnf(t1730,plain,
X1 = multiply(X1,multiply(X1,inverse(inverse(X1)))),
inference(cp,[status(thm)],[t80,t1725]) ).
cnf(t10457,plain,
X1 = multiply(X1,inverse(inverse(X1))),
inference(step,[status(thm)],[t1730,t116]) ).
cnf(t1757,plain,
multiply(X1,inverse(inverse(X1))) = X1,
inference(orient,[status(thm)],[t10457]) ).
cnf(t10461,plain,
inverse(inverse(X1)) = X1,
inference(step,[status(thm)],[t10460,t1757]) ).
cnf(t1778,plain,
inverse(inverse(X1)) = X1,
inference(orient,[status(thm)],[t10461]) ).
cnf(t5179,plain,
multiply(inverse(X1),X2) = multiply(inverse(X1),add(X1,X2)),
inference(cp,[status(thm)],[t5166,t1778]) ).
cnf(t5309,plain,
multiply(inverse(X1),add(X1,X2)) = multiply(inverse(X1),X2),
inference(orient,[status(thm)],[t5179]) ).
cnf(t9164,plain,
add(inverse(inverse(X1)),multiply(X2,add(X1,X3))) = add(inverse(inverse(X1)),multiply(X2,multiply(inverse(X1),X3))),
inference(cp,[status(thm)],[t9135,t5309]) ).
cnf(t10605,plain,
add(X1,multiply(X2,add(X1,X3))) = add(inverse(inverse(X1)),multiply(X2,multiply(inverse(X1),X3))),
inference(step,[status(thm)],[t9164,t1778]) ).
cnf(t10606,plain,
multiply(add(X2,X1),add(X1,X3)) = add(inverse(inverse(X1)),multiply(X2,multiply(inverse(X1),X3))),
inference(step,[status(thm)],[t10605,t3133]) ).
cnf(t10607,plain,
multiply(add(X2,X1),add(X1,X3)) = add(inverse(inverse(X1)),multiply(X2,X3)),
inference(step,[status(thm)],[t10606,t9135]) ).
cnf(t10608,plain,
multiply(add(X2,X1),add(X1,X3)) = add(X1,multiply(X2,X3)),
inference(step,[status(thm)],[t10607,t1778]) ).
cnf(t9243,plain,
multiply(add(X1,X2),add(X2,X3)) = add(X2,multiply(X1,X3)),
inference(orient,[status(thm)],[t10608]) ).
cnf(t9392,plain,
multiply(X1,add(X2,X3)) = multiply(X1,add(X3,multiply(X2,X1))),
inference(cp,[status(thm)],[t951,t9243]) ).
cnf(t10241,plain,
multiply(X1,add(X2,multiply(X3,X1))) = multiply(X1,add(X3,X2)),
inference(orient,[status(thm)],[t9392]) ).
cnf(t10635,plain,
add(multiply(X1,X2),multiply(X3,X2)) = multiply(X2,add(X1,X3)),
inference(step,[status(thm)],[t8172,t10241]) ).
cnf(t10249,plain,
add(multiply(X1,X2),multiply(X3,X2)) = multiply(X2,add(X1,X3)),
inference(orient,[status(thm)],[t10635]) ).
cnf(goal_0,negated_conjecture,
add(multiply(b,a),multiply(c,a)) != multiply(a,add(b,c)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
multiply(a,add(b,c)) != multiply(a,add(b,c)),
inference(rw,[status(thm)],[goal_0,t10249]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : BOO031-1 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/5.39 % Computer : n003.cluster.edu
% 0.09/5.39 % Model : x86_64 x86_64
% 0.09/5.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.39 % Memory : 8046.5625MB
% 0.09/5.39 % OS : Linux 6.8.0-71-generic
% 0.09/5.39 % CPULimit : 300
% 0.09/5.39 % WCLimit : 300
% 0.09/5.39 % DateTime : Fri Sep 25 06:38:13 UTC 2026
% 0.09/5.39 % CPUTime :
% 0.09/5.39 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 22.41/8.43 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 22.41/8.43 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------