%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP655-12 : TPTP v9.3.1. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n006.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:52 PM UTC 2026
% Result : Unsatisfiable 33.14s 5.07s
% Output : CNFRefutation 33.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 108
% Number of leaves : 8
% Syntax : Number of clauses : 360 ( 360 unt; 0 nHn; 136 RR)
% Number of literals : 360 ( 359 equ; 3 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 6 ( 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 : 353 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
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(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(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(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(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(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(t4,axiom,
mult(mult(mult(X1,X2),X3),X2) = mult(X1,mult(X2,mult(X3,X2))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t13,plain,
mult(mult(mult(X1,X2),X3),X2) = mult(X1,mult(X2,mult(X3,X2))),
inference(orient,[status(thm)],[t4]) ).
cnf(t16,plain,
mult(rd(X1,X2),mult(X2,mult(X3,X2))) = mult(mult(X1,X3),X2),
inference(cp,[status(thm)],[t13,t8]) ).
cnf(t232,plain,
mult(rd(X1,X2),mult(X2,mult(X3,X2))) = mult(mult(X1,X3),X2),
inference(orient,[status(thm)],[t16]) ).
cnf(t14,plain,
mult(X1,mult(X2,mult(ld(mult(X1,X2),X3),X2))) = mult(X3,X2),
inference(cp,[status(thm)],[t13,t7]) ).
cnf(t190,plain,
mult(X1,mult(X2,mult(ld(mult(X1,X2),X3),X2))) = mult(X3,X2),
inference(orient,[status(thm)],[t14]) ).
cnf(t210,plain,
mult(X1,mult(ld(mult(X2,X1),X3),X1)) = ld(X2,mult(X3,X1)),
inference(cp,[status(thm)],[t11,t190]) ).
cnf(t1188,plain,
mult(X1,mult(ld(mult(X2,X1),X3),X1)) = ld(X2,mult(X3,X1)),
inference(orient,[status(thm)],[t210]) ).
cnf(t1233,plain,
ld(rd(X1,X2),mult(X3,X2)) = mult(X2,mult(ld(X1,X3),X2)),
inference(cp,[status(thm)],[t1188,t8]) ).
cnf(t1255,plain,
ld(rd(X1,X2),mult(X3,X2)) = mult(X2,mult(ld(X1,X3),X2)),
inference(orient,[status(thm)],[t1233]) ).
cnf(t1256,plain,
mult(X1,mult(ld(X2,rd(X2,X1)),X1)) = X1,
inference(cp,[status(thm)],[t1255,t11]) ).
cnf(t1747,plain,
mult(X1,mult(ld(X2,rd(X2,X1)),X1)) = X1,
inference(orient,[status(thm)],[t1256]) ).
cnf(t1784,plain,
mult(ld(X1,rd(X1,X2)),X2) = ld(X2,X2),
inference(cp,[status(thm)],[t11,t1747]) ).
cnf(t2033,plain,
mult(ld(X1,rd(X1,X2)),X2) = ld(X2,X2),
inference(orient,[status(thm)],[t1784]) ).
cnf(t2079,plain,
mult(mult(X1,ld(X2,rd(X2,X3))),X3) = mult(rd(X1,X3),mult(X3,ld(X3,X3))),
inference(cp,[status(thm)],[t232,t2033]) ).
cnf(t24466,plain,
mult(mult(X1,ld(X2,rd(X2,X3))),X3) = mult(rd(X1,X3),X3),
inference(step,[status(thm)],[t2079,t7]) ).
cnf(t24467,plain,
mult(mult(X1,ld(X2,rd(X2,X3))),X3) = X1,
inference(step,[status(thm)],[t24466,t8]) ).
cnf(t3647,plain,
mult(mult(X1,ld(X2,rd(X2,X3))),X3) = X1,
inference(orient,[status(thm)],[t24467]) ).
cnf(t3655,plain,
rd(X1,ld(X2,rd(X2,X3))) = mult(X1,X3),
inference(cp,[status(thm)],[t3647,t8]) ).
cnf(t3726,plain,
rd(X1,ld(X2,rd(X2,X3))) = mult(X1,X3),
inference(orient,[status(thm)],[t3655]) ).
cnf(t3729,plain,
mult(X1,ld(X2,X3)) = rd(X1,ld(X3,X2)),
inference(cp,[status(thm)],[t3726,t38]) ).
cnf(t3790,plain,
mult(X1,ld(X2,X3)) = rd(X1,ld(X3,X2)),
inference(orient,[status(thm)],[t3729]) ).
cnf(t3846,plain,
ld(X1,X2) = ld(X3,rd(X3,ld(X2,X1))),
inference(cp,[status(thm)],[t11,t3790]) ).
cnf(t4013,plain,
ld(X1,rd(X1,ld(X2,X3))) = ld(X3,X2),
inference(orient,[status(thm)],[t3846]) ).
cnf(t15,plain,
mult(X1,mult(ld(X1,X2),mult(X3,ld(X1,X2)))) = mult(mult(X2,X3),ld(X1,X2)),
inference(cp,[status(thm)],[t13,t7]) ).
cnf(t608,plain,
mult(X1,mult(ld(X1,X2),mult(X3,ld(X1,X2)))) = mult(mult(X2,X3),ld(X1,X2)),
inference(orient,[status(thm)],[t15]) ).
cnf(t641,plain,
mult(mult(X1,X2),ld(X2,X1)) = mult(X2,mult(ld(X2,X1),X1)),
inference(cp,[status(thm)],[t608,t7]) ).
cnf(t690,plain,
mult(mult(X1,X2),ld(X2,X1)) = mult(X2,mult(ld(X2,X1),X1)),
inference(orient,[status(thm)],[t641]) ).
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(t30,plain,
mult(sFlat0,mult(x1,mult(X1,x1))) = mult(mult(x1,X1),x1),
inference(cp,[status(thm)],[t13,t28]) ).
cnf(t40,plain,
mult(sFlat0,mult(x1,mult(X1,x1))) = mult(mult(x1,X1),x1),
inference(orient,[status(thm)],[t30]) ).
cnf(t44,plain,
mult(x1,mult(X1,x1)) = ld(sFlat0,mult(mult(x1,X1),x1)),
inference(cp,[status(thm)],[t11,t40]) ).
cnf(t77,plain,
ld(sFlat0,mult(mult(x1,X1),x1)) = mult(x1,mult(X1,x1)),
inference(orient,[status(thm)],[t44]) ).
cnf(t78,plain,
mult(x1,mult(ld(x1,X1),x1)) = ld(sFlat0,mult(X1,x1)),
inference(cp,[status(thm)],[t77,t7]) ).
cnf(t94,plain,
mult(x1,mult(ld(x1,X1),x1)) = ld(sFlat0,mult(X1,x1)),
inference(orient,[status(thm)],[t78]) ).
cnf(t95,plain,
mult(ld(x1,X1),x1) = ld(x1,ld(sFlat0,mult(X1,x1))),
inference(cp,[status(thm)],[t11,t94]) ).
cnf(t112,plain,
ld(x1,ld(sFlat0,mult(X1,x1))) = mult(ld(x1,X1),x1),
inference(orient,[status(thm)],[t95]) ).
cnf(t113,plain,
mult(ld(x1,sFlat0),x1) = ld(x1,x1),
inference(cp,[status(thm)],[t112,t11]) ).
cnf(t119,plain,
mult(ld(x1,sFlat0),x1) = ld(x1,x1),
inference(orient,[status(thm)],[t113]) ).
cnf(t249,plain,
mult(mult(X1,ld(x1,sFlat0)),x1) = mult(rd(X1,x1),mult(x1,ld(x1,x1))),
inference(cp,[status(thm)],[t232,t119]) ).
cnf(t24254,plain,
mult(mult(X1,ld(x1,sFlat0)),x1) = mult(rd(X1,x1),x1),
inference(step,[status(thm)],[t249,t7]) ).
cnf(t24255,plain,
mult(mult(X1,ld(x1,sFlat0)),x1) = X1,
inference(step,[status(thm)],[t24254,t8]) ).
cnf(t271,plain,
mult(mult(X1,ld(x1,sFlat0)),x1) = X1,
inference(orient,[status(thm)],[t24255]) ).
cnf(t275,plain,
mult(X1,ld(x1,sFlat0)) = rd(X1,x1),
inference(cp,[status(thm)],[t9,t271]) ).
cnf(t286,plain,
mult(X1,ld(x1,sFlat0)) = rd(X1,x1),
inference(orient,[status(thm)],[t275]) ).
cnf(t692,plain,
mult(x1,mult(ld(x1,sFlat0),sFlat0)) = rd(mult(sFlat0,x1),x1),
inference(cp,[status(thm)],[t690,t286]) ).
cnf(t24258,plain,
mult(x1,mult(ld(x1,sFlat0),sFlat0)) = sFlat0,
inference(step,[status(thm)],[t692,t9]) ).
cnf(t764,plain,
mult(x1,mult(ld(x1,sFlat0),sFlat0)) = sFlat0,
inference(orient,[status(thm)],[t24258]) ).
cnf(t766,plain,
mult(ld(x1,sFlat0),sFlat0) = ld(x1,sFlat0),
inference(cp,[status(thm)],[t11,t764]) ).
cnf(t773,plain,
mult(ld(x1,sFlat0),sFlat0) = ld(x1,sFlat0),
inference(orient,[status(thm)],[t766]) ).
cnf(t780,plain,
mult(mult(X1,ld(x1,sFlat0)),sFlat0) = mult(rd(X1,sFlat0),mult(sFlat0,ld(x1,sFlat0))),
inference(cp,[status(thm)],[t232,t773]) ).
cnf(t24261,plain,
mult(rd(X1,x1),sFlat0) = mult(rd(X1,sFlat0),mult(sFlat0,ld(x1,sFlat0))),
inference(step,[status(thm)],[t780,t286]) ).
cnf(t24262,plain,
mult(rd(X1,x1),sFlat0) = mult(rd(X1,sFlat0),rd(sFlat0,x1)),
inference(step,[status(thm)],[t24261,t286]) ).
cnf(t821,plain,
mult(rd(X1,sFlat0),rd(sFlat0,x1)) = mult(rd(X1,x1),sFlat0),
inference(orient,[status(thm)],[t24262]) ).
cnf(t824,plain,
mult(rd(mult(X1,sFlat0),x1),sFlat0) = mult(X1,rd(sFlat0,x1)),
inference(cp,[status(thm)],[t821,t9]) ).
cnf(t846,plain,
mult(rd(mult(X1,sFlat0),x1),sFlat0) = mult(X1,rd(sFlat0,x1)),
inference(orient,[status(thm)],[t824]) ).
cnf(t855,plain,
rd(mult(X1,sFlat0),x1) = rd(mult(X1,rd(sFlat0,x1)),sFlat0),
inference(cp,[status(thm)],[t9,t846]) ).
cnf(t862,plain,
rd(mult(X1,rd(sFlat0,x1)),sFlat0) = rd(mult(X1,sFlat0),x1),
inference(orient,[status(thm)],[t855]) ).
cnf(t776,plain,
ld(x1,sFlat0) = rd(ld(x1,sFlat0),sFlat0),
inference(cp,[status(thm)],[t9,t773]) ).
cnf(t782,plain,
rd(ld(x1,sFlat0),sFlat0) = ld(x1,sFlat0),
inference(orient,[status(thm)],[t776]) ).
cnf(t1762,plain,
sFlat0 = mult(sFlat0,mult(ld(ld(x1,sFlat0),ld(x1,sFlat0)),sFlat0)),
inference(cp,[status(thm)],[t1747,t782]) ).
cnf(t775,plain,
sFlat0 = ld(ld(x1,sFlat0),ld(x1,sFlat0)),
inference(cp,[status(thm)],[t11,t773]) ).
cnf(t787,plain,
ld(ld(x1,sFlat0),ld(x1,sFlat0)) = sFlat0,
inference(orient,[status(thm)],[t775]) ).
cnf(t24274,plain,
sFlat0 = mult(sFlat0,mult(sFlat0,sFlat0)),
inference(step,[status(thm)],[t1762,t787]) ).
cnf(t1801,plain,
mult(sFlat0,mult(sFlat0,sFlat0)) = sFlat0,
inference(orient,[status(thm)],[t24274]) ).
cnf(t1808,plain,
mult(mult(X1,sFlat0),sFlat0) = mult(rd(X1,sFlat0),sFlat0),
inference(cp,[status(thm)],[t232,t1801]) ).
cnf(t24275,plain,
mult(mult(X1,sFlat0),sFlat0) = X1,
inference(step,[status(thm)],[t1808,t8]) ).
cnf(t1835,plain,
mult(mult(X1,sFlat0),sFlat0) = X1,
inference(orient,[status(thm)],[t24275]) ).
cnf(t1844,plain,
rd(X1,sFlat0) = mult(X1,sFlat0),
inference(cp,[status(thm)],[t1835,t8]) ).
cnf(t1858,plain,
mult(X1,sFlat0) = rd(X1,sFlat0),
inference(orient,[status(thm)],[t1844]) ).
cnf(t24284,plain,
rd(mult(X1,rd(sFlat0,x1)),sFlat0) = rd(rd(X1,sFlat0),x1),
inference(step,[status(thm)],[t862,t1858]) ).
cnf(t1867,plain,
rd(mult(X1,rd(sFlat0,x1)),sFlat0) = rd(rd(X1,sFlat0),x1),
inference(orient,[status(thm)],[t24284]) ).
cnf(t43,plain,
mult(mult(x1,rd(X1,x1)),x1) = mult(sFlat0,mult(x1,X1)),
inference(cp,[status(thm)],[t40,t8]) ).
cnf(t70,plain,
mult(mult(x1,rd(X1,x1)),x1) = mult(sFlat0,mult(x1,X1)),
inference(orient,[status(thm)],[t43]) ).
cnf(t73,plain,
mult(x1,rd(X1,x1)) = rd(mult(sFlat0,mult(x1,X1)),x1),
inference(cp,[status(thm)],[t9,t70]) ).
cnf(t90,plain,
rd(mult(sFlat0,mult(x1,X1)),x1) = mult(x1,rd(X1,x1)),
inference(orient,[status(thm)],[t73]) ).
cnf(t91,plain,
mult(x1,rd(ld(x1,X1),x1)) = rd(mult(sFlat0,X1),x1),
inference(cp,[status(thm)],[t90,t7]) ).
cnf(t107,plain,
mult(x1,rd(ld(x1,X1),x1)) = rd(mult(sFlat0,X1),x1),
inference(orient,[status(thm)],[t91]) ).
cnf(t108,plain,
rd(ld(x1,X1),x1) = ld(x1,rd(mult(sFlat0,X1),x1)),
inference(cp,[status(thm)],[t11,t107]) ).
cnf(t145,plain,
ld(x1,rd(mult(sFlat0,X1),x1)) = rd(ld(x1,X1),x1),
inference(orient,[status(thm)],[t108]) ).
cnf(t148,plain,
rd(ld(x1,ld(sFlat0,X1)),x1) = ld(x1,rd(X1,x1)),
inference(cp,[status(thm)],[t145,t7]) ).
cnf(t173,plain,
rd(ld(x1,ld(sFlat0,X1)),x1) = ld(x1,rd(X1,x1)),
inference(orient,[status(thm)],[t148]) ).
cnf(t1889,plain,
rd(ld(x1,sFlat0),x1) = ld(x1,rd(rd(sFlat0,sFlat0),x1)),
inference(cp,[status(thm)],[t145,t1858]) ).
cnf(t260,plain,
mult(mult(X1,sFlat0),x1) = mult(rd(X1,x1),mult(x1,x1)),
inference(cp,[status(thm)],[t232,t28]) ).
cnf(t361,plain,
mult(rd(X1,x1),mult(x1,x1)) = mult(mult(X1,sFlat0),x1),
inference(orient,[status(thm)],[t260]) ).
cnf(t366,plain,
rd(X1,x1) = rd(mult(mult(X1,sFlat0),x1),mult(x1,x1)),
inference(cp,[status(thm)],[t9,t361]) ).
cnf(t471,plain,
rd(mult(mult(X1,sFlat0),x1),mult(x1,x1)) = rd(X1,x1),
inference(orient,[status(thm)],[t366]) ).
cnf(t476,plain,
rd(rd(X1,sFlat0),x1) = rd(mult(X1,x1),mult(x1,x1)),
inference(cp,[status(thm)],[t471,t8]) ).
cnf(t479,plain,
rd(mult(X1,x1),mult(x1,x1)) = rd(rd(X1,sFlat0),x1),
inference(orient,[status(thm)],[t476]) ).
cnf(t483,plain,
rd(rd(sFlat0,sFlat0),x1) = rd(x1,mult(x1,x1)),
inference(cp,[status(thm)],[t479,t28]) ).
cnf(t489,plain,
rd(rd(sFlat0,sFlat0),x1) = rd(x1,mult(x1,x1)),
inference(orient,[status(thm)],[t483]) ).
cnf(t24325,plain,
rd(ld(x1,sFlat0),x1) = ld(x1,rd(x1,mult(x1,x1))),
inference(step,[status(thm)],[t1889,t489]) ).
cnf(t2297,plain,
ld(x1,rd(x1,mult(x1,x1))) = rd(ld(x1,sFlat0),x1),
inference(orient,[status(thm)],[t24325]) ).
cnf(t2300,plain,
ld(mult(x1,x1),mult(x1,x1)) = mult(rd(ld(x1,sFlat0),x1),mult(x1,x1)),
inference(cp,[status(thm)],[t2033,t2297]) ).
cnf(t24276,plain,
mult(rd(X1,x1),mult(x1,x1)) = mult(rd(X1,sFlat0),x1),
inference(step,[status(thm)],[t361,t1858]) ).
cnf(t1859,plain,
mult(rd(X1,x1),mult(x1,x1)) = mult(rd(X1,sFlat0),x1),
inference(orient,[status(thm)],[t24276]) ).
cnf(t24326,plain,
ld(mult(x1,x1),mult(x1,x1)) = mult(rd(ld(x1,sFlat0),sFlat0),x1),
inference(step,[status(thm)],[t2300,t1859]) ).
cnf(t24327,plain,
ld(mult(x1,x1),mult(x1,x1)) = mult(ld(x1,sFlat0),x1),
inference(step,[status(thm)],[t24326,t782]) ).
cnf(t24328,plain,
ld(mult(x1,x1),mult(x1,x1)) = ld(x1,x1),
inference(step,[status(thm)],[t24327,t119]) ).
cnf(t2305,plain,
ld(mult(x1,x1),mult(x1,x1)) = ld(x1,x1),
inference(orient,[status(thm)],[t24328]) ).
cnf(t2306,plain,
mult(x1,x1) = mult(mult(x1,x1),ld(x1,x1)),
inference(cp,[status(thm)],[t7,t2305]) ).
cnf(t24329,plain,
mult(x1,x1) = mult(x1,mult(ld(x1,x1),x1)),
inference(step,[status(thm)],[t2306,t690]) ).
cnf(t24330,plain,
mult(x1,x1) = ld(sFlat0,mult(x1,x1)),
inference(step,[status(thm)],[t24329,t94]) ).
cnf(t2312,plain,
ld(sFlat0,mult(x1,x1)) = mult(x1,x1),
inference(orient,[status(thm)],[t24330]) ).
cnf(t2317,plain,
ld(x1,rd(mult(x1,x1),x1)) = rd(ld(x1,mult(x1,x1)),x1),
inference(cp,[status(thm)],[t173,t2312]) ).
cnf(t24331,plain,
ld(x1,x1) = rd(ld(x1,mult(x1,x1)),x1),
inference(step,[status(thm)],[t2317,t9]) ).
cnf(t24332,plain,
ld(x1,x1) = rd(x1,x1),
inference(step,[status(thm)],[t24331,t11]) ).
cnf(t24333,plain,
ld(x1,x1) = sFlat0,
inference(step,[status(thm)],[t24332,t25]) ).
cnf(t2321,plain,
ld(x1,x1) = sFlat0,
inference(orient,[status(thm)],[t24333]) ).
cnf(t2333,plain,
rd(mult(sFlat0,x1),x1) = mult(x1,rd(sFlat0,x1)),
inference(cp,[status(thm)],[t107,t2321]) ).
cnf(t24374,plain,
sFlat0 = mult(x1,rd(sFlat0,x1)),
inference(step,[status(thm)],[t2333,t9]) ).
cnf(t2388,plain,
mult(x1,rd(sFlat0,x1)) = sFlat0,
inference(orient,[status(thm)],[t24374]) ).
cnf(t2395,plain,
rd(rd(x1,sFlat0),x1) = rd(sFlat0,sFlat0),
inference(cp,[status(thm)],[t1867,t2388]) ).
cnf(t2328,plain,
x1 = mult(x1,sFlat0),
inference(cp,[status(thm)],[t7,t2321]) ).
cnf(t24348,plain,
x1 = rd(x1,sFlat0),
inference(step,[status(thm)],[t2328,t1858]) ).
cnf(t2343,plain,
rd(x1,sFlat0) = x1,
inference(orient,[status(thm)],[t24348]) ).
cnf(t24375,plain,
rd(x1,x1) = rd(sFlat0,sFlat0),
inference(step,[status(thm)],[t2395,t2343]) ).
cnf(t24376,plain,
sFlat0 = rd(sFlat0,sFlat0),
inference(step,[status(thm)],[t24375,t25]) ).
cnf(t2402,plain,
rd(sFlat0,sFlat0) = sFlat0,
inference(orient,[status(thm)],[t24376]) ).
cnf(t2405,plain,
mult(sFlat0,mult(ld(sFlat0,X1),sFlat0)) = ld(sFlat0,mult(X1,sFlat0)),
inference(cp,[status(thm)],[t1255,t2402]) ).
cnf(t24431,plain,
mult(sFlat0,rd(ld(sFlat0,X1),sFlat0)) = ld(sFlat0,mult(X1,sFlat0)),
inference(step,[status(thm)],[t2405,t1858]) ).
cnf(t24432,plain,
mult(sFlat0,rd(ld(sFlat0,X1),sFlat0)) = ld(sFlat0,rd(X1,sFlat0)),
inference(step,[status(thm)],[t24431,t1858]) ).
cnf(t2884,plain,
mult(sFlat0,rd(ld(sFlat0,X1),sFlat0)) = ld(sFlat0,rd(X1,sFlat0)),
inference(orient,[status(thm)],[t24432]) ).
cnf(t265,plain,
mult(mult(X1,rd(X2,X3)),X3) = mult(rd(X1,X3),mult(X3,X2)),
inference(cp,[status(thm)],[t232,t8]) ).
cnf(t379,plain,
mult(mult(X1,rd(X2,X3)),X3) = mult(rd(X1,X3),mult(X3,X2)),
inference(orient,[status(thm)],[t265]) ).
cnf(t2900,plain,
mult(rd(sFlat0,sFlat0),mult(sFlat0,ld(sFlat0,X1))) = mult(ld(sFlat0,rd(X1,sFlat0)),sFlat0),
inference(cp,[status(thm)],[t379,t2884]) ).
cnf(t24433,plain,
mult(sFlat0,mult(sFlat0,ld(sFlat0,X1))) = mult(ld(sFlat0,rd(X1,sFlat0)),sFlat0),
inference(step,[status(thm)],[t2900,t2402]) ).
cnf(t24434,plain,
mult(sFlat0,X1) = mult(ld(sFlat0,rd(X1,sFlat0)),sFlat0),
inference(step,[status(thm)],[t24433,t7]) ).
cnf(t24435,plain,
mult(sFlat0,X1) = rd(ld(sFlat0,rd(X1,sFlat0)),sFlat0),
inference(step,[status(thm)],[t24434,t1858]) ).
cnf(t2918,plain,
rd(ld(sFlat0,rd(X1,sFlat0)),sFlat0) = mult(sFlat0,X1),
inference(orient,[status(thm)],[t24435]) ).
cnf(t2931,plain,
ld(sFlat0,rd(rd(X1,sFlat0),sFlat0)) = mult(sFlat0,mult(sFlat0,X1)),
inference(cp,[status(thm)],[t2884,t2918]) ).
cnf(t1877,plain,
rd(rd(X1,sFlat0),sFlat0) = X1,
inference(cp,[status(thm)],[t1858,t8]) ).
cnf(t1928,plain,
rd(rd(X1,sFlat0),sFlat0) = X1,
inference(orient,[status(thm)],[t1877]) ).
cnf(t24436,plain,
ld(sFlat0,X1) = mult(sFlat0,mult(sFlat0,X1)),
inference(step,[status(thm)],[t2931,t1928]) ).
cnf(t2936,plain,
mult(sFlat0,mult(sFlat0,X1)) = ld(sFlat0,X1),
inference(orient,[status(thm)],[t24436]) ).
cnf(t3843,plain,
ld(sFlat0,ld(X1,X2)) = mult(sFlat0,rd(sFlat0,ld(X2,X1))),
inference(cp,[status(thm)],[t2936,t3790]) ).
cnf(t4223,plain,
mult(sFlat0,rd(sFlat0,ld(X1,X2))) = ld(sFlat0,ld(X2,X1)),
inference(orient,[status(thm)],[t3843]) ).
cnf(t4225,plain,
ld(sFlat0,ld(mult(X1,X2),X1)) = mult(sFlat0,rd(sFlat0,X2)),
inference(cp,[status(thm)],[t4223,t11]) ).
cnf(t4467,plain,
ld(sFlat0,ld(mult(X1,X2),X1)) = mult(sFlat0,rd(sFlat0,X2)),
inference(orient,[status(thm)],[t4225]) ).
cnf(t4520,plain,
ld(ld(mult(X1,X2),X1),sFlat0) = ld(X3,rd(X3,mult(sFlat0,rd(sFlat0,X2)))),
inference(cp,[status(thm)],[t4013,t4467]) ).
cnf(t2943,plain,
ld(sFlat0,ld(sFlat0,X1)) = mult(sFlat0,X1),
inference(cp,[status(thm)],[t2936,t7]) ).
cnf(t2977,plain,
ld(sFlat0,ld(sFlat0,X1)) = mult(sFlat0,X1),
inference(orient,[status(thm)],[t2943]) ).
cnf(t4051,plain,
ld(ld(sFlat0,X1),sFlat0) = ld(X2,rd(X2,mult(sFlat0,X1))),
inference(cp,[status(thm)],[t4013,t2977]) ).
cnf(t4395,plain,
ld(X1,rd(X1,mult(sFlat0,X2))) = ld(ld(sFlat0,X2),sFlat0),
inference(orient,[status(thm)],[t4051]) ).
cnf(t24570,plain,
ld(ld(mult(X1,X2),X1),sFlat0) = ld(ld(sFlat0,rd(sFlat0,X2)),sFlat0),
inference(step,[status(thm)],[t4520,t4395]) ).
cnf(t8239,plain,
ld(ld(mult(X1,X2),X1),sFlat0) = ld(ld(sFlat0,rd(sFlat0,X2)),sFlat0),
inference(orient,[status(thm)],[t24570]) ).
cnf(t8305,plain,
ld(mult(X1,X2),X1) = rd(sFlat0,ld(ld(sFlat0,rd(sFlat0,X2)),sFlat0)),
inference(cp,[status(thm)],[t38,t8239]) ).
cnf(t2950,plain,
sFlat0 = rd(ld(sFlat0,X1),mult(sFlat0,X1)),
inference(cp,[status(thm)],[t9,t2936]) ).
cnf(t3056,plain,
rd(ld(sFlat0,X1),mult(sFlat0,X1)) = sFlat0,
inference(orient,[status(thm)],[t2950]) ).
cnf(t3736,plain,
mult(X1,mult(sFlat0,X2)) = rd(X1,ld(ld(sFlat0,X2),sFlat0)),
inference(cp,[status(thm)],[t3726,t3056]) ).
cnf(t4121,plain,
rd(X1,ld(ld(sFlat0,X2),sFlat0)) = mult(X1,mult(sFlat0,X2)),
inference(orient,[status(thm)],[t3736]) ).
cnf(t24571,plain,
ld(mult(X1,X2),X1) = mult(sFlat0,mult(sFlat0,rd(sFlat0,X2))),
inference(step,[status(thm)],[t8305,t4121]) ).
cnf(t24572,plain,
ld(mult(X1,X2),X1) = ld(sFlat0,rd(sFlat0,X2)),
inference(step,[status(thm)],[t24571,t2936]) ).
cnf(t8310,plain,
ld(mult(X1,X2),X1) = ld(sFlat0,rd(sFlat0,X2)),
inference(orient,[status(thm)],[t24572]) ).
cnf(t6,axiom,
sFlat1 = mult(rd(x1,x1),x0),
introduced(definition) ).
cnf(t21,plain,
mult(rd(x1,x1),x0) = sFlat1,
inference(orient,[status(thm)],[t6]) ).
cnf(t24253,plain,
mult(sFlat0,x0) = sFlat1,
inference(step,[status(thm)],[t21,t25]) ).
cnf(t27,plain,
mult(sFlat0,x0) = sFlat1,
inference(rw,[status(thm)],[t24253]) ).
cnf(t31,plain,
mult(sFlat0,x0) = sFlat1,
inference(orient,[status(thm)],[t27]) ).
cnf(t34,plain,
mult(sFlat0,mult(x0,mult(X1,x0))) = mult(mult(sFlat1,X1),x0),
inference(cp,[status(thm)],[t13,t31]) ).
cnf(t55,plain,
mult(sFlat0,mult(x0,mult(X1,x0))) = mult(mult(sFlat1,X1),x0),
inference(orient,[status(thm)],[t34]) ).
cnf(t58,plain,
mult(mult(sFlat1,rd(X1,x0)),x0) = mult(sFlat0,mult(x0,X1)),
inference(cp,[status(thm)],[t55,t8]) ).
cnf(t80,plain,
mult(mult(sFlat1,rd(X1,x0)),x0) = mult(sFlat0,mult(x0,X1)),
inference(orient,[status(thm)],[t58]) ).
cnf(t83,plain,
mult(sFlat1,rd(X1,x0)) = rd(mult(sFlat0,mult(x0,X1)),x0),
inference(cp,[status(thm)],[t9,t80]) ).
cnf(t99,plain,
rd(mult(sFlat0,mult(x0,X1)),x0) = mult(sFlat1,rd(X1,x0)),
inference(orient,[status(thm)],[t83]) ).
cnf(t100,plain,
mult(sFlat1,rd(ld(x0,X1),x0)) = rd(mult(sFlat0,X1),x0),
inference(cp,[status(thm)],[t99,t7]) ).
cnf(t127,plain,
mult(sFlat1,rd(ld(x0,X1),x0)) = rd(mult(sFlat0,X1),x0),
inference(orient,[status(thm)],[t100]) ).
cnf(t8348,plain,
ld(sFlat0,rd(sFlat0,rd(ld(x0,X1),x0))) = ld(rd(mult(sFlat0,X1),x0),sFlat1),
inference(cp,[status(thm)],[t8310,t127]) ).
cnf(t1324,plain,
mult(x0,mult(ld(X1,sFlat0),x0)) = ld(rd(X1,x0),sFlat1),
inference(cp,[status(thm)],[t1255,t31]) ).
cnf(t1351,plain,
mult(x0,mult(ld(X1,sFlat0),x0)) = ld(rd(X1,x0),sFlat1),
inference(orient,[status(thm)],[t1324]) ).
cnf(t1354,plain,
ld(rd(rd(sFlat0,X1),x0),sFlat1) = mult(x0,mult(X1,x0)),
inference(cp,[status(thm)],[t1351,t39]) ).
cnf(t1387,plain,
ld(rd(rd(sFlat0,X1),x0),sFlat1) = mult(x0,mult(X1,x0)),
inference(orient,[status(thm)],[t1354]) ).
cnf(t1389,plain,
rd(rd(sFlat0,X1),x0) = rd(sFlat1,mult(x0,mult(X1,x0))),
inference(cp,[status(thm)],[t38,t1387]) ).
cnf(t1442,plain,
rd(sFlat1,mult(x0,mult(X1,x0))) = rd(rd(sFlat0,X1),x0),
inference(orient,[status(thm)],[t1389]) ).
cnf(t1451,plain,
rd(rd(sFlat0,rd(X1,x0)),x0) = rd(sFlat1,mult(x0,X1)),
inference(cp,[status(thm)],[t1442,t8]) ).
cnf(t1624,plain,
rd(rd(sFlat0,rd(X1,x0)),x0) = rd(sFlat1,mult(x0,X1)),
inference(orient,[status(thm)],[t1451]) ).
cnf(t1637,plain,
rd(sFlat0,rd(X1,x0)) = mult(rd(sFlat1,mult(x0,X1)),x0),
inference(cp,[status(thm)],[t8,t1624]) ).
cnf(t1690,plain,
mult(rd(sFlat1,mult(x0,X1)),x0) = rd(sFlat0,rd(X1,x0)),
inference(orient,[status(thm)],[t1637]) ).
cnf(t1694,plain,
rd(sFlat0,rd(ld(x0,X1),x0)) = mult(rd(sFlat1,X1),x0),
inference(cp,[status(thm)],[t1690,t7]) ).
cnf(t1735,plain,
rd(sFlat0,rd(ld(x0,X1),x0)) = mult(rd(sFlat1,X1),x0),
inference(orient,[status(thm)],[t1694]) ).
cnf(t24618,plain,
ld(sFlat0,mult(rd(sFlat1,X1),x0)) = ld(rd(mult(sFlat0,X1),x0),sFlat1),
inference(step,[status(thm)],[t8348,t1735]) ).
cnf(t9614,plain,
ld(rd(mult(sFlat0,X1),x0),sFlat1) = ld(sFlat0,mult(rd(sFlat1,X1),x0)),
inference(orient,[status(thm)],[t24618]) ).
cnf(t1327,plain,
mult(X1,mult(ld(X2,rd(X3,X1)),X1)) = ld(rd(X2,X1),X3),
inference(cp,[status(thm)],[t1255,t8]) ).
cnf(t11579,plain,
mult(X1,mult(ld(X2,rd(X3,X1)),X1)) = ld(rd(X2,X1),X3),
inference(orient,[status(thm)],[t1327]) ).
cnf(t11752,plain,
mult(ld(X1,rd(X2,X3)),X3) = ld(X3,ld(rd(X1,X3),X2)),
inference(cp,[status(thm)],[t11,t11579]) ).
cnf(t11830,plain,
ld(X1,ld(rd(X2,X1),X3)) = mult(ld(X2,rd(X3,X1)),X1),
inference(orient,[status(thm)],[t11752]) ).
cnf(t24472,plain,
rd(mult(X1,X2),ld(X1,X2)) = mult(X2,mult(ld(X2,X1),X1)),
inference(step,[status(thm)],[t690,t3790]) ).
cnf(t3871,plain,
rd(mult(X1,X2),ld(X1,X2)) = mult(X2,mult(ld(X2,X1),X1)),
inference(rw,[status(thm)],[t24472]) ).
cnf(t7895,plain,
mult(X1,mult(ld(X1,X2),X2)) = rd(mult(X2,X1),ld(X2,X1)),
inference(orient,[status(thm)],[t3871]) ).
cnf(t8003,plain,
mult(ld(X1,X2),X2) = ld(X1,rd(mult(X2,X1),ld(X2,X1))),
inference(cp,[status(thm)],[t11,t7895]) ).
cnf(t14016,plain,
ld(X1,rd(mult(X2,X1),ld(X2,X1))) = mult(ld(X1,X2),X2),
inference(orient,[status(thm)],[t8003]) ).
cnf(t128,plain,
rd(ld(x0,X1),x0) = ld(sFlat1,rd(mult(sFlat0,X1),x0)),
inference(cp,[status(thm)],[t11,t127]) ).
cnf(t160,plain,
ld(sFlat1,rd(mult(sFlat0,X1),x0)) = rd(ld(x0,X1),x0),
inference(orient,[status(thm)],[t128]) ).
cnf(t163,plain,
rd(ld(x0,ld(sFlat0,X1)),x0) = ld(sFlat1,rd(X1,x0)),
inference(cp,[status(thm)],[t160,t7]) ).
cnf(t177,plain,
rd(ld(x0,ld(sFlat0,X1)),x0) = ld(sFlat1,rd(X1,x0)),
inference(orient,[status(thm)],[t163]) ).
cnf(t1805,plain,
mult(sFlat0,sFlat0) = ld(sFlat0,sFlat0),
inference(cp,[status(thm)],[t11,t1801]) ).
cnf(t1818,plain,
ld(sFlat0,sFlat0) = mult(sFlat0,sFlat0),
inference(orient,[status(thm)],[t1805]) ).
cnf(t1823,plain,
ld(sFlat1,rd(sFlat0,x0)) = rd(ld(x0,mult(sFlat0,sFlat0)),x0),
inference(cp,[status(thm)],[t177,t1818]) ).
cnf(t24322,plain,
ld(sFlat1,rd(sFlat0,x0)) = rd(ld(x0,rd(sFlat0,sFlat0)),x0),
inference(step,[status(thm)],[t1823,t1858]) ).
cnf(t2229,plain,
rd(ld(x0,rd(sFlat0,sFlat0)),x0) = ld(sFlat1,rd(sFlat0,x0)),
inference(orient,[status(thm)],[t24322]) ).
cnf(t24383,plain,
rd(ld(x0,sFlat0),x0) = ld(sFlat1,rd(sFlat0,x0)),
inference(step,[status(thm)],[t2229,t2402]) ).
cnf(t2413,plain,
rd(ld(x0,sFlat0),x0) = ld(sFlat1,rd(sFlat0,x0)),
inference(rw,[status(thm)],[t24383]) ).
cnf(t2660,plain,
ld(sFlat1,rd(sFlat0,x0)) = rd(ld(x0,sFlat0),x0),
inference(orient,[status(thm)],[t2413]) ).
cnf(t14194,plain,
mult(ld(rd(sFlat0,x0),sFlat1),sFlat1) = ld(rd(sFlat0,x0),rd(mult(sFlat1,rd(sFlat0,x0)),rd(ld(x0,sFlat0),x0))),
inference(cp,[status(thm)],[t14016,t2660]) ).
cnf(t2407,plain,
mult(x0,mult(sFlat0,x0)) = ld(rd(sFlat0,x0),sFlat1),
inference(cp,[status(thm)],[t1387,t2402]) ).
cnf(t24399,plain,
mult(x0,sFlat1) = ld(rd(sFlat0,x0),sFlat1),
inference(step,[status(thm)],[t2407,t31]) ).
cnf(t2582,plain,
ld(rd(sFlat0,x0),sFlat1) = mult(x0,sFlat1),
inference(orient,[status(thm)],[t24399]) ).
cnf(t25051,plain,
mult(mult(x0,sFlat1),sFlat1) = ld(rd(sFlat0,x0),rd(mult(sFlat1,rd(sFlat0,x0)),rd(ld(x0,sFlat0),x0))),
inference(step,[status(thm)],[t14194,t2582]) ).
cnf(t261,plain,
mult(mult(X1,sFlat0),x0) = mult(rd(X1,x0),mult(x0,sFlat1)),
inference(cp,[status(thm)],[t232,t31]) ).
cnf(t370,plain,
mult(rd(X1,x0),mult(x0,sFlat1)) = mult(mult(X1,sFlat0),x0),
inference(orient,[status(thm)],[t261]) ).
cnf(t375,plain,
rd(X1,x0) = rd(mult(mult(X1,sFlat0),x0),mult(x0,sFlat1)),
inference(cp,[status(thm)],[t9,t370]) ).
cnf(t544,plain,
rd(mult(mult(X1,sFlat0),x0),mult(x0,sFlat1)) = rd(X1,x0),
inference(orient,[status(thm)],[t375]) ).
cnf(t549,plain,
rd(rd(X1,sFlat0),x0) = rd(mult(X1,x0),mult(x0,sFlat1)),
inference(cp,[status(thm)],[t544,t8]) ).
cnf(t552,plain,
rd(mult(X1,x0),mult(x0,sFlat1)) = rd(rd(X1,sFlat0),x0),
inference(orient,[status(thm)],[t549]) ).
cnf(t556,plain,
rd(rd(sFlat0,sFlat0),x0) = rd(sFlat1,mult(x0,sFlat1)),
inference(cp,[status(thm)],[t552,t31]) ).
cnf(t562,plain,
rd(rd(sFlat0,sFlat0),x0) = rd(sFlat1,mult(x0,sFlat1)),
inference(orient,[status(thm)],[t556]) ).
cnf(t24379,plain,
rd(sFlat0,x0) = rd(sFlat1,mult(x0,sFlat1)),
inference(step,[status(thm)],[t562,t2402]) ).
cnf(t2410,plain,
rd(sFlat0,x0) = rd(sFlat1,mult(x0,sFlat1)),
inference(rw,[status(thm)],[t24379]) ).
cnf(t2592,plain,
rd(sFlat1,mult(x0,sFlat1)) = rd(sFlat0,x0),
inference(orient,[status(thm)],[t2410]) ).
cnf(t3769,plain,
mult(X1,mult(x0,sFlat1)) = rd(X1,ld(sFlat1,rd(sFlat0,x0))),
inference(cp,[status(thm)],[t3726,t2592]) ).
cnf(t24482,plain,
mult(X1,mult(x0,sFlat1)) = rd(X1,rd(ld(x0,sFlat0),x0)),
inference(step,[status(thm)],[t3769,t2660]) ).
cnf(t4144,plain,
rd(X1,rd(ld(x0,sFlat0),x0)) = mult(X1,mult(x0,sFlat1)),
inference(orient,[status(thm)],[t24482]) ).
cnf(t25052,plain,
mult(mult(x0,sFlat1),sFlat1) = ld(rd(sFlat0,x0),mult(mult(sFlat1,rd(sFlat0,x0)),mult(x0,sFlat1))),
inference(step,[status(thm)],[t25051,t4144]) ).
cnf(t24278,plain,
mult(rd(X1,x0),mult(x0,sFlat1)) = mult(rd(X1,sFlat0),x0),
inference(step,[status(thm)],[t370,t1858]) ).
cnf(t1861,plain,
mult(rd(X1,x0),mult(x0,sFlat1)) = mult(rd(X1,sFlat0),x0),
inference(orient,[status(thm)],[t24278]) ).
cnf(t1890,plain,
mult(sFlat1,rd(sFlat0,x0)) = rd(mult(sFlat0,rd(x0,sFlat0)),x0),
inference(cp,[status(thm)],[t99,t1858]) ).
cnf(t2730,plain,
rd(mult(sFlat0,rd(x0,sFlat0)),x0) = mult(sFlat1,rd(sFlat0,x0)),
inference(orient,[status(thm)],[t1890]) ).
cnf(t2920,plain,
mult(sFlat0,rd(X1,sFlat0)) = rd(ld(sFlat0,X1),sFlat0),
inference(cp,[status(thm)],[t2918,t1928]) ).
cnf(t3015,plain,
mult(sFlat0,rd(X1,sFlat0)) = rd(ld(sFlat0,X1),sFlat0),
inference(orient,[status(thm)],[t2920]) ).
cnf(t24446,plain,
rd(rd(ld(sFlat0,x0),sFlat0),x0) = mult(sFlat1,rd(sFlat0,x0)),
inference(step,[status(thm)],[t2730,t3015]) ).
cnf(t2941,plain,
ld(sFlat0,x0) = mult(sFlat0,sFlat1),
inference(cp,[status(thm)],[t2936,t31]) ).
cnf(t2963,plain,
ld(sFlat0,x0) = mult(sFlat0,sFlat1),
inference(orient,[status(thm)],[t2941]) ).
cnf(t24447,plain,
rd(rd(mult(sFlat0,sFlat1),sFlat0),x0) = mult(sFlat1,rd(sFlat0,x0)),
inference(step,[status(thm)],[t24446,t2963]) ).
cnf(t3039,plain,
rd(rd(mult(sFlat0,sFlat1),sFlat0),x0) = mult(sFlat1,rd(sFlat0,x0)),
inference(rw,[status(thm)],[t24447]) ).
cnf(t3419,plain,
rd(rd(mult(sFlat0,sFlat1),sFlat0),x0) = mult(sFlat1,rd(sFlat0,x0)),
inference(orient,[status(thm)],[t3039]) ).
cnf(t3422,plain,
mult(rd(rd(mult(sFlat0,sFlat1),sFlat0),sFlat0),x0) = mult(mult(sFlat1,rd(sFlat0,x0)),mult(x0,sFlat1)),
inference(cp,[status(thm)],[t1861,t3419]) ).
cnf(t24717,plain,
mult(mult(sFlat0,sFlat1),x0) = mult(mult(sFlat1,rd(sFlat0,x0)),mult(x0,sFlat1)),
inference(step,[status(thm)],[t3422,t1928]) ).
cnf(t7991,plain,
rd(mult(x0,sFlat0),ld(x0,sFlat0)) = mult(sFlat0,mult(mult(sFlat0,sFlat1),x0)),
inference(cp,[status(thm)],[t7895,t2963]) ).
cnf(t24614,plain,
rd(rd(x0,sFlat0),ld(x0,sFlat0)) = mult(sFlat0,mult(mult(sFlat0,sFlat1),x0)),
inference(step,[status(thm)],[t7991,t1858]) ).
cnf(t1875,plain,
rd(mult(X1,rd(X2,sFlat0)),sFlat0) = mult(rd(X1,sFlat0),mult(sFlat0,X2)),
inference(cp,[status(thm)],[t1858,t379]) ).
cnf(t5601,plain,
mult(rd(X1,sFlat0),mult(sFlat0,X2)) = rd(mult(X1,rd(X2,sFlat0)),sFlat0),
inference(orient,[status(thm)],[t1875]) ).
cnf(t2965,plain,
sFlat0 = rd(x0,mult(sFlat0,sFlat1)),
inference(cp,[status(thm)],[t38,t2963]) ).
cnf(t2971,plain,
rd(x0,mult(sFlat0,sFlat1)) = sFlat0,
inference(orient,[status(thm)],[t2965]) ).
cnf(t3738,plain,
mult(X1,mult(sFlat0,sFlat1)) = rd(X1,ld(x0,sFlat0)),
inference(cp,[status(thm)],[t3726,t2971]) ).
cnf(t3874,plain,
mult(X1,mult(sFlat0,sFlat1)) = rd(X1,ld(x0,sFlat0)),
inference(orient,[status(thm)],[t3738]) ).
cnf(t5602,plain,
rd(mult(X1,rd(sFlat1,sFlat0)),sFlat0) = rd(rd(X1,sFlat0),ld(x0,sFlat0)),
inference(cp,[status(thm)],[t5601,t3874]) ).
cnf(t8463,plain,
rd(mult(X1,rd(sFlat1,sFlat0)),sFlat0) = rd(rd(X1,sFlat0),ld(x0,sFlat0)),
inference(orient,[status(thm)],[t5602]) ).
cnf(t1883,plain,
mult(X1,mult(X2,mult(sFlat0,X2))) = mult(rd(mult(X1,X2),sFlat0),X2),
inference(cp,[status(thm)],[t13,t1858]) ).
cnf(t6787,plain,
mult(rd(mult(X1,X2),sFlat0),X2) = mult(X1,mult(X2,mult(sFlat0,X2))),
inference(orient,[status(thm)],[t1883]) ).
cnf(t6855,plain,
mult(sFlat0,mult(rd(X1,sFlat0),mult(sFlat0,rd(X1,sFlat0)))) = mult(rd(rd(ld(sFlat0,X1),sFlat0),sFlat0),rd(X1,sFlat0)),
inference(cp,[status(thm)],[t6787,t3015]) ).
cnf(t24595,plain,
mult(sFlat0,rd(mult(X1,rd(rd(X1,sFlat0),sFlat0)),sFlat0)) = mult(rd(rd(ld(sFlat0,X1),sFlat0),sFlat0),rd(X1,sFlat0)),
inference(step,[status(thm)],[t6855,t5601]) ).
cnf(t24596,plain,
rd(ld(sFlat0,mult(X1,rd(rd(X1,sFlat0),sFlat0))),sFlat0) = mult(rd(rd(ld(sFlat0,X1),sFlat0),sFlat0),rd(X1,sFlat0)),
inference(step,[status(thm)],[t24595,t3015]) ).
cnf(t24597,plain,
rd(ld(sFlat0,mult(X1,X1)),sFlat0) = mult(rd(rd(ld(sFlat0,X1),sFlat0),sFlat0),rd(X1,sFlat0)),
inference(step,[status(thm)],[t24596,t1928]) ).
cnf(t18,plain,
mult(mult(X1,X2),X3) = rd(mult(X1,mult(X2,mult(X3,X2))),X2),
inference(cp,[status(thm)],[t9,t13]) ).
cnf(t1044,plain,
rd(mult(X1,mult(X2,mult(X3,X2))),X2) = mult(mult(X1,X2),X3),
inference(orient,[status(thm)],[t18]) ).
cnf(t1087,plain,
mult(mult(X1,X2),rd(X3,X2)) = rd(mult(X1,mult(X2,X3)),X2),
inference(cp,[status(thm)],[t1044,t8]) ).
cnf(t1111,plain,
mult(mult(X1,X2),rd(X3,X2)) = rd(mult(X1,mult(X2,X3)),X2),
inference(orient,[status(thm)],[t1087]) ).
cnf(t1879,plain,
rd(mult(X1,mult(sFlat0,X2)),sFlat0) = mult(rd(X1,sFlat0),rd(X2,sFlat0)),
inference(cp,[status(thm)],[t1111,t1858]) ).
cnf(t6721,plain,
mult(rd(X1,sFlat0),rd(X2,sFlat0)) = rd(mult(X1,mult(sFlat0,X2)),sFlat0),
inference(orient,[status(thm)],[t1879]) ).
cnf(t24598,plain,
rd(ld(sFlat0,mult(X1,X1)),sFlat0) = rd(mult(rd(ld(sFlat0,X1),sFlat0),mult(sFlat0,X1)),sFlat0),
inference(step,[status(thm)],[t24597,t6721]) ).
cnf(t24599,plain,
rd(ld(sFlat0,mult(X1,X1)),sFlat0) = rd(rd(mult(ld(sFlat0,X1),rd(X1,sFlat0)),sFlat0),sFlat0),
inference(step,[status(thm)],[t24598,t5601]) ).
cnf(t24600,plain,
rd(ld(sFlat0,mult(X1,X1)),sFlat0) = mult(ld(sFlat0,X1),rd(X1,sFlat0)),
inference(step,[status(thm)],[t24599,t1928]) ).
cnf(t9130,plain,
mult(ld(sFlat0,X1),rd(X1,sFlat0)) = rd(ld(sFlat0,mult(X1,X1)),sFlat0),
inference(orient,[status(thm)],[t24600]) ).
cnf(t9205,plain,
rd(rd(ld(sFlat0,sFlat1),sFlat0),ld(x0,sFlat0)) = rd(rd(ld(sFlat0,mult(sFlat1,sFlat1)),sFlat0),sFlat0),
inference(cp,[status(thm)],[t8463,t9130]) ).
cnf(t32,plain,
x0 = ld(sFlat0,sFlat1),
inference(cp,[status(thm)],[t11,t31]) ).
cnf(t36,plain,
ld(sFlat0,sFlat1) = x0,
inference(orient,[status(thm)],[t32]) ).
cnf(t24601,plain,
rd(rd(x0,sFlat0),ld(x0,sFlat0)) = rd(rd(ld(sFlat0,mult(sFlat1,sFlat1)),sFlat0),sFlat0),
inference(step,[status(thm)],[t9205,t36]) ).
cnf(t24602,plain,
rd(rd(x0,sFlat0),ld(x0,sFlat0)) = ld(sFlat0,mult(sFlat1,sFlat1)),
inference(step,[status(thm)],[t24601,t1928]) ).
cnf(t9264,plain,
rd(rd(x0,sFlat0),ld(x0,sFlat0)) = ld(sFlat0,mult(sFlat1,sFlat1)),
inference(orient,[status(thm)],[t24602]) ).
cnf(t24615,plain,
ld(sFlat0,mult(sFlat1,sFlat1)) = mult(sFlat0,mult(mult(sFlat0,sFlat1),x0)),
inference(step,[status(thm)],[t24614,t9264]) ).
cnf(t9500,plain,
mult(sFlat0,mult(mult(sFlat0,sFlat1),x0)) = ld(sFlat0,mult(sFlat1,sFlat1)),
inference(orient,[status(thm)],[t24615]) ).
cnf(t9507,plain,
mult(mult(sFlat0,sFlat1),x0) = ld(sFlat0,ld(sFlat0,mult(sFlat1,sFlat1))),
inference(cp,[status(thm)],[t11,t9500]) ).
cnf(t24616,plain,
mult(mult(sFlat0,sFlat1),x0) = mult(sFlat0,mult(sFlat1,sFlat1)),
inference(step,[status(thm)],[t9507,t2977]) ).
cnf(t9527,plain,
mult(mult(sFlat0,sFlat1),x0) = mult(sFlat0,mult(sFlat1,sFlat1)),
inference(orient,[status(thm)],[t24616]) ).
cnf(t24718,plain,
mult(sFlat0,mult(sFlat1,sFlat1)) = mult(mult(sFlat1,rd(sFlat0,x0)),mult(x0,sFlat1)),
inference(step,[status(thm)],[t24717,t9527]) ).
cnf(t12333,plain,
mult(mult(sFlat1,rd(sFlat0,x0)),mult(x0,sFlat1)) = mult(sFlat0,mult(sFlat1,sFlat1)),
inference(orient,[status(thm)],[t24718]) ).
cnf(t25053,plain,
mult(mult(x0,sFlat1),sFlat1) = ld(rd(sFlat0,x0),mult(sFlat0,mult(sFlat1,sFlat1))),
inference(step,[status(thm)],[t25052,t12333]) ).
cnf(t23845,plain,
ld(rd(sFlat0,x0),mult(sFlat0,mult(sFlat1,sFlat1))) = mult(mult(x0,sFlat1),sFlat1),
inference(orient,[status(thm)],[t25053]) ).
cnf(t23851,plain,
mult(ld(sFlat0,rd(mult(sFlat0,mult(sFlat1,sFlat1)),x0)),x0) = ld(x0,mult(mult(x0,sFlat1),sFlat1)),
inference(cp,[status(thm)],[t11830,t23845]) ).
cnf(t9533,plain,
mult(sFlat0,sFlat1) = rd(mult(sFlat0,mult(sFlat1,sFlat1)),x0),
inference(cp,[status(thm)],[t9,t9527]) ).
cnf(t9551,plain,
rd(mult(sFlat0,mult(sFlat1,sFlat1)),x0) = mult(sFlat0,sFlat1),
inference(orient,[status(thm)],[t9533]) ).
cnf(t25054,plain,
mult(ld(sFlat0,mult(sFlat0,sFlat1)),x0) = ld(x0,mult(mult(x0,sFlat1),sFlat1)),
inference(step,[status(thm)],[t23851,t9551]) ).
cnf(t25055,plain,
mult(sFlat1,x0) = ld(x0,mult(mult(x0,sFlat1),sFlat1)),
inference(step,[status(thm)],[t25054,t11]) ).
cnf(t5630,plain,
rd(mult(X1,rd(x0,sFlat0)),sFlat0) = mult(rd(X1,sFlat0),sFlat1),
inference(cp,[status(thm)],[t5601,t31]) ).
cnf(t5662,plain,
rd(mult(X1,rd(x0,sFlat0)),sFlat0) = mult(rd(X1,sFlat0),sFlat1),
inference(orient,[status(thm)],[t5630]) ).
cnf(t396,plain,
mult(X1,rd(X2,X3)) = rd(mult(rd(X1,X3),mult(X3,X2)),X3),
inference(cp,[status(thm)],[t9,t379]) ).
cnf(t11299,plain,
rd(mult(rd(X1,X2),mult(X2,X3)),X2) = mult(X1,rd(X3,X2)),
inference(orient,[status(thm)],[t396]) ).
cnf(t11483,plain,
mult(X1,rd(X2,ld(X3,rd(X3,X2)))) = rd(mult(rd(X1,ld(X3,rd(X3,X2))),ld(X2,X2)),ld(X3,rd(X3,X2))),
inference(cp,[status(thm)],[t11299,t2033]) ).
cnf(t24819,plain,
mult(X1,mult(X2,X2)) = rd(mult(rd(X1,ld(X3,rd(X3,X2))),ld(X2,X2)),ld(X3,rd(X3,X2))),
inference(step,[status(thm)],[t11483,t3726]) ).
cnf(t24820,plain,
mult(X1,mult(X2,X2)) = mult(mult(rd(X1,ld(X3,rd(X3,X2))),ld(X2,X2)),X2),
inference(step,[status(thm)],[t24819,t3726]) ).
cnf(t24821,plain,
mult(X1,mult(X2,X2)) = mult(rd(rd(X1,ld(X3,rd(X3,X2))),ld(X2,X2)),X2),
inference(step,[status(thm)],[t24820,t3790]) ).
cnf(t24822,plain,
mult(X1,mult(X2,X2)) = mult(rd(mult(X1,X2),ld(X2,X2)),X2),
inference(step,[status(thm)],[t24821,t3726]) ).
cnf(t16311,plain,
mult(rd(mult(X1,X2),ld(X2,X2)),X2) = mult(X1,mult(X2,X2)),
inference(orient,[status(thm)],[t24822]) ).
cnf(t16430,plain,
mult(rd(X1,X2),mult(X2,X2)) = mult(rd(X1,ld(X2,X2)),X2),
inference(cp,[status(thm)],[t16311,t8]) ).
cnf(t16496,plain,
mult(rd(X1,ld(X2,X2)),X2) = mult(rd(X1,X2),mult(X2,X2)),
inference(orient,[status(thm)],[t16430]) ).
cnf(t16528,plain,
rd(X1,ld(X2,X2)) = rd(mult(rd(X1,X2),mult(X2,X2)),X2),
inference(cp,[status(thm)],[t9,t16496]) ).
cnf(t24823,plain,
rd(X1,ld(X2,X2)) = mult(X1,rd(X2,X2)),
inference(step,[status(thm)],[t16528,t11299]) ).
cnf(t16581,plain,
mult(X1,rd(X2,X2)) = rd(X1,ld(X2,X2)),
inference(orient,[status(thm)],[t24823]) ).
cnf(t16611,plain,
rd(X1,X1) = ld(X2,rd(X2,ld(X1,X1))),
inference(cp,[status(thm)],[t11,t16581]) ).
cnf(t24824,plain,
rd(X1,X1) = ld(X1,X1),
inference(step,[status(thm)],[t16611,t4013]) ).
cnf(t16661,plain,
ld(X1,X1) = rd(X1,X1),
inference(orient,[status(thm)],[t24824]) ).
cnf(t16673,plain,
rd(mult(X1,X1),ld(X1,X1)) = mult(X1,mult(rd(X1,X1),X1)),
inference(cp,[status(thm)],[t7895,t16661]) ).
cnf(t24843,plain,
rd(mult(X1,X1),rd(X1,X1)) = mult(X1,mult(rd(X1,X1),X1)),
inference(step,[status(thm)],[t16673,t16661]) ).
cnf(t24844,plain,
rd(mult(X1,X1),rd(X1,X1)) = mult(X1,X1),
inference(step,[status(thm)],[t24843,t8]) ).
cnf(t16752,plain,
rd(mult(X1,X1),rd(X1,X1)) = mult(X1,X1),
inference(orient,[status(thm)],[t24844]) ).
cnf(t16784,plain,
mult(X1,X1) = mult(mult(X1,X1),rd(X1,X1)),
inference(cp,[status(thm)],[t8,t16752]) ).
cnf(t24850,plain,
mult(X1,X1) = rd(mult(X1,mult(X1,X1)),X1),
inference(step,[status(thm)],[t16784,t1111]) ).
cnf(t17050,plain,
rd(mult(X1,mult(X1,X1)),X1) = mult(X1,X1),
inference(orient,[status(thm)],[t24850]) ).
cnf(t17080,plain,
mult(X1,mult(X1,X1)) = mult(mult(X1,X1),X1),
inference(cp,[status(thm)],[t8,t17050]) ).
cnf(t17147,plain,
mult(mult(X1,X1),X1) = mult(X1,mult(X1,X1)),
inference(orient,[status(thm)],[t17080]) ).
cnf(t17202,plain,
mult(rd(mult(rd(x0,sFlat0),rd(x0,sFlat0)),sFlat0),sFlat1) = rd(mult(rd(x0,sFlat0),mult(rd(x0,sFlat0),rd(x0,sFlat0))),sFlat0),
inference(cp,[status(thm)],[t5662,t17147]) ).
cnf(t24862,plain,
mult(mult(rd(rd(x0,sFlat0),sFlat0),sFlat1),sFlat1) = rd(mult(rd(x0,sFlat0),mult(rd(x0,sFlat0),rd(x0,sFlat0))),sFlat0),
inference(step,[status(thm)],[t17202,t5662]) ).
cnf(t24863,plain,
mult(mult(x0,sFlat1),sFlat1) = rd(mult(rd(x0,sFlat0),mult(rd(x0,sFlat0),rd(x0,sFlat0))),sFlat0),
inference(step,[status(thm)],[t24862,t1928]) ).
cnf(t5677,plain,
mult(X1,rd(x0,sFlat0)) = rd(mult(rd(X1,sFlat0),sFlat1),sFlat0),
inference(cp,[status(thm)],[t1928,t5662]) ).
cnf(t5696,plain,
rd(mult(rd(X1,sFlat0),sFlat1),sFlat0) = mult(X1,rd(x0,sFlat0)),
inference(orient,[status(thm)],[t5677]) ).
cnf(t5711,plain,
mult(rd(X1,sFlat0),rd(x0,sFlat0)) = rd(mult(X1,sFlat1),sFlat0),
inference(cp,[status(thm)],[t5696,t1928]) ).
cnf(t5741,plain,
mult(rd(X1,sFlat0),rd(x0,sFlat0)) = rd(mult(X1,sFlat1),sFlat0),
inference(orient,[status(thm)],[t5711]) ).
cnf(t24864,plain,
mult(mult(x0,sFlat1),sFlat1) = rd(mult(rd(x0,sFlat0),rd(mult(x0,sFlat1),sFlat0)),sFlat0),
inference(step,[status(thm)],[t24863,t5741]) ).
cnf(t24865,plain,
mult(mult(x0,sFlat1),sFlat1) = rd(rd(mult(x0,mult(sFlat0,mult(x0,sFlat1))),sFlat0),sFlat0),
inference(step,[status(thm)],[t24864,t6721]) ).
cnf(t24866,plain,
mult(mult(x0,sFlat1),sFlat1) = mult(x0,mult(sFlat0,mult(x0,sFlat1))),
inference(step,[status(thm)],[t24865,t1928]) ).
cnf(t17521,plain,
mult(x0,mult(sFlat0,mult(x0,sFlat1))) = mult(mult(x0,sFlat1),sFlat1),
inference(orient,[status(thm)],[t24866]) ).
cnf(t17526,plain,
mult(sFlat0,mult(x0,sFlat1)) = ld(x0,mult(mult(x0,sFlat1),sFlat1)),
inference(cp,[status(thm)],[t11,t17521]) ).
cnf(t17542,plain,
ld(x0,mult(mult(x0,sFlat1),sFlat1)) = mult(sFlat0,mult(x0,sFlat1)),
inference(orient,[status(thm)],[t17526]) ).
cnf(t25056,plain,
mult(sFlat1,x0) = mult(sFlat0,mult(x0,sFlat1)),
inference(step,[status(thm)],[t25055,t17542]) ).
cnf(t23858,plain,
mult(sFlat0,mult(x0,sFlat1)) = mult(sFlat1,x0),
inference(orient,[status(thm)],[t25056]) ).
cnf(t23885,plain,
ld(sFlat0,mult(rd(sFlat1,mult(x0,sFlat1)),x0)) = ld(rd(mult(sFlat1,x0),x0),sFlat1),
inference(cp,[status(thm)],[t9614,t23858]) ).
cnf(t565,plain,
rd(sFlat0,sFlat0) = mult(rd(sFlat1,mult(x0,sFlat1)),x0),
inference(cp,[status(thm)],[t8,t562]) ).
cnf(t569,plain,
mult(rd(sFlat1,mult(x0,sFlat1)),x0) = rd(sFlat0,sFlat0),
inference(orient,[status(thm)],[t565]) ).
cnf(t25068,plain,
ld(sFlat0,rd(sFlat0,sFlat0)) = ld(rd(mult(sFlat1,x0),x0),sFlat1),
inference(step,[status(thm)],[t23885,t569]) ).
cnf(t25069,plain,
ld(sFlat0,sFlat0) = ld(rd(mult(sFlat1,x0),x0),sFlat1),
inference(step,[status(thm)],[t25068,t2402]) ).
cnf(t24290,plain,
ld(sFlat0,sFlat0) = rd(sFlat0,sFlat0),
inference(step,[status(thm)],[t1818,t1858]) ).
cnf(t1873,plain,
ld(sFlat0,sFlat0) = rd(sFlat0,sFlat0),
inference(orient,[status(thm)],[t24290]) ).
cnf(t24377,plain,
ld(sFlat0,sFlat0) = sFlat0,
inference(step,[status(thm)],[t1873,t2402]) ).
cnf(t2403,plain,
ld(sFlat0,sFlat0) = sFlat0,
inference(orient,[status(thm)],[t24377]) ).
cnf(t25070,plain,
sFlat0 = ld(rd(mult(sFlat1,x0),x0),sFlat1),
inference(step,[status(thm)],[t25069,t2403]) ).
cnf(t25071,plain,
sFlat0 = ld(sFlat1,sFlat1),
inference(step,[status(thm)],[t25070,t9]) ).
cnf(t25072,plain,
sFlat0 = rd(sFlat1,sFlat1),
inference(step,[status(thm)],[t25071,t16661]) ).
cnf(t23909,plain,
rd(sFlat1,sFlat1) = sFlat0,
inference(orient,[status(thm)],[t25072]) ).
cnf(t23926,plain,
sFlat1 = ld(sFlat0,sFlat1),
inference(cp,[status(thm)],[t39,t23909]) ).
cnf(t25097,plain,
sFlat1 = x0,
inference(step,[status(thm)],[t23926,t36]) ).
cnf(t23960,plain,
x0 = sFlat1,
inference(orient,[status(thm)],[t25097]) ).
cnf(goal_0,negated_conjecture,
mult(rd(x1,x1),x0) != x0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
sFlat1 != x0,
inference(rw,[status(thm)],[goal_0]) ).
cnf(g0_1,plain,
sFlat1 != sFlat1,
inference(rw,[status(thm)],[g0_0,t23960]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP655-12 : 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 : n006.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.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Wed Sep 23 15:30:11 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 33.14/5.07 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 33.14/5.07 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------