%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : ARI765-1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n015.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 12:56:51 PM UTC 2026
% Result : Unsatisfiable 25.34s 8.69s
% Output : CNFRefutation 25.34s
% Verified :
% SZS Type : Refutation
% Derivation depth : 82
% Number of leaves : 21
% Syntax : Number of clauses : 332 ( 332 unt; 0 nHn; 269 RR)
% Number of literals : 332 ( 331 equ; 11 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 : 17 ( 17 usr; 9 con; 0-3 aty)
% Number of variables : 75 ( 16 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t15,axiom,
sF0 = s(zero),
introduced(definition) ).
cnf(t23,plain,
s(zero) = sF0,
inference(orient,[status(thm)],[t15]) ).
cnf(t16,axiom,
sF1 = s(s(zero)),
introduced(definition) ).
cnf(t9020,plain,
sF1 = s(sF0),
inference(step,[status(thm)],[t16,t23]) ).
cnf(t32,plain,
s(sF0) = sF1,
inference(orient,[status(thm)],[t9020]) ).
cnf(t17,axiom,
sF2 = s(s(s(zero))),
introduced(definition) ).
cnf(t9028,plain,
sF2 = s(s(sF0)),
inference(step,[status(thm)],[t17,t23]) ).
cnf(t9029,plain,
sF2 = s(sF1),
inference(step,[status(thm)],[t9028,t32]) ).
cnf(t55,plain,
s(sF1) = sF2,
inference(orient,[status(thm)],[t9029]) ).
cnf(t18,axiom,
sF3 = s(s(s(s(zero)))),
introduced(definition) ).
cnf(t9087,plain,
sF3 = s(s(s(sF0))),
inference(step,[status(thm)],[t18,t23]) ).
cnf(t9088,plain,
sF3 = s(s(sF1)),
inference(step,[status(thm)],[t9087,t32]) ).
cnf(t9089,plain,
sF3 = s(sF2),
inference(step,[status(thm)],[t9088,t55]) ).
cnf(t272,plain,
s(sF2) = sF3,
inference(orient,[status(thm)],[t9089]) ).
cnf(t19,axiom,
sF4 = e(s(s(s(s(zero))))),
introduced(definition) ).
cnf(t9102,plain,
sF4 = e(s(s(s(sF0)))),
inference(step,[status(thm)],[t19,t23]) ).
cnf(t9103,plain,
sF4 = e(s(s(sF1))),
inference(step,[status(thm)],[t9102,t32]) ).
cnf(t9104,plain,
sF4 = e(s(sF2)),
inference(step,[status(thm)],[t9103,t55]) ).
cnf(t9105,plain,
sF4 = e(sF3),
inference(step,[status(thm)],[t9104,t272]) ).
cnf(t315,plain,
e(sF3) = sF4,
inference(orient,[status(thm)],[t9105]) ).
cnf(t20,axiom,
sF5 = log(e(s(s(s(s(zero)))))),
introduced(definition) ).
cnf(t9119,plain,
sF5 = log(e(s(s(s(sF0))))),
inference(step,[status(thm)],[t20,t23]) ).
cnf(t9120,plain,
sF5 = log(e(s(s(sF1)))),
inference(step,[status(thm)],[t9119,t32]) ).
cnf(t9121,plain,
sF5 = log(e(s(sF2))),
inference(step,[status(thm)],[t9120,t55]) ).
cnf(t9122,plain,
sF5 = log(e(sF3)),
inference(step,[status(thm)],[t9121,t272]) ).
cnf(t9123,plain,
sF5 = log(sF4),
inference(step,[status(thm)],[t9122,t315]) ).
cnf(t345,plain,
log(sF4) = sF5,
inference(orient,[status(thm)],[t9123]) ).
cnf(t13,axiom,
s(log(s(quot(X1,s(s(zero)))))) = log(s(s(X1))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t9049,plain,
s(log(s(quot(X1,s(sF0))))) = log(s(s(X1))),
inference(step,[status(thm)],[t13,t23]) ).
cnf(t9050,plain,
s(log(s(quot(X1,sF1)))) = log(s(s(X1))),
inference(step,[status(thm)],[t9049,t32]) ).
cnf(t177,plain,
s(log(s(quot(X1,sF1)))) = log(s(s(X1))),
inference(orient,[status(thm)],[t9050]) ).
cnf(t14,axiom,
s(quot(minus(X1,X2),s(X2))) = quot(s(X1),s(X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t223,plain,
s(quot(minus(X1,X2),s(X2))) = quot(s(X1),s(X2)),
inference(orient,[status(thm)],[t14]) ).
cnf(t12,axiom,
if_minus(le(s(X1),X2),s(X1),X2) = minus(s(X1),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t122,plain,
if_minus(le(s(X1),X2),s(X1),X2) = minus(s(X1),X2),
inference(orient,[status(thm)],[t12]) ).
cnf(t10,axiom,
le(s(X1),s(X2)) = le(X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t82,plain,
le(s(X1),s(X2)) = le(X1,X2),
inference(orient,[status(thm)],[t10]) ).
cnf(t129,plain,
minus(s(X1),s(X2)) = if_minus(le(X1,X2),s(X1),s(X2)),
inference(cp,[status(thm)],[t122,t82]) ).
cnf(t882,plain,
if_minus(le(X1,X2),s(X1),s(X2)) = minus(s(X1),s(X2)),
inference(orient,[status(thm)],[t129]) ).
cnf(t5,axiom,
le(s(X1),zero) = false,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t33,plain,
le(s(X1),zero) = false,
inference(orient,[status(thm)],[t5]) ).
cnf(t9,axiom,
s(s(d(X1))) = d(s(X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t43,plain,
s(s(d(X1))) = d(s(X1)),
inference(orient,[status(thm)],[t9]) ).
cnf(t47,plain,
false = le(d(s(X1)),zero),
inference(cp,[status(thm)],[t33,t43]) ).
cnf(t406,plain,
le(d(s(X1)),zero) = false,
inference(orient,[status(thm)],[t47]) ).
cnf(t7,axiom,
e(s(X1)) = d(e(X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t29,plain,
d(e(X1)) = e(s(X1)),
inference(orient,[status(thm)],[t7]) ).
cnf(t0,axiom,
d(zero) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t21,plain,
d(zero) = zero,
inference(orient,[status(thm)],[t0]) ).
cnf(t44,plain,
d(s(zero)) = s(s(zero)),
inference(cp,[status(thm)],[t43,t21]) ).
cnf(t9021,plain,
d(sF0) = s(s(zero)),
inference(step,[status(thm)],[t44,t23]) ).
cnf(t4,axiom,
s(zero) = e(zero),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t22,plain,
e(zero) = s(zero),
inference(orient,[status(thm)],[t4]) ).
cnf(t9016,plain,
e(zero) = sF0,
inference(step,[status(thm)],[t22,t23]) ).
cnf(t24,plain,
e(zero) = sF0,
inference(orient,[status(thm)],[t9016]) ).
cnf(t30,plain,
e(s(zero)) = d(sF0),
inference(cp,[status(thm)],[t29,t24]) ).
cnf(t9019,plain,
e(sF0) = d(sF0),
inference(step,[status(thm)],[t30,t23]) ).
cnf(t31,plain,
d(sF0) = e(sF0),
inference(orient,[status(thm)],[t9019]) ).
cnf(t9022,plain,
e(sF0) = s(s(zero)),
inference(step,[status(thm)],[t9021,t31]) ).
cnf(t9023,plain,
e(sF0) = s(sF0),
inference(step,[status(thm)],[t9022,t23]) ).
cnf(t9024,plain,
e(sF0) = sF1,
inference(step,[status(thm)],[t9023,t32]) ).
cnf(t49,plain,
e(sF0) = sF1,
inference(orient,[status(thm)],[t9024]) ).
cnf(t52,plain,
e(s(sF0)) = d(sF1),
inference(cp,[status(thm)],[t29,t49]) ).
cnf(t9027,plain,
e(sF1) = d(sF1),
inference(step,[status(thm)],[t52,t32]) ).
cnf(t53,plain,
d(sF1) = e(sF1),
inference(orient,[status(thm)],[t9027]) ).
cnf(t54,plain,
d(s(sF1)) = s(s(e(sF1))),
inference(cp,[status(thm)],[t43,t53]) ).
cnf(t9037,plain,
d(sF2) = s(s(e(sF1))),
inference(step,[status(thm)],[t54,t55]) ).
cnf(t46,plain,
d(s(sF0)) = s(s(e(sF0))),
inference(cp,[status(thm)],[t43,t31]) ).
cnf(t9030,plain,
d(sF1) = s(s(e(sF0))),
inference(step,[status(thm)],[t46,t32]) ).
cnf(t9031,plain,
e(sF1) = s(s(e(sF0))),
inference(step,[status(thm)],[t9030,t53]) ).
cnf(t9032,plain,
e(sF1) = s(s(sF1)),
inference(step,[status(thm)],[t9031,t49]) ).
cnf(t9033,plain,
e(sF1) = s(sF2),
inference(step,[status(thm)],[t9032,t55]) ).
cnf(t65,plain,
e(sF1) = s(sF2),
inference(orient,[status(thm)],[t9033]) ).
cnf(t9038,plain,
d(sF2) = s(s(s(sF2))),
inference(step,[status(thm)],[t9037,t65]) ).
cnf(t71,plain,
s(s(s(sF2))) = d(sF2),
inference(orient,[status(thm)],[t9038]) ).
cnf(t9095,plain,
s(s(sF3)) = d(sF2),
inference(step,[status(thm)],[t71,t272]) ).
cnf(t278,plain,
s(s(sF3)) = d(sF2),
inference(rw,[status(thm)],[t9095]) ).
cnf(t297,plain,
s(s(sF3)) = d(sF2),
inference(orient,[status(thm)],[t278]) ).
cnf(t414,plain,
false = le(d(d(sF2)),zero),
inference(cp,[status(thm)],[t406,t297]) ).
cnf(t666,plain,
le(d(d(sF2)),zero) = false,
inference(orient,[status(thm)],[t414]) ).
cnf(t958,plain,
minus(s(d(d(sF2))),s(zero)) = if_minus(false,s(d(d(sF2))),s(zero)),
inference(cp,[status(thm)],[t882,t666]) ).
cnf(t9792,plain,
minus(s(d(d(sF2))),sF0) = if_minus(false,s(d(d(sF2))),s(zero)),
inference(step,[status(thm)],[t958,t23]) ).
cnf(t11,axiom,
if_minus(false,s(X1),X2) = s(minus(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t93,plain,
if_minus(false,s(X1),X2) = s(minus(X1,X2)),
inference(orient,[status(thm)],[t11]) ).
cnf(t9793,plain,
minus(s(d(d(sF2))),sF0) = s(minus(d(d(sF2)),s(zero))),
inference(step,[status(thm)],[t9792,t93]) ).
cnf(t9794,plain,
minus(s(d(d(sF2))),sF0) = s(minus(d(d(sF2)),sF0)),
inference(step,[status(thm)],[t9793,t23]) ).
cnf(t4100,plain,
s(minus(d(d(sF2)),sF0)) = minus(s(d(d(sF2))),sF0),
inference(orient,[status(thm)],[t9794]) ).
cnf(t7744,plain,
s(s(d(s(sF3)))) = minus(s(d(d(sF2))),sF0),
inference(rw,[status(thm)],[t4100]) ).
cnf(t10023,plain,
d(s(s(sF3))) = minus(s(d(d(sF2))),sF0),
inference(step,[status(thm)],[t7744,t43]) ).
cnf(t10024,plain,
d(d(sF2)) = minus(s(d(d(sF2))),sF0),
inference(step,[status(thm)],[t10023,t297]) ).
cnf(t8807,plain,
minus(s(d(d(sF2))),sF0) = d(d(sF2)),
inference(orient,[status(thm)],[t10024]) ).
cnf(t8808,plain,
quot(s(s(d(d(sF2)))),s(sF0)) = s(quot(d(d(sF2)),s(sF0))),
inference(cp,[status(thm)],[t223,t8807]) ).
cnf(t10048,plain,
quot(d(s(d(sF2))),s(sF0)) = s(quot(d(d(sF2)),s(sF0))),
inference(step,[status(thm)],[t8808,t43]) ).
cnf(t10049,plain,
quot(d(s(d(sF2))),sF1) = s(quot(d(d(sF2)),s(sF0))),
inference(step,[status(thm)],[t10048,t32]) ).
cnf(t10050,plain,
quot(d(s(d(sF2))),sF1) = s(quot(d(d(sF2)),sF1)),
inference(step,[status(thm)],[t10049,t32]) ).
cnf(t932,plain,
minus(s(d(s(X1))),s(zero)) = if_minus(false,s(d(s(X1))),s(zero)),
inference(cp,[status(thm)],[t882,t406]) ).
cnf(t9780,plain,
minus(s(d(s(X1))),sF0) = if_minus(false,s(d(s(X1))),s(zero)),
inference(step,[status(thm)],[t932,t23]) ).
cnf(t9781,plain,
minus(s(d(s(X1))),sF0) = s(minus(d(s(X1)),s(zero))),
inference(step,[status(thm)],[t9780,t93]) ).
cnf(t9782,plain,
minus(s(d(s(X1))),sF0) = s(minus(d(s(X1)),sF0)),
inference(step,[status(thm)],[t9781,t23]) ).
cnf(t3700,plain,
s(minus(d(s(X1)),sF0)) = minus(s(d(s(X1))),sF0),
inference(orient,[status(thm)],[t9782]) ).
cnf(t883,plain,
minus(s(s(X1)),s(zero)) = if_minus(false,s(s(X1)),s(zero)),
inference(cp,[status(thm)],[t882,t33]) ).
cnf(t9414,plain,
minus(s(s(X1)),sF0) = if_minus(false,s(s(X1)),s(zero)),
inference(step,[status(thm)],[t883,t23]) ).
cnf(t9415,plain,
minus(s(s(X1)),sF0) = s(minus(s(X1),s(zero))),
inference(step,[status(thm)],[t9414,t93]) ).
cnf(t9416,plain,
minus(s(s(X1)),sF0) = s(minus(s(X1),sF0)),
inference(step,[status(thm)],[t9415,t23]) ).
cnf(t1210,plain,
s(minus(s(X1),sF0)) = minus(s(s(X1)),sF0),
inference(orient,[status(thm)],[t9416]) ).
cnf(t413,plain,
false = le(d(sF3),zero),
inference(cp,[status(thm)],[t406,t272]) ).
cnf(t68,plain,
e(s(sF1)) = d(s(sF2)),
inference(cp,[status(thm)],[t29,t65]) ).
cnf(t9036,plain,
e(sF2) = d(s(sF2)),
inference(step,[status(thm)],[t68,t55]) ).
cnf(t69,plain,
d(s(sF2)) = e(sF2),
inference(orient,[status(thm)],[t9036]) ).
cnf(t9094,plain,
d(sF3) = e(sF2),
inference(step,[status(thm)],[t69,t272]) ).
cnf(t277,plain,
d(sF3) = e(sF2),
inference(rw,[status(thm)],[t9094]) ).
cnf(t296,plain,
d(sF3) = e(sF2),
inference(orient,[status(thm)],[t277]) ).
cnf(t9136,plain,
false = le(e(sF2),zero),
inference(step,[status(thm)],[t413,t296]) ).
cnf(t418,plain,
le(e(sF2),zero) = false,
inference(orient,[status(thm)],[t9136]) ).
cnf(t933,plain,
minus(s(e(sF2)),s(zero)) = if_minus(false,s(e(sF2)),s(zero)),
inference(cp,[status(thm)],[t882,t418]) ).
cnf(t9466,plain,
minus(s(e(sF2)),sF0) = if_minus(false,s(e(sF2)),s(zero)),
inference(step,[status(thm)],[t933,t23]) ).
cnf(t9467,plain,
minus(s(e(sF2)),sF0) = s(minus(e(sF2),s(zero))),
inference(step,[status(thm)],[t9466,t93]) ).
cnf(t9468,plain,
minus(s(e(sF2)),sF0) = s(minus(e(sF2),sF0)),
inference(step,[status(thm)],[t9467,t23]) ).
cnf(t72,plain,
false = le(d(sF2),zero),
inference(cp,[status(thm)],[t33,t71]) ).
cnf(t80,plain,
le(d(sF2),zero) = false,
inference(orient,[status(thm)],[t72]) ).
cnf(t885,plain,
minus(s(d(sF2)),s(zero)) = if_minus(false,s(d(sF2)),s(zero)),
inference(cp,[status(thm)],[t882,t80]) ).
cnf(t9418,plain,
minus(s(d(sF2)),sF0) = if_minus(false,s(d(sF2)),s(zero)),
inference(step,[status(thm)],[t885,t23]) ).
cnf(t9419,plain,
minus(s(d(sF2)),sF0) = s(minus(d(sF2),s(zero))),
inference(step,[status(thm)],[t9418,t93]) ).
cnf(t9420,plain,
minus(s(d(sF2)),sF0) = s(minus(d(sF2),sF0)),
inference(step,[status(thm)],[t9419,t23]) ).
cnf(t281,plain,
false = le(sF3,zero),
inference(cp,[status(thm)],[t33,t272]) ).
cnf(t308,plain,
le(sF3,zero) = false,
inference(orient,[status(thm)],[t281]) ).
cnf(t914,plain,
minus(s(sF3),s(zero)) = if_minus(false,s(sF3),s(zero)),
inference(cp,[status(thm)],[t882,t308]) ).
cnf(t9302,plain,
minus(s(sF3),sF0) = if_minus(false,s(sF3),s(zero)),
inference(step,[status(thm)],[t914,t23]) ).
cnf(t9303,plain,
minus(s(sF3),sF0) = s(minus(sF3,s(zero))),
inference(step,[status(thm)],[t9302,t93]) ).
cnf(t9304,plain,
minus(s(sF3),sF0) = s(minus(sF3,sF0)),
inference(step,[status(thm)],[t9303,t23]) ).
cnf(t56,plain,
false = le(sF2,zero),
inference(cp,[status(thm)],[t33,t55]) ).
cnf(t58,plain,
le(sF2,zero) = false,
inference(orient,[status(thm)],[t56]) ).
cnf(t884,plain,
minus(s(sF2),s(zero)) = if_minus(false,s(sF2),s(zero)),
inference(cp,[status(thm)],[t882,t58]) ).
cnf(t9284,plain,
minus(sF3,s(zero)) = if_minus(false,s(sF2),s(zero)),
inference(step,[status(thm)],[t884,t272]) ).
cnf(t9285,plain,
minus(sF3,sF0) = if_minus(false,s(sF2),s(zero)),
inference(step,[status(thm)],[t9284,t23]) ).
cnf(t9286,plain,
minus(sF3,sF0) = s(minus(sF2,s(zero))),
inference(step,[status(thm)],[t9285,t93]) ).
cnf(t286,plain,
s(minus(sF2,X1)) = if_minus(false,sF3,X1),
inference(cp,[status(thm)],[t93,t272]) ).
cnf(t356,plain,
s(minus(sF2,X1)) = if_minus(false,sF3,X1),
inference(orient,[status(thm)],[t286]) ).
cnf(t9287,plain,
minus(sF3,sF0) = if_minus(false,sF3,s(zero)),
inference(step,[status(thm)],[t9286,t356]) ).
cnf(t9288,plain,
minus(sF3,sF0) = if_minus(false,sF3,sF0),
inference(step,[status(thm)],[t9287,t23]) ).
cnf(t127,plain,
minus(s(sF1),X1) = if_minus(le(sF2,X1),s(sF1),X1),
inference(cp,[status(thm)],[t122,t55]) ).
cnf(t9248,plain,
minus(sF2,X1) = if_minus(le(sF2,X1),s(sF1),X1),
inference(step,[status(thm)],[t127,t55]) ).
cnf(t9249,plain,
minus(sF2,X1) = if_minus(le(sF2,X1),sF2,X1),
inference(step,[status(thm)],[t9248,t55]) ).
cnf(t851,plain,
if_minus(le(sF2,X1),sF2,X1) = minus(sF2,X1),
inference(orient,[status(thm)],[t9249]) ).
cnf(t84,plain,
le(X1,zero) = le(s(X1),sF0),
inference(cp,[status(thm)],[t82,t23]) ).
cnf(t108,plain,
le(s(X1),sF0) = le(X1,zero),
inference(orient,[status(thm)],[t84]) ).
cnf(t111,plain,
le(sF1,zero) = le(sF2,sF0),
inference(cp,[status(thm)],[t108,t55]) ).
cnf(t35,plain,
false = le(sF1,zero),
inference(cp,[status(thm)],[t33,t32]) ).
cnf(t40,plain,
le(sF1,zero) = false,
inference(orient,[status(thm)],[t35]) ).
cnf(t9041,plain,
false = le(sF2,sF0),
inference(step,[status(thm)],[t111,t40]) ).
cnf(t114,plain,
le(sF2,sF0) = false,
inference(orient,[status(thm)],[t9041]) ).
cnf(t852,plain,
minus(sF2,sF0) = if_minus(false,sF2,sF0),
inference(cp,[status(thm)],[t851,t114]) ).
cnf(t97,plain,
s(minus(sF1,X1)) = if_minus(false,sF2,X1),
inference(cp,[status(thm)],[t93,t55]) ).
cnf(t161,plain,
s(minus(sF1,X1)) = if_minus(false,sF2,X1),
inference(orient,[status(thm)],[t97]) ).
cnf(t124,plain,
minus(s(sF0),X1) = if_minus(le(sF1,X1),s(sF0),X1),
inference(cp,[status(thm)],[t122,t32]) ).
cnf(t9208,plain,
minus(sF1,X1) = if_minus(le(sF1,X1),s(sF0),X1),
inference(step,[status(thm)],[t124,t32]) ).
cnf(t9209,plain,
minus(sF1,X1) = if_minus(le(sF1,X1),sF1,X1),
inference(step,[status(thm)],[t9208,t32]) ).
cnf(t788,plain,
if_minus(le(sF1,X1),sF1,X1) = minus(sF1,X1),
inference(orient,[status(thm)],[t9209]) ).
cnf(t109,plain,
le(sF0,zero) = le(sF1,sF0),
inference(cp,[status(thm)],[t108,t32]) ).
cnf(t34,plain,
false = le(sF0,zero),
inference(cp,[status(thm)],[t33,t23]) ).
cnf(t39,plain,
le(sF0,zero) = false,
inference(orient,[status(thm)],[t34]) ).
cnf(t9040,plain,
false = le(sF1,sF0),
inference(step,[status(thm)],[t109,t39]) ).
cnf(t113,plain,
le(sF1,sF0) = false,
inference(orient,[status(thm)],[t9040]) ).
cnf(t789,plain,
minus(sF1,sF0) = if_minus(false,sF1,sF0),
inference(cp,[status(thm)],[t788,t113]) ).
cnf(t95,plain,
s(minus(sF0,X1)) = if_minus(false,sF1,X1),
inference(cp,[status(thm)],[t93,t32]) ).
cnf(t147,plain,
s(minus(sF0,X1)) = if_minus(false,sF1,X1),
inference(orient,[status(thm)],[t95]) ).
cnf(t123,plain,
minus(s(zero),X1) = if_minus(le(sF0,X1),s(zero),X1),
inference(cp,[status(thm)],[t122,t23]) ).
cnf(t9183,plain,
minus(sF0,X1) = if_minus(le(sF0,X1),s(zero),X1),
inference(step,[status(thm)],[t123,t23]) ).
cnf(t9184,plain,
minus(sF0,X1) = if_minus(le(sF0,X1),sF0,X1),
inference(step,[status(thm)],[t9183,t23]) ).
cnf(t746,plain,
if_minus(le(sF0,X1),sF0,X1) = minus(sF0,X1),
inference(orient,[status(thm)],[t9184]) ).
cnf(t83,plain,
le(zero,X1) = le(sF0,s(X1)),
inference(cp,[status(thm)],[t82,t23]) ).
cnf(t1,axiom,
le(zero,X1) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t26,plain,
le(zero,X1) = true,
inference(orient,[status(thm)],[t1]) ).
cnf(t9039,plain,
true = le(sF0,s(X1)),
inference(step,[status(thm)],[t83,t26]) ).
cnf(t99,plain,
le(sF0,s(X1)) = true,
inference(orient,[status(thm)],[t9039]) ).
cnf(t100,plain,
true = le(sF0,sF0),
inference(cp,[status(thm)],[t99,t23]) ).
cnf(t105,plain,
le(sF0,sF0) = true,
inference(orient,[status(thm)],[t100]) ).
cnf(t748,plain,
minus(sF0,sF0) = if_minus(true,sF0,sF0),
inference(cp,[status(thm)],[t746,t105]) ).
cnf(t8,axiom,
if_minus(true,s(X1),X2) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t60,plain,
if_minus(true,s(X1),X2) = zero,
inference(orient,[status(thm)],[t8]) ).
cnf(t61,plain,
zero = if_minus(true,sF0,X1),
inference(cp,[status(thm)],[t60,t23]) ).
cnf(t75,plain,
if_minus(true,sF0,X1) = zero,
inference(orient,[status(thm)],[t61]) ).
cnf(t9185,plain,
minus(sF0,sF0) = zero,
inference(step,[status(thm)],[t748,t75]) ).
cnf(t756,plain,
minus(sF0,sF0) = zero,
inference(orient,[status(thm)],[t9185]) ).
cnf(t757,plain,
if_minus(false,sF1,sF0) = s(zero),
inference(cp,[status(thm)],[t147,t756]) ).
cnf(t9222,plain,
if_minus(false,sF1,sF0) = sF0,
inference(step,[status(thm)],[t757,t23]) ).
cnf(t812,plain,
if_minus(false,sF1,sF0) = sF0,
inference(orient,[status(thm)],[t9222]) ).
cnf(t9231,plain,
minus(sF1,sF0) = sF0,
inference(step,[status(thm)],[t789,t812]) ).
cnf(t835,plain,
minus(sF1,sF0) = sF0,
inference(orient,[status(thm)],[t9231]) ).
cnf(t836,plain,
if_minus(false,sF2,sF0) = s(sF0),
inference(cp,[status(thm)],[t161,t835]) ).
cnf(t9261,plain,
if_minus(false,sF2,sF0) = sF1,
inference(step,[status(thm)],[t836,t32]) ).
cnf(t872,plain,
if_minus(false,sF2,sF0) = sF1,
inference(orient,[status(thm)],[t9261]) ).
cnf(t9262,plain,
minus(sF2,sF0) = sF1,
inference(step,[status(thm)],[t852,t872]) ).
cnf(t873,plain,
minus(sF2,sF0) = sF1,
inference(orient,[status(thm)],[t9262]) ).
cnf(t875,plain,
if_minus(false,sF3,sF0) = s(sF1),
inference(cp,[status(thm)],[t356,t873]) ).
cnf(t9283,plain,
if_minus(false,sF3,sF0) = sF2,
inference(step,[status(thm)],[t875,t55]) ).
cnf(t979,plain,
if_minus(false,sF3,sF0) = sF2,
inference(orient,[status(thm)],[t9283]) ).
cnf(t9289,plain,
minus(sF3,sF0) = sF2,
inference(step,[status(thm)],[t9288,t979]) ).
cnf(t980,plain,
minus(sF3,sF0) = sF2,
inference(orient,[status(thm)],[t9289]) ).
cnf(t9305,plain,
minus(s(sF3),sF0) = s(sF2),
inference(step,[status(thm)],[t9304,t980]) ).
cnf(t9306,plain,
minus(s(sF3),sF0) = sF3,
inference(step,[status(thm)],[t9305,t272]) ).
cnf(t999,plain,
minus(s(sF3),sF0) = sF3,
inference(orient,[status(thm)],[t9306]) ).
cnf(t1219,plain,
minus(s(s(sF3)),sF0) = s(sF3),
inference(cp,[status(thm)],[t1210,t999]) ).
cnf(t9417,plain,
minus(d(sF2),sF0) = s(sF3),
inference(step,[status(thm)],[t1219,t297]) ).
cnf(t1270,plain,
minus(d(sF2),sF0) = s(sF3),
inference(orient,[status(thm)],[t9417]) ).
cnf(t9421,plain,
minus(s(d(sF2)),sF0) = s(s(sF3)),
inference(step,[status(thm)],[t9420,t1270]) ).
cnf(t9422,plain,
minus(s(d(sF2)),sF0) = d(sF2),
inference(step,[status(thm)],[t9421,t297]) ).
cnf(t1272,plain,
minus(s(d(sF2)),sF0) = d(sF2),
inference(orient,[status(thm)],[t9422]) ).
cnf(t1275,plain,
minus(s(s(d(sF2))),sF0) = s(d(sF2)),
inference(cp,[status(thm)],[t1210,t1272]) ).
cnf(t9430,plain,
minus(d(s(sF2)),sF0) = s(d(sF2)),
inference(step,[status(thm)],[t1275,t43]) ).
cnf(t9431,plain,
minus(d(sF3),sF0) = s(d(sF2)),
inference(step,[status(thm)],[t9430,t272]) ).
cnf(t9432,plain,
minus(e(sF2),sF0) = s(d(sF2)),
inference(step,[status(thm)],[t9431,t296]) ).
cnf(t1278,plain,
minus(e(sF2),sF0) = s(d(sF2)),
inference(orient,[status(thm)],[t9432]) ).
cnf(t9469,plain,
minus(s(e(sF2)),sF0) = s(s(d(sF2))),
inference(step,[status(thm)],[t9468,t1278]) ).
cnf(t9470,plain,
minus(s(e(sF2)),sF0) = d(s(sF2)),
inference(step,[status(thm)],[t9469,t43]) ).
cnf(t9471,plain,
minus(s(e(sF2)),sF0) = d(sF3),
inference(step,[status(thm)],[t9470,t272]) ).
cnf(t9472,plain,
minus(s(e(sF2)),sF0) = e(sF2),
inference(step,[status(thm)],[t9471,t296]) ).
cnf(t1462,plain,
minus(s(e(sF2)),sF0) = e(sF2),
inference(orient,[status(thm)],[t9472]) ).
cnf(t1464,plain,
minus(s(s(e(sF2))),sF0) = s(e(sF2)),
inference(cp,[status(thm)],[t1210,t1462]) ).
cnf(t70,plain,
d(s(s(sF2))) = s(s(e(sF2))),
inference(cp,[status(thm)],[t43,t69]) ).
cnf(t78,plain,
d(s(s(sF2))) = s(s(e(sF2))),
inference(orient,[status(thm)],[t70]) ).
cnf(t9096,plain,
d(s(sF3)) = s(s(e(sF2))),
inference(step,[status(thm)],[t78,t272]) ).
cnf(t279,plain,
d(s(sF3)) = s(s(e(sF2))),
inference(rw,[status(thm)],[t9096]) ).
cnf(t325,plain,
s(s(e(sF2))) = d(s(sF3)),
inference(orient,[status(thm)],[t279]) ).
cnf(t9577,plain,
minus(d(s(sF3)),sF0) = s(e(sF2)),
inference(step,[status(thm)],[t1464,t325]) ).
cnf(t1725,plain,
minus(d(s(sF3)),sF0) = s(e(sF2)),
inference(orient,[status(thm)],[t9577]) ).
cnf(t3713,plain,
minus(s(d(s(sF3))),sF0) = s(s(e(sF2))),
inference(cp,[status(thm)],[t3700,t1725]) ).
cnf(t9955,plain,
minus(s(d(s(sF3))),sF0) = d(s(sF3)),
inference(step,[status(thm)],[t3713,t325]) ).
cnf(t7731,plain,
minus(s(d(s(sF3))),sF0) = d(s(sF3)),
inference(orient,[status(thm)],[t9955]) ).
cnf(t7732,plain,
quot(s(s(d(s(sF3)))),s(sF0)) = s(quot(d(s(sF3)),s(sF0))),
inference(cp,[status(thm)],[t223,t7731]) ).
cnf(t9956,plain,
quot(d(s(s(sF3))),s(sF0)) = s(quot(d(s(sF3)),s(sF0))),
inference(step,[status(thm)],[t7732,t43]) ).
cnf(t9957,plain,
quot(d(d(sF2)),s(sF0)) = s(quot(d(s(sF3)),s(sF0))),
inference(step,[status(thm)],[t9956,t297]) ).
cnf(t9958,plain,
quot(d(d(sF2)),sF1) = s(quot(d(s(sF3)),s(sF0))),
inference(step,[status(thm)],[t9957,t32]) ).
cnf(t9959,plain,
quot(d(d(sF2)),sF1) = s(quot(d(s(sF3)),sF1)),
inference(step,[status(thm)],[t9958,t32]) ).
cnf(t1463,plain,
quot(s(s(e(sF2))),s(sF0)) = s(quot(e(sF2),s(sF0))),
inference(cp,[status(thm)],[t223,t1462]) ).
cnf(t9568,plain,
quot(d(s(sF3)),s(sF0)) = s(quot(e(sF2),s(sF0))),
inference(step,[status(thm)],[t1463,t325]) ).
cnf(t9569,plain,
quot(d(s(sF3)),sF1) = s(quot(e(sF2),s(sF0))),
inference(step,[status(thm)],[t9568,t32]) ).
cnf(t9570,plain,
quot(d(s(sF3)),sF1) = s(quot(e(sF2),sF1)),
inference(step,[status(thm)],[t9569,t32]) ).
cnf(t1273,plain,
quot(s(s(d(sF2))),s(sF0)) = s(quot(d(sF2),s(sF0))),
inference(cp,[status(thm)],[t223,t1272]) ).
cnf(t9423,plain,
quot(d(s(sF2)),s(sF0)) = s(quot(d(sF2),s(sF0))),
inference(step,[status(thm)],[t1273,t43]) ).
cnf(t9424,plain,
quot(d(sF3),s(sF0)) = s(quot(d(sF2),s(sF0))),
inference(step,[status(thm)],[t9423,t272]) ).
cnf(t9425,plain,
quot(e(sF2),s(sF0)) = s(quot(d(sF2),s(sF0))),
inference(step,[status(thm)],[t9424,t296]) ).
cnf(t9426,plain,
quot(e(sF2),sF1) = s(quot(d(sF2),s(sF0))),
inference(step,[status(thm)],[t9425,t32]) ).
cnf(t9427,plain,
quot(e(sF2),sF1) = s(quot(d(sF2),sF1)),
inference(step,[status(thm)],[t9426,t32]) ).
cnf(t1000,plain,
quot(s(s(sF3)),s(sF0)) = s(quot(sF3,s(sF0))),
inference(cp,[status(thm)],[t223,t999]) ).
cnf(t9339,plain,
quot(d(sF2),s(sF0)) = s(quot(sF3,s(sF0))),
inference(step,[status(thm)],[t1000,t297]) ).
cnf(t9340,plain,
quot(d(sF2),sF1) = s(quot(sF3,s(sF0))),
inference(step,[status(thm)],[t9339,t32]) ).
cnf(t9341,plain,
quot(d(sF2),sF1) = s(quot(sF3,sF1)),
inference(step,[status(thm)],[t9340,t32]) ).
cnf(t874,plain,
quot(s(sF2),s(sF0)) = s(quot(sF1,s(sF0))),
inference(cp,[status(thm)],[t223,t873]) ).
cnf(t9263,plain,
quot(sF3,s(sF0)) = s(quot(sF1,s(sF0))),
inference(step,[status(thm)],[t874,t272]) ).
cnf(t9264,plain,
quot(sF3,sF1) = s(quot(sF1,s(sF0))),
inference(step,[status(thm)],[t9263,t32]) ).
cnf(t9265,plain,
quot(sF3,sF1) = s(quot(sF1,sF1)),
inference(step,[status(thm)],[t9264,t32]) ).
cnf(t758,plain,
quot(s(sF0),s(sF0)) = s(quot(zero,s(sF0))),
inference(cp,[status(thm)],[t223,t756]) ).
cnf(t9189,plain,
quot(sF1,s(sF0)) = s(quot(zero,s(sF0))),
inference(step,[status(thm)],[t758,t32]) ).
cnf(t9190,plain,
quot(sF1,sF1) = s(quot(zero,s(sF0))),
inference(step,[status(thm)],[t9189,t32]) ).
cnf(t6,axiom,
quot(zero,s(X1)) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t36,plain,
quot(zero,s(X1)) = zero,
inference(orient,[status(thm)],[t6]) ).
cnf(t9191,plain,
quot(sF1,sF1) = s(zero),
inference(step,[status(thm)],[t9190,t36]) ).
cnf(t9192,plain,
quot(sF1,sF1) = sF0,
inference(step,[status(thm)],[t9191,t23]) ).
cnf(t768,plain,
quot(sF1,sF1) = sF0,
inference(orient,[status(thm)],[t9192]) ).
cnf(t9266,plain,
quot(sF3,sF1) = s(sF0),
inference(step,[status(thm)],[t9265,t768]) ).
cnf(t9267,plain,
quot(sF3,sF1) = sF1,
inference(step,[status(thm)],[t9266,t32]) ).
cnf(t876,plain,
quot(sF3,sF1) = sF1,
inference(orient,[status(thm)],[t9267]) ).
cnf(t9342,plain,
quot(d(sF2),sF1) = s(sF1),
inference(step,[status(thm)],[t9341,t876]) ).
cnf(t9343,plain,
quot(d(sF2),sF1) = sF2,
inference(step,[status(thm)],[t9342,t55]) ).
cnf(t1038,plain,
quot(d(sF2),sF1) = sF2,
inference(orient,[status(thm)],[t9343]) ).
cnf(t9428,plain,
quot(e(sF2),sF1) = s(sF2),
inference(step,[status(thm)],[t9427,t1038]) ).
cnf(t9429,plain,
quot(e(sF2),sF1) = sF3,
inference(step,[status(thm)],[t9428,t272]) ).
cnf(t1276,plain,
quot(e(sF2),sF1) = sF3,
inference(orient,[status(thm)],[t9429]) ).
cnf(t9571,plain,
quot(d(s(sF3)),sF1) = s(sF3),
inference(step,[status(thm)],[t9570,t1276]) ).
cnf(t1722,plain,
quot(d(s(sF3)),sF1) = s(sF3),
inference(orient,[status(thm)],[t9571]) ).
cnf(t9960,plain,
quot(d(d(sF2)),sF1) = s(s(sF3)),
inference(step,[status(thm)],[t9959,t1722]) ).
cnf(t9961,plain,
quot(d(d(sF2)),sF1) = d(sF2),
inference(step,[status(thm)],[t9960,t297]) ).
cnf(t7736,plain,
quot(d(d(sF2)),sF1) = d(sF2),
inference(orient,[status(thm)],[t9961]) ).
cnf(t10051,plain,
quot(d(s(d(sF2))),sF1) = s(d(sF2)),
inference(step,[status(thm)],[t10050,t7736]) ).
cnf(t9006,plain,
quot(d(s(d(sF2))),sF1) = s(d(sF2)),
inference(orient,[status(thm)],[t10051]) ).
cnf(t9007,plain,
log(s(s(d(s(d(sF2)))))) = s(log(s(s(d(sF2))))),
inference(cp,[status(thm)],[t177,t9006]) ).
cnf(t10052,plain,
log(d(s(s(d(sF2))))) = s(log(s(s(d(sF2))))),
inference(step,[status(thm)],[t9007,t43]) ).
cnf(t10053,plain,
log(d(d(s(sF2)))) = s(log(s(s(d(sF2))))),
inference(step,[status(thm)],[t10052,t43]) ).
cnf(t10054,plain,
log(d(d(sF3))) = s(log(s(s(d(sF2))))),
inference(step,[status(thm)],[t10053,t272]) ).
cnf(t10055,plain,
log(d(e(sF2))) = s(log(s(s(d(sF2))))),
inference(step,[status(thm)],[t10054,t296]) ).
cnf(t10056,plain,
log(e(s(sF2))) = s(log(s(s(d(sF2))))),
inference(step,[status(thm)],[t10055,t29]) ).
cnf(t10057,plain,
log(e(sF3)) = s(log(s(s(d(sF2))))),
inference(step,[status(thm)],[t10056,t272]) ).
cnf(t10058,plain,
log(sF4) = s(log(s(s(d(sF2))))),
inference(step,[status(thm)],[t10057,t315]) ).
cnf(t10059,plain,
sF5 = s(log(s(s(d(sF2))))),
inference(step,[status(thm)],[t10058,t345]) ).
cnf(t10060,plain,
sF5 = s(log(d(s(sF2)))),
inference(step,[status(thm)],[t10059,t43]) ).
cnf(t10061,plain,
sF5 = s(log(d(sF3))),
inference(step,[status(thm)],[t10060,t272]) ).
cnf(t10062,plain,
sF5 = s(log(e(sF2))),
inference(step,[status(thm)],[t10061,t296]) ).
cnf(t1039,plain,
log(s(s(d(sF2)))) = s(log(s(sF2))),
inference(cp,[status(thm)],[t177,t1038]) ).
cnf(t9344,plain,
log(d(s(sF2))) = s(log(s(sF2))),
inference(step,[status(thm)],[t1039,t43]) ).
cnf(t9345,plain,
log(d(sF3)) = s(log(s(sF2))),
inference(step,[status(thm)],[t9344,t272]) ).
cnf(t9346,plain,
log(e(sF2)) = s(log(s(sF2))),
inference(step,[status(thm)],[t9345,t296]) ).
cnf(t9347,plain,
log(e(sF2)) = s(log(sF3)),
inference(step,[status(thm)],[t9346,t272]) ).
cnf(t769,plain,
log(s(s(sF1))) = s(log(s(sF0))),
inference(cp,[status(thm)],[t177,t768]) ).
cnf(t9193,plain,
log(s(sF2)) = s(log(s(sF0))),
inference(step,[status(thm)],[t769,t55]) ).
cnf(t9194,plain,
log(sF3) = s(log(s(sF0))),
inference(step,[status(thm)],[t9193,t272]) ).
cnf(t9195,plain,
log(sF3) = s(log(sF1)),
inference(step,[status(thm)],[t9194,t32]) ).
cnf(t38,plain,
zero = quot(zero,sF1),
inference(cp,[status(thm)],[t36,t32]) ).
cnf(t42,plain,
quot(zero,sF1) = zero,
inference(orient,[status(thm)],[t38]) ).
cnf(t178,plain,
log(s(s(zero))) = s(log(s(zero))),
inference(cp,[status(thm)],[t177,t42]) ).
cnf(t9051,plain,
log(s(sF0)) = s(log(s(zero))),
inference(step,[status(thm)],[t178,t23]) ).
cnf(t9052,plain,
log(sF1) = s(log(s(zero))),
inference(step,[status(thm)],[t9051,t32]) ).
cnf(t9053,plain,
log(sF1) = s(log(sF0)),
inference(step,[status(thm)],[t9052,t23]) ).
cnf(t2,axiom,
log(s(zero)) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t9018,plain,
log(sF0) = zero,
inference(step,[status(thm)],[t2,t23]) ).
cnf(t27,plain,
log(sF0) = zero,
inference(orient,[status(thm)],[t9018]) ).
cnf(t9054,plain,
log(sF1) = s(zero),
inference(step,[status(thm)],[t9053,t27]) ).
cnf(t9055,plain,
log(sF1) = sF0,
inference(step,[status(thm)],[t9054,t23]) ).
cnf(t192,plain,
log(sF1) = sF0,
inference(orient,[status(thm)],[t9055]) ).
cnf(t9196,plain,
log(sF3) = s(sF0),
inference(step,[status(thm)],[t9195,t192]) ).
cnf(t9197,plain,
log(sF3) = sF1,
inference(step,[status(thm)],[t9196,t32]) ).
cnf(t770,plain,
log(sF3) = sF1,
inference(orient,[status(thm)],[t9197]) ).
cnf(t9348,plain,
log(e(sF2)) = s(sF1),
inference(step,[status(thm)],[t9347,t770]) ).
cnf(t9349,plain,
log(e(sF2)) = sF2,
inference(step,[status(thm)],[t9348,t55]) ).
cnf(t1040,plain,
log(e(sF2)) = sF2,
inference(orient,[status(thm)],[t9349]) ).
cnf(t10063,plain,
sF5 = s(sF2),
inference(step,[status(thm)],[t10062,t1040]) ).
cnf(t10064,plain,
sF5 = sF3,
inference(step,[status(thm)],[t10063,t272]) ).
cnf(t9013,plain,
sF5 = sF3,
inference(orient,[status(thm)],[t10064]) ).
cnf(t10065,plain,
log(sF4) = sF3,
inference(step,[status(thm)],[t345,t9013]) ).
cnf(t9014,plain,
log(sF4) = sF3,
inference(orient,[status(thm)],[t10065]) ).
cnf(goal_0,negated_conjecture,
log(e(s(s(s(s(zero)))))) != s(s(s(s(zero)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
log(e(s(s(s(sF0))))) != s(s(s(s(zero)))),
inference(rw,[status(thm)],[goal_0,t23]) ).
cnf(g0_1,plain,
log(e(s(s(sF1)))) != s(s(s(s(zero)))),
inference(rw,[status(thm)],[g0_0,t32]) ).
cnf(g0_2,plain,
log(e(s(sF2))) != s(s(s(s(zero)))),
inference(rw,[status(thm)],[g0_1,t55]) ).
cnf(g0_3,plain,
log(e(sF3)) != s(s(s(s(zero)))),
inference(rw,[status(thm)],[g0_2,t272]) ).
cnf(g0_4,plain,
log(sF4) != s(s(s(s(zero)))),
inference(rw,[status(thm)],[g0_3,t315]) ).
cnf(g0_5,plain,
sF3 != s(s(s(s(zero)))),
inference(rw,[status(thm)],[g0_4,t9014]) ).
cnf(g0_6,plain,
sF3 != s(s(s(sF0))),
inference(rw,[status(thm)],[g0_5,t23]) ).
cnf(g0_7,plain,
sF3 != s(s(sF1)),
inference(rw,[status(thm)],[g0_6,t32]) ).
cnf(g0_8,plain,
sF3 != s(sF2),
inference(rw,[status(thm)],[g0_7,t55]) ).
cnf(g0_9,plain,
sF3 != sF3,
inference(rw,[status(thm)],[g0_8,t272]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_9]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ARI765-1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.11/5.37 % Computer : n015.cluster.edu
% 0.11/5.37 % Model : x86_64 x86_64
% 0.11/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.37 % Memory : 8046.5625MB
% 0.11/5.37 % OS : Linux 6.8.0-71-generic
% 0.11/5.37 % CPULimit : 300
% 0.11/5.37 % WCLimit : 300
% 0.11/5.37 % DateTime : Fri Sep 25 06:28:47 UTC 2026
% 0.11/5.37 % CPUTime :
% 0.11/5.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 25.34/8.69 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 25.34/8.69 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------