%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP654-11 : 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 : n002.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 18.51s 3.19s
% Output : CNFRefutation 18.51s
% Verified :
% SZS Type : Refutation
% Derivation depth : 82
% Number of leaves : 6
% Syntax : Number of formulae : 236 ( 236 unt; 0 def)
% Number of atoms : 236 ( 235 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 24 ( 24 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 12 ( 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 : 532 ( 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(x0,rd(x1,x1)) != x0,
file('theBenchmark.p',goal) ).
cnf(c_7,plain,
mult(x0,rd(x1,x1)) != 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_7302,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_7302]) ).
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_7303,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_7303]) ).
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_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_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_7304,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_7304]) ).
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_7305,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_7305]) ).
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_7306,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_7306]) ).
cnf(c_7307,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_7307]) ).
cnf(c_187,plain,
rd(A,mult(B,A)) = rd(C,mult(B,C)),
inference(paramod,[status(thm)],[c_163,c_163]) ).
cnf(c_7308,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_7308]) ).
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_7309,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_7309]) ).
cnf(c_219,plain,
mult(rd(A,B),C) = ld(rd(B,A),C),
inference(paramod,[status(thm)],[c_3,c_177]) ).
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_328,plain,
mult(x0,rd(A,mult(rd(x1,x1),A))) != 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_7310,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_7311,plain,
mult(ld(A,A),B) = ld(ld(A,A),B),
inference(paramod,[status(thm)],[c_212,c_7310]) ).
cnf(c_373,plain,
ld(ld(A,A),B) = mult(ld(A,A),B),
inference(copy,[status(thm)],[c_7311]) ).
cnf(c_7312,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_7312]) ).
cnf(c_375,plain,
mult(ld(A,A),mult(ld(A,A),B)) = B,
inference(paramod,[status(thm)],[c_373,c_1]) ).
cnf(c_7313,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_7313]) ).
cnf(c_7314,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_7314]) ).
cnf(c_7315,plain,
rd(mult(ld(A,A),B),B) = ld(ld(A,A),rd(ld(A,A),ld(A,A))),
inference(paramod,[status(thm)],[c_373,c_96]) ).
cnf(c_7316,plain,
mult(mult(ld(A,A),rd(B,mult(ld(A,A),B))),ld(A,A)) = ld(ld(A,A),rd(ld(A,A),ld(A,A))),
inference(paramod,[status(thm)],[c_148,c_7315]) ).
cnf(c_7317,plain,
mult(mult(ld(A,A),ld(A,A)),ld(A,A)) = ld(ld(A,A),rd(ld(A,A),ld(A,A))),
inference(paramod,[status(thm)],[c_374,c_7316]) ).
cnf(c_7318,plain,
mult(mult(ld(A,A),ld(A,A)),ld(A,A)) = mult(ld(A,A),rd(ld(A,A),ld(A,A))),
inference(paramod,[status(thm)],[c_373,c_7317]) ).
cnf(c_381,plain,
mult(ld(A,A),rd(ld(A,A),ld(A,A))) = mult(mult(ld(A,A),ld(A,A)),ld(A,A)),
inference(copy,[status(thm)],[c_7318]) ).
cnf(c_7319,plain,
rd(A,mult(ld(B,B),A)) = mult(ld(B,B),rd(ld(B,B),ld(B,B))),
inference(paramod,[status(thm)],[c_373,c_163]) ).
cnf(c_7320,plain,
ld(B,B) = mult(ld(B,B),rd(ld(B,B),ld(B,B))),
inference(paramod,[status(thm)],[c_374,c_7319]) ).
cnf(c_7321,plain,
ld(B,B) = mult(mult(ld(B,B),ld(B,B)),ld(B,B)),
inference(paramod,[status(thm)],[c_381,c_7320]) ).
cnf(c_382,plain,
mult(mult(ld(A,A),ld(A,A)),ld(A,A)) = ld(A,A),
inference(copy,[status(thm)],[c_7321]) ).
cnf(c_7322,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_7323,plain,
ld(ld(A,A),ld(A,A)) = rd(ld(A,A),ld(A,A)),
inference(paramod,[status(thm)],[c_374,c_7322]) ).
cnf(c_7324,plain,
mult(ld(A,A),ld(A,A)) = rd(ld(A,A),ld(A,A)),
inference(paramod,[status(thm)],[c_373,c_7323]) ).
cnf(c_383,plain,
rd(ld(A,A),ld(A,A)) = mult(ld(A,A),ld(A,A)),
inference(copy,[status(thm)],[c_7324]) ).
cnf(c_7325,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_7326,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_7325]) ).
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_7326]) ).
cnf(c_7327,plain,
ld(mult(A,rd(B,mult(A,B))),C) = mult(ld(rd(B,mult(A,B)),rd(B,mult(A,B))),C),
inference(paramod,[status(thm)],[c_193,c_373]) ).
cnf(c_387,plain,
ld(mult(A,rd(B,mult(A,B))),C) = mult(mult(A,rd(B,mult(A,B))),C),
inference(paramod,[status(thm)],[c_193,c_7327]) ).
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_7328,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_7329,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_7328]) ).
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_7329]) ).
cnf(c_478,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_543,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_7330,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_7331,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_7330]) ).
cnf(c_546,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_7331]) ).
cnf(c_7332,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_673,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_7332]) ).
cnf(c_7333,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_738,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_7333]) ).
cnf(c_740,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_7334,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_7335,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_7334]) ).
cnf(c_7336,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_7335]) ).
cnf(c_7337,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_7336]) ).
cnf(c_743,plain,
mult(mult(rd(A,B),rd(B,A)),rd(A,B)) = rd(A,B),
inference(paramod,[status(thm)],[c_2,c_7337]) ).
cnf(c_761,plain,
rd(A,mult(B,A)) = mult(ld(B,B),rd(C,mult(B,C))),
inference(paramod,[status(thm)],[c_740,c_163]) ).
cnf(c_762,plain,
mult(rd(A,mult(B,A)),rd(B,B)) = mult(ld(B,B),rd(C,mult(B,C))),
inference(paramod,[status(thm)],[c_740,c_177]) ).
cnf(c_778,plain,
mult(ld(A,A),rd(B,mult(A,B))) = mult(ld(A,A),rd(C,mult(A,C))),
inference(paramod,[status(thm)],[c_740,c_740]) ).
cnf(c_814,plain,
rd(A,mult(rd(B,B),A)) = mult(B,mult(ld(B,B),rd(C,mult(B,C)))),
inference(paramod,[status(thm)],[c_761,c_337]) ).
cnf(c_7338,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_7339,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_7338]) ).
cnf(c_7340,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_7339]) ).
cnf(c_1063,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_7340]) ).
cnf(c_1070,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_1076,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_1229,plain,
ld(mult(A,A),B) = ld(A,mult(ld(A,A),ld(A,B))),
inference(paramod,[status(thm)],[c_1,c_1076]) ).
cnf(c_1364,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_762]) ).
cnf(c_7341,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_778,c_26]) ).
cnf(c_7342,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_1229,c_7341]) ).
cnf(c_7343,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_7342]) ).
cnf(c_1386,plain,
ld(A,rd(B,mult(A,B))) = ld(A,rd(C,mult(A,C))),
inference(paramod,[status(thm)],[c_375,c_7343]) ).
cnf(c_1585,plain,
mult(ld(A,rd(A,A)),rd(B,mult(A,B))) = ld(A,rd(C,mult(A,C))),
inference(paramod,[status(thm)],[c_1386,c_64]) ).
cnf(c_7344,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_1585]) ).
cnf(c_1607,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_7344]) ).
cnf(c_7345,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_1607]) ).
cnf(c_7346,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_7345]) ).
cnf(c_1721,plain,
ld(A,ld(A,rd(A,A))) = mult(ld(A,rd(A,A)),ld(A,rd(A,A))),
inference(copy,[status(thm)],[c_7346]) ).
cnf(c_7347,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_1721,c_738]) ).
cnf(c_7348,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_7347]) ).
cnf(c_1770,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_1721,c_7348]) ).
cnf(c_7349,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_7350,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_7349]) ).
cnf(c_2093,plain,
ld(mult(A,B),rd(C,mult(A,C))) = ld(mult(A,B),rd(B,mult(A,B))),
inference(copy,[status(thm)],[c_7350]) ).
cnf(c_2358,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_2093]) ).
cnf(c_7351,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_2358]) ).
cnf(c_2929,plain,
ld(A,rd(B,mult(C,B))) = ld(A,rd(D,mult(C,D))),
inference(paramod,[status(thm)],[c_1,c_7351]) ).
cnf(c_7352,plain,
ld(rd(A,mult(B,A)),rd(C,mult(D,C))) = mult(B,rd(E,mult(D,E))),
inference(paramod,[status(thm)],[c_2929,c_193]) ).
cnf(c_2981,plain,
mult(A,rd(B,mult(C,B))) = mult(A,rd(D,mult(C,D))),
inference(paramod,[status(thm)],[c_193,c_7352]) ).
cnf(c_7353,plain,
mult(A,rd(ld(B,C),C)) = mult(A,rd(D,mult(B,D))),
inference(paramod,[status(thm)],[c_1,c_2981]) ).
cnf(c_7354,plain,
mult(A,ld(B,rd(B,B))) = mult(A,rd(D,mult(B,D))),
inference(paramod,[status(thm)],[c_96,c_7353]) ).
cnf(c_3014,plain,
mult(A,rd(B,mult(C,B))) = mult(A,ld(C,rd(C,C))),
inference(copy,[status(thm)],[c_7354]) ).
cnf(c_3112,plain,
mult(rd(A,B),ld(C,rd(C,C))) = ld(rd(B,A),rd(D,mult(C,D))),
inference(paramod,[status(thm)],[c_3014,c_219]) ).
cnf(c_3121,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_3014]) ).
cnf(c_3134,plain,
mult(x0,rd(ld(A,rd(A,A)),mult(rd(x1,x1),rd(B,mult(A,B))))) != x0,
inference(paramod,[status(thm)],[c_3014,c_328]) ).
cnf(c_3163,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_3014,c_740]) ).
cnf(c_3240,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_2981,c_3014]) ).
cnf(c_7355,plain,
mult(x0,rd(mult(ld(A,A),rd(B,mult(A,B))),mult(rd(x1,x1),rd(C,mult(A,C))))) != x0,
inference(paramod,[status(thm)],[c_740,c_3134]) ).
cnf(c_3369,plain,
mult(x0,mult(mult(ld(A,A),rd(rd(B,mult(A,B)),mult(ld(A,A),mult(rd(x1,x1),rd(C,mult(A,C)))))),ld(A,A))) != x0,
inference(paramod,[status(thm)],[c_148,c_7355]) ).
cnf(c_7356,plain,
mult(rd(A,A),ld(B,rd(B,B))) = ld(mult(A,rd(C,mult(A,C))),rd(D,mult(B,D))),
inference(paramod,[status(thm)],[c_168,c_3112]) ).
cnf(c_3825,plain,
mult(rd(A,A),ld(B,rd(B,B))) = mult(mult(A,rd(C,mult(A,C))),rd(D,mult(B,D))),
inference(paramod,[status(thm)],[c_387,c_7356]) ).
cnf(c_7357,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_7358,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_7357]) ).
cnf(c_7359,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_1721,c_7358]) ).
cnf(c_7360,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_7359]) ).
cnf(c_7361,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_1770,c_7360]) ).
cnf(c_7362,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_7361]) ).
cnf(c_7363,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_7362]) ).
cnf(c_4033,plain,
mult(mult(ld(A,rd(A,A)),A),B) = mult(rd(A,A),B),
inference(paramod,[status(thm)],[c_93,c_7363]) ).
cnf(c_4076,plain,
rd(A,mult(rd(B,B),A)) = ld(B,B),
inference(paramod,[status(thm)],[c_4033,c_478]) ).
cnf(c_4101,plain,
mult(A,rd(B,mult(C,B))) = mult(A,ld(C,ld(C,C))),
inference(paramod,[status(thm)],[c_4076,c_3121]) ).
cnf(c_7364,plain,
mult(rd(A,mult(B,A)),ld(B,B)) = mult(ld(B,B),rd(D,mult(B,D))),
inference(paramod,[status(thm)],[c_4076,c_1364]) ).
cnf(c_4115,plain,
mult(rd(A,mult(B,A)),ld(B,B)) = mult(ld(B,B),ld(B,ld(B,B))),
inference(paramod,[status(thm)],[c_4101,c_7364]) ).
cnf(c_7365,plain,
ld(B,B) = mult(B,mult(ld(B,B),rd(C,mult(B,C)))),
inference(paramod,[status(thm)],[c_4076,c_814]) ).
cnf(c_7366,plain,
ld(B,B) = mult(B,mult(ld(B,B),ld(B,ld(B,B)))),
inference(paramod,[status(thm)],[c_4101,c_7365]) ).
cnf(c_4122,plain,
mult(A,mult(ld(A,A),ld(A,ld(A,A)))) = ld(A,A),
inference(copy,[status(thm)],[c_7366]) ).
cnf(c_7367,plain,
rd(A,mult(B,A)) = mult(rd(C,mult(B,C)),ld(B,B)),
inference(paramod,[status(thm)],[c_4076,c_543]) ).
cnf(c_4132,plain,
rd(A,mult(B,A)) = mult(ld(B,B),ld(B,ld(B,B))),
inference(paramod,[status(thm)],[c_4115,c_7367]) ).
cnf(c_7368,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_4132,c_337]) ).
cnf(c_7369,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_7368]) ).
cnf(c_7370,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_7369]) ).
cnf(c_7371,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_7370]) ).
cnf(c_7372,plain,
rd(B,B) = mult(B,rd(C,mult(B,C))),
inference(paramod,[status(thm)],[c_743,c_7371]) ).
cnf(c_7373,plain,
rd(B,B) = mult(B,mult(ld(B,B),ld(B,ld(B,B)))),
inference(paramod,[status(thm)],[c_4132,c_7372]) ).
cnf(c_4134,plain,
rd(A,A) = ld(A,A),
inference(paramod,[status(thm)],[c_4122,c_7373]) ).
cnf(c_7374,plain,
mult(ld(A,A),ld(B,rd(B,B))) = mult(mult(A,rd(C,mult(A,C))),rd(D,mult(B,D))),
inference(paramod,[status(thm)],[c_4134,c_3825]) ).
cnf(c_7375,plain,
mult(ld(A,A),ld(B,ld(B,B))) = mult(mult(A,rd(C,mult(A,C))),rd(D,mult(B,D))),
inference(paramod,[status(thm)],[c_4134,c_7374]) ).
cnf(c_7376,plain,
mult(ld(A,A),ld(B,ld(B,B))) = mult(mult(A,mult(ld(A,A),ld(A,ld(A,A)))),rd(D,mult(B,D))),
inference(paramod,[status(thm)],[c_4132,c_7375]) ).
cnf(c_7377,plain,
mult(ld(A,A),ld(B,ld(B,B))) = mult(ld(A,A),rd(D,mult(B,D))),
inference(paramod,[status(thm)],[c_4122,c_7376]) ).
cnf(c_7378,plain,
mult(ld(A,A),ld(B,ld(B,B))) = mult(ld(A,A),mult(ld(B,B),ld(B,ld(B,B)))),
inference(paramod,[status(thm)],[c_4132,c_7377]) ).
cnf(c_4157,plain,
mult(ld(A,A),mult(ld(B,B),ld(B,ld(B,B)))) = mult(ld(A,A),ld(B,ld(B,B))),
inference(copy,[status(thm)],[c_7378]) ).
cnf(c_7379,plain,
mult(x0,mult(mult(ld(A,A),rd(mult(ld(A,A),ld(A,ld(A,A))),mult(ld(A,A),mult(rd(x1,x1),rd(C,mult(A,C)))))),ld(A,A))) != x0,
inference(paramod,[status(thm)],[c_4132,c_3369]) ).
cnf(c_7380,plain,
mult(x0,mult(mult(ld(A,A),rd(mult(ld(A,A),ld(A,ld(A,A))),mult(ld(A,A),mult(ld(x1,x1),rd(C,mult(A,C)))))),ld(A,A))) != x0,
inference(paramod,[status(thm)],[c_4134,c_7379]) ).
cnf(c_7381,plain,
mult(x0,mult(mult(ld(A,A),rd(mult(ld(A,A),ld(A,ld(A,A))),mult(ld(A,A),mult(ld(x1,x1),mult(ld(A,A),ld(A,ld(A,A))))))),ld(A,A))) != x0,
inference(paramod,[status(thm)],[c_4132,c_7380]) ).
cnf(c_7382,plain,
mult(x0,mult(mult(ld(A,A),rd(mult(ld(A,A),ld(A,ld(A,A))),mult(ld(A,A),mult(ld(x1,x1),ld(A,ld(A,A)))))),ld(A,A))) != x0,
inference(paramod,[status(thm)],[c_4157,c_7381]) ).
cnf(c_7383,plain,
mult(x0,mult(mult(ld(A,A),mult(mult(ld(A,A),rd(ld(A,ld(A,A)),mult(ld(A,A),mult(ld(A,A),mult(ld(x1,x1),ld(A,ld(A,A))))))),ld(A,A))),ld(A,A))) != x0,
inference(paramod,[status(thm)],[c_148,c_7382]) ).
cnf(c_7384,plain,
mult(x0,mult(mult(ld(A,A),mult(mult(ld(A,A),rd(ld(A,ld(A,A)),mult(ld(x1,x1),ld(A,ld(A,A))))),ld(A,A))),ld(A,A))) != x0,
inference(paramod,[status(thm)],[c_375,c_7383]) ).
cnf(c_7385,plain,
mult(x0,mult(mult(ld(A,A),mult(mult(ld(A,A),mult(ld(ld(x1,x1),ld(x1,x1)),ld(ld(x1,x1),ld(ld(x1,x1),ld(x1,x1))))),ld(A,A))),ld(A,A))) != x0,
inference(paramod,[status(thm)],[c_4132,c_7384]) ).
cnf(c_7386,plain,
mult(x0,mult(mult(ld(A,A),mult(mult(ld(A,A),mult(mult(ld(x1,x1),ld(x1,x1)),ld(ld(x1,x1),ld(ld(x1,x1),ld(x1,x1))))),ld(A,A))),ld(A,A))) != x0,
inference(paramod,[status(thm)],[c_373,c_7385]) ).
cnf(c_7387,plain,
mult(x0,mult(mult(ld(A,A),mult(mult(ld(A,A),mult(mult(ld(x1,x1),ld(x1,x1)),ld(ld(x1,x1),mult(ld(x1,x1),ld(x1,x1))))),ld(A,A))),ld(A,A))) != x0,
inference(paramod,[status(thm)],[c_373,c_7386]) ).
cnf(c_7388,plain,
mult(x0,mult(mult(ld(A,A),mult(mult(ld(A,A),mult(mult(ld(x1,x1),ld(x1,x1)),ld(x1,x1))),ld(A,A))),ld(A,A))) != x0,
inference(paramod,[status(thm)],[c_2,c_7387]) ).
cnf(c_4202,plain,
mult(x0,mult(mult(ld(A,A),mult(mult(ld(A,A),ld(x1,x1)),ld(A,A))),ld(A,A))) != x0,
inference(paramod,[status(thm)],[c_382,c_7388]) ).
cnf(c_7389,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_4132,c_3240]) ).
cnf(c_7390,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_4132,c_7389]) ).
cnf(c_7391,plain,
mult(A,mult(ld(D,D),ld(D,ld(D,D)))) = mult(A,ld(D,rd(D,D))),
inference(paramod,[status(thm)],[c_4132,c_7390]) ).
cnf(c_4211,plain,
mult(A,mult(ld(B,B),ld(B,ld(B,B)))) = mult(A,ld(B,ld(B,B))),
inference(paramod,[status(thm)],[c_4134,c_7391]) ).
cnf(c_7392,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_4134,c_3163]) ).
cnf(c_7393,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_4132,c_7392]) ).
cnf(c_7394,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_4211,c_7393]) ).
cnf(c_7395,plain,
mult(ld(A,A),mult(ld(A,A),ld(A,ld(A,A)))) = ld(A,rd(A,A)),
inference(paramod,[status(thm)],[c_4132,c_7394]) ).
cnf(c_7396,plain,
mult(ld(A,A),ld(A,ld(A,A))) = ld(A,rd(A,A)),
inference(paramod,[status(thm)],[c_4211,c_7395]) ).
cnf(c_4223,plain,
mult(ld(A,A),ld(A,ld(A,A))) = ld(A,ld(A,A)),
inference(paramod,[status(thm)],[c_4134,c_7396]) ).
cnf(c_7397,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_4132,c_546]) ).
cnf(c_7398,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_4223,c_7397]) ).
cnf(c_7399,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_4134,c_7398]) ).
cnf(c_7400,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_4134,c_7399]) ).
cnf(c_7401,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_4132,c_7400]) ).
cnf(c_7402,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_4223,c_7401]) ).
cnf(c_7403,plain,
mult(ld(B,ld(B,B)),B) = mult(ld(B,B),mult(ld(B,ld(B,B)),B)),
inference(paramod,[status(thm)],[c_4223,c_7402]) ).
cnf(c_4306,plain,
mult(ld(A,A),mult(ld(A,ld(A,A)),A)) = mult(ld(A,ld(A,A)),A),
inference(copy,[status(thm)],[c_7403]) ).
cnf(c_7404,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_4132,c_395]) ).
cnf(c_7405,plain,
mult(ld(A,A),mult(ld(A,ld(A,A)),A)) = mult(ld(A,A),ld(A,A)),
inference(paramod,[status(thm)],[c_4223,c_7404]) ).
cnf(c_4516,plain,
mult(ld(A,ld(A,A)),A) = mult(ld(A,A),ld(A,A)),
inference(paramod,[status(thm)],[c_4306,c_7405]) ).
cnf(c_7406,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_4132,c_394]) ).
cnf(c_7407,plain,
rd(ld(A,A),mult(ld(A,ld(A,A)),A)) = mult(ld(A,A),ld(A,A)),
inference(paramod,[status(thm)],[c_4223,c_7406]) ).
cnf(c_7408,plain,
rd(ld(A,A),mult(ld(A,A),ld(A,A))) = mult(ld(A,A),ld(A,A)),
inference(paramod,[status(thm)],[c_4516,c_7407]) ).
cnf(c_7409,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_7408]) ).
cnf(c_7410,plain,
ld(ld(A,A),ld(ld(A,A),ld(A,A))) = mult(ld(A,A),ld(A,A)),
inference(paramod,[status(thm)],[c_4134,c_7409]) ).
cnf(c_7411,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_7410]) ).
cnf(c_7412,plain,
ld(A,A) = mult(ld(A,A),ld(A,A)),
inference(paramod,[status(thm)],[c_2,c_7411]) ).
cnf(c_4517,plain,
mult(ld(A,A),ld(A,A)) = ld(A,A),
inference(copy,[status(thm)],[c_7412]) ).
cnf(c_7413,plain,
mult(x0,mult(mult(mult(ld(x1,x1),ld(A,A)),mult(ld(A,A),ld(A,A))),ld(A,A))) != x0,
inference(paramod,[status(thm)],[c_377,c_4202]) ).
cnf(c_5608,plain,
mult(x0,mult(mult(mult(ld(x1,x1),ld(A,A)),ld(A,A)),ld(A,A))) != x0,
inference(paramod,[status(thm)],[c_4517,c_7413]) ).
cnf(c_5642,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_5691,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_7261,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_1063,c_386]) ).
cnf(c_7262,plain,
mult(x0,mult(mult(ld(x1,x1),mult(mult(ld(A,A),ld(x1,x1)),mult(ld(x1,x1),ld(A,A)))),ld(A,A))) != x0,
inference(paramod,[status(thm)],[c_1063,c_5608]) ).
cnf(c_7414,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_673,c_1070]) ).
cnf(c_7415,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_4517,c_7414]) ).
cnf(c_7416,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_673,c_7415]) ).
cnf(c_7417,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_5691,c_7416]) ).
cnf(c_7294,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_7417]) ).
cnf(c_7418,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_7294,c_7261]) ).
cnf(c_7295,plain,
mult(mult(ld(A,A),ld(B,B)),mult(ld(A,A),C)) = C,
inference(paramod,[status(thm)],[c_375,c_7418]) ).
cnf(c_7299,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_7295,c_5642]) ).
cnf(c_7419,plain,
mult(x0,mult(mult(ld(x1,x1),mult(ld(x1,x1),mult(ld(A,A),ld(A,A)))),ld(A,A))) != x0,
inference(paramod,[status(thm)],[c_7299,c_7262]) ).
cnf(c_7420,plain,
mult(x0,mult(mult(ld(x1,x1),mult(ld(x1,x1),ld(A,A))),ld(A,A))) != x0,
inference(paramod,[status(thm)],[c_4517,c_7419]) ).
cnf(c_7421,plain,
mult(x0,mult(ld(A,A),ld(A,A))) != x0,
inference(paramod,[status(thm)],[c_375,c_7420]) ).
cnf(c_7300,plain,
mult(x0,ld(A,A)) != x0,
inference(paramod,[status(thm)],[c_4517,c_7421]) ).
cnf(c_7301,plain,
$false,
inference(resolve,[status(thm)],[c_7300,c_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP654-11 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.38 % Computer : n002.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Fri Sep 25 15:31:36 UTC 2026
% 0.12/0.38 % CPUTime :
% 0.12/0.39 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.12/0.39 % Process 3653152 was started by sandbox on n002,
% 0.12/0.39 % Fri Sep 25 15:31:36 2026
% 0.12/0.39 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.12/0.39
% 0.12/0.39 % From the command line: assign(max_seconds, 300).
% 18.51/3.19
% 18.51/3.19 % SZS status Unsatisfiable for theBenchmark
% 18.51/3.19
% 18.51/3.19 % Proof 1 at 2.34 (+ 0.42) seconds.
% 18.51/3.19 % Length of proof is 110.
% 18.51/3.19 % Level of proof is 36.
% 18.51/3.19 % Maximum clause weight is 96.000.
% 18.51/3.19 % Given clauses 274.
% 18.51/3.19
% 18.51/3.19 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------