%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP654-12 : TPTP v9.3.1. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n007.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:30:51 AM UTC 2026
% Result : Unsatisfiable 37.02s 5.24s
% Output : CNFRefutation 37.02s
% Verified :
% SZS Type : Refutation
% Derivation depth : 107
% Number of leaves : 6
% Syntax : Number of formulae : 339 ( 339 unt; 0 def)
% Number of atoms : 339 ( 338 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 13 ( 13 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 2 con; 0-2 aty)
% Number of variables : 828 ( 0 sgn 11 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f01,axiom,
! [VAR_0,VAR_1] : mult(VAR_0,ld(VAR_0,VAR_1)) = VAR_1,
file('theBenchmark.p',f01) ).
cnf(c_1,plain,
mult(A,ld(A,B)) = B,
inference(clausify,[status(thm)],[f01]) ).
fof(f02,axiom,
! [VAR_0,VAR_1] : ld(VAR_0,mult(VAR_0,VAR_1)) = VAR_1,
file('theBenchmark.p',f02) ).
cnf(c_2,plain,
ld(A,mult(A,B)) = B,
inference(clausify,[status(thm)],[f02]) ).
fof(f03,axiom,
! [VAR_0,VAR_1] : mult(rd(VAR_0,VAR_1),VAR_1) = VAR_0,
file('theBenchmark.p',f03) ).
cnf(c_3,plain,
mult(rd(A,B),B) = A,
inference(clausify,[status(thm)],[f03]) ).
fof(f04,axiom,
! [VAR_0,VAR_1] : rd(mult(VAR_0,VAR_1),VAR_1) = VAR_0,
file('theBenchmark.p',f04) ).
cnf(c_4,plain,
rd(mult(A,B),B) = A,
inference(clausify,[status(thm)],[f04]) ).
fof(f05,axiom,
! [VAR_0,VAR_1,VAR_2] : mult(VAR_0,mult(VAR_1,mult(VAR_0,VAR_2))) = mult(mult(mult(VAR_0,VAR_1),VAR_0),VAR_2),
file('theBenchmark.p',f05) ).
cnf(c_5,plain,
mult(A,mult(B,mult(A,C))) = mult(mult(mult(A,B),A),C),
inference(clausify,[status(thm)],[f05]) ).
cnf(c_6,plain,
mult(mult(mult(A,B),A),C) = mult(A,mult(B,mult(A,C))),
inference(copy,[status(thm)],[c_5]) ).
fof(goal,axiom,
mult(rd(x1,x1),x0) != x0,
file('theBenchmark.p',goal) ).
cnf(c_7,plain,
mult(rd(x1,x1),x0) != x0,
inference(clausify,[status(thm)],[goal]) ).
cnf(c_8,plain,
ld(rd(A,B),A) = B,
inference(paramod,[status(thm)],[c_3,c_2]) ).
cnf(c_9,plain,
rd(A,ld(B,A)) = B,
inference(paramod,[status(thm)],[c_1,c_4]) ).
cnf(c_10,plain,
mult(A,mult(B,mult(A,ld(mult(mult(A,B),A),C)))) = C,
inference(paramod,[status(thm)],[c_6,c_1]) ).
cnf(c_7345,plain,
mult(mult(A,B),C) = mult(B,mult(ld(B,A),mult(B,C))),
inference(paramod,[status(thm)],[c_1,c_6]) ).
cnf(c_11,plain,
mult(A,mult(ld(A,B),mult(A,C))) = mult(mult(B,A),C),
inference(copy,[status(thm)],[c_7345]) ).
cnf(c_14,plain,
rd(mult(A,mult(B,mult(A,C))),C) = mult(mult(A,B),A),
inference(paramod,[status(thm)],[c_6,c_4]) ).
cnf(c_15,plain,
mult(mult(A,mult(B,mult(A,mult(A,B)))),C) = mult(mult(A,B),mult(A,mult(mult(A,B),C))),
inference(paramod,[status(thm)],[c_6,c_6]) ).
cnf(c_7346,plain,
ld(A,B) = mult(C,mult(A,ld(mult(mult(A,C),A),B))),
inference(paramod,[status(thm)],[c_10,c_2]) ).
cnf(c_16,plain,
mult(A,mult(B,ld(mult(mult(B,A),B),C))) = ld(B,C),
inference(copy,[status(thm)],[c_7346]) ).
cnf(c_7347,plain,
mult(A,mult(ld(A,B),C)) = mult(mult(B,A),ld(A,C)),
inference(paramod,[status(thm)],[c_1,c_11]) ).
cnf(c_18,plain,
mult(mult(A,B),ld(B,C)) = mult(B,mult(ld(B,A),C)),
inference(copy,[status(thm)],[c_7347]) ).
cnf(c_19,plain,
ld(A,mult(mult(B,A),C)) = mult(ld(A,B),mult(A,C)),
inference(paramod,[status(thm)],[c_11,c_2]) ).
cnf(c_20,plain,
mult(rd(A,B),mult(ld(rd(A,B),C),A)) = mult(mult(C,rd(A,B)),B),
inference(paramod,[status(thm)],[c_3,c_11]) ).
cnf(c_7348,plain,
mult(A,mult(ld(A,B),mult(mult(C,A),D))) = mult(mult(B,A),mult(ld(A,C),mult(A,D))),
inference(paramod,[status(thm)],[c_11,c_11]) ).
cnf(c_23,plain,
mult(mult(A,B),mult(ld(B,C),mult(B,D))) = mult(B,mult(ld(B,A),mult(mult(C,B),D))),
inference(copy,[status(thm)],[c_7348]) ).
cnf(c_7349,plain,
mult(A,ld(ld(B,A),C)) = mult(ld(B,A),mult(ld(ld(B,A),B),C)),
inference(paramod,[status(thm)],[c_1,c_18]) ).
cnf(c_24,plain,
mult(ld(A,B),mult(ld(ld(A,B),A),C)) = mult(B,ld(ld(A,B),C)),
inference(copy,[status(thm)],[c_7349]) ).
cnf(c_25,plain,
mult(mult(A,B),ld(B,ld(ld(B,A),C))) = mult(B,C),
inference(paramod,[status(thm)],[c_1,c_18]) ).
cnf(c_26,plain,
ld(mult(A,B),mult(B,mult(ld(B,A),C))) = ld(B,C),
inference(paramod,[status(thm)],[c_18,c_2]) ).
cnf(c_29,plain,
rd(mult(mult(A,B),ld(B,C)),mult(ld(B,A),C)) = B,
inference(paramod,[status(thm)],[c_18,c_4]) ).
cnf(c_42,plain,
mult(mult(A,mult(ld(A,B),C)),ld(ld(A,C),D)) = mult(ld(A,C),mult(ld(ld(A,C),mult(B,A)),D)),
inference(paramod,[status(thm)],[c_18,c_18]) ).
cnf(c_43,plain,
mult(mult(mult(A,B),ld(B,C)),ld(mult(ld(B,A),C),D)) = mult(mult(ld(B,A),C),mult(ld(mult(ld(B,A),C),B),D)),
inference(paramod,[status(thm)],[c_18,c_18]) ).
cnf(c_46,plain,
rd(mult(A,ld(B,C)),mult(ld(B,rd(A,B)),C)) = B,
inference(paramod,[status(thm)],[c_3,c_29]) ).
cnf(c_53,plain,
rd(A,mult(ld(B,rd(B,B)),A)) = B,
inference(paramod,[status(thm)],[c_1,c_46]) ).
cnf(c_7350,plain,
ld(A,mult(B,ld(A,C))) = mult(ld(A,rd(B,A)),C),
inference(paramod,[status(thm)],[c_46,c_8]) ).
cnf(c_58,plain,
mult(ld(A,rd(B,A)),C) = ld(A,mult(B,ld(A,C))),
inference(copy,[status(thm)],[c_7350]) ).
cnf(c_64,plain,
mult(ld(A,rd(A,A)),B) = ld(A,B),
inference(paramod,[status(thm)],[c_1,c_58]) ).
cnf(c_68,plain,
rd(ld(A,mult(B,ld(A,C))),C) = ld(A,rd(B,A)),
inference(paramod,[status(thm)],[c_58,c_4]) ).
cnf(c_7351,plain,
mult(A,mult(mult(ld(A,rd(B,A)),C),mult(A,D))) = mult(mult(mult(B,ld(A,C)),A),D),
inference(paramod,[status(thm)],[c_58,c_11]) ).
cnf(c_78,plain,
mult(mult(mult(A,ld(B,C)),B),D) = mult(B,mult(mult(ld(B,rd(A,B)),C),mult(B,D))),
inference(copy,[status(thm)],[c_7351]) ).
cnf(c_93,plain,
mult(A,mult(ld(A,rd(A,A)),B)) = B,
inference(paramod,[status(thm)],[c_64,c_1]) ).
cnf(c_95,plain,
mult(ld(A,rd(A,A)),mult(A,B)) = B,
inference(paramod,[status(thm)],[c_64,c_2]) ).
cnf(c_96,plain,
rd(ld(A,B),B) = ld(A,rd(A,A)),
inference(paramod,[status(thm)],[c_64,c_4]) ).
cnf(c_97,plain,
mult(mult(ld(A,B),ld(A,rd(A,A))),C) = mult(ld(A,rd(A,A)),mult(B,mult(ld(A,rd(A,A)),C))),
inference(paramod,[status(thm)],[c_64,c_6]) ).
cnf(c_148,plain,
rd(mult(A,B),C) = mult(mult(A,rd(B,mult(A,C))),A),
inference(paramod,[status(thm)],[c_3,c_14]) ).
cnf(c_163,plain,
rd(A,mult(B,A)) = ld(B,rd(B,B)),
inference(paramod,[status(thm)],[c_2,c_96]) ).
cnf(c_7352,plain,
mult(A,rd(B,mult(A,B))) = rd(A,A),
inference(paramod,[status(thm)],[c_163,c_1]) ).
cnf(c_168,plain,
rd(A,A) = mult(A,rd(B,mult(A,B))),
inference(copy,[status(thm)],[c_7352]) ).
cnf(c_7353,plain,
mult(mult(rd(A,A),A),ld(A,B)) = mult(A,mult(rd(C,mult(A,C)),B)),
inference(paramod,[status(thm)],[c_163,c_18]) ).
cnf(c_7354,plain,
mult(A,ld(A,B)) = mult(A,mult(rd(C,mult(A,C)),B)),
inference(paramod,[status(thm)],[c_3,c_7353]) ).
cnf(c_7355,plain,
B = mult(A,mult(rd(C,mult(A,C)),B)),
inference(paramod,[status(thm)],[c_1,c_7354]) ).
cnf(c_173,plain,
mult(A,mult(rd(B,mult(A,B)),C)) = C,
inference(copy,[status(thm)],[c_7355]) ).
cnf(c_7356,plain,
mult(rd(A,mult(B,A)),C) = ld(B,mult(B,ld(B,C))),
inference(paramod,[status(thm)],[c_163,c_58]) ).
cnf(c_177,plain,
mult(rd(A,mult(B,A)),C) = ld(B,C),
inference(paramod,[status(thm)],[c_1,c_7356]) ).
cnf(c_187,plain,
rd(A,mult(B,A)) = rd(C,mult(B,C)),
inference(paramod,[status(thm)],[c_163,c_163]) ).
cnf(c_190,plain,
mult(rd(A,mult(B,A)),mult(B,C)) = C,
inference(paramod,[status(thm)],[c_187,c_3]) ).
cnf(c_7357,plain,
rd(A,B) = rd(C,mult(rd(B,A),C)),
inference(paramod,[status(thm)],[c_3,c_187]) ).
cnf(c_191,plain,
rd(A,mult(rd(B,C),A)) = rd(C,B),
inference(copy,[status(thm)],[c_7357]) ).
cnf(c_193,plain,
ld(rd(A,mult(B,A)),C) = mult(B,C),
inference(paramod,[status(thm)],[c_187,c_8]) ).
cnf(c_201,plain,
rd(rd(A,B),rd(A,B)) = mult(rd(A,B),rd(B,A)),
inference(paramod,[status(thm)],[c_3,c_168]) ).
cnf(c_7358,plain,
rd(ld(A,rd(A,A)),ld(A,rd(A,A))) = ld(A,rd(B,mult(ld(A,rd(A,A)),B))),
inference(paramod,[status(thm)],[c_168,c_64]) ).
cnf(c_212,plain,
rd(ld(A,rd(A,A)),ld(A,rd(A,A))) = ld(A,A),
inference(paramod,[status(thm)],[c_53,c_7358]) ).
cnf(c_219,plain,
mult(rd(A,B),C) = ld(rd(B,A),C),
inference(paramod,[status(thm)],[c_3,c_177]) ).
cnf(c_226,plain,
rd(A,mult(rd(B,mult(C,B)),A)) = C,
inference(paramod,[status(thm)],[c_177,c_9]) ).
cnf(c_247,plain,
rd(A,mult(B,A)) = mult(rd(C,mult(B,C)),rd(B,B)),
inference(paramod,[status(thm)],[c_177,c_163]) ).
cnf(c_7359,plain,
ld(A,ld(B,C)) = mult(B,ld(mult(mult(B,A),B),C)),
inference(paramod,[status(thm)],[c_16,c_2]) ).
cnf(c_274,plain,
mult(A,ld(mult(mult(A,B),A),C)) = ld(B,ld(A,C)),
inference(copy,[status(thm)],[c_7359]) ).
cnf(c_328,plain,
mult(rd(A,mult(rd(x1,x1),A)),x0) != x0,
inference(paramod,[status(thm)],[c_191,c_7]) ).
cnf(c_337,plain,
rd(A,mult(rd(B,B),A)) = mult(B,rd(C,mult(B,C))),
inference(paramod,[status(thm)],[c_191,c_168]) ).
cnf(c_364,plain,
mult(ld(A,A),ld(A,rd(A,A))) = ld(A,rd(A,A)),
inference(paramod,[status(thm)],[c_212,c_3]) ).
cnf(c_7360,plain,
mult(ld(A,A),B) = ld(rd(ld(A,rd(A,A)),ld(A,rd(A,A))),B),
inference(paramod,[status(thm)],[c_212,c_219]) ).
cnf(c_7361,plain,
mult(ld(A,A),B) = ld(ld(A,A),B),
inference(paramod,[status(thm)],[c_212,c_7360]) ).
cnf(c_373,plain,
ld(ld(A,A),B) = mult(ld(A,A),B),
inference(copy,[status(thm)],[c_7361]) ).
cnf(c_7362,plain,
rd(A,mult(ld(B,B),A)) = rd(ld(B,rd(B,B)),ld(B,rd(B,B))),
inference(paramod,[status(thm)],[c_212,c_191]) ).
cnf(c_374,plain,
rd(A,mult(ld(B,B),A)) = ld(B,B),
inference(paramod,[status(thm)],[c_212,c_7362]) ).
cnf(c_375,plain,
mult(ld(A,A),mult(ld(A,A),B)) = B,
inference(paramod,[status(thm)],[c_373,c_1]) ).
cnf(c_7363,plain,
mult(ld(A,A),mult(mult(ld(A,A),B),mult(ld(A,A),C))) = mult(mult(B,ld(A,A)),C),
inference(paramod,[status(thm)],[c_373,c_11]) ).
cnf(c_376,plain,
mult(mult(A,ld(B,B)),C) = mult(ld(B,B),mult(mult(ld(B,B),A),mult(ld(B,B),C))),
inference(copy,[status(thm)],[c_7363]) ).
cnf(c_7364,plain,
mult(mult(A,ld(B,B)),mult(ld(B,B),C)) = mult(ld(B,B),mult(ld(ld(B,B),A),C)),
inference(paramod,[status(thm)],[c_373,c_18]) ).
cnf(c_377,plain,
mult(mult(A,ld(B,B)),mult(ld(B,B),C)) = mult(ld(B,B),mult(mult(ld(B,B),A),C)),
inference(paramod,[status(thm)],[c_373,c_7364]) ).
cnf(c_7365,plain,
ld(ld(A,A),rd(B,mult(ld(A,A),B))) = rd(ld(A,A),ld(A,A)),
inference(paramod,[status(thm)],[c_168,c_373]) ).
cnf(c_7366,plain,
ld(ld(A,A),ld(A,A)) = rd(ld(A,A),ld(A,A)),
inference(paramod,[status(thm)],[c_374,c_7365]) ).
cnf(c_7367,plain,
mult(ld(A,A),ld(A,A)) = rd(ld(A,A),ld(A,A)),
inference(paramod,[status(thm)],[c_373,c_7366]) ).
cnf(c_383,plain,
rd(ld(A,A),ld(A,A)) = mult(ld(A,A),ld(A,A)),
inference(copy,[status(thm)],[c_7367]) ).
cnf(c_7368,plain,
mult(ld(A,A),mult(mult(B,ld(A,A)),C)) = mult(ld(ld(A,A),B),mult(ld(A,A),C)),
inference(paramod,[status(thm)],[c_373,c_19]) ).
cnf(c_7369,plain,
mult(ld(A,A),mult(mult(B,ld(A,A)),C)) = mult(mult(ld(A,A),B),mult(ld(A,A),C)),
inference(paramod,[status(thm)],[c_373,c_7368]) ).
cnf(c_386,plain,
mult(mult(ld(A,A),B),mult(ld(A,A),C)) = mult(ld(A,A),mult(mult(B,ld(A,A)),C)),
inference(copy,[status(thm)],[c_7369]) ).
cnf(c_394,plain,
rd(ld(A,A),mult(rd(B,mult(A,B)),A)) = mult(ld(A,A),ld(A,A)),
inference(paramod,[status(thm)],[c_177,c_383]) ).
cnf(c_7370,plain,
rd(ld(A,A),ld(A,A)) = mult(ld(A,A),mult(rd(B,mult(A,B)),A)),
inference(paramod,[status(thm)],[c_177,c_383]) ).
cnf(c_7371,plain,
mult(ld(A,A),ld(A,A)) = mult(ld(A,A),mult(rd(B,mult(A,B)),A)),
inference(paramod,[status(thm)],[c_383,c_7370]) ).
cnf(c_395,plain,
mult(ld(A,A),mult(rd(B,mult(A,B)),A)) = mult(ld(A,A),ld(A,A)),
inference(copy,[status(thm)],[c_7371]) ).
cnf(c_467,plain,
mult(rd(A,mult(mult(x1,rd(B,mult(x1,B))),A)),x0) != x0,
inference(paramod,[status(thm)],[c_168,c_328]) ).
cnf(c_7372,plain,
mult(rd(ld(rd(A,mult(x1,A)),B),mult(rd(A,mult(x1,A)),mult(ld(rd(A,mult(x1,A)),x1),B))),x0) != x0,
inference(paramod,[status(thm)],[c_18,c_467]) ).
cnf(c_7373,plain,
mult(rd(mult(x1,B),mult(rd(A,mult(x1,A)),mult(ld(rd(A,mult(x1,A)),x1),B))),x0) != x0,
inference(paramod,[status(thm)],[c_193,c_7372]) ).
cnf(c_7374,plain,
mult(rd(mult(x1,B),mult(rd(A,mult(x1,A)),mult(mult(x1,x1),B))),x0) != x0,
inference(paramod,[status(thm)],[c_193,c_7373]) ).
cnf(c_7375,plain,
mult(mult(mult(x1,rd(B,mult(x1,mult(rd(A,mult(x1,A)),mult(mult(x1,x1),B))))),x1),x0) != x0,
inference(paramod,[status(thm)],[c_148,c_7374]) ).
cnf(c_7376,plain,
mult(mult(mult(x1,rd(B,mult(mult(x1,x1),B))),x1),x0) != x0,
inference(paramod,[status(thm)],[c_173,c_7375]) ).
cnf(c_471,plain,
mult(x1,mult(rd(A,mult(mult(x1,x1),A)),mult(x1,x0))) != x0,
inference(paramod,[status(thm)],[c_6,c_7376]) ).
cnf(c_477,plain,
rd(A,mult(mult(ld(B,rd(B,B)),B),A)) = ld(B,B),
inference(paramod,[status(thm)],[c_64,c_374]) ).
cnf(c_542,plain,
rd(A,mult(B,A)) = mult(rd(C,mult(B,C)),rd(D,mult(rd(B,B),D))),
inference(paramod,[status(thm)],[c_191,c_247]) ).
cnf(c_7377,plain,
mult(rd(A,A),mult(ld(rd(A,A),rd(B,mult(A,B))),A)) = mult(rd(C,mult(A,C)),A),
inference(paramod,[status(thm)],[c_247,c_20]) ).
cnf(c_7378,plain,
mult(rd(A,A),mult(mult(rd(A,A),rd(B,mult(A,B))),A)) = mult(rd(C,mult(A,C)),A),
inference(paramod,[status(thm)],[c_219,c_7377]) ).
cnf(c_545,plain,
mult(rd(A,mult(B,A)),B) = mult(rd(B,B),mult(mult(rd(B,B),rd(C,mult(B,C))),B)),
inference(copy,[status(thm)],[c_7378]) ).
cnf(c_7379,plain,
mult(mult(ld(A,A),B),mult(ld(ld(ld(A,A),B),ld(A,A)),C)) = mult(B,ld(ld(ld(A,A),B),C)),
inference(paramod,[status(thm)],[c_373,c_24]) ).
cnf(c_7380,plain,
mult(mult(ld(A,A),B),mult(ld(mult(ld(A,A),B),ld(A,A)),C)) = mult(B,ld(ld(ld(A,A),B),C)),
inference(paramod,[status(thm)],[c_373,c_7379]) ).
cnf(c_636,plain,
mult(mult(ld(A,A),B),mult(ld(mult(ld(A,A),B),ld(A,A)),C)) = mult(B,ld(mult(ld(A,A),B),C)),
inference(paramod,[status(thm)],[c_373,c_7380]) ).
cnf(c_7381,plain,
mult(mult(A,ld(B,B)),ld(ld(B,B),ld(mult(ld(B,B),A),C))) = mult(ld(B,B),C),
inference(paramod,[status(thm)],[c_373,c_25]) ).
cnf(c_672,plain,
mult(mult(A,ld(B,B)),mult(ld(B,B),ld(mult(ld(B,B),A),C))) = mult(ld(B,B),C),
inference(paramod,[status(thm)],[c_373,c_7381]) ).
cnf(c_7382,plain,
ld(mult(A,ld(B,B)),mult(ld(B,B),mult(mult(ld(B,B),A),C))) = ld(ld(B,B),C),
inference(paramod,[status(thm)],[c_373,c_26]) ).
cnf(c_711,plain,
ld(mult(A,ld(B,B)),mult(ld(B,B),mult(mult(ld(B,B),A),C))) = mult(ld(B,B),C),
inference(paramod,[status(thm)],[c_373,c_7382]) ).
cnf(c_725,plain,
mult(x1,ld(mult(x1,x1),mult(x1,x0))) != x0,
inference(paramod,[status(thm)],[c_177,c_471]) ).
cnf(c_7383,plain,
mult(ld(A,rd(ld(A,A),A)),rd(A,A)) = ld(A,ld(A,rd(A,A))),
inference(paramod,[status(thm)],[c_364,c_58]) ).
cnf(c_733,plain,
mult(ld(A,ld(A,rd(A,A))),rd(A,A)) = ld(A,ld(A,rd(A,A))),
inference(paramod,[status(thm)],[c_96,c_7383]) ).
cnf(c_735,plain,
mult(ld(A,A),rd(B,mult(A,B))) = ld(A,rd(A,A)),
inference(paramod,[status(thm)],[c_163,c_364]) ).
cnf(c_7384,plain,
mult(mult(rd(A,B),rd(B,A)),ld(rd(B,A),rd(rd(B,A),rd(B,A)))) = ld(rd(B,A),rd(rd(B,A),rd(B,A))),
inference(paramod,[status(thm)],[c_219,c_364]) ).
cnf(c_7385,plain,
mult(mult(rd(A,B),rd(B,A)),ld(rd(B,A),mult(rd(B,A),rd(A,B)))) = ld(rd(B,A),rd(rd(B,A),rd(B,A))),
inference(paramod,[status(thm)],[c_201,c_7384]) ).
cnf(c_7386,plain,
mult(mult(rd(A,B),rd(B,A)),rd(A,B)) = ld(rd(B,A),rd(rd(B,A),rd(B,A))),
inference(paramod,[status(thm)],[c_2,c_7385]) ).
cnf(c_7387,plain,
mult(mult(rd(A,B),rd(B,A)),rd(A,B)) = ld(rd(B,A),mult(rd(B,A),rd(A,B))),
inference(paramod,[status(thm)],[c_201,c_7386]) ).
cnf(c_738,plain,
mult(mult(rd(A,B),rd(B,A)),rd(A,B)) = rd(A,B),
inference(paramod,[status(thm)],[c_2,c_7387]) ).
cnf(c_756,plain,
rd(A,mult(B,A)) = mult(ld(B,B),rd(C,mult(B,C))),
inference(paramod,[status(thm)],[c_735,c_163]) ).
cnf(c_757,plain,
mult(rd(A,mult(B,A)),rd(B,B)) = mult(ld(B,B),rd(C,mult(B,C))),
inference(paramod,[status(thm)],[c_735,c_177]) ).
cnf(c_772,plain,
mult(ld(A,A),rd(B,mult(A,B))) = mult(ld(A,A),rd(C,mult(A,C))),
inference(paramod,[status(thm)],[c_735,c_735]) ).
cnf(c_808,plain,
rd(A,mult(rd(B,B),A)) = mult(B,mult(ld(B,B),rd(C,mult(B,C)))),
inference(paramod,[status(thm)],[c_756,c_337]) ).
cnf(c_7388,plain,
mult(ld(A,A),mult(mult(B,ld(A,A)),ld(ld(A,A),C))) = mult(ld(ld(A,A),B),C),
inference(paramod,[status(thm)],[c_18,c_375]) ).
cnf(c_7389,plain,
mult(ld(A,A),mult(mult(B,ld(A,A)),mult(ld(A,A),C))) = mult(ld(ld(A,A),B),C),
inference(paramod,[status(thm)],[c_373,c_7388]) ).
cnf(c_7390,plain,
mult(ld(A,A),mult(mult(B,ld(A,A)),mult(ld(A,A),C))) = mult(mult(ld(A,A),B),C),
inference(paramod,[status(thm)],[c_373,c_7389]) ).
cnf(c_1043,plain,
mult(mult(ld(A,A),B),C) = mult(ld(A,A),mult(mult(B,ld(A,A)),mult(ld(A,A),C))),
inference(copy,[status(thm)],[c_7390]) ).
cnf(c_1050,plain,
mult(mult(ld(A,A),mult(B,B)),C) = mult(mult(ld(A,A),B),mult(ld(A,A),mult(mult(ld(A,A),B),C))),
inference(paramod,[status(thm)],[c_375,c_15]) ).
cnf(c_1056,plain,
ld(mult(A,A),mult(A,B)) = ld(A,mult(ld(A,A),B)),
inference(paramod,[status(thm)],[c_375,c_26]) ).
cnf(c_7391,plain,
mult(x1,ld(x1,mult(ld(x1,x1),x0))) != x0,
inference(paramod,[status(thm)],[c_1056,c_725]) ).
cnf(c_1063,plain,
mult(ld(x1,x1),x0) != x0,
inference(paramod,[status(thm)],[c_1,c_7391]) ).
cnf(c_1203,plain,
ld(mult(A,A),B) = ld(A,mult(ld(A,A),ld(A,B))),
inference(paramod,[status(thm)],[c_1,c_1056]) ).
cnf(c_1338,plain,
mult(rd(A,mult(B,A)),rd(C,mult(rd(B,B),C))) = mult(ld(B,B),rd(D,mult(B,D))),
inference(paramod,[status(thm)],[c_191,c_757]) ).
cnf(c_7392,plain,
ld(mult(A,A),mult(A,mult(ld(A,A),rd(B,mult(A,B))))) = ld(A,rd(C,mult(A,C))),
inference(paramod,[status(thm)],[c_772,c_26]) ).
cnf(c_7393,plain,
ld(A,mult(ld(A,A),ld(A,mult(A,mult(ld(A,A),rd(B,mult(A,B))))))) = ld(A,rd(C,mult(A,C))),
inference(paramod,[status(thm)],[c_1203,c_7392]) ).
cnf(c_7394,plain,
ld(A,mult(ld(A,A),mult(ld(A,A),rd(B,mult(A,B))))) = ld(A,rd(C,mult(A,C))),
inference(paramod,[status(thm)],[c_2,c_7393]) ).
cnf(c_1360,plain,
ld(A,rd(B,mult(A,B))) = ld(A,rd(C,mult(A,C))),
inference(paramod,[status(thm)],[c_375,c_7394]) ).
cnf(c_1546,plain,
mult(ld(A,rd(A,A)),rd(B,mult(A,B))) = ld(A,rd(C,mult(A,C))),
inference(paramod,[status(thm)],[c_1360,c_64]) ).
cnf(c_7395,plain,
mult(ld(A,rd(A,A)),rd(ld(A,B),B)) = ld(A,rd(C,mult(A,C))),
inference(paramod,[status(thm)],[c_1,c_1546]) ).
cnf(c_1568,plain,
mult(ld(A,rd(A,A)),ld(A,rd(A,A))) = ld(A,rd(B,mult(A,B))),
inference(paramod,[status(thm)],[c_96,c_7395]) ).
cnf(c_7396,plain,
mult(ld(A,rd(A,A)),ld(A,rd(A,A))) = ld(A,rd(ld(A,B),B)),
inference(paramod,[status(thm)],[c_1,c_1568]) ).
cnf(c_7397,plain,
mult(ld(A,rd(A,A)),ld(A,rd(A,A))) = ld(A,ld(A,rd(A,A))),
inference(paramod,[status(thm)],[c_96,c_7396]) ).
cnf(c_1682,plain,
ld(A,ld(A,rd(A,A))) = mult(ld(A,rd(A,A)),ld(A,rd(A,A))),
inference(copy,[status(thm)],[c_7397]) ).
cnf(c_7398,plain,
mult(mult(ld(A,rd(A,A)),ld(A,rd(A,A))),rd(A,A)) = ld(A,ld(A,rd(A,A))),
inference(paramod,[status(thm)],[c_1682,c_733]) ).
cnf(c_7399,plain,
mult(ld(A,rd(A,A)),mult(rd(A,A),mult(ld(A,rd(A,A)),rd(A,A)))) = ld(A,ld(A,rd(A,A))),
inference(paramod,[status(thm)],[c_97,c_7398]) ).
cnf(c_1730,plain,
mult(ld(A,rd(A,A)),mult(rd(A,A),mult(ld(A,rd(A,A)),rd(A,A)))) = mult(ld(A,rd(A,A)),ld(A,rd(A,A))),
inference(paramod,[status(thm)],[c_1682,c_7399]) ).
cnf(c_7400,plain,
rd(ld(mult(A,B),mult(B,ld(mult(A,B),C))),C) = ld(mult(A,B),rd(D,mult(A,D))),
inference(paramod,[status(thm)],[c_187,c_68]) ).
cnf(c_7401,plain,
ld(mult(A,B),rd(B,mult(A,B))) = ld(mult(A,B),rd(D,mult(A,D))),
inference(paramod,[status(thm)],[c_68,c_7400]) ).
cnf(c_2050,plain,
ld(mult(A,B),rd(C,mult(A,C))) = ld(mult(A,B),rd(B,mult(A,B))),
inference(copy,[status(thm)],[c_7401]) ).
cnf(c_2318,plain,
ld(mult(A,B),rd(C,mult(A,C))) = ld(mult(A,B),rd(D,mult(A,D))),
inference(paramod,[status(thm)],[c_187,c_2050]) ).
cnf(c_7402,plain,
ld(A,rd(B,mult(C,B))) = ld(mult(C,ld(C,A)),rd(D,mult(C,D))),
inference(paramod,[status(thm)],[c_1,c_2318]) ).
cnf(c_2944,plain,
ld(A,rd(B,mult(C,B))) = ld(A,rd(D,mult(C,D))),
inference(paramod,[status(thm)],[c_1,c_7402]) ).
cnf(c_7403,plain,
ld(rd(A,mult(B,A)),rd(C,mult(D,C))) = mult(B,rd(E,mult(D,E))),
inference(paramod,[status(thm)],[c_2944,c_193]) ).
cnf(c_2996,plain,
mult(A,rd(B,mult(C,B))) = mult(A,rd(D,mult(C,D))),
inference(paramod,[status(thm)],[c_193,c_7403]) ).
cnf(c_7404,plain,
mult(A,rd(ld(B,C),C)) = mult(A,rd(D,mult(B,D))),
inference(paramod,[status(thm)],[c_1,c_2996]) ).
cnf(c_7405,plain,
mult(A,ld(B,rd(B,B))) = mult(A,rd(D,mult(B,D))),
inference(paramod,[status(thm)],[c_96,c_7404]) ).
cnf(c_3029,plain,
mult(A,rd(B,mult(C,B))) = mult(A,ld(C,rd(C,C))),
inference(copy,[status(thm)],[c_7405]) ).
cnf(c_3078,plain,
mult(rd(rd(A,mult(B,A)),mult(C,rd(D,mult(B,D)))),mult(C,E)) = E,
inference(paramod,[status(thm)],[c_2996,c_190]) ).
cnf(c_3082,plain,
rd(rd(A,mult(B,A)),mult(rd(C,mult(D,C)),rd(E,mult(B,E)))) = D,
inference(paramod,[status(thm)],[c_2996,c_226]) ).
cnf(c_3139,plain,
mult(A,rd(B,mult(C,B))) = mult(A,ld(C,rd(D,mult(rd(C,C),D)))),
inference(paramod,[status(thm)],[c_191,c_3029]) ).
cnf(c_3141,plain,
ld(rd(ld(A,rd(A,A)),mult(B,rd(C,mult(A,C)))),D) = mult(B,D),
inference(paramod,[status(thm)],[c_3029,c_193]) ).
cnf(c_3183,plain,
mult(ld(A,A),rd(ld(B,rd(B,B)),mult(A,rd(C,mult(B,C))))) = ld(A,rd(A,A)),
inference(paramod,[status(thm)],[c_3029,c_735]) ).
cnf(c_3264,plain,
mult(A,rd(rd(B,mult(C,B)),mult(D,rd(E,mult(C,E))))) = mult(A,ld(D,rd(D,D))),
inference(paramod,[status(thm)],[c_2996,c_3029]) ).
cnf(c_7406,plain,
mult(mult(ld(A,rd(A,A)),A),B) = mult(A,mult(mult(ld(A,rd(ld(A,A),A)),rd(A,A)),mult(A,B))),
inference(paramod,[status(thm)],[c_364,c_78]) ).
cnf(c_7407,plain,
mult(mult(ld(A,rd(A,A)),A),B) = mult(A,mult(mult(ld(A,ld(A,rd(A,A))),rd(A,A)),mult(A,B))),
inference(paramod,[status(thm)],[c_96,c_7406]) ).
cnf(c_7408,plain,
mult(mult(ld(A,rd(A,A)),A),B) = mult(A,mult(mult(mult(ld(A,rd(A,A)),ld(A,rd(A,A))),rd(A,A)),mult(A,B))),
inference(paramod,[status(thm)],[c_1682,c_7407]) ).
cnf(c_7409,plain,
mult(mult(ld(A,rd(A,A)),A),B) = mult(A,mult(mult(ld(A,rd(A,A)),mult(rd(A,A),mult(ld(A,rd(A,A)),rd(A,A)))),mult(A,B))),
inference(paramod,[status(thm)],[c_97,c_7408]) ).
cnf(c_7410,plain,
mult(mult(ld(A,rd(A,A)),A),B) = mult(A,mult(mult(ld(A,rd(A,A)),ld(A,rd(A,A))),mult(A,B))),
inference(paramod,[status(thm)],[c_1730,c_7409]) ).
cnf(c_7411,plain,
mult(mult(ld(A,rd(A,A)),A),B) = mult(A,mult(ld(A,rd(A,A)),mult(rd(A,A),mult(ld(A,rd(A,A)),mult(A,B))))),
inference(paramod,[status(thm)],[c_97,c_7410]) ).
cnf(c_7412,plain,
mult(mult(ld(A,rd(A,A)),A),B) = mult(A,mult(ld(A,rd(A,A)),mult(rd(A,A),B))),
inference(paramod,[status(thm)],[c_95,c_7411]) ).
cnf(c_4075,plain,
mult(mult(ld(A,rd(A,A)),A),B) = mult(rd(A,A),B),
inference(paramod,[status(thm)],[c_93,c_7412]) ).
cnf(c_4118,plain,
rd(A,mult(rd(B,B),A)) = ld(B,B),
inference(paramod,[status(thm)],[c_4075,c_477]) ).
cnf(c_4144,plain,
mult(A,rd(B,mult(C,B))) = mult(A,ld(C,ld(C,C))),
inference(paramod,[status(thm)],[c_4118,c_3139]) ).
cnf(c_7413,plain,
mult(rd(A,mult(B,A)),ld(B,B)) = mult(ld(B,B),rd(D,mult(B,D))),
inference(paramod,[status(thm)],[c_4118,c_1338]) ).
cnf(c_4158,plain,
mult(rd(A,mult(B,A)),ld(B,B)) = mult(ld(B,B),ld(B,ld(B,B))),
inference(paramod,[status(thm)],[c_4144,c_7413]) ).
cnf(c_7414,plain,
ld(B,B) = mult(B,mult(ld(B,B),rd(C,mult(B,C)))),
inference(paramod,[status(thm)],[c_4118,c_808]) ).
cnf(c_7415,plain,
ld(B,B) = mult(B,mult(ld(B,B),ld(B,ld(B,B)))),
inference(paramod,[status(thm)],[c_4144,c_7414]) ).
cnf(c_4164,plain,
mult(A,mult(ld(A,A),ld(A,ld(A,A)))) = ld(A,A),
inference(copy,[status(thm)],[c_7415]) ).
cnf(c_7416,plain,
rd(A,mult(B,A)) = mult(rd(C,mult(B,C)),ld(B,B)),
inference(paramod,[status(thm)],[c_4118,c_542]) ).
cnf(c_4174,plain,
rd(A,mult(B,A)) = mult(ld(B,B),ld(B,ld(B,B))),
inference(paramod,[status(thm)],[c_4158,c_7416]) ).
cnf(c_7417,plain,
mult(ld(rd(B,B),rd(B,B)),ld(rd(B,B),ld(rd(B,B),rd(B,B)))) = mult(B,rd(C,mult(B,C))),
inference(paramod,[status(thm)],[c_4174,c_337]) ).
cnf(c_7418,plain,
mult(mult(rd(B,B),rd(B,B)),ld(rd(B,B),ld(rd(B,B),rd(B,B)))) = mult(B,rd(C,mult(B,C))),
inference(paramod,[status(thm)],[c_219,c_7417]) ).
cnf(c_7419,plain,
mult(mult(rd(B,B),rd(B,B)),ld(rd(B,B),mult(rd(B,B),rd(B,B)))) = mult(B,rd(C,mult(B,C))),
inference(paramod,[status(thm)],[c_219,c_7418]) ).
cnf(c_7420,plain,
mult(mult(rd(B,B),rd(B,B)),rd(B,B)) = mult(B,rd(C,mult(B,C))),
inference(paramod,[status(thm)],[c_2,c_7419]) ).
cnf(c_7421,plain,
rd(B,B) = mult(B,rd(C,mult(B,C))),
inference(paramod,[status(thm)],[c_738,c_7420]) ).
cnf(c_7422,plain,
rd(B,B) = mult(B,mult(ld(B,B),ld(B,ld(B,B)))),
inference(paramod,[status(thm)],[c_4174,c_7421]) ).
cnf(c_4176,plain,
rd(A,A) = ld(A,A),
inference(paramod,[status(thm)],[c_4164,c_7422]) ).
cnf(c_7423,plain,
mult(A,rd(mult(ld(C,C),ld(C,ld(C,C))),mult(D,rd(E,mult(C,E))))) = mult(A,ld(D,rd(D,D))),
inference(paramod,[status(thm)],[c_4174,c_3264]) ).
cnf(c_7424,plain,
mult(A,rd(mult(ld(C,C),ld(C,ld(C,C))),mult(D,mult(ld(C,C),ld(C,ld(C,C)))))) = mult(A,ld(D,rd(D,D))),
inference(paramod,[status(thm)],[c_4174,c_7423]) ).
cnf(c_7425,plain,
mult(A,mult(ld(D,D),ld(D,ld(D,D)))) = mult(A,ld(D,rd(D,D))),
inference(paramod,[status(thm)],[c_4174,c_7424]) ).
cnf(c_4254,plain,
mult(A,mult(ld(B,B),ld(B,ld(B,B)))) = mult(A,ld(B,ld(B,B))),
inference(paramod,[status(thm)],[c_4176,c_7425]) ).
cnf(c_7426,plain,
mult(ld(A,A),rd(ld(B,ld(B,B)),mult(A,rd(C,mult(B,C))))) = ld(A,rd(A,A)),
inference(paramod,[status(thm)],[c_4176,c_3183]) ).
cnf(c_7427,plain,
mult(ld(A,A),rd(ld(B,ld(B,B)),mult(A,mult(ld(B,B),ld(B,ld(B,B)))))) = ld(A,rd(A,A)),
inference(paramod,[status(thm)],[c_4174,c_7426]) ).
cnf(c_7428,plain,
mult(ld(A,A),rd(ld(B,ld(B,B)),mult(A,ld(B,ld(B,B))))) = ld(A,rd(A,A)),
inference(paramod,[status(thm)],[c_4254,c_7427]) ).
cnf(c_7429,plain,
mult(ld(A,A),mult(ld(A,A),ld(A,ld(A,A)))) = ld(A,rd(A,A)),
inference(paramod,[status(thm)],[c_4174,c_7428]) ).
cnf(c_7430,plain,
mult(ld(A,A),ld(A,ld(A,A))) = ld(A,rd(A,A)),
inference(paramod,[status(thm)],[c_4254,c_7429]) ).
cnf(c_4269,plain,
mult(ld(A,A),ld(A,ld(A,A))) = ld(A,ld(A,A)),
inference(paramod,[status(thm)],[c_4176,c_7430]) ).
cnf(c_7431,plain,
ld(rd(ld(A,ld(A,A)),mult(B,rd(C,mult(A,C)))),D) = mult(B,D),
inference(paramod,[status(thm)],[c_4176,c_3141]) ).
cnf(c_7432,plain,
ld(rd(ld(A,ld(A,A)),mult(B,mult(ld(A,A),ld(A,ld(A,A))))),D) = mult(B,D),
inference(paramod,[status(thm)],[c_4174,c_7431]) ).
cnf(c_7433,plain,
ld(rd(ld(A,ld(A,A)),mult(B,ld(A,ld(A,A)))),D) = mult(B,D),
inference(paramod,[status(thm)],[c_4269,c_7432]) ).
cnf(c_7434,plain,
ld(mult(ld(B,B),ld(B,ld(B,B))),D) = mult(B,D),
inference(paramod,[status(thm)],[c_4174,c_7433]) ).
cnf(c_4273,plain,
ld(ld(A,ld(A,A)),B) = mult(A,B),
inference(paramod,[status(thm)],[c_4269,c_7434]) ).
cnf(c_7435,plain,
rd(mult(ld(B,B),ld(B,ld(B,B))),mult(rd(C,mult(D,C)),rd(E,mult(B,E)))) = D,
inference(paramod,[status(thm)],[c_4174,c_3082]) ).
cnf(c_7436,plain,
rd(ld(B,ld(B,B)),mult(rd(C,mult(D,C)),rd(E,mult(B,E)))) = D,
inference(paramod,[status(thm)],[c_4269,c_7435]) ).
cnf(c_7437,plain,
rd(ld(B,ld(B,B)),mult(mult(ld(D,D),ld(D,ld(D,D))),rd(E,mult(B,E)))) = D,
inference(paramod,[status(thm)],[c_4174,c_7436]) ).
cnf(c_7438,plain,
rd(ld(B,ld(B,B)),mult(ld(D,ld(D,D)),rd(E,mult(B,E)))) = D,
inference(paramod,[status(thm)],[c_4269,c_7437]) ).
cnf(c_7439,plain,
rd(ld(B,ld(B,B)),mult(ld(D,ld(D,D)),mult(ld(B,B),ld(B,ld(B,B))))) = D,
inference(paramod,[status(thm)],[c_4174,c_7438]) ).
cnf(c_7440,plain,
rd(ld(B,ld(B,B)),mult(ld(D,ld(D,D)),ld(B,ld(B,B)))) = D,
inference(paramod,[status(thm)],[c_4269,c_7439]) ).
cnf(c_7441,plain,
mult(ld(ld(D,ld(D,D)),ld(D,ld(D,D))),ld(ld(D,ld(D,D)),ld(ld(D,ld(D,D)),ld(D,ld(D,D))))) = D,
inference(paramod,[status(thm)],[c_4174,c_7440]) ).
cnf(c_7442,plain,
mult(mult(D,ld(D,ld(D,D))),ld(ld(D,ld(D,D)),ld(ld(D,ld(D,D)),ld(D,ld(D,D))))) = D,
inference(paramod,[status(thm)],[c_4273,c_7441]) ).
cnf(c_7443,plain,
mult(ld(D,D),ld(ld(D,ld(D,D)),ld(ld(D,ld(D,D)),ld(D,ld(D,D))))) = D,
inference(paramod,[status(thm)],[c_1,c_7442]) ).
cnf(c_7444,plain,
mult(ld(D,D),ld(ld(D,ld(D,D)),mult(D,ld(D,ld(D,D))))) = D,
inference(paramod,[status(thm)],[c_4273,c_7443]) ).
cnf(c_7445,plain,
mult(ld(D,D),ld(ld(D,ld(D,D)),ld(D,D))) = D,
inference(paramod,[status(thm)],[c_1,c_7444]) ).
cnf(c_7446,plain,
mult(ld(D,D),mult(D,ld(D,D))) = D,
inference(paramod,[status(thm)],[c_4273,c_7445]) ).
cnf(c_4283,plain,
mult(ld(A,A),A) = A,
inference(paramod,[status(thm)],[c_1,c_7446]) ).
cnf(c_7447,plain,
mult(rd(mult(ld(B,B),ld(B,ld(B,B))),mult(C,rd(D,mult(B,D)))),mult(C,E)) = E,
inference(paramod,[status(thm)],[c_4174,c_3078]) ).
cnf(c_7448,plain,
mult(rd(ld(B,ld(B,B)),mult(C,rd(D,mult(B,D)))),mult(C,E)) = E,
inference(paramod,[status(thm)],[c_4269,c_7447]) ).
cnf(c_7449,plain,
mult(rd(ld(B,ld(B,B)),mult(C,mult(ld(B,B),ld(B,ld(B,B))))),mult(C,E)) = E,
inference(paramod,[status(thm)],[c_4174,c_7448]) ).
cnf(c_7450,plain,
mult(rd(ld(B,ld(B,B)),mult(C,ld(B,ld(B,B)))),mult(C,E)) = E,
inference(paramod,[status(thm)],[c_4269,c_7449]) ).
cnf(c_7451,plain,
mult(mult(ld(C,C),ld(C,ld(C,C))),mult(C,E)) = E,
inference(paramod,[status(thm)],[c_4174,c_7450]) ).
cnf(c_4286,plain,
mult(ld(A,ld(A,A)),mult(A,B)) = B,
inference(paramod,[status(thm)],[c_4269,c_7451]) ).
cnf(c_7452,plain,
mult(mult(ld(B,B),ld(B,ld(B,B))),B) = mult(rd(B,B),mult(mult(rd(B,B),rd(C,mult(B,C))),B)),
inference(paramod,[status(thm)],[c_4174,c_545]) ).
cnf(c_7453,plain,
mult(ld(B,ld(B,B)),B) = mult(rd(B,B),mult(mult(rd(B,B),rd(C,mult(B,C))),B)),
inference(paramod,[status(thm)],[c_4269,c_7452]) ).
cnf(c_7454,plain,
mult(ld(B,ld(B,B)),B) = mult(ld(B,B),mult(mult(rd(B,B),rd(C,mult(B,C))),B)),
inference(paramod,[status(thm)],[c_4176,c_7453]) ).
cnf(c_7455,plain,
mult(ld(B,ld(B,B)),B) = mult(ld(B,B),mult(mult(ld(B,B),rd(C,mult(B,C))),B)),
inference(paramod,[status(thm)],[c_4176,c_7454]) ).
cnf(c_7456,plain,
mult(ld(B,ld(B,B)),B) = mult(ld(B,B),mult(mult(ld(B,B),mult(ld(B,B),ld(B,ld(B,B)))),B)),
inference(paramod,[status(thm)],[c_4174,c_7455]) ).
cnf(c_7457,plain,
mult(ld(B,ld(B,B)),B) = mult(ld(B,B),mult(mult(ld(B,B),ld(B,ld(B,B))),B)),
inference(paramod,[status(thm)],[c_4269,c_7456]) ).
cnf(c_7458,plain,
mult(ld(B,ld(B,B)),B) = mult(ld(B,B),mult(ld(B,ld(B,B)),B)),
inference(paramod,[status(thm)],[c_4269,c_7457]) ).
cnf(c_4357,plain,
mult(ld(A,A),mult(ld(A,ld(A,A)),A)) = mult(ld(A,ld(A,A)),A),
inference(copy,[status(thm)],[c_7458]) ).
cnf(c_7459,plain,
mult(ld(A,A),mult(mult(ld(A,A),ld(A,ld(A,A))),A)) = mult(ld(A,A),ld(A,A)),
inference(paramod,[status(thm)],[c_4174,c_395]) ).
cnf(c_7460,plain,
mult(ld(A,A),mult(ld(A,ld(A,A)),A)) = mult(ld(A,A),ld(A,A)),
inference(paramod,[status(thm)],[c_4269,c_7459]) ).
cnf(c_4582,plain,
mult(ld(A,ld(A,A)),A) = mult(ld(A,A),ld(A,A)),
inference(paramod,[status(thm)],[c_4357,c_7460]) ).
cnf(c_7461,plain,
rd(ld(A,A),mult(mult(ld(A,A),ld(A,ld(A,A))),A)) = mult(ld(A,A),ld(A,A)),
inference(paramod,[status(thm)],[c_4174,c_394]) ).
cnf(c_7462,plain,
rd(ld(A,A),mult(ld(A,ld(A,A)),A)) = mult(ld(A,A),ld(A,A)),
inference(paramod,[status(thm)],[c_4269,c_7461]) ).
cnf(c_7463,plain,
rd(ld(A,A),mult(ld(A,A),ld(A,A))) = mult(ld(A,A),ld(A,A)),
inference(paramod,[status(thm)],[c_4582,c_7462]) ).
cnf(c_7464,plain,
ld(ld(A,A),rd(ld(A,A),ld(A,A))) = mult(ld(A,A),ld(A,A)),
inference(paramod,[status(thm)],[c_163,c_7463]) ).
cnf(c_7465,plain,
ld(ld(A,A),ld(ld(A,A),ld(A,A))) = mult(ld(A,A),ld(A,A)),
inference(paramod,[status(thm)],[c_4176,c_7464]) ).
cnf(c_7466,plain,
ld(ld(A,A),mult(ld(A,A),ld(A,A))) = mult(ld(A,A),ld(A,A)),
inference(paramod,[status(thm)],[c_373,c_7465]) ).
cnf(c_7467,plain,
ld(A,A) = mult(ld(A,A),ld(A,A)),
inference(paramod,[status(thm)],[c_2,c_7466]) ).
cnf(c_4583,plain,
mult(ld(A,A),ld(A,A)) = ld(A,A),
inference(copy,[status(thm)],[c_7467]) ).
cnf(c_7468,plain,
mult(mult(A,A),ld(ld(A,A),B)) = mult(ld(A,A),mult(ld(ld(A,A),mult(A,A)),B)),
inference(paramod,[status(thm)],[c_4283,c_42]) ).
cnf(c_7469,plain,
mult(mult(A,A),mult(ld(A,A),B)) = mult(ld(A,A),mult(ld(ld(A,A),mult(A,A)),B)),
inference(paramod,[status(thm)],[c_373,c_7468]) ).
cnf(c_7470,plain,
mult(mult(A,A),mult(ld(A,A),B)) = mult(ld(A,A),mult(mult(ld(A,A),mult(A,A)),B)),
inference(paramod,[status(thm)],[c_373,c_7469]) ).
cnf(c_7471,plain,
mult(mult(A,A),mult(ld(A,A),B)) = mult(ld(A,A),mult(mult(ld(A,A),A),mult(ld(A,A),mult(mult(ld(A,A),A),B)))),
inference(paramod,[status(thm)],[c_1050,c_7470]) ).
cnf(c_7472,plain,
mult(mult(A,A),mult(ld(A,A),B)) = mult(ld(A,A),mult(A,mult(ld(A,A),mult(mult(ld(A,A),A),B)))),
inference(paramod,[status(thm)],[c_4283,c_7471]) ).
cnf(c_7473,plain,
mult(mult(A,A),mult(ld(A,A),B)) = mult(ld(A,A),mult(A,mult(ld(A,A),mult(A,B)))),
inference(paramod,[status(thm)],[c_4283,c_7472]) ).
cnf(c_7474,plain,
mult(mult(A,A),mult(ld(A,A),B)) = mult(ld(A,A),mult(mult(A,A),B)),
inference(paramod,[status(thm)],[c_11,c_7473]) ).
cnf(c_4698,plain,
mult(ld(A,A),mult(mult(A,A),B)) = mult(mult(A,A),mult(ld(A,A),B)),
inference(copy,[status(thm)],[c_7474]) ).
cnf(c_7475,plain,
mult(mult(A,A),ld(A,ld(A,A))) = mult(A,ld(A,A)),
inference(paramod,[status(thm)],[c_4583,c_18]) ).
cnf(c_4700,plain,
mult(mult(A,A),ld(A,ld(A,A))) = A,
inference(paramod,[status(thm)],[c_1,c_7475]) ).
cnf(c_7476,plain,
mult(mult(mult(A,A),ld(A,ld(A,A))),ld(ld(A,A),B)) = mult(mult(ld(A,A),ld(A,A)),mult(ld(mult(ld(A,A),ld(A,A)),A),B)),
inference(paramod,[status(thm)],[c_4583,c_43]) ).
cnf(c_7477,plain,
mult(A,ld(ld(A,A),B)) = mult(mult(ld(A,A),ld(A,A)),mult(ld(mult(ld(A,A),ld(A,A)),A),B)),
inference(paramod,[status(thm)],[c_4700,c_7476]) ).
cnf(c_7478,plain,
mult(A,mult(ld(A,A),B)) = mult(mult(ld(A,A),ld(A,A)),mult(ld(mult(ld(A,A),ld(A,A)),A),B)),
inference(paramod,[status(thm)],[c_373,c_7477]) ).
cnf(c_7479,plain,
mult(A,mult(ld(A,A),B)) = mult(ld(A,A),mult(ld(mult(ld(A,A),ld(A,A)),A),B)),
inference(paramod,[status(thm)],[c_4583,c_7478]) ).
cnf(c_7480,plain,
mult(A,mult(ld(A,A),B)) = mult(ld(A,A),mult(ld(ld(A,A),A),B)),
inference(paramod,[status(thm)],[c_4583,c_7479]) ).
cnf(c_7481,plain,
mult(A,mult(ld(A,A),B)) = mult(ld(A,A),mult(mult(ld(A,A),A),B)),
inference(paramod,[status(thm)],[c_373,c_7480]) ).
cnf(c_7482,plain,
mult(A,mult(ld(A,A),B)) = mult(ld(A,A),mult(A,B)),
inference(paramod,[status(thm)],[c_4283,c_7481]) ).
cnf(c_4707,plain,
mult(ld(A,A),mult(A,B)) = mult(A,mult(ld(A,A),B)),
inference(copy,[status(thm)],[c_7482]) ).
cnf(c_7483,plain,
mult(ld(A,A),ld(mult(B,ld(A,A)),C)) = ld(mult(ld(A,A),B),ld(ld(A,A),C)),
inference(paramod,[status(thm)],[c_375,c_274]) ).
cnf(c_4791,plain,
mult(ld(A,A),ld(mult(B,ld(A,A)),C)) = ld(mult(ld(A,A),B),mult(ld(A,A),C)),
inference(paramod,[status(thm)],[c_373,c_7483]) ).
cnf(c_4938,plain,
mult(ld(A,A),ld(mult(ld(A,A),B),mult(ld(A,A),C))) = ld(mult(B,ld(A,A)),C),
inference(paramod,[status(thm)],[c_4791,c_375]) ).
cnf(c_4941,plain,
mult(ld(A,A),ld(mult(B,ld(A,A)),mult(ld(A,A),C))) = ld(mult(ld(A,A),B),C),
inference(paramod,[status(thm)],[c_375,c_4791]) ).
cnf(c_4949,plain,
mult(ld(A,A),ld(mult(B,ld(A,A)),A)) = ld(mult(ld(A,A),B),A),
inference(paramod,[status(thm)],[c_4283,c_4791]) ).
cnf(c_4972,plain,
mult(ld(A,A),ld(mult(B,ld(A,A)),mult(A,C))) = ld(mult(ld(A,A),B),mult(A,mult(ld(A,A),C))),
inference(paramod,[status(thm)],[c_4707,c_4791]) ).
cnf(c_5110,plain,
mult(ld(A,A),ld(mult(ld(A,A),B),C)) = ld(mult(B,ld(A,A)),mult(ld(A,A),C)),
inference(paramod,[status(thm)],[c_375,c_4938]) ).
cnf(c_5220,plain,
mult(ld(A,A),ld(mult(ld(A,A),B),mult(A,C))) = ld(mult(B,ld(A,A)),mult(A,mult(ld(A,A),C))),
inference(paramod,[status(thm)],[c_4707,c_5110]) ).
cnf(c_7484,plain,
mult(mult(A,A),mult(ld(A,ld(A,A)),mult(A,mult(ld(A,A),B)))) = mult(A,mult(mult(A,ld(A,A)),B)),
inference(paramod,[status(thm)],[c_376,c_23]) ).
cnf(c_7485,plain,
mult(mult(A,A),mult(ld(A,A),B)) = mult(A,mult(mult(A,ld(A,A)),B)),
inference(paramod,[status(thm)],[c_4286,c_7484]) ).
cnf(c_5601,plain,
mult(mult(A,A),mult(ld(A,A),B)) = mult(A,mult(A,B)),
inference(paramod,[status(thm)],[c_1,c_7485]) ).
cnf(c_5648,plain,
mult(ld(A,A),mult(mult(A,A),B)) = mult(A,mult(A,B)),
inference(paramod,[status(thm)],[c_5601,c_4698]) ).
cnf(c_5687,plain,
mult(mult(ld(A,A),ld(B,B)),mult(ld(B,B),C)) = mult(ld(B,B),mult(ld(A,A),mult(mult(ld(A,A),ld(B,B)),mult(ld(A,A),C)))),
inference(paramod,[status(thm)],[c_376,c_377]) ).
cnf(c_5688,plain,
mult(mult(ld(A,A),ld(B,B)),mult(ld(B,B),mult(ld(A,A),C))) = mult(ld(B,B),mult(ld(A,A),mult(mult(ld(A,A),ld(B,B)),C))),
inference(paramod,[status(thm)],[c_377,c_377]) ).
cnf(c_5736,plain,
mult(mult(ld(A,A),ld(B,B)),mult(ld(A,A),mult(ld(B,B),C))) = mult(ld(A,A),mult(ld(B,B),mult(mult(ld(A,A),ld(B,B)),C))),
inference(paramod,[status(thm)],[c_386,c_386]) ).
cnf(c_5874,plain,
mult(mult(ld(A,A),ld(B,B)),mult(ld(mult(ld(A,A),ld(B,B)),ld(A,A)),mult(ld(B,B),C))) = ld(mult(ld(B,B),ld(A,A)),C),
inference(paramod,[status(thm)],[c_636,c_4941]) ).
cnf(c_7486,plain,
mult(mult(ld(A,A),ld(B,B)),mult(ld(mult(ld(A,A),ld(B,B)),ld(A,A)),mult(ld(B,B),mult(mult(ld(B,B),ld(A,A)),C)))) = mult(ld(B,B),mult(ld(B,B),C)),
inference(paramod,[status(thm)],[c_711,c_636]) ).
cnf(c_6653,plain,
mult(mult(ld(A,A),ld(B,B)),mult(ld(mult(ld(A,A),ld(B,B)),ld(A,A)),mult(ld(B,B),mult(mult(ld(B,B),ld(A,A)),C)))) = C,
inference(paramod,[status(thm)],[c_375,c_7486]) ).
cnf(c_6805,plain,
mult(ld(A,A),ld(mult(B,ld(A,A)),mult(A,C))) = ld(mult(ld(A,A),B),mult(mult(A,A),ld(A,C))),
inference(paramod,[status(thm)],[c_18,c_4972]) ).
cnf(c_7487,plain,
mult(ld(A,A),mult(ld(B,B),ld(mult(ld(B,B),ld(A,A)),mult(B,C)))) = ld(mult(ld(B,B),ld(A,A)),mult(ld(A,A),mult(B,mult(ld(B,B),C)))),
inference(paramod,[status(thm)],[c_5220,c_5110]) ).
cnf(c_6910,plain,
ld(mult(ld(A,A),ld(B,B)),mult(ld(B,B),mult(A,mult(ld(A,A),C)))) = mult(ld(B,B),mult(ld(A,A),ld(mult(ld(A,A),ld(B,B)),mult(A,C)))),
inference(copy,[status(thm)],[c_7487]) ).
cnf(c_7488,plain,
mult(ld(A,A),mult(ld(mult(A,B),mult(A,B)),ld(mult(ld(A,A),ld(mult(A,B),mult(A,B))),mult(A,B)))) = ld(mult(ld(A,A),ld(mult(A,B),mult(A,B))),mult(mult(A,A),ld(A,B))),
inference(paramod,[status(thm)],[c_4949,c_6805]) ).
cnf(c_7026,plain,
ld(mult(ld(A,A),ld(mult(A,B),mult(A,B))),mult(mult(A,A),ld(A,B))) = mult(ld(A,A),mult(ld(mult(A,B),mult(A,B)),ld(mult(ld(A,A),ld(mult(A,B),mult(A,B))),mult(A,B)))),
inference(copy,[status(thm)],[c_7488]) ).
cnf(c_7276,plain,
mult(mult(ld(A,A),ld(B,B)),mult(ld(A,A),C)) = mult(ld(A,A),mult(ld(B,B),mult(mult(ld(A,A),ld(B,B)),mult(ld(B,B),C)))),
inference(paramod,[status(thm)],[c_1043,c_386]) ).
cnf(c_7489,plain,
mult(mult(ld(A,A),mult(ld(B,B),ld(B,B))),C) = mult(ld(B,B),mult(mult(ld(B,B),ld(A,A)),mult(ld(B,B),mult(ld(A,A),mult(mult(ld(A,A),ld(B,B)),C))))),
inference(paramod,[status(thm)],[c_376,c_1050]) ).
cnf(c_7490,plain,
mult(mult(ld(A,A),ld(B,B)),C) = mult(ld(B,B),mult(mult(ld(B,B),ld(A,A)),mult(ld(B,B),mult(ld(A,A),mult(mult(ld(A,A),ld(B,B)),C))))),
inference(paramod,[status(thm)],[c_4583,c_7489]) ).
cnf(c_7491,plain,
mult(mult(ld(A,A),ld(B,B)),C) = mult(ld(B,B),mult(ld(B,B),mult(ld(A,A),mult(mult(ld(B,B),ld(A,A)),mult(mult(ld(A,A),ld(B,B)),C))))),
inference(paramod,[status(thm)],[c_5736,c_7490]) ).
cnf(c_7492,plain,
mult(mult(ld(A,A),ld(B,B)),C) = mult(ld(A,A),mult(mult(ld(B,B),ld(A,A)),mult(mult(ld(A,A),ld(B,B)),C))),
inference(paramod,[status(thm)],[c_375,c_7491]) ).
cnf(c_7305,plain,
mult(ld(A,A),mult(mult(ld(B,B),ld(A,A)),mult(mult(ld(A,A),ld(B,B)),C))) = mult(mult(ld(A,A),ld(B,B)),C),
inference(copy,[status(thm)],[c_7492]) ).
cnf(c_7493,plain,
mult(mult(ld(A,A),mult(ld(B,B),ld(B,B))),mult(ld(B,B),C)) = mult(mult(ld(A,A),ld(B,B)),mult(ld(A,A),mult(ld(B,B),mult(mult(ld(B,B),ld(A,A)),C)))),
inference(paramod,[status(thm)],[c_377,c_1050]) ).
cnf(c_7494,plain,
mult(mult(ld(A,A),ld(B,B)),mult(ld(B,B),C)) = mult(mult(ld(A,A),ld(B,B)),mult(ld(A,A),mult(ld(B,B),mult(mult(ld(B,B),ld(A,A)),C)))),
inference(paramod,[status(thm)],[c_4583,c_7493]) ).
cnf(c_7495,plain,
mult(mult(ld(A,A),ld(B,B)),mult(ld(B,B),C)) = mult(ld(A,A),mult(ld(B,B),mult(mult(ld(A,A),ld(B,B)),mult(mult(ld(B,B),ld(A,A)),C)))),
inference(paramod,[status(thm)],[c_5736,c_7494]) ).
cnf(c_7306,plain,
mult(mult(ld(A,A),ld(B,B)),mult(ld(B,B),C)) = mult(ld(A,A),mult(mult(ld(B,B),ld(A,A)),C)),
inference(paramod,[status(thm)],[c_7305,c_7495]) ).
cnf(c_7496,plain,
mult(mult(ld(A,A),mult(ld(B,B),ld(B,B))),mult(ld(B,B),ld(mult(ld(B,B),ld(A,A)),C))) = mult(mult(ld(A,A),ld(B,B)),mult(ld(A,A),mult(ld(B,B),C))),
inference(paramod,[status(thm)],[c_672,c_1050]) ).
cnf(c_7497,plain,
mult(mult(ld(A,A),ld(B,B)),mult(ld(B,B),ld(mult(ld(B,B),ld(A,A)),C))) = mult(mult(ld(A,A),ld(B,B)),mult(ld(A,A),mult(ld(B,B),C))),
inference(paramod,[status(thm)],[c_4583,c_7496]) ).
cnf(c_7498,plain,
mult(ld(B,B),C) = mult(mult(ld(A,A),ld(B,B)),mult(ld(A,A),mult(ld(B,B),C))),
inference(paramod,[status(thm)],[c_672,c_7497]) ).
cnf(c_7499,plain,
mult(ld(B,B),C) = mult(ld(A,A),mult(ld(B,B),mult(mult(ld(A,A),ld(B,B)),C))),
inference(paramod,[status(thm)],[c_5736,c_7498]) ).
cnf(c_7307,plain,
mult(ld(A,A),mult(ld(B,B),mult(mult(ld(A,A),ld(B,B)),C))) = mult(ld(B,B),C),
inference(copy,[status(thm)],[c_7499]) ).
cnf(c_7500,plain,
mult(mult(ld(A,A),ld(B,B)),mult(ld(A,A),C)) = mult(ld(B,B),mult(ld(B,B),C)),
inference(paramod,[status(thm)],[c_7307,c_7276]) ).
cnf(c_7308,plain,
mult(mult(ld(A,A),ld(B,B)),mult(ld(A,A),C)) = C,
inference(paramod,[status(thm)],[c_375,c_7500]) ).
cnf(c_7312,plain,
mult(mult(ld(A,A),ld(B,B)),mult(ld(B,B),C)) = mult(ld(B,B),mult(ld(A,A),C)),
inference(paramod,[status(thm)],[c_7308,c_5687]) ).
cnf(c_7501,plain,
mult(ld(B,B),mult(ld(A,A),C)) = mult(ld(A,A),mult(mult(ld(B,B),ld(A,A)),C)),
inference(paramod,[status(thm)],[c_7312,c_7306]) ).
cnf(c_7313,plain,
mult(ld(A,A),mult(mult(ld(B,B),ld(A,A)),C)) = mult(ld(B,B),mult(ld(A,A),C)),
inference(copy,[status(thm)],[c_7501]) ).
cnf(c_7502,plain,
mult(ld(B,B),mult(ld(A,A),mult(ld(A,A),C))) = mult(ld(B,B),mult(ld(A,A),mult(mult(ld(A,A),ld(B,B)),C))),
inference(paramod,[status(thm)],[c_7312,c_5688]) ).
cnf(c_7503,plain,
mult(ld(B,B),C) = mult(ld(B,B),mult(ld(A,A),mult(mult(ld(A,A),ld(B,B)),C))),
inference(paramod,[status(thm)],[c_375,c_7502]) ).
cnf(c_7314,plain,
mult(ld(A,A),mult(ld(B,B),mult(mult(ld(B,B),ld(A,A)),C))) = mult(ld(A,A),C),
inference(copy,[status(thm)],[c_7503]) ).
cnf(c_7504,plain,
mult(ld(B,B),mult(ld(A,A),mult(mult(ld(A,A),ld(B,B)),C))) = mult(mult(ld(A,A),ld(B,B)),C),
inference(paramod,[status(thm)],[c_7313,c_7305]) ).
cnf(c_7505,plain,
mult(ld(B,B),C) = mult(mult(ld(A,A),ld(B,B)),C),
inference(paramod,[status(thm)],[c_7314,c_7504]) ).
cnf(c_7315,plain,
mult(mult(ld(A,A),ld(B,B)),C) = mult(ld(B,B),C),
inference(copy,[status(thm)],[c_7505]) ).
cnf(c_7506,plain,
mult(ld(A,A),mult(ld(A,A),C)) = mult(ld(B,B),mult(ld(A,A),C)),
inference(paramod,[status(thm)],[c_7315,c_7313]) ).
cnf(c_7507,plain,
C = mult(ld(B,B),mult(ld(A,A),C)),
inference(paramod,[status(thm)],[c_375,c_7506]) ).
cnf(c_7317,plain,
mult(ld(A,A),mult(ld(B,B),C)) = C,
inference(copy,[status(thm)],[c_7507]) ).
cnf(c_7508,plain,
mult(mult(ld(A,A),ld(B,B)),mult(ld(mult(ld(A,A),ld(B,B)),ld(A,A)),mult(ld(B,B),mult(ld(A,A),C)))) = C,
inference(paramod,[status(thm)],[c_7315,c_6653]) ).
cnf(c_7509,plain,
mult(mult(ld(A,A),ld(B,B)),mult(ld(mult(ld(A,A),ld(B,B)),ld(A,A)),C)) = C,
inference(paramod,[status(thm)],[c_7317,c_7508]) ).
cnf(c_7321,plain,
mult(ld(A,A),mult(ld(mult(ld(B,B),ld(A,A)),ld(B,B)),C)) = C,
inference(paramod,[status(thm)],[c_7315,c_7509]) ).
cnf(c_7510,plain,
mult(ld(B,B),mult(ld(mult(ld(A,A),ld(B,B)),ld(A,A)),mult(ld(B,B),C))) = ld(mult(ld(B,B),ld(A,A)),C),
inference(paramod,[status(thm)],[c_7315,c_5874]) ).
cnf(c_7511,plain,
mult(ld(B,B),C) = ld(mult(ld(B,B),ld(A,A)),C),
inference(paramod,[status(thm)],[c_7321,c_7510]) ).
cnf(c_7325,plain,
ld(mult(ld(A,A),ld(B,B)),C) = mult(ld(A,A),C),
inference(copy,[status(thm)],[c_7511]) ).
cnf(c_7512,plain,
mult(ld(A,A),mult(mult(A,A),ld(A,B))) = mult(ld(A,A),mult(ld(mult(A,B),mult(A,B)),ld(mult(ld(A,A),ld(mult(A,B),mult(A,B))),mult(A,B)))),
inference(paramod,[status(thm)],[c_7325,c_7026]) ).
cnf(c_7513,plain,
mult(A,mult(A,ld(A,B))) = mult(ld(A,A),mult(ld(mult(A,B),mult(A,B)),ld(mult(ld(A,A),ld(mult(A,B),mult(A,B))),mult(A,B)))),
inference(paramod,[status(thm)],[c_5648,c_7512]) ).
cnf(c_7514,plain,
mult(A,B) = mult(ld(A,A),mult(ld(mult(A,B),mult(A,B)),ld(mult(ld(A,A),ld(mult(A,B),mult(A,B))),mult(A,B)))),
inference(paramod,[status(thm)],[c_1,c_7513]) ).
cnf(c_7515,plain,
mult(A,B) = mult(ld(A,A),mult(ld(mult(A,B),mult(A,B)),mult(ld(A,A),mult(A,B)))),
inference(paramod,[status(thm)],[c_7325,c_7514]) ).
cnf(c_7516,plain,
mult(A,B) = mult(ld(A,A),mult(ld(mult(A,B),mult(A,B)),mult(A,mult(ld(A,A),B)))),
inference(paramod,[status(thm)],[c_4707,c_7515]) ).
cnf(c_7517,plain,
mult(A,B) = mult(A,mult(ld(A,A),B)),
inference(paramod,[status(thm)],[c_7317,c_7516]) ).
cnf(c_7333,plain,
mult(A,mult(ld(A,A),B)) = mult(A,B),
inference(copy,[status(thm)],[c_7517]) ).
cnf(c_7518,plain,
ld(mult(ld(A,A),ld(B,B)),mult(ld(B,B),mult(A,C))) = mult(ld(B,B),mult(ld(A,A),ld(mult(ld(A,A),ld(B,B)),mult(A,C)))),
inference(paramod,[status(thm)],[c_7333,c_6910]) ).
cnf(c_7519,plain,
mult(ld(A,A),mult(ld(B,B),mult(A,C))) = mult(ld(B,B),mult(ld(A,A),ld(mult(ld(A,A),ld(B,B)),mult(A,C)))),
inference(paramod,[status(thm)],[c_7325,c_7518]) ).
cnf(c_7520,plain,
mult(A,C) = mult(ld(B,B),mult(ld(A,A),ld(mult(ld(A,A),ld(B,B)),mult(A,C)))),
inference(paramod,[status(thm)],[c_7317,c_7519]) ).
cnf(c_7521,plain,
mult(A,C) = mult(ld(B,B),mult(ld(A,A),mult(ld(A,A),mult(A,C)))),
inference(paramod,[status(thm)],[c_7325,c_7520]) ).
cnf(c_7522,plain,
mult(A,C) = mult(ld(B,B),mult(ld(A,A),mult(A,mult(ld(A,A),C)))),
inference(paramod,[status(thm)],[c_4707,c_7521]) ).
cnf(c_7523,plain,
mult(A,C) = mult(ld(B,B),mult(ld(A,A),mult(A,C))),
inference(paramod,[status(thm)],[c_7333,c_7522]) ).
cnf(c_7524,plain,
mult(A,C) = mult(ld(B,B),mult(A,mult(ld(A,A),C))),
inference(paramod,[status(thm)],[c_4707,c_7523]) ).
cnf(c_7525,plain,
mult(A,C) = mult(ld(B,B),mult(A,C)),
inference(paramod,[status(thm)],[c_7333,c_7524]) ).
cnf(c_7335,plain,
mult(ld(A,A),mult(B,C)) = mult(B,C),
inference(copy,[status(thm)],[c_7525]) ).
cnf(c_7526,plain,
mult(ld(A,A),mult(mult(ld(B,B),ld(B,B)),C)) = C,
inference(paramod,[status(thm)],[c_7325,c_7321]) ).
cnf(c_7527,plain,
mult(ld(A,A),mult(ld(B,B),C)) = C,
inference(paramod,[status(thm)],[c_4583,c_7526]) ).
cnf(c_7343,plain,
mult(ld(A,A),B) = B,
inference(paramod,[status(thm)],[c_7335,c_7527]) ).
cnf(c_7344,plain,
$false,
inference(resolve,[status(thm)],[c_7343,c_1063]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP654-12 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.53 % Computer : n007.cluster.edu
% 0.08/0.53 % Model : x86_64 x86_64
% 0.08/0.53 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.53 % Memory : 8046.5625MB
% 0.08/0.53 % OS : Linux 6.8.0-71-generic
% 0.08/0.53 % CPULimit : 300
% 0.08/0.53 % WCLimit : 300
% 0.08/0.53 % DateTime : Fri Sep 25 15:27:09 UTC 2026
% 0.08/0.54 % CPUTime :
% 0.08/0.54 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.54 % Process 1352135 was started by sandbox on n007,
% 0.08/0.54 % Fri Sep 25 15:27:09 2026
% 0.08/0.54 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.08/0.54
% 0.08/0.54 % From the command line: assign(max_seconds, 300).
% 37.02/5.24
% 37.02/5.24 % SZS status Unsatisfiable for theBenchmark
% 37.02/5.24
% 37.02/5.24 % Proof 1 at 3.93 (+ 0.72) seconds.
% 37.02/5.24 % Length of proof is 150.
% 37.02/5.24 % Level of proof is 43.
% 37.02/5.24 % Maximum clause weight is 100.000.
% 37.02/5.24 % Given clauses 273.
% 37.02/5.24
% 37.02/5.24 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------