%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP705-1 : 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 : n019.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:17 AM UTC 2026
% Result : Unsatisfiable 64.16s 9.54s
% Output : CNFRefutation 64.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 43
% Number of leaves : 10
% Syntax : Number of formulae : 127 ( 127 unt; 0 def)
% Number of atoms : 127 ( 126 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 : 18 ( 3 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 4 con; 0-2 aty)
% Number of variables : 245 ( 0 sgn 13 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(c01,axiom,
! [VAR_0,VAR_1] : mult(VAR_0,ld(VAR_0,VAR_1)) = VAR_1,
file('theBenchmark.p',c01) ).
cnf(c_1,plain,
mult(A,ld(A,B)) = B,
inference(clausify,[status(thm)],[c01]) ).
fof(c02,axiom,
! [VAR_0,VAR_1] : ld(VAR_0,mult(VAR_0,VAR_1)) = VAR_1,
file('theBenchmark.p',c02) ).
cnf(c_2,plain,
ld(A,mult(A,B)) = B,
inference(clausify,[status(thm)],[c02]) ).
fof(c03,axiom,
! [VAR_0,VAR_1] : mult(rd(VAR_0,VAR_1),VAR_1) = VAR_0,
file('theBenchmark.p',c03) ).
cnf(c_3,plain,
mult(rd(A,B),B) = A,
inference(clausify,[status(thm)],[c03]) ).
fof(c04,axiom,
! [VAR_0,VAR_1] : rd(mult(VAR_0,VAR_1),VAR_1) = VAR_0,
file('theBenchmark.p',c04) ).
cnf(c_4,plain,
rd(mult(A,B),B) = A,
inference(clausify,[status(thm)],[c04]) ).
fof(c05,axiom,
! [VAR_0] : mult(VAR_0,unit) = VAR_0,
file('theBenchmark.p',c05) ).
cnf(c_5,plain,
mult(A,unit) = A,
inference(clausify,[status(thm)],[c05]) ).
fof(c06,axiom,
! [VAR_0] : mult(unit,VAR_0) = VAR_0,
file('theBenchmark.p',c06) ).
cnf(c_6,plain,
mult(unit,A) = A,
inference(clausify,[status(thm)],[c06]) ).
fof(c07,axiom,
! [VAR_0,VAR_1,VAR_2] : mult(VAR_0,mult(VAR_1,mult(VAR_1,VAR_2))) = mult(mult(mult(VAR_0,VAR_1),VAR_1),VAR_2),
file('theBenchmark.p',c07) ).
cnf(c_7,plain,
mult(A,mult(B,mult(B,C))) = mult(mult(mult(A,B),B),C),
inference(clausify,[status(thm)],[c07]) ).
cnf(c_8,plain,
mult(mult(mult(A,B),B),C) = mult(A,mult(B,mult(B,C))),
inference(copy,[status(thm)],[c_7]) ).
fof(c08,axiom,
mult(op_a,mult(op_a,mult(op_a,op_a))) = unit,
file('theBenchmark.p',c08) ).
cnf(c_9,plain,
mult(op_a,mult(op_a,mult(op_a,op_a))) = unit,
inference(clausify,[status(thm)],[c08]) ).
fof(c09,axiom,
mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,op_b)))))))) = unit,
file('theBenchmark.p',c09) ).
cnf(c_10,plain,
mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,op_b)))))))) = unit,
inference(clausify,[status(thm)],[c09]) ).
fof(goals,axiom,
mult(op_a,mult(op_b,a)) != mult(mult(op_a,op_b),a),
file('theBenchmark.p',goals) ).
cnf(c_11,plain,
mult(op_a,mult(op_b,a)) != mult(mult(op_a,op_b),a),
inference(clausify,[status(thm)],[goals]) ).
cnf(c_12,plain,
mult(mult(op_a,op_b),a) != mult(op_a,mult(op_b,a)),
inference(copy,[status(thm)],[c_11]) ).
cnf(c_14,plain,
rd(A,ld(B,A)) = B,
inference(paramod,[status(thm)],[c_1,c_4]) ).
cnf(c_19,plain,
mult(A,mult(B,mult(B,ld(mult(mult(A,B),B),C)))) = C,
inference(paramod,[status(thm)],[c_8,c_1]) ).
cnf(c_20,plain,
mult(mult(A,ld(B,A)),C) = mult(B,mult(ld(B,A),mult(ld(B,A),C))),
inference(paramod,[status(thm)],[c_1,c_8]) ).
cnf(c_21,plain,
ld(mult(mult(A,B),B),mult(A,mult(B,mult(B,C)))) = C,
inference(paramod,[status(thm)],[c_8,c_2]) ).
cnf(c_1328,plain,
mult(mult(A,B),C) = mult(rd(A,B),mult(B,mult(B,C))),
inference(paramod,[status(thm)],[c_3,c_8]) ).
cnf(c_22,plain,
mult(rd(A,B),mult(B,mult(B,C))) = mult(mult(A,B),C),
inference(copy,[status(thm)],[c_1328]) ).
cnf(c_1329,plain,
mult(A,mult(B,mult(B,unit))) = mult(mult(A,B),B),
inference(paramod,[status(thm)],[c_8,c_5]) ).
cnf(c_1330,plain,
mult(A,mult(B,B)) = mult(mult(A,B),B),
inference(paramod,[status(thm)],[c_5,c_1329]) ).
cnf(c_24,plain,
mult(mult(A,B),B) = mult(A,mult(B,B)),
inference(copy,[status(thm)],[c_1330]) ).
cnf(c_1331,plain,
mult(mult(A,A),B) = mult(unit,mult(A,mult(A,B))),
inference(paramod,[status(thm)],[c_6,c_8]) ).
cnf(c_25,plain,
mult(mult(A,A),B) = mult(A,mult(A,B)),
inference(paramod,[status(thm)],[c_6,c_1331]) ).
cnf(c_27,plain,
mult(mult(A,mult(B,mult(B,B))),C) = mult(mult(A,B),mult(B,mult(B,C))),
inference(paramod,[status(thm)],[c_8,c_8]) ).
cnf(c_1332,plain,
mult(mult(mult(A,mult(mult(B,C),C)),mult(mult(B,C),C)),D) = mult(A,mult(mult(mult(B,C),C),mult(B,mult(C,mult(C,D))))),
inference(paramod,[status(thm)],[c_8,c_8]) ).
cnf(c_1333,plain,
mult(mult(mult(A,mult(B,mult(C,C))),mult(mult(B,C),C)),D) = mult(A,mult(mult(mult(B,C),C),mult(B,mult(C,mult(C,D))))),
inference(paramod,[status(thm)],[c_24,c_1332]) ).
cnf(c_1334,plain,
mult(mult(mult(A,mult(B,mult(C,C))),mult(B,mult(C,C))),D) = mult(A,mult(mult(mult(B,C),C),mult(B,mult(C,mult(C,D))))),
inference(paramod,[status(thm)],[c_24,c_1333]) ).
cnf(c_1335,plain,
mult(mult(A,mult(mult(B,mult(C,C)),mult(B,mult(C,C)))),D) = mult(A,mult(mult(mult(B,C),C),mult(B,mult(C,mult(C,D))))),
inference(paramod,[status(thm)],[c_24,c_1334]) ).
cnf(c_28,plain,
mult(mult(A,mult(mult(B,mult(C,C)),mult(B,mult(C,C)))),D) = mult(A,mult(mult(B,mult(C,C)),mult(B,mult(C,mult(C,D))))),
inference(paramod,[status(thm)],[c_24,c_1335]) ).
cnf(c_32,plain,
ld(mult(A,mult(B,B)),mult(A,mult(B,mult(B,C)))) = C,
inference(paramod,[status(thm)],[c_24,c_21]) ).
cnf(c_33,plain,
mult(A,mult(B,mult(B,ld(mult(A,mult(B,B)),C)))) = C,
inference(paramod,[status(thm)],[c_24,c_19]) ).
cnf(c_34,plain,
mult(mult(A,mult(B,B)),C) = mult(A,mult(B,mult(B,C))),
inference(paramod,[status(thm)],[c_24,c_8]) ).
cnf(c_1336,plain,
mult(mult(A,mult(B,mult(C,mult(C,mult(B,mult(C,C)))))),D) = mult(A,mult(mult(B,mult(C,C)),mult(B,mult(C,mult(C,D))))),
inference(paramod,[status(thm)],[c_34,c_28]) ).
cnf(c_35,plain,
mult(mult(A,mult(B,mult(C,mult(C,mult(B,mult(C,C)))))),D) = mult(A,mult(B,mult(C,mult(C,mult(B,mult(C,mult(C,D))))))),
inference(paramod,[status(thm)],[c_34,c_1336]) ).
cnf(c_38,plain,
ld(op_a,unit) = mult(op_a,mult(op_a,op_a)),
inference(paramod,[status(thm)],[c_9,c_2]) ).
cnf(c_40,plain,
ld(op_b,unit) = mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,op_b))))))),
inference(paramod,[status(thm)],[c_10,c_2]) ).
cnf(c_42,plain,
mult(A,mult(ld(A,B),mult(ld(A,B),ld(mult(B,ld(A,B)),C)))) = C,
inference(paramod,[status(thm)],[c_20,c_1]) ).
cnf(c_1337,plain,
mult(rd(A,B),mult(B,B)) = mult(mult(A,B),unit),
inference(paramod,[status(thm)],[c_5,c_22]) ).
cnf(c_52,plain,
mult(rd(A,B),mult(B,B)) = mult(A,B),
inference(paramod,[status(thm)],[c_5,c_1337]) ).
cnf(c_1338,plain,
mult(rd(A,op_b),mult(op_b,unit)) = mult(mult(A,op_b),mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,op_b)))))))),
inference(paramod,[status(thm)],[c_10,c_22]) ).
cnf(c_1339,plain,
mult(rd(A,op_b),op_b) = mult(mult(A,op_b),mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,op_b)))))))),
inference(paramod,[status(thm)],[c_5,c_1338]) ).
cnf(c_1340,plain,
A = mult(mult(A,op_b),mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,op_b)))))))),
inference(paramod,[status(thm)],[c_3,c_1339]) ).
cnf(c_56,plain,
mult(mult(A,op_b),mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,op_b)))))))) = A,
inference(copy,[status(thm)],[c_1340]) ).
cnf(c_69,plain,
ld(rd(A,B),mult(A,B)) = mult(B,B),
inference(paramod,[status(thm)],[c_52,c_2]) ).
cnf(c_78,plain,
ld(rd(unit,A),A) = mult(A,A),
inference(paramod,[status(thm)],[c_6,c_69]) ).
cnf(c_1341,plain,
mult(unit,A) = mult(mult(op_a,op_a),mult(op_a,mult(op_a,A))),
inference(paramod,[status(thm)],[c_9,c_27]) ).
cnf(c_1342,plain,
A = mult(mult(op_a,op_a),mult(op_a,mult(op_a,A))),
inference(paramod,[status(thm)],[c_6,c_1341]) ).
cnf(c_1343,plain,
A = mult(op_a,mult(op_a,mult(op_a,mult(op_a,A)))),
inference(paramod,[status(thm)],[c_25,c_1342]) ).
cnf(c_118,plain,
mult(op_a,mult(op_a,mult(op_a,mult(op_a,A)))) = A,
inference(copy,[status(thm)],[c_1343]) ).
cnf(c_169,plain,
ld(mult(A,mult(B,B)),mult(A,mult(B,C))) = ld(B,C),
inference(paramod,[status(thm)],[c_1,c_32]) ).
cnf(c_1344,plain,
ld(A,B) = mult(C,mult(C,ld(mult(A,mult(C,C)),B))),
inference(paramod,[status(thm)],[c_33,c_2]) ).
cnf(c_181,plain,
mult(A,mult(A,ld(mult(B,mult(A,A)),C))) = ld(B,C),
inference(copy,[status(thm)],[c_1344]) ).
cnf(c_1345,plain,
mult(mult(A,mult(A,mult(B,mult(C,mult(C,mult(B,mult(C,C))))))),D) = mult(mult(A,A),mult(B,mult(C,mult(C,mult(B,mult(C,mult(C,D))))))),
inference(paramod,[status(thm)],[c_25,c_35]) ).
cnf(c_249,plain,
mult(mult(A,mult(A,mult(B,mult(C,mult(C,mult(B,mult(C,C))))))),D) = mult(A,mult(A,mult(B,mult(C,mult(C,mult(B,mult(C,mult(C,D)))))))),
inference(paramod,[status(thm)],[c_25,c_1345]) ).
cnf(c_1346,plain,
mult(rd(unit,A),mult(mult(A,A),mult(ld(rd(unit,A),A),ld(mult(A,ld(rd(unit,A),A)),B)))) = B,
inference(paramod,[status(thm)],[c_78,c_42]) ).
cnf(c_1347,plain,
mult(rd(unit,A),mult(mult(A,A),mult(mult(A,A),ld(mult(A,ld(rd(unit,A),A)),B)))) = B,
inference(paramod,[status(thm)],[c_78,c_1346]) ).
cnf(c_1348,plain,
mult(rd(unit,A),mult(mult(A,A),mult(mult(A,A),ld(mult(A,mult(A,A)),B)))) = B,
inference(paramod,[status(thm)],[c_78,c_1347]) ).
cnf(c_1349,plain,
mult(rd(unit,A),mult(mult(A,A),mult(A,mult(A,ld(mult(A,mult(A,A)),B))))) = B,
inference(paramod,[status(thm)],[c_25,c_1348]) ).
cnf(c_1350,plain,
mult(rd(unit,A),mult(mult(A,A),ld(A,B))) = B,
inference(paramod,[status(thm)],[c_181,c_1349]) ).
cnf(c_1351,plain,
mult(rd(unit,A),mult(A,mult(A,ld(A,B)))) = B,
inference(paramod,[status(thm)],[c_25,c_1350]) ).
cnf(c_309,plain,
mult(rd(unit,A),mult(A,B)) = B,
inference(paramod,[status(thm)],[c_1,c_1351]) ).
cnf(c_357,plain,
mult(rd(unit,A),B) = ld(A,B),
inference(paramod,[status(thm)],[c_1,c_309]) ).
cnf(c_1352,plain,
ld(A,unit) = rd(unit,A),
inference(paramod,[status(thm)],[c_357,c_5]) ).
cnf(c_382,plain,
rd(unit,A) = ld(A,unit),
inference(copy,[status(thm)],[c_1352]) ).
cnf(c_1353,plain,
mult(A,B) = ld(ld(A,unit),B),
inference(paramod,[status(thm)],[c_14,c_357]) ).
cnf(c_385,plain,
ld(ld(A,unit),B) = mult(A,B),
inference(copy,[status(thm)],[c_1353]) ).
cnf(c_1354,plain,
mult(rd(rd(unit,A),B),mult(B,B)) = ld(A,B),
inference(paramod,[status(thm)],[c_357,c_52]) ).
cnf(c_1355,plain,
mult(rd(ld(A,unit),B),mult(B,B)) = ld(A,B),
inference(paramod,[status(thm)],[c_382,c_1354]) ).
cnf(c_398,plain,
mult(ld(A,unit),B) = ld(A,B),
inference(paramod,[status(thm)],[c_52,c_1355]) ).
cnf(c_1356,plain,
mult(mult(op_a,mult(op_a,op_a)),A) = ld(op_a,A),
inference(paramod,[status(thm)],[c_38,c_398]) ).
cnf(c_1357,plain,
mult(op_a,mult(op_a,mult(op_a,A))) = ld(op_a,A),
inference(paramod,[status(thm)],[c_34,c_1356]) ).
cnf(c_691,plain,
ld(op_a,A) = mult(op_a,mult(op_a,mult(op_a,A))),
inference(copy,[status(thm)],[c_1357]) ).
cnf(c_1358,plain,
mult(mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,op_b))))))),A) = ld(op_b,A),
inference(paramod,[status(thm)],[c_40,c_398]) ).
cnf(c_1359,plain,
mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,A)))))))) = ld(op_b,A),
inference(paramod,[status(thm)],[c_249,c_1358]) ).
cnf(c_692,plain,
ld(op_b,A) = mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,A)))))))),
inference(copy,[status(thm)],[c_1359]) ).
cnf(c_1360,plain,
mult(ld(A,op_b),mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,op_b)))))))) = ld(A,unit),
inference(paramod,[status(thm)],[c_398,c_56]) ).
cnf(c_725,plain,
ld(A,unit) = mult(ld(A,op_b),mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,op_b)))))))),
inference(copy,[status(thm)],[c_1360]) ).
cnf(c_783,plain,
ld(mult(ld(A,op_b),mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,op_b)))))))),B) = mult(A,B),
inference(paramod,[status(thm)],[c_725,c_385]) ).
cnf(c_862,plain,
ld(mult(A,mult(B,B)),mult(A,C)) = ld(B,ld(B,C)),
inference(paramod,[status(thm)],[c_1,c_169]) ).
cnf(c_895,plain,
ld(mult(A,mult(B,B)),C) = ld(B,ld(B,ld(A,C))),
inference(paramod,[status(thm)],[c_1,c_862]) ).
cnf(c_1361,plain,
ld(mult(A,mult(B,mult(C,mult(C,mult(B,mult(C,C)))))),D) = ld(mult(B,mult(C,C)),ld(mult(B,mult(C,C)),ld(A,D))),
inference(paramod,[status(thm)],[c_34,c_895]) ).
cnf(c_1362,plain,
ld(mult(A,mult(B,mult(C,mult(C,mult(B,mult(C,C)))))),D) = ld(mult(B,mult(C,C)),ld(C,ld(C,ld(B,ld(A,D))))),
inference(paramod,[status(thm)],[c_895,c_1361]) ).
cnf(c_991,plain,
ld(mult(A,mult(B,mult(C,mult(C,mult(B,mult(C,C)))))),D) = ld(C,ld(C,ld(B,ld(C,ld(C,ld(B,ld(A,D))))))),
inference(paramod,[status(thm)],[c_895,c_1362]) ).
cnf(c_1363,plain,
ld(mult(A,mult(B,mult(C,mult(C,mult(B,mult(C,mult(C,mult(D,D)))))))),E) = ld(D,ld(D,ld(mult(A,mult(B,mult(C,mult(C,mult(B,mult(C,C)))))),E))),
inference(paramod,[status(thm)],[c_35,c_895]) ).
cnf(c_993,plain,
ld(mult(A,mult(B,mult(C,mult(C,mult(B,mult(C,mult(C,mult(D,D)))))))),E) = ld(D,ld(D,ld(C,ld(C,ld(B,ld(C,ld(C,ld(B,ld(A,E))))))))),
inference(paramod,[status(thm)],[c_991,c_1363]) ).
cnf(c_1364,plain,
ld(op_b,ld(op_b,ld(op_b,ld(op_b,ld(op_b,ld(op_b,ld(op_b,ld(op_b,ld(ld(A,op_b),B))))))))) = mult(A,B),
inference(paramod,[status(thm)],[c_993,c_783]) ).
cnf(c_1365,plain,
ld(op_b,ld(op_b,ld(op_b,ld(op_b,ld(op_b,ld(op_b,ld(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,ld(ld(A,op_b),B)))))))))))))))) = mult(A,B),
inference(paramod,[status(thm)],[c_692,c_1364]) ).
cnf(c_1366,plain,
ld(op_b,ld(op_b,ld(op_b,ld(op_b,ld(op_b,ld(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,ld(ld(A,op_b),B)))))))))))))) = mult(A,B),
inference(paramod,[status(thm)],[c_2,c_1365]) ).
cnf(c_1367,plain,
ld(op_b,ld(op_b,ld(op_b,ld(op_b,ld(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,ld(ld(A,op_b),B)))))))))))) = mult(A,B),
inference(paramod,[status(thm)],[c_2,c_1366]) ).
cnf(c_1368,plain,
ld(op_b,ld(op_b,ld(op_b,ld(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,ld(ld(A,op_b),B)))))))))) = mult(A,B),
inference(paramod,[status(thm)],[c_2,c_1367]) ).
cnf(c_1369,plain,
ld(op_b,ld(op_b,ld(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,ld(ld(A,op_b),B)))))))) = mult(A,B),
inference(paramod,[status(thm)],[c_2,c_1368]) ).
cnf(c_1370,plain,
ld(op_b,ld(op_b,mult(op_b,mult(op_b,mult(op_b,ld(ld(A,op_b),B)))))) = mult(A,B),
inference(paramod,[status(thm)],[c_2,c_1369]) ).
cnf(c_1371,plain,
ld(op_b,mult(op_b,mult(op_b,ld(ld(A,op_b),B)))) = mult(A,B),
inference(paramod,[status(thm)],[c_2,c_1370]) ).
cnf(c_1005,plain,
mult(op_b,ld(ld(A,op_b),B)) = mult(A,B),
inference(paramod,[status(thm)],[c_2,c_1371]) ).
cnf(c_1372,plain,
ld(op_b,mult(A,B)) = ld(ld(A,op_b),B),
inference(paramod,[status(thm)],[c_1005,c_2]) ).
cnf(c_1373,plain,
mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(A,B))))))))) = ld(ld(A,op_b),B),
inference(paramod,[status(thm)],[c_692,c_1372]) ).
cnf(c_1011,plain,
ld(ld(A,op_b),B) = mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(A,B))))))))),
inference(copy,[status(thm)],[c_1373]) ).
cnf(c_1374,plain,
mult(op_b,A) = mult(B,mult(ld(B,op_b),A)),
inference(paramod,[status(thm)],[c_2,c_1005]) ).
cnf(c_1012,plain,
mult(A,mult(ld(A,op_b),B)) = mult(op_b,B),
inference(copy,[status(thm)],[c_1374]) ).
cnf(c_1021,plain,
mult(op_b,ld(mult(op_a,mult(op_a,mult(op_a,op_b))),A)) = mult(op_a,A),
inference(paramod,[status(thm)],[c_691,c_1005]) ).
cnf(c_1375,plain,
mult(op_a,mult(op_a,mult(op_a,mult(op_b,A)))) = mult(ld(op_a,op_b),A),
inference(paramod,[status(thm)],[c_1012,c_118]) ).
cnf(c_1376,plain,
mult(op_a,mult(op_a,mult(op_a,mult(op_b,A)))) = mult(mult(op_a,mult(op_a,mult(op_a,op_b))),A),
inference(paramod,[status(thm)],[c_691,c_1375]) ).
cnf(c_1043,plain,
mult(mult(op_a,mult(op_a,mult(op_a,op_b))),A) = mult(op_a,mult(op_a,mult(op_a,mult(op_b,A)))),
inference(copy,[status(thm)],[c_1376]) ).
cnf(c_1377,plain,
mult(A,mult(op_b,B)) = mult(op_b,mult(ld(ld(A,op_b),op_b),B)),
inference(paramod,[status(thm)],[c_1012,c_1012]) ).
cnf(c_1378,plain,
mult(A,mult(op_b,B)) = mult(op_b,mult(mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(A,op_b))))))))),B)),
inference(paramod,[status(thm)],[c_1011,c_1377]) ).
cnf(c_1046,plain,
mult(op_b,mult(mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(A,op_b))))))))),B)) = mult(A,mult(op_b,B)),
inference(copy,[status(thm)],[c_1378]) ).
cnf(c_1379,plain,
ld(op_b,mult(op_a,A)) = ld(mult(op_a,mult(op_a,mult(op_a,op_b))),A),
inference(paramod,[status(thm)],[c_1021,c_2]) ).
cnf(c_1380,plain,
mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_a,A))))))))) = ld(mult(op_a,mult(op_a,mult(op_a,op_b))),A),
inference(paramod,[status(thm)],[c_692,c_1379]) ).
cnf(c_1325,plain,
ld(mult(op_a,mult(op_a,mult(op_a,op_b))),A) = mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_a,A))))))))),
inference(copy,[status(thm)],[c_1380]) ).
cnf(c_1381,plain,
mult(mult(op_a,op_b),A) = mult(mult(op_a,mult(op_a,mult(op_a,op_b))),mult(ld(mult(op_a,mult(op_a,mult(op_a,op_b))),op_b),mult(ld(mult(op_a,mult(op_a,mult(op_a,op_b))),op_b),A))),
inference(paramod,[status(thm)],[c_1021,c_20]) ).
cnf(c_1382,plain,
mult(mult(op_a,op_b),A) = mult(mult(op_a,mult(op_a,mult(op_a,op_b))),mult(mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_a,op_b))))))))),mult(ld(mult(op_a,mult(op_a,mult(op_a,op_b))),op_b),A))),
inference(paramod,[status(thm)],[c_1325,c_1381]) ).
cnf(c_1383,plain,
mult(mult(op_a,op_b),A) = mult(mult(op_a,mult(op_a,mult(op_a,op_b))),mult(mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_a,op_b))))))))),mult(mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_a,op_b))))))))),A))),
inference(paramod,[status(thm)],[c_1325,c_1382]) ).
cnf(c_1384,plain,
mult(mult(op_a,op_b),A) = mult(op_a,mult(op_a,mult(op_a,mult(op_b,mult(mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_a,op_b))))))))),mult(mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_a,op_b))))))))),A)))))),
inference(paramod,[status(thm)],[c_1043,c_1383]) ).
cnf(c_1385,plain,
mult(mult(op_a,op_b),A) = mult(op_a,mult(op_a,mult(op_a,mult(op_a,mult(op_b,mult(mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_b,mult(op_a,op_b))))))))),A)))))),
inference(paramod,[status(thm)],[c_1046,c_1384]) ).
cnf(c_1386,plain,
mult(mult(op_a,op_b),A) = mult(op_a,mult(op_a,mult(op_a,mult(op_a,mult(op_a,mult(op_b,A)))))),
inference(paramod,[status(thm)],[c_1046,c_1385]) ).
cnf(c_1326,plain,
mult(mult(op_a,op_b),A) = mult(op_a,mult(op_b,A)),
inference(paramod,[status(thm)],[c_118,c_1386]) ).
cnf(c_1327,plain,
$false,
inference(resolve,[status(thm)],[c_1326,c_12]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : GRP705-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.43 % Computer : n019.cluster.edu
% 0.18/0.43 % Model : x86_64 x86_64
% 0.18/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.43 % Memory : 8046.5625MB
% 0.18/0.43 % OS : Linux 6.8.0-71-generic
% 0.18/0.43 % CPULimit : 300
% 0.18/0.43 % WCLimit : 300
% 0.18/0.44 % DateTime : Fri Sep 25 15:39:20 UTC 2026
% 0.18/0.44 % CPUTime :
% 0.18/0.44 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.18/0.44 % Process 3142453 was started by sandbox2 on n019,
% 0.18/0.44 % Fri Sep 25 15:39:20 2026
% 0.18/0.44 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.18/0.45
% 0.18/0.45 % From the command line: assign(max_seconds, 300).
% 64.16/9.54
% 64.16/9.54 % SZS status Unsatisfiable for theBenchmark
% 64.16/9.54
% 64.16/9.54 % Proof 1 at 0.82 (+ 0.18) seconds.
% 64.16/9.54 % Length of proof is 58.
% 64.16/9.54 % Level of proof is 16.
% 64.16/9.54 % Maximum clause weight is 89.000.
% 64.16/9.54 % Given clauses 111.
% 64.16/9.54
% 64.16/9.54 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------