%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP727-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 10.20s 1.92s
% Output : CNFRefutation 10.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 44
% Number of leaves : 11
% Syntax : Number of clauses : 120 ( 120 unt; 0 nHn; 6 RR)
% Number of literals : 120 ( 119 equ; 3 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 7 con; 0-3 aty)
% Number of variables : 211 ( 20 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t17,axiom,
sFlat0 = asoc(c,d,e),
introduced(definition) ).
cnf(t442,plain,
asoc(c,d,e) = sFlat0,
inference(orient,[status(thm)],[t17]) ).
cnf(t6,axiom,
mult(i(X1),mult(X1,X2)) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t20,plain,
mult(i(X1),mult(X1,X2)) = X2,
inference(orient,[status(thm)],[t6]) ).
cnf(t10,axiom,
mult(mult(X1,mult(X2,X3)),asoc(X1,X2,X3)) = mult(mult(X1,X2),X3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t44,plain,
mult(mult(X1,mult(X2,X3)),asoc(X1,X2,X3)) = mult(mult(X1,X2),X3),
inference(orient,[status(thm)],[t10]) ).
cnf(t56,plain,
asoc(X1,X2,X3) = mult(i(mult(X1,mult(X2,X3))),mult(mult(X1,X2),X3)),
inference(cp,[status(thm)],[t20,t44]) ).
cnf(t10078,plain,
mult(i(mult(X1,mult(X2,X3))),mult(mult(X1,X2),X3)) = asoc(X1,X2,X3),
inference(orient,[status(thm)],[t56]) ).
cnf(t4,axiom,
mult(rd(X1,X2),X2) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t23,plain,
mult(rd(X1,X2),X2) = X1,
inference(orient,[status(thm)],[t4]) ).
cnf(t5,axiom,
rd(mult(X1,X2),X2) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t28,plain,
rd(mult(X1,X2),X2) = X1,
inference(orient,[status(thm)],[t5]) ).
cnf(t7,axiom,
asoc(asoc(X1,X2,X3),X4,X5) = unit,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t439,plain,
asoc(asoc(X1,X2,X3),X4,X5) = unit,
inference(orient,[status(thm)],[t7]) ).
cnf(t443,plain,
unit = asoc(sFlat0,X1,X2),
inference(cp,[status(thm)],[t439,t442]) ).
cnf(t462,plain,
asoc(sFlat0,X1,X2) = unit,
inference(orient,[status(thm)],[t443]) ).
cnf(t463,plain,
mult(mult(sFlat0,X1),X2) = mult(mult(sFlat0,mult(X1,X2)),unit),
inference(cp,[status(thm)],[t44,t462]) ).
cnf(t0,axiom,
mult(X1,unit) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t19,plain,
mult(X1,unit) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t10571,plain,
mult(mult(sFlat0,X1),X2) = mult(sFlat0,mult(X1,X2)),
inference(step,[status(thm)],[t463,t19]) ).
cnf(t724,plain,
mult(mult(sFlat0,X1),X2) = mult(sFlat0,mult(X1,X2)),
inference(orient,[status(thm)],[t10571]) ).
cnf(t733,plain,
mult(sFlat0,X1) = rd(mult(sFlat0,mult(X1,X2)),X2),
inference(cp,[status(thm)],[t28,t724]) ).
cnf(t1092,plain,
rd(mult(sFlat0,mult(X1,X2)),X2) = mult(sFlat0,X1),
inference(orient,[status(thm)],[t733]) ).
cnf(t3,axiom,
mult(i(X1),X1) = unit,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t60,plain,
mult(i(X1),X1) = unit,
inference(orient,[status(thm)],[t3]) ).
cnf(t31,plain,
i(X1) = rd(X2,mult(X1,X2)),
inference(cp,[status(thm)],[t28,t20]) ).
cnf(t466,plain,
rd(X1,mult(X2,X1)) = i(X2),
inference(orient,[status(thm)],[t31]) ).
cnf(t470,plain,
i(rd(X1,X2)) = rd(X2,X1),
inference(cp,[status(thm)],[t466,t23]) ).
cnf(t477,plain,
i(rd(X1,X2)) = rd(X2,X1),
inference(orient,[status(thm)],[t470]) ).
cnf(t482,plain,
unit = mult(rd(X1,X2),rd(X2,X1)),
inference(cp,[status(thm)],[t60,t477]) ).
cnf(t808,plain,
mult(rd(X1,X2),rd(X2,X1)) = unit,
inference(orient,[status(thm)],[t482]) ).
cnf(t1106,plain,
mult(sFlat0,rd(X1,X2)) = rd(mult(sFlat0,unit),rd(X2,X1)),
inference(cp,[status(thm)],[t1092,t808]) ).
cnf(t1105,plain,
mult(sFlat0,rd(X1,X2)) = rd(mult(sFlat0,X1),X2),
inference(cp,[status(thm)],[t1092,t23]) ).
cnf(t1752,plain,
mult(sFlat0,rd(X1,X2)) = rd(mult(sFlat0,X1),X2),
inference(orient,[status(thm)],[t1105]) ).
cnf(t10596,plain,
rd(mult(sFlat0,X1),X2) = rd(mult(sFlat0,unit),rd(X2,X1)),
inference(step,[status(thm)],[t1106,t1752]) ).
cnf(t10597,plain,
rd(mult(sFlat0,X1),X2) = rd(sFlat0,rd(X2,X1)),
inference(step,[status(thm)],[t10596,t19]) ).
cnf(t1799,plain,
rd(mult(sFlat0,X1),X2) = rd(sFlat0,rd(X2,X1)),
inference(orient,[status(thm)],[t10597]) ).
cnf(t1821,plain,
mult(sFlat0,X1) = mult(rd(sFlat0,rd(X2,X1)),X2),
inference(cp,[status(thm)],[t23,t1799]) ).
cnf(t5141,plain,
mult(rd(sFlat0,rd(X1,X2)),X1) = mult(sFlat0,X2),
inference(orient,[status(thm)],[t1821]) ).
cnf(t62,plain,
X1 = mult(i(i(X1)),unit),
inference(cp,[status(thm)],[t20,t60]) ).
cnf(t10567,plain,
X1 = i(i(X1)),
inference(step,[status(thm)],[t62,t19]) ).
cnf(t451,plain,
i(i(X1)) = X1,
inference(orient,[status(thm)],[t10567]) ).
cnf(t452,plain,
X1 = mult(X2,mult(i(X2),X1)),
inference(cp,[status(thm)],[t20,t451]) ).
cnf(t489,plain,
mult(X1,mult(i(X1),X2)) = X2,
inference(orient,[status(thm)],[t452]) ).
cnf(t8,axiom,
mult(i(X1),i(X2)) = i(mult(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t214,plain,
mult(i(X1),i(X2)) = i(mult(X1,X2)),
inference(orient,[status(thm)],[t8]) ).
cnf(t491,plain,
i(X1) = mult(X2,i(mult(X2,X1))),
inference(cp,[status(thm)],[t489,t214]) ).
cnf(t579,plain,
mult(X1,i(mult(X1,X2))) = i(X2),
inference(orient,[status(thm)],[t491]) ).
cnf(t1109,plain,
mult(sFlat0,i(X1)) = rd(mult(sFlat0,unit),X1),
inference(cp,[status(thm)],[t1092,t60]) ).
cnf(t10582,plain,
mult(sFlat0,i(X1)) = rd(sFlat0,X1),
inference(step,[status(thm)],[t1109,t19]) ).
cnf(t1136,plain,
mult(sFlat0,i(X1)) = rd(sFlat0,X1),
inference(orient,[status(thm)],[t10582]) ).
cnf(t1149,plain,
i(i(X1)) = mult(sFlat0,i(rd(sFlat0,X1))),
inference(cp,[status(thm)],[t579,t1136]) ).
cnf(t10585,plain,
X1 = mult(sFlat0,i(rd(sFlat0,X1))),
inference(step,[status(thm)],[t1149,t451]) ).
cnf(t10586,plain,
X1 = rd(sFlat0,rd(sFlat0,X1)),
inference(step,[status(thm)],[t10585,t1136]) ).
cnf(t1234,plain,
rd(sFlat0,rd(sFlat0,X1)) = X1,
inference(orient,[status(thm)],[t10586]) ).
cnf(t1236,plain,
mult(X1,sFlat0) = rd(sFlat0,i(X1)),
inference(cp,[status(thm)],[t1234,t466]) ).
cnf(t2,axiom,
mult(X1,i(X1)) = unit,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t40,plain,
mult(X1,i(X1)) = unit,
inference(orient,[status(thm)],[t2]) ).
cnf(t1097,plain,
mult(sFlat0,X1) = rd(mult(sFlat0,unit),i(X1)),
inference(cp,[status(thm)],[t1092,t40]) ).
cnf(t10581,plain,
mult(sFlat0,X1) = rd(sFlat0,i(X1)),
inference(step,[status(thm)],[t1097,t19]) ).
cnf(t1123,plain,
rd(sFlat0,i(X1)) = mult(sFlat0,X1),
inference(orient,[status(thm)],[t10581]) ).
cnf(t10594,plain,
mult(X1,sFlat0) = mult(sFlat0,X1),
inference(step,[status(thm)],[t1236,t1123]) ).
cnf(t1494,plain,
mult(X1,sFlat0) = mult(sFlat0,X1),
inference(orient,[status(thm)],[t10594]) ).
cnf(t1813,plain,
rd(sFlat0,rd(X1,X2)) = rd(mult(X2,sFlat0),X1),
inference(cp,[status(thm)],[t1799,t1494]) ).
cnf(t2115,plain,
rd(mult(X1,sFlat0),X2) = rd(sFlat0,rd(X2,X1)),
inference(orient,[status(thm)],[t1813]) ).
cnf(t5168,plain,
mult(sFlat0,X1) = mult(rd(sFlat0,rd(sFlat0,rd(X1,X2))),mult(X2,sFlat0)),
inference(cp,[status(thm)],[t5141,t2115]) ).
cnf(t10731,plain,
mult(sFlat0,X1) = mult(rd(X1,X2),mult(X2,sFlat0)),
inference(step,[status(thm)],[t5168,t1234]) ).
cnf(t7733,plain,
mult(rd(X1,X2),mult(X2,sFlat0)) = mult(sFlat0,X1),
inference(orient,[status(thm)],[t10731]) ).
cnf(t10112,plain,
asoc(rd(X1,X2),X2,sFlat0) = mult(i(mult(sFlat0,X1)),mult(mult(rd(X1,X2),X2),sFlat0)),
inference(cp,[status(thm)],[t10078,t7733]) ).
cnf(t453,plain,
i(mult(i(X1),X2)) = mult(X1,i(X2)),
inference(cp,[status(thm)],[t214,t451]) ).
cnf(t528,plain,
i(mult(i(X1),X2)) = mult(X1,i(X2)),
inference(orient,[status(thm)],[t453]) ).
cnf(t582,plain,
i(X1) = mult(rd(X2,X1),i(X2)),
inference(cp,[status(thm)],[t579,t23]) ).
cnf(t648,plain,
mult(rd(X1,X2),i(X1)) = i(X2),
inference(orient,[status(thm)],[t582]) ).
cnf(t1811,plain,
rd(sFlat0,rd(X1,mult(i(sFlat0),X2))) = rd(X2,X1),
inference(cp,[status(thm)],[t1799,t489]) ).
cnf(t454,plain,
i(mult(X1,i(X2))) = mult(i(X1),X2),
inference(cp,[status(thm)],[t214,t451]) ).
cnf(t556,plain,
i(mult(X1,i(X2))) = mult(i(X1),X2),
inference(orient,[status(thm)],[t454]) ).
cnf(t1150,plain,
mult(i(sFlat0),X1) = i(rd(sFlat0,X1)),
inference(cp,[status(thm)],[t556,t1136]) ).
cnf(t10583,plain,
mult(i(sFlat0),X1) = rd(X1,sFlat0),
inference(step,[status(thm)],[t1150,t477]) ).
cnf(t1179,plain,
mult(i(sFlat0),X1) = rd(X1,sFlat0),
inference(orient,[status(thm)],[t10583]) ).
cnf(t10703,plain,
rd(sFlat0,rd(X1,rd(X2,sFlat0))) = rd(X2,X1),
inference(step,[status(thm)],[t1811,t1179]) ).
cnf(t5106,plain,
rd(sFlat0,rd(X1,rd(X2,sFlat0))) = rd(X2,X1),
inference(orient,[status(thm)],[t10703]) ).
cnf(t5116,plain,
rd(X1,mult(X2,rd(X1,sFlat0))) = rd(sFlat0,X2),
inference(cp,[status(thm)],[t5106,t28]) ).
cnf(t7195,plain,
rd(X1,mult(X2,rd(X1,sFlat0))) = rd(sFlat0,X2),
inference(orient,[status(thm)],[t5116]) ).
cnf(t7247,plain,
i(mult(X1,rd(X2,sFlat0))) = mult(rd(sFlat0,X1),i(X2)),
inference(cp,[status(thm)],[t648,t7195]) ).
cnf(t1143,plain,
mult(sFlat0,mult(i(X1),X2)) = mult(rd(sFlat0,X1),X2),
inference(cp,[status(thm)],[t724,t1136]) ).
cnf(t2220,plain,
mult(sFlat0,mult(i(X1),X2)) = mult(rd(sFlat0,X1),X2),
inference(orient,[status(thm)],[t1143]) ).
cnf(t2222,plain,
mult(rd(sFlat0,X1),i(X2)) = mult(sFlat0,i(mult(X1,X2))),
inference(cp,[status(thm)],[t2220,t214]) ).
cnf(t10637,plain,
mult(rd(sFlat0,X1),i(X2)) = rd(sFlat0,mult(X1,X2)),
inference(step,[status(thm)],[t2222,t1136]) ).
cnf(t2714,plain,
mult(rd(sFlat0,X1),i(X2)) = rd(sFlat0,mult(X1,X2)),
inference(orient,[status(thm)],[t10637]) ).
cnf(t10726,plain,
i(mult(X1,rd(X2,sFlat0))) = rd(sFlat0,mult(X1,X2)),
inference(step,[status(thm)],[t7247,t2714]) ).
cnf(t7264,plain,
i(mult(X1,rd(X2,sFlat0))) = rd(sFlat0,mult(X1,X2)),
inference(orient,[status(thm)],[t10726]) ).
cnf(t7314,plain,
mult(X1,rd(X2,sFlat0)) = i(rd(sFlat0,mult(X1,X2))),
inference(cp,[status(thm)],[t451,t7264]) ).
cnf(t10727,plain,
mult(X1,rd(X2,sFlat0)) = rd(mult(X1,X2),sFlat0),
inference(step,[status(thm)],[t7314,t477]) ).
cnf(t7353,plain,
mult(X1,rd(X2,sFlat0)) = rd(mult(X1,X2),sFlat0),
inference(orient,[status(thm)],[t10727]) ).
cnf(t7392,plain,
mult(X1,i(rd(X2,sFlat0))) = i(rd(mult(i(X1),X2),sFlat0)),
inference(cp,[status(thm)],[t528,t7353]) ).
cnf(t10728,plain,
mult(X1,rd(sFlat0,X2)) = i(rd(mult(i(X1),X2),sFlat0)),
inference(step,[status(thm)],[t7392,t477]) ).
cnf(t10729,plain,
mult(X1,rd(sFlat0,X2)) = rd(sFlat0,mult(i(X1),X2)),
inference(step,[status(thm)],[t10728,t477]) ).
cnf(t7413,plain,
rd(sFlat0,mult(i(X1),X2)) = mult(X1,rd(sFlat0,X2)),
inference(orient,[status(thm)],[t10729]) ).
cnf(t7451,plain,
mult(i(X1),rd(sFlat0,X2)) = rd(sFlat0,mult(X1,X2)),
inference(cp,[status(thm)],[t7413,t451]) ).
cnf(t7480,plain,
mult(i(X1),rd(sFlat0,X2)) = rd(sFlat0,mult(X1,X2)),
inference(orient,[status(thm)],[t7451]) ).
cnf(t7494,plain,
rd(sFlat0,mult(X1,i(X2))) = mult(i(X1),mult(sFlat0,X2)),
inference(cp,[status(thm)],[t7480,t1123]) ).
cnf(t2731,plain,
rd(sFlat0,mult(X1,i(X2))) = mult(rd(sFlat0,X1),X2),
inference(cp,[status(thm)],[t2714,t451]) ).
cnf(t2830,plain,
rd(sFlat0,mult(X1,i(X2))) = mult(rd(sFlat0,X1),X2),
inference(orient,[status(thm)],[t2731]) ).
cnf(t10730,plain,
mult(rd(sFlat0,X1),X2) = mult(i(X1),mult(sFlat0,X2)),
inference(step,[status(thm)],[t7494,t2830]) ).
cnf(t7548,plain,
mult(i(X1),mult(sFlat0,X2)) = mult(rd(sFlat0,X1),X2),
inference(orient,[status(thm)],[t10730]) ).
cnf(t7568,plain,
mult(rd(sFlat0,X1),X2) = mult(i(X1),mult(X2,sFlat0)),
inference(cp,[status(thm)],[t7548,t1494]) ).
cnf(t7609,plain,
mult(i(X1),mult(X2,sFlat0)) = mult(rd(sFlat0,X1),X2),
inference(orient,[status(thm)],[t7568]) ).
cnf(t10828,plain,
asoc(rd(X1,X2),X2,sFlat0) = mult(rd(sFlat0,mult(sFlat0,X1)),mult(rd(X1,X2),X2)),
inference(step,[status(thm)],[t10112,t7609]) ).
cnf(t1137,plain,
rd(sFlat0,mult(sFlat0,X1)) = i(X1),
inference(cp,[status(thm)],[t1136,t579]) ).
cnf(t1481,plain,
rd(sFlat0,mult(sFlat0,X1)) = i(X1),
inference(orient,[status(thm)],[t1137]) ).
cnf(t10829,plain,
asoc(rd(X1,X2),X2,sFlat0) = mult(i(X1),mult(rd(X1,X2),X2)),
inference(step,[status(thm)],[t10828,t1481]) ).
cnf(t10830,plain,
asoc(rd(X1,X2),X2,sFlat0) = mult(i(X1),X1),
inference(step,[status(thm)],[t10829,t23]) ).
cnf(t10831,plain,
asoc(rd(X1,X2),X2,sFlat0) = unit,
inference(step,[status(thm)],[t10830,t60]) ).
cnf(t10491,plain,
asoc(rd(X1,X2),X2,sFlat0) = unit,
inference(orient,[status(thm)],[t10831]) ).
cnf(t10548,plain,
unit = asoc(X1,X2,sFlat0),
inference(cp,[status(thm)],[t10491,t28]) ).
cnf(t10563,plain,
asoc(X1,X2,sFlat0) = unit,
inference(orient,[status(thm)],[t10548]) ).
cnf(goal_0,negated_conjecture,
asoc(a,b,asoc(c,d,e)) != unit,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
asoc(a,b,sFlat0) != unit,
inference(rw,[status(thm)],[goal_0,t442]) ).
cnf(g0_1,plain,
unit != unit,
inference(rw,[status(thm)],[g0_0,t10563]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP727-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:34 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 10.20/1.92 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 10.20/1.92 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------