%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP655-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 : 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:27:52 PM UTC 2026
% Result : Unsatisfiable 54.41s 7.33s
% Output : CNFRefutation 54.41s
% Verified :
% SZS Type : Refutation
% Derivation depth : 94
% Number of leaves : 8
% Syntax : Number of clauses : 354 ( 354 unt; 0 nHn; 46 RR)
% Number of literals : 354 ( 353 equ; 6 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 : 512 ( 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(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(t14,plain,
mult(X1,mult(X2,mult(ld(mult(X1,X2),X3),X2))) = mult(X3,X2),
inference(cp,[status(thm)],[t13,t7]) ).
cnf(t196,plain,
mult(X1,mult(X2,mult(ld(mult(X1,X2),X3),X2))) = mult(X3,X2),
inference(orient,[status(thm)],[t14]) ).
cnf(t217,plain,
mult(X1,mult(ld(mult(X2,X1),X3),X1)) = ld(X2,mult(X3,X1)),
inference(cp,[status(thm)],[t11,t196]) ).
cnf(t10595,plain,
mult(X1,mult(ld(mult(X2,X1),X3),X1)) = ld(X2,mult(X3,X1)),
inference(orient,[status(thm)],[t217]) ).
cnf(t10694,plain,
ld(rd(X1,X2),mult(X3,X2)) = mult(X2,mult(ld(X1,X3),X2)),
inference(cp,[status(thm)],[t10595,t8]) ).
cnf(t10743,plain,
ld(rd(X1,X2),mult(X3,X2)) = mult(X2,mult(ld(X1,X3),X2)),
inference(orient,[status(thm)],[t10694]) ).
cnf(t10969,plain,
mult(X1,mult(ld(X2,rd(X3,X1)),X1)) = ld(rd(X2,X1),X3),
inference(cp,[status(thm)],[t10743,t8]) ).
cnf(t26855,plain,
mult(X1,mult(ld(X2,rd(X3,X1)),X1)) = ld(rd(X2,X1),X3),
inference(orient,[status(thm)],[t10969]) ).
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(t26900,plain,
ld(rd(rd(rd(X1,X2),X3),X2),X1) = mult(X2,mult(X3,X2)),
inference(cp,[status(thm)],[t26855,t39]) ).
cnf(t39227,plain,
ld(rd(rd(rd(X1,X2),X3),X2),X1) = mult(X2,mult(X3,X2)),
inference(orient,[status(thm)],[t26900]) ).
cnf(t39609,plain,
rd(rd(rd(X1,X2),X3),X2) = rd(X1,mult(X2,mult(X3,X2))),
inference(cp,[status(thm)],[t38,t39227]) ).
cnf(t39638,plain,
rd(rd(rd(X1,X2),X3),X2) = rd(X1,mult(X2,mult(X3,X2))),
inference(orient,[status(thm)],[t39609]) ).
cnf(t40030,plain,
rd(rd(X1,X2),X3) = mult(rd(X1,mult(X2,mult(X3,X2))),X2),
inference(cp,[status(thm)],[t8,t39638]) ).
cnf(t46853,plain,
mult(rd(X1,mult(X2,mult(X3,X2))),X2) = rd(rd(X1,X2),X3),
inference(orient,[status(thm)],[t40030]) ).
cnf(t47023,plain,
rd(rd(X1,X2),rd(X3,X2)) = mult(rd(X1,mult(X2,X3)),X2),
inference(cp,[status(thm)],[t46853,t8]) ).
cnf(t47086,plain,
mult(rd(X1,mult(X2,X3)),X2) = rd(rd(X1,X2),rd(X3,X2)),
inference(orient,[status(thm)],[t47023]) ).
cnf(t16,plain,
mult(rd(X1,X2),mult(X2,mult(X3,X2))) = mult(mult(X1,X3),X2),
inference(cp,[status(thm)],[t13,t8]) ).
cnf(t234,plain,
mult(rd(X1,X2),mult(X2,mult(X3,X2))) = mult(mult(X1,X3),X2),
inference(orient,[status(thm)],[t16]) ).
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(t5,axiom,
sFlat0 = rd(x1,x1),
introduced(definition) ).
cnf(t25,plain,
rd(x1,x1) = sFlat0,
inference(orient,[status(thm)],[t5]) ).
cnf(t111173,plain,
mult(x0,sFlat0) = sFlat1,
inference(step,[status(thm)],[t21,t25]) ).
cnf(t27,plain,
mult(x0,sFlat0) = sFlat1,
inference(rw,[status(thm)],[t111173]) ).
cnf(t31,plain,
mult(x0,sFlat0) = sFlat1,
inference(orient,[status(thm)],[t27]) ).
cnf(t34,plain,
mult(x0,mult(sFlat0,mult(X1,sFlat0))) = mult(mult(sFlat1,X1),sFlat0),
inference(cp,[status(thm)],[t13,t31]) ).
cnf(t55,plain,
mult(x0,mult(sFlat0,mult(X1,sFlat0))) = mult(mult(sFlat1,X1),sFlat0),
inference(orient,[status(thm)],[t34]) ).
cnf(t59,plain,
mult(sFlat0,mult(X1,sFlat0)) = ld(x0,mult(mult(sFlat1,X1),sFlat0)),
inference(cp,[status(thm)],[t11,t55]) ).
cnf(t87,plain,
ld(x0,mult(mult(sFlat1,X1),sFlat0)) = mult(sFlat0,mult(X1,sFlat0)),
inference(orient,[status(thm)],[t59]) ).
cnf(t88,plain,
mult(sFlat0,mult(ld(sFlat1,X1),sFlat0)) = ld(x0,mult(X1,sFlat0)),
inference(cp,[status(thm)],[t87,t7]) ).
cnf(t111,plain,
mult(sFlat0,mult(ld(sFlat1,X1),sFlat0)) = ld(x0,mult(X1,sFlat0)),
inference(orient,[status(thm)],[t88]) ).
cnf(t112,plain,
mult(ld(sFlat1,X1),sFlat0) = ld(sFlat0,ld(x0,mult(X1,sFlat0))),
inference(cp,[status(thm)],[t11,t111]) ).
cnf(t140,plain,
ld(sFlat0,ld(x0,mult(X1,sFlat0))) = mult(ld(sFlat1,X1),sFlat0),
inference(orient,[status(thm)],[t112]) ).
cnf(t141,plain,
mult(ld(sFlat1,x0),sFlat0) = ld(sFlat0,sFlat0),
inference(cp,[status(thm)],[t140,t11]) ).
cnf(t146,plain,
mult(ld(sFlat1,x0),sFlat0) = ld(sFlat0,sFlat0),
inference(orient,[status(thm)],[t141]) ).
cnf(t251,plain,
mult(mult(X1,ld(sFlat1,x0)),sFlat0) = mult(rd(X1,sFlat0),mult(sFlat0,ld(sFlat0,sFlat0))),
inference(cp,[status(thm)],[t234,t146]) ).
cnf(t111176,plain,
mult(mult(X1,ld(sFlat1,x0)),sFlat0) = mult(rd(X1,sFlat0),sFlat0),
inference(step,[status(thm)],[t251,t7]) ).
cnf(t111177,plain,
mult(mult(X1,ld(sFlat1,x0)),sFlat0) = X1,
inference(step,[status(thm)],[t111176,t8]) ).
cnf(t316,plain,
mult(mult(X1,ld(sFlat1,x0)),sFlat0) = X1,
inference(orient,[status(thm)],[t111177]) ).
cnf(t320,plain,
mult(X1,ld(sFlat1,x0)) = rd(X1,sFlat0),
inference(cp,[status(thm)],[t9,t316]) ).
cnf(t331,plain,
mult(X1,ld(sFlat1,x0)) = rd(X1,sFlat0),
inference(orient,[status(thm)],[t320]) ).
cnf(t318,plain,
rd(X1,ld(sFlat1,x0)) = mult(X1,sFlat0),
inference(cp,[status(thm)],[t316,t8]) ).
cnf(t327,plain,
rd(X1,ld(sFlat1,x0)) = mult(X1,sFlat0),
inference(orient,[status(thm)],[t318]) ).
cnf(t328,plain,
ld(sFlat1,x0) = ld(mult(X1,sFlat0),X1),
inference(cp,[status(thm)],[t39,t327]) ).
cnf(t344,plain,
ld(mult(X1,sFlat0),X1) = ld(sFlat1,x0),
inference(orient,[status(thm)],[t328]) ).
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(t616,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(t647,plain,
mult(mult(X1,X2),ld(X2,X1)) = mult(X2,mult(ld(X2,X1),X1)),
inference(cp,[status(thm)],[t616,t7]) ).
cnf(t706,plain,
mult(mult(X1,X2),ld(X2,X1)) = mult(X2,mult(ld(X2,X1),X1)),
inference(orient,[status(thm)],[t647]) ).
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(t120,plain,
ld(x1,ld(sFlat0,mult(X1,x1))) = mult(ld(x1,X1),x1),
inference(orient,[status(thm)],[t95]) ).
cnf(t121,plain,
mult(ld(x1,sFlat0),x1) = ld(x1,x1),
inference(cp,[status(thm)],[t120,t11]) ).
cnf(t127,plain,
mult(ld(x1,sFlat0),x1) = ld(x1,x1),
inference(orient,[status(thm)],[t121]) ).
cnf(t249,plain,
mult(mult(X1,ld(x1,sFlat0)),x1) = mult(rd(X1,x1),mult(x1,ld(x1,x1))),
inference(cp,[status(thm)],[t234,t127]) ).
cnf(t111174,plain,
mult(mult(X1,ld(x1,sFlat0)),x1) = mult(rd(X1,x1),x1),
inference(step,[status(thm)],[t249,t7]) ).
cnf(t111175,plain,
mult(mult(X1,ld(x1,sFlat0)),x1) = X1,
inference(step,[status(thm)],[t111174,t8]) ).
cnf(t273,plain,
mult(mult(X1,ld(x1,sFlat0)),x1) = X1,
inference(orient,[status(thm)],[t111175]) ).
cnf(t277,plain,
mult(X1,ld(x1,sFlat0)) = rd(X1,x1),
inference(cp,[status(thm)],[t9,t273]) ).
cnf(t288,plain,
mult(X1,ld(x1,sFlat0)) = rd(X1,x1),
inference(orient,[status(thm)],[t277]) ).
cnf(t708,plain,
mult(x1,mult(ld(x1,sFlat0),sFlat0)) = rd(mult(sFlat0,x1),x1),
inference(cp,[status(thm)],[t706,t288]) ).
cnf(t111179,plain,
mult(x1,mult(ld(x1,sFlat0),sFlat0)) = sFlat0,
inference(step,[status(thm)],[t708,t9]) ).
cnf(t780,plain,
mult(x1,mult(ld(x1,sFlat0),sFlat0)) = sFlat0,
inference(orient,[status(thm)],[t111179]) ).
cnf(t782,plain,
mult(ld(x1,sFlat0),sFlat0) = ld(x1,sFlat0),
inference(cp,[status(thm)],[t11,t780]) ).
cnf(t789,plain,
mult(ld(x1,sFlat0),sFlat0) = ld(x1,sFlat0),
inference(orient,[status(thm)],[t782]) ).
cnf(t794,plain,
ld(sFlat1,x0) = ld(ld(x1,sFlat0),ld(x1,sFlat0)),
inference(cp,[status(thm)],[t344,t789]) ).
cnf(t795,plain,
sFlat0 = ld(ld(x1,sFlat0),ld(x1,sFlat0)),
inference(cp,[status(thm)],[t11,t789]) ).
cnf(t825,plain,
ld(ld(x1,sFlat0),ld(x1,sFlat0)) = sFlat0,
inference(orient,[status(thm)],[t795]) ).
cnf(t111189,plain,
ld(sFlat1,x0) = sFlat0,
inference(step,[status(thm)],[t794,t825]) ).
cnf(t829,plain,
ld(sFlat1,x0) = sFlat0,
inference(orient,[status(thm)],[t111189]) ).
cnf(t111214,plain,
mult(X1,sFlat0) = rd(X1,sFlat0),
inference(step,[status(thm)],[t331,t829]) ).
cnf(t855,plain,
mult(X1,sFlat0) = rd(X1,sFlat0),
inference(rw,[status(thm)],[t111214]) ).
cnf(t880,plain,
mult(X1,sFlat0) = rd(X1,sFlat0),
inference(orient,[status(thm)],[t855]) ).
cnf(t47144,plain,
rd(rd(X1,X2),rd(sFlat0,X2)) = mult(rd(X1,rd(X2,sFlat0)),X2),
inference(cp,[status(thm)],[t47086,t880]) ).
cnf(t47301,plain,
mult(rd(X1,rd(X2,sFlat0)),X2) = rd(rd(X1,X2),rd(sFlat0,X2)),
inference(orient,[status(thm)],[t47144]) ).
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(t47506,plain,
rd(rd(X1,sFlat1),rd(sFlat0,sFlat1)) = mult(rd(X1,x0),sFlat1),
inference(cp,[status(thm)],[t47301,t37]) ).
cnf(t47617,plain,
rd(rd(X1,sFlat1),rd(sFlat0,sFlat1)) = mult(rd(X1,x0),sFlat1),
inference(orient,[status(thm)],[t47506]) ).
cnf(t47632,plain,
mult(rd(mult(X1,sFlat1),x0),sFlat1) = rd(X1,rd(sFlat0,sFlat1)),
inference(cp,[status(thm)],[t47617,t9]) ).
cnf(t47776,plain,
mult(rd(mult(X1,sFlat1),x0),sFlat1) = rd(X1,rd(sFlat0,sFlat1)),
inference(orient,[status(thm)],[t47632]) ).
cnf(t47796,plain,
sFlat1 = ld(rd(mult(X1,sFlat1),x0),rd(X1,rd(sFlat0,sFlat1))),
inference(cp,[status(thm)],[t11,t47776]) ).
cnf(t58277,plain,
ld(rd(mult(X1,sFlat1),x0),rd(X1,rd(sFlat0,sFlat1))) = sFlat1,
inference(orient,[status(thm)],[t47796]) ).
cnf(t889,plain,
rd(rd(X1,sFlat0),sFlat0) = X1,
inference(cp,[status(thm)],[t880,t8]) ).
cnf(t926,plain,
rd(rd(X1,sFlat0),sFlat0) = X1,
inference(orient,[status(thm)],[t889]) ).
cnf(t10744,plain,
mult(X1,mult(ld(X2,rd(X2,X1)),X1)) = X1,
inference(cp,[status(thm)],[t10743,t11]) ).
cnf(t11244,plain,
mult(X1,mult(ld(X2,rd(X2,X1)),X1)) = X1,
inference(orient,[status(thm)],[t10744]) ).
cnf(t11364,plain,
mult(ld(X1,rd(X1,X2)),X2) = ld(X2,X2),
inference(cp,[status(thm)],[t11,t11244]) ).
cnf(t11387,plain,
mult(ld(X1,rd(X1,X2)),X2) = ld(X2,X2),
inference(orient,[status(thm)],[t11364]) ).
cnf(t11519,plain,
mult(mult(X1,ld(X2,rd(X2,X3))),X3) = mult(rd(X1,X3),mult(X3,ld(X3,X3))),
inference(cp,[status(thm)],[t234,t11387]) ).
cnf(t111572,plain,
mult(mult(X1,ld(X2,rd(X2,X3))),X3) = mult(rd(X1,X3),X3),
inference(step,[status(thm)],[t11519,t7]) ).
cnf(t111573,plain,
mult(mult(X1,ld(X2,rd(X2,X3))),X3) = X1,
inference(step,[status(thm)],[t111572,t8]) ).
cnf(t11808,plain,
mult(mult(X1,ld(X2,rd(X2,X3))),X3) = X1,
inference(orient,[status(thm)],[t111573]) ).
cnf(t11819,plain,
rd(X1,ld(X2,rd(X2,X3))) = mult(X1,X3),
inference(cp,[status(thm)],[t11808,t8]) ).
cnf(t11966,plain,
rd(X1,ld(X2,rd(X2,X3))) = mult(X1,X3),
inference(orient,[status(thm)],[t11819]) ).
cnf(t11970,plain,
mult(X1,ld(X2,X3)) = rd(X1,ld(X3,X2)),
inference(cp,[status(thm)],[t11966,t38]) ).
cnf(t12097,plain,
mult(X1,ld(X2,X3)) = rd(X1,ld(X3,X2)),
inference(orient,[status(thm)],[t11970]) ).
cnf(t12194,plain,
ld(X1,X2) = ld(X3,rd(X3,ld(X2,X1))),
inference(cp,[status(thm)],[t11,t12097]) ).
cnf(t12356,plain,
ld(X1,rd(X1,ld(X2,X3))) = ld(X3,X2),
inference(orient,[status(thm)],[t12194]) ).
cnf(t852,plain,
mult(mult(x0,X1),ld(sFlat1,x0)) = mult(sFlat1,mult(sFlat0,mult(X1,ld(sFlat1,x0)))),
inference(cp,[status(thm)],[t616,t829]) ).
cnf(t111269,plain,
mult(mult(x0,X1),sFlat0) = mult(sFlat1,mult(sFlat0,mult(X1,ld(sFlat1,x0)))),
inference(step,[status(thm)],[t852,t829]) ).
cnf(t111270,plain,
rd(mult(x0,X1),sFlat0) = mult(sFlat1,mult(sFlat0,mult(X1,ld(sFlat1,x0)))),
inference(step,[status(thm)],[t111269,t880]) ).
cnf(t111271,plain,
rd(mult(x0,X1),sFlat0) = mult(sFlat1,mult(sFlat0,mult(X1,sFlat0))),
inference(step,[status(thm)],[t111270,t829]) ).
cnf(t111272,plain,
rd(mult(x0,X1),sFlat0) = mult(sFlat1,mult(sFlat0,rd(X1,sFlat0))),
inference(step,[status(thm)],[t111271,t880]) ).
cnf(t1150,plain,
mult(sFlat1,mult(sFlat0,rd(X1,sFlat0))) = rd(mult(x0,X1),sFlat0),
inference(orient,[status(thm)],[t111272]) ).
cnf(t1163,plain,
mult(sFlat0,rd(X1,sFlat0)) = ld(sFlat1,rd(mult(x0,X1),sFlat0)),
inference(cp,[status(thm)],[t11,t1150]) ).
cnf(t58,plain,
mult(mult(sFlat1,rd(X1,sFlat0)),sFlat0) = mult(x0,mult(sFlat0,X1)),
inference(cp,[status(thm)],[t55,t8]) ).
cnf(t80,plain,
mult(mult(sFlat1,rd(X1,sFlat0)),sFlat0) = mult(x0,mult(sFlat0,X1)),
inference(orient,[status(thm)],[t58]) ).
cnf(t83,plain,
mult(sFlat1,rd(X1,sFlat0)) = rd(mult(x0,mult(sFlat0,X1)),sFlat0),
inference(cp,[status(thm)],[t9,t80]) ).
cnf(t99,plain,
rd(mult(x0,mult(sFlat0,X1)),sFlat0) = mult(sFlat1,rd(X1,sFlat0)),
inference(orient,[status(thm)],[t83]) ).
cnf(t102,plain,
mult(sFlat1,rd(ld(sFlat0,X1),sFlat0)) = rd(mult(x0,X1),sFlat0),
inference(cp,[status(thm)],[t99,t7]) ).
cnf(t135,plain,
mult(sFlat1,rd(ld(sFlat0,X1),sFlat0)) = rd(mult(x0,X1),sFlat0),
inference(orient,[status(thm)],[t102]) ).
cnf(t137,plain,
rd(ld(sFlat0,X1),sFlat0) = ld(sFlat1,rd(mult(x0,X1),sFlat0)),
inference(cp,[status(thm)],[t11,t135]) ).
cnf(t165,plain,
ld(sFlat1,rd(mult(x0,X1),sFlat0)) = rd(ld(sFlat0,X1),sFlat0),
inference(orient,[status(thm)],[t137]) ).
cnf(t111273,plain,
mult(sFlat0,rd(X1,sFlat0)) = rd(ld(sFlat0,X1),sFlat0),
inference(step,[status(thm)],[t1163,t165]) ).
cnf(t1168,plain,
mult(sFlat0,rd(X1,sFlat0)) = rd(ld(sFlat0,X1),sFlat0),
inference(orient,[status(thm)],[t111273]) ).
cnf(t1172,plain,
rd(ld(sFlat0,rd(X1,sFlat0)),sFlat0) = mult(sFlat0,X1),
inference(cp,[status(thm)],[t1168,t926]) ).
cnf(t1189,plain,
rd(ld(sFlat0,rd(X1,sFlat0)),sFlat0) = mult(sFlat0,X1),
inference(orient,[status(thm)],[t1172]) ).
cnf(t1201,plain,
ld(sFlat0,rd(X1,sFlat0)) = rd(mult(sFlat0,X1),sFlat0),
inference(cp,[status(thm)],[t926,t1189]) ).
cnf(t1210,plain,
ld(sFlat0,rd(X1,sFlat0)) = rd(mult(sFlat0,X1),sFlat0),
inference(orient,[status(thm)],[t1201]) ).
cnf(t12419,plain,
ld(rd(X1,sFlat0),sFlat0) = ld(X2,rd(X2,rd(mult(sFlat0,X1),sFlat0))),
inference(cp,[status(thm)],[t12356,t1210]) ).
cnf(t28044,plain,
ld(X1,rd(X1,rd(mult(sFlat0,X2),sFlat0))) = ld(rd(X2,sFlat0),sFlat0),
inference(orient,[status(thm)],[t12419]) ).
cnf(t267,plain,
mult(mult(X1,rd(X2,X3)),X3) = mult(rd(X1,X3),mult(X3,X2)),
inference(cp,[status(thm)],[t234,t8]) ).
cnf(t382,plain,
mult(mult(X1,rd(X2,X3)),X3) = mult(rd(X1,X3),mult(X3,X2)),
inference(orient,[status(thm)],[t267]) ).
cnf(t398,plain,
mult(X1,rd(X2,X3)) = rd(mult(rd(X1,X3),mult(X3,X2)),X3),
inference(cp,[status(thm)],[t9,t382]) ).
cnf(t24941,plain,
rd(mult(rd(X1,X2),mult(X2,X3)),X2) = mult(X1,rd(X3,X2)),
inference(orient,[status(thm)],[t398]) ).
cnf(t25167,plain,
mult(X1,rd(sFlat0,X2)) = rd(mult(rd(X1,X2),rd(X2,sFlat0)),X2),
inference(cp,[status(thm)],[t24941,t880]) ).
cnf(t32828,plain,
rd(mult(rd(X1,X2),rd(X2,sFlat0)),X2) = mult(X1,rd(sFlat0,X2)),
inference(orient,[status(thm)],[t25167]) ).
cnf(t18,plain,
mult(mult(X1,X2),X3) = rd(mult(X1,mult(X2,mult(X3,X2))),X2),
inference(cp,[status(thm)],[t9,t13]) ).
cnf(t2162,plain,
rd(mult(X1,mult(X2,mult(X3,X2))),X2) = mult(mult(X1,X2),X3),
inference(orient,[status(thm)],[t18]) ).
cnf(t1184,plain,
mult(rd(sFlat0,sFlat0),mult(sFlat0,X1)) = mult(rd(ld(sFlat0,X1),sFlat0),sFlat0),
inference(cp,[status(thm)],[t382,t1168]) ).
cnf(t111274,plain,
mult(rd(sFlat0,sFlat0),mult(sFlat0,X1)) = ld(sFlat0,X1),
inference(step,[status(thm)],[t1184,t8]) ).
cnf(t1226,plain,
mult(rd(sFlat0,sFlat0),mult(sFlat0,X1)) = ld(sFlat0,X1),
inference(orient,[status(thm)],[t111274]) ).
cnf(t1228,plain,
ld(sFlat0,x1) = mult(rd(sFlat0,sFlat0),x1),
inference(cp,[status(thm)],[t1226,t28]) ).
cnf(t29,plain,
x1 = ld(sFlat0,x1),
inference(cp,[status(thm)],[t11,t28]) ).
cnf(t35,plain,
ld(sFlat0,x1) = x1,
inference(orient,[status(thm)],[t29]) ).
cnf(t111275,plain,
x1 = mult(rd(sFlat0,sFlat0),x1),
inference(step,[status(thm)],[t1228,t35]) ).
cnf(t1317,plain,
mult(rd(sFlat0,sFlat0),x1) = x1,
inference(orient,[status(thm)],[t111275]) ).
cnf(t1322,plain,
rd(sFlat0,sFlat0) = rd(x1,x1),
inference(cp,[status(thm)],[t9,t1317]) ).
cnf(t111276,plain,
rd(sFlat0,sFlat0) = sFlat0,
inference(step,[status(thm)],[t1322,t25]) ).
cnf(t1330,plain,
rd(sFlat0,sFlat0) = sFlat0,
inference(orient,[status(thm)],[t111276]) ).
cnf(t111281,plain,
mult(sFlat0,mult(sFlat0,X1)) = ld(sFlat0,X1),
inference(step,[status(thm)],[t1226,t1330]) ).
cnf(t1339,plain,
mult(sFlat0,mult(sFlat0,X1)) = ld(sFlat0,X1),
inference(rw,[status(thm)],[t111281]) ).
cnf(t1353,plain,
mult(sFlat0,mult(sFlat0,X1)) = ld(sFlat0,X1),
inference(orient,[status(thm)],[t1339]) ).
cnf(t1362,plain,
sFlat0 = rd(ld(sFlat0,X1),mult(sFlat0,X1)),
inference(cp,[status(thm)],[t9,t1353]) ).
cnf(t1423,plain,
rd(ld(sFlat0,X1),mult(sFlat0,X1)) = sFlat0,
inference(orient,[status(thm)],[t1362]) ).
cnf(t11487,plain,
ld(mult(sFlat0,X1),mult(sFlat0,X1)) = mult(ld(ld(sFlat0,X1),sFlat0),mult(sFlat0,X1)),
inference(cp,[status(thm)],[t11387,t1423]) ).
cnf(t25171,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)],[t24941,t11387]) ).
cnf(t111928,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)],[t25171,t11966]) ).
cnf(t111929,plain,
mult(X1,mult(X2,X2)) = mult(mult(rd(X1,ld(X3,rd(X3,X2))),ld(X2,X2)),X2),
inference(step,[status(thm)],[t111928,t11966]) ).
cnf(t111930,plain,
mult(X1,mult(X2,X2)) = mult(rd(rd(X1,ld(X3,rd(X3,X2))),ld(X2,X2)),X2),
inference(step,[status(thm)],[t111929,t12097]) ).
cnf(t111931,plain,
mult(X1,mult(X2,X2)) = mult(rd(mult(X1,X2),ld(X2,X2)),X2),
inference(step,[status(thm)],[t111930,t11966]) ).
cnf(t33164,plain,
mult(rd(mult(X1,X2),ld(X2,X2)),X2) = mult(X1,mult(X2,X2)),
inference(orient,[status(thm)],[t111931]) ).
cnf(t33294,plain,
mult(rd(X1,X2),mult(X2,X2)) = mult(rd(X1,ld(X2,X2)),X2),
inference(cp,[status(thm)],[t33164,t8]) ).
cnf(t33348,plain,
mult(rd(X1,ld(X2,X2)),X2) = mult(rd(X1,X2),mult(X2,X2)),
inference(orient,[status(thm)],[t33294]) ).
cnf(t33380,plain,
rd(X1,ld(X2,X2)) = rd(mult(rd(X1,X2),mult(X2,X2)),X2),
inference(cp,[status(thm)],[t9,t33348]) ).
cnf(t111932,plain,
rd(X1,ld(X2,X2)) = mult(X1,rd(X2,X2)),
inference(step,[status(thm)],[t33380,t24941]) ).
cnf(t33483,plain,
mult(X1,rd(X2,X2)) = rd(X1,ld(X2,X2)),
inference(orient,[status(thm)],[t111932]) ).
cnf(t33510,plain,
rd(X1,X1) = ld(X2,rd(X2,ld(X1,X1))),
inference(cp,[status(thm)],[t11,t33483]) ).
cnf(t111941,plain,
rd(X1,X1) = ld(X1,X1),
inference(step,[status(thm)],[t33510,t12356]) ).
cnf(t33566,plain,
ld(X1,X1) = rd(X1,X1),
inference(orient,[status(thm)],[t111941]) ).
cnf(t112794,plain,
rd(mult(sFlat0,X1),mult(sFlat0,X1)) = mult(ld(ld(sFlat0,X1),sFlat0),mult(sFlat0,X1)),
inference(step,[status(thm)],[t11487,t33566]) ).
cnf(t109195,plain,
mult(ld(ld(sFlat0,X1),sFlat0),mult(sFlat0,X1)) = rd(mult(sFlat0,X1),mult(sFlat0,X1)),
inference(orient,[status(thm)],[t112794]) ).
cnf(t109380,plain,
mult(mult(ld(ld(sFlat0,mult(X1,sFlat0)),sFlat0),sFlat0),X1) = rd(rd(mult(sFlat0,mult(X1,sFlat0)),mult(sFlat0,mult(X1,sFlat0))),sFlat0),
inference(cp,[status(thm)],[t2162,t109195]) ).
cnf(t112795,plain,
mult(rd(ld(ld(sFlat0,mult(X1,sFlat0)),sFlat0),sFlat0),X1) = rd(rd(mult(sFlat0,mult(X1,sFlat0)),mult(sFlat0,mult(X1,sFlat0))),sFlat0),
inference(step,[status(thm)],[t109380,t880]) ).
cnf(t112796,plain,
mult(rd(ld(ld(sFlat0,rd(X1,sFlat0)),sFlat0),sFlat0),X1) = rd(rd(mult(sFlat0,mult(X1,sFlat0)),mult(sFlat0,mult(X1,sFlat0))),sFlat0),
inference(step,[status(thm)],[t112795,t880]) ).
cnf(t112797,plain,
mult(rd(ld(rd(mult(sFlat0,X1),sFlat0),sFlat0),sFlat0),X1) = rd(rd(mult(sFlat0,mult(X1,sFlat0)),mult(sFlat0,mult(X1,sFlat0))),sFlat0),
inference(step,[status(thm)],[t112796,t1210]) ).
cnf(t10881,plain,
mult(sFlat0,mult(ld(X1,X2),sFlat0)) = ld(rd(X1,sFlat0),rd(X2,sFlat0)),
inference(cp,[status(thm)],[t10743,t880]) ).
cnf(t111666,plain,
mult(sFlat0,rd(ld(X1,X2),sFlat0)) = ld(rd(X1,sFlat0),rd(X2,sFlat0)),
inference(step,[status(thm)],[t10881,t880]) ).
cnf(t111667,plain,
rd(ld(sFlat0,ld(X1,X2)),sFlat0) = ld(rd(X1,sFlat0),rd(X2,sFlat0)),
inference(step,[status(thm)],[t111666,t1168]) ).
cnf(t14923,plain,
ld(rd(X1,sFlat0),rd(X2,sFlat0)) = rd(ld(sFlat0,ld(X1,X2)),sFlat0),
inference(orient,[status(thm)],[t111667]) ).
cnf(t15115,plain,
rd(ld(sFlat0,ld(X1,sFlat0)),sFlat0) = ld(rd(X1,sFlat0),sFlat0),
inference(cp,[status(thm)],[t14923,t1330]) ).
cnf(t15141,plain,
rd(ld(sFlat0,ld(X1,sFlat0)),sFlat0) = ld(rd(X1,sFlat0),sFlat0),
inference(orient,[status(thm)],[t15115]) ).
cnf(t15144,plain,
ld(rd(rd(sFlat0,X1),sFlat0),sFlat0) = rd(ld(sFlat0,X1),sFlat0),
inference(cp,[status(thm)],[t15141,t39]) ).
cnf(t15368,plain,
ld(rd(rd(sFlat0,X1),sFlat0),sFlat0) = rd(ld(sFlat0,X1),sFlat0),
inference(orient,[status(thm)],[t15144]) ).
cnf(t15371,plain,
rd(ld(sFlat0,ld(X1,rd(X1,X2))),sFlat0) = ld(rd(mult(sFlat0,X2),sFlat0),sFlat0),
inference(cp,[status(thm)],[t15368,t11966]) ).
cnf(t12193,plain,
ld(sFlat0,ld(X1,X2)) = mult(sFlat0,rd(sFlat0,ld(X2,X1))),
inference(cp,[status(thm)],[t1353,t12097]) ).
cnf(t12497,plain,
mult(sFlat0,rd(sFlat0,ld(X1,X2))) = ld(sFlat0,ld(X2,X1)),
inference(orient,[status(thm)],[t12193]) ).
cnf(t12519,plain,
ld(sFlat0,ld(X1,rd(X1,X2))) = mult(sFlat0,rd(sFlat0,X2)),
inference(cp,[status(thm)],[t12497,t39]) ).
cnf(t14194,plain,
ld(sFlat0,ld(X1,rd(X1,X2))) = mult(sFlat0,rd(sFlat0,X2)),
inference(orient,[status(thm)],[t12519]) ).
cnf(t111748,plain,
rd(mult(sFlat0,rd(sFlat0,X2)),sFlat0) = ld(rd(mult(sFlat0,X2),sFlat0),sFlat0),
inference(step,[status(thm)],[t15371,t14194]) ).
cnf(t19626,plain,
ld(rd(mult(sFlat0,X1),sFlat0),sFlat0) = rd(mult(sFlat0,rd(sFlat0,X1)),sFlat0),
inference(orient,[status(thm)],[t111748]) ).
cnf(t112798,plain,
mult(rd(rd(mult(sFlat0,rd(sFlat0,X1)),sFlat0),sFlat0),X1) = rd(rd(mult(sFlat0,mult(X1,sFlat0)),mult(sFlat0,mult(X1,sFlat0))),sFlat0),
inference(step,[status(thm)],[t112797,t19626]) ).
cnf(t112799,plain,
mult(mult(sFlat0,rd(sFlat0,X1)),X1) = rd(rd(mult(sFlat0,mult(X1,sFlat0)),mult(sFlat0,mult(X1,sFlat0))),sFlat0),
inference(step,[status(thm)],[t112798,t926]) ).
cnf(t112800,plain,
mult(rd(sFlat0,X1),mult(X1,sFlat0)) = rd(rd(mult(sFlat0,mult(X1,sFlat0)),mult(sFlat0,mult(X1,sFlat0))),sFlat0),
inference(step,[status(thm)],[t112799,t382]) ).
cnf(t112801,plain,
mult(rd(sFlat0,X1),rd(X1,sFlat0)) = rd(rd(mult(sFlat0,mult(X1,sFlat0)),mult(sFlat0,mult(X1,sFlat0))),sFlat0),
inference(step,[status(thm)],[t112800,t880]) ).
cnf(t888,plain,
rd(mult(mult(X1,sFlat0),X2),sFlat0) = mult(X1,mult(sFlat0,mult(X2,sFlat0))),
inference(cp,[status(thm)],[t880,t13]) ).
cnf(t111519,plain,
rd(mult(rd(X1,sFlat0),X2),sFlat0) = mult(X1,mult(sFlat0,mult(X2,sFlat0))),
inference(step,[status(thm)],[t888,t880]) ).
cnf(t111520,plain,
rd(mult(rd(X1,sFlat0),X2),sFlat0) = mult(X1,mult(sFlat0,rd(X2,sFlat0))),
inference(step,[status(thm)],[t111519,t880]) ).
cnf(t111521,plain,
rd(mult(rd(X1,sFlat0),X2),sFlat0) = mult(X1,rd(ld(sFlat0,X2),sFlat0)),
inference(step,[status(thm)],[t111520,t1168]) ).
cnf(t5727,plain,
mult(X1,rd(ld(sFlat0,X2),sFlat0)) = rd(mult(rd(X1,sFlat0),X2),sFlat0),
inference(orient,[status(thm)],[t111521]) ).
cnf(t1356,plain,
ld(sFlat0,ld(sFlat0,X1)) = mult(sFlat0,X1),
inference(cp,[status(thm)],[t1353,t7]) ).
cnf(t1381,plain,
ld(sFlat0,ld(sFlat0,X1)) = mult(sFlat0,X1),
inference(orient,[status(thm)],[t1356]) ).
cnf(t11511,plain,
ld(X1,rd(X1,X2)) = rd(ld(X2,X2),X2),
inference(cp,[status(thm)],[t9,t11387]) ).
cnf(t23742,plain,
ld(X1,rd(X1,X2)) = rd(ld(X2,X2),X2),
inference(orient,[status(thm)],[t11511]) ).
cnf(t23914,plain,
mult(sFlat0,rd(sFlat0,X1)) = ld(sFlat0,rd(ld(X1,X1),X1)),
inference(cp,[status(thm)],[t1381,t23742]) ).
cnf(t24057,plain,
ld(sFlat0,rd(ld(X1,X1),X1)) = mult(sFlat0,rd(sFlat0,X1)),
inference(orient,[status(thm)],[t23914]) ).
cnf(t24078,plain,
rd(mult(rd(X1,sFlat0),rd(ld(X2,X2),X2)),sFlat0) = mult(X1,rd(mult(sFlat0,rd(sFlat0,X2)),sFlat0)),
inference(cp,[status(thm)],[t5727,t24057]) ).
cnf(t23911,plain,
rd(X1,ld(rd(X2,X3),X2)) = mult(X1,rd(ld(X3,X3),X3)),
inference(cp,[status(thm)],[t12097,t23742]) ).
cnf(t111805,plain,
rd(X1,X3) = mult(X1,rd(ld(X3,X3),X3)),
inference(step,[status(thm)],[t23911,t39]) ).
cnf(t23977,plain,
mult(X1,rd(ld(X2,X2),X2)) = rd(X1,X2),
inference(orient,[status(thm)],[t111805]) ).
cnf(t111806,plain,
rd(rd(rd(X1,sFlat0),X2),sFlat0) = mult(X1,rd(mult(sFlat0,rd(sFlat0,X2)),sFlat0)),
inference(step,[status(thm)],[t24078,t23977]) ).
cnf(t1221,plain,
sFlat0 = rd(rd(X1,sFlat0),rd(mult(sFlat0,X1),sFlat0)),
inference(cp,[status(thm)],[t38,t1210]) ).
cnf(t2539,plain,
rd(rd(X1,sFlat0),rd(mult(sFlat0,X1),sFlat0)) = sFlat0,
inference(orient,[status(thm)],[t1221]) ).
cnf(t12067,plain,
mult(X1,rd(mult(sFlat0,X2),sFlat0)) = rd(X1,ld(rd(X2,sFlat0),sFlat0)),
inference(cp,[status(thm)],[t11966,t2539]) ).
cnf(t18300,plain,
mult(X1,rd(mult(sFlat0,X2),sFlat0)) = rd(X1,ld(rd(X2,sFlat0),sFlat0)),
inference(orient,[status(thm)],[t12067]) ).
cnf(t111807,plain,
rd(rd(rd(X1,sFlat0),X2),sFlat0) = rd(X1,ld(rd(rd(sFlat0,X2),sFlat0),sFlat0)),
inference(step,[status(thm)],[t111806,t18300]) ).
cnf(t111808,plain,
rd(rd(rd(X1,sFlat0),X2),sFlat0) = rd(X1,rd(ld(sFlat0,X2),sFlat0)),
inference(step,[status(thm)],[t111807,t15368]) ).
cnf(t24081,plain,
rd(rd(rd(X1,sFlat0),X2),sFlat0) = rd(X1,rd(ld(sFlat0,X2),sFlat0)),
inference(orient,[status(thm)],[t111808]) ).
cnf(t24223,plain,
rd(rd(X1,sFlat0),rd(ld(sFlat0,X2),sFlat0)) = rd(rd(X1,X2),sFlat0),
inference(cp,[status(thm)],[t24081,t926]) ).
cnf(t31598,plain,
rd(rd(X1,sFlat0),rd(ld(sFlat0,X2),sFlat0)) = rd(rd(X1,X2),sFlat0),
inference(orient,[status(thm)],[t24223]) ).
cnf(t31844,plain,
rd(rd(X1,mult(sFlat0,X2)),sFlat0) = rd(rd(X1,sFlat0),rd(X2,sFlat0)),
inference(cp,[status(thm)],[t31598,t11]) ).
cnf(t32078,plain,
rd(rd(X1,mult(sFlat0,X2)),sFlat0) = rd(rd(X1,sFlat0),rd(X2,sFlat0)),
inference(orient,[status(thm)],[t31844]) ).
cnf(t112802,plain,
mult(rd(sFlat0,X1),rd(X1,sFlat0)) = rd(rd(mult(sFlat0,mult(X1,sFlat0)),sFlat0),rd(mult(X1,sFlat0),sFlat0)),
inference(step,[status(thm)],[t112801,t32078]) ).
cnf(t112803,plain,
mult(rd(sFlat0,X1),rd(X1,sFlat0)) = rd(rd(mult(sFlat0,rd(X1,sFlat0)),sFlat0),rd(mult(X1,sFlat0),sFlat0)),
inference(step,[status(thm)],[t112802,t880]) ).
cnf(t112804,plain,
mult(rd(sFlat0,X1),rd(X1,sFlat0)) = rd(rd(rd(ld(sFlat0,X1),sFlat0),sFlat0),rd(mult(X1,sFlat0),sFlat0)),
inference(step,[status(thm)],[t112803,t1168]) ).
cnf(t112805,plain,
mult(rd(sFlat0,X1),rd(X1,sFlat0)) = rd(ld(sFlat0,X1),rd(mult(X1,sFlat0),sFlat0)),
inference(step,[status(thm)],[t112804,t926]) ).
cnf(t112806,plain,
mult(rd(sFlat0,X1),rd(X1,sFlat0)) = rd(ld(sFlat0,X1),X1),
inference(step,[status(thm)],[t112805,t9]) ).
cnf(t109387,plain,
mult(rd(sFlat0,X1),rd(X1,sFlat0)) = rd(ld(sFlat0,X1),X1),
inference(orient,[status(thm)],[t112806]) ).
cnf(t109763,plain,
mult(sFlat0,rd(sFlat0,X1)) = rd(rd(ld(sFlat0,X1),X1),X1),
inference(cp,[status(thm)],[t32828,t109387]) ).
cnf(t109781,plain,
rd(rd(ld(sFlat0,X1),X1),X1) = mult(sFlat0,rd(sFlat0,X1)),
inference(orient,[status(thm)],[t109763]) ).
cnf(t33605,plain,
ld(X1,X1) = ld(X2,rd(X2,rd(X1,X1))),
inference(cp,[status(thm)],[t12356,t33566]) ).
cnf(t112004,plain,
rd(X1,X1) = ld(X2,rd(X2,rd(X1,X1))),
inference(step,[status(thm)],[t33605,t33566]) ).
cnf(t33774,plain,
ld(X1,rd(X1,rd(X2,X2))) = rd(X2,X2),
inference(orient,[status(thm)],[t112004]) ).
cnf(t109870,plain,
mult(sFlat0,rd(sFlat0,rd(sFlat0,rd(X1,X1)))) = rd(rd(rd(X1,X1),rd(sFlat0,rd(X1,X1))),rd(sFlat0,rd(X1,X1))),
inference(cp,[status(thm)],[t109781,t33774]) ).
cnf(t33579,plain,
rd(rd(X1,sFlat0),rd(X1,sFlat0)) = rd(ld(sFlat0,ld(X1,X1)),sFlat0),
inference(cp,[status(thm)],[t33566,t14923]) ).
cnf(t112034,plain,
rd(rd(X1,sFlat0),rd(X1,sFlat0)) = rd(ld(sFlat0,rd(X1,X1)),sFlat0),
inference(step,[status(thm)],[t33579,t33566]) ).
cnf(t35208,plain,
rd(ld(sFlat0,rd(X1,X1)),sFlat0) = rd(rd(X1,sFlat0),rd(X1,sFlat0)),
inference(orient,[status(thm)],[t112034]) ).
cnf(t35231,plain,
ld(sFlat0,rd(X1,X1)) = rd(rd(rd(X1,sFlat0),rd(X1,sFlat0)),sFlat0),
inference(cp,[status(thm)],[t926,t35208]) ).
cnf(t112035,plain,
ld(sFlat0,rd(X1,X1)) = rd(X1,rd(ld(sFlat0,rd(X1,sFlat0)),sFlat0)),
inference(step,[status(thm)],[t35231,t24081]) ).
cnf(t112036,plain,
ld(sFlat0,rd(X1,X1)) = rd(X1,mult(sFlat0,X1)),
inference(step,[status(thm)],[t112035,t1189]) ).
cnf(t35282,plain,
ld(sFlat0,rd(X1,X1)) = rd(X1,mult(sFlat0,X1)),
inference(orient,[status(thm)],[t112036]) ).
cnf(t2203,plain,
mult(mult(X1,X2),rd(X3,X2)) = rd(mult(X1,mult(X2,X3)),X2),
inference(cp,[status(thm)],[t2162,t8]) ).
cnf(t6795,plain,
mult(mult(X1,X2),rd(X3,X2)) = rd(mult(X1,mult(X2,X3)),X2),
inference(orient,[status(thm)],[t2203]) ).
cnf(t33580,plain,
X1 = rd(X1,rd(X1,X1)),
inference(cp,[status(thm)],[t38,t33566]) ).
cnf(t33628,plain,
rd(X1,rd(X1,X1)) = X1,
inference(orient,[status(thm)],[t33580]) ).
cnf(t33634,plain,
rd(mult(X1,mult(rd(X2,X2),X2)),rd(X2,X2)) = mult(mult(X1,rd(X2,X2)),X2),
inference(cp,[status(thm)],[t6795,t33628]) ).
cnf(t112041,plain,
rd(mult(X1,X2),rd(X2,X2)) = mult(mult(X1,rd(X2,X2)),X2),
inference(step,[status(thm)],[t33634,t8]) ).
cnf(t112042,plain,
rd(mult(X1,X2),rd(X2,X2)) = mult(rd(X1,X2),mult(X2,X2)),
inference(step,[status(thm)],[t112041,t382]) ).
cnf(t35856,plain,
mult(rd(X1,X2),mult(X2,X2)) = rd(mult(X1,X2),rd(X2,X2)),
inference(orient,[status(thm)],[t112042]) ).
cnf(t11510,plain,
X1 = ld(ld(X2,rd(X2,X1)),ld(X1,X1)),
inference(cp,[status(thm)],[t11,t11387]) ).
cnf(t11651,plain,
ld(ld(X1,rd(X1,X2)),ld(X2,X2)) = X2,
inference(orient,[status(thm)],[t11510]) ).
cnf(t111977,plain,
ld(ld(X1,rd(X1,X2)),rd(X2,X2)) = X2,
inference(step,[status(thm)],[t11651,t33566]) ).
cnf(t33623,plain,
ld(ld(X1,rd(X1,X2)),rd(X2,X2)) = X2,
inference(rw,[status(thm)],[t111977]) ).
cnf(t34775,plain,
ld(ld(X1,rd(X1,X2)),rd(X2,X2)) = X2,
inference(orient,[status(thm)],[t33623]) ).
cnf(t23947,plain,
mult(X1,X2) = rd(X1,rd(ld(X2,X2),X2)),
inference(cp,[status(thm)],[t11966,t23742]) ).
cnf(t24036,plain,
rd(X1,rd(ld(X2,X2),X2)) = mult(X1,X2),
inference(orient,[status(thm)],[t23947]) ).
cnf(t111965,plain,
rd(X1,rd(rd(X2,X2),X2)) = mult(X1,X2),
inference(step,[status(thm)],[t24036,t33566]) ).
cnf(t33617,plain,
rd(X1,rd(rd(X2,X2),X2)) = mult(X1,X2),
inference(rw,[status(thm)],[t111965]) ).
cnf(t33962,plain,
rd(X1,rd(rd(X2,X2),X2)) = mult(X1,X2),
inference(orient,[status(thm)],[t33617]) ).
cnf(t34790,plain,
rd(rd(X1,X1),X1) = ld(ld(X2,mult(X2,X1)),rd(rd(rd(X1,X1),X1),rd(rd(X1,X1),X1))),
inference(cp,[status(thm)],[t34775,t33962]) ).
cnf(t112030,plain,
rd(rd(X1,X1),X1) = ld(X1,rd(rd(rd(X1,X1),X1),rd(rd(X1,X1),X1))),
inference(step,[status(thm)],[t34790,t11]) ).
cnf(t112031,plain,
rd(rd(X1,X1),X1) = ld(X1,mult(rd(rd(X1,X1),X1),X1)),
inference(step,[status(thm)],[t112030,t33962]) ).
cnf(t112032,plain,
rd(rd(X1,X1),X1) = ld(X1,rd(X1,X1)),
inference(step,[status(thm)],[t112031,t8]) ).
cnf(t35017,plain,
ld(X1,rd(X1,X1)) = rd(rd(X1,X1),X1),
inference(orient,[status(thm)],[t112032]) ).
cnf(t111593,plain,
rd(mult(X1,X2),ld(X1,X2)) = mult(X2,mult(ld(X2,X1),X1)),
inference(step,[status(thm)],[t706,t12097]) ).
cnf(t12229,plain,
rd(mult(X1,X2),ld(X1,X2)) = mult(X2,mult(ld(X2,X1),X1)),
inference(rw,[status(thm)],[t111593]) ).
cnf(t18580,plain,
mult(X1,mult(ld(X1,X2),X2)) = rd(mult(X2,X1),ld(X2,X1)),
inference(orient,[status(thm)],[t12229]) ).
cnf(t33598,plain,
rd(mult(X1,X1),ld(X1,X1)) = mult(X1,mult(rd(X1,X1),X1)),
inference(cp,[status(thm)],[t18580,t33566]) ).
cnf(t112002,plain,
rd(mult(X1,X1),rd(X1,X1)) = mult(X1,mult(rd(X1,X1),X1)),
inference(step,[status(thm)],[t33598,t33566]) ).
cnf(t112003,plain,
rd(mult(X1,X1),rd(X1,X1)) = mult(X1,X1),
inference(step,[status(thm)],[t112002,t8]) ).
cnf(t33736,plain,
rd(mult(X1,X1),rd(X1,X1)) = mult(X1,X1),
inference(orient,[status(thm)],[t112003]) ).
cnf(t33762,plain,
rd(X1,X1) = ld(mult(X1,X1),mult(X1,X1)),
inference(cp,[status(thm)],[t39,t33736]) ).
cnf(t112008,plain,
rd(X1,X1) = rd(mult(X1,X1),mult(X1,X1)),
inference(step,[status(thm)],[t33762,t33566]) ).
cnf(t34065,plain,
rd(mult(X1,X1),mult(X1,X1)) = rd(X1,X1),
inference(orient,[status(thm)],[t112008]) ).
cnf(t35033,plain,
rd(rd(mult(X1,X1),mult(X1,X1)),mult(X1,X1)) = ld(mult(X1,X1),rd(X1,X1)),
inference(cp,[status(thm)],[t35017,t34065]) ).
cnf(t112047,plain,
rd(rd(X1,X1),mult(X1,X1)) = ld(mult(X1,X1),rd(X1,X1)),
inference(step,[status(thm)],[t35033,t34065]) ).
cnf(t10701,plain,
mult(ld(mult(X1,X2),X3),X2) = ld(X2,ld(X1,mult(X3,X2))),
inference(cp,[status(thm)],[t11,t10595]) ).
cnf(t14789,plain,
ld(X1,ld(X2,mult(X3,X1))) = mult(ld(mult(X2,X1),X3),X1),
inference(orient,[status(thm)],[t10701]) ).
cnf(t14897,plain,
mult(ld(mult(X1,X2),rd(X3,X2)),X2) = ld(X2,ld(X1,X3)),
inference(cp,[status(thm)],[t14789,t8]) ).
cnf(t29018,plain,
mult(ld(mult(X1,X2),rd(X3,X2)),X2) = ld(X2,ld(X1,X3)),
inference(orient,[status(thm)],[t14897]) ).
cnf(t29369,plain,
ld(mult(X1,X2),rd(X3,X2)) = rd(ld(X2,ld(X1,X3)),X2),
inference(cp,[status(thm)],[t9,t29018]) ).
cnf(t29415,plain,
ld(mult(X1,X2),rd(X3,X2)) = rd(ld(X2,ld(X1,X3)),X2),
inference(orient,[status(thm)],[t29369]) ).
cnf(t112048,plain,
rd(rd(X1,X1),mult(X1,X1)) = rd(ld(X1,ld(X1,X1)),X1),
inference(step,[status(thm)],[t112047,t29415]) ).
cnf(t112049,plain,
rd(rd(X1,X1),mult(X1,X1)) = rd(ld(X1,rd(X1,X1)),X1),
inference(step,[status(thm)],[t112048,t33566]) ).
cnf(t112050,plain,
rd(rd(X1,X1),mult(X1,X1)) = rd(rd(rd(X1,X1),X1),X1),
inference(step,[status(thm)],[t112049,t35017]) ).
cnf(t36134,plain,
rd(rd(rd(X1,X1),X1),X1) = rd(rd(X1,X1),mult(X1,X1)),
inference(orient,[status(thm)],[t112050]) ).
cnf(t36155,plain,
rd(mult(rd(rd(X1,X1),X1),X1),rd(X1,X1)) = mult(rd(rd(X1,X1),mult(X1,X1)),mult(X1,X1)),
inference(cp,[status(thm)],[t35856,t36134]) ).
cnf(t112051,plain,
rd(rd(X1,X1),rd(X1,X1)) = mult(rd(rd(X1,X1),mult(X1,X1)),mult(X1,X1)),
inference(step,[status(thm)],[t36155,t8]) ).
cnf(t112052,plain,
rd(rd(X1,X1),rd(X1,X1)) = rd(X1,X1),
inference(step,[status(thm)],[t112051,t8]) ).
cnf(t36210,plain,
rd(rd(X1,X1),rd(X1,X1)) = rd(X1,X1),
inference(orient,[status(thm)],[t112052]) ).
cnf(t36216,plain,
rd(rd(X1,X1),mult(sFlat0,rd(X1,X1))) = ld(sFlat0,rd(X1,X1)),
inference(cp,[status(thm)],[t35282,t36210]) ).
cnf(t111952,plain,
mult(X1,rd(X2,X2)) = rd(X1,rd(X2,X2)),
inference(step,[status(thm)],[t33483,t33566]) ).
cnf(t33577,plain,
mult(X1,rd(X2,X2)) = rd(X1,rd(X2,X2)),
inference(orient,[status(thm)],[t111952]) ).
cnf(t112197,plain,
rd(rd(X1,X1),rd(sFlat0,rd(X1,X1))) = ld(sFlat0,rd(X1,X1)),
inference(step,[status(thm)],[t36216,t33577]) ).
cnf(t112198,plain,
rd(rd(X1,X1),rd(sFlat0,rd(X1,X1))) = rd(X1,mult(sFlat0,X1)),
inference(step,[status(thm)],[t112197,t35282]) ).
cnf(t43897,plain,
rd(rd(X1,X1),rd(sFlat0,rd(X1,X1))) = rd(X1,mult(sFlat0,X1)),
inference(orient,[status(thm)],[t112198]) ).
cnf(t112807,plain,
mult(sFlat0,rd(sFlat0,rd(sFlat0,rd(X1,X1)))) = rd(rd(X1,mult(sFlat0,X1)),rd(sFlat0,rd(X1,X1))),
inference(step,[status(thm)],[t109870,t43897]) ).
cnf(t33508,plain,
sFlat0 = rd(ld(sFlat0,rd(X1,X1)),rd(sFlat0,ld(X1,X1))),
inference(cp,[status(thm)],[t1423,t33483]) ).
cnf(t112354,plain,
sFlat0 = rd(rd(X1,mult(sFlat0,X1)),rd(sFlat0,ld(X1,X1))),
inference(step,[status(thm)],[t33508,t35282]) ).
cnf(t112355,plain,
sFlat0 = rd(rd(X1,mult(sFlat0,X1)),rd(sFlat0,rd(X1,X1))),
inference(step,[status(thm)],[t112354,t33566]) ).
cnf(t58041,plain,
rd(rd(X1,mult(sFlat0,X1)),rd(sFlat0,rd(X1,X1))) = sFlat0,
inference(orient,[status(thm)],[t112355]) ).
cnf(t112808,plain,
mult(sFlat0,rd(sFlat0,rd(sFlat0,rd(X1,X1)))) = sFlat0,
inference(step,[status(thm)],[t112807,t58041]) ).
cnf(t109991,plain,
mult(sFlat0,rd(sFlat0,rd(sFlat0,rd(X1,X1)))) = sFlat0,
inference(orient,[status(thm)],[t112808]) ).
cnf(t110085,plain,
ld(rd(rd(sFlat0,rd(sFlat0,rd(X1,X1))),sFlat0),sFlat0) = ld(X2,rd(X2,rd(sFlat0,sFlat0))),
inference(cp,[status(thm)],[t28044,t109991]) ).
cnf(t112809,plain,
rd(ld(sFlat0,rd(sFlat0,rd(X1,X1))),sFlat0) = ld(X2,rd(X2,rd(sFlat0,sFlat0))),
inference(step,[status(thm)],[t110085,t15368]) ).
cnf(t12498,plain,
ld(sFlat0,ld(mult(X1,X2),X1)) = mult(sFlat0,rd(sFlat0,X2)),
inference(cp,[status(thm)],[t12497,t11]) ).
cnf(t14103,plain,
ld(sFlat0,ld(mult(X1,X2),X1)) = mult(sFlat0,rd(sFlat0,X2)),
inference(orient,[status(thm)],[t12498]) ).
cnf(t14190,plain,
ld(ld(mult(X1,X2),X1),sFlat0) = ld(X3,rd(X3,mult(sFlat0,rd(sFlat0,X2)))),
inference(cp,[status(thm)],[t12356,t14103]) ).
cnf(t12422,plain,
ld(ld(sFlat0,X1),sFlat0) = ld(X2,rd(X2,mult(sFlat0,X1))),
inference(cp,[status(thm)],[t12356,t1381]) ).
cnf(t14004,plain,
ld(X1,rd(X1,mult(sFlat0,X2))) = ld(ld(sFlat0,X2),sFlat0),
inference(orient,[status(thm)],[t12422]) ).
cnf(t111707,plain,
ld(ld(mult(X1,X2),X1),sFlat0) = ld(ld(sFlat0,rd(sFlat0,X2)),sFlat0),
inference(step,[status(thm)],[t14190,t14004]) ).
cnf(t19000,plain,
ld(ld(mult(X1,X2),X1),sFlat0) = ld(ld(sFlat0,rd(sFlat0,X2)),sFlat0),
inference(orient,[status(thm)],[t111707]) ).
cnf(t19082,plain,
ld(mult(X1,X2),X1) = rd(sFlat0,ld(ld(sFlat0,rd(sFlat0,X2)),sFlat0)),
inference(cp,[status(thm)],[t38,t19000]) ).
cnf(t12065,plain,
mult(X1,mult(sFlat0,X2)) = rd(X1,ld(ld(sFlat0,X2),sFlat0)),
inference(cp,[status(thm)],[t11966,t1423]) ).
cnf(t12446,plain,
rd(X1,ld(ld(sFlat0,X2),sFlat0)) = mult(X1,mult(sFlat0,X2)),
inference(orient,[status(thm)],[t12065]) ).
cnf(t111708,plain,
ld(mult(X1,X2),X1) = mult(sFlat0,mult(sFlat0,rd(sFlat0,X2))),
inference(step,[status(thm)],[t19082,t12446]) ).
cnf(t111709,plain,
ld(mult(X1,X2),X1) = ld(sFlat0,rd(sFlat0,X2)),
inference(step,[status(thm)],[t111708,t1353]) ).
cnf(t19086,plain,
ld(mult(X1,X2),X1) = ld(sFlat0,rd(sFlat0,X2)),
inference(orient,[status(thm)],[t111709]) ).
cnf(t33505,plain,
ld(sFlat0,rd(sFlat0,rd(X1,X1))) = ld(rd(X2,ld(X1,X1)),X2),
inference(cp,[status(thm)],[t19086,t33483]) ).
cnf(t112000,plain,
ld(sFlat0,rd(sFlat0,rd(X1,X1))) = ld(X1,X1),
inference(step,[status(thm)],[t33505,t39]) ).
cnf(t112001,plain,
ld(sFlat0,rd(sFlat0,rd(X1,X1))) = rd(X1,X1),
inference(step,[status(thm)],[t112000,t33566]) ).
cnf(t33708,plain,
ld(sFlat0,rd(sFlat0,rd(X1,X1))) = rd(X1,X1),
inference(orient,[status(thm)],[t112001]) ).
cnf(t112810,plain,
rd(rd(X1,X1),sFlat0) = ld(X2,rd(X2,rd(sFlat0,sFlat0))),
inference(step,[status(thm)],[t112809,t33708]) ).
cnf(t112811,plain,
rd(rd(X1,X1),sFlat0) = rd(sFlat0,sFlat0),
inference(step,[status(thm)],[t112810,t33774]) ).
cnf(t112812,plain,
rd(rd(X1,X1),sFlat0) = sFlat0,
inference(step,[status(thm)],[t112811,t1330]) ).
cnf(t110093,plain,
rd(rd(X1,X1),sFlat0) = sFlat0,
inference(orient,[status(thm)],[t112812]) ).
cnf(t110138,plain,
rd(X1,X1) = rd(sFlat0,sFlat0),
inference(cp,[status(thm)],[t926,t110093]) ).
cnf(t112815,plain,
rd(X1,X1) = sFlat0,
inference(step,[status(thm)],[t110138,t1330]) ).
cnf(t110289,plain,
rd(X1,X1) = sFlat0,
inference(orient,[status(thm)],[t112815]) ).
cnf(t110392,plain,
sFlat1 = ld(rd(mult(rd(sFlat0,sFlat1),sFlat1),x0),sFlat0),
inference(cp,[status(thm)],[t58277,t110289]) ).
cnf(t113048,plain,
sFlat1 = ld(rd(sFlat0,x0),sFlat0),
inference(step,[status(thm)],[t110392,t8]) ).
cnf(t113049,plain,
sFlat1 = x0,
inference(step,[status(thm)],[t113048,t39]) ).
cnf(t110533,plain,
x0 = sFlat1,
inference(orient,[status(thm)],[t113049]) ).
cnf(t113050,plain,
rd(sFlat1,sFlat0) = sFlat1,
inference(step,[status(thm)],[t37,t110533]) ).
cnf(t110534,plain,
rd(sFlat1,sFlat0) = sFlat1,
inference(orient,[status(thm)],[t113050]) ).
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,t110533]) ).
cnf(g0_1,plain,
mult(sFlat1,sFlat0) != x0,
inference(rw,[status(thm)],[g0_0,t110289]) ).
cnf(g0_2,plain,
rd(sFlat1,sFlat0) != x0,
inference(rw,[status(thm)],[g0_1,t880]) ).
cnf(g0_3,plain,
sFlat1 != x0,
inference(rw,[status(thm)],[g0_2,t110534]) ).
cnf(g0_4,plain,
sFlat1 != sFlat1,
inference(rw,[status(thm)],[g0_3,t110533]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_4]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP655-11 : TPTP v9.3.1. Released v8.1.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.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Wed Sep 23 15:25:29 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 54.41/7.33 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 54.41/7.33 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------