%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : BOO016-2 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n005.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:38 PM UTC 2026
% Result : Unsatisfiable 5.09s 1.46s
% Output : CNFRefutation 5.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 58
% Number of leaves : 15
% Syntax : Number of clauses : 167 ( 167 unt; 0 nHn; 84 RR)
% Number of literals : 167 ( 166 equ; 6 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 6 con; 0-2 aty)
% Number of variables : 110 ( 2 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t9,axiom,
add(X1,X2) = add(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t68,plain,
add(X1,X2) = add(X2,X1),
inference(orient,[status(thm)],[t9]) ).
cnf(t11,axiom,
add(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,add(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t21,plain,
add(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,add(X2,X3)),
inference(orient,[status(thm)],[t11]) ).
cnf(t13,axiom,
multiply(add(X1,X2),add(X1,X3)) = add(X1,multiply(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t50,plain,
multiply(add(X1,X2),add(X1,X3)) = add(X1,multiply(X2,X3)),
inference(orient,[status(thm)],[t13]) ).
cnf(t15,axiom,
sFlat0 = add(x,z),
introduced(definition) ).
cnf(t1199,plain,
sFlat0 = add(z,x),
inference(step,[status(thm)],[t15,t68]) ).
cnf(t81,plain,
add(z,x) = sFlat0,
inference(orient,[status(thm)],[t1199]) ).
cnf(t83,plain,
add(z,multiply(X1,x)) = multiply(add(z,X1),sFlat0),
inference(cp,[status(thm)],[t50,t81]) ).
cnf(t12,axiom,
add(multiply(X1,X2),multiply(X3,X2)) = multiply(add(X1,X3),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t30,plain,
add(multiply(X1,X2),multiply(X3,X2)) = multiply(add(X1,X3),X2),
inference(orient,[status(thm)],[t12]) ).
cnf(t4,axiom,
multiply(x,y) = z,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t10,axiom,
multiply(X1,X2) = multiply(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t20,plain,
multiply(X1,X2) = multiply(X2,X1),
inference(orient,[status(thm)],[t10]) ).
cnf(t1198,plain,
multiply(y,x) = z,
inference(step,[status(thm)],[t4,t20]) ).
cnf(t63,plain,
multiply(y,x) = z,
inference(orient,[status(thm)],[t1198]) ).
cnf(t66,plain,
multiply(add(y,X1),x) = add(z,multiply(X1,x)),
inference(cp,[status(thm)],[t30,t63]) ).
cnf(t1216,plain,
multiply(x,add(y,X1)) = add(z,multiply(X1,x)),
inference(step,[status(thm)],[t66,t20]) ).
cnf(t205,plain,
add(z,multiply(X1,x)) = multiply(x,add(y,X1)),
inference(orient,[status(thm)],[t1216]) ).
cnf(t1221,plain,
multiply(x,add(y,X1)) = multiply(add(z,X1),sFlat0),
inference(step,[status(thm)],[t83,t205]) ).
cnf(t1222,plain,
multiply(x,add(y,X1)) = multiply(sFlat0,add(z,X1)),
inference(step,[status(thm)],[t1221,t20]) ).
cnf(t256,plain,
multiply(x,add(y,X1)) = multiply(sFlat0,add(z,X1)),
inference(orient,[status(thm)],[t1222]) ).
cnf(t0,axiom,
add(X1,additive_identity) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t18,plain,
add(X1,additive_identity) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t262,plain,
multiply(sFlat0,add(z,additive_identity)) = multiply(x,y),
inference(cp,[status(thm)],[t256,t18]) ).
cnf(t1226,plain,
multiply(sFlat0,z) = multiply(x,y),
inference(step,[status(thm)],[t262,t18]) ).
cnf(t1227,plain,
multiply(sFlat0,z) = multiply(y,x),
inference(step,[status(thm)],[t1226,t20]) ).
cnf(t1228,plain,
multiply(sFlat0,z) = z,
inference(step,[status(thm)],[t1227,t63]) ).
cnf(t273,plain,
multiply(sFlat0,z) = z,
inference(orient,[status(thm)],[t1228]) ).
cnf(t274,plain,
multiply(sFlat0,add(z,X1)) = add(z,multiply(sFlat0,X1)),
inference(cp,[status(thm)],[t21,t273]) ).
cnf(t437,plain,
add(z,multiply(sFlat0,X1)) = multiply(sFlat0,add(z,X1)),
inference(orient,[status(thm)],[t274]) ).
cnf(t64,plain,
multiply(y,add(x,X1)) = add(z,multiply(y,X1)),
inference(cp,[status(thm)],[t21,t63]) ).
cnf(t178,plain,
add(z,multiply(y,X1)) = multiply(y,add(x,X1)),
inference(orient,[status(thm)],[t64]) ).
cnf(t184,plain,
multiply(y,add(x,X1)) = add(z,multiply(X1,y)),
inference(cp,[status(thm)],[t178,t20]) ).
cnf(t354,plain,
add(z,multiply(X1,y)) = multiply(y,add(x,X1)),
inference(orient,[status(thm)],[t184]) ).
cnf(t439,plain,
multiply(sFlat0,add(z,y)) = multiply(y,add(x,sFlat0)),
inference(cp,[status(thm)],[t437,t354]) ).
cnf(t206,plain,
multiply(x,add(y,y)) = multiply(y,add(x,x)),
inference(cp,[status(thm)],[t205,t178]) ).
cnf(t180,plain,
multiply(y,add(x,x)) = add(z,z),
inference(cp,[status(thm)],[t178,t63]) ).
cnf(t189,plain,
multiply(y,add(x,x)) = add(z,z),
inference(orient,[status(thm)],[t180]) ).
cnf(t1217,plain,
multiply(x,add(y,y)) = add(z,z),
inference(step,[status(thm)],[t206,t189]) ).
cnf(t214,plain,
multiply(x,add(y,y)) = add(z,z),
inference(orient,[status(thm)],[t1217]) ).
cnf(t1225,plain,
multiply(sFlat0,add(z,y)) = add(z,z),
inference(step,[status(thm)],[t214,t256]) ).
cnf(t272,plain,
multiply(sFlat0,add(z,y)) = add(z,z),
inference(rw,[status(thm)],[t1225]) ).
cnf(t280,plain,
multiply(sFlat0,add(z,y)) = add(z,z),
inference(orient,[status(thm)],[t272]) ).
cnf(t1251,plain,
add(z,z) = multiply(y,add(x,sFlat0)),
inference(step,[status(thm)],[t439,t280]) ).
cnf(t1252,plain,
add(z,z) = multiply(y,add(sFlat0,x)),
inference(step,[status(thm)],[t1251,t68]) ).
cnf(t457,plain,
multiply(y,add(sFlat0,x)) = add(z,z),
inference(orient,[status(thm)],[t1252]) ).
cnf(t278,plain,
multiply(add(sFlat0,X1),z) = add(z,multiply(X1,z)),
inference(cp,[status(thm)],[t30,t273]) ).
cnf(t1256,plain,
multiply(z,add(sFlat0,X1)) = add(z,multiply(X1,z)),
inference(step,[status(thm)],[t278,t20]) ).
cnf(t3,axiom,
multiply(multiplicative_identity,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t17,plain,
multiply(multiplicative_identity,X1) = X1,
inference(orient,[status(thm)],[t3]) ).
cnf(t33,plain,
multiply(add(multiplicative_identity,X1),X2) = add(X2,multiply(X1,X2)),
inference(cp,[status(thm)],[t30,t17]) ).
cnf(t128,plain,
add(X1,multiply(X2,X1)) = multiply(add(multiplicative_identity,X2),X1),
inference(orient,[status(thm)],[t33]) ).
cnf(t1257,plain,
multiply(z,add(sFlat0,X1)) = multiply(add(multiplicative_identity,X1),z),
inference(step,[status(thm)],[t1256,t128]) ).
cnf(t1258,plain,
multiply(z,add(sFlat0,X1)) = multiply(z,add(multiplicative_identity,X1)),
inference(step,[status(thm)],[t1257,t20]) ).
cnf(t489,plain,
multiply(z,add(multiplicative_identity,X1)) = multiply(z,add(sFlat0,X1)),
inference(orient,[status(thm)],[t1258]) ).
cnf(t2,axiom,
multiply(X1,multiplicative_identity) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t16,plain,
multiply(X1,multiplicative_identity) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t22,plain,
multiply(X1,add(multiplicative_identity,X2)) = add(X1,multiply(X1,X2)),
inference(cp,[status(thm)],[t21,t16]) ).
cnf(t88,plain,
add(X1,multiply(X1,X2)) = multiply(X1,add(multiplicative_identity,X2)),
inference(orient,[status(thm)],[t22]) ).
cnf(t7,axiom,
multiply(X1,inverse(X1)) = additive_identity,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t26,plain,
multiply(X1,inverse(X1)) = additive_identity,
inference(orient,[status(thm)],[t7]) ).
cnf(t92,plain,
multiply(X1,add(multiplicative_identity,inverse(X1))) = add(X1,additive_identity),
inference(cp,[status(thm)],[t88,t26]) ).
cnf(t1203,plain,
multiply(X1,add(multiplicative_identity,inverse(X1))) = X1,
inference(step,[status(thm)],[t92,t18]) ).
cnf(t121,plain,
multiply(X1,add(multiplicative_identity,inverse(X1))) = X1,
inference(orient,[status(thm)],[t1203]) ).
cnf(t132,plain,
multiply(add(multiplicative_identity,X1),add(multiplicative_identity,inverse(X1))) = add(add(multiplicative_identity,inverse(X1)),X1),
inference(cp,[status(thm)],[t128,t121]) ).
cnf(t1208,plain,
add(multiplicative_identity,multiply(X1,inverse(X1))) = add(add(multiplicative_identity,inverse(X1)),X1),
inference(step,[status(thm)],[t132,t50]) ).
cnf(t1209,plain,
add(multiplicative_identity,additive_identity) = add(add(multiplicative_identity,inverse(X1)),X1),
inference(step,[status(thm)],[t1208,t26]) ).
cnf(t1210,plain,
multiplicative_identity = add(add(multiplicative_identity,inverse(X1)),X1),
inference(step,[status(thm)],[t1209,t18]) ).
cnf(t1211,plain,
multiplicative_identity = add(X1,add(multiplicative_identity,inverse(X1))),
inference(step,[status(thm)],[t1210,t68]) ).
cnf(t153,plain,
add(X1,add(multiplicative_identity,inverse(X1))) = multiplicative_identity,
inference(orient,[status(thm)],[t1211]) ).
cnf(t1,axiom,
add(additive_identity,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t19,plain,
add(additive_identity,X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t154,plain,
multiplicative_identity = add(multiplicative_identity,inverse(additive_identity)),
inference(cp,[status(thm)],[t153,t19]) ).
cnf(t5,axiom,
add(X1,inverse(X1)) = multiplicative_identity,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t75,plain,
add(X1,inverse(X1)) = multiplicative_identity,
inference(orient,[status(thm)],[t5]) ).
cnf(t76,plain,
multiplicative_identity = inverse(additive_identity),
inference(cp,[status(thm)],[t75,t19]) ).
cnf(t87,plain,
inverse(additive_identity) = multiplicative_identity,
inference(orient,[status(thm)],[t76]) ).
cnf(t1212,plain,
multiplicative_identity = add(multiplicative_identity,multiplicative_identity),
inference(step,[status(thm)],[t154,t87]) ).
cnf(t162,plain,
add(multiplicative_identity,multiplicative_identity) = multiplicative_identity,
inference(orient,[status(thm)],[t1212]) ).
cnf(t491,plain,
multiply(z,add(sFlat0,multiplicative_identity)) = multiply(z,multiplicative_identity),
inference(cp,[status(thm)],[t489,t162]) ).
cnf(t276,plain,
multiply(add(multiplicative_identity,sFlat0),z) = add(z,z),
inference(cp,[status(thm)],[t128,t273]) ).
cnf(t1229,plain,
multiply(z,add(multiplicative_identity,sFlat0)) = add(z,z),
inference(step,[status(thm)],[t276,t20]) ).
cnf(t1230,plain,
multiply(z,add(sFlat0,multiplicative_identity)) = add(z,z),
inference(step,[status(thm)],[t1229,t68]) ).
cnf(t287,plain,
multiply(z,add(sFlat0,multiplicative_identity)) = add(z,z),
inference(orient,[status(thm)],[t1230]) ).
cnf(t1259,plain,
add(z,z) = multiply(z,multiplicative_identity),
inference(step,[status(thm)],[t491,t287]) ).
cnf(t1260,plain,
add(z,z) = z,
inference(step,[status(thm)],[t1259,t16]) ).
cnf(t505,plain,
add(z,z) = z,
inference(orient,[status(thm)],[t1260]) ).
cnf(t1269,plain,
multiply(y,add(sFlat0,x)) = z,
inference(step,[status(thm)],[t457,t505]) ).
cnf(t514,plain,
multiply(y,add(sFlat0,x)) = z,
inference(orient,[status(thm)],[t1269]) ).
cnf(t14,axiom,
multiply(add(X1,X2),add(X3,X2)) = add(multiply(X1,X3),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t38,plain,
multiply(add(X1,X2),add(X3,X2)) = add(multiply(X1,X3),X2),
inference(orient,[status(thm)],[t14]) ).
cnf(t84,plain,
add(multiply(z,X1),x) = multiply(sFlat0,add(X1,x)),
inference(cp,[status(thm)],[t38,t81]) ).
cnf(t1234,plain,
add(x,multiply(z,X1)) = multiply(sFlat0,add(X1,x)),
inference(step,[status(thm)],[t84,t68]) ).
cnf(t306,plain,
add(x,multiply(z,X1)) = multiply(sFlat0,add(X1,x)),
inference(orient,[status(thm)],[t1234]) ).
cnf(t28,plain,
multiply(X1,add(inverse(X1),X2)) = add(additive_identity,multiply(X1,X2)),
inference(cp,[status(thm)],[t21,t26]) ).
cnf(t1323,plain,
multiply(X1,add(inverse(X1),X2)) = multiply(X1,X2),
inference(step,[status(thm)],[t28,t19]) ).
cnf(t807,plain,
multiply(X1,add(inverse(X1),X2)) = multiply(X1,X2),
inference(orient,[status(thm)],[t1323]) ).
cnf(t815,plain,
multiply(X1,additive_identity) = multiply(X1,inverse(X1)),
inference(cp,[status(thm)],[t807,t18]) ).
cnf(t1324,plain,
multiply(X1,additive_identity) = additive_identity,
inference(step,[status(thm)],[t815,t26]) ).
cnf(t831,plain,
multiply(X1,additive_identity) = additive_identity,
inference(orient,[status(thm)],[t1324]) ).
cnf(t836,plain,
multiply(sFlat0,add(additive_identity,x)) = add(x,additive_identity),
inference(cp,[status(thm)],[t306,t831]) ).
cnf(t1325,plain,
multiply(sFlat0,x) = add(x,additive_identity),
inference(step,[status(thm)],[t836,t19]) ).
cnf(t1326,plain,
multiply(sFlat0,x) = x,
inference(step,[status(thm)],[t1325,t18]) ).
cnf(t839,plain,
multiply(sFlat0,x) = x,
inference(orient,[status(thm)],[t1326]) ).
cnf(t846,plain,
multiply(sFlat0,add(multiplicative_identity,x)) = add(sFlat0,x),
inference(cp,[status(thm)],[t88,t839]) ).
cnf(t277,plain,
multiply(sFlat0,add(multiplicative_identity,z)) = add(sFlat0,z),
inference(cp,[status(thm)],[t88,t273]) ).
cnf(t1231,plain,
multiply(sFlat0,add(z,multiplicative_identity)) = add(sFlat0,z),
inference(step,[status(thm)],[t277,t68]) ).
cnf(t82,plain,
add(z,multiply(x,X1)) = multiply(sFlat0,add(z,X1)),
inference(cp,[status(thm)],[t50,t81]) ).
cnf(t221,plain,
add(z,multiply(x,X1)) = multiply(sFlat0,add(z,X1)),
inference(orient,[status(thm)],[t82]) ).
cnf(t227,plain,
multiply(sFlat0,add(z,multiplicative_identity)) = add(z,x),
inference(cp,[status(thm)],[t221,t16]) ).
cnf(t1218,plain,
multiply(sFlat0,add(z,multiplicative_identity)) = sFlat0,
inference(step,[status(thm)],[t227,t81]) ).
cnf(t234,plain,
multiply(sFlat0,add(z,multiplicative_identity)) = sFlat0,
inference(orient,[status(thm)],[t1218]) ).
cnf(t1232,plain,
sFlat0 = add(sFlat0,z),
inference(step,[status(thm)],[t1231,t234]) ).
cnf(t294,plain,
add(sFlat0,z) = sFlat0,
inference(orient,[status(thm)],[t1232]) ).
cnf(t296,plain,
add(sFlat0,multiply(X1,z)) = multiply(add(sFlat0,X1),sFlat0),
inference(cp,[status(thm)],[t50,t294]) ).
cnf(t1273,plain,
add(sFlat0,multiply(X1,z)) = multiply(sFlat0,add(sFlat0,X1)),
inference(step,[status(thm)],[t296,t20]) ).
cnf(t565,plain,
add(sFlat0,multiply(X1,z)) = multiply(sFlat0,add(sFlat0,X1)),
inference(orient,[status(thm)],[t1273]) ).
cnf(t516,plain,
add(z,multiply(z,X1)) = multiply(z,add(z,X1)),
inference(cp,[status(thm)],[t50,t505]) ).
cnf(t1291,plain,
multiply(z,add(multiplicative_identity,X1)) = multiply(z,add(z,X1)),
inference(step,[status(thm)],[t516,t88]) ).
cnf(t1292,plain,
multiply(z,add(sFlat0,X1)) = multiply(z,add(z,X1)),
inference(step,[status(thm)],[t1291,t489]) ).
cnf(t662,plain,
multiply(z,add(z,X1)) = multiply(z,add(sFlat0,X1)),
inference(orient,[status(thm)],[t1292]) ).
cnf(t664,plain,
multiply(z,add(sFlat0,z)) = multiply(z,z),
inference(cp,[status(thm)],[t662,t505]) ).
cnf(t1293,plain,
multiply(z,sFlat0) = multiply(z,z),
inference(step,[status(thm)],[t664,t294]) ).
cnf(t1294,plain,
multiply(sFlat0,z) = multiply(z,z),
inference(step,[status(thm)],[t1293,t20]) ).
cnf(t1295,plain,
z = multiply(z,z),
inference(step,[status(thm)],[t1294,t273]) ).
cnf(t686,plain,
multiply(z,z) = z,
inference(orient,[status(thm)],[t1295]) ).
cnf(t688,plain,
multiply(sFlat0,add(sFlat0,z)) = add(sFlat0,z),
inference(cp,[status(thm)],[t565,t686]) ).
cnf(t1296,plain,
multiply(sFlat0,sFlat0) = add(sFlat0,z),
inference(step,[status(thm)],[t688,t294]) ).
cnf(t1297,plain,
multiply(sFlat0,sFlat0) = sFlat0,
inference(step,[status(thm)],[t1296,t294]) ).
cnf(t697,plain,
multiply(sFlat0,sFlat0) = sFlat0,
inference(orient,[status(thm)],[t1297]) ).
cnf(t698,plain,
multiply(sFlat0,add(sFlat0,X1)) = add(sFlat0,multiply(sFlat0,X1)),
inference(cp,[status(thm)],[t21,t697]) ).
cnf(t1314,plain,
multiply(sFlat0,add(sFlat0,X1)) = multiply(sFlat0,add(multiplicative_identity,X1)),
inference(step,[status(thm)],[t698,t88]) ).
cnf(t766,plain,
multiply(sFlat0,add(multiplicative_identity,X1)) = multiply(sFlat0,add(sFlat0,X1)),
inference(orient,[status(thm)],[t1314]) ).
cnf(t1327,plain,
multiply(sFlat0,add(sFlat0,x)) = add(sFlat0,x),
inference(step,[status(thm)],[t846,t766]) ).
cnf(t85,plain,
add(multiply(X1,z),x) = multiply(add(X1,x),sFlat0),
inference(cp,[status(thm)],[t38,t81]) ).
cnf(t1240,plain,
add(x,multiply(X1,z)) = multiply(add(X1,x),sFlat0),
inference(step,[status(thm)],[t85,t68]) ).
cnf(t1241,plain,
add(x,multiply(X1,z)) = multiply(sFlat0,add(X1,x)),
inference(step,[status(thm)],[t1240,t20]) ).
cnf(t331,plain,
add(x,multiply(X1,z)) = multiply(sFlat0,add(X1,x)),
inference(orient,[status(thm)],[t1241]) ).
cnf(t333,plain,
multiply(sFlat0,add(sFlat0,x)) = add(x,z),
inference(cp,[status(thm)],[t331,t273]) ).
cnf(t1242,plain,
multiply(sFlat0,add(sFlat0,x)) = add(z,x),
inference(step,[status(thm)],[t333,t68]) ).
cnf(t1243,plain,
multiply(sFlat0,add(sFlat0,x)) = sFlat0,
inference(step,[status(thm)],[t1242,t81]) ).
cnf(t339,plain,
multiply(sFlat0,add(sFlat0,x)) = sFlat0,
inference(orient,[status(thm)],[t1243]) ).
cnf(t1328,plain,
sFlat0 = add(sFlat0,x),
inference(step,[status(thm)],[t1327,t339]) ).
cnf(t849,plain,
add(sFlat0,x) = sFlat0,
inference(orient,[status(thm)],[t1328]) ).
cnf(t1330,plain,
multiply(y,sFlat0) = z,
inference(step,[status(thm)],[t514,t849]) ).
cnf(t855,plain,
multiply(y,sFlat0) = z,
inference(rw,[status(thm)],[t1330]) ).
cnf(t1331,plain,
multiply(sFlat0,y) = z,
inference(step,[status(thm)],[t855,t20]) ).
cnf(t856,plain,
multiply(sFlat0,y) = z,
inference(orient,[status(thm)],[t1331]) ).
cnf(t859,plain,
multiply(sFlat0,add(y,X1)) = add(z,multiply(sFlat0,X1)),
inference(cp,[status(thm)],[t21,t856]) ).
cnf(t1363,plain,
multiply(sFlat0,add(y,X1)) = multiply(sFlat0,add(z,X1)),
inference(step,[status(thm)],[t859,t437]) ).
cnf(t1164,plain,
multiply(sFlat0,add(y,X1)) = multiply(sFlat0,add(z,X1)),
inference(orient,[status(thm)],[t1363]) ).
cnf(t1168,plain,
multiply(sFlat0,add(z,inverse(y))) = multiply(sFlat0,multiplicative_identity),
inference(cp,[status(thm)],[t1164,t75]) ).
cnf(t263,plain,
multiply(sFlat0,add(z,inverse(y))) = multiply(x,multiplicative_identity),
inference(cp,[status(thm)],[t256,t75]) ).
cnf(t1233,plain,
multiply(sFlat0,add(z,inverse(y))) = x,
inference(step,[status(thm)],[t263,t16]) ).
cnf(t299,plain,
multiply(sFlat0,add(z,inverse(y))) = x,
inference(orient,[status(thm)],[t1233]) ).
cnf(t1364,plain,
x = multiply(sFlat0,multiplicative_identity),
inference(step,[status(thm)],[t1168,t299]) ).
cnf(t1365,plain,
x = sFlat0,
inference(step,[status(thm)],[t1364,t16]) ).
cnf(t1182,plain,
x = sFlat0,
inference(orient,[status(thm)],[t1365]) ).
cnf(goal_0,negated_conjecture,
add(x,z) != x,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
add(z,x) != x,
inference(rw,[status(thm)],[goal_0,t68]) ).
cnf(g0_1,plain,
add(z,sFlat0) != x,
inference(rw,[status(thm)],[g0_0,t1182]) ).
cnf(g0_2,plain,
add(sFlat0,z) != x,
inference(rw,[status(thm)],[g0_1,t68]) ).
cnf(g0_3,plain,
sFlat0 != x,
inference(rw,[status(thm)],[g0_2,t294]) ).
cnf(g0_4,plain,
sFlat0 != sFlat0,
inference(rw,[status(thm)],[g0_3,t1182]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_4]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : BOO016-2 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.08/0.35 % Computer : n005.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Fri Sep 25 06:33:18 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 5.09/1.46 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.09/1.46 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------