%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP205-1 : TPTP v9.3.1. Released v2.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n016.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:25:41 PM UTC 2026
% Result : Unsatisfiable 15.60s 2.48s
% Output : CNFRefutation 15.60s
% Verified :
% SZS Type : Refutation
% Derivation depth : 63
% Number of leaves : 9
% Syntax : Number of clauses : 128 ( 128 unt; 0 nHn; 3 RR)
% Number of literals : 128 ( 127 equ; 2 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 : 8 ( 8 usr; 4 con; 0-2 aty)
% Number of variables : 281 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t8,axiom,
multiply(multiply(multiply(X1,X2),X1),X3) = multiply(X1,multiply(X2,multiply(X1,X3))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t23,plain,
multiply(multiply(multiply(X1,X2),X1),X3) = multiply(X1,multiply(X2,multiply(X1,X3))),
inference(orient,[status(thm)],[t8]) ).
cnf(t0,axiom,
multiply(X1,identity) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t10,plain,
multiply(X1,identity) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t25,plain,
multiply(X1,multiply(X2,multiply(X1,identity))) = multiply(multiply(X1,X2),X1),
inference(cp,[status(thm)],[t23,t10]) ).
cnf(t8561,plain,
multiply(X1,multiply(X2,X1)) = multiply(multiply(X1,X2),X1),
inference(step,[status(thm)],[t25,t10]) ).
cnf(t56,plain,
multiply(multiply(X1,X2),X1) = multiply(X1,multiply(X2,X1)),
inference(orient,[status(thm)],[t8561]) ).
cnf(t8562,plain,
multiply(multiply(X1,multiply(X2,X1)),X3) = multiply(X1,multiply(X2,multiply(X1,X3))),
inference(step,[status(thm)],[t23,t56]) ).
cnf(t64,plain,
multiply(multiply(X1,multiply(X2,X1)),X3) = multiply(X1,multiply(X2,multiply(X1,X3))),
inference(rw,[status(thm)],[t8562]) ).
cnf(t219,plain,
multiply(multiply(X1,multiply(X2,X1)),X3) = multiply(X1,multiply(X2,multiply(X1,X3))),
inference(orient,[status(thm)],[t64]) ).
cnf(t6,axiom,
multiply(right_division(X1,X2),X2) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t13,plain,
multiply(right_division(X1,X2),X2) = X1,
inference(orient,[status(thm)],[t6]) ).
cnf(t232,plain,
multiply(X1,multiply(right_division(X2,X1),multiply(X1,X3))) = multiply(multiply(X1,X2),X3),
inference(cp,[status(thm)],[t219,t13]) ).
cnf(t7,axiom,
right_division(multiply(X1,X2),X2) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t15,plain,
right_division(multiply(X1,X2),X2) = X1,
inference(orient,[status(thm)],[t7]) ).
cnf(t4,axiom,
left_division(X1,multiply(X1,X2)) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t19,plain,
left_division(X1,multiply(X1,X2)) = X2,
inference(orient,[status(thm)],[t4]) ).
cnf(t2,axiom,
multiply(X1,right_inverse(X1)) = identity,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t33,plain,
multiply(X1,right_inverse(X1)) = identity,
inference(orient,[status(thm)],[t2]) ).
cnf(t57,plain,
multiply(X1,multiply(right_inverse(X1),X1)) = multiply(identity,X1),
inference(cp,[status(thm)],[t56,t33]) ).
cnf(t1,axiom,
multiply(identity,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t11,plain,
multiply(identity,X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t8563,plain,
multiply(X1,multiply(right_inverse(X1),X1)) = X1,
inference(step,[status(thm)],[t57,t11]) ).
cnf(t65,plain,
multiply(X1,multiply(right_inverse(X1),X1)) = X1,
inference(orient,[status(thm)],[t8563]) ).
cnf(t68,plain,
multiply(right_inverse(X1),X1) = left_division(X1,X1),
inference(cp,[status(thm)],[t19,t65]) ).
cnf(t20,plain,
identity = left_division(X1,X1),
inference(cp,[status(thm)],[t19,t10]) ).
cnf(t49,plain,
left_division(X1,X1) = identity,
inference(orient,[status(thm)],[t20]) ).
cnf(t8564,plain,
multiply(right_inverse(X1),X1) = identity,
inference(step,[status(thm)],[t68,t49]) ).
cnf(t70,plain,
multiply(right_inverse(X1),X1) = identity,
inference(orient,[status(thm)],[t8564]) ).
cnf(t230,plain,
multiply(X1,multiply(right_inverse(X1),multiply(X1,X2))) = multiply(multiply(X1,identity),X2),
inference(cp,[status(thm)],[t219,t70]) ).
cnf(t8607,plain,
multiply(X1,multiply(right_inverse(X1),multiply(X1,X2))) = multiply(X1,X2),
inference(step,[status(thm)],[t230,t10]) ).
cnf(t499,plain,
multiply(X1,multiply(right_inverse(X1),multiply(X1,X2))) = multiply(X1,X2),
inference(orient,[status(thm)],[t8607]) ).
cnf(t5,axiom,
multiply(X1,left_division(X1,X2)) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t9,plain,
multiply(X1,left_division(X1,X2)) = X2,
inference(orient,[status(thm)],[t5]) ).
cnf(t507,plain,
multiply(X1,left_division(X1,X2)) = multiply(X1,multiply(right_inverse(X1),X2)),
inference(cp,[status(thm)],[t499,t9]) ).
cnf(t8608,plain,
X2 = multiply(X1,multiply(right_inverse(X1),X2)),
inference(step,[status(thm)],[t507,t9]) ).
cnf(t526,plain,
multiply(X1,multiply(right_inverse(X1),X2)) = X2,
inference(orient,[status(thm)],[t8608]) ).
cnf(t531,plain,
left_division(right_inverse(X1),X2) = multiply(X1,X2),
inference(cp,[status(thm)],[t526,t9]) ).
cnf(t548,plain,
left_division(right_inverse(X1),X2) = multiply(X1,X2),
inference(orient,[status(thm)],[t531]) ).
cnf(t58,plain,
multiply(X1,multiply(left_division(X1,X2),X1)) = multiply(X2,X1),
inference(cp,[status(thm)],[t56,t9]) ).
cnf(t80,plain,
multiply(X1,multiply(left_division(X1,X2),X1)) = multiply(X2,X1),
inference(orient,[status(thm)],[t58]) ).
cnf(t83,plain,
multiply(left_division(X1,X2),X1) = left_division(X1,multiply(X2,X1)),
inference(cp,[status(thm)],[t19,t80]) ).
cnf(t85,plain,
left_division(X1,multiply(X2,X1)) = multiply(left_division(X1,X2),X1),
inference(orient,[status(thm)],[t83]) ).
cnf(t550,plain,
multiply(X1,multiply(X2,right_inverse(X1))) = multiply(left_division(right_inverse(X1),X2),right_inverse(X1)),
inference(cp,[status(thm)],[t548,t85]) ).
cnf(t8618,plain,
multiply(X1,multiply(X2,right_inverse(X1))) = multiply(multiply(X1,X2),right_inverse(X1)),
inference(step,[status(thm)],[t550,t548]) ).
cnf(t764,plain,
multiply(multiply(X1,X2),right_inverse(X1)) = multiply(X1,multiply(X2,right_inverse(X1))),
inference(orient,[status(thm)],[t8618]) ).
cnf(t765,plain,
multiply(X1,multiply(multiply(X2,X1),right_inverse(X1))) = multiply(X1,multiply(X2,multiply(X1,right_inverse(X1)))),
inference(cp,[status(thm)],[t764,t219]) ).
cnf(t8628,plain,
multiply(X1,multiply(multiply(X2,X1),right_inverse(X1))) = multiply(X1,multiply(X2,identity)),
inference(step,[status(thm)],[t765,t33]) ).
cnf(t8629,plain,
multiply(X1,multiply(multiply(X2,X1),right_inverse(X1))) = multiply(X1,X2),
inference(step,[status(thm)],[t8628,t10]) ).
cnf(t1003,plain,
multiply(X1,multiply(multiply(X2,X1),right_inverse(X1))) = multiply(X1,X2),
inference(orient,[status(thm)],[t8629]) ).
cnf(t1017,plain,
multiply(right_inverse(X1),multiply(X1,X2)) = multiply(right_inverse(X1),multiply(multiply(X1,multiply(X2,right_inverse(X1))),right_inverse(right_inverse(X1)))),
inference(cp,[status(thm)],[t1003,t764]) ).
cnf(t538,plain,
multiply(right_inverse(X1),X2) = left_division(X1,X2),
inference(cp,[status(thm)],[t19,t526]) ).
cnf(t563,plain,
multiply(right_inverse(X1),X2) = left_division(X1,X2),
inference(orient,[status(thm)],[t538]) ).
cnf(t8630,plain,
left_division(X1,multiply(X1,X2)) = multiply(right_inverse(X1),multiply(multiply(X1,multiply(X2,right_inverse(X1))),right_inverse(right_inverse(X1)))),
inference(step,[status(thm)],[t1017,t563]) ).
cnf(t8631,plain,
X2 = multiply(right_inverse(X1),multiply(multiply(X1,multiply(X2,right_inverse(X1))),right_inverse(right_inverse(X1)))),
inference(step,[status(thm)],[t8630,t19]) ).
cnf(t8632,plain,
X2 = left_division(X1,multiply(multiply(X1,multiply(X2,right_inverse(X1))),right_inverse(right_inverse(X1)))),
inference(step,[status(thm)],[t8631,t563]) ).
cnf(t72,plain,
X1 = left_division(right_inverse(X1),identity),
inference(cp,[status(thm)],[t19,t70]) ).
cnf(t36,plain,
right_inverse(X1) = left_division(X1,identity),
inference(cp,[status(thm)],[t19,t33]) ).
cnf(t50,plain,
left_division(X1,identity) = right_inverse(X1),
inference(orient,[status(thm)],[t36]) ).
cnf(t8570,plain,
X1 = right_inverse(right_inverse(X1)),
inference(step,[status(thm)],[t72,t50]) ).
cnf(t79,plain,
right_inverse(right_inverse(X1)) = X1,
inference(orient,[status(thm)],[t8570]) ).
cnf(t8633,plain,
X2 = left_division(X1,multiply(multiply(X1,multiply(X2,right_inverse(X1))),X1)),
inference(step,[status(thm)],[t8632,t79]) ).
cnf(t8634,plain,
X2 = left_division(X1,multiply(X1,multiply(multiply(X2,right_inverse(X1)),X1))),
inference(step,[status(thm)],[t8633,t56]) ).
cnf(t8635,plain,
X2 = multiply(multiply(X2,right_inverse(X1)),X1),
inference(step,[status(thm)],[t8634,t19]) ).
cnf(t1044,plain,
multiply(multiply(X1,right_inverse(X2)),X2) = X1,
inference(orient,[status(thm)],[t8635]) ).
cnf(t1061,plain,
multiply(X1,right_inverse(X2)) = right_division(X1,X2),
inference(cp,[status(thm)],[t15,t1044]) ).
cnf(t1091,plain,
multiply(X1,right_inverse(X2)) = right_division(X1,X2),
inference(orient,[status(thm)],[t1061]) ).
cnf(t16,plain,
X1 = right_division(X2,left_division(X1,X2)),
inference(cp,[status(thm)],[t15,t9]) ).
cnf(t54,plain,
right_division(X1,left_division(X2,X1)) = X2,
inference(orient,[status(thm)],[t16]) ).
cnf(t556,plain,
right_inverse(X1) = right_division(X2,multiply(X1,X2)),
inference(cp,[status(thm)],[t54,t548]) ).
cnf(t586,plain,
right_division(X1,multiply(X2,X1)) = right_inverse(X2),
inference(orient,[status(thm)],[t556]) ).
cnf(t593,plain,
right_inverse(right_division(X1,X2)) = right_division(X2,X1),
inference(cp,[status(thm)],[t586,t13]) ).
cnf(t600,plain,
right_inverse(right_division(X1,X2)) = right_division(X2,X1),
inference(orient,[status(thm)],[t593]) ).
cnf(t1050,plain,
right_division(X1,right_inverse(X2)) = multiply(X1,X2),
inference(cp,[status(thm)],[t1044,t13]) ).
cnf(t1072,plain,
right_division(X1,right_inverse(X2)) = multiply(X1,X2),
inference(orient,[status(thm)],[t1050]) ).
cnf(t1085,plain,
right_division(right_inverse(X1),X2) = right_inverse(multiply(X2,X1)),
inference(cp,[status(thm)],[t600,t1072]) ).
cnf(t1119,plain,
right_inverse(multiply(X1,X2)) = right_division(right_inverse(X2),X1),
inference(orient,[status(thm)],[t1085]) ).
cnf(t1127,plain,
right_division(right_inverse(X1),right_inverse(X2)) = right_inverse(left_division(X2,X1)),
inference(cp,[status(thm)],[t1119,t563]) ).
cnf(t8644,plain,
multiply(right_inverse(X1),X2) = right_inverse(left_division(X2,X1)),
inference(step,[status(thm)],[t1127,t1072]) ).
cnf(t8645,plain,
left_division(X1,X2) = right_inverse(left_division(X2,X1)),
inference(step,[status(thm)],[t8644,t563]) ).
cnf(t1143,plain,
right_inverse(left_division(X1,X2)) = left_division(X2,X1),
inference(orient,[status(thm)],[t8645]) ).
cnf(t1153,plain,
right_division(X1,left_division(X2,X3)) = multiply(X1,left_division(X3,X2)),
inference(cp,[status(thm)],[t1091,t1143]) ).
cnf(t1496,plain,
multiply(X1,left_division(X2,X3)) = right_division(X1,left_division(X3,X2)),
inference(orient,[status(thm)],[t1153]) ).
cnf(t610,plain,
left_division(right_division(X1,X2),X3) = multiply(right_division(X2,X1),X3),
inference(cp,[status(thm)],[t563,t600]) ).
cnf(t635,plain,
left_division(right_division(X1,X2),X3) = multiply(right_division(X2,X1),X3),
inference(orient,[status(thm)],[t610]) ).
cnf(t1504,plain,
right_division(X1,left_division(X2,right_division(X3,Y3))) = multiply(X1,multiply(right_division(Y3,X3),X2)),
inference(cp,[status(thm)],[t1496,t635]) ).
cnf(t3459,plain,
multiply(X1,multiply(right_division(X2,X3),Y3)) = right_division(X1,left_division(Y3,right_division(X3,X2))),
inference(orient,[status(thm)],[t1504]) ).
cnf(t8901,plain,
right_division(X1,left_division(multiply(X1,X3),right_division(X1,X2))) = multiply(multiply(X1,X2),X3),
inference(step,[status(thm)],[t232,t3459]) ).
cnf(t8275,plain,
right_division(X1,left_division(multiply(X1,X2),right_division(X1,X3))) = multiply(multiply(X1,X3),X2),
inference(orient,[status(thm)],[t8901]) ).
cnf(t578,plain,
multiply(X1,multiply(right_inverse(X2),multiply(X1,X3))) = multiply(multiply(X1,left_division(X2,X1)),X3),
inference(cp,[status(thm)],[t219,t563]) ).
cnf(t8701,plain,
multiply(X1,left_division(X2,multiply(X1,X3))) = multiply(multiply(X1,left_division(X2,X1)),X3),
inference(step,[status(thm)],[t578,t563]) ).
cnf(t8702,plain,
right_division(X1,left_division(multiply(X1,X3),X2)) = multiply(multiply(X1,left_division(X2,X1)),X3),
inference(step,[status(thm)],[t8701,t1496]) ).
cnf(t8703,plain,
right_division(X1,left_division(multiply(X1,X3),X2)) = multiply(right_division(X1,left_division(X1,X2)),X3),
inference(step,[status(thm)],[t8702,t1496]) ).
cnf(t2654,plain,
multiply(right_division(X1,left_division(X1,X2)),X3) = right_division(X1,left_division(multiply(X1,X3),X2)),
inference(orient,[status(thm)],[t8703]) ).
cnf(t1084,plain,
multiply(right_division(right_inverse(X1),X2),X3) = left_division(multiply(X2,X1),X3),
inference(cp,[status(thm)],[t635,t1072]) ).
cnf(t1684,plain,
multiply(right_division(right_inverse(X1),X2),X3) = left_division(multiply(X2,X1),X3),
inference(orient,[status(thm)],[t1084]) ).
cnf(t2657,plain,
right_division(right_inverse(X1),left_division(multiply(right_inverse(X1),X2),X3)) = left_division(multiply(left_division(right_inverse(X1),X3),X1),X2),
inference(cp,[status(thm)],[t2654,t1684]) ).
cnf(t1098,plain,
right_division(right_inverse(X1),X2) = left_division(X1,right_inverse(X2)),
inference(cp,[status(thm)],[t1091,t563]) ).
cnf(t1164,plain,
left_division(X1,right_inverse(X2)) = right_division(right_inverse(X1),X2),
inference(orient,[status(thm)],[t1098]) ).
cnf(t1168,plain,
right_division(right_inverse(X1),left_division(X2,X3)) = left_division(X1,left_division(X3,X2)),
inference(cp,[status(thm)],[t1164,t1143]) ).
cnf(t1763,plain,
right_division(right_inverse(X1),left_division(X2,X3)) = left_division(X1,left_division(X3,X2)),
inference(orient,[status(thm)],[t1168]) ).
cnf(t8768,plain,
left_division(X1,left_division(X3,multiply(right_inverse(X1),X2))) = left_division(multiply(left_division(right_inverse(X1),X3),X1),X2),
inference(step,[status(thm)],[t2657,t1763]) ).
cnf(t8769,plain,
left_division(X1,left_division(X3,left_division(X1,X2))) = left_division(multiply(left_division(right_inverse(X1),X3),X1),X2),
inference(step,[status(thm)],[t8768,t563]) ).
cnf(t1155,plain,
left_division(left_division(X1,X2),X3) = multiply(left_division(X2,X1),X3),
inference(cp,[status(thm)],[t563,t1143]) ).
cnf(t1529,plain,
left_division(left_division(X1,X2),X3) = multiply(left_division(X2,X1),X3),
inference(orient,[status(thm)],[t1155]) ).
cnf(t1540,plain,
multiply(left_division(X1,left_division(X2,X3)),Y3) = left_division(multiply(left_division(X3,X2),X1),Y3),
inference(cp,[status(thm)],[t1529,t1529]) ).
cnf(t3779,plain,
left_division(multiply(left_division(X1,X2),X3),Y3) = multiply(left_division(X3,left_division(X2,X1)),Y3),
inference(orient,[status(thm)],[t1540]) ).
cnf(t8770,plain,
left_division(X1,left_division(X3,left_division(X1,X2))) = multiply(left_division(X1,left_division(X3,right_inverse(X1))),X2),
inference(step,[status(thm)],[t8769,t3779]) ).
cnf(t8771,plain,
left_division(X1,left_division(X3,left_division(X1,X2))) = multiply(left_division(X1,right_division(right_inverse(X3),X1)),X2),
inference(step,[status(thm)],[t8770,t1164]) ).
cnf(t1169,plain,
right_division(right_inverse(X1),multiply(X2,X3)) = left_division(X1,right_division(right_inverse(X3),X2)),
inference(cp,[status(thm)],[t1164,t1119]) ).
cnf(t2092,plain,
left_division(X1,right_division(right_inverse(X2),X3)) = right_division(right_inverse(X1),multiply(X3,X2)),
inference(orient,[status(thm)],[t1169]) ).
cnf(t8772,plain,
left_division(X1,left_division(X3,left_division(X1,X2))) = multiply(right_division(right_inverse(X1),multiply(X1,X3)),X2),
inference(step,[status(thm)],[t8771,t2092]) ).
cnf(t8773,plain,
left_division(X1,left_division(X3,left_division(X1,X2))) = left_division(multiply(multiply(X1,X3),X1),X2),
inference(step,[status(thm)],[t8772,t1684]) ).
cnf(t8774,plain,
left_division(X1,left_division(X3,left_division(X1,X2))) = left_division(multiply(X1,multiply(X3,X1)),X2),
inference(step,[status(thm)],[t8773,t56]) ).
cnf(t5049,plain,
left_division(multiply(X1,multiply(X2,X1)),X3) = left_division(X1,left_division(X2,left_division(X1,X3))),
inference(orient,[status(thm)],[t8774]) ).
cnf(t8279,plain,
multiply(multiply(X1,X2),multiply(X3,X1)) = right_division(X1,left_division(X1,left_division(X3,left_division(X1,right_division(X1,X2))))),
inference(cp,[status(thm)],[t8275,t5049]) ).
cnf(t1108,plain,
right_inverse(X1) = left_division(X2,right_division(X2,X1)),
inference(cp,[status(thm)],[t19,t1091]) ).
cnf(t1183,plain,
left_division(X1,right_division(X1,X2)) = right_inverse(X2),
inference(orient,[status(thm)],[t1108]) ).
cnf(t8902,plain,
multiply(multiply(X1,X2),multiply(X3,X1)) = right_division(X1,left_division(X1,left_division(X3,right_inverse(X2)))),
inference(step,[status(thm)],[t8279,t1183]) ).
cnf(t8903,plain,
multiply(multiply(X1,X2),multiply(X3,X1)) = right_division(X1,left_division(X1,right_division(right_inverse(X3),X2))),
inference(step,[status(thm)],[t8902,t1164]) ).
cnf(t8904,plain,
multiply(multiply(X1,X2),multiply(X3,X1)) = right_division(X1,right_division(right_inverse(X1),multiply(X2,X3))),
inference(step,[status(thm)],[t8903,t2092]) ).
cnf(t1134,plain,
multiply(X1,multiply(X2,X3)) = right_division(X1,right_division(right_inverse(X3),X2)),
inference(cp,[status(thm)],[t1072,t1119]) ).
cnf(t1715,plain,
right_division(X1,right_division(right_inverse(X2),X3)) = multiply(X1,multiply(X3,X2)),
inference(orient,[status(thm)],[t1134]) ).
cnf(t8905,plain,
multiply(multiply(X1,X2),multiply(X3,X1)) = multiply(X1,multiply(multiply(X2,X3),X1)),
inference(step,[status(thm)],[t8904,t1715]) ).
cnf(t8421,plain,
multiply(multiply(X1,X2),multiply(X3,X1)) = multiply(X1,multiply(multiply(X2,X3),X1)),
inference(orient,[status(thm)],[t8905]) ).
cnf(goal_0,negated_conjecture,
multiply(x,multiply(multiply(y,z),x)) != multiply(multiply(x,y),multiply(z,x)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
multiply(x,multiply(multiply(y,z),x)) != multiply(x,multiply(multiply(y,z),x)),
inference(rw,[status(thm)],[goal_0,t8421]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP205-1 : TPTP v9.3.1. Released v2.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n016.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.37 % DateTime : Wed Sep 23 14:12:57 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 15.60/2.48 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 15.60/2.48 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------