%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP754-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 : n003.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:23 AM UTC 2026
% Result : Unsatisfiable 110.67s 21.10s
% Output : CNFRefutation 110.67s
% Verified :
% SZS Type : Refutation
% Derivation depth : 49
% Number of leaves : 7
% Syntax : Number of formulae : 191 ( 191 unt; 0 def)
% Number of atoms : 191 ( 190 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 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 : 591 ( 0 sgn 14 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f01,axiom,
! [VAR_0,VAR_1] : mult(VAR_0,ld(VAR_0,VAR_1)) = VAR_1,
file('theBenchmark.p',f01) ).
cnf(c_1,plain,
mult(A,ld(A,B)) = B,
inference(clausify,[status(thm)],[f01]) ).
fof(f02,axiom,
! [VAR_0,VAR_1] : ld(VAR_0,mult(VAR_0,VAR_1)) = VAR_1,
file('theBenchmark.p',f02) ).
cnf(c_2,plain,
ld(A,mult(A,B)) = B,
inference(clausify,[status(thm)],[f02]) ).
fof(f03,axiom,
! [VAR_0,VAR_1] : mult(rd(VAR_0,VAR_1),VAR_1) = VAR_0,
file('theBenchmark.p',f03) ).
cnf(c_3,plain,
mult(rd(A,B),B) = A,
inference(clausify,[status(thm)],[f03]) ).
fof(f04,axiom,
! [VAR_0,VAR_1] : rd(mult(VAR_0,VAR_1),VAR_1) = VAR_0,
file('theBenchmark.p',f04) ).
cnf(c_4,plain,
rd(mult(A,B),B) = A,
inference(clausify,[status(thm)],[f04]) ).
fof(f05,axiom,
! [VAR_0,VAR_1,VAR_2] : mult(VAR_0,mult(VAR_1,VAR_2)) = mult(mult(rd(VAR_0,VAR_0),VAR_1),mult(VAR_0,VAR_2)),
file('theBenchmark.p',f05) ).
cnf(c_5,plain,
mult(A,mult(B,C)) = mult(mult(rd(A,A),B),mult(A,C)),
inference(clausify,[status(thm)],[f05]) ).
cnf(c_6,plain,
mult(mult(rd(A,A),B),mult(A,C)) = mult(A,mult(B,C)),
inference(copy,[status(thm)],[c_5]) ).
fof(f06,axiom,
! [VAR_0,VAR_1,VAR_2] : mult(mult(VAR_0,VAR_1),VAR_2) = mult(mult(VAR_0,VAR_2),mult(VAR_1,ld(VAR_2,VAR_2))),
file('theBenchmark.p',f06) ).
cnf(c_7,plain,
mult(mult(A,B),C) = mult(mult(A,C),mult(B,ld(C,C))),
inference(clausify,[status(thm)],[f06]) ).
cnf(c_8,plain,
mult(mult(A,B),mult(C,ld(B,B))) = mult(mult(A,C),B),
inference(copy,[status(thm)],[c_7]) ).
fof(goals,axiom,
mult(mult(a,a),mult(b,c)) != mult(mult(a,b),mult(a,c)),
file('theBenchmark.p',goals) ).
cnf(c_9,plain,
mult(mult(a,a),mult(b,c)) != mult(mult(a,b),mult(a,c)),
inference(clausify,[status(thm)],[goals]) ).
cnf(c_10,plain,
mult(mult(a,b),mult(a,c)) != mult(mult(a,a),mult(b,c)),
inference(copy,[status(thm)],[c_9]) ).
cnf(c_11,plain,
ld(rd(A,B),A) = B,
inference(paramod,[status(thm)],[c_3,c_2]) ).
cnf(c_12,plain,
rd(A,ld(B,A)) = B,
inference(paramod,[status(thm)],[c_1,c_4]) ).
cnf(c_18073,plain,
mult(A,mult(B,C)) = mult(B,mult(ld(rd(B,B),A),C)),
inference(paramod,[status(thm)],[c_1,c_6]) ).
cnf(c_13,plain,
mult(A,mult(ld(rd(A,A),B),C)) = mult(B,mult(A,C)),
inference(copy,[status(thm)],[c_18073]) ).
cnf(c_14,plain,
mult(mult(rd(A,A),B),C) = mult(A,mult(B,ld(A,C))),
inference(paramod,[status(thm)],[c_1,c_6]) ).
cnf(c_15,plain,
ld(mult(rd(A,A),B),mult(A,mult(B,C))) = mult(A,C),
inference(paramod,[status(thm)],[c_6,c_2]) ).
cnf(c_16,plain,
rd(mult(A,mult(B,C)),mult(A,C)) = mult(rd(A,A),B),
inference(paramod,[status(thm)],[c_6,c_4]) ).
cnf(c_18,plain,
ld(mult(A,B),mult(mult(A,C),B)) = mult(C,ld(B,B)),
inference(paramod,[status(thm)],[c_8,c_2]) ).
cnf(c_18074,plain,
mult(A,mult(B,ld(C,C))) = mult(mult(rd(A,C),B),C),
inference(paramod,[status(thm)],[c_3,c_8]) ).
cnf(c_19,plain,
mult(mult(rd(A,B),C),B) = mult(A,mult(C,ld(B,B))),
inference(copy,[status(thm)],[c_18074]) ).
cnf(c_18075,plain,
mult(mult(A,B),C) = mult(mult(A,rd(C,ld(B,B))),B),
inference(paramod,[status(thm)],[c_3,c_8]) ).
cnf(c_20,plain,
mult(mult(A,rd(B,ld(C,C))),C) = mult(mult(A,C),B),
inference(copy,[status(thm)],[c_18075]) ).
cnf(c_21,plain,
rd(mult(mult(A,B),C),mult(B,ld(C,C))) = mult(A,C),
inference(paramod,[status(thm)],[c_8,c_4]) ).
cnf(c_28,plain,
ld(mult(rd(A,A),B),mult(A,C)) = mult(A,ld(B,C)),
inference(paramod,[status(thm)],[c_1,c_15]) ).
cnf(c_33,plain,
rd(mult(A,B),mult(A,C)) = mult(rd(A,A),rd(B,C)),
inference(paramod,[status(thm)],[c_3,c_16]) ).
cnf(c_18076,plain,
rd(A,mult(B,C)) = mult(rd(B,B),rd(ld(B,A),C)),
inference(paramod,[status(thm)],[c_1,c_33]) ).
cnf(c_41,plain,
mult(rd(A,A),rd(ld(A,B),C)) = rd(B,mult(A,C)),
inference(copy,[status(thm)],[c_18076]) ).
cnf(c_18077,plain,
rd(mult(A,B),C) = mult(rd(A,A),rd(B,ld(A,C))),
inference(paramod,[status(thm)],[c_1,c_33]) ).
cnf(c_42,plain,
mult(rd(A,A),rd(B,ld(A,C))) = rd(mult(A,B),C),
inference(copy,[status(thm)],[c_18077]) ).
cnf(c_50,plain,
ld(mult(A,B),mult(C,B)) = mult(ld(A,C),ld(B,B)),
inference(paramod,[status(thm)],[c_1,c_18]) ).
cnf(c_58,plain,
ld(A,mult(B,mult(A,C))) = mult(ld(rd(A,A),B),C),
inference(paramod,[status(thm)],[c_13,c_2]) ).
cnf(c_18078,plain,
ld(A,mult(B,C)) = mult(ld(rd(A,C),B),ld(C,C)),
inference(paramod,[status(thm)],[c_3,c_50]) ).
cnf(c_72,plain,
mult(ld(rd(A,B),C),ld(B,B)) = ld(A,mult(C,B)),
inference(copy,[status(thm)],[c_18078]) ).
cnf(c_18079,plain,
ld(mult(A,B),C) = mult(ld(A,rd(C,B)),ld(B,B)),
inference(paramod,[status(thm)],[c_3,c_50]) ).
cnf(c_73,plain,
mult(ld(A,rd(B,C)),ld(C,C)) = ld(mult(A,C),B),
inference(copy,[status(thm)],[c_18079]) ).
cnf(c_97,plain,
rd(mult(A,B),mult(C,ld(B,B))) = mult(rd(A,C),B),
inference(paramod,[status(thm)],[c_3,c_21]) ).
cnf(c_107,plain,
ld(mult(rd(A,A),B),C) = mult(A,ld(B,ld(A,C))),
inference(paramod,[status(thm)],[c_1,c_28]) ).
cnf(c_117,plain,
ld(rd(A,A),rd(B,mult(A,C))) = rd(ld(A,B),C),
inference(paramod,[status(thm)],[c_41,c_2]) ).
cnf(c_128,plain,
ld(rd(A,A),rd(mult(A,B),C)) = rd(B,ld(A,C)),
inference(paramod,[status(thm)],[c_42,c_2]) ).
cnf(c_18080,plain,
ld(A,mult(B,C)) = mult(ld(rd(A,A),B),ld(A,C)),
inference(paramod,[status(thm)],[c_1,c_58]) ).
cnf(c_149,plain,
mult(ld(rd(A,A),B),ld(A,C)) = ld(A,mult(B,C)),
inference(copy,[status(thm)],[c_18080]) ).
cnf(c_164,plain,
rd(ld(A,mult(B,C)),ld(C,C)) = ld(rd(A,C),B),
inference(paramod,[status(thm)],[c_72,c_4]) ).
cnf(c_193,plain,
rd(A,mult(B,ld(C,C))) = mult(rd(rd(A,C),B),C),
inference(paramod,[status(thm)],[c_3,c_97]) ).
cnf(c_18081,plain,
mult(rd(A,A),rd(ld(A,mult(B,C)),ld(C,C))) = mult(rd(B,A),C),
inference(paramod,[status(thm)],[c_97,c_41]) ).
cnf(c_202,plain,
mult(rd(A,A),ld(rd(A,B),C)) = mult(rd(C,A),B),
inference(paramod,[status(thm)],[c_164,c_18081]) ).
cnf(c_18082,plain,
ld(rd(A,A),rd(B,C)) = rd(ld(A,B),ld(A,C)),
inference(paramod,[status(thm)],[c_1,c_117]) ).
cnf(c_223,plain,
rd(ld(A,B),ld(A,C)) = ld(rd(A,A),rd(B,C)),
inference(copy,[status(thm)],[c_18082]) ).
cnf(c_244,plain,
rd(mult(mult(A,B),C),B) = mult(A,rd(C,ld(B,B))),
inference(paramod,[status(thm)],[c_20,c_4]) ).
cnf(c_260,plain,
ld(ld(rd(A,A),rd(B,C)),ld(A,B)) = ld(A,C),
inference(paramod,[status(thm)],[c_223,c_11]) ).
cnf(c_18083,plain,
mult(rd(A,ld(B,C)),ld(C,C)) = ld(mult(rd(B,B),C),mult(B,A)),
inference(paramod,[status(thm)],[c_128,c_73]) ).
cnf(c_18084,plain,
mult(rd(A,ld(B,C)),ld(C,C)) = mult(B,ld(C,ld(B,mult(B,A)))),
inference(paramod,[status(thm)],[c_107,c_18083]) ).
cnf(c_298,plain,
mult(rd(A,ld(B,C)),ld(C,C)) = mult(B,ld(C,A)),
inference(paramod,[status(thm)],[c_2,c_18084]) ).
cnf(c_369,plain,
rd(ld(A,B),ld(C,C)) = ld(rd(A,C),rd(B,C)),
inference(paramod,[status(thm)],[c_3,c_164]) ).
cnf(c_18085,plain,
ld(rd(A,A),rd(mult(B,C),mult(A,ld(C,C)))) = ld(rd(A,C),B),
inference(paramod,[status(thm)],[c_164,c_117]) ).
cnf(c_18086,plain,
ld(rd(A,A),mult(rd(rd(mult(B,C),C),A),C)) = ld(rd(A,C),B),
inference(paramod,[status(thm)],[c_193,c_18085]) ).
cnf(c_378,plain,
ld(rd(A,A),mult(rd(B,A),C)) = ld(rd(A,C),B),
inference(paramod,[status(thm)],[c_4,c_18086]) ).
cnf(c_18087,plain,
mult(rd(A,A),ld(B,C)) = mult(rd(C,A),ld(B,A)),
inference(paramod,[status(thm)],[c_12,c_202]) ).
cnf(c_458,plain,
mult(rd(A,B),ld(C,B)) = mult(rd(B,B),ld(C,A)),
inference(copy,[status(thm)],[c_18087]) ).
cnf(c_487,plain,
ld(rd(A,B),mult(rd(B,B),ld(C,A))) = ld(C,B),
inference(paramod,[status(thm)],[c_458,c_2]) ).
cnf(c_488,plain,
mult(rd(mult(A,B),C),ld(A,C)) = mult(rd(C,C),B),
inference(paramod,[status(thm)],[c_2,c_458]) ).
cnf(c_18088,plain,
mult(A,ld(B,C)) = mult(rd(C,C),ld(B,mult(A,C))),
inference(paramod,[status(thm)],[c_4,c_458]) ).
cnf(c_491,plain,
mult(rd(A,A),ld(B,mult(C,A))) = mult(C,ld(B,A)),
inference(copy,[status(thm)],[c_18088]) ).
cnf(c_18089,plain,
rd(mult(A,B),C) = mult(rd(A,C),rd(B,ld(C,C))),
inference(paramod,[status(thm)],[c_3,c_244]) ).
cnf(c_596,plain,
mult(rd(A,B),rd(C,ld(B,B))) = rd(mult(A,C),B),
inference(copy,[status(thm)],[c_18089]) ).
cnf(c_624,plain,
ld(ld(rd(A,A),B),ld(A,C)) = ld(A,ld(B,C)),
inference(paramod,[status(thm)],[c_12,c_260]) ).
cnf(c_639,plain,
rd(mult(A,ld(B,C)),ld(B,B)) = rd(C,ld(A,B)),
inference(paramod,[status(thm)],[c_298,c_4]) ).
cnf(c_642,plain,
mult(rd(A,B),ld(C,C)) = mult(rd(C,B),ld(C,A)),
inference(paramod,[status(thm)],[c_11,c_298]) ).
cnf(c_676,plain,
mult(rd(mult(A,B),C),ld(A,A)) = mult(rd(A,C),B),
inference(paramod,[status(thm)],[c_2,c_642]) ).
cnf(c_677,plain,
rd(mult(rd(A,B),ld(C,C)),ld(C,A)) = rd(C,B),
inference(paramod,[status(thm)],[c_642,c_4]) ).
cnf(c_18090,plain,
ld(rd(mult(A,B),mult(A,B)),mult(mult(rd(A,A),rd(C,B)),D)) = ld(rd(mult(A,B),D),mult(A,C)),
inference(paramod,[status(thm)],[c_33,c_378]) ).
cnf(c_18091,plain,
ld(mult(rd(A,A),rd(B,B)),mult(mult(rd(A,A),rd(C,B)),D)) = ld(rd(mult(A,B),D),mult(A,C)),
inference(paramod,[status(thm)],[c_33,c_18090]) ).
cnf(c_18092,plain,
ld(mult(rd(A,A),rd(B,B)),mult(A,mult(rd(C,B),ld(A,D)))) = ld(rd(mult(A,B),D),mult(A,C)),
inference(paramod,[status(thm)],[c_14,c_18091]) ).
cnf(c_18093,plain,
mult(A,ld(rd(B,B),ld(A,mult(A,mult(rd(C,B),ld(A,D)))))) = ld(rd(mult(A,B),D),mult(A,C)),
inference(paramod,[status(thm)],[c_107,c_18092]) ).
cnf(c_18094,plain,
mult(A,ld(rd(B,B),mult(rd(C,B),ld(A,D)))) = ld(rd(mult(A,B),D),mult(A,C)),
inference(paramod,[status(thm)],[c_2,c_18093]) ).
cnf(c_18095,plain,
mult(A,ld(rd(B,ld(A,D)),C)) = ld(rd(mult(A,B),D),mult(A,C)),
inference(paramod,[status(thm)],[c_378,c_18094]) ).
cnf(c_763,plain,
ld(rd(mult(A,B),C),mult(A,D)) = mult(A,ld(rd(B,ld(A,C)),D)),
inference(copy,[status(thm)],[c_18095]) ).
cnf(c_18096,plain,
ld(rd(A,A),mult(rd(B,A),ld(B,C))) = ld(rd(A,ld(B,B)),C),
inference(paramod,[status(thm)],[c_642,c_378]) ).
cnf(c_789,plain,
ld(rd(A,ld(B,C)),B) = ld(rd(A,ld(B,B)),C),
inference(paramod,[status(thm)],[c_378,c_18096]) ).
cnf(c_1106,plain,
ld(rd(A,B),mult(rd(B,B),C)) = ld(rd(A,C),B),
inference(paramod,[status(thm)],[c_11,c_487]) ).
cnf(c_1152,plain,
rd(mult(rd(A,A),B),ld(C,A)) = rd(mult(C,B),A),
inference(paramod,[status(thm)],[c_488,c_4]) ).
cnf(c_18097,plain,
mult(mult(rd(A,A),rd(B,C)),rd(D,ld(mult(A,C),mult(A,C)))) = rd(mult(mult(A,B),D),mult(A,C)),
inference(paramod,[status(thm)],[c_33,c_596]) ).
cnf(c_18098,plain,
mult(mult(rd(A,A),rd(B,C)),rd(D,mult(ld(A,A),ld(C,C)))) = rd(mult(mult(A,B),D),mult(A,C)),
inference(paramod,[status(thm)],[c_50,c_18097]) ).
cnf(c_18099,plain,
mult(mult(rd(A,A),rd(B,C)),mult(rd(rd(D,C),ld(A,A)),C)) = rd(mult(mult(A,B),D),mult(A,C)),
inference(paramod,[status(thm)],[c_193,c_18098]) ).
cnf(c_1384,plain,
mult(A,mult(rd(B,C),ld(A,mult(rd(rd(D,C),ld(A,A)),C)))) = rd(mult(mult(A,B),D),mult(A,C)),
inference(paramod,[status(thm)],[c_14,c_18099]) ).
cnf(c_1398,plain,
mult(rd(A,B),ld(rd(C,B),rd(D,B))) = rd(mult(A,ld(C,D)),B),
inference(paramod,[status(thm)],[c_369,c_596]) ).
cnf(c_1411,plain,
ld(ld(rd(A,A),B),C) = ld(A,ld(B,mult(A,C))),
inference(paramod,[status(thm)],[c_2,c_624]) ).
cnf(c_1578,plain,
rd(mult(A,B),ld(C,C)) = rd(mult(C,B),ld(A,C)),
inference(paramod,[status(thm)],[c_2,c_639]) ).
cnf(c_18100,plain,
rd(ld(A,mult(B,C)),ld(A,A)) = rd(C,ld(ld(rd(A,A),B),A)),
inference(paramod,[status(thm)],[c_149,c_639]) ).
cnf(c_18101,plain,
ld(rd(A,A),rd(mult(B,C),A)) = rd(C,ld(ld(rd(A,A),B),A)),
inference(paramod,[status(thm)],[c_223,c_18100]) ).
cnf(c_18102,plain,
ld(rd(A,A),rd(mult(B,C),A)) = rd(C,ld(A,ld(B,mult(A,A)))),
inference(paramod,[status(thm)],[c_1411,c_18101]) ).
cnf(c_1593,plain,
rd(A,ld(B,ld(C,mult(B,B)))) = ld(rd(B,B),rd(mult(C,A),B)),
inference(copy,[status(thm)],[c_18102]) ).
cnf(c_18103,plain,
rd(mult(rd(A,A),ld(B,C)),ld(B,B)) = rd(A,ld(rd(C,A),B)),
inference(paramod,[status(thm)],[c_458,c_639]) ).
cnf(c_1600,plain,
rd(A,ld(rd(B,B),C)) = rd(B,ld(rd(A,B),C)),
inference(paramod,[status(thm)],[c_639,c_18103]) ).
cnf(c_18104,plain,
rd(mult(A,ld(B,C)),ld(B,B)) = rd(mult(A,C),ld(rd(C,C),B)),
inference(paramod,[status(thm)],[c_491,c_639]) ).
cnf(c_18105,plain,
rd(C,ld(A,B)) = rd(mult(A,C),ld(rd(C,C),B)),
inference(paramod,[status(thm)],[c_639,c_18104]) ).
cnf(c_1614,plain,
rd(mult(A,B),ld(rd(B,B),C)) = rd(B,ld(A,C)),
inference(copy,[status(thm)],[c_18105]) ).
cnf(c_18106,plain,
mult(rd(A,B),rd(C,ld(D,B))) = rd(mult(A,mult(D,ld(B,C))),B),
inference(paramod,[status(thm)],[c_639,c_596]) ).
cnf(c_1616,plain,
rd(mult(A,mult(B,ld(C,D))),C) = mult(rd(A,C),rd(D,ld(B,C))),
inference(copy,[status(thm)],[c_18106]) ).
cnf(c_18107,plain,
rd(A,ld(B,B)) = rd(mult(B,ld(C,A)),ld(C,B)),
inference(paramod,[status(thm)],[c_1,c_1578]) ).
cnf(c_1621,plain,
rd(mult(A,ld(B,C)),ld(B,A)) = rd(C,ld(A,A)),
inference(copy,[status(thm)],[c_18107]) ).
cnf(c_1628,plain,
rd(mult(rd(A,B),C),ld(A,A)) = rd(mult(A,C),B),
inference(paramod,[status(thm)],[c_11,c_1578]) ).
cnf(c_18108,plain,
mult(mult(rd(A,B),C),B) = mult(mult(A,C),mult(ld(A,A),ld(B,B))),
inference(paramod,[status(thm)],[c_676,c_19]) ).
cnf(c_18109,plain,
mult(A,mult(C,ld(B,B))) = mult(mult(A,C),mult(ld(A,A),ld(B,B))),
inference(paramod,[status(thm)],[c_19,c_18108]) ).
cnf(c_1819,plain,
mult(mult(A,B),mult(ld(A,A),ld(C,C))) = mult(A,mult(B,ld(C,C))),
inference(copy,[status(thm)],[c_18109]) ).
cnf(c_18110,plain,
ld(rd(A,A),mult(rd(B,A),C)) = ld(rd(A,ld(B,B)),mult(B,C)),
inference(paramod,[status(thm)],[c_676,c_378]) ).
cnf(c_18111,plain,
ld(rd(A,C),B) = ld(rd(A,ld(B,B)),mult(B,C)),
inference(paramod,[status(thm)],[c_378,c_18110]) ).
cnf(c_1840,plain,
ld(rd(A,ld(B,B)),mult(B,C)) = ld(rd(A,C),B),
inference(copy,[status(thm)],[c_18111]) ).
cnf(c_1867,plain,
rd(mult(A,ld(B,B)),ld(B,C)) = rd(B,ld(A,C)),
inference(paramod,[status(thm)],[c_12,c_677]) ).
cnf(c_18112,plain,
rd(mult(rd(A,A),B),C) = rd(mult(rd(A,C),B),A),
inference(paramod,[status(thm)],[c_11,c_1152]) ).
cnf(c_2715,plain,
rd(mult(rd(A,B),C),A) = rd(mult(rd(A,A),C),B),
inference(copy,[status(thm)],[c_18112]) ).
cnf(c_3022,plain,
mult(rd(A,A),ld(rd(B,ld(rd(A,A),C)),D)) = mult(rd(D,A),ld(rd(B,A),C)),
inference(paramod,[status(thm)],[c_1600,c_202]) ).
cnf(c_18113,plain,
rd(mult(A,ld(B,B)),ld(rd(ld(B,B),ld(B,C)),B)) = rd(ld(B,B),ld(A,C)),
inference(paramod,[status(thm)],[c_789,c_1614]) ).
cnf(c_18114,plain,
rd(mult(A,ld(B,B)),ld(ld(rd(B,B),rd(B,C)),B)) = rd(ld(B,B),ld(A,C)),
inference(paramod,[status(thm)],[c_223,c_18113]) ).
cnf(c_18115,plain,
rd(mult(A,ld(B,B)),ld(B,ld(rd(B,C),mult(B,B)))) = rd(ld(B,B),ld(A,C)),
inference(paramod,[status(thm)],[c_1411,c_18114]) ).
cnf(c_18116,plain,
ld(rd(B,B),rd(mult(rd(B,C),mult(A,ld(B,B))),B)) = rd(ld(B,B),ld(A,C)),
inference(paramod,[status(thm)],[c_1593,c_18115]) ).
cnf(c_18117,plain,
ld(rd(B,B),mult(rd(rd(B,C),B),rd(B,ld(A,B)))) = rd(ld(B,B),ld(A,C)),
inference(paramod,[status(thm)],[c_1616,c_18116]) ).
cnf(c_18118,plain,
ld(rd(B,B),mult(rd(rd(B,C),B),A)) = rd(ld(B,B),ld(A,C)),
inference(paramod,[status(thm)],[c_12,c_18117]) ).
cnf(c_18119,plain,
ld(rd(B,A),rd(B,C)) = rd(ld(B,B),ld(A,C)),
inference(paramod,[status(thm)],[c_378,c_18118]) ).
cnf(c_3203,plain,
rd(ld(A,A),ld(B,C)) = ld(rd(A,B),rd(A,C)),
inference(copy,[status(thm)],[c_18119]) ).
cnf(c_18120,plain,
rd(ld(A,A),B) = ld(rd(A,C),rd(A,mult(C,B))),
inference(paramod,[status(thm)],[c_2,c_3203]) ).
cnf(c_3264,plain,
ld(rd(A,B),rd(A,mult(B,C))) = rd(ld(A,A),C),
inference(copy,[status(thm)],[c_18120]) ).
cnf(c_18121,plain,
rd(ld(mult(A,B),mult(A,B)),ld(B,C)) = ld(A,rd(mult(A,B),C)),
inference(paramod,[status(thm)],[c_4,c_3203]) ).
cnf(c_18122,plain,
rd(mult(ld(A,A),ld(B,B)),ld(B,C)) = ld(A,rd(mult(A,B),C)),
inference(paramod,[status(thm)],[c_50,c_18121]) ).
cnf(c_3266,plain,
rd(A,ld(ld(B,B),C)) = ld(B,rd(mult(B,A),C)),
inference(paramod,[status(thm)],[c_1867,c_18122]) ).
cnf(c_18123,plain,
rd(ld(A,A),B) = ld(rd(A,rd(C,B)),rd(A,C)),
inference(paramod,[status(thm)],[c_11,c_3203]) ).
cnf(c_3269,plain,
ld(rd(A,rd(B,C)),rd(A,B)) = rd(ld(A,A),C),
inference(copy,[status(thm)],[c_18123]) ).
cnf(c_18124,plain,
rd(mult(mult(A,B),ld(A,C)),B) = rd(C,ld(mult(A,B),mult(A,B))),
inference(paramod,[status(thm)],[c_2,c_1621]) ).
cnf(c_18125,plain,
mult(A,rd(ld(A,C),ld(B,B))) = rd(C,ld(mult(A,B),mult(A,B))),
inference(paramod,[status(thm)],[c_244,c_18124]) ).
cnf(c_18126,plain,
mult(A,ld(rd(A,B),rd(C,B))) = rd(C,ld(mult(A,B),mult(A,B))),
inference(paramod,[status(thm)],[c_369,c_18125]) ).
cnf(c_18127,plain,
mult(A,ld(rd(A,B),rd(C,B))) = rd(C,mult(ld(A,A),ld(B,B))),
inference(paramod,[status(thm)],[c_50,c_18126]) ).
cnf(c_18128,plain,
mult(A,ld(rd(A,B),rd(C,B))) = mult(rd(rd(C,B),ld(A,A)),B),
inference(paramod,[status(thm)],[c_193,c_18127]) ).
cnf(c_3385,plain,
mult(rd(rd(A,B),ld(C,C)),B) = mult(C,ld(rd(C,B),rd(A,B))),
inference(copy,[status(thm)],[c_18128]) ).
cnf(c_18129,plain,
mult(A,mult(rd(B,C),ld(A,mult(A,ld(rd(A,C),rd(D,C)))))) = rd(mult(mult(A,B),D),mult(A,C)),
inference(paramod,[status(thm)],[c_3385,c_1384]) ).
cnf(c_18130,plain,
mult(A,mult(rd(B,C),ld(rd(A,C),rd(D,C)))) = rd(mult(mult(A,B),D),mult(A,C)),
inference(paramod,[status(thm)],[c_2,c_18129]) ).
cnf(c_18131,plain,
mult(A,rd(mult(B,ld(A,D)),C)) = rd(mult(mult(A,B),D),mult(A,C)),
inference(paramod,[status(thm)],[c_1398,c_18130]) ).
cnf(c_3503,plain,
rd(mult(mult(A,B),C),mult(A,D)) = mult(A,rd(mult(B,ld(A,C)),D)),
inference(copy,[status(thm)],[c_18131]) ).
cnf(c_18132,plain,
ld(rd(mult(A,B),C),mult(A,D)) = ld(rd(mult(rd(A,C),B),D),A),
inference(paramod,[status(thm)],[c_1628,c_1840]) ).
cnf(c_18133,plain,
mult(A,ld(rd(B,ld(A,C)),D)) = ld(rd(mult(rd(A,C),B),D),A),
inference(paramod,[status(thm)],[c_763,c_18132]) ).
cnf(c_3985,plain,
ld(rd(mult(rd(A,B),C),D),A) = mult(A,ld(rd(C,ld(A,B)),D)),
inference(copy,[status(thm)],[c_18133]) ).
cnf(c_3999,plain,
rd(mult(A,ld(B,B)),C) = rd(B,ld(A,mult(B,C))),
inference(paramod,[status(thm)],[c_2,c_1867]) ).
cnf(c_18134,plain,
ld(rd(mult(rd(A,A),B),C),mult(rd(A,A),D)) = ld(rd(mult(rd(A,C),B),D),A),
inference(paramod,[status(thm)],[c_2715,c_1106]) ).
cnf(c_18135,plain,
mult(rd(A,A),ld(rd(B,ld(rd(A,A),C)),D)) = ld(rd(mult(rd(A,C),B),D),A),
inference(paramod,[status(thm)],[c_763,c_18134]) ).
cnf(c_18136,plain,
mult(rd(D,A),ld(rd(B,A),C)) = ld(rd(mult(rd(A,C),B),D),A),
inference(paramod,[status(thm)],[c_3022,c_18135]) ).
cnf(c_4771,plain,
mult(rd(A,B),ld(rd(C,B),D)) = mult(B,ld(rd(C,ld(B,D)),A)),
inference(paramod,[status(thm)],[c_3985,c_18136]) ).
cnf(c_4888,plain,
mult(A,ld(rd(B,ld(A,rd(C,A))),D)) = rd(mult(D,ld(B,C)),A),
inference(paramod,[status(thm)],[c_4771,c_1398]) ).
cnf(c_4913,plain,
mult(rd(A,B),rd(ld(A,A),C)) = rd(A,mult(B,C)),
inference(paramod,[status(thm)],[c_3264,c_1]) ).
cnf(c_18137,plain,
mult(ld(A,rd(mult(A,B),C)),ld(C,C)) = mult(ld(A,A),ld(C,B)),
inference(paramod,[status(thm)],[c_3266,c_298]) ).
cnf(c_5209,plain,
ld(mult(A,B),mult(A,C)) = mult(ld(A,A),ld(B,C)),
inference(paramod,[status(thm)],[c_73,c_18137]) ).
cnf(c_18138,plain,
ld(rd(mult(A,B),mult(A,B)),rd(mult(mult(A,B),C),mult(A,D))) = rd(C,mult(ld(A,A),ld(B,D))),
inference(paramod,[status(thm)],[c_5209,c_128]) ).
cnf(c_18139,plain,
ld(mult(rd(A,A),rd(B,B)),rd(mult(mult(A,B),C),mult(A,D))) = rd(C,mult(ld(A,A),ld(B,D))),
inference(paramod,[status(thm)],[c_33,c_18138]) ).
cnf(c_18140,plain,
ld(mult(rd(A,A),rd(B,B)),mult(A,rd(mult(B,ld(A,C)),D))) = rd(C,mult(ld(A,A),ld(B,D))),
inference(paramod,[status(thm)],[c_3503,c_18139]) ).
cnf(c_18141,plain,
mult(A,ld(rd(B,B),ld(A,mult(A,rd(mult(B,ld(A,C)),D))))) = rd(C,mult(ld(A,A),ld(B,D))),
inference(paramod,[status(thm)],[c_107,c_18140]) ).
cnf(c_18142,plain,
mult(A,ld(rd(B,B),rd(mult(B,ld(A,C)),D))) = rd(C,mult(ld(A,A),ld(B,D))),
inference(paramod,[status(thm)],[c_2,c_18141]) ).
cnf(c_18143,plain,
mult(A,rd(ld(A,C),ld(B,D))) = rd(C,mult(ld(A,A),ld(B,D))),
inference(paramod,[status(thm)],[c_128,c_18142]) ).
cnf(c_5309,plain,
rd(A,mult(ld(B,B),ld(C,D))) = mult(B,rd(ld(B,A),ld(C,D))),
inference(copy,[status(thm)],[c_18143]) ).
cnf(c_18144,plain,
mult(rd(A,mult(ld(B,B),ld(C,D))),ld(mult(B,D),mult(B,D))) = mult(mult(B,C),ld(mult(B,D),A)),
inference(paramod,[status(thm)],[c_5209,c_298]) ).
cnf(c_18145,plain,
mult(mult(B,rd(ld(B,A),ld(C,D))),ld(mult(B,D),mult(B,D))) = mult(mult(B,C),ld(mult(B,D),A)),
inference(paramod,[status(thm)],[c_5309,c_18144]) ).
cnf(c_18146,plain,
mult(mult(B,rd(ld(B,A),ld(C,D))),mult(ld(B,B),ld(D,D))) = mult(mult(B,C),ld(mult(B,D),A)),
inference(paramod,[status(thm)],[c_5209,c_18145]) ).
cnf(c_18147,plain,
mult(B,mult(rd(ld(B,A),ld(C,D)),ld(D,D))) = mult(mult(B,C),ld(mult(B,D),A)),
inference(paramod,[status(thm)],[c_1819,c_18146]) ).
cnf(c_18148,plain,
mult(B,mult(C,ld(D,ld(B,A)))) = mult(mult(B,C),ld(mult(B,D),A)),
inference(paramod,[status(thm)],[c_298,c_18147]) ).
cnf(c_5323,plain,
mult(mult(A,B),ld(mult(A,C),D)) = mult(A,mult(B,ld(C,ld(A,D)))),
inference(copy,[status(thm)],[c_18148]) ).
cnf(c_18149,plain,
mult(rd(ld(A,A),B),ld(rd(C,B),rd(C,B))) = ld(A,mult(rd(A,C),rd(C,B))),
inference(paramod,[status(thm)],[c_3269,c_72]) ).
cnf(c_18150,plain,
mult(B,ld(rd(C,ld(B,rd(C,B))),ld(A,A))) = ld(A,mult(rd(A,C),rd(C,B))),
inference(paramod,[status(thm)],[c_4771,c_18149]) ).
cnf(c_18151,plain,
rd(mult(ld(A,A),ld(C,C)),B) = ld(A,mult(rd(A,C),rd(C,B))),
inference(paramod,[status(thm)],[c_4888,c_18150]) ).
cnf(c_18152,plain,
rd(C,ld(ld(A,A),mult(C,B))) = ld(A,mult(rd(A,C),rd(C,B))),
inference(paramod,[status(thm)],[c_3999,c_18151]) ).
cnf(c_5410,plain,
ld(A,rd(mult(A,B),mult(B,C))) = ld(A,mult(rd(A,B),rd(B,C))),
inference(paramod,[status(thm)],[c_3266,c_18152]) ).
cnf(c_18153,plain,
mult(A,rd(ld(mult(A,B),mult(A,B)),C)) = rd(mult(A,B),mult(B,C)),
inference(paramod,[status(thm)],[c_4,c_4913]) ).
cnf(c_18154,plain,
mult(A,rd(mult(ld(A,A),ld(B,B)),C)) = rd(mult(A,B),mult(B,C)),
inference(paramod,[status(thm)],[c_5209,c_18153]) ).
cnf(c_18155,plain,
mult(A,rd(B,ld(ld(A,A),mult(B,C)))) = rd(mult(A,B),mult(B,C)),
inference(paramod,[status(thm)],[c_3999,c_18154]) ).
cnf(c_18156,plain,
mult(A,ld(A,rd(mult(A,B),mult(B,C)))) = rd(mult(A,B),mult(B,C)),
inference(paramod,[status(thm)],[c_3266,c_18155]) ).
cnf(c_18157,plain,
mult(A,ld(A,mult(rd(A,B),rd(B,C)))) = rd(mult(A,B),mult(B,C)),
inference(paramod,[status(thm)],[c_5410,c_18156]) ).
cnf(c_18158,plain,
mult(rd(A,B),rd(B,C)) = rd(mult(A,B),mult(B,C)),
inference(paramod,[status(thm)],[c_1,c_18157]) ).
cnf(c_6714,plain,
rd(mult(A,B),mult(B,C)) = mult(rd(A,B),rd(B,C)),
inference(copy,[status(thm)],[c_18158]) ).
cnf(c_18159,plain,
mult(ld(mult(rd(A,A),rd(A,A)),B),ld(mult(A,A),C)) = ld(mult(A,A),mult(B,C)),
inference(paramod,[status(thm)],[c_6714,c_149]) ).
cnf(c_18160,plain,
mult(mult(A,ld(rd(A,A),ld(A,B))),ld(mult(A,A),C)) = ld(mult(A,A),mult(B,C)),
inference(paramod,[status(thm)],[c_107,c_18159]) ).
cnf(c_18161,plain,
mult(A,mult(ld(rd(A,A),ld(A,B)),ld(A,ld(A,C)))) = ld(mult(A,A),mult(B,C)),
inference(paramod,[status(thm)],[c_5323,c_18160]) ).
cnf(c_18162,plain,
mult(A,ld(A,mult(ld(A,B),ld(A,C)))) = ld(mult(A,A),mult(B,C)),
inference(paramod,[status(thm)],[c_149,c_18161]) ).
cnf(c_18163,plain,
mult(ld(A,B),ld(A,C)) = ld(mult(A,A),mult(B,C)),
inference(paramod,[status(thm)],[c_1,c_18162]) ).
cnf(c_6835,plain,
ld(mult(A,A),mult(B,C)) = mult(ld(A,B),ld(A,C)),
inference(copy,[status(thm)],[c_18163]) ).
cnf(c_7061,plain,
mult(mult(A,A),mult(ld(A,B),ld(A,C))) = mult(B,C),
inference(paramod,[status(thm)],[c_6835,c_1]) ).
cnf(c_10417,plain,
mult(mult(A,A),mult(B,ld(A,C))) = mult(mult(A,B),C),
inference(paramod,[status(thm)],[c_2,c_7061]) ).
cnf(c_18164,plain,
mult(mult(A,A),mult(B,C)) = mult(mult(A,B),mult(A,C)),
inference(paramod,[status(thm)],[c_2,c_10417]) ).
cnf(c_18071,plain,
mult(mult(A,B),mult(A,C)) = mult(mult(A,A),mult(B,C)),
inference(copy,[status(thm)],[c_18164]) ).
cnf(c_18072,plain,
$false,
inference(resolve,[status(thm)],[c_18071,c_10]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP754-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.11/0.43 % Computer : n003.cluster.edu
% 0.11/0.43 % Model : x86_64 x86_64
% 0.11/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.43 % Memory : 8046.5625MB
% 0.11/0.43 % OS : Linux 6.8.0-71-generic
% 0.11/0.43 % CPULimit : 300
% 0.11/0.43 % WCLimit : 300
% 0.11/0.43 % DateTime : Fri Sep 25 15:45:37 UTC 2026
% 0.11/0.43 % CPUTime :
% 0.11/0.43 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.11/0.43 % Process 567448 was started by sandbox on n003,
% 0.11/0.43 % Fri Sep 25 15:45:37 2026
% 0.11/0.43 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.11/0.44
% 0.11/0.44 % From the command line: assign(max_seconds, 300).
% 110.67/21.10
% 110.67/21.10 % SZS status Unsatisfiable for theBenchmark
% 110.67/21.10
% 110.67/21.10 % Proof 1 at 3.80 (+ 0.68) seconds.
% 110.67/21.10 % Length of proof is 92.
% 110.67/21.10 % Level of proof is 20.
% 110.67/21.10 % Maximum clause weight is 62.000.
% 110.67/21.10 % Given clauses 191.
% 110.67/21.10
% 110.67/21.10 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------