%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP667-10 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n026.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:08 AM UTC 2026
% Result : Unsatisfiable 26.76s 4.05s
% Output : CNFRefutation 26.76s
% Verified :
% SZS Type : Refutation
% Derivation depth : 66
% Number of leaves : 13
% Syntax : Number of formulae : 243 ( 243 unt; 0 def)
% Number of atoms : 243 ( 242 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 4 ( 4 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 4 con; 0-4 aty)
% Number of variables : 472 ( 1 sgn 25 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ifeq_axiom,axiom,
! [VAR_0,VAR_1,VAR_2] : ifeq(VAR_0,VAR_0,VAR_1,VAR_2) = VAR_1,
file('theBenchmark.p',ifeq_axiom) ).
cnf(c_1,plain,
ifeq(A,A,B,C) = B,
inference(clausify,[status(thm)],[ifeq_axiom]) ).
fof(f01,axiom,
! [VAR_0,VAR_1] : mult(VAR_0,ld(VAR_0,VAR_1)) = VAR_1,
file('theBenchmark.p',f01) ).
cnf(c_2,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_3,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_4,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_5,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_6,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_7,plain,
mult(unit,A) = A,
inference(clausify,[status(thm)],[f06]) ).
fof(f07,axiom,
! [VAR_0,VAR_1,VAR_2] : mult(mult(VAR_0,VAR_1),mult(mult(VAR_2,VAR_1),VAR_2)) = mult(mult(VAR_0,mult(mult(VAR_1,VAR_2),VAR_1)),VAR_2),
file('theBenchmark.p',f07) ).
cnf(c_8,plain,
mult(mult(A,B),mult(mult(C,B),C)) = mult(mult(A,mult(mult(B,C),B)),C),
inference(clausify,[status(thm)],[f07]) ).
cnf(c_9,plain,
mult(mult(A,mult(mult(B,C),B)),C) = mult(mult(A,B),mult(mult(C,B),C)),
inference(copy,[status(thm)],[c_8]) ).
fof(f08,axiom,
! [VAR_0,VAR_1] : mult(mult(VAR_0,VAR_1),VAR_0) = mult(VAR_0,mult(VAR_1,VAR_0)),
file('theBenchmark.p',f08) ).
cnf(c_10,plain,
mult(mult(A,B),A) = mult(A,mult(B,A)),
inference(clausify,[status(thm)],[f08]) ).
fof(f09,axiom,
! [VAR_0] : mult(f(VAR_0),f(VAR_0)) = VAR_0,
file('theBenchmark.p',f09) ).
cnf(c_11,plain,
mult(f(A),f(A)) = A,
inference(clausify,[status(thm)],[f09]) ).
fof(f10,axiom,
! [VAR_0,VAR_1,VAR_2] : ifeq(mult(VAR_0,mult(VAR_1,mult(VAR_2,VAR_1))),mult(mult(mult(VAR_0,VAR_1),VAR_2),VAR_1),mult(VAR_1,mult(VAR_0,mult(VAR_1,VAR_2))),mult(mult(mult(VAR_1,VAR_0),VAR_1),VAR_2)) = mult(mult(mult(VAR_1,VAR_0),VAR_1),VAR_2),
file('theBenchmark.p',f10) ).
cnf(c_12,plain,
ifeq(mult(A,mult(B,mult(C,B))),mult(mult(mult(A,B),C),B),mult(B,mult(A,mult(B,C))),mult(mult(mult(B,A),B),C)) = mult(mult(mult(B,A),B),C),
inference(clausify,[status(thm)],[f10]) ).
cnf(c_8137,plain,
ifeq(mult(A,mult(B,mult(C,B))),mult(mult(mult(A,B),C),B),mult(B,mult(A,mult(B,C))),mult(mult(B,mult(A,B)),C)) = mult(mult(mult(B,A),B),C),
inference(paramod,[status(thm)],[c_10,c_12]) ).
cnf(c_13,plain,
ifeq(mult(A,mult(B,mult(C,B))),mult(mult(mult(A,B),C),B),mult(B,mult(A,mult(B,C))),mult(mult(B,mult(A,B)),C)) = mult(mult(B,mult(A,B)),C),
inference(paramod,[status(thm)],[c_10,c_8137]) ).
fof(f11,axiom,
! [VAR_0,VAR_1,VAR_2] : ifeq(mult(mult(VAR_0,VAR_1),mult(VAR_2,VAR_0)),mult(mult(VAR_0,mult(VAR_1,VAR_2)),VAR_0),mult(VAR_0,mult(VAR_1,mult(VAR_0,VAR_2))),mult(mult(mult(VAR_0,VAR_1),VAR_0),VAR_2)) = mult(mult(mult(VAR_0,VAR_1),VAR_0),VAR_2),
file('theBenchmark.p',f11) ).
cnf(c_14,plain,
ifeq(mult(mult(A,B),mult(C,A)),mult(mult(A,mult(B,C)),A),mult(A,mult(B,mult(A,C))),mult(mult(mult(A,B),A),C)) = mult(mult(mult(A,B),A),C),
inference(clausify,[status(thm)],[f11]) ).
cnf(c_8138,plain,
ifeq(mult(mult(A,B),mult(C,A)),mult(A,mult(mult(B,C),A)),mult(A,mult(B,mult(A,C))),mult(mult(mult(A,B),A),C)) = mult(mult(mult(A,B),A),C),
inference(paramod,[status(thm)],[c_10,c_14]) ).
cnf(c_8139,plain,
ifeq(mult(mult(A,B),mult(C,A)),mult(A,mult(mult(B,C),A)),mult(A,mult(B,mult(A,C))),mult(mult(A,mult(B,A)),C)) = mult(mult(mult(A,B),A),C),
inference(paramod,[status(thm)],[c_10,c_8138]) ).
cnf(c_15,plain,
ifeq(mult(mult(A,B),mult(C,A)),mult(A,mult(mult(B,C),A)),mult(A,mult(B,mult(A,C))),mult(mult(A,mult(B,A)),C)) = mult(mult(A,mult(B,A)),C),
inference(paramod,[status(thm)],[c_10,c_8139]) ).
fof(goals,axiom,
mult(a,mult(b,mult(a,c))) != mult(mult(mult(a,b),a),c),
file('theBenchmark.p',goals) ).
cnf(c_17,plain,
mult(a,mult(b,mult(a,c))) != mult(mult(mult(a,b),a),c),
inference(clausify,[status(thm)],[goals]) ).
cnf(c_8140,plain,
mult(a,mult(b,mult(a,c))) != mult(mult(a,mult(b,a)),c),
inference(paramod,[status(thm)],[c_10,c_17]) ).
cnf(c_18,plain,
mult(mult(a,mult(b,a)),c) != mult(a,mult(b,mult(a,c))),
inference(copy,[status(thm)],[c_8140]) ).
cnf(c_8141,plain,
mult(mult(A,mult(B,mult(C,B))),C) = mult(mult(A,B),mult(mult(C,B),C)),
inference(paramod,[status(thm)],[c_10,c_9]) ).
cnf(c_19,plain,
mult(mult(A,mult(B,mult(C,B))),C) = mult(mult(A,B),mult(C,mult(B,C))),
inference(paramod,[status(thm)],[c_10,c_8141]) ).
cnf(c_20,plain,
ld(rd(A,B),A) = B,
inference(paramod,[status(thm)],[c_4,c_3]) ).
cnf(c_21,plain,
rd(A,ld(B,A)) = B,
inference(paramod,[status(thm)],[c_2,c_5]) ).
cnf(c_22,plain,
ld(A,A) = unit,
inference(paramod,[status(thm)],[c_6,c_3]) ).
cnf(c_25,plain,
rd(A,A) = unit,
inference(paramod,[status(thm)],[c_7,c_5]) ).
cnf(c_8142,plain,
mult(A,B) = mult(B,mult(ld(B,A),B)),
inference(paramod,[status(thm)],[c_2,c_10]) ).
cnf(c_26,plain,
mult(A,mult(ld(A,B),A)) = mult(B,A),
inference(copy,[status(thm)],[c_8142]) ).
cnf(c_8143,plain,
mult(A,rd(A,B)) = mult(rd(A,B),mult(B,rd(A,B))),
inference(paramod,[status(thm)],[c_4,c_10]) ).
cnf(c_28,plain,
mult(rd(A,B),mult(B,rd(A,B))) = mult(A,rd(A,B)),
inference(copy,[status(thm)],[c_8143]) ).
cnf(c_31,plain,
ld(f(A),A) = f(A),
inference(paramod,[status(thm)],[c_11,c_3]) ).
cnf(c_8144,plain,
mult(A,f(A)) = mult(f(A),mult(f(A),f(A))),
inference(paramod,[status(thm)],[c_11,c_10]) ).
cnf(c_8145,plain,
mult(A,f(A)) = mult(f(A),A),
inference(paramod,[status(thm)],[c_11,c_8144]) ).
cnf(c_33,plain,
mult(f(A),A) = mult(A,f(A)),
inference(copy,[status(thm)],[c_8145]) ).
cnf(c_8146,plain,
ifeq(mult(rd(A,B),mult(B,mult(C,B))),mult(mult(A,C),B),mult(B,mult(rd(A,B),mult(B,C))),mult(mult(B,mult(rd(A,B),B)),C)) = mult(mult(B,mult(rd(A,B),B)),C),
inference(paramod,[status(thm)],[c_4,c_13]) ).
cnf(c_8147,plain,
ifeq(mult(rd(A,B),mult(B,mult(C,B))),mult(mult(A,C),B),mult(B,mult(rd(A,B),mult(B,C))),mult(mult(B,A),C)) = mult(mult(B,mult(rd(A,B),B)),C),
inference(paramod,[status(thm)],[c_4,c_8146]) ).
cnf(c_34,plain,
ifeq(mult(rd(A,B),mult(B,mult(C,B))),mult(mult(A,C),B),mult(B,mult(rd(A,B),mult(B,C))),mult(mult(B,A),C)) = mult(mult(B,A),C),
inference(paramod,[status(thm)],[c_4,c_8147]) ).
cnf(c_8148,plain,
ifeq(mult(A,mult(B,A)),mult(mult(mult(unit,A),B),A),mult(A,mult(unit,mult(A,B))),mult(mult(A,mult(unit,A)),B)) = mult(mult(A,mult(unit,A)),B),
inference(paramod,[status(thm)],[c_7,c_13]) ).
cnf(c_8149,plain,
ifeq(mult(A,mult(B,A)),mult(mult(A,B),A),mult(A,mult(unit,mult(A,B))),mult(mult(A,mult(unit,A)),B)) = mult(mult(A,mult(unit,A)),B),
inference(paramod,[status(thm)],[c_7,c_8148]) ).
cnf(c_8150,plain,
ifeq(mult(A,mult(B,A)),mult(A,mult(B,A)),mult(A,mult(unit,mult(A,B))),mult(mult(A,mult(unit,A)),B)) = mult(mult(A,mult(unit,A)),B),
inference(paramod,[status(thm)],[c_10,c_8149]) ).
cnf(c_8151,plain,
ifeq(mult(A,mult(B,A)),mult(A,mult(B,A)),mult(A,mult(A,B)),mult(mult(A,mult(unit,A)),B)) = mult(mult(A,mult(unit,A)),B),
inference(paramod,[status(thm)],[c_7,c_8150]) ).
cnf(c_8152,plain,
ifeq(mult(A,mult(B,A)),mult(A,mult(B,A)),mult(A,mult(A,B)),mult(mult(A,A),B)) = mult(mult(A,mult(unit,A)),B),
inference(paramod,[status(thm)],[c_7,c_8151]) ).
cnf(c_8153,plain,
mult(A,mult(A,B)) = mult(mult(A,mult(unit,A)),B),
inference(paramod,[status(thm)],[c_1,c_8152]) ).
cnf(c_8154,plain,
mult(A,mult(A,B)) = mult(mult(A,A),B),
inference(paramod,[status(thm)],[c_7,c_8153]) ).
cnf(c_36,plain,
mult(mult(A,A),B) = mult(A,mult(A,B)),
inference(copy,[status(thm)],[c_8154]) ).
cnf(c_8155,plain,
ifeq(mult(A,mult(B,C)),mult(C,mult(mult(ld(C,A),B),C)),mult(C,mult(ld(C,A),mult(C,B))),mult(mult(C,mult(ld(C,A),C)),B)) = mult(mult(C,mult(ld(C,A),C)),B),
inference(paramod,[status(thm)],[c_2,c_15]) ).
cnf(c_8156,plain,
ifeq(mult(A,mult(B,C)),mult(C,mult(mult(ld(C,A),B),C)),mult(C,mult(ld(C,A),mult(C,B))),mult(mult(A,C),B)) = mult(mult(C,mult(ld(C,A),C)),B),
inference(paramod,[status(thm)],[c_26,c_8155]) ).
cnf(c_37,plain,
ifeq(mult(A,mult(B,C)),mult(C,mult(mult(ld(C,A),B),C)),mult(C,mult(ld(C,A),mult(C,B))),mult(mult(A,C),B)) = mult(mult(A,C),B),
inference(paramod,[status(thm)],[c_26,c_8156]) ).
cnf(c_8157,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_2,c_19]) ).
cnf(c_39,plain,
mult(mult(A,mult(ld(B,C),C)),B) = mult(mult(A,ld(B,C)),mult(C,B)),
inference(paramod,[status(thm)],[c_26,c_8157]) ).
cnf(c_8158,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_4,c_19]) ).
cnf(c_42,plain,
mult(mult(A,mult(B,C)),rd(C,B)) = mult(mult(A,B),mult(C,rd(C,B))),
inference(paramod,[status(thm)],[c_28,c_8158]) ).
cnf(c_8159,plain,
mult(A,B) = mult(mult(rd(A,mult(C,mult(B,C))),C),mult(B,mult(C,B))),
inference(paramod,[status(thm)],[c_4,c_19]) ).
cnf(c_43,plain,
mult(mult(rd(A,mult(B,mult(C,B))),B),mult(C,mult(B,C))) = mult(A,C),
inference(copy,[status(thm)],[c_8159]) ).
cnf(c_8160,plain,
mult(mult(A,mult(rd(B,C),mult(C,rd(B,C)))),C) = mult(mult(A,rd(B,C)),mult(C,B)),
inference(paramod,[status(thm)],[c_4,c_19]) ).
cnf(c_44,plain,
mult(mult(A,mult(B,rd(B,C))),C) = mult(mult(A,rd(B,C)),mult(C,B)),
inference(paramod,[status(thm)],[c_28,c_8160]) ).
cnf(c_45,plain,
rd(mult(mult(A,B),mult(C,mult(B,C))),C) = mult(A,mult(B,mult(C,B))),
inference(paramod,[status(thm)],[c_19,c_5]) ).
cnf(c_8161,plain,
mult(mult(A,B),mult(unit,mult(B,unit))) = mult(A,mult(B,mult(unit,B))),
inference(paramod,[status(thm)],[c_19,c_6]) ).
cnf(c_8162,plain,
mult(mult(A,B),mult(unit,B)) = mult(A,mult(B,mult(unit,B))),
inference(paramod,[status(thm)],[c_6,c_8161]) ).
cnf(c_8163,plain,
mult(mult(A,B),B) = mult(A,mult(B,mult(unit,B))),
inference(paramod,[status(thm)],[c_7,c_8162]) ).
cnf(c_46,plain,
mult(mult(A,B),B) = mult(A,mult(B,B)),
inference(paramod,[status(thm)],[c_7,c_8163]) ).
cnf(c_8164,plain,
mult(mult(A,mult(B,A)),B) = mult(mult(unit,A),mult(B,mult(A,B))),
inference(paramod,[status(thm)],[c_7,c_19]) ).
cnf(c_47,plain,
mult(mult(A,mult(B,A)),B) = mult(A,mult(B,mult(A,B))),
inference(paramod,[status(thm)],[c_7,c_8164]) ).
cnf(c_8165,plain,
mult(mult(A,B),mult(A,mult(B,A))) = mult(A,mult(mult(B,mult(A,B)),A)),
inference(paramod,[status(thm)],[c_19,c_10]) ).
cnf(c_48,plain,
mult(mult(A,B),mult(A,mult(B,A))) = mult(A,mult(B,mult(A,mult(B,A)))),
inference(paramod,[status(thm)],[c_47,c_8165]) ).
cnf(c_50,plain,
ld(A,mult(B,A)) = mult(ld(A,B),A),
inference(paramod,[status(thm)],[c_26,c_3]) ).
cnf(c_8166,plain,
ld(A,B) = mult(ld(A,rd(B,A)),A),
inference(paramod,[status(thm)],[c_4,c_50]) ).
cnf(c_64,plain,
mult(ld(A,rd(B,A)),A) = ld(A,B),
inference(copy,[status(thm)],[c_8166]) ).
cnf(c_8167,plain,
ld(A,A) = mult(ld(A,unit),A),
inference(paramod,[status(thm)],[c_7,c_50]) ).
cnf(c_8168,plain,
unit = mult(ld(A,unit),A),
inference(paramod,[status(thm)],[c_22,c_8167]) ).
cnf(c_65,plain,
mult(ld(A,unit),A) = unit,
inference(copy,[status(thm)],[c_8168]) ).
cnf(c_8169,plain,
ld(A,mult(A,f(A))) = mult(ld(A,f(A)),A),
inference(paramod,[status(thm)],[c_33,c_50]) ).
cnf(c_8170,plain,
f(A) = mult(ld(A,f(A)),A),
inference(paramod,[status(thm)],[c_3,c_8169]) ).
cnf(c_68,plain,
mult(ld(A,f(A)),A) = f(A),
inference(copy,[status(thm)],[c_8170]) ).
cnf(c_71,plain,
rd(unit,A) = ld(A,unit),
inference(paramod,[status(thm)],[c_65,c_5]) ).
cnf(c_90,plain,
rd(f(A),A) = ld(A,f(A)),
inference(paramod,[status(thm)],[c_68,c_5]) ).
cnf(c_8171,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_10]) ).
cnf(c_8172,plain,
mult(f(A),ld(A,f(A))) = mult(ld(A,f(A)),f(A)),
inference(paramod,[status(thm)],[c_2,c_8171]) ).
cnf(c_91,plain,
mult(ld(A,f(A)),f(A)) = mult(f(A),ld(A,f(A))),
inference(copy,[status(thm)],[c_8172]) ).
cnf(c_8173,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_19]) ).
cnf(c_8174,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_2,c_8173]) ).
cnf(c_92,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_91,c_8174]) ).
cnf(c_100,plain,
rd(ld(A,B),A) = ld(A,rd(B,A)),
inference(paramod,[status(thm)],[c_64,c_5]) ).
cnf(c_8175,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_10]) ).
cnf(c_8176,plain,
mult(ld(A,B),ld(A,rd(B,A))) = mult(ld(A,rd(B,A)),rd(B,A)),
inference(paramod,[status(thm)],[c_2,c_8175]) ).
cnf(c_101,plain,
mult(ld(A,rd(B,A)),rd(B,A)) = mult(ld(A,B),ld(A,rd(B,A))),
inference(copy,[status(thm)],[c_8176]) ).
cnf(c_8177,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_19]) ).
cnf(c_8178,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_2,c_8177]) ).
cnf(c_8179,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_2,c_8178]) ).
cnf(c_8180,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_101,c_8179]) ).
cnf(c_104,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_8180]) ).
cnf(c_8181,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_91,c_10]) ).
cnf(c_8182,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_46,c_8181]) ).
cnf(c_171,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_8182]) ).
cnf(c_8183,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_91,c_50]) ).
cnf(c_8184,plain,
ld(A,f(A)) = mult(ld(f(A),ld(A,f(A))),f(A)),
inference(paramod,[status(thm)],[c_3,c_8183]) ).
cnf(c_174,plain,
mult(ld(f(A),ld(A,f(A))),f(A)) = ld(A,f(A)),
inference(copy,[status(thm)],[c_8184]) ).
cnf(c_8185,plain,
ifeq(mult(rd(f(A),f(A)),mult(f(A),mult(B,f(A)))),mult(mult(f(A),B),f(A)),mult(f(A),mult(rd(f(A),f(A)),mult(f(A),B))),mult(A,B)) = mult(mult(f(A),f(A)),B),
inference(paramod,[status(thm)],[c_11,c_34]) ).
cnf(c_8186,plain,
ifeq(mult(unit,mult(f(A),mult(B,f(A)))),mult(mult(f(A),B),f(A)),mult(f(A),mult(rd(f(A),f(A)),mult(f(A),B))),mult(A,B)) = mult(mult(f(A),f(A)),B),
inference(paramod,[status(thm)],[c_25,c_8185]) ).
cnf(c_8187,plain,
ifeq(mult(f(A),mult(B,f(A))),mult(mult(f(A),B),f(A)),mult(f(A),mult(rd(f(A),f(A)),mult(f(A),B))),mult(A,B)) = mult(mult(f(A),f(A)),B),
inference(paramod,[status(thm)],[c_7,c_8186]) ).
cnf(c_8188,plain,
ifeq(mult(f(A),mult(B,f(A))),mult(f(A),mult(B,f(A))),mult(f(A),mult(rd(f(A),f(A)),mult(f(A),B))),mult(A,B)) = mult(mult(f(A),f(A)),B),
inference(paramod,[status(thm)],[c_10,c_8187]) ).
cnf(c_8189,plain,
ifeq(mult(f(A),mult(B,f(A))),mult(f(A),mult(B,f(A))),mult(f(A),mult(unit,mult(f(A),B))),mult(A,B)) = mult(mult(f(A),f(A)),B),
inference(paramod,[status(thm)],[c_25,c_8188]) ).
cnf(c_8190,plain,
ifeq(mult(f(A),mult(B,f(A))),mult(f(A),mult(B,f(A))),mult(f(A),mult(f(A),B)),mult(A,B)) = mult(mult(f(A),f(A)),B),
inference(paramod,[status(thm)],[c_7,c_8189]) ).
cnf(c_8191,plain,
mult(f(A),mult(f(A),B)) = mult(mult(f(A),f(A)),B),
inference(paramod,[status(thm)],[c_1,c_8190]) ).
cnf(c_189,plain,
mult(f(A),mult(f(A),B)) = mult(A,B),
inference(paramod,[status(thm)],[c_11,c_8191]) ).
cnf(c_201,plain,
rd(mult(A,mult(A,B)),B) = mult(A,A),
inference(paramod,[status(thm)],[c_36,c_5]) ).
cnf(c_8192,plain,
mult(A,ld(B,A)) = mult(B,mult(ld(B,A),ld(B,A))),
inference(paramod,[status(thm)],[c_2,c_46]) ).
cnf(c_223,plain,
mult(A,mult(ld(A,B),ld(A,B))) = mult(B,ld(A,B)),
inference(copy,[status(thm)],[c_8192]) ).
cnf(c_8193,plain,
mult(A,B) = mult(rd(A,B),mult(B,B)),
inference(paramod,[status(thm)],[c_4,c_46]) ).
cnf(c_224,plain,
mult(rd(A,B),mult(B,B)) = mult(A,B),
inference(copy,[status(thm)],[c_8193]) ).
cnf(c_8194,plain,
mult(unit,A) = mult(ld(A,unit),mult(A,A)),
inference(paramod,[status(thm)],[c_65,c_46]) ).
cnf(c_8195,plain,
A = mult(ld(A,unit),mult(A,A)),
inference(paramod,[status(thm)],[c_7,c_8194]) ).
cnf(c_229,plain,
mult(ld(A,unit),mult(A,A)) = A,
inference(copy,[status(thm)],[c_8195]) ).
cnf(c_242,plain,
rd(A,mult(A,A)) = ld(A,unit),
inference(paramod,[status(thm)],[c_229,c_5]) ).
cnf(c_8196,plain,
rd(f(A),A) = ld(f(A),unit),
inference(paramod,[status(thm)],[c_11,c_242]) ).
cnf(c_8197,plain,
ld(A,f(A)) = ld(f(A),unit),
inference(paramod,[status(thm)],[c_90,c_8196]) ).
cnf(c_257,plain,
ld(f(A),unit) = ld(A,f(A)),
inference(copy,[status(thm)],[c_8197]) ).
cnf(c_8198,plain,
ifeq(mult(A,mult(B,f(A))),mult(f(A),mult(mult(f(A),B),f(A))),mult(f(A),mult(ld(f(A),A),mult(f(A),B))),mult(mult(A,f(A)),B)) = mult(mult(A,f(A)),B),
inference(paramod,[status(thm)],[c_31,c_37]) ).
cnf(c_8199,plain,
ifeq(mult(A,mult(B,f(A))),mult(f(A),mult(f(A),mult(B,f(A)))),mult(f(A),mult(ld(f(A),A),mult(f(A),B))),mult(mult(A,f(A)),B)) = mult(mult(A,f(A)),B),
inference(paramod,[status(thm)],[c_10,c_8198]) ).
cnf(c_8200,plain,
ifeq(mult(A,mult(B,f(A))),mult(A,mult(B,f(A))),mult(f(A),mult(ld(f(A),A),mult(f(A),B))),mult(mult(A,f(A)),B)) = mult(mult(A,f(A)),B),
inference(paramod,[status(thm)],[c_189,c_8199]) ).
cnf(c_8201,plain,
ifeq(mult(A,mult(B,f(A))),mult(A,mult(B,f(A))),mult(f(A),mult(f(A),mult(f(A),B))),mult(mult(A,f(A)),B)) = mult(mult(A,f(A)),B),
inference(paramod,[status(thm)],[c_31,c_8200]) ).
cnf(c_8202,plain,
ifeq(mult(A,mult(B,f(A))),mult(A,mult(B,f(A))),mult(f(A),mult(A,B)),mult(mult(A,f(A)),B)) = mult(mult(A,f(A)),B),
inference(paramod,[status(thm)],[c_189,c_8201]) ).
cnf(c_8203,plain,
mult(f(A),mult(A,B)) = mult(mult(A,f(A)),B),
inference(paramod,[status(thm)],[c_1,c_8202]) ).
cnf(c_267,plain,
mult(mult(A,f(A)),B) = mult(f(A),mult(A,B)),
inference(copy,[status(thm)],[c_8203]) ).
cnf(c_274,plain,
mult(f(A),ld(A,f(A))) = unit,
inference(paramod,[status(thm)],[c_257,c_2]) ).
cnf(c_8204,plain,
mult(ld(A,f(A)),unit) = mult(f(A),mult(ld(A,f(A)),ld(A,f(A)))),
inference(paramod,[status(thm)],[c_274,c_171]) ).
cnf(c_8205,plain,
ld(A,f(A)) = mult(f(A),mult(ld(A,f(A)),ld(A,f(A)))),
inference(paramod,[status(thm)],[c_6,c_8204]) ).
cnf(c_282,plain,
mult(f(A),mult(ld(A,f(A)),ld(A,f(A)))) = ld(A,f(A)),
inference(copy,[status(thm)],[c_8205]) ).
cnf(c_8206,plain,
mult(mult(A,mult(B,f(B))),ld(B,f(B))) = mult(mult(A,B),unit),
inference(paramod,[status(thm)],[c_274,c_92]) ).
cnf(c_284,plain,
mult(mult(A,mult(B,f(B))),ld(B,f(B))) = mult(A,B),
inference(paramod,[status(thm)],[c_6,c_8206]) ).
cnf(c_285,plain,
mult(ld(A,f(A)),f(A)) = unit,
inference(paramod,[status(thm)],[c_274,c_91]) ).
cnf(c_328,plain,
ld(rd(A,B),mult(A,B)) = mult(B,B),
inference(paramod,[status(thm)],[c_224,c_3]) ).
cnf(c_329,plain,
rd(mult(A,B),mult(B,B)) = rd(A,B),
inference(paramod,[status(thm)],[c_224,c_5]) ).
cnf(c_8207,plain,
ld(rd(f(A),ld(A,f(A))),unit) = mult(ld(A,f(A)),ld(A,f(A))),
inference(paramod,[status(thm)],[c_274,c_328]) ).
cnf(c_8208,plain,
ld(A,unit) = mult(ld(A,f(A)),ld(A,f(A))),
inference(paramod,[status(thm)],[c_21,c_8207]) ).
cnf(c_371,plain,
mult(ld(A,f(A)),ld(A,f(A))) = ld(A,unit),
inference(copy,[status(thm)],[c_8208]) ).
cnf(c_379,plain,
mult(f(A),ld(A,unit)) = ld(A,f(A)),
inference(paramod,[status(thm)],[c_371,c_282]) ).
cnf(c_8209,plain,
rd(A,mult(B,B)) = rd(rd(A,B),B),
inference(paramod,[status(thm)],[c_4,c_329]) ).
cnf(c_381,plain,
rd(rd(A,B),B) = rd(A,mult(B,B)),
inference(copy,[status(thm)],[c_8209]) ).
cnf(c_411,plain,
ld(f(A),ld(A,f(A))) = ld(A,unit),
inference(paramod,[status(thm)],[c_379,c_3]) ).
cnf(c_429,plain,
mult(ld(A,unit),f(A)) = ld(A,f(A)),
inference(paramod,[status(thm)],[c_411,c_174]) ).
cnf(c_514,plain,
mult(rd(A,mult(B,B)),B) = rd(A,B),
inference(paramod,[status(thm)],[c_381,c_4]) ).
cnf(c_601,plain,
mult(rd(A,B),f(B)) = rd(A,f(B)),
inference(paramod,[status(thm)],[c_11,c_514]) ).
cnf(c_8210,plain,
mult(A,f(B)) = rd(mult(A,B),f(B)),
inference(paramod,[status(thm)],[c_5,c_601]) ).
cnf(c_622,plain,
rd(mult(A,B),f(B)) = mult(A,f(B)),
inference(copy,[status(thm)],[c_8210]) ).
cnf(c_649,plain,
ld(mult(A,f(B)),mult(A,B)) = f(B),
inference(paramod,[status(thm)],[c_622,c_20]) ).
cnf(c_8211,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_100]) ).
cnf(c_760,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_8211]) ).
cnf(c_8212,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_371,c_39]) ).
cnf(c_8213,plain,
mult(mult(ld(A,f(A)),unit),A) = mult(ld(A,unit),mult(f(A),A)),
inference(paramod,[status(thm)],[c_285,c_8212]) ).
cnf(c_8214,plain,
mult(ld(A,f(A)),A) = mult(ld(A,unit),mult(f(A),A)),
inference(paramod,[status(thm)],[c_6,c_8213]) ).
cnf(c_8215,plain,
f(A) = mult(ld(A,unit),mult(f(A),A)),
inference(paramod,[status(thm)],[c_68,c_8214]) ).
cnf(c_8216,plain,
f(A) = mult(ld(A,unit),mult(A,f(A))),
inference(paramod,[status(thm)],[c_33,c_8215]) ).
cnf(c_805,plain,
mult(ld(A,unit),mult(A,f(A))) = f(A),
inference(copy,[status(thm)],[c_8216]) ).
cnf(c_8217,plain,
mult(mult(A,rd(A,B)),B) = mult(mult(unit,rd(A,B)),mult(B,A)),
inference(paramod,[status(thm)],[c_7,c_44]) ).
cnf(c_1222,plain,
mult(mult(A,rd(A,B)),B) = mult(rd(A,B),mult(B,A)),
inference(paramod,[status(thm)],[c_7,c_8217]) ).
cnf(c_8218,plain,
mult(mult(A,ld(A,rd(B,A))),mult(A,ld(A,B))) = mult(A,mult(ld(A,rd(B,A)),mult(A,mult(ld(A,rd(B,A)),A)))),
inference(paramod,[status(thm)],[c_64,c_48]) ).
cnf(c_8219,plain,
mult(rd(B,A),mult(A,ld(A,B))) = mult(A,mult(ld(A,rd(B,A)),mult(A,mult(ld(A,rd(B,A)),A)))),
inference(paramod,[status(thm)],[c_2,c_8218]) ).
cnf(c_8220,plain,
mult(rd(B,A),B) = mult(A,mult(ld(A,rd(B,A)),mult(A,mult(ld(A,rd(B,A)),A)))),
inference(paramod,[status(thm)],[c_2,c_8219]) ).
cnf(c_8221,plain,
mult(rd(B,A),B) = mult(A,mult(ld(A,rd(B,A)),mult(A,ld(A,B)))),
inference(paramod,[status(thm)],[c_64,c_8220]) ).
cnf(c_8222,plain,
mult(rd(B,A),B) = mult(A,mult(ld(A,rd(B,A)),B)),
inference(paramod,[status(thm)],[c_2,c_8221]) ).
cnf(c_1767,plain,
mult(A,mult(ld(A,rd(B,A)),B)) = mult(rd(B,A),B),
inference(copy,[status(thm)],[c_8222]) ).
cnf(c_8223,plain,
mult(f(A),B) = mult(A,ld(f(A),B)),
inference(paramod,[status(thm)],[c_2,c_189]) ).
cnf(c_2293,plain,
mult(A,ld(f(A),B)) = mult(f(A),B),
inference(copy,[status(thm)],[c_8223]) ).
cnf(c_2294,plain,
ld(f(A),mult(A,B)) = mult(f(A),B),
inference(paramod,[status(thm)],[c_189,c_3]) ).
cnf(c_8224,plain,
mult(mult(A,B),f(A)) = mult(f(A),mult(mult(f(A),B),f(A))),
inference(paramod,[status(thm)],[c_189,c_10]) ).
cnf(c_8225,plain,
mult(mult(A,B),f(A)) = mult(f(A),mult(f(A),mult(B,f(A)))),
inference(paramod,[status(thm)],[c_10,c_8224]) ).
cnf(c_2296,plain,
mult(mult(A,B),f(A)) = mult(A,mult(B,f(A))),
inference(paramod,[status(thm)],[c_189,c_8225]) ).
cnf(c_8226,plain,
ifeq(mult(f(A),mult(f(A),mult(B,f(A)))),mult(mult(mult(f(A),f(A)),B),f(A)),mult(A,mult(f(A),B)),mult(mult(f(A),mult(f(A),f(A))),B)) = mult(mult(f(A),mult(f(A),f(A))),B),
inference(paramod,[status(thm)],[c_189,c_13]) ).
cnf(c_8227,plain,
ifeq(mult(A,mult(B,f(A))),mult(mult(mult(f(A),f(A)),B),f(A)),mult(A,mult(f(A),B)),mult(mult(f(A),mult(f(A),f(A))),B)) = mult(mult(f(A),mult(f(A),f(A))),B),
inference(paramod,[status(thm)],[c_189,c_8226]) ).
cnf(c_8228,plain,
ifeq(mult(A,mult(B,f(A))),mult(mult(A,B),f(A)),mult(A,mult(f(A),B)),mult(mult(f(A),mult(f(A),f(A))),B)) = mult(mult(f(A),mult(f(A),f(A))),B),
inference(paramod,[status(thm)],[c_11,c_8227]) ).
cnf(c_8229,plain,
ifeq(mult(A,mult(B,f(A))),mult(A,mult(B,f(A))),mult(A,mult(f(A),B)),mult(mult(f(A),mult(f(A),f(A))),B)) = mult(mult(f(A),mult(f(A),f(A))),B),
inference(paramod,[status(thm)],[c_2296,c_8228]) ).
cnf(c_8230,plain,
ifeq(mult(A,mult(B,f(A))),mult(A,mult(B,f(A))),mult(A,mult(f(A),B)),mult(mult(f(A),A),B)) = mult(mult(f(A),mult(f(A),f(A))),B),
inference(paramod,[status(thm)],[c_11,c_8229]) ).
cnf(c_8231,plain,
ifeq(mult(A,mult(B,f(A))),mult(A,mult(B,f(A))),mult(A,mult(f(A),B)),mult(mult(A,f(A)),B)) = mult(mult(f(A),mult(f(A),f(A))),B),
inference(paramod,[status(thm)],[c_33,c_8230]) ).
cnf(c_8232,plain,
ifeq(mult(A,mult(B,f(A))),mult(A,mult(B,f(A))),mult(A,mult(f(A),B)),mult(f(A),mult(A,B))) = mult(mult(f(A),mult(f(A),f(A))),B),
inference(paramod,[status(thm)],[c_267,c_8231]) ).
cnf(c_8233,plain,
mult(A,mult(f(A),B)) = mult(mult(f(A),mult(f(A),f(A))),B),
inference(paramod,[status(thm)],[c_1,c_8232]) ).
cnf(c_8234,plain,
mult(A,mult(f(A),B)) = mult(mult(f(A),A),B),
inference(paramod,[status(thm)],[c_11,c_8233]) ).
cnf(c_8235,plain,
mult(A,mult(f(A),B)) = mult(mult(A,f(A)),B),
inference(paramod,[status(thm)],[c_33,c_8234]) ).
cnf(c_8236,plain,
mult(A,mult(f(A),B)) = mult(f(A),mult(A,B)),
inference(paramod,[status(thm)],[c_267,c_8235]) ).
cnf(c_2299,plain,
mult(f(A),mult(A,B)) = mult(A,mult(f(A),B)),
inference(copy,[status(thm)],[c_8236]) ).
cnf(c_2372,plain,
mult(mult(A,f(A)),B) = mult(A,mult(f(A),B)),
inference(paramod,[status(thm)],[c_2299,c_267]) ).
cnf(c_8237,plain,
ld(f(A),B) = mult(f(A),ld(A,B)),
inference(paramod,[status(thm)],[c_2,c_2294]) ).
cnf(c_2399,plain,
mult(f(A),ld(A,B)) = ld(f(A),B),
inference(copy,[status(thm)],[c_8237]) ).
cnf(c_8238,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_805,c_43]) ).
cnf(c_8239,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_46,c_8238]) ).
cnf(c_8240,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_11,c_8239]) ).
cnf(c_8241,plain,
mult(mult(rd(A,mult(B,B)),mult(B,f(B))),mult(ld(B,unit),mult(B,mult(f(B),ld(B,unit))))) = mult(A,ld(B,unit)),
inference(paramod,[status(thm)],[c_2372,c_8240]) ).
cnf(c_8242,plain,
mult(mult(rd(A,mult(B,B)),mult(B,f(B))),mult(ld(B,unit),mult(B,ld(f(B),unit)))) = mult(A,ld(B,unit)),
inference(paramod,[status(thm)],[c_2399,c_8241]) ).
cnf(c_8243,plain,
mult(mult(rd(A,mult(B,B)),mult(B,f(B))),mult(ld(B,unit),mult(f(B),unit))) = mult(A,ld(B,unit)),
inference(paramod,[status(thm)],[c_2293,c_8242]) ).
cnf(c_8244,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_6,c_8243]) ).
cnf(c_8245,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_429,c_8244]) ).
cnf(c_8246,plain,
mult(rd(A,mult(B,B)),B) = mult(A,ld(B,unit)),
inference(paramod,[status(thm)],[c_284,c_8245]) ).
cnf(c_8247,plain,
rd(A,B) = mult(A,ld(B,unit)),
inference(paramod,[status(thm)],[c_514,c_8246]) ).
cnf(c_3884,plain,
mult(A,ld(B,unit)) = rd(A,B),
inference(copy,[status(thm)],[c_8247]) ).
cnf(c_4381,plain,
ld(A,rd(A,B)) = ld(B,unit),
inference(paramod,[status(thm)],[c_3884,c_3]) ).
cnf(c_8248,plain,
mult(A,B) = rd(A,rd(unit,B)),
inference(paramod,[status(thm)],[c_20,c_3884]) ).
cnf(c_8249,plain,
mult(A,B) = rd(A,ld(B,unit)),
inference(paramod,[status(thm)],[c_71,c_8248]) ).
cnf(c_4390,plain,
rd(A,ld(B,unit)) = mult(A,B),
inference(copy,[status(thm)],[c_8249]) ).
cnf(c_8250,plain,
mult(f(A),rd(f(A),B)) = mult(A,ld(B,unit)),
inference(paramod,[status(thm)],[c_3884,c_189]) ).
cnf(c_4431,plain,
mult(f(A),rd(f(A),B)) = rd(A,B),
inference(paramod,[status(thm)],[c_3884,c_8250]) ).
cnf(c_8251,plain,
rd(mult(A,rd(A,B)),ld(B,unit)) = mult(A,A),
inference(paramod,[status(thm)],[c_3884,c_201]) ).
cnf(c_8252,plain,
mult(mult(A,rd(A,B)),B) = mult(A,A),
inference(paramod,[status(thm)],[c_4390,c_8251]) ).
cnf(c_4443,plain,
mult(rd(A,B),mult(B,A)) = mult(A,A),
inference(paramod,[status(thm)],[c_1222,c_8252]) ).
cnf(c_8253,plain,
mult(rd(ld(A,B),A),B) = mult(ld(A,B),ld(A,B)),
inference(paramod,[status(thm)],[c_2,c_4443]) ).
cnf(c_5586,plain,
mult(ld(A,rd(B,A)),B) = mult(ld(A,B),ld(A,B)),
inference(paramod,[status(thm)],[c_100,c_8253]) ).
cnf(c_8254,plain,
mult(A,mult(ld(A,B),ld(A,B))) = mult(rd(B,A),B),
inference(paramod,[status(thm)],[c_5586,c_1767]) ).
cnf(c_8255,plain,
mult(B,ld(A,B)) = mult(rd(B,A),B),
inference(paramod,[status(thm)],[c_223,c_8254]) ).
cnf(c_5704,plain,
mult(rd(A,B),A) = mult(A,ld(B,A)),
inference(copy,[status(thm)],[c_8255]) ).
cnf(c_8256,plain,
ld(A,mult(A,ld(B,A))) = mult(ld(A,rd(A,B)),A),
inference(paramod,[status(thm)],[c_5704,c_50]) ).
cnf(c_8257,plain,
ld(B,A) = mult(ld(A,rd(A,B)),A),
inference(paramod,[status(thm)],[c_3,c_8256]) ).
cnf(c_8258,plain,
ld(B,A) = mult(ld(B,unit),A),
inference(paramod,[status(thm)],[c_4381,c_8257]) ).
cnf(c_6027,plain,
mult(ld(A,unit),B) = ld(A,B),
inference(copy,[status(thm)],[c_8258]) ).
cnf(c_6380,plain,
rd(ld(A,B),B) = ld(A,unit),
inference(paramod,[status(thm)],[c_6027,c_5]) ).
cnf(c_6640,plain,
rd(A,mult(B,A)) = ld(B,unit),
inference(paramod,[status(thm)],[c_3,c_6380]) ).
cnf(c_6667,plain,
ld(mult(A,f(B)),rd(mult(A,B),mult(A,f(B)))) = ld(A,unit),
inference(paramod,[status(thm)],[c_6640,c_760]) ).
cnf(c_8259,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_104]) ).
cnf(c_8260,plain,
mult(mult(A,mult(B,f(C))),mult(f(C),ld(B,unit))) = mult(mult(A,mult(B,C)),ld(mult(B,f(C)),rd(mult(B,C),mult(B,f(C))))),
inference(paramod,[status(thm)],[c_6667,c_8259]) ).
cnf(c_8261,plain,
mult(mult(A,mult(B,f(C))),rd(f(C),B)) = mult(mult(A,mult(B,C)),ld(mult(B,f(C)),rd(mult(B,C),mult(B,f(C))))),
inference(paramod,[status(thm)],[c_3884,c_8260]) ).
cnf(c_8262,plain,
mult(mult(A,B),mult(f(C),rd(f(C),B))) = mult(mult(A,mult(B,C)),ld(mult(B,f(C)),rd(mult(B,C),mult(B,f(C))))),
inference(paramod,[status(thm)],[c_42,c_8261]) ).
cnf(c_8263,plain,
mult(mult(A,B),rd(C,B)) = mult(mult(A,mult(B,C)),ld(mult(B,f(C)),rd(mult(B,C),mult(B,f(C))))),
inference(paramod,[status(thm)],[c_4431,c_8262]) ).
cnf(c_8264,plain,
mult(mult(A,B),rd(C,B)) = mult(mult(A,mult(B,C)),ld(B,unit)),
inference(paramod,[status(thm)],[c_6667,c_8263]) ).
cnf(c_8265,plain,
mult(mult(A,B),rd(C,B)) = rd(mult(A,mult(B,C)),B),
inference(paramod,[status(thm)],[c_3884,c_8264]) ).
cnf(c_8007,plain,
rd(mult(A,mult(B,C)),B) = mult(mult(A,B),rd(C,B)),
inference(copy,[status(thm)],[c_8265]) ).
cnf(c_8266,plain,
mult(mult(mult(A,B),C),rd(mult(B,C),C)) = mult(A,mult(B,mult(C,B))),
inference(paramod,[status(thm)],[c_8007,c_45]) ).
cnf(c_8079,plain,
mult(mult(mult(A,B),C),B) = mult(A,mult(B,mult(C,B))),
inference(paramod,[status(thm)],[c_5,c_8266]) ).
cnf(c_8267,plain,
ifeq(mult(A,mult(B,mult(C,B))),mult(A,mult(B,mult(C,B))),mult(B,mult(A,mult(B,C))),mult(mult(B,mult(A,B)),C)) = mult(mult(B,mult(A,B)),C),
inference(paramod,[status(thm)],[c_8079,c_13]) ).
cnf(c_8268,plain,
mult(B,mult(A,mult(B,C))) = mult(mult(B,mult(A,B)),C),
inference(paramod,[status(thm)],[c_1,c_8267]) ).
cnf(c_8135,plain,
mult(mult(A,mult(B,A)),C) = mult(A,mult(B,mult(A,C))),
inference(copy,[status(thm)],[c_8268]) ).
cnf(c_8136,plain,
$false,
inference(resolve,[status(thm)],[c_8135,c_18]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : GRP667-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.63 % Computer : n026.cluster.edu
% 0.17/0.63 % Model : x86_64 x86_64
% 0.17/0.63 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.63 % Memory : 8046.5625MB
% 0.17/0.63 % OS : Linux 6.8.0-71-generic
% 0.17/0.63 % CPULimit : 300
% 0.17/0.63 % WCLimit : 300
% 0.17/0.63 % DateTime : Fri Sep 25 15:36:56 UTC 2026
% 0.17/0.63 % CPUTime :
% 0.17/0.63 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.17/0.63 % Process 2911001 was started by sandbox2 on n026,
% 0.17/0.63 % Fri Sep 25 15:36:56 2026
% 0.17/0.63 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.17/0.64
% 0.17/0.64 % From the command line: assign(max_seconds, 300).
% 26.76/4.05
% 26.76/4.05 % Assigning unary symbol f kb_weight 0 and highest precedence (10).
% 26.76/4.05
% 26.76/4.05 % SZS status Unsatisfiable for theBenchmark
% 26.76/4.05
% 26.76/4.05 % Proof 1 at 2.61 (+ 0.75) seconds.
% 26.76/4.05 % Length of proof is 98.
% 26.76/4.05 % Level of proof is 24.
% 26.76/4.05 % Maximum clause weight is 112.000.
% 26.76/4.05 % Given clauses 224.
% 26.76/4.05
% 26.76/4.05 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------