%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP667+6 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n020.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:09 AM UTC 2026
% Result : Theorem 25.59s 9.12s
% Output : CNFRefutation 25.59s
% Verified :
% SZS Type : Refutation
% Derivation depth : 63
% Number of leaves : 10
% Syntax : Number of formulae : 245 ( 241 unt; 0 def)
% Number of atoms : 257 ( 256 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 22 ( 10 ~; 6 |; 6 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 1 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 17 ( 17 usr; 13 con; 0-2 aty)
% Number of variables : 435 ( 0 sgn 40 !; 12 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f01,axiom,
! [B,A] : mult(A,ld(A,B)) = B,
file('theBenchmark.p',f01) ).
fof(f02,axiom,
! [B,A] : ld(A,mult(A,B)) = B,
file('theBenchmark.p',f02) ).
fof(f03,axiom,
! [B,A] : mult(rd(A,B),B) = A,
file('theBenchmark.p',f03) ).
fof(f04,axiom,
! [B,A] : rd(mult(A,B),B) = A,
file('theBenchmark.p',f04) ).
fof(f05,axiom,
! [A] : mult(A,unit) = A,
file('theBenchmark.p',f05) ).
fof(f06,axiom,
! [A] : mult(unit,A) = A,
file('theBenchmark.p',f06) ).
fof(f07,axiom,
! [C,B,A] : mult(mult(A,B),mult(mult(C,B),C)) = mult(mult(A,mult(mult(B,C),B)),C),
file('theBenchmark.p',f07) ).
fof(f08,axiom,
! [B,A] : mult(mult(A,B),A) = mult(A,mult(B,A)),
file('theBenchmark.p',f08) ).
fof(f09,axiom,
! [A] : mult(f(A),f(A)) = A,
file('theBenchmark.p',f09) ).
fof(goals,conjecture,
( ! [X9,X10,X11] : mult(mult(X11,X9),mult(X10,X11)) = mult(X11,mult(mult(X9,X10),X11))
| ! [X6,X7,X8] : mult(mult(X8,X6),mult(X7,X8)) = mult(mult(X8,mult(X6,X7)),X8)
| ! [X3,X4,X5] : mult(X3,mult(X5,mult(X4,X5))) = mult(mult(mult(X3,X5),X4),X5)
| ! [X0,X1,X2] : mult(X2,mult(X0,mult(X2,X1))) = mult(mult(mult(X2,X0),X2),X1) ),
file('theBenchmark.p',goals) ).
fof(goals_neg,negated_conjecture,
~ ( ! [X9,X10,X11] : mult(mult(X11,X9),mult(X10,X11)) = mult(X11,mult(mult(X9,X10),X11))
| ! [X6,X7,X8] : mult(mult(X8,X6),mult(X7,X8)) = mult(mult(X8,mult(X6,X7)),X8)
| ! [X3,X4,X5] : mult(X3,mult(X5,mult(X4,X5))) = mult(mult(mult(X3,X5),X4),X5)
| ! [X0,X1,X2] : mult(X2,mult(X0,mult(X2,X1))) = mult(mult(mult(X2,X0),X2),X1) ),
inference(assume_negation,[status(cth)],[goals]) ).
cnf(c_11,plain,
mult(A,ld(A,B)) = B,
inference(clausify,[status(thm)],[f01]) ).
cnf(c_12,plain,
ld(A,mult(A,B)) = B,
inference(clausify,[status(thm)],[f02]) ).
cnf(c_13,plain,
mult(rd(A,B),B) = A,
inference(clausify,[status(thm)],[f03]) ).
cnf(c_14,plain,
rd(mult(A,B),B) = A,
inference(clausify,[status(thm)],[f04]) ).
cnf(c_15,plain,
mult(A,unit) = A,
inference(clausify,[status(thm)],[f05]) ).
cnf(c_16,plain,
mult(unit,A) = A,
inference(clausify,[status(thm)],[f06]) ).
cnf(c_17,plain,
mult(mult(A,mult(mult(B,C),B)),C) = mult(mult(A,B),mult(mult(C,B),C)),
inference(clausify,[status(thm)],[f07]) ).
cnf(c_18,plain,
mult(mult(A,B),A) = mult(A,mult(B,A)),
inference(clausify,[status(thm)],[f08]) ).
cnf(c_19,plain,
mult(f(A),f(A)) = A,
inference(clausify,[status(thm)],[f09]) ).
fof(nnf_10,plain,
( ? [X9,X10,X11] : mult(mult(X11,X9),mult(X10,X11)) != mult(X11,mult(mult(X9,X10),X11))
& ? [X6,X7,X8] : mult(mult(X8,mult(X6,X7)),X8) != mult(mult(X8,X6),mult(X7,X8))
& ? [X3,X4,X5] : mult(mult(mult(X3,X5),X4),X5) != mult(X3,mult(X5,mult(X4,X5)))
& ? [X0,X1,X2] : mult(mult(mult(X2,X0),X2),X1) != mult(X2,mult(X0,mult(X2,X1))) ),
inference(fof_nnf,[status(thm)],[goals_neg]) ).
fof(sk_goals_neg,plain,
( mult(mult(sK9,sK10),mult(sK11,sK9)) != mult(sK9,mult(mult(sK10,sK11),sK9))
& mult(mult(sK6,mult(sK7,sK8)),sK6) != mult(mult(sK6,sK7),mult(sK8,sK6))
& mult(mult(mult(sK0,sK1),sK2),sK1) != mult(sK0,mult(sK1,mult(sK2,sK1)))
& mult(mult(mult(sK3,sK4),sK3),sK5) != mult(sK3,mult(sK4,mult(sK3,sK5))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3,sK4,sK5,sK0,sK1,sK2,sK6,sK7,sK8,sK9,sK10,sK11]),skolemize(X0,sK4),skolemize(X1,sK5),skolemize(X2,sK3),skolemize(X3,sK0),skolemize(X4,sK2),skolemize(X5,sK1),skolemize(X6,sK7),skolemize(X7,sK8),skolemize(X8,sK6),skolemize(X9,sK10),skolemize(X10,sK11),skolemize(X11,sK9)],[nnf_10]) ).
cnf(c_22,negated_conjecture,
mult(mult(mult(sK0,sK1),sK2),sK1) != mult(sK0,mult(sK1,mult(sK2,sK1))),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_9398,plain,
mult(mult(A,mult(B,mult(C,B))),C) = mult(mult(A,B),mult(mult(C,B),C)),
inference(paramod,[status(thm)],[c_18,c_17]) ).
cnf(c_26,plain,
mult(mult(A,mult(B,mult(C,B))),C) = mult(mult(A,B),mult(C,mult(B,C))),
inference(paramod,[status(thm)],[c_18,c_9398]) ).
cnf(c_27,plain,
ld(rd(A,B),A) = B,
inference(paramod,[status(thm)],[c_13,c_12]) ).
cnf(c_28,plain,
rd(A,ld(B,A)) = B,
inference(paramod,[status(thm)],[c_11,c_14]) ).
cnf(c_29,plain,
ld(A,A) = unit,
inference(paramod,[status(thm)],[c_15,c_12]) ).
cnf(c_9399,plain,
mult(A,B) = mult(B,mult(ld(B,A),B)),
inference(paramod,[status(thm)],[c_11,c_18]) ).
cnf(c_33,plain,
mult(A,mult(ld(A,B),A)) = mult(B,A),
inference(copy,[status(thm)],[c_9399]) ).
cnf(c_34,plain,
ld(mult(A,B),mult(A,mult(B,A))) = A,
inference(paramod,[status(thm)],[c_18,c_12]) ).
cnf(c_9400,plain,
mult(A,rd(A,B)) = mult(rd(A,B),mult(B,rd(A,B))),
inference(paramod,[status(thm)],[c_13,c_18]) ).
cnf(c_35,plain,
mult(rd(A,B),mult(B,rd(A,B))) = mult(A,rd(A,B)),
inference(copy,[status(thm)],[c_9400]) ).
cnf(c_9401,plain,
mult(A,f(A)) = mult(f(A),mult(f(A),f(A))),
inference(paramod,[status(thm)],[c_19,c_18]) ).
cnf(c_9402,plain,
mult(A,f(A)) = mult(f(A),A),
inference(paramod,[status(thm)],[c_19,c_9401]) ).
cnf(c_40,plain,
mult(f(A),A) = mult(A,f(A)),
inference(copy,[status(thm)],[c_9402]) ).
cnf(c_9403,plain,
mult(mult(A,mult(ld(B,C),C)),B) = mult(mult(A,ld(B,C)),mult(B,mult(ld(B,C),B))),
inference(paramod,[status(thm)],[c_11,c_26]) ).
cnf(c_41,plain,
mult(mult(A,mult(ld(B,C),C)),B) = mult(mult(A,ld(B,C)),mult(C,B)),
inference(paramod,[status(thm)],[c_33,c_9403]) ).
cnf(c_9404,plain,
mult(mult(A,mult(B,C)),rd(C,B)) = mult(mult(A,B),mult(rd(C,B),mult(B,rd(C,B)))),
inference(paramod,[status(thm)],[c_13,c_26]) ).
cnf(c_44,plain,
mult(mult(A,mult(B,C)),rd(C,B)) = mult(mult(A,B),mult(C,rd(C,B))),
inference(paramod,[status(thm)],[c_35,c_9404]) ).
cnf(c_9405,plain,
mult(A,B) = mult(mult(rd(A,mult(C,mult(B,C))),C),mult(B,mult(C,B))),
inference(paramod,[status(thm)],[c_13,c_26]) ).
cnf(c_45,plain,
mult(mult(rd(A,mult(B,mult(C,B))),B),mult(C,mult(B,C))) = mult(A,C),
inference(copy,[status(thm)],[c_9405]) ).
cnf(c_47,plain,
rd(mult(mult(A,B),mult(C,mult(B,C))),C) = mult(A,mult(B,mult(C,B))),
inference(paramod,[status(thm)],[c_26,c_14]) ).
cnf(c_9406,plain,
mult(mult(A,B),mult(unit,mult(B,unit))) = mult(A,mult(B,mult(unit,B))),
inference(paramod,[status(thm)],[c_26,c_15]) ).
cnf(c_9407,plain,
mult(mult(A,B),mult(unit,B)) = mult(A,mult(B,mult(unit,B))),
inference(paramod,[status(thm)],[c_15,c_9406]) ).
cnf(c_9408,plain,
mult(mult(A,B),B) = mult(A,mult(B,mult(unit,B))),
inference(paramod,[status(thm)],[c_16,c_9407]) ).
cnf(c_48,plain,
mult(mult(A,B),B) = mult(A,mult(B,B)),
inference(paramod,[status(thm)],[c_16,c_9408]) ).
cnf(c_52,plain,
ld(A,mult(B,A)) = mult(ld(A,B),A),
inference(paramod,[status(thm)],[c_33,c_12]) ).
cnf(c_9409,plain,
ld(A,B) = mult(ld(A,rd(B,A)),A),
inference(paramod,[status(thm)],[c_13,c_52]) ).
cnf(c_64,plain,
mult(ld(A,rd(B,A)),A) = ld(A,B),
inference(copy,[status(thm)],[c_9409]) ).
cnf(c_9410,plain,
ld(A,A) = mult(ld(A,unit),A),
inference(paramod,[status(thm)],[c_16,c_52]) ).
cnf(c_9411,plain,
unit = mult(ld(A,unit),A),
inference(paramod,[status(thm)],[c_29,c_9410]) ).
cnf(c_65,plain,
mult(ld(A,unit),A) = unit,
inference(copy,[status(thm)],[c_9411]) ).
cnf(c_9412,plain,
ld(A,mult(A,f(A))) = mult(ld(A,f(A)),A),
inference(paramod,[status(thm)],[c_40,c_52]) ).
cnf(c_9413,plain,
f(A) = mult(ld(A,f(A)),A),
inference(paramod,[status(thm)],[c_12,c_9412]) ).
cnf(c_68,plain,
mult(ld(A,f(A)),A) = f(A),
inference(copy,[status(thm)],[c_9413]) ).
cnf(c_70,plain,
ld(ld(A,unit),unit) = A,
inference(paramod,[status(thm)],[c_65,c_12]) ).
cnf(c_71,plain,
rd(unit,A) = ld(A,unit),
inference(paramod,[status(thm)],[c_65,c_14]) ).
cnf(c_74,plain,
ld(mult(ld(A,B),A),mult(ld(A,B),B)) = ld(A,B),
inference(paramod,[status(thm)],[c_11,c_34]) ).
cnf(c_75,plain,
ld(mult(A,rd(B,A)),mult(A,B)) = A,
inference(paramod,[status(thm)],[c_13,c_34]) ).
cnf(c_85,plain,
rd(f(A),A) = ld(A,f(A)),
inference(paramod,[status(thm)],[c_68,c_14]) ).
cnf(c_9414,plain,
mult(f(A),ld(A,f(A))) = mult(ld(A,f(A)),mult(A,ld(A,f(A)))),
inference(paramod,[status(thm)],[c_68,c_18]) ).
cnf(c_9415,plain,
mult(f(A),ld(A,f(A))) = mult(ld(A,f(A)),f(A)),
inference(paramod,[status(thm)],[c_11,c_9414]) ).
cnf(c_86,plain,
mult(ld(A,f(A)),f(A)) = mult(f(A),ld(A,f(A))),
inference(copy,[status(thm)],[c_9415]) ).
cnf(c_9416,plain,
mult(mult(A,mult(B,f(B))),ld(B,f(B))) = mult(mult(A,B),mult(ld(B,f(B)),mult(B,ld(B,f(B))))),
inference(paramod,[status(thm)],[c_68,c_26]) ).
cnf(c_9417,plain,
mult(mult(A,mult(B,f(B))),ld(B,f(B))) = mult(mult(A,B),mult(ld(B,f(B)),f(B))),
inference(paramod,[status(thm)],[c_11,c_9416]) ).
cnf(c_87,plain,
mult(mult(A,mult(B,f(B))),ld(B,f(B))) = mult(mult(A,B),mult(f(B),ld(B,f(B)))),
inference(paramod,[status(thm)],[c_86,c_9417]) ).
cnf(c_95,plain,
rd(ld(A,B),A) = ld(A,rd(B,A)),
inference(paramod,[status(thm)],[c_64,c_14]) ).
cnf(c_9418,plain,
mult(ld(A,B),ld(A,rd(B,A))) = mult(ld(A,rd(B,A)),mult(A,ld(A,rd(B,A)))),
inference(paramod,[status(thm)],[c_64,c_18]) ).
cnf(c_9419,plain,
mult(ld(A,B),ld(A,rd(B,A))) = mult(ld(A,rd(B,A)),rd(B,A)),
inference(paramod,[status(thm)],[c_11,c_9418]) ).
cnf(c_96,plain,
mult(ld(A,rd(B,A)),rd(B,A)) = mult(ld(A,B),ld(A,rd(B,A))),
inference(copy,[status(thm)],[c_9419]) ).
cnf(c_9420,plain,
mult(mult(A,mult(B,ld(B,C))),ld(B,rd(C,B))) = mult(mult(A,B),mult(ld(B,rd(C,B)),mult(B,ld(B,rd(C,B))))),
inference(paramod,[status(thm)],[c_64,c_26]) ).
cnf(c_9421,plain,
mult(mult(A,C),ld(B,rd(C,B))) = mult(mult(A,B),mult(ld(B,rd(C,B)),mult(B,ld(B,rd(C,B))))),
inference(paramod,[status(thm)],[c_11,c_9420]) ).
cnf(c_9422,plain,
mult(mult(A,C),ld(B,rd(C,B))) = mult(mult(A,B),mult(ld(B,rd(C,B)),rd(C,B))),
inference(paramod,[status(thm)],[c_11,c_9421]) ).
cnf(c_9423,plain,
mult(mult(A,C),ld(B,rd(C,B))) = mult(mult(A,B),mult(ld(B,C),ld(B,rd(C,B)))),
inference(paramod,[status(thm)],[c_96,c_9422]) ).
cnf(c_97,plain,
mult(mult(A,B),mult(ld(B,C),ld(B,rd(C,B)))) = mult(mult(A,C),ld(B,rd(C,B))),
inference(copy,[status(thm)],[c_9423]) ).
cnf(c_9424,plain,
rd(A,ld(A,unit)) = ld(ld(A,unit),rd(unit,ld(A,unit))),
inference(paramod,[status(thm)],[c_70,c_95]) ).
cnf(c_103,plain,
rd(A,ld(A,unit)) = ld(ld(A,unit),A),
inference(paramod,[status(thm)],[c_28,c_9424]) ).
cnf(c_111,plain,
rd(mult(A,B),A) = mult(A,rd(B,A)),
inference(paramod,[status(thm)],[c_75,c_28]) ).
cnf(c_9425,plain,
mult(mult(f(A),ld(A,f(A))),ld(A,f(A))) = mult(ld(A,f(A)),mult(f(A),ld(A,f(A)))),
inference(paramod,[status(thm)],[c_86,c_18]) ).
cnf(c_9426,plain,
mult(f(A),mult(ld(A,f(A)),ld(A,f(A)))) = mult(ld(A,f(A)),mult(f(A),ld(A,f(A)))),
inference(paramod,[status(thm)],[c_48,c_9425]) ).
cnf(c_150,plain,
mult(ld(A,f(A)),mult(f(A),ld(A,f(A)))) = mult(f(A),mult(ld(A,f(A)),ld(A,f(A)))),
inference(copy,[status(thm)],[c_9426]) ).
cnf(c_9427,plain,
ld(f(A),mult(f(A),ld(A,f(A)))) = mult(ld(f(A),ld(A,f(A))),f(A)),
inference(paramod,[status(thm)],[c_86,c_52]) ).
cnf(c_9428,plain,
ld(A,f(A)) = mult(ld(f(A),ld(A,f(A))),f(A)),
inference(paramod,[status(thm)],[c_12,c_9427]) ).
cnf(c_153,plain,
mult(ld(f(A),ld(A,f(A))),f(A)) = ld(A,f(A)),
inference(copy,[status(thm)],[c_9428]) ).
cnf(c_9429,plain,
mult(A,B) = mult(rd(A,B),mult(B,B)),
inference(paramod,[status(thm)],[c_13,c_48]) ).
cnf(c_182,plain,
mult(rd(A,B),mult(B,B)) = mult(A,B),
inference(copy,[status(thm)],[c_9429]) ).
cnf(c_9430,plain,
mult(mult(A,mult(B,A)),A) = mult(mult(A,B),mult(A,A)),
inference(paramod,[status(thm)],[c_18,c_48]) ).
cnf(c_9431,plain,
mult(A,mult(mult(B,A),A)) = mult(mult(A,B),mult(A,A)),
inference(paramod,[status(thm)],[c_18,c_9430]) ).
cnf(c_9432,plain,
mult(A,mult(B,mult(A,A))) = mult(mult(A,B),mult(A,A)),
inference(paramod,[status(thm)],[c_48,c_9431]) ).
cnf(c_184,plain,
mult(mult(A,B),mult(A,A)) = mult(A,mult(B,mult(A,A))),
inference(copy,[status(thm)],[c_9432]) ).
cnf(c_9433,plain,
mult(unit,A) = mult(ld(A,unit),mult(A,A)),
inference(paramod,[status(thm)],[c_65,c_48]) ).
cnf(c_9434,plain,
A = mult(ld(A,unit),mult(A,A)),
inference(paramod,[status(thm)],[c_16,c_9433]) ).
cnf(c_188,plain,
mult(ld(A,unit),mult(A,A)) = A,
inference(copy,[status(thm)],[c_9434]) ).
cnf(c_206,plain,
ld(ld(A,unit),A) = mult(A,A),
inference(paramod,[status(thm)],[c_188,c_12]) ).
cnf(c_207,plain,
rd(A,mult(A,A)) = ld(A,unit),
inference(paramod,[status(thm)],[c_188,c_14]) ).
cnf(c_9435,plain,
mult(A,ld(A,unit)) = mult(ld(A,unit),mult(mult(A,A),ld(A,unit))),
inference(paramod,[status(thm)],[c_188,c_18]) ).
cnf(c_9436,plain,
unit = mult(ld(A,unit),mult(mult(A,A),ld(A,unit))),
inference(paramod,[status(thm)],[c_11,c_9435]) ).
cnf(c_208,plain,
mult(ld(A,unit),mult(mult(A,A),ld(A,unit))) = unit,
inference(copy,[status(thm)],[c_9436]) ).
cnf(c_9437,plain,
mult(mult(A,mult(mult(B,B),B)),ld(B,unit)) = mult(mult(A,mult(B,B)),mult(ld(B,unit),mult(mult(B,B),ld(B,unit)))),
inference(paramod,[status(thm)],[c_188,c_26]) ).
cnf(c_9438,plain,
mult(mult(A,mult(B,mult(B,B))),ld(B,unit)) = mult(mult(A,mult(B,B)),mult(ld(B,unit),mult(mult(B,B),ld(B,unit)))),
inference(paramod,[status(thm)],[c_18,c_9437]) ).
cnf(c_9439,plain,
mult(mult(A,mult(B,mult(B,B))),ld(B,unit)) = mult(mult(A,mult(B,B)),unit),
inference(paramod,[status(thm)],[c_208,c_9438]) ).
cnf(c_210,plain,
mult(mult(A,mult(B,mult(B,B))),ld(B,unit)) = mult(A,mult(B,B)),
inference(paramod,[status(thm)],[c_15,c_9439]) ).
cnf(c_219,plain,
rd(A,ld(A,unit)) = mult(A,A),
inference(paramod,[status(thm)],[c_206,c_103]) ).
cnf(c_9440,plain,
rd(f(A),A) = ld(f(A),unit),
inference(paramod,[status(thm)],[c_19,c_207]) ).
cnf(c_9441,plain,
ld(A,f(A)) = ld(f(A),unit),
inference(paramod,[status(thm)],[c_85,c_9440]) ).
cnf(c_221,plain,
ld(f(A),unit) = ld(A,f(A)),
inference(copy,[status(thm)],[c_9441]) ).
cnf(c_9442,plain,
rd(mult(mult(A,A),A),mult(A,A)) = mult(mult(A,A),ld(A,unit)),
inference(paramod,[status(thm)],[c_207,c_111]) ).
cnf(c_9443,plain,
rd(mult(A,mult(A,A)),mult(A,A)) = mult(mult(A,A),ld(A,unit)),
inference(paramod,[status(thm)],[c_18,c_9442]) ).
cnf(c_9444,plain,
A = mult(mult(A,A),ld(A,unit)),
inference(paramod,[status(thm)],[c_14,c_9443]) ).
cnf(c_223,plain,
mult(mult(A,A),ld(A,unit)) = A,
inference(copy,[status(thm)],[c_9444]) ).
cnf(c_9445,plain,
rd(rd(unit,A),A) = mult(rd(unit,A),rd(unit,A)),
inference(paramod,[status(thm)],[c_27,c_219]) ).
cnf(c_9446,plain,
rd(ld(A,unit),A) = mult(rd(unit,A),rd(unit,A)),
inference(paramod,[status(thm)],[c_71,c_9445]) ).
cnf(c_9447,plain,
ld(A,rd(unit,A)) = mult(rd(unit,A),rd(unit,A)),
inference(paramod,[status(thm)],[c_95,c_9446]) ).
cnf(c_9448,plain,
ld(A,ld(A,unit)) = mult(rd(unit,A),rd(unit,A)),
inference(paramod,[status(thm)],[c_71,c_9447]) ).
cnf(c_9449,plain,
ld(A,ld(A,unit)) = mult(ld(A,unit),rd(unit,A)),
inference(paramod,[status(thm)],[c_71,c_9448]) ).
cnf(c_9450,plain,
ld(A,ld(A,unit)) = mult(ld(A,unit),ld(A,unit)),
inference(paramod,[status(thm)],[c_71,c_9449]) ).
cnf(c_226,plain,
mult(ld(A,unit),ld(A,unit)) = ld(A,ld(A,unit)),
inference(copy,[status(thm)],[c_9450]) ).
cnf(c_9451,plain,
rd(ld(ld(A,unit),A),ld(A,unit)) = ld(ld(A,unit),mult(A,A)),
inference(paramod,[status(thm)],[c_219,c_95]) ).
cnf(c_227,plain,
rd(mult(A,A),ld(A,unit)) = ld(ld(A,unit),mult(A,A)),
inference(paramod,[status(thm)],[c_206,c_9451]) ).
cnf(c_228,plain,
mult(f(A),ld(A,f(A))) = unit,
inference(paramod,[status(thm)],[c_221,c_11]) ).
cnf(c_229,plain,
mult(A,ld(f(A),unit)) = f(A),
inference(paramod,[status(thm)],[c_221,c_11]) ).
cnf(c_9452,plain,
rd(ld(A,f(A)),f(A)) = ld(f(A),rd(unit,f(A))),
inference(paramod,[status(thm)],[c_221,c_95]) ).
cnf(c_231,plain,
rd(ld(A,f(A)),f(A)) = ld(f(A),ld(f(A),unit)),
inference(paramod,[status(thm)],[c_71,c_9452]) ).
cnf(c_9453,plain,
mult(ld(A,f(A)),unit) = mult(f(A),mult(ld(A,f(A)),ld(A,f(A)))),
inference(paramod,[status(thm)],[c_228,c_150]) ).
cnf(c_9454,plain,
ld(A,f(A)) = mult(f(A),mult(ld(A,f(A)),ld(A,f(A)))),
inference(paramod,[status(thm)],[c_15,c_9453]) ).
cnf(c_236,plain,
mult(f(A),mult(ld(A,f(A)),ld(A,f(A)))) = ld(A,f(A)),
inference(copy,[status(thm)],[c_9454]) ).
cnf(c_9455,plain,
mult(mult(A,mult(B,f(B))),ld(B,f(B))) = mult(mult(A,B),unit),
inference(paramod,[status(thm)],[c_228,c_87]) ).
cnf(c_237,plain,
mult(mult(A,mult(B,f(B))),ld(B,f(B))) = mult(A,B),
inference(paramod,[status(thm)],[c_15,c_9455]) ).
cnf(c_238,plain,
mult(ld(A,f(A)),f(A)) = unit,
inference(paramod,[status(thm)],[c_228,c_86]) ).
cnf(c_313,plain,
ld(rd(A,B),mult(A,B)) = mult(B,B),
inference(paramod,[status(thm)],[c_182,c_12]) ).
cnf(c_314,plain,
rd(mult(A,B),mult(B,B)) = rd(A,B),
inference(paramod,[status(thm)],[c_182,c_14]) ).
cnf(c_9456,plain,
mult(rd(A,ld(f(A),unit)),mult(ld(f(A),unit),ld(f(A),unit))) = f(A),
inference(paramod,[status(thm)],[c_229,c_182]) ).
cnf(c_331,plain,
mult(rd(A,ld(f(A),unit)),ld(f(A),ld(f(A),unit))) = f(A),
inference(paramod,[status(thm)],[c_226,c_9456]) ).
cnf(c_9457,plain,
ld(mult(A,A),mult(A,ld(A,unit))) = mult(ld(A,unit),ld(A,unit)),
inference(paramod,[status(thm)],[c_219,c_313]) ).
cnf(c_9458,plain,
ld(mult(A,A),unit) = mult(ld(A,unit),ld(A,unit)),
inference(paramod,[status(thm)],[c_11,c_9457]) ).
cnf(c_357,plain,
ld(mult(A,A),unit) = ld(A,ld(A,unit)),
inference(paramod,[status(thm)],[c_226,c_9458]) ).
cnf(c_9459,plain,
ld(rd(f(A),ld(A,f(A))),unit) = mult(ld(A,f(A)),ld(A,f(A))),
inference(paramod,[status(thm)],[c_228,c_313]) ).
cnf(c_9460,plain,
ld(A,unit) = mult(ld(A,f(A)),ld(A,f(A))),
inference(paramod,[status(thm)],[c_28,c_9459]) ).
cnf(c_361,plain,
mult(ld(A,f(A)),ld(A,f(A))) = ld(A,unit),
inference(copy,[status(thm)],[c_9460]) ).
cnf(c_365,plain,
mult(f(A),ld(A,unit)) = ld(A,f(A)),
inference(paramod,[status(thm)],[c_361,c_236]) ).
cnf(c_9461,plain,
rd(A,mult(B,B)) = rd(rd(A,B),B),
inference(paramod,[status(thm)],[c_13,c_314]) ).
cnf(c_367,plain,
rd(rd(A,B),B) = rd(A,mult(B,B)),
inference(copy,[status(thm)],[c_9461]) ).
cnf(c_9462,plain,
rd(A,mult(ld(A,unit),ld(A,unit))) = rd(mult(A,A),ld(A,unit)),
inference(paramod,[status(thm)],[c_223,c_314]) ).
cnf(c_9463,plain,
rd(A,ld(A,ld(A,unit))) = rd(mult(A,A),ld(A,unit)),
inference(paramod,[status(thm)],[c_226,c_9462]) ).
cnf(c_382,plain,
rd(A,ld(A,ld(A,unit))) = ld(ld(A,unit),mult(A,A)),
inference(paramod,[status(thm)],[c_227,c_9463]) ).
cnf(c_9464,plain,
rd(f(A),mult(ld(f(A),unit),ld(f(A),unit))) = rd(A,ld(f(A),unit)),
inference(paramod,[status(thm)],[c_229,c_314]) ).
cnf(c_9465,plain,
rd(f(A),ld(f(A),ld(f(A),unit))) = rd(A,ld(f(A),unit)),
inference(paramod,[status(thm)],[c_226,c_9464]) ).
cnf(c_9466,plain,
ld(ld(f(A),unit),mult(f(A),f(A))) = rd(A,ld(f(A),unit)),
inference(paramod,[status(thm)],[c_382,c_9465]) ).
cnf(c_9467,plain,
ld(ld(f(A),unit),A) = rd(A,ld(f(A),unit)),
inference(paramod,[status(thm)],[c_19,c_9466]) ).
cnf(c_383,plain,
rd(A,ld(f(A),unit)) = ld(ld(f(A),unit),A),
inference(copy,[status(thm)],[c_9467]) ).
cnf(c_9468,plain,
rd(unit,mult(f(A),f(A))) = rd(ld(A,f(A)),f(A)),
inference(paramod,[status(thm)],[c_238,c_314]) ).
cnf(c_9469,plain,
rd(unit,A) = rd(ld(A,f(A)),f(A)),
inference(paramod,[status(thm)],[c_19,c_9468]) ).
cnf(c_9470,plain,
ld(A,unit) = rd(ld(A,f(A)),f(A)),
inference(paramod,[status(thm)],[c_71,c_9469]) ).
cnf(c_384,plain,
rd(ld(A,f(A)),f(A)) = ld(A,unit),
inference(copy,[status(thm)],[c_9470]) ).
cnf(c_392,plain,
mult(ld(ld(f(A),unit),A),ld(f(A),ld(f(A),unit))) = f(A),
inference(paramod,[status(thm)],[c_383,c_331]) ).
cnf(c_9471,plain,
ld(A,unit) = ld(f(A),ld(f(A),unit)),
inference(paramod,[status(thm)],[c_384,c_231]) ).
cnf(c_393,plain,
ld(f(A),ld(f(A),unit)) = ld(A,unit),
inference(copy,[status(thm)],[c_9471]) ).
cnf(c_398,plain,
mult(ld(ld(f(A),unit),A),ld(A,unit)) = f(A),
inference(paramod,[status(thm)],[c_393,c_392]) ).
cnf(c_400,plain,
ld(f(A),ld(A,f(A))) = ld(A,unit),
inference(paramod,[status(thm)],[c_365,c_12]) ).
cnf(c_420,plain,
mult(ld(A,unit),f(A)) = ld(A,f(A)),
inference(paramod,[status(thm)],[c_400,c_153]) ).
cnf(c_9472,plain,
rd(mult(A,A),ld(A,ld(A,unit))) = mult(mult(A,A),mult(A,A)),
inference(paramod,[status(thm)],[c_357,c_219]) ).
cnf(c_517,plain,
rd(mult(A,A),ld(A,ld(A,unit))) = mult(A,mult(A,mult(A,A))),
inference(paramod,[status(thm)],[c_184,c_9472]) ).
cnf(c_524,plain,
mult(rd(A,mult(B,B)),B) = rd(A,B),
inference(paramod,[status(thm)],[c_367,c_13]) ).
cnf(c_588,plain,
mult(rd(A,B),f(B)) = rd(A,f(B)),
inference(paramod,[status(thm)],[c_19,c_524]) ).
cnf(c_614,plain,
ld(rd(A,B),rd(A,f(B))) = f(B),
inference(paramod,[status(thm)],[c_588,c_12]) ).
cnf(c_9473,plain,
mult(A,f(B)) = rd(mult(A,B),f(B)),
inference(paramod,[status(thm)],[c_14,c_588]) ).
cnf(c_615,plain,
rd(mult(A,B),f(B)) = mult(A,f(B)),
inference(copy,[status(thm)],[c_9473]) ).
cnf(c_649,plain,
ld(mult(A,f(B)),mult(A,B)) = f(B),
inference(paramod,[status(thm)],[c_615,c_27]) ).
cnf(c_9474,plain,
rd(f(A),mult(B,f(A))) = ld(mult(B,f(A)),rd(mult(B,A),mult(B,f(A)))),
inference(paramod,[status(thm)],[c_649,c_95]) ).
cnf(c_745,plain,
ld(mult(A,f(B)),rd(mult(A,B),mult(A,f(B)))) = rd(f(B),mult(A,f(B))),
inference(copy,[status(thm)],[c_9474]) ).
cnf(c_9475,plain,
mult(mult(ld(A,f(A)),mult(ld(A,f(A)),f(A))),A) = mult(ld(A,unit),mult(f(A),A)),
inference(paramod,[status(thm)],[c_361,c_41]) ).
cnf(c_9476,plain,
mult(mult(ld(A,f(A)),unit),A) = mult(ld(A,unit),mult(f(A),A)),
inference(paramod,[status(thm)],[c_238,c_9475]) ).
cnf(c_9477,plain,
mult(ld(A,f(A)),A) = mult(ld(A,unit),mult(f(A),A)),
inference(paramod,[status(thm)],[c_15,c_9476]) ).
cnf(c_9478,plain,
f(A) = mult(ld(A,unit),mult(f(A),A)),
inference(paramod,[status(thm)],[c_68,c_9477]) ).
cnf(c_9479,plain,
f(A) = mult(ld(A,unit),mult(A,f(A))),
inference(paramod,[status(thm)],[c_40,c_9478]) ).
cnf(c_789,plain,
mult(ld(A,unit),mult(A,f(A))) = f(A),
inference(copy,[status(thm)],[c_9479]) ).
cnf(c_9480,plain,
rd(mult(unit,mult(A,mult(B,A))),A) = mult(ld(B,unit),mult(B,mult(A,B))),
inference(paramod,[status(thm)],[c_65,c_47]) ).
cnf(c_9481,plain,
rd(mult(A,mult(B,A)),A) = mult(ld(B,unit),mult(B,mult(A,B))),
inference(paramod,[status(thm)],[c_16,c_9480]) ).
cnf(c_9482,plain,
mult(A,rd(mult(B,A),A)) = mult(ld(B,unit),mult(B,mult(A,B))),
inference(paramod,[status(thm)],[c_111,c_9481]) ).
cnf(c_9483,plain,
mult(A,B) = mult(ld(B,unit),mult(B,mult(A,B))),
inference(paramod,[status(thm)],[c_14,c_9482]) ).
cnf(c_900,plain,
mult(ld(A,unit),mult(A,mult(B,A))) = mult(B,A),
inference(copy,[status(thm)],[c_9483]) ).
cnf(c_9484,plain,
mult(rd(mult(A,A),mult(ld(A,unit),ld(A,unit))),ld(A,unit)) = ld(ld(A,unit),mult(A,A)),
inference(paramod,[status(thm)],[c_227,c_524]) ).
cnf(c_9485,plain,
mult(rd(mult(A,A),ld(A,ld(A,unit))),ld(A,unit)) = ld(ld(A,unit),mult(A,A)),
inference(paramod,[status(thm)],[c_226,c_9484]) ).
cnf(c_9486,plain,
mult(mult(A,mult(A,mult(A,A))),ld(A,unit)) = ld(ld(A,unit),mult(A,A)),
inference(paramod,[status(thm)],[c_517,c_9485]) ).
cnf(c_9487,plain,
mult(A,mult(A,A)) = ld(ld(A,unit),mult(A,A)),
inference(paramod,[status(thm)],[c_210,c_9486]) ).
cnf(c_1553,plain,
ld(ld(A,unit),mult(A,A)) = mult(A,mult(A,A)),
inference(copy,[status(thm)],[c_9487]) ).
cnf(c_1565,plain,
rd(mult(A,A),ld(A,unit)) = mult(A,mult(A,A)),
inference(paramod,[status(thm)],[c_1553,c_227]) ).
cnf(c_9488,plain,
rd(A,ld(f(A),unit)) = mult(f(A),mult(f(A),f(A))),
inference(paramod,[status(thm)],[c_19,c_1565]) ).
cnf(c_9489,plain,
ld(ld(f(A),unit),A) = mult(f(A),mult(f(A),f(A))),
inference(paramod,[status(thm)],[c_383,c_9488]) ).
cnf(c_9490,plain,
ld(ld(f(A),unit),A) = mult(f(A),A),
inference(paramod,[status(thm)],[c_19,c_9489]) ).
cnf(c_1566,plain,
ld(ld(f(A),unit),A) = mult(A,f(A)),
inference(paramod,[status(thm)],[c_40,c_9490]) ).
cnf(c_1577,plain,
mult(mult(A,f(A)),ld(A,unit)) = f(A),
inference(paramod,[status(thm)],[c_1566,c_398]) ).
cnf(c_9491,plain,
mult(mult(rd(A,mult(mult(B,f(B)),f(B))),mult(B,f(B))),mult(ld(B,unit),mult(mult(B,f(B)),ld(B,unit)))) = mult(A,ld(B,unit)),
inference(paramod,[status(thm)],[c_789,c_45]) ).
cnf(c_9492,plain,
mult(mult(rd(A,mult(B,mult(f(B),f(B)))),mult(B,f(B))),mult(ld(B,unit),mult(mult(B,f(B)),ld(B,unit)))) = mult(A,ld(B,unit)),
inference(paramod,[status(thm)],[c_48,c_9491]) ).
cnf(c_9493,plain,
mult(mult(rd(A,mult(B,B)),mult(B,f(B))),mult(ld(B,unit),mult(mult(B,f(B)),ld(B,unit)))) = mult(A,ld(B,unit)),
inference(paramod,[status(thm)],[c_19,c_9492]) ).
cnf(c_9494,plain,
mult(mult(rd(A,mult(B,B)),mult(B,f(B))),mult(ld(B,unit),f(B))) = mult(A,ld(B,unit)),
inference(paramod,[status(thm)],[c_1577,c_9493]) ).
cnf(c_9495,plain,
mult(mult(rd(A,mult(B,B)),mult(B,f(B))),ld(B,f(B))) = mult(A,ld(B,unit)),
inference(paramod,[status(thm)],[c_420,c_9494]) ).
cnf(c_9496,plain,
mult(rd(A,mult(B,B)),B) = mult(A,ld(B,unit)),
inference(paramod,[status(thm)],[c_237,c_9495]) ).
cnf(c_9497,plain,
rd(A,B) = mult(A,ld(B,unit)),
inference(paramod,[status(thm)],[c_524,c_9496]) ).
cnf(c_2276,plain,
mult(A,ld(B,unit)) = rd(A,B),
inference(copy,[status(thm)],[c_9497]) ).
cnf(c_2611,plain,
ld(A,rd(A,B)) = ld(B,unit),
inference(paramod,[status(thm)],[c_2276,c_12]) ).
cnf(c_9498,plain,
mult(A,B) = rd(A,rd(unit,B)),
inference(paramod,[status(thm)],[c_27,c_2276]) ).
cnf(c_9499,plain,
mult(A,B) = rd(A,ld(B,unit)),
inference(paramod,[status(thm)],[c_71,c_9498]) ).
cnf(c_2618,plain,
rd(A,ld(B,unit)) = mult(A,B),
inference(copy,[status(thm)],[c_9499]) ).
cnf(c_2775,plain,
ld(mult(A,B),A) = ld(B,unit),
inference(paramod,[status(thm)],[c_14,c_2611]) ).
cnf(c_9500,plain,
ld(A,B) = ld(ld(B,A),unit),
inference(paramod,[status(thm)],[c_28,c_2611]) ).
cnf(c_2776,plain,
ld(ld(A,B),unit) = ld(B,A),
inference(copy,[status(thm)],[c_9500]) ).
cnf(c_9501,plain,
mult(mult(ld(A,unit),B),A) = mult(ld(A,unit),rd(B,ld(A,unit))),
inference(paramod,[status(thm)],[c_2618,c_111]) ).
cnf(c_2803,plain,
mult(mult(ld(A,unit),B),A) = mult(ld(A,unit),mult(B,A)),
inference(paramod,[status(thm)],[c_2618,c_9501]) ).
cnf(c_2817,plain,
ld(mult(A,mult(B,A)),mult(A,B)) = ld(A,unit),
inference(paramod,[status(thm)],[c_18,c_2775]) ).
cnf(c_9502,plain,
ld(ld(A,B),unit) = ld(mult(ld(A,B),B),mult(ld(A,B),A)),
inference(paramod,[status(thm)],[c_74,c_2776]) ).
cnf(c_9503,plain,
ld(B,A) = ld(mult(ld(A,B),B),mult(ld(A,B),A)),
inference(paramod,[status(thm)],[c_2776,c_9502]) ).
cnf(c_2841,plain,
ld(mult(ld(A,B),B),mult(ld(A,B),A)) = ld(B,A),
inference(copy,[status(thm)],[c_9503]) ).
cnf(c_9504,plain,
ld(mult(ld(mult(A,mult(B,A)),mult(A,B)),mult(A,B)),mult(ld(mult(A,mult(B,A)),mult(A,B)),mult(A,mult(B,A)))) = A,
inference(paramod,[status(thm)],[c_34,c_2841]) ).
cnf(c_9505,plain,
ld(mult(ld(A,unit),mult(A,B)),mult(ld(mult(A,mult(B,A)),mult(A,B)),mult(A,mult(B,A)))) = A,
inference(paramod,[status(thm)],[c_2817,c_9504]) ).
cnf(c_9506,plain,
ld(mult(ld(A,unit),mult(A,B)),mult(ld(A,unit),mult(A,mult(B,A)))) = A,
inference(paramod,[status(thm)],[c_2817,c_9505]) ).
cnf(c_3621,plain,
ld(mult(ld(A,unit),mult(A,B)),mult(B,A)) = A,
inference(paramod,[status(thm)],[c_900,c_9506]) ).
cnf(c_6186,plain,
ld(mult(ld(A,unit),B),mult(ld(A,B),A)) = A,
inference(paramod,[status(thm)],[c_11,c_3621]) ).
cnf(c_9507,plain,
mult(mult(ld(A,unit),B),A) = mult(ld(A,B),A),
inference(paramod,[status(thm)],[c_6186,c_11]) ).
cnf(c_6278,plain,
mult(ld(A,unit),mult(B,A)) = mult(ld(A,B),A),
inference(paramod,[status(thm)],[c_2803,c_9507]) ).
cnf(c_9508,plain,
mult(ld(A,unit),B) = mult(ld(A,rd(B,A)),A),
inference(paramod,[status(thm)],[c_13,c_6278]) ).
cnf(c_6470,plain,
mult(ld(A,unit),B) = ld(A,B),
inference(paramod,[status(thm)],[c_64,c_9508]) ).
cnf(c_7649,plain,
rd(ld(A,B),B) = ld(A,unit),
inference(paramod,[status(thm)],[c_6470,c_14]) ).
cnf(c_9509,plain,
mult(mult(A,mult(B,f(C))),mult(f(C),ld(mult(B,f(C)),rd(mult(B,C),mult(B,f(C)))))) = mult(mult(A,mult(B,C)),ld(mult(B,f(C)),rd(mult(B,C),mult(B,f(C))))),
inference(paramod,[status(thm)],[c_649,c_97]) ).
cnf(c_9510,plain,
mult(mult(A,mult(B,f(C))),mult(f(C),rd(f(C),mult(B,f(C))))) = mult(mult(A,mult(B,C)),ld(mult(B,f(C)),rd(mult(B,C),mult(B,f(C))))),
inference(paramod,[status(thm)],[c_745,c_9509]) ).
cnf(c_8202,plain,
mult(mult(A,mult(B,f(C))),mult(f(C),rd(f(C),mult(B,f(C))))) = mult(mult(A,mult(B,C)),rd(f(C),mult(B,f(C)))),
inference(paramod,[status(thm)],[c_745,c_9510]) ).
cnf(c_8247,plain,
rd(A,mult(B,A)) = ld(B,unit),
inference(paramod,[status(thm)],[c_12,c_7649]) ).
cnf(c_9511,plain,
rd(A,B) = ld(rd(B,A),unit),
inference(paramod,[status(thm)],[c_27,c_7649]) ).
cnf(c_8248,plain,
ld(rd(A,B),unit) = rd(B,A),
inference(copy,[status(thm)],[c_9511]) ).
cnf(c_9512,plain,
rd(f(A),rd(B,f(A))) = ld(rd(B,A),unit),
inference(paramod,[status(thm)],[c_614,c_7649]) ).
cnf(c_8257,plain,
rd(f(A),rd(B,f(A))) = rd(A,B),
inference(paramod,[status(thm)],[c_8248,c_9512]) ).
cnf(c_9513,plain,
mult(mult(A,mult(B,f(C))),mult(f(C),ld(B,unit))) = mult(mult(A,mult(B,C)),rd(f(C),mult(B,f(C)))),
inference(paramod,[status(thm)],[c_8247,c_8202]) ).
cnf(c_9514,plain,
mult(mult(A,mult(B,f(C))),rd(f(C),B)) = mult(mult(A,mult(B,C)),rd(f(C),mult(B,f(C)))),
inference(paramod,[status(thm)],[c_2276,c_9513]) ).
cnf(c_9515,plain,
mult(mult(A,B),mult(f(C),rd(f(C),B))) = mult(mult(A,mult(B,C)),rd(f(C),mult(B,f(C)))),
inference(paramod,[status(thm)],[c_44,c_9514]) ).
cnf(c_9516,plain,
mult(mult(A,B),mult(f(C),rd(f(C),B))) = mult(mult(A,mult(B,C)),ld(B,unit)),
inference(paramod,[status(thm)],[c_8247,c_9515]) ).
cnf(c_8294,plain,
mult(mult(A,B),mult(f(C),rd(f(C),B))) = rd(mult(A,mult(B,C)),B),
inference(paramod,[status(thm)],[c_2276,c_9516]) ).
cnf(c_9517,plain,
mult(A,rd(B,C)) = rd(A,rd(C,B)),
inference(paramod,[status(thm)],[c_8248,c_2276]) ).
cnf(c_8882,plain,
rd(A,rd(B,C)) = mult(A,rd(C,B)),
inference(copy,[status(thm)],[c_9517]) ).
cnf(c_8985,plain,
mult(f(A),rd(f(A),B)) = rd(A,B),
inference(paramod,[status(thm)],[c_8882,c_8257]) ).
cnf(c_9518,plain,
mult(mult(A,B),rd(C,B)) = rd(mult(A,mult(B,C)),B),
inference(paramod,[status(thm)],[c_8985,c_8294]) ).
cnf(c_9289,plain,
rd(mult(A,mult(B,C)),B) = mult(mult(A,B),rd(C,B)),
inference(copy,[status(thm)],[c_9518]) ).
cnf(c_9519,plain,
mult(mult(mult(A,B),C),rd(mult(B,C),C)) = mult(A,mult(B,mult(C,B))),
inference(paramod,[status(thm)],[c_9289,c_47]) ).
cnf(c_9396,plain,
mult(mult(mult(A,B),C),B) = mult(A,mult(B,mult(C,B))),
inference(paramod,[status(thm)],[c_14,c_9519]) ).
cnf(c_9397,plain,
$false,
inference(resolve,[status(thm)],[c_9396,c_22]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRP667+6 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/5.45 % Computer : n020.cluster.edu
% 0.19/5.45 % Model : x86_64 x86_64
% 0.19/5.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/5.45 % Memory : 8046.5625MB
% 0.19/5.45 % OS : Linux 6.8.0-71-generic
% 0.19/5.45 % CPULimit : 300
% 0.19/5.45 % WCLimit : 300
% 0.19/5.45 % DateTime : Fri Sep 25 15:35:40 UTC 2026
% 0.19/5.45 % CPUTime :
% 0.19/5.46 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.19/5.46 % Process 3270472 was started by sandbox2 on n020,
% 0.19/5.46 % Fri Sep 25 15:35:40 2026
% 0.19/5.46 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.19/5.46
% 0.19/5.46 % From the command line: assign(max_seconds, 300).
% 25.59/9.12
% 25.59/9.12 % Assigning unary symbol f kb_weight 0 and highest precedence (18).
% 25.59/9.12
% 25.59/9.12 % SZS status Theorem for theBenchmark
% 25.59/9.12
% 25.59/9.12 % Proof 1 at 2.69 (+ 0.74) seconds.
% 25.59/9.12 % Length of proof is 120.
% 25.59/9.12 % Level of proof is 29.
% 25.59/9.12 % Maximum clause weight is 86.000.
% 25.59/9.12 % Given clauses 249.
% 25.59/9.12
% 25.59/9.12 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------