%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP685+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n008.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:12 AM UTC 2026
% Result : Theorem 0.88s 0.51s
% Output : CNFRefutation 0.88s
% Verified :
% SZS Type : Refutation
% Derivation depth : 58
% Number of leaves : 8
% Syntax : Number of formulae : 276 ( 257 unt; 0 def)
% Number of atoms : 295 ( 294 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 57 ( 38 ~; 17 |; 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 : 626 ( 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,
! [X6,X7,X8] :
( rd(mult(X6,rd(X7,X8)),rd(X7,X8)) = rd(mult(X6,X8),X8)
& rd(mult(X6,ld(X7,X8)),ld(X7,X8)) = rd(mult(X6,X8),X8) ),
file('theBenchmark.p',goals) ).
fof(goals_neg,negated_conjecture,
~ ! [X6,X7,X8] :
( rd(mult(X6,rd(X7,X8)),rd(X7,X8)) = rd(mult(X6,X8),X8)
& rd(mult(X6,ld(X7,X8)),ld(X7,X8)) = rd(mult(X6,X8),X8) ),
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_869,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_869]) ).
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_870,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_870]) ).
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_871,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_871]) ).
fof(nnf_8,plain,
? [X6,X7,X8] :
( rd(mult(X6,rd(X7,X8)),rd(X7,X8)) != rd(mult(X6,X8),X8)
| rd(mult(X6,ld(X7,X8)),ld(X7,X8)) != rd(mult(X6,X8),X8) ),
inference(fof_nnf,[status(thm)],[goals_neg]) ).
fof(sk_goals_neg,plain,
( rd(mult(sK0,rd(sK1,sK2)),rd(sK1,sK2)) != rd(mult(sK0,sK2),sK2)
| rd(mult(sK0,ld(sK1,sK2)),ld(sK1,sK2)) != rd(mult(sK0,sK2),sK2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2]),skolemize(X6,sK0),skolemize(X7,sK1),skolemize(X8,sK2)],[nnf_8]) ).
cnf(c_19,negated_conjecture,
( rd(mult(sK0,rd(sK1,sK2)),rd(sK1,sK2)) != rd(mult(sK0,sK2),sK2)
| rd(mult(sK0,ld(sK1,sK2)),ld(sK1,sK2)) != rd(mult(sK0,sK2),sK2) ),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_872,negated_conjecture,
( rd(mult(sK0,rd(sK1,sK2)),rd(sK1,sK2)) != rd(mult(sK0,sK2),sK2)
| mult(rd(sK0,ld(sK1,sK2)),ld(sK1,sK2)) != rd(mult(sK0,sK2),sK2) ),
inference(paramod,[status(thm)],[c_12,c_19]) ).
cnf(c_873,negated_conjecture,
( rd(mult(sK0,rd(sK1,sK2)),rd(sK1,sK2)) != rd(mult(sK0,sK2),sK2)
| mult(rd(sK0,ld(sK1,sK2)),ld(sK1,sK2)) != mult(rd(sK0,sK2),sK2) ),
inference(paramod,[status(thm)],[c_12,c_872]) ).
cnf(c_874,negated_conjecture,
( mult(rd(sK0,rd(sK1,sK2)),rd(sK1,sK2)) != rd(mult(sK0,sK2),sK2)
| mult(rd(sK0,ld(sK1,sK2)),ld(sK1,sK2)) != mult(rd(sK0,sK2),sK2) ),
inference(paramod,[status(thm)],[c_12,c_873]) ).
cnf(c_20,negated_conjecture,
( mult(rd(sK0,rd(sK1,sK2)),rd(sK1,sK2)) != mult(rd(sK0,sK2),sK2)
| mult(rd(sK0,ld(sK1,sK2)),ld(sK1,sK2)) != mult(rd(sK0,sK2),sK2) ),
inference(paramod,[status(thm)],[c_12,c_874]) ).
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_875,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_875]) ).
cnf(c_876,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_876]) ).
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_877,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_877]) ).
cnf(c_878,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_878]) ).
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_879,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_879]) ).
cnf(c_880,plain,
rd(A,A) = mult(rd(rd(A,A),A),A),
inference(paramod,[status(thm)],[c_22,c_12]) ).
cnf(c_881,plain,
rd(A,A) = mult(A,ld(A,ld(A,A))),
inference(paramod,[status(thm)],[c_18,c_880]) ).
cnf(c_44,plain,
rd(A,A) = ld(A,A),
inference(paramod,[status(thm)],[c_39,c_881]) ).
cnf(c_882,plain,
rd(mult(A,A),A) = A,
inference(paramod,[status(thm)],[c_22,c_12]) ).
cnf(c_883,plain,
mult(rd(A,A),A) = A,
inference(paramod,[status(thm)],[c_12,c_882]) ).
cnf(c_45,plain,
mult(ld(A,A),A) = A,
inference(paramod,[status(thm)],[c_44,c_883]) ).
cnf(c_884,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_884]) ).
cnf(c_885,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_886,plain,
ld(A,A) = mult(A,ld(A,ld(rd(A,A),rd(A,A)))),
inference(paramod,[status(thm)],[c_44,c_885]) ).
cnf(c_887,plain,
ld(A,A) = mult(A,ld(A,ld(ld(A,A),rd(A,A)))),
inference(paramod,[status(thm)],[c_44,c_886]) ).
cnf(c_888,plain,
ld(A,A) = mult(A,ld(A,ld(ld(A,A),ld(A,A)))),
inference(paramod,[status(thm)],[c_44,c_887]) ).
cnf(c_50,plain,
mult(A,ld(A,ld(ld(A,A),ld(A,A)))) = ld(A,A),
inference(copy,[status(thm)],[c_888]) ).
cnf(c_889,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_890,plain,
mult(ld(A,A),ld(ld(A,A),A)) = ld(rd(A,A),A),
inference(paramod,[status(thm)],[c_44,c_889]) ).
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_890]) ).
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_891,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_891]) ).
cnf(c_892,negated_conjecture,
( mult(ld(sK0,sK0),mult(rd(sK0,sK2),sK2)) != mult(rd(sK0,sK2),sK2)
| mult(rd(sK0,ld(sK1,sK2)),ld(sK1,sK2)) != mult(rd(sK0,sK2),sK2) ),
inference(paramod,[status(thm)],[c_47,c_20]) ).
cnf(c_893,negated_conjecture,
( mult(sK0,mult(sK0,ld(sK0,ld(sK2,sK2)))) != mult(rd(sK0,sK2),sK2)
| mult(rd(sK0,ld(sK1,sK2)),ld(sK1,sK2)) != mult(rd(sK0,sK2),sK2) ),
inference(paramod,[status(thm)],[c_57,c_892]) ).
cnf(c_60,negated_conjecture,
( mult(rd(sK0,sK2),sK2) != mult(sK0,mult(sK0,ld(sK0,ld(sK2,sK2))))
| mult(rd(sK0,ld(sK1,sK2)),ld(sK1,sK2)) != mult(rd(sK0,sK2),sK2) ),
inference(copy,[status(thm)],[c_893]) ).
cnf(c_894,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_61,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_894]) ).
cnf(c_63,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_895,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_72,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_895]) ).
cnf(c_896,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_81,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_896]) ).
cnf(c_897,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_86,plain,
mult(A,ld(A,mult(B,C))) = mult(mult(A,ld(A,B)),C),
inference(paramod,[status(thm)],[c_21,c_897]) ).
cnf(c_109,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_86,c_81]) ).
cnf(c_113,plain,
mult(mult(ld(A,B),ld(ld(A,B),C)),D) = mult(mult(A,ld(A,C)),D),
inference(paramod,[status(thm)],[c_86,c_14]) ).
cnf(c_898,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_899,plain,
ld(ld(A,A),A) = mult(mult(A,ld(A,ld(A,A))),A),
inference(paramod,[status(thm)],[c_51,c_898]) ).
cnf(c_900,plain,
ld(ld(A,A),A) = mult(ld(A,A),A),
inference(paramod,[status(thm)],[c_39,c_899]) ).
cnf(c_134,plain,
ld(ld(A,A),A) = A,
inference(paramod,[status(thm)],[c_45,c_900]) ).
cnf(c_901,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_134,c_23]) ).
cnf(c_902,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_134,c_901]) ).
cnf(c_903,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_134,c_902]) ).
cnf(c_904,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_134,c_903]) ).
cnf(c_136,plain,
mult(A,ld(A,ld(A,mult(B,C)))) = ld(A,mult(mult(A,ld(A,B)),C)),
inference(paramod,[status(thm)],[c_113,c_904]) ).
cnf(c_905,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_134,c_25]) ).
cnf(c_906,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_134,c_905]) ).
cnf(c_907,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_134,c_906]) ).
cnf(c_908,plain,
mult(A,mult(A,ld(A,B))) = mult(mult(ld(A,A),ld(ld(A,A),A)),B),
inference(paramod,[status(thm)],[c_134,c_907]) ).
cnf(c_909,plain,
mult(A,mult(A,ld(A,B))) = mult(mult(ld(A,A),A),B),
inference(paramod,[status(thm)],[c_134,c_908]) ).
cnf(c_138,plain,
mult(A,mult(A,ld(A,B))) = mult(A,B),
inference(paramod,[status(thm)],[c_45,c_909]) ).
cnf(c_910,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_138,c_109]) ).
cnf(c_139,plain,
mult(mult(mult(A,B),ld(mult(A,B),C)),D) = mult(mult(A,ld(A,C)),D),
inference(paramod,[status(thm)],[c_138,c_910]) ).
cnf(c_140,plain,
mult(rd(A,rd(B,C)),rd(B,C)) = mult(A,ld(C,C)),
inference(paramod,[status(thm)],[c_138,c_63]) ).
cnf(c_142,plain,
mult(mult(A,B),ld(C,C)) = mult(A,mult(rd(B,C),C)),
inference(paramod,[status(thm)],[c_138,c_61]) ).
cnf(c_143,negated_conjecture,
( mult(rd(sK0,sK2),sK2) != mult(sK0,ld(sK2,sK2))
| mult(rd(sK0,ld(sK1,sK2)),ld(sK1,sK2)) != mult(rd(sK0,sK2),sK2) ),
inference(paramod,[status(thm)],[c_138,c_60]) ).
cnf(c_911,plain,
mult(ld(A,B),C) = mult(mult(A,ld(A,ld(A,B))),C),
inference(paramod,[status(thm)],[c_138,c_25]) ).
cnf(c_147,plain,
mult(mult(A,ld(A,ld(A,B))),C) = mult(ld(A,B),C),
inference(copy,[status(thm)],[c_911]) ).
cnf(c_912,plain,
mult(A,ld(A,A)) = mult(A,ld(ld(A,A),ld(A,A))),
inference(paramod,[status(thm)],[c_50,c_138]) ).
cnf(c_913,plain,
A = mult(A,ld(ld(A,A),ld(A,A))),
inference(paramod,[status(thm)],[c_21,c_912]) ).
cnf(c_151,plain,
mult(A,ld(ld(A,A),ld(A,A))) = A,
inference(copy,[status(thm)],[c_913]) ).
cnf(c_914,plain,
mult(A,ld(A,B)) = mult(mult(A,ld(A,B)),ld(B,B)),
inference(paramod,[status(thm)],[c_21,c_86]) ).
cnf(c_154,plain,
mult(mult(A,ld(A,B)),ld(B,B)) = mult(A,ld(A,B)),
inference(copy,[status(thm)],[c_914]) ).
cnf(c_915,plain,
mult(A,ld(A,B)) = mult(mult(A,ld(A,ld(B,B))),B),
inference(paramod,[status(thm)],[c_45,c_86]) ).
cnf(c_155,plain,
mult(mult(A,ld(A,ld(B,B))),B) = mult(A,ld(A,B)),
inference(copy,[status(thm)],[c_915]) ).
cnf(c_160,plain,
mult(A,mult(mult(A,ld(A,B)),C)) = mult(A,mult(B,C)),
inference(paramod,[status(thm)],[c_86,c_138]) ).
cnf(c_916,plain,
mult(A,ld(A,B)) = mult(mult(A,ld(A,B)),ld(ld(B,B),ld(B,B))),
inference(paramod,[status(thm)],[c_151,c_86]) ).
cnf(c_162,plain,
mult(mult(A,ld(A,B)),ld(ld(B,B),ld(B,B))) = mult(A,ld(A,B)),
inference(copy,[status(thm)],[c_916]) ).
cnf(c_166,plain,
mult(ld(A,B),ld(ld(A,B),C)) = mult(A,ld(A,C)),
inference(paramod,[status(thm)],[c_154,c_41]) ).
cnf(c_917,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_155,c_72]) ).
cnf(c_167,plain,
ld(ld(A,B),mult(A,ld(A,C))) = mult(A,ld(A,ld(ld(A,B),C))),
inference(paramod,[status(thm)],[c_166,c_917]) ).
cnf(c_182,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_918,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_919,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_154,c_918]) ).
cnf(c_920,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_919]) ).
cnf(c_183,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_920]) ).
cnf(c_921,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_140]) ).
cnf(c_204,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_921]) ).
cnf(c_922,plain,
mult(rd(A,ld(B,B)),rd(B,B)) = mult(A,ld(B,B)),
inference(paramod,[status(thm)],[c_44,c_140]) ).
cnf(c_206,plain,
mult(rd(A,ld(B,B)),ld(B,B)) = mult(A,ld(B,B)),
inference(paramod,[status(thm)],[c_44,c_922]) ).
cnf(c_923,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_140]) ).
cnf(c_924,plain,
rd(A,B) = mult(rd(A,B),ld(B,B)),
inference(paramod,[status(thm)],[c_45,c_923]) ).
cnf(c_207,plain,
mult(rd(A,B),ld(B,B)) = rd(A,B),
inference(copy,[status(thm)],[c_924]) ).
cnf(c_925,plain,
mult(A,ld(A,A)) = rd(A,ld(A,A)),
inference(paramod,[status(thm)],[c_206,c_40]) ).
cnf(c_926,plain,
A = rd(A,ld(A,A)),
inference(paramod,[status(thm)],[c_21,c_925]) ).
cnf(c_215,plain,
rd(A,ld(A,A)) = A,
inference(copy,[status(thm)],[c_926]) ).
cnf(c_927,plain,
mult(rd(A,B),rd(B,ld(B,B))) = mult(A,ld(ld(B,B),ld(B,B))),
inference(paramod,[status(thm)],[c_215,c_140]) ).
cnf(c_217,plain,
mult(rd(A,B),B) = mult(A,ld(ld(B,B),ld(B,B))),
inference(paramod,[status(thm)],[c_215,c_927]) ).
cnf(c_928,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_217,c_204]) ).
cnf(c_929,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_217,c_928]) ).
cnf(c_221,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_217,c_929]) ).
cnf(c_233,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_217,c_183]) ).
cnf(c_234,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_217,c_182]) ).
cnf(c_930,negated_conjecture,
( mult(rd(sK0,sK2),sK2) != mult(sK0,ld(sK2,sK2))
| mult(sK0,ld(ld(ld(sK1,sK2),ld(sK1,sK2)),ld(ld(sK1,sK2),ld(sK1,sK2)))) != mult(rd(sK0,sK2),sK2) ),
inference(paramod,[status(thm)],[c_217,c_143]) ).
cnf(c_931,negated_conjecture,
( mult(rd(sK0,sK2),sK2) != mult(sK0,ld(sK2,sK2))
| mult(sK0,ld(ld(ld(sK1,sK2),ld(sK1,sK2)),ld(ld(sK1,sK2),ld(sK1,sK2)))) != mult(sK0,ld(ld(sK2,sK2),ld(sK2,sK2))) ),
inference(paramod,[status(thm)],[c_217,c_930]) ).
cnf(c_245,negated_conjecture,
( mult(sK0,ld(ld(sK2,sK2),ld(sK2,sK2))) != mult(sK0,ld(sK2,sK2))
| mult(sK0,ld(ld(ld(sK1,sK2),ld(sK1,sK2)),ld(ld(sK1,sK2),ld(sK1,sK2)))) != mult(sK0,ld(ld(sK2,sK2),ld(sK2,sK2))) ),
inference(paramod,[status(thm)],[c_217,c_931]) ).
cnf(c_246,plain,
mult(mult(A,B),ld(C,C)) = mult(A,mult(B,ld(ld(C,C),ld(C,C)))),
inference(paramod,[status(thm)],[c_217,c_142]) ).
cnf(c_254,plain,
mult(ld(A,A),ld(ld(B,B),ld(B,B))) = mult(A,ld(A,ld(B,B))),
inference(paramod,[status(thm)],[c_217,c_56]) ).
cnf(c_262,plain,
rd(mult(A,B),B) = mult(A,ld(ld(B,B),ld(B,B))),
inference(paramod,[status(thm)],[c_217,c_12]) ).
cnf(c_932,plain,
mult(ld(A,A),ld(A,A)) = rd(A,A),
inference(paramod,[status(thm)],[c_44,c_207]) ).
cnf(c_267,plain,
mult(ld(A,A),ld(A,A)) = ld(A,A),
inference(paramod,[status(thm)],[c_44,c_932]) ).
cnf(c_933,plain,
ld(ld(A,A),ld(A,A)) = mult(ld(A,A),ld(ld(A,A),ld(A,A))),
inference(paramod,[status(thm)],[c_267,c_11]) ).
cnf(c_279,plain,
ld(ld(A,A),ld(A,A)) = ld(A,A),
inference(paramod,[status(thm)],[c_21,c_933]) ).
cnf(c_934,plain,
mult(A,ld(A,ld(B,B))) = mult(mult(A,ld(A,ld(B,B))),ld(B,B)),
inference(paramod,[status(thm)],[c_267,c_86]) ).
cnf(c_280,plain,
mult(mult(A,ld(A,ld(B,B))),ld(B,B)) = mult(A,ld(A,ld(B,B))),
inference(copy,[status(thm)],[c_934]) ).
cnf(c_287,plain,
rd(mult(A,B),B) = mult(A,ld(B,B)),
inference(paramod,[status(thm)],[c_279,c_262]) ).
cnf(c_295,plain,
mult(ld(A,A),ld(B,B)) = mult(A,ld(A,ld(B,B))),
inference(paramod,[status(thm)],[c_279,c_254]) ).
cnf(c_301,plain,
mult(mult(A,B),ld(C,C)) = mult(A,mult(B,ld(C,C))),
inference(paramod,[status(thm)],[c_279,c_246]) ).
cnf(c_935,negated_conjecture,
( mult(sK0,ld(ld(sK2,sK2),ld(sK2,sK2))) != mult(sK0,ld(sK2,sK2))
| mult(sK0,ld(ld(sK1,sK2),ld(sK1,sK2))) != mult(sK0,ld(ld(sK2,sK2),ld(sK2,sK2))) ),
inference(paramod,[status(thm)],[c_279,c_245]) ).
cnf(c_936,negated_conjecture,
( mult(sK0,ld(ld(sK2,sK2),ld(sK2,sK2))) != mult(sK0,ld(sK2,sK2))
| mult(sK0,ld(ld(sK1,sK2),ld(sK1,sK2))) != mult(sK0,ld(sK2,sK2)) ),
inference(paramod,[status(thm)],[c_279,c_935]) ).
cnf(c_937,negated_conjecture,
( mult(sK0,ld(sK2,sK2)) != mult(sK0,ld(sK2,sK2))
| mult(sK0,ld(ld(sK1,sK2),ld(sK1,sK2))) != mult(sK0,ld(sK2,sK2)) ),
inference(paramod,[status(thm)],[c_279,c_936]) ).
cnf(c_302,negated_conjecture,
mult(sK0,ld(ld(sK1,sK2),ld(sK1,sK2))) != mult(sK0,ld(sK2,sK2)),
inference(copy,[status(thm)],[c_937]) ).
cnf(c_312,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_279,c_234]) ).
cnf(c_313,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_279,c_233]) ).
cnf(c_938,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_279,c_221]) ).
cnf(c_939,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_279,c_938]) ).
cnf(c_940,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_279,c_939]) ).
cnf(c_941,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_279,c_940]) ).
cnf(c_323,plain,
mult(A,ld(mult(B,ld(C,C)),mult(B,ld(C,C)))) = mult(A,ld(C,C)),
inference(paramod,[status(thm)],[c_279,c_941]) ).
cnf(c_324,plain,
mult(rd(A,B),B) = mult(A,ld(B,B)),
inference(paramod,[status(thm)],[c_279,c_217]) ).
cnf(c_942,plain,
mult(mult(A,ld(A,B)),ld(B,B)) = mult(A,ld(A,B)),
inference(paramod,[status(thm)],[c_279,c_162]) ).
cnf(c_325,plain,
mult(A,mult(ld(A,B),ld(B,B))) = mult(A,ld(A,B)),
inference(paramod,[status(thm)],[c_301,c_942]) ).
cnf(c_330,plain,
mult(A,mult(ld(A,ld(B,B)),ld(B,B))) = mult(A,ld(A,ld(B,B))),
inference(paramod,[status(thm)],[c_301,c_280]) ).
cnf(c_943,plain,
mult(A,ld(A,mult(B,ld(C,C)))) = mult(mult(A,ld(A,rd(B,C))),C),
inference(paramod,[status(thm)],[c_324,c_86]) ).
cnf(c_944,plain,
mult(mult(A,ld(A,B)),ld(C,C)) = mult(mult(A,ld(A,rd(B,C))),C),
inference(paramod,[status(thm)],[c_86,c_943]) ).
cnf(c_945,plain,
mult(A,mult(ld(A,B),ld(C,C))) = mult(mult(A,ld(A,rd(B,C))),C),
inference(paramod,[status(thm)],[c_301,c_944]) ).
cnf(c_339,plain,
mult(mult(A,ld(A,rd(B,C))),C) = mult(A,mult(ld(A,B),ld(C,C))),
inference(copy,[status(thm)],[c_945]) ).
cnf(c_946,plain,
mult(mult(A,ld(B,B)),B) = mult(mult(A,B),ld(B,B)),
inference(paramod,[status(thm)],[c_287,c_324]) ).
cnf(c_947,plain,
mult(mult(A,ld(B,B)),B) = mult(A,mult(B,ld(B,B))),
inference(paramod,[status(thm)],[c_301,c_946]) ).
cnf(c_340,plain,
mult(mult(A,ld(B,B)),B) = mult(A,B),
inference(paramod,[status(thm)],[c_21,c_947]) ).
cnf(c_948,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_147]) ).
cnf(c_949,plain,
mult(A,mult(ld(A,ld(A,B)),ld(ld(A,B),ld(A,B)))) = ld(A,B),
inference(paramod,[status(thm)],[c_301,c_948]) ).
cnf(c_350,plain,
mult(A,ld(A,ld(A,B))) = ld(A,B),
inference(paramod,[status(thm)],[c_325,c_949]) ).
cnf(c_950,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_147,c_138]) ).
cnf(c_951,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_350,c_950]) ).
cnf(c_952,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_350,c_951]) ).
cnf(c_953,plain,
mult(ld(A,B),mult(A,ld(A,C))) = mult(mult(A,ld(A,ld(A,B))),C),
inference(paramod,[status(thm)],[c_166,c_952]) ).
cnf(c_351,plain,
mult(ld(A,B),mult(A,ld(A,C))) = mult(ld(A,B),C),
inference(paramod,[status(thm)],[c_350,c_953]) ).
cnf(c_954,plain,
ld(A,mult(B,C)) = ld(A,mult(mult(A,ld(A,B)),C)),
inference(paramod,[status(thm)],[c_350,c_136]) ).
cnf(c_353,plain,
ld(A,mult(mult(A,ld(A,B)),C)) = ld(A,mult(B,C)),
inference(copy,[status(thm)],[c_954]) ).
cnf(c_955,plain,
rd(mult(A,ld(A,B)),B) = mult(mult(A,ld(A,ld(B,B))),ld(B,B)),
inference(paramod,[status(thm)],[c_155,c_287]) ).
cnf(c_956,plain,
rd(mult(A,ld(A,B)),B) = mult(A,mult(ld(A,ld(B,B)),ld(B,B))),
inference(paramod,[status(thm)],[c_301,c_955]) ).
cnf(c_404,plain,
rd(mult(A,ld(A,B)),B) = mult(A,ld(A,ld(B,B))),
inference(paramod,[status(thm)],[c_330,c_956]) ).
cnf(c_957,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_166,c_11]) ).
cnf(c_958,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_167,c_957]) ).
cnf(c_438,plain,
mult(A,ld(A,ld(ld(A,B),C))) = ld(ld(A,B),C),
inference(paramod,[status(thm)],[c_350,c_958]) ).
cnf(c_446,plain,
ld(ld(A,B),mult(A,ld(A,C))) = ld(ld(A,B),C),
inference(paramod,[status(thm)],[c_438,c_167]) ).
cnf(c_959,plain,
mult(mult(A,ld(A,ld(B,B))),B) = mult(ld(A,A),B),
inference(paramod,[status(thm)],[c_295,c_340]) ).
cnf(c_960,plain,
mult(A,ld(A,B)) = mult(ld(A,A),B),
inference(paramod,[status(thm)],[c_155,c_959]) ).
cnf(c_536,plain,
mult(ld(A,A),B) = mult(A,ld(A,B)),
inference(copy,[status(thm)],[c_960]) ).
cnf(c_542,plain,
mult(ld(A,A),ld(ld(A,B),C)) = ld(ld(A,B),C),
inference(paramod,[status(thm)],[c_536,c_438]) ).
cnf(c_543,plain,
mult(ld(A,A),ld(A,B)) = ld(A,B),
inference(paramod,[status(thm)],[c_536,c_350]) ).
cnf(c_961,plain,
mult(ld(A,A),mult(A,B)) = mult(A,mult(A,ld(A,B))),
inference(paramod,[status(thm)],[c_11,c_536]) ).
cnf(c_545,plain,
mult(ld(A,A),mult(A,B)) = mult(A,B),
inference(paramod,[status(thm)],[c_138,c_961]) ).
cnf(c_962,plain,
mult(ld(A,A),mult(A,ld(A,ld(ld(A,A),B)))) = mult(ld(A,A),B),
inference(paramod,[status(thm)],[c_536,c_138]) ).
cnf(c_963,plain,
mult(ld(A,A),mult(ld(A,A),ld(ld(A,A),B))) = mult(ld(A,A),B),
inference(paramod,[status(thm)],[c_536,c_962]) ).
cnf(c_964,plain,
mult(ld(A,A),ld(ld(A,A),B)) = mult(ld(A,A),B),
inference(paramod,[status(thm)],[c_542,c_963]) ).
cnf(c_546,plain,
ld(ld(A,A),B) = mult(ld(A,A),B),
inference(paramod,[status(thm)],[c_542,c_964]) ).
cnf(c_548,plain,
mult(A,mult(ld(A,A),B)) = mult(A,B),
inference(paramod,[status(thm)],[c_536,c_138]) ).
cnf(c_562,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_536,c_160]) ).
cnf(c_965,plain,
mult(mult(A,ld(A,ld(B,B))),B) = mult(mult(A,C),ld(mult(A,C),B)),
inference(paramod,[status(thm)],[c_139,c_155]) ).
cnf(c_966,plain,
mult(A,ld(A,B)) = mult(mult(A,C),ld(mult(A,C),B)),
inference(paramod,[status(thm)],[c_155,c_965]) ).
cnf(c_581,plain,
mult(mult(A,B),ld(mult(A,B),C)) = mult(A,ld(A,C)),
inference(copy,[status(thm)],[c_966]) ).
cnf(c_967,plain,
rd(mult(A,B),mult(A,B)) = mult(ld(A,A),ld(mult(A,B),mult(A,B))),
inference(paramod,[status(thm)],[c_545,c_287]) ).
cnf(c_968,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_967]) ).
cnf(c_600,plain,
mult(ld(A,A),ld(mult(A,B),mult(A,B))) = ld(mult(A,B),mult(A,B)),
inference(copy,[status(thm)],[c_968]) ).
cnf(c_969,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_546,c_86]) ).
cnf(c_970,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_546,c_969]) ).
cnf(c_605,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_970]) ).
cnf(c_971,plain,
mult(mult(ld(A,A),ld(A,A)),B) = mult(ld(A,A),ld(ld(A,A),B)),
inference(paramod,[status(thm)],[c_546,c_536]) ).
cnf(c_972,plain,
mult(ld(A,A),B) = mult(ld(A,A),ld(ld(A,A),B)),
inference(paramod,[status(thm)],[c_543,c_971]) ).
cnf(c_973,plain,
mult(ld(A,A),B) = mult(ld(A,A),mult(ld(A,A),B)),
inference(paramod,[status(thm)],[c_546,c_972]) ).
cnf(c_608,plain,
mult(ld(A,A),mult(ld(A,A),B)) = mult(ld(A,A),B),
inference(copy,[status(thm)],[c_973]) ).
cnf(c_974,plain,
mult(mult(ld(A,A),B),C) = mult(ld(A,A),mult(ld(A,A),mult(B,C))),
inference(paramod,[status(thm)],[c_608,c_605]) ).
cnf(c_616,plain,
mult(mult(ld(A,A),B),C) = mult(ld(A,A),mult(B,C)),
inference(paramod,[status(thm)],[c_608,c_974]) ).
cnf(c_975,plain,
mult(ld(A,B),ld(C,C)) = mult(ld(A,A),mult(ld(A,B),ld(C,C))),
inference(paramod,[status(thm)],[c_543,c_301]) ).
cnf(c_650,plain,
mult(ld(A,A),mult(ld(A,B),ld(C,C))) = mult(ld(A,B),ld(C,C)),
inference(copy,[status(thm)],[c_975]) ).
cnf(c_976,plain,
ld(A,mult(A,ld(A,B))) = mult(A,ld(A,mult(ld(A,B),ld(B,B)))),
inference(paramod,[status(thm)],[c_325,c_11]) ).
cnf(c_977,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_976]) ).
cnf(c_978,plain,
mult(ld(A,A),ld(A,B)) = mult(A,ld(A,mult(ld(A,B),ld(B,B)))),
inference(paramod,[status(thm)],[c_536,c_977]) ).
cnf(c_979,plain,
ld(A,B) = mult(A,ld(A,mult(ld(A,B),ld(B,B)))),
inference(paramod,[status(thm)],[c_543,c_978]) ).
cnf(c_980,plain,
ld(A,B) = mult(ld(A,A),mult(ld(A,B),ld(B,B))),
inference(paramod,[status(thm)],[c_536,c_979]) ).
cnf(c_981,plain,
ld(A,B) = mult(ld(A,B),ld(B,B)),
inference(paramod,[status(thm)],[c_650,c_980]) ).
cnf(c_665,plain,
mult(ld(A,B),ld(B,B)) = ld(A,B),
inference(copy,[status(thm)],[c_981]) ).
cnf(c_982,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_325,c_160]) ).
cnf(c_983,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_581,c_982]) ).
cnf(c_984,plain,
mult(A,C) = mult(A,mult(B,mult(ld(mult(A,ld(A,B)),C),ld(C,C)))),
inference(paramod,[status(thm)],[c_138,c_983]) ).
cnf(c_985,plain,
mult(A,C) = mult(A,mult(B,ld(mult(A,ld(A,B)),C))),
inference(paramod,[status(thm)],[c_665,c_984]) ).
cnf(c_667,plain,
mult(A,mult(B,ld(mult(A,ld(A,B)),C))) = mult(A,C),
inference(copy,[status(thm)],[c_985]) ).
cnf(c_669,plain,
mult(A,mult(ld(mult(A,ld(A,B)),mult(A,ld(A,B))),C)) = mult(A,C),
inference(paramod,[status(thm)],[c_667,c_562]) ).
cnf(c_986,plain,
ld(ld(A,B),ld(A,B)) = mult(ld(A,B),ld(ld(A,B),ld(B,B))),
inference(paramod,[status(thm)],[c_665,c_11]) ).
cnf(c_670,plain,
ld(ld(A,B),ld(A,B)) = mult(A,ld(A,ld(B,B))),
inference(paramod,[status(thm)],[c_166,c_986]) ).
cnf(c_987,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_670,c_313]) ).
cnf(c_988,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_166,c_987]) ).
cnf(c_696,plain,
rd(mult(A,ld(A,B)),ld(ld(A,C),B)) = mult(ld(A,C),ld(B,B)),
inference(paramod,[status(thm)],[c_351,c_988]) ).
cnf(c_989,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_670,c_312]) ).
cnf(c_990,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_166,c_989]) ).
cnf(c_991,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_536,c_990]) ).
cnf(c_992,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_323,c_991]) ).
cnf(c_697,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_600,c_992]) ).
cnf(c_993,negated_conjecture,
mult(sK0,mult(sK1,ld(sK1,ld(sK2,sK2)))) != mult(sK0,ld(sK2,sK2)),
inference(paramod,[status(thm)],[c_670,c_302]) ).
cnf(c_701,negated_conjecture,
mult(sK0,mult(ld(sK1,sK1),ld(sK2,sK2))) != mult(sK0,ld(sK2,sK2)),
inference(paramod,[status(thm)],[c_536,c_993]) ).
cnf(c_994,plain,
ld(A,mult(mult(A,ld(A,rd(B,C))),C)) = ld(A,mult(B,ld(C,C))),
inference(paramod,[status(thm)],[c_324,c_353]) ).
cnf(c_995,plain,
ld(A,mult(A,mult(ld(A,B),ld(C,C)))) = ld(A,mult(B,ld(C,C))),
inference(paramod,[status(thm)],[c_339,c_994]) ).
cnf(c_996,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_995]) ).
cnf(c_997,plain,
mult(ld(A,A),mult(ld(A,B),ld(C,C))) = ld(A,mult(B,ld(C,C))),
inference(paramod,[status(thm)],[c_536,c_996]) ).
cnf(c_998,plain,
mult(ld(A,B),ld(C,C)) = ld(A,mult(B,ld(C,C))),
inference(paramod,[status(thm)],[c_650,c_997]) ).
cnf(c_751,plain,
ld(A,mult(B,ld(C,C))) = mult(ld(A,B),ld(C,C)),
inference(copy,[status(thm)],[c_998]) ).
cnf(c_766,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_751,c_697]) ).
cnf(c_999,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_446]) ).
cnf(c_825,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_999]) ).
cnf(c_1000,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_446,c_665]) ).
cnf(c_1001,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_825,c_1000]) ).
cnf(c_834,plain,
mult(ld(ld(A,B),C),ld(mult(A,ld(A,C)),C)) = ld(ld(A,B),C),
inference(paramod,[status(thm)],[c_446,c_1001]) ).
cnf(c_1002,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_446,c_404]) ).
cnf(c_1003,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_166,c_1002]) ).
cnf(c_1004,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_1003]) ).
cnf(c_1005,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_825,c_1004]) ).
cnf(c_1006,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_825,c_1005]) ).
cnf(c_1007,plain,
ld(mult(A,ld(A,C)),C) = mult(A,ld(A,ld(mult(A,ld(A,C)),C))),
inference(paramod,[status(thm)],[c_166,c_1006]) ).
cnf(c_1008,plain,
ld(mult(A,ld(A,C)),C) = mult(ld(A,A),ld(mult(A,ld(A,C)),C)),
inference(paramod,[status(thm)],[c_536,c_1007]) ).
cnf(c_836,plain,
mult(ld(A,A),ld(mult(A,ld(A,B)),B)) = ld(mult(A,ld(A,B)),B),
inference(copy,[status(thm)],[c_1008]) ).
cnf(c_1009,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_825,c_766]) ).
cnf(c_1010,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_834,c_1009]) ).
cnf(c_1011,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_696,c_1010]) ).
cnf(c_1012,plain,
mult(ld(A,C),ld(B,B)) = mult(ld(A,C),ld(mult(A,ld(A,B)),B)),
inference(paramod,[status(thm)],[c_825,c_1011]) ).
cnf(c_840,plain,
mult(ld(A,B),ld(mult(A,ld(A,C)),C)) = mult(ld(A,B),ld(C,C)),
inference(copy,[status(thm)],[c_1012]) ).
cnf(c_845,plain,
mult(A,mult(ld(mult(A,ld(A,B)),B),C)) = mult(A,C),
inference(paramod,[status(thm)],[c_825,c_669]) ).
cnf(c_1013,plain,
mult(ld(A,A),ld(B,B)) = ld(mult(A,ld(A,B)),B),
inference(paramod,[status(thm)],[c_840,c_836]) ).
cnf(c_861,plain,
ld(mult(A,ld(A,B)),B) = mult(ld(A,A),ld(B,B)),
inference(copy,[status(thm)],[c_1013]) ).
cnf(c_1014,plain,
mult(A,mult(mult(ld(A,A),ld(B,B)),C)) = mult(A,C),
inference(paramod,[status(thm)],[c_861,c_845]) ).
cnf(c_1015,plain,
mult(A,mult(ld(A,A),mult(ld(B,B),C))) = mult(A,C),
inference(paramod,[status(thm)],[c_616,c_1014]) ).
cnf(c_867,plain,
mult(A,mult(ld(B,B),C)) = mult(A,C),
inference(paramod,[status(thm)],[c_548,c_1015]) ).
cnf(c_868,plain,
$false,
inference(resolve,[status(thm)],[c_867,c_701]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP685+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n008.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Fri Sep 25 15:38:09 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.38 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.38 % Process 1388939 was started by sandbox on n008,
% 0.10/0.38 % Fri Sep 25 15:38:09 2026
% 0.10/0.38 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.14/0.38
% 0.14/0.38 % From the command line: assign(max_seconds, 300).
% 0.88/0.51
% 0.88/0.51 % SZS status Theorem for theBenchmark
% 0.88/0.51
% 0.88/0.51 % Proof 1 at 0.09 (+ 0.02) seconds.
% 0.88/0.51 % Length of proof is 126.
% 0.88/0.51 % Level of proof is 25.
% 0.88/0.51 % Maximum clause weight is 99.000.
% 0.88/0.51 % Given clauses 70.
% 0.88/0.51
% 0.88/0.51 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------