%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : GRP745+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 : art09.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:03 EST 2010
% Result : Theorem 19.39s
% Output : Solution 19.39s
% 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/SystemOnTPTP23267/GRP745+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% found
% SZS status THM for /tmp/SystemOnTPTP23267/GRP745+1.tptp
% SZS output start Solution for /tmp/SystemOnTPTP23267/GRP745+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 23363
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.00 WC
% PrfWatch: 1.91 CPU 2.01 WC
% PrfWatch: 3.52 CPU 4.01 WC
% PrfWatch: 5.17 CPU 6.02 WC
% PrfWatch: 7.16 CPU 8.02 WC
% PrfWatch: 9.16 CPU 10.03 WC
% PrfWatch: 11.13 CPU 12.03 WC
% # Preprocessing time : 0.011 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% PrfWatch: 13.12 CPU 14.04 WC
% PrfWatch: 15.12 CPU 16.04 WC
% PrfWatch: 17.11 CPU 18.05 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(X4,mult(X6,X5))&mult(mult(X4,X6),X5)=mult(X4,mult(X5,X6)))),file('/tmp/SRASS.s.p', f08)).
% fof(9, conjecture,mult(a,mult(b,mult(c,a)))=mult(mult(mult(a,b),c),a),file('/tmp/SRASS.s.p', goals)).
% fof(10, negated_conjecture,~(mult(a,mult(b,mult(c,a)))=mult(mult(mult(a,b),c),a)),inference(assume_negation,[status(cth)],[9])).
% fof(11, negated_conjecture,~(mult(a,mult(b,mult(c,a)))=mult(mult(mult(a,b),c),a)),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(X7,mult(X9,X8))&mult(mult(X7,X9),X8)=mult(X7,mult(X8,X9)))),inference(variable_rename,[status(thm)],[8])).
% fof(27, plain,![X7]:![X8]:![X9]:(((mult(mult(X7,X8),X9)=mult(X7,mult(X9,X8))|mult(mult(X7,X8),X9)=mult(X7,mult(X8,X9)))&(mult(mult(X7,X9),X8)=mult(X7,mult(X8,X9))|mult(mult(X7,X8),X9)=mult(X7,mult(X8,X9))))&((mult(mult(X7,X8),X9)=mult(X7,mult(X9,X8))|mult(mult(X7,X9),X8)=mult(X7,mult(X9,X8)))&(mult(mult(X7,X9),X8)=mult(X7,mult(X8,X9))|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(mult(X1,X2),X3)=mult(X1,mult(X3,X2))),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(X1,mult(X2,X3))),inference(split_conjunct,[status(thm)],[27])).
% cnf(32,negated_conjecture,(mult(a,mult(b,mult(c,a)))!=mult(mult(mult(a,b),c),a)),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(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(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(61,plain,(ld(mult(X1,X2),mult(X1,mult(X3,X2)))=X3|mult(mult(X1,X3),X2)=mult(X1,mult(X3,X2))),inference(spm,[status(thm)],[15,29,theory(equality)])).
% cnf(62,plain,(rd(mult(X1,mult(X3,X2)),X3)=mult(X1,X2)|mult(mult(X1,X3),X2)=mult(X1,mult(X3,X2))),inference(spm,[status(thm)],[19,29,theory(equality)])).
% cnf(76,negated_conjecture,(mult(mult(mult(a,b),a),c)=mult(mult(a,b),mult(c,a))|mult(mult(a,b),mult(c,a))!=mult(a,mult(b,mult(c,a)))),inference(spm,[status(thm)],[32,29,theory(equality)])).
% cnf(112,plain,(mult(mult(X4,X5),X6)=mult(X4,mult(X6,X5))|mult(X4,mult(X5,X6))!=mult(X4,mult(X6,X5))),inference(ef,[status(thm)],[28,theory(equality)])).
% cnf(113,plain,(mult(mult(X7,X8),X9)=mult(X7,mult(X8,X9))|mult(X7,mult(X9,X8))!=mult(X7,mult(X8,X9))),inference(ef,[status(thm)],[28,theory(equality)])).
% cnf(115,plain,(mult(X1,mult(ld(mult(X1,X2),X3),X2))=X3|mult(mult(X1,X2),ld(mult(X1,X2),X3))=mult(X1,mult(X2,ld(mult(X1,X2),X3)))),inference(spm,[status(thm)],[13,28,theory(equality)])).
% cnf(123,plain,(mult(mult(X1,X2),mult(X2,X3))=mult(X1,mult(mult(X2,X3),X2))|mult(mult(mult(X1,X2),X3),X2)=mult(mult(X1,X2),mult(X3,X2))),inference(spm,[status(thm)],[25,28,theory(equality)])).
% cnf(127,plain,(ld(mult(X1,X2),mult(X1,mult(X2,X3)))=X3|mult(mult(X1,X2),X3)=mult(X1,mult(X3,X2))),inference(spm,[status(thm)],[15,28,theory(equality)])).
% cnf(138,plain,(mult(X1,X3)=mult(rd(X1,X2),mult(X2,X3))|mult(X1,X3)=mult(rd(X1,X2),mult(X3,X2))),inference(spm,[status(thm)],[28,17,theory(equality)])).
% cnf(155,plain,(mult(X1,mult(ld(mult(X1,X2),X3),X2))=X3|X3=mult(X1,mult(X2,ld(mult(X1,X2),X3)))),inference(rw,[status(thm)],[115,13,theory(equality)])).
% cnf(156,plain,(mult(mult(X1,X2),mult(X2,X3))=mult(X1,mult(mult(X2,X3),X2))|mult(X1,mult(mult(X2,X3),X2))=mult(mult(X1,X2),mult(X3,X2))),inference(rw,[status(thm)],[123,25,theory(equality)])).
% cnf(254,plain,(mult(mult(X1,mult(X2,X3)),X3)=mult(mult(X1,X2),mult(X3,X3))|mult(mult(X1,X3),X2)=mult(X1,mult(X2,X3))),inference(spm,[status(thm)],[57,29,theory(equality)])).
% cnf(412,plain,(rd(mult(X1,mult(X3,X2)),X2)=mult(mult(X1,X2),ld(X2,X3))),inference(spm,[status(thm)],[43,13,theory(equality)])).
% cnf(881,plain,(ld(rd(X1,X2),mult(mult(X1,X3),X2))=mult(mult(X2,X3),X2)),inference(spm,[status(thm)],[15,47,theory(equality)])).
% cnf(918,plain,(mult(rd(X1,X2),mult(X3,X2))=mult(mult(X1,ld(X2,X3)),X2)),inference(spm,[status(thm)],[47,13,theory(equality)])).
% cnf(1392,plain,(ld(X1,mult(X3,X2))=mult(mult(X2,ld(mult(X1,X2),X3)),X2)),inference(spm,[status(thm)],[15,51,theory(equality)])).
% cnf(2315,plain,(rd(mult(X1,X2),X2)=mult(mult(X1,X2),ld(X2,unit))),inference(spm,[status(thm)],[412,23,theory(equality)])).
% cnf(2377,plain,(X1=mult(mult(X1,X2),ld(X2,unit))),inference(rw,[status(thm)],[2315,19,theory(equality)])).
% cnf(2395,plain,(ld(mult(X1,X2),X1)=ld(X2,unit)),inference(spm,[status(thm)],[15,2377,theory(equality)])).
% cnf(2433,plain,(mult(mult(X1,rd(unit,X2)),X2)=X1),inference(spm,[status(thm)],[2377,37,theory(equality)])).
% cnf(2440,plain,(mult(X1,ld(X2,unit))=rd(X1,X2)),inference(spm,[status(thm)],[2377,17,theory(equality)])).
% cnf(2496,plain,(rd(X1,ld(X2,unit))=mult(X1,X2)),inference(spm,[status(thm)],[40,2395,theory(equality)])).
% cnf(2502,plain,(ld(X1,rd(X1,X2))=ld(X2,unit)),inference(spm,[status(thm)],[2395,17,theory(equality)])).
% cnf(2504,negated_conjecture,(ld(mult(mult(a,b),mult(c,a)),mult(mult(a,b),a))=ld(c,unit)|mult(mult(a,b),mult(c,a))!=mult(a,mult(b,mult(c,a)))),inference(spm,[status(thm)],[2395,76,theory(equality)])).
% cnf(2530,plain,(ld(X2,X1)=ld(ld(X1,X2),unit)),inference(spm,[status(thm)],[2395,13,theory(equality)])).
% cnf(2792,plain,(ld(X1,mult(X1,rd(unit,X2)))=ld(X2,unit)),inference(spm,[status(thm)],[2395,2433,theory(equality)])).
% cnf(2843,plain,(rd(unit,X2)=ld(X2,unit)),inference(rw,[status(thm)],[2792,15,theory(equality)])).
% cnf(2868,plain,(mult(ld(X1,unit),X1)=unit),inference(spm,[status(thm)],[17,2843,theory(equality)])).
% cnf(2870,plain,(mult(ld(X1,unit),mult(mult(X1,X2),X1))=mult(mult(unit,X2),X1)),inference(spm,[status(thm)],[47,2843,theory(equality)])).
% cnf(2883,plain,(mult(ld(X1,unit),mult(mult(X1,X2),X1))=mult(X2,X1)),inference(rw,[status(thm)],[2870,23,theory(equality)])).
% cnf(3712,plain,(mult(rd(mult(X1,X2),X3),X2)=mult(X1,mult(mult(X2,ld(X3,unit)),X2))),inference(spm,[status(thm)],[25,2440,theory(equality)])).
% cnf(3762,plain,(mult(X1,mult(rd(X2,mult(X1,X2)),X2))=mult(unit,X2)),inference(spm,[status(thm)],[51,2440,theory(equality)])).
% cnf(3803,plain,(mult(rd(mult(X1,X2),X3),X2)=mult(X1,mult(rd(X2,X3),X2))),inference(rw,[status(thm)],[3712,2440,theory(equality)])).
% cnf(3871,plain,(mult(X1,mult(rd(X2,mult(X1,X2)),X2))=X2),inference(rw,[status(thm)],[3762,23,theory(equality)])).
% cnf(4910,plain,(rd(X1,ld(X3,X2))=mult(X1,ld(X2,X3))),inference(spm,[status(thm)],[2496,2530,theory(equality)])).
% cnf(5185,plain,(ld(X1,X2)=mult(rd(X2,mult(X1,X2)),X2)),inference(spm,[status(thm)],[15,3871,theory(equality)])).
% cnf(5709,plain,(rd(ld(X2,X1),X1)=rd(X1,mult(X2,X1))),inference(spm,[status(thm)],[19,5185,theory(equality)])).
% cnf(5736,plain,(rd(mult(X1,ld(X3,X2)),X2)=mult(mult(X1,X2),ld(X2,rd(X2,mult(X3,X2))))),inference(spm,[status(thm)],[412,5185,theory(equality)])).
% cnf(5746,plain,(mult(rd(X1,X2),X1)=ld(rd(X2,X1),X1)),inference(spm,[status(thm)],[5185,17,theory(equality)])).
% cnf(5802,plain,(rd(mult(X1,ld(X3,X2)),X2)=rd(mult(X1,X2),mult(X3,X2))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[5736,2502,theory(equality)]),2440,theory(equality)])).
% cnf(6339,plain,(rd(X2,X1)=rd(X1,mult(rd(X1,X2),X1))),inference(spm,[status(thm)],[5709,37,theory(equality)])).
% cnf(6377,plain,(mult(rd(X1,X2),mult(rd(X2,X1),X2))=X2),inference(spm,[status(thm)],[13,5746,theory(equality)])).
% cnf(7039,plain,(mult(rd(X1,mult(X2,X1)),mult(X2,mult(X2,X1)))=mult(X2,X1)),inference(spm,[status(thm)],[6377,19,theory(equality)])).
% cnf(8490,plain,(mult(ld(X1,unit),mult(X2,X1))=mult(ld(X1,X2),X1)),inference(spm,[status(thm)],[2883,13,theory(equality)])).
% cnf(9338,plain,(rd(mult(ld(X1,X2),X1),mult(X2,X1))=ld(X1,unit)),inference(spm,[status(thm)],[19,8490,theory(equality)])).
% cnf(9405,plain,(mult(ld(X1,unit),X2)=mult(ld(X1,rd(X2,X1)),X1)),inference(spm,[status(thm)],[8490,17,theory(equality)])).
% cnf(9465,plain,(mult(ld(ld(X1,unit),unit),rd(X2,X1))=mult(ld(ld(X1,unit),X2),ld(X1,unit))),inference(spm,[status(thm)],[8490,2440,theory(equality)])).
% cnf(9566,plain,(mult(X1,rd(X2,X1))=mult(ld(ld(X1,unit),X2),ld(X1,unit))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[9465,2530,theory(equality)]),33,theory(equality)])).
% cnf(9567,plain,(mult(X1,rd(X2,X1))=rd(ld(ld(X1,unit),X2),X1)),inference(rw,[status(thm)],[9566,2440,theory(equality)])).
% cnf(14744,plain,(X2=mult(ld(X1,ld(mult(ld(X1,unit),X1),X2)),X1)|mult(ld(X1,unit),mult(X1,ld(mult(ld(X1,unit),X1),X2)))=X2),inference(spm,[status(thm)],[8490,155,theory(equality)])).
% cnf(14912,plain,(X2=mult(ld(X1,X2),X1)|mult(ld(X1,unit),mult(X1,ld(mult(ld(X1,unit),X1),X2)))=X2),inference(rw,[status(thm)],[inference(rw,[status(thm)],[14744,2868,theory(equality)]),33,theory(equality)])).
% cnf(14913,plain,(X2=mult(ld(X1,X2),X1)|mult(ld(X1,unit),mult(X1,X2))=X2),inference(rw,[status(thm)],[inference(rw,[status(thm)],[14912,2868,theory(equality)]),33,theory(equality)])).
% cnf(14986,plain,(rd(X2,mult(X1,X2))=ld(X1,unit)|mult(ld(X1,X2),X1)=X2),inference(spm,[status(thm)],[19,14913,theory(equality)])).
% cnf(24687,plain,(mult(rd(mult(X1,X2),X2),mult(ld(X1,unit),X2))=X2|mult(ld(X1,X2),X1)=X2),inference(spm,[status(thm)],[7039,14913,theory(equality)])).
% cnf(24881,plain,(mult(X1,mult(ld(X1,unit),X2))=X2|mult(ld(X1,X2),X1)=X2),inference(rw,[status(thm)],[24687,19,theory(equality)])).
% cnf(26213,plain,(mult(mult(X1,ld(unit,X2)),X1)=ld(ld(X1,unit),mult(X2,X1))),inference(spm,[status(thm)],[1392,2868,theory(equality)])).
% cnf(26329,plain,(mult(mult(X1,X2),X1)=ld(ld(X1,unit),mult(X2,X1))),inference(rw,[status(thm)],[26213,33,theory(equality)])).
% cnf(27329,plain,(ld(ld(X1,unit),X2)=mult(mult(X1,rd(X2,X1)),X1)),inference(spm,[status(thm)],[26329,17,theory(equality)])).
% cnf(31908,plain,(ld(X1,X2)=mult(ld(X1,unit),X2)|mult(ld(X1,X2),X1)=X2),inference(spm,[status(thm)],[15,24881,theory(equality)])).
% cnf(39962,plain,(mult(ld(ld(X1,unit),unit),mult(X2,X1))=mult(mult(X1,X2),X1)|mult(mult(mult(X1,X2),X1),ld(X1,unit))=mult(X2,X1)),inference(spm,[status(thm)],[31908,26329,theory(equality)])).
% cnf(40212,plain,(mult(X1,mult(X2,X1))=mult(mult(X1,X2),X1)|mult(mult(mult(X1,X2),X1),ld(X1,unit))=mult(X2,X1)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[39962,2530,theory(equality)]),33,theory(equality)])).
% cnf(40213,plain,(mult(X1,mult(X2,X1))=mult(mult(X1,X2),X1)|mult(X1,X2)=mult(X2,X1)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[40212,2440,theory(equality)]),19,theory(equality)])).
% cnf(40284,plain,(rd(mult(X1,mult(X2,X1)),X1)=mult(X1,X2)|mult(X1,X2)=mult(X2,X1)),inference(spm,[status(thm)],[19,40213,theory(equality)])).
% cnf(40440,plain,(mult(X1,mult(ld(X1,X2),X1))=mult(rd(X1,X1),mult(X2,X1))|mult(X1,ld(X1,X2))=mult(ld(X1,X2),X1)),inference(spm,[status(thm)],[918,40213,theory(equality)])).
% cnf(40676,plain,(mult(mult(X1,X1),ld(X1,X2))=mult(X1,X2)|mult(X1,X2)=mult(X2,X1)),inference(rw,[status(thm)],[40284,412,theory(equality)])).
% cnf(40713,plain,(mult(X1,mult(ld(X1,X2),X1))=mult(X2,X1)|mult(X1,ld(X1,X2))=mult(ld(X1,X2),X1)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[40440,38,theory(equality)]),23,theory(equality)])).
% cnf(40714,plain,(mult(X1,mult(ld(X1,X2),X1))=mult(X2,X1)|X2=mult(ld(X1,X2),X1)),inference(rw,[status(thm)],[40713,13,theory(equality)])).
% cnf(46935,plain,(rd(mult(X2,X1),mult(mult(X1,X2),X1))=ld(X1,unit)),inference(spm,[status(thm)],[9338,15,theory(equality)])).
% cnf(48113,plain,(ld(mult(X1,rd(X2,X1)),ld(ld(X1,unit),X2))=X1),inference(spm,[status(thm)],[37,9567,theory(equality)])).
% cnf(73497,plain,(rd(mult(X1,X2),X2)=rd(mult(mult(X1,X1),X2),mult(X1,X2))|mult(X1,X2)=mult(X2,X1)),inference(spm,[status(thm)],[5802,40676,theory(equality)])).
% cnf(73583,plain,(X1=rd(mult(mult(X1,X1),X2),mult(X1,X2))|mult(X1,X2)=mult(X2,X1)),inference(rw,[status(thm)],[73497,19,theory(equality)])).
% cnf(73599,plain,(ld(X1,mult(mult(X1,X1),X2))=mult(X1,X2)|mult(X1,X2)=mult(X2,X1)),inference(spm,[status(thm)],[37,73583,theory(equality)])).
% cnf(75793,plain,(ld(X1,mult(X1,mult(X2,X1)))=mult(X1,X2)|mult(X1,X2)=mult(X2,X1)|mult(X1,mult(X1,X2))!=mult(X1,mult(X2,X1))),inference(spm,[status(thm)],[73599,112,theory(equality)])).
% cnf(76050,plain,(mult(X2,X1)=mult(X1,X2)|mult(X1,X2)=mult(X2,X1)|mult(X1,mult(X1,X2))!=mult(X1,mult(X2,X1))),inference(rw,[status(thm)],[75793,15,theory(equality)])).
% cnf(76051,plain,(mult(X2,X1)=mult(X1,X2)|mult(X1,mult(X1,X2))!=mult(X1,mult(X2,X1))),inference(cn,[status(thm)],[76050,theory(equality)])).
% cnf(77723,plain,(mult(ld(X1,X2),X1)=mult(X1,ld(X1,X2))|mult(ld(X1,X2),X1)=X2|mult(X1,mult(X1,ld(X1,X2)))!=mult(X2,X1)),inference(spm,[status(thm)],[76051,40714,theory(equality)])).
% cnf(78008,plain,(mult(ld(X1,X2),X1)=X2|mult(ld(X1,X2),X1)=X2|mult(X1,mult(X1,ld(X1,X2)))!=mult(X2,X1)),inference(rw,[status(thm)],[77723,13,theory(equality)])).
% cnf(78009,plain,(mult(ld(X1,X2),X1)=X2|mult(ld(X1,X2),X1)=X2|mult(X1,X2)!=mult(X2,X1)),inference(rw,[status(thm)],[78008,13,theory(equality)])).
% cnf(78010,plain,(mult(ld(X1,X2),X1)=X2|mult(X1,X2)!=mult(X2,X1)),inference(cn,[status(thm)],[78009,theory(equality)])).
% cnf(78189,plain,(rd(X2,X1)=ld(X1,X2)|mult(X1,X2)!=mult(X2,X1)),inference(spm,[status(thm)],[19,78010,theory(equality)])).
% cnf(78234,plain,(rd(X2,mult(mult(X1,ld(X1,X2)),X1))=ld(X1,unit)|mult(X1,X2)!=mult(X2,X1)),inference(spm,[status(thm)],[46935,78010,theory(equality)])).
% cnf(78393,plain,(mult(mult(mult(X1,X2),X1),ld(X1,unit))=mult(X2,X1)|mult(ld(X1,unit),mult(X2,X1))!=mult(mult(X2,X1),ld(X1,unit))),inference(spm,[status(thm)],[78010,26329,theory(equality)])).
% cnf(78427,plain,(rd(X2,mult(X2,X1))=ld(X1,unit)|mult(X1,X2)!=mult(X2,X1)),inference(rw,[status(thm)],[78234,13,theory(equality)])).
% cnf(78565,plain,(mult(X1,X2)=mult(X2,X1)|mult(ld(X1,unit),mult(X2,X1))!=mult(mult(X2,X1),ld(X1,unit))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[78393,2440,theory(equality)]),19,theory(equality)])).
% cnf(78566,plain,(mult(X1,X2)=mult(X2,X1)|mult(ld(X1,X2),X1)!=mult(mult(X2,X1),ld(X1,unit))),inference(rw,[status(thm)],[78565,8490,theory(equality)])).
% cnf(78567,plain,(mult(X1,X2)=mult(X2,X1)|mult(ld(X1,X2),X1)!=X2),inference(rw,[status(thm)],[inference(rw,[status(thm)],[78566,2440,theory(equality)]),19,theory(equality)])).
% cnf(79591,plain,(ld(X2,mult(X1,X2))=X1|mult(X2,mult(X1,X2))!=mult(mult(X1,X2),X2)),inference(spm,[status(thm)],[19,78189,theory(equality)])).
% cnf(79662,plain,(ld(X2,mult(X1,X2))=X1|mult(X2,mult(X1,X2))!=mult(X1,mult(X2,X2))),inference(rw,[status(thm)],[79591,57,theory(equality)])).
% cnf(89136,plain,(rd(ld(X1,X2),X2)=ld(X1,unit)|rd(X2,mult(X1,X2))=ld(X1,unit)|mult(X1,ld(X1,X2))!=X2),inference(spm,[status(thm)],[78427,14986,theory(equality)])).
% cnf(89255,plain,(rd(X2,mult(X1,X2))=ld(X1,unit)|rd(X2,mult(X1,X2))=ld(X1,unit)|mult(X1,ld(X1,X2))!=X2),inference(rw,[status(thm)],[89136,5709,theory(equality)])).
% cnf(89256,plain,(rd(X2,mult(X1,X2))=ld(X1,unit)|rd(X2,mult(X1,X2))=ld(X1,unit)|$false),inference(rw,[status(thm)],[89255,13,theory(equality)])).
% cnf(89257,plain,(rd(X2,mult(X1,X2))=ld(X1,unit)),inference(cn,[status(thm)],[89256,theory(equality)])).
% cnf(89278,plain,(mult(ld(X2,unit),mult(X2,X1))=X1),inference(spm,[status(thm)],[17,89257,theory(equality)])).
% cnf(89522,plain,(mult(ld(X2,unit),X1)=ld(X2,X1)),inference(rw,[status(thm)],[5185,89257,theory(equality)])).
% cnf(89524,plain,(rd(ld(X1,X2),X2)=ld(X1,unit)),inference(rw,[status(thm)],[5709,89257,theory(equality)])).
% cnf(89528,plain,(ld(rd(X1,X2),unit)=rd(X2,X1)),inference(rw,[status(thm)],[6339,89257,theory(equality)])).
% cnf(90954,plain,(mult(ld(ld(X1,unit),unit),mult(ld(X1,X2),X1))=mult(X2,X1)),inference(spm,[status(thm)],[89278,8490,theory(equality)])).
% cnf(91298,plain,(mult(X1,mult(ld(X1,X2),X1))=mult(X2,X1)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[90954,2530,theory(equality)]),33,theory(equality)])).
% cnf(92786,plain,(ld(X1,mult(X2,X1))=mult(ld(X1,X2),X1)),inference(spm,[status(thm)],[15,91298,theory(equality)])).
% cnf(92787,plain,(rd(mult(X2,X1),mult(ld(X1,X2),X1))=X1),inference(spm,[status(thm)],[19,91298,theory(equality)])).
% cnf(93044,plain,(mult(X1,mult(X2,X1))=mult(mult(X1,X2),X1)),inference(spm,[status(thm)],[91298,15,theory(equality)])).
% cnf(93606,plain,(mult(ld(X1,rd(X2,X1)),X1)=ld(X1,X2)),inference(rw,[status(thm)],[9405,89522,theory(equality)])).
% cnf(95078,plain,(rd(mult(X1,mult(X2,X1)),X1)=mult(X1,X2)),inference(spm,[status(thm)],[19,93044,theory(equality)])).
% cnf(95148,plain,(rd(mult(X1,mult(X2,mult(X3,X2))),X2)=mult(mult(X1,X2),ld(X2,mult(X2,X3)))),inference(spm,[status(thm)],[412,93044,theory(equality)])).
% cnf(95334,plain,(mult(rd(X1,X2),X1)=mult(X1,mult(ld(X2,unit),X1))),inference(spm,[status(thm)],[93044,2440,theory(equality)])).
% cnf(95346,plain,(ld(rd(X1,X2),mult(mult(X1,X3),X2))=mult(X2,mult(X3,X2))),inference(rw,[status(thm)],[881,93044,theory(equality)])).
% cnf(95355,plain,(mult(mult(X1,X2),mult(X3,X2))=mult(X1,mult(X2,mult(X3,X2)))|mult(mult(X1,X2),mult(X2,X3))=mult(X1,mult(mult(X2,X3),X2))),inference(rw,[status(thm)],[156,93044,theory(equality)])).
% cnf(95356,plain,(mult(mult(X1,X2),mult(X3,X2))=mult(X1,mult(X2,mult(X3,X2)))|mult(mult(X1,X2),mult(X2,X3))=mult(X1,mult(X2,mult(X3,X2)))),inference(rw,[status(thm)],[95355,93044,theory(equality)])).
% cnf(95362,plain,(mult(rd(X1,X2),mult(X2,mult(X3,X2)))=mult(mult(X1,X3),X2)),inference(rw,[status(thm)],[47,93044,theory(equality)])).
% cnf(95372,plain,(ld(ld(X1,unit),X2)=mult(X1,X2)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[27329,93044,theory(equality)]),17,theory(equality)])).
% cnf(95405,negated_conjecture,(ld(mult(mult(a,b),mult(c,a)),mult(a,mult(b,a)))=ld(c,unit)|mult(mult(a,b),mult(c,a))!=mult(a,mult(b,mult(c,a)))),inference(rw,[status(thm)],[2504,93044,theory(equality)])).
% cnf(95436,negated_conjecture,(mult(mult(a,mult(b,a)),c)=mult(mult(a,b),mult(c,a))|mult(mult(a,b),mult(c,a))!=mult(a,mult(b,mult(c,a)))),inference(rw,[status(thm)],[76,93044,theory(equality)])).
% cnf(95530,plain,(mult(mult(X1,X1),ld(X1,X2))=mult(X1,X2)),inference(rw,[status(thm)],[95078,412,theory(equality)])).
% cnf(95533,plain,(rd(mult(X1,mult(X2,mult(X3,X2))),X2)=mult(mult(X1,X2),X3)),inference(rw,[status(thm)],[95148,15,theory(equality)])).
% cnf(95601,plain,(mult(rd(X1,X2),X1)=mult(X1,ld(X2,X1))),inference(rw,[status(thm)],[95334,89522,theory(equality)])).
% cnf(95792,plain,(mult(mult(X1,X1),X2)=mult(X1,mult(X1,X2))),inference(spm,[status(thm)],[95530,15,theory(equality)])).
% cnf(98396,plain,(mult(rd(X1,X2),rd(X2,X1))=unit),inference(spm,[status(thm)],[13,89528,theory(equality)])).
% cnf(98416,plain,(rd(X1,rd(X3,X2))=mult(X1,ld(unit,rd(X2,X3)))),inference(spm,[status(thm)],[4910,89528,theory(equality)])).
% cnf(98425,plain,(mult(rd(X2,X1),X3)=ld(rd(X1,X2),X3)),inference(spm,[status(thm)],[89522,89528,theory(equality)])).
% cnf(98504,plain,(rd(X1,rd(X3,X2))=mult(X1,rd(X2,X3))),inference(rw,[status(thm)],[98416,33,theory(equality)])).
% cnf(98881,plain,(mult(ld(X1,X2),X1)=X2|mult(X1,mult(X2,X1))!=mult(X2,mult(X1,X1))),inference(spm,[status(thm)],[79662,92786,theory(equality)])).
% cnf(99210,plain,(mult(mult(X1,X2),ld(X1,unit))=X2|mult(ld(X1,unit),X2)!=mult(X2,ld(X1,unit))),inference(spm,[status(thm)],[78010,95372,theory(equality)])).
% cnf(99239,plain,(ld(mult(X1,rd(X2,X1)),mult(X1,X2))=X1),inference(rw,[status(thm)],[48113,95372,theory(equality)])).
% cnf(99240,plain,(rd(mult(X1,X2),X1)=mult(X1,rd(X2,X1))),inference(rw,[status(thm)],[9567,95372,theory(equality)])).
% cnf(99282,plain,(rd(mult(X1,X2),X1)=X2|mult(ld(X1,unit),X2)!=mult(X2,ld(X1,unit))),inference(rw,[status(thm)],[99210,2440,theory(equality)])).
% cnf(99283,plain,(rd(mult(X1,X2),X1)=X2|ld(X1,X2)!=mult(X2,ld(X1,unit))),inference(rw,[status(thm)],[99282,89522,theory(equality)])).
% cnf(99284,plain,(rd(mult(X1,X2),X1)=X2|ld(X1,X2)!=rd(X2,X1)),inference(rw,[status(thm)],[99283,2440,theory(equality)])).
% cnf(100603,plain,(mult(rd(mult(X1,X2),X3),X2)=mult(X1,mult(X2,ld(X3,X2)))),inference(rw,[status(thm)],[3803,95601,theory(equality)])).
% cnf(111554,plain,(mult(rd(X1,X2),mult(X2,X3))=mult(mult(X1,rd(X3,X2)),X2)),inference(spm,[status(thm)],[95362,17,theory(equality)])).
% cnf(111707,plain,(mult(ld(X1,unit),mult(X2,mult(X3,X2)))=mult(mult(ld(X1,X2),X3),X2)),inference(spm,[status(thm)],[95362,89524,theory(equality)])).
% cnf(111856,plain,(ld(X1,mult(X2,mult(X3,X2)))=mult(mult(ld(X1,X2),X3),X2)),inference(rw,[status(thm)],[111707,89522,theory(equality)])).
% cnf(119070,plain,(mult(mult(X1,X2),mult(X2,ld(X2,X3)))=mult(X1,mult(X2,X3))|mult(mult(X1,X2),X3)=mult(X1,mult(X2,X3))|mult(X2,X3)!=mult(X3,X2)),inference(spm,[status(thm)],[95356,78010,theory(equality)])).
% cnf(119736,plain,(mult(mult(X1,X2),X3)=mult(X1,mult(X2,X3))|mult(mult(X1,X2),X3)=mult(X1,mult(X2,X3))|mult(X2,X3)!=mult(X3,X2)),inference(rw,[status(thm)],[119070,13,theory(equality)])).
% cnf(119737,plain,(mult(mult(X1,X2),X3)=mult(X1,mult(X2,X3))|mult(X2,X3)!=mult(X3,X2)),inference(cn,[status(thm)],[119736,theory(equality)])).
% cnf(135640,plain,(mult(X1,rd(X2,X1))=X2|rd(X2,X1)!=ld(X1,X2)),inference(rw,[status(thm)],[99284,99240,theory(equality)])).
% cnf(146711,plain,(mult(rd(X2,X1),mult(mult(X1,X3),X2))=mult(X2,mult(X3,X2))),inference(rw,[status(thm)],[95346,98425,theory(equality)])).
% cnf(149931,plain,(mult(rd(X1,rd(X2,X3)),mult(X2,X1))=mult(X1,mult(X3,X1))),inference(spm,[status(thm)],[146711,17,theory(equality)])).
% cnf(150445,plain,(mult(mult(X1,rd(X3,X2)),mult(X2,X1))=mult(X1,mult(X3,X1))),inference(rw,[status(thm)],[149931,98504,theory(equality)])).
% cnf(164447,negated_conjecture,(mult(mult(a,b),mult(c,a))!=mult(a,mult(b,mult(c,a)))|mult(c,a)!=mult(a,c)),inference(spm,[status(thm)],[32,119737,theory(equality)])).
% cnf(180625,plain,(rd(mult(X1,mult(X2,X3)),X2)=mult(mult(X1,X2),rd(X3,X2))),inference(spm,[status(thm)],[95533,17,theory(equality)])).
% cnf(203257,plain,(mult(mult(X1,X2),mult(X3,X1))=mult(X1,mult(mult(X2,X3),X1))),inference(spm,[status(thm)],[150445,19,theory(equality)])).
% cnf(207002,plain,(rd(mult(X1,mult(mult(X2,X3),X1)),X1)=mult(mult(mult(X1,X2),X1),ld(X1,X3))),inference(spm,[status(thm)],[412,203257,theory(equality)])).
% cnf(207183,plain,(mult(mult(X1,X2),X3)=mult(X1,mult(mult(X2,rd(X3,X1)),X1))),inference(spm,[status(thm)],[203257,17,theory(equality)])).
% cnf(207333,plain,(mult(mult(X1,X2),ld(X1,X3))=mult(X1,mult(mult(X2,ld(X1,rd(X3,X1))),X1))),inference(spm,[status(thm)],[203257,93606,theory(equality)])).
% cnf(207573,plain,(mult(X2,mult(X3,X1))=mult(X1,mult(mult(ld(X1,X2),X3),X1))),inference(spm,[status(thm)],[203257,13,theory(equality)])).
% cnf(207591,negated_conjecture,(mult(a,mult(mult(b,c),a))!=mult(a,mult(b,mult(c,a)))|mult(c,a)!=mult(a,c)),inference(rw,[status(thm)],[164447,203257,theory(equality)])).
% cnf(207606,negated_conjecture,(ld(mult(a,mult(mult(b,c),a)),mult(a,mult(b,a)))=ld(c,unit)|mult(mult(a,b),mult(c,a))!=mult(a,mult(b,mult(c,a)))),inference(rw,[status(thm)],[95405,203257,theory(equality)])).
% cnf(207607,negated_conjecture,(ld(mult(a,mult(mult(b,c),a)),mult(a,mult(b,a)))=ld(c,unit)|mult(a,mult(mult(b,c),a))!=mult(a,mult(b,mult(c,a)))),inference(rw,[status(thm)],[207606,203257,theory(equality)])).
% cnf(207644,negated_conjecture,(mult(mult(a,mult(b,a)),c)=mult(a,mult(mult(b,c),a))|mult(mult(a,b),mult(c,a))!=mult(a,mult(b,mult(c,a)))),inference(rw,[status(thm)],[95436,203257,theory(equality)])).
% cnf(207645,negated_conjecture,(mult(mult(a,mult(b,a)),c)=mult(a,mult(mult(b,c),a))|mult(a,mult(mult(b,c),a))!=mult(a,mult(b,mult(c,a)))),inference(rw,[status(thm)],[207644,203257,theory(equality)])).
% cnf(207851,plain,(mult(X1,mult(X2,X3))=mult(mult(mult(X1,X2),X1),ld(X1,X3))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[207002,412,theory(equality)]),95792,theory(equality)]),13,theory(equality)])).
% cnf(207852,plain,(mult(X1,mult(X2,X3))=mult(mult(X1,mult(X2,X1)),ld(X1,X3))),inference(rw,[status(thm)],[207851,93044,theory(equality)])).
% cnf(208052,plain,(mult(mult(X1,X2),ld(X1,X3))=mult(X1,mult(rd(X2,X1),X3))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[207333,918,theory(equality)]),17,theory(equality)])).
% cnf(208121,negated_conjecture,(mult(c,a)!=mult(a,c)),inference(spm,[status(thm)],[207591,119737,theory(equality)])).
% cnf(211997,plain,(mult(mult(X1,mult(X2,X1)),X3)=mult(X1,mult(X2,mult(X1,X3)))),inference(spm,[status(thm)],[207852,15,theory(equality)])).
% cnf(213223,plain,(rd(mult(X1,mult(X2,mult(X1,X3))),X3)=mult(X1,mult(X2,X1))),inference(spm,[status(thm)],[19,211997,theory(equality)])).
% cnf(213572,plain,(mult(mult(X1,X2),X3)=mult(X1,mult(rd(X2,X1),mult(X1,X3)))),inference(spm,[status(thm)],[211997,17,theory(equality)])).
% cnf(214809,plain,(mult(X1,mult(X2,X1))=mult(mult(X1,rd(X2,rd(X3,X1))),X3)),inference(spm,[status(thm)],[207183,17,theory(equality)])).
% cnf(215181,plain,(mult(X1,mult(X2,X1))=mult(mult(X1,mult(X2,rd(X1,X3))),X3)),inference(rw,[status(thm)],[214809,98504,theory(equality)])).
% cnf(215366,plain,(rd(mult(X2,mult(X3,X1)),X1)=mult(X1,rd(mult(mult(ld(X1,X2),X3),X1),X1))),inference(spm,[status(thm)],[99240,207573,theory(equality)])).
% cnf(215772,plain,(mult(mult(X2,X1),ld(X1,X3))=mult(X1,rd(mult(mult(ld(X1,X2),X3),X1),X1))),inference(rw,[status(thm)],[215366,412,theory(equality)])).
% cnf(215773,plain,(mult(mult(X2,X1),ld(X1,X3))=mult(X1,mult(ld(X1,X2),X3))),inference(rw,[status(thm)],[215772,19,theory(equality)])).
% cnf(218271,plain,(ld(X1,mult(mult(X1,X2),X3))=mult(rd(X2,X1),mult(X1,X3))),inference(spm,[status(thm)],[15,213572,theory(equality)])).
% cnf(242486,negated_conjecture,(mult(ld(mult(mult(b,c),a),b),a)=ld(c,unit)|mult(a,mult(mult(b,c),a))!=mult(a,mult(b,mult(c,a)))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[207607,111856,theory(equality)]),2395,theory(equality)]),89522,theory(equality)])).
% cnf(242648,negated_conjecture,(mult(ld(mult(b,mult(c,a)),b),a)=ld(c,unit)|mult(b,mult(a,c))!=mult(b,mult(c,a))),inference(spm,[status(thm)],[242486,113,theory(equality)])).
% cnf(242904,negated_conjecture,(ld(mult(c,a),a)=ld(c,unit)|mult(b,mult(a,c))!=mult(b,mult(c,a))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[242648,2395,theory(equality)]),89522,theory(equality)])).
% cnf(251684,negated_conjecture,(rd(mult(a,mult(c,a)),mult(ld(c,unit),mult(c,a)))=mult(c,a)|mult(b,mult(c,a))!=mult(b,mult(a,c))),inference(spm,[status(thm)],[92787,242904,theory(equality)])).
% cnf(251765,negated_conjecture,(mult(a,c)=mult(c,a)|mult(b,mult(c,a))!=mult(b,mult(a,c))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[251684,89522,theory(equality)]),15,theory(equality)]),412,theory(equality)]),95792,theory(equality)]),13,theory(equality)])).
% cnf(251766,negated_conjecture,(mult(b,mult(c,a))!=mult(b,mult(a,c))),inference(sr,[status(thm)],[251765,208121,theory(equality)])).
% cnf(255008,plain,(rd(mult(X1,mult(X2,X3)),X3)=mult(X3,mult(ld(X3,X1),X2))),inference(rw,[status(thm)],[412,215773,theory(equality)])).
% cnf(271311,negated_conjecture,(mult(a,mult(b,mult(a,c)))=mult(a,mult(mult(b,c),a))|mult(a,mult(mult(b,c),a))!=mult(a,mult(b,mult(c,a)))),inference(rw,[status(thm)],[207645,211997,theory(equality)])).
% cnf(271312,negated_conjecture,(mult(a,mult(b,mult(c,a)))=mult(a,mult(b,mult(a,c)))|mult(mult(b,a),c)=mult(b,mult(c,a))),inference(spm,[status(thm)],[271311,29,theory(equality)])).
% cnf(395836,negated_conjecture,(ld(a,mult(a,mult(b,mult(a,c))))=mult(b,mult(c,a))|mult(mult(b,a),c)=mult(b,mult(c,a))),inference(spm,[status(thm)],[15,271312,theory(equality)])).
% cnf(396086,negated_conjecture,(mult(b,mult(a,c))=mult(b,mult(c,a))|mult(mult(b,a),c)=mult(b,mult(c,a))),inference(rw,[status(thm)],[395836,15,theory(equality)])).
% cnf(396087,negated_conjecture,(mult(mult(b,a),c)=mult(b,mult(c,a))),inference(sr,[status(thm)],[396086,251766,theory(equality)])).
% cnf(396240,negated_conjecture,(rd(mult(b,mult(c,a)),c)=mult(b,a)),inference(spm,[status(thm)],[19,396087,theory(equality)])).
% cnf(396447,negated_conjecture,(ld(b,mult(b,mult(c,a)))=mult(rd(a,b),mult(b,c))),inference(spm,[status(thm)],[218271,396087,theory(equality)])).
% cnf(396459,negated_conjecture,(mult(mult(b,c),rd(a,c))=mult(b,a)),inference(rw,[status(thm)],[396240,180625,theory(equality)])).
% cnf(396488,negated_conjecture,(mult(c,a)=mult(rd(a,b),mult(b,c))),inference(rw,[status(thm)],[396447,15,theory(equality)])).
% cnf(396492,negated_conjecture,(rd(mult(b,a),rd(a,c))=mult(b,c)),inference(spm,[status(thm)],[19,396459,theory(equality)])).
% cnf(396717,negated_conjecture,(mult(mult(b,a),rd(c,a))=mult(b,c)),inference(rw,[status(thm)],[396492,98504,theory(equality)])).
% cnf(397018,negated_conjecture,(rd(mult(b,c),mult(c,a))=ld(rd(a,b),unit)),inference(spm,[status(thm)],[89257,396488,theory(equality)])).
% cnf(397031,negated_conjecture,(mult(mult(rd(a,b),b),c)=mult(c,a)|ld(mult(rd(a,b),c),mult(c,a))=b),inference(spm,[status(thm)],[61,396488,theory(equality)])).
% cnf(397032,negated_conjecture,(mult(mult(rd(a,b),b),c)=mult(c,a)|rd(mult(c,a),b)=mult(rd(a,b),c)),inference(spm,[status(thm)],[62,396488,theory(equality)])).
% cnf(397068,negated_conjecture,(rd(mult(c,a),b)=mult(mult(rd(a,b),b),rd(c,b))),inference(spm,[status(thm)],[180625,396488,theory(equality)])).
% cnf(397190,negated_conjecture,(rd(mult(b,c),mult(c,a))=rd(b,a)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[397018,98425,theory(equality)]),21,theory(equality)])).
% cnf(397192,negated_conjecture,(mult(a,c)=mult(c,a)|ld(mult(rd(a,b),c),mult(c,a))=b),inference(rw,[status(thm)],[397031,17,theory(equality)])).
% cnf(397193,negated_conjecture,(ld(mult(rd(a,b),c),mult(c,a))=b),inference(sr,[status(thm)],[397192,208121,theory(equality)])).
% cnf(397194,negated_conjecture,(mult(a,c)=mult(c,a)|rd(mult(c,a),b)=mult(rd(a,b),c)),inference(rw,[status(thm)],[397032,17,theory(equality)])).
% cnf(397195,negated_conjecture,(rd(mult(c,a),b)=mult(rd(a,b),c)),inference(sr,[status(thm)],[397194,208121,theory(equality)])).
% cnf(397245,negated_conjecture,(rd(mult(c,a),b)=mult(a,rd(c,b))),inference(rw,[status(thm)],[397068,17,theory(equality)])).
% cnf(399089,negated_conjecture,(mult(mult(b,c),a)=mult(rd(mult(b,a),a),mult(a,c))),inference(spm,[status(thm)],[111554,396717,theory(equality)])).
% cnf(399213,negated_conjecture,(mult(mult(b,c),a)=mult(b,mult(a,c))),inference(rw,[status(thm)],[399089,19,theory(equality)])).
% cnf(399448,negated_conjecture,(ld(b,mult(b,mult(a,c)))=mult(rd(c,b),mult(b,a))),inference(spm,[status(thm)],[218271,399213,theory(equality)])).
% cnf(399540,negated_conjecture,(mult(a,c)=mult(rd(c,b),mult(b,a))),inference(rw,[status(thm)],[399448,15,theory(equality)])).
% cnf(401245,negated_conjecture,(mult(rd(a,b),c)=mult(a,rd(c,b))),inference(rw,[status(thm)],[397245,397195,theory(equality)])).
% cnf(401246,negated_conjecture,(ld(rd(a,b),mult(a,rd(c,b)))=c),inference(spm,[status(thm)],[15,401245,theory(equality)])).
% cnf(401448,negated_conjecture,(mult(rd(b,a),mult(a,rd(c,b)))=c),inference(rw,[status(thm)],[401246,98425,theory(equality)])).
% cnf(401687,negated_conjecture,(rd(mult(b,a),mult(a,c))=ld(rd(c,b),unit)),inference(spm,[status(thm)],[89257,399540,theory(equality)])).
% cnf(401701,negated_conjecture,(mult(mult(rd(c,b),b),a)=mult(a,c)|rd(mult(a,c),b)=mult(rd(c,b),a)),inference(spm,[status(thm)],[62,399540,theory(equality)])).
% cnf(401737,negated_conjecture,(rd(mult(a,c),b)=mult(mult(rd(c,b),b),rd(a,b))),inference(spm,[status(thm)],[180625,399540,theory(equality)])).
% cnf(401754,negated_conjecture,(mult(rd(c,b),mult(a,b))=mult(c,a)|mult(a,c)=mult(c,a)),inference(spm,[status(thm)],[138,399540,theory(equality)])).
% cnf(401859,negated_conjecture,(rd(mult(b,a),mult(a,c))=rd(b,c)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[401687,98425,theory(equality)]),21,theory(equality)])).
% cnf(401863,negated_conjecture,(mult(c,a)=mult(a,c)|rd(mult(a,c),b)=mult(rd(c,b),a)),inference(rw,[status(thm)],[401701,17,theory(equality)])).
% cnf(401864,negated_conjecture,(rd(mult(a,c),b)=mult(rd(c,b),a)),inference(sr,[status(thm)],[401863,208121,theory(equality)])).
% cnf(401914,negated_conjecture,(rd(mult(a,c),b)=mult(c,rd(a,b))),inference(rw,[status(thm)],[401737,17,theory(equality)])).
% cnf(401933,negated_conjecture,(mult(rd(c,b),mult(a,b))=mult(c,a)),inference(sr,[status(thm)],[401754,208121,theory(equality)])).
% cnf(402453,negated_conjecture,(ld(rd(c,b),mult(c,a))=mult(a,b)),inference(spm,[status(thm)],[15,401933,theory(equality)])).
% cnf(402707,negated_conjecture,(mult(rd(b,c),mult(c,a))=mult(a,b)),inference(rw,[status(thm)],[402453,98425,theory(equality)])).
% cnf(402993,negated_conjecture,(mult(rd(c,b),a)=mult(c,rd(a,b))),inference(rw,[status(thm)],[401914,401864,theory(equality)])).
% cnf(403498,negated_conjecture,(rd(mult(c,mult(a,b)),a)=mult(c,mult(rd(b,c),c))),inference(spm,[status(thm)],[213223,402707,theory(equality)])).
% cnf(403506,negated_conjecture,(mult(c,mult(a,b))=mult(mult(c,b),a)),inference(spm,[status(thm)],[213572,402707,theory(equality)])).
% cnf(403686,negated_conjecture,(mult(mult(c,a),rd(b,a))=mult(c,mult(rd(b,c),c))),inference(rw,[status(thm)],[403498,180625,theory(equality)])).
% cnf(403687,negated_conjecture,(mult(mult(c,a),rd(b,a))=mult(c,b)),inference(rw,[status(thm)],[403686,17,theory(equality)])).
% cnf(403953,negated_conjecture,(rd(mult(c,b),rd(b,a))=mult(c,a)),inference(spm,[status(thm)],[19,403687,theory(equality)])).
% cnf(404176,negated_conjecture,(mult(mult(c,b),rd(a,b))=mult(c,a)),inference(rw,[status(thm)],[403953,98504,theory(equality)])).
% cnf(404972,negated_conjecture,(mult(mult(c,a),b)=mult(rd(mult(c,b),b),mult(b,a))),inference(spm,[status(thm)],[111554,404176,theory(equality)])).
% cnf(405093,negated_conjecture,(mult(mult(c,a),b)=mult(c,mult(b,a))),inference(rw,[status(thm)],[404972,19,theory(equality)])).
% cnf(408663,negated_conjecture,(ld(mult(mult(c,a),rd(b,a)),mult(mult(c,a),mult(b,c)))=mult(c,a)),inference(spm,[status(thm)],[99239,397190,theory(equality)])).
% cnf(408671,negated_conjecture,(mult(rd(b,a),c)=mult(b,mult(c,ld(mult(c,a),c)))),inference(spm,[status(thm)],[100603,397190,theory(equality)])).
% cnf(408728,negated_conjecture,(mult(mult(ld(b,a),b),c)=mult(c,a)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[408663,403687,theory(equality)]),203257,theory(equality)]),111856,theory(equality)]),2395,theory(equality)]),8490,theory(equality)])).
% cnf(408740,negated_conjecture,(mult(rd(b,a),c)=mult(b,rd(c,a))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[408671,2395,theory(equality)]),2440,theory(equality)])).
% cnf(408962,negated_conjecture,(mult(a,c)=mult(c,a)|mult(b,mult(a,b))!=mult(a,mult(b,b))),inference(spm,[status(thm)],[408728,98881,theory(equality)])).
% cnf(409027,negated_conjecture,(mult(b,mult(a,b))!=mult(a,mult(b,b))),inference(sr,[status(thm)],[408962,208121,theory(equality)])).
% cnf(411578,negated_conjecture,(mult(rd(b,c),a)=mult(b,mult(a,ld(mult(a,c),a)))),inference(spm,[status(thm)],[100603,401859,theory(equality)])).
% cnf(411631,negated_conjecture,(mult(rd(b,c),a)=mult(b,rd(a,c))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[411578,2395,theory(equality)]),2440,theory(equality)])).
% cnf(422730,negated_conjecture,(ld(mult(a,rd(c,b)),mult(c,a))=b),inference(rw,[status(thm)],[397193,401245,theory(equality)])).
% cnf(422801,negated_conjecture,(mult(a,mult(rd(c,b),b))=mult(c,a)|mult(a,mult(b,rd(c,b)))=mult(c,a)),inference(spm,[status(thm)],[155,422730,theory(equality)])).
% cnf(422829,negated_conjecture,(mult(a,c)=mult(c,a)|mult(a,mult(b,rd(c,b)))=mult(c,a)),inference(rw,[status(thm)],[422801,17,theory(equality)])).
% cnf(422830,negated_conjecture,(mult(a,mult(b,rd(c,b)))=mult(c,a)),inference(sr,[status(thm)],[422829,208121,theory(equality)])).
% cnf(422832,negated_conjecture,(ld(a,mult(c,a))=mult(b,rd(c,b))),inference(spm,[status(thm)],[15,422830,theory(equality)])).
% cnf(423076,negated_conjecture,(mult(a,c)=mult(c,a)|rd(c,b)!=ld(b,c)),inference(spm,[status(thm)],[422830,135640,theory(equality)])).
% cnf(423077,negated_conjecture,(mult(ld(a,c),a)=mult(b,rd(c,b))),inference(rw,[status(thm)],[422832,92786,theory(equality)])).
% cnf(423230,negated_conjecture,(rd(c,b)!=ld(b,c)),inference(sr,[status(thm)],[423076,208121,theory(equality)])).
% cnf(423980,negated_conjecture,(mult(a,c)=mult(c,a)|mult(b,rd(c,b))!=c),inference(spm,[status(thm)],[78567,423077,theory(equality)])).
% cnf(424205,negated_conjecture,(mult(b,rd(c,b))!=c),inference(sr,[status(thm)],[423980,208121,theory(equality)])).
% cnf(430477,negated_conjecture,(mult(mult(rd(b,a),a),rd(c,b))=mult(rd(b,a),mult(rd(c,b),a))|ld(mult(rd(b,a),a),c)=rd(c,b)),inference(spm,[status(thm)],[127,401448,theory(equality)])).
% cnf(430519,negated_conjecture,(rd(mult(a,c),rd(c,b))=mult(a,mult(rd(b,a),a))),inference(spm,[status(thm)],[213223,401448,theory(equality)])).
% cnf(430526,negated_conjecture,(mult(a,c)=mult(mult(a,b),rd(c,b))),inference(spm,[status(thm)],[213572,401448,theory(equality)])).
% cnf(430638,negated_conjecture,(mult(b,rd(c,b))=mult(rd(b,a),mult(rd(c,b),a))|ld(mult(rd(b,a),a),c)=rd(c,b)),inference(rw,[status(thm)],[430477,17,theory(equality)])).
% cnf(430639,negated_conjecture,(mult(b,rd(c,b))=mult(rd(b,a),mult(c,rd(a,b)))|ld(mult(rd(b,a),a),c)=rd(c,b)),inference(rw,[status(thm)],[430638,402993,theory(equality)])).
% cnf(430640,negated_conjecture,(mult(b,rd(c,b))=mult(rd(b,a),mult(c,rd(a,b)))|ld(b,c)=rd(c,b)),inference(rw,[status(thm)],[430639,17,theory(equality)])).
% cnf(430641,negated_conjecture,(mult(rd(b,a),mult(c,rd(a,b)))=mult(b,rd(c,b))),inference(sr,[status(thm)],[430640,423230,theory(equality)])).
% cnf(430717,negated_conjecture,(mult(mult(a,c),rd(b,c))=mult(a,mult(rd(b,a),a))),inference(rw,[status(thm)],[430519,98504,theory(equality)])).
% cnf(430718,negated_conjecture,(mult(mult(a,c),rd(b,c))=mult(a,b)),inference(rw,[status(thm)],[430717,17,theory(equality)])).
% cnf(431198,negated_conjecture,(mult(mult(a,b),c)=mult(rd(mult(a,c),c),mult(c,b))),inference(spm,[status(thm)],[111554,430718,theory(equality)])).
% cnf(431369,negated_conjecture,(mult(mult(a,b),c)=mult(a,mult(c,b))),inference(rw,[status(thm)],[431198,19,theory(equality)])).
% cnf(431602,negated_conjecture,(ld(a,mult(a,mult(c,b)))=mult(rd(b,a),mult(a,c))),inference(spm,[status(thm)],[218271,431369,theory(equality)])).
% cnf(431641,negated_conjecture,(mult(a,mult(c,mult(a,b)))!=mult(a,mult(b,mult(c,a)))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[32,431369,theory(equality)]),93044,theory(equality)]),403506,theory(equality)])).
% cnf(431677,negated_conjecture,(mult(c,b)=mult(rd(b,a),mult(a,c))),inference(rw,[status(thm)],[431602,15,theory(equality)])).
% cnf(431873,negated_conjecture,(mult(mult(rd(b,a),c),rd(a,b))=mult(b,rd(c,b))|ld(mult(rd(b,a),rd(a,b)),mult(b,rd(c,b)))=c),inference(spm,[status(thm)],[61,430641,theory(equality)])).
% cnf(432070,negated_conjecture,(mult(mult(b,rd(c,a)),rd(a,b))=mult(b,rd(c,b))|ld(mult(rd(b,a),rd(a,b)),mult(b,rd(c,b)))=c),inference(rw,[status(thm)],[431873,408740,theory(equality)])).
% cnf(432071,negated_conjecture,(mult(mult(b,rd(c,a)),rd(a,b))=mult(b,rd(c,b))|mult(b,rd(c,b))=c),inference(rw,[status(thm)],[inference(rw,[status(thm)],[432070,98396,theory(equality)]),33,theory(equality)])).
% cnf(432072,negated_conjecture,(mult(mult(b,rd(c,a)),rd(a,b))=mult(b,rd(c,b))),inference(sr,[status(thm)],[432071,424205,theory(equality)])).
% cnf(432408,negated_conjecture,(mult(mult(a,c),b)=mult(rd(mult(a,b),b),mult(b,c))),inference(spm,[status(thm)],[111554,430526,theory(equality)])).
% cnf(432580,negated_conjecture,(mult(mult(a,c),b)=mult(a,mult(b,c))),inference(rw,[status(thm)],[432408,19,theory(equality)])).
% cnf(433910,negated_conjecture,(mult(mult(a,mult(b,rd(c,b))),b)=mult(a,mult(mult(b,rd(c,a)),a))),inference(spm,[status(thm)],[215181,432072,theory(equality)])).
% cnf(434077,negated_conjecture,(mult(c,mult(b,a))=mult(a,mult(mult(b,rd(c,a)),a))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[433910,422830,theory(equality)]),405093,theory(equality)])).
% cnf(434078,negated_conjecture,(mult(c,mult(b,a))=mult(a,mult(c,b))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[434077,111554,theory(equality)]),431677,theory(equality)])).
% cnf(434309,negated_conjecture,(rd(mult(a,mult(c,b)),b)=mult(mult(c,b),rd(a,b))),inference(spm,[status(thm)],[180625,434078,theory(equality)])).
% cnf(434484,negated_conjecture,(mult(b,mult(ld(b,a),c))=mult(mult(c,b),rd(a,b))),inference(rw,[status(thm)],[434309,255008,theory(equality)])).
% cnf(434485,negated_conjecture,(mult(b,mult(ld(b,a),c))=mult(c,a)),inference(rw,[status(thm)],[434484,404176,theory(equality)])).
% cnf(436728,negated_conjecture,(mult(mult(b,ld(b,a)),c)=mult(b,mult(c,ld(b,a)))|ld(mult(b,ld(b,a)),mult(c,a))=c),inference(spm,[status(thm)],[127,434485,theory(equality)])).
% cnf(436851,negated_conjecture,(mult(a,c)=mult(b,mult(c,ld(b,a)))|ld(mult(b,ld(b,a)),mult(c,a))=c),inference(rw,[status(thm)],[436728,13,theory(equality)])).
% cnf(436852,negated_conjecture,(mult(a,c)=mult(b,mult(c,ld(b,a)))|mult(b,rd(c,b))=c),inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[436851,13,theory(equality)]),92786,theory(equality)]),423077,theory(equality)])).
% cnf(436853,negated_conjecture,(mult(b,mult(c,ld(b,a)))=mult(a,c)),inference(sr,[status(thm)],[436852,424205,theory(equality)])).
% cnf(436999,negated_conjecture,(mult(mult(a,c),b)=mult(b,mult(mult(c,ld(b,a)),b))),inference(spm,[status(thm)],[93044,436853,theory(equality)])).
% cnf(437207,negated_conjecture,(mult(a,mult(b,c))=mult(b,mult(mult(c,ld(b,a)),b))),inference(rw,[status(thm)],[436999,432580,theory(equality)])).
% cnf(437208,negated_conjecture,(mult(a,mult(b,c))=mult(b,mult(c,a))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[437207,918,theory(equality)]),401933,theory(equality)])).
% cnf(438400,negated_conjecture,(rd(mult(a,mult(b,c)),c)=mult(mult(b,c),rd(a,c))),inference(spm,[status(thm)],[180625,437208,theory(equality)])).
% cnf(438484,negated_conjecture,(mult(a,mult(c,mult(a,b)))!=mult(a,mult(a,mult(b,c)))),inference(rw,[status(thm)],[431641,437208,theory(equality)])).
% cnf(438638,negated_conjecture,(mult(c,mult(ld(c,a),b))=mult(mult(b,c),rd(a,c))),inference(rw,[status(thm)],[438400,255008,theory(equality)])).
% cnf(438639,negated_conjecture,(mult(c,mult(ld(c,a),b))=mult(b,a)),inference(rw,[status(thm)],[438638,396459,theory(equality)])).
% cnf(444152,negated_conjecture,(mult(mult(b,a),b)=mult(mult(c,ld(c,a)),mult(b,b))|mult(mult(c,b),ld(c,a))=mult(b,a)),inference(spm,[status(thm)],[254,438639,theory(equality)])).
% cnf(444295,negated_conjecture,(mult(b,mult(a,b))=mult(mult(c,ld(c,a)),mult(b,b))|mult(mult(c,b),ld(c,a))=mult(b,a)),inference(rw,[status(thm)],[444152,93044,theory(equality)])).
% cnf(444296,negated_conjecture,(mult(b,mult(a,b))=mult(a,mult(b,b))|mult(mult(c,b),ld(c,a))=mult(b,a)),inference(rw,[status(thm)],[444295,13,theory(equality)])).
% cnf(444297,negated_conjecture,(mult(b,mult(a,b))=mult(a,mult(b,b))|mult(c,mult(b,rd(a,c)))=mult(b,a)),inference(rw,[status(thm)],[inference(rw,[status(thm)],[444296,208052,theory(equality)]),411631,theory(equality)])).
% cnf(444298,negated_conjecture,(mult(c,mult(b,rd(a,c)))=mult(b,a)),inference(sr,[status(thm)],[444297,409027,theory(equality)])).
% cnf(444425,negated_conjecture,(mult(mult(b,a),c)=mult(c,mult(mult(b,rd(a,c)),c))),inference(spm,[status(thm)],[93044,444298,theory(equality)])).
% cnf(444632,negated_conjecture,(mult(a,mult(b,c))=mult(c,mult(mult(b,rd(a,c)),c))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[444425,396087,theory(equality)]),437208,theory(equality)])).
% cnf(444633,negated_conjecture,(mult(a,mult(b,c))=mult(c,mult(a,b))),inference(rw,[status(thm)],[inference(rw,[status(thm)],[444632,111554,theory(equality)]),402707,theory(equality)])).
% cnf(459044,negated_conjecture,($false),inference(rw,[status(thm)],[438484,444633,theory(equality)])).
% cnf(459045,negated_conjecture,($false),inference(cn,[status(thm)],[459044,theory(equality)])).
% cnf(459046,negated_conjecture,($false),459045,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 3176
% # ...of these trivial : 435
% # ...subsumed : 1501
% # ...remaining for further processing: 1240
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 112
% # Backward-rewritten : 650
% # Generated clauses : 272129
% # ...of the previous two non-trivial : 254228
% # Contextual simplify-reflections : 45
% # Paramodulations : 272092
% # Factorizations : 35
% # Equation resolutions : 2
% # Current number of processed clauses: 477
% # Positive orientable unit clauses: 294
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 33
% # Non-unit-clauses : 150
% # Current number of unprocessed clauses: 105462
% # ...number of literals in the above : 238285
% # Clause-clause subsumption calls (NU) : 65178
% # Rec. Clause-clause subsumption calls : 60807
% # Unit Clause-clause subsumption calls : 12545
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 2604
% # Indexed BW rewrite successes : 273
% # Backwards rewriting index: 337 leaves, 1.99+/-2.876 terms/leaf
% # Paramod-from index: 235 leaves, 1.57+/-1.626 terms/leaf
% # Paramod-into index: 315 leaves, 1.84+/-2.495 terms/leaf
% # -------------------------------------------------
% # User time : 11.086 s
% # System time : 0.367 s
% # Total time : 11.453 s
% # Maximum resident set size: 0 pages
% PrfWatch: 18.52 CPU 19.52 WC
% FINAL PrfWatch: 18.52 CPU 19.52 WC
% SZS output end Solution for /tmp/SystemOnTPTP23267/GRP745+1.tptp
%
%------------------------------------------------------------------------------