%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP683-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 : n005.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 : Unsatisfiable 0.14s 5.68s
% Output : CNFRefutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 75
% Number of leaves : 8
% Syntax : Number of formulae : 291 ( 291 unt; 0 def)
% Number of atoms : 291 ( 290 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 4 ( 4 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 1 avg)
% Maximal term depth : 8 ( 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 : 751 ( 0 sgn 16 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f01,axiom,
! [VAR_0] : ld(VAR_0,mult(VAR_0,VAR_0)) = VAR_0,
file('theBenchmark.p',f01) ).
cnf(c_1,plain,
ld(A,mult(A,A)) = A,
inference(clausify,[status(thm)],[f01]) ).
fof(f02,axiom,
! [VAR_0] : rd(mult(VAR_0,VAR_0),VAR_0) = VAR_0,
file('theBenchmark.p',f02) ).
cnf(c_2,plain,
rd(mult(A,A),A) = A,
inference(clausify,[status(thm)],[f02]) ).
fof(f03,axiom,
! [VAR_0,VAR_1] : mult(VAR_0,ld(VAR_0,VAR_1)) = ld(VAR_0,mult(VAR_0,VAR_1)),
file('theBenchmark.p',f03) ).
cnf(c_3,plain,
mult(A,ld(A,B)) = ld(A,mult(A,B)),
inference(clausify,[status(thm)],[f03]) ).
cnf(c_4,plain,
ld(A,mult(A,B)) = mult(A,ld(A,B)),
inference(copy,[status(thm)],[c_3]) ).
fof(f04,axiom,
! [VAR_0,VAR_1] : mult(rd(VAR_0,VAR_1),VAR_1) = rd(mult(VAR_0,VAR_1),VAR_1),
file('theBenchmark.p',f04) ).
cnf(c_5,plain,
mult(rd(A,B),B) = rd(mult(A,B),B),
inference(clausify,[status(thm)],[f04]) ).
cnf(c_6,plain,
rd(mult(A,B),B) = mult(rd(A,B),B),
inference(copy,[status(thm)],[c_5]) ).
fof(f05,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] : ld(ld(VAR_0,VAR_1),mult(ld(VAR_0,VAR_1),mult(VAR_2,VAR_3))) = mult(ld(VAR_0,mult(VAR_0,VAR_2)),VAR_3),
file('theBenchmark.p',f05) ).
cnf(c_7,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_838,plain,
mult(ld(A,B),ld(ld(A,B),mult(C,D))) = mult(ld(A,mult(A,C)),D),
inference(paramod,[status(thm)],[c_4,c_7]) ).
cnf(c_8,plain,
mult(ld(A,B),ld(ld(A,B),mult(C,D))) = mult(mult(A,ld(A,C)),D),
inference(paramod,[status(thm)],[c_4,c_838]) ).
fof(f06,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] : rd(mult(mult(VAR_0,VAR_1),rd(VAR_2,VAR_3)),rd(VAR_2,VAR_3)) = mult(VAR_0,rd(mult(VAR_1,VAR_3),VAR_3)),
file('theBenchmark.p',f06) ).
cnf(c_9,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_839,plain,
mult(rd(mult(A,B),rd(C,D)),rd(C,D)) = mult(A,rd(mult(B,D),D)),
inference(paramod,[status(thm)],[c_6,c_9]) ).
cnf(c_10,plain,
mult(rd(mult(A,B),rd(C,D)),rd(C,D)) = mult(A,mult(rd(B,D),D)),
inference(paramod,[status(thm)],[c_6,c_839]) ).
fof(f07,axiom,
! [VAR_0,VAR_1] : ld(VAR_0,mult(VAR_0,ld(VAR_1,VAR_1))) = rd(mult(rd(VAR_0,VAR_0),VAR_1),VAR_1),
file('theBenchmark.p',f07) ).
cnf(c_11,plain,
ld(A,mult(A,ld(B,B))) = rd(mult(rd(A,A),B),B),
inference(clausify,[status(thm)],[f07]) ).
cnf(c_840,plain,
mult(A,ld(A,ld(B,B))) = rd(mult(rd(A,A),B),B),
inference(paramod,[status(thm)],[c_4,c_11]) ).
cnf(c_841,plain,
mult(A,ld(A,ld(B,B))) = mult(rd(rd(A,A),B),B),
inference(paramod,[status(thm)],[c_6,c_840]) ).
cnf(c_12,plain,
mult(rd(rd(A,A),B),B) = mult(A,ld(A,ld(B,B))),
inference(copy,[status(thm)],[c_841]) ).
fof(goal,axiom,
mult(rd(mult(x3,x4),x4),x5) != mult(x3,x5),
file('theBenchmark.p',goal) ).
cnf(c_13,plain,
mult(rd(mult(x3,x4),x4),x5) != mult(x3,x5),
inference(clausify,[status(thm)],[goal]) ).
cnf(c_14,plain,
mult(mult(rd(x3,x4),x4),x5) != mult(x3,x5),
inference(paramod,[status(thm)],[c_6,c_13]) ).
cnf(c_15,plain,
mult(A,ld(A,A)) = A,
inference(paramod,[status(thm)],[c_4,c_1]) ).
cnf(c_16,plain,
mult(rd(A,A),A) = A,
inference(paramod,[status(thm)],[c_6,c_2]) ).
cnf(c_842,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_8,c_4]) ).
cnf(c_17,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_842]) ).
cnf(c_843,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_4,c_8]) ).
cnf(c_18,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_4,c_843]) ).
cnf(c_844,plain,
ld(A,A) = mult(A,ld(A,ld(A,A))),
inference(paramod,[status(thm)],[c_15,c_4]) ).
cnf(c_33,plain,
mult(A,ld(A,ld(A,A))) = ld(A,A),
inference(copy,[status(thm)],[c_844]) ).
cnf(c_845,plain,
rd(A,ld(A,A)) = mult(rd(A,ld(A,A)),ld(A,A)),
inference(paramod,[status(thm)],[c_15,c_6]) ).
cnf(c_34,plain,
mult(rd(A,ld(A,A)),ld(A,A)) = rd(A,ld(A,A)),
inference(copy,[status(thm)],[c_845]) ).
cnf(c_36,plain,
mult(rd(A,rd(B,C)),rd(B,C)) = mult(A,mult(rd(ld(A,A),C),C)),
inference(paramod,[status(thm)],[c_15,c_10]) ).
cnf(c_846,plain,
rd(A,A) = mult(rd(rd(A,A),A),A),
inference(paramod,[status(thm)],[c_16,c_6]) ).
cnf(c_847,plain,
rd(A,A) = mult(A,ld(A,ld(A,A))),
inference(paramod,[status(thm)],[c_12,c_846]) ).
cnf(c_38,plain,
rd(A,A) = ld(A,A),
inference(paramod,[status(thm)],[c_33,c_847]) ).
cnf(c_848,plain,
rd(mult(A,A),A) = A,
inference(paramod,[status(thm)],[c_16,c_6]) ).
cnf(c_849,plain,
mult(rd(A,A),A) = A,
inference(paramod,[status(thm)],[c_6,c_848]) ).
cnf(c_39,plain,
mult(ld(A,A),A) = A,
inference(paramod,[status(thm)],[c_38,c_849]) ).
cnf(c_850,plain,
mult(ld(A,B),ld(ld(A,B),C)) = mult(mult(A,ld(A,rd(C,C))),C),
inference(paramod,[status(thm)],[c_16,c_8]) ).
cnf(c_40,plain,
mult(ld(A,B),ld(ld(A,B),C)) = mult(mult(A,ld(A,ld(C,C))),C),
inference(paramod,[status(thm)],[c_38,c_850]) ).
cnf(c_48,plain,
mult(rd(ld(A,A),B),B) = mult(A,ld(A,ld(B,B))),
inference(paramod,[status(thm)],[c_38,c_12]) ).
cnf(c_49,plain,
mult(rd(A,rd(B,C)),rd(B,C)) = mult(A,mult(A,ld(A,ld(C,C)))),
inference(paramod,[status(thm)],[c_48,c_36]) ).
cnf(c_851,plain,
mult(mult(A,ld(A,B)),ld(ld(A,mult(A,B)),ld(ld(A,mult(A,B)),mult(C,D)))) = ld(ld(A,mult(A,B)),mult(mult(A,ld(A,C)),D)),
inference(paramod,[status(thm)],[c_4,c_17]) ).
cnf(c_852,plain,
mult(mult(A,ld(A,B)),ld(mult(A,ld(A,B)),ld(ld(A,mult(A,B)),mult(C,D)))) = ld(ld(A,mult(A,B)),mult(mult(A,ld(A,C)),D)),
inference(paramod,[status(thm)],[c_4,c_851]) ).
cnf(c_853,plain,
mult(mult(A,ld(A,B)),ld(mult(A,ld(A,B)),ld(mult(A,ld(A,B)),mult(C,D)))) = ld(ld(A,mult(A,B)),mult(mult(A,ld(A,C)),D)),
inference(paramod,[status(thm)],[c_4,c_852]) ).
cnf(c_50,plain,
mult(mult(A,ld(A,B)),ld(mult(A,ld(A,B)),ld(mult(A,ld(A,B)),mult(C,D)))) = ld(mult(A,ld(A,B)),mult(mult(A,ld(A,C)),D)),
inference(paramod,[status(thm)],[c_4,c_853]) ).
cnf(c_854,plain,
mult(rd(mult(A,B),ld(C,C)),rd(C,C)) = mult(A,mult(rd(B,C),C)),
inference(paramod,[status(thm)],[c_38,c_10]) ).
cnf(c_53,plain,
mult(rd(mult(A,B),ld(C,C)),ld(C,C)) = mult(A,mult(rd(B,C),C)),
inference(paramod,[status(thm)],[c_38,c_854]) ).
cnf(c_855,plain,
mult(rd(A,ld(B,B)),ld(B,B)) = mult(A,mult(rd(ld(A,A),B),B)),
inference(paramod,[status(thm)],[c_15,c_53]) ).
cnf(c_70,plain,
mult(rd(A,ld(B,B)),ld(B,B)) = mult(A,mult(A,ld(A,ld(B,B)))),
inference(paramod,[status(thm)],[c_48,c_855]) ).
cnf(c_856,plain,
mult(A,ld(mult(A,ld(A,A)),mult(B,C))) = mult(mult(A,ld(A,B)),C),
inference(paramod,[status(thm)],[c_15,c_18]) ).
cnf(c_857,plain,
mult(A,ld(A,mult(B,C))) = mult(mult(A,ld(A,B)),C),
inference(paramod,[status(thm)],[c_15,c_856]) ).
cnf(c_81,plain,
mult(mult(A,ld(A,B)),C) = mult(A,ld(A,mult(B,C))),
inference(copy,[status(thm)],[c_857]) ).
cnf(c_858,plain,
mult(mult(A,ld(A,B)),ld(mult(A,ld(A,B)),C)) = mult(mult(A,ld(A,C)),ld(C,C)),
inference(paramod,[status(thm)],[c_15,c_18]) ).
cnf(c_859,plain,
mult(A,ld(A,mult(B,ld(mult(A,ld(A,B)),C)))) = mult(mult(A,ld(A,C)),ld(C,C)),
inference(paramod,[status(thm)],[c_81,c_858]) ).
cnf(c_860,plain,
mult(A,ld(A,mult(B,ld(mult(A,ld(A,B)),C)))) = mult(A,ld(A,mult(C,ld(C,C)))),
inference(paramod,[status(thm)],[c_81,c_859]) ).
cnf(c_82,plain,
mult(A,ld(A,mult(B,ld(mult(A,ld(A,B)),C)))) = mult(A,ld(A,C)),
inference(paramod,[status(thm)],[c_15,c_860]) ).
cnf(c_861,plain,
mult(mult(A,ld(A,B)),ld(mult(A,ld(A,B)),mult(A,C))) = mult(A,C),
inference(paramod,[status(thm)],[c_15,c_18]) ).
cnf(c_862,plain,
mult(A,ld(A,mult(B,ld(mult(A,ld(A,B)),mult(A,C))))) = mult(A,C),
inference(paramod,[status(thm)],[c_81,c_861]) ).
cnf(c_863,plain,
mult(A,ld(A,mult(A,C))) = mult(A,C),
inference(paramod,[status(thm)],[c_82,c_862]) ).
cnf(c_83,plain,
mult(A,mult(A,ld(A,B))) = mult(A,B),
inference(paramod,[status(thm)],[c_4,c_863]) ).
cnf(c_864,plain,
mult(A,ld(A,mult(B,ld(mult(A,ld(A,B)),ld(mult(A,ld(A,B)),mult(C,D)))))) = ld(mult(A,ld(A,B)),mult(mult(A,ld(A,C)),D)),
inference(paramod,[status(thm)],[c_81,c_50]) ).
cnf(c_865,plain,
mult(A,ld(A,ld(mult(A,ld(A,B)),mult(C,D)))) = ld(mult(A,ld(A,B)),mult(mult(A,ld(A,C)),D)),
inference(paramod,[status(thm)],[c_82,c_864]) ).
cnf(c_866,plain,
mult(A,ld(A,ld(mult(A,ld(A,B)),mult(C,D)))) = ld(mult(A,ld(A,B)),mult(A,ld(A,mult(C,D)))),
inference(paramod,[status(thm)],[c_81,c_865]) ).
cnf(c_98,plain,
ld(mult(A,ld(A,B)),mult(A,ld(A,mult(C,D)))) = mult(A,ld(A,ld(mult(A,ld(A,B)),mult(C,D)))),
inference(copy,[status(thm)],[c_866]) ).
cnf(c_867,plain,
mult(ld(A,B),ld(ld(A,B),C)) = mult(A,ld(A,mult(ld(C,C),C))),
inference(paramod,[status(thm)],[c_81,c_40]) ).
cnf(c_99,plain,
mult(ld(A,B),ld(ld(A,B),C)) = mult(A,ld(A,C)),
inference(paramod,[status(thm)],[c_39,c_867]) ).
cnf(c_104,plain,
mult(rd(A,ld(B,B)),ld(B,B)) = mult(A,ld(B,B)),
inference(paramod,[status(thm)],[c_83,c_70]) ).
cnf(c_105,plain,
mult(rd(A,rd(B,C)),rd(B,C)) = mult(A,ld(C,C)),
inference(paramod,[status(thm)],[c_83,c_49]) ).
cnf(c_114,plain,
mult(mult(A,B),ld(C,C)) = mult(A,mult(rd(B,C),C)),
inference(paramod,[status(thm)],[c_104,c_53]) ).
cnf(c_868,plain,
mult(A,ld(A,A)) = rd(A,ld(A,A)),
inference(paramod,[status(thm)],[c_104,c_34]) ).
cnf(c_869,plain,
A = rd(A,ld(A,A)),
inference(paramod,[status(thm)],[c_15,c_868]) ).
cnf(c_115,plain,
rd(A,ld(A,A)) = A,
inference(copy,[status(thm)],[c_869]) ).
cnf(c_870,plain,
ld(rd(A,ld(B,B)),mult(A,ld(B,B))) = mult(rd(A,ld(B,B)),ld(rd(A,ld(B,B)),ld(B,B))),
inference(paramod,[status(thm)],[c_104,c_4]) ).
cnf(c_121,plain,
mult(rd(A,ld(B,B)),ld(rd(A,ld(B,B)),ld(B,B))) = ld(rd(A,ld(B,B)),mult(A,ld(B,B))),
inference(copy,[status(thm)],[c_870]) ).
cnf(c_871,plain,
mult(ld(ld(A,A),ld(A,A)),ld(A,A)) = mult(ld(A,A),ld(A,A)),
inference(paramod,[status(thm)],[c_38,c_104]) ).
cnf(c_872,plain,
ld(A,A) = mult(ld(A,A),ld(A,A)),
inference(paramod,[status(thm)],[c_39,c_871]) ).
cnf(c_122,plain,
mult(ld(A,A),ld(A,A)) = ld(A,A),
inference(copy,[status(thm)],[c_872]) ).
cnf(c_873,plain,
mult(ld(A,A),ld(B,B)) = mult(A,ld(A,ld(ld(B,B),ld(B,B)))),
inference(paramod,[status(thm)],[c_104,c_48]) ).
cnf(c_123,plain,
mult(A,ld(A,ld(ld(B,B),ld(B,B)))) = mult(ld(A,A),ld(B,B)),
inference(copy,[status(thm)],[c_873]) ).
cnf(c_874,plain,
ld(ld(A,A),ld(A,A)) = mult(ld(A,A),ld(ld(A,A),ld(A,A))),
inference(paramod,[status(thm)],[c_122,c_4]) ).
cnf(c_126,plain,
ld(ld(A,A),ld(A,A)) = ld(A,A),
inference(paramod,[status(thm)],[c_15,c_874]) ).
cnf(c_875,plain,
mult(A,ld(A,ld(B,B))) = mult(ld(A,A),ld(B,B)),
inference(paramod,[status(thm)],[c_126,c_123]) ).
cnf(c_127,plain,
mult(ld(A,A),ld(B,B)) = mult(A,ld(A,ld(B,B))),
inference(copy,[status(thm)],[c_875]) ).
cnf(c_876,plain,
rd(mult(A,B),mult(A,ld(A,B))) = mult(rd(A,mult(A,ld(A,B))),mult(A,ld(A,B))),
inference(paramod,[status(thm)],[c_83,c_6]) ).
cnf(c_130,plain,
mult(rd(A,mult(A,ld(A,B))),mult(A,ld(A,B))) = rd(mult(A,B),mult(A,ld(A,B))),
inference(copy,[status(thm)],[c_876]) ).
cnf(c_877,plain,
ld(mult(A,ld(A,B)),mult(A,ld(A,mult(B,C)))) = mult(mult(A,ld(A,B)),ld(mult(A,ld(A,B)),C)),
inference(paramod,[status(thm)],[c_81,c_4]) ).
cnf(c_878,plain,
mult(A,ld(A,ld(mult(A,ld(A,B)),mult(B,C)))) = mult(mult(A,ld(A,B)),ld(mult(A,ld(A,B)),C)),
inference(paramod,[status(thm)],[c_98,c_877]) ).
cnf(c_879,plain,
mult(A,ld(A,ld(mult(A,ld(A,B)),mult(B,C)))) = mult(A,ld(A,mult(B,ld(mult(A,ld(A,B)),C)))),
inference(paramod,[status(thm)],[c_81,c_878]) ).
cnf(c_139,plain,
mult(A,ld(A,ld(mult(A,ld(A,B)),mult(B,C)))) = mult(A,ld(A,C)),
inference(paramod,[status(thm)],[c_82,c_879]) ).
cnf(c_880,plain,
mult(mult(A,mult(A,ld(A,B))),C) = mult(A,ld(A,mult(mult(A,B),C))),
inference(paramod,[status(thm)],[c_4,c_81]) ).
cnf(c_881,plain,
mult(mult(A,B),C) = mult(A,ld(A,mult(mult(A,B),C))),
inference(paramod,[status(thm)],[c_83,c_880]) ).
cnf(c_140,plain,
mult(A,ld(A,mult(mult(A,B),C))) = mult(mult(A,B),C),
inference(copy,[status(thm)],[c_881]) ).
cnf(c_882,plain,
mult(mult(A,ld(A,B)),ld(B,B)) = mult(A,ld(A,B)),
inference(paramod,[status(thm)],[c_15,c_81]) ).
cnf(c_142,plain,
mult(A,mult(rd(ld(A,B),B),B)) = mult(A,ld(A,B)),
inference(paramod,[status(thm)],[c_114,c_882]) ).
cnf(c_883,plain,
mult(rd(mult(A,ld(A,B)),ld(C,C)),ld(C,C)) = mult(A,ld(A,mult(B,ld(C,C)))),
inference(paramod,[status(thm)],[c_81,c_104]) ).
cnf(c_884,plain,
mult(mult(A,ld(A,B)),ld(C,C)) = mult(A,ld(A,mult(B,ld(C,C)))),
inference(paramod,[status(thm)],[c_104,c_883]) ).
cnf(c_885,plain,
mult(A,mult(rd(ld(A,B),C),C)) = mult(A,ld(A,mult(B,ld(C,C)))),
inference(paramod,[status(thm)],[c_114,c_884]) ).
cnf(c_143,plain,
mult(A,ld(A,mult(B,ld(C,C)))) = mult(A,mult(rd(ld(A,B),C),C)),
inference(copy,[status(thm)],[c_885]) ).
cnf(c_151,plain,
mult(A,ld(A,ld(A,B))) = ld(A,B),
inference(paramod,[status(thm)],[c_99,c_15]) ).
cnf(c_886,plain,
ld(mult(A,ld(A,B)),C) = mult(A,ld(A,mult(B,ld(mult(A,ld(A,B)),ld(mult(A,ld(A,B)),C))))),
inference(paramod,[status(thm)],[c_151,c_81]) ).
cnf(c_887,plain,
ld(mult(A,ld(A,B)),C) = mult(A,ld(A,ld(mult(A,ld(A,B)),C))),
inference(paramod,[status(thm)],[c_82,c_886]) ).
cnf(c_157,plain,
mult(A,ld(A,ld(mult(A,ld(A,B)),C))) = ld(mult(A,ld(A,B)),C),
inference(copy,[status(thm)],[c_887]) ).
cnf(c_159,plain,
ld(mult(A,ld(A,B)),mult(B,C)) = mult(A,ld(A,C)),
inference(paramod,[status(thm)],[c_157,c_139]) ).
cnf(c_888,plain,
ld(mult(A,mult(A,ld(A,B))),mult(mult(A,B),C)) = mult(A,ld(A,C)),
inference(paramod,[status(thm)],[c_4,c_159]) ).
cnf(c_889,plain,
ld(mult(A,B),mult(mult(A,B),C)) = mult(A,ld(A,C)),
inference(paramod,[status(thm)],[c_83,c_888]) ).
cnf(c_162,plain,
mult(mult(A,B),ld(mult(A,B),C)) = mult(A,ld(A,C)),
inference(paramod,[status(thm)],[c_4,c_889]) ).
cnf(c_163,plain,
ld(mult(A,ld(A,B)),B) = mult(A,ld(A,ld(B,B))),
inference(paramod,[status(thm)],[c_15,c_159]) ).
cnf(c_890,plain,
ld(mult(A,ld(A,B)),mult(B,C)) = mult(A,ld(A,mult(B,ld(B,C)))),
inference(paramod,[status(thm)],[c_83,c_159]) ).
cnf(c_891,plain,
mult(A,ld(A,C)) = mult(A,ld(A,mult(B,ld(B,C)))),
inference(paramod,[status(thm)],[c_159,c_890]) ).
cnf(c_167,plain,
mult(A,ld(A,mult(B,ld(B,C)))) = mult(A,ld(A,C)),
inference(copy,[status(thm)],[c_891]) ).
cnf(c_892,plain,
mult(rd(A,mult(rd(B,C),C)),rd(mult(B,C),C)) = mult(A,ld(C,C)),
inference(paramod,[status(thm)],[c_6,c_105]) ).
cnf(c_173,plain,
mult(rd(A,mult(rd(B,C),C)),mult(rd(B,C),C)) = mult(A,ld(C,C)),
inference(paramod,[status(thm)],[c_6,c_892]) ).
cnf(c_893,plain,
mult(ld(rd(A,B),rd(A,B)),rd(A,B)) = mult(rd(A,B),ld(B,B)),
inference(paramod,[status(thm)],[c_38,c_105]) ).
cnf(c_894,plain,
rd(A,B) = mult(rd(A,B),ld(B,B)),
inference(paramod,[status(thm)],[c_39,c_893]) ).
cnf(c_174,plain,
mult(rd(A,B),ld(B,B)) = rd(A,B),
inference(copy,[status(thm)],[c_894]) ).
cnf(c_895,plain,
mult(rd(A,B),rd(B,ld(B,B))) = mult(A,ld(ld(B,B),ld(B,B))),
inference(paramod,[status(thm)],[c_115,c_105]) ).
cnf(c_896,plain,
mult(rd(A,B),B) = mult(A,ld(ld(B,B),ld(B,B))),
inference(paramod,[status(thm)],[c_115,c_895]) ).
cnf(c_175,plain,
mult(rd(A,B),B) = mult(A,ld(B,B)),
inference(paramod,[status(thm)],[c_126,c_896]) ).
cnf(c_897,plain,
mult(rd(A,mult(B,ld(C,C))),mult(rd(B,C),C)) = mult(A,ld(C,C)),
inference(paramod,[status(thm)],[c_175,c_173]) ).
cnf(c_898,plain,
mult(rd(A,mult(B,ld(C,C))),mult(B,ld(C,C))) = mult(A,ld(C,C)),
inference(paramod,[status(thm)],[c_175,c_897]) ).
cnf(c_184,plain,
mult(A,ld(mult(B,ld(C,C)),mult(B,ld(C,C)))) = mult(A,ld(C,C)),
inference(paramod,[status(thm)],[c_175,c_898]) ).
cnf(c_191,plain,
mult(A,ld(A,mult(B,ld(C,C)))) = mult(A,mult(ld(A,B),ld(C,C))),
inference(paramod,[status(thm)],[c_175,c_143]) ).
cnf(c_192,plain,
mult(A,mult(ld(A,B),ld(B,B))) = mult(A,ld(A,B)),
inference(paramod,[status(thm)],[c_175,c_142]) ).
cnf(c_196,plain,
mult(A,ld(mult(A,ld(A,B)),mult(A,ld(A,B)))) = rd(mult(A,B),mult(A,ld(A,B))),
inference(paramod,[status(thm)],[c_175,c_130]) ).
cnf(c_202,plain,
mult(mult(A,B),ld(C,C)) = mult(A,mult(B,ld(C,C))),
inference(paramod,[status(thm)],[c_175,c_114]) ).
cnf(c_212,plain,
mult(mult(x3,ld(x4,x4)),x5) != mult(x3,x5),
inference(paramod,[status(thm)],[c_175,c_14]) ).
cnf(c_213,plain,
rd(mult(A,B),B) = mult(A,ld(B,B)),
inference(paramod,[status(thm)],[c_175,c_6]) ).
cnf(c_899,plain,
ld(rd(A,B),rd(A,B)) = mult(rd(A,B),ld(rd(A,B),ld(B,B))),
inference(paramod,[status(thm)],[c_174,c_4]) ).
cnf(c_223,plain,
mult(rd(A,B),ld(rd(A,B),ld(B,B))) = ld(rd(A,B),rd(A,B)),
inference(copy,[status(thm)],[c_899]) ).
cnf(c_900,plain,
mult(rd(A,ld(B,B)),ld(B,B)) = rd(A,ld(B,B)),
inference(paramod,[status(thm)],[c_126,c_174]) ).
cnf(c_901,plain,
mult(A,ld(ld(B,B),ld(B,B))) = rd(A,ld(B,B)),
inference(paramod,[status(thm)],[c_175,c_900]) ).
cnf(c_902,plain,
mult(A,ld(B,B)) = rd(A,ld(B,B)),
inference(paramod,[status(thm)],[c_126,c_901]) ).
cnf(c_224,plain,
rd(A,ld(B,B)) = mult(A,ld(B,B)),
inference(copy,[status(thm)],[c_902]) ).
cnf(c_903,plain,
mult(mult(A,ld(B,B)),ld(rd(A,ld(B,B)),ld(B,B))) = ld(rd(A,ld(B,B)),mult(A,ld(B,B))),
inference(paramod,[status(thm)],[c_224,c_121]) ).
cnf(c_904,plain,
mult(mult(A,ld(B,B)),ld(mult(A,ld(B,B)),ld(B,B))) = ld(rd(A,ld(B,B)),mult(A,ld(B,B))),
inference(paramod,[status(thm)],[c_224,c_903]) ).
cnf(c_905,plain,
mult(A,ld(A,ld(B,B))) = ld(rd(A,ld(B,B)),mult(A,ld(B,B))),
inference(paramod,[status(thm)],[c_162,c_904]) ).
cnf(c_906,plain,
mult(A,ld(A,ld(B,B))) = ld(mult(A,ld(B,B)),mult(A,ld(B,B))),
inference(paramod,[status(thm)],[c_224,c_905]) ).
cnf(c_230,plain,
ld(mult(A,ld(B,B)),mult(A,ld(B,B))) = mult(A,ld(A,ld(B,B))),
inference(copy,[status(thm)],[c_906]) ).
cnf(c_231,plain,
mult(A,mult(B,ld(B,ld(C,C)))) = mult(A,ld(C,C)),
inference(paramod,[status(thm)],[c_230,c_184]) ).
cnf(c_233,plain,
ld(rd(A,B),mult(A,ld(B,B))) = mult(rd(A,B),ld(rd(A,B),B)),
inference(paramod,[status(thm)],[c_175,c_4]) ).
cnf(c_907,plain,
rd(mult(rd(A,B),B),B) = rd(A,B),
inference(paramod,[status(thm)],[c_174,c_213]) ).
cnf(c_235,plain,
rd(mult(A,ld(B,B)),B) = rd(A,B),
inference(paramod,[status(thm)],[c_175,c_907]) ).
cnf(c_908,plain,
mult(mult(A,ld(B,B)),B) = mult(mult(A,B),ld(B,B)),
inference(paramod,[status(thm)],[c_213,c_175]) ).
cnf(c_909,plain,
mult(mult(A,ld(B,B)),B) = mult(A,mult(B,ld(B,B))),
inference(paramod,[status(thm)],[c_202,c_908]) ).
cnf(c_236,plain,
mult(mult(A,ld(B,B)),B) = mult(A,B),
inference(paramod,[status(thm)],[c_15,c_909]) ).
cnf(c_910,plain,
ld(mult(A,ld(B,B)),mult(A,B)) = mult(mult(A,ld(B,B)),ld(mult(A,ld(B,B)),B)),
inference(paramod,[status(thm)],[c_236,c_4]) ).
cnf(c_254,plain,
ld(mult(A,ld(B,B)),mult(A,B)) = mult(A,ld(A,B)),
inference(paramod,[status(thm)],[c_162,c_910]) ).
cnf(c_911,plain,
ld(mult(rd(A,B),mult(rd(A,B),ld(rd(A,B),B))),mult(mult(A,ld(B,B)),C)) = mult(rd(A,B),ld(rd(A,B),C)),
inference(paramod,[status(thm)],[c_233,c_159]) ).
cnf(c_912,plain,
ld(mult(rd(A,B),B),mult(mult(A,ld(B,B)),C)) = mult(rd(A,B),ld(rd(A,B),C)),
inference(paramod,[status(thm)],[c_83,c_911]) ).
cnf(c_913,plain,
ld(mult(A,ld(B,B)),mult(mult(A,ld(B,B)),C)) = mult(rd(A,B),ld(rd(A,B),C)),
inference(paramod,[status(thm)],[c_175,c_912]) ).
cnf(c_914,plain,
mult(mult(A,ld(B,B)),ld(mult(A,ld(B,B)),C)) = mult(rd(A,B),ld(rd(A,B),C)),
inference(paramod,[status(thm)],[c_4,c_913]) ).
cnf(c_915,plain,
mult(A,ld(A,C)) = mult(rd(A,B),ld(rd(A,B),C)),
inference(paramod,[status(thm)],[c_162,c_914]) ).
cnf(c_284,plain,
mult(rd(A,B),ld(rd(A,B),C)) = mult(A,ld(A,C)),
inference(copy,[status(thm)],[c_915]) ).
cnf(c_288,plain,
ld(rd(A,B),mult(A,ld(B,B))) = mult(A,ld(A,B)),
inference(paramod,[status(thm)],[c_284,c_233]) ).
cnf(c_916,plain,
mult(A,ld(A,ld(B,B))) = ld(rd(A,B),rd(A,B)),
inference(paramod,[status(thm)],[c_284,c_223]) ).
cnf(c_289,plain,
ld(rd(A,B),rd(A,B)) = mult(A,ld(A,ld(B,B))),
inference(copy,[status(thm)],[c_916]) ).
cnf(c_917,plain,
ld(rd(A,B),mult(A,ld(A,C))) = mult(rd(A,B),ld(rd(A,B),ld(rd(A,B),C))),
inference(paramod,[status(thm)],[c_284,c_4]) ).
cnf(c_291,plain,
ld(rd(A,B),mult(A,ld(A,C))) = ld(rd(A,B),C),
inference(paramod,[status(thm)],[c_151,c_917]) ).
cnf(c_918,plain,
mult(rd(A,B),mult(rd(A,B),ld(rd(A,B),C))) = mult(A,ld(A,mult(rd(A,B),C))),
inference(paramod,[status(thm)],[c_4,c_284]) ).
cnf(c_292,plain,
mult(rd(A,B),mult(A,ld(A,C))) = mult(A,ld(A,mult(rd(A,B),C))),
inference(paramod,[status(thm)],[c_284,c_918]) ).
cnf(c_919,plain,
mult(rd(A,B),mult(A,ld(A,C))) = mult(rd(A,B),C),
inference(paramod,[status(thm)],[c_284,c_83]) ).
cnf(c_294,plain,
mult(A,ld(A,mult(rd(A,B),C))) = mult(rd(A,B),C),
inference(paramod,[status(thm)],[c_292,c_919]) ).
cnf(c_302,plain,
mult(rd(A,B),mult(A,ld(A,C))) = mult(rd(A,B),C),
inference(paramod,[status(thm)],[c_294,c_292]) ).
cnf(c_920,plain,
ld(mult(A,ld(B,B)),mult(mult(A,B),ld(mult(A,B),C))) = ld(rd(mult(A,B),B),C),
inference(paramod,[status(thm)],[c_213,c_291]) ).
cnf(c_921,plain,
ld(mult(A,ld(B,B)),mult(A,ld(A,C))) = ld(rd(mult(A,B),B),C),
inference(paramod,[status(thm)],[c_162,c_920]) ).
cnf(c_318,plain,
ld(mult(A,ld(B,B)),mult(A,ld(A,C))) = ld(mult(A,ld(B,B)),C),
inference(paramod,[status(thm)],[c_213,c_921]) ).
cnf(c_922,plain,
mult(mult(A,ld(A,ld(B,B))),B) = mult(ld(A,A),B),
inference(paramod,[status(thm)],[c_127,c_236]) ).
cnf(c_923,plain,
mult(A,ld(A,mult(ld(B,B),B))) = mult(ld(A,A),B),
inference(paramod,[status(thm)],[c_81,c_922]) ).
cnf(c_924,plain,
mult(A,ld(A,B)) = mult(ld(A,A),B),
inference(paramod,[status(thm)],[c_39,c_923]) ).
cnf(c_333,plain,
mult(ld(A,A),B) = mult(A,ld(A,B)),
inference(copy,[status(thm)],[c_924]) ).
cnf(c_925,plain,
ld(mult(mult(A,ld(B,B)),ld(mult(A,ld(A,C)),mult(A,ld(A,C)))),mult(mult(A,ld(B,B)),mult(A,ld(A,C)))) = mult(mult(A,ld(B,B)),ld(mult(A,ld(B,B)),C)),
inference(paramod,[status(thm)],[c_318,c_254]) ).
cnf(c_926,plain,
ld(mult(A,mult(ld(B,B),ld(mult(A,ld(A,C)),mult(A,ld(A,C))))),mult(mult(A,ld(B,B)),mult(A,ld(A,C)))) = mult(mult(A,ld(B,B)),ld(mult(A,ld(B,B)),C)),
inference(paramod,[status(thm)],[c_202,c_925]) ).
cnf(c_927,plain,
ld(mult(A,mult(B,ld(B,ld(mult(A,ld(A,C)),mult(A,ld(A,C)))))),mult(mult(A,ld(B,B)),mult(A,ld(A,C)))) = mult(mult(A,ld(B,B)),ld(mult(A,ld(B,B)),C)),
inference(paramod,[status(thm)],[c_333,c_926]) ).
cnf(c_928,plain,
ld(mult(A,ld(mult(A,ld(A,C)),mult(A,ld(A,C)))),mult(mult(A,ld(B,B)),mult(A,ld(A,C)))) = mult(mult(A,ld(B,B)),ld(mult(A,ld(B,B)),C)),
inference(paramod,[status(thm)],[c_231,c_927]) ).
cnf(c_929,plain,
ld(rd(mult(A,C),mult(A,ld(A,C))),mult(mult(A,ld(B,B)),mult(A,ld(A,C)))) = mult(mult(A,ld(B,B)),ld(mult(A,ld(B,B)),C)),
inference(paramod,[status(thm)],[c_196,c_928]) ).
cnf(c_348,plain,
ld(rd(mult(A,B),mult(A,ld(A,B))),mult(mult(A,ld(C,C)),mult(A,ld(A,B)))) = mult(A,ld(A,B)),
inference(paramod,[status(thm)],[c_162,c_929]) ).
cnf(c_930,plain,
ld(mult(A,B),mult(A,ld(A,C))) = mult(mult(A,B),ld(mult(A,B),ld(mult(A,B),C))),
inference(paramod,[status(thm)],[c_162,c_4]) ).
cnf(c_370,plain,
ld(mult(A,B),mult(A,ld(A,C))) = ld(mult(A,B),C),
inference(paramod,[status(thm)],[c_151,c_930]) ).
cnf(c_931,plain,
mult(mult(A,B),mult(mult(A,B),ld(mult(A,B),C))) = mult(A,ld(A,mult(mult(A,B),C))),
inference(paramod,[status(thm)],[c_4,c_162]) ).
cnf(c_932,plain,
mult(mult(A,B),mult(A,ld(A,C))) = mult(A,ld(A,mult(mult(A,B),C))),
inference(paramod,[status(thm)],[c_162,c_931]) ).
cnf(c_371,plain,
mult(mult(A,B),mult(A,ld(A,C))) = mult(mult(A,B),C),
inference(paramod,[status(thm)],[c_140,c_932]) ).
cnf(c_933,plain,
mult(A,ld(mult(A,ld(A,B)),B)) = rd(mult(A,B),mult(A,ld(A,B))),
inference(paramod,[status(thm)],[c_370,c_196]) ).
cnf(c_934,plain,
mult(A,mult(A,ld(A,ld(B,B)))) = rd(mult(A,B),mult(A,ld(A,B))),
inference(paramod,[status(thm)],[c_163,c_933]) ).
cnf(c_935,plain,
mult(A,ld(B,B)) = rd(mult(A,B),mult(A,ld(A,B))),
inference(paramod,[status(thm)],[c_83,c_934]) ).
cnf(c_386,plain,
rd(mult(A,B),mult(A,ld(A,B))) = mult(A,ld(B,B)),
inference(copy,[status(thm)],[c_935]) ).
cnf(c_936,plain,
ld(mult(A,ld(B,B)),mult(mult(A,ld(C,C)),mult(A,ld(A,B)))) = mult(A,ld(A,B)),
inference(paramod,[status(thm)],[c_386,c_348]) ).
cnf(c_387,plain,
ld(mult(A,ld(B,B)),mult(mult(A,ld(C,C)),B)) = mult(A,ld(A,B)),
inference(paramod,[status(thm)],[c_371,c_936]) ).
cnf(c_937,plain,
rd(mult(A,ld(mult(B,ld(B,C)),C)),mult(B,ld(B,C))) = rd(A,mult(B,ld(B,C))),
inference(paramod,[status(thm)],[c_370,c_235]) ).
cnf(c_938,plain,
rd(mult(A,mult(B,ld(B,ld(C,C)))),mult(B,ld(B,C))) = rd(A,mult(B,ld(B,C))),
inference(paramod,[status(thm)],[c_163,c_937]) ).
cnf(c_399,plain,
rd(mult(A,ld(B,B)),mult(C,ld(C,B))) = rd(A,mult(C,ld(C,B))),
inference(paramod,[status(thm)],[c_231,c_938]) ).
cnf(c_939,plain,
rd(mult(rd(A,B),B),mult(rd(A,B),ld(rd(A,B),B))) = rd(A,B),
inference(paramod,[status(thm)],[c_174,c_386]) ).
cnf(c_940,plain,
rd(mult(A,ld(B,B)),mult(rd(A,B),ld(rd(A,B),B))) = rd(A,B),
inference(paramod,[status(thm)],[c_175,c_939]) ).
cnf(c_941,plain,
rd(mult(A,ld(B,B)),mult(A,ld(A,B))) = rd(A,B),
inference(paramod,[status(thm)],[c_284,c_940]) ).
cnf(c_408,plain,
rd(A,mult(A,ld(A,B))) = rd(A,B),
inference(paramod,[status(thm)],[c_399,c_941]) ).
cnf(c_415,plain,
rd(mult(A,B),mult(A,ld(A,C))) = rd(mult(A,B),C),
inference(paramod,[status(thm)],[c_162,c_408]) ).
cnf(c_942,plain,
rd(mult(A,ld(mult(B,ld(C,C)),mult(B,ld(C,C)))),mult(rd(B,C),mult(B,ld(B,C)))) = rd(A,mult(rd(B,C),ld(rd(B,C),mult(B,ld(C,C))))),
inference(paramod,[status(thm)],[c_288,c_399]) ).
cnf(c_943,plain,
rd(mult(A,mult(B,ld(B,ld(C,C)))),mult(rd(B,C),mult(B,ld(B,C)))) = rd(A,mult(rd(B,C),ld(rd(B,C),mult(B,ld(C,C))))),
inference(paramod,[status(thm)],[c_230,c_942]) ).
cnf(c_944,plain,
rd(mult(A,ld(C,C)),mult(rd(B,C),mult(B,ld(B,C)))) = rd(A,mult(rd(B,C),ld(rd(B,C),mult(B,ld(C,C))))),
inference(paramod,[status(thm)],[c_231,c_943]) ).
cnf(c_945,plain,
rd(mult(A,ld(C,C)),mult(rd(B,C),C)) = rd(A,mult(rd(B,C),ld(rd(B,C),mult(B,ld(C,C))))),
inference(paramod,[status(thm)],[c_302,c_944]) ).
cnf(c_946,plain,
rd(mult(A,ld(C,C)),mult(B,ld(C,C))) = rd(A,mult(rd(B,C),ld(rd(B,C),mult(B,ld(C,C))))),
inference(paramod,[status(thm)],[c_175,c_945]) ).
cnf(c_947,plain,
rd(mult(A,ld(C,C)),mult(B,ld(C,C))) = rd(A,mult(rd(B,C),mult(B,ld(B,C)))),
inference(paramod,[status(thm)],[c_288,c_946]) ).
cnf(c_948,plain,
rd(mult(A,ld(C,C)),mult(B,ld(C,C))) = rd(A,mult(rd(B,C),C)),
inference(paramod,[status(thm)],[c_302,c_947]) ).
cnf(c_456,plain,
rd(mult(A,ld(B,B)),mult(C,ld(B,B))) = rd(A,mult(C,ld(B,B))),
inference(paramod,[status(thm)],[c_175,c_948]) ).
cnf(c_949,plain,
rd(mult(A,ld(B,B)),mult(mult(A,ld(B,B)),ld(mult(A,ld(B,B)),mult(C,ld(C,B))))) = rd(A,mult(C,ld(C,B))),
inference(paramod,[status(thm)],[c_399,c_408]) ).
cnf(c_950,plain,
rd(mult(A,ld(B,B)),mult(mult(A,ld(B,B)),ld(mult(A,ld(B,B)),B))) = rd(A,mult(C,ld(C,B))),
inference(paramod,[status(thm)],[c_167,c_949]) ).
cnf(c_951,plain,
rd(mult(A,ld(B,B)),mult(A,ld(A,B))) = rd(A,mult(C,ld(C,B))),
inference(paramod,[status(thm)],[c_162,c_950]) ).
cnf(c_952,plain,
rd(mult(A,ld(B,B)),B) = rd(A,mult(C,ld(C,B))),
inference(paramod,[status(thm)],[c_415,c_951]) ).
cnf(c_953,plain,
rd(A,B) = rd(A,mult(C,ld(C,B))),
inference(paramod,[status(thm)],[c_235,c_952]) ).
cnf(c_458,plain,
rd(A,mult(B,ld(B,C))) = rd(A,C),
inference(copy,[status(thm)],[c_953]) ).
cnf(c_954,plain,
rd(mult(A,ld(B,B)),mult(C,ld(C,mult(D,ld(B,B))))) = rd(A,mult(mult(C,ld(C,D)),ld(B,B))),
inference(paramod,[status(thm)],[c_81,c_456]) ).
cnf(c_955,plain,
rd(mult(A,ld(B,B)),mult(C,mult(ld(C,D),ld(B,B)))) = rd(A,mult(mult(C,ld(C,D)),ld(B,B))),
inference(paramod,[status(thm)],[c_191,c_954]) ).
cnf(c_473,plain,
rd(mult(A,ld(B,B)),mult(C,mult(ld(C,D),ld(B,B)))) = rd(A,mult(C,mult(ld(C,D),ld(B,B)))),
inference(paramod,[status(thm)],[c_202,c_955]) ).
cnf(c_956,plain,
rd(mult(A,ld(B,B)),mult(C,ld(C,mult(D,ld(B,B))))) = rd(A,mult(D,ld(B,B))),
inference(paramod,[status(thm)],[c_456,c_458]) ).
cnf(c_957,plain,
rd(mult(A,ld(B,B)),mult(C,mult(ld(C,D),ld(B,B)))) = rd(A,mult(D,ld(B,B))),
inference(paramod,[status(thm)],[c_191,c_956]) ).
cnf(c_478,plain,
rd(A,mult(B,mult(ld(B,C),ld(D,D)))) = rd(A,mult(C,ld(D,D))),
inference(paramod,[status(thm)],[c_473,c_957]) ).
cnf(c_958,plain,
ld(A,mult(A,ld(A,B))) = mult(A,ld(A,ld(A,mult(C,ld(C,B))))),
inference(paramod,[status(thm)],[c_167,c_4]) ).
cnf(c_959,plain,
mult(A,ld(A,ld(A,B))) = mult(A,ld(A,ld(A,mult(C,ld(C,B))))),
inference(paramod,[status(thm)],[c_4,c_958]) ).
cnf(c_960,plain,
ld(A,B) = mult(A,ld(A,ld(A,mult(C,ld(C,B))))),
inference(paramod,[status(thm)],[c_151,c_959]) ).
cnf(c_961,plain,
ld(A,B) = ld(A,mult(C,ld(C,B))),
inference(paramod,[status(thm)],[c_151,c_960]) ).
cnf(c_488,plain,
ld(A,mult(B,ld(B,C))) = ld(A,C),
inference(copy,[status(thm)],[c_961]) ).
cnf(c_962,plain,
mult(A,mult(A,ld(A,B))) = mult(A,mult(C,ld(C,B))),
inference(paramod,[status(thm)],[c_167,c_83]) ).
cnf(c_963,plain,
mult(A,B) = mult(A,mult(C,ld(C,B))),
inference(paramod,[status(thm)],[c_83,c_962]) ).
cnf(c_489,plain,
mult(A,mult(B,ld(B,C))) = mult(A,C),
inference(copy,[status(thm)],[c_963]) ).
cnf(c_964,plain,
ld(mult(A,ld(A,B)),mult(B,ld(B,C))) = mult(A,ld(A,ld(B,mult(D,ld(D,C))))),
inference(paramod,[status(thm)],[c_167,c_159]) ).
cnf(c_965,plain,
ld(mult(A,ld(A,B)),C) = mult(A,ld(A,ld(B,mult(D,ld(D,C))))),
inference(paramod,[status(thm)],[c_488,c_964]) ).
cnf(c_490,plain,
ld(mult(A,ld(A,B)),C) = mult(A,ld(A,ld(B,C))),
inference(paramod,[status(thm)],[c_488,c_965]) ).
cnf(c_966,plain,
ld(A,mult(A,ld(A,B))) = mult(A,ld(A,mult(ld(A,B),ld(B,B)))),
inference(paramod,[status(thm)],[c_192,c_4]) ).
cnf(c_967,plain,
mult(A,ld(A,ld(A,B))) = mult(A,ld(A,mult(ld(A,B),ld(B,B)))),
inference(paramod,[status(thm)],[c_4,c_966]) ).
cnf(c_968,plain,
ld(A,B) = mult(A,ld(A,mult(ld(A,B),ld(B,B)))),
inference(paramod,[status(thm)],[c_151,c_967]) ).
cnf(c_969,plain,
ld(A,B) = mult(A,mult(ld(A,ld(A,B)),ld(B,B))),
inference(paramod,[status(thm)],[c_191,c_968]) ).
cnf(c_492,plain,
mult(A,mult(ld(A,ld(A,B)),ld(B,B))) = ld(A,B),
inference(copy,[status(thm)],[c_969]) ).
cnf(c_970,plain,
rd(mult(A,ld(A,B)),mult(ld(A,B),ld(B,B))) = mult(A,ld(mult(ld(A,B),ld(B,B)),mult(ld(A,B),ld(B,B)))),
inference(paramod,[status(thm)],[c_192,c_213]) ).
cnf(c_971,plain,
rd(mult(A,ld(A,B)),mult(ld(A,B),ld(B,B))) = mult(A,mult(ld(A,B),ld(ld(A,B),ld(B,B)))),
inference(paramod,[status(thm)],[c_230,c_970]) ).
cnf(c_972,plain,
rd(mult(A,ld(A,B)),mult(ld(A,B),ld(B,B))) = mult(A,mult(A,ld(A,ld(B,B)))),
inference(paramod,[status(thm)],[c_99,c_971]) ).
cnf(c_495,plain,
rd(mult(A,ld(A,B)),mult(ld(A,B),ld(B,B))) = mult(A,ld(B,B)),
inference(paramod,[status(thm)],[c_489,c_972]) ).
cnf(c_973,plain,
ld(mult(A,ld(mult(ld(A,B),ld(B,B)),mult(ld(A,B),ld(B,B)))),mult(A,ld(A,B))) = mult(A,ld(A,mult(ld(A,B),ld(B,B)))),
inference(paramod,[status(thm)],[c_192,c_254]) ).
cnf(c_974,plain,
ld(mult(A,mult(ld(A,B),ld(ld(A,B),ld(B,B)))),mult(A,ld(A,B))) = mult(A,ld(A,mult(ld(A,B),ld(B,B)))),
inference(paramod,[status(thm)],[c_230,c_973]) ).
cnf(c_975,plain,
ld(mult(A,mult(A,ld(A,ld(B,B)))),mult(A,ld(A,B))) = mult(A,ld(A,mult(ld(A,B),ld(B,B)))),
inference(paramod,[status(thm)],[c_99,c_974]) ).
cnf(c_976,plain,
ld(mult(A,ld(B,B)),mult(A,ld(A,B))) = mult(A,ld(A,mult(ld(A,B),ld(B,B)))),
inference(paramod,[status(thm)],[c_489,c_975]) ).
cnf(c_977,plain,
ld(mult(A,ld(B,B)),B) = mult(A,ld(A,mult(ld(A,B),ld(B,B)))),
inference(paramod,[status(thm)],[c_488,c_976]) ).
cnf(c_978,plain,
ld(mult(A,ld(B,B)),B) = mult(A,mult(ld(A,ld(A,B)),ld(B,B))),
inference(paramod,[status(thm)],[c_191,c_977]) ).
cnf(c_497,plain,
ld(mult(A,ld(B,B)),B) = ld(A,B),
inference(paramod,[status(thm)],[c_492,c_978]) ).
cnf(c_979,plain,
rd(mult(A,ld(A,mult(B,ld(mult(A,ld(A,B)),C)))),mult(ld(mult(A,ld(A,B)),C),ld(C,C))) = mult(mult(A,ld(A,B)),ld(C,C)),
inference(paramod,[status(thm)],[c_81,c_495]) ).
cnf(c_980,plain,
rd(mult(A,ld(A,mult(B,mult(A,ld(A,ld(B,C)))))),mult(ld(mult(A,ld(A,B)),C),ld(C,C))) = mult(mult(A,ld(A,B)),ld(C,C)),
inference(paramod,[status(thm)],[c_490,c_979]) ).
cnf(c_981,plain,
rd(mult(A,ld(A,mult(B,ld(B,C)))),mult(ld(mult(A,ld(A,B)),C),ld(C,C))) = mult(mult(A,ld(A,B)),ld(C,C)),
inference(paramod,[status(thm)],[c_489,c_980]) ).
cnf(c_982,plain,
rd(mult(A,ld(A,C)),mult(ld(mult(A,ld(A,B)),C),ld(C,C))) = mult(mult(A,ld(A,B)),ld(C,C)),
inference(paramod,[status(thm)],[c_488,c_981]) ).
cnf(c_983,plain,
rd(mult(A,ld(A,C)),mult(mult(A,ld(A,ld(B,C))),ld(C,C))) = mult(mult(A,ld(A,B)),ld(C,C)),
inference(paramod,[status(thm)],[c_490,c_982]) ).
cnf(c_984,plain,
rd(mult(A,ld(A,C)),mult(A,mult(ld(A,ld(B,C)),ld(C,C)))) = mult(mult(A,ld(A,B)),ld(C,C)),
inference(paramod,[status(thm)],[c_202,c_983]) ).
cnf(c_985,plain,
rd(mult(A,ld(A,C)),mult(ld(B,C),ld(C,C))) = mult(mult(A,ld(A,B)),ld(C,C)),
inference(paramod,[status(thm)],[c_478,c_984]) ).
cnf(c_506,plain,
rd(mult(A,ld(A,B)),mult(ld(C,B),ld(B,B))) = mult(A,mult(ld(A,C),ld(B,B))),
inference(paramod,[status(thm)],[c_202,c_985]) ).
cnf(c_986,plain,
rd(mult(A,ld(A,B)),mult(ld(ld(A,C),B),ld(B,B))) = mult(ld(A,C),ld(B,B)),
inference(paramod,[status(thm)],[c_99,c_495]) ).
cnf(c_507,plain,
mult(A,mult(ld(A,ld(A,B)),ld(C,C))) = mult(ld(A,B),ld(C,C)),
inference(paramod,[status(thm)],[c_506,c_986]) ).
cnf(c_515,plain,
mult(ld(A,B),ld(B,B)) = ld(A,B),
inference(paramod,[status(thm)],[c_507,c_492]) ).
cnf(c_987,plain,
ld(ld(A,B),ld(A,B)) = mult(ld(A,B),ld(ld(A,B),ld(B,B))),
inference(paramod,[status(thm)],[c_515,c_4]) ).
cnf(c_531,plain,
ld(ld(A,B),ld(A,B)) = mult(A,ld(A,ld(B,B))),
inference(paramod,[status(thm)],[c_99,c_987]) ).
cnf(c_988,plain,
rd(mult(A,ld(B,B)),ld(C,B)) = rd(A,mult(ld(C,B),ld(B,B))),
inference(paramod,[status(thm)],[c_515,c_456]) ).
cnf(c_536,plain,
rd(mult(A,ld(B,B)),ld(C,B)) = rd(A,ld(C,B)),
inference(paramod,[status(thm)],[c_515,c_988]) ).
cnf(c_989,plain,
mult(rd(A,ld(B,C)),ld(ld(B,C),ld(B,C))) = rd(mult(A,ld(C,C)),ld(B,C)),
inference(paramod,[status(thm)],[c_536,c_174]) ).
cnf(c_990,plain,
mult(rd(A,ld(B,C)),mult(B,ld(B,ld(C,C)))) = rd(mult(A,ld(C,C)),ld(B,C)),
inference(paramod,[status(thm)],[c_531,c_989]) ).
cnf(c_991,plain,
mult(rd(A,ld(B,C)),ld(C,C)) = rd(mult(A,ld(C,C)),ld(B,C)),
inference(paramod,[status(thm)],[c_489,c_990]) ).
cnf(c_543,plain,
mult(rd(A,ld(B,C)),ld(C,C)) = rd(A,ld(B,C)),
inference(paramod,[status(thm)],[c_536,c_991]) ).
cnf(c_992,plain,
mult(rd(A,mult(B,ld(B,C))),ld(mult(B,C),mult(B,C))) = rd(A,ld(B,mult(B,C))),
inference(paramod,[status(thm)],[c_4,c_543]) ).
cnf(c_993,plain,
mult(rd(A,C),ld(mult(B,C),mult(B,C))) = rd(A,ld(B,mult(B,C))),
inference(paramod,[status(thm)],[c_458,c_992]) ).
cnf(c_994,plain,
mult(rd(A,C),ld(mult(B,C),mult(B,C))) = rd(A,mult(B,ld(B,C))),
inference(paramod,[status(thm)],[c_4,c_993]) ).
cnf(c_551,plain,
mult(rd(A,B),ld(mult(C,B),mult(C,B))) = rd(A,B),
inference(paramod,[status(thm)],[c_458,c_994]) ).
cnf(c_995,plain,
mult(rd(A,ld(mult(B,C),mult(B,C))),ld(rd(D,C),mult(rd(D,C),ld(mult(B,C),mult(B,C))))) = rd(A,ld(mult(B,C),mult(B,C))),
inference(paramod,[status(thm)],[c_551,c_551]) ).
cnf(c_996,plain,
mult(mult(A,ld(mult(B,C),mult(B,C))),ld(rd(D,C),mult(rd(D,C),ld(mult(B,C),mult(B,C))))) = rd(A,ld(mult(B,C),mult(B,C))),
inference(paramod,[status(thm)],[c_224,c_995]) ).
cnf(c_997,plain,
mult(mult(A,ld(mult(B,C),mult(B,C))),ld(rd(D,C),rd(D,C))) = rd(A,ld(mult(B,C),mult(B,C))),
inference(paramod,[status(thm)],[c_551,c_996]) ).
cnf(c_998,plain,
mult(mult(A,ld(mult(B,C),mult(B,C))),mult(D,ld(D,ld(C,C)))) = rd(A,ld(mult(B,C),mult(B,C))),
inference(paramod,[status(thm)],[c_289,c_997]) ).
cnf(c_999,plain,
mult(mult(A,ld(mult(B,C),mult(B,C))),ld(C,C)) = rd(A,ld(mult(B,C),mult(B,C))),
inference(paramod,[status(thm)],[c_489,c_998]) ).
cnf(c_1000,plain,
mult(A,mult(ld(mult(B,C),mult(B,C)),ld(C,C))) = rd(A,ld(mult(B,C),mult(B,C))),
inference(paramod,[status(thm)],[c_202,c_999]) ).
cnf(c_1001,plain,
mult(A,mult(mult(B,C),ld(mult(B,C),ld(C,C)))) = rd(A,ld(mult(B,C),mult(B,C))),
inference(paramod,[status(thm)],[c_333,c_1000]) ).
cnf(c_1002,plain,
mult(A,mult(B,ld(B,ld(C,C)))) = rd(A,ld(mult(B,C),mult(B,C))),
inference(paramod,[status(thm)],[c_162,c_1001]) ).
cnf(c_1003,plain,
mult(A,ld(C,C)) = rd(A,ld(mult(B,C),mult(B,C))),
inference(paramod,[status(thm)],[c_489,c_1002]) ).
cnf(c_1004,plain,
mult(A,ld(C,C)) = mult(A,ld(mult(B,C),mult(B,C))),
inference(paramod,[status(thm)],[c_224,c_1003]) ).
cnf(c_568,plain,
mult(A,ld(mult(B,C),mult(B,C))) = mult(A,ld(C,C)),
inference(copy,[status(thm)],[c_1004]) ).
cnf(c_609,plain,
ld(mult(A,ld(B,B)),mult(C,B)) = ld(A,mult(C,B)),
inference(paramod,[status(thm)],[c_568,c_497]) ).
cnf(c_615,plain,
ld(A,mult(mult(A,ld(B,B)),C)) = mult(A,ld(A,C)),
inference(paramod,[status(thm)],[c_609,c_387]) ).
cnf(c_1005,plain,
mult(mult(A,B),ld(mult(A,B),mult(mult(A,ld(B,B)),C))) = mult(rd(mult(A,B),B),C),
inference(paramod,[status(thm)],[c_213,c_294]) ).
cnf(c_1006,plain,
mult(A,ld(A,mult(mult(A,ld(B,B)),C))) = mult(rd(mult(A,B),B),C),
inference(paramod,[status(thm)],[c_162,c_1005]) ).
cnf(c_1007,plain,
mult(A,mult(A,ld(A,C))) = mult(rd(mult(A,B),B),C),
inference(paramod,[status(thm)],[c_615,c_1006]) ).
cnf(c_1008,plain,
mult(A,C) = mult(rd(mult(A,B),B),C),
inference(paramod,[status(thm)],[c_489,c_1007]) ).
cnf(c_1009,plain,
mult(A,C) = mult(mult(A,ld(B,B)),C),
inference(paramod,[status(thm)],[c_213,c_1008]) ).
cnf(c_836,plain,
mult(mult(A,ld(B,B)),C) = mult(A,C),
inference(copy,[status(thm)],[c_1009]) ).
cnf(c_837,plain,
$false,
inference(resolve,[status(thm)],[c_836,c_212]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP683-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.10/5.37 % Computer : n005.cluster.edu
% 0.10/5.37 % Model : x86_64 x86_64
% 0.10/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.37 % Memory : 8046.5625MB
% 0.10/5.37 % OS : Linux 6.8.0-71-generic
% 0.10/5.37 % CPULimit : 300
% 0.10/5.37 % WCLimit : 300
% 0.10/5.37 % DateTime : Fri Sep 25 15:36:37 UTC 2026
% 0.10/5.37 % CPUTime :
% 0.10/5.38 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/5.38 % Process 3855621 was started by sandbox on n005,
% 0.10/5.38 % Fri Sep 25 15:36:37 2026
% 0.10/5.38 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.10/5.38
% 0.10/5.38 % From the command line: assign(max_seconds, 300).
% 0.14/5.68
% 0.14/5.68 % SZS status Unsatisfiable for theBenchmark
% 0.14/5.68
% 0.14/5.68 % Proof 1 at 0.20 (+ 0.08) seconds.
% 0.14/5.68 % Length of proof is 111.
% 0.14/5.68 % Level of proof is 29.
% 0.14/5.68 % Maximum clause weight is 80.000.
% 0.14/5.68 % Given clauses 110.
% 0.14/5.68
% 0.14/5.68 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------