%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP727-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:20 AM UTC 2026
% Result : Unsatisfiable 214.80s 28.67s
% Output : CNFRefutation 214.80s
% Verified :
% SZS Type : Refutation
% Derivation depth : 68
% Number of leaves : 12
% Syntax : Number of formulae : 198 ( 198 unt; 0 def)
% Number of atoms : 198 ( 197 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 2 ( 2 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 1 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 6 con; 0-3 aty)
% Number of variables : 600 ( 27 sgn 23 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(c01,axiom,
! [VAR_0] : mult(unit,VAR_0) = VAR_0,
file('theBenchmark.p',c01) ).
cnf(c_1,plain,
mult(unit,A) = A,
inference(clausify,[status(thm)],[c01]) ).
fof(c02,axiom,
! [VAR_0] : mult(VAR_0,unit) = VAR_0,
file('theBenchmark.p',c02) ).
cnf(c_2,plain,
mult(A,unit) = A,
inference(clausify,[status(thm)],[c02]) ).
fof(c03,axiom,
! [VAR_0] : mult(VAR_0,i(VAR_0)) = unit,
file('theBenchmark.p',c03) ).
cnf(c_3,plain,
mult(A,i(A)) = unit,
inference(clausify,[status(thm)],[c03]) ).
fof(c04,axiom,
! [VAR_0] : mult(i(VAR_0),VAR_0) = unit,
file('theBenchmark.p',c04) ).
cnf(c_4,plain,
mult(i(A),A) = unit,
inference(clausify,[status(thm)],[c04]) ).
fof(c05,axiom,
! [VAR_0,VAR_1] : i(mult(VAR_0,VAR_1)) = mult(i(VAR_0),i(VAR_1)),
file('theBenchmark.p',c05) ).
cnf(c_5,plain,
i(mult(A,B)) = mult(i(A),i(B)),
inference(clausify,[status(thm)],[c05]) ).
fof(c06,axiom,
! [VAR_0,VAR_1] : mult(i(VAR_0),mult(VAR_0,VAR_1)) = VAR_1,
file('theBenchmark.p',c06) ).
cnf(c_6,plain,
mult(i(A),mult(A,B)) = B,
inference(clausify,[status(thm)],[c06]) ).
fof(c07,axiom,
! [VAR_0,VAR_1] : rd(mult(VAR_0,VAR_1),VAR_1) = VAR_0,
file('theBenchmark.p',c07) ).
cnf(c_7,plain,
rd(mult(A,B),B) = A,
inference(clausify,[status(thm)],[c07]) ).
fof(c08,axiom,
! [VAR_0,VAR_1] : mult(rd(VAR_0,VAR_1),VAR_1) = VAR_0,
file('theBenchmark.p',c08) ).
cnf(c_8,plain,
mult(rd(A,B),B) = A,
inference(clausify,[status(thm)],[c08]) ).
fof(c09,axiom,
! [VAR_0,VAR_1,VAR_2] : mult(mult(VAR_0,mult(VAR_1,VAR_0)),VAR_2) = mult(VAR_0,mult(VAR_1,mult(VAR_0,VAR_2))),
file('theBenchmark.p',c09) ).
cnf(c_9,plain,
mult(mult(A,mult(B,A)),C) = mult(A,mult(B,mult(A,C))),
inference(clausify,[status(thm)],[c09]) ).
fof(c10,axiom,
! [VAR_0,VAR_1,VAR_2] : mult(mult(VAR_0,VAR_1),VAR_2) = mult(mult(VAR_0,mult(VAR_1,VAR_2)),asoc(VAR_0,VAR_1,VAR_2)),
file('theBenchmark.p',c10) ).
cnf(c_10,plain,
mult(mult(A,B),C) = mult(mult(A,mult(B,C)),asoc(A,B,C)),
inference(clausify,[status(thm)],[c10]) ).
cnf(c_11,plain,
mult(mult(A,mult(B,C)),asoc(A,B,C)) = mult(mult(A,B),C),
inference(copy,[status(thm)],[c_10]) ).
fof(c20,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4] : asoc(asoc(VAR_0,VAR_1,VAR_2),VAR_3,VAR_4) = unit,
file('theBenchmark.p',c20) ).
cnf(c_28,plain,
asoc(asoc(A,B,C),D,E) = unit,
inference(clausify,[status(thm)],[c20]) ).
fof(goals,axiom,
asoc(a,b,asoc(c,d,e)) != unit,
file('theBenchmark.p',goals) ).
cnf(c_29,plain,
asoc(a,b,asoc(c,d,e)) != unit,
inference(clausify,[status(thm)],[goals]) ).
cnf(c_9550,plain,
mult(i(i(A)),unit) = A,
inference(paramod,[status(thm)],[c_4,c_6]) ).
cnf(c_33,plain,
i(i(A)) = A,
inference(paramod,[status(thm)],[c_2,c_9550]) ).
cnf(c_35,plain,
mult(mult(i(A),i(B)),mult(mult(A,B),C)) = C,
inference(paramod,[status(thm)],[c_5,c_6]) ).
cnf(c_40,plain,
rd(A,mult(B,A)) = i(B),
inference(paramod,[status(thm)],[c_6,c_7]) ).
cnf(c_9551,plain,
i(A) = mult(i(rd(A,B)),i(B)),
inference(paramod,[status(thm)],[c_8,c_5]) ).
cnf(c_41,plain,
mult(i(rd(A,B)),i(B)) = i(A),
inference(copy,[status(thm)],[c_9551]) ).
cnf(c_46,plain,
rd(mult(A,mult(B,mult(A,C))),C) = mult(A,mult(B,A)),
inference(paramod,[status(thm)],[c_9,c_7]) ).
cnf(c_9552,plain,
mult(mult(A,B),C) = mult(A,mult(rd(B,A),mult(A,C))),
inference(paramod,[status(thm)],[c_8,c_9]) ).
cnf(c_47,plain,
mult(A,mult(rd(B,A),mult(A,C))) = mult(mult(A,B),C),
inference(copy,[status(thm)],[c_9552]) ).
cnf(c_9553,plain,
mult(mult(A,unit),asoc(A,B,i(B))) = mult(mult(A,B),i(B)),
inference(paramod,[status(thm)],[c_3,c_11]) ).
cnf(c_53,plain,
mult(A,asoc(A,B,i(B))) = mult(mult(A,B),i(B)),
inference(paramod,[status(thm)],[c_2,c_9553]) ).
cnf(c_9554,plain,
mult(mult(A,unit),asoc(A,i(B),B)) = mult(mult(A,i(B)),B),
inference(paramod,[status(thm)],[c_4,c_11]) ).
cnf(c_54,plain,
mult(A,asoc(A,i(B),B)) = mult(mult(A,i(B)),B),
inference(paramod,[status(thm)],[c_2,c_9554]) ).
cnf(c_9555,plain,
i(mult(mult(A,B),C)) = mult(i(mult(A,mult(B,C))),i(asoc(A,B,C))),
inference(paramod,[status(thm)],[c_11,c_5]) ).
cnf(c_9556,plain,
mult(i(mult(A,B)),i(C)) = mult(i(mult(A,mult(B,C))),i(asoc(A,B,C))),
inference(paramod,[status(thm)],[c_5,c_9555]) ).
cnf(c_9557,plain,
mult(mult(i(A),i(B)),i(C)) = mult(i(mult(A,mult(B,C))),i(asoc(A,B,C))),
inference(paramod,[status(thm)],[c_5,c_9556]) ).
cnf(c_9558,plain,
mult(mult(i(A),i(B)),i(C)) = mult(mult(i(A),i(mult(B,C))),i(asoc(A,B,C))),
inference(paramod,[status(thm)],[c_5,c_9557]) ).
cnf(c_9559,plain,
mult(mult(i(A),i(B)),i(C)) = mult(mult(i(A),mult(i(B),i(C))),i(asoc(A,B,C))),
inference(paramod,[status(thm)],[c_5,c_9558]) ).
cnf(c_57,plain,
mult(mult(i(A),mult(i(B),i(C))),i(asoc(A,B,C))) = mult(mult(i(A),i(B)),i(C)),
inference(copy,[status(thm)],[c_9559]) ).
cnf(c_9560,plain,
mult(i(mult(A,mult(B,C))),mult(mult(A,B),C)) = asoc(A,B,C),
inference(paramod,[status(thm)],[c_11,c_6]) ).
cnf(c_9561,plain,
mult(mult(i(A),i(mult(B,C))),mult(mult(A,B),C)) = asoc(A,B,C),
inference(paramod,[status(thm)],[c_5,c_9560]) ).
cnf(c_58,plain,
mult(mult(i(A),mult(i(B),i(C))),mult(mult(A,B),C)) = asoc(A,B,C),
inference(paramod,[status(thm)],[c_5,c_9561]) ).
cnf(c_61,plain,
mult(mult(A,B),asoc(A,rd(B,C),C)) = mult(mult(A,rd(B,C)),C),
inference(paramod,[status(thm)],[c_8,c_11]) ).
cnf(c_9562,plain,
mult(mult(asoc(A,B,C),mult(mult(A,B),C)),D) = mult(asoc(A,B,C),mult(mult(A,mult(B,C)),mult(asoc(A,B,C),D))),
inference(paramod,[status(thm)],[c_11,c_9]) ).
cnf(c_63,plain,
mult(asoc(A,B,C),mult(mult(A,mult(B,C)),mult(asoc(A,B,C),D))) = mult(mult(asoc(A,B,C),mult(mult(A,B),C)),D),
inference(copy,[status(thm)],[c_9562]) ).
cnf(c_9563,plain,
mult(mult(asoc(A,B,C),mult(D,E)),unit) = mult(mult(asoc(A,B,C),D),E),
inference(paramod,[status(thm)],[c_28,c_11]) ).
cnf(c_9564,plain,
mult(asoc(A,B,C),mult(D,E)) = mult(mult(asoc(A,B,C),D),E),
inference(paramod,[status(thm)],[c_2,c_9563]) ).
cnf(c_150,plain,
mult(mult(asoc(A,B,C),D),E) = mult(asoc(A,B,C),mult(D,E)),
inference(copy,[status(thm)],[c_9564]) ).
cnf(c_152,plain,
mult(asoc(A,B,C),mult(mult(A,mult(B,C)),mult(asoc(A,B,C),D))) = mult(asoc(A,B,C),mult(mult(mult(A,B),C),D)),
inference(paramod,[status(thm)],[c_150,c_63]) ).
cnf(c_9565,plain,
rd(A,B) = i(rd(B,A)),
inference(paramod,[status(thm)],[c_8,c_40]) ).
cnf(c_179,plain,
i(rd(A,B)) = rd(B,A),
inference(copy,[status(thm)],[c_9565]) ).
cnf(c_188,plain,
mult(rd(A,B),i(A)) = i(B),
inference(paramod,[status(thm)],[c_179,c_41]) ).
cnf(c_203,plain,
rd(i(A),i(B)) = rd(B,A),
inference(paramod,[status(thm)],[c_188,c_7]) ).
cnf(c_234,plain,
rd(i(A),mult(i(B),i(C))) = rd(mult(B,C),A),
inference(paramod,[status(thm)],[c_5,c_203]) ).
cnf(c_238,plain,
rd(A,i(B)) = rd(B,i(A)),
inference(paramod,[status(thm)],[c_33,c_203]) ).
cnf(c_9566,plain,
rd(mult(A,mult(B,unit)),i(A)) = mult(A,mult(B,A)),
inference(paramod,[status(thm)],[c_3,c_46]) ).
cnf(c_9567,plain,
rd(mult(A,B),i(A)) = mult(A,mult(B,A)),
inference(paramod,[status(thm)],[c_2,c_9566]) ).
cnf(c_9568,plain,
rd(A,i(mult(A,B))) = mult(A,mult(B,A)),
inference(paramod,[status(thm)],[c_238,c_9567]) ).
cnf(c_454,plain,
rd(A,mult(i(A),i(B))) = mult(A,mult(B,A)),
inference(paramod,[status(thm)],[c_5,c_9568]) ).
cnf(c_9569,plain,
mult(A,mult(rd(B,A),unit)) = mult(mult(A,B),i(A)),
inference(paramod,[status(thm)],[c_3,c_47]) ).
cnf(c_9570,plain,
mult(A,rd(B,A)) = mult(mult(A,B),i(A)),
inference(paramod,[status(thm)],[c_2,c_9569]) ).
cnf(c_500,plain,
mult(mult(A,B),i(A)) = mult(A,rd(B,A)),
inference(copy,[status(thm)],[c_9570]) ).
cnf(c_9571,plain,
mult(i(A),mult(mult(A,B),C)) = mult(rd(B,A),mult(A,C)),
inference(paramod,[status(thm)],[c_47,c_6]) ).
cnf(c_502,plain,
mult(rd(A,B),mult(B,C)) = mult(i(B),mult(mult(B,A),C)),
inference(copy,[status(thm)],[c_9571]) ).
cnf(c_9572,plain,
mult(i(A),mult(rd(B,i(A)),C)) = mult(mult(i(A),B),mult(A,C)),
inference(paramod,[status(thm)],[c_6,c_47]) ).
cnf(c_503,plain,
mult(mult(i(A),B),mult(A,C)) = mult(i(A),mult(rd(B,i(A)),C)),
inference(copy,[status(thm)],[c_9572]) ).
cnf(c_9573,plain,
mult(mult(A,B),i(A)) = mult(A,rd(i(A),i(B))),
inference(paramod,[status(thm)],[c_203,c_500]) ).
cnf(c_9574,plain,
mult(A,rd(B,A)) = mult(A,rd(i(A),i(B))),
inference(paramod,[status(thm)],[c_500,c_9573]) ).
cnf(c_626,plain,
mult(A,rd(i(A),i(B))) = mult(A,rd(B,A)),
inference(copy,[status(thm)],[c_9574]) ).
cnf(c_782,plain,
mult(i(A),mult(mult(A,B),i(B))) = asoc(A,B,i(B)),
inference(paramod,[status(thm)],[c_53,c_6]) ).
cnf(c_9575,plain,
mult(i(mult(i(A),mult(i(B),i(C)))),mult(mult(i(A),i(B)),i(C))) = i(asoc(A,B,C)),
inference(paramod,[status(thm)],[c_57,c_6]) ).
cnf(c_9576,plain,
mult(mult(i(i(A)),i(mult(i(B),i(C)))),mult(mult(i(A),i(B)),i(C))) = i(asoc(A,B,C)),
inference(paramod,[status(thm)],[c_5,c_9575]) ).
cnf(c_9577,plain,
mult(mult(A,i(mult(i(B),i(C)))),mult(mult(i(A),i(B)),i(C))) = i(asoc(A,B,C)),
inference(paramod,[status(thm)],[c_33,c_9576]) ).
cnf(c_9578,plain,
mult(mult(A,mult(i(i(B)),i(i(C)))),mult(mult(i(A),i(B)),i(C))) = i(asoc(A,B,C)),
inference(paramod,[status(thm)],[c_5,c_9577]) ).
cnf(c_9579,plain,
mult(mult(A,mult(B,i(i(C)))),mult(mult(i(A),i(B)),i(C))) = i(asoc(A,B,C)),
inference(paramod,[status(thm)],[c_33,c_9578]) ).
cnf(c_1132,plain,
mult(mult(A,mult(B,C)),mult(mult(i(A),i(B)),i(C))) = i(asoc(A,B,C)),
inference(paramod,[status(thm)],[c_33,c_9579]) ).
cnf(c_9580,plain,
mult(mult(i(mult(A,B)),mult(i(i(A)),i(C))),mult(mult(A,rd(B,A)),C)) = asoc(mult(A,B),i(A),C),
inference(paramod,[status(thm)],[c_500,c_58]) ).
cnf(c_9581,plain,
mult(mult(mult(i(A),i(B)),mult(i(i(A)),i(C))),mult(mult(A,rd(B,A)),C)) = asoc(mult(A,B),i(A),C),
inference(paramod,[status(thm)],[c_5,c_9580]) ).
cnf(c_9582,plain,
mult(mult(mult(i(A),i(B)),mult(A,i(C))),mult(mult(A,rd(B,A)),C)) = asoc(mult(A,B),i(A),C),
inference(paramod,[status(thm)],[c_33,c_9581]) ).
cnf(c_1343,plain,
mult(mult(i(A),mult(rd(i(B),i(A)),i(C))),mult(mult(A,rd(B,A)),C)) = asoc(mult(A,B),i(A),C),
inference(paramod,[status(thm)],[c_503,c_9582]) ).
cnf(c_9583,plain,
mult(mult(i(A),mult(i(rd(i(A),i(B))),i(C))),mult(mult(A,rd(B,A)),C)) = asoc(A,rd(i(A),i(B)),C),
inference(paramod,[status(thm)],[c_626,c_58]) ).
cnf(c_9584,plain,
mult(mult(i(A),mult(rd(i(B),i(A)),i(C))),mult(mult(A,rd(B,A)),C)) = asoc(A,rd(i(A),i(B)),C),
inference(paramod,[status(thm)],[c_179,c_9583]) ).
cnf(c_1356,plain,
asoc(mult(A,B),i(A),C) = asoc(A,rd(i(A),i(B)),C),
inference(paramod,[status(thm)],[c_1343,c_9584]) ).
cnf(c_9585,plain,
rd(i(A),mult(i(mult(i(B),mult(i(C),i(D)))),i(mult(mult(B,C),D)))) = rd(asoc(B,C,D),A),
inference(paramod,[status(thm)],[c_58,c_234]) ).
cnf(c_9586,plain,
rd(i(A),mult(mult(i(i(B)),i(mult(i(C),i(D)))),i(mult(mult(B,C),D)))) = rd(asoc(B,C,D),A),
inference(paramod,[status(thm)],[c_5,c_9585]) ).
cnf(c_9587,plain,
rd(i(A),mult(mult(B,i(mult(i(C),i(D)))),i(mult(mult(B,C),D)))) = rd(asoc(B,C,D),A),
inference(paramod,[status(thm)],[c_33,c_9586]) ).
cnf(c_9588,plain,
rd(i(A),mult(mult(B,mult(i(i(C)),i(i(D)))),i(mult(mult(B,C),D)))) = rd(asoc(B,C,D),A),
inference(paramod,[status(thm)],[c_5,c_9587]) ).
cnf(c_9589,plain,
rd(i(A),mult(mult(B,mult(C,i(i(D)))),i(mult(mult(B,C),D)))) = rd(asoc(B,C,D),A),
inference(paramod,[status(thm)],[c_33,c_9588]) ).
cnf(c_9590,plain,
rd(i(A),mult(mult(B,mult(C,D)),i(mult(mult(B,C),D)))) = rd(asoc(B,C,D),A),
inference(paramod,[status(thm)],[c_33,c_9589]) ).
cnf(c_9591,plain,
rd(i(A),mult(mult(B,mult(C,D)),mult(i(mult(B,C)),i(D)))) = rd(asoc(B,C,D),A),
inference(paramod,[status(thm)],[c_5,c_9590]) ).
cnf(c_9592,plain,
rd(i(A),mult(mult(B,mult(C,D)),mult(mult(i(B),i(C)),i(D)))) = rd(asoc(B,C,D),A),
inference(paramod,[status(thm)],[c_5,c_9591]) ).
cnf(c_9593,plain,
rd(i(A),i(asoc(B,C,D))) = rd(asoc(B,C,D),A),
inference(paramod,[status(thm)],[c_1132,c_9592]) ).
cnf(c_1367,plain,
rd(asoc(A,B,C),D) = rd(i(D),i(asoc(A,B,C))),
inference(copy,[status(thm)],[c_9593]) ).
cnf(c_1817,plain,
rd(A,mult(i(A),B)) = mult(A,mult(i(B),A)),
inference(paramod,[status(thm)],[c_33,c_454]) ).
cnf(c_9594,plain,
asoc(A,i(i(B)),C) = asoc(i(B),rd(i(i(B)),i(mult(B,A))),C),
inference(paramod,[status(thm)],[c_6,c_1356]) ).
cnf(c_9595,plain,
asoc(A,B,C) = asoc(i(B),rd(i(i(B)),i(mult(B,A))),C),
inference(paramod,[status(thm)],[c_33,c_9594]) ).
cnf(c_9596,plain,
asoc(A,B,C) = asoc(i(B),rd(B,i(mult(B,A))),C),
inference(paramod,[status(thm)],[c_33,c_9595]) ).
cnf(c_9597,plain,
asoc(A,B,C) = asoc(i(B),rd(B,mult(i(B),i(A))),C),
inference(paramod,[status(thm)],[c_5,c_9596]) ).
cnf(c_9598,plain,
asoc(A,B,C) = asoc(i(B),mult(B,mult(i(i(A)),B)),C),
inference(paramod,[status(thm)],[c_1817,c_9597]) ).
cnf(c_9599,plain,
asoc(A,B,C) = asoc(i(B),mult(B,mult(A,B)),C),
inference(paramod,[status(thm)],[c_33,c_9598]) ).
cnf(c_2296,plain,
asoc(i(A),mult(A,mult(B,A)),C) = asoc(B,A,C),
inference(copy,[status(thm)],[c_9599]) ).
cnf(c_9600,plain,
asoc(i(A),mult(A,B),C) = asoc(rd(B,A),A,C),
inference(paramod,[status(thm)],[c_8,c_2296]) ).
cnf(c_2503,plain,
asoc(rd(A,B),B,C) = asoc(i(B),mult(B,A),C),
inference(copy,[status(thm)],[c_9600]) ).
cnf(c_9601,plain,
mult(rd(A,B),asoc(i(B),mult(B,A),i(B))) = mult(mult(rd(A,B),B),i(B)),
inference(paramod,[status(thm)],[c_2503,c_53]) ).
cnf(c_2626,plain,
mult(rd(A,B),asoc(i(B),mult(B,A),i(B))) = mult(A,i(B)),
inference(paramod,[status(thm)],[c_8,c_9601]) ).
cnf(c_9602,plain,
mult(rd(A,i(B)),asoc(i(i(B)),mult(i(B),A),B)) = mult(mult(rd(A,i(B)),i(B)),B),
inference(paramod,[status(thm)],[c_2503,c_54]) ).
cnf(c_9603,plain,
mult(rd(A,i(B)),asoc(B,mult(i(B),A),B)) = mult(mult(rd(A,i(B)),i(B)),B),
inference(paramod,[status(thm)],[c_33,c_9602]) ).
cnf(c_2629,plain,
mult(rd(A,i(B)),asoc(B,mult(i(B),A),B)) = mult(A,B),
inference(paramod,[status(thm)],[c_8,c_9603]) ).
cnf(c_9604,plain,
mult(i(rd(A,B)),mult(A,i(B))) = asoc(i(B),mult(B,A),i(B)),
inference(paramod,[status(thm)],[c_2626,c_6]) ).
cnf(c_9605,plain,
mult(rd(B,A),mult(A,i(B))) = asoc(i(B),mult(B,A),i(B)),
inference(paramod,[status(thm)],[c_179,c_9604]) ).
cnf(c_9606,plain,
mult(i(A),mult(mult(A,B),i(B))) = asoc(i(B),mult(B,A),i(B)),
inference(paramod,[status(thm)],[c_502,c_9605]) ).
cnf(c_9607,plain,
asoc(A,B,i(B)) = asoc(i(B),mult(B,A),i(B)),
inference(paramod,[status(thm)],[c_782,c_9606]) ).
cnf(c_4608,plain,
asoc(i(A),mult(A,B),i(A)) = asoc(B,A,i(A)),
inference(copy,[status(thm)],[c_9607]) ).
cnf(c_9608,plain,
mult(rd(i(A),i(asoc(B,C,D))),asoc(i(A),mult(A,asoc(B,C,D)),i(A))) = mult(asoc(B,C,D),i(A)),
inference(paramod,[status(thm)],[c_1367,c_2626]) ).
cnf(c_9609,plain,
mult(rd(i(A),i(asoc(B,C,D))),asoc(asoc(B,C,D),A,i(A))) = mult(asoc(B,C,D),i(A)),
inference(paramod,[status(thm)],[c_4608,c_9608]) ).
cnf(c_9610,plain,
mult(rd(i(A),i(asoc(B,C,D))),unit) = mult(asoc(B,C,D),i(A)),
inference(paramod,[status(thm)],[c_28,c_9609]) ).
cnf(c_4704,plain,
rd(i(A),i(asoc(B,C,D))) = mult(asoc(B,C,D),i(A)),
inference(paramod,[status(thm)],[c_2,c_9610]) ).
cnf(c_9611,plain,
mult(rd(asoc(A,B,C),D),asoc(i(i(asoc(A,B,C))),mult(i(asoc(A,B,C)),i(D)),i(i(asoc(A,B,C))))) = mult(i(D),i(i(asoc(A,B,C)))),
inference(paramod,[status(thm)],[c_1367,c_2626]) ).
cnf(c_9612,plain,
mult(rd(asoc(A,B,C),D),asoc(asoc(A,B,C),mult(i(asoc(A,B,C)),i(D)),i(i(asoc(A,B,C))))) = mult(i(D),i(i(asoc(A,B,C)))),
inference(paramod,[status(thm)],[c_33,c_9611]) ).
cnf(c_9613,plain,
mult(rd(asoc(A,B,C),D),asoc(asoc(A,B,C),mult(i(asoc(A,B,C)),i(D)),asoc(A,B,C))) = mult(i(D),i(i(asoc(A,B,C)))),
inference(paramod,[status(thm)],[c_33,c_9612]) ).
cnf(c_9614,plain,
mult(rd(asoc(A,B,C),D),unit) = mult(i(D),i(i(asoc(A,B,C)))),
inference(paramod,[status(thm)],[c_28,c_9613]) ).
cnf(c_9615,plain,
rd(asoc(A,B,C),D) = mult(i(D),i(i(asoc(A,B,C)))),
inference(paramod,[status(thm)],[c_2,c_9614]) ).
cnf(c_4705,plain,
rd(asoc(A,B,C),D) = mult(i(D),asoc(A,B,C)),
inference(paramod,[status(thm)],[c_33,c_9615]) ).
cnf(c_4750,plain,
mult(rd(A,B),asoc(A,B,i(B))) = mult(A,i(B)),
inference(paramod,[status(thm)],[c_4608,c_2626]) ).
cnf(c_9616,plain,
mult(i(D),asoc(A,B,C)) = rd(i(D),i(asoc(A,B,C))),
inference(paramod,[status(thm)],[c_4705,c_1367]) ).
cnf(c_9617,plain,
mult(i(D),asoc(A,B,C)) = mult(asoc(A,B,C),i(D)),
inference(paramod,[status(thm)],[c_4704,c_9616]) ).
cnf(c_4775,plain,
mult(asoc(A,B,C),i(D)) = mult(i(D),asoc(A,B,C)),
inference(copy,[status(thm)],[c_9617]) ).
cnf(c_9618,plain,
asoc(A,mult(i(A),B),i(i(A))) = asoc(B,i(A),i(i(A))),
inference(paramod,[status(thm)],[c_33,c_4608]) ).
cnf(c_9619,plain,
asoc(A,mult(i(A),B),A) = asoc(B,i(A),i(i(A))),
inference(paramod,[status(thm)],[c_33,c_9618]) ).
cnf(c_4819,plain,
asoc(A,mult(i(A),B),A) = asoc(B,i(A),A),
inference(paramod,[status(thm)],[c_33,c_9619]) ).
cnf(c_4850,plain,
asoc(mult(A,B),B,i(B)) = asoc(A,B,i(B)),
inference(paramod,[status(thm)],[c_4608,c_2296]) ).
cnf(c_4876,plain,
mult(rd(A,i(B)),asoc(A,i(B),B)) = mult(A,B),
inference(paramod,[status(thm)],[c_4819,c_2629]) ).
cnf(c_9620,plain,
asoc(asoc(A,B,C),mult(mult(A,B),C),i(mult(mult(A,B),C))) = asoc(mult(i(A),mult(i(B),i(C))),mult(mult(A,B),C),i(mult(mult(A,B),C))),
inference(paramod,[status(thm)],[c_58,c_4850]) ).
cnf(c_9621,plain,
asoc(asoc(A,B,C),mult(mult(A,B),C),mult(i(mult(A,B)),i(C))) = asoc(mult(i(A),mult(i(B),i(C))),mult(mult(A,B),C),i(mult(mult(A,B),C))),
inference(paramod,[status(thm)],[c_5,c_9620]) ).
cnf(c_9622,plain,
asoc(asoc(A,B,C),mult(mult(A,B),C),mult(mult(i(A),i(B)),i(C))) = asoc(mult(i(A),mult(i(B),i(C))),mult(mult(A,B),C),i(mult(mult(A,B),C))),
inference(paramod,[status(thm)],[c_5,c_9621]) ).
cnf(c_9623,plain,
unit = asoc(mult(i(A),mult(i(B),i(C))),mult(mult(A,B),C),i(mult(mult(A,B),C))),
inference(paramod,[status(thm)],[c_28,c_9622]) ).
cnf(c_9624,plain,
unit = asoc(mult(i(A),mult(i(B),i(C))),mult(mult(A,B),C),mult(i(mult(A,B)),i(C))),
inference(paramod,[status(thm)],[c_5,c_9623]) ).
cnf(c_9625,plain,
unit = asoc(mult(i(A),mult(i(B),i(C))),mult(mult(A,B),C),mult(mult(i(A),i(B)),i(C))),
inference(paramod,[status(thm)],[c_5,c_9624]) ).
cnf(c_4992,plain,
asoc(mult(i(A),mult(i(B),i(C))),mult(mult(A,B),C),mult(mult(i(A),i(B)),i(C))) = unit,
inference(copy,[status(thm)],[c_9625]) ).
cnf(c_9626,plain,
mult(asoc(A,B,C),D) = mult(i(i(D)),asoc(A,B,C)),
inference(paramod,[status(thm)],[c_33,c_4775]) ).
cnf(c_5163,plain,
mult(asoc(A,B,C),D) = mult(D,asoc(A,B,C)),
inference(paramod,[status(thm)],[c_33,c_9626]) ).
cnf(c_5278,plain,
rd(mult(A,asoc(B,C,D)),A) = asoc(B,C,D),
inference(paramod,[status(thm)],[c_5163,c_7]) ).
cnf(c_9627,plain,
mult(mult(asoc(A,B,C),mult(D,E)),asoc(asoc(A,B,C),D,E)) = mult(mult(D,asoc(A,B,C)),E),
inference(paramod,[status(thm)],[c_5163,c_11]) ).
cnf(c_9628,plain,
mult(mult(asoc(A,B,C),mult(D,E)),unit) = mult(mult(D,asoc(A,B,C)),E),
inference(paramod,[status(thm)],[c_28,c_9627]) ).
cnf(c_9629,plain,
mult(asoc(A,B,C),mult(D,E)) = mult(mult(D,asoc(A,B,C)),E),
inference(paramod,[status(thm)],[c_2,c_9628]) ).
cnf(c_5288,plain,
mult(mult(A,asoc(B,C,D)),E) = mult(asoc(B,C,D),mult(A,E)),
inference(copy,[status(thm)],[c_9629]) ).
cnf(c_5291,plain,
rd(A,mult(A,asoc(B,C,D))) = i(asoc(B,C,D)),
inference(paramod,[status(thm)],[c_5163,c_40]) ).
cnf(c_5293,plain,
mult(mult(i(A),i(B)),mult(asoc(C,D,E),mult(A,B))) = asoc(C,D,E),
inference(paramod,[status(thm)],[c_5163,c_35]) ).
cnf(c_5322,plain,
mult(asoc(A,B,i(B)),A) = mult(mult(A,B),i(B)),
inference(paramod,[status(thm)],[c_5163,c_53]) ).
cnf(c_5337,plain,
mult(mult(i(A),mult(i(B),i(asoc(C,D,E)))),mult(asoc(C,D,E),mult(A,B))) = asoc(A,B,asoc(C,D,E)),
inference(paramod,[status(thm)],[c_5163,c_58]) ).
cnf(c_5380,plain,
asoc(i(asoc(A,B,C)),mult(asoc(A,B,C),mult(asoc(A,B,C),D)),E) = asoc(D,asoc(A,B,C),E),
inference(paramod,[status(thm)],[c_5163,c_2296]) ).
cnf(c_6254,plain,
rd(mult(mult(A,B),i(B)),A) = asoc(A,B,i(B)),
inference(paramod,[status(thm)],[c_53,c_5278]) ).
cnf(c_6257,plain,
rd(mult(mult(A,i(B)),B),A) = asoc(A,i(B),B),
inference(paramod,[status(thm)],[c_54,c_5278]) ).
cnf(c_6627,plain,
mult(asoc(A,B,i(B)),rd(A,B)) = mult(A,i(B)),
inference(paramod,[status(thm)],[c_4750,c_5163]) ).
cnf(c_6999,plain,
mult(asoc(A,i(B),B),rd(A,i(B))) = mult(A,B),
inference(paramod,[status(thm)],[c_4876,c_5163]) ).
cnf(c_7070,plain,
rd(mult(A,mult(B,C)),mult(mult(A,B),C)) = i(asoc(A,B,C)),
inference(paramod,[status(thm)],[c_11,c_5291]) ).
cnf(c_9630,plain,
mult(mult(asoc(A,B,i(B)),A),asoc(asoc(A,B,i(B)),rd(A,B),B)) = mult(mult(A,i(B)),B),
inference(paramod,[status(thm)],[c_6627,c_61]) ).
cnf(c_9631,plain,
mult(mult(mult(A,B),i(B)),asoc(asoc(A,B,i(B)),rd(A,B),B)) = mult(mult(A,i(B)),B),
inference(paramod,[status(thm)],[c_5322,c_9630]) ).
cnf(c_9632,plain,
mult(mult(mult(A,B),i(B)),unit) = mult(mult(A,i(B)),B),
inference(paramod,[status(thm)],[c_28,c_9631]) ).
cnf(c_9633,plain,
mult(mult(A,B),i(B)) = mult(mult(A,i(B)),B),
inference(paramod,[status(thm)],[c_2,c_9632]) ).
cnf(c_7456,plain,
mult(mult(A,i(B)),B) = mult(mult(A,B),i(B)),
inference(copy,[status(thm)],[c_9633]) ).
cnf(c_9634,plain,
rd(mult(mult(A,B),i(B)),A) = asoc(A,i(B),B),
inference(paramod,[status(thm)],[c_7456,c_6257]) ).
cnf(c_9635,plain,
asoc(A,B,i(B)) = asoc(A,i(B),B),
inference(paramod,[status(thm)],[c_6254,c_9634]) ).
cnf(c_7559,plain,
asoc(A,i(B),B) = asoc(A,B,i(B)),
inference(copy,[status(thm)],[c_9635]) ).
cnf(c_7676,plain,
mult(asoc(A,B,i(B)),rd(A,i(B))) = mult(A,B),
inference(paramod,[status(thm)],[c_7559,c_6999]) ).
cnf(c_9636,plain,
mult(asoc(A,asoc(B,C,D),E),mult(mult(A,mult(E,asoc(B,C,D))),mult(asoc(A,asoc(B,C,D),E),F))) = mult(asoc(A,asoc(B,C,D),E),mult(mult(mult(A,asoc(B,C,D)),E),F)),
inference(paramod,[status(thm)],[c_5163,c_152]) ).
cnf(c_9637,plain,
mult(asoc(A,asoc(B,C,D),E),mult(mult(A,mult(E,asoc(B,C,D))),mult(asoc(A,asoc(B,C,D),E),F))) = mult(asoc(A,asoc(B,C,D),E),mult(mult(asoc(B,C,D),mult(A,E)),F)),
inference(paramod,[status(thm)],[c_5288,c_9636]) ).
cnf(c_8853,plain,
mult(asoc(A,asoc(B,C,D),E),mult(mult(A,mult(E,asoc(B,C,D))),mult(asoc(A,asoc(B,C,D),E),F))) = mult(asoc(A,asoc(B,C,D),E),mult(asoc(B,C,D),mult(mult(A,E),F))),
inference(paramod,[status(thm)],[c_150,c_9637]) ).
cnf(c_9638,plain,
mult(asoc(mult(i(A),mult(i(B),i(C))),mult(mult(A,B),C),i(mult(mult(A,B),C))),rd(mult(i(A),mult(i(B),i(C))),i(mult(mult(A,B),C)))) = asoc(A,B,C),
inference(paramod,[status(thm)],[c_58,c_7676]) ).
cnf(c_9639,plain,
mult(asoc(mult(i(A),mult(i(B),i(C))),mult(mult(A,B),C),mult(i(mult(A,B)),i(C))),rd(mult(i(A),mult(i(B),i(C))),i(mult(mult(A,B),C)))) = asoc(A,B,C),
inference(paramod,[status(thm)],[c_5,c_9638]) ).
cnf(c_9640,plain,
mult(asoc(mult(i(A),mult(i(B),i(C))),mult(mult(A,B),C),mult(mult(i(A),i(B)),i(C))),rd(mult(i(A),mult(i(B),i(C))),i(mult(mult(A,B),C)))) = asoc(A,B,C),
inference(paramod,[status(thm)],[c_5,c_9639]) ).
cnf(c_9641,plain,
mult(unit,rd(mult(i(A),mult(i(B),i(C))),i(mult(mult(A,B),C)))) = asoc(A,B,C),
inference(paramod,[status(thm)],[c_4992,c_9640]) ).
cnf(c_9642,plain,
mult(unit,rd(mult(i(A),mult(i(B),i(C))),mult(i(mult(A,B)),i(C)))) = asoc(A,B,C),
inference(paramod,[status(thm)],[c_5,c_9641]) ).
cnf(c_9643,plain,
mult(unit,rd(mult(i(A),mult(i(B),i(C))),mult(mult(i(A),i(B)),i(C)))) = asoc(A,B,C),
inference(paramod,[status(thm)],[c_5,c_9642]) ).
cnf(c_9644,plain,
mult(unit,i(asoc(i(A),i(B),i(C)))) = asoc(A,B,C),
inference(paramod,[status(thm)],[c_7070,c_9643]) ).
cnf(c_9003,plain,
i(asoc(i(A),i(B),i(C))) = asoc(A,B,C),
inference(paramod,[status(thm)],[c_1,c_9644]) ).
cnf(c_9043,plain,
mult(asoc(i(A),i(B),i(C)),asoc(A,B,C)) = unit,
inference(paramod,[status(thm)],[c_9003,c_3]) ).
cnf(c_9050,plain,
i(asoc(A,B,C)) = asoc(i(A),i(B),i(C)),
inference(paramod,[status(thm)],[c_9003,c_33]) ).
cnf(c_9645,plain,
asoc(asoc(i(A),i(B),i(C)),mult(asoc(A,B,C),mult(asoc(A,B,C),D)),E) = asoc(D,asoc(A,B,C),E),
inference(paramod,[status(thm)],[c_9050,c_5380]) ).
cnf(c_9646,plain,
unit = asoc(D,asoc(A,B,C),E),
inference(paramod,[status(thm)],[c_28,c_9645]) ).
cnf(c_9324,plain,
asoc(A,asoc(B,C,D),E) = unit,
inference(copy,[status(thm)],[c_9646]) ).
cnf(c_9336,plain,
mult(mult(i(A),mult(i(B),asoc(i(C),i(D),i(E)))),mult(asoc(C,D,E),mult(A,B))) = asoc(A,B,asoc(C,D,E)),
inference(paramod,[status(thm)],[c_9050,c_5337]) ).
cnf(c_9647,plain,
mult(unit,mult(mult(A,mult(E,asoc(B,C,D))),mult(asoc(A,asoc(B,C,D),E),F))) = mult(asoc(A,asoc(B,C,D),E),mult(asoc(B,C,D),mult(mult(A,E),F))),
inference(paramod,[status(thm)],[c_9324,c_8853]) ).
cnf(c_9648,plain,
mult(unit,mult(mult(A,mult(E,asoc(B,C,D))),mult(unit,F))) = mult(asoc(A,asoc(B,C,D),E),mult(asoc(B,C,D),mult(mult(A,E),F))),
inference(paramod,[status(thm)],[c_9324,c_9647]) ).
cnf(c_9649,plain,
mult(unit,mult(mult(A,mult(E,asoc(B,C,D))),F)) = mult(asoc(A,asoc(B,C,D),E),mult(asoc(B,C,D),mult(mult(A,E),F))),
inference(paramod,[status(thm)],[c_1,c_9648]) ).
cnf(c_9650,plain,
mult(mult(A,mult(E,asoc(B,C,D))),F) = mult(asoc(A,asoc(B,C,D),E),mult(asoc(B,C,D),mult(mult(A,E),F))),
inference(paramod,[status(thm)],[c_1,c_9649]) ).
cnf(c_9651,plain,
mult(mult(A,mult(E,asoc(B,C,D))),F) = mult(unit,mult(asoc(B,C,D),mult(mult(A,E),F))),
inference(paramod,[status(thm)],[c_9324,c_9650]) ).
cnf(c_9525,plain,
mult(mult(A,mult(B,asoc(C,D,E))),F) = mult(asoc(C,D,E),mult(mult(A,B),F)),
inference(paramod,[status(thm)],[c_1,c_9651]) ).
cnf(c_9652,plain,
mult(asoc(i(C),i(D),i(E)),mult(mult(i(A),i(B)),mult(asoc(C,D,E),mult(A,B)))) = asoc(A,B,asoc(C,D,E)),
inference(paramod,[status(thm)],[c_9525,c_9336]) ).
cnf(c_9653,plain,
mult(asoc(i(C),i(D),i(E)),asoc(C,D,E)) = asoc(A,B,asoc(C,D,E)),
inference(paramod,[status(thm)],[c_5293,c_9652]) ).
cnf(c_9654,plain,
unit = asoc(A,B,asoc(C,D,E)),
inference(paramod,[status(thm)],[c_9043,c_9653]) ).
cnf(c_9548,plain,
asoc(A,B,asoc(C,D,E)) = unit,
inference(copy,[status(thm)],[c_9654]) ).
cnf(c_9549,plain,
$false,
inference(resolve,[status(thm)],[c_9548,c_29]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP727-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.35 % Computer : n003.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Fri Sep 25 15:43:07 UTC 2026
% 0.10/0.35 % CPUTime :
% 0.10/0.35 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.35 % Process 558813 was started by sandbox on n003,
% 0.10/0.35 % Fri Sep 25 15:43:07 2026
% 0.10/0.35 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.10/0.36
% 0.10/0.36 % From the command line: assign(max_seconds, 300).
% 214.80/28.67
% 214.80/28.67 % Assigning unary symbol i kb_weight 0 and highest precedence (14).
% 214.80/28.67
% 214.80/28.67 % SZS status Unsatisfiable for theBenchmark
% 214.80/28.67
% 214.80/28.67 % Proof 1 at 3.36 (+ 0.75) seconds.
% 214.80/28.67 % Length of proof is 81.
% 214.80/28.67 % Level of proof is 24.
% 214.80/28.67 % Maximum clause weight is 89.000.
% 214.80/28.67 % Given clauses 249.
% 214.80/28.67
% 214.80/28.67 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------