%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP696-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 : n007.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:13 AM UTC 2026
% Result : Unsatisfiable 1.89s 0.72s
% Output : CNFRefutation 1.89s
% Verified :
% SZS Type : Refutation
% Derivation depth : 44
% Number of leaves : 12
% Syntax : Number of formulae : 218 ( 218 unt; 0 def)
% Number of atoms : 218 ( 217 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 7 ( 7 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 4 con; 0-2 aty)
% Number of variables : 423 ( 0 sgn 20 !; 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] : mult(VAR_0,i(mult(VAR_1,VAR_0))) = i(VAR_1),
file('theBenchmark.p',c07) ).
cnf(c_7,plain,
mult(A,i(mult(B,A))) = i(B),
inference(clausify,[status(thm)],[c07]) ).
fof(c08,axiom,
! [VAR_0,VAR_1,VAR_2] : mult(VAR_0,mult(VAR_1,VAR_2)) = mult(rd(mult(VAR_0,VAR_1),VAR_0),mult(VAR_0,VAR_2)),
file('theBenchmark.p',c08) ).
cnf(c_8,plain,
mult(A,mult(B,C)) = mult(rd(mult(A,B),A),mult(A,C)),
inference(clausify,[status(thm)],[c08]) ).
cnf(c_9,plain,
mult(rd(mult(A,B),A),mult(A,C)) = mult(A,mult(B,C)),
inference(copy,[status(thm)],[c_8]) ).
fof(c09,axiom,
! [VAR_0,VAR_1,VAR_2] : mult(mult(VAR_0,VAR_1),VAR_2) = mult(mult(VAR_0,VAR_2),ld(VAR_2,mult(VAR_1,VAR_2))),
file('theBenchmark.p',c09) ).
cnf(c_10,plain,
mult(mult(A,B),C) = mult(mult(A,C),ld(C,mult(B,C))),
inference(clausify,[status(thm)],[c09]) ).
cnf(c_11,plain,
mult(mult(A,B),ld(B,mult(C,B))) = mult(mult(A,C),B),
inference(copy,[status(thm)],[c_10]) ).
fof(c10,axiom,
! [VAR_0] : mult(i(VAR_0),VAR_0) = unit,
file('theBenchmark.p',c10) ).
cnf(c_12,plain,
mult(i(A),A) = unit,
inference(clausify,[status(thm)],[c10]) ).
fof(c11,axiom,
! [VAR_0] : mult(VAR_0,i(VAR_0)) = unit,
file('theBenchmark.p',c11) ).
cnf(c_13,plain,
mult(A,i(A)) = unit,
inference(clausify,[status(thm)],[c11]) ).
fof(goals,axiom,
mult(mult(mult(a,b),a),mult(a,c)) != mult(a,mult(mult(mult(b,a),a),c)),
file('theBenchmark.p',goals) ).
cnf(c_14,plain,
mult(mult(mult(a,b),a),mult(a,c)) != mult(a,mult(mult(mult(b,a),a),c)),
inference(clausify,[status(thm)],[goals]) ).
cnf(c_19,plain,
ld(unit,A) = A,
inference(paramod,[status(thm)],[c_6,c_1]) ).
cnf(c_21,plain,
mult(ld(A,B),i(B)) = i(A),
inference(paramod,[status(thm)],[c_1,c_7]) ).
cnf(c_1696,plain,
ld(A,i(B)) = i(mult(B,A)),
inference(paramod,[status(thm)],[c_7,c_2]) ).
cnf(c_22,plain,
i(mult(A,B)) = ld(B,i(A)),
inference(copy,[status(thm)],[c_1696]) ).
cnf(c_1697,plain,
mult(A,i(B)) = i(rd(B,A)),
inference(paramod,[status(thm)],[c_3,c_7]) ).
cnf(c_23,plain,
i(rd(A,B)) = mult(B,i(A)),
inference(copy,[status(thm)],[c_1697]) ).
cnf(c_1698,plain,
mult(A,i(A)) = i(unit),
inference(paramod,[status(thm)],[c_6,c_7]) ).
cnf(c_1699,plain,
unit = i(unit),
inference(paramod,[status(thm)],[c_13,c_1698]) ).
cnf(c_24,plain,
i(unit) = unit,
inference(copy,[status(thm)],[c_1699]) ).
cnf(c_25,plain,
mult(rd(A,B),mult(B,C)) = mult(B,mult(ld(B,A),C)),
inference(paramod,[status(thm)],[c_1,c_9]) ).
cnf(c_32,plain,
mult(A,ld(ld(B,A),mult(C,ld(B,A)))) = mult(mult(B,C),ld(B,A)),
inference(paramod,[status(thm)],[c_1,c_11]) ).
cnf(c_33,plain,
mult(mult(A,ld(B,C)),ld(ld(B,C),C)) = mult(mult(A,B),ld(B,C)),
inference(paramod,[status(thm)],[c_1,c_11]) ).
cnf(c_34,plain,
ld(mult(A,B),mult(mult(A,C),B)) = ld(B,mult(C,B)),
inference(paramod,[status(thm)],[c_11,c_2]) ).
cnf(c_41,plain,
rd(unit,A) = i(A),
inference(paramod,[status(thm)],[c_12,c_4]) ).
cnf(c_1700,plain,
mult(unit,ld(A,mult(B,A))) = mult(mult(i(A),B),A),
inference(paramod,[status(thm)],[c_12,c_11]) ).
cnf(c_42,plain,
ld(A,mult(B,A)) = mult(mult(i(A),B),A),
inference(paramod,[status(thm)],[c_6,c_1700]) ).
cnf(c_43,plain,
mult(mult(A,B),ld(B,unit)) = mult(mult(A,i(B)),B),
inference(paramod,[status(thm)],[c_12,c_11]) ).
cnf(c_47,plain,
ld(mult(A,B),mult(mult(A,C),B)) = mult(mult(i(B),C),B),
inference(paramod,[status(thm)],[c_42,c_34]) ).
cnf(c_48,plain,
mult(A,mult(mult(i(ld(B,A)),C),ld(B,A))) = mult(mult(B,C),ld(B,A)),
inference(paramod,[status(thm)],[c_42,c_32]) ).
cnf(c_49,plain,
mult(mult(A,B),mult(mult(i(B),C),B)) = mult(mult(A,C),B),
inference(paramod,[status(thm)],[c_42,c_11]) ).
cnf(c_50,plain,
ld(A,unit) = i(A),
inference(paramod,[status(thm)],[c_13,c_2]) ).
cnf(c_1701,plain,
rd(unit,i(A)) = A,
inference(paramod,[status(thm)],[c_13,c_4]) ).
cnf(c_51,plain,
i(i(A)) = A,
inference(paramod,[status(thm)],[c_41,c_1701]) ).
cnf(c_1702,plain,
mult(mult(A,B),i(B)) = mult(mult(A,i(B)),B),
inference(paramod,[status(thm)],[c_50,c_43]) ).
cnf(c_52,plain,
mult(mult(A,i(B)),B) = mult(mult(A,B),i(B)),
inference(copy,[status(thm)],[c_1702]) ).
cnf(c_53,plain,
ld(ld(A,B),i(A)) = i(B),
inference(paramod,[status(thm)],[c_21,c_2]) ).
cnf(c_54,plain,
rd(i(A),i(B)) = ld(A,B),
inference(paramod,[status(thm)],[c_21,c_4]) ).
cnf(c_55,plain,
mult(ld(A,i(B)),mult(B,A)) = unit,
inference(paramod,[status(thm)],[c_22,c_12]) ).
cnf(c_1703,plain,
i(ld(A,B)) = mult(i(B),i(i(A))),
inference(paramod,[status(thm)],[c_54,c_23]) ).
cnf(c_63,plain,
i(ld(A,B)) = mult(i(B),A),
inference(paramod,[status(thm)],[c_51,c_1703]) ).
cnf(c_66,plain,
mult(A,mult(mult(mult(i(A),B),C),ld(B,A))) = mult(mult(B,C),ld(B,A)),
inference(paramod,[status(thm)],[c_63,c_48]) ).
cnf(c_1704,plain,
mult(A,mult(B,C)) = mult(B,mult(ld(B,mult(A,B)),C)),
inference(paramod,[status(thm)],[c_4,c_25]) ).
cnf(c_1705,plain,
mult(A,mult(B,C)) = mult(B,mult(mult(mult(i(B),A),B),C)),
inference(paramod,[status(thm)],[c_42,c_1704]) ).
cnf(c_77,plain,
mult(A,mult(mult(mult(i(A),B),A),C)) = mult(B,mult(A,C)),
inference(copy,[status(thm)],[c_1705]) ).
cnf(c_1706,plain,
mult(i(A),mult(A,B)) = mult(A,mult(ld(A,unit),B)),
inference(paramod,[status(thm)],[c_41,c_25]) ).
cnf(c_80,plain,
mult(i(A),mult(A,B)) = mult(A,mult(i(A),B)),
inference(paramod,[status(thm)],[c_50,c_1706]) ).
cnf(c_1707,plain,
i(mult(A,mult(ld(A,B),C))) = ld(mult(A,C),i(rd(B,A))),
inference(paramod,[status(thm)],[c_25,c_22]) ).
cnf(c_1708,plain,
ld(mult(ld(A,B),C),i(A)) = ld(mult(A,C),i(rd(B,A))),
inference(paramod,[status(thm)],[c_22,c_1707]) ).
cnf(c_83,plain,
ld(mult(ld(A,B),C),i(A)) = ld(mult(A,C),mult(A,i(B))),
inference(paramod,[status(thm)],[c_23,c_1708]) ).
cnf(c_108,plain,
ld(ld(i(A),B),A) = i(B),
inference(paramod,[status(thm)],[c_51,c_53]) ).
cnf(c_1709,plain,
ld(i(A),unit) = mult(mult(i(i(A)),A),i(A)),
inference(paramod,[status(thm)],[c_13,c_42]) ).
cnf(c_1710,plain,
i(i(A)) = mult(mult(i(i(A)),A),i(A)),
inference(paramod,[status(thm)],[c_50,c_1709]) ).
cnf(c_1711,plain,
A = mult(mult(i(i(A)),A),i(A)),
inference(paramod,[status(thm)],[c_51,c_1710]) ).
cnf(c_1712,plain,
A = mult(mult(A,A),i(A)),
inference(paramod,[status(thm)],[c_51,c_1711]) ).
cnf(c_131,plain,
mult(mult(A,A),i(A)) = A,
inference(copy,[status(thm)],[c_1712]) ).
cnf(c_1713,plain,
i(mult(mult(i(A),B),A)) = mult(i(mult(B,A)),A),
inference(paramod,[status(thm)],[c_42,c_63]) ).
cnf(c_1714,plain,
ld(A,i(mult(i(A),B))) = mult(i(mult(B,A)),A),
inference(paramod,[status(thm)],[c_22,c_1713]) ).
cnf(c_1715,plain,
ld(A,ld(B,i(i(A)))) = mult(i(mult(B,A)),A),
inference(paramod,[status(thm)],[c_22,c_1714]) ).
cnf(c_1716,plain,
ld(A,ld(B,A)) = mult(i(mult(B,A)),A),
inference(paramod,[status(thm)],[c_51,c_1715]) ).
cnf(c_133,plain,
ld(A,ld(B,A)) = mult(ld(A,i(B)),A),
inference(paramod,[status(thm)],[c_22,c_1716]) ).
cnf(c_1717,plain,
ld(mult(mult(i(A),B),A),i(A)) = i(mult(B,A)),
inference(paramod,[status(thm)],[c_42,c_53]) ).
cnf(c_134,plain,
ld(mult(mult(i(A),B),A),i(A)) = ld(A,i(B)),
inference(paramod,[status(thm)],[c_22,c_1717]) ).
cnf(c_1718,plain,
ld(ld(ld(A,B),B),mult(ld(A,B),ld(ld(A,B),B))) = mult(mult(i(ld(ld(A,B),B)),A),ld(A,B)),
inference(paramod,[status(thm)],[c_33,c_42]) ).
cnf(c_1719,plain,
ld(ld(ld(A,B),B),B) = mult(mult(i(ld(ld(A,B),B)),A),ld(A,B)),
inference(paramod,[status(thm)],[c_1,c_1718]) ).
cnf(c_1720,plain,
ld(ld(ld(A,B),B),B) = mult(mult(mult(i(B),ld(A,B)),A),ld(A,B)),
inference(paramod,[status(thm)],[c_63,c_1719]) ).
cnf(c_139,plain,
mult(mult(mult(i(A),ld(B,A)),B),ld(B,A)) = ld(ld(ld(B,A),A),A),
inference(copy,[status(thm)],[c_1720]) ).
cnf(c_1721,plain,
ld(mult(A,B),mult(unit,B)) = mult(mult(i(B),i(A)),B),
inference(paramod,[status(thm)],[c_13,c_47]) ).
cnf(c_152,plain,
ld(mult(A,B),B) = mult(mult(i(B),i(A)),B),
inference(paramod,[status(thm)],[c_6,c_1721]) ).
cnf(c_1722,plain,
ld(mult(ld(A,unit),B),i(A)) = ld(mult(A,B),mult(A,unit)),
inference(paramod,[status(thm)],[c_24,c_83]) ).
cnf(c_1723,plain,
ld(mult(i(A),B),i(A)) = ld(mult(A,B),mult(A,unit)),
inference(paramod,[status(thm)],[c_50,c_1722]) ).
cnf(c_167,plain,
ld(mult(i(A),B),i(A)) = ld(mult(A,B),A),
inference(paramod,[status(thm)],[c_5,c_1723]) ).
cnf(c_1724,plain,
ld(unit,i(A)) = ld(mult(A,mult(B,A)),mult(A,i(i(B)))),
inference(paramod,[status(thm)],[c_55,c_83]) ).
cnf(c_1725,plain,
i(A) = ld(mult(A,mult(B,A)),mult(A,i(i(B)))),
inference(paramod,[status(thm)],[c_19,c_1724]) ).
cnf(c_1726,plain,
i(A) = ld(mult(A,mult(B,A)),mult(A,B)),
inference(paramod,[status(thm)],[c_51,c_1725]) ).
cnf(c_181,plain,
ld(mult(A,mult(B,A)),mult(A,B)) = i(A),
inference(copy,[status(thm)],[c_1726]) ).
cnf(c_1727,plain,
mult(ld(mult(A,B),A),i(i(A))) = i(mult(i(A),B)),
inference(paramod,[status(thm)],[c_167,c_21]) ).
cnf(c_1728,plain,
mult(ld(mult(A,B),A),A) = i(mult(i(A),B)),
inference(paramod,[status(thm)],[c_51,c_1727]) ).
cnf(c_1729,plain,
mult(ld(mult(A,B),A),A) = ld(B,i(i(A))),
inference(paramod,[status(thm)],[c_22,c_1728]) ).
cnf(c_191,plain,
mult(ld(mult(A,B),A),A) = ld(B,A),
inference(paramod,[status(thm)],[c_51,c_1729]) ).
cnf(c_1730,plain,
mult(ld(A,B),B) = ld(ld(B,A),B),
inference(paramod,[status(thm)],[c_1,c_191]) ).
cnf(c_202,plain,
ld(ld(A,B),A) = mult(ld(B,A),A),
inference(copy,[status(thm)],[c_1730]) ).
cnf(c_1731,plain,
mult(ld(unit,A),A) = ld(i(A),A),
inference(paramod,[status(thm)],[c_13,c_191]) ).
cnf(c_1732,plain,
mult(A,A) = ld(i(A),A),
inference(paramod,[status(thm)],[c_19,c_1731]) ).
cnf(c_204,plain,
ld(i(A),A) = mult(A,A),
inference(copy,[status(thm)],[c_1732]) ).
cnf(c_1733,plain,
mult(mult(A,mult(B,B)),ld(ld(i(B),B),B)) = mult(mult(A,i(B)),ld(i(B),B)),
inference(paramod,[status(thm)],[c_204,c_33]) ).
cnf(c_1734,plain,
mult(mult(A,mult(B,B)),ld(mult(B,B),B)) = mult(mult(A,i(B)),ld(i(B),B)),
inference(paramod,[status(thm)],[c_204,c_1733]) ).
cnf(c_1735,plain,
mult(mult(A,mult(B,B)),mult(mult(i(B),i(B)),B)) = mult(mult(A,i(B)),ld(i(B),B)),
inference(paramod,[status(thm)],[c_152,c_1734]) ).
cnf(c_1736,plain,
mult(mult(A,mult(B,B)),mult(mult(i(B),B),i(B))) = mult(mult(A,i(B)),ld(i(B),B)),
inference(paramod,[status(thm)],[c_52,c_1735]) ).
cnf(c_1737,plain,
mult(mult(A,mult(B,B)),mult(unit,i(B))) = mult(mult(A,i(B)),ld(i(B),B)),
inference(paramod,[status(thm)],[c_12,c_1736]) ).
cnf(c_1738,plain,
mult(mult(A,mult(B,B)),i(B)) = mult(mult(A,i(B)),ld(i(B),B)),
inference(paramod,[status(thm)],[c_6,c_1737]) ).
cnf(c_222,plain,
mult(mult(A,mult(B,B)),i(B)) = mult(mult(A,i(B)),mult(B,B)),
inference(paramod,[status(thm)],[c_204,c_1738]) ).
cnf(c_1739,plain,
i(mult(ld(A,B),B)) = mult(i(B),ld(B,A)),
inference(paramod,[status(thm)],[c_202,c_63]) ).
cnf(c_1740,plain,
ld(B,i(ld(A,B))) = mult(i(B),ld(B,A)),
inference(paramod,[status(thm)],[c_22,c_1739]) ).
cnf(c_228,plain,
ld(A,mult(i(A),B)) = mult(i(A),ld(A,B)),
inference(paramod,[status(thm)],[c_63,c_1740]) ).
cnf(c_1741,plain,
mult(mult(A,B),mult(C,B)) = mult(mult(A,ld(i(B),C)),B),
inference(paramod,[status(thm)],[c_1,c_49]) ).
cnf(c_244,plain,
mult(mult(A,ld(i(B),C)),B) = mult(mult(A,B),mult(C,B)),
inference(copy,[status(thm)],[c_1741]) ).
cnf(c_264,plain,
mult(A,mult(i(A),ld(A,B))) = mult(i(A),B),
inference(paramod,[status(thm)],[c_228,c_1]) ).
cnf(c_1742,plain,
ld(i(A),mult(A,B)) = mult(i(i(A)),ld(i(A),B)),
inference(paramod,[status(thm)],[c_51,c_228]) ).
cnf(c_269,plain,
ld(i(A),mult(A,B)) = mult(A,ld(i(A),B)),
inference(paramod,[status(thm)],[c_51,c_1742]) ).
cnf(c_1743,plain,
ld(mult(ld(A,i(B)),A),i(A)) = i(ld(B,A)),
inference(paramod,[status(thm)],[c_133,c_53]) ).
cnf(c_1744,plain,
ld(mult(A,A),mult(A,i(i(B)))) = i(ld(B,A)),
inference(paramod,[status(thm)],[c_83,c_1743]) ).
cnf(c_1745,plain,
ld(mult(A,A),mult(A,B)) = i(ld(B,A)),
inference(paramod,[status(thm)],[c_51,c_1744]) ).
cnf(c_317,plain,
ld(mult(A,A),mult(A,B)) = mult(i(A),B),
inference(paramod,[status(thm)],[c_63,c_1745]) ).
cnf(c_348,plain,
ld(mult(A,A),B) = mult(i(A),ld(A,B)),
inference(paramod,[status(thm)],[c_1,c_317]) ).
cnf(c_1746,plain,
i(mult(i(A),ld(A,B))) = mult(i(B),mult(A,A)),
inference(paramod,[status(thm)],[c_348,c_63]) ).
cnf(c_1747,plain,
ld(ld(A,B),i(i(A))) = mult(i(B),mult(A,A)),
inference(paramod,[status(thm)],[c_22,c_1746]) ).
cnf(c_1748,plain,
ld(ld(A,B),A) = mult(i(B),mult(A,A)),
inference(paramod,[status(thm)],[c_51,c_1747]) ).
cnf(c_366,plain,
mult(ld(A,B),B) = mult(i(A),mult(B,B)),
inference(paramod,[status(thm)],[c_202,c_1748]) ).
cnf(c_410,plain,
ld(ld(A,B),A) = mult(i(B),mult(A,A)),
inference(paramod,[status(thm)],[c_366,c_202]) ).
cnf(c_1749,plain,
mult(i(A),B) = mult(i(ld(i(B),A)),mult(B,B)),
inference(paramod,[status(thm)],[c_108,c_366]) ).
cnf(c_1750,plain,
mult(i(A),B) = mult(mult(i(A),i(B)),mult(B,B)),
inference(paramod,[status(thm)],[c_63,c_1749]) ).
cnf(c_421,plain,
mult(mult(i(A),i(B)),mult(B,B)) = mult(i(A),B),
inference(copy,[status(thm)],[c_1750]) ).
cnf(c_1751,plain,
mult(A,mult(mult(mult(i(A),ld(B,A)),ld(B,A)),ld(ld(B,A),A))) = mult(mult(ld(B,A),B),ld(B,A)),
inference(paramod,[status(thm)],[c_33,c_66]) ).
cnf(c_1752,plain,
mult(A,mult(mult(mult(i(A),ld(B,A)),B),ld(B,A))) = mult(mult(ld(B,A),B),ld(B,A)),
inference(paramod,[status(thm)],[c_33,c_1751]) ).
cnf(c_1753,plain,
mult(A,ld(ld(ld(B,A),A),A)) = mult(mult(ld(B,A),B),ld(B,A)),
inference(paramod,[status(thm)],[c_139,c_1752]) ).
cnf(c_534,plain,
mult(mult(ld(A,B),A),ld(A,B)) = mult(B,ld(ld(ld(A,B),B),B)),
inference(copy,[status(thm)],[c_1753]) ).
cnf(c_1754,plain,
mult(A,mult(mult(mult(i(A),mult(B,B)),i(B)),ld(mult(B,B),A))) = mult(B,ld(mult(B,B),A)),
inference(paramod,[status(thm)],[c_131,c_66]) ).
cnf(c_1755,plain,
mult(A,mult(mult(mult(i(A),i(B)),mult(B,B)),ld(mult(B,B),A))) = mult(B,ld(mult(B,B),A)),
inference(paramod,[status(thm)],[c_222,c_1754]) ).
cnf(c_1756,plain,
mult(A,mult(mult(i(A),B),ld(mult(B,B),A))) = mult(B,ld(mult(B,B),A)),
inference(paramod,[status(thm)],[c_421,c_1755]) ).
cnf(c_1757,plain,
mult(A,mult(mult(i(A),B),mult(i(B),ld(B,A)))) = mult(B,ld(mult(B,B),A)),
inference(paramod,[status(thm)],[c_348,c_1756]) ).
cnf(c_1758,plain,
mult(A,mult(mult(i(A),B),mult(i(B),ld(B,A)))) = mult(B,mult(i(B),ld(B,A))),
inference(paramod,[status(thm)],[c_348,c_1757]) ).
cnf(c_537,plain,
mult(A,mult(mult(i(A),B),mult(i(B),ld(B,A)))) = mult(i(B),A),
inference(paramod,[status(thm)],[c_264,c_1758]) ).
cnf(c_1759,plain,
mult(i(A),i(mult(A,B))) = i(mult(A,mult(B,A))),
inference(paramod,[status(thm)],[c_181,c_21]) ).
cnf(c_1760,plain,
mult(i(A),ld(B,i(A))) = i(mult(A,mult(B,A))),
inference(paramod,[status(thm)],[c_22,c_1759]) ).
cnf(c_1761,plain,
mult(i(A),ld(B,i(A))) = ld(mult(B,A),i(A)),
inference(paramod,[status(thm)],[c_22,c_1760]) ).
cnf(c_615,plain,
ld(mult(A,B),i(B)) = mult(i(B),ld(A,i(B))),
inference(copy,[status(thm)],[c_1761]) ).
cnf(c_1762,plain,
ld(mult(i(A),i(B)),mult(i(A),ld(B,A))) = i(i(A)),
inference(paramod,[status(thm)],[c_21,c_181]) ).
cnf(c_616,plain,
ld(mult(i(A),i(B)),mult(i(A),ld(B,A))) = A,
inference(paramod,[status(thm)],[c_51,c_1762]) ).
cnf(c_1763,plain,
mult(i(A),ld(mult(i(A),B),i(A))) = ld(A,i(B)),
inference(paramod,[status(thm)],[c_615,c_134]) ).
cnf(c_645,plain,
mult(i(A),ld(mult(A,B),A)) = ld(A,i(B)),
inference(paramod,[status(thm)],[c_167,c_1763]) ).
cnf(c_1764,plain,
mult(i(A),ld(B,A)) = ld(A,i(ld(A,B))),
inference(paramod,[status(thm)],[c_1,c_645]) ).
cnf(c_1765,plain,
mult(i(A),ld(B,A)) = ld(A,mult(i(B),A)),
inference(paramod,[status(thm)],[c_63,c_1764]) ).
cnf(c_1766,plain,
mult(i(A),ld(B,A)) = mult(mult(i(A),i(B)),A),
inference(paramod,[status(thm)],[c_42,c_1765]) ).
cnf(c_646,plain,
mult(mult(i(A),i(B)),A) = mult(i(A),ld(B,A)),
inference(copy,[status(thm)],[c_1766]) ).
cnf(c_677,plain,
ld(mult(A,B),B) = mult(i(B),ld(A,B)),
inference(paramod,[status(thm)],[c_646,c_152]) ).
cnf(c_1767,plain,
i(mult(i(A),ld(B,A))) = mult(i(A),mult(B,A)),
inference(paramod,[status(thm)],[c_677,c_63]) ).
cnf(c_1768,plain,
ld(ld(B,A),i(i(A))) = mult(i(A),mult(B,A)),
inference(paramod,[status(thm)],[c_22,c_1767]) ).
cnf(c_726,plain,
ld(ld(A,B),B) = mult(i(B),mult(A,B)),
inference(paramod,[status(thm)],[c_51,c_1768]) ).
cnf(c_760,plain,
mult(mult(ld(A,B),A),ld(A,B)) = mult(B,ld(mult(i(B),mult(A,B)),B)),
inference(paramod,[status(thm)],[c_726,c_534]) ).
cnf(c_1769,plain,
ld(i(A),i(i(B))) = mult(i(i(B)),ld(ld(A,B),i(i(B)))),
inference(paramod,[status(thm)],[c_21,c_615]) ).
cnf(c_1770,plain,
ld(i(A),B) = mult(i(i(B)),ld(ld(A,B),i(i(B)))),
inference(paramod,[status(thm)],[c_51,c_1769]) ).
cnf(c_1771,plain,
ld(i(A),B) = mult(B,ld(ld(A,B),i(i(B)))),
inference(paramod,[status(thm)],[c_51,c_1770]) ).
cnf(c_1772,plain,
ld(i(A),B) = mult(B,ld(ld(A,B),B)),
inference(paramod,[status(thm)],[c_51,c_1771]) ).
cnf(c_1773,plain,
ld(i(A),B) = mult(B,mult(i(B),mult(A,B))),
inference(paramod,[status(thm)],[c_726,c_1772]) ).
cnf(c_784,plain,
mult(A,mult(i(A),mult(B,A))) = ld(i(B),A),
inference(copy,[status(thm)],[c_1773]) ).
cnf(c_1774,plain,
ld(mult(A,i(B)),B) = mult(i(i(B)),ld(A,i(i(B)))),
inference(paramod,[status(thm)],[c_51,c_615]) ).
cnf(c_1775,plain,
ld(mult(A,i(B)),B) = mult(B,ld(A,i(i(B)))),
inference(paramod,[status(thm)],[c_51,c_1774]) ).
cnf(c_788,plain,
ld(mult(A,i(B)),B) = mult(B,ld(A,B)),
inference(paramod,[status(thm)],[c_51,c_1775]) ).
cnf(c_1776,plain,
ld(mult(A,i(mult(B,A))),mult(B,A)) = mult(mult(B,A),mult(mult(i(A),B),A)),
inference(paramod,[status(thm)],[c_42,c_788]) ).
cnf(c_1777,plain,
ld(mult(A,ld(A,i(B))),mult(B,A)) = mult(mult(B,A),mult(mult(i(A),B),A)),
inference(paramod,[status(thm)],[c_22,c_1776]) ).
cnf(c_1778,plain,
ld(i(B),mult(B,A)) = mult(mult(B,A),mult(mult(i(A),B),A)),
inference(paramod,[status(thm)],[c_1,c_1777]) ).
cnf(c_1779,plain,
mult(B,ld(i(B),A)) = mult(mult(B,A),mult(mult(i(A),B),A)),
inference(paramod,[status(thm)],[c_269,c_1778]) ).
cnf(c_1780,plain,
mult(B,ld(i(B),A)) = mult(mult(B,B),A),
inference(paramod,[status(thm)],[c_49,c_1779]) ).
cnf(c_817,plain,
mult(mult(A,A),B) = mult(A,ld(i(A),B)),
inference(copy,[status(thm)],[c_1780]) ).
cnf(c_1781,plain,
ld(A,i(mult(i(A),i(B)))) = i(mult(i(A),ld(B,A))),
inference(paramod,[status(thm)],[c_616,c_53]) ).
cnf(c_1782,plain,
ld(A,ld(i(B),i(i(A)))) = i(mult(i(A),ld(B,A))),
inference(paramod,[status(thm)],[c_22,c_1781]) ).
cnf(c_1783,plain,
ld(A,ld(i(B),A)) = i(mult(i(A),ld(B,A))),
inference(paramod,[status(thm)],[c_51,c_1782]) ).
cnf(c_1784,plain,
mult(ld(A,i(i(B))),A) = i(mult(i(A),ld(B,A))),
inference(paramod,[status(thm)],[c_133,c_1783]) ).
cnf(c_1785,plain,
mult(ld(A,B),A) = i(mult(i(A),ld(B,A))),
inference(paramod,[status(thm)],[c_51,c_1784]) ).
cnf(c_1786,plain,
mult(ld(A,B),A) = ld(ld(B,A),i(i(A))),
inference(paramod,[status(thm)],[c_22,c_1785]) ).
cnf(c_1787,plain,
mult(ld(A,B),A) = ld(ld(B,A),A),
inference(paramod,[status(thm)],[c_51,c_1786]) ).
cnf(c_848,plain,
mult(ld(A,B),A) = mult(i(A),mult(B,A)),
inference(paramod,[status(thm)],[c_726,c_1787]) ).
cnf(c_872,plain,
mult(mult(i(A),mult(B,A)),ld(A,B)) = mult(B,ld(mult(i(B),mult(A,B)),B)),
inference(paramod,[status(thm)],[c_848,c_760]) ).
cnf(c_1788,plain,
mult(i(A),ld(B,A)) = mult(i(ld(B,A)),mult(i(B),ld(B,A))),
inference(paramod,[status(thm)],[c_53,c_848]) ).
cnf(c_1789,plain,
mult(i(A),ld(B,A)) = mult(mult(i(A),B),mult(i(B),ld(B,A))),
inference(paramod,[status(thm)],[c_63,c_1788]) ).
cnf(c_908,plain,
mult(mult(i(A),B),mult(i(B),ld(B,A))) = mult(i(A),ld(B,A)),
inference(copy,[status(thm)],[c_1789]) ).
cnf(c_1790,plain,
ld(mult(i(A),mult(B,A)),A) = mult(i(A),ld(ld(A,B),A)),
inference(paramod,[status(thm)],[c_848,c_677]) ).
cnf(c_930,plain,
ld(mult(i(A),mult(B,A)),A) = mult(i(A),mult(i(B),mult(A,A))),
inference(paramod,[status(thm)],[c_410,c_1790]) ).
cnf(c_937,plain,
mult(A,mult(i(A),ld(B,A))) = mult(i(B),A),
inference(paramod,[status(thm)],[c_908,c_537]) ).
cnf(c_940,plain,
mult(mult(i(A),mult(B,A)),ld(A,B)) = mult(B,mult(i(B),mult(i(A),mult(B,B)))),
inference(paramod,[status(thm)],[c_930,c_872]) ).
cnf(c_1791,plain,
ld(A,mult(mult(i(i(A)),ld(i(A),B)),A)) = mult(mult(i(i(A)),B),A),
inference(paramod,[status(thm)],[c_264,c_42]) ).
cnf(c_1792,plain,
ld(A,mult(mult(A,ld(i(A),B)),A)) = mult(mult(i(i(A)),B),A),
inference(paramod,[status(thm)],[c_51,c_1791]) ).
cnf(c_1793,plain,
ld(A,mult(mult(A,A),mult(B,A))) = mult(mult(i(i(A)),B),A),
inference(paramod,[status(thm)],[c_244,c_1792]) ).
cnf(c_1794,plain,
ld(A,mult(A,ld(i(A),mult(B,A)))) = mult(mult(i(i(A)),B),A),
inference(paramod,[status(thm)],[c_817,c_1793]) ).
cnf(c_1795,plain,
ld(i(A),mult(B,A)) = mult(mult(i(i(A)),B),A),
inference(paramod,[status(thm)],[c_2,c_1794]) ).
cnf(c_1168,plain,
ld(i(A),mult(B,A)) = mult(mult(A,B),A),
inference(paramod,[status(thm)],[c_51,c_1795]) ).
cnf(c_1222,plain,
mult(A,mult(mult(mult(A,mult(i(A),B)),A),C)) = mult(mult(A,B),mult(A,C)),
inference(paramod,[status(thm)],[c_80,c_77]) ).
cnf(c_1796,plain,
ld(i(ld(A,B)),B) = mult(mult(ld(A,B),A),ld(A,B)),
inference(paramod,[status(thm)],[c_1,c_1168]) ).
cnf(c_1797,plain,
ld(mult(i(B),A),B) = mult(mult(ld(A,B),A),ld(A,B)),
inference(paramod,[status(thm)],[c_63,c_1796]) ).
cnf(c_1798,plain,
ld(mult(i(B),A),B) = mult(mult(i(A),mult(B,A)),ld(A,B)),
inference(paramod,[status(thm)],[c_848,c_1797]) ).
cnf(c_1230,plain,
mult(mult(i(A),mult(B,A)),ld(A,B)) = ld(mult(i(B),A),B),
inference(copy,[status(thm)],[c_1798]) ).
cnf(c_1799,plain,
ld(mult(i(B),A),B) = mult(B,mult(i(B),mult(i(A),mult(B,B)))),
inference(paramod,[status(thm)],[c_1230,c_940]) ).
cnf(c_1259,plain,
mult(A,mult(i(A),mult(i(B),mult(A,A)))) = ld(mult(i(A),B),A),
inference(copy,[status(thm)],[c_1799]) ).
cnf(c_1800,plain,
ld(i(A),mult(i(B),A)) = mult(A,ld(i(A),mult(i(A),ld(B,A)))),
inference(paramod,[status(thm)],[c_937,c_269]) ).
cnf(c_1801,plain,
mult(mult(A,i(B)),A) = mult(A,ld(i(A),mult(i(A),ld(B,A)))),
inference(paramod,[status(thm)],[c_1168,c_1800]) ).
cnf(c_1362,plain,
mult(mult(A,i(B)),A) = mult(A,ld(B,A)),
inference(paramod,[status(thm)],[c_2,c_1801]) ).
cnf(c_1802,plain,
mult(A,mult(i(A),mult(i(B),mult(A,A)))) = mult(i(ld(A,B)),A),
inference(paramod,[status(thm)],[c_410,c_937]) ).
cnf(c_1803,plain,
ld(mult(i(A),B),A) = mult(i(ld(A,B)),A),
inference(paramod,[status(thm)],[c_1259,c_1802]) ).
cnf(c_1382,plain,
ld(mult(i(A),B),A) = mult(mult(i(B),A),A),
inference(paramod,[status(thm)],[c_63,c_1803]) ).
cnf(c_1622,plain,
mult(mult(A,B),A) = mult(A,ld(i(B),A)),
inference(paramod,[status(thm)],[c_51,c_1362]) ).
cnf(c_1804,plain,
mult(A,mult(mult(A,ld(i(mult(i(A),B)),A)),C)) = mult(mult(A,B),mult(A,C)),
inference(paramod,[status(thm)],[c_1622,c_1222]) ).
cnf(c_1805,plain,
mult(A,mult(mult(A,ld(ld(B,i(i(A))),A)),C)) = mult(mult(A,B),mult(A,C)),
inference(paramod,[status(thm)],[c_22,c_1804]) ).
cnf(c_1806,plain,
mult(A,mult(mult(A,ld(ld(B,A),A)),C)) = mult(mult(A,B),mult(A,C)),
inference(paramod,[status(thm)],[c_51,c_1805]) ).
cnf(c_1807,plain,
mult(A,mult(mult(A,mult(i(A),mult(B,A))),C)) = mult(mult(A,B),mult(A,C)),
inference(paramod,[status(thm)],[c_726,c_1806]) ).
cnf(c_1808,plain,
mult(A,mult(ld(i(B),A),C)) = mult(mult(A,B),mult(A,C)),
inference(paramod,[status(thm)],[c_784,c_1807]) ).
cnf(c_1651,plain,
mult(mult(A,B),mult(A,C)) = mult(A,mult(ld(i(B),A),C)),
inference(copy,[status(thm)],[c_1808]) ).
cnf(c_1809,plain,
mult(mult(a,ld(i(b),a)),mult(a,c)) != mult(a,mult(mult(mult(b,a),a),c)),
inference(paramod,[status(thm)],[c_1622,c_14]) ).
cnf(c_1810,plain,
mult(a,mult(ld(i(ld(i(b),a)),a),c)) != mult(a,mult(mult(mult(b,a),a),c)),
inference(paramod,[status(thm)],[c_1651,c_1809]) ).
cnf(c_1811,plain,
mult(a,mult(ld(mult(i(a),i(b)),a),c)) != mult(a,mult(mult(mult(b,a),a),c)),
inference(paramod,[status(thm)],[c_63,c_1810]) ).
cnf(c_1812,plain,
mult(a,mult(mult(mult(i(i(b)),a),a),c)) != mult(a,mult(mult(mult(b,a),a),c)),
inference(paramod,[status(thm)],[c_1382,c_1811]) ).
cnf(c_1813,plain,
mult(a,mult(mult(mult(b,a),a),c)) != mult(a,mult(mult(mult(b,a),a),c)),
inference(paramod,[status(thm)],[c_51,c_1812]) ).
cnf(c_1695,plain,
$false,
inference(copy,[status(thm)],[c_1813]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP696-1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.05 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.41 % Computer : n007.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:35:38 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 1377406 was started by sandbox2 on n007,
% 0.15/0.42 % Fri Sep 25 15:35:38 2026
% 0.15/0.42 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.15/0.43
% 0.15/0.43 % From the command line: assign(max_seconds, 300).
% 1.89/0.72
% 1.89/0.72 % Assigning unary symbol i kb_weight 0 and highest precedence (9).
% 1.89/0.72
% 1.89/0.72 % SZS status Unsatisfiable for theBenchmark
% 1.89/0.72
% 1.89/0.72 % Proof 1 at 0.21 (+ 0.06) seconds.
% 1.89/0.72 % Length of proof is 88.
% 1.89/0.72 % Level of proof is 16.
% 1.89/0.72 % Maximum clause weight is 85.000.
% 1.89/0.72 % Given clauses 89.
% 1.89/0.72
% 1.89/0.72 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------