%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : BOO008-2 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n017.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:33 PM UTC 2026
% Result : Unsatisfiable 6.63s 1.36s
% Output : CNFRefutation 6.63s
% Verified :
% SZS Type : Refutation
% Derivation depth : 51
% Number of leaves : 17
% Syntax : Number of clauses : 237 ( 237 unt; 0 nHn; 127 RR)
% Number of literals : 237 ( 236 equ; 10 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 9 con; 0-2 aty)
% Number of variables : 147 ( 19 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t8,axiom,
add(X1,X2) = add(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t22,plain,
add(X1,X2) = add(X2,X1),
inference(orient,[status(thm)],[t8]) ).
cnf(t14,axiom,
sFlat0 = add(a,b),
introduced(definition) ).
cnf(t1727,plain,
sFlat0 = add(b,a),
inference(step,[status(thm)],[t14,t22]) ).
cnf(t80,plain,
add(b,a) = sFlat0,
inference(orient,[status(thm)],[t1727]) ).
cnf(t15,axiom,
sFlat1 = add(add(a,b),c),
introduced(definition) ).
cnf(t1721,plain,
sFlat1 = add(c,add(a,b)),
inference(step,[status(thm)],[t15,t22]) ).
cnf(t1722,plain,
sFlat1 = add(c,add(b,a)),
inference(step,[status(thm)],[t1721,t22]) ).
cnf(t32,plain,
add(c,add(b,a)) = sFlat1,
inference(orient,[status(thm)],[t1722]) ).
cnf(t1728,plain,
add(c,sFlat0) = sFlat1,
inference(step,[status(thm)],[t32,t80]) ).
cnf(t85,plain,
add(c,sFlat0) = sFlat1,
inference(rw,[status(thm)],[t1728]) ).
cnf(t1729,plain,
add(sFlat0,c) = sFlat1,
inference(step,[status(thm)],[t85,t22]) ).
cnf(t101,plain,
add(sFlat0,c) = sFlat1,
inference(orient,[status(thm)],[t1729]) ).
cnf(t16,axiom,
sFlat2 = add(b,c),
introduced(definition) ).
cnf(t1723,plain,
sFlat2 = add(c,b),
inference(step,[status(thm)],[t16,t22]) ).
cnf(t70,plain,
add(c,b) = sFlat2,
inference(orient,[status(thm)],[t1723]) ).
cnf(t17,axiom,
sFlat3 = add(a,add(b,c)),
introduced(definition) ).
cnf(t1724,plain,
sFlat3 = add(a,add(c,b)),
inference(step,[status(thm)],[t17,t22]) ).
cnf(t1725,plain,
sFlat3 = add(a,sFlat2),
inference(step,[status(thm)],[t1724,t70]) ).
cnf(t1726,plain,
sFlat3 = add(sFlat2,a),
inference(step,[status(thm)],[t1725,t22]) ).
cnf(t75,plain,
add(sFlat2,a) = sFlat3,
inference(orient,[status(thm)],[t1726]) ).
cnf(t12,axiom,
multiply(add(X1,X2),add(X1,X3)) = add(X1,multiply(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t23,plain,
multiply(add(X1,X2),add(X1,X3)) = add(X1,multiply(X2,X3)),
inference(orient,[status(thm)],[t12]) ).
cnf(t77,plain,
add(sFlat2,multiply(X1,a)) = multiply(add(sFlat2,X1),sFlat3),
inference(cp,[status(thm)],[t23,t75]) ).
cnf(t9,axiom,
multiply(X1,X2) = multiply(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t86,plain,
multiply(X1,X2) = multiply(X2,X1),
inference(orient,[status(thm)],[t9]) ).
cnf(t1753,plain,
add(sFlat2,multiply(X1,a)) = multiply(sFlat3,add(sFlat2,X1)),
inference(step,[status(thm)],[t77,t86]) ).
cnf(t268,plain,
add(sFlat2,multiply(X1,a)) = multiply(sFlat3,add(sFlat2,X1)),
inference(orient,[status(thm)],[t1753]) ).
cnf(t11,axiom,
add(multiply(X1,X2),multiply(X3,X2)) = multiply(add(X1,X3),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t45,plain,
add(multiply(X1,X2),multiply(X3,X2)) = multiply(add(X1,X3),X2),
inference(orient,[status(thm)],[t11]) ).
cnf(t13,axiom,
multiply(add(X1,X2),add(X3,X2)) = add(multiply(X1,X3),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t35,plain,
multiply(add(X1,X2),add(X3,X2)) = add(multiply(X1,X3),X2),
inference(orient,[status(thm)],[t13]) ).
cnf(t84,plain,
add(multiply(X1,b),a) = multiply(add(X1,a),sFlat0),
inference(cp,[status(thm)],[t35,t80]) ).
cnf(t1787,plain,
add(a,multiply(X1,b)) = multiply(add(X1,a),sFlat0),
inference(step,[status(thm)],[t84,t22]) ).
cnf(t1788,plain,
add(a,multiply(X1,b)) = multiply(sFlat0,add(X1,a)),
inference(step,[status(thm)],[t1787,t86]) ).
cnf(t504,plain,
add(a,multiply(X1,b)) = multiply(sFlat0,add(X1,a)),
inference(orient,[status(thm)],[t1788]) ).
cnf(t10,axiom,
add(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,add(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t57,plain,
add(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,add(X2,X3)),
inference(orient,[status(thm)],[t10]) ).
cnf(t2,axiom,
multiply(X1,multiplicative_identity) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t20,plain,
multiply(X1,multiplicative_identity) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t60,plain,
multiply(X1,add(multiplicative_identity,X2)) = add(X1,multiply(X1,X2)),
inference(cp,[status(thm)],[t57,t20]) ).
cnf(t147,plain,
add(X1,multiply(X1,X2)) = multiply(X1,add(multiplicative_identity,X2)),
inference(orient,[status(thm)],[t60]) ).
cnf(t506,plain,
multiply(sFlat0,add(a,a)) = multiply(a,add(multiplicative_identity,b)),
inference(cp,[status(thm)],[t504,t147]) ).
cnf(t0,axiom,
add(X1,additive_identity) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t18,plain,
add(X1,additive_identity) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t24,plain,
add(X1,multiply(additive_identity,X2)) = multiply(X1,add(X1,X2)),
inference(cp,[status(thm)],[t23,t18]) ).
cnf(t360,plain,
add(X1,multiply(additive_identity,X2)) = multiply(X1,add(X1,X2)),
inference(orient,[status(thm)],[t24]) ).
cnf(t3,axiom,
multiply(multiplicative_identity,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t21,plain,
multiply(multiplicative_identity,X1) = X1,
inference(orient,[status(thm)],[t3]) ).
cnf(t49,plain,
multiply(add(multiplicative_identity,X1),X2) = add(X2,multiply(X1,X2)),
inference(cp,[status(thm)],[t45,t21]) ).
cnf(t106,plain,
add(X1,multiply(X2,X1)) = multiply(add(multiplicative_identity,X2),X1),
inference(orient,[status(thm)],[t49]) ).
cnf(t1,axiom,
add(additive_identity,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t19,plain,
add(additive_identity,X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t108,plain,
multiply(add(multiplicative_identity,X1),additive_identity) = multiply(X1,additive_identity),
inference(cp,[status(thm)],[t106,t19]) ).
cnf(t1730,plain,
multiply(additive_identity,add(multiplicative_identity,X1)) = multiply(X1,additive_identity),
inference(step,[status(thm)],[t108,t86]) ).
cnf(t118,plain,
multiply(additive_identity,add(multiplicative_identity,X1)) = multiply(X1,additive_identity),
inference(orient,[status(thm)],[t1730]) ).
cnf(t119,plain,
multiply(additive_identity,additive_identity) = multiply(additive_identity,multiplicative_identity),
inference(cp,[status(thm)],[t118,t18]) ).
cnf(t1731,plain,
multiply(additive_identity,additive_identity) = additive_identity,
inference(step,[status(thm)],[t119,t20]) ).
cnf(t127,plain,
multiply(additive_identity,additive_identity) = additive_identity,
inference(orient,[status(thm)],[t1731]) ).
cnf(t371,plain,
multiply(X1,add(X1,additive_identity)) = add(X1,additive_identity),
inference(cp,[status(thm)],[t360,t127]) ).
cnf(t1768,plain,
multiply(X1,X1) = add(X1,additive_identity),
inference(step,[status(thm)],[t371,t18]) ).
cnf(t1769,plain,
multiply(X1,X1) = X1,
inference(step,[status(thm)],[t1768,t18]) ).
cnf(t398,plain,
multiply(X1,X1) = X1,
inference(orient,[status(thm)],[t1769]) ).
cnf(t404,plain,
multiply(X1,add(multiplicative_identity,X1)) = add(X1,X1),
inference(cp,[status(thm)],[t147,t398]) ).
cnf(t6,axiom,
multiply(X1,inverse(X1)) = additive_identity,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t93,plain,
multiply(X1,inverse(X1)) = additive_identity,
inference(orient,[status(thm)],[t6]) ).
cnf(t152,plain,
multiply(X1,add(multiplicative_identity,inverse(X1))) = add(X1,additive_identity),
inference(cp,[status(thm)],[t147,t93]) ).
cnf(t1734,plain,
multiply(X1,add(multiplicative_identity,inverse(X1))) = X1,
inference(step,[status(thm)],[t152,t18]) ).
cnf(t164,plain,
multiply(X1,add(multiplicative_identity,inverse(X1))) = X1,
inference(orient,[status(thm)],[t1734]) ).
cnf(t372,plain,
multiply(X1,add(X1,add(multiplicative_identity,inverse(additive_identity)))) = add(X1,additive_identity),
inference(cp,[status(thm)],[t360,t164]) ).
cnf(t4,axiom,
add(X1,inverse(X1)) = multiplicative_identity,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t28,plain,
add(X1,inverse(X1)) = multiplicative_identity,
inference(orient,[status(thm)],[t4]) ).
cnf(t29,plain,
multiplicative_identity = inverse(additive_identity),
inference(cp,[status(thm)],[t28,t19]) ).
cnf(t99,plain,
inverse(additive_identity) = multiplicative_identity,
inference(orient,[status(thm)],[t29]) ).
cnf(t1772,plain,
multiply(X1,add(X1,add(multiplicative_identity,multiplicative_identity))) = add(X1,additive_identity),
inference(step,[status(thm)],[t372,t99]) ).
cnf(t167,plain,
multiply(add(multiplicative_identity,X1),add(multiplicative_identity,inverse(X1))) = add(add(multiplicative_identity,inverse(X1)),X1),
inference(cp,[status(thm)],[t106,t164]) ).
cnf(t1735,plain,
add(multiplicative_identity,multiply(X1,inverse(X1))) = add(add(multiplicative_identity,inverse(X1)),X1),
inference(step,[status(thm)],[t167,t23]) ).
cnf(t1736,plain,
add(multiplicative_identity,additive_identity) = add(add(multiplicative_identity,inverse(X1)),X1),
inference(step,[status(thm)],[t1735,t93]) ).
cnf(t1737,plain,
multiplicative_identity = add(add(multiplicative_identity,inverse(X1)),X1),
inference(step,[status(thm)],[t1736,t18]) ).
cnf(t1738,plain,
multiplicative_identity = add(X1,add(multiplicative_identity,inverse(X1))),
inference(step,[status(thm)],[t1737,t22]) ).
cnf(t172,plain,
add(X1,add(multiplicative_identity,inverse(X1))) = multiplicative_identity,
inference(orient,[status(thm)],[t1738]) ).
cnf(t173,plain,
multiplicative_identity = add(multiplicative_identity,inverse(additive_identity)),
inference(cp,[status(thm)],[t172,t19]) ).
cnf(t1739,plain,
multiplicative_identity = add(multiplicative_identity,multiplicative_identity),
inference(step,[status(thm)],[t173,t99]) ).
cnf(t181,plain,
add(multiplicative_identity,multiplicative_identity) = multiplicative_identity,
inference(orient,[status(thm)],[t1739]) ).
cnf(t1773,plain,
multiply(X1,add(X1,multiplicative_identity)) = add(X1,additive_identity),
inference(step,[status(thm)],[t1772,t181]) ).
cnf(t1774,plain,
multiply(X1,add(X1,multiplicative_identity)) = X1,
inference(step,[status(thm)],[t1773,t18]) ).
cnf(t425,plain,
multiply(X1,add(X1,multiplicative_identity)) = X1,
inference(orient,[status(thm)],[t1774]) ).
cnf(t426,plain,
X1 = multiply(X1,add(multiplicative_identity,X1)),
inference(cp,[status(thm)],[t425,t22]) ).
cnf(t439,plain,
multiply(X1,add(multiplicative_identity,X1)) = X1,
inference(orient,[status(thm)],[t426]) ).
cnf(t1778,plain,
X1 = add(X1,X1),
inference(step,[status(thm)],[t404,t439]) ).
cnf(t465,plain,
add(X1,X1) = X1,
inference(orient,[status(thm)],[t1778]) ).
cnf(t1789,plain,
multiply(sFlat0,a) = multiply(a,add(multiplicative_identity,b)),
inference(step,[status(thm)],[t506,t465]) ).
cnf(t514,plain,
multiply(a,add(multiplicative_identity,b)) = multiply(sFlat0,a),
inference(orient,[status(thm)],[t1789]) ).
cnf(t409,plain,
multiply(add(X1,X2),X2) = add(multiply(X1,X2),X2),
inference(cp,[status(thm)],[t45,t398]) ).
cnf(t1838,plain,
multiply(X2,add(X1,X2)) = add(multiply(X1,X2),X2),
inference(step,[status(thm)],[t409,t86]) ).
cnf(t1839,plain,
multiply(X2,add(X1,X2)) = add(X2,multiply(X1,X2)),
inference(step,[status(thm)],[t1838,t22]) ).
cnf(t1840,plain,
multiply(X2,add(X1,X2)) = multiply(add(multiplicative_identity,X1),X2),
inference(step,[status(thm)],[t1839,t106]) ).
cnf(t791,plain,
multiply(X1,add(X2,X1)) = multiply(add(multiplicative_identity,X2),X1),
inference(orient,[status(thm)],[t1840]) ).
cnf(t798,plain,
multiply(add(multiplicative_identity,X1),add(multiplicative_identity,inverse(X1))) = multiply(add(multiplicative_identity,inverse(X1)),multiplicative_identity),
inference(cp,[status(thm)],[t791,t172]) ).
cnf(t1841,plain,
add(multiplicative_identity,multiply(X1,inverse(X1))) = multiply(add(multiplicative_identity,inverse(X1)),multiplicative_identity),
inference(step,[status(thm)],[t798,t23]) ).
cnf(t1842,plain,
add(multiplicative_identity,additive_identity) = multiply(add(multiplicative_identity,inverse(X1)),multiplicative_identity),
inference(step,[status(thm)],[t1841,t93]) ).
cnf(t1843,plain,
multiplicative_identity = multiply(add(multiplicative_identity,inverse(X1)),multiplicative_identity),
inference(step,[status(thm)],[t1842,t18]) ).
cnf(t1844,plain,
multiplicative_identity = add(multiplicative_identity,inverse(X1)),
inference(step,[status(thm)],[t1843,t20]) ).
cnf(t859,plain,
add(multiplicative_identity,inverse(X1)) = multiplicative_identity,
inference(orient,[status(thm)],[t1844]) ).
cnf(t1845,plain,
add(X1,multiplicative_identity) = multiplicative_identity,
inference(step,[status(thm)],[t172,t859]) ).
cnf(t865,plain,
add(X1,multiplicative_identity) = multiplicative_identity,
inference(rw,[status(thm)],[t1845]) ).
cnf(t866,plain,
add(X1,multiplicative_identity) = multiplicative_identity,
inference(orient,[status(thm)],[t865]) ).
cnf(t867,plain,
multiplicative_identity = add(multiplicative_identity,X1),
inference(cp,[status(thm)],[t866,t22]) ).
cnf(t873,plain,
add(multiplicative_identity,X1) = multiplicative_identity,
inference(orient,[status(thm)],[t867]) ).
cnf(t1876,plain,
multiply(a,multiplicative_identity) = multiply(sFlat0,a),
inference(step,[status(thm)],[t514,t873]) ).
cnf(t1877,plain,
a = multiply(sFlat0,a),
inference(step,[status(thm)],[t1876,t20]) ).
cnf(t885,plain,
a = multiply(sFlat0,a),
inference(rw,[status(thm)],[t1877]) ).
cnf(t954,plain,
multiply(sFlat0,a) = a,
inference(orient,[status(thm)],[t885]) ).
cnf(t961,plain,
multiply(add(sFlat0,X1),a) = add(a,multiply(X1,a)),
inference(cp,[status(thm)],[t45,t954]) ).
cnf(t1916,plain,
multiply(a,add(sFlat0,X1)) = add(a,multiply(X1,a)),
inference(step,[status(thm)],[t961,t86]) ).
cnf(t1854,plain,
add(X1,multiply(X2,X1)) = multiply(multiplicative_identity,X1),
inference(step,[status(thm)],[t106,t873]) ).
cnf(t1855,plain,
add(X1,multiply(X2,X1)) = X1,
inference(step,[status(thm)],[t1854,t21]) ).
cnf(t874,plain,
add(X1,multiply(X2,X1)) = X1,
inference(orient,[status(thm)],[t1855]) ).
cnf(t1917,plain,
multiply(a,add(sFlat0,X1)) = a,
inference(step,[status(thm)],[t1916,t874]) ).
cnf(t1354,plain,
multiply(a,add(sFlat0,X1)) = a,
inference(orient,[status(thm)],[t1917]) ).
cnf(t102,plain,
add(sFlat0,multiply(c,X1)) = multiply(sFlat1,add(sFlat0,X1)),
inference(cp,[status(thm)],[t23,t101]) ).
cnf(t530,plain,
add(sFlat0,multiply(c,X1)) = multiply(sFlat1,add(sFlat0,X1)),
inference(orient,[status(thm)],[t102]) ).
cnf(t531,plain,
multiply(sFlat1,add(sFlat0,sFlat0)) = multiply(add(multiplicative_identity,c),sFlat0),
inference(cp,[status(thm)],[t530,t106]) ).
cnf(t1795,plain,
multiply(sFlat1,sFlat0) = multiply(add(multiplicative_identity,c),sFlat0),
inference(step,[status(thm)],[t531,t465]) ).
cnf(t1796,plain,
multiply(sFlat0,sFlat1) = multiply(add(multiplicative_identity,c),sFlat0),
inference(step,[status(thm)],[t1795,t86]) ).
cnf(t1797,plain,
multiply(sFlat0,sFlat1) = multiply(sFlat0,add(multiplicative_identity,c)),
inference(step,[status(thm)],[t1796,t86]) ).
cnf(t549,plain,
multiply(sFlat0,add(multiplicative_identity,c)) = multiply(sFlat0,sFlat1),
inference(orient,[status(thm)],[t1797]) ).
cnf(t1874,plain,
multiply(sFlat0,multiplicative_identity) = multiply(sFlat0,sFlat1),
inference(step,[status(thm)],[t549,t873]) ).
cnf(t1875,plain,
sFlat0 = multiply(sFlat0,sFlat1),
inference(step,[status(thm)],[t1874,t20]) ).
cnf(t884,plain,
sFlat0 = multiply(sFlat0,sFlat1),
inference(rw,[status(thm)],[t1875]) ).
cnf(t947,plain,
multiply(sFlat0,sFlat1) = sFlat0,
inference(orient,[status(thm)],[t884]) ).
cnf(t949,plain,
sFlat1 = add(sFlat1,sFlat0),
inference(cp,[status(thm)],[t874,t947]) ).
cnf(t1885,plain,
sFlat1 = add(sFlat0,sFlat1),
inference(step,[status(thm)],[t949,t22]) ).
cnf(t1078,plain,
add(sFlat0,sFlat1) = sFlat1,
inference(orient,[status(thm)],[t1885]) ).
cnf(t1357,plain,
a = multiply(a,sFlat1),
inference(cp,[status(thm)],[t1354,t1078]) ).
cnf(t1918,plain,
a = multiply(sFlat1,a),
inference(step,[status(thm)],[t1357,t86]) ).
cnf(t1374,plain,
multiply(sFlat1,a) = a,
inference(orient,[status(thm)],[t1918]) ).
cnf(t1376,plain,
multiply(sFlat3,add(sFlat2,sFlat1)) = add(sFlat2,a),
inference(cp,[status(thm)],[t268,t1374]) ).
cnf(t1932,plain,
multiply(sFlat3,add(sFlat1,sFlat2)) = add(sFlat2,a),
inference(step,[status(thm)],[t1376,t22]) ).
cnf(t1858,plain,
add(X1,multiply(X1,X2)) = multiply(X1,multiplicative_identity),
inference(step,[status(thm)],[t147,t873]) ).
cnf(t1859,plain,
add(X1,multiply(X1,X2)) = X1,
inference(step,[status(thm)],[t1858,t20]) ).
cnf(t876,plain,
add(X1,multiply(X1,X2)) = X1,
inference(orient,[status(thm)],[t1859]) ).
cnf(t104,plain,
add(multiply(sFlat0,X1),c) = multiply(sFlat1,add(X1,c)),
inference(cp,[status(thm)],[t35,t101]) ).
cnf(t1800,plain,
add(c,multiply(sFlat0,X1)) = multiply(sFlat1,add(X1,c)),
inference(step,[status(thm)],[t104,t22]) ).
cnf(t570,plain,
add(c,multiply(sFlat0,X1)) = multiply(sFlat1,add(X1,c)),
inference(orient,[status(thm)],[t1800]) ).
cnf(t81,plain,
add(b,multiply(a,X1)) = multiply(sFlat0,add(b,X1)),
inference(cp,[status(thm)],[t23,t80]) ).
cnf(t309,plain,
add(b,multiply(a,X1)) = multiply(sFlat0,add(b,X1)),
inference(orient,[status(thm)],[t81]) ).
cnf(t311,plain,
multiply(sFlat0,add(b,b)) = multiply(add(multiplicative_identity,a),b),
inference(cp,[status(thm)],[t309,t106]) ).
cnf(t1830,plain,
multiply(sFlat0,b) = multiply(add(multiplicative_identity,a),b),
inference(step,[status(thm)],[t311,t465]) ).
cnf(t1831,plain,
multiply(sFlat0,b) = multiply(b,add(multiplicative_identity,a)),
inference(step,[status(thm)],[t1830,t86]) ).
cnf(t693,plain,
multiply(b,add(multiplicative_identity,a)) = multiply(sFlat0,b),
inference(orient,[status(thm)],[t1831]) ).
cnf(t1866,plain,
multiply(b,multiplicative_identity) = multiply(sFlat0,b),
inference(step,[status(thm)],[t693,t873]) ).
cnf(t1867,plain,
b = multiply(sFlat0,b),
inference(step,[status(thm)],[t1866,t20]) ).
cnf(t880,plain,
b = multiply(sFlat0,b),
inference(rw,[status(thm)],[t1867]) ).
cnf(t913,plain,
multiply(sFlat0,b) = b,
inference(orient,[status(thm)],[t880]) ).
cnf(t914,plain,
multiply(sFlat1,add(b,c)) = add(c,b),
inference(cp,[status(thm)],[t570,t913]) ).
cnf(t1896,plain,
multiply(sFlat1,add(c,b)) = add(c,b),
inference(step,[status(thm)],[t914,t22]) ).
cnf(t1897,plain,
multiply(sFlat1,sFlat2) = add(c,b),
inference(step,[status(thm)],[t1896,t70]) ).
cnf(t1898,plain,
multiply(sFlat1,sFlat2) = sFlat2,
inference(step,[status(thm)],[t1897,t70]) ).
cnf(t1187,plain,
multiply(sFlat1,sFlat2) = sFlat2,
inference(orient,[status(thm)],[t1898]) ).
cnf(t1189,plain,
sFlat1 = add(sFlat1,sFlat2),
inference(cp,[status(thm)],[t876,t1187]) ).
cnf(t1194,plain,
add(sFlat1,sFlat2) = sFlat1,
inference(orient,[status(thm)],[t1189]) ).
cnf(t1933,plain,
multiply(sFlat3,sFlat1) = add(sFlat2,a),
inference(step,[status(thm)],[t1932,t1194]) ).
cnf(t1934,plain,
multiply(sFlat1,sFlat3) = add(sFlat2,a),
inference(step,[status(thm)],[t1933,t86]) ).
cnf(t103,plain,
add(sFlat0,multiply(X1,c)) = multiply(add(sFlat0,X1),sFlat1),
inference(cp,[status(thm)],[t23,t101]) ).
cnf(t1799,plain,
add(sFlat0,multiply(X1,c)) = multiply(sFlat1,add(sFlat0,X1)),
inference(step,[status(thm)],[t103,t86]) ).
cnf(t563,plain,
add(sFlat0,multiply(X1,c)) = multiply(sFlat1,add(sFlat0,X1)),
inference(orient,[status(thm)],[t1799]) ).
cnf(t71,plain,
add(c,multiply(b,X1)) = multiply(sFlat2,add(c,X1)),
inference(cp,[status(thm)],[t23,t70]) ).
cnf(t182,plain,
add(c,multiply(b,X1)) = multiply(sFlat2,add(c,X1)),
inference(orient,[status(thm)],[t71]) ).
cnf(t183,plain,
multiply(sFlat2,add(c,c)) = multiply(add(multiplicative_identity,b),c),
inference(cp,[status(thm)],[t182,t106]) ).
cnf(t1810,plain,
multiply(sFlat2,c) = multiply(add(multiplicative_identity,b),c),
inference(step,[status(thm)],[t183,t465]) ).
cnf(t1811,plain,
multiply(sFlat2,c) = multiply(c,add(multiplicative_identity,b)),
inference(step,[status(thm)],[t1810,t86]) ).
cnf(t623,plain,
multiply(c,add(multiplicative_identity,b)) = multiply(sFlat2,c),
inference(orient,[status(thm)],[t1811]) ).
cnf(t1872,plain,
multiply(c,multiplicative_identity) = multiply(sFlat2,c),
inference(step,[status(thm)],[t623,t873]) ).
cnf(t1873,plain,
c = multiply(sFlat2,c),
inference(step,[status(thm)],[t1872,t20]) ).
cnf(t883,plain,
c = multiply(sFlat2,c),
inference(rw,[status(thm)],[t1873]) ).
cnf(t938,plain,
multiply(sFlat2,c) = c,
inference(orient,[status(thm)],[t883]) ).
cnf(t945,plain,
multiply(add(sFlat2,X1),c) = add(c,multiply(X1,c)),
inference(cp,[status(thm)],[t45,t938]) ).
cnf(t1907,plain,
multiply(c,add(sFlat2,X1)) = add(c,multiply(X1,c)),
inference(step,[status(thm)],[t945,t86]) ).
cnf(t1908,plain,
multiply(c,add(sFlat2,X1)) = c,
inference(step,[status(thm)],[t1907,t874]) ).
cnf(t1290,plain,
multiply(c,add(sFlat2,X1)) = c,
inference(orient,[status(thm)],[t1908]) ).
cnf(t76,plain,
add(sFlat2,multiply(a,X1)) = multiply(sFlat3,add(sFlat2,X1)),
inference(cp,[status(thm)],[t23,t75]) ).
cnf(t244,plain,
add(sFlat2,multiply(a,X1)) = multiply(sFlat3,add(sFlat2,X1)),
inference(orient,[status(thm)],[t76]) ).
cnf(t245,plain,
multiply(sFlat3,add(sFlat2,sFlat2)) = multiply(add(multiplicative_identity,a),sFlat2),
inference(cp,[status(thm)],[t244,t106]) ).
cnf(t1822,plain,
multiply(sFlat3,sFlat2) = multiply(add(multiplicative_identity,a),sFlat2),
inference(step,[status(thm)],[t245,t465]) ).
cnf(t1823,plain,
multiply(sFlat2,sFlat3) = multiply(add(multiplicative_identity,a),sFlat2),
inference(step,[status(thm)],[t1822,t86]) ).
cnf(t1824,plain,
multiply(sFlat2,sFlat3) = multiply(sFlat2,add(multiplicative_identity,a)),
inference(step,[status(thm)],[t1823,t86]) ).
cnf(t667,plain,
multiply(sFlat2,add(multiplicative_identity,a)) = multiply(sFlat2,sFlat3),
inference(orient,[status(thm)],[t1824]) ).
cnf(t1868,plain,
multiply(sFlat2,multiplicative_identity) = multiply(sFlat2,sFlat3),
inference(step,[status(thm)],[t667,t873]) ).
cnf(t1869,plain,
sFlat2 = multiply(sFlat2,sFlat3),
inference(step,[status(thm)],[t1868,t20]) ).
cnf(t881,plain,
sFlat2 = multiply(sFlat2,sFlat3),
inference(rw,[status(thm)],[t1869]) ).
cnf(t922,plain,
multiply(sFlat2,sFlat3) = sFlat2,
inference(orient,[status(thm)],[t881]) ).
cnf(t924,plain,
sFlat3 = add(sFlat3,sFlat2),
inference(cp,[status(thm)],[t874,t922]) ).
cnf(t1884,plain,
sFlat3 = add(sFlat2,sFlat3),
inference(step,[status(thm)],[t924,t22]) ).
cnf(t1057,plain,
add(sFlat2,sFlat3) = sFlat3,
inference(orient,[status(thm)],[t1884]) ).
cnf(t1293,plain,
c = multiply(c,sFlat3),
inference(cp,[status(thm)],[t1290,t1057]) ).
cnf(t1909,plain,
c = multiply(sFlat3,c),
inference(step,[status(thm)],[t1293,t86]) ).
cnf(t1309,plain,
multiply(sFlat3,c) = c,
inference(orient,[status(thm)],[t1909]) ).
cnf(t1310,plain,
multiply(sFlat1,add(sFlat0,sFlat3)) = add(sFlat0,c),
inference(cp,[status(thm)],[t563,t1309]) ).
cnf(t73,plain,
add(multiply(c,X1),b) = multiply(sFlat2,add(X1,b)),
inference(cp,[status(thm)],[t35,t70]) ).
cnf(t1744,plain,
add(b,multiply(c,X1)) = multiply(sFlat2,add(X1,b)),
inference(step,[status(thm)],[t73,t22]) ).
cnf(t213,plain,
add(b,multiply(c,X1)) = multiply(sFlat2,add(X1,b)),
inference(orient,[status(thm)],[t1744]) ).
cnf(t214,plain,
multiply(sFlat2,add(b,b)) = multiply(add(multiplicative_identity,c),b),
inference(cp,[status(thm)],[t213,t106]) ).
cnf(t1814,plain,
multiply(sFlat2,b) = multiply(add(multiplicative_identity,c),b),
inference(step,[status(thm)],[t214,t465]) ).
cnf(t1815,plain,
multiply(sFlat2,b) = multiply(b,add(multiplicative_identity,c)),
inference(step,[status(thm)],[t1814,t86]) ).
cnf(t641,plain,
multiply(b,add(multiplicative_identity,c)) = multiply(sFlat2,b),
inference(orient,[status(thm)],[t1815]) ).
cnf(t1870,plain,
multiply(b,multiplicative_identity) = multiply(sFlat2,b),
inference(step,[status(thm)],[t641,t873]) ).
cnf(t1871,plain,
b = multiply(sFlat2,b),
inference(step,[status(thm)],[t1870,t20]) ).
cnf(t882,plain,
b = multiply(sFlat2,b),
inference(rw,[status(thm)],[t1871]) ).
cnf(t929,plain,
multiply(sFlat2,b) = b,
inference(orient,[status(thm)],[t882]) ).
cnf(t930,plain,
multiply(sFlat0,add(sFlat2,a)) = add(a,b),
inference(cp,[status(thm)],[t504,t929]) ).
cnf(t1886,plain,
multiply(sFlat0,sFlat3) = add(a,b),
inference(step,[status(thm)],[t930,t75]) ).
cnf(t1887,plain,
multiply(sFlat0,sFlat3) = add(b,a),
inference(step,[status(thm)],[t1886,t22]) ).
cnf(t1888,plain,
multiply(sFlat0,sFlat3) = sFlat0,
inference(step,[status(thm)],[t1887,t80]) ).
cnf(t1092,plain,
multiply(sFlat0,sFlat3) = sFlat0,
inference(orient,[status(thm)],[t1888]) ).
cnf(t1094,plain,
sFlat3 = add(sFlat3,sFlat0),
inference(cp,[status(thm)],[t874,t1092]) ).
cnf(t1889,plain,
sFlat3 = add(sFlat0,sFlat3),
inference(step,[status(thm)],[t1094,t22]) ).
cnf(t1099,plain,
add(sFlat0,sFlat3) = sFlat3,
inference(orient,[status(thm)],[t1889]) ).
cnf(t1910,plain,
multiply(sFlat1,sFlat3) = add(sFlat0,c),
inference(step,[status(thm)],[t1310,t1099]) ).
cnf(t1911,plain,
multiply(sFlat1,sFlat3) = sFlat1,
inference(step,[status(thm)],[t1910,t101]) ).
cnf(t1317,plain,
multiply(sFlat1,sFlat3) = sFlat1,
inference(orient,[status(thm)],[t1911]) ).
cnf(t1935,plain,
sFlat1 = add(sFlat2,a),
inference(step,[status(thm)],[t1934,t1317]) ).
cnf(t1936,plain,
sFlat1 = sFlat3,
inference(step,[status(thm)],[t1935,t75]) ).
cnf(t1703,plain,
sFlat3 = sFlat1,
inference(orient,[status(thm)],[t1936]) ).
cnf(t1937,plain,
add(sFlat2,a) = sFlat1,
inference(step,[status(thm)],[t75,t1703]) ).
cnf(t1704,plain,
add(sFlat2,a) = sFlat1,
inference(orient,[status(thm)],[t1937]) ).
cnf(goal_0,negated_conjecture,
add(add(a,b),c) != add(a,add(b,c)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
add(c,add(a,b)) != add(a,add(b,c)),
inference(rw,[status(thm)],[goal_0,t22]) ).
cnf(g0_1,plain,
add(c,add(b,a)) != add(a,add(b,c)),
inference(rw,[status(thm)],[g0_0,t22]) ).
cnf(g0_2,plain,
add(c,sFlat0) != add(a,add(b,c)),
inference(rw,[status(thm)],[g0_1,t80]) ).
cnf(g0_3,plain,
add(sFlat0,c) != add(a,add(b,c)),
inference(rw,[status(thm)],[g0_2,t22]) ).
cnf(g0_4,plain,
sFlat1 != add(a,add(b,c)),
inference(rw,[status(thm)],[g0_3,t101]) ).
cnf(g0_5,plain,
sFlat1 != add(a,add(c,b)),
inference(rw,[status(thm)],[g0_4,t22]) ).
cnf(g0_6,plain,
sFlat1 != add(a,sFlat2),
inference(rw,[status(thm)],[g0_5,t70]) ).
cnf(g0_7,plain,
sFlat1 != add(sFlat2,a),
inference(rw,[status(thm)],[g0_6,t22]) ).
cnf(g0_8,plain,
sFlat1 != sFlat1,
inference(rw,[status(thm)],[g0_7,t1704]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_8]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : BOO008-2 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.35 % Computer : n017.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Fri Sep 25 06:24:18 UTC 2026
% 0.09/0.35 % CPUTime :
% 0.09/0.35 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 6.63/1.36 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.63/1.36 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------