%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : BOO015-2 : TPTP v9.3.1. Bugfixed v1.0.1.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/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:37 PM UTC 2026
% Result : Unsatisfiable 8.32s 1.73s
% Output : CNFRefutation 8.32s
% Verified :
% SZS Type : Refutation
% Derivation depth : 64
% Number of leaves : 16
% Syntax : Number of clauses : 240 ( 240 unt; 0 nHn; 91 RR)
% Number of literals : 240 ( 239 equ; 3 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 : 10 ( 10 usr; 7 con; 0-2 aty)
% Number of variables : 208 ( 29 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t16,axiom,
sFlat0 = inverse(c),
introduced(definition) ).
cnf(t87,plain,
inverse(c) = sFlat0,
inference(orient,[status(thm)],[t16]) ).
cnf(t12,axiom,
add(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,add(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t22,plain,
add(multiply(X1,X2),multiply(X1,X3)) = multiply(X1,add(X2,X3)),
inference(orient,[status(thm)],[t12]) ).
cnf(t7,axiom,
multiply(X1,inverse(X1)) = additive_identity,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t27,plain,
multiply(X1,inverse(X1)) = additive_identity,
inference(orient,[status(thm)],[t7]) ).
cnf(t89,plain,
additive_identity = multiply(c,sFlat0),
inference(cp,[status(thm)],[t27,t87]) ).
cnf(t11,axiom,
multiply(X1,X2) = multiply(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t21,plain,
multiply(X1,X2) = multiply(X2,X1),
inference(orient,[status(thm)],[t11]) ).
cnf(t3807,plain,
additive_identity = multiply(sFlat0,c),
inference(step,[status(thm)],[t89,t21]) ).
cnf(t97,plain,
multiply(sFlat0,c) = additive_identity,
inference(orient,[status(thm)],[t3807]) ).
cnf(t99,plain,
multiply(sFlat0,add(X1,c)) = add(multiply(sFlat0,X1),additive_identity),
inference(cp,[status(thm)],[t22,t97]) ).
cnf(t0,axiom,
add(X1,additive_identity) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t19,plain,
add(X1,additive_identity) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t3826,plain,
multiply(sFlat0,add(X1,c)) = multiply(sFlat0,X1),
inference(step,[status(thm)],[t99,t19]) ).
cnf(t172,plain,
multiply(sFlat0,add(X1,c)) = multiply(sFlat0,X1),
inference(orient,[status(thm)],[t3826]) ).
cnf(t14,axiom,
multiply(add(X1,X2),add(X1,X3)) = add(X1,multiply(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t51,plain,
multiply(add(X1,X2),add(X1,X3)) = add(X1,multiply(X2,X3)),
inference(orient,[status(thm)],[t14]) ).
cnf(t5,axiom,
add(X1,inverse(X1)) = multiplicative_identity,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t76,plain,
add(X1,inverse(X1)) = multiplicative_identity,
inference(orient,[status(thm)],[t5]) ).
cnf(t78,plain,
add(X1,multiply(inverse(X1),X2)) = multiply(multiplicative_identity,add(X1,X2)),
inference(cp,[status(thm)],[t51,t76]) ).
cnf(t4,axiom,
multiply(multiplicative_identity,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t18,plain,
multiply(multiplicative_identity,X1) = X1,
inference(orient,[status(thm)],[t4]) ).
cnf(t4195,plain,
add(X1,multiply(inverse(X1),X2)) = add(X1,X2),
inference(step,[status(thm)],[t78,t18]) ).
cnf(t3709,plain,
add(X1,multiply(inverse(X1),X2)) = add(X1,X2),
inference(orient,[status(thm)],[t4195]) ).
cnf(t24,plain,
multiply(X1,add(X2,X3)) = add(multiply(X2,X1),multiply(X1,X3)),
inference(cp,[status(thm)],[t22,t21]) ).
cnf(t1105,plain,
add(multiply(X1,X2),multiply(X2,X3)) = multiply(X2,add(X1,X3)),
inference(orient,[status(thm)],[t24]) ).
cnf(t15,axiom,
multiply(add(X1,X2),add(X3,X2)) = add(multiply(X1,X3),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t39,plain,
multiply(add(X1,X2),add(X3,X2)) = add(multiply(X1,X3),X2),
inference(orient,[status(thm)],[t15]) ).
cnf(t2,axiom,
multiply(X1,multiplicative_identity) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t17,plain,
multiply(X1,multiplicative_identity) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t23,plain,
multiply(X1,add(multiplicative_identity,X2)) = add(X1,multiply(X1,X2)),
inference(cp,[status(thm)],[t22,t17]) ).
cnf(t310,plain,
add(X1,multiply(X1,X2)) = multiply(X1,add(multiplicative_identity,X2)),
inference(orient,[status(thm)],[t23]) ).
cnf(t314,plain,
multiply(X1,add(multiplicative_identity,multiplicative_identity)) = add(X1,X1),
inference(cp,[status(thm)],[t310,t17]) ).
cnf(t88,plain,
multiplicative_identity = add(c,sFlat0),
inference(cp,[status(thm)],[t76,t87]) ).
cnf(t9,axiom,
add(X1,X2) = add(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t69,plain,
add(X1,X2) = add(X2,X1),
inference(orient,[status(thm)],[t9]) ).
cnf(t3806,plain,
multiplicative_identity = add(sFlat0,c),
inference(step,[status(thm)],[t88,t69]) ).
cnf(t92,plain,
add(sFlat0,c) = multiplicative_identity,
inference(orient,[status(thm)],[t3806]) ).
cnf(t93,plain,
add(sFlat0,multiply(c,X1)) = multiply(multiplicative_identity,add(sFlat0,X1)),
inference(cp,[status(thm)],[t51,t92]) ).
cnf(t3808,plain,
add(sFlat0,multiply(c,X1)) = add(sFlat0,X1),
inference(step,[status(thm)],[t93,t18]) ).
cnf(t102,plain,
add(sFlat0,multiply(c,X1)) = add(sFlat0,X1),
inference(orient,[status(thm)],[t3808]) ).
cnf(t103,plain,
add(sFlat0,multiplicative_identity) = add(sFlat0,c),
inference(cp,[status(thm)],[t102,t17]) ).
cnf(t3809,plain,
add(sFlat0,multiplicative_identity) = multiplicative_identity,
inference(step,[status(thm)],[t103,t92]) ).
cnf(t110,plain,
add(sFlat0,multiplicative_identity) = multiplicative_identity,
inference(orient,[status(thm)],[t3809]) ).
cnf(t111,plain,
add(multiply(sFlat0,X1),multiplicative_identity) = multiply(multiplicative_identity,add(X1,multiplicative_identity)),
inference(cp,[status(thm)],[t39,t110]) ).
cnf(t3837,plain,
add(multiplicative_identity,multiply(sFlat0,X1)) = multiply(multiplicative_identity,add(X1,multiplicative_identity)),
inference(step,[status(thm)],[t111,t69]) ).
cnf(t3838,plain,
add(multiplicative_identity,multiply(sFlat0,X1)) = add(X1,multiplicative_identity),
inference(step,[status(thm)],[t3837,t18]) ).
cnf(t212,plain,
add(multiplicative_identity,multiply(sFlat0,X1)) = add(X1,multiplicative_identity),
inference(orient,[status(thm)],[t3838]) ).
cnf(t217,plain,
add(multiplicative_identity,multiplicative_identity) = add(multiplicative_identity,sFlat0),
inference(cp,[status(thm)],[t212,t17]) ).
cnf(t3839,plain,
add(multiplicative_identity,multiplicative_identity) = add(sFlat0,multiplicative_identity),
inference(step,[status(thm)],[t217,t69]) ).
cnf(t3840,plain,
add(multiplicative_identity,multiplicative_identity) = multiplicative_identity,
inference(step,[status(thm)],[t3839,t110]) ).
cnf(t224,plain,
add(multiplicative_identity,multiplicative_identity) = multiplicative_identity,
inference(orient,[status(thm)],[t3840]) ).
cnf(t3863,plain,
multiply(X1,multiplicative_identity) = add(X1,X1),
inference(step,[status(thm)],[t314,t224]) ).
cnf(t3864,plain,
X1 = add(X1,X1),
inference(step,[status(thm)],[t3863,t17]) ).
cnf(t337,plain,
add(X1,X1) = X1,
inference(orient,[status(thm)],[t3864]) ).
cnf(t344,plain,
add(multiply(X1,X2),X1) = multiply(X1,add(X2,X1)),
inference(cp,[status(thm)],[t39,t337]) ).
cnf(t3926,plain,
add(X1,multiply(X1,X2)) = multiply(X1,add(X2,X1)),
inference(step,[status(thm)],[t344,t69]) ).
cnf(t3927,plain,
multiply(X1,add(multiplicative_identity,X2)) = multiply(X1,add(X2,X1)),
inference(step,[status(thm)],[t3926,t310]) ).
cnf(t936,plain,
multiply(X1,add(multiplicative_identity,X2)) = multiply(X1,add(X2,X1)),
inference(orient,[status(thm)],[t3927]) ).
cnf(t13,axiom,
add(multiply(X1,X2),multiply(X3,X2)) = multiply(add(X1,X3),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t31,plain,
add(multiply(X1,X2),multiply(X3,X2)) = multiply(add(X1,X3),X2),
inference(orient,[status(thm)],[t13]) ).
cnf(t34,plain,
multiply(add(multiplicative_identity,X1),X2) = add(X2,multiply(X1,X2)),
inference(cp,[status(thm)],[t31,t18]) ).
cnf(t465,plain,
add(X1,multiply(X2,X1)) = multiply(add(multiplicative_identity,X2),X1),
inference(orient,[status(thm)],[t34]) ).
cnf(t315,plain,
multiply(X1,add(multiplicative_identity,inverse(X1))) = add(X1,additive_identity),
inference(cp,[status(thm)],[t310,t27]) ).
cnf(t3881,plain,
multiply(X1,add(multiplicative_identity,inverse(X1))) = X1,
inference(step,[status(thm)],[t315,t19]) ).
cnf(t453,plain,
multiply(X1,add(multiplicative_identity,inverse(X1))) = X1,
inference(orient,[status(thm)],[t3881]) ).
cnf(t471,plain,
multiply(add(multiplicative_identity,X1),add(multiplicative_identity,inverse(X1))) = add(add(multiplicative_identity,inverse(X1)),X1),
inference(cp,[status(thm)],[t465,t453]) ).
cnf(t3890,plain,
add(multiplicative_identity,multiply(X1,inverse(X1))) = add(add(multiplicative_identity,inverse(X1)),X1),
inference(step,[status(thm)],[t471,t51]) ).
cnf(t3891,plain,
add(multiplicative_identity,additive_identity) = add(add(multiplicative_identity,inverse(X1)),X1),
inference(step,[status(thm)],[t3890,t27]) ).
cnf(t3892,plain,
multiplicative_identity = add(add(multiplicative_identity,inverse(X1)),X1),
inference(step,[status(thm)],[t3891,t19]) ).
cnf(t3893,plain,
multiplicative_identity = add(X1,add(multiplicative_identity,inverse(X1))),
inference(step,[status(thm)],[t3892,t69]) ).
cnf(t514,plain,
add(X1,add(multiplicative_identity,inverse(X1))) = multiplicative_identity,
inference(orient,[status(thm)],[t3893]) ).
cnf(t345,plain,
add(multiply(X1,X2),X2) = multiply(add(X1,X2),X2),
inference(cp,[status(thm)],[t39,t337]) ).
cnf(t3928,plain,
add(X2,multiply(X1,X2)) = multiply(add(X1,X2),X2),
inference(step,[status(thm)],[t345,t69]) ).
cnf(t3929,plain,
multiply(add(multiplicative_identity,X1),X2) = multiply(add(X1,X2),X2),
inference(step,[status(thm)],[t3928,t465]) ).
cnf(t3930,plain,
multiply(add(multiplicative_identity,X1),X2) = multiply(X2,add(X1,X2)),
inference(step,[status(thm)],[t3929,t21]) ).
cnf(t997,plain,
multiply(add(multiplicative_identity,X1),X2) = multiply(X2,add(X1,X2)),
inference(orient,[status(thm)],[t3930]) ).
cnf(t1036,plain,
multiply(add(multiplicative_identity,X1),add(multiplicative_identity,inverse(X1))) = multiply(add(multiplicative_identity,inverse(X1)),multiplicative_identity),
inference(cp,[status(thm)],[t997,t514]) ).
cnf(t3931,plain,
add(multiplicative_identity,multiply(X1,inverse(X1))) = multiply(add(multiplicative_identity,inverse(X1)),multiplicative_identity),
inference(step,[status(thm)],[t1036,t51]) ).
cnf(t3932,plain,
add(multiplicative_identity,additive_identity) = multiply(add(multiplicative_identity,inverse(X1)),multiplicative_identity),
inference(step,[status(thm)],[t3931,t27]) ).
cnf(t3933,plain,
multiplicative_identity = multiply(add(multiplicative_identity,inverse(X1)),multiplicative_identity),
inference(step,[status(thm)],[t3932,t19]) ).
cnf(t3934,plain,
multiplicative_identity = add(multiplicative_identity,inverse(X1)),
inference(step,[status(thm)],[t3933,t17]) ).
cnf(t1065,plain,
add(multiplicative_identity,inverse(X1)) = multiplicative_identity,
inference(orient,[status(thm)],[t3934]) ).
cnf(t3935,plain,
add(X1,multiplicative_identity) = multiplicative_identity,
inference(step,[status(thm)],[t514,t1065]) ).
cnf(t1075,plain,
add(X1,multiplicative_identity) = multiplicative_identity,
inference(rw,[status(thm)],[t3935]) ).
cnf(t1076,plain,
add(X1,multiplicative_identity) = multiplicative_identity,
inference(orient,[status(thm)],[t1075]) ).
cnf(t1087,plain,
multiplicative_identity = add(multiplicative_identity,X1),
inference(cp,[status(thm)],[t1076,t69]) ).
cnf(t1091,plain,
add(multiplicative_identity,X1) = multiplicative_identity,
inference(orient,[status(thm)],[t1087]) ).
cnf(t3962,plain,
multiply(X1,multiplicative_identity) = multiply(X1,add(X2,X1)),
inference(step,[status(thm)],[t936,t1091]) ).
cnf(t3963,plain,
X1 = multiply(X1,add(X2,X1)),
inference(step,[status(thm)],[t3962,t17]) ).
cnf(t1098,plain,
X1 = multiply(X1,add(X2,X1)),
inference(rw,[status(thm)],[t3963]) ).
cnf(t1245,plain,
multiply(X1,add(X2,X1)) = X1,
inference(orient,[status(thm)],[t1098]) ).
cnf(t10,axiom,
add(inverse(a),inverse(b)) = d,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t3805,plain,
add(inverse(b),inverse(a)) = d,
inference(step,[status(thm)],[t10,t69]) ).
cnf(t82,plain,
add(inverse(b),inverse(a)) = d,
inference(orient,[status(thm)],[t3805]) ).
cnf(t1257,plain,
inverse(a) = multiply(inverse(a),d),
inference(cp,[status(thm)],[t1245,t82]) ).
cnf(t3996,plain,
inverse(a) = multiply(d,inverse(a)),
inference(step,[status(thm)],[t1257,t21]) ).
cnf(t1273,plain,
multiply(d,inverse(a)) = inverse(a),
inference(orient,[status(thm)],[t3996]) ).
cnf(t1276,plain,
multiply(inverse(a),add(d,X1)) = add(inverse(a),multiply(inverse(a),X1)),
inference(cp,[status(thm)],[t1105,t1273]) ).
cnf(t3950,plain,
add(X1,multiply(X1,X2)) = multiply(X1,multiplicative_identity),
inference(step,[status(thm)],[t310,t1091]) ).
cnf(t3951,plain,
add(X1,multiply(X1,X2)) = X1,
inference(step,[status(thm)],[t3950,t17]) ).
cnf(t1092,plain,
add(X1,multiply(X1,X2)) = X1,
inference(orient,[status(thm)],[t3951]) ).
cnf(t4081,plain,
multiply(inverse(a),add(d,X1)) = inverse(a),
inference(step,[status(thm)],[t1276,t1092]) ).
cnf(t2131,plain,
multiply(inverse(a),add(d,X1)) = inverse(a),
inference(orient,[status(thm)],[t4081]) ).
cnf(t3954,plain,
add(X1,multiply(X2,X1)) = multiply(multiplicative_identity,X1),
inference(step,[status(thm)],[t465,t1091]) ).
cnf(t3955,plain,
add(X1,multiply(X2,X1)) = X1,
inference(step,[status(thm)],[t3954,t18]) ).
cnf(t1094,plain,
add(X1,multiply(X2,X1)) = X1,
inference(orient,[status(thm)],[t3955]) ).
cnf(t1267,plain,
add(X1,X2) = add(add(X1,X2),X2),
inference(cp,[status(thm)],[t1094,t1245]) ).
cnf(t4032,plain,
add(X1,X2) = add(X2,add(X1,X2)),
inference(step,[status(thm)],[t1267,t69]) ).
cnf(t1578,plain,
add(X1,add(X2,X1)) = add(X2,X1),
inference(orient,[status(thm)],[t4032]) ).
cnf(t2137,plain,
inverse(a) = multiply(inverse(a),add(X1,d)),
inference(cp,[status(thm)],[t2131,t1578]) ).
cnf(t2219,plain,
multiply(inverse(a),add(X1,d)) = inverse(a),
inference(orient,[status(thm)],[t2137]) ).
cnf(t3721,plain,
add(a,add(X1,d)) = add(a,inverse(a)),
inference(cp,[status(thm)],[t3709,t2219]) ).
cnf(t4201,plain,
add(a,add(X1,d)) = multiplicative_identity,
inference(step,[status(thm)],[t3721,t76]) ).
cnf(t3763,plain,
add(a,add(X1,d)) = multiplicative_identity,
inference(orient,[status(thm)],[t4201]) ).
cnf(t100,plain,
multiply(add(sFlat0,X1),c) = add(additive_identity,multiply(X1,c)),
inference(cp,[status(thm)],[t31,t97]) ).
cnf(t3827,plain,
multiply(c,add(sFlat0,X1)) = add(additive_identity,multiply(X1,c)),
inference(step,[status(thm)],[t100,t21]) ).
cnf(t1,axiom,
add(additive_identity,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t20,plain,
add(additive_identity,X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t3828,plain,
multiply(c,add(sFlat0,X1)) = multiply(X1,c),
inference(step,[status(thm)],[t3827,t20]) ).
cnf(t178,plain,
multiply(c,add(sFlat0,X1)) = multiply(X1,c),
inference(orient,[status(thm)],[t3828]) ).
cnf(t180,plain,
multiply(c,c) = multiply(c,multiplicative_identity),
inference(cp,[status(thm)],[t178,t92]) ).
cnf(t3829,plain,
multiply(c,c) = c,
inference(step,[status(thm)],[t180,t17]) ).
cnf(t191,plain,
multiply(c,c) = c,
inference(orient,[status(thm)],[t3829]) ).
cnf(t192,plain,
multiply(c,add(c,X1)) = add(c,multiply(c,X1)),
inference(cp,[status(thm)],[t22,t191]) ).
cnf(t3904,plain,
multiply(c,add(c,X1)) = multiply(c,add(multiplicative_identity,X1)),
inference(step,[status(thm)],[t192,t310]) ).
cnf(t632,plain,
multiply(c,add(c,X1)) = multiply(c,add(multiplicative_identity,X1)),
inference(orient,[status(thm)],[t3904]) ).
cnf(t3958,plain,
multiply(c,add(c,X1)) = multiply(c,multiplicative_identity),
inference(step,[status(thm)],[t632,t1091]) ).
cnf(t3959,plain,
multiply(c,add(c,X1)) = c,
inference(step,[status(thm)],[t3958,t17]) ).
cnf(t1096,plain,
multiply(c,add(c,X1)) = c,
inference(orient,[status(thm)],[t3959]) ).
cnf(t3,axiom,
multiply(a,b) = c,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t3804,plain,
multiply(b,a) = c,
inference(step,[status(thm)],[t3,t21]) ).
cnf(t64,plain,
multiply(b,a) = c,
inference(orient,[status(thm)],[t3804]) ).
cnf(t489,plain,
multiply(add(multiplicative_identity,b),a) = add(a,c),
inference(cp,[status(thm)],[t465,t64]) ).
cnf(t3888,plain,
multiply(a,add(multiplicative_identity,b)) = add(a,c),
inference(step,[status(thm)],[t489,t21]) ).
cnf(t3889,plain,
multiply(a,add(multiplicative_identity,b)) = add(c,a),
inference(step,[status(thm)],[t3888,t69]) ).
cnf(t507,plain,
multiply(a,add(multiplicative_identity,b)) = add(c,a),
inference(orient,[status(thm)],[t3889]) ).
cnf(t3970,plain,
multiply(a,multiplicative_identity) = add(c,a),
inference(step,[status(thm)],[t507,t1091]) ).
cnf(t3971,plain,
a = add(c,a),
inference(step,[status(thm)],[t3970,t17]) ).
cnf(t1102,plain,
a = add(c,a),
inference(rw,[status(thm)],[t3971]) ).
cnf(t1188,plain,
add(c,a) = a,
inference(orient,[status(thm)],[t1102]) ).
cnf(t1191,plain,
c = multiply(c,a),
inference(cp,[status(thm)],[t1096,t1188]) ).
cnf(t1212,plain,
multiply(c,a) = c,
inference(orient,[status(thm)],[t1191]) ).
cnf(t1220,plain,
add(sFlat0,a) = add(sFlat0,c),
inference(cp,[status(thm)],[t102,t1212]) ).
cnf(t3994,plain,
add(sFlat0,a) = multiplicative_identity,
inference(step,[status(thm)],[t1220,t92]) ).
cnf(t1233,plain,
add(sFlat0,a) = multiplicative_identity,
inference(orient,[status(thm)],[t3994]) ).
cnf(t1237,plain,
add(multiply(sFlat0,X1),a) = multiply(multiplicative_identity,add(X1,a)),
inference(cp,[status(thm)],[t39,t1233]) ).
cnf(t4013,plain,
add(a,multiply(sFlat0,X1)) = multiply(multiplicative_identity,add(X1,a)),
inference(step,[status(thm)],[t1237,t69]) ).
cnf(t4014,plain,
add(a,multiply(sFlat0,X1)) = add(X1,a),
inference(step,[status(thm)],[t4013,t18]) ).
cnf(t1447,plain,
add(a,multiply(sFlat0,X1)) = add(X1,a),
inference(orient,[status(thm)],[t4014]) ).
cnf(t98,plain,
multiply(sFlat0,add(c,X1)) = add(additive_identity,multiply(sFlat0,X1)),
inference(cp,[status(thm)],[t22,t97]) ).
cnf(t3822,plain,
multiply(sFlat0,add(c,X1)) = multiply(sFlat0,X1),
inference(step,[status(thm)],[t98,t20]) ).
cnf(t151,plain,
multiply(sFlat0,add(c,X1)) = multiply(sFlat0,X1),
inference(orient,[status(thm)],[t3822]) ).
cnf(t1451,plain,
add(add(c,X1),a) = add(a,multiply(sFlat0,X1)),
inference(cp,[status(thm)],[t1447,t151]) ).
cnf(t4048,plain,
add(a,add(c,X1)) = add(a,multiply(sFlat0,X1)),
inference(step,[status(thm)],[t1451,t69]) ).
cnf(t4049,plain,
add(a,add(c,X1)) = add(X1,a),
inference(step,[status(thm)],[t4048,t1447]) ).
cnf(t1772,plain,
add(a,add(c,X1)) = add(X1,a),
inference(orient,[status(thm)],[t4049]) ).
cnf(t3764,plain,
multiplicative_identity = add(d,a),
inference(cp,[status(thm)],[t3763,t1772]) ).
cnf(t67,plain,
multiply(add(b,X1),a) = add(c,multiply(X1,a)),
inference(cp,[status(thm)],[t31,t64]) ).
cnf(t3899,plain,
multiply(a,add(b,X1)) = add(c,multiply(X1,a)),
inference(step,[status(thm)],[t67,t21]) ).
cnf(t577,plain,
add(c,multiply(X1,a)) = multiply(a,add(b,X1)),
inference(orient,[status(thm)],[t3899]) ).
cnf(t583,plain,
multiply(a,add(b,X1)) = add(c,multiply(a,X1)),
inference(cp,[status(thm)],[t577,t21]) ).
cnf(t2284,plain,
add(c,multiply(a,X1)) = multiply(a,add(b,X1)),
inference(orient,[status(thm)],[t583]) ).
cnf(t1194,plain,
add(c,multiply(a,X1)) = multiply(a,add(c,X1)),
inference(cp,[status(thm)],[t51,t1188]) ).
cnf(t4086,plain,
multiply(a,add(b,X1)) = multiply(a,add(c,X1)),
inference(step,[status(thm)],[t1194,t2284]) ).
cnf(t2319,plain,
multiply(a,add(b,X1)) = multiply(a,add(c,X1)),
inference(orient,[status(thm)],[t4086]) ).
cnf(t4089,plain,
add(c,multiply(a,X1)) = multiply(a,add(c,X1)),
inference(step,[status(thm)],[t2284,t2319]) ).
cnf(t2322,plain,
add(c,multiply(a,X1)) = multiply(a,add(c,X1)),
inference(orient,[status(thm)],[t4089]) ).
cnf(t30,plain,
multiply(X1,add(X2,inverse(X1))) = add(multiply(X1,X2),additive_identity),
inference(cp,[status(thm)],[t22,t27]) ).
cnf(t4113,plain,
multiply(X1,add(X2,inverse(X1))) = multiply(X1,X2),
inference(step,[status(thm)],[t30,t19]) ).
cnf(t2599,plain,
multiply(X1,add(X2,inverse(X1))) = multiply(X1,X2),
inference(orient,[status(thm)],[t4113]) ).
cnf(t2608,plain,
multiply(a,inverse(b)) = multiply(a,d),
inference(cp,[status(thm)],[t2599,t82]) ).
cnf(t4116,plain,
multiply(a,inverse(b)) = multiply(d,a),
inference(step,[status(thm)],[t2608,t21]) ).
cnf(t2632,plain,
multiply(a,inverse(b)) = multiply(d,a),
inference(orient,[status(thm)],[t4116]) ).
cnf(t2635,plain,
multiply(a,add(c,inverse(b))) = add(c,multiply(d,a)),
inference(cp,[status(thm)],[t2322,t2632]) ).
cnf(t2333,plain,
multiply(a,add(c,inverse(b))) = multiply(a,multiplicative_identity),
inference(cp,[status(thm)],[t2319,t76]) ).
cnf(t4092,plain,
multiply(a,add(c,inverse(b))) = a,
inference(step,[status(thm)],[t2333,t17]) ).
cnf(t2347,plain,
multiply(a,add(c,inverse(b))) = a,
inference(orient,[status(thm)],[t4092]) ).
cnf(t4128,plain,
a = add(c,multiply(d,a)),
inference(step,[status(thm)],[t2635,t2347]) ).
cnf(t4087,plain,
add(c,multiply(X1,a)) = multiply(a,add(c,X1)),
inference(step,[status(thm)],[t577,t2319]) ).
cnf(t2320,plain,
add(c,multiply(X1,a)) = multiply(a,add(c,X1)),
inference(orient,[status(thm)],[t4087]) ).
cnf(t4129,plain,
a = multiply(a,add(c,d)),
inference(step,[status(thm)],[t4128,t2320]) ).
cnf(t4130,plain,
a = multiply(a,add(d,c)),
inference(step,[status(thm)],[t4129,t69]) ).
cnf(t2744,plain,
multiply(a,add(d,c)) = a,
inference(orient,[status(thm)],[t4130]) ).
cnf(t2753,plain,
add(d,c) = add(add(d,c),a),
inference(cp,[status(thm)],[t1094,t2744]) ).
cnf(t4150,plain,
add(d,c) = add(a,add(d,c)),
inference(step,[status(thm)],[t2753,t69]) ).
cnf(t1452,plain,
add(add(X1,c),a) = add(a,multiply(sFlat0,X1)),
inference(cp,[status(thm)],[t1447,t172]) ).
cnf(t4054,plain,
add(a,add(X1,c)) = add(a,multiply(sFlat0,X1)),
inference(step,[status(thm)],[t1452,t69]) ).
cnf(t4055,plain,
add(a,add(X1,c)) = add(X1,a),
inference(step,[status(thm)],[t4054,t1447]) ).
cnf(t1818,plain,
add(a,add(X1,c)) = add(X1,a),
inference(orient,[status(thm)],[t4055]) ).
cnf(t4151,plain,
add(d,c) = add(d,a),
inference(step,[status(thm)],[t4150,t1818]) ).
cnf(t3022,plain,
add(d,a) = add(d,c),
inference(orient,[status(thm)],[t4151]) ).
cnf(t4202,plain,
multiplicative_identity = add(d,c),
inference(step,[status(thm)],[t3764,t3022]) ).
cnf(t3776,plain,
add(d,c) = multiplicative_identity,
inference(orient,[status(thm)],[t4202]) ).
cnf(t3782,plain,
multiply(sFlat0,d) = multiply(sFlat0,multiplicative_identity),
inference(cp,[status(thm)],[t172,t3776]) ).
cnf(t325,plain,
multiply(b,add(multiplicative_identity,a)) = add(b,c),
inference(cp,[status(thm)],[t310,t64]) ).
cnf(t3879,plain,
multiply(b,add(multiplicative_identity,a)) = add(c,b),
inference(step,[status(thm)],[t325,t69]) ).
cnf(t441,plain,
multiply(b,add(multiplicative_identity,a)) = add(c,b),
inference(orient,[status(thm)],[t3879]) ).
cnf(t3972,plain,
multiply(b,multiplicative_identity) = add(c,b),
inference(step,[status(thm)],[t441,t1091]) ).
cnf(t3973,plain,
b = add(c,b),
inference(step,[status(thm)],[t3972,t17]) ).
cnf(t1103,plain,
b = add(c,b),
inference(rw,[status(thm)],[t3973]) ).
cnf(t1198,plain,
add(c,b) = b,
inference(orient,[status(thm)],[t1103]) ).
cnf(t1203,plain,
c = multiply(c,b),
inference(cp,[status(thm)],[t1096,t1198]) ).
cnf(t1223,plain,
multiply(c,b) = c,
inference(orient,[status(thm)],[t1203]) ).
cnf(t1230,plain,
add(sFlat0,b) = add(sFlat0,c),
inference(cp,[status(thm)],[t102,t1223]) ).
cnf(t3995,plain,
add(sFlat0,b) = multiplicative_identity,
inference(step,[status(thm)],[t1230,t92]) ).
cnf(t1239,plain,
add(sFlat0,b) = multiplicative_identity,
inference(orient,[status(thm)],[t3995]) ).
cnf(t1241,plain,
add(sFlat0,multiply(b,X1)) = multiply(multiplicative_identity,add(sFlat0,X1)),
inference(cp,[status(thm)],[t51,t1239]) ).
cnf(t4017,plain,
add(sFlat0,multiply(b,X1)) = add(sFlat0,X1),
inference(step,[status(thm)],[t1241,t18]) ).
cnf(t1471,plain,
add(sFlat0,multiply(b,X1)) = add(sFlat0,X1),
inference(orient,[status(thm)],[t4017]) ).
cnf(t29,plain,
multiply(X1,add(inverse(X1),X2)) = add(additive_identity,multiply(X1,X2)),
inference(cp,[status(thm)],[t22,t27]) ).
cnf(t4105,plain,
multiply(X1,add(inverse(X1),X2)) = multiply(X1,X2),
inference(step,[status(thm)],[t29,t20]) ).
cnf(t2490,plain,
multiply(X1,add(inverse(X1),X2)) = multiply(X1,X2),
inference(orient,[status(thm)],[t4105]) ).
cnf(t2499,plain,
multiply(b,inverse(a)) = multiply(b,d),
inference(cp,[status(thm)],[t2490,t82]) ).
cnf(t4106,plain,
multiply(b,inverse(a)) = multiply(d,b),
inference(step,[status(thm)],[t2499,t21]) ).
cnf(t2524,plain,
multiply(b,inverse(a)) = multiply(d,b),
inference(orient,[status(thm)],[t4106]) ).
cnf(t2531,plain,
add(sFlat0,inverse(a)) = add(sFlat0,multiply(d,b)),
inference(cp,[status(thm)],[t1471,t2524]) ).
cnf(t1235,plain,
add(sFlat0,multiply(a,X1)) = multiply(multiplicative_identity,add(sFlat0,X1)),
inference(cp,[status(thm)],[t51,t1233]) ).
cnf(t4006,plain,
add(sFlat0,multiply(a,X1)) = add(sFlat0,X1),
inference(step,[status(thm)],[t1235,t18]) ).
cnf(t1408,plain,
add(sFlat0,multiply(a,X1)) = add(sFlat0,X1),
inference(orient,[status(thm)],[t4006]) ).
cnf(t1409,plain,
add(sFlat0,inverse(a)) = add(sFlat0,additive_identity),
inference(cp,[status(thm)],[t1408,t27]) ).
cnf(t4007,plain,
add(sFlat0,inverse(a)) = sFlat0,
inference(step,[status(thm)],[t1409,t19]) ).
cnf(t1417,plain,
add(sFlat0,inverse(a)) = sFlat0,
inference(orient,[status(thm)],[t4007]) ).
cnf(t4107,plain,
sFlat0 = add(sFlat0,multiply(d,b)),
inference(step,[status(thm)],[t2531,t1417]) ).
cnf(t1242,plain,
add(sFlat0,multiply(X1,b)) = multiply(add(sFlat0,X1),multiplicative_identity),
inference(cp,[status(thm)],[t51,t1239]) ).
cnf(t4023,plain,
add(sFlat0,multiply(X1,b)) = add(sFlat0,X1),
inference(step,[status(thm)],[t1242,t17]) ).
cnf(t1504,plain,
add(sFlat0,multiply(X1,b)) = add(sFlat0,X1),
inference(orient,[status(thm)],[t4023]) ).
cnf(t4108,plain,
sFlat0 = add(sFlat0,d),
inference(step,[status(thm)],[t4107,t1504]) ).
cnf(t2539,plain,
add(sFlat0,d) = sFlat0,
inference(orient,[status(thm)],[t4108]) ).
cnf(t2548,plain,
d = multiply(d,sFlat0),
inference(cp,[status(thm)],[t1245,t2539]) ).
cnf(t4109,plain,
d = multiply(sFlat0,d),
inference(step,[status(thm)],[t2548,t21]) ).
cnf(t2554,plain,
multiply(sFlat0,d) = d,
inference(orient,[status(thm)],[t4109]) ).
cnf(t4207,plain,
d = multiply(sFlat0,multiplicative_identity),
inference(step,[status(thm)],[t3782,t2554]) ).
cnf(t4208,plain,
d = sFlat0,
inference(step,[status(thm)],[t4207,t17]) ).
cnf(t3787,plain,
d = sFlat0,
inference(orient,[status(thm)],[t4208]) ).
cnf(goal_0,negated_conjecture,
inverse(c) != d,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
sFlat0 != d,
inference(rw,[status(thm)],[goal_0,t87]) ).
cnf(g0_1,plain,
sFlat0 != sFlat0,
inference(rw,[status(thm)],[g0_0,t3787]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : BOO015-2 : TPTP v9.3.1. Bugfixed v1.0.1.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n003.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Fri Sep 25 06:34:38 UTC 2026
% 0.14/0.36 % CPUTime :
% 0.14/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 8.32/1.73 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 8.32/1.73 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------