%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP779+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 : n014.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:26 AM UTC 2026
% Result : Theorem 41.57s 6.41s
% Output : CNFRefutation 41.57s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 15
% Syntax : Number of formulae : 201 ( 197 unt; 0 def)
% Number of atoms : 205 ( 187 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 14 ( 10 ~; 2 |; 0 &)
% ( 2 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 1 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 8 con; 0-2 aty)
% Number of variables : 218 ( 0 sgn 21 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(sos01,axiom,
! [B,A] : difference(A,product(A,B)) = B,
file('theBenchmark.p',sos01) ).
fof(sos02,axiom,
! [B,A] : product(A,difference(A,B)) = B,
file('theBenchmark.p',sos02) ).
fof(sos03,axiom,
! [B,A] : quotient(product(A,B),B) = A,
file('theBenchmark.p',sos03) ).
fof(sos04,axiom,
! [B,A] : product(quotient(A,B),B) = A,
file('theBenchmark.p',sos04) ).
fof(sos05,axiom,
! [D,C,B,A] : product(product(A,B),product(C,D)) = product(product(A,C),product(B,D)),
file('theBenchmark.p',sos05) ).
fof(sos06,axiom,
! [A] : product(A,A) = A,
file('theBenchmark.p',sos06) ).
fof(sos07,axiom,
! [B,A] : product(product(product(A,B),B),product(B,product(B,A))) = B,
file('theBenchmark.p',sos07) ).
fof(sos08,axiom,
! [X0,X1,X2] :
( d(X0,X1,X2)
<=> product(X0,X1) = product(X1,X2) ),
file('theBenchmark.p',sos08) ).
fof(sos09,axiom,
! [X3,X4,X5] :
( m(X3,X4,X5)
<=> product(product(X3,X4),product(X4,X5)) = product(X3,X5) ),
file('theBenchmark.p',sos09) ).
fof(goals,conjecture,
m(bigA,b1,bigC),
file('theBenchmark.p',goals) ).
fof(goals_neg,negated_conjecture,
~ m(bigA,b1,bigC),
inference(assume_negation,[status(cth)],[goals]) ).
cnf(c_12,plain,
( product(B,C) = product(A,B)
| ~ d(A,B,C) ),
inference(clausify,[status(thm)],[sos08]) ).
fof(sos10,axiom,
d(b,bigA,c),
file('theBenchmark.p',sos10) ).
cnf(c_13,plain,
d(b,bigA,c),
inference(clausify,[status(thm)],[sos10]) ).
fof(sos12,axiom,
d(b,a,bigC),
file('theBenchmark.p',sos12) ).
cnf(c_15,plain,
d(b,a,bigC),
inference(clausify,[status(thm)],[sos12]) ).
fof(sos13,axiom,
d(a,b1,c1),
file('theBenchmark.p',sos13) ).
cnf(c_16,plain,
d(a,b1,c1),
inference(clausify,[status(thm)],[sos13]) ).
fof(sos14,axiom,
d(a1,b,c1),
file('theBenchmark.p',sos14) ).
cnf(c_17,plain,
d(a1,b,c1),
inference(clausify,[status(thm)],[sos14]) ).
fof(sos15,axiom,
d(a1,b1,c),
file('theBenchmark.p',sos15) ).
cnf(c_18,plain,
d(a1,b1,c),
inference(clausify,[status(thm)],[sos15]) ).
cnf(c_19,plain,
product(b1,c) = product(a1,b1),
inference(resolve,[status(thm)],[c_18,c_12]) ).
cnf(c_20,plain,
product(a1,b1) = product(b1,c),
inference(copy,[status(thm)],[c_19]) ).
cnf(c_21,plain,
product(b,c1) = product(a1,b),
inference(resolve,[status(thm)],[c_17,c_12]) ).
cnf(c_22,plain,
product(a1,b) = product(b,c1),
inference(copy,[status(thm)],[c_21]) ).
cnf(c_23,plain,
product(b1,c1) = product(a,b1),
inference(resolve,[status(thm)],[c_16,c_12]) ).
cnf(c_24,plain,
product(a,bigC) = product(b,a),
inference(resolve,[status(thm)],[c_15,c_12]) ).
cnf(c_25,plain,
product(b,a) = product(a,bigC),
inference(copy,[status(thm)],[c_24]) ).
cnf(c_28,plain,
product(bigA,c) = product(b,bigA),
inference(resolve,[status(thm)],[c_13,c_12]) ).
cnf(c_29,negated_conjecture,
~ m(bigA,b1,bigC),
inference(clausify,[status(thm)],[goals_neg]) ).
cnf(c_30,plain,
( product(product(A,B),product(B,C)) != product(A,C)
| m(A,B,C) ),
inference(clausify,[status(thm)],[sos09]) ).
cnf(c_32,plain,
product(product(product(A,B),B),product(B,product(B,A))) = B,
inference(clausify,[status(thm)],[sos07]) ).
cnf(c_33,plain,
product(A,A) = A,
inference(clausify,[status(thm)],[sos06]) ).
cnf(c_34,plain,
product(product(A,B),product(C,D)) = product(product(A,C),product(B,D)),
inference(clausify,[status(thm)],[sos05]) ).
cnf(c_35,plain,
product(quotient(A,B),B) = A,
inference(clausify,[status(thm)],[sos04]) ).
cnf(c_36,plain,
quotient(product(A,B),B) = A,
inference(clausify,[status(thm)],[sos03]) ).
cnf(c_37,plain,
product(A,difference(A,B)) = B,
inference(clausify,[status(thm)],[sos02]) ).
cnf(c_38,plain,
difference(A,product(A,B)) = B,
inference(clausify,[status(thm)],[sos01]) ).
cnf(c_39,negated_conjecture,
product(product(bigA,b1),product(b1,bigC)) != product(bigA,bigC),
inference(resolve,[status(thm)],[c_30,c_29]) ).
cnf(c_11026,plain,
product(product(b1,c),product(A,B)) = product(product(a1,A),product(b1,B)),
inference(paramod,[status(thm)],[c_20,c_34]) ).
cnf(c_75,plain,
product(product(a1,A),product(b1,B)) = product(product(b1,c),product(A,B)),
inference(copy,[status(thm)],[c_11026]) ).
cnf(c_11027,plain,
product(product(A,B),product(b1,c)) = product(product(A,a1),product(B,b1)),
inference(paramod,[status(thm)],[c_20,c_34]) ).
cnf(c_76,plain,
product(product(A,a1),product(B,b1)) = product(product(A,B),product(b1,c)),
inference(copy,[status(thm)],[c_11027]) ).
cnf(c_11028,plain,
product(product(b,c1),product(A,B)) = product(product(a1,A),product(b,B)),
inference(paramod,[status(thm)],[c_22,c_34]) ).
cnf(c_77,plain,
product(product(a1,A),product(b,B)) = product(product(b,c1),product(A,B)),
inference(copy,[status(thm)],[c_11028]) ).
cnf(c_11029,plain,
product(product(A,B),product(b,c1)) = product(product(A,a1),product(B,b)),
inference(paramod,[status(thm)],[c_22,c_34]) ).
cnf(c_78,plain,
product(product(A,a1),product(B,b)) = product(product(A,B),product(b,c1)),
inference(copy,[status(thm)],[c_11029]) ).
cnf(c_11030,plain,
product(product(a,b1),product(A,B)) = product(product(b1,A),product(c1,B)),
inference(paramod,[status(thm)],[c_23,c_34]) ).
cnf(c_79,plain,
product(product(b1,A),product(c1,B)) = product(product(a,b1),product(A,B)),
inference(copy,[status(thm)],[c_11030]) ).
cnf(c_11031,plain,
product(product(A,B),product(a,b1)) = product(product(A,b1),product(B,c1)),
inference(paramod,[status(thm)],[c_23,c_34]) ).
cnf(c_80,plain,
product(product(A,b1),product(B,c1)) = product(product(A,B),product(a,b1)),
inference(copy,[status(thm)],[c_11031]) ).
cnf(c_11032,plain,
product(product(a,bigC),product(A,B)) = product(product(b,A),product(a,B)),
inference(paramod,[status(thm)],[c_25,c_34]) ).
cnf(c_81,plain,
product(product(b,A),product(a,B)) = product(product(a,bigC),product(A,B)),
inference(copy,[status(thm)],[c_11032]) ).
cnf(c_11033,plain,
product(product(A,B),product(a,bigC)) = product(product(A,b),product(B,a)),
inference(paramod,[status(thm)],[c_25,c_34]) ).
cnf(c_82,plain,
product(product(A,b),product(B,a)) = product(product(A,B),product(a,bigC)),
inference(copy,[status(thm)],[c_11033]) ).
cnf(c_11034,plain,
product(product(A,B),product(b,bigA)) = product(product(A,bigA),product(B,c)),
inference(paramod,[status(thm)],[c_28,c_34]) ).
cnf(c_86,plain,
product(product(A,bigA),product(B,c)) = product(product(A,B),product(b,bigA)),
inference(copy,[status(thm)],[c_11034]) ).
cnf(c_11035,plain,
product(A,product(B,C)) = product(product(A,B),product(A,C)),
inference(paramod,[status(thm)],[c_33,c_34]) ).
cnf(c_87,plain,
product(product(A,B),product(A,C)) = product(A,product(B,C)),
inference(copy,[status(thm)],[c_11035]) ).
cnf(c_11036,plain,
product(product(A,B),C) = product(product(A,C),product(B,C)),
inference(paramod,[status(thm)],[c_33,c_34]) ).
cnf(c_88,plain,
product(product(A,B),product(C,B)) = product(product(A,C),B),
inference(copy,[status(thm)],[c_11036]) ).
cnf(c_11037,plain,
product(product(A,B),C) = product(product(A,quotient(C,D)),product(B,D)),
inference(paramod,[status(thm)],[c_35,c_34]) ).
cnf(c_98,plain,
product(product(A,quotient(B,C)),product(D,C)) = product(product(A,D),B),
inference(copy,[status(thm)],[c_11037]) ).
cnf(c_11038,plain,
product(A,product(B,C)) = product(product(D,B),product(difference(D,A),C)),
inference(paramod,[status(thm)],[c_37,c_34]) ).
cnf(c_112,plain,
product(product(A,B),product(difference(A,C),D)) = product(C,product(B,D)),
inference(copy,[status(thm)],[c_11038]) ).
cnf(c_11039,plain,
product(product(A,B),C) = product(product(A,D),product(B,difference(D,C))),
inference(paramod,[status(thm)],[c_37,c_34]) ).
cnf(c_113,plain,
product(product(A,B),product(C,difference(B,D))) = product(product(A,C),D),
inference(copy,[status(thm)],[c_11039]) ).
cnf(c_114,plain,
quotient(A,difference(B,A)) = B,
inference(paramod,[status(thm)],[c_37,c_36]) ).
cnf(c_121,plain,
difference(product(product(A,B),B),B) = product(B,product(B,A)),
inference(paramod,[status(thm)],[c_32,c_38]) ).
cnf(c_124,plain,
difference(quotient(A,B),A) = B,
inference(paramod,[status(thm)],[c_35,c_38]) ).
cnf(c_11040,plain,
product(a1,product(A,b1)) = product(product(a1,A),product(b1,c)),
inference(paramod,[status(thm)],[c_33,c_76]) ).
cnf(c_11041,plain,
product(a1,product(A,b1)) = product(product(b1,c),product(A,c)),
inference(paramod,[status(thm)],[c_75,c_11040]) ).
cnf(c_291,plain,
product(product(b1,c),product(A,c)) = product(a1,product(A,b1)),
inference(copy,[status(thm)],[c_11041]) ).
cnf(c_11042,plain,
product(a1,product(A,b)) = product(product(a1,A),product(b,c1)),
inference(paramod,[status(thm)],[c_33,c_78]) ).
cnf(c_11043,plain,
product(a1,product(A,b)) = product(product(b,c1),product(A,c1)),
inference(paramod,[status(thm)],[c_77,c_11042]) ).
cnf(c_316,plain,
product(product(b,c1),product(A,c1)) = product(a1,product(A,b)),
inference(copy,[status(thm)],[c_11043]) ).
cnf(c_327,plain,
product(product(b1,A),c1) = product(product(a,b1),product(A,c1)),
inference(paramod,[status(thm)],[c_33,c_79]) ).
cnf(c_338,plain,
product(product(A,b1),product(B,c1)) = product(product(A,a),product(B,b1)),
inference(paramod,[status(thm)],[c_80,c_34]) ).
cnf(c_11044,plain,
product(product(b1,A),c1) = product(product(a,a),product(A,b1)),
inference(paramod,[status(thm)],[c_338,c_327]) ).
cnf(c_349,plain,
product(product(b1,A),c1) = product(a,product(A,b1)),
inference(paramod,[status(thm)],[c_33,c_11044]) ).
cnf(c_11045,plain,
product(b,product(A,a)) = product(product(b,A),product(a,bigC)),
inference(paramod,[status(thm)],[c_33,c_82]) ).
cnf(c_11046,plain,
product(b,product(A,a)) = product(product(a,bigC),product(A,bigC)),
inference(paramod,[status(thm)],[c_81,c_11045]) ).
cnf(c_365,plain,
product(product(a,bigC),product(A,bigC)) = product(b,product(A,a)),
inference(copy,[status(thm)],[c_11046]) ).
cnf(c_421,plain,
product(product(A,bigA),product(B,c)) = product(product(A,b),product(B,bigA)),
inference(paramod,[status(thm)],[c_86,c_34]) ).
cnf(c_441,plain,
product(product(A,B),A) = product(A,product(B,A)),
inference(paramod,[status(thm)],[c_33,c_87]) ).
cnf(c_475,plain,
product(product(A,B),product(difference(A,C),B)) = product(C,B),
inference(paramod,[status(thm)],[c_37,c_88]) ).
cnf(c_11047,plain,
product(product(a1,A),product(b1,c)) = product(product(b1,A),c),
inference(paramod,[status(thm)],[c_88,c_75]) ).
cnf(c_11048,plain,
product(product(b1,c),product(A,c)) = product(product(b1,A),c),
inference(paramod,[status(thm)],[c_75,c_11047]) ).
cnf(c_11049,plain,
product(a1,product(A,b1)) = product(product(b1,A),c),
inference(paramod,[status(thm)],[c_291,c_11048]) ).
cnf(c_484,plain,
product(product(b1,A),c) = product(a1,product(A,b1)),
inference(copy,[status(thm)],[c_11049]) ).
cnf(c_11050,plain,
product(product(a1,A),product(b,c1)) = product(product(b,A),c1),
inference(paramod,[status(thm)],[c_88,c_77]) ).
cnf(c_11051,plain,
product(product(b,c1),product(A,c1)) = product(product(b,A),c1),
inference(paramod,[status(thm)],[c_77,c_11050]) ).
cnf(c_11052,plain,
product(a1,product(A,b)) = product(product(b,A),c1),
inference(paramod,[status(thm)],[c_316,c_11051]) ).
cnf(c_487,plain,
product(product(b,A),c1) = product(a1,product(A,b)),
inference(copy,[status(thm)],[c_11052]) ).
cnf(c_11053,plain,
product(product(b,A),product(a,bigC)) = product(product(a,A),bigC),
inference(paramod,[status(thm)],[c_88,c_81]) ).
cnf(c_11054,plain,
product(product(a,bigC),product(A,bigC)) = product(product(a,A),bigC),
inference(paramod,[status(thm)],[c_81,c_11053]) ).
cnf(c_11055,plain,
product(b,product(A,a)) = product(product(a,A),bigC),
inference(paramod,[status(thm)],[c_365,c_11054]) ).
cnf(c_489,plain,
product(product(a,A),bigC) = product(b,product(A,a)),
inference(copy,[status(thm)],[c_11055]) ).
cnf(c_503,plain,
quotient(product(a,product(A,b1)),c1) = product(b1,A),
inference(paramod,[status(thm)],[c_349,c_36]) ).
cnf(c_534,plain,
quotient(product(A,product(B,A)),A) = product(A,B),
inference(paramod,[status(thm)],[c_441,c_36]) ).
cnf(c_554,plain,
product(product(bigA,quotient(product(b1,bigC),A)),product(b1,A)) != product(bigA,bigC),
inference(paramod,[status(thm)],[c_98,c_39]) ).
cnf(c_574,plain,
product(product(bigA,A),product(b1,difference(A,product(b1,bigC)))) != product(bigA,bigC),
inference(paramod,[status(thm)],[c_114,c_554]) ).
cnf(c_580,plain,
product(product(a1,product(c1,b)),product(c1,product(c1,b))) = c1,
inference(paramod,[status(thm)],[c_487,c_32]) ).
cnf(c_631,plain,
quotient(product(a,A),c1) = product(b1,quotient(A,b1)),
inference(paramod,[status(thm)],[c_35,c_503]) ).
cnf(c_632,plain,
quotient(a,c1) = product(b1,quotient(a,b1)),
inference(paramod,[status(thm)],[c_33,c_631]) ).
cnf(c_633,plain,
product(b1,quotient(c1,b1)) = a,
inference(paramod,[status(thm)],[c_631,c_36]) ).
cnf(c_11056,plain,
quotient(A,c1) = product(b1,quotient(difference(a,A),b1)),
inference(paramod,[status(thm)],[c_37,c_631]) ).
cnf(c_634,plain,
product(b1,quotient(difference(a,A),b1)) = quotient(A,c1),
inference(copy,[status(thm)],[c_11056]) ).
cnf(c_11057,plain,
difference(b1,a) = quotient(c1,b1),
inference(paramod,[status(thm)],[c_633,c_38]) ).
cnf(c_645,plain,
quotient(c1,b1) = difference(b1,a),
inference(copy,[status(thm)],[c_11057]) ).
cnf(c_650,plain,
product(difference(b1,a),b1) = c1,
inference(paramod,[status(thm)],[c_645,c_35]) ).
cnf(c_11058,plain,
product(product(b1,difference(b1,a)),c) = product(a1,c1),
inference(paramod,[status(thm)],[c_650,c_484]) ).
cnf(c_11059,plain,
product(a,c) = product(a1,c1),
inference(paramod,[status(thm)],[c_37,c_11058]) ).
cnf(c_686,plain,
product(a1,c1) = product(a,c),
inference(copy,[status(thm)],[c_11059]) ).
cnf(c_11060,plain,
product(product(a,c),product(A,B)) = product(product(a1,A),product(c1,B)),
inference(paramod,[status(thm)],[c_686,c_34]) ).
cnf(c_701,plain,
product(product(a1,A),product(c1,B)) = product(product(a,c),product(A,B)),
inference(copy,[status(thm)],[c_11060]) ).
cnf(c_11061,plain,
product(product(a,c),product(product(c1,b),product(c1,b))) = c1,
inference(paramod,[status(thm)],[c_701,c_580]) ).
cnf(c_734,plain,
product(product(a,c),product(c1,b)) = c1,
inference(paramod,[status(thm)],[c_33,c_11061]) ).
cnf(c_763,plain,
product(product(A,B),product(difference(A,C),difference(B,D))) = product(C,D),
inference(paramod,[status(thm)],[c_37,c_112]) ).
cnf(c_807,plain,
difference(product(A,B),product(product(A,C),D)) = product(C,difference(B,D)),
inference(paramod,[status(thm)],[c_113,c_38]) ).
cnf(c_11062,plain,
difference(b1,quotient(A,c1)) = quotient(difference(a,A),b1),
inference(paramod,[status(thm)],[c_634,c_38]) ).
cnf(c_1097,plain,
quotient(difference(a,A),b1) = difference(b1,quotient(A,c1)),
inference(copy,[status(thm)],[c_11062]) ).
cnf(c_1103,plain,
product(difference(b1,quotient(A,c1)),b1) = difference(a,A),
inference(paramod,[status(thm)],[c_1097,c_35]) ).
cnf(c_11063,plain,
c1 = product(product(a,c1),product(c,b)),
inference(paramod,[status(thm)],[c_734,c_34]) ).
cnf(c_1125,plain,
product(product(a,c1),product(c,b)) = c1,
inference(copy,[status(thm)],[c_11063]) ).
cnf(c_1208,plain,
product(difference(b1,A),b1) = difference(a,product(A,c1)),
inference(paramod,[status(thm)],[c_36,c_1103]) ).
cnf(c_1311,plain,
difference(product(a,c1),c1) = product(c,b),
inference(paramod,[status(thm)],[c_1125,c_38]) ).
cnf(c_1572,plain,
quotient(product(A,B),A) = product(A,quotient(B,A)),
inference(paramod,[status(thm)],[c_35,c_534]) ).
cnf(c_11064,plain,
quotient(product(b,bigA),bigA) = product(bigA,quotient(c,bigA)),
inference(paramod,[status(thm)],[c_28,c_1572]) ).
cnf(c_11065,plain,
b = product(bigA,quotient(c,bigA)),
inference(paramod,[status(thm)],[c_36,c_11064]) ).
cnf(c_1585,plain,
product(bigA,quotient(c,bigA)) = b,
inference(copy,[status(thm)],[c_11065]) ).
cnf(c_11066,plain,
quotient(A,B) = product(B,quotient(difference(B,A),B)),
inference(paramod,[status(thm)],[c_37,c_1572]) ).
cnf(c_1587,plain,
product(A,quotient(difference(A,B),A)) = quotient(B,A),
inference(copy,[status(thm)],[c_11066]) ).
cnf(c_1588,plain,
difference(product(A,quotient(B,A)),product(A,B)) = A,
inference(paramod,[status(thm)],[c_1572,c_124]) ).
cnf(c_11067,plain,
difference(bigA,b) = quotient(c,bigA),
inference(paramod,[status(thm)],[c_1585,c_38]) ).
cnf(c_1631,plain,
quotient(c,bigA) = difference(bigA,b),
inference(copy,[status(thm)],[c_11067]) ).
cnf(c_1645,plain,
product(difference(bigA,b),bigA) = c,
inference(paramod,[status(thm)],[c_1631,c_35]) ).
cnf(c_11068,plain,
difference(product(c,bigA),bigA) = product(bigA,product(bigA,difference(bigA,b))),
inference(paramod,[status(thm)],[c_1645,c_121]) ).
cnf(c_1675,plain,
difference(product(c,bigA),bigA) = product(bigA,b),
inference(paramod,[status(thm)],[c_37,c_11068]) ).
cnf(c_11069,plain,
difference(A,quotient(B,A)) = quotient(difference(A,B),A),
inference(paramod,[status(thm)],[c_1587,c_38]) ).
cnf(c_1741,plain,
quotient(difference(A,B),A) = difference(A,quotient(B,A)),
inference(copy,[status(thm)],[c_11069]) ).
cnf(c_1754,plain,
product(difference(A,quotient(B,A)),A) = difference(A,B),
inference(paramod,[status(thm)],[c_1741,c_35]) ).
cnf(c_1787,plain,
difference(product(c1,product(b1,quotient(a,b1))),product(c1,a)) = c1,
inference(paramod,[status(thm)],[c_632,c_1588]) ).
cnf(c_11070,plain,
product(difference(A,B),A) = difference(A,product(B,A)),
inference(paramod,[status(thm)],[c_36,c_1754]) ).
cnf(c_1845,plain,
difference(A,product(B,A)) = product(difference(A,B),A),
inference(copy,[status(thm)],[c_11070]) ).
cnf(c_11071,plain,
difference(product(difference(A,B),A),A) = product(A,product(A,difference(A,quotient(B,A)))),
inference(paramod,[status(thm)],[c_1754,c_121]) ).
cnf(c_11072,plain,
difference(product(difference(A,B),A),A) = product(A,quotient(B,A)),
inference(paramod,[status(thm)],[c_37,c_11071]) ).
cnf(c_1856,plain,
product(A,quotient(B,A)) = difference(product(difference(A,B),A),A),
inference(copy,[status(thm)],[c_11072]) ).
cnf(c_11073,plain,
difference(product(c1,difference(product(difference(b1,a),b1),b1)),product(c1,a)) = c1,
inference(paramod,[status(thm)],[c_1856,c_1787]) ).
cnf(c_11074,plain,
difference(product(c1,difference(difference(a,product(a,c1)),b1)),product(c1,a)) = c1,
inference(paramod,[status(thm)],[c_1208,c_11073]) ).
cnf(c_11075,plain,
difference(product(c1,difference(c1,b1)),product(c1,a)) = c1,
inference(paramod,[status(thm)],[c_38,c_11074]) ).
cnf(c_1896,plain,
difference(b1,product(c1,a)) = c1,
inference(paramod,[status(thm)],[c_37,c_11075]) ).
cnf(c_11076,plain,
quotient(a,c1) = difference(product(difference(b1,a),b1),b1),
inference(paramod,[status(thm)],[c_1856,c_632]) ).
cnf(c_11077,plain,
quotient(a,c1) = difference(difference(a,product(a,c1)),b1),
inference(paramod,[status(thm)],[c_1208,c_11076]) ).
cnf(c_1937,plain,
quotient(a,c1) = difference(c1,b1),
inference(paramod,[status(thm)],[c_38,c_11077]) ).
cnf(c_1957,plain,
product(difference(c1,b1),c1) = a,
inference(paramod,[status(thm)],[c_1937,c_35]) ).
cnf(c_11078,plain,
product(b1,c1) = product(c1,a),
inference(paramod,[status(thm)],[c_1896,c_37]) ).
cnf(c_11079,plain,
product(a,b1) = product(c1,a),
inference(paramod,[status(thm)],[c_23,c_11078]) ).
cnf(c_2039,plain,
product(c1,a) = product(a,b1),
inference(copy,[status(thm)],[c_11079]) ).
cnf(c_11080,plain,
difference(product(a,c1),c1) = product(c1,product(c1,difference(c1,b1))),
inference(paramod,[status(thm)],[c_1957,c_121]) ).
cnf(c_11081,plain,
product(c,b) = product(c1,product(c1,difference(c1,b1))),
inference(paramod,[status(thm)],[c_1311,c_11080]) ).
cnf(c_11082,plain,
product(c,b) = product(c1,b1),
inference(paramod,[status(thm)],[c_37,c_11081]) ).
cnf(c_2159,plain,
product(c1,b1) = product(c,b),
inference(copy,[status(thm)],[c_11082]) ).
cnf(c_2244,plain,
difference(c1,product(c,b)) = b1,
inference(paramod,[status(thm)],[c_2159,c_38]) ).
cnf(c_11083,plain,
difference(a,product(a,b1)) = product(difference(a,c1),a),
inference(paramod,[status(thm)],[c_2039,c_1845]) ).
cnf(c_11084,plain,
b1 = product(difference(a,c1),a),
inference(paramod,[status(thm)],[c_38,c_11083]) ).
cnf(c_2636,plain,
product(difference(a,c1),a) = b1,
inference(copy,[status(thm)],[c_11084]) ).
cnf(c_11085,plain,
product(product(a,difference(a,c1)),bigC) = product(b,b1),
inference(paramod,[status(thm)],[c_2636,c_489]) ).
cnf(c_2679,plain,
product(c1,bigC) = product(b,b1),
inference(paramod,[status(thm)],[c_37,c_11085]) ).
cnf(c_11086,plain,
difference(product(A,b),product(product(A,bigA),product(B,c))) = product(B,bigA),
inference(paramod,[status(thm)],[c_421,c_38]) ).
cnf(c_3565,plain,
product(bigA,difference(b,product(A,c))) = product(A,bigA),
inference(paramod,[status(thm)],[c_807,c_11086]) ).
cnf(c_4611,plain,
difference(product(A,B),product(C,B)) = product(difference(A,C),B),
inference(paramod,[status(thm)],[c_475,c_38]) ).
cnf(c_11087,plain,
difference(bigA,product(A,bigA)) = difference(b,product(A,c)),
inference(paramod,[status(thm)],[c_3565,c_38]) ).
cnf(c_4747,plain,
product(difference(bigA,A),bigA) = difference(b,product(A,c)),
inference(paramod,[status(thm)],[c_1845,c_11087]) ).
cnf(c_6238,plain,
difference(product(A,B),B) = product(difference(A,B),B),
inference(paramod,[status(thm)],[c_33,c_4611]) ).
cnf(c_6299,plain,
difference(product(b,b1),product(A,bigC)) = product(difference(c1,A),bigC),
inference(paramod,[status(thm)],[c_2679,c_4611]) ).
cnf(c_6467,plain,
product(difference(c,bigA),bigA) = product(bigA,b),
inference(paramod,[status(thm)],[c_6238,c_1675]) ).
cnf(c_11088,plain,
difference(bigA,product(bigA,b)) = product(difference(bigA,difference(c,bigA)),bigA),
inference(paramod,[status(thm)],[c_6467,c_1845]) ).
cnf(c_11089,plain,
b = product(difference(bigA,difference(c,bigA)),bigA),
inference(paramod,[status(thm)],[c_38,c_11088]) ).
cnf(c_11090,plain,
b = difference(b,product(difference(c,bigA),c)),
inference(paramod,[status(thm)],[c_4747,c_11089]) ).
cnf(c_6669,plain,
difference(b,product(difference(c,bigA),c)) = b,
inference(copy,[status(thm)],[c_11090]) ).
cnf(c_11091,plain,
product(b,b) = product(difference(c,bigA),c),
inference(paramod,[status(thm)],[c_6669,c_37]) ).
cnf(c_11092,plain,
b = product(difference(c,bigA),c),
inference(paramod,[status(thm)],[c_33,c_11091]) ).
cnf(c_6913,plain,
product(difference(c,bigA),c) = b,
inference(copy,[status(thm)],[c_11092]) ).
cnf(c_11093,plain,
product(product(c,difference(c,bigA)),c) = product(c,b),
inference(paramod,[status(thm)],[c_6913,c_441]) ).
cnf(c_11094,plain,
product(bigA,c) = product(c,b),
inference(paramod,[status(thm)],[c_37,c_11093]) ).
cnf(c_11095,plain,
product(b,bigA) = product(c,b),
inference(paramod,[status(thm)],[c_28,c_11094]) ).
cnf(c_6943,plain,
product(c,b) = product(b,bigA),
inference(copy,[status(thm)],[c_11095]) ).
cnf(c_7069,plain,
difference(c1,product(b,bigA)) = b1,
inference(paramod,[status(thm)],[c_6943,c_2244]) ).
cnf(c_7785,plain,
difference(product(A,B),product(C,D)) = product(difference(A,C),difference(B,D)),
inference(paramod,[status(thm)],[c_763,c_38]) ).
cnf(c_11096,plain,
product(difference(b,A),difference(b1,bigC)) = product(difference(c1,A),bigC),
inference(paramod,[status(thm)],[c_7785,c_6299]) ).
cnf(c_7873,plain,
product(difference(c1,A),bigC) = product(difference(b,A),difference(b1,bigC)),
inference(copy,[status(thm)],[c_11096]) ).
cnf(c_11097,plain,
product(b1,bigC) = product(difference(b,product(b,bigA)),difference(b1,bigC)),
inference(paramod,[status(thm)],[c_7069,c_7873]) ).
cnf(c_11098,plain,
product(b1,bigC) = product(bigA,difference(b1,bigC)),
inference(paramod,[status(thm)],[c_38,c_11097]) ).
cnf(c_10988,plain,
product(bigA,difference(b1,bigC)) = product(b1,bigC),
inference(copy,[status(thm)],[c_11098]) ).
cnf(c_10995,plain,
difference(bigA,product(b1,bigC)) = difference(b1,bigC),
inference(paramod,[status(thm)],[c_10988,c_38]) ).
cnf(c_11099,plain,
product(product(bigA,bigA),product(b1,difference(b1,bigC))) != product(bigA,bigC),
inference(paramod,[status(thm)],[c_10995,c_574]) ).
cnf(c_11100,plain,
product(bigA,product(b1,difference(b1,bigC))) != product(bigA,bigC),
inference(paramod,[status(thm)],[c_33,c_11099]) ).
cnf(c_11101,plain,
product(bigA,bigC) != product(bigA,bigC),
inference(paramod,[status(thm)],[c_37,c_11100]) ).
cnf(c_11025,plain,
$false,
inference(copy,[status(thm)],[c_11101]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP779+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.10/0.36 % Computer : n014.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Fri Sep 25 15:46:17 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.37 % Process 606199 was started by sandbox on n014,
% 0.10/0.37 % Fri Sep 25 15:46:17 2026
% 0.10/0.37 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.10/0.37
% 0.10/0.37 % From the command line: assign(max_seconds, 300).
% 41.57/6.41
% 41.57/6.41 % given #500 (T,wt=15): 1926 m(difference(c,b1),c,c) | product(a1,c) != a1. [back_rewrite(1394),rewrite([1856(5),1208(5),686(4),38(5)])].
% 41.57/6.41
% 41.57/6.41 % given #1000 (A,wt=25): 623 m(b,A,difference(A,c1)) | product(b,difference(A,c1)) != product(a1,product(A,b)). [para(487(a,1),109(b,1)),flip(b)].
% 41.57/6.41
% 41.57/6.41 % SZS status Theorem for theBenchmark
% 41.57/6.41
% 41.57/6.41 % Proof 1 at 4.42 (+ 1.29) seconds.
% 41.57/6.41 % Length of proof is 119.
% 41.57/6.41 % Level of proof is 21.
% 41.57/6.41 % Maximum clause weight is 29.000.
% 41.57/6.41 % Given clauses 1429.
% 41.57/6.41
% 41.57/6.41 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------