%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : GRP780+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:26 AM UTC 2026
% Result : Theorem 5.49s 1.14s
% Output : CNFRefutation 5.49s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 13
% Syntax : Number of formulae : 139 ( 136 unt; 0 def)
% Number of atoms : 142 ( 113 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 29 ( 26 ~; 2 |; 0 &)
% ( 1 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 1 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-3 aty)
% Number of functors : 13 ( 13 usr; 9 con; 0-3 aty)
% Number of variables : 171 ( 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,
! [C,B,A] : bigC(A,B,C) = product(product(A,B),product(C,A)),
file('theBenchmark.p',sos09) ).
fof(goals,conjecture,
d(bigC(a1,b3,c2),bigC(a2,b1,c3),bigC(a3,b2,c1)),
file('theBenchmark.p',goals) ).
fof(goals_neg,negated_conjecture,
~ d(bigC(a1,b3,c2),bigC(a2,b1,c3),bigC(a3,b2,c1)),
inference(assume_negation,[status(cth)],[goals]) ).
cnf(c_11,plain,
difference(A,product(A,B)) = B,
inference(clausify,[status(thm)],[sos01]) ).
cnf(c_12,plain,
product(A,difference(A,B)) = B,
inference(clausify,[status(thm)],[sos02]) ).
cnf(c_13,plain,
quotient(product(A,B),B) = A,
inference(clausify,[status(thm)],[sos03]) ).
cnf(c_14,plain,
product(quotient(A,B),B) = A,
inference(clausify,[status(thm)],[sos04]) ).
cnf(c_15,plain,
product(product(A,B),product(C,D)) = product(product(A,C),product(B,D)),
inference(clausify,[status(thm)],[sos05]) ).
cnf(c_16,plain,
product(A,A) = A,
inference(clausify,[status(thm)],[sos06]) ).
cnf(c_17,plain,
product(product(product(A,B),B),product(B,product(B,A))) = B,
inference(clausify,[status(thm)],[sos07]) ).
cnf(c_18,plain,
( product(B,C) = product(A,B)
| ~ d(A,B,C) ),
inference(clausify,[status(thm)],[sos08]) ).
cnf(c_19,plain,
( product(B,C) != product(A,B)
| d(A,B,C) ),
inference(clausify,[status(thm)],[sos08]) ).
cnf(c_20,plain,
bigC(A,B,C) = product(product(A,B),product(C,A)),
inference(clausify,[status(thm)],[sos09]) ).
fof(sos10,axiom,
d(a1,a2,a3),
file('theBenchmark.p',sos10) ).
cnf(c_21,plain,
d(a1,a2,a3),
inference(clausify,[status(thm)],[sos10]) ).
fof(sos11,axiom,
d(b1,b2,b3),
file('theBenchmark.p',sos11) ).
cnf(c_22,plain,
d(b1,b2,b3),
inference(clausify,[status(thm)],[sos11]) ).
fof(sos12,axiom,
d(c1,c2,c3),
file('theBenchmark.p',sos12) ).
cnf(c_23,plain,
d(c1,c2,c3),
inference(clausify,[status(thm)],[sos12]) ).
cnf(c_24,negated_conjecture,
~ d(bigC(a1,b3,c2),bigC(a2,b1,c3),bigC(a3,b2,c1)),
inference(clausify,[status(thm)],[goals_neg]) ).
cnf(c_4142,negated_conjecture,
~ d(product(product(a1,b3),product(c2,a1)),bigC(a2,b1,c3),bigC(a3,b2,c1)),
inference(paramod,[status(thm)],[c_20,c_24]) ).
cnf(c_4143,negated_conjecture,
~ d(product(product(a1,b3),product(c2,a1)),product(product(a2,b1),product(c3,a2)),bigC(a3,b2,c1)),
inference(paramod,[status(thm)],[c_20,c_4142]) ).
cnf(c_25,negated_conjecture,
~ d(product(product(a1,b3),product(c2,a1)),product(product(a2,b1),product(c3,a2)),product(product(a3,b2),product(c1,a3))),
inference(paramod,[status(thm)],[c_20,c_4143]) ).
cnf(c_28,plain,
difference(product(A,B),product(product(A,C),product(B,D))) = product(C,D),
inference(paramod,[status(thm)],[c_15,c_11]) ).
cnf(c_4144,plain,
product(A,product(B,C)) = product(product(D,B),product(difference(D,A),C)),
inference(paramod,[status(thm)],[c_12,c_15]) ).
cnf(c_29,plain,
product(product(A,B),product(difference(A,C),D)) = product(C,product(B,D)),
inference(copy,[status(thm)],[c_4144]) ).
cnf(c_34,plain,
product(product(product(A,B),product(C,D)),product(E,F)) = product(product(product(A,C),E),product(product(B,D),F)),
inference(paramod,[status(thm)],[c_15,c_15]) ).
cnf(c_4145,plain,
product(product(A,B),product(product(C,D),product(E,F))) = product(product(A,product(C,E)),product(B,product(D,F))),
inference(paramod,[status(thm)],[c_15,c_15]) ).
cnf(c_35,plain,
product(product(A,product(B,C)),product(D,product(E,F))) = product(product(A,D),product(product(B,E),product(C,F))),
inference(copy,[status(thm)],[c_4145]) ).
cnf(c_37,plain,
quotient(A,A) = A,
inference(paramod,[status(thm)],[c_16,c_13]) ).
cnf(c_4146,plain,
product(A,product(B,C)) = product(product(A,B),product(A,C)),
inference(paramod,[status(thm)],[c_16,c_15]) ).
cnf(c_38,plain,
product(product(A,B),product(A,C)) = product(A,product(B,C)),
inference(copy,[status(thm)],[c_4146]) ).
cnf(c_4147,plain,
product(product(A,B),C) = product(product(A,C),product(B,C)),
inference(paramod,[status(thm)],[c_16,c_15]) ).
cnf(c_39,plain,
product(product(A,B),product(C,B)) = product(product(A,C),B),
inference(copy,[status(thm)],[c_4147]) ).
cnf(c_4148,plain,
d(product(A,B),product(A,A),product(B,A)),
inference(resolve,[status(thm)],[c_19,c_15]) ).
cnf(c_54,plain,
d(product(A,B),A,product(B,A)),
inference(paramod,[status(thm)],[c_16,c_4148]) ).
cnf(c_60,plain,
product(a2,a3) = product(a1,a2),
inference(resolve,[status(thm)],[c_18,c_21]) ).
cnf(c_61,plain,
product(b2,b3) = product(b1,b2),
inference(resolve,[status(thm)],[c_18,c_22]) ).
cnf(c_62,plain,
product(c2,c3) = product(c1,c2),
inference(resolve,[status(thm)],[c_18,c_23]) ).
cnf(c_63,negated_conjecture,
product(product(product(a2,b1),product(c3,a2)),product(product(a3,b2),product(c1,a3))) != product(product(product(a1,b3),product(c2,a1)),product(product(a2,b1),product(c3,a2))),
inference(resolve,[status(thm)],[c_19,c_25]) ).
cnf(c_4149,plain,
product(product(A,B),product(a1,a2)) = product(product(A,a2),product(B,a3)),
inference(paramod,[status(thm)],[c_60,c_15]) ).
cnf(c_78,plain,
product(product(A,a2),product(B,a3)) = product(product(A,B),product(a1,a2)),
inference(copy,[status(thm)],[c_4149]) ).
cnf(c_99,plain,
product(product(product(a2,b1),product(c3,a2)),product(product(a3,b2),product(c1,a3))) != product(product(product(a1,b3),product(a2,b1)),product(product(c2,a1),product(c3,a2))),
inference(paramod,[status(thm)],[c_15,c_63]) ).
cnf(c_4150,plain,
product(A,product(B,A)) = product(product(A,B),A),
inference(resolve,[status(thm)],[c_18,c_54]) ).
cnf(c_100,plain,
product(product(A,B),A) = product(A,product(B,A)),
inference(copy,[status(thm)],[c_4150]) ).
cnf(c_108,plain,
d(product(product(A,product(A,B)),product(product(B,A),A)),product(A,product(A,B)),A),
inference(paramod,[status(thm)],[c_17,c_54]) ).
cnf(c_109,plain,
d(product(a1,a2),a2,product(a3,a2)),
inference(paramod,[status(thm)],[c_60,c_54]) ).
cnf(c_4151,plain,
product(a2,product(a3,a2)) = product(product(a1,a2),a2),
inference(resolve,[status(thm)],[c_18,c_109]) ).
cnf(c_115,plain,
product(product(a1,a2),a2) = product(a2,product(a3,a2)),
inference(copy,[status(thm)],[c_4151]) ).
cnf(c_118,plain,
difference(product(A,B),product(C,product(B,D))) = product(difference(A,C),D),
inference(paramod,[status(thm)],[c_12,c_28]) ).
cnf(c_144,plain,
product(A,product(difference(A,B),C)) = product(B,product(A,C)),
inference(paramod,[status(thm)],[c_16,c_29]) ).
cnf(c_228,plain,
quotient(product(A,product(B,A)),A) = product(A,B),
inference(paramod,[status(thm)],[c_100,c_13]) ).
cnf(c_4152,plain,
product(product(product(A,B),product(A,C)),product(product(C,D),product(B,D))) = product(product(A,C),product(B,D)),
inference(paramod,[status(thm)],[c_34,c_16]) ).
cnf(c_4153,plain,
product(product(A,product(B,C)),product(product(C,D),product(B,D))) = product(product(A,C),product(B,D)),
inference(paramod,[status(thm)],[c_38,c_4152]) ).
cnf(c_342,plain,
product(product(A,product(B,C)),product(product(C,B),D)) = product(product(A,C),product(B,D)),
inference(paramod,[status(thm)],[c_39,c_4153]) ).
cnf(c_4154,plain,
product(product(product(A,B),C),product(D,E)) = product(product(product(A,C),D),product(product(B,C),E)),
inference(paramod,[status(thm)],[c_16,c_34]) ).
cnf(c_344,plain,
product(product(product(A,B),C),product(product(D,B),E)) = product(product(product(A,D),B),product(C,E)),
inference(copy,[status(thm)],[c_4154]) ).
cnf(c_4155,plain,
product(product(product(a2,a3),product(b1,b2)),product(product(c3,a2),product(c1,a3))) != product(product(product(a1,b3),product(a2,b1)),product(product(c2,a1),product(c3,a2))),
inference(paramod,[status(thm)],[c_34,c_99]) ).
cnf(c_4156,plain,
product(product(product(a1,a2),product(b1,b2)),product(product(c3,a2),product(c1,a3))) != product(product(product(a1,b3),product(a2,b1)),product(product(c2,a1),product(c3,a2))),
inference(paramod,[status(thm)],[c_60,c_4155]) ).
cnf(c_4157,plain,
product(product(product(a1,c3),a2),product(product(b1,b2),product(c1,a3))) != product(product(product(a1,b3),product(a2,b1)),product(product(c2,a1),product(c3,a2))),
inference(paramod,[status(thm)],[c_344,c_4156]) ).
cnf(c_418,plain,
product(product(product(a1,b3),product(a2,b1)),product(product(c2,a1),product(c3,a2))) != product(product(product(a1,c3),a2),product(product(b1,b2),product(c1,a3))),
inference(copy,[status(thm)],[c_4157]) ).
cnf(c_4158,plain,
d(product(product(A,B),product(A,A)),product(A,product(A,B)),A),
inference(paramod,[status(thm)],[c_342,c_108]) ).
cnf(c_4159,plain,
d(product(product(A,B),A),product(A,product(A,B)),A),
inference(paramod,[status(thm)],[c_16,c_4158]) ).
cnf(c_495,plain,
d(product(A,product(B,A)),product(A,product(A,B)),A),
inference(paramod,[status(thm)],[c_100,c_4159]) ).
cnf(c_4160,plain,
d(product(A,product(difference(A,B),A)),product(A,B),A),
inference(paramod,[status(thm)],[c_12,c_495]) ).
cnf(c_4161,plain,
d(product(B,product(A,A)),product(A,B),A),
inference(paramod,[status(thm)],[c_144,c_4160]) ).
cnf(c_518,plain,
d(product(A,B),product(B,A),B),
inference(paramod,[status(thm)],[c_16,c_4161]) ).
cnf(c_561,plain,
d(product(a3,a2),product(a1,a2),a2),
inference(paramod,[status(thm)],[c_60,c_518]) ).
cnf(c_562,plain,
d(product(b1,b2),product(b3,b2),b3),
inference(paramod,[status(thm)],[c_61,c_518]) ).
cnf(c_564,plain,
d(product(c1,c2),product(c3,c2),c3),
inference(paramod,[status(thm)],[c_62,c_518]) ).
cnf(c_4162,plain,
product(product(a1,a2),a2) = product(product(a3,a2),product(a1,a2)),
inference(resolve,[status(thm)],[c_18,c_561]) ).
cnf(c_4163,plain,
product(a2,product(a3,a2)) = product(product(a3,a2),product(a1,a2)),
inference(paramod,[status(thm)],[c_115,c_4162]) ).
cnf(c_4164,plain,
product(a2,product(a3,a2)) = product(product(a3,a1),a2),
inference(paramod,[status(thm)],[c_39,c_4163]) ).
cnf(c_785,plain,
product(product(a3,a1),a2) = product(a2,product(a3,a2)),
inference(copy,[status(thm)],[c_4164]) ).
cnf(c_4165,plain,
product(product(b3,b2),b3) = product(product(b1,b2),product(b3,b2)),
inference(resolve,[status(thm)],[c_18,c_562]) ).
cnf(c_4166,plain,
product(b3,product(b2,b3)) = product(product(b1,b2),product(b3,b2)),
inference(paramod,[status(thm)],[c_100,c_4165]) ).
cnf(c_4167,plain,
product(b3,product(b1,b2)) = product(product(b1,b2),product(b3,b2)),
inference(paramod,[status(thm)],[c_61,c_4166]) ).
cnf(c_4168,plain,
product(b3,product(b1,b2)) = product(product(b1,b3),b2),
inference(paramod,[status(thm)],[c_39,c_4167]) ).
cnf(c_786,plain,
product(product(b1,b3),b2) = product(b3,product(b1,b2)),
inference(copy,[status(thm)],[c_4168]) ).
cnf(c_4169,plain,
product(product(c3,c2),c3) = product(product(c1,c2),product(c3,c2)),
inference(resolve,[status(thm)],[c_18,c_564]) ).
cnf(c_4170,plain,
product(c3,product(c2,c3)) = product(product(c1,c2),product(c3,c2)),
inference(paramod,[status(thm)],[c_100,c_4169]) ).
cnf(c_4171,plain,
product(c3,product(c1,c2)) = product(product(c1,c2),product(c3,c2)),
inference(paramod,[status(thm)],[c_62,c_4170]) ).
cnf(c_4172,plain,
product(c3,product(c1,c2)) = product(product(c1,c3),c2),
inference(paramod,[status(thm)],[c_39,c_4171]) ).
cnf(c_788,plain,
product(product(c1,c3),c2) = product(c3,product(c1,c2)),
inference(copy,[status(thm)],[c_4172]) ).
cnf(c_795,plain,
product(product(a2,A),product(a1,a2)) = product(a2,product(A,a3)),
inference(paramod,[status(thm)],[c_60,c_38]) ).
cnf(c_4173,plain,
product(product(product(a1,b3),product(c2,c3)),product(product(a2,b1),product(a1,a2))) != product(product(product(a1,c3),a2),product(product(b1,b2),product(c1,a3))),
inference(paramod,[status(thm)],[c_35,c_418]) ).
cnf(c_4174,plain,
product(product(product(a1,b3),product(c1,c2)),product(product(a2,b1),product(a1,a2))) != product(product(product(a1,c3),a2),product(product(b1,b2),product(c1,a3))),
inference(paramod,[status(thm)],[c_62,c_4173]) ).
cnf(c_853,plain,
product(product(product(a1,b3),product(c1,c2)),product(a2,product(b1,a3))) != product(product(product(a1,c3),a2),product(product(b1,b2),product(c1,a3))),
inference(paramod,[status(thm)],[c_795,c_4174]) ).
cnf(c_4175,plain,
product(product(product(a1,b3),a2),product(product(c1,c2),product(b1,a3))) != product(product(product(a1,c3),a2),product(product(b1,b2),product(c1,a3))),
inference(paramod,[status(thm)],[c_15,c_853]) ).
cnf(c_856,plain,
product(product(product(a1,c3),a2),product(product(b1,b2),product(c1,a3))) != product(product(product(a1,b3),a2),product(product(c1,c2),product(b1,a3))),
inference(copy,[status(thm)],[c_4175]) ).
cnf(c_4176,plain,
quotient(product(a2,product(a3,a2)),a2) = product(a3,a1),
inference(paramod,[status(thm)],[c_785,c_13]) ).
cnf(c_4177,plain,
product(a2,a3) = product(a3,a1),
inference(paramod,[status(thm)],[c_228,c_4176]) ).
cnf(c_4178,plain,
product(a1,a2) = product(a3,a1),
inference(paramod,[status(thm)],[c_60,c_4177]) ).
cnf(c_902,plain,
product(a3,a1) = product(a1,a2),
inference(copy,[status(thm)],[c_4178]) ).
cnf(c_936,plain,
product(product(a3,A),product(a1,a2)) = product(a3,product(A,a1)),
inference(paramod,[status(thm)],[c_902,c_38]) ).
cnf(c_997,plain,
product(product(product(a1,b1),product(c3,b2)),product(a2,product(c1,a3))) != product(product(product(a1,b3),a2),product(product(c1,c2),product(b1,a3))),
inference(paramod,[status(thm)],[c_34,c_856]) ).
cnf(c_4179,plain,
product(product(product(a1,b1),a2),product(product(c3,c1),product(b2,a3))) != product(product(product(a1,b3),a2),product(product(c1,c2),product(b1,a3))),
inference(paramod,[status(thm)],[c_35,c_997]) ).
cnf(c_1298,plain,
product(product(product(a1,b3),a2),product(product(c1,c2),product(b1,a3))) != product(product(product(a1,b1),a2),product(product(c3,c1),product(b2,a3))),
inference(copy,[status(thm)],[c_4179]) ).
cnf(c_1912,plain,
product(product(A,a2),product(B,a3)) = product(product(A,a1),product(B,a2)),
inference(paramod,[status(thm)],[c_78,c_15]) ).
cnf(c_4180,plain,
bigC(a3,a2,A) = product(product(a3,A),product(a1,a2)),
inference(paramod,[status(thm)],[c_78,c_20]) ).
cnf(c_4181,plain,
product(product(a3,a2),product(A,a3)) = product(product(a3,A),product(a1,a2)),
inference(paramod,[status(thm)],[c_20,c_4180]) ).
cnf(c_4182,plain,
product(product(a3,a1),product(A,a2)) = product(product(a3,A),product(a1,a2)),
inference(paramod,[status(thm)],[c_1912,c_4181]) ).
cnf(c_4183,plain,
product(product(a1,a2),product(A,a2)) = product(product(a3,A),product(a1,a2)),
inference(paramod,[status(thm)],[c_902,c_4182]) ).
cnf(c_4184,plain,
product(product(a1,A),a2) = product(product(a3,A),product(a1,a2)),
inference(paramod,[status(thm)],[c_39,c_4183]) ).
cnf(c_1915,plain,
product(product(a1,A),a2) = product(a3,product(A,a1)),
inference(paramod,[status(thm)],[c_936,c_4184]) ).
cnf(c_4185,plain,
product(product(a3,product(b3,a1)),product(product(c1,c2),product(b1,a3))) != product(product(product(a1,b1),a2),product(product(c3,c1),product(b2,a3))),
inference(paramod,[status(thm)],[c_1915,c_1298]) ).
cnf(c_2007,plain,
product(product(a3,product(b3,a1)),product(product(c1,c2),product(b1,a3))) != product(product(a3,product(b1,a1)),product(product(c3,c1),product(b2,a3))),
inference(paramod,[status(thm)],[c_1915,c_4185]) ).
cnf(c_2799,plain,
difference(product(b1,b3),product(b3,product(b1,b2))) = b2,
inference(paramod,[status(thm)],[c_786,c_11]) ).
cnf(c_2866,plain,
difference(A,product(B,product(C,D))) = product(difference(quotient(A,C),B),D),
inference(paramod,[status(thm)],[c_14,c_118]) ).
cnf(c_4186,plain,
difference(product(A,B),product(B,product(C,D))) = product(difference(A,product(B,C)),D),
inference(paramod,[status(thm)],[c_38,c_118]) ).
cnf(c_2889,plain,
product(difference(quotient(product(A,B),C),B),D) = product(difference(A,product(B,C)),D),
inference(paramod,[status(thm)],[c_2866,c_4186]) ).
cnf(c_4187,plain,
product(difference(quotient(product(b1,b3),b1),b3),b2) = b2,
inference(paramod,[status(thm)],[c_2866,c_2799]) ).
cnf(c_2911,plain,
product(difference(b1,product(b3,b1)),b2) = b2,
inference(paramod,[status(thm)],[c_2889,c_4187]) ).
cnf(c_4188,plain,
quotient(b2,b2) = difference(b1,product(b3,b1)),
inference(paramod,[status(thm)],[c_2911,c_13]) ).
cnf(c_4189,plain,
b2 = difference(b1,product(b3,b1)),
inference(paramod,[status(thm)],[c_37,c_4188]) ).
cnf(c_3059,plain,
difference(b1,product(b3,b1)) = b2,
inference(copy,[status(thm)],[c_4189]) ).
cnf(c_4190,plain,
product(b1,b2) = product(b3,b1),
inference(paramod,[status(thm)],[c_3059,c_12]) ).
cnf(c_3061,plain,
product(b3,b1) = product(b1,b2),
inference(copy,[status(thm)],[c_4190]) ).
cnf(c_3170,plain,
product(product(A,product(b3,B)),product(C,product(b1,D))) = product(product(A,C),product(product(b1,b2),product(B,D))),
inference(paramod,[status(thm)],[c_3061,c_35]) ).
cnf(c_4191,plain,
product(product(a3,product(b3,a1)),product(product(c1,c2),product(b1,a3))) != product(product(a3,product(c3,c1)),product(product(b1,b2),product(a1,a3))),
inference(paramod,[status(thm)],[c_35,c_2007]) ).
cnf(c_3696,plain,
product(product(a3,product(c3,c1)),product(product(b1,b2),product(a1,a3))) != product(product(a3,product(b3,a1)),product(product(c1,c2),product(b1,a3))),
inference(copy,[status(thm)],[c_4191]) ).
cnf(c_4192,plain,
difference(product(c1,c3),product(c3,product(c1,c2))) = c2,
inference(paramod,[status(thm)],[c_788,c_11]) ).
cnf(c_4193,plain,
product(difference(quotient(product(c1,c3),c1),c3),c2) = c2,
inference(paramod,[status(thm)],[c_2866,c_4192]) ).
cnf(c_3955,plain,
product(difference(c1,product(c3,c1)),c2) = c2,
inference(paramod,[status(thm)],[c_2889,c_4193]) ).
cnf(c_4194,plain,
quotient(c2,c2) = difference(c1,product(c3,c1)),
inference(paramod,[status(thm)],[c_3955,c_13]) ).
cnf(c_4195,plain,
c2 = difference(c1,product(c3,c1)),
inference(paramod,[status(thm)],[c_37,c_4194]) ).
cnf(c_4024,plain,
difference(c1,product(c3,c1)) = c2,
inference(copy,[status(thm)],[c_4195]) ).
cnf(c_4196,plain,
product(c1,c2) = product(c3,c1),
inference(paramod,[status(thm)],[c_4024,c_12]) ).
cnf(c_4133,plain,
product(c3,c1) = product(c1,c2),
inference(copy,[status(thm)],[c_4196]) ).
cnf(c_4197,plain,
product(product(a3,product(c1,c2)),product(product(b1,b2),product(a1,a3))) != product(product(a3,product(b3,a1)),product(product(c1,c2),product(b1,a3))),
inference(paramod,[status(thm)],[c_4133,c_3696]) ).
cnf(c_4141,plain,
$false,
inference(resolve,[status(thm)],[c_3170,c_4197]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP780+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 : n026.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:49:25 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.36 % Process 2945810 was started by sandbox on n026,
% 0.10/0.36 % Fri Sep 25 15:49:25 2026
% 0.10/0.36 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.10/0.36
% 0.10/0.36 % From the command line: assign(max_seconds, 300).
% 5.49/1.14
% 5.49/1.14 % SZS status Theorem for theBenchmark
% 5.49/1.14
% 5.49/1.14 % Proof 1 at 0.64 (+ 0.11) seconds.
% 5.49/1.14 % Length of proof is 79.
% 5.49/1.14 % Level of proof is 13.
% 5.49/1.14 % Maximum clause weight is 75.000.
% 5.49/1.14 % Given clauses 394.
% 5.49/1.14
% 5.49/1.14 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------