%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP728-1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/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 01:28:18 PM UTC 2026
% Result : Unsatisfiable 4.56s 1.04s
% Output : CNFRefutation 4.56s
% Verified :
% SZS Type : Refutation
% Derivation depth : 44
% Number of leaves : 13
% Syntax : Number of clauses : 104 ( 104 unt; 0 nHn; 6 RR)
% Number of literals : 104 ( 103 equ; 3 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 5 con; 0-3 aty)
% Number of variables : 173 ( 38 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t19,axiom,
sFlat0 = op_k(a,b),
introduced(definition) ).
cnf(t494,plain,
op_k(a,b) = sFlat0,
inference(orient,[status(thm)],[t19]) ).
cnf(t6,axiom,
mult(i(X1),mult(X1,X2)) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t22,plain,
mult(i(X1),mult(X1,X2)) = X2,
inference(orient,[status(thm)],[t6]) ).
cnf(t3,axiom,
mult(i(X1),X1) = unit,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t76,plain,
mult(i(X1),X1) = unit,
inference(orient,[status(thm)],[t3]) ).
cnf(t78,plain,
X1 = mult(i(i(X1)),unit),
inference(cp,[status(thm)],[t22,t76]) ).
cnf(t0,axiom,
mult(X1,unit) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t21,plain,
mult(X1,unit) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t6566,plain,
X1 = i(i(X1)),
inference(step,[status(thm)],[t78,t21]) ).
cnf(t500,plain,
i(i(X1)) = X1,
inference(orient,[status(thm)],[t6566]) ).
cnf(t501,plain,
X1 = mult(X2,mult(i(X2),X1)),
inference(cp,[status(thm)],[t22,t500]) ).
cnf(t662,plain,
mult(X1,mult(i(X1),X2)) = X2,
inference(orient,[status(thm)],[t501]) ).
cnf(t9,axiom,
mult(i(X1),i(X2)) = i(mult(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t245,plain,
mult(i(X1),i(X2)) = i(mult(X1,X2)),
inference(orient,[status(thm)],[t9]) ).
cnf(t664,plain,
i(X1) = mult(X2,i(mult(X2,X1))),
inference(cp,[status(thm)],[t662,t245]) ).
cnf(t761,plain,
mult(X1,i(mult(X1,X2))) = i(X2),
inference(orient,[status(thm)],[t664]) ).
cnf(t10,axiom,
mult(mult(X1,X2),op_k(X2,X1)) = mult(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t34,plain,
mult(mult(X1,X2),op_k(X2,X1)) = mult(X2,X1),
inference(orient,[status(thm)],[t10]) ).
cnf(t765,plain,
i(op_k(X1,X2)) = mult(mult(X2,X1),i(mult(X1,X2))),
inference(cp,[status(thm)],[t761,t34]) ).
cnf(t3698,plain,
mult(mult(X1,X2),i(mult(X2,X1))) = i(op_k(X2,X1)),
inference(orient,[status(thm)],[t765]) ).
cnf(t5,axiom,
rd(mult(X1,X2),X2) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t30,plain,
rd(mult(X1,X2),X2) = X1,
inference(orient,[status(thm)],[t5]) ).
cnf(t41,plain,
mult(X1,X2) = rd(mult(X2,X1),op_k(X2,X1)),
inference(cp,[status(thm)],[t30,t34]) ).
cnf(t1083,plain,
rd(mult(X1,X2),op_k(X1,X2)) = mult(X2,X1),
inference(orient,[status(thm)],[t41]) ).
cnf(t4,axiom,
mult(rd(X1,X2),X2) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t25,plain,
mult(rd(X1,X2),X2) = X1,
inference(orient,[status(thm)],[t4]) ).
cnf(t1094,plain,
mult(X1,rd(X2,X1)) = rd(X2,op_k(rd(X2,X1),X1)),
inference(cp,[status(thm)],[t1083,t25]) ).
cnf(t1715,plain,
rd(X1,op_k(rd(X1,X2),X2)) = mult(X2,rd(X1,X2)),
inference(orient,[status(thm)],[t1094]) ).
cnf(t12,axiom,
mult(mult(X1,mult(X2,X3)),asoc(X1,X2,X3)) = mult(mult(X1,X2),X3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t58,plain,
mult(mult(X1,mult(X2,X3)),asoc(X1,X2,X3)) = mult(mult(X1,X2),X3),
inference(orient,[status(thm)],[t12]) ).
cnf(t71,plain,
asoc(X1,X2,X3) = mult(i(mult(X1,mult(X2,X3))),mult(mult(X1,X2),X3)),
inference(cp,[status(thm)],[t22,t58]) ).
cnf(t5668,plain,
mult(i(mult(X1,mult(X2,X3))),mult(mult(X1,X2),X3)) = asoc(X1,X2,X3),
inference(orient,[status(thm)],[t71]) ).
cnf(t5739,plain,
asoc(X1,X2,i(mult(X2,X1))) = mult(i(mult(X1,mult(X2,i(mult(X2,X1))))),i(op_k(X2,X1))),
inference(cp,[status(thm)],[t5668,t3698]) ).
cnf(t6638,plain,
asoc(X1,X2,i(mult(X2,X1))) = i(mult(mult(X1,mult(X2,i(mult(X2,X1)))),op_k(X2,X1))),
inference(step,[status(thm)],[t5739,t245]) ).
cnf(t6639,plain,
asoc(X1,X2,i(mult(X2,X1))) = i(mult(mult(X1,i(X1)),op_k(X2,X1))),
inference(step,[status(thm)],[t6638,t761]) ).
cnf(t2,axiom,
mult(X1,i(X1)) = unit,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t53,plain,
mult(X1,i(X1)) = unit,
inference(orient,[status(thm)],[t2]) ).
cnf(t6640,plain,
asoc(X1,X2,i(mult(X2,X1))) = i(mult(unit,op_k(X2,X1))),
inference(step,[status(thm)],[t6639,t53]) ).
cnf(t1,axiom,
mult(unit,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t28,plain,
mult(unit,X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t6641,plain,
asoc(X1,X2,i(mult(X2,X1))) = i(op_k(X2,X1)),
inference(step,[status(thm)],[t6640,t28]) ).
cnf(t5964,plain,
asoc(X1,X2,i(mult(X2,X1))) = i(op_k(X2,X1)),
inference(orient,[status(thm)],[t6641]) ).
cnf(t8,axiom,
asoc(asoc(X1,X2,X3),X4,X5) = unit,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t487,plain,
asoc(asoc(X1,X2,X3),X4,X5) = unit,
inference(orient,[status(thm)],[t8]) ).
cnf(t5965,plain,
i(op_k(X1,asoc(X2,X3,X4))) = unit,
inference(cp,[status(thm)],[t5964,t487]) ).
cnf(t6009,plain,
i(op_k(X1,asoc(X2,X3,X4))) = unit,
inference(orient,[status(thm)],[t5965]) ).
cnf(t6015,plain,
unit = i(op_k(X1,i(op_k(X2,X3)))),
inference(cp,[status(thm)],[t6009,t5964]) ).
cnf(t39,plain,
op_k(X1,X2) = mult(i(mult(X2,X1)),mult(X1,X2)),
inference(cp,[status(thm)],[t22,t34]) ).
cnf(t1791,plain,
mult(i(mult(X1,X2)),mult(X2,X1)) = op_k(X2,X1),
inference(orient,[status(thm)],[t39]) ).
cnf(t1833,plain,
op_k(i(X1),i(X2)) = mult(i(mult(i(X2),i(X1))),i(mult(X1,X2))),
inference(cp,[status(thm)],[t1791,t245]) ).
cnf(t6601,plain,
op_k(i(X1),i(X2)) = i(mult(mult(i(X2),i(X1)),mult(X1,X2))),
inference(step,[status(thm)],[t1833,t245]) ).
cnf(t6602,plain,
op_k(i(X1),i(X2)) = i(mult(i(mult(X2,X1)),mult(X1,X2))),
inference(step,[status(thm)],[t6601,t245]) ).
cnf(t6603,plain,
op_k(i(X1),i(X2)) = i(op_k(X1,X2)),
inference(step,[status(thm)],[t6602,t1791]) ).
cnf(t1874,plain,
op_k(i(X1),i(X2)) = i(op_k(X1,X2)),
inference(orient,[status(thm)],[t6603]) ).
cnf(t1888,plain,
i(op_k(X1,i(X2))) = op_k(i(X1),X2),
inference(cp,[status(thm)],[t1874,t500]) ).
cnf(t1937,plain,
i(op_k(X1,i(X2))) = op_k(i(X1),X2),
inference(orient,[status(thm)],[t1888]) ).
cnf(t6642,plain,
unit = op_k(i(X1),op_k(X2,X3)),
inference(step,[status(thm)],[t6015,t1937]) ).
cnf(t6102,plain,
op_k(i(X1),op_k(X2,X3)) = unit,
inference(orient,[status(thm)],[t6642]) ).
cnf(t6128,plain,
unit = op_k(i(X1),sFlat0),
inference(cp,[status(thm)],[t6102,t494]) ).
cnf(t6139,plain,
op_k(i(X1),sFlat0) = unit,
inference(orient,[status(thm)],[t6128]) ).
cnf(t6159,plain,
unit = op_k(X1,sFlat0),
inference(cp,[status(thm)],[t6139,t500]) ).
cnf(t6169,plain,
op_k(X1,sFlat0) = unit,
inference(orient,[status(thm)],[t6159]) ).
cnf(t6180,plain,
mult(sFlat0,rd(X1,sFlat0)) = rd(X1,unit),
inference(cp,[status(thm)],[t1715,t6169]) ).
cnf(t26,plain,
X1 = rd(X1,unit),
inference(cp,[status(thm)],[t25,t21]) ).
cnf(t498,plain,
rd(X1,unit) = X1,
inference(orient,[status(thm)],[t26]) ).
cnf(t6647,plain,
mult(sFlat0,rd(X1,sFlat0)) = X1,
inference(step,[status(thm)],[t6180,t498]) ).
cnf(t6262,plain,
mult(sFlat0,rd(X1,sFlat0)) = X1,
inference(orient,[status(thm)],[t6647]) ).
cnf(t6269,plain,
rd(X1,sFlat0) = mult(i(sFlat0),X1),
inference(cp,[status(thm)],[t22,t6262]) ).
cnf(t6304,plain,
mult(i(sFlat0),X1) = rd(X1,sFlat0),
inference(orient,[status(thm)],[t6269]) ).
cnf(t6320,plain,
mult(X1,i(sFlat0)) = mult(rd(X1,sFlat0),op_k(X1,i(sFlat0))),
inference(cp,[status(thm)],[t34,t6304]) ).
cnf(t1881,plain,
i(op_k(i(X1),X2)) = op_k(X1,i(X2)),
inference(cp,[status(thm)],[t1874,t500]) ).
cnf(t1889,plain,
i(op_k(i(X1),X2)) = op_k(X1,i(X2)),
inference(orient,[status(thm)],[t1881]) ).
cnf(t1917,plain,
unit = mult(op_k(i(X1),X2),op_k(X1,i(X2))),
inference(cp,[status(thm)],[t53,t1889]) ).
cnf(t2783,plain,
mult(op_k(i(X1),X2),op_k(X1,i(X2))) = unit,
inference(orient,[status(thm)],[t1917]) ).
cnf(t6165,plain,
unit = mult(unit,op_k(X1,i(sFlat0))),
inference(cp,[status(thm)],[t2783,t6139]) ).
cnf(t6645,plain,
unit = op_k(X1,i(sFlat0)),
inference(step,[status(thm)],[t6165,t28]) ).
cnf(t6231,plain,
op_k(X1,i(sFlat0)) = unit,
inference(orient,[status(thm)],[t6645]) ).
cnf(t6649,plain,
mult(X1,i(sFlat0)) = mult(rd(X1,sFlat0),unit),
inference(step,[status(thm)],[t6320,t6231]) ).
cnf(t6650,plain,
mult(X1,i(sFlat0)) = rd(X1,sFlat0),
inference(step,[status(thm)],[t6649,t21]) ).
cnf(t6455,plain,
mult(X1,i(sFlat0)) = rd(X1,sFlat0),
inference(orient,[status(thm)],[t6650]) ).
cnf(t6474,plain,
i(op_k(i(sFlat0),X1)) = mult(rd(X1,sFlat0),i(mult(i(sFlat0),X1))),
inference(cp,[status(thm)],[t3698,t6455]) ).
cnf(t6651,plain,
op_k(sFlat0,i(X1)) = mult(rd(X1,sFlat0),i(mult(i(sFlat0),X1))),
inference(step,[status(thm)],[t6474,t1889]) ).
cnf(t502,plain,
i(mult(i(X1),X2)) = mult(X1,i(X2)),
inference(cp,[status(thm)],[t245,t500]) ).
cnf(t702,plain,
i(mult(i(X1),X2)) = mult(X1,i(X2)),
inference(orient,[status(thm)],[t502]) ).
cnf(t6652,plain,
op_k(sFlat0,i(X1)) = mult(rd(X1,sFlat0),mult(sFlat0,i(X1))),
inference(step,[status(thm)],[t6651,t702]) ).
cnf(t6284,plain,
i(rd(X1,sFlat0)) = mult(sFlat0,i(X1)),
inference(cp,[status(thm)],[t761,t6262]) ).
cnf(t33,plain,
i(X1) = rd(X2,mult(X1,X2)),
inference(cp,[status(thm)],[t30,t22]) ).
cnf(t580,plain,
rd(X1,mult(X2,X1)) = i(X2),
inference(orient,[status(thm)],[t33]) ).
cnf(t585,plain,
i(rd(X1,X2)) = rd(X2,X1),
inference(cp,[status(thm)],[t580,t25]) ).
cnf(t592,plain,
i(rd(X1,X2)) = rd(X2,X1),
inference(orient,[status(thm)],[t585]) ).
cnf(t6648,plain,
rd(sFlat0,X1) = mult(sFlat0,i(X1)),
inference(step,[status(thm)],[t6284,t592]) ).
cnf(t6395,plain,
mult(sFlat0,i(X1)) = rd(sFlat0,X1),
inference(orient,[status(thm)],[t6648]) ).
cnf(t6653,plain,
op_k(sFlat0,i(X1)) = mult(rd(X1,sFlat0),rd(sFlat0,X1)),
inference(step,[status(thm)],[t6652,t6395]) ).
cnf(t599,plain,
unit = mult(rd(X1,X2),rd(X2,X1)),
inference(cp,[status(thm)],[t76,t592]) ).
cnf(t961,plain,
mult(rd(X1,X2),rd(X2,X1)) = unit,
inference(orient,[status(thm)],[t599]) ).
cnf(t6654,plain,
op_k(sFlat0,i(X1)) = unit,
inference(step,[status(thm)],[t6653,t961]) ).
cnf(t6533,plain,
op_k(sFlat0,i(X1)) = unit,
inference(orient,[status(thm)],[t6654]) ).
cnf(t6544,plain,
unit = op_k(sFlat0,X1),
inference(cp,[status(thm)],[t6533,t500]) ).
cnf(t6552,plain,
op_k(sFlat0,X1) = unit,
inference(orient,[status(thm)],[t6544]) ).
cnf(goal_0,negated_conjecture,
op_k(op_k(a,b),c) != unit,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
op_k(sFlat0,c) != unit,
inference(rw,[status(thm)],[goal_0,t494]) ).
cnf(g0_1,plain,
unit != unit,
inference(rw,[status(thm)],[g0_0,t6552]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP728-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.08/0.36 % Computer : n003.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Wed Sep 23 15:53:19 UTC 2026
% 0.08/0.37 % CPUTime :
% 0.08/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 4.56/1.04 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.56/1.04 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------