%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : BOO028-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 : n015.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 9.86s 1.92s
% Output : CNFRefutation 9.86s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 14
% Syntax : Number of clauses : 206 ( 206 unt; 0 nHn; 136 RR)
% Number of literals : 206 ( 205 equ; 10 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 8 con; 0-2 aty)
% Number of variables : 108 ( 35 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t0,axiom,
add(X1,X2) = add(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t91,plain,
add(X1,X2) = add(X2,X1),
inference(orient,[status(thm)],[t0]) ).
cnf(t11,axiom,
sFlat1 = multiply(c,a),
introduced(definition) ).
cnf(t85,plain,
multiply(c,a) = sFlat1,
inference(orient,[status(thm)],[t11]) ).
cnf(t10,axiom,
sFlat0 = multiply(b,a),
introduced(definition) ).
cnf(t79,plain,
multiply(b,a) = sFlat0,
inference(orient,[status(thm)],[t10]) ).
cnf(t12,axiom,
sFlat2 = add(multiply(b,a),multiply(c,a)),
introduced(definition) ).
cnf(t4266,plain,
sFlat2 = add(multiply(c,a),multiply(b,a)),
inference(step,[status(thm)],[t12,t91]) ).
cnf(t4267,plain,
sFlat2 = add(sFlat1,multiply(b,a)),
inference(step,[status(thm)],[t4266,t85]) ).
cnf(t4268,plain,
sFlat2 = add(sFlat1,sFlat0),
inference(step,[status(thm)],[t4267,t79]) ).
cnf(t4269,plain,
sFlat2 = add(sFlat0,sFlat1),
inference(step,[status(thm)],[t4268,t91]) ).
cnf(t108,plain,
add(sFlat0,sFlat1) = sFlat2,
inference(orient,[status(thm)],[t4269]) ).
cnf(t13,axiom,
sFlat3 = add(b,c),
introduced(definition) ).
cnf(t4270,plain,
sFlat3 = add(c,b),
inference(step,[status(thm)],[t13,t91]) ).
cnf(t112,plain,
add(c,b) = sFlat3,
inference(orient,[status(thm)],[t4270]) ).
cnf(t1,axiom,
multiply(X1,X2) = multiply(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t53,plain,
multiply(X1,X2) = multiply(X2,X1),
inference(orient,[status(thm)],[t1]) ).
cnf(t14,axiom,
sFlat4 = multiply(a,add(b,c)),
introduced(definition) ).
cnf(t73,plain,
multiply(a,add(b,c)) = sFlat4,
inference(orient,[status(thm)],[t14]) ).
cnf(t96,plain,
multiply(a,add(b,c)) = sFlat4,
inference(rw,[status(thm)],[t73]) ).
cnf(t4275,plain,
multiply(a,add(c,b)) = sFlat4,
inference(step,[status(thm)],[t96,t91]) ).
cnf(t4276,plain,
multiply(a,sFlat3) = sFlat4,
inference(step,[status(thm)],[t4275,t112]) ).
cnf(t4277,plain,
multiply(sFlat3,a) = sFlat4,
inference(step,[status(thm)],[t4276,t53]) ).
cnf(t196,plain,
multiply(sFlat3,a) = sFlat4,
inference(orient,[status(thm)],[t4277]) ).
cnf(t4,axiom,
add(multiply(X1,X2),multiply(X1,inverse(X2))) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t29,plain,
add(multiply(X1,X2),multiply(X1,inverse(X2))) = X1,
inference(orient,[status(thm)],[t4]) ).
cnf(t8,axiom,
multiply(multiply(X1,X2),X3) = multiply(X1,multiply(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t61,plain,
multiply(multiply(X1,X2),X3) = multiply(X1,multiply(X2,X3)),
inference(orient,[status(thm)],[t8]) ).
cnf(t80,plain,
multiply(b,multiply(a,X1)) = multiply(sFlat0,X1),
inference(cp,[status(thm)],[t61,t79]) ).
cnf(t537,plain,
multiply(b,multiply(a,X1)) = multiply(sFlat0,X1),
inference(orient,[status(thm)],[t80]) ).
cnf(t539,plain,
multiply(sFlat0,X1) = multiply(b,multiply(X1,a)),
inference(cp,[status(thm)],[t537,t53]) ).
cnf(t1462,plain,
multiply(b,multiply(X1,a)) = multiply(sFlat0,X1),
inference(orient,[status(thm)],[t539]) ).
cnf(t3,axiom,
multiply(X1,add(X2,add(X1,X3))) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t15,plain,
multiply(X1,add(X2,add(X1,X3))) = X1,
inference(orient,[status(thm)],[t3]) ).
cnf(t2,axiom,
add(X1,multiply(X2,multiply(X1,X3))) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t20,plain,
add(X1,multiply(X2,multiply(X1,X3))) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t25,plain,
X1 = multiply(X1,add(X2,X1)),
inference(cp,[status(thm)],[t15,t20]) ).
cnf(t135,plain,
multiply(X1,add(X2,X1)) = X1,
inference(orient,[status(thm)],[t25]) ).
cnf(t145,plain,
X1 = multiply(X1,add(X1,X2)),
inference(cp,[status(thm)],[t135,t91]) ).
cnf(t311,plain,
multiply(X1,add(X1,X2)) = X1,
inference(orient,[status(thm)],[t145]) ).
cnf(t22,plain,
X1 = add(X1,multiply(X2,X1)),
inference(cp,[status(thm)],[t20,t15]) ).
cnf(t116,plain,
add(X1,multiply(X2,X1)) = X1,
inference(orient,[status(thm)],[t22]) ).
cnf(t198,plain,
a = add(a,sFlat4),
inference(cp,[status(thm)],[t116,t196]) ).
cnf(t4278,plain,
a = add(sFlat4,a),
inference(step,[status(thm)],[t198,t91]) ).
cnf(t201,plain,
add(sFlat4,a) = a,
inference(orient,[status(thm)],[t4278]) ).
cnf(t313,plain,
sFlat4 = multiply(sFlat4,a),
inference(cp,[status(thm)],[t311,t201]) ).
cnf(t350,plain,
multiply(sFlat4,a) = sFlat4,
inference(orient,[status(thm)],[t313]) ).
cnf(t1464,plain,
multiply(sFlat0,sFlat4) = multiply(b,sFlat4),
inference(cp,[status(thm)],[t1462,t350]) ).
cnf(t140,plain,
b = multiply(b,sFlat3),
inference(cp,[status(thm)],[t135,t112]) ).
cnf(t4273,plain,
b = multiply(sFlat3,b),
inference(step,[status(thm)],[t140,t53]) ).
cnf(t153,plain,
multiply(sFlat3,b) = b,
inference(orient,[status(thm)],[t4273]) ).
cnf(t157,plain,
sFlat3 = add(sFlat3,multiply(X1,b)),
inference(cp,[status(thm)],[t20,t153]) ).
cnf(t362,plain,
add(sFlat3,multiply(X1,b)) = sFlat3,
inference(orient,[status(thm)],[t157]) ).
cnf(t123,plain,
X1 = add(X1,multiply(X1,X2)),
inference(cp,[status(thm)],[t116,t53]) ).
cnf(t226,plain,
add(X1,multiply(X1,X2)) = X1,
inference(orient,[status(thm)],[t123]) ).
cnf(t237,plain,
b = add(b,sFlat0),
inference(cp,[status(thm)],[t226,t79]) ).
cnf(t4281,plain,
b = add(sFlat0,b),
inference(step,[status(thm)],[t237,t91]) ).
cnf(t264,plain,
add(sFlat0,b) = b,
inference(orient,[status(thm)],[t4281]) ).
cnf(t316,plain,
sFlat0 = multiply(sFlat0,b),
inference(cp,[status(thm)],[t311,t264]) ).
cnf(t358,plain,
multiply(sFlat0,b) = sFlat0,
inference(orient,[status(thm)],[t316]) ).
cnf(t363,plain,
sFlat3 = add(sFlat3,sFlat0),
inference(cp,[status(thm)],[t362,t358]) ).
cnf(t4285,plain,
sFlat3 = add(sFlat0,sFlat3),
inference(step,[status(thm)],[t363,t91]) ).
cnf(t368,plain,
add(sFlat0,sFlat3) = sFlat3,
inference(orient,[status(thm)],[t4285]) ).
cnf(t369,plain,
sFlat0 = multiply(sFlat0,sFlat3),
inference(cp,[status(thm)],[t311,t368]) ).
cnf(t374,plain,
multiply(sFlat0,sFlat3) = sFlat0,
inference(orient,[status(thm)],[t369]) ).
cnf(t375,plain,
multiply(sFlat0,multiply(sFlat3,X1)) = multiply(sFlat0,X1),
inference(cp,[status(thm)],[t61,t374]) ).
cnf(t1194,plain,
multiply(sFlat0,multiply(sFlat3,X1)) = multiply(sFlat0,X1),
inference(orient,[status(thm)],[t375]) ).
cnf(t1196,plain,
multiply(sFlat0,a) = multiply(sFlat0,sFlat4),
inference(cp,[status(thm)],[t1194,t196]) ).
cnf(t120,plain,
a = add(a,sFlat0),
inference(cp,[status(thm)],[t116,t79]) ).
cnf(t4272,plain,
a = add(sFlat0,a),
inference(step,[status(thm)],[t120,t91]) ).
cnf(t131,plain,
add(sFlat0,a) = a,
inference(orient,[status(thm)],[t4272]) ).
cnf(t133,plain,
sFlat0 = multiply(sFlat0,add(X1,a)),
inference(cp,[status(thm)],[t15,t131]) ).
cnf(t299,plain,
multiply(sFlat0,add(X1,a)) = sFlat0,
inference(orient,[status(thm)],[t133]) ).
cnf(t228,plain,
X1 = add(X1,X1),
inference(cp,[status(thm)],[t226,t15]) ).
cnf(t243,plain,
add(X1,X1) = X1,
inference(orient,[status(thm)],[t228]) ).
cnf(t300,plain,
sFlat0 = multiply(sFlat0,a),
inference(cp,[status(thm)],[t299,t243]) ).
cnf(t308,plain,
multiply(sFlat0,a) = sFlat0,
inference(orient,[status(thm)],[t300]) ).
cnf(t4294,plain,
sFlat0 = multiply(sFlat0,sFlat4),
inference(step,[status(thm)],[t1196,t308]) ).
cnf(t1203,plain,
multiply(sFlat0,sFlat4) = sFlat0,
inference(orient,[status(thm)],[t4294]) ).
cnf(t4308,plain,
sFlat0 = multiply(b,sFlat4),
inference(step,[status(thm)],[t1464,t1203]) ).
cnf(t4309,plain,
sFlat0 = multiply(sFlat4,b),
inference(step,[status(thm)],[t4308,t53]) ).
cnf(t1489,plain,
multiply(sFlat4,b) = sFlat0,
inference(orient,[status(thm)],[t4309]) ).
cnf(t1499,plain,
sFlat4 = add(sFlat0,multiply(sFlat4,inverse(b))),
inference(cp,[status(thm)],[t29,t1489]) ).
cnf(t86,plain,
multiply(c,multiply(a,X1)) = multiply(sFlat1,X1),
inference(cp,[status(thm)],[t61,t85]) ).
cnf(t596,plain,
multiply(c,multiply(a,X1)) = multiply(sFlat1,X1),
inference(orient,[status(thm)],[t86]) ).
cnf(t598,plain,
multiply(sFlat1,X1) = multiply(c,multiply(X1,a)),
inference(cp,[status(thm)],[t596,t53]) ).
cnf(t1556,plain,
multiply(c,multiply(X1,a)) = multiply(sFlat1,X1),
inference(orient,[status(thm)],[t598]) ).
cnf(t1558,plain,
multiply(sFlat1,sFlat4) = multiply(c,sFlat4),
inference(cp,[status(thm)],[t1556,t350]) ).
cnf(t235,plain,
c = add(c,sFlat1),
inference(cp,[status(thm)],[t226,t85]) ).
cnf(t4280,plain,
c = add(sFlat1,c),
inference(step,[status(thm)],[t235,t91]) ).
cnf(t259,plain,
add(sFlat1,c) = c,
inference(orient,[status(thm)],[t4280]) ).
cnf(t262,plain,
sFlat1 = multiply(sFlat1,add(X1,c)),
inference(cp,[status(thm)],[t15,t259]) ).
cnf(t438,plain,
multiply(sFlat1,add(X1,c)) = sFlat1,
inference(orient,[status(thm)],[t262]) ).
cnf(t114,plain,
c = multiply(c,add(X1,sFlat3)),
inference(cp,[status(thm)],[t15,t112]) ).
cnf(t220,plain,
multiply(c,add(X1,sFlat3)) = c,
inference(orient,[status(thm)],[t114]) ).
cnf(t245,plain,
c = multiply(c,sFlat3),
inference(cp,[status(thm)],[t220,t243]) ).
cnf(t4282,plain,
c = multiply(sFlat3,c),
inference(step,[status(thm)],[t245,t53]) ).
cnf(t268,plain,
multiply(sFlat3,c) = c,
inference(orient,[status(thm)],[t4282]) ).
cnf(t270,plain,
sFlat3 = add(sFlat3,c),
inference(cp,[status(thm)],[t226,t268]) ).
cnf(t283,plain,
add(sFlat3,c) = sFlat3,
inference(orient,[status(thm)],[t270]) ).
cnf(t439,plain,
sFlat1 = multiply(sFlat1,sFlat3),
inference(cp,[status(thm)],[t438,t283]) ).
cnf(t446,plain,
multiply(sFlat1,sFlat3) = sFlat1,
inference(orient,[status(thm)],[t439]) ).
cnf(t447,plain,
multiply(sFlat1,multiply(sFlat3,X1)) = multiply(sFlat1,X1),
inference(cp,[status(thm)],[t61,t446]) ).
cnf(t1344,plain,
multiply(sFlat1,multiply(sFlat3,X1)) = multiply(sFlat1,X1),
inference(orient,[status(thm)],[t447]) ).
cnf(t1346,plain,
multiply(sFlat1,a) = multiply(sFlat1,sFlat4),
inference(cp,[status(thm)],[t1344,t196]) ).
cnf(t119,plain,
a = add(a,sFlat1),
inference(cp,[status(thm)],[t116,t85]) ).
cnf(t4271,plain,
a = add(sFlat1,a),
inference(step,[status(thm)],[t119,t91]) ).
cnf(t127,plain,
add(sFlat1,a) = a,
inference(orient,[status(thm)],[t4271]) ).
cnf(t129,plain,
sFlat1 = multiply(sFlat1,add(X1,a)),
inference(cp,[status(thm)],[t15,t127]) ).
cnf(t287,plain,
multiply(sFlat1,add(X1,a)) = sFlat1,
inference(orient,[status(thm)],[t129]) ).
cnf(t288,plain,
sFlat1 = multiply(sFlat1,a),
inference(cp,[status(thm)],[t287,t243]) ).
cnf(t296,plain,
multiply(sFlat1,a) = sFlat1,
inference(orient,[status(thm)],[t288]) ).
cnf(t4300,plain,
sFlat1 = multiply(sFlat1,sFlat4),
inference(step,[status(thm)],[t1346,t296]) ).
cnf(t1354,plain,
multiply(sFlat1,sFlat4) = sFlat1,
inference(orient,[status(thm)],[t4300]) ).
cnf(t4317,plain,
sFlat1 = multiply(c,sFlat4),
inference(step,[status(thm)],[t1558,t1354]) ).
cnf(t4318,plain,
sFlat1 = multiply(sFlat4,c),
inference(step,[status(thm)],[t4317,t53]) ).
cnf(t1582,plain,
multiply(sFlat4,c) = sFlat1,
inference(orient,[status(thm)],[t4318]) ).
cnf(t1583,plain,
multiply(sFlat4,multiply(c,X1)) = multiply(sFlat1,X1),
inference(cp,[status(thm)],[t61,t1582]) ).
cnf(t2844,plain,
multiply(sFlat4,multiply(c,X1)) = multiply(sFlat1,X1),
inference(orient,[status(thm)],[t1583]) ).
cnf(t34,plain,
multiply(X1,X2) = multiply(multiply(X1,X2),add(X3,X1)),
inference(cp,[status(thm)],[t15,t29]) ).
cnf(t4296,plain,
multiply(X1,X2) = multiply(X1,multiply(X2,add(X3,X1))),
inference(step,[status(thm)],[t34,t61]) ).
cnf(t1230,plain,
multiply(X1,multiply(X2,add(X3,X1))) = multiply(X1,X2),
inference(orient,[status(thm)],[t4296]) ).
cnf(t5,axiom,
multiply(add(X1,X2),add(X1,inverse(X2))) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t18,plain,
multiply(add(X1,X2),add(X1,inverse(X2))) = X1,
inference(orient,[status(thm)],[t5]) ).
cnf(t115,plain,
c = multiply(sFlat3,add(c,inverse(b))),
inference(cp,[status(thm)],[t18,t112]) ).
cnf(t3580,plain,
multiply(sFlat3,add(c,inverse(b))) = c,
inference(orient,[status(thm)],[t115]) ).
cnf(t3588,plain,
multiply(inverse(b),sFlat3) = multiply(inverse(b),c),
inference(cp,[status(thm)],[t1230,t3580]) ).
cnf(t4361,plain,
multiply(sFlat3,inverse(b)) = multiply(inverse(b),c),
inference(step,[status(thm)],[t3588,t53]) ).
cnf(t4362,plain,
multiply(sFlat3,inverse(b)) = multiply(c,inverse(b)),
inference(step,[status(thm)],[t4361,t53]) ).
cnf(t3592,plain,
multiply(c,inverse(b)) = multiply(sFlat3,inverse(b)),
inference(orient,[status(thm)],[t4362]) ).
cnf(t3594,plain,
multiply(sFlat1,inverse(b)) = multiply(sFlat4,multiply(sFlat3,inverse(b))),
inference(cp,[status(thm)],[t2844,t3592]) ).
cnf(t200,plain,
sFlat3 = add(sFlat3,multiply(X1,sFlat4)),
inference(cp,[status(thm)],[t20,t196]) ).
cnf(t409,plain,
add(sFlat3,multiply(X1,sFlat4)) = sFlat3,
inference(orient,[status(thm)],[t200]) ).
cnf(t411,plain,
sFlat3 = add(sFlat3,multiply(sFlat4,X1)),
inference(cp,[status(thm)],[t409,t53]) ).
cnf(t497,plain,
add(sFlat3,multiply(sFlat4,X1)) = sFlat3,
inference(orient,[status(thm)],[t411]) ).
cnf(t499,plain,
multiply(sFlat4,X1) = multiply(multiply(sFlat4,X1),sFlat3),
inference(cp,[status(thm)],[t135,t497]) ).
cnf(t4304,plain,
multiply(sFlat4,X1) = multiply(sFlat4,multiply(X1,sFlat3)),
inference(step,[status(thm)],[t499,t61]) ).
cnf(t1444,plain,
multiply(sFlat4,multiply(X1,sFlat3)) = multiply(sFlat4,X1),
inference(orient,[status(thm)],[t4304]) ).
cnf(t1448,plain,
multiply(sFlat4,X1) = multiply(sFlat4,multiply(sFlat3,X1)),
inference(cp,[status(thm)],[t1444,t53]) ).
cnf(t2626,plain,
multiply(sFlat4,multiply(sFlat3,X1)) = multiply(sFlat4,X1),
inference(orient,[status(thm)],[t1448]) ).
cnf(t4363,plain,
multiply(sFlat1,inverse(b)) = multiply(sFlat4,inverse(b)),
inference(step,[status(thm)],[t3594,t2626]) ).
cnf(t3605,plain,
multiply(sFlat4,inverse(b)) = multiply(sFlat1,inverse(b)),
inference(orient,[status(thm)],[t4363]) ).
cnf(t4415,plain,
sFlat4 = add(sFlat0,multiply(sFlat1,inverse(b))),
inference(step,[status(thm)],[t1499,t3605]) ).
cnf(t6,axiom,
add(add(X1,X2),X3) = add(X1,add(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t98,plain,
add(add(X1,X2),X3) = add(X1,add(X2,X3)),
inference(orient,[status(thm)],[t6]) ).
cnf(t109,plain,
add(sFlat0,add(sFlat1,X1)) = add(sFlat2,X1),
inference(cp,[status(thm)],[t98,t108]) ).
cnf(t655,plain,
add(sFlat0,add(sFlat1,X1)) = add(sFlat2,X1),
inference(orient,[status(thm)],[t109]) ).
cnf(t659,plain,
add(sFlat2,a) = add(sFlat0,a),
inference(cp,[status(thm)],[t655,t127]) ).
cnf(t4288,plain,
add(sFlat2,a) = a,
inference(step,[status(thm)],[t659,t131]) ).
cnf(t675,plain,
add(sFlat2,a) = a,
inference(orient,[status(thm)],[t4288]) ).
cnf(t676,plain,
sFlat2 = multiply(sFlat2,a),
inference(cp,[status(thm)],[t311,t675]) ).
cnf(t684,plain,
multiply(sFlat2,a) = sFlat2,
inference(orient,[status(thm)],[t676]) ).
cnf(t1463,plain,
multiply(sFlat0,sFlat2) = multiply(b,sFlat2),
inference(cp,[status(thm)],[t1462,t684]) ).
cnf(t110,plain,
sFlat0 = multiply(sFlat0,add(X1,sFlat2)),
inference(cp,[status(thm)],[t15,t108]) ).
cnf(t205,plain,
multiply(sFlat0,add(X1,sFlat2)) = sFlat0,
inference(orient,[status(thm)],[t110]) ).
cnf(t141,plain,
sFlat1 = multiply(sFlat1,sFlat2),
inference(cp,[status(thm)],[t135,t108]) ).
cnf(t158,plain,
multiply(sFlat1,sFlat2) = sFlat1,
inference(orient,[status(thm)],[t141]) ).
cnf(t160,plain,
sFlat2 = add(sFlat2,sFlat1),
inference(cp,[status(thm)],[t116,t158]) ).
cnf(t4274,plain,
sFlat2 = add(sFlat1,sFlat2),
inference(step,[status(thm)],[t160,t91]) ).
cnf(t169,plain,
add(sFlat1,sFlat2) = sFlat2,
inference(orient,[status(thm)],[t4274]) ).
cnf(t170,plain,
sFlat2 = multiply(sFlat2,sFlat2),
inference(cp,[status(thm)],[t135,t169]) ).
cnf(t177,plain,
multiply(sFlat2,sFlat2) = sFlat2,
inference(orient,[status(thm)],[t170]) ).
cnf(t179,plain,
sFlat2 = add(sFlat2,sFlat2),
inference(cp,[status(thm)],[t116,t177]) ).
cnf(t181,plain,
add(sFlat2,sFlat2) = sFlat2,
inference(orient,[status(thm)],[t179]) ).
cnf(t206,plain,
sFlat0 = multiply(sFlat0,sFlat2),
inference(cp,[status(thm)],[t205,t181]) ).
cnf(t213,plain,
multiply(sFlat0,sFlat2) = sFlat0,
inference(orient,[status(thm)],[t206]) ).
cnf(t4306,plain,
sFlat0 = multiply(b,sFlat2),
inference(step,[status(thm)],[t1463,t213]) ).
cnf(t4307,plain,
sFlat0 = multiply(sFlat2,b),
inference(step,[status(thm)],[t4306,t53]) ).
cnf(t1480,plain,
multiply(sFlat2,b) = sFlat0,
inference(orient,[status(thm)],[t4307]) ).
cnf(t1488,plain,
sFlat2 = add(sFlat0,multiply(sFlat2,inverse(b))),
inference(cp,[status(thm)],[t29,t1480]) ).
cnf(t1557,plain,
multiply(sFlat1,sFlat2) = multiply(c,sFlat2),
inference(cp,[status(thm)],[t1556,t684]) ).
cnf(t4315,plain,
sFlat1 = multiply(c,sFlat2),
inference(step,[status(thm)],[t1557,t158]) ).
cnf(t4316,plain,
sFlat1 = multiply(sFlat2,c),
inference(step,[status(thm)],[t4315,t53]) ).
cnf(t1574,plain,
multiply(sFlat2,c) = sFlat1,
inference(orient,[status(thm)],[t4316]) ).
cnf(t1575,plain,
multiply(sFlat2,multiply(c,X1)) = multiply(sFlat1,X1),
inference(cp,[status(thm)],[t61,t1574]) ).
cnf(t2825,plain,
multiply(sFlat2,multiply(c,X1)) = multiply(sFlat1,X1),
inference(orient,[status(thm)],[t1575]) ).
cnf(t3595,plain,
multiply(sFlat1,inverse(b)) = multiply(sFlat2,multiply(sFlat3,inverse(b))),
inference(cp,[status(thm)],[t2825,t3592]) ).
cnf(t449,plain,
sFlat3 = add(sFlat3,sFlat1),
inference(cp,[status(thm)],[t116,t446]) ).
cnf(t4286,plain,
sFlat3 = add(sFlat1,sFlat3),
inference(step,[status(thm)],[t449,t91]) ).
cnf(t451,plain,
add(sFlat1,sFlat3) = sFlat3,
inference(orient,[status(thm)],[t4286]) ).
cnf(t657,plain,
add(sFlat2,sFlat3) = add(sFlat0,sFlat3),
inference(cp,[status(thm)],[t655,t451]) ).
cnf(t4287,plain,
add(sFlat2,sFlat3) = sFlat3,
inference(step,[status(thm)],[t657,t368]) ).
cnf(t669,plain,
add(sFlat2,sFlat3) = sFlat3,
inference(orient,[status(thm)],[t4287]) ).
cnf(t670,plain,
sFlat2 = multiply(sFlat2,sFlat3),
inference(cp,[status(thm)],[t311,t669]) ).
cnf(t680,plain,
multiply(sFlat2,sFlat3) = sFlat2,
inference(orient,[status(thm)],[t670]) ).
cnf(t681,plain,
multiply(sFlat2,multiply(sFlat3,X1)) = multiply(sFlat2,X1),
inference(cp,[status(thm)],[t61,t680]) ).
cnf(t1750,plain,
multiply(sFlat2,multiply(sFlat3,X1)) = multiply(sFlat2,X1),
inference(orient,[status(thm)],[t681]) ).
cnf(t4364,plain,
multiply(sFlat1,inverse(b)) = multiply(sFlat2,inverse(b)),
inference(step,[status(thm)],[t3595,t1750]) ).
cnf(t3618,plain,
multiply(sFlat2,inverse(b)) = multiply(sFlat1,inverse(b)),
inference(orient,[status(thm)],[t4364]) ).
cnf(t4412,plain,
sFlat2 = add(sFlat0,multiply(sFlat1,inverse(b))),
inference(step,[status(thm)],[t1488,t3618]) ).
cnf(t4223,plain,
add(sFlat0,multiply(sFlat1,inverse(b))) = sFlat2,
inference(orient,[status(thm)],[t4412]) ).
cnf(t4416,plain,
sFlat4 = sFlat2,
inference(step,[status(thm)],[t4415,t4223]) ).
cnf(t4245,plain,
sFlat4 = sFlat2,
inference(orient,[status(thm)],[t4416]) ).
cnf(t4417,plain,
multiply(sFlat3,a) = sFlat2,
inference(step,[status(thm)],[t196,t4245]) ).
cnf(t4246,plain,
multiply(sFlat3,a) = sFlat2,
inference(orient,[status(thm)],[t4417]) ).
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,
add(multiply(c,a),multiply(b,a)) != multiply(a,add(b,c)),
inference(rw,[status(thm)],[goal_0,t91]) ).
cnf(g0_1,plain,
add(sFlat1,multiply(b,a)) != multiply(a,add(b,c)),
inference(rw,[status(thm)],[g0_0,t85]) ).
cnf(g0_2,plain,
add(sFlat1,sFlat0) != multiply(a,add(b,c)),
inference(rw,[status(thm)],[g0_1,t79]) ).
cnf(g0_3,plain,
add(sFlat0,sFlat1) != multiply(a,add(b,c)),
inference(rw,[status(thm)],[g0_2,t91]) ).
cnf(g0_4,plain,
sFlat2 != multiply(a,add(b,c)),
inference(rw,[status(thm)],[g0_3,t108]) ).
cnf(g0_5,plain,
sFlat2 != multiply(a,add(c,b)),
inference(rw,[status(thm)],[g0_4,t91]) ).
cnf(g0_6,plain,
sFlat2 != multiply(a,sFlat3),
inference(rw,[status(thm)],[g0_5,t112]) ).
cnf(g0_7,plain,
sFlat2 != multiply(sFlat3,a),
inference(rw,[status(thm)],[g0_6,t53]) ).
cnf(g0_8,plain,
sFlat2 != sFlat2,
inference(rw,[status(thm)],[g0_7,t4246]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_8]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : BOO028-1 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n015.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Fri Sep 25 06:38:57 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 9.86/1.92 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 9.86/1.92 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------