%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP731-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 : 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 01:28:18 PM UTC 2026
% Result : Unsatisfiable 5.91s 1.24s
% Output : CNFRefutation 5.91s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 15
% Syntax : Number of clauses : 87 ( 87 unt; 0 nHn; 20 RR)
% Number of literals : 87 ( 86 equ; 4 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 : 14 ( 14 usr; 7 con; 0-3 aty)
% Number of variables : 121 ( 16 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t22,axiom,
sFlat0 = asoc(a,b,c),
introduced(definition) ).
cnf(t206,plain,
asoc(a,b,c) = sFlat0,
inference(orient,[status(thm)],[t22]) ).
cnf(t23,axiom,
sFlat1 = op_k(asoc(a,b,c),d),
introduced(definition) ).
cnf(t2109,plain,
sFlat1 = op_k(sFlat0,d),
inference(step,[status(thm)],[t23,t206]) ).
cnf(t210,plain,
op_k(sFlat0,d) = sFlat1,
inference(orient,[status(thm)],[t2109]) ).
cnf(t16,axiom,
mult(i(mult(X1,X2)),mult(X1,mult(X2,X3))) = op_l(X3,X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t112,plain,
mult(i(mult(X1,X2)),mult(X1,mult(X2,X3))) = op_l(X3,X2,X1),
inference(orient,[status(thm)],[t16]) ).
cnf(t11,axiom,
mult(mult(X1,X2),op_k(X2,X1)) = mult(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t37,plain,
mult(mult(X1,X2),op_k(X2,X1)) = mult(X2,X1),
inference(orient,[status(thm)],[t11]) ).
cnf(t211,plain,
mult(sFlat0,d) = mult(mult(d,sFlat0),sFlat1),
inference(cp,[status(thm)],[t37,t210]) ).
cnf(t314,plain,
mult(mult(d,sFlat0),sFlat1) = mult(sFlat0,d),
inference(orient,[status(thm)],[t211]) ).
cnf(t1974,plain,
mult(mult(d,sFlat0),sFlat1) = mult(sFlat0,d),
inference(rw,[status(thm)],[t314]) ).
cnf(t6,axiom,
mult(i(X1),mult(X1,X2)) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t25,plain,
mult(i(X1),mult(X1,X2)) = X2,
inference(orient,[status(thm)],[t6]) ).
cnf(t3,axiom,
mult(i(X1),X1) = unit,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t79,plain,
mult(i(X1),X1) = unit,
inference(orient,[status(thm)],[t3]) ).
cnf(t81,plain,
X1 = mult(i(i(X1)),unit),
inference(cp,[status(thm)],[t25,t79]) ).
cnf(t0,axiom,
mult(X1,unit) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t24,plain,
mult(X1,unit) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t2110,plain,
X1 = i(i(X1)),
inference(step,[status(thm)],[t81,t24]) ).
cnf(t216,plain,
i(i(X1)) = X1,
inference(orient,[status(thm)],[t2110]) ).
cnf(t217,plain,
X1 = mult(X2,mult(i(X2),X1)),
inference(cp,[status(thm)],[t25,t216]) ).
cnf(t334,plain,
mult(X1,mult(i(X1),X2)) = X2,
inference(orient,[status(thm)],[t217]) ).
cnf(t10,axiom,
mult(i(X1),mult(X2,X1)) = op_t(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t86,plain,
mult(i(X1),mult(X2,X1)) = op_t(X2,X1),
inference(orient,[status(thm)],[t10]) ).
cnf(t337,plain,
mult(X1,X2) = mult(X2,op_t(X1,X2)),
inference(cp,[status(thm)],[t334,t86]) ).
cnf(t356,plain,
mult(X1,op_t(X2,X1)) = mult(X2,X1),
inference(orient,[status(thm)],[t337]) ).
cnf(t9,axiom,
mult(i(X1),i(X2)) = i(mult(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t104,plain,
mult(i(X1),i(X2)) = i(mult(X1,X2)),
inference(orient,[status(thm)],[t9]) ).
cnf(t107,plain,
op_t(i(X1),i(X2)) = mult(i(i(X2)),i(mult(X1,X2))),
inference(cp,[status(thm)],[t86,t104]) ).
cnf(t2134,plain,
op_t(i(X1),i(X2)) = i(mult(i(X2),mult(X1,X2))),
inference(step,[status(thm)],[t107,t104]) ).
cnf(t2135,plain,
op_t(i(X1),i(X2)) = i(op_t(X1,X2)),
inference(step,[status(thm)],[t2134,t86]) ).
cnf(t380,plain,
op_t(i(X1),i(X2)) = i(op_t(X1,X2)),
inference(orient,[status(thm)],[t2135]) ).
cnf(t382,plain,
i(op_t(i(X1),X2)) = op_t(X1,i(X2)),
inference(cp,[status(thm)],[t380,t216]) ).
cnf(t444,plain,
i(op_t(i(X1),X2)) = op_t(X1,i(X2)),
inference(orient,[status(thm)],[t382]) ).
cnf(t336,plain,
i(X1) = mult(X2,i(mult(X2,X1))),
inference(cp,[status(thm)],[t334,t104]) ).
cnf(t496,plain,
mult(X1,i(mult(X1,X2))) = i(X2),
inference(orient,[status(thm)],[t336]) ).
cnf(t4,axiom,
mult(rd(X1,X2),X2) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t30,plain,
mult(rd(X1,X2),X2) = X1,
inference(orient,[status(thm)],[t4]) ).
cnf(t502,plain,
i(X1) = mult(rd(X2,X1),i(X2)),
inference(cp,[status(thm)],[t496,t30]) ).
cnf(t533,plain,
mult(rd(X1,X2),i(X1)) = i(X2),
inference(orient,[status(thm)],[t502]) ).
cnf(t5,axiom,
rd(mult(X1,X2),X2) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t33,plain,
rd(mult(X1,X2),X2) = X1,
inference(orient,[status(thm)],[t5]) ).
cnf(t21,axiom,
mult(mult(X1,mult(X2,X3)),asoc(X1,X2,X3)) = mult(mult(X1,X2),X3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t61,plain,
mult(mult(X1,mult(X2,X3)),asoc(X1,X2,X3)) = mult(mult(X1,X2),X3),
inference(orient,[status(thm)],[t21]) ).
cnf(t8,axiom,
asoc(asoc(X1,X2,X3),X4,X5) = unit,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t201,plain,
asoc(asoc(X1,X2,X3),X4,X5) = unit,
inference(orient,[status(thm)],[t8]) ).
cnf(t207,plain,
unit = asoc(sFlat0,X1,X2),
inference(cp,[status(thm)],[t201,t206]) ).
cnf(t240,plain,
asoc(sFlat0,X1,X2) = unit,
inference(orient,[status(thm)],[t207]) ).
cnf(t241,plain,
mult(mult(sFlat0,X1),X2) = mult(mult(sFlat0,mult(X1,X2)),unit),
inference(cp,[status(thm)],[t61,t240]) ).
cnf(t2143,plain,
mult(mult(sFlat0,X1),X2) = mult(sFlat0,mult(X1,X2)),
inference(step,[status(thm)],[t241,t24]) ).
cnf(t597,plain,
mult(mult(sFlat0,X1),X2) = mult(sFlat0,mult(X1,X2)),
inference(orient,[status(thm)],[t2143]) ).
cnf(t612,plain,
mult(sFlat0,X1) = rd(mult(sFlat0,mult(X1,X2)),X2),
inference(cp,[status(thm)],[t33,t597]) ).
cnf(t1475,plain,
rd(mult(sFlat0,mult(X1,X2)),X2) = mult(sFlat0,X1),
inference(orient,[status(thm)],[t612]) ).
cnf(t2,axiom,
mult(X1,i(X1)) = unit,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t56,plain,
mult(X1,i(X1)) = unit,
inference(orient,[status(thm)],[t2]) ).
cnf(t1485,plain,
mult(sFlat0,X1) = rd(mult(sFlat0,unit),i(X1)),
inference(cp,[status(thm)],[t1475,t56]) ).
cnf(t2180,plain,
mult(sFlat0,X1) = rd(sFlat0,i(X1)),
inference(step,[status(thm)],[t1485,t24]) ).
cnf(t1520,plain,
rd(sFlat0,i(X1)) = mult(sFlat0,X1),
inference(orient,[status(thm)],[t2180]) ).
cnf(t1538,plain,
i(i(X1)) = mult(mult(sFlat0,X1),i(sFlat0)),
inference(cp,[status(thm)],[t533,t1520]) ).
cnf(t2181,plain,
X1 = mult(mult(sFlat0,X1),i(sFlat0)),
inference(step,[status(thm)],[t1538,t216]) ).
cnf(t2182,plain,
X1 = mult(sFlat0,mult(X1,i(sFlat0))),
inference(step,[status(thm)],[t2181,t597]) ).
cnf(t220,plain,
op_t(X1,i(X2)) = mult(X2,mult(X1,i(X2))),
inference(cp,[status(thm)],[t86,t216]) ).
cnf(t800,plain,
mult(X1,mult(X2,i(X1))) = op_t(X2,i(X1)),
inference(orient,[status(thm)],[t220]) ).
cnf(t2183,plain,
X1 = op_t(X1,i(sFlat0)),
inference(step,[status(thm)],[t2182,t800]) ).
cnf(t1542,plain,
op_t(X1,i(sFlat0)) = X1,
inference(orient,[status(thm)],[t2183]) ).
cnf(t1553,plain,
op_t(X1,i(i(sFlat0))) = i(i(X1)),
inference(cp,[status(thm)],[t444,t1542]) ).
cnf(t2184,plain,
op_t(X1,sFlat0) = i(i(X1)),
inference(step,[status(thm)],[t1553,t216]) ).
cnf(t2185,plain,
op_t(X1,sFlat0) = X1,
inference(step,[status(thm)],[t2184,t216]) ).
cnf(t1554,plain,
op_t(X1,sFlat0) = X1,
inference(orient,[status(thm)],[t2185]) ).
cnf(t1561,plain,
mult(X1,sFlat0) = mult(sFlat0,X1),
inference(cp,[status(thm)],[t356,t1554]) ).
cnf(t1944,plain,
mult(X1,sFlat0) = mult(sFlat0,X1),
inference(orient,[status(thm)],[t1561]) ).
cnf(t2219,plain,
mult(mult(sFlat0,d),sFlat1) = mult(sFlat0,d),
inference(step,[status(thm)],[t1974,t1944]) ).
cnf(t2220,plain,
mult(sFlat0,mult(d,sFlat1)) = mult(sFlat0,d),
inference(step,[status(thm)],[t2219,t597]) ).
cnf(t2037,plain,
mult(sFlat0,mult(d,sFlat1)) = mult(sFlat0,d),
inference(orient,[status(thm)],[t2220]) ).
cnf(t2059,plain,
op_l(sFlat1,d,sFlat0) = mult(i(mult(sFlat0,d)),mult(sFlat0,d)),
inference(cp,[status(thm)],[t112,t2037]) ).
cnf(t607,plain,
X1 = mult(i(mult(sFlat0,X2)),mult(sFlat0,mult(X2,X1))),
inference(cp,[status(thm)],[t25,t597]) ).
cnf(t2144,plain,
X1 = op_l(X1,X2,sFlat0),
inference(step,[status(thm)],[t607,t112]) ).
cnf(t625,plain,
op_l(X1,X2,sFlat0) = X1,
inference(orient,[status(thm)],[t2144]) ).
cnf(t2221,plain,
sFlat1 = mult(i(mult(sFlat0,d)),mult(sFlat0,d)),
inference(step,[status(thm)],[t2059,t625]) ).
cnf(t2222,plain,
sFlat1 = unit,
inference(step,[status(thm)],[t2221,t79]) ).
cnf(t2062,plain,
unit = sFlat1,
inference(orient,[status(thm)],[t2222]) ).
cnf(goal_0,negated_conjecture,
op_k(asoc(a,b,c),d) != unit,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
op_k(sFlat0,d) != unit,
inference(rw,[status(thm)],[goal_0,t206]) ).
cnf(g0_1,plain,
sFlat1 != unit,
inference(rw,[status(thm)],[g0_0,t210]) ).
cnf(g0_2,plain,
sFlat1 != sFlat1,
inference(rw,[status(thm)],[g0_1,t2062]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP731-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n017.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 : Wed Sep 23 15:47:29 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 5.91/1.24 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.91/1.24 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------