%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : GRP746+1 : TPTP v5.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %s
% Computer : art04.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 2018MB
% OS : Linux 2.6.26.8-57.fc8
% CPULimit : 300s
% DateTime : Wed Dec 29 07:22:23 EST 2010
% Result : Theorem 16.84s
% Output : Solution 16.84s
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----ERROR: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Reading problem from /tmp/SystemOnTPTP6077/GRP746+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP6077/GRP746+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP6077/GRP746+1.tptp
% TreeLimitedRun: ----------------------------------------------------------
% TreeLimitedRun: /home/graph/tptp/Systems/EP---1.2/eproof --print-statistics -xAuto -tAuto --cpu-limit=60 --proof-time-unlimited --memory-limit=Auto --tstp-in --tstp-out /tmp/SRASS.s.p
% TreeLimitedRun: CPU time limit is 60s
% TreeLimitedRun: WC time limit is 120s
% TreeLimitedRun: PID is 6173
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.02 WC
% PrfWatch: 1.93 CPU 2.02 WC
% PrfWatch: 3.91 CPU 4.03 WC
% PrfWatch: 5.91 CPU 6.03 WC
% PrfWatch: 7.90 CPU 8.04 WC
% # Preprocessing time : 0.011 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% PrfWatch: 9.88 CPU 10.04 WC
% PrfWatch: 11.88 CPU 12.05 WC
% PrfWatch: 13.87 CPU 14.05 WC
% PrfWatch: 15.86 CPU 16.06 WC
% # SZS output start CNFRefutation.
% fof(1, axiom,![X1]:![X2]:mult(X2,ld(X2,X1))=X1,file('/tmp/SRASS.s.p', f01)).
% fof(2, axiom,![X1]:![X2]:ld(X2,mult(X2,X1))=X1,file('/tmp/SRASS.s.p', f02)).
% fof(3, axiom,![X1]:![X2]:mult(rd(X2,X1),X1)=X2,file('/tmp/SRASS.s.p', f03)).
% fof(4, axiom,![X1]:![X2]:rd(mult(X2,X1),X1)=X2,file('/tmp/SRASS.s.p', f04)).
% fof(5, axiom,![X2]:mult(X2,unit)=X2,file('/tmp/SRASS.s.p', f05)).
% fof(6, axiom,![X2]:mult(unit,X2)=X2,file('/tmp/SRASS.s.p', f06)).
% fof(7, axiom,![X3]:![X1]:![X2]:mult(mult(mult(X2,X1),X3),X1)=mult(X2,mult(mult(X1,X3),X1)),file('/tmp/SRASS.s.p', f07)).
% fof(8, axiom,![X4]:![X5]:![X6]:((mult(mult(X4,X5),X6)=mult(X4,mult(X5,X6))&mult(mult(X4,X6),X5)=mult(X4,mult(X6,X5)))|(mult(mult(X4,X5),X6)=mult(mult(X4,X6),X5)&mult(X4,mult(X5,X6))=mult(X4,mult(X6,X5)))),file('/tmp/SRASS.s.p', f08)).
% fof(9, conjecture,mult(mult(a,b),c)=mult(a,mult(b,c)),file('/tmp/SRASS.s.p', goals)).
% fof(10, negated_conjecture,~(mult(mult(a,b),c)=mult(a,mult(b,c))),inference(assume_negation,[status(cth)],[9])).
% fof(11, negated_conjecture,~(mult(mult(a,b),c)=mult(a,mult(b,c))),inference(fof_simplification,[status(thm)],[10,theory(equality)])).
% fof(12, plain,![X3]:![X4]:mult(X4,ld(X4,X3))=X3,inference(variable_rename,[status(thm)],[1])).
% cnf(13,plain,(mult(X1,ld(X1,X2))=X2),inference(split_conjunct,[status(thm)],[12])).
% fof(14, plain,![X3]:![X4]:ld(X4,mult(X4,X3))=X3,inference(variable_rename,[status(thm)],[2])).
% cnf(15,plain,(ld(X1,mult(X1,X2))=X2),inference(split_conjunct,[status(thm)],[14])).
% fof(16, plain,![X3]:![X4]:mult(rd(X4,X3),X3)=X4,inference(variable_rename,[status(thm)],[3])).
% cnf(17,plain,(mult(rd(X1,X2),X2)=X1),inference(split_conjunct,[status(thm)],[16])).
% fof(18, plain,![X3]:![X4]:rd(mult(X4,X3),X3)=X4,inference(variable_rename,[status(thm)],[4])).
% cnf(19,plain,(rd(mult(X1,X2),X2)=X1),inference(split_conjunct,[status(thm)],[18])).
% fof(20, plain,![X3]:mult(X3,unit)=X3,inference(variable_rename,[status(thm)],[5])).
% cnf(21,plain,(mult(X1,unit)=X1),inference(split_conjunct,[status(thm)],[20])).
% fof(22, plain,![X3]:mult(unit,X3)=X3,inference(variable_rename,[status(thm)],[6])).
% cnf(23,plain,(mult(unit,X1)=X1),inference(split_conjunct,[status(thm)],[22])).
% fof(24, plain,![X4]:![X5]:![X6]:mult(mult(mult(X6,X5),X4),X5)=mult(X6,mult(mult(X5,X4),X5)),inference(variable_rename,[status(thm)],[7])).
% cnf(25,plain,(mult(mult(mult(X1,X2),X3),X2)=mult(X1,mult(mult(X2,X3),X2))),inference(split_conjunct,[status(thm)],[24])).
% fof(26, plain,![X7]:![X8]:![X9]:((mult(mult(X7,X8),X9)=mult(X7,mult(X8,X9))&mult(mult(X7,X9),X8)=mult(X7,mult(X9,X8)))|(mult(mult(X7,X8),X9)=mult(mult(X7,X9),X8)&mult(X7,mult(X8,X9))=mult(X7,mult(X9,X8)))),inference(variable_rename,[status(thm)],[8])).
% fof(27, plain,![X7]:![X8]:![X9]:(((mult(mult(X7,X8),X9)=mult(mult(X7,X9),X8)|mult(mult(X7,X8),X9)=mult(X7,mult(X8,X9)))&(mult(X7,mult(X8,X9))=mult(X7,mult(X9,X8))|mult(mult(X7,X8),X9)=mult(X7,mult(X8,X9))))&((mult(mult(X7,X8),X9)=mult(mult(X7,X9),X8)|mult(mult(X7,X9),X8)=mult(X7,mult(X9,X8)))&(mult(X7,mult(X8,X9))=mult(X7,mult(X9,X8))|mult(mult(X7,X9),X8)=mult(X7,mult(X9,X8))))),inference(distribute,[status(thm)],[26])).
% cnf(28,plain,(mult(mult(X1,X2),X3)=mult(X1,mult(X2,X3))|mult(X1,mult(X3,X2))=mult(X1,mult(X2,X3))),inference(split_conjunct,[status(thm)],[27])).
% cnf(29,plain,(mult(mult(X1,X2),X3)=mult(X1,mult(X2,X3))|mult(mult(X1,X3),X2)=mult(mult(X1,X2),X3)),inference(split_conjunct,[status(thm)],[27])).
% cnf(32,negated_conjecture,(mult(mult(a,b),c)!=mult(a,mult(b,c))),inference(split_conjunct,[status(thm)],[11])).
% cnf(33,plain,(ld(unit,X1)=X1),inference(spm,[status(thm)],[15,23,theory(equality)])).
% cnf(37,plain,(ld(rd(X1,X2),X1)=X2),inference(spm,[status(thm)],[15,17,theory(equality)])).
% cnf(38,plain,(rd(X1,X1)=unit),inference(spm,[status(thm)],[19,23,theory(equality)])).
% cnf(40,plain,(rd(X2,ld(X1,X2))=X1),inference(spm,[status(thm)],[19,13,theory(equality)])).
% cnf(42,plain,(ld(mult(mult(X1,X2),X3),mult(X1,mult(mult(X2,X3),X2)))=X2),inference(spm,[status(thm)],[15,25,theory(equality)])).
% cnf(43,plain,(rd(mult(X1,mult(mult(X2,X3),X2)),X2)=mult(mult(X1,X2),X3)),inference(spm,[status(thm)],[19,25,theory(equality)])).
% cnf(47,plain,(mult(mult(X1,X3),X2)=mult(rd(X1,X2),mult(mult(X2,X3),X2))),inference(spm,[status(thm)],[25,17,theory(equality)])).
% cnf(49,plain,(mult(mult(X2,X3),ld(X1,X2))=mult(X1,mult(mult(ld(X1,X2),X3),ld(X1,X2)))),inference(spm,[status(thm)],[25,13,theory(equality)])).
% cnf(50,plain,(mult(mult(X1,X2),X2)=mult(X1,mult(mult(X2,unit),X2))),inference(spm,[status(thm)],[25,21,theory(equality)])).
% cnf(51,plain,(mult(X3,X2)=mult(X1,mult(mult(X2,ld(mult(X1,X2),X3)),X2))),inference(spm,[status(thm)],[25,13,theory(equality)])).
% cnf(57,plain,(mult(mult(X1,X2),X2)=mult(X1,mult(X2,X2))),inference(rw,[status(thm)],[50,21,theory(equality)])).
% cnf(64,negated_conjecture,(mult(a,mult(b,c))=mult(a,mult(c,b))),inference(spm,[status(thm)],[32,28,theory(equality)])).
% cnf(68,plain,(mult(X1,X3)=mult(rd(X1,X2),mult(X2,X3))|mult(rd(X1,X2),mult(X2,X3))=mult(rd(X1,X2),mult(X3,X2))),inference(spm,[status(thm)],[28,17,theory(equality)])).
% cnf(71,plain,(mult(X2,X3)=mult(X1,mult(ld(X1,X2),X3))|mult(X1,mult(ld(X1,X2),X3))=mult(X1,mult(X3,ld(X1,X2)))),inference(spm,[status(thm)],[28,13,theory(equality)])).
% cnf(83,plain,(mult(mult(X4,X5),X6)=mult(X4,mult(X5,X6))|mult(mult(X4,X6),X5)!=mult(X4,mult(X5,X6))),inference(ef,[status(thm)],[29,theory(equality)])).
% cnf(94,plain,(mult(mult(mult(X1,X3),X2),X2)=mult(X1,mult(mult(X2,X3),X2))|mult(mult(X1,X3),X2)=mult(X1,mult(X3,X2))),inference(spm,[status(thm)],[25,29,theory(equality)])).
% cnf(112,plain,(mult(X1,X3)=mult(mult(rd(X1,X2),X3),X2)|mult(X1,X3)=mult(rd(X1,X2),mult(X2,X3))),inference(spm,[status(thm)],[29,17,theory(equality)])).
% cnf(138,negated_conjecture,(ld(a,mult(a,mult(b,c)))=mult(c,b)),inference(spm,[status(thm)],[15,64,theory(equality)])).
% cnf(144,negated_conjecture,(mult(b,c)=mult(c,b)),inference(rw,[status(thm)],[138,15,theory(equality)])).
% cnf(145,negated_conjecture,(ld(c,mult(b,c))=b),inference(spm,[status(thm)],[15,144,theory(equality)])).
% cnf(146,negated_conjecture,(rd(mult(b,c),b)=c),inference(spm,[status(thm)],[19,144,theory(equality)])).
% cnf(149,negated_conjecture,(mult(mult(mult(b,c),X1),b)=mult(c,mult(mult(b,X1),b))),inference(spm,[status(thm)],[25,144,theory(equality)])).
% cnf(175,negated_conjecture,(mult(mult(b,c),b)=mult(c,mult(mult(b,unit),b))),inference(spm,[status(thm)],[149,21,theory(equality)])).
% cnf(180,negated_conjecture,(mult(mult(b,c),b)=mult(c,mult(b,b))),inference(rw,[status(thm)],[175,21,theory(equality)])).
% cnf(181,negated_conjecture,(ld(mult(b,c),mult(c,mult(b,b)))=b),inference(spm,[status(thm)],[15,180,theory(equality)])).
% cnf(236,plain,(ld(mult(mult(X1,X2),ld(X2,X3)),mult(X1,mult(X3,X2)))=X2),inference(spm,[status(thm)],[42,13,theory(equality)])).
% cnf(301,plain,(rd(mult(X1,mult(X2,X2)),X2)=mult(X1,X2)),inference(spm,[status(thm)],[19,57,theory(equality)])).
% cnf(309,negated_conjecture,(mult(mult(b,c),mult(b,b))=mult(c,mult(mult(b,b),b))),inference(spm,[status(thm)],[149,57,theory(equality)])).
% cnf(333,negated_conjecture,(mult(mult(b,c),mult(b,b))=mult(c,mult(b,mult(b,b)))),inference(rw,[status(thm)],[309,57,theory(equality)])).
% cnf(421,negated_conjecture,(rd(mult(X1,mult(mult(b,c),c)),c)=mult(mult(X1,c),b)),inference(spm,[status(thm)],[43,144,theory(equality)])).
% cnf(434,plain,(rd(mult(X1,mult(X3,X2)),X2)=mult(mult(X1,X2),ld(X2,X3))),inference(spm,[status(thm)],[43,13,theory(equality)])).
% cnf(453,negated_conjecture,(rd(mult(X1,mult(b,mult(c,c))),c)=mult(mult(X1,c),b)),inference(rw,[status(thm)],[421,57,theory(equality)])).
% cnf(487,negated_conjecture,(rd(mult(c,mult(b,mult(b,b))),mult(b,b))=mult(b,c)),inference(spm,[status(thm)],[19,333,theory(equality)])).
% cnf(1064,negated_conjecture,(mult(rd(X1,c),mult(mult(b,c),c))=mult(mult(X1,b),c)),inference(spm,[status(thm)],[47,144,theory(equality)])).
% cnf(1083,plain,(mult(rd(X1,X2),mult(X3,X2))=mult(mult(X1,ld(X2,X3)),X2)),inference(spm,[status(thm)],[47,13,theory(equality)])).
% cnf(1086,negated_conjecture,(mult(rd(X1,b),mult(c,mult(b,b)))=mult(mult(X1,c),b)),inference(spm,[status(thm)],[47,180,theory(equality)])).
% cnf(1114,negated_conjecture,(mult(rd(X1,c),mult(b,mult(c,c)))=mult(mult(X1,b),c)),inference(rw,[status(thm)],[1064,57,theory(equality)])).
% cnf(1132,negated_conjecture,(ld(rd(X1,c),mult(mult(X1,b),c))=mult(b,mult(c,c))),inference(spm,[status(thm)],[15,1114,theory(equality)])).
% cnf(1160,negated_conjecture,(ld(rd(X1,b),mult(mult(X1,c),b))=mult(c,mult(b,b))),inference(spm,[status(thm)],[15,1086,theory(equality)])).
% cnf(2438,negated_conjecture,(ld(rd(unit,c),mult(b,c))=mult(b,mult(c,c))),inference(spm,[status(thm)],[1132,23,theory(equality)])).
% cnf(2483,negated_conjecture,(rd(mult(b,c),mult(b,mult(c,c)))=rd(unit,c)),inference(spm,[status(thm)],[40,2438,theory(equality)])).
% cnf(2498,negated_conjecture,(ld(rd(unit,b),mult(c,b))=mult(c,mult(b,b))),inference(spm,[status(thm)],[1160,23,theory(equality)])).
% cnf(2532,negated_conjecture,(ld(rd(unit,b),mult(b,c))=mult(c,mult(b,b))),inference(rw,[status(thm)],[2498,144,theory(equality)])).
% cnf(2572,negated_conjecture,(rd(mult(X1,mult(b,c)),b)=mult(mult(X1,b),ld(b,c))),inference(spm,[status(thm)],[434,144,theory(equality)])).
% cnf(2573,plain,(rd(mult(X1,X2),X2)=mult(mult(X1,X2),ld(X2,unit))),inference(spm,[status(thm)],[434,23,theory(equality)])).
% cnf(2631,negated_conjecture,(mult(mult(c,mult(b,b)),ld(mult(b,b),b))=mult(b,c)),inference(rw,[status(thm)],[487,434,theory(equality)])).
% cnf(2635,plain,(X1=mult(mult(X1,X2),ld(X2,unit))),inference(rw,[status(thm)],[2573,19,theory(equality)])).
% cnf(2904,plain,(ld(mult(X1,X2),X1)=ld(X2,unit)),inference(spm,[status(thm)],[15,2635,theory(equality)])).
% cnf(2942,plain,(mult(mult(X1,rd(unit,X2)),X2)=X1),inference(spm,[status(thm)],[2635,37,theory(equality)])).
% cnf(2952,plain,(mult(X1,ld(X2,unit))=rd(X1,X2)),inference(spm,[status(thm)],[2635,17,theory(equality)])).
% cnf(3014,plain,(rd(X1,ld(X2,unit))=mult(X1,X2)),inference(spm,[status(thm)],[40,2904,theory(equality)])).
% cnf(3019,negated_conjecture,(ld(mult(b,c),c)=ld(b,unit)),inference(spm,[status(thm)],[2904,144,theory(equality)])).
% cnf(3056,plain,(ld(X2,X1)=ld(ld(X1,X2),unit)),inference(spm,[status(thm)],[2904,13,theory(equality)])).
% cnf(3057,negated_conjecture,(mult(mult(c,mult(b,b)),ld(b,unit))=mult(b,c)),inference(rw,[status(thm)],[2631,2904,theory(equality)])).
% cnf(3075,negated_conjecture,(mult(b,mult(mult(c,ld(b,unit)),c))=mult(c,c)),inference(spm,[status(thm)],[51,3019,theory(equality)])).
% cnf(3095,negated_conjecture,(ld(mult(b,c),mult(c,mult(b,b)))=ld(ld(b,unit),unit)),inference(spm,[status(thm)],[2904,3057,theory(equality)])).
% cnf(3113,negated_conjecture,(b=ld(ld(b,unit),unit)),inference(rw,[status(thm)],[3095,181,theory(equality)])).
% cnf(3336,negated_conjecture,(rd(unit,b)=ld(b,unit)),inference(spm,[status(thm)],[40,3113,theory(equality)])).
% cnf(3418,negated_conjecture,(ld(ld(b,unit),mult(b,c))=mult(c,mult(b,b))),inference(rw,[status(thm)],[2532,3336,theory(equality)])).
% cnf(3460,plain,(ld(X1,mult(X1,rd(unit,X2)))=ld(X2,unit)),inference(spm,[status(thm)],[2904,2942,theory(equality)])).
% cnf(3506,plain,(rd(unit,X2)=ld(X2,unit)),inference(rw,[status(thm)],[3460,15,theory(equality)])).
% cnf(3729,plain,(mult(ld(X1,unit),mult(mult(X1,X2),X1))=mult(mult(unit,X2),X1)),inference(spm,[status(thm)],[47,3506,theory(equality)])).
% cnf(3740,negated_conjecture,(rd(mult(b,c),mult(b,mult(c,c)))=ld(c,unit)),inference(rw,[status(thm)],[2483,3506,theory(equality)])).
% cnf(3749,plain,(mult(ld(X1,unit),mult(mult(X1,X2),X1))=mult(X2,X1)),inference(rw,[status(thm)],[3729,23,theory(equality)])).
% cnf(4263,plain,(mult(rd(mult(X1,X2),X3),X2)=mult(X1,mult(mult(X2,ld(X3,unit)),X2))),inference(spm,[status(thm)],[25,2952,theory(equality)])).
% cnf(4271,plain,(mult(X1,rd(mult(ld(X1,unit),X2),X1))=mult(mult(unit,X2),ld(X1,unit))),inference(spm,[status(thm)],[49,2952,theory(equality)])).
% cnf(4311,plain,(mult(X1,mult(rd(X2,mult(X1,X2)),X2))=mult(unit,X2)),inference(spm,[status(thm)],[51,2952,theory(equality)])).
% cnf(4353,plain,(mult(rd(mult(X1,X2),X3),X2)=mult(X1,mult(rd(X2,X3),X2))),inference(rw,[status(thm)],[4263,2952,theory(equality)])).
% cnf(4364,plain,(mult(X1,rd(mult(ld(X1,unit),X2),X1))=rd(X2,X1)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[4271,23,theory(equality)]),2952,theory(equality)])).
% cnf(4407,plain,(mult(X1,mult(rd(X2,mult(X1,X2)),X2))=X2),inference(rw,[status(thm)],[4311,23,theory(equality)])).
% cnf(5578,negated_conjecture,(mult(b,mult(rd(c,b),c))=mult(c,c)),inference(rw,[status(thm)],[3075,2952,theory(equality)])).
% cnf(5631,plain,(rd(X1,ld(X3,X2))=mult(X1,ld(X2,X3))),inference(spm,[status(thm)],[3014,3056,theory(equality)])).
% cnf(5685,plain,(ld(rd(X1,X2),mult(rd(X1,X2),mult(X2,X3)))=mult(X3,X2)|mult(rd(X1,X2),mult(X2,X3))=mult(X1,X3)),inference(spm,[status(thm)],[15,68,theory(equality)])).
% cnf(5888,plain,(mult(X2,X3)=mult(X3,X2)|mult(rd(X1,X2),mult(X2,X3))=mult(X1,X3)),inference(rw,[status(thm)],[5685,15,theory(equality)])).
% cnf(6439,plain,(ld(X1,X2)=mult(rd(X2,mult(X1,X2)),X2)),inference(spm,[status(thm)],[15,4407,theory(equality)])).
% cnf(7130,plain,(rd(ld(X2,X1),X1)=rd(X1,mult(X2,X1))),inference(spm,[status(thm)],[19,6439,theory(equality)])).
% cnf(7180,plain,(mult(rd(X1,X2),X1)=ld(rd(X2,X1),X1)),inference(spm,[status(thm)],[6439,17,theory(equality)])).
% cnf(7550,plain,(rd(X2,X1)=rd(X1,mult(rd(X1,X2),X1))),inference(spm,[status(thm)],[7130,37,theory(equality)])).
% cnf(8032,plain,(mult(rd(X1,X2),mult(rd(X2,X1),X2))=X2),inference(spm,[status(thm)],[13,7180,theory(equality)])).
% cnf(8644,plain,(mult(rd(X1,mult(X2,X1)),mult(X2,mult(X2,X1)))=mult(X2,X1)),inference(spm,[status(thm)],[8032,19,theory(equality)])).
% cnf(9311,plain,(mult(X1,mult(X2,X3))=mult(mult(X1,X2),X3)|mult(X2,X3)=mult(X3,X2)),inference(spm,[status(thm)],[5888,19,theory(equality)])).
% cnf(9744,plain,(rd(mult(X1,mult(X2,X3)),X3)=mult(X1,X2)|mult(X2,X3)=mult(X3,X2)),inference(spm,[status(thm)],[19,9311,theory(equality)])).
% cnf(9910,plain,(mult(mult(X1,X3),ld(X3,X2))=mult(X1,X2)|mult(X2,X3)=mult(X3,X2)),inference(rw,[status(thm)],[9744,434,theory(equality)])).
% cnf(11443,plain,(mult(ld(X1,unit),mult(X2,X1))=mult(ld(X1,X2),X1)),inference(spm,[status(thm)],[3749,13,theory(equality)])).
% cnf(13428,negated_conjecture,(mult(ld(b,unit),mult(b,c))=mult(ld(b,c),b)),inference(spm,[status(thm)],[11443,144,theory(equality)])).
% cnf(13627,plain,(mult(mult(X1,X3),mult(X2,X2))=mult(X1,mult(mult(X2,X3),X2))|mult(mult(X1,X3),X2)=mult(X1,mult(X3,X2))),inference(rw,[status(thm)],[94,57,theory(equality)])).
% cnf(14013,negated_conjecture,(mult(b,mult(ld(b,c),b))=mult(b,mult(mult(b,c),ld(b,unit)))|mult(b,mult(ld(b,c),b))=mult(unit,mult(b,c))),inference(spm,[status(thm)],[71,13428,theory(equality)])).
% cnf(14067,negated_conjecture,(mult(b,mult(ld(b,c),b))=mult(b,c)|mult(b,mult(ld(b,c),b))=mult(unit,mult(b,c))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[14013,2952,theory(equality)]),146,theory(equality)])).
% cnf(14068,negated_conjecture,(mult(b,mult(ld(b,c),b))=mult(b,c)|mult(b,mult(ld(b,c),b))=mult(b,c)),inference(rw,[status(thm)],[14067,23,theory(equality)])).
% cnf(14069,negated_conjecture,(mult(b,mult(ld(b,c),b))=mult(b,c)),inference(cn,[status(thm)],[14068,theory(equality)])).
% cnf(14070,negated_conjecture,(ld(b,mult(b,c))=mult(ld(b,c),b)),inference(spm,[status(thm)],[15,14069,theory(equality)])).
% cnf(14120,negated_conjecture,(c=mult(ld(b,c),b)),inference(rw,[status(thm)],[14070,15,theory(equality)])).
% cnf(14149,negated_conjecture,(ld(ld(b,c),c)=b),inference(spm,[status(thm)],[15,14120,theory(equality)])).
% cnf(14150,negated_conjecture,(rd(c,b)=ld(b,c)),inference(spm,[status(thm)],[19,14120,theory(equality)])).
% cnf(14153,negated_conjecture,(mult(mult(c,X1),b)=mult(ld(b,c),mult(mult(b,X1),b))),inference(spm,[status(thm)],[25,14120,theory(equality)])).
% cnf(14202,negated_conjecture,(mult(ld(b,unit),mult(b,c))=c),inference(rw,[status(thm)],[13428,14120,theory(equality)])).
% cnf(14240,negated_conjecture,(mult(rd(b,c),mult(ld(b,c),c))=c),inference(spm,[status(thm)],[8032,14150,theory(equality)])).
% cnf(14251,negated_conjecture,(mult(b,mult(ld(b,c),c))=mult(c,c)),inference(rw,[status(thm)],[5578,14150,theory(equality)])).
% cnf(14313,negated_conjecture,(mult(rd(mult(b,c),c),mult(b,c))=ld(ld(b,unit),mult(b,c))),inference(spm,[status(thm)],[6439,14202,theory(equality)])).
% cnf(14361,negated_conjecture,(mult(b,mult(b,c))=ld(ld(b,unit),mult(b,c))),inference(rw,[status(thm)],[14313,19,theory(equality)])).
% cnf(14362,negated_conjecture,(mult(b,mult(b,c))=mult(c,mult(b,b))),inference(rw,[status(thm)],[14361,3418,theory(equality)])).
% cnf(14547,negated_conjecture,(mult(rd(X1,b),mult(b,mult(b,c)))=mult(mult(X1,c),b)),inference(rw,[status(thm)],[1086,14362,theory(equality)])).
% cnf(17273,negated_conjecture,(mult(rd(b,c),mult(c,ld(b,c)))=c|mult(rd(b,c),mult(c,ld(b,c)))=mult(b,ld(b,c))),inference(spm,[status(thm)],[68,14240,theory(equality)])).
% cnf(17283,negated_conjecture,(mult(rd(b,c),mult(c,ld(b,c)))=c|mult(rd(b,c),mult(c,ld(b,c)))=c),inference(rw,[status(thm)],[17273,13,theory(equality)])).
% cnf(17284,negated_conjecture,(mult(rd(b,c),mult(c,ld(b,c)))=c),inference(cn,[status(thm)],[17283,theory(equality)])).
% cnf(18703,negated_conjecture,(ld(rd(b,c),c)=mult(c,ld(b,c))),inference(spm,[status(thm)],[15,17284,theory(equality)])).
% cnf(18757,negated_conjecture,(mult(ld(b,c),c)=mult(c,ld(b,c))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[18703,7180,theory(equality)]),14150,theory(equality)])).
% cnf(18823,negated_conjecture,(mult(b,mult(c,ld(b,c)))=mult(c,c)),inference(rw,[status(thm)],[14251,18757,theory(equality)])).
% cnf(18902,negated_conjecture,(rd(mult(c,c),ld(b,c))=mult(mult(b,ld(b,c)),ld(ld(b,c),c))),inference(spm,[status(thm)],[434,18823,theory(equality)])).
% cnf(18909,negated_conjecture,(mult(mult(c,c),ld(c,b))=mult(mult(b,ld(b,c)),ld(ld(b,c),c))),inference(rw,[status(thm)],[18902,5631,theory(equality)])).
% cnf(18910,negated_conjecture,(mult(mult(c,c),ld(c,b))=mult(b,c)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[18909,13,theory(equality)]),14149,theory(equality)]),144,theory(equality)])).
% cnf(18962,negated_conjecture,(mult(mult(b,c),c)=mult(c,mult(mult(c,ld(c,b)),c))),inference(spm,[status(thm)],[25,18910,theory(equality)])).
% cnf(18993,negated_conjecture,(mult(b,mult(c,c))=mult(c,mult(mult(c,ld(c,b)),c))),inference(rw,[status(thm)],[18962,57,theory(equality)])).
% cnf(18994,negated_conjecture,(mult(b,mult(c,c))=mult(c,mult(b,c))),inference(rw,[status(thm)],[18993,13,theory(equality)])).
% cnf(19066,negated_conjecture,(mult(rd(mult(b,c),mult(b,mult(c,c))),mult(b,c))=ld(c,mult(b,c))),inference(spm,[status(thm)],[6439,18994,theory(equality)])).
% cnf(19104,negated_conjecture,(mult(ld(c,b),c)=ld(c,mult(b,c))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[19066,3740,theory(equality)]),11443,theory(equality)])).
% cnf(19105,negated_conjecture,(mult(ld(c,b),c)=b),inference(rw,[status(thm)],[19104,145,theory(equality)])).
% cnf(19188,negated_conjecture,(mult(mult(b,X1),c)=mult(ld(c,b),mult(mult(c,X1),c))),inference(spm,[status(thm)],[25,19105,theory(equality)])).
% cnf(68841,plain,(mult(mult(X1,X2),X3)=mult(X1,mult(X2,X3))|mult(mult(X2,X3),X2)=mult(X2,mult(X2,X3))),inference(spm,[status(thm)],[9910,15,theory(equality)])).
% cnf(72883,plain,(mult(mult(X1,X1),X2)=mult(X1,mult(X1,X2))|mult(mult(X3,X1),X2)=mult(X3,mult(X1,X2))),inference(spm,[status(thm)],[83,68841,theory(equality)])).
% cnf(75811,plain,(mult(mult(X4,X4),X5)=mult(X4,mult(X4,X5))),inference(ef,[status(thm)],[72883,theory(equality)])).
% cnf(77341,plain,(ld(mult(X1,mult(X1,ld(X1,X2))),mult(X1,mult(X2,X1)))=X1),inference(spm,[status(thm)],[236,75811,theory(equality)])).
% cnf(77789,plain,(ld(mult(X1,X2),mult(X1,mult(X2,X1)))=X1),inference(rw,[status(thm)],[77341,13,theory(equality)])).
% cnf(85087,plain,(mult(mult(X1,X2),X1)=mult(X1,mult(X2,X1))),inference(spm,[status(thm)],[13,77789,theory(equality)])).
% cnf(85829,plain,(rd(mult(X1,mult(X2,mult(X3,X2))),X2)=mult(mult(X1,X2),ld(X2,mult(X2,X3)))),inference(spm,[status(thm)],[434,85087,theory(equality)])).
% cnf(85885,plain,(mult(X1,mult(ld(X1,X2),X1))=mult(rd(X1,X1),mult(X2,X1))),inference(spm,[status(thm)],[1083,85087,theory(equality)])).
% cnf(86051,plain,(mult(rd(X2,X1),X1)=mult(X1,mult(rd(mult(ld(X1,unit),X2),X1),X1))),inference(spm,[status(thm)],[85087,4364,theory(equality)])).
% cnf(86072,plain,(mult(mult(X1,X2),mult(X3,X3))=mult(X1,mult(X3,mult(X2,X3)))|mult(mult(X1,X2),X3)=mult(X1,mult(X2,X3))),inference(rw,[status(thm)],[13627,85087,theory(equality)])).
% cnf(86092,plain,(mult(rd(X1,X2),mult(X2,mult(X3,X2)))=mult(mult(X1,X3),X2)),inference(rw,[status(thm)],[47,85087,theory(equality)])).
% cnf(86098,plain,(mult(mult(mult(X1,X2),X3),X2)=mult(X1,mult(X2,mult(X3,X2)))),inference(rw,[status(thm)],[25,85087,theory(equality)])).
% cnf(86104,negated_conjecture,(mult(ld(b,c),mult(b,mult(X1,b)))=mult(mult(c,X1),b)),inference(rw,[status(thm)],[14153,85087,theory(equality)])).
% cnf(86125,negated_conjecture,(mult(ld(c,b),mult(c,mult(X1,c)))=mult(mult(b,X1),c)),inference(rw,[status(thm)],[19188,85087,theory(equality)])).
% cnf(86146,plain,(rd(mult(X1,mult(X2,mult(X3,X2))),X2)=mult(mult(X1,X2),X3)),inference(rw,[status(thm)],[85829,15,theory(equality)])).
% cnf(86179,plain,(mult(X1,mult(ld(X1,X2),X1))=mult(X2,X1)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[85885,38,theory(equality)]),23,theory(equality)])).
% cnf(86345,plain,(X2=mult(X1,mult(rd(mult(ld(X1,unit),X2),X1),X1))),inference(rw,[status(thm)],[86051,17,theory(equality)])).
% cnf(86346,plain,(X2=mult(X1,mult(ld(X1,unit),X2))),inference(rw,[status(thm)],[86345,17,theory(equality)])).
% cnf(88359,negated_conjecture,(mult(ld(b,c),mult(b,X1))=mult(mult(c,rd(X1,b)),b)),inference(spm,[status(thm)],[86104,17,theory(equality)])).
% cnf(88577,plain,(mult(rd(mult(ld(X1,unit),X2),X2),mult(X1,X2))=X2),inference(spm,[status(thm)],[8644,86346,theory(equality)])).
% cnf(88667,plain,(mult(ld(X1,unit),mult(X1,X2))=X2),inference(rw,[status(thm)],[88577,19,theory(equality)])).
% cnf(88759,plain,(rd(X2,mult(X1,X2))=ld(X1,unit)),inference(spm,[status(thm)],[19,88667,theory(equality)])).
% cnf(89205,plain,(ld(ld(X2,unit),X1)=mult(X2,X1)),inference(spm,[status(thm)],[37,88759,theory(equality)])).
% cnf(89382,plain,(mult(ld(X2,unit),X1)=ld(X2,X1)),inference(rw,[status(thm)],[6439,88759,theory(equality)])).
% cnf(89384,plain,(rd(ld(X1,X2),X2)=ld(X1,unit)),inference(rw,[status(thm)],[7130,88759,theory(equality)])).
% cnf(89386,plain,(ld(rd(X1,X2),unit)=rd(X2,X1)),inference(rw,[status(thm)],[7550,88759,theory(equality)])).
% cnf(90716,negated_conjecture,(mult(ld(c,b),mult(c,X1))=mult(mult(b,rd(X1,c)),c)),inference(spm,[status(thm)],[86125,17,theory(equality)])).
% cnf(91316,plain,(ld(X1,mult(X2,X1))=mult(ld(X1,X2),X1)),inference(spm,[status(thm)],[15,86179,theory(equality)])).
% cnf(91904,plain,(mult(ld(X2,X1),X3)=ld(ld(X1,X2),X3)),inference(spm,[status(thm)],[89382,3056,theory(equality)])).
% cnf(91909,plain,(mult(X1,rd(ld(X1,X2),X1))=rd(X2,X1)),inference(rw,[status(thm)],[4364,89382,theory(equality)])).
% cnf(94419,negated_conjecture,(mult(ld(X1,unit),mult(b,mult(c,c)))=mult(mult(ld(X1,c),b),c)),inference(spm,[status(thm)],[1114,89384,theory(equality)])).
% cnf(94421,negated_conjecture,(mult(ld(X1,unit),mult(b,mult(b,c)))=mult(mult(ld(X1,b),c),b)),inference(spm,[status(thm)],[14547,89384,theory(equality)])).
% cnf(94556,negated_conjecture,(ld(X1,mult(b,mult(c,c)))=mult(mult(ld(X1,c),b),c)),inference(rw,[status(thm)],[94419,89382,theory(equality)])).
% cnf(94558,negated_conjecture,(ld(X1,mult(b,mult(b,c)))=mult(mult(ld(X1,b),c),b)),inference(rw,[status(thm)],[94421,89382,theory(equality)])).
% cnf(96002,negated_conjecture,(mult(X1,mult(mult(ld(X1,c),b),c))=mult(b,mult(c,c))),inference(spm,[status(thm)],[13,94556,theory(equality)])).
% cnf(96047,negated_conjecture,(mult(X1,mult(mult(ld(X1,b),c),b))=mult(b,mult(b,c))),inference(spm,[status(thm)],[13,94558,theory(equality)])).
% cnf(96740,plain,(rd(X1,rd(X3,X2))=mult(X1,ld(unit,rd(X2,X3)))),inference(spm,[status(thm)],[5631,89386,theory(equality)])).
% cnf(96750,plain,(mult(rd(X2,X1),X3)=ld(rd(X1,X2),X3)),inference(spm,[status(thm)],[89382,89386,theory(equality)])).
% cnf(96826,plain,(rd(X1,rd(X3,X2))=mult(X1,rd(X2,X3))),inference(rw,[status(thm)],[96740,33,theory(equality)])).
% cnf(97827,negated_conjecture,(mult(mult(c,X1),mult(mult(ld(X1,unit),b),c))=mult(b,mult(c,c))),inference(spm,[status(thm)],[96002,2904,theory(equality)])).
% cnf(97908,negated_conjecture,(mult(mult(c,X1),mult(ld(X1,b),c))=mult(b,mult(c,c))),inference(rw,[status(thm)],[97827,89382,theory(equality)])).
% cnf(98077,negated_conjecture,(mult(mult(b,X1),mult(mult(ld(X1,unit),c),b))=mult(b,mult(b,c))),inference(spm,[status(thm)],[96047,2904,theory(equality)])).
% cnf(98158,negated_conjecture,(mult(mult(b,X1),mult(ld(X1,c),b))=mult(b,mult(b,c))),inference(rw,[status(thm)],[98077,89382,theory(equality)])).
% cnf(98414,plain,(mult(X1,mult(X2,ld(X1,unit)))=mult(ld(ld(X1,unit),X2),ld(X1,unit))),inference(spm,[status(thm)],[91316,89205,theory(equality)])).
% cnf(98491,plain,(mult(X1,rd(X2,X1))=mult(ld(ld(X1,unit),X2),ld(X1,unit))),inference(rw,[status(thm)],[98414,2952,theory(equality)])).
% cnf(98492,plain,(mult(X1,rd(X2,X1))=rd(mult(X1,X2),X1)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[98491,2952,theory(equality)]),89205,theory(equality)])).
% cnf(98938,plain,(ld(rd(X2,X1),X1)=ld(rd(ld(X1,X2),X1),unit)),inference(spm,[status(thm)],[2904,91909,theory(equality)])).
% cnf(99081,plain,(mult(rd(X1,X2),X1)=ld(rd(ld(X1,X2),X1),unit)),inference(rw,[status(thm)],[98938,7180,theory(equality)])).
% cnf(99082,plain,(mult(rd(X1,X2),X1)=mult(X1,ld(X2,X1))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[99081,89386,theory(equality)]),5631,theory(equality)])).
% cnf(100010,negated_conjecture,(mult(mult(c,mult(b,X1)),mult(ld(X1,unit),c))=mult(b,mult(c,c))),inference(spm,[status(thm)],[97908,2904,theory(equality)])).
% cnf(100053,negated_conjecture,(mult(mult(c,mult(b,X1)),ld(X1,c))=mult(b,mult(c,c))),inference(rw,[status(thm)],[100010,89382,theory(equality)])).
% cnf(100445,negated_conjecture,(mult(mult(b,mult(c,X1)),mult(ld(X1,unit),b))=mult(b,mult(b,c))),inference(spm,[status(thm)],[98158,2904,theory(equality)])).
% cnf(100494,negated_conjecture,(mult(mult(b,mult(c,X1)),ld(X1,b))=mult(b,mult(b,c))),inference(rw,[status(thm)],[100445,89382,theory(equality)])).
% cnf(100703,plain,(mult(ld(X2,unit),X1)=mult(X1,ld(mult(X2,X1),X1))),inference(spm,[status(thm)],[99082,88759,theory(equality)])).
% cnf(100708,plain,(mult(rd(mult(X1,X2),X3),X2)=mult(X1,mult(X2,ld(X3,X2)))),inference(rw,[status(thm)],[4353,99082,theory(equality)])).
% cnf(100816,plain,(ld(X2,X1)=mult(X1,ld(mult(X2,X1),X1))),inference(rw,[status(thm)],[100703,89382,theory(equality)])).
% cnf(102138,negated_conjecture,(rd(mult(b,mult(c,c)),ld(X1,c))=mult(c,mult(b,X1))),inference(spm,[status(thm)],[19,100053,theory(equality)])).
% cnf(102258,negated_conjecture,(mult(mult(c,mult(b,rd(c,X1))),X1)=mult(b,mult(c,c))),inference(spm,[status(thm)],[100053,37,theory(equality)])).
% cnf(102293,negated_conjecture,(mult(mult(b,mult(c,c)),ld(c,X1))=mult(c,mult(b,X1))),inference(rw,[status(thm)],[102138,5631,theory(equality)])).
% cnf(104601,negated_conjecture,(rd(mult(b,mult(b,c)),ld(X1,b))=mult(b,mult(c,X1))),inference(spm,[status(thm)],[19,100494,theory(equality)])).
% cnf(104726,negated_conjecture,(mult(mult(b,mult(c,rd(b,X1))),X1)=mult(b,mult(b,c))),inference(spm,[status(thm)],[100494,37,theory(equality)])).
% cnf(104763,negated_conjecture,(mult(mult(b,mult(b,c)),ld(b,X1))=mult(b,mult(c,X1))),inference(rw,[status(thm)],[104601,5631,theory(equality)])).
% cnf(105045,negated_conjecture,(mult(mult(c,mult(b,X1)),c)=mult(rd(mult(b,mult(c,c)),c),mult(X1,c))),inference(spm,[status(thm)],[1083,102293,theory(equality)])).
% cnf(105115,negated_conjecture,(mult(c,mult(mult(b,X1),c))=mult(rd(mult(b,mult(c,c)),c),mult(X1,c))),inference(rw,[status(thm)],[105045,85087,theory(equality)])).
% cnf(105116,negated_conjecture,(mult(c,mult(mult(b,X1),c))=mult(mult(b,c),mult(X1,c))),inference(rw,[status(thm)],[105115,301,theory(equality)])).
% cnf(106512,negated_conjecture,(mult(mult(b,c),X1)=mult(c,mult(mult(b,rd(X1,c)),c))),inference(spm,[status(thm)],[105116,17,theory(equality)])).
% cnf(106622,negated_conjecture,(mult(mult(b,c),X1)=mult(c,mult(ld(c,b),mult(c,X1)))),inference(rw,[status(thm)],[106512,90716,theory(equality)])).
% cnf(109562,negated_conjecture,(mult(mult(b,mult(c,X1)),b)=mult(rd(mult(b,mult(b,c)),b),mult(X1,b))),inference(spm,[status(thm)],[1083,104763,theory(equality)])).
% cnf(109603,negated_conjecture,(mult(mult(b,mult(b,c)),X1)=mult(b,mult(c,mult(b,X1)))),inference(spm,[status(thm)],[104763,15,theory(equality)])).
% cnf(109637,negated_conjecture,(mult(b,mult(mult(c,X1),b))=mult(rd(mult(b,mult(b,c)),b),mult(X1,b))),inference(rw,[status(thm)],[109562,85087,theory(equality)])).
% cnf(109638,negated_conjecture,(mult(b,mult(mult(c,X1),b))=mult(mult(b,c),mult(X1,b))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[109637,2572,theory(equality)]),75811,theory(equality)]),13,theory(equality)])).
% cnf(109844,negated_conjecture,(mult(mult(b,c),X1)=mult(b,mult(mult(c,rd(X1,b)),b))),inference(spm,[status(thm)],[109638,17,theory(equality)])).
% cnf(109925,negated_conjecture,(mult(mult(b,c),X1)=mult(b,mult(ld(b,c),mult(b,X1)))),inference(rw,[status(thm)],[109844,88359,theory(equality)])).
% cnf(115944,negated_conjecture,(mult(c,mult(ld(c,b),X1))=mult(mult(b,c),ld(c,X1))),inference(spm,[status(thm)],[106622,13,theory(equality)])).
% cnf(120954,negated_conjecture,(mult(b,mult(ld(b,c),X1))=mult(mult(b,c),ld(b,X1))),inference(spm,[status(thm)],[109925,13,theory(equality)])).
% cnf(131374,negated_conjecture,(mult(mult(c,mult(ld(c,b),X1)),c)=mult(rd(mult(b,c),c),mult(X1,c))),inference(spm,[status(thm)],[1083,115944,theory(equality)])).
% cnf(131461,negated_conjecture,(mult(c,mult(mult(ld(c,b),X1),c))=mult(rd(mult(b,c),c),mult(X1,c))),inference(rw,[status(thm)],[131374,85087,theory(equality)])).
% cnf(131462,negated_conjecture,(mult(c,mult(mult(ld(c,b),X1),c))=mult(b,mult(X1,c))),inference(rw,[status(thm)],[131461,19,theory(equality)])).
% cnf(132087,plain,(mult(rd(X2,X1),mult(rd(X1,X2),X3))=X3),inference(spm,[status(thm)],[15,96750,theory(equality)])).
% cnf(156291,plain,(mult(rd(X1,X2),mult(mult(X2,X3),X1))=mult(X1,mult(X3,X1))),inference(spm,[status(thm)],[132087,86092,theory(equality)])).
% cnf(189110,plain,(mult(rd(X1,rd(X2,X3)),mult(X2,X1))=mult(X1,mult(X3,X1))),inference(spm,[status(thm)],[156291,17,theory(equality)])).
% cnf(189385,negated_conjecture,(mult(rd(X1,c),mult(b,mult(c,c)))=mult(X1,mult(mult(b,rd(c,X1)),X1))),inference(spm,[status(thm)],[156291,102258,theory(equality)])).
% cnf(189396,negated_conjecture,(mult(rd(X1,b),mult(b,mult(b,c)))=mult(X1,mult(mult(c,rd(b,X1)),X1))),inference(spm,[status(thm)],[156291,104726,theory(equality)])).
% cnf(189638,plain,(mult(mult(X1,rd(X3,X2)),mult(X2,X1))=mult(X1,mult(X3,X1))),inference(rw,[status(thm)],[189110,96826,theory(equality)])).
% cnf(189821,negated_conjecture,(mult(mult(X1,b),c)=mult(X1,mult(mult(b,rd(c,X1)),X1))),inference(rw,[status(thm)],[189385,1114,theory(equality)])).
% cnf(189823,negated_conjecture,(mult(mult(X1,c),b)=mult(X1,mult(mult(c,rd(b,X1)),X1))),inference(rw,[status(thm)],[189396,14547,theory(equality)])).
% cnf(194554,negated_conjecture,(mult(X1,mult(b,mult(rd(c,X1),X1)))=mult(mult(X1,b),c)|mult(rd(c,X1),X1)=mult(X1,rd(c,X1))),inference(spm,[status(thm)],[189821,9311,theory(equality)])).
% cnf(194862,negated_conjecture,(mult(X1,mult(b,c))=mult(mult(X1,b),c)|mult(rd(c,X1),X1)=mult(X1,rd(c,X1))),inference(rw,[status(thm)],[194554,17,theory(equality)])).
% cnf(194863,negated_conjecture,(mult(X1,mult(b,c))=mult(mult(X1,b),c)|c=mult(X1,rd(c,X1))),inference(rw,[status(thm)],[194862,17,theory(equality)])).
% cnf(196492,negated_conjecture,(mult(c,X1)=mult(X1,mult(rd(c,X1),X1))|mult(mult(X1,b),c)=mult(X1,mult(b,c))),inference(spm,[status(thm)],[85087,194863,theory(equality)])).
% cnf(196852,negated_conjecture,(mult(c,X1)=mult(X1,c)|mult(mult(X1,b),c)=mult(X1,mult(b,c))),inference(rw,[status(thm)],[196492,17,theory(equality)])).
% cnf(197134,negated_conjecture,(mult(c,a)=mult(a,c)),inference(spm,[status(thm)],[32,196852,theory(equality)])).
% cnf(197419,negated_conjecture,(ld(c,mult(a,c))=a),inference(spm,[status(thm)],[15,197134,theory(equality)])).
% cnf(197464,negated_conjecture,(mult(rd(mult(a,c),X1),a)=mult(c,mult(a,ld(X1,a)))),inference(spm,[status(thm)],[100708,197134,theory(equality)])).
% cnf(197487,negated_conjecture,(rd(mult(X1,mult(a,c)),a)=mult(mult(X1,a),ld(a,c))),inference(spm,[status(thm)],[434,197134,theory(equality)])).
% cnf(197499,negated_conjecture,(rd(mult(X1,mult(a,mult(a,c))),a)=mult(mult(X1,a),c)),inference(spm,[status(thm)],[86146,197134,theory(equality)])).
% cnf(197521,negated_conjecture,(mult(a,ld(mult(a,c),a))=ld(c,a)),inference(spm,[status(thm)],[100816,197134,theory(equality)])).
% cnf(197546,negated_conjecture,(mult(ld(c,a),c)=a),inference(rw,[status(thm)],[197419,91316,theory(equality)])).
% cnf(197560,negated_conjecture,(rd(a,c)=ld(c,a)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[197521,2904,theory(equality)]),2952,theory(equality)])).
% cnf(199069,negated_conjecture,(rd(c,a)=ld(ld(c,a),unit)),inference(spm,[status(thm)],[88759,197546,theory(equality)])).
% cnf(199179,negated_conjecture,(rd(c,a)=ld(a,c)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[199069,91904,theory(equality)]),21,theory(equality)])).
% cnf(200876,negated_conjecture,(mult(a,mult(mult(b,ld(a,c)),a))=mult(mult(a,b),c)),inference(spm,[status(thm)],[189821,199179,theory(equality)])).
% cnf(200907,negated_conjecture,(mult(a,mult(rd(b,a),mult(a,c)))=mult(mult(a,b),c)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[200876,1083,theory(equality)]),197134,theory(equality)])).
% cnf(241141,negated_conjecture,(mult(X1,mult(c,mult(rd(b,X1),X1)))=mult(mult(X1,c),b)|mult(rd(b,X1),X1)=mult(X1,rd(b,X1))),inference(spm,[status(thm)],[189823,9311,theory(equality)])).
% cnf(241520,negated_conjecture,(mult(X1,mult(b,c))=mult(mult(X1,c),b)|mult(rd(b,X1),X1)=mult(X1,rd(b,X1))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[241141,17,theory(equality)]),144,theory(equality)])).
% cnf(241521,negated_conjecture,(mult(X1,mult(b,c))=mult(mult(X1,c),b)|b=mult(X1,rd(b,X1))),inference(rw,[status(thm)],[241520,17,theory(equality)])).
% cnf(241736,negated_conjecture,(mult(b,X1)=mult(X1,mult(rd(b,X1),X1))|mult(mult(X1,c),b)=mult(X1,mult(b,c))),inference(spm,[status(thm)],[85087,241521,theory(equality)])).
% cnf(242122,negated_conjecture,(mult(b,X1)=mult(X1,b)|mult(mult(X1,c),b)=mult(X1,mult(b,c))),inference(rw,[status(thm)],[241736,17,theory(equality)])).
% cnf(242462,negated_conjecture,(mult(mult(X1,b),c)=mult(X1,mult(b,c))|mult(b,X1)=mult(X1,b)),inference(spm,[status(thm)],[83,242122,theory(equality)])).
% cnf(242997,negated_conjecture,(mult(rd(X1,c),mult(c,b))=mult(X1,b)|mult(rd(X1,c),mult(b,c))=mult(X1,b)|mult(b,rd(X1,c))=mult(rd(X1,c),b)),inference(spm,[status(thm)],[112,242462,theory(equality)])).
% cnf(243055,negated_conjecture,(mult(b,a)=mult(a,b)),inference(spm,[status(thm)],[32,242462,theory(equality)])).
% cnf(243170,negated_conjecture,(mult(rd(X1,c),mult(b,c))=mult(X1,b)|mult(rd(X1,c),mult(b,c))=mult(X1,b)|mult(b,rd(X1,c))=mult(rd(X1,c),b)),inference(rw,[status(thm)],[242997,144,theory(equality)])).
% cnf(243171,negated_conjecture,(mult(rd(X1,c),mult(b,c))=mult(X1,b)|mult(b,rd(X1,c))=mult(rd(X1,c),b)),inference(cn,[status(thm)],[243170,theory(equality)])).
% cnf(243323,negated_conjecture,(ld(b,mult(a,b))=a),inference(spm,[status(thm)],[15,243055,theory(equality)])).
% cnf(243327,negated_conjecture,(mult(mult(mult(a,b),X1),a)=mult(b,mult(a,mult(X1,a)))),inference(spm,[status(thm)],[86098,243055,theory(equality)])).
% cnf(243372,negated_conjecture,(ld(mult(a,b),b)=ld(a,unit)),inference(spm,[status(thm)],[2904,243055,theory(equality)])).
% cnf(243441,negated_conjecture,(rd(a,mult(a,b))=ld(b,unit)),inference(spm,[status(thm)],[88759,243055,theory(equality)])).
% cnf(243454,negated_conjecture,(mult(b,mult(ld(b,c),mult(a,b)))=mult(mult(b,c),a)),inference(spm,[status(thm)],[109925,243055,theory(equality)])).
% cnf(243461,negated_conjecture,(mult(ld(b,a),b)=a),inference(rw,[status(thm)],[243323,91316,theory(equality)])).
% cnf(243627,negated_conjecture,(rd(b,a)=ld(ld(b,a),unit)),inference(spm,[status(thm)],[88759,243461,theory(equality)])).
% cnf(243760,negated_conjecture,(rd(b,a)=ld(a,b)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[243627,91904,theory(equality)]),21,theory(equality)])).
% cnf(247611,negated_conjecture,(mult(mult(a,b),mult(mult(ld(a,unit),c),b))=mult(b,mult(b,c))),inference(spm,[status(thm)],[96047,243372,theory(equality)])).
% cnf(247680,negated_conjecture,(mult(mult(a,b),mult(ld(a,c),b))=mult(b,mult(b,c))),inference(rw,[status(thm)],[247611,89382,theory(equality)])).
% cnf(309237,plain,(mult(mult(X1,X2),mult(X3,X1))=mult(X1,mult(mult(X2,X3),X1))),inference(spm,[status(thm)],[189638,19,theory(equality)])).
% cnf(310363,negated_conjecture,(mult(mult(a,X1),mult(a,c))=mult(a,mult(mult(X1,c),a))),inference(spm,[status(thm)],[309237,197134,theory(equality)])).
% cnf(340723,negated_conjecture,(mult(a,mult(ld(a,b),mult(a,c)))=mult(mult(a,b),c)),inference(rw,[status(thm)],[200907,243760,theory(equality)])).
% cnf(382161,negated_conjecture,(mult(rd(X1,c),mult(c,mult(b,c)))=mult(X1,mult(b,c))|mult(mult(X1,b),c)=mult(X1,mult(b,c))|mult(rd(X1,c),b)=mult(b,rd(X1,c))),inference(spm,[status(thm)],[112,243171,theory(equality)])).
% cnf(382354,negated_conjecture,(mult(mult(X1,b),c)=mult(X1,mult(b,c))|mult(mult(X1,b),c)=mult(X1,mult(b,c))|mult(rd(X1,c),b)=mult(b,rd(X1,c))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[382161,18994,theory(equality)]),1114,theory(equality)])).
% cnf(382355,negated_conjecture,(mult(mult(X1,b),c)=mult(X1,mult(b,c))|mult(rd(X1,c),b)=mult(b,rd(X1,c))),inference(cn,[status(thm)],[382354,theory(equality)])).
% cnf(382600,negated_conjecture,(mult(ld(c,a),b)=mult(b,ld(c,a))|mult(mult(a,b),c)=mult(a,mult(b,c))),inference(spm,[status(thm)],[382355,197560,theory(equality)])).
% cnf(382712,negated_conjecture,(mult(ld(c,a),b)=mult(b,ld(c,a))),inference(sr,[status(thm)],[382600,32,theory(equality)])).
% cnf(382900,negated_conjecture,(mult(b,ld(mult(b,ld(c,a)),b))=ld(ld(c,a),b)),inference(spm,[status(thm)],[100816,382712,theory(equality)])).
% cnf(382972,negated_conjecture,(mult(b,ld(a,c))=ld(ld(c,a),b)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[382900,2904,theory(equality)]),91904,theory(equality)]),21,theory(equality)])).
% cnf(382973,negated_conjecture,(mult(b,ld(a,c))=mult(ld(a,c),b)),inference(rw,[status(thm)],[382972,91904,theory(equality)])).
% cnf(394052,negated_conjecture,(mult(mult(a,b),mult(b,ld(a,c)))=mult(b,mult(b,c))),inference(rw,[status(thm)],[247680,382973,theory(equality)])).
% cnf(394269,negated_conjecture,(mult(mult(b,mult(b,c)),a)=mult(b,mult(a,mult(mult(b,ld(a,c)),a)))),inference(spm,[status(thm)],[243327,394052,theory(equality)])).
% cnf(394571,negated_conjecture,(mult(b,mult(c,mult(a,b)))=mult(b,mult(a,mult(mult(b,ld(a,c)),a)))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[394269,109603,theory(equality)]),243055,theory(equality)])).
% cnf(394572,negated_conjecture,(mult(b,mult(c,mult(a,b)))=mult(b,mult(mult(a,b),c))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[394571,1083,theory(equality)]),243760,theory(equality)]),197134,theory(equality)]),340723,theory(equality)])).
% cnf(394575,negated_conjecture,(ld(b,mult(b,mult(c,mult(a,b))))=mult(mult(a,b),c)),inference(spm,[status(thm)],[15,394572,theory(equality)])).
% cnf(394762,negated_conjecture,(mult(c,mult(a,b))=mult(mult(a,b),c)),inference(rw,[status(thm)],[394575,15,theory(equality)])).
% cnf(394869,negated_conjecture,(rd(mult(c,mult(a,b)),c)=mult(a,b)),inference(spm,[status(thm)],[19,394762,theory(equality)])).
% cnf(394877,negated_conjecture,(mult(mult(c,mult(a,b)),c)=mult(mult(a,b),mult(c,c))),inference(spm,[status(thm)],[57,394762,theory(equality)])).
% cnf(395065,negated_conjecture,(mult(mult(c,mult(a,b)),a)=mult(b,mult(a,mult(c,a)))),inference(spm,[status(thm)],[243327,394762,theory(equality)])).
% cnf(395083,negated_conjecture,(mult(c,mult(a,b))!=mult(a,mult(b,c))),inference(rw,[status(thm)],[32,394762,theory(equality)])).
% cnf(395085,negated_conjecture,(mult(c,rd(mult(a,b),c))=mult(a,b)),inference(rw,[status(thm)],[394869,98492,theory(equality)])).
% cnf(395086,negated_conjecture,(mult(c,mult(c,mult(a,b)))=mult(mult(a,b),mult(c,c))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[394877,85087,theory(equality)]),394762,theory(equality)])).
% cnf(395160,negated_conjecture,(mult(mult(c,mult(a,b)),a)=mult(b,mult(a,mult(a,c)))),inference(rw,[status(thm)],[395065,197134,theory(equality)])).
% cnf(395473,negated_conjecture,(ld(c,mult(a,b))=rd(mult(a,b),c)),inference(spm,[status(thm)],[15,395085,theory(equality)])).
% cnf(398630,negated_conjecture,(mult(c,mult(c,mult(a,b)))=mult(a,mult(c,mult(b,c)))|mult(mult(a,b),c)=mult(a,mult(b,c))),inference(spm,[status(thm)],[86072,395086,theory(equality)])).
% cnf(398955,negated_conjecture,(mult(c,mult(c,mult(a,b)))=mult(a,mult(b,mult(c,c)))|mult(mult(a,b),c)=mult(a,mult(b,c))),inference(rw,[status(thm)],[398630,18994,theory(equality)])).
% cnf(398956,negated_conjecture,(mult(c,mult(c,mult(a,b)))=mult(a,mult(b,mult(c,c)))|mult(c,mult(a,b))=mult(a,mult(b,c))),inference(rw,[status(thm)],[398955,394762,theory(equality)])).
% cnf(398957,negated_conjecture,(mult(c,mult(c,mult(a,b)))=mult(a,mult(b,mult(c,c)))),inference(sr,[status(thm)],[398956,395083,theory(equality)])).
% cnf(399782,negated_conjecture,(rd(mult(a,mult(b,mult(c,c))),c)=mult(c,rd(mult(c,mult(a,b)),c))),inference(spm,[status(thm)],[98492,398957,theory(equality)])).
% cnf(399947,negated_conjecture,(mult(mult(a,c),b)=mult(c,rd(mult(c,mult(a,b)),c))),inference(rw,[status(thm)],[399782,453,theory(equality)])).
% cnf(399948,negated_conjecture,(mult(mult(a,c),b)=mult(c,mult(a,b))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[399947,98492,theory(equality)]),395473,theory(equality)]),13,theory(equality)])).
% cnf(400056,negated_conjecture,(rd(mult(c,mult(a,b)),b)=mult(a,c)),inference(spm,[status(thm)],[19,399948,theory(equality)])).
% cnf(400300,negated_conjecture,(mult(b,mult(ld(b,c),a))=mult(a,c)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[400056,434,theory(equality)]),144,theory(equality)]),120954,theory(equality)])).
% cnf(401718,negated_conjecture,(rd(mult(a,c),mult(ld(b,c),a))=b),inference(spm,[status(thm)],[19,400300,theory(equality)])).
% cnf(401881,negated_conjecture,(rd(mult(a,c),a)=mult(mult(b,a),ld(a,ld(b,c)))),inference(spm,[status(thm)],[434,400300,theory(equality)])).
% cnf(401972,negated_conjecture,(c=mult(mult(b,a),ld(a,ld(b,c)))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[401881,98492,theory(equality)]),199179,theory(equality)]),13,theory(equality)])).
% cnf(401973,negated_conjecture,(c=mult(mult(a,b),ld(a,ld(b,c)))),inference(rw,[status(thm)],[401972,243055,theory(equality)])).
% cnf(404966,negated_conjecture,(mult(b,a)=mult(c,mult(a,ld(mult(ld(b,c),a),a)))),inference(spm,[status(thm)],[197464,401718,theory(equality)])).
% cnf(405003,negated_conjecture,(mult(a,b)=mult(c,mult(a,ld(mult(ld(b,c),a),a)))),inference(rw,[status(thm)],[404966,243055,theory(equality)])).
% cnf(405004,negated_conjecture,(mult(a,b)=mult(c,mult(ld(c,b),a))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[405003,100816,theory(equality)]),91904,theory(equality)])).
% cnf(405006,negated_conjecture,(ld(mult(a,b),c)=ld(a,ld(b,c))),inference(spm,[status(thm)],[15,401973,theory(equality)])).
% cnf(405801,negated_conjecture,(mult(mult(a,b),c)=mult(c,mult(mult(ld(c,b),a),c))),inference(spm,[status(thm)],[85087,405004,theory(equality)])).
% cnf(405959,negated_conjecture,(mult(c,mult(a,b))=mult(c,mult(mult(ld(c,b),a),c))),inference(rw,[status(thm)],[405801,394762,theory(equality)])).
% cnf(405960,negated_conjecture,(mult(c,mult(a,b))=mult(b,mult(a,c))),inference(rw,[status(thm)],[405959,131462,theory(equality)])).
% cnf(406224,negated_conjecture,(mult(mult(b,mult(a,c)),a)=mult(b,mult(a,mult(a,c)))),inference(rw,[status(thm)],[395160,405960,theory(equality)])).
% cnf(406227,negated_conjecture,(mult(b,mult(a,c))!=mult(a,mult(b,c))),inference(rw,[status(thm)],[395083,405960,theory(equality)])).
% cnf(412612,negated_conjecture,(mult(a,ld(mult(a,b),c))=ld(b,c)),inference(spm,[status(thm)],[13,405006,theory(equality)])).
% cnf(412834,negated_conjecture,(mult(ld(b,c),mult(a,b))=mult(rd(a,mult(a,b)),mult(c,mult(a,b)))),inference(spm,[status(thm)],[1083,412612,theory(equality)])).
% cnf(412890,negated_conjecture,(mult(ld(b,c),mult(a,b))=mult(a,c)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[412834,243441,theory(equality)]),405960,theory(equality)]),89382,theory(equality)]),15,theory(equality)])).
% cnf(413087,negated_conjecture,(mult(b,mult(a,c))=mult(mult(b,c),a)),inference(rw,[status(thm)],[243454,412890,theory(equality)])).
% cnf(413263,negated_conjecture,(rd(mult(b,mult(a,c)),a)=mult(b,c)),inference(spm,[status(thm)],[19,413087,theory(equality)])).
% cnf(413494,negated_conjecture,(mult(mult(a,b),ld(a,c))=mult(b,c)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[413263,197487,theory(equality)]),243055,theory(equality)])).
% cnf(417919,negated_conjecture,(mult(mult(b,a),mult(a,c))=mult(b,mult(a,mult(a,c)))),inference(spm,[status(thm)],[83,406224,theory(equality)])).
% cnf(418004,negated_conjecture,(mult(a,mult(b,mult(a,c)))=mult(b,mult(a,mult(a,c)))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[417919,243055,theory(equality)]),310363,theory(equality)]),413087,theory(equality)])).
% cnf(418591,negated_conjecture,(rd(mult(a,mult(b,mult(a,c))),a)=mult(mult(b,a),c)),inference(spm,[status(thm)],[197499,418004,theory(equality)])).
% cnf(418696,negated_conjecture,(mult(a,mult(b,c))=mult(mult(b,a),c)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[418591,98492,theory(equality)]),197487,theory(equality)]),243055,theory(equality)]),413494,theory(equality)])).
% cnf(418697,negated_conjecture,(mult(a,mult(b,c))=mult(b,mult(a,c))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[418696,243055,theory(equality)]),394762,theory(equality)]),405960,theory(equality)])).
% cnf(418698,negated_conjecture,($false),inference(sr,[status(thm)],[418697,406227,theory(equality)])).
% cnf(418699,negated_conjecture,($false),418698,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 2251
% # ...of these trivial : 941
% # ...subsumed : 170
% # ...remaining for further processing: 1140
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 8
% # Backward-rewritten : 467
% # Generated clauses : 223256
% # ...of the previous two non-trivial : 194191
% # Contextual simplify-reflections : 3
% # Paramodulations : 223200
% # Factorizations : 56
% # Equation resolutions : 0
% # Current number of processed clauses: 665
% # Positive orientable unit clauses: 490
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 1
% # Non-unit-clauses : 174
% # Current number of unprocessed clauses: 129482
% # ...number of literals in the above : 280053
% # Clause-clause subsumption calls (NU) : 9029
% # Rec. Clause-clause subsumption calls : 7368
% # Unit Clause-clause subsumption calls : 15151
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 2292
% # Indexed BW rewrite successes : 337
% # Backwards rewriting index: 600 leaves, 1.69+/-2.215 terms/leaf
% # Paramod-from index: 413 leaves, 1.46+/-1.312 terms/leaf
% # Paramod-into index: 538 leaves, 1.64+/-1.924 terms/leaf
% # -------------------------------------------------
% # User time : 8.609 s
% # System time : 0.329 s
% # Total time : 8.938 s
% # Maximum resident set size: 0 pages
% PrfWatch: 15.99 CPU 16.21 WC
% FINAL PrfWatch: 15.99 CPU 16.21 WC
% SZS output end Solution for /tmp/SystemOnTPTP6077/GRP746+1.tptp
%
%------------------------------------------------------------------------------