%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP768-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/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:25 AM UTC 2026
% Result : Unsatisfiable 36.98s 5.76s
% Output : CNFRefutation 36.98s
% Verified :
% SZS Type : Refutation
% Derivation depth : 70
% Number of leaves : 19
% Syntax : Number of formulae : 413 ( 413 unt; 0 def)
% Number of atoms : 413 ( 412 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 15 ( 15 ~; 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 : 11 ( 11 usr; 4 con; 0-2 aty)
% Number of variables : 675 ( 0 sgn 32 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(sos01,axiom,
! [VAR_0] : product(VAR_0,one) = VAR_0,
file('theBenchmark.p',sos01) ).
cnf(c_1,plain,
product(A,one) = A,
inference(clausify,[status(thm)],[sos01]) ).
fof(sos02,axiom,
! [VAR_0] : product(one,VAR_0) = VAR_0,
file('theBenchmark.p',sos02) ).
cnf(c_2,plain,
product(one,A) = A,
inference(clausify,[status(thm)],[sos02]) ).
fof(sos03,axiom,
! [VAR_0,VAR_1] : product(VAR_0,difference(VAR_0,VAR_1)) = VAR_1,
file('theBenchmark.p',sos03) ).
cnf(c_3,plain,
product(A,difference(A,B)) = B,
inference(clausify,[status(thm)],[sos03]) ).
fof(sos04,axiom,
! [VAR_0,VAR_1] : difference(VAR_0,product(VAR_0,VAR_1)) = VAR_1,
file('theBenchmark.p',sos04) ).
cnf(c_4,plain,
difference(A,product(A,B)) = B,
inference(clausify,[status(thm)],[sos04]) ).
fof(sos05,axiom,
! [VAR_0,VAR_1] : quotient(product(VAR_0,VAR_1),VAR_1) = VAR_0,
file('theBenchmark.p',sos05) ).
cnf(c_5,plain,
quotient(product(A,B),B) = A,
inference(clausify,[status(thm)],[sos05]) ).
fof(sos06,axiom,
! [VAR_0,VAR_1] : product(quotient(VAR_0,VAR_1),VAR_1) = VAR_0,
file('theBenchmark.p',sos06) ).
cnf(c_6,plain,
product(quotient(A,B),B) = A,
inference(clausify,[status(thm)],[sos06]) ).
fof(sos07,axiom,
! [VAR_0,VAR_1,VAR_2] : difference(VAR_0,product(product(VAR_0,VAR_1),VAR_2)) = quotient(product(VAR_1,product(VAR_2,VAR_0)),VAR_0),
file('theBenchmark.p',sos07) ).
cnf(c_7,plain,
difference(A,product(product(A,B),C)) = quotient(product(B,product(C,A)),A),
inference(clausify,[status(thm)],[sos07]) ).
fof(sos08,axiom,
! [VAR_0,VAR_1,VAR_2] : difference(product(VAR_0,VAR_1),product(VAR_0,product(VAR_1,VAR_2))) = quotient(quotient(product(VAR_2,product(VAR_0,VAR_1)),VAR_1),VAR_0),
file('theBenchmark.p',sos08) ).
cnf(c_8,plain,
difference(product(A,B),product(A,product(B,C))) = quotient(quotient(product(C,product(A,B)),B),A),
inference(clausify,[status(thm)],[sos08]) ).
fof(sos09,axiom,
! [VAR_0] : i(VAR_0) = difference(VAR_0,one),
file('theBenchmark.p',sos09) ).
cnf(c_9,plain,
i(A) = difference(A,one),
inference(clausify,[status(thm)],[sos09]) ).
fof(sos10,axiom,
! [VAR_0] : j(VAR_0) = quotient(one,VAR_0),
file('theBenchmark.p',sos10) ).
cnf(c_10,plain,
j(A) = quotient(one,A),
inference(clausify,[status(thm)],[sos10]) ).
fof(sos11,axiom,
! [VAR_0] : product(i(VAR_0),VAR_0) = product(VAR_0,j(VAR_0)),
file('theBenchmark.p',sos11) ).
cnf(c_11,plain,
product(i(A),A) = product(A,j(A)),
inference(clausify,[status(thm)],[sos11]) ).
cnf(c_12094,plain,
product(difference(A,one),A) = product(A,j(A)),
inference(paramod,[status(thm)],[c_9,c_11]) ).
cnf(c_12,plain,
product(difference(A,one),A) = product(A,quotient(one,A)),
inference(paramod,[status(thm)],[c_10,c_12094]) ).
fof(sos12,axiom,
! [VAR_0] : eta(VAR_0) = product(i(VAR_0),VAR_0),
file('theBenchmark.p',sos12) ).
cnf(c_13,plain,
eta(A) = product(i(A),A),
inference(clausify,[status(thm)],[sos12]) ).
cnf(c_12095,plain,
eta(A) = product(difference(A,one),A),
inference(paramod,[status(thm)],[c_9,c_13]) ).
cnf(c_14,plain,
eta(A) = product(A,quotient(one,A)),
inference(paramod,[status(thm)],[c_12,c_12095]) ).
fof(sos13,axiom,
! [VAR_0,VAR_1] : product(i(i(VAR_0)),VAR_1) = product(eta(VAR_0),product(VAR_0,VAR_1)),
file('theBenchmark.p',sos13) ).
cnf(c_15,plain,
product(i(i(A)),B) = product(eta(A),product(A,B)),
inference(clausify,[status(thm)],[sos13]) ).
cnf(c_12096,plain,
product(i(difference(A,one)),B) = product(eta(A),product(A,B)),
inference(paramod,[status(thm)],[c_9,c_15]) ).
cnf(c_12097,plain,
product(difference(difference(A,one),one),B) = product(eta(A),product(A,B)),
inference(paramod,[status(thm)],[c_9,c_12096]) ).
cnf(c_12098,plain,
product(difference(difference(A,one),one),B) = product(product(A,quotient(one,A)),product(A,B)),
inference(paramod,[status(thm)],[c_14,c_12097]) ).
cnf(c_16,plain,
product(product(A,quotient(one,A)),product(A,B)) = product(difference(difference(A,one),one),B),
inference(copy,[status(thm)],[c_12098]) ).
fof(sos14,axiom,
! [VAR_0,VAR_1] : product(VAR_0,product(eta(VAR_0),VAR_1)) = product(j(j(VAR_0)),VAR_1),
file('theBenchmark.p',sos14) ).
cnf(c_17,plain,
product(A,product(eta(A),B)) = product(j(j(A)),B),
inference(clausify,[status(thm)],[sos14]) ).
cnf(c_12099,plain,
product(A,product(product(A,quotient(one,A)),B)) = product(j(j(A)),B),
inference(paramod,[status(thm)],[c_14,c_17]) ).
cnf(c_12100,plain,
product(A,product(product(A,quotient(one,A)),B)) = product(j(quotient(one,A)),B),
inference(paramod,[status(thm)],[c_10,c_12099]) ).
cnf(c_18,plain,
product(A,product(product(A,quotient(one,A)),B)) = product(quotient(one,quotient(one,A)),B),
inference(paramod,[status(thm)],[c_10,c_12100]) ).
fof(sos15,axiom,
! [VAR_0,VAR_1] : product(VAR_0,product(VAR_1,eta(VAR_0))) = product(product(VAR_0,VAR_1),eta(VAR_0)),
file('theBenchmark.p',sos15) ).
cnf(c_19,plain,
product(A,product(B,eta(A))) = product(product(A,B),eta(A)),
inference(clausify,[status(thm)],[sos15]) ).
cnf(c_12101,plain,
product(A,product(B,product(A,quotient(one,A)))) = product(product(A,B),eta(A)),
inference(paramod,[status(thm)],[c_14,c_19]) ).
cnf(c_12102,plain,
product(A,product(B,product(A,quotient(one,A)))) = product(product(A,B),product(A,quotient(one,A))),
inference(paramod,[status(thm)],[c_14,c_12101]) ).
cnf(c_20,plain,
product(product(A,B),product(A,quotient(one,A))) = product(A,product(B,product(A,quotient(one,A)))),
inference(copy,[status(thm)],[c_12102]) ).
fof(sos16,axiom,
! [VAR_0,VAR_1,VAR_2] : product(eta(VAR_0),product(VAR_1,VAR_2)) = product(product(eta(VAR_0),VAR_1),VAR_2),
file('theBenchmark.p',sos16) ).
cnf(c_21,plain,
product(eta(A),product(B,C)) = product(product(eta(A),B),C),
inference(clausify,[status(thm)],[sos16]) ).
cnf(c_12103,plain,
product(product(A,quotient(one,A)),product(B,C)) = product(product(eta(A),B),C),
inference(paramod,[status(thm)],[c_14,c_21]) ).
cnf(c_12104,plain,
product(product(A,quotient(one,A)),product(B,C)) = product(product(product(A,quotient(one,A)),B),C),
inference(paramod,[status(thm)],[c_14,c_12103]) ).
cnf(c_22,plain,
product(product(product(A,quotient(one,A)),B),C) = product(product(A,quotient(one,A)),product(B,C)),
inference(copy,[status(thm)],[c_12104]) ).
fof(sos17,axiom,
! [VAR_0] : quotient(j(VAR_0),VAR_0) = product(j(VAR_0),i(VAR_0)),
file('theBenchmark.p',sos17) ).
cnf(c_23,plain,
quotient(j(A),A) = product(j(A),i(A)),
inference(clausify,[status(thm)],[sos17]) ).
cnf(c_12105,plain,
quotient(quotient(one,A),A) = product(j(A),i(A)),
inference(paramod,[status(thm)],[c_10,c_23]) ).
cnf(c_12106,plain,
quotient(quotient(one,A),A) = product(quotient(one,A),i(A)),
inference(paramod,[status(thm)],[c_10,c_12105]) ).
cnf(c_12107,plain,
quotient(quotient(one,A),A) = product(quotient(one,A),difference(A,one)),
inference(paramod,[status(thm)],[c_9,c_12106]) ).
cnf(c_24,plain,
product(quotient(one,A),difference(A,one)) = quotient(quotient(one,A),A),
inference(copy,[status(thm)],[c_12107]) ).
fof(sos19,axiom,
! [VAR_0,VAR_1] : t(VAR_0,VAR_1) = quotient(product(VAR_0,VAR_1),VAR_0),
file('theBenchmark.p',sos19) ).
cnf(c_27,plain,
t(A,B) = quotient(product(A,B),A),
inference(clausify,[status(thm)],[sos19]) ).
fof(goals,axiom,
t(eta(x0),product(x1,x2)) != product(t(eta(x0),x1),t(eta(x0),x2)),
file('theBenchmark.p',goals) ).
cnf(c_28,plain,
t(eta(x0),product(x1,x2)) != product(t(eta(x0),x1),t(eta(x0),x2)),
inference(clausify,[status(thm)],[goals]) ).
cnf(c_12108,plain,
t(product(x0,quotient(one,x0)),product(x1,x2)) != product(t(eta(x0),x1),t(eta(x0),x2)),
inference(paramod,[status(thm)],[c_14,c_28]) ).
cnf(c_12109,plain,
quotient(product(product(x0,quotient(one,x0)),product(x1,x2)),product(x0,quotient(one,x0))) != product(t(eta(x0),x1),t(eta(x0),x2)),
inference(paramod,[status(thm)],[c_27,c_12108]) ).
cnf(c_12110,plain,
quotient(product(product(x0,quotient(one,x0)),product(x1,x2)),product(x0,quotient(one,x0))) != product(t(product(x0,quotient(one,x0)),x1),t(eta(x0),x2)),
inference(paramod,[status(thm)],[c_14,c_12109]) ).
cnf(c_12111,plain,
quotient(product(product(x0,quotient(one,x0)),product(x1,x2)),product(x0,quotient(one,x0))) != product(quotient(product(product(x0,quotient(one,x0)),x1),product(x0,quotient(one,x0))),t(eta(x0),x2)),
inference(paramod,[status(thm)],[c_27,c_12110]) ).
cnf(c_12112,plain,
quotient(product(product(x0,quotient(one,x0)),product(x1,x2)),product(x0,quotient(one,x0))) != product(quotient(product(product(x0,quotient(one,x0)),x1),product(x0,quotient(one,x0))),t(product(x0,quotient(one,x0)),x2)),
inference(paramod,[status(thm)],[c_14,c_12111]) ).
cnf(c_12113,plain,
quotient(product(product(x0,quotient(one,x0)),product(x1,x2)),product(x0,quotient(one,x0))) != product(quotient(product(product(x0,quotient(one,x0)),x1),product(x0,quotient(one,x0))),quotient(product(product(x0,quotient(one,x0)),x2),product(x0,quotient(one,x0)))),
inference(paramod,[status(thm)],[c_27,c_12112]) ).
cnf(c_29,plain,
product(quotient(product(product(x0,quotient(one,x0)),x1),product(x0,quotient(one,x0))),quotient(product(product(x0,quotient(one,x0)),x2),product(x0,quotient(one,x0)))) != quotient(product(product(x0,quotient(one,x0)),product(x1,x2)),product(x0,quotient(one,x0))),
inference(copy,[status(thm)],[c_12113]) ).
cnf(c_12114,plain,
A = difference(one,A),
inference(paramod,[status(thm)],[c_3,c_2]) ).
cnf(c_30,plain,
difference(one,A) = A,
inference(copy,[status(thm)],[c_12114]) ).
cnf(c_31,plain,
difference(A,A) = one,
inference(paramod,[status(thm)],[c_1,c_4]) ).
cnf(c_32,plain,
quotient(A,one) = A,
inference(paramod,[status(thm)],[c_1,c_5]) ).
cnf(c_33,plain,
quotient(A,A) = one,
inference(paramod,[status(thm)],[c_2,c_5]) ).
cnf(c_34,plain,
quotient(A,difference(B,A)) = B,
inference(paramod,[status(thm)],[c_3,c_5]) ).
cnf(c_35,plain,
difference(quotient(A,B),A) = B,
inference(paramod,[status(thm)],[c_6,c_4]) ).
cnf(c_36,plain,
product(A,quotient(product(B,product(C,A)),A)) = product(product(A,B),C),
inference(paramod,[status(thm)],[c_7,c_3]) ).
cnf(c_12115,plain,
difference(A,product(B,C)) = quotient(product(difference(A,B),product(C,A)),A),
inference(paramod,[status(thm)],[c_3,c_7]) ).
cnf(c_37,plain,
quotient(product(difference(A,B),product(C,A)),A) = difference(A,product(B,C)),
inference(copy,[status(thm)],[c_12115]) ).
cnf(c_12116,plain,
difference(product(A,B),product(A,C)) = quotient(quotient(product(difference(B,C),product(A,B)),B),A),
inference(paramod,[status(thm)],[c_3,c_8]) ).
cnf(c_42,plain,
difference(product(A,B),product(A,C)) = quotient(difference(B,product(C,A)),A),
inference(paramod,[status(thm)],[c_37,c_12116]) ).
cnf(c_12117,plain,
difference(A,product(quotient(A,B),product(B,C))) = quotient(quotient(product(C,product(quotient(A,B),B)),B),quotient(A,B)),
inference(paramod,[status(thm)],[c_6,c_8]) ).
cnf(c_43,plain,
difference(A,product(quotient(A,B),product(B,C))) = quotient(quotient(product(C,A),B),quotient(A,B)),
inference(paramod,[status(thm)],[c_6,c_12117]) ).
cnf(c_45,plain,
difference(difference(A,one),product(A,quotient(one,A))) = A,
inference(paramod,[status(thm)],[c_12,c_4]) ).
cnf(c_47,plain,
difference(difference(A,one),product(product(A,quotient(one,A)),B)) = quotient(product(A,product(B,difference(A,one))),difference(A,one)),
inference(paramod,[status(thm)],[c_12,c_7]) ).
cnf(c_12118,plain,
product(product(A,quotient(one,A)),A) = product(difference(difference(A,one),one),one),
inference(paramod,[status(thm)],[c_1,c_16]) ).
cnf(c_48,plain,
product(product(A,quotient(one,A)),A) = difference(difference(A,one),one),
inference(paramod,[status(thm)],[c_1,c_12118]) ).
cnf(c_12119,plain,
product(product(A,quotient(one,A)),B) = product(difference(difference(A,one),one),difference(A,B)),
inference(paramod,[status(thm)],[c_3,c_16]) ).
cnf(c_49,plain,
product(difference(difference(A,one),one),difference(A,B)) = product(product(A,quotient(one,A)),B),
inference(copy,[status(thm)],[c_12119]) ).
cnf(c_50,plain,
difference(product(A,quotient(one,A)),product(difference(difference(A,one),one),B)) = product(A,B),
inference(paramod,[status(thm)],[c_16,c_4]) ).
cnf(c_51,plain,
quotient(product(difference(difference(A,one),one),B),product(A,B)) = product(A,quotient(one,A)),
inference(paramod,[status(thm)],[c_16,c_5]) ).
cnf(c_12120,plain,
product(product(difference(A,one),quotient(one,difference(A,one))),product(A,quotient(one,A))) = product(difference(difference(difference(A,one),one),one),A),
inference(paramod,[status(thm)],[c_12,c_16]) ).
cnf(c_12121,plain,
product(product(difference(A,one),A),product(A,quotient(one,A))) = product(difference(difference(difference(A,one),one),one),A),
inference(paramod,[status(thm)],[c_34,c_12120]) ).
cnf(c_12122,plain,
product(product(A,quotient(one,A)),product(A,quotient(one,A))) = product(difference(difference(difference(A,one),one),one),A),
inference(paramod,[status(thm)],[c_12,c_12121]) ).
cnf(c_55,plain,
product(A,product(quotient(one,A),product(A,quotient(one,A)))) = product(difference(difference(difference(A,one),one),one),A),
inference(paramod,[status(thm)],[c_20,c_12122]) ).
cnf(c_12123,plain,
product(A,product(A,quotient(one,A))) = product(quotient(one,quotient(one,A)),one),
inference(paramod,[status(thm)],[c_1,c_18]) ).
cnf(c_57,plain,
product(A,product(A,quotient(one,A))) = quotient(one,quotient(one,A)),
inference(paramod,[status(thm)],[c_1,c_12123]) ).
cnf(c_12124,plain,
difference(product(A,B),product(A,product(B,product(A,quotient(one,A))))) = product(A,quotient(one,A)),
inference(paramod,[status(thm)],[c_20,c_4]) ).
cnf(c_12125,plain,
quotient(difference(B,product(product(B,product(A,quotient(one,A))),A)),A) = product(A,quotient(one,A)),
inference(paramod,[status(thm)],[c_42,c_12124]) ).
cnf(c_12126,plain,
quotient(quotient(product(product(A,quotient(one,A)),product(A,B)),B),A) = product(A,quotient(one,A)),
inference(paramod,[status(thm)],[c_7,c_12125]) ).
cnf(c_12127,plain,
quotient(quotient(product(difference(difference(A,one),one),B),B),A) = product(A,quotient(one,A)),
inference(paramod,[status(thm)],[c_16,c_12126]) ).
cnf(c_70,plain,
quotient(difference(difference(A,one),one),A) = product(A,quotient(one,A)),
inference(paramod,[status(thm)],[c_5,c_12127]) ).
cnf(c_12128,plain,
product(product(A,quotient(one,A)),product(difference(A,one),quotient(one,difference(A,one)))) = product(difference(A,one),product(A,product(difference(A,one),quotient(one,difference(A,one))))),
inference(paramod,[status(thm)],[c_12,c_20]) ).
cnf(c_12129,plain,
product(product(A,quotient(one,A)),product(difference(A,one),A)) = product(difference(A,one),product(A,product(difference(A,one),quotient(one,difference(A,one))))),
inference(paramod,[status(thm)],[c_34,c_12128]) ).
cnf(c_12130,plain,
product(product(A,quotient(one,A)),product(A,quotient(one,A))) = product(difference(A,one),product(A,product(difference(A,one),quotient(one,difference(A,one))))),
inference(paramod,[status(thm)],[c_12,c_12129]) ).
cnf(c_12131,plain,
product(A,product(quotient(one,A),product(A,quotient(one,A)))) = product(difference(A,one),product(A,product(difference(A,one),quotient(one,difference(A,one))))),
inference(paramod,[status(thm)],[c_20,c_12130]) ).
cnf(c_12132,plain,
product(difference(difference(difference(A,one),one),one),A) = product(difference(A,one),product(A,product(difference(A,one),quotient(one,difference(A,one))))),
inference(paramod,[status(thm)],[c_55,c_12131]) ).
cnf(c_12133,plain,
product(difference(difference(difference(A,one),one),one),A) = product(difference(A,one),product(A,product(difference(A,one),A))),
inference(paramod,[status(thm)],[c_34,c_12132]) ).
cnf(c_12134,plain,
product(difference(difference(difference(A,one),one),one),A) = product(difference(A,one),product(A,product(A,quotient(one,A)))),
inference(paramod,[status(thm)],[c_12,c_12133]) ).
cnf(c_76,plain,
product(difference(difference(difference(A,one),one),one),A) = product(difference(A,one),quotient(one,quotient(one,A))),
inference(paramod,[status(thm)],[c_57,c_12134]) ).
cnf(c_12135,plain,
product(A,product(quotient(one,A),product(A,quotient(one,A)))) = product(difference(difference(A,one),one),quotient(one,A)),
inference(paramod,[status(thm)],[c_20,c_16]) ).
cnf(c_12136,plain,
product(difference(difference(difference(A,one),one),one),A) = product(difference(difference(A,one),one),quotient(one,A)),
inference(paramod,[status(thm)],[c_55,c_12135]) ).
cnf(c_12137,plain,
product(difference(A,one),quotient(one,quotient(one,A))) = product(difference(difference(A,one),one),quotient(one,A)),
inference(paramod,[status(thm)],[c_76,c_12136]) ).
cnf(c_78,plain,
product(difference(difference(A,one),one),quotient(one,A)) = product(difference(A,one),quotient(one,quotient(one,A))),
inference(copy,[status(thm)],[c_12137]) ).
cnf(c_12138,plain,
product(product(quotient(one,quotient(one,A)),B),product(A,quotient(one,A))) = product(A,product(product(product(A,quotient(one,A)),B),product(A,quotient(one,A)))),
inference(paramod,[status(thm)],[c_18,c_20]) ).
cnf(c_12139,plain,
product(product(quotient(one,quotient(one,A)),B),product(A,quotient(one,A))) = product(A,product(product(A,quotient(one,A)),product(B,product(A,quotient(one,A))))),
inference(paramod,[status(thm)],[c_22,c_12138]) ).
cnf(c_80,plain,
product(product(quotient(one,quotient(one,A)),B),product(A,quotient(one,A))) = product(quotient(one,quotient(one,A)),product(B,product(A,quotient(one,A)))),
inference(paramod,[status(thm)],[c_18,c_12139]) ).
cnf(c_82,plain,
product(A,product(quotient(one,A),product(A,quotient(one,A)))) = product(difference(A,one),quotient(one,quotient(one,A))),
inference(paramod,[status(thm)],[c_76,c_55]) ).
cnf(c_83,plain,
product(product(A,quotient(one,A)),product(B,difference(product(product(A,quotient(one,A)),B),C))) = C,
inference(paramod,[status(thm)],[c_22,c_3]) ).
cnf(c_12140,plain,
product(A,B) = product(product(C,quotient(one,C)),product(difference(product(C,quotient(one,C)),A),B)),
inference(paramod,[status(thm)],[c_3,c_22]) ).
cnf(c_84,plain,
product(product(A,quotient(one,A)),product(difference(product(A,quotient(one,A)),B),C)) = product(B,C),
inference(copy,[status(thm)],[c_12140]) ).
cnf(c_12141,plain,
difference(product(product(A,quotient(one,A)),B),product(product(A,quotient(one,A)),product(B,C))) = C,
inference(paramod,[status(thm)],[c_22,c_4]) ).
cnf(c_12142,plain,
quotient(difference(B,product(product(B,C),product(A,quotient(one,A)))),product(A,quotient(one,A))) = C,
inference(paramod,[status(thm)],[c_42,c_12141]) ).
cnf(c_85,plain,
quotient(quotient(product(A,product(product(B,quotient(one,B)),C)),C),product(B,quotient(one,B))) = A,
inference(paramod,[status(thm)],[c_7,c_12142]) ).
cnf(c_86,plain,
quotient(product(product(A,quotient(one,A)),product(B,C)),C) = product(product(A,quotient(one,A)),B),
inference(paramod,[status(thm)],[c_22,c_5]) ).
cnf(c_12143,plain,
difference(product(A,quotient(one,A)),product(product(A,quotient(one,A)),product(B,C))) = quotient(product(B,product(C,product(A,quotient(one,A)))),product(A,quotient(one,A))),
inference(paramod,[status(thm)],[c_22,c_7]) ).
cnf(c_12144,plain,
product(B,C) = quotient(product(B,product(C,product(A,quotient(one,A)))),product(A,quotient(one,A))),
inference(paramod,[status(thm)],[c_4,c_12143]) ).
cnf(c_88,plain,
quotient(product(A,product(B,product(C,quotient(one,C)))),product(C,quotient(one,C))) = product(A,B),
inference(copy,[status(thm)],[c_12144]) ).
cnf(c_98,plain,
difference(quotient(one,A),quotient(quotient(one,A),A)) = difference(A,one),
inference(paramod,[status(thm)],[c_24,c_4]) ).
cnf(c_12145,plain,
product(A,product(product(A,quotient(one,A)),difference(quotient(one,A),one))) = quotient(quotient(one,quotient(one,A)),quotient(one,A)),
inference(paramod,[status(thm)],[c_24,c_18]) ).
cnf(c_12146,plain,
product(A,product(product(A,quotient(one,A)),A)) = quotient(quotient(one,quotient(one,A)),quotient(one,A)),
inference(paramod,[status(thm)],[c_35,c_12145]) ).
cnf(c_12147,plain,
product(A,difference(difference(A,one),one)) = quotient(quotient(one,quotient(one,A)),quotient(one,A)),
inference(paramod,[status(thm)],[c_48,c_12146]) ).
cnf(c_102,plain,
quotient(quotient(one,quotient(one,A)),quotient(one,A)) = product(A,difference(difference(A,one),one)),
inference(copy,[status(thm)],[c_12147]) ).
cnf(c_12148,plain,
product(A,difference(difference(A,one),one)) = quotient(quotient(one,difference(A,one)),difference(A,one)),
inference(paramod,[status(thm)],[c_34,c_24]) ).
cnf(c_113,plain,
product(A,difference(difference(A,one),one)) = quotient(A,difference(A,one)),
inference(paramod,[status(thm)],[c_34,c_12148]) ).
cnf(c_115,plain,
quotient(quotient(one,quotient(one,A)),quotient(one,A)) = quotient(A,difference(A,one)),
inference(paramod,[status(thm)],[c_113,c_102]) ).
cnf(c_12149,plain,
product(A,quotient(one,A)) = product(quotient(one,A),quotient(one,quotient(one,A))),
inference(paramod,[status(thm)],[c_35,c_12]) ).
cnf(c_116,plain,
product(quotient(one,A),quotient(one,quotient(one,A))) = product(A,quotient(one,A)),
inference(copy,[status(thm)],[c_12149]) ).
cnf(c_12150,plain,
product(A,quotient(product(B,C),A)) = product(product(A,B),quotient(C,A)),
inference(paramod,[status(thm)],[c_6,c_36]) ).
cnf(c_124,plain,
product(product(A,B),quotient(C,A)) = product(A,quotient(product(B,C),A)),
inference(copy,[status(thm)],[c_12150]) ).
cnf(c_12151,plain,
product(product(A,B),quotient(product(product(A,quotient(one,A)),product(C,product(A,B))),product(A,B))) = product(product(A,product(B,product(A,quotient(one,A)))),C),
inference(paramod,[status(thm)],[c_20,c_36]) ).
cnf(c_12152,plain,
product(product(A,B),product(product(A,quotient(one,A)),C)) = product(product(A,product(B,product(A,quotient(one,A)))),C),
inference(paramod,[status(thm)],[c_86,c_12151]) ).
cnf(c_137,plain,
product(product(A,product(B,product(A,quotient(one,A)))),C) = product(product(A,B),product(product(A,quotient(one,A)),C)),
inference(copy,[status(thm)],[c_12152]) ).
cnf(c_138,plain,
product(A,quotient(product(B,product(product(C,quotient(one,C)),product(D,A))),A)) = product(product(A,B),product(product(C,quotient(one,C)),D)),
inference(paramod,[status(thm)],[c_22,c_36]) ).
cnf(c_12153,plain,
difference(product(A,B),A) = quotient(difference(B,product(one,A)),A),
inference(paramod,[status(thm)],[c_1,c_42]) ).
cnf(c_147,plain,
difference(product(A,B),A) = quotient(difference(B,A),A),
inference(paramod,[status(thm)],[c_2,c_12153]) ).
cnf(c_12154,plain,
difference(product(quotient(one,A),difference(A,one)),product(quotient(one,A),A)) = quotient(A,quotient(one,A)),
inference(paramod,[status(thm)],[c_45,c_42]) ).
cnf(c_12155,plain,
difference(quotient(quotient(one,A),A),product(quotient(one,A),A)) = quotient(A,quotient(one,A)),
inference(paramod,[status(thm)],[c_24,c_12154]) ).
cnf(c_169,plain,
difference(quotient(quotient(one,A),A),one) = quotient(A,quotient(one,A)),
inference(paramod,[status(thm)],[c_6,c_12155]) ).
cnf(c_12156,plain,
difference(A,B) = quotient(difference(difference(B,A),B),B),
inference(paramod,[status(thm)],[c_3,c_147]) ).
cnf(c_172,plain,
quotient(difference(difference(A,B),A),A) = difference(B,A),
inference(copy,[status(thm)],[c_12156]) ).
cnf(c_12157,plain,
difference(product(difference(difference(A,one),one),B),product(A,quotient(one,A))) = quotient(difference(product(A,B),product(A,quotient(one,A))),product(A,quotient(one,A))),
inference(paramod,[status(thm)],[c_16,c_147]) ).
cnf(c_12158,plain,
difference(product(difference(difference(A,one),one),B),product(A,quotient(one,A))) = quotient(quotient(difference(B,product(quotient(one,A),A)),A),product(A,quotient(one,A))),
inference(paramod,[status(thm)],[c_42,c_12157]) ).
cnf(c_175,plain,
difference(product(difference(difference(A,one),one),B),product(A,quotient(one,A))) = quotient(quotient(difference(B,one),A),product(A,quotient(one,A))),
inference(paramod,[status(thm)],[c_6,c_12158]) ).
cnf(c_12159,plain,
difference(product(A,product(B,product(A,quotient(one,A)))),product(A,B)) = quotient(difference(product(A,quotient(one,A)),product(A,B)),product(A,B)),
inference(paramod,[status(thm)],[c_20,c_147]) ).
cnf(c_12160,plain,
quotient(difference(product(B,product(A,quotient(one,A))),product(B,A)),A) = quotient(difference(product(A,quotient(one,A)),product(A,B)),product(A,B)),
inference(paramod,[status(thm)],[c_42,c_12159]) ).
cnf(c_12161,plain,
quotient(quotient(difference(product(A,quotient(one,A)),product(A,B)),B),A) = quotient(difference(product(A,quotient(one,A)),product(A,B)),product(A,B)),
inference(paramod,[status(thm)],[c_42,c_12160]) ).
cnf(c_12162,plain,
quotient(quotient(quotient(difference(quotient(one,A),product(B,A)),A),B),A) = quotient(difference(product(A,quotient(one,A)),product(A,B)),product(A,B)),
inference(paramod,[status(thm)],[c_42,c_12161]) ).
cnf(c_177,plain,
quotient(quotient(quotient(difference(quotient(one,A),product(B,A)),A),B),A) = quotient(quotient(difference(quotient(one,A),product(B,A)),A),product(A,B)),
inference(paramod,[status(thm)],[c_42,c_12162]) ).
cnf(c_12163,plain,
product(difference(A,B),B) = difference(difference(B,A),B),
inference(paramod,[status(thm)],[c_172,c_6]) ).
cnf(c_183,plain,
difference(difference(A,B),A) = product(difference(B,A),A),
inference(copy,[status(thm)],[c_12163]) ).
cnf(c_186,plain,
product(difference(A,B),product(difference(B,A),A)) = A,
inference(paramod,[status(thm)],[c_183,c_3]) ).
cnf(c_189,plain,
quotient(A,product(difference(B,A),A)) = difference(A,B),
inference(paramod,[status(thm)],[c_183,c_34]) ).
cnf(c_12164,plain,
difference(A,quotient(B,A)) = product(difference(B,quotient(B,A)),quotient(B,A)),
inference(paramod,[status(thm)],[c_35,c_183]) ).
cnf(c_190,plain,
product(difference(A,quotient(A,B)),quotient(A,B)) = difference(B,quotient(A,B)),
inference(copy,[status(thm)],[c_12164]) ).
cnf(c_12165,plain,
quotient(A,product(B,A)) = difference(A,quotient(A,B)),
inference(paramod,[status(thm)],[c_35,c_189]) ).
cnf(c_198,plain,
difference(A,quotient(A,B)) = quotient(A,product(B,A)),
inference(copy,[status(thm)],[c_12165]) ).
cnf(c_203,plain,
product(quotient(A,product(B,A)),quotient(A,B)) = difference(B,quotient(A,B)),
inference(paramod,[status(thm)],[c_198,c_190]) ).
cnf(c_205,plain,
quotient(quotient(one,A),product(A,quotient(one,A))) = difference(A,one),
inference(paramod,[status(thm)],[c_198,c_98]) ).
cnf(c_12166,plain,
quotient(product(difference(A,B),C),A) = difference(A,product(B,quotient(C,A))),
inference(paramod,[status(thm)],[c_6,c_37]) ).
cnf(c_208,plain,
difference(A,product(B,quotient(C,A))) = quotient(product(difference(A,B),C),A),
inference(copy,[status(thm)],[c_12166]) ).
cnf(c_229,plain,
product(A,quotient(A,product(B,A))) = quotient(A,B),
inference(paramod,[status(thm)],[c_198,c_3]) ).
cnf(c_12167,plain,
product(A,quotient(A,B)) = quotient(A,quotient(B,A)),
inference(paramod,[status(thm)],[c_6,c_229]) ).
cnf(c_246,plain,
quotient(A,quotient(B,A)) = product(A,quotient(A,B)),
inference(copy,[status(thm)],[c_12167]) ).
cnf(c_12168,plain,
difference(quotient(quotient(one,A),A),one) = product(A,quotient(A,one)),
inference(paramod,[status(thm)],[c_246,c_169]) ).
cnf(c_268,plain,
difference(quotient(quotient(one,A),A),one) = product(A,A),
inference(paramod,[status(thm)],[c_32,c_12168]) ).
cnf(c_12169,plain,
quotient(one,product(A,A)) = quotient(quotient(one,A),A),
inference(paramod,[status(thm)],[c_268,c_34]) ).
cnf(c_301,plain,
quotient(quotient(one,A),A) = quotient(one,product(A,A)),
inference(copy,[status(thm)],[c_12169]) ).
cnf(c_302,plain,
difference(quotient(A,difference(A,one)),one) = product(difference(A,one),difference(A,one)),
inference(paramod,[status(thm)],[c_34,c_268]) ).
cnf(c_314,plain,
quotient(one,product(quotient(one,A),quotient(one,A))) = quotient(A,difference(A,one)),
inference(paramod,[status(thm)],[c_301,c_115]) ).
cnf(c_317,plain,
product(quotient(one,A),difference(A,one)) = quotient(one,product(A,A)),
inference(paramod,[status(thm)],[c_301,c_24]) ).
cnf(c_320,plain,
difference(quotient(one,product(A,A)),quotient(one,A)) = A,
inference(paramod,[status(thm)],[c_301,c_35]) ).
cnf(c_12170,plain,
difference(quotient(one,A),quotient(one,product(A,A))) = quotient(quotient(one,A),product(A,quotient(one,A))),
inference(paramod,[status(thm)],[c_301,c_198]) ).
cnf(c_321,plain,
difference(quotient(one,A),quotient(one,product(A,A))) = difference(A,one),
inference(paramod,[status(thm)],[c_205,c_12170]) ).
cnf(c_12171,plain,
difference(difference(quotient(one,A),quotient(one,product(A,A))),quotient(one,A)) = product(A,quotient(one,A)),
inference(paramod,[status(thm)],[c_320,c_183]) ).
cnf(c_338,plain,
difference(difference(A,one),quotient(one,A)) = product(A,quotient(one,A)),
inference(paramod,[status(thm)],[c_321,c_12171]) ).
cnf(c_12172,plain,
product(difference(quotient(one,A),quotient(one,product(A,A))),product(A,quotient(one,A))) = quotient(one,A),
inference(paramod,[status(thm)],[c_320,c_186]) ).
cnf(c_339,plain,
product(difference(A,one),product(A,quotient(one,A))) = quotient(one,A),
inference(paramod,[status(thm)],[c_321,c_12172]) ).
cnf(c_12173,plain,
quotient(quotient(one,A),product(product(A,quotient(one,A)),quotient(one,A))) = difference(quotient(one,A),difference(A,one)),
inference(paramod,[status(thm)],[c_338,c_189]) ).
cnf(c_12174,plain,
quotient(quotient(one,A),product(A,quotient(product(quotient(one,A),one),A))) = difference(quotient(one,A),difference(A,one)),
inference(paramod,[status(thm)],[c_124,c_12173]) ).
cnf(c_12175,plain,
quotient(quotient(one,A),product(A,quotient(quotient(one,A),A))) = difference(quotient(one,A),difference(A,one)),
inference(paramod,[status(thm)],[c_1,c_12174]) ).
cnf(c_358,plain,
quotient(quotient(one,A),product(A,quotient(one,product(A,A)))) = difference(quotient(one,A),difference(A,one)),
inference(paramod,[status(thm)],[c_301,c_12175]) ).
cnf(c_12176,plain,
quotient(difference(A,one),quotient(one,A)) = product(quotient(one,A),quotient(one,quotient(one,A))),
inference(paramod,[status(thm)],[c_35,c_70]) ).
cnf(c_366,plain,
quotient(difference(A,one),quotient(one,A)) = product(A,quotient(one,A)),
inference(paramod,[status(thm)],[c_116,c_12176]) ).
cnf(c_12177,plain,
product(product(A,quotient(one,A)),quotient(one,A)) = difference(A,one),
inference(paramod,[status(thm)],[c_366,c_6]) ).
cnf(c_12178,plain,
product(A,quotient(product(quotient(one,A),one),A)) = difference(A,one),
inference(paramod,[status(thm)],[c_124,c_12177]) ).
cnf(c_12179,plain,
product(A,quotient(quotient(one,A),A)) = difference(A,one),
inference(paramod,[status(thm)],[c_1,c_12178]) ).
cnf(c_370,plain,
product(A,quotient(one,product(A,A))) = difference(A,one),
inference(paramod,[status(thm)],[c_301,c_12179]) ).
cnf(c_12180,plain,
quotient(quotient(one,A),difference(A,one)) = difference(quotient(one,A),difference(A,one)),
inference(paramod,[status(thm)],[c_370,c_358]) ).
cnf(c_376,plain,
difference(quotient(one,A),difference(A,one)) = quotient(quotient(one,A),difference(A,one)),
inference(copy,[status(thm)],[c_12180]) ).
cnf(c_12181,plain,
product(product(A,quotient(one,A)),quotient(one,product(difference(difference(A,one),one),quotient(one,A)))) = difference(product(A,quotient(one,A)),one),
inference(paramod,[status(thm)],[c_16,c_370]) ).
cnf(c_387,plain,
product(product(A,quotient(one,A)),quotient(one,product(difference(A,one),quotient(one,quotient(one,A))))) = difference(product(A,quotient(one,A)),one),
inference(paramod,[status(thm)],[c_78,c_12181]) ).
cnf(c_12182,plain,
product(quotient(one,A),quotient(one,product(quotient(one,A),quotient(one,A)))) = A,
inference(paramod,[status(thm)],[c_35,c_370]) ).
cnf(c_392,plain,
product(quotient(one,A),quotient(A,difference(A,one))) = A,
inference(paramod,[status(thm)],[c_314,c_12182]) ).
cnf(c_12183,plain,
product(quotient(one,quotient(one,A)),quotient(quotient(one,A),A)) = quotient(one,A),
inference(paramod,[status(thm)],[c_35,c_392]) ).
cnf(c_445,plain,
product(quotient(one,quotient(one,A)),quotient(one,product(A,A))) = quotient(one,A),
inference(paramod,[status(thm)],[c_301,c_12183]) ).
cnf(c_12184,plain,
difference(A,difference(difference(A,one),one)) = quotient(quotient(one,difference(A,one)),difference(difference(A,one),one)),
inference(paramod,[status(thm)],[c_34,c_376]) ).
cnf(c_455,plain,
difference(A,difference(difference(A,one),one)) = quotient(A,difference(difference(A,one),one)),
inference(paramod,[status(thm)],[c_34,c_12184]) ).
cnf(c_12185,plain,
quotient(quotient(product(A,one),B),quotient(one,B)) = product(quotient(one,B),product(B,A)),
inference(paramod,[status(thm)],[c_43,c_30]) ).
cnf(c_479,plain,
quotient(quotient(A,B),quotient(one,B)) = product(quotient(one,B),product(B,A)),
inference(paramod,[status(thm)],[c_1,c_12185]) ).
cnf(c_515,plain,
product(quotient(one,A),quotient(one,A)) = difference(A,quotient(one,A)),
inference(paramod,[status(thm)],[c_1,c_203]) ).
cnf(c_545,plain,
quotient(one,difference(A,quotient(one,A))) = quotient(A,difference(A,one)),
inference(paramod,[status(thm)],[c_515,c_314]) ).
cnf(c_12186,plain,
product(product(quotient(one,A),quotient(one,quotient(one,A))),difference(A,quotient(one,A))) = product(difference(difference(quotient(one,A),one),one),quotient(one,A)),
inference(paramod,[status(thm)],[c_515,c_16]) ).
cnf(c_12187,plain,
product(product(A,quotient(one,A)),difference(A,quotient(one,A))) = product(difference(difference(quotient(one,A),one),one),quotient(one,A)),
inference(paramod,[status(thm)],[c_116,c_12186]) ).
cnf(c_553,plain,
product(product(A,quotient(one,A)),difference(A,quotient(one,A))) = product(difference(A,one),quotient(one,A)),
inference(paramod,[status(thm)],[c_35,c_12187]) ).
cnf(c_12188,plain,
difference(quotient(A,difference(A,one)),one) = difference(A,quotient(one,A)),
inference(paramod,[status(thm)],[c_545,c_35]) ).
cnf(c_566,plain,
product(difference(A,one),difference(A,one)) = difference(A,quotient(one,A)),
inference(paramod,[status(thm)],[c_302,c_12188]) ).
cnf(c_585,plain,
quotient(difference(A,quotient(one,A)),difference(A,one)) = difference(A,one),
inference(paramod,[status(thm)],[c_566,c_5]) ).
cnf(c_12189,plain,
product(difference(A,quotient(one,A)),product(difference(A,one),quotient(one,difference(A,one)))) = product(difference(A,one),product(difference(A,one),product(difference(A,one),quotient(one,difference(A,one))))),
inference(paramod,[status(thm)],[c_566,c_20]) ).
cnf(c_12190,plain,
product(difference(A,quotient(one,A)),product(difference(A,one),A)) = product(difference(A,one),product(difference(A,one),product(difference(A,one),quotient(one,difference(A,one))))),
inference(paramod,[status(thm)],[c_34,c_12189]) ).
cnf(c_12191,plain,
product(difference(A,quotient(one,A)),product(A,quotient(one,A))) = product(difference(A,one),product(difference(A,one),product(difference(A,one),quotient(one,difference(A,one))))),
inference(paramod,[status(thm)],[c_12,c_12190]) ).
cnf(c_12192,plain,
product(difference(A,quotient(one,A)),product(A,quotient(one,A))) = product(difference(A,one),product(difference(A,one),product(difference(A,one),A))),
inference(paramod,[status(thm)],[c_34,c_12191]) ).
cnf(c_12193,plain,
product(difference(A,quotient(one,A)),product(A,quotient(one,A))) = product(difference(A,one),product(difference(A,one),product(A,quotient(one,A)))),
inference(paramod,[status(thm)],[c_12,c_12192]) ).
cnf(c_588,plain,
product(difference(A,quotient(one,A)),product(A,quotient(one,A))) = product(difference(A,one),quotient(one,A)),
inference(paramod,[status(thm)],[c_339,c_12193]) ).
cnf(c_12194,plain,
difference(difference(A,quotient(one,A)),difference(A,one)) = quotient(difference(difference(A,one),difference(A,one)),difference(A,one)),
inference(paramod,[status(thm)],[c_566,c_147]) ).
cnf(c_12195,plain,
difference(difference(A,quotient(one,A)),difference(A,one)) = quotient(one,difference(A,one)),
inference(paramod,[status(thm)],[c_31,c_12194]) ).
cnf(c_593,plain,
difference(difference(A,quotient(one,A)),difference(A,one)) = A,
inference(paramod,[status(thm)],[c_34,c_12195]) ).
cnf(c_12196,plain,
difference(difference(A,quotient(one,A)),difference(A,one)) = quotient(difference(A,quotient(one,A)),product(difference(A,one),difference(A,quotient(one,A)))),
inference(paramod,[status(thm)],[c_585,c_198]) ).
cnf(c_12197,plain,
A = quotient(difference(A,quotient(one,A)),product(difference(A,one),difference(A,quotient(one,A)))),
inference(paramod,[status(thm)],[c_593,c_12196]) ).
cnf(c_635,plain,
quotient(difference(A,quotient(one,A)),product(difference(A,one),difference(A,quotient(one,A)))) = A,
inference(copy,[status(thm)],[c_12197]) ).
cnf(c_12198,plain,
product(difference(A,quotient(one,A)),quotient(difference(A,quotient(one,A)),product(difference(A,one),difference(A,quotient(one,A))))) = difference(A,one),
inference(paramod,[status(thm)],[c_585,c_229]) ).
cnf(c_636,plain,
product(difference(A,quotient(one,A)),A) = difference(A,one),
inference(paramod,[status(thm)],[c_635,c_12198]) ).
cnf(c_12199,plain,
quotient(difference(A,one),A) = difference(A,quotient(one,A)),
inference(paramod,[status(thm)],[c_636,c_5]) ).
cnf(c_639,plain,
difference(A,quotient(one,A)) = quotient(difference(A,one),A),
inference(copy,[status(thm)],[c_12199]) ).
cnf(c_12200,plain,
product(difference(difference(A,one),A),difference(A,one)) = difference(difference(A,one),one),
inference(paramod,[status(thm)],[c_34,c_636]) ).
cnf(c_12201,plain,
product(product(difference(one,A),A),difference(A,one)) = difference(difference(A,one),one),
inference(paramod,[status(thm)],[c_183,c_12200]) ).
cnf(c_640,plain,
product(product(A,A),difference(A,one)) = difference(difference(A,one),one),
inference(paramod,[status(thm)],[c_30,c_12201]) ).
cnf(c_674,plain,
product(quotient(difference(A,one),A),product(A,quotient(one,A))) = product(difference(A,one),quotient(one,A)),
inference(paramod,[status(thm)],[c_639,c_588]) ).
cnf(c_12202,plain,
product(product(A,quotient(one,A)),quotient(difference(A,one),A)) = product(difference(A,one),quotient(one,A)),
inference(paramod,[status(thm)],[c_639,c_553]) ).
cnf(c_12203,plain,
product(A,quotient(product(quotient(one,A),difference(A,one)),A)) = product(difference(A,one),quotient(one,A)),
inference(paramod,[status(thm)],[c_124,c_12202]) ).
cnf(c_703,plain,
product(A,quotient(quotient(one,product(A,A)),A)) = product(difference(A,one),quotient(one,A)),
inference(paramod,[status(thm)],[c_317,c_12203]) ).
cnf(c_711,plain,
product(quotient(one,A),quotient(one,A)) = quotient(difference(A,one),A),
inference(paramod,[status(thm)],[c_639,c_515]) ).
cnf(c_720,plain,
product(A,quotient(difference(A,one),A)) = quotient(one,A),
inference(paramod,[status(thm)],[c_639,c_3]) ).
cnf(c_12204,plain,
difference(difference(product(A,quotient(one,A)),one),product(product(A,quotient(one,A)),product(quotient(one,product(A,quotient(one,A))),B))) = quotient(product(product(A,quotient(one,A)),product(B,difference(product(A,quotient(one,A)),one))),difference(product(A,quotient(one,A)),one)),
inference(paramod,[status(thm)],[c_22,c_47]) ).
cnf(c_733,plain,
difference(difference(product(A,quotient(one,A)),one),product(product(A,quotient(one,A)),product(quotient(one,product(A,quotient(one,A))),B))) = product(product(A,quotient(one,A)),B),
inference(paramod,[status(thm)],[c_86,c_12204]) ).
cnf(c_12205,plain,
product(A,product(product(A,quotient(one,A)),quotient(difference(quotient(one,quotient(one,A)),one),quotient(one,quotient(one,A))))) = quotient(one,quotient(one,quotient(one,A))),
inference(paramod,[status(thm)],[c_720,c_18]) ).
cnf(c_12206,plain,
product(A,product(product(A,quotient(one,A)),quotient(quotient(one,A),quotient(one,quotient(one,A))))) = quotient(one,quotient(one,quotient(one,A))),
inference(paramod,[status(thm)],[c_35,c_12205]) ).
cnf(c_12207,plain,
product(A,product(product(A,quotient(one,A)),product(quotient(one,A),quotient(quotient(one,A),one)))) = quotient(one,quotient(one,quotient(one,A))),
inference(paramod,[status(thm)],[c_246,c_12206]) ).
cnf(c_12208,plain,
product(A,product(product(A,quotient(one,A)),product(quotient(one,A),quotient(one,A)))) = quotient(one,quotient(one,quotient(one,A))),
inference(paramod,[status(thm)],[c_32,c_12207]) ).
cnf(c_12209,plain,
product(A,product(product(A,quotient(one,A)),quotient(difference(A,one),A))) = quotient(one,quotient(one,quotient(one,A))),
inference(paramod,[status(thm)],[c_711,c_12208]) ).
cnf(c_12210,plain,
product(A,product(A,quotient(product(quotient(one,A),difference(A,one)),A))) = quotient(one,quotient(one,quotient(one,A))),
inference(paramod,[status(thm)],[c_124,c_12209]) ).
cnf(c_12211,plain,
product(A,product(A,quotient(quotient(one,product(A,A)),A))) = quotient(one,quotient(one,quotient(one,A))),
inference(paramod,[status(thm)],[c_317,c_12210]) ).
cnf(c_748,plain,
product(A,product(difference(A,one),quotient(one,A))) = quotient(one,quotient(one,quotient(one,A))),
inference(paramod,[status(thm)],[c_703,c_12211]) ).
cnf(c_12212,plain,
product(quotient(one,A),product(A,quotient(one,A))) = product(A,product(quotient(difference(A,one),A),product(A,quotient(one,A)))),
inference(paramod,[status(thm)],[c_720,c_20]) ).
cnf(c_12213,plain,
product(quotient(one,A),product(A,quotient(one,A))) = product(A,product(difference(A,one),quotient(one,A))),
inference(paramod,[status(thm)],[c_674,c_12212]) ).
cnf(c_749,plain,
product(quotient(one,A),product(A,quotient(one,A))) = quotient(one,quotient(one,quotient(one,A))),
inference(paramod,[status(thm)],[c_748,c_12213]) ).
cnf(c_12214,plain,
product(A,quotient(one,quotient(one,quotient(one,A)))) = product(difference(A,one),quotient(one,quotient(one,A))),
inference(paramod,[status(thm)],[c_749,c_82]) ).
cnf(c_765,plain,
product(difference(A,one),quotient(one,quotient(one,A))) = product(A,quotient(one,quotient(one,quotient(one,A)))),
inference(copy,[status(thm)],[c_12214]) ).
cnf(c_770,plain,
product(product(A,quotient(one,A)),quotient(one,product(A,quotient(one,quotient(one,quotient(one,A)))))) = difference(product(A,quotient(one,A)),one),
inference(paramod,[status(thm)],[c_765,c_387]) ).
cnf(c_780,plain,
product(difference(difference(A,one),one),quotient(one,A)) = product(A,quotient(one,quotient(one,quotient(one,A)))),
inference(paramod,[status(thm)],[c_765,c_78]) ).
cnf(c_12215,plain,
difference(A,difference(difference(A,one),one)) = quotient(product(A,product(difference(A,one),A)),A),
inference(paramod,[status(thm)],[c_640,c_7]) ).
cnf(c_12216,plain,
quotient(A,difference(difference(A,one),one)) = quotient(product(A,product(difference(A,one),A)),A),
inference(paramod,[status(thm)],[c_455,c_12215]) ).
cnf(c_12217,plain,
quotient(A,difference(difference(A,one),one)) = quotient(product(A,product(A,quotient(one,A))),A),
inference(paramod,[status(thm)],[c_12,c_12216]) ).
cnf(c_12218,plain,
quotient(A,difference(difference(A,one),one)) = quotient(quotient(one,quotient(one,A)),A),
inference(paramod,[status(thm)],[c_57,c_12217]) ).
cnf(c_784,plain,
quotient(quotient(one,quotient(one,A)),A) = quotient(A,difference(difference(A,one),one)),
inference(copy,[status(thm)],[c_12218]) ).
cnf(c_12219,plain,
difference(difference(product(A,quotient(one,A)),one),one) = product(product(A,quotient(one,A)),product(product(A,quotient(one,A)),difference(product(A,quotient(one,A)),one))),
inference(paramod,[status(thm)],[c_640,c_22]) ).
cnf(c_12220,plain,
difference(difference(product(A,quotient(one,A)),one),one) = product(product(A,quotient(one,A)),one),
inference(paramod,[status(thm)],[c_3,c_12219]) ).
cnf(c_787,plain,
difference(difference(product(A,quotient(one,A)),one),one) = product(A,quotient(one,A)),
inference(paramod,[status(thm)],[c_1,c_12220]) ).
cnf(c_12221,plain,
difference(A,quotient(B,A)) = quotient(product(difference(A,one),B),A),
inference(paramod,[status(thm)],[c_2,c_208]) ).
cnf(c_861,plain,
quotient(product(difference(A,one),B),A) = difference(A,quotient(B,A)),
inference(copy,[status(thm)],[c_12221]) ).
cnf(c_903,plain,
product(difference(A,quotient(B,A)),A) = product(difference(A,one),B),
inference(paramod,[status(thm)],[c_861,c_6]) ).
cnf(c_12222,plain,
product(difference(A,B),A) = product(difference(A,one),product(B,A)),
inference(paramod,[status(thm)],[c_5,c_903]) ).
cnf(c_922,plain,
product(difference(A,one),product(B,A)) = product(difference(A,B),A),
inference(copy,[status(thm)],[c_12222]) ).
cnf(c_949,plain,
difference(difference(A,one),product(difference(A,B),A)) = product(B,A),
inference(paramod,[status(thm)],[c_922,c_4]) ).
cnf(c_950,plain,
quotient(product(difference(A,B),A),product(B,A)) = difference(A,one),
inference(paramod,[status(thm)],[c_922,c_5]) ).
cnf(c_12223,plain,
product(difference(difference(product(A,quotient(one,A)),one),one),difference(product(A,quotient(one,A)),B)) = product(product(A,quotient(one,A)),product(quotient(one,product(A,quotient(one,A))),B)),
inference(paramod,[status(thm)],[c_22,c_49]) ).
cnf(c_12224,plain,
product(product(A,quotient(one,A)),difference(product(A,quotient(one,A)),B)) = product(product(A,quotient(one,A)),product(quotient(one,product(A,quotient(one,A))),B)),
inference(paramod,[status(thm)],[c_787,c_12223]) ).
cnf(c_12225,plain,
B = product(product(A,quotient(one,A)),product(quotient(one,product(A,quotient(one,A))),B)),
inference(paramod,[status(thm)],[c_3,c_12224]) ).
cnf(c_982,plain,
product(product(A,quotient(one,A)),product(quotient(one,product(A,quotient(one,A))),B)) = B,
inference(copy,[status(thm)],[c_12225]) ).
cnf(c_1005,plain,
difference(difference(product(A,quotient(one,A)),one),B) = product(product(A,quotient(one,A)),B),
inference(paramod,[status(thm)],[c_982,c_733]) ).
cnf(c_1008,plain,
quotient(product(A,B),product(product(B,A),B)) = difference(B,one),
inference(paramod,[status(thm)],[c_4,c_950]) ).
cnf(c_12226,plain,
quotient(product(difference(product(A,quotient(one,A)),product(A,B)),product(A,quotient(one,A))),product(A,product(B,product(A,quotient(one,A))))) = difference(product(A,quotient(one,A)),one),
inference(paramod,[status(thm)],[c_20,c_950]) ).
cnf(c_1012,plain,
quotient(product(quotient(difference(quotient(one,A),product(B,A)),A),product(A,quotient(one,A))),product(A,product(B,product(A,quotient(one,A))))) = difference(product(A,quotient(one,A)),one),
inference(paramod,[status(thm)],[c_42,c_12226]) ).
cnf(c_12227,plain,
difference(product(A,quotient(one,A)),product(quotient(one,quotient(one,difference(difference(A,one),one))),B)) = product(A,product(product(difference(difference(A,one),one),quotient(one,difference(difference(A,one),one))),B)),
inference(paramod,[status(thm)],[c_18,c_50]) ).
cnf(c_12228,plain,
difference(product(A,quotient(one,A)),product(quotient(one,difference(A,one)),B)) = product(A,product(product(difference(difference(A,one),one),quotient(one,difference(difference(A,one),one))),B)),
inference(paramod,[status(thm)],[c_34,c_12227]) ).
cnf(c_12229,plain,
difference(product(A,quotient(one,A)),product(A,B)) = product(A,product(product(difference(difference(A,one),one),quotient(one,difference(difference(A,one),one))),B)),
inference(paramod,[status(thm)],[c_34,c_12228]) ).
cnf(c_12230,plain,
quotient(difference(quotient(one,A),product(B,A)),A) = product(A,product(product(difference(difference(A,one),one),quotient(one,difference(difference(A,one),one))),B)),
inference(paramod,[status(thm)],[c_42,c_12229]) ).
cnf(c_12231,plain,
quotient(difference(quotient(one,A),product(B,A)),A) = product(A,product(product(difference(difference(A,one),one),difference(A,one)),B)),
inference(paramod,[status(thm)],[c_34,c_12230]) ).
cnf(c_12232,plain,
quotient(difference(quotient(one,A),product(B,A)),A) = product(A,product(product(difference(A,one),quotient(one,difference(A,one))),B)),
inference(paramod,[status(thm)],[c_12,c_12231]) ).
cnf(c_12233,plain,
quotient(difference(quotient(one,A),product(B,A)),A) = product(A,product(product(difference(A,one),A),B)),
inference(paramod,[status(thm)],[c_34,c_12232]) ).
cnf(c_12234,plain,
quotient(difference(quotient(one,A),product(B,A)),A) = product(A,product(product(A,quotient(one,A)),B)),
inference(paramod,[status(thm)],[c_12,c_12233]) ).
cnf(c_1109,plain,
quotient(difference(quotient(one,A),product(B,A)),A) = product(quotient(one,quotient(one,A)),B),
inference(paramod,[status(thm)],[c_18,c_12234]) ).
cnf(c_12235,plain,
quotient(product(difference(difference(A,one),one),B),product(product(A,B),product(difference(difference(A,one),one),B))) = difference(product(difference(difference(A,one),one),B),product(A,quotient(one,A))),
inference(paramod,[status(thm)],[c_50,c_189]) ).
cnf(c_1114,plain,
quotient(product(difference(difference(A,one),one),B),product(product(A,B),product(difference(difference(A,one),one),B))) = quotient(quotient(difference(B,one),A),product(A,quotient(one,A))),
inference(paramod,[status(thm)],[c_175,c_12235]) ).
cnf(c_12236,plain,
quotient(product(product(quotient(one,quotient(one,A)),B),product(A,quotient(one,A))),product(A,product(B,product(A,quotient(one,A))))) = difference(product(A,quotient(one,A)),one),
inference(paramod,[status(thm)],[c_1109,c_1012]) ).
cnf(c_1127,plain,
quotient(product(quotient(one,quotient(one,A)),product(B,product(A,quotient(one,A)))),product(A,product(B,product(A,quotient(one,A))))) = difference(product(A,quotient(one,A)),one),
inference(paramod,[status(thm)],[c_80,c_12236]) ).
cnf(c_12237,plain,
quotient(quotient(product(quotient(one,quotient(one,A)),B),B),A) = quotient(quotient(difference(quotient(one,A),product(B,A)),A),product(A,B)),
inference(paramod,[status(thm)],[c_1109,c_177]) ).
cnf(c_12238,plain,
quotient(quotient(one,quotient(one,A)),A) = quotient(quotient(difference(quotient(one,A),product(B,A)),A),product(A,B)),
inference(paramod,[status(thm)],[c_5,c_12237]) ).
cnf(c_12239,plain,
quotient(A,difference(difference(A,one),one)) = quotient(quotient(difference(quotient(one,A),product(B,A)),A),product(A,B)),
inference(paramod,[status(thm)],[c_784,c_12238]) ).
cnf(c_12240,plain,
quotient(A,difference(difference(A,one),one)) = quotient(product(quotient(one,quotient(one,A)),B),product(A,B)),
inference(paramod,[status(thm)],[c_1109,c_12239]) ).
cnf(c_1129,plain,
quotient(product(quotient(one,quotient(one,A)),B),product(A,B)) = quotient(A,difference(difference(A,one),one)),
inference(copy,[status(thm)],[c_12240]) ).
cnf(c_12241,plain,
quotient(A,difference(difference(A,one),one)) = difference(product(A,quotient(one,A)),one),
inference(paramod,[status(thm)],[c_1129,c_1127]) ).
cnf(c_1135,plain,
difference(product(A,quotient(one,A)),one) = quotient(A,difference(difference(A,one),one)),
inference(copy,[status(thm)],[c_12241]) ).
cnf(c_1138,plain,
difference(quotient(A,difference(difference(A,one),one)),B) = product(product(A,quotient(one,A)),B),
inference(paramod,[status(thm)],[c_1135,c_1005]) ).
cnf(c_1146,plain,
product(product(A,quotient(one,A)),quotient(one,product(A,quotient(one,quotient(one,quotient(one,A)))))) = quotient(A,difference(difference(A,one),one)),
inference(paramod,[status(thm)],[c_1135,c_770]) ).
cnf(c_12242,plain,
difference(product(A,quotient(one,A)),product(product(product(A,quotient(one,A)),B),difference(A,one))) = quotient(product(B,quotient(one,A)),product(A,quotient(one,A))),
inference(paramod,[status(thm)],[c_339,c_7]) ).
cnf(c_12243,plain,
difference(product(A,quotient(one,A)),product(product(A,quotient(one,A)),product(B,difference(A,one)))) = quotient(product(B,quotient(one,A)),product(A,quotient(one,A))),
inference(paramod,[status(thm)],[c_22,c_12242]) ).
cnf(c_12244,plain,
product(B,difference(A,one)) = quotient(product(B,quotient(one,A)),product(A,quotient(one,A))),
inference(paramod,[status(thm)],[c_4,c_12243]) ).
cnf(c_1172,plain,
quotient(product(A,quotient(one,B)),product(B,quotient(one,B))) = product(A,difference(B,one)),
inference(copy,[status(thm)],[c_12244]) ).
cnf(c_12245,plain,
quotient(product(difference(difference(product(A,quotient(one,A)),one),one),product(A,B)),product(difference(difference(A,one),one),B)) = product(product(A,quotient(one,A)),quotient(one,product(A,quotient(one,A)))),
inference(paramod,[status(thm)],[c_16,c_51]) ).
cnf(c_12246,plain,
quotient(product(difference(quotient(A,difference(difference(A,one),one)),one),product(A,B)),product(difference(difference(A,one),one),B)) = product(product(A,quotient(one,A)),quotient(one,product(A,quotient(one,A)))),
inference(paramod,[status(thm)],[c_1135,c_12245]) ).
cnf(c_12247,plain,
quotient(product(product(product(A,quotient(one,A)),one),product(A,B)),product(difference(difference(A,one),one),B)) = product(product(A,quotient(one,A)),quotient(one,product(A,quotient(one,A)))),
inference(paramod,[status(thm)],[c_1138,c_12246]) ).
cnf(c_12248,plain,
quotient(product(product(A,quotient(one,A)),product(A,B)),product(difference(difference(A,one),one),B)) = product(product(A,quotient(one,A)),quotient(one,product(A,quotient(one,A)))),
inference(paramod,[status(thm)],[c_1,c_12247]) ).
cnf(c_12249,plain,
quotient(product(difference(difference(A,one),one),B),product(difference(difference(A,one),one),B)) = product(product(A,quotient(one,A)),quotient(one,product(A,quotient(one,A)))),
inference(paramod,[status(thm)],[c_16,c_12248]) ).
cnf(c_12250,plain,
one = product(product(A,quotient(one,A)),quotient(one,product(A,quotient(one,A)))),
inference(paramod,[status(thm)],[c_33,c_12249]) ).
cnf(c_1202,plain,
product(product(A,quotient(one,A)),quotient(one,product(A,quotient(one,A)))) = one,
inference(copy,[status(thm)],[c_12250]) ).
cnf(c_1303,plain,
difference(difference(A,one),product(B,A)) = product(product(A,B),A),
inference(paramod,[status(thm)],[c_4,c_949]) ).
cnf(c_12251,plain,
difference(difference(A,one),B) = product(product(A,quotient(B,A)),A),
inference(paramod,[status(thm)],[c_6,c_1303]) ).
cnf(c_1321,plain,
product(product(A,quotient(B,A)),A) = difference(difference(A,one),B),
inference(copy,[status(thm)],[c_12251]) ).
cnf(c_12252,plain,
difference(A,product(B,quotient(one,A))) = product(product(quotient(one,A),B),quotient(one,A)),
inference(paramod,[status(thm)],[c_35,c_1303]) ).
cnf(c_12253,plain,
quotient(product(difference(A,B),one),A) = product(product(quotient(one,A),B),quotient(one,A)),
inference(paramod,[status(thm)],[c_208,c_12252]) ).
cnf(c_12254,plain,
quotient(difference(A,B),A) = product(product(quotient(one,A),B),quotient(one,A)),
inference(paramod,[status(thm)],[c_1,c_12253]) ).
cnf(c_1326,plain,
product(product(quotient(one,A),B),quotient(one,A)) = quotient(difference(A,B),A),
inference(copy,[status(thm)],[c_12254]) ).
cnf(c_12255,plain,
quotient(product(difference(difference(A,one),one),B),product(product(product(A,B),product(A,quotient(one,A))),product(A,B))) = difference(product(A,B),one),
inference(paramod,[status(thm)],[c_16,c_1008]) ).
cnf(c_12256,plain,
quotient(product(difference(difference(A,one),one),B),product(product(A,product(B,product(A,quotient(one,A)))),product(A,B))) = difference(product(A,B),one),
inference(paramod,[status(thm)],[c_20,c_12255]) ).
cnf(c_12257,plain,
quotient(product(difference(difference(A,one),one),B),product(product(A,B),product(product(A,quotient(one,A)),product(A,B)))) = difference(product(A,B),one),
inference(paramod,[status(thm)],[c_137,c_12256]) ).
cnf(c_12258,plain,
quotient(product(difference(difference(A,one),one),B),product(product(A,B),product(difference(difference(A,one),one),B))) = difference(product(A,B),one),
inference(paramod,[status(thm)],[c_16,c_12257]) ).
cnf(c_1394,plain,
quotient(quotient(difference(A,one),B),product(B,quotient(one,B))) = difference(product(B,A),one),
inference(paramod,[status(thm)],[c_1114,c_12258]) ).
cnf(c_12259,plain,
quotient(product(A,quotient(one,B)),product(product(quotient(one,B),A),quotient(one,B))) = B,
inference(paramod,[status(thm)],[c_35,c_1008]) ).
cnf(c_1400,plain,
quotient(product(A,quotient(one,B)),quotient(difference(B,A),B)) = B,
inference(paramod,[status(thm)],[c_1326,c_12259]) ).
cnf(c_1459,plain,
product(A,quotient(difference(A,B),A)) = product(B,quotient(one,A)),
inference(paramod,[status(thm)],[c_1400,c_6]) ).
cnf(c_12260,plain,
difference(difference(A,one),product(quotient(difference(A,B),A),A)) = product(product(B,quotient(one,A)),A),
inference(paramod,[status(thm)],[c_1459,c_1303]) ).
cnf(c_1528,plain,
difference(difference(A,one),difference(A,B)) = product(product(B,quotient(one,A)),A),
inference(paramod,[status(thm)],[c_6,c_12260]) ).
cnf(c_12261,plain,
product(difference(difference(A,one),one),difference(A,product(product(A,quotient(one,A)),quotient(one,product(A,quotient(one,A)))))) = quotient(one,quotient(one,product(A,quotient(one,A)))),
inference(paramod,[status(thm)],[c_57,c_49]) ).
cnf(c_12262,plain,
product(difference(difference(A,one),one),difference(A,one)) = quotient(one,quotient(one,product(A,quotient(one,A)))),
inference(paramod,[status(thm)],[c_1202,c_12261]) ).
cnf(c_12263,plain,
product(difference(A,one),quotient(one,difference(A,one))) = quotient(one,quotient(one,product(A,quotient(one,A)))),
inference(paramod,[status(thm)],[c_12,c_12262]) ).
cnf(c_12264,plain,
product(difference(A,one),A) = quotient(one,quotient(one,product(A,quotient(one,A)))),
inference(paramod,[status(thm)],[c_34,c_12263]) ).
cnf(c_12265,plain,
product(A,quotient(one,A)) = quotient(one,quotient(one,product(A,quotient(one,A)))),
inference(paramod,[status(thm)],[c_12,c_12264]) ).
cnf(c_1555,plain,
quotient(one,quotient(one,product(A,quotient(one,A)))) = product(A,quotient(one,A)),
inference(copy,[status(thm)],[c_12265]) ).
cnf(c_12266,plain,
quotient(A,quotient(one,B)) = product(quotient(one,B),product(B,product(A,B))),
inference(paramod,[status(thm)],[c_5,c_479]) ).
cnf(c_1579,plain,
product(quotient(one,A),product(A,product(B,A))) = quotient(B,quotient(one,A)),
inference(copy,[status(thm)],[c_12266]) ).
cnf(c_12267,plain,
quotient(product(difference(quotient(one,A),one),quotient(B,A)),quotient(one,A)) = difference(quotient(one,A),product(quotient(one,A),product(A,B))),
inference(paramod,[status(thm)],[c_479,c_861]) ).
cnf(c_12268,plain,
quotient(product(A,quotient(B,A)),quotient(one,A)) = difference(quotient(one,A),product(quotient(one,A),product(A,B))),
inference(paramod,[status(thm)],[c_35,c_12267]) ).
cnf(c_1598,plain,
quotient(product(A,quotient(B,A)),quotient(one,A)) = product(A,B),
inference(paramod,[status(thm)],[c_4,c_12268]) ).
cnf(c_1612,plain,
quotient(product(A,B),quotient(one,A)) = product(A,product(B,A)),
inference(paramod,[status(thm)],[c_5,c_1598]) ).
cnf(c_12269,plain,
quotient(product(A,difference(A,quotient(B,A))),quotient(one,A)) = product(A,product(difference(A,one),B)),
inference(paramod,[status(thm)],[c_861,c_1598]) ).
cnf(c_12270,plain,
quotient(quotient(B,A),quotient(one,A)) = product(A,product(difference(A,one),B)),
inference(paramod,[status(thm)],[c_3,c_12269]) ).
cnf(c_1629,plain,
product(quotient(one,A),product(A,B)) = product(A,product(difference(A,one),B)),
inference(paramod,[status(thm)],[c_479,c_12270]) ).
cnf(c_12271,plain,
product(A,product(difference(A,one),product(B,A))) = quotient(B,quotient(one,A)),
inference(paramod,[status(thm)],[c_1629,c_1579]) ).
cnf(c_1679,plain,
product(A,product(difference(A,B),A)) = quotient(B,quotient(one,A)),
inference(paramod,[status(thm)],[c_922,c_12271]) ).
cnf(c_12272,plain,
quotient(A,quotient(one,quotient(A,B))) = product(quotient(A,B),product(B,quotient(A,B))),
inference(paramod,[status(thm)],[c_6,c_1612]) ).
cnf(c_1685,plain,
product(quotient(A,B),product(B,quotient(A,B))) = quotient(A,quotient(one,quotient(A,B))),
inference(copy,[status(thm)],[c_12272]) ).
cnf(c_12273,plain,
quotient(product(difference(A,one),B),A) = product(difference(A,one),product(B,difference(A,one))),
inference(paramod,[status(thm)],[c_34,c_1612]) ).
cnf(c_12274,plain,
difference(A,quotient(B,A)) = product(difference(A,one),product(B,difference(A,one))),
inference(paramod,[status(thm)],[c_861,c_12273]) ).
cnf(c_1692,plain,
product(difference(A,one),product(B,difference(A,one))) = difference(A,quotient(B,A)),
inference(copy,[status(thm)],[c_12274]) ).
cnf(c_1790,plain,
product(product(A,quotient(one,A)),quotient(product(B,C),product(A,quotient(one,A)))) = product(product(A,quotient(one,A)),product(B,quotient(C,product(A,quotient(one,A))))),
inference(paramod,[status(thm)],[c_124,c_22]) ).
cnf(c_12275,plain,
product(quotient(one,quotient(one,product(A,quotient(one,A)))),quotient(one,product(difference(difference(A,one),one),quotient(one,A)))) = quotient(one,product(A,quotient(one,A))),
inference(paramod,[status(thm)],[c_16,c_445]) ).
cnf(c_12276,plain,
product(product(A,quotient(one,A)),quotient(one,product(difference(difference(A,one),one),quotient(one,A)))) = quotient(one,product(A,quotient(one,A))),
inference(paramod,[status(thm)],[c_1555,c_12275]) ).
cnf(c_12277,plain,
product(product(A,quotient(one,A)),quotient(one,product(A,quotient(one,quotient(one,quotient(one,A)))))) = quotient(one,product(A,quotient(one,A))),
inference(paramod,[status(thm)],[c_780,c_12276]) ).
cnf(c_12278,plain,
quotient(A,difference(difference(A,one),one)) = quotient(one,product(A,quotient(one,A))),
inference(paramod,[status(thm)],[c_1146,c_12277]) ).
cnf(c_2445,plain,
quotient(one,product(A,quotient(one,A))) = quotient(A,difference(difference(A,one),one)),
inference(copy,[status(thm)],[c_12278]) ).
cnf(c_12279,plain,
quotient(product(quotient(A,difference(difference(A,one),one)),product(B,product(A,quotient(one,A)))),product(A,quotient(one,A))) = difference(product(A,quotient(one,A)),product(one,B)),
inference(paramod,[status(thm)],[c_1135,c_37]) ).
cnf(c_12280,plain,
product(quotient(A,difference(difference(A,one),one)),B) = difference(product(A,quotient(one,A)),product(one,B)),
inference(paramod,[status(thm)],[c_88,c_12279]) ).
cnf(c_3011,plain,
product(quotient(A,difference(difference(A,one),one)),B) = difference(product(A,quotient(one,A)),B),
inference(paramod,[status(thm)],[c_2,c_12280]) ).
cnf(c_12281,plain,
quotient(product(A,quotient(one,product(B,quotient(one,B)))),product(product(B,quotient(one,B)),quotient(one,product(B,quotient(one,B))))) = product(A,quotient(B,difference(difference(B,one),one))),
inference(paramod,[status(thm)],[c_1135,c_1172]) ).
cnf(c_12282,plain,
quotient(product(A,quotient(one,product(B,quotient(one,B)))),one) = product(A,quotient(B,difference(difference(B,one),one))),
inference(paramod,[status(thm)],[c_1202,c_12281]) ).
cnf(c_3067,plain,
product(A,quotient(one,product(B,quotient(one,B)))) = product(A,quotient(B,difference(difference(B,one),one))),
inference(paramod,[status(thm)],[c_32,c_12282]) ).
cnf(c_3206,plain,
quotient(difference(difference(A,one),B),A) = product(A,quotient(B,A)),
inference(paramod,[status(thm)],[c_1321,c_5]) ).
cnf(c_12283,plain,
quotient(difference(quotient(A,difference(difference(A,one),one)),B),product(A,quotient(one,A))) = product(product(A,quotient(one,A)),quotient(B,product(A,quotient(one,A)))),
inference(paramod,[status(thm)],[c_1135,c_3206]) ).
cnf(c_3265,plain,
quotient(product(product(A,quotient(one,A)),B),product(A,quotient(one,A))) = product(product(A,quotient(one,A)),quotient(B,product(A,quotient(one,A)))),
inference(paramod,[status(thm)],[c_1138,c_12283]) ).
cnf(c_12284,plain,
product(product(product(x0,quotient(one,x0)),quotient(x1,product(x0,quotient(one,x0)))),quotient(product(product(x0,quotient(one,x0)),x2),product(x0,quotient(one,x0)))) != quotient(product(product(x0,quotient(one,x0)),product(x1,x2)),product(x0,quotient(one,x0))),
inference(paramod,[status(thm)],[c_3265,c_29]) ).
cnf(c_12285,plain,
product(product(product(x0,quotient(one,x0)),quotient(x1,product(x0,quotient(one,x0)))),product(product(x0,quotient(one,x0)),quotient(x2,product(x0,quotient(one,x0))))) != quotient(product(product(x0,quotient(one,x0)),product(x1,x2)),product(x0,quotient(one,x0))),
inference(paramod,[status(thm)],[c_3265,c_12284]) ).
cnf(c_12286,plain,
product(product(x0,quotient(one,x0)),product(quotient(x1,product(x0,quotient(one,x0))),product(product(x0,quotient(one,x0)),quotient(x2,product(x0,quotient(one,x0)))))) != quotient(product(product(x0,quotient(one,x0)),product(x1,x2)),product(x0,quotient(one,x0))),
inference(paramod,[status(thm)],[c_22,c_12285]) ).
cnf(c_12287,plain,
product(product(x0,quotient(one,x0)),product(quotient(x1,product(x0,quotient(one,x0))),product(product(x0,quotient(one,x0)),quotient(x2,product(x0,quotient(one,x0)))))) != product(product(x0,quotient(one,x0)),quotient(product(x1,x2),product(x0,quotient(one,x0)))),
inference(paramod,[status(thm)],[c_3265,c_12286]) ).
cnf(c_3270,plain,
product(product(x0,quotient(one,x0)),product(quotient(x1,product(x0,quotient(one,x0))),product(product(x0,quotient(one,x0)),quotient(x2,product(x0,quotient(one,x0)))))) != product(product(x0,quotient(one,x0)),product(x1,quotient(x2,product(x0,quotient(one,x0))))),
inference(paramod,[status(thm)],[c_1790,c_12287]) ).
cnf(c_12288,plain,
product(product(product(A,quotient(one,A)),difference(product(A,quotient(one,A)),B)),product(A,quotient(one,A))) = quotient(B,quotient(one,product(A,quotient(one,A)))),
inference(paramod,[status(thm)],[c_1679,c_22]) ).
cnf(c_12289,plain,
product(B,product(A,quotient(one,A))) = quotient(B,quotient(one,product(A,quotient(one,A)))),
inference(paramod,[status(thm)],[c_3,c_12288]) ).
cnf(c_3469,plain,
quotient(A,quotient(one,product(B,quotient(one,B)))) = product(A,product(B,quotient(one,B))),
inference(copy,[status(thm)],[c_12289]) ).
cnf(c_12290,plain,
difference(difference(A,one),difference(A,quotient(B,A))) = product(B,difference(A,one)),
inference(paramod,[status(thm)],[c_1692,c_4]) ).
cnf(c_3562,plain,
product(product(quotient(A,B),quotient(one,B)),B) = product(A,difference(B,one)),
inference(paramod,[status(thm)],[c_1528,c_12290]) ).
cnf(c_12291,plain,
difference(product(A,quotient(one,A)),B) = product(C,difference(product(product(A,quotient(one,A)),C),B)),
inference(paramod,[status(thm)],[c_83,c_4]) ).
cnf(c_5388,plain,
product(A,difference(product(product(B,quotient(one,B)),A),C)) = difference(product(B,quotient(one,B)),C),
inference(copy,[status(thm)],[c_12291]) ).
cnf(c_12292,plain,
difference(product(A,quotient(one,A)),product(B,C)) = quotient(product(product(D,difference(product(product(A,quotient(one,A)),D),B)),product(C,product(A,quotient(one,A)))),product(A,quotient(one,A))),
inference(paramod,[status(thm)],[c_83,c_7]) ).
cnf(c_12293,plain,
difference(product(A,quotient(one,A)),product(B,C)) = quotient(product(difference(product(A,quotient(one,A)),B),product(C,product(A,quotient(one,A)))),product(A,quotient(one,A))),
inference(paramod,[status(thm)],[c_5388,c_12292]) ).
cnf(c_5389,plain,
difference(product(A,quotient(one,A)),product(B,C)) = product(difference(product(A,quotient(one,A)),B),C),
inference(paramod,[status(thm)],[c_88,c_12293]) ).
cnf(c_12294,plain,
product(product(A,quotient(one,A)),product(difference(product(A,quotient(one,A)),B),product(A,quotient(one,A)))) = quotient(B,quotient(A,difference(difference(A,one),one))),
inference(paramod,[status(thm)],[c_2445,c_1679]) ).
cnf(c_12295,plain,
quotient(B,quotient(one,product(A,quotient(one,A)))) = quotient(B,quotient(A,difference(difference(A,one),one))),
inference(paramod,[status(thm)],[c_1679,c_12294]) ).
cnf(c_12296,plain,
product(B,product(A,quotient(one,A))) = quotient(B,quotient(A,difference(difference(A,one),one))),
inference(paramod,[status(thm)],[c_3469,c_12295]) ).
cnf(c_5475,plain,
quotient(A,quotient(B,difference(difference(B,one),one))) = product(A,product(B,quotient(one,B))),
inference(copy,[status(thm)],[c_12296]) ).
cnf(c_12297,plain,
product(product(quotient(A,product(B,quotient(one,B))),quotient(B,difference(difference(B,one),one))),product(B,quotient(one,B))) = product(A,difference(product(B,quotient(one,B)),one)),
inference(paramod,[status(thm)],[c_2445,c_3562]) ).
cnf(c_5976,plain,
product(product(quotient(A,product(B,quotient(one,B))),quotient(B,difference(difference(B,one),one))),product(B,quotient(one,B))) = product(A,quotient(B,difference(difference(B,one),one))),
inference(paramod,[status(thm)],[c_1135,c_12297]) ).
cnf(c_6024,plain,
quotient(quotient(A,B),product(C,quotient(one,C))) = quotient(A,product(product(C,quotient(one,C)),B)),
inference(paramod,[status(thm)],[c_6,c_85]) ).
cnf(c_12298,plain,
quotient(quotient(product(A,difference(product(B,quotient(one,B)),one)),quotient(one,product(product(B,quotient(one,B)),product(B,quotient(one,B))))),product(B,quotient(one,B))) = A,
inference(paramod,[status(thm)],[c_370,c_85]) ).
cnf(c_12299,plain,
quotient(quotient(product(A,quotient(B,difference(difference(B,one),one))),quotient(one,product(product(B,quotient(one,B)),product(B,quotient(one,B))))),product(B,quotient(one,B))) = A,
inference(paramod,[status(thm)],[c_1135,c_12298]) ).
cnf(c_12300,plain,
quotient(quotient(product(A,quotient(B,difference(difference(B,one),one))),quotient(one,product(B,product(quotient(one,B),product(B,quotient(one,B)))))),product(B,quotient(one,B))) = A,
inference(paramod,[status(thm)],[c_20,c_12299]) ).
cnf(c_12301,plain,
quotient(quotient(product(A,quotient(B,difference(difference(B,one),one))),quotient(one,product(B,quotient(one,quotient(one,quotient(one,B)))))),product(B,quotient(one,B))) = A,
inference(paramod,[status(thm)],[c_1685,c_12300]) ).
cnf(c_12302,plain,
quotient(product(A,quotient(B,difference(difference(B,one),one))),product(product(B,quotient(one,B)),quotient(one,product(B,quotient(one,quotient(one,quotient(one,B))))))) = A,
inference(paramod,[status(thm)],[c_6024,c_12301]) ).
cnf(c_12303,plain,
quotient(product(A,quotient(B,difference(difference(B,one),one))),quotient(B,difference(difference(B,one),one))) = A,
inference(paramod,[status(thm)],[c_1146,c_12302]) ).
cnf(c_6028,plain,
product(product(A,quotient(B,difference(difference(B,one),one))),product(B,quotient(one,B))) = A,
inference(paramod,[status(thm)],[c_5475,c_12303]) ).
cnf(c_12304,plain,
quotient(difference(A,one),product(product(B,quotient(one,B)),B)) = difference(product(B,A),one),
inference(paramod,[status(thm)],[c_6024,c_1394]) ).
cnf(c_6047,plain,
quotient(difference(A,one),difference(difference(B,one),one)) = difference(product(B,A),one),
inference(paramod,[status(thm)],[c_1321,c_12304]) ).
cnf(c_12305,plain,
quotient(A,product(B,quotient(one,B))) = product(A,quotient(B,difference(difference(B,one),one))),
inference(paramod,[status(thm)],[c_6028,c_5976]) ).
cnf(c_6054,plain,
product(A,quotient(B,difference(difference(B,one),one))) = quotient(A,product(B,quotient(one,B))),
inference(copy,[status(thm)],[c_12305]) ).
cnf(c_6110,plain,
product(A,quotient(one,product(B,quotient(one,B)))) = quotient(A,product(B,quotient(one,B))),
inference(paramod,[status(thm)],[c_6054,c_3067]) ).
cnf(c_12306,plain,
quotient(A,difference(difference(B,one),one)) = difference(product(B,quotient(one,A)),one),
inference(paramod,[status(thm)],[c_35,c_6047]) ).
cnf(c_7421,plain,
difference(product(A,quotient(one,B)),one) = quotient(B,difference(difference(A,one),one)),
inference(copy,[status(thm)],[c_12306]) ).
cnf(c_12307,plain,
product(A,quotient(product(product(B,quotient(one,B)),product(difference(product(B,quotient(one,B)),one),product(C,A))),A)) = product(product(A,quotient(one,product(B,quotient(one,B)))),product(product(B,quotient(one,B)),C)),
inference(paramod,[status(thm)],[c_1629,c_138]) ).
cnf(c_12308,plain,
product(A,quotient(product(product(B,quotient(one,B)),product(quotient(B,difference(difference(B,one),one)),product(C,A))),A)) = product(product(A,quotient(one,product(B,quotient(one,B)))),product(product(B,quotient(one,B)),C)),
inference(paramod,[status(thm)],[c_7421,c_12307]) ).
cnf(c_12309,plain,
product(A,quotient(product(product(B,quotient(one,B)),difference(product(B,quotient(one,B)),product(C,A))),A)) = product(product(A,quotient(one,product(B,quotient(one,B)))),product(product(B,quotient(one,B)),C)),
inference(paramod,[status(thm)],[c_3011,c_12308]) ).
cnf(c_12310,plain,
product(A,quotient(product(product(B,quotient(one,B)),product(difference(product(B,quotient(one,B)),C),A)),A)) = product(product(A,quotient(one,product(B,quotient(one,B)))),product(product(B,quotient(one,B)),C)),
inference(paramod,[status(thm)],[c_5389,c_12309]) ).
cnf(c_12311,plain,
product(A,quotient(product(C,A),A)) = product(product(A,quotient(one,product(B,quotient(one,B)))),product(product(B,quotient(one,B)),C)),
inference(paramod,[status(thm)],[c_84,c_12310]) ).
cnf(c_12312,plain,
product(A,C) = product(product(A,quotient(one,product(B,quotient(one,B)))),product(product(B,quotient(one,B)),C)),
inference(paramod,[status(thm)],[c_5,c_12311]) ).
cnf(c_12313,plain,
product(A,C) = product(quotient(A,product(B,quotient(one,B))),product(product(B,quotient(one,B)),C)),
inference(paramod,[status(thm)],[c_6110,c_12312]) ).
cnf(c_12074,plain,
product(quotient(A,product(B,quotient(one,B))),product(product(B,quotient(one,B)),C)) = product(A,C),
inference(copy,[status(thm)],[c_12313]) ).
cnf(c_12314,plain,
product(product(x0,quotient(one,x0)),product(x1,quotient(x2,product(x0,quotient(one,x0))))) != product(product(x0,quotient(one,x0)),product(x1,quotient(x2,product(x0,quotient(one,x0))))),
inference(paramod,[status(thm)],[c_12074,c_3270]) ).
cnf(c_12093,plain,
$false,
inference(copy,[status(thm)],[c_12314]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP768-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.37 % Computer : n026.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Fri Sep 25 15:47:54 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.37 % Process 2939954 was started by sandbox on n026,
% 0.09/0.37 % Fri Sep 25 15:47:54 2026
% 0.09/0.37 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.09/0.38
% 0.09/0.38 % From the command line: assign(max_seconds, 300).
% 36.98/5.76
% 36.98/5.76 % SZS status Unsatisfiable for theBenchmark
% 36.98/5.76
% 36.98/5.76 % Proof 1 at 4.15 (+ 0.91) seconds.
% 36.98/5.76 % Length of proof is 173.
% 36.98/5.76 % Level of proof is 31.
% 36.98/5.76 % Maximum clause weight is 90.000.
% 36.98/5.76 % Given clauses 323.
% 36.98/5.76
% 36.98/5.76 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------