%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP778+1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 07:31:26 AM UTC 2026
% Result : Theorem 56.55s 8.51s
% Output : CNFRefutation 56.55s
% Verified :
% SZS Type : Refutation
% Derivation depth : 44
% Number of leaves : 14
% Syntax : Number of formulae : 216 ( 212 unt; 0 def)
% Number of atoms : 220 ( 204 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 15 ( 11 ~; 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 : 10 ( 10 usr; 7 con; 0-2 aty)
% Number of variables : 141 ( 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(b1,b,b2),
file('theBenchmark.p',goals) ).
fof(goals_neg,negated_conjecture,
~ m(b1,b,b2),
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(a1,b,c),
file('theBenchmark.p',sos10) ).
cnf(c_13,plain,
d(a1,b,c),
inference(clausify,[status(thm)],[sos10]) ).
fof(sos11,axiom,
d(a,b1,c),
file('theBenchmark.p',sos11) ).
cnf(c_14,plain,
d(a,b1,c),
inference(clausify,[status(thm)],[sos11]) ).
fof(sos12,axiom,
d(a,b,c1),
file('theBenchmark.p',sos12) ).
cnf(c_15,plain,
d(a,b,c1),
inference(clausify,[status(thm)],[sos12]) ).
fof(sos14,axiom,
d(a1,b2,c1),
file('theBenchmark.p',sos14) ).
cnf(c_17,plain,
d(a1,b2,c1),
inference(clausify,[status(thm)],[sos14]) ).
cnf(c_21,plain,
product(b2,c1) = product(a1,b2),
inference(resolve,[status(thm)],[c_17,c_12]) ).
cnf(c_24,plain,
product(b,c1) = product(a,b),
inference(resolve,[status(thm)],[c_15,c_12]) ).
cnf(c_25,plain,
product(a,b) = product(b,c1),
inference(copy,[status(thm)],[c_24]) ).
cnf(c_26,plain,
product(b1,c) = product(a,b1),
inference(resolve,[status(thm)],[c_14,c_12]) ).
cnf(c_27,plain,
product(a,b1) = product(b1,c),
inference(copy,[status(thm)],[c_26]) ).
cnf(c_28,plain,
product(b,c) = product(a1,b),
inference(resolve,[status(thm)],[c_13,c_12]) ).
cnf(c_29,plain,
product(a1,b) = product(b,c),
inference(copy,[status(thm)],[c_28]) ).
cnf(c_30,negated_conjecture,
~ m(b1,b,b2),
inference(clausify,[status(thm)],[goals_neg]) ).
cnf(c_31,plain,
( product(product(A,B),product(B,C)) != product(A,C)
| m(A,B,C) ),
inference(clausify,[status(thm)],[sos09]) ).
cnf(c_33,plain,
product(product(product(A,B),B),product(B,product(B,A))) = B,
inference(clausify,[status(thm)],[sos07]) ).
cnf(c_34,plain,
product(A,A) = A,
inference(clausify,[status(thm)],[sos06]) ).
cnf(c_35,plain,
product(product(A,B),product(C,D)) = product(product(A,C),product(B,D)),
inference(clausify,[status(thm)],[sos05]) ).
cnf(c_36,plain,
product(quotient(A,B),B) = A,
inference(clausify,[status(thm)],[sos04]) ).
cnf(c_37,plain,
quotient(product(A,B),B) = A,
inference(clausify,[status(thm)],[sos03]) ).
cnf(c_38,plain,
product(A,difference(A,B)) = B,
inference(clausify,[status(thm)],[sos02]) ).
cnf(c_39,plain,
difference(A,product(A,B)) = B,
inference(clausify,[status(thm)],[sos01]) ).
cnf(c_40,negated_conjecture,
product(product(b1,b),product(b,b2)) != product(b1,b2),
inference(resolve,[status(thm)],[c_31,c_30]) ).
cnf(c_65,plain,
product(product(product(b,c1),b),product(b,product(b,a))) = b,
inference(paramod,[status(thm)],[c_25,c_33]) ).
cnf(c_22192,plain,
product(product(a1,b2),product(A,B)) = product(product(b2,A),product(c1,B)),
inference(paramod,[status(thm)],[c_21,c_35]) ).
cnf(c_83,plain,
product(product(b2,A),product(c1,B)) = product(product(a1,b2),product(A,B)),
inference(copy,[status(thm)],[c_22192]) ).
cnf(c_22193,plain,
product(product(b,c1),product(A,B)) = product(product(a,A),product(b,B)),
inference(paramod,[status(thm)],[c_25,c_35]) ).
cnf(c_87,plain,
product(product(a,A),product(b,B)) = product(product(b,c1),product(A,B)),
inference(copy,[status(thm)],[c_22193]) ).
cnf(c_22194,plain,
product(product(A,B),product(b,c1)) = product(product(A,a),product(B,b)),
inference(paramod,[status(thm)],[c_25,c_35]) ).
cnf(c_88,plain,
product(product(A,a),product(B,b)) = product(product(A,B),product(b,c1)),
inference(copy,[status(thm)],[c_22194]) ).
cnf(c_22195,plain,
product(product(b1,c),product(A,B)) = product(product(a,A),product(b1,B)),
inference(paramod,[status(thm)],[c_27,c_35]) ).
cnf(c_89,plain,
product(product(a,A),product(b1,B)) = product(product(b1,c),product(A,B)),
inference(copy,[status(thm)],[c_22195]) ).
cnf(c_22196,plain,
product(A,product(B,C)) = product(product(A,B),product(A,C)),
inference(paramod,[status(thm)],[c_34,c_35]) ).
cnf(c_102,plain,
product(product(A,B),product(A,C)) = product(A,product(B,C)),
inference(copy,[status(thm)],[c_22196]) ).
cnf(c_22197,plain,
product(product(A,B),C) = product(product(A,C),product(B,C)),
inference(paramod,[status(thm)],[c_34,c_35]) ).
cnf(c_103,plain,
product(product(A,B),product(C,B)) = product(product(A,C),B),
inference(copy,[status(thm)],[c_22197]) ).
cnf(c_114,plain,
product(product(A,B),product(B,product(B,quotient(A,B)))) = B,
inference(paramod,[status(thm)],[c_36,c_33]) ).
cnf(c_22198,plain,
product(product(A,B),C) = product(product(A,quotient(C,D)),product(B,D)),
inference(paramod,[status(thm)],[c_36,c_35]) ).
cnf(c_117,plain,
product(product(A,quotient(B,C)),product(D,C)) = product(product(A,D),B),
inference(copy,[status(thm)],[c_22198]) ).
cnf(c_119,plain,
quotient(product(a1,b2),c1) = b2,
inference(paramod,[status(thm)],[c_21,c_37]) ).
cnf(c_122,plain,
quotient(product(b1,c),b1) = a,
inference(paramod,[status(thm)],[c_27,c_37]) ).
cnf(c_123,plain,
quotient(product(b,c),b) = a1,
inference(paramod,[status(thm)],[c_29,c_37]) ).
cnf(c_124,plain,
quotient(A,product(A,product(A,B))) = product(product(B,A),A),
inference(paramod,[status(thm)],[c_33,c_37]) ).
cnf(c_22199,plain,
product(A,product(B,C)) = product(product(D,B),product(difference(D,A),C)),
inference(paramod,[status(thm)],[c_38,c_35]) ).
cnf(c_132,plain,
product(product(A,B),product(difference(A,C),D)) = product(C,product(B,D)),
inference(copy,[status(thm)],[c_22199]) ).
cnf(c_134,plain,
quotient(A,difference(B,A)) = B,
inference(paramod,[status(thm)],[c_38,c_37]) ).
cnf(c_142,plain,
difference(A,A) = A,
inference(paramod,[status(thm)],[c_34,c_39]) ).
cnf(c_144,plain,
difference(quotient(A,B),A) = B,
inference(paramod,[status(thm)],[c_36,c_39]) ).
cnf(c_476,plain,
product(product(a1,b2),product(b2,A)) = product(b2,product(c1,A)),
inference(paramod,[status(thm)],[c_21,c_102]) ).
cnf(c_22200,plain,
product(product(a,A),product(b,c1)) = product(a,product(A,b)),
inference(paramod,[status(thm)],[c_25,c_102]) ).
cnf(c_481,plain,
product(product(b,c1),product(A,c1)) = product(a,product(A,b)),
inference(paramod,[status(thm)],[c_87,c_22200]) ).
cnf(c_22201,plain,
product(product(a,A),product(b1,c)) = product(a,product(A,b1)),
inference(paramod,[status(thm)],[c_27,c_102]) ).
cnf(c_483,plain,
product(product(b1,c),product(A,c)) = product(a,product(A,b1)),
inference(paramod,[status(thm)],[c_89,c_22201]) ).
cnf(c_492,plain,
product(product(A,B),A) = product(A,product(B,A)),
inference(paramod,[status(thm)],[c_34,c_102]) ).
cnf(c_22202,plain,
product(product(product(product(b,c1),b),b),product(product(product(b,c1),b),product(b,a))) = b,
inference(paramod,[status(thm)],[c_65,c_102]) ).
cnf(c_22203,plain,
product(product(product(b,product(c1,b)),b),product(product(product(b,c1),b),product(b,a))) = b,
inference(paramod,[status(thm)],[c_492,c_22202]) ).
cnf(c_22204,plain,
product(product(b,product(product(c1,b),b)),product(product(product(b,c1),b),product(b,a))) = b,
inference(paramod,[status(thm)],[c_492,c_22203]) ).
cnf(c_22205,plain,
product(product(b,product(product(c1,b),b)),product(product(b,product(c1,b)),product(b,a))) = b,
inference(paramod,[status(thm)],[c_492,c_22204]) ).
cnf(c_22206,plain,
product(product(b,product(product(c1,b),b)),product(b,product(product(c1,b),a))) = b,
inference(paramod,[status(thm)],[c_102,c_22205]) ).
cnf(c_22207,plain,
product(b,product(product(product(c1,b),b),product(product(c1,b),a))) = b,
inference(paramod,[status(thm)],[c_102,c_22206]) ).
cnf(c_521,plain,
product(b,product(product(c1,b),product(b,a))) = b,
inference(paramod,[status(thm)],[c_102,c_22207]) ).
cnf(c_630,plain,
product(product(a1,b2),b2) = product(b2,product(c1,b2)),
inference(paramod,[status(thm)],[c_21,c_492]) ).
cnf(c_633,plain,
product(product(b1,c),a) = product(a,product(b1,a)),
inference(paramod,[status(thm)],[c_27,c_492]) ).
cnf(c_642,plain,
quotient(product(A,product(B,A)),A) = product(A,B),
inference(paramod,[status(thm)],[c_492,c_37]) ).
cnf(c_22208,plain,
difference(b,b) = product(product(c1,b),product(b,a)),
inference(paramod,[status(thm)],[c_521,c_39]) ).
cnf(c_22209,plain,
b = product(product(c1,b),product(b,a)),
inference(paramod,[status(thm)],[c_142,c_22208]) ).
cnf(c_847,plain,
product(product(c1,b),product(b,a)) = b,
inference(copy,[status(thm)],[c_22209]) ).
cnf(c_22210,plain,
product(product(b2,product(c1,b2)),product(b2,product(b2,a1))) = b2,
inference(paramod,[status(thm)],[c_630,c_33]) ).
cnf(c_1280,plain,
product(b2,product(product(c1,b2),product(b2,a1))) = b2,
inference(paramod,[status(thm)],[c_102,c_22210]) ).
cnf(c_1446,plain,
quotient(product(A,B),A) = product(A,quotient(B,A)),
inference(paramod,[status(thm)],[c_36,c_642]) ).
cnf(c_1479,plain,
product(b,quotient(c,b)) = a1,
inference(paramod,[status(thm)],[c_1446,c_123]) ).
cnf(c_1480,plain,
product(b1,quotient(c,b1)) = a,
inference(paramod,[status(thm)],[c_1446,c_122]) ).
cnf(c_22211,plain,
difference(b,a1) = quotient(c,b),
inference(paramod,[status(thm)],[c_1479,c_39]) ).
cnf(c_1496,plain,
quotient(c,b) = difference(b,a1),
inference(copy,[status(thm)],[c_22211]) ).
cnf(c_22212,plain,
difference(b1,a) = quotient(c,b1),
inference(paramod,[status(thm)],[c_1480,c_39]) ).
cnf(c_1678,plain,
quotient(c,b1) = difference(b1,a),
inference(copy,[status(thm)],[c_22212]) ).
cnf(c_1756,plain,
product(difference(b,a1),b) = c,
inference(paramod,[status(thm)],[c_1496,c_36]) ).
cnf(c_1758,plain,
product(difference(b1,a),b1) = c,
inference(paramod,[status(thm)],[c_1678,c_36]) ).
cnf(c_2095,plain,
product(product(b,a),product(c1,b)) = product(b,c1),
inference(paramod,[status(thm)],[c_88,c_34]) ).
cnf(c_22213,plain,
difference(b2,b2) = product(product(c1,b2),product(b2,a1)),
inference(paramod,[status(thm)],[c_1280,c_39]) ).
cnf(c_22214,plain,
b2 = product(product(c1,b2),product(b2,a1)),
inference(paramod,[status(thm)],[c_142,c_22213]) ).
cnf(c_2360,plain,
product(product(c1,b2),product(b2,a1)) = b2,
inference(copy,[status(thm)],[c_22214]) ).
cnf(c_22215,plain,
product(product(product(b2,a1),product(c1,b2)),product(b2,a1)) = product(product(b2,a1),b2),
inference(paramod,[status(thm)],[c_2360,c_492]) ).
cnf(c_22216,plain,
product(product(product(a1,b2),product(a1,b2)),product(b2,a1)) = product(product(b2,a1),b2),
inference(paramod,[status(thm)],[c_83,c_22215]) ).
cnf(c_22217,plain,
product(product(a1,b2),product(b2,a1)) = product(product(b2,a1),b2),
inference(paramod,[status(thm)],[c_34,c_22216]) ).
cnf(c_22218,plain,
product(b2,product(c1,a1)) = product(product(b2,a1),b2),
inference(paramod,[status(thm)],[c_476,c_22217]) ).
cnf(c_2382,plain,
product(b2,product(c1,a1)) = product(b2,product(a1,b2)),
inference(paramod,[status(thm)],[c_492,c_22218]) ).
cnf(c_2641,plain,
quotient(product(b,c1),a) = product(a,quotient(b,a)),
inference(paramod,[status(thm)],[c_25,c_1446]) ).
cnf(c_22219,plain,
quotient(A,B) = product(B,quotient(difference(B,A),B)),
inference(paramod,[status(thm)],[c_38,c_1446]) ).
cnf(c_2647,plain,
product(A,quotient(difference(A,B),A)) = quotient(B,A),
inference(copy,[status(thm)],[c_22219]) ).
cnf(c_2648,plain,
difference(product(A,quotient(B,A)),product(A,B)) = A,
inference(paramod,[status(thm)],[c_1446,c_144]) ).
cnf(c_22220,plain,
product(product(b,c1),product(b,a)) = product(product(b,a),product(product(c1,b),product(b,a))),
inference(paramod,[status(thm)],[c_2095,c_492]) ).
cnf(c_22221,plain,
product(b,product(c1,a)) = product(product(b,a),product(product(c1,b),product(b,a))),
inference(paramod,[status(thm)],[c_102,c_22220]) ).
cnf(c_22222,plain,
product(b,product(c1,a)) = product(product(b,a),b),
inference(paramod,[status(thm)],[c_847,c_22221]) ).
cnf(c_22223,plain,
product(b,product(c1,a)) = product(b,product(a,b)),
inference(paramod,[status(thm)],[c_492,c_22222]) ).
cnf(c_4229,plain,
product(b,product(c1,a)) = product(b,product(b,c1)),
inference(paramod,[status(thm)],[c_25,c_22223]) ).
cnf(c_6231,plain,
product(product(A,product(B,C)),product(D,product(B,C))) = product(product(A,B),product(D,C)),
inference(paramod,[status(thm)],[c_103,c_35]) ).
cnf(c_22224,plain,
product(product(a,A),product(b,c1)) = product(product(b,A),c1),
inference(paramod,[status(thm)],[c_103,c_87]) ).
cnf(c_22225,plain,
product(product(b,c1),product(A,c1)) = product(product(b,A),c1),
inference(paramod,[status(thm)],[c_87,c_22224]) ).
cnf(c_22226,plain,
product(a,product(A,b)) = product(product(b,A),c1),
inference(paramod,[status(thm)],[c_481,c_22225]) ).
cnf(c_6413,plain,
product(product(b,A),c1) = product(a,product(A,b)),
inference(copy,[status(thm)],[c_22226]) ).
cnf(c_22227,plain,
product(product(a,A),product(b1,c)) = product(product(b1,A),c),
inference(paramod,[status(thm)],[c_103,c_89]) ).
cnf(c_22228,plain,
product(product(b1,c),product(A,c)) = product(product(b1,A),c),
inference(paramod,[status(thm)],[c_89,c_22227]) ).
cnf(c_22229,plain,
product(a,product(A,b1)) = product(product(b1,A),c),
inference(paramod,[status(thm)],[c_483,c_22228]) ).
cnf(c_6436,plain,
product(product(b1,A),c) = product(a,product(A,b1)),
inference(copy,[status(thm)],[c_22229]) ).
cnf(c_22230,plain,
difference(b2,product(b2,product(a1,b2))) = product(c1,a1),
inference(paramod,[status(thm)],[c_2382,c_39]) ).
cnf(c_22231,plain,
product(a1,b2) = product(c1,a1),
inference(paramod,[status(thm)],[c_39,c_22230]) ).
cnf(c_8410,plain,
product(c1,a1) = product(a1,b2),
inference(copy,[status(thm)],[c_22231]) ).
cnf(c_22232,plain,
quotient(product(a1,b2),a1) = c1,
inference(paramod,[status(thm)],[c_8410,c_37]) ).
cnf(c_8455,plain,
product(a1,quotient(b2,a1)) = c1,
inference(paramod,[status(thm)],[c_1446,c_22232]) ).
cnf(c_22233,plain,
quotient(product(a1,b2),c1) = product(c1,quotient(a1,c1)),
inference(paramod,[status(thm)],[c_8410,c_1446]) ).
cnf(c_22234,plain,
b2 = product(c1,quotient(a1,c1)),
inference(paramod,[status(thm)],[c_119,c_22233]) ).
cnf(c_8476,plain,
product(c1,quotient(a1,c1)) = b2,
inference(copy,[status(thm)],[c_22234]) ).
cnf(c_22235,plain,
difference(a1,c1) = quotient(b2,a1),
inference(paramod,[status(thm)],[c_8455,c_39]) ).
cnf(c_8543,plain,
quotient(b2,a1) = difference(a1,c1),
inference(copy,[status(thm)],[c_22235]) ).
cnf(c_22236,plain,
difference(c1,b2) = quotient(a1,c1),
inference(paramod,[status(thm)],[c_8476,c_39]) ).
cnf(c_8556,plain,
quotient(a1,c1) = difference(c1,b2),
inference(copy,[status(thm)],[c_22236]) ).
cnf(c_8563,plain,
product(difference(a1,c1),a1) = b2,
inference(paramod,[status(thm)],[c_8543,c_36]) ).
cnf(c_8568,plain,
product(difference(c1,b2),c1) = a1,
inference(paramod,[status(thm)],[c_8556,c_36]) ).
cnf(c_22237,plain,
difference(A,quotient(B,A)) = quotient(difference(A,B),A),
inference(paramod,[status(thm)],[c_2647,c_39]) ).
cnf(c_8774,plain,
quotient(difference(A,B),A) = difference(A,quotient(B,A)),
inference(copy,[status(thm)],[c_22237]) ).
cnf(c_22238,plain,
product(c,product(b1,product(b1,quotient(difference(b1,a),b1)))) = b1,
inference(paramod,[status(thm)],[c_1758,c_114]) ).
cnf(c_22239,plain,
product(c,product(b1,product(b1,difference(b1,quotient(a,b1))))) = b1,
inference(paramod,[status(thm)],[c_8774,c_22238]) ).
cnf(c_9455,plain,
product(c,product(b1,quotient(a,b1))) = b1,
inference(paramod,[status(thm)],[c_38,c_22239]) ).
cnf(c_22240,plain,
product(a1,product(c1,product(c1,quotient(difference(c1,b2),c1)))) = c1,
inference(paramod,[status(thm)],[c_8568,c_114]) ).
cnf(c_22241,plain,
product(a1,product(c1,product(c1,difference(c1,quotient(b2,c1))))) = c1,
inference(paramod,[status(thm)],[c_8774,c_22240]) ).
cnf(c_9490,plain,
product(a1,product(c1,quotient(b2,c1))) = c1,
inference(paramod,[status(thm)],[c_38,c_22241]) ).
cnf(c_22242,plain,
difference(c,b1) = product(b1,quotient(a,b1)),
inference(paramod,[status(thm)],[c_9455,c_39]) ).
cnf(c_10033,plain,
product(b1,quotient(a,b1)) = difference(c,b1),
inference(copy,[status(thm)],[c_22242]) ).
cnf(c_10082,plain,
product(product(b1,quotient(product(b,b2),A)),product(b,A)) != product(b1,b2),
inference(paramod,[status(thm)],[c_117,c_40]) ).
cnf(c_10708,plain,
quotient(A,product(A,B)) = product(product(difference(A,B),A),A),
inference(paramod,[status(thm)],[c_38,c_124]) ).
cnf(c_22243,plain,
difference(a1,c1) = product(c1,quotient(b2,c1)),
inference(paramod,[status(thm)],[c_9490,c_39]) ).
cnf(c_10854,plain,
product(c1,quotient(b2,c1)) = difference(a1,c1),
inference(copy,[status(thm)],[c_22243]) ).
cnf(c_22244,plain,
difference(b1,difference(c,b1)) = quotient(a,b1),
inference(paramod,[status(thm)],[c_10033,c_39]) ).
cnf(c_11260,plain,
quotient(a,b1) = difference(b1,difference(c,b1)),
inference(copy,[status(thm)],[c_22244]) ).
cnf(c_11269,plain,
difference(difference(c,b1),product(b1,a)) = b1,
inference(paramod,[status(thm)],[c_10033,c_2648]) ).
cnf(c_22245,plain,
difference(c1,difference(a1,c1)) = quotient(b2,c1),
inference(paramod,[status(thm)],[c_10854,c_39]) ).
cnf(c_11669,plain,
quotient(b2,c1) = difference(c1,difference(a1,c1)),
inference(copy,[status(thm)],[c_22245]) ).
cnf(c_12199,plain,
product(product(A,difference(a1,c1)),product(difference(A,B),a1)) = product(B,b2),
inference(paramod,[status(thm)],[c_8563,c_132]) ).
cnf(c_12418,plain,
product(difference(b1,difference(c,b1)),b1) = a,
inference(paramod,[status(thm)],[c_11260,c_36]) ).
cnf(c_12425,plain,
product(difference(c,b1),b1) = product(b1,a),
inference(paramod,[status(thm)],[c_11269,c_38]) ).
cnf(c_13251,plain,
product(difference(c1,difference(a1,c1)),c1) = b2,
inference(paramod,[status(thm)],[c_11669,c_36]) ).
cnf(c_22246,plain,
quotient(product(b1,a),difference(c,b1)) = product(difference(c,b1),quotient(b1,difference(c,b1))),
inference(paramod,[status(thm)],[c_12425,c_1446]) ).
cnf(c_13498,plain,
quotient(product(b1,a),difference(c,b1)) = product(difference(c,b1),c),
inference(paramod,[status(thm)],[c_134,c_22246]) ).
cnf(c_22247,plain,
difference(product(difference(c,b1),quotient(b1,difference(c,b1))),product(b1,a)) = difference(c,b1),
inference(paramod,[status(thm)],[c_12425,c_2648]) ).
cnf(c_13513,plain,
difference(product(difference(c,b1),c),product(b1,a)) = difference(c,b1),
inference(paramod,[status(thm)],[c_134,c_22247]) ).
cnf(c_22248,plain,
difference(b,product(b,product(b,c1))) = product(c1,a),
inference(paramod,[status(thm)],[c_4229,c_39]) ).
cnf(c_22249,plain,
product(b,c1) = product(c1,a),
inference(paramod,[status(thm)],[c_39,c_22248]) ).
cnf(c_15817,plain,
product(c1,a) = product(b,c1),
inference(copy,[status(thm)],[c_22249]) ).
cnf(c_22250,plain,
quotient(product(b,c1),a) = c1,
inference(paramod,[status(thm)],[c_15817,c_37]) ).
cnf(c_15887,plain,
product(a,quotient(b,a)) = c1,
inference(paramod,[status(thm)],[c_2641,c_22250]) ).
cnf(c_22251,plain,
quotient(product(b,c1),c1) = product(c1,quotient(a,c1)),
inference(paramod,[status(thm)],[c_15817,c_1446]) ).
cnf(c_22252,plain,
b = product(c1,quotient(a,c1)),
inference(paramod,[status(thm)],[c_37,c_22251]) ).
cnf(c_15907,plain,
product(c1,quotient(a,c1)) = b,
inference(copy,[status(thm)],[c_22252]) ).
cnf(c_22253,plain,
product(product(b,c1),product(A,a)) = product(product(c1,A),a),
inference(paramod,[status(thm)],[c_15817,c_103]) ).
cnf(c_15914,plain,
product(product(c1,A),a) = product(product(b,c1),product(A,a)),
inference(copy,[status(thm)],[c_22253]) ).
cnf(c_22254,plain,
difference(a,c1) = quotient(b,a),
inference(paramod,[status(thm)],[c_15887,c_39]) ).
cnf(c_15986,plain,
quotient(b,a) = difference(a,c1),
inference(copy,[status(thm)],[c_22254]) ).
cnf(c_22255,plain,
product(b,product(A,c1)) = product(product(c1,A),a),
inference(paramod,[status(thm)],[c_15907,c_117]) ).
cnf(c_22256,plain,
product(b,product(A,c1)) = product(product(b,c1),product(A,a)),
inference(paramod,[status(thm)],[c_15914,c_22255]) ).
cnf(c_16034,plain,
product(product(b,c1),product(A,a)) = product(b,product(A,c1)),
inference(copy,[status(thm)],[c_22256]) ).
cnf(c_16036,plain,
product(product(c1,A),a) = product(b,product(A,c1)),
inference(paramod,[status(thm)],[c_16034,c_15914]) ).
cnf(c_16038,plain,
product(difference(a,c1),a) = b,
inference(paramod,[status(thm)],[c_15986,c_36]) ).
cnf(c_22257,plain,
product(product(b,difference(b,a1)),c1) = product(a,c),
inference(paramod,[status(thm)],[c_1756,c_6413]) ).
cnf(c_22258,plain,
product(a1,c1) = product(a,c),
inference(paramod,[status(thm)],[c_38,c_22257]) ).
cnf(c_17438,plain,
product(a,c) = product(a1,c1),
inference(copy,[status(thm)],[c_22258]) ).
cnf(c_17537,plain,
product(product(product(c,a),a),product(a,product(a1,c1))) = a,
inference(paramod,[status(thm)],[c_17438,c_33]) ).
cnf(c_22259,plain,
product(product(b1,difference(b1,difference(c,b1))),c) = product(a,a),
inference(paramod,[status(thm)],[c_12418,c_6436]) ).
cnf(c_22260,plain,
product(difference(c,b1),c) = product(a,a),
inference(paramod,[status(thm)],[c_38,c_22259]) ).
cnf(c_18202,plain,
product(difference(c,b1),c) = a,
inference(paramod,[status(thm)],[c_34,c_22260]) ).
cnf(c_22261,plain,
difference(a,product(b1,a)) = difference(c,b1),
inference(paramod,[status(thm)],[c_18202,c_13513]) ).
cnf(c_18207,plain,
difference(c,b1) = difference(a,product(b1,a)),
inference(copy,[status(thm)],[c_22261]) ).
cnf(c_22262,plain,
quotient(product(b1,a),difference(a,product(b1,a))) = product(difference(c,b1),c),
inference(paramod,[status(thm)],[c_18207,c_13498]) ).
cnf(c_22263,plain,
a = product(difference(c,b1),c),
inference(paramod,[status(thm)],[c_134,c_22262]) ).
cnf(c_22264,plain,
a = product(difference(a,product(b1,a)),c),
inference(paramod,[status(thm)],[c_18207,c_22263]) ).
cnf(c_18208,plain,
product(difference(a,product(b1,a)),c) = a,
inference(copy,[status(thm)],[c_22264]) ).
cnf(c_18387,plain,
product(c,difference(a,product(b1,a))) = b1,
inference(paramod,[status(thm)],[c_18207,c_38]) ).
cnf(c_22265,plain,
product(product(c,difference(a,product(b1,a))),c) = product(c,a),
inference(paramod,[status(thm)],[c_18208,c_492]) ).
cnf(c_22266,plain,
product(b1,c) = product(c,a),
inference(paramod,[status(thm)],[c_18387,c_22265]) ).
cnf(c_18411,plain,
product(c,a) = product(b1,c),
inference(copy,[status(thm)],[c_22266]) ).
cnf(c_22267,plain,
product(product(a,difference(a,product(b1,a))),product(b1,c)) = product(product(b1,c),a),
inference(paramod,[status(thm)],[c_18208,c_89]) ).
cnf(c_22268,plain,
product(product(b1,a),product(b1,c)) = product(product(b1,c),a),
inference(paramod,[status(thm)],[c_38,c_22267]) ).
cnf(c_22269,plain,
product(b1,product(a,c)) = product(product(b1,c),a),
inference(paramod,[status(thm)],[c_102,c_22268]) ).
cnf(c_22270,plain,
product(b1,product(a1,c1)) = product(product(b1,c),a),
inference(paramod,[status(thm)],[c_17438,c_22269]) ).
cnf(c_22271,plain,
product(b1,product(a1,c1)) = product(a,product(b1,a)),
inference(paramod,[status(thm)],[c_633,c_22270]) ).
cnf(c_18415,plain,
product(a,product(b1,a)) = product(b1,product(a1,c1)),
inference(copy,[status(thm)],[c_22271]) ).
cnf(c_22272,plain,
product(product(product(b1,c),a),product(a,product(a1,c1))) = a,
inference(paramod,[status(thm)],[c_18411,c_17537]) ).
cnf(c_22273,plain,
product(product(a,product(b1,a)),product(a,product(a1,c1))) = a,
inference(paramod,[status(thm)],[c_633,c_22272]) ).
cnf(c_22274,plain,
product(product(b1,product(a1,c1)),product(a,product(a1,c1))) = a,
inference(paramod,[status(thm)],[c_18415,c_22273]) ).
cnf(c_18446,plain,
product(product(b1,a1),product(a,c1)) = a,
inference(paramod,[status(thm)],[c_6231,c_22274]) ).
cnf(c_22275,plain,
quotient(a,product(a,c1)) = product(b1,a1),
inference(paramod,[status(thm)],[c_18446,c_37]) ).
cnf(c_22276,plain,
product(product(difference(a,c1),a),a) = product(b1,a1),
inference(paramod,[status(thm)],[c_10708,c_22275]) ).
cnf(c_18832,plain,
product(b,a) = product(b1,a1),
inference(paramod,[status(thm)],[c_16038,c_22276]) ).
cnf(c_22277,plain,
product(product(b1,quotient(product(b,b2),a)),product(b1,a1)) != product(b1,b2),
inference(paramod,[status(thm)],[c_18832,c_10082]) ).
cnf(c_19140,plain,
product(b1,product(quotient(product(b,b2),a),a1)) != product(b1,b2),
inference(paramod,[status(thm)],[c_102,c_22277]) ).
cnf(c_19250,plain,
product(product(A,quotient(product(b,b2),a)),product(difference(A,b1),a1)) != product(b1,b2),
inference(paramod,[status(thm)],[c_132,c_19140]) ).
cnf(c_22278,plain,
product(product(c1,difference(c1,difference(a1,c1))),a) = product(b,b2),
inference(paramod,[status(thm)],[c_13251,c_16036]) ).
cnf(c_22017,plain,
product(difference(a1,c1),a) = product(b,b2),
inference(paramod,[status(thm)],[c_38,c_22278]) ).
cnf(c_22150,plain,
quotient(product(b,b2),a) = difference(a1,c1),
inference(paramod,[status(thm)],[c_22017,c_37]) ).
cnf(c_22279,plain,
product(product(A,difference(a1,c1)),product(difference(A,b1),a1)) != product(b1,b2),
inference(paramod,[status(thm)],[c_22150,c_19250]) ).
cnf(c_22280,plain,
product(b1,b2) != product(b1,b2),
inference(paramod,[status(thm)],[c_12199,c_22279]) ).
cnf(c_22191,plain,
$false,
inference(copy,[status(thm)],[c_22280]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP778+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n007.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:44:38 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 1400375 was started by sandbox2 on n007,
% 0.10/0.37 % Fri Sep 25 15:44:38 2026
% 0.10/0.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.10/0.38
% 0.10/0.38 % From the command line: assign(max_seconds, 300).
% 56.55/8.51
% 56.55/8.51 % given #500 (F,wt=17): 13247 product(b1,product(product(b,b2),product(quotient(difference(b1,b),b),b2))) != product(b1,b2). [para(103(a,2),13233(a,1,2))].
% 56.55/8.51
% 56.55/8.51 % given #1000 (T,wt=9): 21042 difference(difference(b1,a1),product(c1,c2)) = b2. [para(20884(a,1),39(a,1,2))].
% 56.55/8.51
% 56.55/8.51 % SZS status Theorem for theBenchmark
% 56.55/8.51
% 56.55/8.51 % Proof 1 at 7.15 (+ 0.77) seconds.
% 56.55/8.51 % Length of proof is 122.
% 56.55/8.51 % Level of proof is 21.
% 56.55/8.51 % Maximum clause weight is 19.000.
% 56.55/8.51 % Given clauses 1134.
% 56.55/8.51
% 56.55/8.51 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------