%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP755-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 : n018.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 21.98s 3.23s
% Output : CNFRefutation 21.98s
% Verified :
% SZS Type : Refutation
% Derivation depth : 96
% Number of leaves : 10
% Syntax : Number of formulae : 216 ( 92 unt; 0 def)
% Number of atoms : 355 ( 354 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 147 ( 8 ~; 139 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 2 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 3 con; 0-2 aty)
% Number of variables : 299 ( 0 sgn 17 !; 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] : mult(VAR_0,unit) = VAR_0,
file('theBenchmark.p',f05) ).
cnf(c_5,plain,
mult(A,unit) = A,
inference(clausify,[status(thm)],[f05]) ).
fof(f06,axiom,
! [VAR_0] : mult(unit,VAR_0) = VAR_0,
file('theBenchmark.p',f06) ).
cnf(c_6,plain,
mult(unit,A) = A,
inference(clausify,[status(thm)],[f06]) ).
fof(f07,axiom,
! [VAR_0,VAR_1,VAR_2] :
( mult(VAR_0,mult(VAR_1,VAR_2)) = mult(mult(VAR_0,VAR_2),VAR_1)
| mult(VAR_0,mult(VAR_1,VAR_2)) = mult(mult(VAR_0,VAR_1),VAR_2) ),
file('theBenchmark.p',f07) ).
cnf(c_7,plain,
( mult(A,mult(B,C)) = mult(mult(A,C),B)
| mult(A,mult(B,C)) = mult(mult(A,B),C) ),
inference(clausify,[status(thm)],[f07]) ).
cnf(c_8064,plain,
( mult(A,mult(B,C)) = mult(mult(A,C),B)
| mult(mult(A,B),C) = mult(A,mult(B,C)) ),
inference(copy,[status(thm)],[c_7]) ).
cnf(c_8,plain,
( mult(mult(A,C),B) = mult(A,mult(B,C))
| mult(mult(A,B),C) = mult(A,mult(B,C)) ),
inference(copy,[status(thm)],[c_8064]) ).
fof(f08,axiom,
! [VAR_0,VAR_1,VAR_2] :
( mult(VAR_0,mult(VAR_2,VAR_1)) = mult(mult(VAR_0,VAR_1),VAR_2)
| mult(VAR_0,mult(VAR_1,VAR_2)) = mult(mult(VAR_0,VAR_1),VAR_2) ),
file('theBenchmark.p',f08) ).
cnf(c_9,plain,
( mult(A,mult(C,B)) = mult(mult(A,B),C)
| mult(A,mult(B,C)) = mult(mult(A,B),C) ),
inference(clausify,[status(thm)],[f08]) ).
cnf(c_8065,plain,
( mult(A,mult(C,B)) = mult(mult(A,B),C)
| mult(mult(A,B),C) = mult(A,mult(B,C)) ),
inference(copy,[status(thm)],[c_9]) ).
cnf(c_10,plain,
( mult(mult(A,B),C) = mult(A,mult(C,B))
| mult(mult(A,B),C) = mult(A,mult(B,C)) ),
inference(copy,[status(thm)],[c_8065]) ).
fof(f09,axiom,
! [VAR_0] : i(VAR_0) = ld(VAR_0,unit),
file('theBenchmark.p',f09) ).
cnf(c_11,plain,
i(A) = ld(A,unit),
inference(clausify,[status(thm)],[f09]) ).
fof(goals,axiom,
i(mult(a,b)) != mult(i(b),i(a)),
file('theBenchmark.p',goals) ).
cnf(c_12,plain,
i(mult(a,b)) != mult(i(b),i(a)),
inference(clausify,[status(thm)],[goals]) ).
cnf(c_8066,plain,
ld(mult(a,b),unit) != mult(i(b),i(a)),
inference(paramod,[status(thm)],[c_11,c_12]) ).
cnf(c_8067,plain,
ld(mult(a,b),unit) != mult(ld(b,unit),i(a)),
inference(paramod,[status(thm)],[c_11,c_8066]) ).
cnf(c_8068,plain,
ld(mult(a,b),unit) != mult(ld(b,unit),ld(a,unit)),
inference(paramod,[status(thm)],[c_11,c_8067]) ).
cnf(c_13,plain,
mult(ld(b,unit),ld(a,unit)) != ld(mult(a,b),unit),
inference(copy,[status(thm)],[c_8068]) ).
cnf(c_14,plain,
mult(mult(A,B),B) = mult(A,mult(B,B)),
inference(factor,[status(thm)],[c_8]) ).
cnf(c_15,plain,
ld(rd(A,B),A) = B,
inference(paramod,[status(thm)],[c_3,c_2]) ).
cnf(c_16,plain,
rd(A,ld(B,A)) = B,
inference(paramod,[status(thm)],[c_1,c_4]) ).
cnf(c_17,plain,
ld(A,A) = unit,
inference(paramod,[status(thm)],[c_5,c_2]) ).
cnf(c_19,plain,
ld(unit,A) = A,
inference(paramod,[status(thm)],[c_6,c_1]) ).
cnf(c_22,plain,
( mult(A,mult(ld(mult(A,B),C),B)) = C
| mult(mult(A,ld(mult(A,B),C)),B) = mult(A,mult(ld(mult(A,B),C),B)) ),
inference(paramod,[status(thm)],[c_8,c_1]) ).
cnf(c_8069,plain,
( mult(mult(A,ld(B,C)),B) = mult(A,mult(B,ld(B,C)))
| mult(mult(A,B),ld(B,C)) = mult(A,C) ),
inference(paramod,[status(thm)],[c_1,c_8]) ).
cnf(c_24,plain,
( mult(mult(A,ld(B,C)),B) = mult(A,C)
| mult(mult(A,B),ld(B,C)) = mult(A,C) ),
inference(paramod,[status(thm)],[c_1,c_8069]) ).
cnf(c_8070,plain,
( mult(C,B) = mult(A,mult(B,ld(A,C)))
| mult(mult(A,B),ld(A,C)) = mult(A,mult(B,ld(A,C))) ),
inference(paramod,[status(thm)],[c_1,c_8]) ).
cnf(c_25,plain,
( mult(A,mult(B,ld(A,C))) = mult(C,B)
| mult(mult(A,B),ld(A,C)) = mult(A,mult(B,ld(A,C))) ),
inference(copy,[status(thm)],[c_8070]) ).
cnf(c_8071,plain,
( mult(mult(C,ld(C,A)),B) = mult(C,mult(B,ld(C,A)))
| mult(A,B) = mult(C,mult(ld(C,A),B)) ),
inference(paramod,[status(thm)],[c_1,c_10]) ).
cnf(c_8072,plain,
( mult(A,B) = mult(C,mult(B,ld(C,A)))
| mult(A,B) = mult(C,mult(ld(C,A),B)) ),
inference(paramod,[status(thm)],[c_1,c_8071]) ).
cnf(c_8073,plain,
( mult(A,B) = mult(C,mult(B,ld(C,A)))
| mult(C,mult(ld(C,A),B)) = mult(A,B) ),
inference(copy,[status(thm)],[c_8072]) ).
cnf(c_35,plain,
( mult(A,mult(C,ld(A,B))) = mult(B,C)
| mult(A,mult(ld(A,B),C)) = mult(B,C) ),
inference(copy,[status(thm)],[c_8073]) ).
cnf(c_8074,plain,
( mult(mult(rd(A,C),C),B) = mult(rd(A,C),mult(B,C))
| mult(A,B) = mult(rd(A,C),mult(C,B)) ),
inference(paramod,[status(thm)],[c_3,c_10]) ).
cnf(c_8075,plain,
( mult(A,B) = mult(rd(A,C),mult(B,C))
| mult(A,B) = mult(rd(A,C),mult(C,B)) ),
inference(paramod,[status(thm)],[c_3,c_8074]) ).
cnf(c_8076,plain,
( mult(A,B) = mult(rd(A,C),mult(B,C))
| mult(rd(A,C),mult(C,B)) = mult(A,B) ),
inference(copy,[status(thm)],[c_8075]) ).
cnf(c_40,plain,
( mult(rd(A,B),mult(C,B)) = mult(A,C)
| mult(rd(A,B),mult(B,C)) = mult(A,C) ),
inference(copy,[status(thm)],[c_8076]) ).
cnf(c_43,plain,
( mult(mult(A,B),rd(C,B)) = mult(A,C)
| mult(mult(A,B),rd(C,B)) = mult(A,mult(B,rd(C,B))) ),
inference(paramod,[status(thm)],[c_3,c_10]) ).
cnf(c_48,plain,
mult(rd(A,B),mult(B,B)) = mult(A,B),
inference(factor,[status(thm)],[c_40]) ).
cnf(c_49,plain,
ld(mult(A,B),mult(A,mult(B,B))) = B,
inference(paramod,[status(thm)],[c_14,c_2]) ).
cnf(c_64,plain,
ld(rd(A,B),mult(A,B)) = mult(B,B),
inference(paramod,[status(thm)],[c_48,c_2]) ).
cnf(c_65,plain,
rd(mult(A,B),mult(B,B)) = rd(A,B),
inference(paramod,[status(thm)],[c_48,c_4]) ).
cnf(c_86,plain,
ld(rd(unit,A),A) = mult(A,A),
inference(paramod,[status(thm)],[c_6,c_64]) ).
cnf(c_91,plain,
ld(A,mult(B,ld(A,B))) = mult(ld(A,B),ld(A,B)),
inference(paramod,[status(thm)],[c_16,c_64]) ).
cnf(c_94,plain,
rd(A,mult(A,A)) = rd(unit,A),
inference(paramod,[status(thm)],[c_86,c_16]) ).
cnf(c_8077,plain,
ld(A,ld(A,unit)) = mult(ld(A,unit),ld(A,unit)),
inference(paramod,[status(thm)],[c_16,c_86]) ).
cnf(c_95,plain,
mult(ld(A,unit),ld(A,unit)) = ld(A,ld(A,unit)),
inference(copy,[status(thm)],[c_8077]) ).
cnf(c_101,plain,
rd(A,mult(ld(B,A),ld(B,A))) = rd(B,ld(B,A)),
inference(paramod,[status(thm)],[c_1,c_65]) ).
cnf(c_159,plain,
mult(rd(A,ld(B,unit)),ld(B,ld(B,unit))) = mult(A,ld(B,unit)),
inference(paramod,[status(thm)],[c_95,c_48]) ).
cnf(c_8078,plain,
rd(mult(ld(A,unit),ld(A,unit)),mult(mult(ld(A,unit),ld(A,unit)),mult(ld(A,unit),ld(A,unit)))) = rd(A,ld(A,unit)),
inference(paramod,[status(thm)],[c_101,c_94]) ).
cnf(c_8079,plain,
rd(ld(A,ld(A,unit)),mult(mult(ld(A,unit),ld(A,unit)),mult(ld(A,unit),ld(A,unit)))) = rd(A,ld(A,unit)),
inference(paramod,[status(thm)],[c_95,c_8078]) ).
cnf(c_8080,plain,
rd(ld(A,ld(A,unit)),mult(ld(A,ld(A,unit)),mult(ld(A,unit),ld(A,unit)))) = rd(A,ld(A,unit)),
inference(paramod,[status(thm)],[c_95,c_8079]) ).
cnf(c_8081,plain,
rd(ld(A,ld(A,unit)),mult(ld(A,ld(A,unit)),ld(A,ld(A,unit)))) = rd(A,ld(A,unit)),
inference(paramod,[status(thm)],[c_95,c_8080]) ).
cnf(c_174,plain,
rd(unit,ld(A,ld(A,unit))) = rd(A,ld(A,unit)),
inference(paramod,[status(thm)],[c_94,c_8081]) ).
cnf(c_235,plain,
( mult(B,A) = mult(A,B)
| mult(mult(A,A),ld(A,B)) = mult(A,B) ),
inference(paramod,[status(thm)],[c_1,c_24]) ).
cnf(c_264,plain,
( rd(mult(B,A),ld(B,A)) = mult(B,B)
| mult(A,B) = mult(B,A) ),
inference(paramod,[status(thm)],[c_235,c_4]) ).
cnf(c_8082,plain,
( rd(mult(rd(unit,A),A),mult(A,A)) = mult(rd(unit,A),rd(unit,A))
| mult(A,rd(unit,A)) = mult(rd(unit,A),A) ),
inference(paramod,[status(thm)],[c_86,c_264]) ).
cnf(c_8083,plain,
( rd(mult(rd(unit,A),A),mult(A,A)) = mult(rd(unit,A),rd(unit,A))
| mult(A,rd(unit,A)) = unit ),
inference(paramod,[status(thm)],[c_3,c_8082]) ).
cnf(c_8084,plain,
( rd(unit,mult(A,A)) = mult(rd(unit,A),rd(unit,A))
| mult(A,rd(unit,A)) = unit ),
inference(paramod,[status(thm)],[c_3,c_8083]) ).
cnf(c_341,plain,
( mult(rd(unit,A),rd(unit,A)) = rd(unit,mult(A,A))
| mult(A,rd(unit,A)) = unit ),
inference(copy,[status(thm)],[c_8084]) ).
cnf(c_8085,plain,
( mult(A,rd(unit,ld(A,unit))) = rd(unit,mult(ld(A,unit),ld(A,unit)))
| mult(ld(A,unit),rd(unit,ld(A,unit))) = unit ),
inference(paramod,[status(thm)],[c_16,c_341]) ).
cnf(c_8086,plain,
( mult(A,rd(unit,ld(A,unit))) = rd(unit,mult(ld(A,unit),ld(A,unit)))
| mult(ld(A,unit),A) = unit ),
inference(paramod,[status(thm)],[c_16,c_8085]) ).
cnf(c_8087,plain,
( mult(A,A) = rd(unit,mult(ld(A,unit),ld(A,unit)))
| mult(ld(A,unit),A) = unit ),
inference(paramod,[status(thm)],[c_16,c_8086]) ).
cnf(c_8088,plain,
( mult(A,A) = rd(unit,ld(A,ld(A,unit)))
| mult(ld(A,unit),A) = unit ),
inference(paramod,[status(thm)],[c_95,c_8087]) ).
cnf(c_8089,plain,
( mult(A,A) = rd(A,ld(A,unit))
| mult(ld(A,unit),A) = unit ),
inference(paramod,[status(thm)],[c_174,c_8088]) ).
cnf(c_362,plain,
( rd(A,ld(A,unit)) = mult(A,A)
| mult(ld(A,unit),A) = unit ),
inference(copy,[status(thm)],[c_8089]) ).
cnf(c_387,plain,
( ld(mult(A,A),A) = ld(A,unit)
| mult(ld(A,unit),A) = unit ),
inference(paramod,[status(thm)],[c_362,c_15]) ).
cnf(c_8090,plain,
( mult(mult(B,A),ld(A,unit)) = mult(B,unit)
| mult(mult(B,A),ld(A,unit)) = mult(B,mult(A,ld(A,unit)))
| ld(mult(A,A),A) = ld(A,unit) ),
inference(paramod,[status(thm)],[c_387,c_10]) ).
cnf(c_8091,plain,
( mult(mult(B,A),ld(A,unit)) = mult(B,unit)
| mult(mult(B,A),ld(A,unit)) = mult(B,unit)
| ld(mult(A,A),A) = ld(A,unit) ),
inference(paramod,[status(thm)],[c_1,c_8090]) ).
cnf(c_8092,plain,
( mult(mult(B,A),ld(A,unit)) = mult(B,unit)
| mult(mult(B,A),ld(A,unit)) = B
| ld(mult(A,A),A) = ld(A,unit) ),
inference(paramod,[status(thm)],[c_5,c_8091]) ).
cnf(c_8093,plain,
( mult(mult(B,A),ld(A,unit)) = B
| mult(mult(B,A),ld(A,unit)) = B
| ld(mult(A,A),A) = ld(A,unit) ),
inference(paramod,[status(thm)],[c_5,c_8092]) ).
cnf(c_404,plain,
( mult(mult(B,A),ld(A,unit)) = B
| ld(mult(A,A),A) = ld(A,unit) ),
inference(copy,[status(thm)],[c_8093]) ).
cnf(c_8094,plain,
( mult(rd(mult(A,B),ld(A,unit)),ld(A,ld(A,unit))) = mult(A,mult(B,ld(A,unit)))
| mult(A,mult(B,ld(A,unit))) = mult(unit,B) ),
inference(paramod,[status(thm)],[c_25,c_159]) ).
cnf(c_8095,plain,
( mult(rd(mult(A,B),ld(A,unit)),ld(A,ld(A,unit))) = mult(A,mult(B,ld(A,unit)))
| mult(A,mult(B,ld(A,unit))) = B ),
inference(paramod,[status(thm)],[c_6,c_8094]) ).
cnf(c_452,plain,
( mult(mult(A,B),ld(A,unit)) = mult(A,mult(B,ld(A,unit)))
| mult(A,mult(B,ld(A,unit))) = B ),
inference(paramod,[status(thm)],[c_159,c_8095]) ).
cnf(c_877,plain,
( ld(mult(B,A),B) = ld(A,unit)
| ld(mult(A,A),A) = ld(A,unit) ),
inference(paramod,[status(thm)],[c_404,c_2]) ).
cnf(c_914,plain,
ld(mult(A,A),A) = ld(A,unit),
inference(factor,[status(thm)],[c_877]) ).
cnf(c_8096,plain,
( mult(A,mult(ld(mult(A,A),A),A)) = A
| mult(mult(A,ld(A,unit)),A) = mult(A,mult(ld(mult(A,A),A),A)) ),
inference(paramod,[status(thm)],[c_914,c_22]) ).
cnf(c_8097,plain,
( mult(A,mult(ld(mult(A,A),A),A)) = A
| mult(unit,A) = mult(A,mult(ld(mult(A,A),A),A)) ),
inference(paramod,[status(thm)],[c_1,c_8096]) ).
cnf(c_8098,plain,
( mult(A,mult(ld(mult(A,A),A),A)) = A
| A = mult(A,mult(ld(mult(A,A),A),A)) ),
inference(paramod,[status(thm)],[c_6,c_8097]) ).
cnf(c_8099,plain,
( mult(A,mult(ld(mult(A,A),A),A)) = A
| A = mult(A,mult(ld(A,unit),A)) ),
inference(paramod,[status(thm)],[c_914,c_8098]) ).
cnf(c_8100,plain,
( mult(A,mult(ld(A,unit),A)) = A
| A = mult(A,mult(ld(A,unit),A)) ),
inference(paramod,[status(thm)],[c_914,c_8099]) ).
cnf(c_8101,plain,
( mult(A,mult(ld(A,unit),A)) = A
| mult(A,mult(ld(A,unit),A)) = A ),
inference(copy,[status(thm)],[c_8100]) ).
cnf(c_970,plain,
mult(A,mult(ld(A,unit),A)) = A,
inference(copy,[status(thm)],[c_8101]) ).
cnf(c_8102,plain,
ld(mult(A,A),mult(A,ld(A,unit))) = mult(ld(mult(A,A),A),ld(mult(A,A),A)),
inference(paramod,[status(thm)],[c_914,c_91]) ).
cnf(c_8103,plain,
ld(mult(A,A),unit) = mult(ld(mult(A,A),A),ld(mult(A,A),A)),
inference(paramod,[status(thm)],[c_1,c_8102]) ).
cnf(c_8104,plain,
ld(mult(A,A),unit) = mult(ld(A,unit),ld(mult(A,A),A)),
inference(paramod,[status(thm)],[c_914,c_8103]) ).
cnf(c_8105,plain,
ld(mult(A,A),unit) = mult(ld(A,unit),ld(A,unit)),
inference(paramod,[status(thm)],[c_914,c_8104]) ).
cnf(c_974,plain,
ld(mult(A,A),unit) = ld(A,ld(A,unit)),
inference(paramod,[status(thm)],[c_95,c_8105]) ).
cnf(c_8106,plain,
ld(A,A) = mult(ld(A,unit),A),
inference(paramod,[status(thm)],[c_970,c_2]) ).
cnf(c_8107,plain,
unit = mult(ld(A,unit),A),
inference(paramod,[status(thm)],[c_17,c_8106]) ).
cnf(c_1099,plain,
mult(ld(A,unit),A) = unit,
inference(copy,[status(thm)],[c_8107]) ).
cnf(c_1105,plain,
rd(unit,A) = ld(A,unit),
inference(paramod,[status(thm)],[c_1099,c_4]) ).
cnf(c_8108,plain,
( mult(mult(A,B),ld(B,unit)) = mult(A,unit)
| mult(mult(A,B),ld(B,unit)) = mult(A,mult(B,ld(B,unit))) ),
inference(paramod,[status(thm)],[c_1099,c_10]) ).
cnf(c_8109,plain,
( mult(mult(A,B),ld(B,unit)) = mult(A,unit)
| mult(mult(A,B),ld(B,unit)) = mult(A,unit) ),
inference(paramod,[status(thm)],[c_1,c_8108]) ).
cnf(c_8110,plain,
( mult(mult(A,B),ld(B,unit)) = mult(A,unit)
| mult(mult(A,B),ld(B,unit)) = A ),
inference(paramod,[status(thm)],[c_5,c_8109]) ).
cnf(c_8111,plain,
( mult(mult(A,B),ld(B,unit)) = A
| mult(mult(A,B),ld(B,unit)) = A ),
inference(paramod,[status(thm)],[c_5,c_8110]) ).
cnf(c_1112,plain,
mult(mult(A,B),ld(B,unit)) = A,
inference(copy,[status(thm)],[c_8111]) ).
cnf(c_8112,plain,
rd(unit,mult(A,A)) = rd(ld(A,unit),A),
inference(paramod,[status(thm)],[c_1099,c_65]) ).
cnf(c_8113,plain,
ld(mult(A,A),unit) = rd(ld(A,unit),A),
inference(paramod,[status(thm)],[c_1105,c_8112]) ).
cnf(c_8114,plain,
ld(A,ld(A,unit)) = rd(ld(A,unit),A),
inference(paramod,[status(thm)],[c_974,c_8113]) ).
cnf(c_1117,plain,
rd(ld(A,unit),A) = ld(A,ld(A,unit)),
inference(copy,[status(thm)],[c_8114]) ).
cnf(c_1177,plain,
ld(mult(A,B),A) = ld(B,unit),
inference(paramod,[status(thm)],[c_1112,c_2]) ).
cnf(c_1178,plain,
mult(A,ld(B,unit)) = rd(A,B),
inference(paramod,[status(thm)],[c_3,c_1112]) ).
cnf(c_8115,plain,
mult(A,ld(B,unit)) = mult(mult(A,B),mult(ld(B,unit),ld(B,unit))),
inference(paramod,[status(thm)],[c_1112,c_14]) ).
cnf(c_8116,plain,
rd(A,B) = mult(mult(A,B),mult(ld(B,unit),ld(B,unit))),
inference(paramod,[status(thm)],[c_1178,c_8115]) ).
cnf(c_8117,plain,
rd(A,B) = mult(mult(A,B),rd(ld(B,unit),B)),
inference(paramod,[status(thm)],[c_1178,c_8116]) ).
cnf(c_8118,plain,
rd(A,B) = mult(mult(A,B),ld(B,ld(B,unit))),
inference(paramod,[status(thm)],[c_1117,c_8117]) ).
cnf(c_1186,plain,
mult(mult(A,B),ld(B,ld(B,unit))) = rd(A,B),
inference(copy,[status(thm)],[c_8118]) ).
cnf(c_8119,plain,
ld(A,mult(mult(A,B),mult(ld(B,unit),ld(B,unit)))) = ld(B,unit),
inference(paramod,[status(thm)],[c_1112,c_49]) ).
cnf(c_8120,plain,
ld(A,mult(mult(A,B),rd(ld(B,unit),B))) = ld(B,unit),
inference(paramod,[status(thm)],[c_1178,c_8119]) ).
cnf(c_8121,plain,
ld(A,mult(mult(A,B),ld(B,ld(B,unit)))) = ld(B,unit),
inference(paramod,[status(thm)],[c_1117,c_8120]) ).
cnf(c_1191,plain,
ld(A,rd(A,B)) = ld(B,unit),
inference(paramod,[status(thm)],[c_1186,c_8121]) ).
cnf(c_8122,plain,
( mult(mult(A,B),ld(A,unit)) = mult(A,mult(B,ld(A,unit)))
| mult(A,rd(B,A)) = B ),
inference(paramod,[status(thm)],[c_1178,c_452]) ).
cnf(c_8123,plain,
( rd(mult(A,B),A) = mult(A,mult(B,ld(A,unit)))
| mult(A,rd(B,A)) = B ),
inference(paramod,[status(thm)],[c_1178,c_8122]) ).
cnf(c_1220,plain,
( rd(mult(A,B),A) = mult(A,rd(B,A))
| mult(A,rd(B,A)) = B ),
inference(paramod,[status(thm)],[c_1178,c_8123]) ).
cnf(c_1238,plain,
rd(ld(b,unit),a) != ld(mult(a,b),unit),
inference(paramod,[status(thm)],[c_1178,c_13]) ).
cnf(c_8124,plain,
ld(A,B) = ld(ld(B,A),unit),
inference(paramod,[status(thm)],[c_1,c_1177]) ).
cnf(c_1244,plain,
ld(ld(A,B),unit) = ld(B,A),
inference(copy,[status(thm)],[c_8124]) ).
cnf(c_8125,plain,
mult(A,ld(B,C)) = rd(A,ld(C,B)),
inference(paramod,[status(thm)],[c_1244,c_1178]) ).
cnf(c_1357,plain,
rd(A,ld(B,C)) = mult(A,ld(C,B)),
inference(copy,[status(thm)],[c_8125]) ).
cnf(c_8126,plain,
( mult(A,mult(B,ld(A,unit))) = mult(unit,B)
| mult(A,mult(ld(A,unit),B)) = B ),
inference(paramod,[status(thm)],[c_6,c_35]) ).
cnf(c_8127,plain,
( mult(A,rd(B,A)) = mult(unit,B)
| mult(A,mult(ld(A,unit),B)) = B ),
inference(paramod,[status(thm)],[c_1178,c_8126]) ).
cnf(c_2393,plain,
( mult(A,rd(B,A)) = B
| mult(A,mult(ld(A,unit),B)) = B ),
inference(paramod,[status(thm)],[c_6,c_8127]) ).
cnf(c_8128,plain,
( ld(A,B) = mult(ld(A,unit),B)
| mult(A,rd(B,A)) = B ),
inference(paramod,[status(thm)],[c_2393,c_2]) ).
cnf(c_3019,plain,
( mult(ld(A,unit),B) = ld(A,B)
| mult(A,rd(B,A)) = B ),
inference(copy,[status(thm)],[c_8128]) ).
cnf(c_8129,plain,
( ld(A,B) = rd(B,A)
| mult(ld(A,unit),B) = ld(A,B) ),
inference(paramod,[status(thm)],[c_3019,c_2]) ).
cnf(c_3075,plain,
( rd(B,A) = ld(A,B)
| mult(ld(A,unit),B) = ld(A,B) ),
inference(copy,[status(thm)],[c_8129]) ).
cnf(c_3250,plain,
( rd(ld(B,A),A) = ld(B,unit)
| rd(A,B) = ld(B,A) ),
inference(paramod,[status(thm)],[c_3075,c_4]) ).
cnf(c_8130,plain,
( rd(B,mult(A,B)) = ld(A,unit)
| rd(mult(A,B),A) = ld(A,mult(A,B)) ),
inference(paramod,[status(thm)],[c_2,c_3250]) ).
cnf(c_3472,plain,
( rd(B,mult(A,B)) = ld(A,unit)
| rd(mult(A,B),A) = B ),
inference(paramod,[status(thm)],[c_2,c_8130]) ).
cnf(c_3520,plain,
( mult(A,B) = mult(B,A)
| rd(A,mult(B,A)) = ld(B,unit) ),
inference(paramod,[status(thm)],[c_3472,c_3]) ).
cnf(c_3529,plain,
( ld(A,mult(B,A)) = B
| rd(A,mult(B,A)) = ld(B,unit) ),
inference(paramod,[status(thm)],[c_3472,c_15]) ).
cnf(c_8131,plain,
( mult(A,rd(B,A)) = mult(rd(B,A),A)
| rd(A,B) = ld(rd(B,A),unit) ),
inference(paramod,[status(thm)],[c_3,c_3520]) ).
cnf(c_8132,plain,
( mult(A,rd(B,A)) = B
| rd(A,B) = ld(rd(B,A),unit) ),
inference(paramod,[status(thm)],[c_3,c_8131]) ).
cnf(c_3696,plain,
( mult(B,rd(A,B)) = A
| ld(rd(A,B),unit) = rd(B,A) ),
inference(copy,[status(thm)],[c_8132]) ).
cnf(c_8133,plain,
( ld(A,mult(rd(B,A),A)) = rd(B,A)
| rd(A,B) = ld(rd(B,A),unit) ),
inference(paramod,[status(thm)],[c_3,c_3529]) ).
cnf(c_8134,plain,
( ld(A,B) = rd(B,A)
| rd(A,B) = ld(rd(B,A),unit) ),
inference(paramod,[status(thm)],[c_3,c_8133]) ).
cnf(c_8135,plain,
( ld(A,B) = rd(B,A)
| ld(rd(B,A),unit) = rd(A,B) ),
inference(copy,[status(thm)],[c_8134]) ).
cnf(c_3755,plain,
( rd(A,B) = ld(B,A)
| ld(rd(A,B),unit) = rd(B,A) ),
inference(copy,[status(thm)],[c_8135]) ).
cnf(c_8136,plain,
( ld(A,B) = ld(rd(A,B),unit)
| ld(rd(A,B),unit) = rd(B,A) ),
inference(paramod,[status(thm)],[c_3696,c_1177]) ).
cnf(c_4108,plain,
( ld(rd(A,B),unit) = ld(A,B)
| ld(rd(A,B),unit) = rd(B,A) ),
inference(copy,[status(thm)],[c_8136]) ).
cnf(c_8137,plain,
( mult(B,rd(rd(A,ld(B,unit)),B)) = rd(A,ld(B,unit))
| mult(B,A) = rd(A,ld(B,unit))
| ld(rd(A,ld(B,unit)),unit) = rd(ld(B,unit),A) ),
inference(paramod,[status(thm)],[c_3696,c_2393]) ).
cnf(c_8138,plain,
( mult(B,rd(rd(A,ld(B,unit)),B)) = rd(A,ld(B,unit))
| mult(B,A) = rd(A,ld(B,unit))
| ld(mult(A,ld(unit,B)),unit) = rd(ld(B,unit),A) ),
inference(paramod,[status(thm)],[c_1357,c_8137]) ).
cnf(c_8139,plain,
( mult(B,rd(rd(A,ld(B,unit)),B)) = rd(A,ld(B,unit))
| mult(B,A) = rd(A,ld(B,unit))
| ld(mult(A,B),unit) = rd(ld(B,unit),A) ),
inference(paramod,[status(thm)],[c_19,c_8138]) ).
cnf(c_8140,plain,
( mult(B,rd(rd(A,ld(B,unit)),B)) = rd(A,ld(B,unit))
| mult(B,A) = mult(A,ld(unit,B))
| ld(mult(A,B),unit) = rd(ld(B,unit),A) ),
inference(paramod,[status(thm)],[c_1357,c_8139]) ).
cnf(c_8141,plain,
( mult(B,rd(rd(A,ld(B,unit)),B)) = rd(A,ld(B,unit))
| mult(B,A) = mult(A,B)
| ld(mult(A,B),unit) = rd(ld(B,unit),A) ),
inference(paramod,[status(thm)],[c_19,c_8140]) ).
cnf(c_8142,plain,
( mult(B,rd(mult(A,ld(unit,B)),B)) = rd(A,ld(B,unit))
| mult(B,A) = mult(A,B)
| ld(mult(A,B),unit) = rd(ld(B,unit),A) ),
inference(paramod,[status(thm)],[c_1357,c_8141]) ).
cnf(c_8143,plain,
( mult(B,rd(mult(A,B),B)) = rd(A,ld(B,unit))
| mult(B,A) = mult(A,B)
| ld(mult(A,B),unit) = rd(ld(B,unit),A) ),
inference(paramod,[status(thm)],[c_19,c_8142]) ).
cnf(c_8144,plain,
( mult(B,A) = rd(A,ld(B,unit))
| mult(B,A) = mult(A,B)
| ld(mult(A,B),unit) = rd(ld(B,unit),A) ),
inference(paramod,[status(thm)],[c_4,c_8143]) ).
cnf(c_8145,plain,
( mult(B,A) = mult(A,ld(unit,B))
| mult(B,A) = mult(A,B)
| ld(mult(A,B),unit) = rd(ld(B,unit),A) ),
inference(paramod,[status(thm)],[c_1357,c_8144]) ).
cnf(c_8146,plain,
( mult(B,A) = mult(A,B)
| mult(B,A) = mult(A,B)
| ld(mult(A,B),unit) = rd(ld(B,unit),A) ),
inference(paramod,[status(thm)],[c_19,c_8145]) ).
cnf(c_8147,plain,
( mult(B,A) = mult(A,B)
| mult(B,A) = mult(A,B)
| rd(ld(B,unit),A) = ld(mult(A,B),unit) ),
inference(copy,[status(thm)],[c_8146]) ).
cnf(c_4154,plain,
( mult(A,B) = mult(B,A)
| rd(ld(A,unit),B) = ld(mult(B,A),unit) ),
inference(copy,[status(thm)],[c_8147]) ).
cnf(c_8148,plain,
( ld(rd(B,A),unit) = ld(unit,rd(A,B))
| rd(A,B) = ld(B,A) ),
inference(paramod,[status(thm)],[c_3755,c_1244]) ).
cnf(c_4190,plain,
( ld(rd(B,A),unit) = rd(A,B)
| rd(A,B) = ld(B,A) ),
inference(paramod,[status(thm)],[c_19,c_8148]) ).
cnf(c_6365,plain,
mult(b,a) = mult(a,b),
inference(resolve,[status(thm)],[c_4154,c_1238]) ).
cnf(c_6458,plain,
rd(mult(a,b),a) = b,
inference(paramod,[status(thm)],[c_6365,c_4]) ).
cnf(c_8149,plain,
( rd(mult(a,b),b) = mult(b,rd(a,b))
| mult(b,rd(a,b)) = a ),
inference(paramod,[status(thm)],[c_6365,c_1220]) ).
cnf(c_8150,plain,
( a = mult(b,rd(a,b))
| mult(b,rd(a,b)) = a ),
inference(paramod,[status(thm)],[c_4,c_8149]) ).
cnf(c_8151,plain,
( mult(b,rd(a,b)) = a
| mult(b,rd(a,b)) = a ),
inference(copy,[status(thm)],[c_8150]) ).
cnf(c_6478,plain,
mult(b,rd(a,b)) = a,
inference(copy,[status(thm)],[c_8151]) ).
cnf(c_8152,plain,
( ld(b,unit) = rd(a,mult(a,b))
| rd(a,mult(a,b)) = ld(mult(a,b),a) ),
inference(paramod,[status(thm)],[c_6458,c_4190]) ).
cnf(c_8153,plain,
( ld(b,unit) = rd(a,mult(a,b))
| rd(a,mult(a,b)) = ld(b,unit) ),
inference(paramod,[status(thm)],[c_1177,c_8152]) ).
cnf(c_8154,plain,
( rd(a,mult(a,b)) = ld(b,unit)
| rd(a,mult(a,b)) = ld(b,unit) ),
inference(copy,[status(thm)],[c_8153]) ).
cnf(c_6519,plain,
rd(a,mult(a,b)) = ld(b,unit),
inference(copy,[status(thm)],[c_8154]) ).
cnf(c_8155,plain,
ld(b,a) = rd(a,b),
inference(paramod,[status(thm)],[c_6478,c_2]) ).
cnf(c_6520,plain,
rd(a,b) = ld(b,a),
inference(copy,[status(thm)],[c_8155]) ).
cnf(c_6523,plain,
mult(ld(b,a),b) = a,
inference(paramod,[status(thm)],[c_6520,c_3]) ).
cnf(c_8156,plain,
( ld(ld(b,a),unit) = rd(b,a)
| rd(b,a) = ld(a,b) ),
inference(paramod,[status(thm)],[c_6520,c_4190]) ).
cnf(c_8157,plain,
( ld(a,b) = rd(b,a)
| rd(b,a) = ld(a,b) ),
inference(paramod,[status(thm)],[c_1244,c_8156]) ).
cnf(c_8158,plain,
( rd(b,a) = ld(a,b)
| rd(b,a) = ld(a,b) ),
inference(copy,[status(thm)],[c_8157]) ).
cnf(c_6540,plain,
rd(b,a) = ld(a,b),
inference(copy,[status(thm)],[c_8158]) ).
cnf(c_8159,plain,
( mult(mult(A,a),rd(b,a)) = mult(A,b)
| mult(mult(A,a),ld(a,b)) = mult(A,mult(a,rd(b,a))) ),
inference(paramod,[status(thm)],[c_6540,c_43]) ).
cnf(c_8160,plain,
( mult(mult(A,a),rd(b,a)) = mult(A,b)
| mult(mult(A,a),ld(a,b)) = mult(A,mult(a,ld(a,b))) ),
inference(paramod,[status(thm)],[c_6540,c_8159]) ).
cnf(c_8161,plain,
( mult(mult(A,a),rd(b,a)) = mult(A,b)
| mult(mult(A,a),ld(a,b)) = mult(A,b) ),
inference(paramod,[status(thm)],[c_1,c_8160]) ).
cnf(c_8162,plain,
( mult(mult(A,a),ld(a,b)) = mult(A,b)
| mult(mult(A,a),ld(a,b)) = mult(A,b) ),
inference(paramod,[status(thm)],[c_6540,c_8161]) ).
cnf(c_6658,plain,
mult(mult(A,a),ld(a,b)) = mult(A,b),
inference(copy,[status(thm)],[c_8162]) ).
cnf(c_8163,plain,
( mult(rd(A,b),a) = mult(A,ld(b,a))
| mult(rd(A,b),mult(b,ld(b,a))) = mult(A,ld(b,a)) ),
inference(paramod,[status(thm)],[c_6523,c_40]) ).
cnf(c_8164,plain,
( mult(rd(A,b),a) = mult(A,ld(b,a))
| mult(rd(A,b),a) = mult(A,ld(b,a)) ),
inference(paramod,[status(thm)],[c_1,c_8163]) ).
cnf(c_6677,plain,
mult(rd(A,b),a) = mult(A,ld(b,a)),
inference(copy,[status(thm)],[c_8164]) ).
cnf(c_8165,plain,
ld(a,ld(b,unit)) = ld(mult(a,b),unit),
inference(paramod,[status(thm)],[c_6519,c_1191]) ).
cnf(c_6730,plain,
ld(mult(a,b),unit) = ld(a,ld(b,unit)),
inference(copy,[status(thm)],[c_8165]) ).
cnf(c_6747,plain,
rd(ld(b,unit),a) != ld(a,ld(b,unit)),
inference(paramod,[status(thm)],[c_6730,c_1238]) ).
cnf(c_8166,plain,
mult(rd(unit,b),a) = ld(b,a),
inference(paramod,[status(thm)],[c_6,c_6677]) ).
cnf(c_6926,plain,
mult(ld(b,unit),a) = ld(b,a),
inference(paramod,[status(thm)],[c_1105,c_8166]) ).
cnf(c_7020,plain,
rd(ld(b,a),mult(a,a)) = rd(ld(b,unit),a),
inference(paramod,[status(thm)],[c_6926,c_65]) ).
cnf(c_8167,plain,
( ld(rd(mult(a,a),ld(b,a)),unit) = rd(ld(b,unit),a)
| rd(ld(b,a),mult(a,a)) = ld(mult(a,a),ld(b,a)) ),
inference(paramod,[status(thm)],[c_7020,c_4190]) ).
cnf(c_8168,plain,
( ld(rd(mult(a,a),ld(b,a)),unit) = rd(ld(b,unit),a)
| rd(ld(b,unit),a) = ld(mult(a,a),ld(b,a)) ),
inference(paramod,[status(thm)],[c_7020,c_8167]) ).
cnf(c_8169,plain,
( ld(mult(mult(a,a),ld(a,b)),unit) = rd(ld(b,unit),a)
| rd(ld(b,unit),a) = ld(mult(a,a),ld(b,a)) ),
inference(paramod,[status(thm)],[c_1357,c_8168]) ).
cnf(c_8170,plain,
( ld(mult(a,b),unit) = rd(ld(b,unit),a)
| rd(ld(b,unit),a) = ld(mult(a,a),ld(b,a)) ),
inference(paramod,[status(thm)],[c_6658,c_8169]) ).
cnf(c_8171,plain,
( ld(a,ld(b,unit)) = rd(ld(b,unit),a)
| rd(ld(b,unit),a) = ld(mult(a,a),ld(b,a)) ),
inference(paramod,[status(thm)],[c_6730,c_8170]) ).
cnf(c_8172,plain,
( ld(a,ld(b,unit)) = rd(ld(b,unit),a)
| ld(mult(a,a),ld(b,a)) = rd(ld(b,unit),a) ),
inference(copy,[status(thm)],[c_8171]) ).
cnf(c_8173,plain,
( rd(ld(b,unit),a) = ld(a,ld(b,unit))
| ld(mult(a,a),ld(b,a)) = rd(ld(b,unit),a) ),
inference(copy,[status(thm)],[c_8172]) ).
cnf(c_8057,plain,
ld(mult(a,a),ld(b,a)) = rd(ld(b,unit),a),
inference(resolve,[status(thm)],[c_6747,c_8173]) ).
cnf(c_8174,plain,
( ld(rd(mult(a,a),ld(b,a)),unit) = ld(mult(a,a),ld(b,a))
| ld(rd(mult(a,a),ld(b,a)),unit) = rd(ld(b,unit),a) ),
inference(paramod,[status(thm)],[c_7020,c_4108]) ).
cnf(c_8175,plain,
( ld(rd(mult(a,a),ld(b,a)),unit) = ld(mult(a,a),ld(b,a))
| ld(mult(mult(a,a),ld(a,b)),unit) = rd(ld(b,unit),a) ),
inference(paramod,[status(thm)],[c_1357,c_8174]) ).
cnf(c_8176,plain,
( ld(rd(mult(a,a),ld(b,a)),unit) = ld(mult(a,a),ld(b,a))
| ld(mult(a,b),unit) = rd(ld(b,unit),a) ),
inference(paramod,[status(thm)],[c_6658,c_8175]) ).
cnf(c_8177,plain,
( ld(rd(mult(a,a),ld(b,a)),unit) = ld(mult(a,a),ld(b,a))
| ld(a,ld(b,unit)) = rd(ld(b,unit),a) ),
inference(paramod,[status(thm)],[c_6730,c_8176]) ).
cnf(c_8178,plain,
( ld(mult(mult(a,a),ld(a,b)),unit) = ld(mult(a,a),ld(b,a))
| ld(a,ld(b,unit)) = rd(ld(b,unit),a) ),
inference(paramod,[status(thm)],[c_1357,c_8177]) ).
cnf(c_8179,plain,
( ld(mult(a,b),unit) = ld(mult(a,a),ld(b,a))
| ld(a,ld(b,unit)) = rd(ld(b,unit),a) ),
inference(paramod,[status(thm)],[c_6658,c_8178]) ).
cnf(c_8180,plain,
( ld(a,ld(b,unit)) = ld(mult(a,a),ld(b,a))
| ld(a,ld(b,unit)) = rd(ld(b,unit),a) ),
inference(paramod,[status(thm)],[c_6730,c_8179]) ).
cnf(c_8181,plain,
( ld(a,ld(b,unit)) = rd(ld(b,unit),a)
| ld(a,ld(b,unit)) = rd(ld(b,unit),a) ),
inference(paramod,[status(thm)],[c_8057,c_8180]) ).
cnf(c_8182,plain,
( ld(a,ld(b,unit)) = rd(ld(b,unit),a)
| rd(ld(b,unit),a) = ld(a,ld(b,unit)) ),
inference(copy,[status(thm)],[c_8181]) ).
cnf(c_8183,plain,
( rd(ld(b,unit),a) = ld(a,ld(b,unit))
| rd(ld(b,unit),a) = ld(a,ld(b,unit)) ),
inference(copy,[status(thm)],[c_8182]) ).
cnf(c_8184,plain,
rd(ld(b,unit),a) = ld(a,ld(b,unit)),
inference(copy,[status(thm)],[c_8183]) ).
cnf(c_8063,plain,
$false,
inference(resolve,[status(thm)],[c_6747,c_8184]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRP755-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.41 % Computer : n018.cluster.edu
% 0.15/0.41 % Model : x86_64 x86_64
% 0.15/0.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.41 % Memory : 8046.5625MB
% 0.15/0.41 % OS : Linux 6.8.0-71-generic
% 0.15/0.41 % CPULimit : 300
% 0.15/0.41 % WCLimit : 300
% 0.15/0.41 % DateTime : Fri Sep 25 15:46:05 UTC 2026
% 0.15/0.42 % CPUTime :
% 0.15/0.42 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.15/0.42 % Process 2340293 was started by sandbox on n018,
% 0.15/0.42 % Fri Sep 25 15:46:05 2026
% 0.15/0.42 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.15/0.43
% 0.15/0.43 % From the command line: assign(max_seconds, 300).
% 21.98/3.23
% 21.98/3.23 % Assigning unary symbol i kb_weight 0 and highest precedence (8).
% 21.98/3.23
% 21.98/3.23 % SZS status Unsatisfiable for theBenchmark
% 21.98/3.23
% 21.98/3.23 % Proof 1 at 2.48 (+ 0.30) seconds.
% 21.98/3.23 % Length of proof is 85.
% 21.98/3.23 % Level of proof is 33.
% 21.98/3.23 % Maximum clause weight is 70.000.
% 21.98/3.23 % Given clauses 206.
% 21.98/3.23
% 21.98/3.23 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------