%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP654-11 : TPTP v9.3.1. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n011.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:27:50 PM UTC 2026
% Result : Unsatisfiable 24.61s 3.69s
% Output : CNFRefutation 24.61s
% Verified :
% SZS Type : Refutation
% Derivation depth : 106
% Number of leaves : 8
% Syntax : Number of clauses : 243 ( 243 unt; 0 nHn; 84 RR)
% Number of literals : 243 ( 242 equ; 5 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 : 7 ( 7 usr; 4 con; 0-2 aty)
% Number of variables : 233 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t1,axiom,
mult(X1,ld(X1,X2)) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t7,plain,
mult(X1,ld(X1,X2)) = X2,
inference(orient,[status(thm)],[t1]) ).
cnf(t3,axiom,
rd(mult(X1,X2),X2) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t9,plain,
rd(mult(X1,X2),X2) = X1,
inference(orient,[status(thm)],[t3]) ).
cnf(t4,axiom,
mult(mult(mult(X1,X2),X1),X3) = mult(X1,mult(X2,mult(X1,X3))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t13,plain,
mult(mult(mult(X1,X2),X1),X3) = mult(X1,mult(X2,mult(X1,X3))),
inference(orient,[status(thm)],[t4]) ).
cnf(t15,plain,
mult(X1,mult(ld(X1,X2),mult(X1,X3))) = mult(mult(X2,X1),X3),
inference(cp,[status(thm)],[t13,t7]) ).
cnf(t147,plain,
mult(X1,mult(ld(X1,X2),mult(X1,X3))) = mult(mult(X2,X1),X3),
inference(orient,[status(thm)],[t15]) ).
cnf(t159,plain,
mult(mult(X1,X2),ld(X2,X3)) = mult(X2,mult(ld(X2,X1),X3)),
inference(cp,[status(thm)],[t147,t7]) ).
cnf(t1102,plain,
mult(mult(X1,X2),ld(X2,X3)) = mult(X2,mult(ld(X2,X1),X3)),
inference(orient,[status(thm)],[t159]) ).
cnf(t2,axiom,
mult(rd(X1,X2),X2) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t8,plain,
mult(rd(X1,X2),X2) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t14,plain,
mult(X1,mult(X2,mult(X1,ld(mult(mult(X1,X2),X1),X3)))) = X3,
inference(cp,[status(thm)],[t13,t7]) ).
cnf(t239,plain,
mult(X1,mult(X2,mult(X1,ld(mult(mult(X1,X2),X1),X3)))) = X3,
inference(orient,[status(thm)],[t14]) ).
cnf(t0,axiom,
ld(X1,mult(X1,X2)) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t11,plain,
ld(X1,mult(X1,X2)) = X2,
inference(orient,[status(thm)],[t0]) ).
cnf(t5,axiom,
sFlat0 = rd(x1,x1),
introduced(definition) ).
cnf(t25,plain,
rd(x1,x1) = sFlat0,
inference(orient,[status(thm)],[t5]) ).
cnf(t26,plain,
x1 = mult(sFlat0,x1),
inference(cp,[status(thm)],[t8,t25]) ).
cnf(t28,plain,
mult(sFlat0,x1) = x1,
inference(orient,[status(thm)],[t26]) ).
cnf(t167,plain,
mult(mult(X1,sFlat0),x1) = mult(sFlat0,mult(ld(sFlat0,X1),x1)),
inference(cp,[status(thm)],[t147,t28]) ).
cnf(t197,plain,
mult(sFlat0,mult(ld(sFlat0,X1),x1)) = mult(mult(X1,sFlat0),x1),
inference(orient,[status(thm)],[t167]) ).
cnf(t201,plain,
mult(ld(sFlat0,X1),x1) = ld(sFlat0,mult(mult(X1,sFlat0),x1)),
inference(cp,[status(thm)],[t11,t197]) ).
cnf(t218,plain,
ld(sFlat0,mult(mult(X1,sFlat0),x1)) = mult(ld(sFlat0,X1),x1),
inference(orient,[status(thm)],[t201]) ).
cnf(t223,plain,
mult(ld(sFlat0,rd(X1,sFlat0)),x1) = ld(sFlat0,mult(X1,x1)),
inference(cp,[status(thm)],[t218,t8]) ).
cnf(t287,plain,
mult(ld(sFlat0,rd(X1,sFlat0)),x1) = ld(sFlat0,mult(X1,x1)),
inference(orient,[status(thm)],[t223]) ).
cnf(t290,plain,
ld(sFlat0,rd(X1,sFlat0)) = rd(ld(sFlat0,mult(X1,x1)),x1),
inference(cp,[status(thm)],[t9,t287]) ).
cnf(t362,plain,
rd(ld(sFlat0,mult(X1,x1)),x1) = ld(sFlat0,rd(X1,sFlat0)),
inference(orient,[status(thm)],[t290]) ).
cnf(t363,plain,
ld(sFlat0,rd(sFlat0,sFlat0)) = rd(x1,x1),
inference(cp,[status(thm)],[t362,t11]) ).
cnf(t23690,plain,
ld(sFlat0,rd(sFlat0,sFlat0)) = sFlat0,
inference(step,[status(thm)],[t363,t25]) ).
cnf(t371,plain,
ld(sFlat0,rd(sFlat0,sFlat0)) = sFlat0,
inference(orient,[status(thm)],[t23690]) ).
cnf(t372,plain,
rd(sFlat0,sFlat0) = mult(sFlat0,sFlat0),
inference(cp,[status(thm)],[t7,t371]) ).
cnf(t379,plain,
mult(sFlat0,sFlat0) = rd(sFlat0,sFlat0),
inference(orient,[status(thm)],[t372]) ).
cnf(t389,plain,
X1 = mult(sFlat0,mult(sFlat0,mult(sFlat0,ld(mult(rd(sFlat0,sFlat0),sFlat0),X1)))),
inference(cp,[status(thm)],[t239,t379]) ).
cnf(t23691,plain,
X1 = mult(sFlat0,mult(sFlat0,mult(sFlat0,ld(sFlat0,X1)))),
inference(step,[status(thm)],[t389,t8]) ).
cnf(t23692,plain,
X1 = mult(sFlat0,mult(sFlat0,X1)),
inference(step,[status(thm)],[t23691,t7]) ).
cnf(t392,plain,
mult(sFlat0,mult(sFlat0,X1)) = X1,
inference(orient,[status(thm)],[t23692]) ).
cnf(t404,plain,
mult(mult(X1,sFlat0),mult(sFlat0,X2)) = mult(sFlat0,mult(ld(sFlat0,X1),X2)),
inference(cp,[status(thm)],[t147,t392]) ).
cnf(t397,plain,
ld(sFlat0,X1) = mult(sFlat0,X1),
inference(cp,[status(thm)],[t392,t7]) ).
cnf(t409,plain,
ld(sFlat0,X1) = mult(sFlat0,X1),
inference(orient,[status(thm)],[t397]) ).
cnf(t23755,plain,
mult(mult(X1,sFlat0),mult(sFlat0,X2)) = mult(sFlat0,mult(mult(sFlat0,X1),X2)),
inference(step,[status(thm)],[t404,t409]) ).
cnf(t1679,plain,
mult(mult(X1,sFlat0),mult(sFlat0,X2)) = mult(sFlat0,mult(mult(sFlat0,X1),X2)),
inference(orient,[status(thm)],[t23755]) ).
cnf(t1703,plain,
mult(sFlat0,mult(mult(sFlat0,X1),sFlat0)) = mult(mult(X1,sFlat0),rd(sFlat0,sFlat0)),
inference(cp,[status(thm)],[t1679,t379]) ).
cnf(t23711,plain,
rd(mult(sFlat0,mult(X1,x1)),x1) = ld(sFlat0,rd(X1,sFlat0)),
inference(step,[status(thm)],[t362,t409]) ).
cnf(t23712,plain,
rd(mult(sFlat0,mult(X1,x1)),x1) = mult(sFlat0,rd(X1,sFlat0)),
inference(step,[status(thm)],[t23711,t409]) ).
cnf(t427,plain,
rd(mult(sFlat0,mult(X1,x1)),x1) = mult(sFlat0,rd(X1,sFlat0)),
inference(rw,[status(thm)],[t23712]) ).
cnf(t533,plain,
rd(mult(sFlat0,mult(X1,x1)),x1) = mult(sFlat0,rd(X1,sFlat0)),
inference(orient,[status(thm)],[t427]) ).
cnf(t23717,plain,
mult(sFlat0,mult(mult(sFlat0,X1),x1)) = mult(mult(X1,sFlat0),x1),
inference(step,[status(thm)],[t197,t409]) ).
cnf(t430,plain,
mult(sFlat0,mult(mult(sFlat0,X1),x1)) = mult(mult(X1,sFlat0),x1),
inference(rw,[status(thm)],[t23717]) ).
cnf(t631,plain,
mult(sFlat0,mult(mult(sFlat0,X1),x1)) = mult(mult(X1,sFlat0),x1),
inference(orient,[status(thm)],[t430]) ).
cnf(t649,plain,
mult(sFlat0,rd(mult(sFlat0,X1),sFlat0)) = rd(mult(mult(X1,sFlat0),x1),x1),
inference(cp,[status(thm)],[t533,t631]) ).
cnf(t23735,plain,
mult(sFlat0,rd(mult(sFlat0,X1),sFlat0)) = mult(X1,sFlat0),
inference(step,[status(thm)],[t649,t9]) ).
cnf(t655,plain,
mult(sFlat0,rd(mult(sFlat0,X1),sFlat0)) = mult(X1,sFlat0),
inference(orient,[status(thm)],[t23735]) ).
cnf(t670,plain,
rd(mult(sFlat0,X1),sFlat0) = mult(sFlat0,mult(X1,sFlat0)),
inference(cp,[status(thm)],[t392,t655]) ).
cnf(t702,plain,
mult(sFlat0,mult(X1,sFlat0)) = rd(mult(sFlat0,X1),sFlat0),
inference(orient,[status(thm)],[t670]) ).
cnf(t23756,plain,
rd(mult(sFlat0,mult(sFlat0,X1)),sFlat0) = mult(mult(X1,sFlat0),rd(sFlat0,sFlat0)),
inference(step,[status(thm)],[t1703,t702]) ).
cnf(t23757,plain,
rd(X1,sFlat0) = mult(mult(X1,sFlat0),rd(sFlat0,sFlat0)),
inference(step,[status(thm)],[t23756,t392]) ).
cnf(t1723,plain,
mult(mult(X1,sFlat0),rd(sFlat0,sFlat0)) = rd(X1,sFlat0),
inference(orient,[status(thm)],[t23757]) ).
cnf(t1139,plain,
mult(x1,mult(ld(x1,sFlat0),X1)) = mult(x1,ld(x1,X1)),
inference(cp,[status(thm)],[t1102,t28]) ).
cnf(t23745,plain,
mult(x1,mult(ld(x1,sFlat0),X1)) = X1,
inference(step,[status(thm)],[t1139,t7]) ).
cnf(t1178,plain,
mult(x1,mult(ld(x1,sFlat0),X1)) = X1,
inference(orient,[status(thm)],[t23745]) ).
cnf(t1183,plain,
mult(ld(x1,sFlat0),X1) = ld(x1,X1),
inference(cp,[status(thm)],[t11,t1178]) ).
cnf(t1194,plain,
mult(ld(x1,sFlat0),X1) = ld(x1,X1),
inference(orient,[status(thm)],[t1183]) ).
cnf(t1725,plain,
rd(ld(x1,sFlat0),sFlat0) = mult(ld(x1,sFlat0),rd(sFlat0,sFlat0)),
inference(cp,[status(thm)],[t1723,t1194]) ).
cnf(t1199,plain,
ld(x1,sFlat0) = rd(ld(x1,X1),X1),
inference(cp,[status(thm)],[t9,t1194]) ).
cnf(t1220,plain,
rd(ld(x1,X1),X1) = ld(x1,sFlat0),
inference(orient,[status(thm)],[t1199]) ).
cnf(t23758,plain,
ld(x1,sFlat0) = mult(ld(x1,sFlat0),rd(sFlat0,sFlat0)),
inference(step,[status(thm)],[t1725,t1220]) ).
cnf(t23759,plain,
ld(x1,sFlat0) = ld(x1,rd(sFlat0,sFlat0)),
inference(step,[status(thm)],[t23758,t1194]) ).
cnf(t1741,plain,
ld(x1,rd(sFlat0,sFlat0)) = ld(x1,sFlat0),
inference(orient,[status(thm)],[t23759]) ).
cnf(t1742,plain,
rd(sFlat0,sFlat0) = mult(x1,ld(x1,sFlat0)),
inference(cp,[status(thm)],[t7,t1741]) ).
cnf(t23761,plain,
rd(sFlat0,sFlat0) = sFlat0,
inference(step,[status(thm)],[t1742,t7]) ).
cnf(t1748,plain,
rd(sFlat0,sFlat0) = sFlat0,
inference(orient,[status(thm)],[t23761]) ).
cnf(t23772,plain,
mult(mult(X1,sFlat0),sFlat0) = rd(X1,sFlat0),
inference(step,[status(thm)],[t1723,t1748]) ).
cnf(t1760,plain,
mult(mult(X1,sFlat0),sFlat0) = rd(X1,sFlat0),
inference(rw,[status(thm)],[t23772]) ).
cnf(t1793,plain,
mult(mult(X1,sFlat0),sFlat0) = rd(X1,sFlat0),
inference(orient,[status(thm)],[t1760]) ).
cnf(t1146,plain,
mult(X1,mult(ld(X1,rd(X2,X1)),X3)) = mult(X2,ld(X1,X3)),
inference(cp,[status(thm)],[t1102,t8]) ).
cnf(t5860,plain,
mult(X1,mult(ld(X1,rd(X2,X1)),X3)) = mult(X2,ld(X1,X3)),
inference(orient,[status(thm)],[t1146]) ).
cnf(t5961,plain,
mult(ld(X1,rd(X2,X1)),X3) = ld(X1,mult(X2,ld(X1,X3))),
inference(cp,[status(thm)],[t11,t5860]) ).
cnf(t6015,plain,
ld(X1,mult(X2,ld(X1,X3))) = mult(ld(X1,rd(X2,X1)),X3),
inference(orient,[status(thm)],[t5961]) ).
cnf(t6016,plain,
mult(ld(X1,rd(X1,X1)),X2) = ld(X1,X2),
inference(cp,[status(thm)],[t6015,t11]) ).
cnf(t6133,plain,
mult(ld(X1,rd(X1,X1)),X2) = ld(X1,X2),
inference(orient,[status(thm)],[t6016]) ).
cnf(t6142,plain,
rd(ld(X1,rd(X1,X1)),sFlat0) = mult(ld(X1,sFlat0),sFlat0),
inference(cp,[status(thm)],[t1793,t6133]) ).
cnf(t6234,plain,
rd(ld(X1,rd(X1,X1)),sFlat0) = mult(ld(X1,sFlat0),sFlat0),
inference(orient,[status(thm)],[t6142]) ).
cnf(t6238,plain,
ld(X1,rd(X1,X1)) = mult(mult(ld(X1,sFlat0),sFlat0),sFlat0),
inference(cp,[status(thm)],[t8,t6234]) ).
cnf(t24028,plain,
ld(X1,rd(X1,X1)) = rd(ld(X1,sFlat0),sFlat0),
inference(step,[status(thm)],[t6238,t1793]) ).
cnf(t6249,plain,
ld(X1,rd(X1,X1)) = rd(ld(X1,sFlat0),sFlat0),
inference(orient,[status(thm)],[t24028]) ).
cnf(t6251,plain,
rd(X1,X1) = mult(X1,rd(ld(X1,sFlat0),sFlat0)),
inference(cp,[status(thm)],[t7,t6249]) ).
cnf(t6263,plain,
mult(X1,rd(ld(X1,sFlat0),sFlat0)) = rd(X1,X1),
inference(orient,[status(thm)],[t6251]) ).
cnf(t10,plain,
X1 = rd(X2,ld(X1,X2)),
inference(cp,[status(thm)],[t9,t7]) ).
cnf(t38,plain,
rd(X1,ld(X2,X1)) = X2,
inference(orient,[status(thm)],[t10]) ).
cnf(t24029,plain,
mult(rd(ld(X1,sFlat0),sFlat0),X2) = ld(X1,X2),
inference(step,[status(thm)],[t6133,t6249]) ).
cnf(t6262,plain,
mult(rd(ld(X1,sFlat0),sFlat0),X2) = ld(X1,X2),
inference(rw,[status(thm)],[t24029]) ).
cnf(t6295,plain,
mult(rd(ld(X1,sFlat0),sFlat0),X2) = ld(X1,X2),
inference(orient,[status(thm)],[t6262]) ).
cnf(t12,plain,
X1 = ld(rd(X2,X1),X2),
inference(cp,[status(thm)],[t11,t8]) ).
cnf(t39,plain,
ld(rd(X1,X2),X1) = X2,
inference(orient,[status(thm)],[t12]) ).
cnf(t6303,plain,
ld(rd(sFlat0,X1),X2) = mult(rd(X1,sFlat0),X2),
inference(cp,[status(thm)],[t6295,t39]) ).
cnf(t6339,plain,
ld(rd(sFlat0,X1),X2) = mult(rd(X1,sFlat0),X2),
inference(orient,[status(thm)],[t6303]) ).
cnf(t6348,plain,
rd(sFlat0,X1) = rd(X2,mult(rd(X1,sFlat0),X2)),
inference(cp,[status(thm)],[t38,t6339]) ).
cnf(t6353,plain,
rd(X1,mult(rd(X2,sFlat0),X1)) = rd(sFlat0,X2),
inference(orient,[status(thm)],[t6348]) ).
cnf(t6359,plain,
rd(sFlat0,X1) = rd(ld(rd(X1,sFlat0),X2),X2),
inference(cp,[status(thm)],[t6353,t7]) ).
cnf(t6379,plain,
rd(ld(rd(X1,sFlat0),X2),X2) = rd(sFlat0,X1),
inference(orient,[status(thm)],[t6359]) ).
cnf(t6394,plain,
rd(sFlat0,mult(X1,sFlat0)) = rd(ld(X1,X2),X2),
inference(cp,[status(thm)],[t6379,t9]) ).
cnf(t6417,plain,
rd(ld(X1,X2),X2) = rd(sFlat0,mult(X1,sFlat0)),
inference(orient,[status(thm)],[t6394]) ).
cnf(t24033,plain,
mult(X1,rd(sFlat0,mult(X1,sFlat0))) = rd(X1,X1),
inference(step,[status(thm)],[t6263,t6417]) ).
cnf(t6485,plain,
mult(X1,rd(sFlat0,mult(X1,sFlat0))) = rd(X1,X1),
inference(rw,[status(thm)],[t24033]) ).
cnf(t6724,plain,
mult(X1,rd(sFlat0,mult(X1,sFlat0))) = rd(X1,X1),
inference(orient,[status(thm)],[t6485]) ).
cnf(t6760,plain,
mult(rd(sFlat0,mult(X1,sFlat0)),mult(ld(rd(sFlat0,mult(X1,sFlat0)),X1),X2)) = mult(rd(X1,X1),ld(rd(sFlat0,mult(X1,sFlat0)),X2)),
inference(cp,[status(thm)],[t1102,t6724]) ).
cnf(t6467,plain,
ld(X1,X2) = mult(rd(sFlat0,mult(X1,sFlat0)),X2),
inference(cp,[status(thm)],[t8,t6417]) ).
cnf(t6658,plain,
mult(rd(sFlat0,mult(X1,sFlat0)),X2) = ld(X1,X2),
inference(orient,[status(thm)],[t6467]) ).
cnf(t24052,plain,
ld(X1,mult(ld(rd(sFlat0,mult(X1,sFlat0)),X1),X2)) = mult(rd(X1,X1),ld(rd(sFlat0,mult(X1,sFlat0)),X2)),
inference(step,[status(thm)],[t6760,t6658]) ).
cnf(t24053,plain,
ld(X1,mult(mult(rd(mult(X1,sFlat0),sFlat0),X1),X2)) = mult(rd(X1,X1),ld(rd(sFlat0,mult(X1,sFlat0)),X2)),
inference(step,[status(thm)],[t24052,t6339]) ).
cnf(t175,plain,
mult(ld(X1,X2),mult(X1,X3)) = ld(X1,mult(mult(X2,X1),X3)),
inference(cp,[status(thm)],[t11,t147]) ).
cnf(t1371,plain,
ld(X1,mult(mult(X2,X1),X3)) = mult(ld(X1,X2),mult(X1,X3)),
inference(orient,[status(thm)],[t175]) ).
cnf(t24054,plain,
mult(ld(X1,rd(mult(X1,sFlat0),sFlat0)),mult(X1,X2)) = mult(rd(X1,X1),ld(rd(sFlat0,mult(X1,sFlat0)),X2)),
inference(step,[status(thm)],[t24053,t1371]) ).
cnf(t24055,plain,
mult(ld(X1,X1),mult(X1,X2)) = mult(rd(X1,X1),ld(rd(sFlat0,mult(X1,sFlat0)),X2)),
inference(step,[status(thm)],[t24054,t9]) ).
cnf(t24056,plain,
mult(ld(X1,X1),mult(X1,X2)) = mult(rd(X1,X1),mult(rd(mult(X1,sFlat0),sFlat0),X2)),
inference(step,[status(thm)],[t24055,t6339]) ).
cnf(t24057,plain,
mult(ld(X1,X1),mult(X1,X2)) = mult(rd(X1,X1),mult(X1,X2)),
inference(step,[status(thm)],[t24056,t9]) ).
cnf(t7733,plain,
mult(ld(X1,X1),mult(X1,X2)) = mult(rd(X1,X1),mult(X1,X2)),
inference(orient,[status(thm)],[t24057]) ).
cnf(t7804,plain,
ld(X1,X1) = rd(mult(rd(X1,X1),mult(X1,X2)),mult(X1,X2)),
inference(cp,[status(thm)],[t9,t7733]) ).
cnf(t24058,plain,
ld(X1,X1) = rd(X1,X1),
inference(step,[status(thm)],[t7804,t9]) ).
cnf(t7827,plain,
ld(X1,X1) = rd(X1,X1),
inference(orient,[status(thm)],[t24058]) ).
cnf(t7830,plain,
X1 = mult(X1,rd(X1,X1)),
inference(cp,[status(thm)],[t7,t7827]) ).
cnf(t7840,plain,
mult(X1,rd(X1,X1)) = X1,
inference(orient,[status(thm)],[t7830]) ).
cnf(t19,plain,
mult(mult(X1,X2),mult(X1,mult(mult(X1,X2),X3))) = mult(mult(X1,mult(X2,mult(X1,mult(X1,X2)))),X3),
inference(cp,[status(thm)],[t13,t13]) ).
cnf(t3114,plain,
mult(mult(X1,mult(X2,mult(X1,mult(X1,X2)))),X3) = mult(mult(X1,X2),mult(X1,mult(mult(X1,X2),X3))),
inference(orient,[status(thm)],[t19]) ).
cnf(t660,plain,
mult(mult(sFlat0,X1),sFlat0) = mult(sFlat0,rd(X1,sFlat0)),
inference(cp,[status(thm)],[t655,t392]) ).
cnf(t680,plain,
mult(mult(sFlat0,X1),sFlat0) = mult(sFlat0,rd(X1,sFlat0)),
inference(orient,[status(thm)],[t660]) ).
cnf(t3116,plain,
mult(mult(sFlat0,X1),mult(sFlat0,mult(mult(sFlat0,X1),sFlat0))) = mult(sFlat0,rd(mult(X1,mult(sFlat0,mult(sFlat0,X1))),sFlat0)),
inference(cp,[status(thm)],[t3114,t680]) ).
cnf(t398,plain,
mult(ld(sFlat0,X1),mult(sFlat0,X2)) = mult(sFlat0,mult(mult(X1,sFlat0),X2)),
inference(cp,[status(thm)],[t392,t147]) ).
cnf(t23754,plain,
mult(mult(sFlat0,X1),mult(sFlat0,X2)) = mult(sFlat0,mult(mult(X1,sFlat0),X2)),
inference(step,[status(thm)],[t398,t409]) ).
cnf(t1619,plain,
mult(mult(sFlat0,X1),mult(sFlat0,X2)) = mult(sFlat0,mult(mult(X1,sFlat0),X2)),
inference(orient,[status(thm)],[t23754]) ).
cnf(t23976,plain,
mult(sFlat0,mult(mult(X1,sFlat0),mult(mult(sFlat0,X1),sFlat0))) = mult(sFlat0,rd(mult(X1,mult(sFlat0,mult(sFlat0,X1))),sFlat0)),
inference(step,[status(thm)],[t3116,t1619]) ).
cnf(t23977,plain,
mult(sFlat0,mult(mult(X1,sFlat0),mult(sFlat0,rd(X1,sFlat0)))) = mult(sFlat0,rd(mult(X1,mult(sFlat0,mult(sFlat0,X1))),sFlat0)),
inference(step,[status(thm)],[t23976,t680]) ).
cnf(t23978,plain,
mult(sFlat0,mult(sFlat0,mult(mult(sFlat0,X1),rd(X1,sFlat0)))) = mult(sFlat0,rd(mult(X1,mult(sFlat0,mult(sFlat0,X1))),sFlat0)),
inference(step,[status(thm)],[t23977,t1679]) ).
cnf(t23979,plain,
mult(mult(sFlat0,X1),rd(X1,sFlat0)) = mult(sFlat0,rd(mult(X1,mult(sFlat0,mult(sFlat0,X1))),sFlat0)),
inference(step,[status(thm)],[t23978,t392]) ).
cnf(t23980,plain,
mult(mult(sFlat0,X1),rd(X1,sFlat0)) = mult(sFlat0,rd(mult(X1,X1),sFlat0)),
inference(step,[status(thm)],[t23979,t392]) ).
cnf(t4735,plain,
mult(mult(sFlat0,X1),rd(X1,sFlat0)) = mult(sFlat0,rd(mult(X1,X1),sFlat0)),
inference(orient,[status(thm)],[t23980]) ).
cnf(t6,axiom,
sFlat1 = mult(x0,rd(x1,x1)),
introduced(definition) ).
cnf(t21,plain,
mult(x0,rd(x1,x1)) = sFlat1,
inference(orient,[status(thm)],[t6]) ).
cnf(t23687,plain,
mult(x0,sFlat0) = sFlat1,
inference(step,[status(thm)],[t21,t25]) ).
cnf(t27,plain,
mult(x0,sFlat0) = sFlat1,
inference(rw,[status(thm)],[t23687]) ).
cnf(t31,plain,
mult(x0,sFlat0) = sFlat1,
inference(orient,[status(thm)],[t27]) ).
cnf(t1118,plain,
mult(sFlat0,mult(ld(sFlat0,x0),X1)) = mult(sFlat1,ld(sFlat0,X1)),
inference(cp,[status(thm)],[t1102,t31]) ).
cnf(t23746,plain,
mult(sFlat0,mult(mult(sFlat0,x0),X1)) = mult(sFlat1,ld(sFlat0,X1)),
inference(step,[status(thm)],[t1118,t409]) ).
cnf(t23747,plain,
mult(sFlat0,mult(mult(sFlat0,x0),X1)) = mult(sFlat1,mult(sFlat0,X1)),
inference(step,[status(thm)],[t23746,t409]) ).
cnf(t1231,plain,
mult(sFlat0,mult(mult(sFlat0,x0),X1)) = mult(sFlat1,mult(sFlat0,X1)),
inference(orient,[status(thm)],[t23747]) ).
cnf(t1235,plain,
mult(sFlat1,mult(sFlat0,ld(mult(sFlat0,x0),X1))) = mult(sFlat0,X1),
inference(cp,[status(thm)],[t1231,t7]) ).
cnf(t5154,plain,
mult(sFlat1,mult(sFlat0,ld(mult(sFlat0,x0),X1))) = mult(sFlat0,X1),
inference(orient,[status(thm)],[t1235]) ).
cnf(t5158,plain,
mult(sFlat0,ld(mult(sFlat0,x0),X1)) = ld(sFlat1,mult(sFlat0,X1)),
inference(cp,[status(thm)],[t11,t5154]) ).
cnf(t5170,plain,
mult(sFlat0,ld(mult(sFlat0,x0),X1)) = ld(sFlat1,mult(sFlat0,X1)),
inference(orient,[status(thm)],[t5158]) ).
cnf(t5184,plain,
ld(mult(sFlat0,x0),X1) = mult(sFlat0,ld(sFlat1,mult(sFlat0,X1))),
inference(cp,[status(thm)],[t392,t5170]) ).
cnf(t5212,plain,
mult(sFlat0,ld(sFlat1,mult(sFlat0,X1))) = ld(mult(sFlat0,x0),X1),
inference(orient,[status(thm)],[t5184]) ).
cnf(t5230,plain,
ld(mult(sFlat0,x0),mult(sFlat0,X1)) = mult(sFlat0,ld(sFlat1,X1)),
inference(cp,[status(thm)],[t5212,t392]) ).
cnf(t5311,plain,
ld(mult(sFlat0,x0),mult(sFlat0,X1)) = mult(sFlat0,ld(sFlat1,X1)),
inference(orient,[status(thm)],[t5230]) ).
cnf(t7829,plain,
rd(mult(sFlat0,x0),mult(sFlat0,x0)) = mult(sFlat0,ld(sFlat1,x0)),
inference(cp,[status(thm)],[t7827,t5311]) ).
cnf(t8129,plain,
rd(mult(sFlat0,x0),mult(sFlat0,x0)) = mult(sFlat0,ld(sFlat1,x0)),
inference(orient,[status(thm)],[t7829]) ).
cnf(t8136,plain,
mult(sFlat0,x0) = mult(mult(sFlat0,ld(sFlat1,x0)),mult(sFlat0,x0)),
inference(cp,[status(thm)],[t8,t8129]) ).
cnf(t24086,plain,
mult(sFlat0,x0) = mult(sFlat0,mult(mult(ld(sFlat1,x0),sFlat0),x0)),
inference(step,[status(thm)],[t8136,t1619]) ).
cnf(t9615,plain,
mult(sFlat0,mult(mult(ld(sFlat1,x0),sFlat0),x0)) = mult(sFlat0,x0),
inference(orient,[status(thm)],[t24086]) ).
cnf(t9630,plain,
mult(mult(ld(sFlat1,x0),sFlat0),x0) = mult(sFlat0,mult(sFlat0,x0)),
inference(cp,[status(thm)],[t392,t9615]) ).
cnf(t24087,plain,
mult(mult(ld(sFlat1,x0),sFlat0),x0) = x0,
inference(step,[status(thm)],[t9630,t392]) ).
cnf(t9674,plain,
mult(mult(ld(sFlat1,x0),sFlat0),x0) = x0,
inference(orient,[status(thm)],[t24087]) ).
cnf(t9679,plain,
mult(ld(sFlat1,x0),sFlat0) = rd(x0,x0),
inference(cp,[status(thm)],[t9,t9674]) ).
cnf(t9696,plain,
mult(ld(sFlat1,x0),sFlat0) = rd(x0,x0),
inference(orient,[status(thm)],[t9679]) ).
cnf(t9705,plain,
ld(sFlat1,x0) = rd(rd(x0,x0),sFlat0),
inference(cp,[status(thm)],[t9,t9696]) ).
cnf(t9729,plain,
rd(rd(x0,x0),sFlat0) = ld(sFlat1,x0),
inference(orient,[status(thm)],[t9705]) ).
cnf(t9735,plain,
mult(sFlat0,rd(mult(rd(x0,x0),rd(x0,x0)),sFlat0)) = mult(mult(sFlat0,rd(x0,x0)),ld(sFlat1,x0)),
inference(cp,[status(thm)],[t4735,t9729]) ).
cnf(t164,plain,
mult(mult(X1,x0),sFlat0) = mult(x0,mult(ld(x0,X1),sFlat1)),
inference(cp,[status(thm)],[t147,t31]) ).
cnf(t187,plain,
mult(x0,mult(ld(x0,X1),sFlat1)) = mult(mult(X1,x0),sFlat0),
inference(orient,[status(thm)],[t164]) ).
cnf(t191,plain,
mult(ld(x0,X1),sFlat1) = ld(x0,mult(mult(X1,x0),sFlat0)),
inference(cp,[status(thm)],[t11,t187]) ).
cnf(t208,plain,
ld(x0,mult(mult(X1,x0),sFlat0)) = mult(ld(x0,X1),sFlat1),
inference(orient,[status(thm)],[t191]) ).
cnf(t211,plain,
mult(ld(x0,rd(X1,x0)),sFlat1) = ld(x0,mult(X1,sFlat0)),
inference(cp,[status(thm)],[t208,t8]) ).
cnf(t281,plain,
mult(ld(x0,rd(X1,x0)),sFlat1) = ld(x0,mult(X1,sFlat0)),
inference(orient,[status(thm)],[t211]) ).
cnf(t283,plain,
ld(x0,rd(X1,x0)) = rd(ld(x0,mult(X1,sFlat0)),sFlat1),
inference(cp,[status(thm)],[t9,t281]) ).
cnf(t294,plain,
rd(ld(x0,mult(X1,sFlat0)),sFlat1) = ld(x0,rd(X1,x0)),
inference(orient,[status(thm)],[t283]) ).
cnf(t295,plain,
ld(x0,rd(x0,x0)) = rd(sFlat0,sFlat1),
inference(cp,[status(thm)],[t294,t11]) ).
cnf(t301,plain,
ld(x0,rd(x0,x0)) = rd(sFlat0,sFlat1),
inference(orient,[status(thm)],[t295]) ).
cnf(t302,plain,
rd(x0,x0) = mult(x0,rd(sFlat0,sFlat1)),
inference(cp,[status(thm)],[t7,t301]) ).
cnf(t308,plain,
mult(x0,rd(sFlat0,sFlat1)) = rd(x0,x0),
inference(orient,[status(thm)],[t302]) ).
cnf(t1115,plain,
mult(rd(sFlat0,sFlat1),mult(ld(rd(sFlat0,sFlat1),x0),X1)) = mult(rd(x0,x0),ld(rd(sFlat0,sFlat1),X1)),
inference(cp,[status(thm)],[t1102,t308]) ).
cnf(t315,plain,
X1 = mult(x0,mult(rd(sFlat0,sFlat1),mult(x0,ld(mult(rd(x0,x0),x0),X1)))),
inference(cp,[status(thm)],[t239,t308]) ).
cnf(t23688,plain,
X1 = mult(x0,mult(rd(sFlat0,sFlat1),mult(x0,ld(x0,X1)))),
inference(step,[status(thm)],[t315,t8]) ).
cnf(t23689,plain,
X1 = mult(x0,mult(rd(sFlat0,sFlat1),X1)),
inference(step,[status(thm)],[t23688,t7]) ).
cnf(t317,plain,
mult(x0,mult(rd(sFlat0,sFlat1),X1)) = X1,
inference(orient,[status(thm)],[t23689]) ).
cnf(t322,plain,
mult(rd(sFlat0,sFlat1),X1) = ld(x0,X1),
inference(cp,[status(thm)],[t11,t317]) ).
cnf(t334,plain,
mult(rd(sFlat0,sFlat1),X1) = ld(x0,X1),
inference(orient,[status(thm)],[t322]) ).
cnf(t23928,plain,
ld(x0,mult(ld(rd(sFlat0,sFlat1),x0),X1)) = mult(rd(x0,x0),ld(rd(sFlat0,sFlat1),X1)),
inference(step,[status(thm)],[t1115,t334]) ).
cnf(t318,plain,
ld(rd(sFlat0,sFlat1),X1) = mult(x0,X1),
inference(cp,[status(thm)],[t317,t7]) ).
cnf(t330,plain,
ld(rd(sFlat0,sFlat1),X1) = mult(x0,X1),
inference(orient,[status(thm)],[t318]) ).
cnf(t23929,plain,
ld(x0,mult(mult(x0,x0),X1)) = mult(rd(x0,x0),ld(rd(sFlat0,sFlat1),X1)),
inference(step,[status(thm)],[t23928,t330]) ).
cnf(t23930,plain,
mult(ld(x0,x0),mult(x0,X1)) = mult(rd(x0,x0),ld(rd(sFlat0,sFlat1),X1)),
inference(step,[status(thm)],[t23929,t1371]) ).
cnf(t23931,plain,
mult(ld(x0,x0),mult(x0,X1)) = mult(rd(x0,x0),mult(x0,X1)),
inference(step,[status(thm)],[t23930,t330]) ).
cnf(t3509,plain,
mult(ld(x0,x0),mult(x0,X1)) = mult(rd(x0,x0),mult(x0,X1)),
inference(orient,[status(thm)],[t23931]) ).
cnf(t3524,plain,
ld(x0,x0) = rd(mult(rd(x0,x0),mult(x0,X1)),mult(x0,X1)),
inference(cp,[status(thm)],[t9,t3509]) ).
cnf(t23932,plain,
ld(x0,x0) = rd(x0,x0),
inference(step,[status(thm)],[t3524,t9]) ).
cnf(t3541,plain,
ld(x0,x0) = rd(x0,x0),
inference(orient,[status(thm)],[t23932]) ).
cnf(t3542,plain,
x0 = mult(x0,rd(x0,x0)),
inference(cp,[status(thm)],[t7,t3541]) ).
cnf(t3553,plain,
mult(x0,rd(x0,x0)) = x0,
inference(orient,[status(thm)],[t3542]) ).
cnf(t3554,plain,
mult(rd(x0,x0),mult(ld(rd(x0,x0),x0),X1)) = mult(x0,ld(rd(x0,x0),X1)),
inference(cp,[status(thm)],[t1102,t3553]) ).
cnf(t23995,plain,
mult(rd(x0,x0),mult(x0,X1)) = mult(x0,ld(rd(x0,x0),X1)),
inference(step,[status(thm)],[t3554,t39]) ).
cnf(t4905,plain,
mult(rd(x0,x0),mult(x0,X1)) = mult(x0,ld(rd(x0,x0),X1)),
inference(orient,[status(thm)],[t23995]) ).
cnf(t4907,plain,
mult(x0,ld(rd(x0,x0),rd(x0,x0))) = mult(rd(x0,x0),x0),
inference(cp,[status(thm)],[t4905,t3553]) ).
cnf(t23996,plain,
mult(x0,ld(rd(x0,x0),rd(x0,x0))) = x0,
inference(step,[status(thm)],[t4907,t8]) ).
cnf(t4969,plain,
mult(x0,ld(rd(x0,x0),rd(x0,x0))) = x0,
inference(orient,[status(thm)],[t23996]) ).
cnf(t4974,plain,
ld(rd(x0,x0),rd(x0,x0)) = ld(x0,x0),
inference(cp,[status(thm)],[t11,t4969]) ).
cnf(t23997,plain,
ld(rd(x0,x0),rd(x0,x0)) = rd(x0,x0),
inference(step,[status(thm)],[t4974,t3541]) ).
cnf(t4988,plain,
ld(rd(x0,x0),rd(x0,x0)) = rd(x0,x0),
inference(orient,[status(thm)],[t23997]) ).
cnf(t4989,plain,
rd(x0,x0) = mult(rd(x0,x0),rd(x0,x0)),
inference(cp,[status(thm)],[t7,t4988]) ).
cnf(t4993,plain,
mult(rd(x0,x0),rd(x0,x0)) = rd(x0,x0),
inference(orient,[status(thm)],[t4989]) ).
cnf(t24466,plain,
mult(sFlat0,rd(rd(x0,x0),sFlat0)) = mult(mult(sFlat0,rd(x0,x0)),ld(sFlat1,x0)),
inference(step,[status(thm)],[t9735,t4993]) ).
cnf(t24467,plain,
mult(sFlat0,ld(sFlat1,x0)) = mult(mult(sFlat0,rd(x0,x0)),ld(sFlat1,x0)),
inference(step,[status(thm)],[t24466,t9729]) ).
cnf(t23195,plain,
mult(mult(sFlat0,rd(x0,x0)),ld(sFlat1,x0)) = mult(sFlat0,ld(sFlat1,x0)),
inference(orient,[status(thm)],[t24467]) ).
cnf(t23201,plain,
mult(sFlat0,rd(x0,x0)) = rd(mult(sFlat0,ld(sFlat1,x0)),ld(sFlat1,x0)),
inference(cp,[status(thm)],[t9,t23195]) ).
cnf(t24468,plain,
mult(sFlat0,rd(x0,x0)) = sFlat0,
inference(step,[status(thm)],[t23201,t9]) ).
cnf(t23232,plain,
mult(sFlat0,rd(x0,x0)) = sFlat0,
inference(orient,[status(thm)],[t24468]) ).
cnf(t23254,plain,
rd(x0,x0) = mult(sFlat0,sFlat0),
inference(cp,[status(thm)],[t392,t23232]) ).
cnf(t23764,plain,
mult(sFlat0,sFlat0) = sFlat0,
inference(step,[status(thm)],[t379,t1748]) ).
cnf(t1751,plain,
mult(sFlat0,sFlat0) = sFlat0,
inference(orient,[status(thm)],[t23764]) ).
cnf(t24543,plain,
rd(x0,x0) = sFlat0,
inference(step,[status(thm)],[t23254,t1751]) ).
cnf(t23366,plain,
rd(x0,x0) = sFlat0,
inference(orient,[status(thm)],[t24543]) ).
cnf(t23389,plain,
x0 = mult(x0,sFlat0),
inference(cp,[status(thm)],[t7840,t23366]) ).
cnf(t24573,plain,
x0 = sFlat1,
inference(step,[status(thm)],[t23389,t31]) ).
cnf(t23421,plain,
x0 = sFlat1,
inference(orient,[status(thm)],[t24573]) ).
cnf(t1232,plain,
mult(sFlat1,mult(sFlat0,sFlat0)) = rd(mult(sFlat0,mult(sFlat0,x0)),sFlat0),
inference(cp,[status(thm)],[t1231,t702]) ).
cnf(t23748,plain,
mult(sFlat1,rd(sFlat0,sFlat0)) = rd(mult(sFlat0,mult(sFlat0,x0)),sFlat0),
inference(step,[status(thm)],[t1232,t379]) ).
cnf(t23749,plain,
mult(sFlat1,rd(sFlat0,sFlat0)) = rd(x0,sFlat0),
inference(step,[status(thm)],[t23748,t392]) ).
cnf(t1260,plain,
mult(sFlat1,rd(sFlat0,sFlat0)) = rd(x0,sFlat0),
inference(orient,[status(thm)],[t23749]) ).
cnf(t23776,plain,
mult(sFlat1,sFlat0) = rd(x0,sFlat0),
inference(step,[status(thm)],[t1260,t1748]) ).
cnf(t1763,plain,
mult(sFlat1,sFlat0) = rd(x0,sFlat0),
inference(rw,[status(thm)],[t23776]) ).
cnf(t1772,plain,
mult(sFlat1,sFlat0) = rd(x0,sFlat0),
inference(orient,[status(thm)],[t1763]) ).
cnf(t24582,plain,
mult(sFlat1,sFlat0) = rd(sFlat1,sFlat0),
inference(step,[status(thm)],[t1772,t23421]) ).
cnf(t33,plain,
x0 = rd(sFlat1,sFlat0),
inference(cp,[status(thm)],[t9,t31]) ).
cnf(t37,plain,
rd(sFlat1,sFlat0) = x0,
inference(orient,[status(thm)],[t33]) ).
cnf(t24574,plain,
rd(sFlat1,sFlat0) = sFlat1,
inference(step,[status(thm)],[t37,t23421]) ).
cnf(t23422,plain,
rd(sFlat1,sFlat0) = sFlat1,
inference(orient,[status(thm)],[t24574]) ).
cnf(t24583,plain,
mult(sFlat1,sFlat0) = sFlat1,
inference(step,[status(thm)],[t24582,t23422]) ).
cnf(t23430,plain,
mult(sFlat1,sFlat0) = sFlat1,
inference(orient,[status(thm)],[t24583]) ).
cnf(goal_0,negated_conjecture,
mult(x0,rd(x1,x1)) != x0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
mult(sFlat1,rd(x1,x1)) != x0,
inference(rw,[status(thm)],[goal_0,t23421]) ).
cnf(g0_1,plain,
mult(sFlat1,sFlat0) != x0,
inference(rw,[status(thm)],[g0_0,t25]) ).
cnf(g0_2,plain,
sFlat1 != x0,
inference(rw,[status(thm)],[g0_1,t23430]) ).
cnf(g0_3,plain,
sFlat1 != sFlat1,
inference(rw,[status(thm)],[g0_2,t23421]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP654-11 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n011.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Wed Sep 23 15:29:42 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 24.61/3.69 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 24.61/3.69 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------