%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP729-1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n002.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 23.90s 3.65s
% Output : CNFRefutation 23.90s
% Verified :
% SZS Type : Refutation
% Derivation depth : 43
% Number of leaves : 15
% Syntax : Number of clauses : 156 ( 156 unt; 0 nHn; 21 RR)
% Number of literals : 156 ( 155 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 : 12 ( 12 usr; 7 con; 0-3 aty)
% Number of variables : 237 ( 40 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t19,axiom,
sFlat0 = op_k(c,d),
introduced(definition) ).
cnf(t496,plain,
op_k(c,d) = sFlat0,
inference(orient,[status(thm)],[t19]) ).
cnf(t6,axiom,
mult(i(X1),mult(X1,X2)) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t22,plain,
mult(i(X1),mult(X1,X2)) = X2,
inference(orient,[status(thm)],[t6]) ).
cnf(t12,axiom,
mult(mult(X1,mult(X2,X3)),asoc(X1,X2,X3)) = mult(mult(X1,X2),X3),
file('/export/starexec/sandbox2/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(t10161,plain,
mult(i(mult(X1,mult(X2,X3))),mult(mult(X1,X2),X3)) = asoc(X1,X2,X3),
inference(orient,[status(thm)],[t71]) ).
cnf(t9,axiom,
mult(i(X1),i(X2)) = i(mult(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t245,plain,
mult(i(X1),i(X2)) = i(mult(X1,X2)),
inference(orient,[status(thm)],[t9]) ).
cnf(t3,axiom,
mult(i(X1),X1) = unit,
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p') ).
cnf(t21,plain,
mult(X1,unit) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t15502,plain,
X1 = i(i(X1)),
inference(step,[status(thm)],[t78,t21]) ).
cnf(t502,plain,
i(i(X1)) = X1,
inference(orient,[status(thm)],[t15502]) ).
cnf(t504,plain,
i(mult(i(X1),X2)) = mult(X1,i(X2)),
inference(cp,[status(thm)],[t245,t502]) ).
cnf(t682,plain,
i(mult(i(X1),X2)) = mult(X1,i(X2)),
inference(orient,[status(thm)],[t504]) ).
cnf(t2,axiom,
mult(X1,i(X1)) = unit,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t53,plain,
mult(X1,i(X1)) = unit,
inference(orient,[status(thm)],[t2]) ).
cnf(t65,plain,
mult(mult(X1,X2),i(X2)) = mult(mult(X1,unit),asoc(X1,X2,i(X2))),
inference(cp,[status(thm)],[t58,t53]) ).
cnf(t15665,plain,
mult(mult(X1,X2),i(X2)) = mult(X1,asoc(X1,X2,i(X2))),
inference(step,[status(thm)],[t65,t21]) ).
cnf(t5556,plain,
mult(X1,asoc(X1,X2,i(X2))) = mult(mult(X1,X2),i(X2)),
inference(orient,[status(thm)],[t15665]) ).
cnf(t7,axiom,
asoc(X1,X2,asoc(X3,X4,X5)) = unit,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t484,plain,
asoc(X1,X2,asoc(X3,X4,X5)) = unit,
inference(orient,[status(thm)],[t7]) ).
cnf(t503,plain,
X1 = mult(X2,mult(i(X2),X1)),
inference(cp,[status(thm)],[t22,t502]) ).
cnf(t642,plain,
mult(X1,mult(i(X1),X2)) = X2,
inference(orient,[status(thm)],[t503]) ).
cnf(t644,plain,
i(X1) = mult(X2,i(mult(X2,X1))),
inference(cp,[status(thm)],[t642,t245]) ).
cnf(t739,plain,
mult(X1,i(mult(X1,X2))) = i(X2),
inference(orient,[status(thm)],[t644]) ).
cnf(t10,axiom,
mult(mult(X1,X2),op_k(X2,X1)) = mult(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t34,plain,
mult(mult(X1,X2),op_k(X2,X1)) = mult(X2,X1),
inference(orient,[status(thm)],[t10]) ).
cnf(t497,plain,
mult(c,d) = mult(mult(d,c),sFlat0),
inference(cp,[status(thm)],[t34,t496]) ).
cnf(t614,plain,
mult(mult(d,c),sFlat0) = mult(c,d),
inference(orient,[status(thm)],[t497]) ).
cnf(t740,plain,
i(sFlat0) = mult(mult(d,c),i(mult(c,d))),
inference(cp,[status(thm)],[t739,t614]) ).
cnf(t8924,plain,
mult(mult(d,c),i(mult(c,d))) = i(sFlat0),
inference(orient,[status(thm)],[t740]) ).
cnf(t10272,plain,
asoc(d,c,i(mult(c,d))) = mult(i(mult(d,mult(c,i(mult(c,d))))),i(sFlat0)),
inference(cp,[status(thm)],[t10161,t8924]) ).
cnf(t15890,plain,
asoc(d,c,i(mult(c,d))) = i(mult(mult(d,mult(c,i(mult(c,d)))),sFlat0)),
inference(step,[status(thm)],[t10272,t245]) ).
cnf(t15891,plain,
asoc(d,c,i(mult(c,d))) = i(mult(mult(d,i(d)),sFlat0)),
inference(step,[status(thm)],[t15890,t739]) ).
cnf(t15892,plain,
asoc(d,c,i(mult(c,d))) = i(mult(unit,sFlat0)),
inference(step,[status(thm)],[t15891,t53]) ).
cnf(t1,axiom,
mult(unit,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t28,plain,
mult(unit,X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t15893,plain,
asoc(d,c,i(mult(c,d))) = i(sFlat0),
inference(step,[status(thm)],[t15892,t28]) ).
cnf(t11046,plain,
asoc(d,c,i(mult(c,d))) = i(sFlat0),
inference(orient,[status(thm)],[t15893]) ).
cnf(t11048,plain,
unit = asoc(X1,X2,i(sFlat0)),
inference(cp,[status(thm)],[t484,t11046]) ).
cnf(t11053,plain,
asoc(X1,X2,i(sFlat0)) = unit,
inference(orient,[status(thm)],[t11048]) ).
cnf(t11054,plain,
mult(mult(X1,sFlat0),i(sFlat0)) = mult(X1,unit),
inference(cp,[status(thm)],[t5556,t11053]) ).
cnf(t15894,plain,
mult(mult(X1,sFlat0),i(sFlat0)) = X1,
inference(step,[status(thm)],[t11054,t21]) ).
cnf(t11057,plain,
mult(mult(X1,sFlat0),i(sFlat0)) = X1,
inference(orient,[status(thm)],[t15894]) ).
cnf(t4,axiom,
mult(rd(X1,X2),X2) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t25,plain,
mult(rd(X1,X2),X2) = X1,
inference(orient,[status(thm)],[t4]) ).
cnf(t11069,plain,
rd(X1,sFlat0) = mult(X1,i(sFlat0)),
inference(cp,[status(thm)],[t11057,t25]) ).
cnf(t11116,plain,
mult(X1,i(sFlat0)) = rd(X1,sFlat0),
inference(orient,[status(thm)],[t11069]) ).
cnf(t11181,plain,
mult(mult(X1,X2),i(sFlat0)) = mult(mult(X1,rd(X2,sFlat0)),asoc(X1,X2,i(sFlat0))),
inference(cp,[status(thm)],[t58,t11116]) ).
cnf(t15925,plain,
rd(mult(X1,X2),sFlat0) = mult(mult(X1,rd(X2,sFlat0)),asoc(X1,X2,i(sFlat0))),
inference(step,[status(thm)],[t11181,t11116]) ).
cnf(t15926,plain,
rd(mult(X1,X2),sFlat0) = mult(mult(X1,rd(X2,sFlat0)),unit),
inference(step,[status(thm)],[t15925,t11053]) ).
cnf(t15927,plain,
rd(mult(X1,X2),sFlat0) = mult(X1,rd(X2,sFlat0)),
inference(step,[status(thm)],[t15926,t21]) ).
cnf(t12566,plain,
mult(X1,rd(X2,sFlat0)) = rd(mult(X1,X2),sFlat0),
inference(orient,[status(thm)],[t15927]) ).
cnf(t12662,plain,
mult(X1,i(rd(X2,sFlat0))) = i(rd(mult(i(X1),X2),sFlat0)),
inference(cp,[status(thm)],[t682,t12566]) ).
cnf(t5,axiom,
rd(mult(X1,X2),X2) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t30,plain,
rd(mult(X1,X2),X2) = X1,
inference(orient,[status(thm)],[t5]) ).
cnf(t33,plain,
i(X1) = rd(X2,mult(X1,X2)),
inference(cp,[status(thm)],[t30,t22]) ).
cnf(t588,plain,
rd(X1,mult(X2,X1)) = i(X2),
inference(orient,[status(thm)],[t33]) ).
cnf(t593,plain,
i(rd(X1,X2)) = rd(X2,X1),
inference(cp,[status(thm)],[t588,t25]) ).
cnf(t600,plain,
i(rd(X1,X2)) = rd(X2,X1),
inference(orient,[status(thm)],[t593]) ).
cnf(t15994,plain,
mult(X1,rd(sFlat0,X2)) = i(rd(mult(i(X1),X2),sFlat0)),
inference(step,[status(thm)],[t12662,t600]) ).
cnf(t15995,plain,
mult(X1,rd(sFlat0,X2)) = rd(sFlat0,mult(i(X1),X2)),
inference(step,[status(thm)],[t15994,t600]) ).
cnf(t15166,plain,
rd(sFlat0,mult(i(X1),X2)) = mult(X1,rd(sFlat0,X2)),
inference(orient,[status(thm)],[t15995]) ).
cnf(t15169,plain,
mult(X1,rd(sFlat0,i(X2))) = rd(sFlat0,i(mult(X1,X2))),
inference(cp,[status(thm)],[t15166,t245]) ).
cnf(t8,axiom,
asoc(asoc(X1,X2,X3),X4,X5) = unit,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t487,plain,
asoc(asoc(X1,X2,X3),X4,X5) = unit,
inference(orient,[status(thm)],[t8]) ).
cnf(t20,axiom,
sFlat1 = asoc(a,b,op_k(c,d)),
introduced(definition) ).
cnf(t492,plain,
asoc(a,b,op_k(c,d)) = sFlat1,
inference(orient,[status(thm)],[t20]) ).
cnf(t15501,plain,
asoc(a,b,sFlat0) = sFlat1,
inference(step,[status(thm)],[t492,t496]) ).
cnf(t498,plain,
asoc(a,b,sFlat0) = sFlat1,
inference(rw,[status(thm)],[t15501]) ).
cnf(t519,plain,
asoc(a,b,sFlat0) = sFlat1,
inference(orient,[status(thm)],[t498]) ).
cnf(t520,plain,
unit = asoc(sFlat1,X1,X2),
inference(cp,[status(thm)],[t487,t519]) ).
cnf(t524,plain,
asoc(sFlat1,X1,X2) = unit,
inference(orient,[status(thm)],[t520]) ).
cnf(t525,plain,
mult(mult(sFlat1,X1),X2) = mult(mult(sFlat1,mult(X1,X2)),unit),
inference(cp,[status(thm)],[t58,t524]) ).
cnf(t15512,plain,
mult(mult(sFlat1,X1),X2) = mult(sFlat1,mult(X1,X2)),
inference(step,[status(thm)],[t525,t21]) ).
cnf(t931,plain,
mult(mult(sFlat1,X1),X2) = mult(sFlat1,mult(X1,X2)),
inference(orient,[status(thm)],[t15512]) ).
cnf(t944,plain,
mult(sFlat1,X1) = rd(mult(sFlat1,mult(X1,X2)),X2),
inference(cp,[status(thm)],[t30,t931]) ).
cnf(t1410,plain,
rd(mult(sFlat1,mult(X1,X2)),X2) = mult(sFlat1,X1),
inference(orient,[status(thm)],[t944]) ).
cnf(t1430,plain,
mult(sFlat1,i(X1)) = rd(mult(sFlat1,unit),X1),
inference(cp,[status(thm)],[t1410,t76]) ).
cnf(t15525,plain,
mult(sFlat1,i(X1)) = rd(sFlat1,X1),
inference(step,[status(thm)],[t1430,t21]) ).
cnf(t1463,plain,
mult(sFlat1,i(X1)) = rd(sFlat1,X1),
inference(orient,[status(thm)],[t15525]) ).
cnf(t1464,plain,
rd(sFlat1,mult(sFlat1,X1)) = i(X1),
inference(cp,[status(thm)],[t1463,t739]) ).
cnf(t1875,plain,
rd(sFlat1,mult(sFlat1,X1)) = i(X1),
inference(orient,[status(thm)],[t1464]) ).
cnf(t1472,plain,
mult(sFlat1,mult(i(X1),X2)) = mult(rd(sFlat1,X1),X2),
inference(cp,[status(thm)],[t931,t1463]) ).
cnf(t3206,plain,
mult(sFlat1,mult(i(X1),X2)) = mult(rd(sFlat1,X1),X2),
inference(orient,[status(thm)],[t1472]) ).
cnf(t3238,plain,
i(mult(i(X1),X2)) = rd(sFlat1,mult(rd(sFlat1,X1),X2)),
inference(cp,[status(thm)],[t1875,t3206]) ).
cnf(t15727,plain,
mult(X1,i(X2)) = rd(sFlat1,mult(rd(sFlat1,X1),X2)),
inference(step,[status(thm)],[t3238,t682]) ).
cnf(t8238,plain,
rd(sFlat1,mult(rd(sFlat1,X1),X2)) = mult(X1,i(X2)),
inference(orient,[status(thm)],[t15727]) ).
cnf(t11161,plain,
mult(X1,i(i(sFlat0))) = rd(sFlat1,rd(rd(sFlat1,X1),sFlat0)),
inference(cp,[status(thm)],[t8238,t11116]) ).
cnf(t15895,plain,
mult(X1,sFlat0) = rd(sFlat1,rd(rd(sFlat1,X1),sFlat0)),
inference(step,[status(thm)],[t11161,t502]) ).
cnf(t1479,plain,
i(i(X1)) = mult(sFlat1,i(rd(sFlat1,X1))),
inference(cp,[status(thm)],[t739,t1463]) ).
cnf(t15528,plain,
X1 = mult(sFlat1,i(rd(sFlat1,X1))),
inference(step,[status(thm)],[t1479,t502]) ).
cnf(t15529,plain,
X1 = rd(sFlat1,rd(sFlat1,X1)),
inference(step,[status(thm)],[t15528,t1463]) ).
cnf(t1570,plain,
rd(sFlat1,rd(sFlat1,X1)) = X1,
inference(orient,[status(thm)],[t15529]) ).
cnf(t607,plain,
unit = mult(rd(X1,X2),rd(X2,X1)),
inference(cp,[status(thm)],[t76,t600]) ).
cnf(t1017,plain,
mult(rd(X1,X2),rd(X2,X1)) = unit,
inference(orient,[status(thm)],[t607]) ).
cnf(t1427,plain,
mult(sFlat1,rd(X1,X2)) = rd(mult(sFlat1,unit),rd(X2,X1)),
inference(cp,[status(thm)],[t1410,t1017]) ).
cnf(t1426,plain,
mult(sFlat1,rd(X1,X2)) = rd(mult(sFlat1,X1),X2),
inference(cp,[status(thm)],[t1410,t25]) ).
cnf(t2572,plain,
mult(sFlat1,rd(X1,X2)) = rd(mult(sFlat1,X1),X2),
inference(orient,[status(thm)],[t1426]) ).
cnf(t15570,plain,
rd(mult(sFlat1,X1),X2) = rd(mult(sFlat1,unit),rd(X2,X1)),
inference(step,[status(thm)],[t1427,t2572]) ).
cnf(t15571,plain,
rd(mult(sFlat1,X1),X2) = rd(sFlat1,rd(X2,X1)),
inference(step,[status(thm)],[t15570,t21]) ).
cnf(t2628,plain,
rd(mult(sFlat1,X1),X2) = rd(sFlat1,rd(X2,X1)),
inference(orient,[status(thm)],[t15571]) ).
cnf(t2636,plain,
rd(sFlat1,rd(X1,i(X2))) = rd(rd(sFlat1,X2),X1),
inference(cp,[status(thm)],[t2628,t1463]) ).
cnf(t3359,plain,
rd(sFlat1,rd(X1,i(X2))) = rd(rd(sFlat1,X2),X1),
inference(orient,[status(thm)],[t2636]) ).
cnf(t3384,plain,
rd(X1,i(X2)) = rd(sFlat1,rd(rd(sFlat1,X2),X1)),
inference(cp,[status(thm)],[t1570,t3359]) ).
cnf(t8348,plain,
rd(sFlat1,rd(rd(sFlat1,X1),X2)) = rd(X2,i(X1)),
inference(orient,[status(thm)],[t3384]) ).
cnf(t15896,plain,
mult(X1,sFlat0) = rd(sFlat0,i(X1)),
inference(step,[status(thm)],[t15895,t8348]) ).
cnf(t11210,plain,
rd(sFlat0,i(X1)) = mult(X1,sFlat0),
inference(orient,[status(thm)],[t15896]) ).
cnf(t15996,plain,
mult(X1,mult(X2,sFlat0)) = rd(sFlat0,i(mult(X1,X2))),
inference(step,[status(thm)],[t15169,t11210]) ).
cnf(t15997,plain,
mult(X1,mult(X2,sFlat0)) = mult(mult(X1,X2),sFlat0),
inference(step,[status(thm)],[t15996,t11210]) ).
cnf(t11047,plain,
unit = asoc(i(sFlat0),X1,X2),
inference(cp,[status(thm)],[t487,t11046]) ).
cnf(t11049,plain,
asoc(i(sFlat0),X1,X2) = unit,
inference(orient,[status(thm)],[t11047]) ).
cnf(t11050,plain,
mult(mult(i(sFlat0),X1),i(X1)) = mult(i(sFlat0),unit),
inference(cp,[status(thm)],[t5556,t11049]) ).
cnf(t15934,plain,
mult(mult(i(sFlat0),X1),i(X1)) = i(sFlat0),
inference(step,[status(thm)],[t11050,t21]) ).
cnf(t12859,plain,
mult(mult(i(sFlat0),X1),i(X1)) = i(sFlat0),
inference(orient,[status(thm)],[t15934]) ).
cnf(t12895,plain,
i(mult(i(sFlat0),X1)) = rd(i(X1),i(sFlat0)),
inference(cp,[status(thm)],[t588,t12859]) ).
cnf(t15935,plain,
mult(sFlat0,i(X1)) = rd(i(X1),i(sFlat0)),
inference(step,[status(thm)],[t12895,t682]) ).
cnf(t744,plain,
i(X1) = mult(rd(X2,X1),i(X2)),
inference(cp,[status(thm)],[t739,t25]) ).
cnf(t812,plain,
mult(rd(X1,X2),i(X1)) = i(X2),
inference(orient,[status(thm)],[t744]) ).
cnf(t818,plain,
i(rd(X1,X2)) = rd(i(X1),i(X2)),
inference(cp,[status(thm)],[t588,t812]) ).
cnf(t15510,plain,
rd(X2,X1) = rd(i(X1),i(X2)),
inference(step,[status(thm)],[t818,t600]) ).
cnf(t840,plain,
rd(i(X1),i(X2)) = rd(X2,X1),
inference(orient,[status(thm)],[t15510]) ).
cnf(t15936,plain,
mult(sFlat0,i(X1)) = rd(sFlat0,X1),
inference(step,[status(thm)],[t15935,t840]) ).
cnf(t12938,plain,
mult(sFlat0,i(X1)) = rd(sFlat0,X1),
inference(orient,[status(thm)],[t15936]) ).
cnf(t12953,plain,
rd(sFlat0,i(X1)) = mult(sFlat0,X1),
inference(cp,[status(thm)],[t12938,t502]) ).
cnf(t15953,plain,
mult(X1,sFlat0) = mult(sFlat0,X1),
inference(step,[status(thm)],[t12953,t11210]) ).
cnf(t13451,plain,
mult(X1,sFlat0) = mult(sFlat0,X1),
inference(orient,[status(thm)],[t15953]) ).
cnf(t15998,plain,
mult(X1,mult(X2,sFlat0)) = mult(sFlat0,mult(X1,X2)),
inference(step,[status(thm)],[t15997,t13451]) ).
cnf(t15243,plain,
mult(X1,mult(X2,sFlat0)) = mult(sFlat0,mult(X1,X2)),
inference(orient,[status(thm)],[t15998]) ).
cnf(t15373,plain,
asoc(X1,X2,sFlat0) = mult(i(mult(sFlat0,mult(X1,X2))),mult(mult(X1,X2),sFlat0)),
inference(cp,[status(thm)],[t10161,t15243]) ).
cnf(t39,plain,
op_k(X1,X2) = mult(i(mult(X2,X1)),mult(X1,X2)),
inference(cp,[status(thm)],[t22,t34]) ).
cnf(t2109,plain,
mult(i(mult(X1,X2)),mult(X2,X1)) = op_k(X2,X1),
inference(orient,[status(thm)],[t39]) ).
cnf(t15999,plain,
asoc(X1,X2,sFlat0) = op_k(mult(X1,X2),sFlat0),
inference(step,[status(thm)],[t15373,t2109]) ).
cnf(t12976,plain,
op_k(i(X1),sFlat0) = mult(i(rd(sFlat0,X1)),mult(i(X1),sFlat0)),
inference(cp,[status(thm)],[t2109,t12938]) ).
cnf(t15937,plain,
op_k(i(X1),sFlat0) = mult(rd(X1,sFlat0),mult(i(X1),sFlat0)),
inference(step,[status(thm)],[t12976,t600]) ).
cnf(t505,plain,
i(mult(X1,i(X2))) = mult(i(X1),X2),
inference(cp,[status(thm)],[t245,t502]) ).
cnf(t712,plain,
i(mult(X1,i(X2))) = mult(i(X1),X2),
inference(orient,[status(thm)],[t505]) ).
cnf(t11178,plain,
mult(i(X1),sFlat0) = i(rd(X1,sFlat0)),
inference(cp,[status(thm)],[t712,t11116]) ).
cnf(t15897,plain,
mult(i(X1),sFlat0) = rd(sFlat0,X1),
inference(step,[status(thm)],[t11178,t600]) ).
cnf(t11251,plain,
mult(i(X1),sFlat0) = rd(sFlat0,X1),
inference(orient,[status(thm)],[t15897]) ).
cnf(t15938,plain,
op_k(i(X1),sFlat0) = mult(rd(X1,sFlat0),rd(sFlat0,X1)),
inference(step,[status(thm)],[t15937,t11251]) ).
cnf(t15939,plain,
op_k(i(X1),sFlat0) = unit,
inference(step,[status(thm)],[t15938,t1017]) ).
cnf(t13001,plain,
op_k(i(X1),sFlat0) = unit,
inference(orient,[status(thm)],[t15939]) ).
cnf(t13017,plain,
unit = op_k(X1,sFlat0),
inference(cp,[status(thm)],[t13001,t502]) ).
cnf(t13021,plain,
op_k(X1,sFlat0) = unit,
inference(orient,[status(thm)],[t13017]) ).
cnf(t16000,plain,
asoc(X1,X2,sFlat0) = unit,
inference(step,[status(thm)],[t15999,t13021]) ).
cnf(t15496,plain,
asoc(X1,X2,sFlat0) = unit,
inference(orient,[status(thm)],[t16000]) ).
cnf(goal_0,negated_conjecture,
asoc(a,b,op_k(c,d)) != unit,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
asoc(a,b,sFlat0) != unit,
inference(rw,[status(thm)],[goal_0,t496]) ).
cnf(g0_1,plain,
unit != unit,
inference(rw,[status(thm)],[g0_0,t15496]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP729-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.11/0.37 % Computer : n002.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Wed Sep 23 15:54:33 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 23.90/3.65 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 23.90/3.65 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------