%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP767-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n011.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 : Fri Sep 25 01:28:22 PM UTC 2026
% Result : Unsatisfiable 27.22s 19.01s
% Output : CNFRefutation 27.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 18
% Syntax : Number of clauses : 108 ( 108 unt; 0 nHn; 57 RR)
% Number of literals : 108 ( 107 equ; 5 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 8 con; 0-2 aty)
% Number of variables : 81 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t3,axiom,
product(X1,difference(X1,X2)) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t21,plain,
product(X1,difference(X1,X2)) = X2,
inference(orient,[status(thm)],[t3]) ).
cnf(t2,axiom,
difference(X1,product(X1,X2)) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t27,plain,
difference(X1,product(X1,X2)) = X2,
inference(orient,[status(thm)],[t2]) ).
cnf(u6,axiom,
product(eta(A),product(B,C)) = product(product(eta(A),B),C),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(u1,axiom,
eta(A) = product(i(A),A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(d0,axiom,
i(A) = difference(A,one),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(d2,axiom,
eta(A) = product(difference(A,one),A),
inference(definition_unfolding,[status(thm)],[u1,d0]) ).
cnf(t11,plain,
product(product(product(difference(X1,one),X1),X2),X3) = product(product(difference(X1,one),X1),product(X2,X3)),
inference(definition_unfolding,[status(thm)],[u6,d2]) ).
cnf(u0,axiom,
product(i(A),A) = product(A,j(A)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(d1,axiom,
j(A) = quotient(one,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t6,plain,
product(difference(X1,one),X1) = product(X1,quotient(one,X1)),
inference(definition_unfolding,[status(thm)],[u0,d0,d1]) ).
cnf(t51,plain,
product(difference(X1,one),X1) = product(X1,quotient(one,X1)),
inference(orient,[status(thm)],[t6]) ).
cnf(t9016,plain,
product(product(product(X1,quotient(one,X1)),X2),X3) = product(product(difference(X1,one),X1),product(X2,X3)),
inference(step,[status(thm)],[t11,t51]) ).
cnf(t9017,plain,
product(product(product(X1,quotient(one,X1)),X2),X3) = product(product(X1,quotient(one,X1)),product(X2,X3)),
inference(step,[status(thm)],[t9016,t51]) ).
cnf(t57,plain,
product(product(product(X1,quotient(one,X1)),X2),X3) = product(product(X1,quotient(one,X1)),product(X2,X3)),
inference(orient,[status(thm)],[t9017]) ).
cnf(u2,axiom,
product(i(i(A)),B) = product(eta(A),product(A,B)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t9,plain,
product(product(difference(X1,one),X1),product(X1,X2)) = product(difference(difference(X1,one),one),X2),
inference(definition_unfolding,[status(thm)],[u2,d0,d2]) ).
cnf(t9018,plain,
product(product(X1,quotient(one,X1)),product(X1,X2)) = product(difference(difference(X1,one),one),X2),
inference(step,[status(thm)],[t9,t51]) ).
cnf(t65,plain,
product(product(X1,quotient(one,X1)),product(X1,X2)) = product(difference(difference(X1,one),one),X2),
inference(orient,[status(thm)],[t9018]) ).
cnf(t78,plain,
product(product(X1,quotient(one,X1)),product(product(X1,X2),X3)) = product(product(difference(difference(X1,one),one),X2),X3),
inference(cp,[status(thm)],[t57,t65]) ).
cnf(t7265,plain,
product(product(X1,quotient(one,X1)),product(product(X1,X2),X3)) = product(product(difference(difference(X1,one),one),X2),X3),
inference(orient,[status(thm)],[t78]) ).
cnf(t19,axiom,
sFlat4 = product(quotient(one,quotient(one,x0)),quotient(one,product(x1,x0))),
introduced(definition) ).
cnf(t131,plain,
product(quotient(one,quotient(one,x0)),quotient(one,product(x1,x0))) = sFlat4,
inference(orient,[status(thm)],[t19]) ).
cnf(t17,axiom,
sFlat2 = product(x1,x0),
introduced(definition) ).
cnf(t137,plain,
product(x1,x0) = sFlat2,
inference(orient,[status(thm)],[t17]) ).
cnf(t9025,plain,
product(quotient(one,quotient(one,x0)),quotient(one,sFlat2)) = sFlat4,
inference(step,[status(thm)],[t131,t137]) ).
cnf(t143,plain,
product(quotient(one,quotient(one,x0)),quotient(one,sFlat2)) = sFlat4,
inference(rw,[status(thm)],[t9025]) ).
cnf(t15,axiom,
sFlat0 = quotient(one,x0),
introduced(definition) ).
cnf(t200,plain,
quotient(one,x0) = sFlat0,
inference(orient,[status(thm)],[t15]) ).
cnf(t9666,plain,
product(quotient(one,sFlat0),quotient(one,sFlat2)) = sFlat4,
inference(step,[status(thm)],[t143,t200]) ).
cnf(t16,axiom,
sFlat1 = quotient(one,quotient(one,x0)),
introduced(definition) ).
cnf(t192,plain,
quotient(one,quotient(one,x0)) = sFlat1,
inference(orient,[status(thm)],[t16]) ).
cnf(t9030,plain,
quotient(one,sFlat0) = sFlat1,
inference(step,[status(thm)],[t192,t200]) ).
cnf(t208,plain,
quotient(one,sFlat0) = sFlat1,
inference(rw,[status(thm)],[t9030]) ).
cnf(t237,plain,
quotient(one,sFlat0) = sFlat1,
inference(orient,[status(thm)],[t208]) ).
cnf(t9667,plain,
product(sFlat1,quotient(one,sFlat2)) = sFlat4,
inference(step,[status(thm)],[t9666,t237]) ).
cnf(t18,axiom,
sFlat3 = quotient(one,product(x1,x0)),
introduced(definition) ).
cnf(t9029,plain,
sFlat3 = quotient(one,sFlat2),
inference(step,[status(thm)],[t18,t137]) ).
cnf(t184,plain,
quotient(one,sFlat2) = sFlat3,
inference(orient,[status(thm)],[t9029]) ).
cnf(t9668,plain,
product(sFlat1,sFlat3) = sFlat4,
inference(step,[status(thm)],[t9667,t184]) ).
cnf(t6602,plain,
product(sFlat1,sFlat3) = sFlat4,
inference(orient,[status(thm)],[t9668]) ).
cnf(t7477,plain,
product(product(difference(difference(sFlat1,one),one),sFlat3),X1) = product(product(sFlat1,quotient(one,sFlat1)),product(sFlat4,X1)),
inference(cp,[status(thm)],[t7265,t6602]) ).
cnf(t4,axiom,
product(quotient(X1,X2),X2) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t25,plain,
product(quotient(X1,X2),X2) = X1,
inference(orient,[status(thm)],[t4]) ).
cnf(t238,plain,
one = product(sFlat1,sFlat0),
inference(cp,[status(thm)],[t25,t237]) ).
cnf(t255,plain,
product(sFlat1,sFlat0) = one,
inference(orient,[status(thm)],[t238]) ).
cnf(t256,plain,
sFlat0 = difference(sFlat1,one),
inference(cp,[status(thm)],[t27,t255]) ).
cnf(t263,plain,
difference(sFlat1,one) = sFlat0,
inference(orient,[status(thm)],[t256]) ).
cnf(t9724,plain,
product(product(difference(sFlat0,one),sFlat3),X1) = product(product(sFlat1,quotient(one,sFlat1)),product(sFlat4,X1)),
inference(step,[status(thm)],[t7477,t263]) ).
cnf(t201,plain,
one = product(sFlat0,x0),
inference(cp,[status(thm)],[t25,t200]) ).
cnf(t231,plain,
product(sFlat0,x0) = one,
inference(orient,[status(thm)],[t201]) ).
cnf(t232,plain,
x0 = difference(sFlat0,one),
inference(cp,[status(thm)],[t27,t231]) ).
cnf(t253,plain,
difference(sFlat0,one) = x0,
inference(orient,[status(thm)],[t232]) ).
cnf(t9725,plain,
product(product(x0,sFlat3),X1) = product(product(sFlat1,quotient(one,sFlat1)),product(sFlat4,X1)),
inference(step,[status(thm)],[t9724,t253]) ).
cnf(t264,plain,
product(sFlat1,quotient(one,sFlat1)) = product(sFlat0,sFlat1),
inference(cp,[status(thm)],[t51,t263]) ).
cnf(t311,plain,
product(sFlat1,quotient(one,sFlat1)) = product(sFlat0,sFlat1),
inference(orient,[status(thm)],[t264]) ).
cnf(t5,axiom,
quotient(product(X1,X2),X2) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t31,plain,
quotient(product(X1,X2),X2) = X1,
inference(orient,[status(thm)],[t5]) ).
cnf(t7,axiom,
quotient(product(X1,product(X2,X3)),X3) = difference(X3,product(product(X3,X1),X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t144,plain,
difference(X1,product(product(X1,X2),X3)) = quotient(product(X2,product(X3,X1)),X1),
inference(orient,[status(thm)],[t7]) ).
cnf(t260,plain,
quotient(product(sFlat0,product(X1,sFlat1)),sFlat1) = difference(sFlat1,product(one,X1)),
inference(cp,[status(thm)],[t144,t255]) ).
cnf(t1,axiom,
product(one,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t23,plain,
product(one,X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t9060,plain,
quotient(product(sFlat0,product(X1,sFlat1)),sFlat1) = difference(sFlat1,X1),
inference(step,[status(thm)],[t260,t23]) ).
cnf(t611,plain,
quotient(product(sFlat0,product(X1,sFlat1)),sFlat1) = difference(sFlat1,X1),
inference(orient,[status(thm)],[t9060]) ).
cnf(t618,plain,
product(sFlat0,product(X1,sFlat1)) = product(difference(sFlat1,X1),sFlat1),
inference(cp,[status(thm)],[t25,t611]) ).
cnf(t624,plain,
product(difference(sFlat1,X1),sFlat1) = product(sFlat0,product(X1,sFlat1)),
inference(orient,[status(thm)],[t618]) ).
cnf(t313,plain,
quotient(one,sFlat1) = difference(sFlat1,product(sFlat0,sFlat1)),
inference(cp,[status(thm)],[t27,t311]) ).
cnf(t328,plain,
difference(sFlat1,product(sFlat0,sFlat1)) = quotient(one,sFlat1),
inference(orient,[status(thm)],[t313]) ).
cnf(t626,plain,
product(sFlat0,product(product(sFlat0,sFlat1),sFlat1)) = product(quotient(one,sFlat1),sFlat1),
inference(cp,[status(thm)],[t624,t328]) ).
cnf(t9061,plain,
product(sFlat0,product(product(sFlat0,sFlat1),sFlat1)) = one,
inference(step,[status(thm)],[t626,t25]) ).
cnf(t635,plain,
product(sFlat0,product(product(sFlat0,sFlat1),sFlat1)) = one,
inference(orient,[status(thm)],[t9061]) ).
cnf(t638,plain,
product(product(sFlat0,sFlat1),sFlat1) = difference(sFlat0,one),
inference(cp,[status(thm)],[t27,t635]) ).
cnf(t9062,plain,
product(product(sFlat0,sFlat1),sFlat1) = x0,
inference(step,[status(thm)],[t638,t253]) ).
cnf(t644,plain,
product(product(sFlat0,sFlat1),sFlat1) = x0,
inference(orient,[status(thm)],[t9062]) ).
cnf(t645,plain,
product(sFlat0,sFlat1) = quotient(x0,sFlat1),
inference(cp,[status(thm)],[t31,t644]) ).
cnf(t652,plain,
product(sFlat0,sFlat1) = quotient(x0,sFlat1),
inference(orient,[status(thm)],[t645]) ).
cnf(t9065,plain,
product(sFlat1,quotient(one,sFlat1)) = quotient(x0,sFlat1),
inference(step,[status(thm)],[t311,t652]) ).
cnf(t655,plain,
product(sFlat1,quotient(one,sFlat1)) = quotient(x0,sFlat1),
inference(orient,[status(thm)],[t9065]) ).
cnf(t9726,plain,
product(product(x0,sFlat3),X1) = product(quotient(x0,sFlat1),product(sFlat4,X1)),
inference(step,[status(thm)],[t9725,t655]) ).
cnf(t314,plain,
product(difference(difference(sFlat1,one),one),X1) = product(product(sFlat0,sFlat1),product(sFlat1,X1)),
inference(cp,[status(thm)],[t65,t311]) ).
cnf(t9074,plain,
product(difference(sFlat0,one),X1) = product(product(sFlat0,sFlat1),product(sFlat1,X1)),
inference(step,[status(thm)],[t314,t263]) ).
cnf(t9075,plain,
product(x0,X1) = product(product(sFlat0,sFlat1),product(sFlat1,X1)),
inference(step,[status(thm)],[t9074,t253]) ).
cnf(t9076,plain,
product(x0,X1) = product(quotient(x0,sFlat1),product(sFlat1,X1)),
inference(step,[status(thm)],[t9075,t652]) ).
cnf(t718,plain,
product(quotient(x0,sFlat1),product(sFlat1,X1)) = product(x0,X1),
inference(orient,[status(thm)],[t9076]) ).
cnf(t723,plain,
product(x0,difference(sFlat1,X1)) = product(quotient(x0,sFlat1),X1),
inference(cp,[status(thm)],[t718,t21]) ).
cnf(t731,plain,
product(quotient(x0,sFlat1),X1) = product(x0,difference(sFlat1,X1)),
inference(orient,[status(thm)],[t723]) ).
cnf(t9727,plain,
product(product(x0,sFlat3),X1) = product(x0,difference(sFlat1,product(sFlat4,X1))),
inference(step,[status(thm)],[t9726,t731]) ).
cnf(t8095,plain,
product(x0,difference(sFlat1,product(sFlat4,X1))) = product(product(x0,sFlat3),X1),
inference(orient,[status(thm)],[t9727]) ).
cnf(t8113,plain,
difference(sFlat1,product(sFlat4,X1)) = difference(x0,product(product(x0,sFlat3),X1)),
inference(cp,[status(thm)],[t27,t8095]) ).
cnf(t9767,plain,
difference(sFlat1,product(sFlat4,X1)) = quotient(product(sFlat3,product(X1,x0)),x0),
inference(step,[status(thm)],[t8113,t144]) ).
cnf(t8946,plain,
quotient(product(sFlat3,product(X1,x0)),x0) = difference(sFlat1,product(sFlat4,X1)),
inference(orient,[status(thm)],[t9767]) ).
cnf(t8970,plain,
difference(sFlat1,product(sFlat4,x1)) = quotient(product(sFlat3,sFlat2),x0),
inference(cp,[status(thm)],[t8946,t137]) ).
cnf(t185,plain,
one = product(sFlat3,sFlat2),
inference(cp,[status(thm)],[t25,t184]) ).
cnf(t225,plain,
product(sFlat3,sFlat2) = one,
inference(orient,[status(thm)],[t185]) ).
cnf(t9768,plain,
difference(sFlat1,product(sFlat4,x1)) = quotient(one,x0),
inference(step,[status(thm)],[t8970,t225]) ).
cnf(t9769,plain,
difference(sFlat1,product(sFlat4,x1)) = sFlat0,
inference(step,[status(thm)],[t9768,t200]) ).
cnf(t8985,plain,
difference(sFlat1,product(sFlat4,x1)) = sFlat0,
inference(orient,[status(thm)],[t9769]) ).
cnf(t8986,plain,
product(sFlat4,x1) = product(sFlat1,sFlat0),
inference(cp,[status(thm)],[t21,t8985]) ).
cnf(t9770,plain,
product(sFlat4,x1) = one,
inference(step,[status(thm)],[t8986,t255]) ).
cnf(t8996,plain,
product(sFlat4,x1) = one,
inference(orient,[status(thm)],[t9770]) ).
cnf(u4,negated_conjecture,
product(j(j(x0)),j(product(x1,x0))) != j(x1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(goal_0,negated_conjecture,
product(quotient(one,quotient(one,x0)),quotient(one,product(x1,x0))) != quotient(one,x1),
inference(definition_unfolding,[status(thm)],[u4,d1]) ).
cnf(g0_0,plain,
sFlat4 != quotient(one,x1),
inference(rw,[status(thm)],[goal_0]) ).
cnf(g0_1,plain,
sFlat4 != quotient(product(sFlat4,x1),x1),
inference(rw,[status(thm)],[g0_0,t8996]) ).
cnf(g0_2,plain,
sFlat4 != sFlat4,
inference(rw,[status(thm)],[g0_1,t31]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRP767-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.07 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.08/0.34 % Computer : n011.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.17/15.51 % CPULimit : 300
% 0.17/15.51 % WCLimit : 300
% 0.17/15.51 % DateTime : Wed Sep 23 15:59:50 UTC 2026
% 0.17/15.51 % CPUTime :
% 0.17/15.51 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 27.22/19.01 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 27.22/19.01 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------