%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : NUN133-1 : TPTP v9.3.1. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n026.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 02:29:37 PM UTC 2026
% Result : Unsatisfiable 40.26s 5.66s
% Output : CNFRefutation 40.26s
% Verified :
% SZS Type : Refutation
% Derivation depth : 57
% Number of leaves : 18
% Syntax : Number of clauses : 191 ( 191 unt; 0 nHn; 95 RR)
% Number of literals : 191 ( 190 equ; 26 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 6 con; 0-2 aty)
% Number of variables : 161 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t19,axiom,
sFlat2 = times(sum(s(a)),sum(s(a))),
introduced(definition) ).
cnf(t50,plain,
times(sum(s(a)),sum(s(a))) = sFlat2,
inference(orient,[status(thm)],[t19]) ).
cnf(t17,axiom,
sFlat0 = s(a),
introduced(definition) ).
cnf(t93,plain,
s(a) = sFlat0,
inference(orient,[status(thm)],[t17]) ).
cnf(t99022,plain,
times(sum(sFlat0),sum(s(a))) = sFlat2,
inference(step,[status(thm)],[t50,t93]) ).
cnf(t99023,plain,
times(sum(sFlat0),sum(sFlat0)) = sFlat2,
inference(step,[status(thm)],[t99022,t93]) ).
cnf(t98,plain,
times(sum(sFlat0),sum(sFlat0)) = sFlat2,
inference(rw,[status(thm)],[t99023]) ).
cnf(t18,axiom,
sFlat1 = sum(s(a)),
introduced(definition) ).
cnf(t99024,plain,
sFlat1 = sum(sFlat0),
inference(step,[status(thm)],[t18,t93]) ).
cnf(t99,plain,
sum(sFlat0) = sFlat1,
inference(orient,[status(thm)],[t99024]) ).
cnf(t99044,plain,
times(sFlat1,sum(sFlat0)) = sFlat2,
inference(step,[status(thm)],[t98,t99]) ).
cnf(t99045,plain,
times(sFlat1,sFlat1) = sFlat2,
inference(step,[status(thm)],[t99044,t99]) ).
cnf(t161,plain,
times(sFlat1,sFlat1) = sFlat2,
inference(orient,[status(thm)],[t99045]) ).
cnf(t8,axiom,
qtd0(s(X1),sum(X1)) = sum(s(X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t5,axiom,
qtd0(X1,X2) = qtd0(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t64,plain,
qtd0(X1,X2) = qtd0(X2,X1),
inference(orient,[status(thm)],[t5]) ).
cnf(t99021,plain,
qtd0(sum(X1),s(X1)) = sum(s(X1)),
inference(step,[status(thm)],[t8,t64]) ).
cnf(t89,plain,
qtd0(sum(X1),s(X1)) = sum(s(X1)),
inference(orient,[status(thm)],[t99021]) ).
cnf(t94,plain,
sum(s(a)) = qtd0(sum(a),sFlat0),
inference(cp,[status(thm)],[t89,t93]) ).
cnf(t99040,plain,
sum(sFlat0) = qtd0(sum(a),sFlat0),
inference(step,[status(thm)],[t94,t93]) ).
cnf(t99041,plain,
sFlat1 = qtd0(sum(a),sFlat0),
inference(step,[status(thm)],[t99040,t99]) ).
cnf(t99042,plain,
sFlat1 = qtd0(sFlat0,sum(a)),
inference(step,[status(thm)],[t99041,t64]) ).
cnf(t141,plain,
qtd0(sFlat0,sum(a)) = sFlat1,
inference(orient,[status(thm)],[t99042]) ).
cnf(t20,axiom,
sFlat3 = cubes(s(a)),
introduced(definition) ).
cnf(t99025,plain,
sFlat3 = cubes(sFlat0),
inference(step,[status(thm)],[t20,t93]) ).
cnf(t109,plain,
cubes(sFlat0) = sFlat3,
inference(orient,[status(thm)],[t99025]) ).
cnf(t16,axiom,
qtd0(times(s(X1),times(s(X1),s(X1))),cubes(X1)) = cubes(s(X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t99020,plain,
qtd0(cubes(X1),times(s(X1),times(s(X1),s(X1)))) = cubes(s(X1)),
inference(step,[status(thm)],[t16,t64]) ).
cnf(t77,plain,
qtd0(cubes(X1),times(s(X1),times(s(X1),s(X1)))) = cubes(s(X1)),
inference(orient,[status(thm)],[t99020]) ).
cnf(t95,plain,
cubes(s(a)) = qtd0(cubes(a),times(sFlat0,times(s(a),s(a)))),
inference(cp,[status(thm)],[t77,t93]) ).
cnf(t99144,plain,
cubes(sFlat0) = qtd0(cubes(a),times(sFlat0,times(s(a),s(a)))),
inference(step,[status(thm)],[t95,t93]) ).
cnf(t99145,plain,
sFlat3 = qtd0(cubes(a),times(sFlat0,times(s(a),s(a)))),
inference(step,[status(thm)],[t99144,t109]) ).
cnf(t99146,plain,
sFlat3 = qtd0(cubes(a),times(sFlat0,times(sFlat0,s(a)))),
inference(step,[status(thm)],[t99145,t93]) ).
cnf(t99147,plain,
sFlat3 = qtd0(cubes(a),times(sFlat0,times(sFlat0,sFlat0))),
inference(step,[status(thm)],[t99146,t93]) ).
cnf(t1250,plain,
qtd0(cubes(a),times(sFlat0,times(sFlat0,sFlat0))) = sFlat3,
inference(orient,[status(thm)],[t99147]) ).
cnf(t12,axiom,
qtd0(qtd0(X1,X2),X3) = qtd0(X1,qtd0(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t68,plain,
qtd0(qtd0(X1,X2),X3) = qtd0(X1,qtd0(X2,X3)),
inference(orient,[status(thm)],[t12]) ).
cnf(t143,plain,
qtd0(sFlat0,qtd0(sum(a),X1)) = qtd0(sFlat1,X1),
inference(cp,[status(thm)],[t68,t141]) ).
cnf(t442,plain,
qtd0(sFlat0,qtd0(sum(a),X1)) = qtd0(sFlat1,X1),
inference(orient,[status(thm)],[t143]) ).
cnf(t10,axiom,
qtd0(X1,times(X2,X1)) = times(s(X2),X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t45,plain,
qtd0(X1,times(X2,X1)) = times(s(X2),X1),
inference(orient,[status(thm)],[t10]) ).
cnf(t6,axiom,
times(X1,X2) = times(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t23,plain,
times(X1,X2) = times(X2,X1),
inference(orient,[status(thm)],[t6]) ).
cnf(t3,axiom,
times(X1,one) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t21,plain,
times(X1,one) = X1,
inference(orient,[status(thm)],[t3]) ).
cnf(t24,plain,
times(one,X1) = X1,
inference(cp,[status(thm)],[t23,t21]) ).
cnf(t111,plain,
times(one,X1) = X1,
inference(orient,[status(thm)],[t24]) ).
cnf(t112,plain,
times(s(one),X1) = qtd0(X1,X1),
inference(cp,[status(thm)],[t45,t111]) ).
cnf(t250,plain,
times(s(one),X1) = qtd0(X1,X1),
inference(orient,[status(thm)],[t112]) ).
cnf(t452,plain,
qtd0(sFlat1,sum(a)) = qtd0(sFlat0,times(s(one),sum(a))),
inference(cp,[status(thm)],[t442,t250]) ).
cnf(t11,axiom,
qtd0(sum(X1),sum(X1)) = times(X1,s(X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t34,plain,
qtd0(sum(X1),sum(X1)) = times(X1,s(X1)),
inference(orient,[status(thm)],[t11]) ).
cnf(t269,plain,
qtd0(sum(X1),sum(X1)) = times(X1,s(X1)),
inference(rw,[status(thm)],[t34]) ).
cnf(t99057,plain,
times(s(one),sum(X1)) = times(X1,s(X1)),
inference(step,[status(thm)],[t269,t250]) ).
cnf(t343,plain,
times(s(one),sum(X1)) = times(X1,s(X1)),
inference(orient,[status(thm)],[t99057]) ).
cnf(t99136,plain,
qtd0(sFlat1,sum(a)) = qtd0(sFlat0,times(a,s(a))),
inference(step,[status(thm)],[t452,t343]) ).
cnf(t99137,plain,
qtd0(sFlat1,sum(a)) = qtd0(sFlat0,times(a,sFlat0)),
inference(step,[status(thm)],[t99136,t93]) ).
cnf(t99138,plain,
qtd0(sFlat1,sum(a)) = qtd0(sFlat0,times(sFlat0,a)),
inference(step,[status(thm)],[t99137,t23]) ).
cnf(t49,plain,
times(s(X1),X2) = qtd0(X2,times(X2,X1)),
inference(cp,[status(thm)],[t45,t23]) ).
cnf(t214,plain,
qtd0(X1,times(X1,X2)) = times(s(X2),X1),
inference(orient,[status(thm)],[t49]) ).
cnf(t99139,plain,
qtd0(sFlat1,sum(a)) = times(s(a),sFlat0),
inference(step,[status(thm)],[t99138,t214]) ).
cnf(t99140,plain,
qtd0(sFlat1,sum(a)) = times(sFlat0,s(a)),
inference(step,[status(thm)],[t99139,t23]) ).
cnf(t99141,plain,
qtd0(sFlat1,sum(a)) = times(sFlat0,sFlat0),
inference(step,[status(thm)],[t99140,t93]) ).
cnf(t1162,plain,
qtd0(sFlat1,sum(a)) = times(sFlat0,sFlat0),
inference(orient,[status(thm)],[t99141]) ).
cnf(t1166,plain,
qtd0(sFlat1,qtd0(sum(a),X1)) = qtd0(times(sFlat0,sFlat0),X1),
inference(cp,[status(thm)],[t68,t1162]) ).
cnf(t1175,plain,
qtd0(sFlat1,qtd0(sum(a),X1)) = qtd0(times(sFlat0,sFlat0),X1),
inference(orient,[status(thm)],[t1166]) ).
cnf(t1189,plain,
qtd0(times(sFlat0,sFlat0),times(sum(a),X1)) = qtd0(sFlat1,times(s(X1),sum(a))),
inference(cp,[status(thm)],[t1175,t214]) ).
cnf(t99742,plain,
qtd0(times(sFlat0,sFlat0),times(sum(a),X1)) = qtd0(sFlat1,times(sum(a),s(X1))),
inference(step,[status(thm)],[t1189,t23]) ).
cnf(t28348,plain,
qtd0(times(sFlat0,sFlat0),times(sum(a),X1)) = qtd0(sFlat1,times(sum(a),s(X1))),
inference(orient,[status(thm)],[t99742]) ).
cnf(t14,axiom,
qtd0(times(X1,X2),times(X1,X3)) = times(X1,qtd0(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t29,plain,
qtd0(times(X1,X2),times(X1,X3)) = times(X1,qtd0(X2,X3)),
inference(orient,[status(thm)],[t14]) ).
cnf(t33,plain,
times(X1,qtd0(X2,X3)) = qtd0(times(X1,X2),times(X3,X1)),
inference(cp,[status(thm)],[t29,t23]) ).
cnf(t1514,plain,
qtd0(times(X1,X2),times(X3,X1)) = times(X1,qtd0(X2,X3)),
inference(orient,[status(thm)],[t33]) ).
cnf(t15,axiom,
qtd0(times(X1,X2),times(X3,X2)) = times(qtd0(X1,X3),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t39,plain,
qtd0(times(X1,X2),times(X3,X2)) = times(qtd0(X1,X3),X2),
inference(orient,[status(thm)],[t15]) ).
cnf(t349,plain,
times(qtd0(s(one),X1),sum(X2)) = qtd0(times(X2,s(X2)),times(X1,sum(X2))),
inference(cp,[status(thm)],[t39,t343]) ).
cnf(t9,axiom,
s(qtd0(X1,X2)) = qtd0(s(X1),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t79,plain,
s(qtd0(X1,X2)) = qtd0(s(X1),X2),
inference(orient,[status(thm)],[t9]) ).
cnf(t47,plain,
times(s(X1),one) = qtd0(one,X1),
inference(cp,[status(thm)],[t45,t21]) ).
cnf(t99026,plain,
s(X1) = qtd0(one,X1),
inference(step,[status(thm)],[t47,t21]) ).
cnf(t120,plain,
qtd0(one,X1) = s(X1),
inference(orient,[status(thm)],[t99026]) ).
cnf(t123,plain,
qtd0(s(one),X1) = s(s(X1)),
inference(cp,[status(thm)],[t79,t120]) ).
cnf(t154,plain,
qtd0(s(one),X1) = s(s(X1)),
inference(orient,[status(thm)],[t123]) ).
cnf(t100682,plain,
times(s(s(X1)),sum(X2)) = qtd0(times(X2,s(X2)),times(X1,sum(X2))),
inference(step,[status(thm)],[t349,t154]) ).
cnf(t90347,plain,
qtd0(times(X1,s(X1)),times(X2,sum(X1))) = times(s(s(X2)),sum(X1)),
inference(orient,[status(thm)],[t100682]) ).
cnf(t90349,plain,
times(s(s(X1)),sum(X1)) = times(X1,qtd0(s(X1),sum(X1))),
inference(cp,[status(thm)],[t90347,t29]) ).
cnf(t100683,plain,
times(sum(X1),s(s(X1))) = times(X1,qtd0(s(X1),sum(X1))),
inference(step,[status(thm)],[t90349,t23]) ).
cnf(t122,plain,
s(X1) = qtd0(X1,one),
inference(cp,[status(thm)],[t120,t64]) ).
cnf(t133,plain,
qtd0(X1,one) = s(X1),
inference(orient,[status(thm)],[t122]) ).
cnf(t134,plain,
s(qtd0(X1,X2)) = qtd0(X1,qtd0(X2,one)),
inference(cp,[status(thm)],[t133,t68]) ).
cnf(t99047,plain,
qtd0(s(X1),X2) = qtd0(X1,qtd0(X2,one)),
inference(step,[status(thm)],[t134,t79]) ).
cnf(t99048,plain,
qtd0(s(X1),X2) = qtd0(X1,s(X2)),
inference(step,[status(thm)],[t99047,t133]) ).
cnf(t175,plain,
qtd0(s(X1),X2) = qtd0(X1,s(X2)),
inference(orient,[status(thm)],[t99048]) ).
cnf(t100684,plain,
times(sum(X1),s(s(X1))) = times(X1,qtd0(X1,s(sum(X1)))),
inference(step,[status(thm)],[t100683,t175]) ).
cnf(t521,plain,
qtd0(sum(X1),s(X1)) = sum(s(X1)),
inference(rw,[status(thm)],[t89]) ).
cnf(t85,plain,
qtd0(s(X1),X2) = s(qtd0(X2,X1)),
inference(cp,[status(thm)],[t79,t64]) ).
cnf(t99080,plain,
qtd0(X1,s(X2)) = s(qtd0(X2,X1)),
inference(step,[status(thm)],[t85,t175]) ).
cnf(t99049,plain,
s(qtd0(X1,X2)) = qtd0(X1,s(X2)),
inference(step,[status(thm)],[t79,t175]) ).
cnf(t176,plain,
s(qtd0(X1,X2)) = qtd0(X1,s(X2)),
inference(orient,[status(thm)],[t99049]) ).
cnf(t99081,plain,
qtd0(X1,s(X2)) = qtd0(X2,s(X1)),
inference(step,[status(thm)],[t99080,t176]) ).
cnf(t506,plain,
qtd0(X1,s(X2)) = qtd0(X2,s(X1)),
inference(orient,[status(thm)],[t99081]) ).
cnf(t99082,plain,
qtd0(X1,s(sum(X1))) = sum(s(X1)),
inference(step,[status(thm)],[t521,t506]) ).
cnf(t522,plain,
qtd0(X1,s(sum(X1))) = sum(s(X1)),
inference(orient,[status(thm)],[t99082]) ).
cnf(t100685,plain,
times(sum(X1),s(s(X1))) = times(X1,sum(s(X1))),
inference(step,[status(thm)],[t100684,t522]) ).
cnf(t90526,plain,
times(sum(X1),s(s(X1))) = times(X1,sum(s(X1))),
inference(orient,[status(thm)],[t100685]) ).
cnf(t90643,plain,
times(a,sum(s(a))) = times(sum(a),s(sFlat0)),
inference(cp,[status(thm)],[t90526,t93]) ).
cnf(t100686,plain,
times(a,sum(sFlat0)) = times(sum(a),s(sFlat0)),
inference(step,[status(thm)],[t90643,t93]) ).
cnf(t100687,plain,
times(a,sFlat1) = times(sum(a),s(sFlat0)),
inference(step,[status(thm)],[t100686,t99]) ).
cnf(t100688,plain,
times(sFlat1,a) = times(sum(a),s(sFlat0)),
inference(step,[status(thm)],[t100687,t23]) ).
cnf(t90727,plain,
times(sum(a),s(sFlat0)) = times(sFlat1,a),
inference(orient,[status(thm)],[t100688]) ).
cnf(t90729,plain,
times(sum(a),qtd0(s(sFlat0),X1)) = qtd0(times(sFlat1,a),times(X1,sum(a))),
inference(cp,[status(thm)],[t1514,t90727]) ).
cnf(t100825,plain,
times(sum(a),qtd0(sFlat0,s(X1))) = qtd0(times(sFlat1,a),times(X1,sum(a))),
inference(step,[status(thm)],[t90729,t175]) ).
cnf(t93901,plain,
qtd0(times(sFlat1,a),times(X1,sum(a))) = times(sum(a),qtd0(sFlat0,s(X1))),
inference(orient,[status(thm)],[t100825]) ).
cnf(t31,plain,
times(X1,qtd0(X2,X3)) = qtd0(times(X2,X1),times(X1,X3)),
inference(cp,[status(thm)],[t29,t23]) ).
cnf(t1437,plain,
qtd0(times(X1,X2),times(X2,X3)) = times(X2,qtd0(X1,X3)),
inference(orient,[status(thm)],[t31]) ).
cnf(t93903,plain,
times(sum(a),qtd0(sFlat0,s(a))) = times(a,qtd0(sFlat1,sum(a))),
inference(cp,[status(thm)],[t93901,t1437]) ).
cnf(t100826,plain,
times(sum(a),qtd0(sFlat0,sFlat0)) = times(a,qtd0(sFlat1,sum(a))),
inference(step,[status(thm)],[t93903,t93]) ).
cnf(t100827,plain,
times(sum(a),qtd0(sFlat0,sFlat0)) = times(a,times(sFlat0,sFlat0)),
inference(step,[status(thm)],[t100826,t1162]) ).
cnf(t13,axiom,
times(times(X1,X2),X3) = times(X1,times(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t25,plain,
times(times(X1,X2),X3) = times(X1,times(X2,X3)),
inference(orient,[status(thm)],[t13]) ).
cnf(t26,plain,
times(X1,times(X2,X3)) = times(X3,times(X1,X2)),
inference(cp,[status(thm)],[t25,t23]) ).
cnf(t288,plain,
times(X1,times(X2,X3)) = times(X3,times(X1,X2)),
inference(orient,[status(thm)],[t26]) ).
cnf(t319,plain,
times(X1,times(X2,X3)) = times(X3,times(X2,X1)),
inference(cp,[status(thm)],[t288,t23]) ).
cnf(t10395,plain,
times(X1,times(X2,X3)) = times(X3,times(X2,X1)),
inference(orient,[status(thm)],[t319]) ).
cnf(t100828,plain,
times(sum(a),qtd0(sFlat0,sFlat0)) = times(sFlat0,times(sFlat0,a)),
inference(step,[status(thm)],[t100827,t10395]) ).
cnf(t93957,plain,
times(sum(a),qtd0(sFlat0,sFlat0)) = times(sFlat0,times(sFlat0,a)),
inference(orient,[status(thm)],[t100828]) ).
cnf(t93978,plain,
qtd0(sFlat1,times(sum(a),s(qtd0(sFlat0,sFlat0)))) = qtd0(times(sFlat0,sFlat0),times(sFlat0,times(sFlat0,a))),
inference(cp,[status(thm)],[t28348,t93957]) ).
cnf(t100916,plain,
qtd0(sFlat1,times(sum(a),qtd0(sFlat0,s(sFlat0)))) = qtd0(times(sFlat0,sFlat0),times(sFlat0,times(sFlat0,a))),
inference(step,[status(thm)],[t93978,t176]) ).
cnf(t313,plain,
times(X1,qtd0(X2,times(X3,Y3))) = qtd0(times(X1,X2),times(Y3,times(X1,X3))),
inference(cp,[status(thm)],[t29,t288]) ).
cnf(t94275,plain,
qtd0(times(X1,X2),times(X3,times(X1,Y3))) = times(X1,qtd0(X2,times(Y3,X3))),
inference(orient,[status(thm)],[t313]) ).
cnf(t100917,plain,
qtd0(sFlat1,times(sum(a),qtd0(sFlat0,s(sFlat0)))) = times(sFlat0,qtd0(sFlat0,times(a,sFlat0))),
inference(step,[status(thm)],[t100916,t94275]) ).
cnf(t100918,plain,
qtd0(sFlat1,times(sum(a),qtd0(sFlat0,s(sFlat0)))) = times(sFlat0,times(s(a),sFlat0)),
inference(step,[status(thm)],[t100917,t45]) ).
cnf(t100919,plain,
qtd0(sFlat1,times(sum(a),qtd0(sFlat0,s(sFlat0)))) = times(sFlat0,times(sFlat0,s(a))),
inference(step,[status(thm)],[t100918,t23]) ).
cnf(t100920,plain,
qtd0(sFlat1,times(sum(a),qtd0(sFlat0,s(sFlat0)))) = times(sFlat0,times(sFlat0,sFlat0)),
inference(step,[status(thm)],[t100919,t93]) ).
cnf(t98992,plain,
qtd0(sFlat1,times(sum(a),qtd0(sFlat0,s(sFlat0)))) = times(sFlat0,times(sFlat0,sFlat0)),
inference(orient,[status(thm)],[t100920]) ).
cnf(t70,plain,
qtd0(X1,qtd0(X2,X3)) = qtd0(X3,qtd0(X1,X2)),
inference(cp,[status(thm)],[t68,t64]) ).
cnf(t8882,plain,
qtd0(X1,qtd0(X2,X3)) = qtd0(X3,qtd0(X1,X2)),
inference(orient,[status(thm)],[t70]) ).
cnf(t7,axiom,
times(sum(a),sum(a)) = cubes(a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t57,plain,
times(sum(a),sum(a)) = cubes(a),
inference(orient,[status(thm)],[t7]) ).
cnf(t62,plain,
times(sum(a),qtd0(sum(a),X1)) = qtd0(cubes(a),times(sum(a),X1)),
inference(cp,[status(thm)],[t29,t57]) ).
cnf(t5564,plain,
qtd0(cubes(a),times(sum(a),X1)) = times(sum(a),qtd0(sum(a),X1)),
inference(orient,[status(thm)],[t62]) ).
cnf(t142,plain,
qtd0(s(sFlat0),sum(a)) = s(sFlat1),
inference(cp,[status(thm)],[t79,t141]) ).
cnf(t99051,plain,
qtd0(sFlat0,s(sum(a))) = s(sFlat1),
inference(step,[status(thm)],[t142,t175]) ).
cnf(t188,plain,
qtd0(sFlat0,s(sum(a))) = s(sFlat1),
inference(orient,[status(thm)],[t99051]) ).
cnf(t9066,plain,
qtd0(s(sum(a)),qtd0(X1,sFlat0)) = qtd0(X1,s(sFlat1)),
inference(cp,[status(thm)],[t8882,t188]) ).
cnf(t99450,plain,
qtd0(sum(a),s(qtd0(X1,sFlat0))) = qtd0(X1,s(sFlat1)),
inference(step,[status(thm)],[t9066,t175]) ).
cnf(t99451,plain,
qtd0(sum(a),qtd0(X1,s(sFlat0))) = qtd0(X1,s(sFlat1)),
inference(step,[status(thm)],[t99450,t176]) ).
cnf(t9437,plain,
qtd0(sum(a),qtd0(X1,s(sFlat0))) = qtd0(X1,s(sFlat1)),
inference(orient,[status(thm)],[t99451]) ).
cnf(t91,plain,
qtd0(s(sum(X1)),s(X1)) = s(sum(s(X1))),
inference(cp,[status(thm)],[t79,t89]) ).
cnf(t99068,plain,
qtd0(sum(X1),s(s(X1))) = s(sum(s(X1))),
inference(step,[status(thm)],[t91,t175]) ).
cnf(t464,plain,
qtd0(sum(X1),s(s(X1))) = s(sum(s(X1))),
inference(orient,[status(thm)],[t99068]) ).
cnf(t471,plain,
qtd0(sFlat1,s(s(a))) = qtd0(sFlat0,s(sum(s(a)))),
inference(cp,[status(thm)],[t442,t464]) ).
cnf(t99069,plain,
qtd0(sFlat1,s(sFlat0)) = qtd0(sFlat0,s(sum(s(a)))),
inference(step,[status(thm)],[t471,t93]) ).
cnf(t100,plain,
sum(s(sFlat0)) = qtd0(sFlat1,s(sFlat0)),
inference(cp,[status(thm)],[t89,t99]) ).
cnf(t144,plain,
qtd0(sFlat1,s(sFlat0)) = sum(s(sFlat0)),
inference(orient,[status(thm)],[t100]) ).
cnf(t99070,plain,
sum(s(sFlat0)) = qtd0(sFlat0,s(sum(s(a)))),
inference(step,[status(thm)],[t99069,t144]) ).
cnf(t99071,plain,
sum(s(sFlat0)) = qtd0(sFlat0,s(sum(sFlat0))),
inference(step,[status(thm)],[t99070,t93]) ).
cnf(t99072,plain,
sum(s(sFlat0)) = qtd0(sFlat0,s(sFlat1)),
inference(step,[status(thm)],[t99071,t99]) ).
cnf(t472,plain,
qtd0(sFlat0,s(sFlat1)) = sum(s(sFlat0)),
inference(orient,[status(thm)],[t99072]) ).
cnf(t93904,plain,
times(sum(a),qtd0(sFlat0,s(sFlat1))) = times(sFlat1,qtd0(a,sum(a))),
inference(cp,[status(thm)],[t93901,t29]) ).
cnf(t100830,plain,
times(sum(a),sum(s(sFlat0))) = times(sFlat1,qtd0(a,sum(a))),
inference(step,[status(thm)],[t93904,t472]) ).
cnf(t94025,plain,
times(sum(a),sum(s(sFlat0))) = times(sFlat1,qtd0(a,sum(a))),
inference(orient,[status(thm)],[t100830]) ).
cnf(t182,plain,
qtd0(a,s(X1)) = qtd0(sFlat0,X1),
inference(cp,[status(thm)],[t175,t93]) ).
cnf(t183,plain,
qtd0(a,s(X1)) = qtd0(sFlat0,X1),
inference(orient,[status(thm)],[t182]) ).
cnf(goal_0,negated_conjecture,
times(sum(s(a)),sum(s(a))) != cubes(s(a)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
times(sum(s(a)),sum(s(a))) != sFlat2,
inference(rw,[status(thm)],[goal_0]) ).
cnf(g0_1,plain,
times(sum(s(a)),sum(s(a))) != times(sFlat1,sFlat1),
inference(rw,[status(thm)],[g0_0,t161]) ).
cnf(g0_2,plain,
times(sum(s(a)),sum(s(a))) != times(sFlat1,qtd0(sFlat0,sum(a))),
inference(rw,[status(thm)],[g0_1,t141]) ).
cnf(g0_3,plain,
cubes(sFlat0) != times(sFlat1,qtd0(sFlat0,sum(a))),
inference(rw,[status(thm)],[g0_2,t93]) ).
cnf(g0_4,plain,
sFlat3 != times(sFlat1,qtd0(sFlat0,sum(a))),
inference(rw,[status(thm)],[g0_3,t109]) ).
cnf(g0_5,plain,
qtd0(cubes(a),times(sFlat0,times(sFlat0,sFlat0))) != times(sFlat1,qtd0(sFlat0,sum(a))),
inference(rw,[status(thm)],[g0_4,t1250]) ).
cnf(g0_6,plain,
qtd0(times(sFlat0,times(sFlat0,sFlat0)),cubes(a)) != times(sFlat1,qtd0(sFlat0,sum(a))),
inference(rw,[status(thm)],[g0_5,t64]) ).
cnf(g0_7,plain,
qtd0(qtd0(sFlat1,times(sum(a),qtd0(sFlat0,s(sFlat0)))),cubes(a)) != times(sFlat1,qtd0(sFlat0,sum(a))),
inference(rw,[status(thm)],[g0_6,t98992]) ).
cnf(g0_8,plain,
qtd0(qtd0(sFlat1,times(sum(a),qtd0(s(sFlat0),sFlat0))),cubes(a)) != times(sFlat1,qtd0(sFlat0,sum(a))),
inference(rw,[status(thm)],[g0_7,t64]) ).
cnf(g0_9,plain,
qtd0(qtd0(sFlat1,times(qtd0(s(sFlat0),sFlat0),sum(a))),cubes(a)) != times(sFlat1,qtd0(sFlat0,sum(a))),
inference(rw,[status(thm)],[g0_8,t23]) ).
cnf(g0_10,plain,
qtd0(qtd0(times(qtd0(s(sFlat0),sFlat0),sum(a)),sFlat1),cubes(a)) != times(sFlat1,qtd0(sFlat0,sum(a))),
inference(rw,[status(thm)],[g0_9,t64]) ).
cnf(g0_11,plain,
qtd0(cubes(a),qtd0(times(qtd0(s(sFlat0),sFlat0),sum(a)),sFlat1)) != times(sFlat1,qtd0(sFlat0,sum(a))),
inference(rw,[status(thm)],[g0_10,t64]) ).
cnf(g0_12,plain,
qtd0(cubes(a),qtd0(times(sum(a),qtd0(s(sFlat0),sFlat0)),sFlat1)) != times(sFlat1,qtd0(sFlat0,sum(a))),
inference(rw,[status(thm)],[g0_11,t23]) ).
cnf(g0_13,plain,
qtd0(times(sum(a),qtd0(s(sFlat0),sFlat0)),qtd0(sFlat1,cubes(a))) != times(sFlat1,qtd0(sFlat0,sum(a))),
inference(rw,[status(thm)],[g0_12,t8882]) ).
cnf(g0_14,plain,
qtd0(qtd0(sFlat1,cubes(a)),times(sum(a),qtd0(s(sFlat0),sFlat0))) != times(sFlat1,qtd0(sFlat0,sum(a))),
inference(rw,[status(thm)],[g0_13,t64]) ).
cnf(g0_15,plain,
qtd0(qtd0(sFlat1,cubes(a)),times(sum(a),qtd0(sFlat0,s(sFlat0)))) != times(sFlat1,qtd0(sFlat0,sum(a))),
inference(rw,[status(thm)],[g0_14,t64]) ).
cnf(g0_16,plain,
qtd0(sFlat1,qtd0(cubes(a),times(sum(a),qtd0(sFlat0,s(sFlat0))))) != times(sFlat1,qtd0(sFlat0,sum(a))),
inference(rw,[status(thm)],[g0_15,t68]) ).
cnf(g0_17,plain,
qtd0(sFlat1,times(sum(a),qtd0(sum(a),qtd0(sFlat0,s(sFlat0))))) != times(sFlat1,qtd0(sFlat0,sum(a))),
inference(rw,[status(thm)],[g0_16,t5564]) ).
cnf(g0_18,plain,
qtd0(sFlat1,times(sum(a),qtd0(sFlat0,s(sFlat1)))) != times(sFlat1,qtd0(sFlat0,sum(a))),
inference(rw,[status(thm)],[g0_17,t9437]) ).
cnf(g0_19,plain,
qtd0(sFlat1,times(sum(a),sum(s(sFlat0)))) != times(sFlat1,qtd0(sFlat0,sum(a))),
inference(rw,[status(thm)],[g0_18,t472]) ).
cnf(g0_20,plain,
qtd0(sFlat1,times(sFlat1,qtd0(a,sum(a)))) != times(sFlat1,qtd0(sFlat0,sum(a))),
inference(rw,[status(thm)],[g0_19,t94025]) ).
cnf(g0_21,plain,
times(s(qtd0(a,sum(a))),sFlat1) != times(sFlat1,qtd0(sFlat0,sum(a))),
inference(rw,[status(thm)],[g0_20,t214]) ).
cnf(g0_22,plain,
times(sFlat1,s(qtd0(a,sum(a)))) != times(sFlat1,qtd0(sFlat0,sum(a))),
inference(rw,[status(thm)],[g0_21,t23]) ).
cnf(g0_23,plain,
times(sFlat1,qtd0(a,s(sum(a)))) != times(sFlat1,qtd0(sFlat0,sum(a))),
inference(rw,[status(thm)],[g0_22,t176]) ).
cnf(g0_24,plain,
times(sFlat1,qtd0(sFlat0,sum(a))) != times(sFlat1,qtd0(sFlat0,sum(a))),
inference(rw,[status(thm)],[g0_23,t183]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_24]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUN133-1 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n026.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.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Thu Sep 24 06:07:23 UTC 2026
% 0.14/0.36 % CPUTime :
% 0.14/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 40.26/5.66 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 40.26/5.66 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------