%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP667+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 07:31:08 AM UTC 2026
% Result : Theorem 19.53s 7.95s
% Output : CNFRefutation 19.53s
% Verified :
% SZS Type : Refutation
% Derivation depth : 72
% Number of leaves : 12
% Syntax : Number of formulae : 324 ( 292 unt; 0 def)
% Number of atoms : 356 ( 355 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 66 ( 34 ~; 30 |; 0 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 1 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 4 con; 0-2 aty)
% Number of variables : 553 ( 0 sgn 22 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f01,axiom,
! [B,A] : mult(A,ld(A,B)) = B,
file('theBenchmark.p',f01) ).
fof(f02,axiom,
! [B,A] : ld(A,mult(A,B)) = B,
file('theBenchmark.p',f02) ).
fof(f03,axiom,
! [B,A] : mult(rd(A,B),B) = A,
file('theBenchmark.p',f03) ).
fof(f04,axiom,
! [B,A] : rd(mult(A,B),B) = A,
file('theBenchmark.p',f04) ).
fof(f05,axiom,
! [A] : mult(A,unit) = A,
file('theBenchmark.p',f05) ).
fof(f06,axiom,
! [A] : mult(unit,A) = A,
file('theBenchmark.p',f06) ).
fof(f07,axiom,
! [C,B,A] : mult(mult(A,B),mult(mult(C,B),C)) = mult(mult(A,mult(mult(B,C),B)),C),
file('theBenchmark.p',f07) ).
fof(f08,axiom,
! [B,A] : mult(mult(A,B),A) = mult(A,mult(B,A)),
file('theBenchmark.p',f08) ).
fof(f09,axiom,
! [A] : mult(f(A),f(A)) = A,
file('theBenchmark.p',f09) ).
fof(f10,axiom,
! [X0,X1,X2] :
( mult(X0,mult(X1,mult(X2,X1))) = mult(mult(mult(X0,X1),X2),X1)
=> mult(X1,mult(X0,mult(X1,X2))) = mult(mult(mult(X1,X0),X1),X2) ),
file('theBenchmark.p',f10) ).
fof(f11,axiom,
! [X3,X4,X5] :
( mult(mult(X3,X4),mult(X5,X3)) = mult(mult(X3,mult(X4,X5)),X3)
=> mult(X3,mult(X4,mult(X3,X5))) = mult(mult(mult(X3,X4),X3),X5) ),
file('theBenchmark.p',f11) ).
fof(goals,conjecture,
mult(a,mult(b,mult(a,c))) = mult(mult(mult(a,b),a),c),
file('theBenchmark.p',goals) ).
fof(goals_neg,negated_conjecture,
mult(a,mult(b,mult(a,c))) != mult(mult(mult(a,b),a),c),
inference(assume_negation,[status(cth)],[goals]) ).
cnf(c_14,plain,
mult(A,ld(A,B)) = B,
inference(clausify,[status(thm)],[f01]) ).
cnf(c_15,plain,
ld(A,mult(A,B)) = B,
inference(clausify,[status(thm)],[f02]) ).
cnf(c_16,plain,
mult(rd(A,B),B) = A,
inference(clausify,[status(thm)],[f03]) ).
cnf(c_17,plain,
rd(mult(A,B),B) = A,
inference(clausify,[status(thm)],[f04]) ).
cnf(c_18,plain,
mult(A,unit) = A,
inference(clausify,[status(thm)],[f05]) ).
cnf(c_19,plain,
mult(unit,A) = A,
inference(clausify,[status(thm)],[f06]) ).
cnf(c_20,plain,
mult(mult(A,mult(mult(B,C),B)),C) = mult(mult(A,B),mult(mult(C,B),C)),
inference(clausify,[status(thm)],[f07]) ).
cnf(c_21,plain,
mult(mult(A,B),A) = mult(A,mult(B,A)),
inference(clausify,[status(thm)],[f08]) ).
cnf(c_22,plain,
mult(f(A),f(A)) = A,
inference(clausify,[status(thm)],[f09]) ).
cnf(c_23,plain,
( mult(mult(mult(B,A),B),C) = mult(B,mult(A,mult(B,C)))
| mult(mult(mult(A,B),C),B) != mult(A,mult(B,mult(C,B))) ),
inference(clausify,[status(thm)],[f10]) ).
cnf(c_24,plain,
( mult(mult(B,mult(A,B)),C) = mult(B,mult(A,mult(B,C)))
| mult(mult(mult(A,B),C),B) != mult(A,mult(B,mult(C,B))) ),
inference(paramod,[status(thm)],[c_21,c_23]) ).
cnf(c_25,plain,
( mult(mult(mult(A,B),A),C) = mult(A,mult(B,mult(A,C)))
| mult(mult(A,mult(B,C)),A) != mult(mult(A,B),mult(C,A)) ),
inference(clausify,[status(thm)],[f11]) ).
cnf(c_8920,plain,
( mult(mult(mult(A,B),A),C) = mult(A,mult(B,mult(A,C)))
| mult(A,mult(mult(B,C),A)) != mult(mult(A,B),mult(C,A)) ),
inference(paramod,[status(thm)],[c_21,c_25]) ).
cnf(c_8921,plain,
( mult(mult(A,mult(B,A)),C) = mult(A,mult(B,mult(A,C)))
| mult(A,mult(mult(B,C),A)) != mult(mult(A,B),mult(C,A)) ),
inference(paramod,[status(thm)],[c_21,c_8920]) ).
cnf(c_26,plain,
( mult(mult(A,mult(B,A)),C) = mult(A,mult(B,mult(A,C)))
| mult(mult(A,B),mult(C,A)) != mult(A,mult(mult(B,C),A)) ),
inference(copy,[status(thm)],[c_8921]) ).
cnf(c_28,negated_conjecture,
mult(mult(mult(a,b),a),c) != mult(a,mult(b,mult(a,c))),
inference(clausify,[status(thm)],[goals_neg]) ).
cnf(c_29,negated_conjecture,
mult(mult(a,mult(b,a)),c) != mult(a,mult(b,mult(a,c))),
inference(paramod,[status(thm)],[c_21,c_28]) ).
cnf(c_8922,plain,
mult(mult(A,mult(B,mult(C,B))),C) = mult(mult(A,B),mult(mult(C,B),C)),
inference(paramod,[status(thm)],[c_21,c_20]) ).
cnf(c_30,plain,
mult(mult(A,mult(B,mult(C,B))),C) = mult(mult(A,B),mult(C,mult(B,C))),
inference(paramod,[status(thm)],[c_21,c_8922]) ).
cnf(c_31,plain,
ld(rd(A,B),A) = B,
inference(paramod,[status(thm)],[c_16,c_15]) ).
cnf(c_32,plain,
rd(A,ld(B,A)) = B,
inference(paramod,[status(thm)],[c_14,c_17]) ).
cnf(c_33,plain,
ld(A,A) = unit,
inference(paramod,[status(thm)],[c_18,c_15]) ).
cnf(c_8923,plain,
mult(A,B) = mult(B,mult(ld(B,A),B)),
inference(paramod,[status(thm)],[c_14,c_21]) ).
cnf(c_37,plain,
mult(A,mult(ld(A,B),A)) = mult(B,A),
inference(copy,[status(thm)],[c_8923]) ).
cnf(c_38,plain,
ld(mult(A,B),mult(A,mult(B,A))) = A,
inference(paramod,[status(thm)],[c_21,c_15]) ).
cnf(c_8924,plain,
mult(A,rd(A,B)) = mult(rd(A,B),mult(B,rd(A,B))),
inference(paramod,[status(thm)],[c_16,c_21]) ).
cnf(c_39,plain,
mult(rd(A,B),mult(B,rd(A,B))) = mult(A,rd(A,B)),
inference(copy,[status(thm)],[c_8924]) ).
cnf(c_42,plain,
ld(f(A),A) = f(A),
inference(paramod,[status(thm)],[c_22,c_15]) ).
cnf(c_8925,plain,
mult(A,f(A)) = mult(f(A),mult(f(A),f(A))),
inference(paramod,[status(thm)],[c_22,c_21]) ).
cnf(c_8926,plain,
mult(A,f(A)) = mult(f(A),A),
inference(paramod,[status(thm)],[c_22,c_8925]) ).
cnf(c_44,plain,
mult(f(A),A) = mult(A,f(A)),
inference(copy,[status(thm)],[c_8926]) ).
cnf(c_8927,plain,
( mult(mult(B,mult(C,B)),ld(mult(C,B),A)) = mult(B,mult(C,mult(B,ld(mult(C,B),A))))
| mult(A,B) != mult(C,mult(B,mult(ld(mult(C,B),A),B))) ),
inference(paramod,[status(thm)],[c_14,c_24]) ).
cnf(c_46,plain,
( mult(mult(B,mult(A,B)),ld(mult(A,B),C)) = mult(B,mult(A,mult(B,ld(mult(A,B),C))))
| mult(A,mult(B,mult(ld(mult(A,B),C),B))) != mult(C,B) ),
inference(copy,[status(thm)],[c_8927]) ).
cnf(c_8928,plain,
( mult(mult(A,mult(unit,A)),B) = mult(A,mult(unit,mult(A,B)))
| mult(mult(A,B),A) != mult(unit,mult(A,mult(B,A))) ),
inference(paramod,[status(thm)],[c_19,c_24]) ).
cnf(c_8929,plain,
( mult(mult(A,mult(unit,A)),B) = mult(A,mult(unit,mult(A,B)))
| mult(A,mult(B,A)) != mult(unit,mult(A,mult(B,A))) ),
inference(paramod,[status(thm)],[c_21,c_8928]) ).
cnf(c_8930,plain,
( mult(mult(A,mult(unit,A)),B) = mult(A,mult(unit,mult(A,B)))
| mult(A,mult(B,A)) != mult(A,mult(B,A)) ),
inference(paramod,[status(thm)],[c_19,c_8929]) ).
cnf(c_8931,plain,
( mult(mult(A,A),B) = mult(A,mult(unit,mult(A,B)))
| mult(A,mult(B,A)) != mult(A,mult(B,A)) ),
inference(paramod,[status(thm)],[c_19,c_8930]) ).
cnf(c_8932,plain,
( mult(mult(A,A),B) = mult(A,mult(A,B))
| mult(A,mult(B,A)) != mult(A,mult(B,A)) ),
inference(paramod,[status(thm)],[c_19,c_8931]) ).
cnf(c_49,plain,
mult(mult(A,A),B) = mult(A,mult(A,B)),
inference(copy,[status(thm)],[c_8932]) ).
cnf(c_8933,plain,
( mult(mult(f(A),mult(f(A),f(A))),B) = mult(f(A),mult(f(A),mult(f(A),B)))
| mult(A,mult(B,f(A))) != mult(f(A),mult(mult(f(A),B),f(A))) ),
inference(paramod,[status(thm)],[c_22,c_26]) ).
cnf(c_8934,plain,
( mult(mult(f(A),mult(f(A),f(A))),B) = mult(f(A),mult(f(A),mult(f(A),B)))
| mult(A,mult(B,f(A))) != mult(f(A),mult(f(A),mult(B,f(A)))) ),
inference(paramod,[status(thm)],[c_21,c_8933]) ).
cnf(c_8935,plain,
( mult(mult(f(A),A),B) = mult(f(A),mult(f(A),mult(f(A),B)))
| mult(A,mult(B,f(A))) != mult(f(A),mult(f(A),mult(B,f(A)))) ),
inference(paramod,[status(thm)],[c_22,c_8934]) ).
cnf(c_8936,plain,
( mult(mult(A,f(A)),B) = mult(f(A),mult(f(A),mult(f(A),B)))
| mult(A,mult(B,f(A))) != mult(f(A),mult(f(A),mult(B,f(A)))) ),
inference(paramod,[status(thm)],[c_44,c_8935]) ).
cnf(c_8937,plain,
( mult(mult(A,f(A)),B) = mult(f(A),mult(f(A),mult(f(A),B)))
| mult(f(A),mult(f(A),mult(B,f(A)))) != mult(A,mult(B,f(A))) ),
inference(copy,[status(thm)],[c_8936]) ).
cnf(c_59,plain,
( mult(f(A),mult(f(A),mult(f(A),B))) = mult(mult(A,f(A)),B)
| mult(f(A),mult(f(A),mult(B,f(A)))) != mult(A,mult(B,f(A))) ),
inference(copy,[status(thm)],[c_8937]) ).
cnf(c_63,negated_conjecture,
mult(mult(mult(b,a),c),a) != mult(b,mult(a,mult(c,a))),
inference(resolve,[status(thm)],[c_24,c_29]) ).
cnf(c_8938,plain,
mult(mult(A,mult(ld(B,C),C)),B) = mult(mult(A,ld(B,C)),mult(B,mult(ld(B,C),B))),
inference(paramod,[status(thm)],[c_14,c_30]) ).
cnf(c_64,plain,
mult(mult(A,mult(ld(B,C),C)),B) = mult(mult(A,ld(B,C)),mult(C,B)),
inference(paramod,[status(thm)],[c_37,c_8938]) ).
cnf(c_8939,plain,
mult(mult(A,mult(B,C)),rd(C,B)) = mult(mult(A,B),mult(rd(C,B),mult(B,rd(C,B)))),
inference(paramod,[status(thm)],[c_16,c_30]) ).
cnf(c_67,plain,
mult(mult(A,mult(B,C)),rd(C,B)) = mult(mult(A,B),mult(C,rd(C,B))),
inference(paramod,[status(thm)],[c_39,c_8939]) ).
cnf(c_8940,plain,
mult(A,B) = mult(mult(rd(A,mult(C,mult(B,C))),C),mult(B,mult(C,B))),
inference(paramod,[status(thm)],[c_16,c_30]) ).
cnf(c_68,plain,
mult(mult(rd(A,mult(B,mult(C,B))),B),mult(C,mult(B,C))) = mult(A,C),
inference(copy,[status(thm)],[c_8940]) ).
cnf(c_70,plain,
rd(mult(mult(A,B),mult(C,mult(B,C))),C) = mult(A,mult(B,mult(C,B))),
inference(paramod,[status(thm)],[c_30,c_17]) ).
cnf(c_8941,plain,
mult(mult(A,B),mult(unit,mult(B,unit))) = mult(A,mult(B,mult(unit,B))),
inference(paramod,[status(thm)],[c_30,c_18]) ).
cnf(c_8942,plain,
mult(mult(A,B),mult(unit,B)) = mult(A,mult(B,mult(unit,B))),
inference(paramod,[status(thm)],[c_18,c_8941]) ).
cnf(c_8943,plain,
mult(mult(A,B),B) = mult(A,mult(B,mult(unit,B))),
inference(paramod,[status(thm)],[c_19,c_8942]) ).
cnf(c_71,plain,
mult(mult(A,B),B) = mult(A,mult(B,B)),
inference(paramod,[status(thm)],[c_19,c_8943]) ).
cnf(c_8944,plain,
mult(mult(A,mult(B,A)),B) = mult(mult(unit,A),mult(B,mult(A,B))),
inference(paramod,[status(thm)],[c_19,c_30]) ).
cnf(c_72,plain,
mult(mult(A,mult(B,A)),B) = mult(A,mult(B,mult(A,B))),
inference(paramod,[status(thm)],[c_19,c_8944]) ).
cnf(c_8945,plain,
mult(mult(A,B),mult(A,mult(B,A))) = mult(A,mult(mult(B,mult(A,B)),A)),
inference(paramod,[status(thm)],[c_30,c_21]) ).
cnf(c_73,plain,
mult(mult(A,B),mult(A,mult(B,A))) = mult(A,mult(B,mult(A,mult(B,A)))),
inference(paramod,[status(thm)],[c_72,c_8945]) ).
cnf(c_75,plain,
ld(A,mult(B,A)) = mult(ld(A,B),A),
inference(paramod,[status(thm)],[c_37,c_15]) ).
cnf(c_76,plain,
rd(mult(A,B),mult(ld(B,A),B)) = B,
inference(paramod,[status(thm)],[c_37,c_17]) ).
cnf(c_8946,plain,
mult(mult(A,f(A)),f(A)) = mult(f(A),mult(A,f(A))),
inference(paramod,[status(thm)],[c_44,c_21]) ).
cnf(c_8947,plain,
mult(A,mult(f(A),f(A))) = mult(f(A),mult(A,f(A))),
inference(paramod,[status(thm)],[c_71,c_8946]) ).
cnf(c_8948,plain,
mult(A,A) = mult(f(A),mult(A,f(A))),
inference(paramod,[status(thm)],[c_22,c_8947]) ).
cnf(c_83,plain,
mult(f(A),mult(A,f(A))) = mult(A,A),
inference(copy,[status(thm)],[c_8948]) ).
cnf(c_8949,plain,
ld(A,B) = mult(ld(A,rd(B,A)),A),
inference(paramod,[status(thm)],[c_16,c_75]) ).
cnf(c_93,plain,
mult(ld(A,rd(B,A)),A) = ld(A,B),
inference(copy,[status(thm)],[c_8949]) ).
cnf(c_8950,plain,
ld(A,A) = mult(ld(A,unit),A),
inference(paramod,[status(thm)],[c_19,c_75]) ).
cnf(c_8951,plain,
unit = mult(ld(A,unit),A),
inference(paramod,[status(thm)],[c_33,c_8950]) ).
cnf(c_94,plain,
mult(ld(A,unit),A) = unit,
inference(copy,[status(thm)],[c_8951]) ).
cnf(c_8952,plain,
ld(A,mult(A,f(A))) = mult(ld(A,f(A)),A),
inference(paramod,[status(thm)],[c_44,c_75]) ).
cnf(c_8953,plain,
f(A) = mult(ld(A,f(A)),A),
inference(paramod,[status(thm)],[c_15,c_8952]) ).
cnf(c_97,plain,
mult(ld(A,f(A)),A) = f(A),
inference(copy,[status(thm)],[c_8953]) ).
cnf(c_99,plain,
ld(ld(A,unit),unit) = A,
inference(paramod,[status(thm)],[c_94,c_15]) ).
cnf(c_100,plain,
rd(unit,A) = ld(A,unit),
inference(paramod,[status(thm)],[c_94,c_17]) ).
cnf(c_109,plain,
ld(mult(A,rd(B,A)),mult(A,B)) = A,
inference(paramod,[status(thm)],[c_16,c_38]) ).
cnf(c_8954,plain,
ld(mult(A,f(A)),mult(f(A),mult(A,f(A)))) = f(A),
inference(paramod,[status(thm)],[c_44,c_38]) ).
cnf(c_115,plain,
ld(mult(A,f(A)),mult(A,A)) = f(A),
inference(paramod,[status(thm)],[c_83,c_8954]) ).
cnf(c_119,plain,
rd(f(A),A) = ld(A,f(A)),
inference(paramod,[status(thm)],[c_97,c_17]) ).
cnf(c_8955,plain,
mult(f(A),ld(A,f(A))) = mult(ld(A,f(A)),mult(A,ld(A,f(A)))),
inference(paramod,[status(thm)],[c_97,c_21]) ).
cnf(c_8956,plain,
mult(f(A),ld(A,f(A))) = mult(ld(A,f(A)),f(A)),
inference(paramod,[status(thm)],[c_14,c_8955]) ).
cnf(c_120,plain,
mult(ld(A,f(A)),f(A)) = mult(f(A),ld(A,f(A))),
inference(copy,[status(thm)],[c_8956]) ).
cnf(c_8957,plain,
mult(mult(A,mult(B,f(B))),ld(B,f(B))) = mult(mult(A,B),mult(ld(B,f(B)),mult(B,ld(B,f(B))))),
inference(paramod,[status(thm)],[c_97,c_30]) ).
cnf(c_8958,plain,
mult(mult(A,mult(B,f(B))),ld(B,f(B))) = mult(mult(A,B),mult(ld(B,f(B)),f(B))),
inference(paramod,[status(thm)],[c_14,c_8957]) ).
cnf(c_124,plain,
mult(mult(A,mult(B,f(B))),ld(B,f(B))) = mult(mult(A,B),mult(f(B),ld(B,f(B)))),
inference(paramod,[status(thm)],[c_120,c_8958]) ).
cnf(c_132,plain,
rd(ld(A,B),A) = ld(A,rd(B,A)),
inference(paramod,[status(thm)],[c_93,c_17]) ).
cnf(c_8959,plain,
mult(ld(A,B),ld(A,rd(B,A))) = mult(ld(A,rd(B,A)),mult(A,ld(A,rd(B,A)))),
inference(paramod,[status(thm)],[c_93,c_21]) ).
cnf(c_8960,plain,
mult(ld(A,B),ld(A,rd(B,A))) = mult(ld(A,rd(B,A)),rd(B,A)),
inference(paramod,[status(thm)],[c_14,c_8959]) ).
cnf(c_133,plain,
mult(ld(A,rd(B,A)),rd(B,A)) = mult(ld(A,B),ld(A,rd(B,A))),
inference(copy,[status(thm)],[c_8960]) ).
cnf(c_8961,plain,
mult(mult(A,mult(B,ld(B,C))),ld(B,rd(C,B))) = mult(mult(A,B),mult(ld(B,rd(C,B)),mult(B,ld(B,rd(C,B))))),
inference(paramod,[status(thm)],[c_93,c_30]) ).
cnf(c_8962,plain,
mult(mult(A,C),ld(B,rd(C,B))) = mult(mult(A,B),mult(ld(B,rd(C,B)),mult(B,ld(B,rd(C,B))))),
inference(paramod,[status(thm)],[c_14,c_8961]) ).
cnf(c_8963,plain,
mult(mult(A,C),ld(B,rd(C,B))) = mult(mult(A,B),mult(ld(B,rd(C,B)),rd(C,B))),
inference(paramod,[status(thm)],[c_14,c_8962]) ).
cnf(c_8964,plain,
mult(mult(A,C),ld(B,rd(C,B))) = mult(mult(A,B),mult(ld(B,C),ld(B,rd(C,B)))),
inference(paramod,[status(thm)],[c_133,c_8963]) ).
cnf(c_137,plain,
mult(mult(A,B),mult(ld(B,C),ld(B,rd(C,B)))) = mult(mult(A,C),ld(B,rd(C,B))),
inference(copy,[status(thm)],[c_8964]) ).
cnf(c_8965,plain,
rd(A,ld(A,unit)) = ld(ld(A,unit),rd(unit,ld(A,unit))),
inference(paramod,[status(thm)],[c_99,c_132]) ).
cnf(c_143,plain,
rd(A,ld(A,unit)) = ld(ld(A,unit),A),
inference(paramod,[status(thm)],[c_32,c_8965]) ).
cnf(c_152,plain,
rd(mult(A,B),A) = mult(A,rd(B,A)),
inference(paramod,[status(thm)],[c_109,c_32]) ).
cnf(c_164,plain,
rd(mult(A,A),f(A)) = mult(A,f(A)),
inference(paramod,[status(thm)],[c_115,c_32]) ).
cnf(c_8966,plain,
mult(ld(f(A),mult(A,f(A))),f(A)) = ld(f(A),mult(A,A)),
inference(paramod,[status(thm)],[c_164,c_93]) ).
cnf(c_8967,plain,
mult(mult(ld(f(A),A),f(A)),f(A)) = ld(f(A),mult(A,A)),
inference(paramod,[status(thm)],[c_75,c_8966]) ).
cnf(c_8968,plain,
mult(mult(f(A),f(A)),f(A)) = ld(f(A),mult(A,A)),
inference(paramod,[status(thm)],[c_42,c_8967]) ).
cnf(c_8969,plain,
mult(A,f(A)) = ld(f(A),mult(A,A)),
inference(paramod,[status(thm)],[c_22,c_8968]) ).
cnf(c_170,plain,
ld(f(A),mult(A,A)) = mult(A,f(A)),
inference(copy,[status(thm)],[c_8969]) ).
cnf(c_173,plain,
rd(mult(A,A),mult(A,f(A))) = f(A),
inference(paramod,[status(thm)],[c_170,c_32]) ).
cnf(c_8970,plain,
mult(ld(mult(A,f(A)),f(A)),mult(A,f(A))) = ld(mult(A,f(A)),mult(A,A)),
inference(paramod,[status(thm)],[c_173,c_93]) ).
cnf(c_188,plain,
mult(ld(mult(A,f(A)),f(A)),mult(A,f(A))) = f(A),
inference(paramod,[status(thm)],[c_115,c_8970]) ).
cnf(c_8971,plain,
mult(mult(f(A),ld(A,f(A))),ld(A,f(A))) = mult(ld(A,f(A)),mult(f(A),ld(A,f(A)))),
inference(paramod,[status(thm)],[c_120,c_21]) ).
cnf(c_8972,plain,
mult(f(A),mult(ld(A,f(A)),ld(A,f(A)))) = mult(ld(A,f(A)),mult(f(A),ld(A,f(A)))),
inference(paramod,[status(thm)],[c_71,c_8971]) ).
cnf(c_197,plain,
mult(ld(A,f(A)),mult(f(A),ld(A,f(A)))) = mult(f(A),mult(ld(A,f(A)),ld(A,f(A)))),
inference(copy,[status(thm)],[c_8972]) ).
cnf(c_8973,plain,
ld(f(A),mult(f(A),ld(A,f(A)))) = mult(ld(f(A),ld(A,f(A))),f(A)),
inference(paramod,[status(thm)],[c_120,c_75]) ).
cnf(c_8974,plain,
ld(A,f(A)) = mult(ld(f(A),ld(A,f(A))),f(A)),
inference(paramod,[status(thm)],[c_15,c_8973]) ).
cnf(c_200,plain,
mult(ld(f(A),ld(A,f(A))),f(A)) = ld(A,f(A)),
inference(copy,[status(thm)],[c_8974]) ).
cnf(c_217,plain,
ld(mult(A,A),mult(A,mult(A,B))) = B,
inference(paramod,[status(thm)],[c_49,c_15]) ).
cnf(c_218,plain,
rd(mult(A,mult(A,B)),B) = mult(A,A),
inference(paramod,[status(thm)],[c_49,c_17]) ).
cnf(c_8975,plain,
mult(A,B) = mult(f(A),mult(f(A),B)),
inference(paramod,[status(thm)],[c_22,c_49]) ).
cnf(c_220,plain,
mult(f(A),mult(f(A),B)) = mult(A,B),
inference(copy,[status(thm)],[c_8975]) ).
cnf(c_223,plain,
ld(A,mult(B,mult(B,A))) = mult(ld(A,mult(B,B)),A),
inference(paramod,[status(thm)],[c_49,c_75]) ).
cnf(c_8976,plain,
mult(mult(A,mult(A,mult(A,A))),B) = mult(mult(A,A),mult(mult(A,A),B)),
inference(paramod,[status(thm)],[c_49,c_49]) ).
cnf(c_8977,plain,
mult(mult(A,mult(A,mult(A,A))),B) = mult(mult(A,A),mult(A,mult(A,B))),
inference(paramod,[status(thm)],[c_49,c_8976]) ).
cnf(c_238,plain,
mult(mult(A,mult(A,mult(A,A))),B) = mult(A,mult(A,mult(A,mult(A,B)))),
inference(paramod,[status(thm)],[c_49,c_8977]) ).
cnf(c_8978,plain,
( mult(f(A),mult(f(A),mult(f(A),B))) = mult(mult(A,f(A)),B)
| mult(A,mult(B,f(A))) != mult(A,mult(B,f(A))) ),
inference(paramod,[status(thm)],[c_220,c_59]) ).
cnf(c_8979,plain,
( mult(f(A),mult(A,B)) = mult(mult(A,f(A)),B)
| mult(A,mult(B,f(A))) != mult(A,mult(B,f(A))) ),
inference(paramod,[status(thm)],[c_220,c_8978]) ).
cnf(c_8980,plain,
( mult(mult(A,f(A)),B) = mult(f(A),mult(A,B))
| mult(A,mult(B,f(A))) != mult(A,mult(B,f(A))) ),
inference(copy,[status(thm)],[c_8979]) ).
cnf(c_242,plain,
mult(mult(A,f(A)),B) = mult(f(A),mult(A,B)),
inference(copy,[status(thm)],[c_8980]) ).
cnf(c_8981,plain,
mult(A,ld(B,A)) = mult(B,mult(ld(B,A),ld(B,A))),
inference(paramod,[status(thm)],[c_14,c_71]) ).
cnf(c_252,plain,
mult(A,mult(ld(A,B),ld(A,B))) = mult(B,ld(A,B)),
inference(copy,[status(thm)],[c_8981]) ).
cnf(c_8982,plain,
mult(A,B) = mult(rd(A,B),mult(B,B)),
inference(paramod,[status(thm)],[c_16,c_71]) ).
cnf(c_253,plain,
mult(rd(A,B),mult(B,B)) = mult(A,B),
inference(copy,[status(thm)],[c_8982]) ).
cnf(c_8983,plain,
mult(mult(A,B),mult(ld(B,A),B)) = mult(B,mult(mult(ld(B,A),B),mult(ld(B,A),B))),
inference(paramod,[status(thm)],[c_37,c_71]) ).
cnf(c_257,plain,
mult(A,mult(mult(ld(A,B),A),mult(ld(A,B),A))) = mult(mult(B,A),mult(ld(A,B),A)),
inference(copy,[status(thm)],[c_8983]) ).
cnf(c_8984,plain,
mult(unit,A) = mult(ld(A,unit),mult(A,A)),
inference(paramod,[status(thm)],[c_94,c_71]) ).
cnf(c_8985,plain,
A = mult(ld(A,unit),mult(A,A)),
inference(paramod,[status(thm)],[c_19,c_8984]) ).
cnf(c_258,plain,
mult(ld(A,unit),mult(A,A)) = A,
inference(copy,[status(thm)],[c_8985]) ).
cnf(c_269,plain,
ld(ld(A,unit),A) = mult(A,A),
inference(paramod,[status(thm)],[c_258,c_15]) ).
cnf(c_270,plain,
rd(A,mult(A,A)) = ld(A,unit),
inference(paramod,[status(thm)],[c_258,c_17]) ).
cnf(c_282,plain,
rd(A,ld(A,unit)) = mult(A,A),
inference(paramod,[status(thm)],[c_269,c_143]) ).
cnf(c_8986,plain,
rd(f(A),A) = ld(f(A),unit),
inference(paramod,[status(thm)],[c_22,c_270]) ).
cnf(c_8987,plain,
ld(A,f(A)) = ld(f(A),unit),
inference(paramod,[status(thm)],[c_119,c_8986]) ).
cnf(c_284,plain,
ld(f(A),unit) = ld(A,f(A)),
inference(copy,[status(thm)],[c_8987]) ).
cnf(c_8988,plain,
rd(rd(unit,A),A) = mult(rd(unit,A),rd(unit,A)),
inference(paramod,[status(thm)],[c_31,c_282]) ).
cnf(c_8989,plain,
rd(ld(A,unit),A) = mult(rd(unit,A),rd(unit,A)),
inference(paramod,[status(thm)],[c_100,c_8988]) ).
cnf(c_8990,plain,
ld(A,rd(unit,A)) = mult(rd(unit,A),rd(unit,A)),
inference(paramod,[status(thm)],[c_132,c_8989]) ).
cnf(c_8991,plain,
ld(A,ld(A,unit)) = mult(rd(unit,A),rd(unit,A)),
inference(paramod,[status(thm)],[c_100,c_8990]) ).
cnf(c_8992,plain,
ld(A,ld(A,unit)) = mult(ld(A,unit),rd(unit,A)),
inference(paramod,[status(thm)],[c_100,c_8991]) ).
cnf(c_8993,plain,
ld(A,ld(A,unit)) = mult(ld(A,unit),ld(A,unit)),
inference(paramod,[status(thm)],[c_100,c_8992]) ).
cnf(c_289,plain,
mult(ld(A,unit),ld(A,unit)) = ld(A,ld(A,unit)),
inference(copy,[status(thm)],[c_8993]) ).
cnf(c_8994,plain,
rd(ld(ld(A,unit),A),ld(A,unit)) = ld(ld(A,unit),mult(A,A)),
inference(paramod,[status(thm)],[c_282,c_132]) ).
cnf(c_290,plain,
rd(mult(A,A),ld(A,unit)) = ld(ld(A,unit),mult(A,A)),
inference(paramod,[status(thm)],[c_269,c_8994]) ).
cnf(c_8995,plain,
( mult(mult(rd(B,A),mult(A,rd(B,A))),ld(mult(A,rd(B,A)),mult(A,B))) = mult(rd(B,A),mult(A,mult(rd(B,A),ld(mult(A,rd(B,A)),mult(A,B)))))
| mult(A,mult(rd(B,A),mult(A,rd(B,A)))) != mult(mult(A,B),rd(B,A)) ),
inference(paramod,[status(thm)],[c_109,c_46]) ).
cnf(c_8996,plain,
( mult(mult(rd(B,A),mult(A,rd(B,A))),ld(mult(A,rd(B,A)),mult(A,B))) = mult(rd(B,A),mult(A,mult(rd(B,A),ld(mult(A,rd(B,A)),mult(A,B)))))
| mult(A,mult(B,rd(B,A))) != mult(mult(A,B),rd(B,A)) ),
inference(paramod,[status(thm)],[c_39,c_8995]) ).
cnf(c_8997,plain,
( mult(mult(B,rd(B,A)),ld(mult(A,rd(B,A)),mult(A,B))) = mult(rd(B,A),mult(A,mult(rd(B,A),ld(mult(A,rd(B,A)),mult(A,B)))))
| mult(A,mult(B,rd(B,A))) != mult(mult(A,B),rd(B,A)) ),
inference(paramod,[status(thm)],[c_39,c_8996]) ).
cnf(c_8998,plain,
( mult(mult(B,rd(B,A)),A) = mult(rd(B,A),mult(A,mult(rd(B,A),ld(mult(A,rd(B,A)),mult(A,B)))))
| mult(A,mult(B,rd(B,A))) != mult(mult(A,B),rd(B,A)) ),
inference(paramod,[status(thm)],[c_109,c_8997]) ).
cnf(c_8999,plain,
( mult(mult(B,rd(B,A)),A) = mult(rd(B,A),mult(A,mult(rd(B,A),A)))
| mult(A,mult(B,rd(B,A))) != mult(mult(A,B),rd(B,A)) ),
inference(paramod,[status(thm)],[c_109,c_8998]) ).
cnf(c_9000,plain,
( mult(mult(B,rd(B,A)),A) = mult(rd(B,A),mult(A,B))
| mult(A,mult(B,rd(B,A))) != mult(mult(A,B),rd(B,A)) ),
inference(paramod,[status(thm)],[c_16,c_8999]) ).
cnf(c_294,plain,
( mult(mult(B,rd(B,A)),A) = mult(rd(B,A),mult(A,B))
| mult(mult(A,B),rd(B,A)) != mult(A,mult(B,rd(B,A))) ),
inference(copy,[status(thm)],[c_9000]) ).
cnf(c_297,plain,
mult(f(A),ld(A,f(A))) = unit,
inference(paramod,[status(thm)],[c_284,c_14]) ).
cnf(c_298,plain,
mult(A,ld(f(A),unit)) = f(A),
inference(paramod,[status(thm)],[c_284,c_14]) ).
cnf(c_9001,plain,
rd(ld(A,f(A)),f(A)) = ld(f(A),rd(unit,f(A))),
inference(paramod,[status(thm)],[c_284,c_132]) ).
cnf(c_300,plain,
rd(ld(A,f(A)),f(A)) = ld(f(A),ld(f(A),unit)),
inference(paramod,[status(thm)],[c_100,c_9001]) ).
cnf(c_9002,plain,
mult(ld(A,f(A)),unit) = mult(f(A),mult(ld(A,f(A)),ld(A,f(A)))),
inference(paramod,[status(thm)],[c_297,c_197]) ).
cnf(c_9003,plain,
ld(A,f(A)) = mult(f(A),mult(ld(A,f(A)),ld(A,f(A)))),
inference(paramod,[status(thm)],[c_18,c_9002]) ).
cnf(c_308,plain,
mult(f(A),mult(ld(A,f(A)),ld(A,f(A)))) = ld(A,f(A)),
inference(copy,[status(thm)],[c_9003]) ).
cnf(c_9004,plain,
mult(mult(A,mult(B,f(B))),ld(B,f(B))) = mult(mult(A,B),unit),
inference(paramod,[status(thm)],[c_297,c_124]) ).
cnf(c_310,plain,
mult(mult(A,mult(B,f(B))),ld(B,f(B))) = mult(A,B),
inference(paramod,[status(thm)],[c_18,c_9004]) ).
cnf(c_311,plain,
mult(ld(A,f(A)),f(A)) = unit,
inference(paramod,[status(thm)],[c_297,c_120]) ).
cnf(c_368,plain,
ld(rd(A,B),mult(A,B)) = mult(B,B),
inference(paramod,[status(thm)],[c_253,c_15]) ).
cnf(c_369,plain,
rd(mult(A,B),mult(B,B)) = rd(A,B),
inference(paramod,[status(thm)],[c_253,c_17]) ).
cnf(c_395,plain,
ld(A,mult(mult(B,A),mult(ld(A,B),A))) = mult(mult(ld(A,B),A),mult(ld(A,B),A)),
inference(paramod,[status(thm)],[c_76,c_368]) ).
cnf(c_9005,plain,
ld(mult(A,A),mult(A,ld(A,unit))) = mult(ld(A,unit),ld(A,unit)),
inference(paramod,[status(thm)],[c_282,c_368]) ).
cnf(c_9006,plain,
ld(mult(A,A),unit) = mult(ld(A,unit),ld(A,unit)),
inference(paramod,[status(thm)],[c_14,c_9005]) ).
cnf(c_406,plain,
ld(mult(A,A),unit) = ld(A,ld(A,unit)),
inference(paramod,[status(thm)],[c_289,c_9006]) ).
cnf(c_9007,plain,
ld(rd(f(A),ld(A,f(A))),unit) = mult(ld(A,f(A)),ld(A,f(A))),
inference(paramod,[status(thm)],[c_297,c_368]) ).
cnf(c_9008,plain,
ld(A,unit) = mult(ld(A,f(A)),ld(A,f(A))),
inference(paramod,[status(thm)],[c_32,c_9007]) ).
cnf(c_408,plain,
mult(ld(A,f(A)),ld(A,f(A))) = ld(A,unit),
inference(copy,[status(thm)],[c_9008]) ).
cnf(c_9009,plain,
ld(rd(A,ld(f(A),unit)),f(A)) = mult(ld(f(A),unit),ld(f(A),unit)),
inference(paramod,[status(thm)],[c_298,c_368]) ).
cnf(c_409,plain,
ld(rd(A,ld(f(A),unit)),f(A)) = ld(f(A),ld(f(A),unit)),
inference(paramod,[status(thm)],[c_289,c_9009]) ).
cnf(c_415,plain,
mult(f(A),ld(A,unit)) = ld(A,f(A)),
inference(paramod,[status(thm)],[c_408,c_308]) ).
cnf(c_9010,plain,
rd(A,mult(B,B)) = rd(rd(A,B),B),
inference(paramod,[status(thm)],[c_16,c_369]) ).
cnf(c_417,plain,
rd(rd(A,B),B) = rd(A,mult(B,B)),
inference(copy,[status(thm)],[c_9010]) ).
cnf(c_9011,plain,
rd(f(A),mult(ld(f(A),unit),ld(f(A),unit))) = rd(A,ld(f(A),unit)),
inference(paramod,[status(thm)],[c_298,c_369]) ).
cnf(c_431,plain,
rd(f(A),ld(f(A),ld(f(A),unit))) = rd(A,ld(f(A),unit)),
inference(paramod,[status(thm)],[c_289,c_9011]) ).
cnf(c_9012,plain,
rd(unit,mult(f(A),f(A))) = rd(ld(A,f(A)),f(A)),
inference(paramod,[status(thm)],[c_311,c_369]) ).
cnf(c_9013,plain,
rd(unit,A) = rd(ld(A,f(A)),f(A)),
inference(paramod,[status(thm)],[c_22,c_9012]) ).
cnf(c_9014,plain,
ld(A,unit) = rd(ld(A,f(A)),f(A)),
inference(paramod,[status(thm)],[c_100,c_9013]) ).
cnf(c_432,plain,
rd(ld(A,f(A)),f(A)) = ld(A,unit),
inference(copy,[status(thm)],[c_9014]) ).
cnf(c_9015,plain,
ld(A,unit) = ld(f(A),ld(f(A),unit)),
inference(paramod,[status(thm)],[c_432,c_300]) ).
cnf(c_437,plain,
ld(f(A),ld(f(A),unit)) = ld(A,unit),
inference(copy,[status(thm)],[c_9015]) ).
cnf(c_441,plain,
rd(f(A),ld(A,unit)) = rd(A,ld(f(A),unit)),
inference(paramod,[status(thm)],[c_437,c_431]) ).
cnf(c_442,plain,
ld(rd(A,ld(f(A),unit)),f(A)) = ld(A,unit),
inference(paramod,[status(thm)],[c_437,c_409]) ).
cnf(c_444,plain,
ld(f(A),ld(A,f(A))) = ld(A,unit),
inference(paramod,[status(thm)],[c_415,c_15]) ).
cnf(c_445,plain,
rd(ld(A,f(A)),ld(A,unit)) = f(A),
inference(paramod,[status(thm)],[c_415,c_17]) ).
cnf(c_455,plain,
ld(mult(f(A),rd(ld(A,unit),f(A))),ld(A,f(A))) = f(A),
inference(paramod,[status(thm)],[c_415,c_109]) ).
cnf(c_9016,plain,
rd(ld(A,f(A)),f(A)) = mult(f(A),rd(ld(A,unit),f(A))),
inference(paramod,[status(thm)],[c_415,c_152]) ).
cnf(c_9017,plain,
ld(A,unit) = mult(f(A),rd(ld(A,unit),f(A))),
inference(paramod,[status(thm)],[c_432,c_9016]) ).
cnf(c_456,plain,
mult(f(A),rd(ld(A,unit),f(A))) = ld(A,unit),
inference(copy,[status(thm)],[c_9017]) ).
cnf(c_466,plain,
mult(ld(A,unit),f(A)) = ld(A,f(A)),
inference(paramod,[status(thm)],[c_444,c_200]) ).
cnf(c_467,plain,
ld(ld(A,unit),ld(A,f(A))) = f(A),
inference(paramod,[status(thm)],[c_456,c_455]) ).
cnf(c_9018,plain,
rd(mult(A,A),ld(A,ld(A,unit))) = mult(mult(A,A),mult(A,A)),
inference(paramod,[status(thm)],[c_406,c_282]) ).
cnf(c_540,plain,
rd(mult(A,A),ld(A,ld(A,unit))) = mult(A,mult(A,mult(A,A))),
inference(paramod,[status(thm)],[c_49,c_9018]) ).
cnf(c_545,plain,
mult(rd(A,mult(B,B)),B) = rd(A,B),
inference(paramod,[status(thm)],[c_417,c_16]) ).
cnf(c_9019,plain,
rd(ld(ld(A,unit),ld(A,f(A))),ld(A,unit)) = ld(ld(A,unit),f(A)),
inference(paramod,[status(thm)],[c_445,c_132]) ).
cnf(c_9020,plain,
rd(f(A),ld(A,unit)) = ld(ld(A,unit),f(A)),
inference(paramod,[status(thm)],[c_467,c_9019]) ).
cnf(c_597,plain,
rd(A,ld(f(A),unit)) = ld(ld(A,unit),f(A)),
inference(paramod,[status(thm)],[c_441,c_9020]) ).
cnf(c_605,plain,
ld(ld(ld(A,unit),f(A)),f(A)) = ld(A,unit),
inference(paramod,[status(thm)],[c_597,c_442]) ).
cnf(c_608,plain,
mult(rd(A,B),f(B)) = rd(A,f(B)),
inference(paramod,[status(thm)],[c_22,c_545]) ).
cnf(c_9021,plain,
mult(A,f(B)) = rd(mult(A,B),f(B)),
inference(paramod,[status(thm)],[c_17,c_608]) ).
cnf(c_630,plain,
rd(mult(A,B),f(B)) = mult(A,f(B)),
inference(copy,[status(thm)],[c_9021]) ).
cnf(c_662,plain,
ld(mult(A,f(B)),mult(A,B)) = f(B),
inference(paramod,[status(thm)],[c_630,c_31]) ).
cnf(c_9022,plain,
rd(f(A),mult(B,f(A))) = ld(mult(B,f(A)),rd(mult(B,A),mult(B,f(A)))),
inference(paramod,[status(thm)],[c_662,c_132]) ).
cnf(c_739,plain,
ld(mult(A,f(B)),rd(mult(A,B),mult(A,f(B)))) = rd(f(B),mult(A,f(B))),
inference(copy,[status(thm)],[c_9022]) ).
cnf(c_9023,plain,
mult(rd(mult(A,A),mult(ld(A,unit),ld(A,unit))),ld(A,unit)) = ld(ld(A,unit),mult(A,A)),
inference(paramod,[status(thm)],[c_290,c_545]) ).
cnf(c_9024,plain,
mult(rd(mult(A,A),ld(A,ld(A,unit))),ld(A,unit)) = ld(ld(A,unit),mult(A,A)),
inference(paramod,[status(thm)],[c_289,c_9023]) ).
cnf(c_9025,plain,
mult(mult(A,mult(A,mult(A,A))),ld(A,unit)) = ld(ld(A,unit),mult(A,A)),
inference(paramod,[status(thm)],[c_540,c_9024]) ).
cnf(c_9026,plain,
mult(A,mult(A,mult(A,mult(A,ld(A,unit))))) = ld(ld(A,unit),mult(A,A)),
inference(paramod,[status(thm)],[c_238,c_9025]) ).
cnf(c_9027,plain,
mult(A,mult(A,mult(A,unit))) = ld(ld(A,unit),mult(A,A)),
inference(paramod,[status(thm)],[c_14,c_9026]) ).
cnf(c_9028,plain,
mult(A,mult(A,A)) = ld(ld(A,unit),mult(A,A)),
inference(paramod,[status(thm)],[c_18,c_9027]) ).
cnf(c_1216,plain,
ld(ld(A,unit),mult(A,A)) = mult(A,mult(A,A)),
inference(copy,[status(thm)],[c_9028]) ).
cnf(c_1227,plain,
rd(mult(A,A),ld(A,unit)) = mult(A,mult(A,A)),
inference(paramod,[status(thm)],[c_1216,c_290]) ).
cnf(c_9029,plain,
rd(A,ld(f(A),unit)) = mult(f(A),mult(f(A),f(A))),
inference(paramod,[status(thm)],[c_22,c_1227]) ).
cnf(c_9030,plain,
ld(ld(A,unit),f(A)) = mult(f(A),mult(f(A),f(A))),
inference(paramod,[status(thm)],[c_597,c_9029]) ).
cnf(c_9031,plain,
ld(ld(A,unit),f(A)) = mult(f(A),A),
inference(paramod,[status(thm)],[c_22,c_9030]) ).
cnf(c_1271,plain,
ld(ld(A,unit),f(A)) = mult(A,f(A)),
inference(paramod,[status(thm)],[c_44,c_9031]) ).
cnf(c_1291,plain,
ld(mult(A,f(A)),f(A)) = ld(A,unit),
inference(paramod,[status(thm)],[c_1271,c_605]) ).
cnf(c_1325,plain,
mult(ld(A,unit),mult(A,f(A))) = f(A),
inference(paramod,[status(thm)],[c_1291,c_188]) ).
cnf(c_9032,plain,
mult(mult(ld(A,B),B),A) = mult(mult(unit,ld(A,B)),mult(B,A)),
inference(paramod,[status(thm)],[c_19,c_64]) ).
cnf(c_1373,plain,
mult(mult(ld(A,B),B),A) = mult(ld(A,B),mult(B,A)),
inference(paramod,[status(thm)],[c_19,c_9032]) ).
cnf(c_9033,plain,
mult(mult(A,ld(A,B)),mult(B,A)) = mult(A,mult(mult(ld(A,B),B),A)),
inference(paramod,[status(thm)],[c_64,c_21]) ).
cnf(c_9034,plain,
mult(B,mult(B,A)) = mult(A,mult(mult(ld(A,B),B),A)),
inference(paramod,[status(thm)],[c_14,c_9033]) ).
cnf(c_9035,plain,
mult(B,mult(B,A)) = mult(A,mult(ld(A,B),mult(B,A))),
inference(paramod,[status(thm)],[c_1373,c_9034]) ).
cnf(c_1374,plain,
mult(A,mult(ld(A,B),mult(B,A))) = mult(B,mult(B,A)),
inference(copy,[status(thm)],[c_9035]) ).
cnf(c_9036,plain,
mult(mult(A,B),rd(B,A)) = mult(mult(unit,A),mult(B,rd(B,A))),
inference(paramod,[status(thm)],[c_19,c_67]) ).
cnf(c_1910,plain,
mult(mult(A,B),rd(B,A)) = mult(A,mult(B,rd(B,A))),
inference(paramod,[status(thm)],[c_19,c_9036]) ).
cnf(c_9037,plain,
( mult(mult(B,rd(B,A)),A) = mult(rd(B,A),mult(A,B))
| mult(A,mult(B,rd(B,A))) != mult(A,mult(B,rd(B,A))) ),
inference(paramod,[status(thm)],[c_1910,c_294]) ).
cnf(c_1967,plain,
mult(mult(A,rd(A,B)),B) = mult(rd(A,B),mult(B,A)),
inference(copy,[status(thm)],[c_9037]) ).
cnf(c_2010,plain,
ld(mult(A,A),mult(A,B)) = ld(A,B),
inference(paramod,[status(thm)],[c_14,c_217]) ).
cnf(c_2018,plain,
ld(A,mult(f(A),B)) = ld(f(A),B),
inference(paramod,[status(thm)],[c_22,c_2010]) ).
cnf(c_2019,plain,
rd(mult(A,B),ld(A,B)) = mult(A,A),
inference(paramod,[status(thm)],[c_2010,c_32]) ).
cnf(c_2061,plain,
rd(mult(rd(A,B),A),B) = mult(rd(A,B),rd(A,B)),
inference(paramod,[status(thm)],[c_31,c_2019]) ).
cnf(c_9038,plain,
rd(mult(mult(A,B),mult(A,mult(B,A))),A) = mult(mult(A,B),mult(A,B)),
inference(paramod,[status(thm)],[c_38,c_2019]) ).
cnf(c_9039,plain,
rd(mult(A,mult(B,mult(A,mult(B,A)))),A) = mult(mult(A,B),mult(A,B)),
inference(paramod,[status(thm)],[c_73,c_9038]) ).
cnf(c_2064,plain,
mult(A,rd(mult(B,mult(A,mult(B,A))),A)) = mult(mult(A,B),mult(A,B)),
inference(paramod,[status(thm)],[c_152,c_9039]) ).
cnf(c_2196,plain,
mult(A,ld(f(A),B)) = mult(f(A),B),
inference(paramod,[status(thm)],[c_2018,c_14]) ).
cnf(c_9040,plain,
rd(mult(A,mult(B,mult(A,B))),B) = mult(unit,mult(A,mult(B,A))),
inference(paramod,[status(thm)],[c_19,c_70]) ).
cnf(c_2851,plain,
rd(mult(A,mult(B,mult(A,B))),B) = mult(A,mult(B,A)),
inference(paramod,[status(thm)],[c_19,c_9040]) ).
cnf(c_9041,plain,
mult(A,mult(B,mult(A,B))) = mult(mult(A,B),mult(A,B)),
inference(paramod,[status(thm)],[c_2851,c_2064]) ).
cnf(c_2931,plain,
mult(mult(A,B),mult(A,B)) = mult(A,mult(B,mult(A,B))),
inference(copy,[status(thm)],[c_9041]) ).
cnf(c_9042,plain,
ld(A,mult(mult(B,A),mult(ld(A,B),A))) = mult(ld(A,B),mult(A,mult(ld(A,B),A))),
inference(paramod,[status(thm)],[c_2931,c_395]) ).
cnf(c_2977,plain,
ld(A,mult(mult(B,A),mult(ld(A,B),A))) = mult(ld(A,B),mult(B,A)),
inference(paramod,[status(thm)],[c_37,c_9042]) ).
cnf(c_9043,plain,
mult(A,mult(ld(A,B),mult(A,mult(ld(A,B),A)))) = mult(mult(B,A),mult(ld(A,B),A)),
inference(paramod,[status(thm)],[c_2931,c_257]) ).
cnf(c_9044,plain,
mult(A,mult(ld(A,B),mult(B,A))) = mult(mult(B,A),mult(ld(A,B),A)),
inference(paramod,[status(thm)],[c_37,c_9043]) ).
cnf(c_9045,plain,
mult(B,mult(B,A)) = mult(mult(B,A),mult(ld(A,B),A)),
inference(paramod,[status(thm)],[c_1374,c_9044]) ).
cnf(c_2979,plain,
mult(mult(A,B),mult(ld(B,A),B)) = mult(A,mult(A,B)),
inference(copy,[status(thm)],[c_9045]) ).
cnf(c_9046,plain,
ld(A,mult(B,mult(B,A))) = mult(ld(A,B),mult(B,A)),
inference(paramod,[status(thm)],[c_2979,c_2977]) ).
cnf(c_3000,plain,
mult(ld(A,mult(B,B)),A) = mult(ld(A,B),mult(B,A)),
inference(paramod,[status(thm)],[c_223,c_9046]) ).
cnf(c_9047,plain,
mult(ld(A,mult(rd(B,A),rd(B,A))),A) = ld(A,mult(rd(B,A),B)),
inference(paramod,[status(thm)],[c_2061,c_93]) ).
cnf(c_9048,plain,
mult(ld(A,rd(B,A)),mult(rd(B,A),A)) = ld(A,mult(rd(B,A),B)),
inference(paramod,[status(thm)],[c_3000,c_9047]) ).
cnf(c_9049,plain,
mult(ld(A,rd(B,A)),B) = ld(A,mult(rd(B,A),B)),
inference(paramod,[status(thm)],[c_16,c_9048]) ).
cnf(c_3006,plain,
ld(A,mult(rd(B,A),B)) = mult(ld(A,rd(B,A)),B),
inference(copy,[status(thm)],[c_9049]) ).
cnf(c_3267,plain,
mult(A,mult(ld(A,rd(B,A)),B)) = mult(rd(B,A),B),
inference(paramod,[status(thm)],[c_3006,c_14]) ).
cnf(c_3426,plain,
ld(f(A),mult(A,B)) = mult(f(A),B),
inference(paramod,[status(thm)],[c_220,c_15]) ).
cnf(c_9050,plain,
mult(mult(f(A),f(A)),mult(f(A),B)) = mult(f(A),mult(A,B)),
inference(paramod,[status(thm)],[c_220,c_49]) ).
cnf(c_9051,plain,
mult(A,mult(f(A),B)) = mult(f(A),mult(A,B)),
inference(paramod,[status(thm)],[c_22,c_9050]) ).
cnf(c_3435,plain,
mult(f(A),mult(A,B)) = mult(A,mult(f(A),B)),
inference(copy,[status(thm)],[c_9051]) ).
cnf(c_3489,plain,
mult(mult(A,f(A)),B) = mult(A,mult(f(A),B)),
inference(paramod,[status(thm)],[c_3435,c_242]) ).
cnf(c_9052,plain,
ld(f(A),B) = mult(f(A),ld(A,B)),
inference(paramod,[status(thm)],[c_14,c_3426]) ).
cnf(c_3496,plain,
mult(f(A),ld(A,B)) = ld(f(A),B),
inference(copy,[status(thm)],[c_9052]) ).
cnf(c_9053,plain,
mult(mult(rd(A,mult(mult(B,f(B)),f(B))),mult(B,f(B))),mult(ld(B,unit),mult(mult(B,f(B)),ld(B,unit)))) = mult(A,ld(B,unit)),
inference(paramod,[status(thm)],[c_1325,c_68]) ).
cnf(c_9054,plain,
mult(mult(rd(A,mult(B,mult(f(B),f(B)))),mult(B,f(B))),mult(ld(B,unit),mult(mult(B,f(B)),ld(B,unit)))) = mult(A,ld(B,unit)),
inference(paramod,[status(thm)],[c_71,c_9053]) ).
cnf(c_9055,plain,
mult(mult(rd(A,mult(B,B)),mult(B,f(B))),mult(ld(B,unit),mult(mult(B,f(B)),ld(B,unit)))) = mult(A,ld(B,unit)),
inference(paramod,[status(thm)],[c_22,c_9054]) ).
cnf(c_9056,plain,
mult(mult(rd(A,mult(B,B)),mult(B,f(B))),mult(ld(B,unit),mult(B,mult(f(B),ld(B,unit))))) = mult(A,ld(B,unit)),
inference(paramod,[status(thm)],[c_3489,c_9055]) ).
cnf(c_9057,plain,
mult(mult(rd(A,mult(B,B)),mult(B,f(B))),mult(ld(B,unit),mult(B,ld(f(B),unit)))) = mult(A,ld(B,unit)),
inference(paramod,[status(thm)],[c_3496,c_9056]) ).
cnf(c_9058,plain,
mult(mult(rd(A,mult(B,B)),mult(B,f(B))),mult(ld(B,unit),mult(f(B),unit))) = mult(A,ld(B,unit)),
inference(paramod,[status(thm)],[c_2196,c_9057]) ).
cnf(c_9059,plain,
mult(mult(rd(A,mult(B,B)),mult(B,f(B))),mult(ld(B,unit),f(B))) = mult(A,ld(B,unit)),
inference(paramod,[status(thm)],[c_18,c_9058]) ).
cnf(c_9060,plain,
mult(mult(rd(A,mult(B,B)),mult(B,f(B))),ld(B,f(B))) = mult(A,ld(B,unit)),
inference(paramod,[status(thm)],[c_466,c_9059]) ).
cnf(c_9061,plain,
mult(rd(A,mult(B,B)),B) = mult(A,ld(B,unit)),
inference(paramod,[status(thm)],[c_310,c_9060]) ).
cnf(c_9062,plain,
rd(A,B) = mult(A,ld(B,unit)),
inference(paramod,[status(thm)],[c_545,c_9061]) ).
cnf(c_4042,plain,
mult(A,ld(B,unit)) = rd(A,B),
inference(copy,[status(thm)],[c_9062]) ).
cnf(c_4463,plain,
ld(A,rd(A,B)) = ld(B,unit),
inference(paramod,[status(thm)],[c_4042,c_15]) ).
cnf(c_9063,plain,
mult(A,B) = rd(A,rd(unit,B)),
inference(paramod,[status(thm)],[c_31,c_4042]) ).
cnf(c_9064,plain,
mult(A,B) = rd(A,ld(B,unit)),
inference(paramod,[status(thm)],[c_100,c_9063]) ).
cnf(c_4475,plain,
rd(A,ld(B,unit)) = mult(A,B),
inference(copy,[status(thm)],[c_9064]) ).
cnf(c_9065,plain,
rd(mult(A,rd(A,B)),ld(B,unit)) = mult(A,A),
inference(paramod,[status(thm)],[c_4042,c_218]) ).
cnf(c_9066,plain,
mult(mult(A,rd(A,B)),B) = mult(A,A),
inference(paramod,[status(thm)],[c_4475,c_9065]) ).
cnf(c_4528,plain,
mult(rd(A,B),mult(B,A)) = mult(A,A),
inference(paramod,[status(thm)],[c_1967,c_9066]) ).
cnf(c_9067,plain,
mult(f(A),rd(f(A),B)) = mult(A,ld(B,unit)),
inference(paramod,[status(thm)],[c_4042,c_220]) ).
cnf(c_4529,plain,
mult(f(A),rd(f(A),B)) = rd(A,B),
inference(paramod,[status(thm)],[c_4042,c_9067]) ).
cnf(c_9068,plain,
mult(rd(ld(A,B),A),B) = mult(ld(A,B),ld(A,B)),
inference(paramod,[status(thm)],[c_14,c_4528]) ).
cnf(c_5552,plain,
mult(ld(A,rd(B,A)),B) = mult(ld(A,B),ld(A,B)),
inference(paramod,[status(thm)],[c_132,c_9068]) ).
cnf(c_9069,plain,
mult(A,mult(ld(A,B),ld(A,B))) = mult(rd(B,A),B),
inference(paramod,[status(thm)],[c_5552,c_3267]) ).
cnf(c_9070,plain,
mult(B,ld(A,B)) = mult(rd(B,A),B),
inference(paramod,[status(thm)],[c_252,c_9069]) ).
cnf(c_5661,plain,
mult(rd(A,B),A) = mult(A,ld(B,A)),
inference(copy,[status(thm)],[c_9070]) ).
cnf(c_9071,plain,
ld(A,mult(A,ld(B,A))) = mult(ld(A,rd(A,B)),A),
inference(paramod,[status(thm)],[c_5661,c_75]) ).
cnf(c_9072,plain,
ld(B,A) = mult(ld(A,rd(A,B)),A),
inference(paramod,[status(thm)],[c_15,c_9071]) ).
cnf(c_9073,plain,
ld(B,A) = mult(ld(B,unit),A),
inference(paramod,[status(thm)],[c_4463,c_9072]) ).
cnf(c_5942,plain,
mult(ld(A,unit),B) = ld(A,B),
inference(copy,[status(thm)],[c_9073]) ).
cnf(c_6358,plain,
rd(ld(A,B),B) = ld(A,unit),
inference(paramod,[status(thm)],[c_5942,c_17]) ).
cnf(c_6596,plain,
rd(A,mult(B,A)) = ld(B,unit),
inference(paramod,[status(thm)],[c_15,c_6358]) ).
cnf(c_6620,plain,
ld(mult(A,f(B)),rd(mult(A,B),mult(A,f(B)))) = ld(A,unit),
inference(paramod,[status(thm)],[c_6596,c_739]) ).
cnf(c_9074,plain,
mult(mult(A,mult(B,f(C))),mult(f(C),ld(mult(B,f(C)),rd(mult(B,C),mult(B,f(C)))))) = mult(mult(A,mult(B,C)),ld(mult(B,f(C)),rd(mult(B,C),mult(B,f(C))))),
inference(paramod,[status(thm)],[c_662,c_137]) ).
cnf(c_9075,plain,
mult(mult(A,mult(B,f(C))),mult(f(C),ld(B,unit))) = mult(mult(A,mult(B,C)),ld(mult(B,f(C)),rd(mult(B,C),mult(B,f(C))))),
inference(paramod,[status(thm)],[c_6620,c_9074]) ).
cnf(c_9076,plain,
mult(mult(A,mult(B,f(C))),rd(f(C),B)) = mult(mult(A,mult(B,C)),ld(mult(B,f(C)),rd(mult(B,C),mult(B,f(C))))),
inference(paramod,[status(thm)],[c_4042,c_9075]) ).
cnf(c_9077,plain,
mult(mult(A,B),mult(f(C),rd(f(C),B))) = mult(mult(A,mult(B,C)),ld(mult(B,f(C)),rd(mult(B,C),mult(B,f(C))))),
inference(paramod,[status(thm)],[c_67,c_9076]) ).
cnf(c_9078,plain,
mult(mult(A,B),rd(C,B)) = mult(mult(A,mult(B,C)),ld(mult(B,f(C)),rd(mult(B,C),mult(B,f(C))))),
inference(paramod,[status(thm)],[c_4529,c_9077]) ).
cnf(c_9079,plain,
mult(mult(A,B),rd(C,B)) = mult(mult(A,mult(B,C)),ld(B,unit)),
inference(paramod,[status(thm)],[c_6620,c_9078]) ).
cnf(c_9080,plain,
mult(mult(A,B),rd(C,B)) = rd(mult(A,mult(B,C)),B),
inference(paramod,[status(thm)],[c_4042,c_9079]) ).
cnf(c_8823,plain,
rd(mult(A,mult(B,C)),B) = mult(mult(A,B),rd(C,B)),
inference(copy,[status(thm)],[c_9080]) ).
cnf(c_9081,plain,
mult(mult(mult(A,B),C),rd(mult(B,C),C)) = mult(A,mult(B,mult(C,B))),
inference(paramod,[status(thm)],[c_8823,c_70]) ).
cnf(c_8918,plain,
mult(mult(mult(A,B),C),B) = mult(A,mult(B,mult(C,B))),
inference(paramod,[status(thm)],[c_17,c_9081]) ).
cnf(c_8919,plain,
$false,
inference(resolve,[status(thm)],[c_8918,c_63]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRP667+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/5.44 % Computer : n018.cluster.edu
% 0.17/5.44 % Model : x86_64 x86_64
% 0.17/5.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/5.44 % Memory : 8046.5625MB
% 0.17/5.44 % OS : Linux 6.8.0-71-generic
% 0.17/5.44 % CPULimit : 300
% 0.17/5.44 % WCLimit : 300
% 0.17/5.44 % DateTime : Fri Sep 25 15:36:26 UTC 2026
% 0.17/5.44 % CPUTime :
% 0.17/5.44 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.17/5.44 % Process 2311583 was started by sandbox2 on n018,
% 0.17/5.44 % Fri Sep 25 15:36:26 2026
% 0.17/5.44 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.17/5.45
% 0.17/5.45 % From the command line: assign(max_seconds, 300).
% 19.53/7.95
% 19.53/7.95 % Assigning unary symbol f kb_weight 0 and highest precedence (9).
% 19.53/7.95
% 19.53/7.95 % SZS status Theorem for theBenchmark
% 19.53/7.95
% 19.53/7.95 % Proof 1 at 1.96 (+ 0.51) seconds.
% 19.53/7.95 % Length of proof is 161.
% 19.53/7.95 % Level of proof is 28.
% 19.53/7.95 % Maximum clause weight is 98.000.
% 19.53/7.95 % Given clauses 246.
% 19.53/7.95
% 19.53/7.95 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------