%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : GRP479-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n002.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:27:08 PM UTC 2026
% Result : Unsatisfiable 5.28s 1.57s
% Output : CNFRefutation 5.28s
% Verified :
% SZS Type : Refutation
% Derivation depth : 110
% Number of leaves : 7
% Syntax : Number of clauses : 248 ( 248 unt; 0 nHn; 99 RR)
% Number of literals : 248 ( 247 equ; 5 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 6 con; 0-2 aty)
% Number of variables : 216 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t0,axiom,
divide(inverse(divide(divide(divide(X1,X1),X2),divide(X3,divide(X2,X4)))),X4) = X3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t5,plain,
divide(inverse(divide(divide(divide(X1,X1),X2),divide(X3,divide(X2,X4)))),X4) = X3,
inference(orient,[status(thm)],[t0]) ).
cnf(t2,axiom,
sFlat1 = divide(inverse(b2),inverse(b2)),
introduced(definition) ).
cnf(t11,plain,
divide(inverse(b2),inverse(b2)) = sFlat1,
inference(orient,[status(thm)],[t2]) ).
cnf(t1,axiom,
sFlat0 = inverse(b2),
introduced(definition) ).
cnf(t15,plain,
inverse(b2) = sFlat0,
inference(orient,[status(thm)],[t1]) ).
cnf(t1884,plain,
divide(sFlat0,inverse(b2)) = sFlat1,
inference(step,[status(thm)],[t11,t15]) ).
cnf(t1885,plain,
divide(sFlat0,sFlat0) = sFlat1,
inference(step,[status(thm)],[t1884,t15]) ).
cnf(t16,plain,
divide(sFlat0,sFlat0) = sFlat1,
inference(rw,[status(thm)],[t1885]) ).
cnf(t18,plain,
divide(sFlat0,sFlat0) = sFlat1,
inference(orient,[status(thm)],[t16]) ).
cnf(t19,plain,
X1 = divide(inverse(divide(divide(sFlat1,X2),divide(X1,divide(X2,X3)))),X3),
inference(cp,[status(thm)],[t5,t18]) ).
cnf(t23,plain,
divide(inverse(divide(divide(sFlat1,X1),divide(X2,divide(X1,X3)))),X3) = X2,
inference(orient,[status(thm)],[t19]) ).
cnf(t4,axiom,
sFlat3 = divide(divide(inverse(b2),inverse(b2)),inverse(a2)),
introduced(definition) ).
cnf(t8,plain,
divide(divide(inverse(b2),inverse(b2)),inverse(a2)) = sFlat3,
inference(orient,[status(thm)],[t4]) ).
cnf(t1883,plain,
divide(sFlat1,inverse(a2)) = sFlat3,
inference(step,[status(thm)],[t8,t11]) ).
cnf(t14,plain,
divide(sFlat1,inverse(a2)) = sFlat3,
inference(rw,[status(thm)],[t1883]) ).
cnf(t3,axiom,
sFlat2 = inverse(a2),
introduced(definition) ).
cnf(t17,plain,
inverse(a2) = sFlat2,
inference(orient,[status(thm)],[t3]) ).
cnf(t1886,plain,
divide(sFlat1,sFlat2) = sFlat3,
inference(step,[status(thm)],[t14,t17]) ).
cnf(t21,plain,
divide(sFlat1,sFlat2) = sFlat3,
inference(orient,[status(thm)],[t1886]) ).
cnf(t24,plain,
X1 = divide(inverse(divide(sFlat3,divide(X1,divide(sFlat2,X2)))),X2),
inference(cp,[status(thm)],[t23,t21]) ).
cnf(t33,plain,
divide(inverse(divide(sFlat3,divide(X1,divide(sFlat2,X2)))),X2) = X1,
inference(orient,[status(thm)],[t24]) ).
cnf(t39,plain,
inverse(divide(sFlat3,divide(X1,divide(sFlat2,divide(X2,X3))))) = divide(inverse(divide(divide(sFlat1,X2),X1)),X3),
inference(cp,[status(thm)],[t23,t33]) ).
cnf(t113,plain,
inverse(divide(sFlat3,divide(X1,divide(sFlat2,divide(X2,X3))))) = divide(inverse(divide(divide(sFlat1,X2),X1)),X3),
inference(orient,[status(thm)],[t39]) ).
cnf(t127,plain,
X1 = divide(divide(inverse(divide(divide(sFlat1,X2),X1)),X3),divide(X2,X3)),
inference(cp,[status(thm)],[t33,t113]) ).
cnf(t128,plain,
divide(divide(inverse(divide(divide(sFlat1,X1),X2)),X3),divide(X1,X3)) = X2,
inference(orient,[status(thm)],[t127]) ).
cnf(t137,plain,
X1 = divide(divide(inverse(divide(divide(sFlat1,inverse(divide(divide(sFlat1,X2),divide(X3,divide(X2,X4))))),X1)),X4),X3),
inference(cp,[status(thm)],[t128,t23]) ).
cnf(t1703,plain,
divide(divide(inverse(divide(divide(sFlat1,inverse(divide(divide(sFlat1,X1),divide(X2,divide(X1,X3))))),X4)),X3),X2) = X4,
inference(orient,[status(thm)],[t137]) ).
cnf(t26,plain,
X1 = divide(inverse(divide(divide(sFlat1,sFlat1),divide(X1,sFlat3))),sFlat2),
inference(cp,[status(thm)],[t23,t21]) ).
cnf(t41,plain,
divide(inverse(divide(divide(sFlat1,sFlat1),divide(X1,sFlat3))),sFlat2) = X1,
inference(orient,[status(thm)],[t26]) ).
cnf(t44,plain,
inverse(divide(divide(sFlat1,X1),divide(X2,divide(X1,sFlat3)))) = divide(inverse(divide(divide(sFlat1,sFlat1),X2)),sFlat2),
inference(cp,[status(thm)],[t41,t23]) ).
cnf(t145,plain,
inverse(divide(divide(sFlat1,X1),divide(X2,divide(X1,sFlat3)))) = divide(inverse(divide(divide(sFlat1,sFlat1),X2)),sFlat2),
inference(orient,[status(thm)],[t44]) ).
cnf(t28,plain,
X1 = divide(inverse(divide(divide(sFlat1,sFlat0),divide(X1,sFlat1))),sFlat0),
inference(cp,[status(thm)],[t23,t18]) ).
cnf(t47,plain,
divide(inverse(divide(divide(sFlat1,sFlat0),divide(X1,sFlat1))),sFlat0) = X1,
inference(orient,[status(thm)],[t28]) ).
cnf(t48,plain,
inverse(divide(sFlat3,divide(X1,divide(sFlat2,sFlat1)))) = divide(inverse(divide(divide(sFlat1,sFlat0),X1)),sFlat0),
inference(cp,[status(thm)],[t47,t33]) ).
cnf(t61,plain,
inverse(divide(sFlat3,divide(X1,divide(sFlat2,sFlat1)))) = divide(inverse(divide(divide(sFlat1,sFlat0),X1)),sFlat0),
inference(orient,[status(thm)],[t48]) ).
cnf(t65,plain,
X1 = divide(divide(inverse(divide(divide(sFlat1,sFlat0),X1)),sFlat0),sFlat1),
inference(cp,[status(thm)],[t33,t61]) ).
cnf(t66,plain,
divide(divide(inverse(divide(divide(sFlat1,sFlat0),X1)),sFlat0),sFlat1) = X1,
inference(orient,[status(thm)],[t65]) ).
cnf(t153,plain,
divide(X1,divide(sFlat0,sFlat3)) = divide(divide(divide(inverse(divide(divide(sFlat1,sFlat1),X1)),sFlat2),sFlat0),sFlat1),
inference(cp,[status(thm)],[t66,t145]) ).
cnf(t205,plain,
divide(divide(divide(inverse(divide(divide(sFlat1,sFlat1),X1)),sFlat2),sFlat0),sFlat1) = divide(X1,divide(sFlat0,sFlat3)),
inference(orient,[status(thm)],[t153]) ).
cnf(t206,plain,
divide(divide(X1,sFlat3),divide(sFlat0,sFlat3)) = divide(divide(X1,sFlat0),sFlat1),
inference(cp,[status(thm)],[t205,t41]) ).
cnf(t214,plain,
divide(divide(X1,sFlat3),divide(sFlat0,sFlat3)) = divide(divide(X1,sFlat0),sFlat1),
inference(orient,[status(thm)],[t206]) ).
cnf(t216,plain,
divide(inverse(divide(divide(sFlat1,sFlat1),divide(X1,sFlat3))),sFlat2) = inverse(divide(divide(sFlat1,sFlat0),divide(divide(X1,sFlat0),sFlat1))),
inference(cp,[status(thm)],[t145,t214]) ).
cnf(t1889,plain,
X1 = inverse(divide(divide(sFlat1,sFlat0),divide(divide(X1,sFlat0),sFlat1))),
inference(step,[status(thm)],[t216,t41]) ).
cnf(t222,plain,
inverse(divide(divide(sFlat1,sFlat0),divide(divide(X1,sFlat0),sFlat1))) = X1,
inference(orient,[status(thm)],[t1889]) ).
cnf(t226,plain,
divide(divide(X1,sFlat0),sFlat1) = divide(divide(X1,X2),divide(sFlat0,X2)),
inference(cp,[status(thm)],[t128,t222]) ).
cnf(t233,plain,
divide(divide(X1,X2),divide(sFlat0,X2)) = divide(divide(X1,sFlat0),sFlat1),
inference(orient,[status(thm)],[t226]) ).
cnf(t239,plain,
divide(divide(sFlat1,sFlat0),sFlat1) = divide(sFlat3,divide(sFlat0,sFlat2)),
inference(cp,[status(thm)],[t233,t21]) ).
cnf(t251,plain,
divide(divide(sFlat1,sFlat0),sFlat1) = divide(sFlat3,divide(sFlat0,sFlat2)),
inference(orient,[status(thm)],[t239]) ).
cnf(t256,plain,
sFlat1 = divide(divide(inverse(divide(sFlat3,divide(sFlat0,sFlat2))),X1),divide(sFlat0,X1)),
inference(cp,[status(thm)],[t128,t251]) ).
cnf(t1890,plain,
sFlat1 = divide(divide(inverse(divide(sFlat3,divide(sFlat0,sFlat2))),sFlat0),sFlat1),
inference(step,[status(thm)],[t256,t233]) ).
cnf(t262,plain,
divide(divide(inverse(divide(sFlat3,divide(sFlat0,sFlat2))),sFlat0),sFlat1) = sFlat1,
inference(orient,[status(thm)],[t1890]) ).
cnf(t38,plain,
inverse(divide(sFlat3,divide(X1,divide(sFlat2,divide(sFlat2,X2))))) = divide(inverse(divide(sFlat3,X1)),X2),
inference(cp,[status(thm)],[t33,t33]) ).
cnf(t83,plain,
inverse(divide(sFlat3,divide(X1,divide(sFlat2,divide(sFlat2,X2))))) = divide(inverse(divide(sFlat3,X1)),X2),
inference(orient,[status(thm)],[t38]) ).
cnf(t86,plain,
X1 = divide(divide(inverse(divide(sFlat3,X1)),X2),divide(sFlat2,X2)),
inference(cp,[status(thm)],[t33,t83]) ).
cnf(t87,plain,
divide(divide(inverse(divide(sFlat3,X1)),X2),divide(sFlat2,X2)) = X1,
inference(orient,[status(thm)],[t86]) ).
cnf(t31,plain,
inverse(divide(divide(sFlat1,X1),divide(X2,divide(X1,divide(X3,X4))))) = divide(inverse(divide(divide(sFlat1,X3),X2)),X4),
inference(cp,[status(thm)],[t23,t23]) ).
cnf(t334,plain,
inverse(divide(divide(sFlat1,X1),divide(X2,divide(X1,divide(X3,X4))))) = divide(inverse(divide(divide(sFlat1,X3),X2)),X4),
inference(orient,[status(thm)],[t31]) ).
cnf(t225,plain,
sFlat0 = inverse(divide(divide(sFlat1,sFlat0),divide(sFlat1,sFlat1))),
inference(cp,[status(thm)],[t222,t18]) ).
cnf(t227,plain,
inverse(divide(divide(sFlat1,sFlat0),divide(sFlat1,sFlat1))) = sFlat0,
inference(orient,[status(thm)],[t225]) ).
cnf(t223,plain,
inverse(divide(sFlat3,divide(X1,divide(sFlat2,sFlat0)))) = inverse(divide(divide(sFlat1,sFlat0),divide(X1,sFlat1))),
inference(cp,[status(thm)],[t222,t33]) ).
cnf(t270,plain,
inverse(divide(divide(sFlat1,sFlat0),divide(X1,sFlat1))) = inverse(divide(sFlat3,divide(X1,divide(sFlat2,sFlat0)))),
inference(orient,[status(thm)],[t223]) ).
cnf(t1891,plain,
inverse(divide(sFlat3,divide(sFlat1,divide(sFlat2,sFlat0)))) = sFlat0,
inference(step,[status(thm)],[t227,t270]) ).
cnf(t276,plain,
inverse(divide(sFlat3,divide(sFlat1,divide(sFlat2,sFlat0)))) = sFlat0,
inference(rw,[status(thm)],[t1891]) ).
cnf(t278,plain,
inverse(divide(sFlat3,divide(sFlat1,divide(sFlat2,sFlat0)))) = sFlat0,
inference(orient,[status(thm)],[t276]) ).
cnf(t279,plain,
divide(sFlat1,divide(sFlat2,sFlat0)) = divide(divide(sFlat0,X1),divide(sFlat2,X1)),
inference(cp,[status(thm)],[t87,t278]) ).
cnf(t280,plain,
divide(divide(sFlat0,X1),divide(sFlat2,X1)) = divide(sFlat1,divide(sFlat2,sFlat0)),
inference(orient,[status(thm)],[t279]) ).
cnf(t244,plain,
divide(sFlat0,X1) = divide(divide(inverse(divide(divide(sFlat1,sFlat0),sFlat1)),X2),divide(X1,X2)),
inference(cp,[status(thm)],[t128,t233]) ).
cnf(t1897,plain,
divide(sFlat0,X1) = divide(divide(inverse(divide(sFlat3,divide(sFlat0,sFlat2))),X2),divide(X1,X2)),
inference(step,[status(thm)],[t244,t251]) ).
cnf(t371,plain,
divide(divide(inverse(divide(sFlat3,divide(sFlat0,sFlat2))),X1),divide(X2,X1)) = divide(sFlat0,X2),
inference(orient,[status(thm)],[t1897]) ).
cnf(t140,plain,
divide(inverse(divide(divide(sFlat1,X1),X2)),X3) = divide(inverse(divide(divide(divide(X4,X4),X1),X2)),X3),
inference(cp,[status(thm)],[t5,t128]) ).
cnf(t175,plain,
divide(inverse(divide(divide(divide(X1,X1),X2),X3)),X4) = divide(inverse(divide(divide(sFlat1,X2),X3)),X4),
inference(orient,[status(thm)],[t140]) ).
cnf(t178,plain,
inverse(divide(divide(divide(X1,X1),X2),X3)) = divide(inverse(divide(divide(sFlat1,sFlat1),divide(inverse(divide(divide(sFlat1,X2),X3)),sFlat3))),sFlat2),
inference(cp,[status(thm)],[t41,t175]) ).
cnf(t1888,plain,
inverse(divide(divide(divide(X1,X1),X2),X3)) = inverse(divide(divide(sFlat1,X2),X3)),
inference(step,[status(thm)],[t178,t41]) ).
cnf(t194,plain,
inverse(divide(divide(divide(X1,X1),X2),X3)) = inverse(divide(divide(sFlat1,X2),X3)),
inference(orient,[status(thm)],[t1888]) ).
cnf(t196,plain,
inverse(divide(divide(sFlat1,divide(sFlat2,inverse(divide(sFlat3,X1)))),X2)) = inverse(divide(X1,X2)),
inference(cp,[status(thm)],[t194,t87]) ).
cnf(t197,plain,
inverse(divide(divide(sFlat1,divide(sFlat2,inverse(divide(sFlat3,X1)))),X2)) = inverse(divide(X1,X2)),
inference(orient,[status(thm)],[t196]) ).
cnf(t249,plain,
inverse(divide(X1,divide(sFlat0,divide(sFlat2,inverse(divide(sFlat3,X1)))))) = inverse(divide(divide(sFlat1,sFlat0),sFlat1)),
inference(cp,[status(thm)],[t197,t233]) ).
cnf(t1898,plain,
inverse(divide(X1,divide(sFlat0,divide(sFlat2,inverse(divide(sFlat3,X1)))))) = inverse(divide(sFlat3,divide(sFlat0,sFlat2))),
inference(step,[status(thm)],[t249,t251]) ).
cnf(t412,plain,
inverse(divide(X1,divide(sFlat0,divide(sFlat2,inverse(divide(sFlat3,X1)))))) = inverse(divide(sFlat3,divide(sFlat0,sFlat2))),
inference(orient,[status(thm)],[t1898]) ).
cnf(t425,plain,
sFlat0 = divide(inverse(divide(sFlat3,divide(sFlat0,sFlat2))),inverse(divide(sFlat3,sFlat3))),
inference(cp,[status(thm)],[t33,t412]) ).
cnf(t469,plain,
divide(inverse(divide(sFlat3,divide(sFlat0,sFlat2))),inverse(divide(sFlat3,sFlat3))) = sFlat0,
inference(orient,[status(thm)],[t425]) ).
cnf(t473,plain,
divide(sFlat0,inverse(divide(sFlat3,divide(sFlat0,sFlat2)))) = divide(divide(inverse(divide(sFlat3,divide(sFlat0,sFlat2))),inverse(divide(sFlat3,sFlat3))),sFlat0),
inference(cp,[status(thm)],[t371,t469]) ).
cnf(t1903,plain,
divide(sFlat0,inverse(divide(sFlat3,divide(sFlat0,sFlat2)))) = divide(sFlat0,sFlat0),
inference(step,[status(thm)],[t473,t469]) ).
cnf(t1904,plain,
divide(sFlat0,inverse(divide(sFlat3,divide(sFlat0,sFlat2)))) = sFlat1,
inference(step,[status(thm)],[t1903,t18]) ).
cnf(t487,plain,
divide(sFlat0,inverse(divide(sFlat3,divide(sFlat0,sFlat2)))) = sFlat1,
inference(orient,[status(thm)],[t1904]) ).
cnf(t489,plain,
divide(sFlat1,divide(sFlat2,sFlat0)) = divide(sFlat1,divide(sFlat2,inverse(divide(sFlat3,divide(sFlat0,sFlat2))))),
inference(cp,[status(thm)],[t280,t487]) ).
cnf(t519,plain,
divide(sFlat1,divide(sFlat2,inverse(divide(sFlat3,divide(sFlat0,sFlat2))))) = divide(sFlat1,divide(sFlat2,sFlat0)),
inference(orient,[status(thm)],[t489]) ).
cnf(t528,plain,
divide(inverse(divide(divide(sFlat1,sFlat2),X1)),inverse(divide(sFlat3,divide(sFlat0,sFlat2)))) = inverse(divide(divide(sFlat1,sFlat1),divide(X1,divide(sFlat1,divide(sFlat2,sFlat0))))),
inference(cp,[status(thm)],[t334,t519]) ).
cnf(t1909,plain,
divide(inverse(divide(sFlat3,X1)),inverse(divide(sFlat3,divide(sFlat0,sFlat2)))) = inverse(divide(divide(sFlat1,sFlat1),divide(X1,divide(sFlat1,divide(sFlat2,sFlat0))))),
inference(step,[status(thm)],[t528,t21]) ).
cnf(t1910,plain,
divide(inverse(divide(sFlat3,X1)),inverse(divide(sFlat3,divide(sFlat0,sFlat2)))) = divide(inverse(divide(divide(sFlat1,sFlat2),X1)),sFlat0),
inference(step,[status(thm)],[t1909,t334]) ).
cnf(t1911,plain,
divide(inverse(divide(sFlat3,X1)),inverse(divide(sFlat3,divide(sFlat0,sFlat2)))) = divide(inverse(divide(sFlat3,X1)),sFlat0),
inference(step,[status(thm)],[t1910,t21]) ).
cnf(t597,plain,
divide(inverse(divide(sFlat3,X1)),inverse(divide(sFlat3,divide(sFlat0,sFlat2)))) = divide(inverse(divide(sFlat3,X1)),sFlat0),
inference(orient,[status(thm)],[t1911]) ).
cnf(t1892,plain,
inverse(divide(sFlat3,divide(divide(X1,sFlat0),divide(sFlat2,sFlat0)))) = X1,
inference(step,[status(thm)],[t222,t270]) ).
cnf(t277,plain,
inverse(divide(sFlat3,divide(divide(X1,sFlat0),divide(sFlat2,sFlat0)))) = X1,
inference(rw,[status(thm)],[t1892]) ).
cnf(t288,plain,
inverse(divide(sFlat3,divide(divide(X1,sFlat0),divide(sFlat2,sFlat0)))) = X1,
inference(orient,[status(thm)],[t277]) ).
cnf(t599,plain,
divide(inverse(divide(sFlat3,divide(divide(X1,sFlat0),divide(sFlat2,sFlat0)))),sFlat0) = divide(X1,inverse(divide(sFlat3,divide(sFlat0,sFlat2)))),
inference(cp,[status(thm)],[t597,t288]) ).
cnf(t1912,plain,
divide(X1,sFlat0) = divide(X1,inverse(divide(sFlat3,divide(sFlat0,sFlat2)))),
inference(step,[status(thm)],[t599,t33]) ).
cnf(t609,plain,
divide(X1,inverse(divide(sFlat3,divide(sFlat0,sFlat2)))) = divide(X1,sFlat0),
inference(orient,[status(thm)],[t1912]) ).
cnf(t614,plain,
inverse(divide(sFlat3,divide(sFlat0,sFlat2))) = divide(divide(inverse(divide(sFlat3,sFlat0)),X1),divide(sFlat2,X1)),
inference(cp,[status(thm)],[t87,t609]) ).
cnf(t1913,plain,
inverse(divide(sFlat3,divide(sFlat0,sFlat2))) = sFlat0,
inference(step,[status(thm)],[t614,t87]) ).
cnf(t625,plain,
inverse(divide(sFlat3,divide(sFlat0,sFlat2))) = sFlat0,
inference(orient,[status(thm)],[t1913]) ).
cnf(t1921,plain,
divide(divide(sFlat0,sFlat0),sFlat1) = sFlat1,
inference(step,[status(thm)],[t262,t625]) ).
cnf(t1922,plain,
divide(sFlat1,sFlat1) = sFlat1,
inference(step,[status(thm)],[t1921,t18]) ).
cnf(t636,plain,
divide(sFlat1,sFlat1) = sFlat1,
inference(rw,[status(thm)],[t1922]) ).
cnf(t637,plain,
divide(sFlat1,sFlat1) = sFlat1,
inference(orient,[status(thm)],[t636]) ).
cnf(t655,plain,
X1 = divide(inverse(divide(divide(sFlat1,sFlat1),divide(X1,sFlat1))),sFlat1),
inference(cp,[status(thm)],[t23,t637]) ).
cnf(t1965,plain,
X1 = divide(inverse(divide(sFlat1,divide(X1,sFlat1))),sFlat1),
inference(step,[status(thm)],[t655,t637]) ).
cnf(t939,plain,
divide(inverse(divide(sFlat1,divide(X1,sFlat1))),sFlat1) = X1,
inference(orient,[status(thm)],[t1965]) ).
cnf(t1919,plain,
divide(divide(sFlat0,X1),divide(X2,X1)) = divide(sFlat0,X2),
inference(step,[status(thm)],[t371,t625]) ).
cnf(t634,plain,
divide(divide(sFlat0,X1),divide(X2,X1)) = divide(sFlat0,X2),
inference(rw,[status(thm)],[t1919]) ).
cnf(t708,plain,
divide(divide(sFlat0,X1),divide(X2,X1)) = divide(sFlat0,X2),
inference(orient,[status(thm)],[t634]) ).
cnf(t710,plain,
divide(sFlat0,X1) = divide(sFlat1,divide(X1,sFlat0)),
inference(cp,[status(thm)],[t708,t18]) ).
cnf(t739,plain,
divide(sFlat1,divide(X1,sFlat0)) = divide(sFlat0,X1),
inference(orient,[status(thm)],[t710]) ).
cnf(t726,plain,
divide(sFlat0,sFlat1) = divide(divide(sFlat0,sFlat1),sFlat1),
inference(cp,[status(thm)],[t708,t637]) ).
cnf(t757,plain,
divide(divide(sFlat0,sFlat1),sFlat1) = divide(sFlat0,sFlat1),
inference(orient,[status(thm)],[t726]) ).
cnf(t759,plain,
divide(sFlat0,divide(sFlat0,sFlat1)) = divide(divide(sFlat0,sFlat1),divide(sFlat0,sFlat1)),
inference(cp,[status(thm)],[t708,t757]) ).
cnf(t228,plain,
divide(sFlat1,sFlat1) = divide(divide(sFlat0,X1),divide(sFlat0,X1)),
inference(cp,[status(thm)],[t128,t227]) ).
cnf(t229,plain,
divide(divide(sFlat0,X1),divide(sFlat0,X1)) = divide(sFlat1,sFlat1),
inference(orient,[status(thm)],[t228]) ).
cnf(t1942,plain,
divide(sFlat0,divide(sFlat0,sFlat1)) = divide(sFlat1,sFlat1),
inference(step,[status(thm)],[t759,t229]) ).
cnf(t1943,plain,
divide(sFlat0,divide(sFlat0,sFlat1)) = sFlat1,
inference(step,[status(thm)],[t1942,t637]) ).
cnf(t766,plain,
divide(sFlat0,divide(sFlat0,sFlat1)) = sFlat1,
inference(orient,[status(thm)],[t1943]) ).
cnf(t776,plain,
sFlat0 = divide(inverse(divide(divide(sFlat1,sFlat0),sFlat1)),sFlat1),
inference(cp,[status(thm)],[t23,t766]) ).
cnf(t642,plain,
divide(divide(sFlat1,sFlat0),sFlat1) = divide(sFlat1,divide(sFlat0,sFlat1)),
inference(cp,[status(thm)],[t233,t637]) ).
cnf(t1934,plain,
divide(sFlat3,divide(sFlat0,sFlat2)) = divide(sFlat1,divide(sFlat0,sFlat1)),
inference(step,[status(thm)],[t642,t251]) ).
cnf(t688,plain,
divide(sFlat3,divide(sFlat0,sFlat2)) = divide(sFlat1,divide(sFlat0,sFlat1)),
inference(orient,[status(thm)],[t1934]) ).
cnf(t1935,plain,
divide(divide(sFlat1,sFlat0),sFlat1) = divide(sFlat1,divide(sFlat0,sFlat1)),
inference(step,[status(thm)],[t251,t688]) ).
cnf(t689,plain,
divide(divide(sFlat1,sFlat0),sFlat1) = divide(sFlat1,divide(sFlat0,sFlat1)),
inference(orient,[status(thm)],[t1935]) ).
cnf(t1944,plain,
sFlat0 = divide(inverse(divide(sFlat1,divide(sFlat0,sFlat1))),sFlat1),
inference(step,[status(thm)],[t776,t689]) ).
cnf(t1937,plain,
inverse(divide(sFlat1,divide(sFlat0,sFlat1))) = sFlat0,
inference(step,[status(thm)],[t625,t688]) ).
cnf(t704,plain,
inverse(divide(sFlat1,divide(sFlat0,sFlat1))) = sFlat0,
inference(rw,[status(thm)],[t1937]) ).
cnf(t707,plain,
inverse(divide(sFlat1,divide(sFlat0,sFlat1))) = sFlat0,
inference(orient,[status(thm)],[t704]) ).
cnf(t1945,plain,
sFlat0 = divide(sFlat0,sFlat1),
inference(step,[status(thm)],[t1944,t707]) ).
cnf(t778,plain,
divide(sFlat0,sFlat1) = sFlat0,
inference(orient,[status(thm)],[t1945]) ).
cnf(t785,plain,
divide(divide(X1,sFlat0),sFlat1) = divide(divide(X1,sFlat1),sFlat0),
inference(cp,[status(thm)],[t233,t778]) ).
cnf(t812,plain,
divide(divide(X1,sFlat1),sFlat0) = divide(divide(X1,sFlat0),sFlat1),
inference(orient,[status(thm)],[t785]) ).
cnf(t818,plain,
divide(sFlat0,divide(X1,sFlat1)) = divide(sFlat1,divide(divide(X1,sFlat0),sFlat1)),
inference(cp,[status(thm)],[t739,t812]) ).
cnf(t786,plain,
divide(sFlat0,X1) = divide(sFlat0,divide(X1,sFlat1)),
inference(cp,[status(thm)],[t708,t778]) ).
cnf(t797,plain,
divide(sFlat0,divide(X1,sFlat1)) = divide(sFlat0,X1),
inference(orient,[status(thm)],[t786]) ).
cnf(t1954,plain,
divide(sFlat0,X1) = divide(sFlat1,divide(divide(X1,sFlat0),sFlat1)),
inference(step,[status(thm)],[t818,t797]) ).
cnf(t830,plain,
divide(sFlat1,divide(divide(X1,sFlat0),sFlat1)) = divide(sFlat0,X1),
inference(orient,[status(thm)],[t1954]) ).
cnf(t940,plain,
divide(X1,sFlat0) = divide(inverse(divide(sFlat0,X1)),sFlat1),
inference(cp,[status(thm)],[t939,t830]) ).
cnf(t1180,plain,
divide(inverse(divide(sFlat0,X1)),sFlat1) = divide(X1,sFlat0),
inference(orient,[status(thm)],[t940]) ).
cnf(t1192,plain,
inverse(divide(sFlat0,X1)) = divide(inverse(divide(sFlat1,divide(X1,sFlat0))),sFlat1),
inference(cp,[status(thm)],[t939,t1180]) ).
cnf(t1994,plain,
inverse(divide(sFlat0,X1)) = divide(inverse(divide(sFlat0,X1)),sFlat1),
inference(step,[status(thm)],[t1192,t739]) ).
cnf(t1995,plain,
inverse(divide(sFlat0,X1)) = divide(X1,sFlat0),
inference(step,[status(thm)],[t1994,t1180]) ).
cnf(t1212,plain,
inverse(divide(sFlat0,X1)) = divide(X1,sFlat0),
inference(orient,[status(thm)],[t1995]) ).
cnf(t1218,plain,
divide(divide(X1,sFlat1),sFlat0) = inverse(divide(sFlat0,X1)),
inference(cp,[status(thm)],[t1212,t797]) ).
cnf(t1997,plain,
divide(divide(X1,sFlat0),sFlat1) = inverse(divide(sFlat0,X1)),
inference(step,[status(thm)],[t1218,t812]) ).
cnf(t1998,plain,
divide(divide(X1,sFlat0),sFlat1) = divide(X1,sFlat0),
inference(step,[status(thm)],[t1997,t1212]) ).
cnf(t1230,plain,
divide(divide(X1,sFlat0),sFlat1) = divide(X1,sFlat0),
inference(orient,[status(thm)],[t1998]) ).
cnf(t1235,plain,
divide(inverse(divide(sFlat3,divide(X1,divide(sFlat2,sFlat0)))),sFlat0) = divide(X1,sFlat1),
inference(cp,[status(thm)],[t1230,t33]) ).
cnf(t2005,plain,
X1 = divide(X1,sFlat1),
inference(step,[status(thm)],[t1235,t33]) ).
cnf(t1248,plain,
divide(X1,sFlat1) = X1,
inference(orient,[status(thm)],[t2005]) ).
cnf(t1719,plain,
sFlat1 = divide(divide(inverse(divide(sFlat1,inverse(divide(divide(sFlat1,X1),divide(X2,divide(X1,X3)))))),X3),X2),
inference(cp,[status(thm)],[t1703,t1248]) ).
cnf(t2006,plain,
inverse(divide(sFlat1,divide(X1,sFlat1))) = X1,
inference(step,[status(thm)],[t939,t1248]) ).
cnf(t2007,plain,
inverse(divide(sFlat1,X1)) = X1,
inference(step,[status(thm)],[t2006,t1248]) ).
cnf(t1279,plain,
inverse(divide(sFlat1,X1)) = X1,
inference(rw,[status(thm)],[t2007]) ).
cnf(t1283,plain,
inverse(divide(sFlat1,X1)) = X1,
inference(orient,[status(thm)],[t1279]) ).
cnf(t2080,plain,
sFlat1 = divide(divide(inverse(divide(divide(sFlat1,X1),divide(X2,divide(X1,X3)))),X3),X2),
inference(step,[status(thm)],[t1719,t1283]) ).
cnf(t2081,plain,
sFlat1 = divide(X2,X2),
inference(step,[status(thm)],[t2080,t23]) ).
cnf(t1805,plain,
divide(X1,X1) = sFlat1,
inference(orient,[status(thm)],[t2081]) ).
cnf(t1999,plain,
divide(divide(X1,X2),divide(sFlat0,X2)) = divide(X1,sFlat0),
inference(step,[status(thm)],[t233,t1230]) ).
cnf(t1231,plain,
divide(divide(X1,X2),divide(sFlat0,X2)) = divide(X1,sFlat0),
inference(orient,[status(thm)],[t1999]) ).
cnf(t1806,plain,
divide(X1,sFlat0) = divide(sFlat1,divide(sFlat0,X1)),
inference(cp,[status(thm)],[t1231,t1805]) ).
cnf(t1825,plain,
divide(sFlat1,divide(sFlat0,X1)) = divide(X1,sFlat0),
inference(orient,[status(thm)],[t1806]) ).
cnf(t1829,plain,
divide(sFlat0,X1) = inverse(divide(X1,sFlat0)),
inference(cp,[status(thm)],[t1283,t1825]) ).
cnf(t1850,plain,
inverse(divide(X1,sFlat0)) = divide(sFlat0,X1),
inference(orient,[status(thm)],[t1829]) ).
cnf(t1259,plain,
X1 = divide(inverse(divide(sFlat3,X1)),divide(sFlat2,sFlat1)),
inference(cp,[status(thm)],[t87,t1248]) ).
cnf(t2026,plain,
X1 = divide(inverse(divide(sFlat3,X1)),sFlat2),
inference(step,[status(thm)],[t1259,t1248]) ).
cnf(t1336,plain,
divide(inverse(divide(sFlat3,X1)),sFlat2) = X1,
inference(orient,[status(thm)],[t2026]) ).
cnf(t42,plain,
inverse(divide(sFlat3,divide(X1,divide(sFlat2,sFlat3)))) = divide(inverse(divide(divide(sFlat1,sFlat1),X1)),sFlat2),
inference(cp,[status(thm)],[t41,t33]) ).
cnf(t53,plain,
inverse(divide(sFlat3,divide(X1,divide(sFlat2,sFlat3)))) = divide(inverse(divide(divide(sFlat1,sFlat1),X1)),sFlat2),
inference(orient,[status(thm)],[t42]) ).
cnf(t1923,plain,
inverse(divide(sFlat3,divide(X1,divide(sFlat2,sFlat3)))) = divide(inverse(divide(sFlat1,X1)),sFlat2),
inference(step,[status(thm)],[t53,t637]) ).
cnf(t638,plain,
inverse(divide(sFlat3,divide(X1,divide(sFlat2,sFlat3)))) = divide(inverse(divide(sFlat1,X1)),sFlat2),
inference(orient,[status(thm)],[t1923]) ).
cnf(t2012,plain,
inverse(divide(sFlat3,divide(X1,divide(sFlat2,sFlat3)))) = divide(X1,sFlat2),
inference(step,[status(thm)],[t638,t1283]) ).
cnf(t1284,plain,
inverse(divide(sFlat3,divide(X1,divide(sFlat2,sFlat3)))) = divide(X1,sFlat2),
inference(orient,[status(thm)],[t2012]) ).
cnf(t1340,plain,
divide(X1,divide(sFlat2,sFlat3)) = divide(divide(X1,sFlat2),sFlat2),
inference(cp,[status(thm)],[t1336,t1284]) ).
cnf(t1377,plain,
divide(divide(X1,sFlat2),sFlat2) = divide(X1,divide(sFlat2,sFlat3)),
inference(orient,[status(thm)],[t1340]) ).
cnf(t1341,plain,
sFlat1 = divide(inverse(sFlat3),sFlat2),
inference(cp,[status(thm)],[t1336,t1248]) ).
cnf(t649,plain,
X1 = divide(divide(inverse(divide(divide(sFlat1,sFlat1),X1)),sFlat1),sFlat1),
inference(cp,[status(thm)],[t128,t637]) ).
cnf(t1961,plain,
X1 = divide(divide(inverse(divide(sFlat1,X1)),sFlat1),sFlat1),
inference(step,[status(thm)],[t649,t637]) ).
cnf(t854,plain,
divide(divide(inverse(divide(sFlat1,X1)),sFlat1),sFlat1) = X1,
inference(orient,[status(thm)],[t1961]) ).
cnf(t858,plain,
sFlat2 = divide(divide(inverse(sFlat3),sFlat1),sFlat1),
inference(cp,[status(thm)],[t854,t21]) ).
cnf(t869,plain,
divide(divide(inverse(sFlat3),sFlat1),sFlat1) = sFlat2,
inference(orient,[status(thm)],[t858]) ).
cnf(t872,plain,
divide(sFlat0,divide(inverse(sFlat3),sFlat1)) = divide(sFlat0,sFlat2),
inference(cp,[status(thm)],[t797,t869]) ).
cnf(t1962,plain,
divide(sFlat0,inverse(sFlat3)) = divide(sFlat0,sFlat2),
inference(step,[status(thm)],[t872,t797]) ).
cnf(t880,plain,
divide(sFlat0,inverse(sFlat3)) = divide(sFlat0,sFlat2),
inference(orient,[status(thm)],[t1962]) ).
cnf(t1186,plain,
divide(inverse(sFlat3),sFlat0) = divide(inverse(divide(sFlat0,sFlat2)),sFlat1),
inference(cp,[status(thm)],[t1180,t880]) ).
cnf(t1991,plain,
divide(inverse(sFlat3),sFlat0) = divide(sFlat2,sFlat0),
inference(step,[status(thm)],[t1186,t1180]) ).
cnf(t1200,plain,
divide(inverse(sFlat3),sFlat0) = divide(sFlat2,sFlat0),
inference(orient,[status(thm)],[t1991]) ).
cnf(t1203,plain,
inverse(sFlat3) = inverse(divide(sFlat3,divide(divide(sFlat2,sFlat0),divide(sFlat2,sFlat0)))),
inference(cp,[status(thm)],[t288,t1200]) ).
cnf(t1992,plain,
inverse(sFlat3) = sFlat2,
inference(step,[status(thm)],[t1203,t288]) ).
cnf(t1210,plain,
inverse(sFlat3) = sFlat2,
inference(orient,[status(thm)],[t1992]) ).
cnf(t2027,plain,
sFlat1 = divide(sFlat2,sFlat2),
inference(step,[status(thm)],[t1341,t1210]) ).
cnf(t1351,plain,
divide(sFlat2,sFlat2) = sFlat1,
inference(orient,[status(thm)],[t2027]) ).
cnf(t1378,plain,
divide(sFlat2,divide(sFlat2,sFlat3)) = divide(sFlat1,sFlat2),
inference(cp,[status(thm)],[t1377,t1351]) ).
cnf(t2028,plain,
divide(sFlat2,divide(sFlat2,sFlat3)) = sFlat3,
inference(step,[status(thm)],[t1378,t21]) ).
cnf(t1396,plain,
divide(sFlat2,divide(sFlat2,sFlat3)) = sFlat3,
inference(orient,[status(thm)],[t2028]) ).
cnf(t1405,plain,
sFlat2 = divide(inverse(divide(sFlat3,sFlat3)),sFlat3),
inference(cp,[status(thm)],[t33,t1396]) ).
cnf(t1249,plain,
inverse(divide(sFlat3,divide(X1,divide(sFlat2,sFlat1)))) = X1,
inference(cp,[status(thm)],[t1248,t33]) ).
cnf(t2022,plain,
inverse(divide(sFlat3,divide(X1,sFlat2))) = X1,
inference(step,[status(thm)],[t1249,t1248]) ).
cnf(t1317,plain,
inverse(divide(sFlat3,divide(X1,sFlat2))) = X1,
inference(orient,[status(thm)],[t2022]) ).
cnf(t1319,plain,
sFlat1 = inverse(divide(sFlat3,sFlat3)),
inference(cp,[status(thm)],[t1317,t21]) ).
cnf(t1325,plain,
inverse(divide(sFlat3,sFlat3)) = sFlat1,
inference(orient,[status(thm)],[t1319]) ).
cnf(t2029,plain,
sFlat2 = divide(sFlat1,sFlat3),
inference(step,[status(thm)],[t1405,t1325]) ).
cnf(t1412,plain,
divide(sFlat1,sFlat3) = sFlat2,
inference(orient,[status(thm)],[t2029]) ).
cnf(t1413,plain,
divide(sFlat1,sFlat0) = divide(sFlat2,divide(sFlat0,sFlat3)),
inference(cp,[status(thm)],[t1231,t1412]) ).
cnf(t1946,plain,
divide(divide(sFlat1,sFlat0),sFlat1) = divide(sFlat1,sFlat0),
inference(step,[status(thm)],[t689,t778]) ).
cnf(t779,plain,
divide(divide(sFlat1,sFlat0),sFlat1) = divide(sFlat1,sFlat0),
inference(orient,[status(thm)],[t1946]) ).
cnf(t941,plain,
divide(sFlat1,sFlat0) = divide(inverse(divide(sFlat1,divide(sFlat1,sFlat0))),sFlat1),
inference(cp,[status(thm)],[t939,t779]) ).
cnf(t1966,plain,
divide(sFlat1,sFlat0) = divide(inverse(divide(sFlat0,sFlat1)),sFlat1),
inference(step,[status(thm)],[t941,t739]) ).
cnf(t1967,plain,
divide(sFlat1,sFlat0) = divide(inverse(sFlat0),sFlat1),
inference(step,[status(thm)],[t1966,t778]) ).
cnf(t1074,plain,
divide(inverse(sFlat0),sFlat1) = divide(sFlat1,sFlat0),
inference(orient,[status(thm)],[t1967]) ).
cnf(t1078,plain,
inverse(sFlat0) = divide(inverse(divide(sFlat1,divide(sFlat1,sFlat0))),sFlat1),
inference(cp,[status(thm)],[t939,t1074]) ).
cnf(t1968,plain,
inverse(sFlat0) = divide(inverse(divide(sFlat0,sFlat1)),sFlat1),
inference(step,[status(thm)],[t1078,t739]) ).
cnf(t1969,plain,
inverse(sFlat0) = divide(inverse(sFlat0),sFlat1),
inference(step,[status(thm)],[t1968,t778]) ).
cnf(t1970,plain,
inverse(sFlat0) = divide(sFlat1,sFlat0),
inference(step,[status(thm)],[t1969,t1074]) ).
cnf(t1086,plain,
divide(sFlat1,sFlat0) = inverse(sFlat0),
inference(orient,[status(thm)],[t1970]) ).
cnf(t2061,plain,
inverse(sFlat0) = divide(sFlat2,divide(sFlat0,sFlat3)),
inference(step,[status(thm)],[t1413,t1086]) ).
cnf(t1493,plain,
divide(sFlat2,divide(sFlat0,sFlat3)) = inverse(sFlat0),
inference(orient,[status(thm)],[t2061]) ).
cnf(t1499,plain,
X1 = divide(inverse(divide(divide(sFlat1,sFlat2),divide(X1,inverse(sFlat0)))),divide(sFlat0,sFlat3)),
inference(cp,[status(thm)],[t23,t1493]) ).
cnf(t2066,plain,
X1 = divide(inverse(divide(sFlat3,divide(X1,inverse(sFlat0)))),divide(sFlat0,sFlat3)),
inference(step,[status(thm)],[t1499,t21]) ).
cnf(t1424,plain,
divide(inverse(divide(divide(sFlat1,sFlat1),X1)),sFlat3) = inverse(divide(sFlat3,divide(X1,divide(sFlat2,sFlat2)))),
inference(cp,[status(thm)],[t113,t1412]) ).
cnf(t2030,plain,
divide(inverse(divide(sFlat1,X1)),sFlat3) = inverse(divide(sFlat3,divide(X1,divide(sFlat2,sFlat2)))),
inference(step,[status(thm)],[t1424,t637]) ).
cnf(t2031,plain,
divide(X1,sFlat3) = inverse(divide(sFlat3,divide(X1,divide(sFlat2,sFlat2)))),
inference(step,[status(thm)],[t2030,t1283]) ).
cnf(t2032,plain,
divide(X1,sFlat3) = inverse(divide(sFlat3,divide(X1,sFlat1))),
inference(step,[status(thm)],[t2031,t1351]) ).
cnf(t2033,plain,
divide(X1,sFlat3) = inverse(divide(sFlat3,X1)),
inference(step,[status(thm)],[t2032,t1248]) ).
cnf(t1431,plain,
inverse(divide(sFlat3,X1)) = divide(X1,sFlat3),
inference(orient,[status(thm)],[t2033]) ).
cnf(t2067,plain,
X1 = divide(divide(divide(X1,inverse(sFlat0)),sFlat3),divide(sFlat0,sFlat3)),
inference(step,[status(thm)],[t2066,t1431]) ).
cnf(t2068,plain,
X1 = divide(divide(divide(X1,inverse(sFlat0)),sFlat0),sFlat1),
inference(step,[status(thm)],[t2067,t214]) ).
cnf(t2069,plain,
X1 = divide(divide(X1,inverse(sFlat0)),sFlat0),
inference(step,[status(thm)],[t2068,t1230]) ).
cnf(t1542,plain,
divide(divide(X1,inverse(sFlat0)),sFlat0) = X1,
inference(orient,[status(thm)],[t2069]) ).
cnf(t1852,plain,
divide(sFlat0,divide(X1,inverse(sFlat0))) = inverse(X1),
inference(cp,[status(thm)],[t1850,t1542]) ).
cnf(t1545,plain,
divide(sFlat0,divide(X1,inverse(sFlat0))) = divide(sFlat1,X1),
inference(cp,[status(thm)],[t739,t1542]) ).
cnf(t1673,plain,
divide(sFlat0,divide(X1,inverse(sFlat0))) = divide(sFlat1,X1),
inference(orient,[status(thm)],[t1545]) ).
cnf(t2082,plain,
divide(sFlat1,X1) = inverse(X1),
inference(step,[status(thm)],[t1852,t1673]) ).
cnf(t1860,plain,
divide(sFlat1,X1) = inverse(X1),
inference(orient,[status(thm)],[t2082]) ).
cnf(t2090,plain,
inverse(inverse(X1)) = X1,
inference(step,[status(thm)],[t1283,t1860]) ).
cnf(t1869,plain,
inverse(inverse(X1)) = X1,
inference(rw,[status(thm)],[t2090]) ).
cnf(t1877,plain,
inverse(inverse(X1)) = X1,
inference(orient,[status(thm)],[t1869]) ).
cnf(u0,negated_conjecture,
multiply(multiply(inverse(b2),b2),a2) != a2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(d0,axiom,
multiply(A,B) = divide(A,inverse(B)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(goal_0,negated_conjecture,
divide(divide(inverse(b2),inverse(b2)),inverse(a2)) != a2,
inference(definition_unfolding,[status(thm)],[u0,d0]) ).
cnf(g0_0,plain,
divide(sFlat1,inverse(a2)) != a2,
inference(rw,[status(thm)],[goal_0,t1805]) ).
cnf(g0_1,plain,
inverse(inverse(a2)) != a2,
inference(rw,[status(thm)],[g0_0,t1860]) ).
cnf(g0_2,plain,
a2 != a2,
inference(rw,[status(thm)],[g0_1,t1877]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP479-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.11/0.58 % Computer : n002.cluster.edu
% 0.11/0.58 % Model : x86_64 x86_64
% 0.11/0.58 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.58 % Memory : 8046.5625MB
% 0.11/0.58 % OS : Linux 6.8.0-71-generic
% 0.11/0.58 % CPULimit : 300
% 0.11/0.58 % WCLimit : 300
% 0.11/0.58 % DateTime : Wed Sep 23 14:54:36 UTC 2026
% 0.11/0.58 % CPUTime :
% 0.11/0.58 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 5.28/1.57 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 5.28/1.57 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------