%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP683+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 : 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:31:11 AM UTC 2026
% Result : Theorem 1.80s 0.72s
% Output : CNFRefutation 1.80s
% Verified :
% SZS Type : Refutation
% Derivation depth : 62
% Number of leaves : 8
% Syntax : Number of formulae : 275 ( 264 unt; 0 def)
% Number of atoms : 286 ( 285 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 31 ( 20 ~; 9 |; 2 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 1 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 3 con; 0-2 aty)
% Number of variables : 653 ( 0 sgn 22 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f01,axiom,
! [A] : ld(A,mult(A,A)) = A,
file('theBenchmark.p',f01) ).
fof(f02,axiom,
! [A] : rd(mult(A,A),A) = A,
file('theBenchmark.p',f02) ).
fof(f03,axiom,
! [B,A] : mult(A,ld(A,B)) = ld(A,mult(A,B)),
file('theBenchmark.p',f03) ).
fof(f04,axiom,
! [B,A] : mult(rd(A,B),B) = rd(mult(A,B),B),
file('theBenchmark.p',f04) ).
fof(f05,axiom,
! [D,C,B,A] : ld(ld(A,B),mult(ld(A,B),mult(C,D))) = mult(ld(A,mult(A,C)),D),
file('theBenchmark.p',f05) ).
fof(f06,axiom,
! [D,C,B,A] : rd(mult(mult(A,B),rd(C,D)),rd(C,D)) = mult(A,rd(mult(B,D),D)),
file('theBenchmark.p',f06) ).
fof(f07,axiom,
! [B,A] : ld(A,mult(A,ld(B,B))) = rd(mult(rd(A,A),B),B),
file('theBenchmark.p',f07) ).
fof(goals,conjecture,
! [X3,X4,X5] :
( mult(rd(mult(X3,X4),X4),X5) = mult(X3,X5)
& mult(X3,ld(X4,mult(X4,X5))) = mult(X3,X5) ),
file('theBenchmark.p',goals) ).
fof(goals_neg,negated_conjecture,
~ ! [X3,X4,X5] :
( mult(rd(mult(X3,X4),X4),X5) = mult(X3,X5)
& mult(X3,ld(X4,mult(X4,X5))) = mult(X3,X5) ),
inference(assume_negation,[status(cth)],[goals]) ).
cnf(c_9,plain,
ld(A,mult(A,A)) = A,
inference(clausify,[status(thm)],[f01]) ).
cnf(c_10,plain,
rd(mult(A,A),A) = A,
inference(clausify,[status(thm)],[f02]) ).
cnf(c_11,plain,
ld(A,mult(A,B)) = mult(A,ld(A,B)),
inference(clausify,[status(thm)],[f03]) ).
cnf(c_12,plain,
rd(mult(A,B),B) = mult(rd(A,B),B),
inference(clausify,[status(thm)],[f04]) ).
cnf(c_13,plain,
ld(ld(A,B),mult(ld(A,B),mult(C,D))) = mult(ld(A,mult(A,C)),D),
inference(clausify,[status(thm)],[f05]) ).
cnf(c_1211,plain,
mult(ld(A,B),ld(ld(A,B),mult(C,D))) = mult(ld(A,mult(A,C)),D),
inference(paramod,[status(thm)],[c_11,c_13]) ).
cnf(c_14,plain,
mult(ld(A,B),ld(ld(A,B),mult(C,D))) = mult(mult(A,ld(A,C)),D),
inference(paramod,[status(thm)],[c_11,c_1211]) ).
cnf(c_15,plain,
rd(mult(mult(A,B),rd(C,D)),rd(C,D)) = mult(A,rd(mult(B,D),D)),
inference(clausify,[status(thm)],[f06]) ).
cnf(c_1212,plain,
mult(rd(mult(A,B),rd(C,D)),rd(C,D)) = mult(A,rd(mult(B,D),D)),
inference(paramod,[status(thm)],[c_12,c_15]) ).
cnf(c_16,plain,
mult(rd(mult(A,B),rd(C,D)),rd(C,D)) = mult(A,mult(rd(B,D),D)),
inference(paramod,[status(thm)],[c_12,c_1212]) ).
cnf(c_17,plain,
rd(mult(rd(A,A),B),B) = ld(A,mult(A,ld(B,B))),
inference(clausify,[status(thm)],[f07]) ).
cnf(c_1213,plain,
mult(rd(rd(A,A),B),B) = ld(A,mult(A,ld(B,B))),
inference(paramod,[status(thm)],[c_12,c_17]) ).
cnf(c_18,plain,
mult(rd(rd(A,A),B),B) = mult(A,ld(A,ld(B,B))),
inference(paramod,[status(thm)],[c_11,c_1213]) ).
fof(nnf_8,plain,
? [X3,X4,X5] :
( mult(rd(mult(X3,X4),X4),X5) != mult(X3,X5)
| mult(X3,ld(X4,mult(X4,X5))) != mult(X3,X5) ),
inference(fof_nnf,[status(thm)],[goals_neg]) ).
fof(sk_goals_neg,plain,
( mult(rd(mult(sK0,sK1),sK1),sK2) != mult(sK0,sK2)
| mult(sK0,ld(sK1,mult(sK1,sK2))) != mult(sK0,sK2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2]),skolemize(X3,sK0),skolemize(X4,sK1),skolemize(X5,sK2)],[nnf_8]) ).
cnf(c_19,negated_conjecture,
( mult(rd(mult(sK0,sK1),sK1),sK2) != mult(sK0,sK2)
| mult(sK0,ld(sK1,mult(sK1,sK2))) != mult(sK0,sK2) ),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_1214,negated_conjecture,
( mult(rd(mult(sK0,sK1),sK1),sK2) != mult(sK0,sK2)
| mult(sK0,mult(sK1,ld(sK1,sK2))) != mult(sK0,sK2) ),
inference(paramod,[status(thm)],[c_11,c_19]) ).
cnf(c_20,negated_conjecture,
( mult(mult(rd(sK0,sK1),sK1),sK2) != mult(sK0,sK2)
| mult(sK0,mult(sK1,ld(sK1,sK2))) != mult(sK0,sK2) ),
inference(paramod,[status(thm)],[c_12,c_1214]) ).
cnf(c_21,plain,
mult(A,ld(A,A)) = A,
inference(paramod,[status(thm)],[c_11,c_9]) ).
cnf(c_22,plain,
mult(rd(A,A),A) = A,
inference(paramod,[status(thm)],[c_12,c_10]) ).
cnf(c_1215,plain,
ld(ld(A,B),mult(mult(A,ld(A,C)),D)) = mult(ld(A,B),ld(ld(A,B),ld(ld(A,B),mult(C,D)))),
inference(paramod,[status(thm)],[c_14,c_11]) ).
cnf(c_23,plain,
mult(ld(A,B),ld(ld(A,B),ld(ld(A,B),mult(C,D)))) = ld(ld(A,B),mult(mult(A,ld(A,C)),D)),
inference(copy,[status(thm)],[c_1215]) ).
cnf(c_1216,plain,
mult(mult(A,ld(A,B)),ld(ld(A,mult(A,B)),mult(C,D))) = mult(mult(A,ld(A,C)),D),
inference(paramod,[status(thm)],[c_11,c_14]) ).
cnf(c_24,plain,
mult(mult(A,ld(A,B)),ld(mult(A,ld(A,B)),mult(C,D))) = mult(mult(A,ld(A,C)),D),
inference(paramod,[status(thm)],[c_11,c_1216]) ).
cnf(c_25,plain,
mult(ld(A,B),mult(ld(A,B),ld(ld(A,B),C))) = mult(mult(A,ld(A,ld(A,B))),C),
inference(paramod,[status(thm)],[c_11,c_14]) ).
cnf(c_26,plain,
rd(mult(mult(A,ld(A,B)),C),ld(ld(A,D),mult(B,C))) = mult(rd(ld(A,D),ld(ld(A,D),mult(B,C))),ld(ld(A,D),mult(B,C))),
inference(paramod,[status(thm)],[c_14,c_12]) ).
cnf(c_1217,plain,
ld(A,A) = mult(A,ld(A,ld(A,A))),
inference(paramod,[status(thm)],[c_21,c_11]) ).
cnf(c_39,plain,
mult(A,ld(A,ld(A,A))) = ld(A,A),
inference(copy,[status(thm)],[c_1217]) ).
cnf(c_1218,plain,
rd(A,ld(A,A)) = mult(rd(A,ld(A,A)),ld(A,A)),
inference(paramod,[status(thm)],[c_21,c_12]) ).
cnf(c_40,plain,
mult(rd(A,ld(A,A)),ld(A,A)) = rd(A,ld(A,A)),
inference(copy,[status(thm)],[c_1218]) ).
cnf(c_41,plain,
mult(ld(A,B),ld(ld(A,B),C)) = mult(mult(A,ld(A,C)),ld(C,C)),
inference(paramod,[status(thm)],[c_21,c_14]) ).
cnf(c_42,plain,
mult(rd(A,rd(B,C)),rd(B,C)) = mult(A,mult(rd(ld(A,A),C),C)),
inference(paramod,[status(thm)],[c_21,c_16]) ).
cnf(c_1219,plain,
ld(rd(A,A),A) = mult(rd(A,A),ld(rd(A,A),A)),
inference(paramod,[status(thm)],[c_22,c_11]) ).
cnf(c_43,plain,
mult(rd(A,A),ld(rd(A,A),A)) = ld(rd(A,A),A),
inference(copy,[status(thm)],[c_1219]) ).
cnf(c_1220,plain,
rd(A,A) = mult(rd(rd(A,A),A),A),
inference(paramod,[status(thm)],[c_22,c_12]) ).
cnf(c_1221,plain,
rd(A,A) = mult(A,ld(A,ld(A,A))),
inference(paramod,[status(thm)],[c_18,c_1220]) ).
cnf(c_44,plain,
rd(A,A) = ld(A,A),
inference(paramod,[status(thm)],[c_39,c_1221]) ).
cnf(c_1222,plain,
rd(mult(A,A),A) = A,
inference(paramod,[status(thm)],[c_22,c_12]) ).
cnf(c_1223,plain,
mult(rd(A,A),A) = A,
inference(paramod,[status(thm)],[c_12,c_1222]) ).
cnf(c_45,plain,
mult(ld(A,A),A) = A,
inference(paramod,[status(thm)],[c_44,c_1223]) ).
cnf(c_1224,plain,
mult(rd(A,rd(B,C)),rd(B,C)) = mult(rd(A,A),mult(rd(A,C),C)),
inference(paramod,[status(thm)],[c_22,c_16]) ).
cnf(c_47,plain,
mult(rd(A,rd(B,C)),rd(B,C)) = mult(ld(A,A),mult(rd(A,C),C)),
inference(paramod,[status(thm)],[c_44,c_1224]) ).
cnf(c_1225,plain,
rd(A,A) = mult(A,ld(A,ld(rd(A,A),rd(A,A)))),
inference(paramod,[status(thm)],[c_22,c_18]) ).
cnf(c_1226,plain,
ld(A,A) = mult(A,ld(A,ld(rd(A,A),rd(A,A)))),
inference(paramod,[status(thm)],[c_44,c_1225]) ).
cnf(c_1227,plain,
ld(A,A) = mult(A,ld(A,ld(ld(A,A),rd(A,A)))),
inference(paramod,[status(thm)],[c_44,c_1226]) ).
cnf(c_1228,plain,
ld(A,A) = mult(A,ld(A,ld(ld(A,A),ld(A,A)))),
inference(paramod,[status(thm)],[c_44,c_1227]) ).
cnf(c_50,plain,
mult(A,ld(A,ld(ld(A,A),ld(A,A)))) = ld(A,A),
inference(copy,[status(thm)],[c_1228]) ).
cnf(c_1229,plain,
mult(ld(A,A),ld(rd(A,A),A)) = ld(rd(A,A),A),
inference(paramod,[status(thm)],[c_44,c_43]) ).
cnf(c_1230,plain,
mult(ld(A,A),ld(ld(A,A),A)) = ld(rd(A,A),A),
inference(paramod,[status(thm)],[c_44,c_1229]) ).
cnf(c_51,plain,
mult(ld(A,A),ld(ld(A,A),A)) = ld(ld(A,A),A),
inference(paramod,[status(thm)],[c_44,c_1230]) ).
cnf(c_56,plain,
mult(rd(ld(A,A),B),B) = mult(A,ld(A,ld(B,B))),
inference(paramod,[status(thm)],[c_44,c_18]) ).
cnf(c_1231,plain,
mult(ld(A,A),mult(rd(A,C),C)) = mult(A,mult(rd(ld(A,A),C),C)),
inference(paramod,[status(thm)],[c_47,c_42]) ).
cnf(c_57,plain,
mult(ld(A,A),mult(rd(A,B),B)) = mult(A,mult(A,ld(A,ld(B,B)))),
inference(paramod,[status(thm)],[c_56,c_1231]) ).
cnf(c_1232,plain,
mult(ld(mult(A,B),mult(A,B)),mult(rd(mult(A,B),D),D)) = mult(A,mult(rd(B,D),D)),
inference(paramod,[status(thm)],[c_47,c_16]) ).
cnf(c_60,plain,
mult(mult(A,B),mult(mult(A,B),ld(mult(A,B),ld(C,C)))) = mult(A,mult(rd(B,C),C)),
inference(paramod,[status(thm)],[c_57,c_1232]) ).
cnf(c_62,plain,
mult(rd(A,rd(B,C)),rd(B,C)) = mult(A,mult(A,ld(A,ld(C,C)))),
inference(paramod,[status(thm)],[c_57,c_47]) ).
cnf(c_1233,plain,
mult(ld(A,B),ld(ld(A,B),ld(ld(A,B),C))) = ld(ld(A,B),mult(mult(A,ld(A,ld(C,C))),C)),
inference(paramod,[status(thm)],[c_45,c_23]) ).
cnf(c_71,plain,
ld(ld(A,B),mult(mult(A,ld(A,ld(C,C))),C)) = mult(ld(A,B),ld(ld(A,B),ld(ld(A,B),C))),
inference(copy,[status(thm)],[c_1233]) ).
cnf(c_1234,plain,
mult(mult(A,mult(A,ld(A,B))),ld(mult(A,ld(A,mult(A,B))),mult(C,D))) = mult(mult(A,ld(A,C)),D),
inference(paramod,[status(thm)],[c_11,c_24]) ).
cnf(c_80,plain,
mult(mult(A,mult(A,ld(A,B))),ld(mult(A,mult(A,ld(A,B))),mult(C,D))) = mult(mult(A,ld(A,C)),D),
inference(paramod,[status(thm)],[c_11,c_1234]) ).
cnf(c_1235,plain,
mult(A,ld(mult(A,ld(A,A)),mult(B,C))) = mult(mult(A,ld(A,B)),C),
inference(paramod,[status(thm)],[c_21,c_24]) ).
cnf(c_85,plain,
mult(A,ld(A,mult(B,C))) = mult(mult(A,ld(A,B)),C),
inference(paramod,[status(thm)],[c_21,c_1235]) ).
cnf(c_108,plain,
mult(mult(mult(A,mult(A,ld(A,B))),ld(mult(A,mult(A,ld(A,B))),C)),D) = mult(mult(A,ld(A,C)),D),
inference(paramod,[status(thm)],[c_85,c_80]) ).
cnf(c_112,plain,
mult(mult(ld(A,B),ld(ld(A,B),C)),D) = mult(mult(A,ld(A,C)),D),
inference(paramod,[status(thm)],[c_85,c_14]) ).
cnf(c_1236,plain,
mult(ld(A,A),ld(ld(A,A),A)) = mult(mult(A,ld(A,ld(A,A))),A),
inference(paramod,[status(thm)],[c_51,c_25]) ).
cnf(c_1237,plain,
ld(ld(A,A),A) = mult(mult(A,ld(A,ld(A,A))),A),
inference(paramod,[status(thm)],[c_51,c_1236]) ).
cnf(c_1238,plain,
ld(ld(A,A),A) = mult(ld(A,A),A),
inference(paramod,[status(thm)],[c_39,c_1237]) ).
cnf(c_133,plain,
ld(ld(A,A),A) = A,
inference(paramod,[status(thm)],[c_45,c_1238]) ).
cnf(c_1239,plain,
mult(A,ld(ld(ld(A,A),A),ld(ld(ld(A,A),A),mult(B,C)))) = ld(ld(ld(A,A),A),mult(mult(ld(A,A),ld(ld(A,A),B)),C)),
inference(paramod,[status(thm)],[c_133,c_23]) ).
cnf(c_1240,plain,
mult(A,ld(A,ld(ld(ld(A,A),A),mult(B,C)))) = ld(ld(ld(A,A),A),mult(mult(ld(A,A),ld(ld(A,A),B)),C)),
inference(paramod,[status(thm)],[c_133,c_1239]) ).
cnf(c_1241,plain,
mult(A,ld(A,ld(A,mult(B,C)))) = ld(ld(ld(A,A),A),mult(mult(ld(A,A),ld(ld(A,A),B)),C)),
inference(paramod,[status(thm)],[c_133,c_1240]) ).
cnf(c_1242,plain,
mult(A,ld(A,ld(A,mult(B,C)))) = ld(A,mult(mult(ld(A,A),ld(ld(A,A),B)),C)),
inference(paramod,[status(thm)],[c_133,c_1241]) ).
cnf(c_135,plain,
mult(A,ld(A,ld(A,mult(B,C)))) = ld(A,mult(mult(A,ld(A,B)),C)),
inference(paramod,[status(thm)],[c_112,c_1242]) ).
cnf(c_1243,plain,
mult(A,mult(ld(ld(A,A),A),ld(ld(ld(A,A),A),B))) = mult(mult(ld(A,A),ld(ld(A,A),ld(ld(A,A),A))),B),
inference(paramod,[status(thm)],[c_133,c_25]) ).
cnf(c_1244,plain,
mult(A,mult(A,ld(ld(ld(A,A),A),B))) = mult(mult(ld(A,A),ld(ld(A,A),ld(ld(A,A),A))),B),
inference(paramod,[status(thm)],[c_133,c_1243]) ).
cnf(c_1245,plain,
mult(A,mult(A,ld(A,B))) = mult(mult(ld(A,A),ld(ld(A,A),ld(ld(A,A),A))),B),
inference(paramod,[status(thm)],[c_133,c_1244]) ).
cnf(c_1246,plain,
mult(A,mult(A,ld(A,B))) = mult(mult(ld(A,A),ld(ld(A,A),A)),B),
inference(paramod,[status(thm)],[c_133,c_1245]) ).
cnf(c_1247,plain,
mult(A,mult(A,ld(A,B))) = mult(mult(ld(A,A),A),B),
inference(paramod,[status(thm)],[c_133,c_1246]) ).
cnf(c_137,plain,
mult(A,mult(A,ld(A,B))) = mult(A,B),
inference(paramod,[status(thm)],[c_45,c_1247]) ).
cnf(c_1248,plain,
mult(mult(mult(A,B),ld(mult(A,mult(A,ld(A,B))),C)),D) = mult(mult(A,ld(A,C)),D),
inference(paramod,[status(thm)],[c_137,c_108]) ).
cnf(c_138,plain,
mult(mult(mult(A,B),ld(mult(A,B),C)),D) = mult(mult(A,ld(A,C)),D),
inference(paramod,[status(thm)],[c_137,c_1248]) ).
cnf(c_139,plain,
mult(rd(A,rd(B,C)),rd(B,C)) = mult(A,ld(C,C)),
inference(paramod,[status(thm)],[c_137,c_62]) ).
cnf(c_141,plain,
mult(mult(A,B),ld(C,C)) = mult(A,mult(rd(B,C),C)),
inference(paramod,[status(thm)],[c_137,c_60]) ).
cnf(c_1249,plain,
mult(ld(A,B),C) = mult(mult(A,ld(A,ld(A,B))),C),
inference(paramod,[status(thm)],[c_137,c_25]) ).
cnf(c_145,plain,
mult(mult(A,ld(A,ld(A,B))),C) = mult(ld(A,B),C),
inference(copy,[status(thm)],[c_1249]) ).
cnf(c_1250,plain,
mult(A,ld(A,A)) = mult(A,ld(ld(A,A),ld(A,A))),
inference(paramod,[status(thm)],[c_50,c_137]) ).
cnf(c_1251,plain,
A = mult(A,ld(ld(A,A),ld(A,A))),
inference(paramod,[status(thm)],[c_21,c_1250]) ).
cnf(c_149,plain,
mult(A,ld(ld(A,A),ld(A,A))) = A,
inference(copy,[status(thm)],[c_1251]) ).
cnf(c_1252,plain,
mult(A,ld(A,B)) = mult(mult(A,ld(A,B)),ld(B,B)),
inference(paramod,[status(thm)],[c_21,c_85]) ).
cnf(c_152,plain,
mult(mult(A,ld(A,B)),ld(B,B)) = mult(A,ld(A,B)),
inference(copy,[status(thm)],[c_1252]) ).
cnf(c_1253,plain,
mult(A,ld(A,B)) = mult(mult(A,ld(A,ld(B,B))),B),
inference(paramod,[status(thm)],[c_45,c_85]) ).
cnf(c_153,plain,
mult(mult(A,ld(A,ld(B,B))),B) = mult(A,ld(A,B)),
inference(copy,[status(thm)],[c_1253]) ).
cnf(c_158,plain,
mult(A,mult(mult(A,ld(A,B)),C)) = mult(A,mult(B,C)),
inference(paramod,[status(thm)],[c_85,c_137]) ).
cnf(c_1254,plain,
mult(A,ld(A,B)) = mult(mult(A,ld(A,B)),ld(ld(B,B),ld(B,B))),
inference(paramod,[status(thm)],[c_149,c_85]) ).
cnf(c_160,plain,
mult(mult(A,ld(A,B)),ld(ld(B,B),ld(B,B))) = mult(A,ld(A,B)),
inference(copy,[status(thm)],[c_1254]) ).
cnf(c_164,plain,
mult(ld(A,B),ld(ld(A,B),C)) = mult(A,ld(A,C)),
inference(paramod,[status(thm)],[c_152,c_41]) ).
cnf(c_1255,plain,
ld(ld(A,B),mult(A,ld(A,C))) = mult(ld(A,B),ld(ld(A,B),ld(ld(A,B),C))),
inference(paramod,[status(thm)],[c_153,c_71]) ).
cnf(c_165,plain,
ld(ld(A,B),mult(A,ld(A,C))) = mult(A,ld(A,ld(ld(A,B),C))),
inference(paramod,[status(thm)],[c_164,c_1255]) ).
cnf(c_180,plain,
rd(mult(A,ld(A,B)),ld(ld(A,C),mult(B,ld(mult(A,ld(A,B)),mult(A,ld(A,B)))))) = mult(rd(ld(A,C),ld(ld(A,C),mult(B,ld(mult(A,ld(A,B)),mult(A,ld(A,B)))))),ld(ld(A,C),mult(B,ld(mult(A,ld(A,B)),mult(A,ld(A,B)))))),
inference(paramod,[status(thm)],[c_21,c_26]) ).
cnf(c_1256,plain,
rd(mult(mult(A,ld(A,B)),ld(B,B)),ld(ld(A,C),B)) = mult(rd(ld(A,C),ld(ld(A,C),mult(B,ld(B,B)))),ld(ld(A,C),mult(B,ld(B,B)))),
inference(paramod,[status(thm)],[c_21,c_26]) ).
cnf(c_1257,plain,
rd(mult(A,ld(A,B)),ld(ld(A,C),B)) = mult(rd(ld(A,C),ld(ld(A,C),mult(B,ld(B,B)))),ld(ld(A,C),mult(B,ld(B,B)))),
inference(paramod,[status(thm)],[c_152,c_1256]) ).
cnf(c_1258,plain,
rd(mult(A,ld(A,B)),ld(ld(A,C),B)) = mult(rd(ld(A,C),ld(ld(A,C),B)),ld(ld(A,C),mult(B,ld(B,B)))),
inference(paramod,[status(thm)],[c_21,c_1257]) ).
cnf(c_181,plain,
rd(mult(A,ld(A,B)),ld(ld(A,C),B)) = mult(rd(ld(A,C),ld(ld(A,C),B)),ld(ld(A,C),B)),
inference(paramod,[status(thm)],[c_21,c_1258]) ).
cnf(c_1259,plain,
mult(rd(A,mult(rd(B,C),C)),rd(mult(B,C),C)) = mult(A,ld(C,C)),
inference(paramod,[status(thm)],[c_12,c_139]) ).
cnf(c_202,plain,
mult(rd(A,mult(rd(B,C),C)),mult(rd(B,C),C)) = mult(A,ld(C,C)),
inference(paramod,[status(thm)],[c_12,c_1259]) ).
cnf(c_1260,plain,
mult(rd(A,ld(B,B)),rd(B,B)) = mult(A,ld(B,B)),
inference(paramod,[status(thm)],[c_44,c_139]) ).
cnf(c_204,plain,
mult(rd(A,ld(B,B)),ld(B,B)) = mult(A,ld(B,B)),
inference(paramod,[status(thm)],[c_44,c_1260]) ).
cnf(c_1261,plain,
mult(ld(rd(A,B),rd(A,B)),rd(A,B)) = mult(rd(A,B),ld(B,B)),
inference(paramod,[status(thm)],[c_44,c_139]) ).
cnf(c_1262,plain,
rd(A,B) = mult(rd(A,B),ld(B,B)),
inference(paramod,[status(thm)],[c_45,c_1261]) ).
cnf(c_205,plain,
mult(rd(A,B),ld(B,B)) = rd(A,B),
inference(copy,[status(thm)],[c_1262]) ).
cnf(c_1263,plain,
mult(A,ld(A,A)) = rd(A,ld(A,A)),
inference(paramod,[status(thm)],[c_204,c_40]) ).
cnf(c_1264,plain,
A = rd(A,ld(A,A)),
inference(paramod,[status(thm)],[c_21,c_1263]) ).
cnf(c_213,plain,
rd(A,ld(A,A)) = A,
inference(copy,[status(thm)],[c_1264]) ).
cnf(c_1265,plain,
mult(rd(A,B),rd(B,ld(B,B))) = mult(A,ld(ld(B,B),ld(B,B))),
inference(paramod,[status(thm)],[c_213,c_139]) ).
cnf(c_215,plain,
mult(rd(A,B),B) = mult(A,ld(ld(B,B),ld(B,B))),
inference(paramod,[status(thm)],[c_213,c_1265]) ).
cnf(c_1266,plain,
mult(rd(A,mult(B,ld(ld(C,C),ld(C,C)))),mult(rd(B,C),C)) = mult(A,ld(C,C)),
inference(paramod,[status(thm)],[c_215,c_202]) ).
cnf(c_1267,plain,
mult(rd(A,mult(B,ld(ld(C,C),ld(C,C)))),mult(B,ld(ld(C,C),ld(C,C)))) = mult(A,ld(C,C)),
inference(paramod,[status(thm)],[c_215,c_1266]) ).
cnf(c_219,plain,
mult(A,ld(ld(mult(B,ld(ld(C,C),ld(C,C))),mult(B,ld(ld(C,C),ld(C,C)))),ld(mult(B,ld(ld(C,C),ld(C,C))),mult(B,ld(ld(C,C),ld(C,C)))))) = mult(A,ld(C,C)),
inference(paramod,[status(thm)],[c_215,c_1267]) ).
cnf(c_231,plain,
rd(mult(A,ld(A,B)),ld(ld(A,C),B)) = mult(ld(A,C),ld(ld(ld(ld(A,C),B),ld(ld(A,C),B)),ld(ld(ld(A,C),B),ld(ld(A,C),B)))),
inference(paramod,[status(thm)],[c_215,c_181]) ).
cnf(c_232,plain,
rd(mult(A,ld(A,B)),ld(ld(A,C),mult(B,ld(mult(A,ld(A,B)),mult(A,ld(A,B)))))) = mult(ld(A,C),ld(ld(ld(ld(A,C),mult(B,ld(mult(A,ld(A,B)),mult(A,ld(A,B))))),ld(ld(A,C),mult(B,ld(mult(A,ld(A,B)),mult(A,ld(A,B)))))),ld(ld(ld(A,C),mult(B,ld(mult(A,ld(A,B)),mult(A,ld(A,B))))),ld(ld(A,C),mult(B,ld(mult(A,ld(A,B)),mult(A,ld(A,B)))))))),
inference(paramod,[status(thm)],[c_215,c_180]) ).
cnf(c_243,plain,
mult(mult(A,B),ld(C,C)) = mult(A,mult(B,ld(ld(C,C),ld(C,C)))),
inference(paramod,[status(thm)],[c_215,c_141]) ).
cnf(c_251,plain,
mult(ld(A,A),ld(ld(B,B),ld(B,B))) = mult(A,ld(A,ld(B,B))),
inference(paramod,[status(thm)],[c_215,c_56]) ).
cnf(c_259,negated_conjecture,
( mult(mult(sK0,ld(ld(sK1,sK1),ld(sK1,sK1))),sK2) != mult(sK0,sK2)
| mult(sK0,mult(sK1,ld(sK1,sK2))) != mult(sK0,sK2) ),
inference(paramod,[status(thm)],[c_215,c_20]) ).
cnf(c_260,plain,
rd(mult(A,B),B) = mult(A,ld(ld(B,B),ld(B,B))),
inference(paramod,[status(thm)],[c_215,c_12]) ).
cnf(c_1268,plain,
mult(ld(A,A),ld(A,A)) = rd(A,A),
inference(paramod,[status(thm)],[c_44,c_205]) ).
cnf(c_265,plain,
mult(ld(A,A),ld(A,A)) = ld(A,A),
inference(paramod,[status(thm)],[c_44,c_1268]) ).
cnf(c_1269,plain,
ld(ld(A,A),ld(A,A)) = mult(ld(A,A),ld(ld(A,A),ld(A,A))),
inference(paramod,[status(thm)],[c_265,c_11]) ).
cnf(c_277,plain,
ld(ld(A,A),ld(A,A)) = ld(A,A),
inference(paramod,[status(thm)],[c_21,c_1269]) ).
cnf(c_1270,plain,
mult(A,ld(A,ld(B,B))) = mult(mult(A,ld(A,ld(B,B))),ld(B,B)),
inference(paramod,[status(thm)],[c_265,c_85]) ).
cnf(c_278,plain,
mult(mult(A,ld(A,ld(B,B))),ld(B,B)) = mult(A,ld(A,ld(B,B))),
inference(copy,[status(thm)],[c_1270]) ).
cnf(c_285,plain,
rd(mult(A,B),B) = mult(A,ld(B,B)),
inference(paramod,[status(thm)],[c_277,c_260]) ).
cnf(c_286,negated_conjecture,
( mult(mult(sK0,ld(sK1,sK1)),sK2) != mult(sK0,sK2)
| mult(sK0,mult(sK1,ld(sK1,sK2))) != mult(sK0,sK2) ),
inference(paramod,[status(thm)],[c_277,c_259]) ).
cnf(c_294,plain,
mult(ld(A,A),ld(B,B)) = mult(A,ld(A,ld(B,B))),
inference(paramod,[status(thm)],[c_277,c_251]) ).
cnf(c_300,plain,
mult(mult(A,B),ld(C,C)) = mult(A,mult(B,ld(C,C))),
inference(paramod,[status(thm)],[c_277,c_243]) ).
cnf(c_310,plain,
rd(mult(A,ld(A,B)),ld(ld(A,C),mult(B,ld(mult(A,ld(A,B)),mult(A,ld(A,B)))))) = mult(ld(A,C),ld(ld(ld(A,C),mult(B,ld(mult(A,ld(A,B)),mult(A,ld(A,B))))),ld(ld(A,C),mult(B,ld(mult(A,ld(A,B)),mult(A,ld(A,B))))))),
inference(paramod,[status(thm)],[c_277,c_232]) ).
cnf(c_311,plain,
rd(mult(A,ld(A,B)),ld(ld(A,C),B)) = mult(ld(A,C),ld(ld(ld(A,C),B),ld(ld(A,C),B))),
inference(paramod,[status(thm)],[c_277,c_231]) ).
cnf(c_1271,plain,
mult(A,ld(ld(mult(B,ld(C,C)),mult(B,ld(ld(C,C),ld(C,C)))),ld(mult(B,ld(ld(C,C),ld(C,C))),mult(B,ld(ld(C,C),ld(C,C)))))) = mult(A,ld(C,C)),
inference(paramod,[status(thm)],[c_277,c_219]) ).
cnf(c_1272,plain,
mult(A,ld(ld(mult(B,ld(C,C)),mult(B,ld(C,C))),ld(mult(B,ld(ld(C,C),ld(C,C))),mult(B,ld(ld(C,C),ld(C,C)))))) = mult(A,ld(C,C)),
inference(paramod,[status(thm)],[c_277,c_1271]) ).
cnf(c_1273,plain,
mult(A,ld(ld(mult(B,ld(C,C)),mult(B,ld(C,C))),ld(mult(B,ld(C,C)),mult(B,ld(ld(C,C),ld(C,C)))))) = mult(A,ld(C,C)),
inference(paramod,[status(thm)],[c_277,c_1272]) ).
cnf(c_1274,plain,
mult(A,ld(ld(mult(B,ld(C,C)),mult(B,ld(C,C))),ld(mult(B,ld(C,C)),mult(B,ld(C,C))))) = mult(A,ld(C,C)),
inference(paramod,[status(thm)],[c_277,c_1273]) ).
cnf(c_321,plain,
mult(A,ld(mult(B,ld(C,C)),mult(B,ld(C,C)))) = mult(A,ld(C,C)),
inference(paramod,[status(thm)],[c_277,c_1274]) ).
cnf(c_322,plain,
mult(rd(A,B),B) = mult(A,ld(B,B)),
inference(paramod,[status(thm)],[c_277,c_215]) ).
cnf(c_1275,plain,
mult(mult(A,ld(A,B)),ld(B,B)) = mult(A,ld(A,B)),
inference(paramod,[status(thm)],[c_277,c_160]) ).
cnf(c_323,plain,
mult(A,mult(ld(A,B),ld(B,B))) = mult(A,ld(A,B)),
inference(paramod,[status(thm)],[c_300,c_1275]) ).
cnf(c_328,plain,
mult(A,mult(ld(A,ld(B,B)),ld(B,B))) = mult(A,ld(A,ld(B,B))),
inference(paramod,[status(thm)],[c_300,c_278]) ).
cnf(c_1276,plain,
mult(A,ld(A,mult(B,ld(C,C)))) = mult(mult(A,ld(A,rd(B,C))),C),
inference(paramod,[status(thm)],[c_322,c_85]) ).
cnf(c_1277,plain,
mult(mult(A,ld(A,B)),ld(C,C)) = mult(mult(A,ld(A,rd(B,C))),C),
inference(paramod,[status(thm)],[c_85,c_1276]) ).
cnf(c_1278,plain,
mult(A,mult(ld(A,B),ld(C,C))) = mult(mult(A,ld(A,rd(B,C))),C),
inference(paramod,[status(thm)],[c_300,c_1277]) ).
cnf(c_337,plain,
mult(mult(A,ld(A,rd(B,C))),C) = mult(A,mult(ld(A,B),ld(C,C))),
inference(copy,[status(thm)],[c_1278]) ).
cnf(c_1279,plain,
mult(mult(A,ld(B,B)),B) = mult(mult(A,B),ld(B,B)),
inference(paramod,[status(thm)],[c_285,c_322]) ).
cnf(c_1280,plain,
mult(mult(A,ld(B,B)),B) = mult(A,mult(B,ld(B,B))),
inference(paramod,[status(thm)],[c_300,c_1279]) ).
cnf(c_338,plain,
mult(mult(A,ld(B,B)),B) = mult(A,B),
inference(paramod,[status(thm)],[c_21,c_1280]) ).
cnf(c_1281,plain,
mult(mult(A,ld(A,ld(A,B))),ld(ld(A,B),ld(A,B))) = ld(A,B),
inference(paramod,[status(thm)],[c_21,c_145]) ).
cnf(c_1282,plain,
mult(A,mult(ld(A,ld(A,B)),ld(ld(A,B),ld(A,B)))) = ld(A,B),
inference(paramod,[status(thm)],[c_300,c_1281]) ).
cnf(c_348,plain,
mult(A,ld(A,ld(A,B))) = ld(A,B),
inference(paramod,[status(thm)],[c_323,c_1282]) ).
cnf(c_1283,plain,
mult(mult(A,ld(A,ld(A,B))),mult(ld(A,B),ld(mult(A,ld(A,ld(A,B))),C))) = mult(mult(A,ld(A,ld(A,B))),C),
inference(paramod,[status(thm)],[c_145,c_137]) ).
cnf(c_1284,plain,
mult(ld(A,B),mult(ld(A,B),ld(mult(A,ld(A,ld(A,B))),C))) = mult(mult(A,ld(A,ld(A,B))),C),
inference(paramod,[status(thm)],[c_348,c_1283]) ).
cnf(c_1285,plain,
mult(ld(A,B),mult(ld(A,B),ld(ld(A,B),C))) = mult(mult(A,ld(A,ld(A,B))),C),
inference(paramod,[status(thm)],[c_348,c_1284]) ).
cnf(c_1286,plain,
mult(ld(A,B),mult(A,ld(A,C))) = mult(mult(A,ld(A,ld(A,B))),C),
inference(paramod,[status(thm)],[c_164,c_1285]) ).
cnf(c_349,plain,
mult(ld(A,B),mult(A,ld(A,C))) = mult(ld(A,B),C),
inference(paramod,[status(thm)],[c_348,c_1286]) ).
cnf(c_1287,plain,
ld(A,mult(B,C)) = ld(A,mult(mult(A,ld(A,B)),C)),
inference(paramod,[status(thm)],[c_348,c_135]) ).
cnf(c_351,plain,
ld(A,mult(mult(A,ld(A,B)),C)) = ld(A,mult(B,C)),
inference(copy,[status(thm)],[c_1287]) ).
cnf(c_1288,plain,
rd(mult(A,ld(A,B)),B) = mult(mult(A,ld(A,ld(B,B))),ld(B,B)),
inference(paramod,[status(thm)],[c_153,c_285]) ).
cnf(c_1289,plain,
rd(mult(A,ld(A,B)),B) = mult(A,mult(ld(A,ld(B,B)),ld(B,B))),
inference(paramod,[status(thm)],[c_300,c_1288]) ).
cnf(c_402,plain,
rd(mult(A,ld(A,B)),B) = mult(A,ld(A,ld(B,B))),
inference(paramod,[status(thm)],[c_328,c_1289]) ).
cnf(c_1290,plain,
ld(ld(A,B),mult(A,ld(A,C))) = mult(ld(A,B),ld(ld(A,B),ld(ld(A,B),C))),
inference(paramod,[status(thm)],[c_164,c_11]) ).
cnf(c_1291,plain,
mult(A,ld(A,ld(ld(A,B),C))) = mult(ld(A,B),ld(ld(A,B),ld(ld(A,B),C))),
inference(paramod,[status(thm)],[c_165,c_1290]) ).
cnf(c_436,plain,
mult(A,ld(A,ld(ld(A,B),C))) = ld(ld(A,B),C),
inference(paramod,[status(thm)],[c_348,c_1291]) ).
cnf(c_444,plain,
ld(ld(A,B),mult(A,ld(A,C))) = ld(ld(A,B),C),
inference(paramod,[status(thm)],[c_436,c_165]) ).
cnf(c_1292,plain,
mult(mult(A,ld(A,ld(B,B))),B) = mult(ld(A,A),B),
inference(paramod,[status(thm)],[c_294,c_338]) ).
cnf(c_1293,plain,
mult(A,ld(A,B)) = mult(ld(A,A),B),
inference(paramod,[status(thm)],[c_153,c_1292]) ).
cnf(c_534,plain,
mult(ld(A,A),B) = mult(A,ld(A,B)),
inference(copy,[status(thm)],[c_1293]) ).
cnf(c_540,plain,
mult(ld(A,A),ld(ld(A,B),C)) = ld(ld(A,B),C),
inference(paramod,[status(thm)],[c_534,c_436]) ).
cnf(c_541,plain,
mult(ld(A,A),ld(A,B)) = ld(A,B),
inference(paramod,[status(thm)],[c_534,c_348]) ).
cnf(c_542,negated_conjecture,
( mult(mult(sK0,ld(sK1,sK1)),sK2) != mult(sK0,sK2)
| mult(sK0,mult(ld(sK1,sK1),sK2)) != mult(sK0,sK2) ),
inference(paramod,[status(thm)],[c_534,c_286]) ).
cnf(c_1294,plain,
mult(ld(A,A),mult(A,B)) = mult(A,mult(A,ld(A,B))),
inference(paramod,[status(thm)],[c_11,c_534]) ).
cnf(c_544,plain,
mult(ld(A,A),mult(A,B)) = mult(A,B),
inference(paramod,[status(thm)],[c_137,c_1294]) ).
cnf(c_1295,plain,
mult(ld(A,A),mult(A,ld(A,ld(ld(A,A),B)))) = mult(ld(A,A),B),
inference(paramod,[status(thm)],[c_534,c_137]) ).
cnf(c_1296,plain,
mult(ld(A,A),mult(ld(A,A),ld(ld(A,A),B))) = mult(ld(A,A),B),
inference(paramod,[status(thm)],[c_534,c_1295]) ).
cnf(c_1297,plain,
mult(ld(A,A),ld(ld(A,A),B)) = mult(ld(A,A),B),
inference(paramod,[status(thm)],[c_540,c_1296]) ).
cnf(c_545,plain,
ld(ld(A,A),B) = mult(ld(A,A),B),
inference(paramod,[status(thm)],[c_540,c_1297]) ).
cnf(c_547,plain,
mult(A,mult(ld(A,A),B)) = mult(A,B),
inference(paramod,[status(thm)],[c_534,c_137]) ).
cnf(c_561,plain,
mult(A,mult(ld(mult(A,ld(A,B)),mult(A,ld(A,B))),C)) = mult(A,mult(B,ld(mult(A,ld(A,B)),C))),
inference(paramod,[status(thm)],[c_534,c_158]) ).
cnf(c_1298,plain,
mult(mult(A,ld(A,ld(B,B))),B) = mult(mult(A,C),ld(mult(A,C),B)),
inference(paramod,[status(thm)],[c_138,c_153]) ).
cnf(c_1299,plain,
mult(A,ld(A,B)) = mult(mult(A,C),ld(mult(A,C),B)),
inference(paramod,[status(thm)],[c_153,c_1298]) ).
cnf(c_580,plain,
mult(mult(A,B),ld(mult(A,B),C)) = mult(A,ld(A,C)),
inference(copy,[status(thm)],[c_1299]) ).
cnf(c_1300,plain,
rd(mult(A,B),mult(A,B)) = mult(ld(A,A),ld(mult(A,B),mult(A,B))),
inference(paramod,[status(thm)],[c_544,c_285]) ).
cnf(c_1301,plain,
ld(mult(A,B),mult(A,B)) = mult(ld(A,A),ld(mult(A,B),mult(A,B))),
inference(paramod,[status(thm)],[c_44,c_1300]) ).
cnf(c_599,plain,
mult(ld(A,A),ld(mult(A,B),mult(A,B))) = ld(mult(A,B),mult(A,B)),
inference(copy,[status(thm)],[c_1301]) ).
cnf(c_1302,plain,
mult(ld(A,A),mult(ld(A,A),mult(B,C))) = mult(mult(ld(A,A),ld(ld(A,A),B)),C),
inference(paramod,[status(thm)],[c_545,c_85]) ).
cnf(c_1303,plain,
mult(ld(A,A),mult(ld(A,A),mult(B,C))) = mult(mult(ld(A,A),mult(ld(A,A),B)),C),
inference(paramod,[status(thm)],[c_545,c_1302]) ).
cnf(c_604,plain,
mult(mult(ld(A,A),mult(ld(A,A),B)),C) = mult(ld(A,A),mult(ld(A,A),mult(B,C))),
inference(copy,[status(thm)],[c_1303]) ).
cnf(c_1304,plain,
mult(mult(ld(A,A),ld(A,A)),B) = mult(ld(A,A),ld(ld(A,A),B)),
inference(paramod,[status(thm)],[c_545,c_534]) ).
cnf(c_1305,plain,
mult(ld(A,A),B) = mult(ld(A,A),ld(ld(A,A),B)),
inference(paramod,[status(thm)],[c_541,c_1304]) ).
cnf(c_1306,plain,
mult(ld(A,A),B) = mult(ld(A,A),mult(ld(A,A),B)),
inference(paramod,[status(thm)],[c_545,c_1305]) ).
cnf(c_607,plain,
mult(ld(A,A),mult(ld(A,A),B)) = mult(ld(A,A),B),
inference(copy,[status(thm)],[c_1306]) ).
cnf(c_1307,plain,
mult(mult(ld(A,A),B),C) = mult(ld(A,A),mult(ld(A,A),mult(B,C))),
inference(paramod,[status(thm)],[c_607,c_604]) ).
cnf(c_615,plain,
mult(mult(ld(A,A),B),C) = mult(ld(A,A),mult(B,C)),
inference(paramod,[status(thm)],[c_607,c_1307]) ).
cnf(c_1308,plain,
mult(mult(A,ld(B,B)),ld(C,C)) = mult(rd(A,B),mult(B,ld(C,C))),
inference(paramod,[status(thm)],[c_322,c_300]) ).
cnf(c_1309,plain,
mult(A,mult(ld(B,B),ld(C,C))) = mult(rd(A,B),mult(B,ld(C,C))),
inference(paramod,[status(thm)],[c_300,c_1308]) ).
cnf(c_642,plain,
mult(rd(A,B),mult(B,ld(C,C))) = mult(A,mult(ld(B,B),ld(C,C))),
inference(copy,[status(thm)],[c_1309]) ).
cnf(c_644,plain,
mult(mult(A,mult(B,ld(C,C))),C) = mult(mult(A,B),C),
inference(paramod,[status(thm)],[c_300,c_338]) ).
cnf(c_1310,plain,
mult(ld(A,B),ld(C,C)) = mult(ld(A,A),mult(ld(A,B),ld(C,C))),
inference(paramod,[status(thm)],[c_541,c_300]) ).
cnf(c_649,plain,
mult(ld(A,A),mult(ld(A,B),ld(C,C))) = mult(ld(A,B),ld(C,C)),
inference(copy,[status(thm)],[c_1310]) ).
cnf(c_1311,plain,
ld(A,mult(A,ld(A,B))) = mult(A,ld(A,mult(ld(A,B),ld(B,B)))),
inference(paramod,[status(thm)],[c_323,c_11]) ).
cnf(c_1312,plain,
mult(A,ld(A,ld(A,B))) = mult(A,ld(A,mult(ld(A,B),ld(B,B)))),
inference(paramod,[status(thm)],[c_11,c_1311]) ).
cnf(c_1313,plain,
mult(ld(A,A),ld(A,B)) = mult(A,ld(A,mult(ld(A,B),ld(B,B)))),
inference(paramod,[status(thm)],[c_534,c_1312]) ).
cnf(c_1314,plain,
ld(A,B) = mult(A,ld(A,mult(ld(A,B),ld(B,B)))),
inference(paramod,[status(thm)],[c_541,c_1313]) ).
cnf(c_1315,plain,
ld(A,B) = mult(ld(A,A),mult(ld(A,B),ld(B,B))),
inference(paramod,[status(thm)],[c_534,c_1314]) ).
cnf(c_1316,plain,
ld(A,B) = mult(ld(A,B),ld(B,B)),
inference(paramod,[status(thm)],[c_649,c_1315]) ).
cnf(c_664,plain,
mult(ld(A,B),ld(B,B)) = ld(A,B),
inference(copy,[status(thm)],[c_1316]) ).
cnf(c_1317,plain,
mult(A,mult(mult(A,ld(A,B)),ld(mult(A,ld(A,B)),C))) = mult(A,mult(B,mult(ld(mult(A,ld(A,B)),C),ld(C,C)))),
inference(paramod,[status(thm)],[c_323,c_158]) ).
cnf(c_1318,plain,
mult(A,mult(A,ld(A,C))) = mult(A,mult(B,mult(ld(mult(A,ld(A,B)),C),ld(C,C)))),
inference(paramod,[status(thm)],[c_580,c_1317]) ).
cnf(c_1319,plain,
mult(A,C) = mult(A,mult(B,mult(ld(mult(A,ld(A,B)),C),ld(C,C)))),
inference(paramod,[status(thm)],[c_137,c_1318]) ).
cnf(c_1320,plain,
mult(A,C) = mult(A,mult(B,ld(mult(A,ld(A,B)),C))),
inference(paramod,[status(thm)],[c_664,c_1319]) ).
cnf(c_666,plain,
mult(A,mult(B,ld(mult(A,ld(A,B)),C))) = mult(A,C),
inference(copy,[status(thm)],[c_1320]) ).
cnf(c_668,plain,
mult(A,mult(ld(mult(A,ld(A,B)),mult(A,ld(A,B))),C)) = mult(A,C),
inference(paramod,[status(thm)],[c_666,c_561]) ).
cnf(c_1321,plain,
ld(ld(A,B),ld(A,B)) = mult(ld(A,B),ld(ld(A,B),ld(B,B))),
inference(paramod,[status(thm)],[c_664,c_11]) ).
cnf(c_669,plain,
ld(ld(A,B),ld(A,B)) = mult(A,ld(A,ld(B,B))),
inference(paramod,[status(thm)],[c_164,c_1321]) ).
cnf(c_1322,plain,
rd(mult(A,ld(A,B)),ld(ld(A,C),B)) = mult(ld(A,C),mult(ld(A,C),ld(ld(A,C),ld(B,B)))),
inference(paramod,[status(thm)],[c_669,c_311]) ).
cnf(c_1323,plain,
rd(mult(A,ld(A,B)),ld(ld(A,C),B)) = mult(ld(A,C),mult(A,ld(A,ld(B,B)))),
inference(paramod,[status(thm)],[c_164,c_1322]) ).
cnf(c_695,plain,
rd(mult(A,ld(A,B)),ld(ld(A,C),B)) = mult(ld(A,C),ld(B,B)),
inference(paramod,[status(thm)],[c_349,c_1323]) ).
cnf(c_1324,plain,
rd(mult(A,ld(A,B)),ld(ld(A,C),mult(B,ld(mult(A,ld(A,B)),mult(A,ld(A,B)))))) = mult(ld(A,C),mult(ld(A,C),ld(ld(A,C),ld(mult(B,ld(mult(A,ld(A,B)),mult(A,ld(A,B)))),mult(B,ld(mult(A,ld(A,B)),mult(A,ld(A,B)))))))),
inference(paramod,[status(thm)],[c_669,c_310]) ).
cnf(c_1325,plain,
rd(mult(A,ld(A,B)),ld(ld(A,C),mult(B,ld(mult(A,ld(A,B)),mult(A,ld(A,B)))))) = mult(ld(A,C),mult(A,ld(A,ld(mult(B,ld(mult(A,ld(A,B)),mult(A,ld(A,B)))),mult(B,ld(mult(A,ld(A,B)),mult(A,ld(A,B)))))))),
inference(paramod,[status(thm)],[c_164,c_1324]) ).
cnf(c_1326,plain,
rd(mult(A,ld(A,B)),ld(ld(A,C),mult(B,ld(mult(A,ld(A,B)),mult(A,ld(A,B)))))) = mult(ld(A,C),mult(ld(A,A),ld(mult(B,ld(mult(A,ld(A,B)),mult(A,ld(A,B)))),mult(B,ld(mult(A,ld(A,B)),mult(A,ld(A,B))))))),
inference(paramod,[status(thm)],[c_534,c_1325]) ).
cnf(c_1327,plain,
rd(mult(A,ld(A,B)),ld(ld(A,C),mult(B,ld(mult(A,ld(A,B)),mult(A,ld(A,B)))))) = mult(ld(A,C),mult(ld(A,A),ld(mult(A,ld(A,B)),mult(A,ld(A,B))))),
inference(paramod,[status(thm)],[c_321,c_1326]) ).
cnf(c_696,plain,
rd(mult(A,ld(A,B)),ld(ld(A,C),mult(B,ld(mult(A,ld(A,B)),mult(A,ld(A,B)))))) = mult(ld(A,C),ld(mult(A,ld(A,B)),mult(A,ld(A,B)))),
inference(paramod,[status(thm)],[c_599,c_1327]) ).
cnf(c_1328,plain,
ld(A,mult(mult(A,ld(A,rd(B,C))),C)) = ld(A,mult(B,ld(C,C))),
inference(paramod,[status(thm)],[c_322,c_351]) ).
cnf(c_1329,plain,
ld(A,mult(A,mult(ld(A,B),ld(C,C)))) = ld(A,mult(B,ld(C,C))),
inference(paramod,[status(thm)],[c_337,c_1328]) ).
cnf(c_1330,plain,
mult(A,ld(A,mult(ld(A,B),ld(C,C)))) = ld(A,mult(B,ld(C,C))),
inference(paramod,[status(thm)],[c_11,c_1329]) ).
cnf(c_1331,plain,
mult(ld(A,A),mult(ld(A,B),ld(C,C))) = ld(A,mult(B,ld(C,C))),
inference(paramod,[status(thm)],[c_534,c_1330]) ).
cnf(c_1332,plain,
mult(ld(A,B),ld(C,C)) = ld(A,mult(B,ld(C,C))),
inference(paramod,[status(thm)],[c_649,c_1331]) ).
cnf(c_749,plain,
ld(A,mult(B,ld(C,C))) = mult(ld(A,B),ld(C,C)),
inference(copy,[status(thm)],[c_1332]) ).
cnf(c_764,plain,
rd(mult(A,ld(A,B)),mult(ld(ld(A,C),B),ld(mult(A,ld(A,B)),mult(A,ld(A,B))))) = mult(ld(A,C),ld(mult(A,ld(A,B)),mult(A,ld(A,B)))),
inference(paramod,[status(thm)],[c_749,c_696]) ).
cnf(c_1333,plain,
ld(mult(A,ld(A,B)),mult(A,ld(A,C))) = ld(ld(A,mult(A,B)),C),
inference(paramod,[status(thm)],[c_11,c_444]) ).
cnf(c_823,plain,
ld(mult(A,ld(A,B)),mult(A,ld(A,C))) = ld(mult(A,ld(A,B)),C),
inference(paramod,[status(thm)],[c_11,c_1333]) ).
cnf(c_1334,plain,
mult(ld(ld(A,B),C),ld(mult(A,ld(A,C)),mult(A,ld(A,C)))) = ld(ld(A,B),mult(A,ld(A,C))),
inference(paramod,[status(thm)],[c_444,c_664]) ).
cnf(c_1335,plain,
mult(ld(ld(A,B),C),ld(mult(A,ld(A,C)),C)) = ld(ld(A,B),mult(A,ld(A,C))),
inference(paramod,[status(thm)],[c_823,c_1334]) ).
cnf(c_832,plain,
mult(ld(ld(A,B),C),ld(mult(A,ld(A,C)),C)) = ld(ld(A,B),C),
inference(paramod,[status(thm)],[c_444,c_1335]) ).
cnf(c_1336,plain,
rd(mult(ld(A,B),ld(ld(A,B),C)),mult(A,ld(A,C))) = mult(ld(A,B),ld(ld(A,B),ld(mult(A,ld(A,C)),mult(A,ld(A,C))))),
inference(paramod,[status(thm)],[c_444,c_402]) ).
cnf(c_1337,plain,
rd(mult(A,ld(A,C)),mult(A,ld(A,C))) = mult(ld(A,B),ld(ld(A,B),ld(mult(A,ld(A,C)),mult(A,ld(A,C))))),
inference(paramod,[status(thm)],[c_164,c_1336]) ).
cnf(c_1338,plain,
ld(mult(A,ld(A,C)),mult(A,ld(A,C))) = mult(ld(A,B),ld(ld(A,B),ld(mult(A,ld(A,C)),mult(A,ld(A,C))))),
inference(paramod,[status(thm)],[c_44,c_1337]) ).
cnf(c_1339,plain,
ld(mult(A,ld(A,C)),C) = mult(ld(A,B),ld(ld(A,B),ld(mult(A,ld(A,C)),mult(A,ld(A,C))))),
inference(paramod,[status(thm)],[c_823,c_1338]) ).
cnf(c_1340,plain,
ld(mult(A,ld(A,C)),C) = mult(ld(A,B),ld(ld(A,B),ld(mult(A,ld(A,C)),C))),
inference(paramod,[status(thm)],[c_823,c_1339]) ).
cnf(c_1341,plain,
ld(mult(A,ld(A,C)),C) = mult(A,ld(A,ld(mult(A,ld(A,C)),C))),
inference(paramod,[status(thm)],[c_164,c_1340]) ).
cnf(c_1342,plain,
ld(mult(A,ld(A,C)),C) = mult(ld(A,A),ld(mult(A,ld(A,C)),C)),
inference(paramod,[status(thm)],[c_534,c_1341]) ).
cnf(c_834,plain,
mult(ld(A,A),ld(mult(A,ld(A,B)),B)) = ld(mult(A,ld(A,B)),B),
inference(copy,[status(thm)],[c_1342]) ).
cnf(c_1343,plain,
rd(mult(A,ld(A,B)),mult(ld(ld(A,C),B),ld(mult(A,ld(A,B)),B))) = mult(ld(A,C),ld(mult(A,ld(A,B)),mult(A,ld(A,B)))),
inference(paramod,[status(thm)],[c_823,c_764]) ).
cnf(c_1344,plain,
rd(mult(A,ld(A,B)),ld(ld(A,C),B)) = mult(ld(A,C),ld(mult(A,ld(A,B)),mult(A,ld(A,B)))),
inference(paramod,[status(thm)],[c_832,c_1343]) ).
cnf(c_1345,plain,
mult(ld(A,C),ld(B,B)) = mult(ld(A,C),ld(mult(A,ld(A,B)),mult(A,ld(A,B)))),
inference(paramod,[status(thm)],[c_695,c_1344]) ).
cnf(c_1346,plain,
mult(ld(A,C),ld(B,B)) = mult(ld(A,C),ld(mult(A,ld(A,B)),B)),
inference(paramod,[status(thm)],[c_823,c_1345]) ).
cnf(c_838,plain,
mult(ld(A,B),ld(mult(A,ld(A,C)),C)) = mult(ld(A,B),ld(C,C)),
inference(copy,[status(thm)],[c_1346]) ).
cnf(c_843,plain,
mult(A,mult(ld(mult(A,ld(A,B)),B),C)) = mult(A,C),
inference(paramod,[status(thm)],[c_823,c_668]) ).
cnf(c_1347,plain,
mult(ld(A,A),ld(B,B)) = ld(mult(A,ld(A,B)),B),
inference(paramod,[status(thm)],[c_838,c_834]) ).
cnf(c_859,plain,
ld(mult(A,ld(A,B)),B) = mult(ld(A,A),ld(B,B)),
inference(copy,[status(thm)],[c_1347]) ).
cnf(c_1348,plain,
mult(A,mult(mult(ld(A,A),ld(B,B)),C)) = mult(A,C),
inference(paramod,[status(thm)],[c_859,c_843]) ).
cnf(c_1349,plain,
mult(A,mult(ld(A,A),mult(ld(B,B),C))) = mult(A,C),
inference(paramod,[status(thm)],[c_615,c_1348]) ).
cnf(c_865,plain,
mult(A,mult(ld(B,B),C)) = mult(A,C),
inference(paramod,[status(thm)],[c_547,c_1349]) ).
cnf(c_873,plain,
mult(rd(A,B),mult(B,ld(C,C))) = mult(A,ld(C,C)),
inference(paramod,[status(thm)],[c_865,c_642]) ).
cnf(c_1350,negated_conjecture,
( mult(mult(sK0,ld(sK1,sK1)),sK2) != mult(sK0,sK2)
| mult(sK0,sK2) != mult(sK0,sK2) ),
inference(paramod,[status(thm)],[c_865,c_542]) ).
cnf(c_876,negated_conjecture,
mult(mult(sK0,ld(sK1,sK1)),sK2) != mult(sK0,sK2),
inference(copy,[status(thm)],[c_1350]) ).
cnf(c_1351,plain,
mult(mult(rd(A,B),mult(B,ld(C,C))),C) = mult(mult(A,ld(B,B)),C),
inference(paramod,[status(thm)],[c_322,c_644]) ).
cnf(c_1352,plain,
mult(mult(A,ld(C,C)),C) = mult(mult(A,ld(B,B)),C),
inference(paramod,[status(thm)],[c_873,c_1351]) ).
cnf(c_1353,plain,
mult(A,C) = mult(mult(A,ld(B,B)),C),
inference(paramod,[status(thm)],[c_338,c_1352]) ).
cnf(c_1209,plain,
mult(mult(A,ld(B,B)),C) = mult(A,C),
inference(copy,[status(thm)],[c_1353]) ).
cnf(c_1210,plain,
$false,
inference(resolve,[status(thm)],[c_1209,c_876]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP683+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.14/0.40 % Computer : n007.cluster.edu
% 0.14/0.40 % Model : x86_64 x86_64
% 0.14/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.40 % Memory : 8046.5625MB
% 0.14/0.40 % OS : Linux 6.8.0-71-generic
% 0.14/0.40 % CPULimit : 300
% 0.14/0.40 % WCLimit : 300
% 0.14/0.40 % DateTime : Fri Sep 25 15:34:54 UTC 2026
% 0.14/0.40 % CPUTime :
% 0.17/0.41 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.17/0.41 % Process 1373207 was started by sandbox2 on n007,
% 0.17/0.41 % Fri Sep 25 15:34:54 2026
% 0.17/0.41 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.17/0.41
% 0.17/0.41 % From the command line: assign(max_seconds, 300).
% 1.80/0.72
% 1.80/0.72 % SZS status Theorem for theBenchmark
% 1.80/0.72
% 1.80/0.72 % Proof 1 at 0.22 (+ 0.06) seconds.
% 1.80/0.72 % Length of proof is 129.
% 1.80/0.72 % Level of proof is 27.
% 1.80/0.72 % Maximum clause weight is 99.000.
% 1.80/0.72 % Given clauses 92.
% 1.80/0.72
% 1.80/0.72 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------