%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP768-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 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 : Fri Sep 25 01:28:22 PM UTC 2026
% Result : Unsatisfiable 16.48s 7.78s
% Output : CNFRefutation 16.48s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 25
% Syntax : Number of clauses : 182 ( 182 unt; 0 nHn; 121 RR)
% Number of literals : 182 ( 181 equ; 28 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 21 ( 21 usr; 14 con; 0-2 aty)
% Number of variables : 100 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t4,axiom,
product(quotient(X1,X2),X2) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t29,plain,
product(quotient(X1,X2),X2) = X1,
inference(orient,[status(thm)],[t4]) ).
cnf(t8,axiom,
quotient(product(X1,product(X2,X3)),X3) = difference(X3,product(product(X3,X1),X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t134,plain,
difference(X1,product(product(X1,X2),X3)) = quotient(product(X2,product(X3,X1)),X1),
inference(orient,[status(thm)],[t8]) ).
cnf(t3,axiom,
product(X1,difference(X1,X2)) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t25,plain,
product(X1,difference(X1,X2)) = X2,
inference(orient,[status(thm)],[t3]) ).
cnf(t15,axiom,
sFlat0 = difference(x0,one),
introduced(definition) ).
cnf(t183,plain,
difference(x0,one) = sFlat0,
inference(orient,[status(thm)],[t15]) ).
cnf(t184,plain,
one = product(x0,sFlat0),
inference(cp,[status(thm)],[t25,t183]) ).
cnf(t219,plain,
product(x0,sFlat0) = one,
inference(orient,[status(thm)],[t184]) ).
cnf(t224,plain,
quotient(product(sFlat0,product(X1,x0)),x0) = difference(x0,product(one,X1)),
inference(cp,[status(thm)],[t134,t219]) ).
cnf(t1,axiom,
product(one,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t27,plain,
product(one,X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t2803,plain,
quotient(product(sFlat0,product(X1,x0)),x0) = difference(x0,X1),
inference(step,[status(thm)],[t224,t27]) ).
cnf(t1229,plain,
quotient(product(sFlat0,product(X1,x0)),x0) = difference(x0,X1),
inference(orient,[status(thm)],[t2803]) ).
cnf(t1239,plain,
product(sFlat0,product(X1,x0)) = product(difference(x0,X1),x0),
inference(cp,[status(thm)],[t29,t1229]) ).
cnf(t1256,plain,
product(difference(x0,X1),x0) = product(sFlat0,product(X1,x0)),
inference(orient,[status(thm)],[t1239]) ).
cnf(u0,axiom,
product(i(A),A) = product(A,j(A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(d0,axiom,
i(A) = difference(A,one),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(d1,axiom,
j(A) = quotient(one,A),
file('/export/starexec/sandbox2/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(t55,plain,
product(difference(X1,one),X1) = product(X1,quotient(one,X1)),
inference(orient,[status(thm)],[t6]) ).
cnf(t186,plain,
product(x0,quotient(one,x0)) = product(sFlat0,x0),
inference(cp,[status(thm)],[t55,t183]) ).
cnf(t16,axiom,
sFlat1 = product(difference(x0,one),x0),
introduced(definition) ).
cnf(t2738,plain,
sFlat1 = product(x0,quotient(one,x0)),
inference(step,[status(thm)],[t16,t55]) ).
cnf(t113,plain,
product(x0,quotient(one,x0)) = sFlat1,
inference(orient,[status(thm)],[t2738]) ).
cnf(t2766,plain,
sFlat1 = product(sFlat0,x0),
inference(step,[status(thm)],[t186,t113]) ).
cnf(t225,plain,
product(sFlat0,x0) = sFlat1,
inference(orient,[status(thm)],[t2766]) ).
cnf(t17,axiom,
sFlat2 = product(product(difference(x0,one),x0),x1),
introduced(definition) ).
cnf(t2736,plain,
sFlat2 = product(product(x0,quotient(one,x0)),x1),
inference(step,[status(thm)],[t17,t55]) ).
cnf(t103,plain,
product(product(x0,quotient(one,x0)),x1) = sFlat2,
inference(orient,[status(thm)],[t2736]) ).
cnf(t2740,plain,
product(sFlat1,x1) = sFlat2,
inference(step,[status(thm)],[t103,t113]) ).
cnf(t120,plain,
product(sFlat1,x1) = sFlat2,
inference(rw,[status(thm)],[t2740]) ).
cnf(t209,plain,
product(sFlat1,x1) = sFlat2,
inference(orient,[status(thm)],[t120]) ).
cnf(t18,axiom,
sFlat3 = quotient(product(product(difference(x0,one),x0),x1),product(difference(x0,one),x0)),
introduced(definition) ).
cnf(t2755,plain,
sFlat3 = quotient(product(product(x0,quotient(one,x0)),x1),product(difference(x0,one),x0)),
inference(step,[status(thm)],[t18,t55]) ).
cnf(t2756,plain,
sFlat3 = quotient(product(sFlat1,x1),product(difference(x0,one),x0)),
inference(step,[status(thm)],[t2755,t113]) ).
cnf(t2757,plain,
sFlat3 = quotient(product(sFlat1,x1),product(x0,quotient(one,x0))),
inference(step,[status(thm)],[t2756,t55]) ).
cnf(t2758,plain,
sFlat3 = quotient(product(sFlat1,x1),sFlat1),
inference(step,[status(thm)],[t2757,t113]) ).
cnf(t189,plain,
quotient(product(sFlat1,x1),sFlat1) = sFlat3,
inference(orient,[status(thm)],[t2758]) ).
cnf(t2765,plain,
quotient(sFlat2,sFlat1) = sFlat3,
inference(step,[status(thm)],[t189,t209]) ).
cnf(t216,plain,
quotient(sFlat2,sFlat1) = sFlat3,
inference(rw,[status(thm)],[t2765]) ).
cnf(t238,plain,
quotient(sFlat2,sFlat1) = sFlat3,
inference(orient,[status(thm)],[t216]) ).
cnf(t19,axiom,
sFlat4 = product(product(difference(x0,one),x0),x2),
introduced(definition) ).
cnf(t2737,plain,
sFlat4 = product(product(x0,quotient(one,x0)),x2),
inference(step,[status(thm)],[t19,t55]) ).
cnf(t108,plain,
product(product(x0,quotient(one,x0)),x2) = sFlat4,
inference(orient,[status(thm)],[t2737]) ).
cnf(t2739,plain,
product(sFlat1,x2) = sFlat4,
inference(step,[status(thm)],[t108,t113]) ).
cnf(t119,plain,
product(sFlat1,x2) = sFlat4,
inference(rw,[status(thm)],[t2739]) ).
cnf(t201,plain,
product(sFlat1,x2) = sFlat4,
inference(orient,[status(thm)],[t119]) ).
cnf(t20,axiom,
sFlat5 = quotient(product(product(difference(x0,one),x0),x2),product(difference(x0,one),x0)),
introduced(definition) ).
cnf(t2760,plain,
sFlat5 = quotient(product(product(x0,quotient(one,x0)),x2),product(difference(x0,one),x0)),
inference(step,[status(thm)],[t20,t55]) ).
cnf(t2761,plain,
sFlat5 = quotient(product(sFlat1,x2),product(difference(x0,one),x0)),
inference(step,[status(thm)],[t2760,t113]) ).
cnf(t2762,plain,
sFlat5 = quotient(product(sFlat1,x2),product(x0,quotient(one,x0))),
inference(step,[status(thm)],[t2761,t55]) ).
cnf(t2763,plain,
sFlat5 = quotient(product(sFlat1,x2),sFlat1),
inference(step,[status(thm)],[t2762,t113]) ).
cnf(t192,plain,
quotient(product(sFlat1,x2),sFlat1) = sFlat5,
inference(orient,[status(thm)],[t2763]) ).
cnf(t2764,plain,
quotient(sFlat4,sFlat1) = sFlat5,
inference(step,[status(thm)],[t192,t201]) ).
cnf(t208,plain,
quotient(sFlat4,sFlat1) = sFlat5,
inference(rw,[status(thm)],[t2764]) ).
cnf(t234,plain,
quotient(sFlat4,sFlat1) = sFlat5,
inference(orient,[status(thm)],[t208]) ).
cnf(t21,axiom,
sFlat6 = product(quotient(product(product(difference(x0,one),x0),x1),product(difference(x0,one),x0)),quotient(product(product(difference(x0,one),x0),x2),product(difference(x0,one),x0))),
introduced(definition) ).
cnf(t2742,plain,
sFlat6 = product(quotient(product(product(x0,quotient(one,x0)),x1),product(difference(x0,one),x0)),quotient(product(product(difference(x0,one),x0),x2),product(difference(x0,one),x0))),
inference(step,[status(thm)],[t21,t55]) ).
cnf(t2743,plain,
sFlat6 = product(quotient(product(sFlat1,x1),product(difference(x0,one),x0)),quotient(product(product(difference(x0,one),x0),x2),product(difference(x0,one),x0))),
inference(step,[status(thm)],[t2742,t113]) ).
cnf(t2744,plain,
sFlat6 = product(quotient(product(sFlat1,x1),product(x0,quotient(one,x0))),quotient(product(product(difference(x0,one),x0),x2),product(difference(x0,one),x0))),
inference(step,[status(thm)],[t2743,t55]) ).
cnf(t2745,plain,
sFlat6 = product(quotient(product(sFlat1,x1),sFlat1),quotient(product(product(difference(x0,one),x0),x2),product(difference(x0,one),x0))),
inference(step,[status(thm)],[t2744,t113]) ).
cnf(t2746,plain,
sFlat6 = product(quotient(product(sFlat1,x1),sFlat1),quotient(product(product(x0,quotient(one,x0)),x2),product(difference(x0,one),x0))),
inference(step,[status(thm)],[t2745,t55]) ).
cnf(t2747,plain,
sFlat6 = product(quotient(product(sFlat1,x1),sFlat1),quotient(product(sFlat1,x2),product(difference(x0,one),x0))),
inference(step,[status(thm)],[t2746,t113]) ).
cnf(t2748,plain,
sFlat6 = product(quotient(product(sFlat1,x1),sFlat1),quotient(product(sFlat1,x2),product(x0,quotient(one,x0)))),
inference(step,[status(thm)],[t2747,t55]) ).
cnf(t2749,plain,
sFlat6 = product(quotient(product(sFlat1,x1),sFlat1),quotient(product(sFlat1,x2),sFlat1)),
inference(step,[status(thm)],[t2748,t113]) ).
cnf(t122,plain,
product(quotient(product(sFlat1,x1),sFlat1),quotient(product(sFlat1,x2),sFlat1)) = sFlat6,
inference(orient,[status(thm)],[t2749]) ).
cnf(t2759,plain,
product(sFlat3,quotient(product(sFlat1,x2),sFlat1)) = sFlat6,
inference(step,[status(thm)],[t122,t189]) ).
cnf(t191,plain,
product(sFlat3,quotient(product(sFlat1,x2),sFlat1)) = sFlat6,
inference(rw,[status(thm)],[t2759]) ).
cnf(t2784,plain,
product(sFlat3,quotient(sFlat4,sFlat1)) = sFlat6,
inference(step,[status(thm)],[t191,t201]) ).
cnf(t2785,plain,
product(sFlat3,sFlat5) = sFlat6,
inference(step,[status(thm)],[t2784,t234]) ).
cnf(t619,plain,
product(sFlat3,sFlat5) = sFlat6,
inference(orient,[status(thm)],[t2785]) ).
cnf(u7,axiom,
product(eta(A),product(B,C)) = product(product(eta(A),B),C),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(u1,axiom,
eta(A) = product(i(A),A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(d2,axiom,
eta(A) = product(difference(A,one),A),
inference(definition_unfolding,[status(thm)],[u1,d0]) ).
cnf(t12,plain,
product(product(product(difference(X1,one),X1),X2),X3) = product(product(difference(X1,one),X1),product(X2,X3)),
inference(definition_unfolding,[status(thm)],[u7,d2]) ).
cnf(t2732,plain,
product(product(product(X1,quotient(one,X1)),X2),X3) = product(product(difference(X1,one),X1),product(X2,X3)),
inference(step,[status(thm)],[t12,t55]) ).
cnf(t2733,plain,
product(product(product(X1,quotient(one,X1)),X2),X3) = product(product(X1,quotient(one,X1)),product(X2,X3)),
inference(step,[status(thm)],[t2732,t55]) ).
cnf(t61,plain,
product(product(product(X1,quotient(one,X1)),X2),X3) = product(product(X1,quotient(one,X1)),product(X2,X3)),
inference(orient,[status(thm)],[t2733]) ).
cnf(t118,plain,
product(product(x0,quotient(one,x0)),product(X1,X2)) = product(product(sFlat1,X1),X2),
inference(cp,[status(thm)],[t61,t113]) ).
cnf(t2772,plain,
product(sFlat1,product(X1,X2)) = product(product(sFlat1,X1),X2),
inference(step,[status(thm)],[t118,t113]) ).
cnf(t305,plain,
product(product(sFlat1,X1),X2) = product(sFlat1,product(X1,X2)),
inference(orient,[status(thm)],[t2772]) ).
cnf(t310,plain,
product(sFlat1,product(x1,X1)) = product(sFlat2,X1),
inference(cp,[status(thm)],[t305,t209]) ).
cnf(t344,plain,
product(sFlat1,product(x1,X1)) = product(sFlat2,X1),
inference(orient,[status(thm)],[t310]) ).
cnf(t22,axiom,
sFlat7 = product(x1,x2),
introduced(definition) ).
cnf(t130,plain,
product(x1,x2) = sFlat7,
inference(orient,[status(thm)],[t22]) ).
cnf(t345,plain,
product(sFlat2,x2) = product(sFlat1,sFlat7),
inference(cp,[status(thm)],[t344,t130]) ).
cnf(t23,axiom,
sFlat8 = product(product(difference(x0,one),x0),product(x1,x2)),
introduced(definition) ).
cnf(t2735,plain,
sFlat8 = product(product(x0,quotient(one,x0)),product(x1,x2)),
inference(step,[status(thm)],[t23,t55]) ).
cnf(t98,plain,
product(product(x0,quotient(one,x0)),product(x1,x2)) = sFlat8,
inference(orient,[status(thm)],[t2735]) ).
cnf(t2741,plain,
product(sFlat1,product(x1,x2)) = sFlat8,
inference(step,[status(thm)],[t98,t113]) ).
cnf(t121,plain,
product(sFlat1,product(x1,x2)) = sFlat8,
inference(rw,[status(thm)],[t2741]) ).
cnf(t2767,plain,
product(sFlat1,sFlat7) = sFlat8,
inference(step,[status(thm)],[t121,t130]) ).
cnf(t280,plain,
product(sFlat1,sFlat7) = sFlat8,
inference(orient,[status(thm)],[t2767]) ).
cnf(t2773,plain,
product(sFlat2,x2) = sFlat8,
inference(step,[status(thm)],[t345,t280]) ).
cnf(t355,plain,
product(sFlat2,x2) = sFlat8,
inference(orient,[status(thm)],[t2773]) ).
cnf(t24,axiom,
sFlat9 = quotient(product(product(difference(x0,one),x0),product(x1,x2)),product(difference(x0,one),x0)),
introduced(definition) ).
cnf(t2750,plain,
sFlat9 = quotient(product(product(x0,quotient(one,x0)),product(x1,x2)),product(difference(x0,one),x0)),
inference(step,[status(thm)],[t24,t55]) ).
cnf(t2751,plain,
sFlat9 = quotient(product(sFlat1,product(x1,x2)),product(difference(x0,one),x0)),
inference(step,[status(thm)],[t2750,t113]) ).
cnf(t2752,plain,
sFlat9 = quotient(product(sFlat1,sFlat7),product(difference(x0,one),x0)),
inference(step,[status(thm)],[t2751,t130]) ).
cnf(t2753,plain,
sFlat9 = quotient(product(sFlat1,sFlat7),product(x0,quotient(one,x0))),
inference(step,[status(thm)],[t2752,t55]) ).
cnf(t2754,plain,
sFlat9 = quotient(product(sFlat1,sFlat7),sFlat1),
inference(step,[status(thm)],[t2753,t113]) ).
cnf(t187,plain,
quotient(product(sFlat1,sFlat7),sFlat1) = sFlat9,
inference(orient,[status(thm)],[t2754]) ).
cnf(t2770,plain,
quotient(sFlat8,sFlat1) = sFlat9,
inference(step,[status(thm)],[t187,t280]) ).
cnf(t289,plain,
quotient(sFlat8,sFlat1) = sFlat9,
inference(rw,[status(thm)],[t2770]) ).
cnf(t293,plain,
quotient(sFlat8,sFlat1) = sFlat9,
inference(orient,[status(thm)],[t289]) ).
cnf(t319,plain,
quotient(product(X1,product(X2,sFlat1)),sFlat1) = difference(sFlat1,product(sFlat1,product(X1,X2))),
inference(cp,[status(thm)],[t134,t305]) ).
cnf(t2,axiom,
difference(X1,product(X1,X2)) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t31,plain,
difference(X1,product(X1,X2)) = X2,
inference(orient,[status(thm)],[t2]) ).
cnf(t311,plain,
product(sFlat1,product(difference(sFlat1,X1),X2)) = product(X1,X2),
inference(cp,[status(thm)],[t305,t25]) ).
cnf(t1370,plain,
product(sFlat1,product(difference(sFlat1,X1),X2)) = product(X1,X2),
inference(orient,[status(thm)],[t311]) ).
cnf(t1385,plain,
product(difference(sFlat1,X1),X2) = difference(sFlat1,product(X1,X2)),
inference(cp,[status(thm)],[t31,t1370]) ).
cnf(t1391,plain,
difference(sFlat1,product(X1,X2)) = product(difference(sFlat1,X1),X2),
inference(orient,[status(thm)],[t1385]) ).
cnf(t2875,plain,
quotient(product(X1,product(X2,sFlat1)),sFlat1) = product(difference(sFlat1,sFlat1),product(X1,X2)),
inference(step,[status(thm)],[t319,t1391]) ).
cnf(t0,axiom,
product(X1,one) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t26,plain,
product(X1,one) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t32,plain,
one = difference(X1,X1),
inference(cp,[status(thm)],[t31,t26]) ).
cnf(t199,plain,
difference(X1,X1) = one,
inference(orient,[status(thm)],[t32]) ).
cnf(t2876,plain,
quotient(product(X1,product(X2,sFlat1)),sFlat1) = product(one,product(X1,X2)),
inference(step,[status(thm)],[t2875,t199]) ).
cnf(t2877,plain,
quotient(product(X1,product(X2,sFlat1)),sFlat1) = product(X1,X2),
inference(step,[status(thm)],[t2876,t27]) ).
cnf(t2558,plain,
quotient(product(X1,product(X2,sFlat1)),sFlat1) = product(X1,X2),
inference(orient,[status(thm)],[t2877]) ).
cnf(t235,plain,
sFlat4 = product(sFlat5,sFlat1),
inference(cp,[status(thm)],[t29,t234]) ).
cnf(t247,plain,
product(sFlat5,sFlat1) = sFlat4,
inference(orient,[status(thm)],[t235]) ).
cnf(t2577,plain,
product(X1,sFlat5) = quotient(product(X1,sFlat4),sFlat1),
inference(cp,[status(thm)],[t2558,t247]) ).
cnf(t2680,plain,
quotient(product(X1,sFlat4),sFlat1) = product(X1,sFlat5),
inference(orient,[status(thm)],[t2577]) ).
cnf(t13,axiom,
quotient(quotient(product(X1,product(X2,X3)),X3),X2) = difference(product(X2,X3),product(X2,product(X3,X1))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t151,plain,
difference(product(X1,X2),product(X1,product(X2,X3))) = quotient(quotient(product(X3,product(X1,X2)),X2),X1),
inference(orient,[status(thm)],[t13]) ).
cnf(t309,plain,
product(sFlat1,product(x2,X1)) = product(sFlat4,X1),
inference(cp,[status(thm)],[t305,t201]) ).
cnf(t334,plain,
product(sFlat1,product(x2,X1)) = product(sFlat4,X1),
inference(orient,[status(thm)],[t309]) ).
cnf(t341,plain,
quotient(quotient(product(X1,product(sFlat1,x2)),x2),sFlat1) = difference(product(sFlat1,x2),product(sFlat4,X1)),
inference(cp,[status(thm)],[t151,t334]) ).
cnf(t2790,plain,
quotient(quotient(product(X1,sFlat4),x2),sFlat1) = difference(product(sFlat1,x2),product(sFlat4,X1)),
inference(step,[status(thm)],[t341,t201]) ).
cnf(t2791,plain,
quotient(quotient(product(X1,sFlat4),x2),sFlat1) = difference(sFlat4,product(sFlat4,X1)),
inference(step,[status(thm)],[t2790,t201]) ).
cnf(t2792,plain,
quotient(quotient(product(X1,sFlat4),x2),sFlat1) = X1,
inference(step,[status(thm)],[t2791,t31]) ).
cnf(t724,plain,
quotient(quotient(product(X1,sFlat4),x2),sFlat1) = X1,
inference(orient,[status(thm)],[t2792]) ).
cnf(t729,plain,
quotient(X1,sFlat4) = quotient(quotient(X1,x2),sFlat1),
inference(cp,[status(thm)],[t724,t29]) ).
cnf(t733,plain,
quotient(quotient(X1,x2),sFlat1) = quotient(X1,sFlat4),
inference(orient,[status(thm)],[t729]) ).
cnf(t5,axiom,
quotient(product(X1,X2),X2) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t35,plain,
quotient(product(X1,X2),X2) = X1,
inference(orient,[status(thm)],[t5]) ).
cnf(t356,plain,
sFlat2 = quotient(sFlat8,x2),
inference(cp,[status(thm)],[t35,t355]) ).
cnf(t362,plain,
quotient(sFlat8,x2) = sFlat2,
inference(orient,[status(thm)],[t356]) ).
cnf(t735,plain,
quotient(sFlat8,sFlat4) = quotient(sFlat2,sFlat1),
inference(cp,[status(thm)],[t733,t362]) ).
cnf(t2793,plain,
quotient(sFlat8,sFlat4) = sFlat3,
inference(step,[status(thm)],[t735,t238]) ).
cnf(t742,plain,
quotient(sFlat8,sFlat4) = sFlat3,
inference(orient,[status(thm)],[t2793]) ).
cnf(t744,plain,
sFlat8 = product(sFlat3,sFlat4),
inference(cp,[status(thm)],[t29,t742]) ).
cnf(t747,plain,
product(sFlat3,sFlat4) = sFlat8,
inference(orient,[status(thm)],[t744]) ).
cnf(t2685,plain,
product(sFlat3,sFlat5) = quotient(sFlat8,sFlat1),
inference(cp,[status(thm)],[t2680,t747]) ).
cnf(t2880,plain,
sFlat6 = quotient(sFlat8,sFlat1),
inference(step,[status(thm)],[t2685,t619]) ).
cnf(t2881,plain,
sFlat6 = sFlat9,
inference(step,[status(thm)],[t2880,t293]) ).
cnf(t2703,plain,
sFlat9 = sFlat6,
inference(orient,[status(thm)],[t2881]) ).
cnf(t2882,plain,
quotient(sFlat8,sFlat1) = sFlat6,
inference(step,[status(thm)],[t293,t2703]) ).
cnf(t2704,plain,
quotient(sFlat8,sFlat1) = sFlat6,
inference(orient,[status(thm)],[t2882]) ).
cnf(u8,negated_conjecture,
t(eta(x0),product(x1,x2)) != product(t(eta(x0),x1),t(eta(x0),x2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(d3,axiom,
t(A,B) = quotient(product(A,B),A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(goal_0,negated_conjecture,
product(quotient(product(product(difference(x0,one),x0),x1),product(difference(x0,one),x0)),quotient(product(product(difference(x0,one),x0),x2),product(difference(x0,one),x0))) != quotient(product(product(difference(x0,one),x0),product(x1,x2)),product(difference(x0,one),x0)),
inference(definition_unfolding,[status(thm)],[u8,d2,d3]) ).
cnf(g0_0,plain,
product(quotient(product(product(sFlat0,product(one,x0)),x1),product(difference(x0,one),x0)),quotient(product(product(difference(x0,one),x0),x2),product(difference(x0,one),x0))) != quotient(product(product(difference(x0,one),x0),product(x1,x2)),product(difference(x0,one),x0)),
inference(rw,[status(thm)],[goal_0,t1256]) ).
cnf(g0_1,plain,
product(quotient(product(product(sFlat0,x0),x1),product(difference(x0,one),x0)),quotient(product(product(difference(x0,one),x0),x2),product(difference(x0,one),x0))) != quotient(product(product(difference(x0,one),x0),product(x1,x2)),product(difference(x0,one),x0)),
inference(rw,[status(thm)],[g0_0,t27]) ).
cnf(g0_2,plain,
product(quotient(product(sFlat1,x1),product(difference(x0,one),x0)),quotient(product(product(difference(x0,one),x0),x2),product(difference(x0,one),x0))) != quotient(product(product(difference(x0,one),x0),product(x1,x2)),product(difference(x0,one),x0)),
inference(rw,[status(thm)],[g0_1,t225]) ).
cnf(g0_3,plain,
product(quotient(sFlat2,product(difference(x0,one),x0)),quotient(product(product(difference(x0,one),x0),x2),product(difference(x0,one),x0))) != quotient(product(product(difference(x0,one),x0),product(x1,x2)),product(difference(x0,one),x0)),
inference(rw,[status(thm)],[g0_2,t209]) ).
cnf(g0_4,plain,
product(quotient(sFlat2,product(sFlat0,product(one,x0))),quotient(product(product(difference(x0,one),x0),x2),product(difference(x0,one),x0))) != quotient(product(product(difference(x0,one),x0),product(x1,x2)),product(difference(x0,one),x0)),
inference(rw,[status(thm)],[g0_3,t1256]) ).
cnf(g0_5,plain,
product(quotient(sFlat2,product(sFlat0,x0)),quotient(product(product(difference(x0,one),x0),x2),product(difference(x0,one),x0))) != quotient(product(product(difference(x0,one),x0),product(x1,x2)),product(difference(x0,one),x0)),
inference(rw,[status(thm)],[g0_4,t27]) ).
cnf(g0_6,plain,
product(quotient(sFlat2,sFlat1),quotient(product(product(difference(x0,one),x0),x2),product(difference(x0,one),x0))) != quotient(product(product(difference(x0,one),x0),product(x1,x2)),product(difference(x0,one),x0)),
inference(rw,[status(thm)],[g0_5,t225]) ).
cnf(g0_7,plain,
product(sFlat3,quotient(product(product(difference(x0,one),x0),x2),product(difference(x0,one),x0))) != quotient(product(product(difference(x0,one),x0),product(x1,x2)),product(difference(x0,one),x0)),
inference(rw,[status(thm)],[g0_6,t238]) ).
cnf(g0_8,plain,
product(sFlat3,quotient(product(product(sFlat0,product(one,x0)),x2),product(difference(x0,one),x0))) != quotient(product(product(difference(x0,one),x0),product(x1,x2)),product(difference(x0,one),x0)),
inference(rw,[status(thm)],[g0_7,t1256]) ).
cnf(g0_9,plain,
product(sFlat3,quotient(product(product(sFlat0,x0),x2),product(difference(x0,one),x0))) != quotient(product(product(difference(x0,one),x0),product(x1,x2)),product(difference(x0,one),x0)),
inference(rw,[status(thm)],[g0_8,t27]) ).
cnf(g0_10,plain,
product(sFlat3,quotient(product(sFlat1,x2),product(difference(x0,one),x0))) != quotient(product(product(difference(x0,one),x0),product(x1,x2)),product(difference(x0,one),x0)),
inference(rw,[status(thm)],[g0_9,t225]) ).
cnf(g0_11,plain,
product(sFlat3,quotient(sFlat4,product(difference(x0,one),x0))) != quotient(product(product(difference(x0,one),x0),product(x1,x2)),product(difference(x0,one),x0)),
inference(rw,[status(thm)],[g0_10,t201]) ).
cnf(g0_12,plain,
product(sFlat3,quotient(sFlat4,product(sFlat0,product(one,x0)))) != quotient(product(product(difference(x0,one),x0),product(x1,x2)),product(difference(x0,one),x0)),
inference(rw,[status(thm)],[g0_11,t1256]) ).
cnf(g0_13,plain,
product(sFlat3,quotient(sFlat4,product(sFlat0,x0))) != quotient(product(product(difference(x0,one),x0),product(x1,x2)),product(difference(x0,one),x0)),
inference(rw,[status(thm)],[g0_12,t27]) ).
cnf(g0_14,plain,
product(sFlat3,quotient(sFlat4,sFlat1)) != quotient(product(product(difference(x0,one),x0),product(x1,x2)),product(difference(x0,one),x0)),
inference(rw,[status(thm)],[g0_13,t225]) ).
cnf(g0_15,plain,
product(sFlat3,sFlat5) != quotient(product(product(difference(x0,one),x0),product(x1,x2)),product(difference(x0,one),x0)),
inference(rw,[status(thm)],[g0_14,t234]) ).
cnf(g0_16,plain,
sFlat6 != quotient(product(product(difference(x0,one),x0),product(x1,x2)),product(difference(x0,one),x0)),
inference(rw,[status(thm)],[g0_15,t619]) ).
cnf(g0_17,plain,
sFlat6 != quotient(product(product(sFlat0,product(one,x0)),product(x1,x2)),product(difference(x0,one),x0)),
inference(rw,[status(thm)],[g0_16,t1256]) ).
cnf(g0_18,plain,
sFlat6 != quotient(product(product(sFlat0,x0),product(x1,x2)),product(difference(x0,one),x0)),
inference(rw,[status(thm)],[g0_17,t27]) ).
cnf(g0_19,plain,
sFlat6 != quotient(product(sFlat1,product(x1,x2)),product(difference(x0,one),x0)),
inference(rw,[status(thm)],[g0_18,t225]) ).
cnf(g0_20,plain,
sFlat6 != quotient(product(sFlat2,x2),product(difference(x0,one),x0)),
inference(rw,[status(thm)],[g0_19,t344]) ).
cnf(g0_21,plain,
sFlat6 != quotient(sFlat8,product(difference(x0,one),x0)),
inference(rw,[status(thm)],[g0_20,t355]) ).
cnf(g0_22,plain,
sFlat6 != quotient(sFlat8,product(sFlat0,product(one,x0))),
inference(rw,[status(thm)],[g0_21,t1256]) ).
cnf(g0_23,plain,
sFlat6 != quotient(sFlat8,product(sFlat0,x0)),
inference(rw,[status(thm)],[g0_22,t27]) ).
cnf(g0_24,plain,
sFlat6 != quotient(sFlat8,sFlat1),
inference(rw,[status(thm)],[g0_23,t225]) ).
cnf(g0_25,plain,
sFlat6 != sFlat6,
inference(rw,[status(thm)],[g0_24,t2704]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_25]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP768-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/5.39 % Computer : n014.cluster.edu
% 0.10/5.39 % Model : x86_64 x86_64
% 0.10/5.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.39 % Memory : 8046.5625MB
% 0.10/5.39 % OS : Linux 6.8.0-71-generic
% 0.10/5.39 % CPULimit : 300
% 0.10/5.39 % WCLimit : 300
% 0.10/5.39 % DateTime : Wed Sep 23 15:59:39 UTC 2026
% 0.10/5.39 % CPUTime :
% 0.10/5.39 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 16.48/7.78 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 16.48/7.78 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------