%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP772-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 : n004.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 184.87s 27.72s
% Output : CNFRefutation 184.87s
% Verified :
% SZS Type : Refutation
% Derivation depth : 50
% Number of leaves : 21
% Syntax : Number of clauses : 129 ( 129 unt; 0 nHn; 3 RR)
% Number of literals : 129 ( 128 equ; 2 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 3 con; 0-3 aty)
% Number of variables : 231 ( 6 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t10,axiom,
quotient(product(X1,X2),X1) = t(X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t307,plain,
quotient(product(X1,X2),X1) = t(X1,X2),
inference(orient,[status(thm)],[t10]) ).
cnf(t5,axiom,
product(X1,difference(X1,X2)) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t32,plain,
product(X1,difference(X1,X2)) = X2,
inference(orient,[status(thm)],[t5]) ).
cnf(t312,plain,
t(X1,difference(X1,X2)) = quotient(X2,X1),
inference(cp,[status(thm)],[t307,t32]) ).
cnf(t622,plain,
t(X1,difference(X1,X2)) = quotient(X2,X1),
inference(orient,[status(thm)],[t312]) ).
cnf(t4,axiom,
difference(X1,product(X1,X2)) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t42,plain,
difference(X1,product(X1,X2)) = X2,
inference(orient,[status(thm)],[t4]) ).
cnf(t22,axiom,
product(a(X1,X2,X3),difference(X3,product(a(X3,X1,X2),X3))) = one,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t196,plain,
product(a(X1,X2,X3),difference(X3,product(a(X3,X1,X2),X3))) = one,
inference(orient,[status(thm)],[t22]) ).
cnf(t201,plain,
difference(X1,product(a(X1,X2,X3),X1)) = difference(a(X2,X3,X1),one),
inference(cp,[status(thm)],[t42,t196]) ).
cnf(t2,axiom,
difference(X1,one) = i(X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t305,plain,
difference(X1,one) = i(X1),
inference(orient,[status(thm)],[t2]) ).
cnf(t357118,plain,
difference(X1,product(a(X1,X2,X3),X1)) = i(a(X2,X3,X1)),
inference(step,[status(thm)],[t201,t305]) ).
cnf(t19,axiom,
product(eta(X1),product(X1,X2)) = product(i(i(X1)),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t250,plain,
product(eta(X1),product(X1,X2)) = product(i(i(X1)),X2),
inference(orient,[status(thm)],[t19]) ).
cnf(t0,axiom,
product(X1,one) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t33,plain,
product(X1,one) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t256,plain,
product(i(i(X1)),one) = product(eta(X1),X1),
inference(cp,[status(thm)],[t250,t33]) ).
cnf(t353669,plain,
i(i(X1)) = product(eta(X1),X1),
inference(step,[status(thm)],[t256,t33]) ).
cnf(t530,plain,
product(eta(X1),X1) = i(i(X1)),
inference(orient,[status(thm)],[t353669]) ).
cnf(t9,axiom,
product(i(X1),X1) = product(X1,j(X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t91,plain,
product(i(X1),X1) = product(X1,j(X1)),
inference(orient,[status(thm)],[t9]) ).
cnf(t6,axiom,
product(i(X1),X1) = eta(X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t353651,plain,
product(X1,j(X1)) = eta(X1),
inference(step,[status(thm)],[t6,t91]) ).
cnf(t205,plain,
product(X1,j(X1)) = eta(X1),
inference(orient,[status(thm)],[t353651]) ).
cnf(t353652,plain,
product(i(X1),X1) = eta(X1),
inference(step,[status(thm)],[t91,t205]) ).
cnf(t206,plain,
product(i(X1),X1) = eta(X1),
inference(orient,[status(thm)],[t353652]) ).
cnf(t7,axiom,
product(quotient(X1,X2),X2) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t34,plain,
product(quotient(X1,X2),X2) = X1,
inference(orient,[status(thm)],[t7]) ).
cnf(t3,axiom,
quotient(one,X1) = j(X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t290,plain,
quotient(one,X1) = j(X1),
inference(orient,[status(thm)],[t3]) ).
cnf(t291,plain,
one = product(j(X1),X1),
inference(cp,[status(thm)],[t34,t290]) ).
cnf(t447,plain,
product(j(X1),X1) = one,
inference(orient,[status(thm)],[t291]) ).
cnf(t453,plain,
X1 = difference(j(X1),one),
inference(cp,[status(thm)],[t42,t447]) ).
cnf(t353662,plain,
X1 = i(j(X1)),
inference(step,[status(thm)],[t453,t305]) ).
cnf(t459,plain,
i(j(X1)) = X1,
inference(orient,[status(thm)],[t353662]) ).
cnf(t463,plain,
eta(j(X1)) = product(X1,j(X1)),
inference(cp,[status(thm)],[t206,t459]) ).
cnf(t353663,plain,
eta(j(X1)) = eta(X1),
inference(step,[status(thm)],[t463,t205]) ).
cnf(t465,plain,
eta(j(X1)) = eta(X1),
inference(orient,[status(thm)],[t353663]) ).
cnf(t532,plain,
i(i(j(X1))) = product(eta(X1),j(X1)),
inference(cp,[status(thm)],[t530,t465]) ).
cnf(t353675,plain,
i(X1) = product(eta(X1),j(X1)),
inference(step,[status(thm)],[t532,t459]) ).
cnf(t578,plain,
product(eta(X1),j(X1)) = i(X1),
inference(orient,[status(thm)],[t353675]) ).
cnf(t585,plain,
j(X1) = difference(eta(X1),i(X1)),
inference(cp,[status(thm)],[t42,t578]) ).
cnf(t607,plain,
difference(eta(X1),i(X1)) = j(X1),
inference(orient,[status(thm)],[t585]) ).
cnf(t8,axiom,
quotient(product(X1,X2),X2) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t38,plain,
quotient(product(X1,X2),X2) = X1,
inference(orient,[status(thm)],[t8]) ).
cnf(t28,axiom,
product(product(X1,X2),a(X3,X4,X5)) = product(X1,product(X2,a(X3,X4,X5))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t54,plain,
product(product(X1,X2),a(X3,X4,X5)) = product(X1,product(X2,a(X3,X4,X5))),
inference(orient,[status(thm)],[t28]) ).
cnf(t61,plain,
product(X1,X2) = quotient(product(X1,product(X2,a(X3,X4,X5))),a(X3,X4,X5)),
inference(cp,[status(thm)],[t38,t54]) ).
cnf(t9120,plain,
quotient(product(X1,product(X2,a(X3,X4,X5))),a(X3,X4,X5)) = product(X1,X2),
inference(orient,[status(thm)],[t61]) ).
cnf(t16,axiom,
product(j(j(X1)),j(product(X2,X1))) = j(X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t174,plain,
product(j(j(X1)),j(product(X2,X1))) = j(X2),
inference(orient,[status(thm)],[t16]) ).
cnf(t189,plain,
j(quotient(X1,X2)) = product(j(j(X2)),j(X1)),
inference(cp,[status(thm)],[t174,t34]) ).
cnf(t1141,plain,
product(j(j(X1)),j(X2)) = j(quotient(X2,X1)),
inference(orient,[status(thm)],[t189]) ).
cnf(t306,plain,
one = product(X1,i(X1)),
inference(cp,[status(thm)],[t32,t305]) ).
cnf(t469,plain,
product(X1,i(X1)) = one,
inference(orient,[status(thm)],[t306]) ).
cnf(t479,plain,
X1 = quotient(one,i(X1)),
inference(cp,[status(thm)],[t38,t469]) ).
cnf(t353664,plain,
X1 = j(i(X1)),
inference(step,[status(thm)],[t479,t290]) ).
cnf(t490,plain,
j(i(X1)) = X1,
inference(orient,[status(thm)],[t353664]) ).
cnf(t1145,plain,
j(quotient(X1,i(X2))) = product(j(X2),j(X1)),
inference(cp,[status(thm)],[t1141,t490]) ).
cnf(t1394,plain,
j(quotient(X1,i(X2))) = product(j(X2),j(X1)),
inference(orient,[status(thm)],[t1145]) ).
cnf(t18,axiom,
product(X1,product(eta(X1),X2)) = product(j(j(X1)),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t83,plain,
product(X1,product(eta(X1),X2)) = product(j(j(X1)),X2),
inference(orient,[status(thm)],[t18]) ).
cnf(t537,plain,
product(j(j(X1)),X1) = product(X1,i(i(X1))),
inference(cp,[status(thm)],[t83,t530]) ).
cnf(t12,axiom,
product(j(X1),i(X1)) = quotient(j(X1),X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t168,plain,
product(j(X1),i(X1)) = quotient(j(X1),X1),
inference(orient,[status(thm)],[t12]) ).
cnf(t494,plain,
quotient(j(i(X1)),i(X1)) = product(X1,i(i(X1))),
inference(cp,[status(thm)],[t168,t490]) ).
cnf(t353681,plain,
quotient(X1,i(X1)) = product(X1,i(i(X1))),
inference(step,[status(thm)],[t494,t490]) ).
cnf(t699,plain,
product(X1,i(i(X1))) = quotient(X1,i(X1)),
inference(orient,[status(thm)],[t353681]) ).
cnf(t353682,plain,
product(j(j(X1)),X1) = quotient(X1,i(X1)),
inference(step,[status(thm)],[t537,t699]) ).
cnf(t764,plain,
product(j(j(X1)),X1) = quotient(X1,i(X1)),
inference(orient,[status(thm)],[t353682]) ).
cnf(t772,plain,
j(j(X1)) = quotient(quotient(X1,i(X1)),X1),
inference(cp,[status(thm)],[t38,t764]) ).
cnf(t949,plain,
quotient(quotient(X1,i(X1)),X1) = j(j(X1)),
inference(orient,[status(thm)],[t772]) ).
cnf(t1396,plain,
product(j(X1),j(quotient(i(X1),i(i(X1))))) = j(j(j(i(X1)))),
inference(cp,[status(thm)],[t1394,t949]) ).
cnf(t1147,plain,
j(quotient(i(X1),X2)) = product(j(j(X2)),X1),
inference(cp,[status(thm)],[t1141,t490]) ).
cnf(t1446,plain,
j(quotient(i(X1),X2)) = product(j(j(X2)),X1),
inference(orient,[status(thm)],[t1147]) ).
cnf(t353731,plain,
product(j(X1),product(j(j(i(i(X1)))),X1)) = j(j(j(i(X1)))),
inference(step,[status(thm)],[t1396,t1446]) ).
cnf(t353732,plain,
product(j(X1),product(j(i(X1)),X1)) = j(j(j(i(X1)))),
inference(step,[status(thm)],[t353731,t490]) ).
cnf(t353733,plain,
product(j(X1),product(X1,X1)) = j(j(j(i(X1)))),
inference(step,[status(thm)],[t353732,t490]) ).
cnf(t353734,plain,
product(j(X1),product(X1,X1)) = j(j(X1)),
inference(step,[status(thm)],[t353733,t490]) ).
cnf(t1580,plain,
product(j(X1),product(X1,X1)) = j(j(X1)),
inference(orient,[status(thm)],[t353734]) ).
cnf(t1595,plain,
product(i(i(j(X1))),product(X1,X1)) = product(eta(j(X1)),j(j(X1))),
inference(cp,[status(thm)],[t250,t1580]) ).
cnf(t353738,plain,
product(i(X1),product(X1,X1)) = product(eta(j(X1)),j(j(X1))),
inference(step,[status(thm)],[t1595,t459]) ).
cnf(t353739,plain,
product(i(X1),product(X1,X1)) = i(j(X1)),
inference(step,[status(thm)],[t353738,t578]) ).
cnf(t353740,plain,
product(i(X1),product(X1,X1)) = X1,
inference(step,[status(thm)],[t353739,t459]) ).
cnf(t1713,plain,
product(i(X1),product(X1,X1)) = X1,
inference(orient,[status(thm)],[t353740]) ).
cnf(t9135,plain,
product(i(a(X1,X2,X3)),a(X1,X2,X3)) = quotient(a(X1,X2,X3),a(X1,X2,X3)),
inference(cp,[status(thm)],[t9120,t1713]) ).
cnf(t353858,plain,
eta(a(X1,X2,X3)) = quotient(a(X1,X2,X3),a(X1,X2,X3)),
inference(step,[status(thm)],[t9135,t206]) ).
cnf(t1,axiom,
product(one,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t36,plain,
product(one,X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t41,plain,
one = quotient(X1,X1),
inference(cp,[status(thm)],[t38,t36]) ).
cnf(t440,plain,
quotient(X1,X1) = one,
inference(orient,[status(thm)],[t41]) ).
cnf(t353859,plain,
eta(a(X1,X2,X3)) = one,
inference(step,[status(thm)],[t353858,t440]) ).
cnf(t9161,plain,
eta(a(X1,X2,X3)) = one,
inference(orient,[status(thm)],[t353859]) ).
cnf(t9172,plain,
j(a(X1,X2,X3)) = difference(one,i(a(X1,X2,X3))),
inference(cp,[status(thm)],[t607,t9161]) ).
cnf(t37,plain,
difference(one,X1) = X1,
inference(cp,[status(thm)],[t36,t32]) ).
cnf(t438,plain,
difference(one,X1) = X1,
inference(orient,[status(thm)],[t37]) ).
cnf(t353864,plain,
j(a(X1,X2,X3)) = i(a(X1,X2,X3)),
inference(step,[status(thm)],[t9172,t438]) ).
cnf(t9243,plain,
i(a(X1,X2,X3)) = j(a(X1,X2,X3)),
inference(orient,[status(thm)],[t353864]) ).
cnf(t357119,plain,
difference(X1,product(a(X1,X2,X3),X1)) = j(a(X2,X3,X1)),
inference(step,[status(thm)],[t357118,t9243]) ).
cnf(t352208,plain,
difference(X1,product(a(X1,X2,X3),X1)) = j(a(X2,X3,X1)),
inference(orient,[status(thm)],[t357119]) ).
cnf(t352232,plain,
quotient(product(a(X1,X2,X3),X1),X1) = t(X1,j(a(X2,X3,X1))),
inference(cp,[status(thm)],[t622,t352208]) ).
cnf(t357121,plain,
a(X1,X2,X3) = t(X1,j(a(X2,X3,X1))),
inference(step,[status(thm)],[t352232,t38]) ).
cnf(t352389,plain,
t(X1,j(a(X2,X3,X1))) = a(X1,X2,X3),
inference(orient,[status(thm)],[t357121]) ).
cnf(t14,axiom,
a(j(X1),X2,X3) = a(i(X1),X2,X3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t11,axiom,
a(j(X1),X2,X3) = a(X2,X3,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t292,plain,
a(j(X1),X2,X3) = a(X2,X3,X1),
inference(orient,[status(thm)],[t11]) ).
cnf(t353654,plain,
a(X2,X3,X1) = a(i(X1),X2,X3),
inference(step,[status(thm)],[t14,t292]) ).
cnf(t301,plain,
a(i(X1),X2,X3) = a(X2,X3,X1),
inference(orient,[status(thm)],[t353654]) ).
cnf(t352399,plain,
a(X1,i(X2),X3) = t(X1,j(a(X3,X1,X2))),
inference(cp,[status(thm)],[t352389,t301]) ).
cnf(t13,axiom,
a(X1,j(X2),X3) = a(X1,i(X2),X3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t296,plain,
a(X1,i(X2),X3) = a(X1,j(X2),X3),
inference(orient,[status(thm)],[t13]) ).
cnf(t357128,plain,
a(X1,j(X2),X3) = t(X1,j(a(X3,X1,X2))),
inference(step,[status(thm)],[t352399,t296]) ).
cnf(t353032,plain,
t(X1,j(a(X2,X1,X3))) = a(X1,j(X3),X2),
inference(orient,[status(thm)],[t357128]) ).
cnf(t353033,plain,
a(X1,j(X1),X2) = a(X1,X2,X1),
inference(cp,[status(thm)],[t353032,t352389]) ).
cnf(t353423,plain,
a(X1,j(X1),X2) = a(X1,X2,X1),
inference(orient,[status(thm)],[t353033]) ).
cnf(t460,plain,
a(X1,X2,j(X3)) = a(X3,X1,X2),
inference(cp,[status(thm)],[t301,t459]) ).
cnf(t684,plain,
a(X1,X2,j(X3)) = a(X3,X1,X2),
inference(orient,[status(thm)],[t460]) ).
cnf(t353425,plain,
a(X1,j(X2),X1) = a(X2,X1,j(X1)),
inference(cp,[status(thm)],[t353423,t684]) ).
cnf(t357135,plain,
a(X1,j(X2),X1) = a(X1,X2,X1),
inference(step,[status(thm)],[t353425,t684]) ).
cnf(t353524,plain,
a(X1,j(X2),X1) = a(X1,X2,X1),
inference(orient,[status(thm)],[t357135]) ).
cnf(t353564,plain,
a(X1,X1,j(X2)) = t(X1,j(a(X1,X2,X1))),
inference(cp,[status(thm)],[t352389,t353524]) ).
cnf(t357136,plain,
a(X2,X1,X1) = t(X1,j(a(X1,X2,X1))),
inference(step,[status(thm)],[t353564,t684]) ).
cnf(t357137,plain,
a(X2,X1,X1) = a(X1,X1,X2),
inference(step,[status(thm)],[t357136,t352389]) ).
cnf(t353569,plain,
a(X1,X2,X2) = a(X2,X2,X1),
inference(orient,[status(thm)],[t357137]) ).
cnf(goal_0,negated_conjecture,
a(x1,x1,x0) != a(x0,x1,x1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
a(x1,x1,x0) != a(x1,x1,x0),
inference(rw,[status(thm)],[goal_0,t353569]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP772-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/0.37 % Computer : n004.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Wed Sep 23 16:00:05 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 184.87/27.72 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 184.87/27.72 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------