%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LCL153-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 02:01:05 PM UTC 2026
% Result : Unsatisfiable 8.33s 1.73s
% Output : CNFRefutation 8.33s
% Verified :
% SZS Type : Refutation
% Derivation depth : 60
% Number of leaves : 17
% Syntax : Number of clauses : 191 ( 191 unt; 0 nHn; 126 RR)
% Number of literals : 191 ( 190 equ; 20 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 : 14 ( 14 usr; 9 con; 0-2 aty)
% Number of variables : 97 ( 7 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t3,axiom,
implies(implies(X1,X2),X2) = implies(implies(X2,X1),X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t77,plain,
implies(implies(X1,X2),X2) = implies(implies(X2,X1),X1),
inference(orient,[status(thm)],[t3]) ).
cnf(u1,axiom,
or(X,Y) = or(Y,X),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(d0,axiom,
or(X,Y) = implies(not(X),Y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t2,plain,
implies(not(X1),X2) = implies(not(X2),X1),
inference(definition_unfolding,[status(thm)],[u1,d0]) ).
cnf(t40,plain,
implies(not(X1),X2) = implies(not(X2),X1),
inference(orient,[status(thm)],[t2]) ).
cnf(t13,axiom,
sF1 = not(not(x)),
introduced(definition) ).
cnf(t12,axiom,
sF0 = not(x),
introduced(definition) ).
cnf(t24,plain,
not(x) = sF0,
inference(orient,[status(thm)],[t12]) ).
cnf(t1271,plain,
sF1 = not(sF0),
inference(step,[status(thm)],[t13,t24]) ).
cnf(t29,plain,
not(sF0) = sF1,
inference(orient,[status(thm)],[t1271]) ).
cnf(t43,plain,
implies(not(X1),sF0) = implies(sF1,X1),
inference(cp,[status(thm)],[t40,t29]) ).
cnf(t70,plain,
implies(not(X1),sF0) = implies(sF1,X1),
inference(orient,[status(thm)],[t43]) ).
cnf(t15,axiom,
sF3 = not(not(truth)),
introduced(definition) ).
cnf(t0,axiom,
not(truth) = falsehood,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t23,plain,
not(truth) = falsehood,
inference(orient,[status(thm)],[t0]) ).
cnf(t14,axiom,
sF2 = not(truth),
introduced(definition) ).
cnf(t1268,plain,
sF2 = falsehood,
inference(step,[status(thm)],[t14,t23]) ).
cnf(t25,plain,
falsehood = sF2,
inference(orient,[status(thm)],[t1268]) ).
cnf(t1269,plain,
not(truth) = sF2,
inference(step,[status(thm)],[t23,t25]) ).
cnf(t26,plain,
not(truth) = sF2,
inference(orient,[status(thm)],[t1269]) ).
cnf(t1272,plain,
sF3 = not(sF2),
inference(step,[status(thm)],[t15,t26]) ).
cnf(t30,plain,
not(sF2) = sF3,
inference(orient,[status(thm)],[t1272]) ).
cnf(t71,plain,
implies(sF1,sF2) = implies(sF3,sF0),
inference(cp,[status(thm)],[t70,t30]) ).
cnf(t94,plain,
implies(sF3,sF0) = implies(sF1,sF2),
inference(orient,[status(thm)],[t71]) ).
cnf(t1,axiom,
implies(truth,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t28,plain,
implies(truth,X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t4,axiom,
implies(implies(not(X1),not(X2)),implies(X2,X1)) = truth,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t122,plain,
implies(implies(not(X1),not(X2)),implies(X2,X1)) = truth,
inference(orient,[status(thm)],[t4]) ).
cnf(t124,plain,
truth = implies(implies(not(X1),sF2),implies(truth,X1)),
inference(cp,[status(thm)],[t122,t26]) ).
cnf(t44,plain,
implies(not(X1),sF2) = implies(sF3,X1),
inference(cp,[status(thm)],[t40,t30]) ).
cnf(t98,plain,
implies(not(X1),sF2) = implies(sF3,X1),
inference(orient,[status(thm)],[t44]) ).
cnf(t1286,plain,
truth = implies(implies(sF3,X1),implies(truth,X1)),
inference(step,[status(thm)],[t124,t98]) ).
cnf(t1287,plain,
truth = implies(implies(sF3,X1),X1),
inference(step,[status(thm)],[t1286,t28]) ).
cnf(t305,plain,
implies(implies(sF3,X1),X1) = truth,
inference(orient,[status(thm)],[t1287]) ).
cnf(t41,plain,
implies(not(X1),truth) = implies(sF2,X1),
inference(cp,[status(thm)],[t40,t26]) ).
cnf(t50,plain,
implies(not(X1),truth) = implies(sF2,X1),
inference(orient,[status(thm)],[t41]) ).
cnf(t53,plain,
implies(sF2,sF2) = implies(sF3,truth),
inference(cp,[status(thm)],[t50,t30]) ).
cnf(t60,plain,
implies(sF3,truth) = implies(sF2,sF2),
inference(orient,[status(thm)],[t53]) ).
cnf(t306,plain,
truth = implies(implies(sF2,sF2),truth),
inference(cp,[status(thm)],[t305,t60]) ).
cnf(t86,plain,
implies(implies(truth,sF3),sF3) = implies(implies(sF2,sF2),truth),
inference(cp,[status(thm)],[t77,t60]) ).
cnf(t1280,plain,
implies(sF3,sF3) = implies(implies(sF2,sF2),truth),
inference(step,[status(thm)],[t86,t28]) ).
cnf(t163,plain,
implies(implies(sF2,sF2),truth) = implies(sF3,sF3),
inference(orient,[status(thm)],[t1280]) ).
cnf(t1288,plain,
truth = implies(sF3,sF3),
inference(step,[status(thm)],[t306,t163]) ).
cnf(t316,plain,
implies(sF3,sF3) = truth,
inference(orient,[status(thm)],[t1288]) ).
cnf(t319,plain,
implies(implies(sF3,sF3),sF3) = implies(truth,sF3),
inference(cp,[status(thm)],[t77,t316]) ).
cnf(t1291,plain,
truth = implies(truth,sF3),
inference(step,[status(thm)],[t319,t305]) ).
cnf(t1292,plain,
truth = sF3,
inference(step,[status(thm)],[t1291,t28]) ).
cnf(t324,plain,
truth = sF3,
inference(orient,[status(thm)],[t1292]) ).
cnf(t1294,plain,
implies(sF3,X1) = X1,
inference(step,[status(thm)],[t28,t324]) ).
cnf(t326,plain,
implies(sF3,X1) = X1,
inference(rw,[status(thm)],[t1294]) ).
cnf(t349,plain,
implies(sF3,X1) = X1,
inference(orient,[status(thm)],[t326]) ).
cnf(t1312,plain,
sF0 = implies(sF1,sF2),
inference(step,[status(thm)],[t94,t349]) ).
cnf(t351,plain,
sF0 = implies(sF1,sF2),
inference(rw,[status(thm)],[t1312]) ).
cnf(t387,plain,
implies(sF1,sF2) = sF0,
inference(orient,[status(thm)],[t351]) ).
cnf(t389,plain,
implies(implies(sF2,sF1),sF1) = implies(sF0,sF2),
inference(cp,[status(thm)],[t77,t387]) ).
cnf(t19,axiom,
sF7 = not(not(not(x))),
introduced(definition) ).
cnf(t1273,plain,
sF7 = not(not(sF0)),
inference(step,[status(thm)],[t19,t24]) ).
cnf(t1274,plain,
sF7 = not(sF1),
inference(step,[status(thm)],[t1273,t29]) ).
cnf(t31,plain,
not(sF1) = sF7,
inference(orient,[status(thm)],[t1274]) ).
cnf(t45,plain,
implies(not(X1),sF1) = implies(sF7,X1),
inference(cp,[status(thm)],[t40,t31]) ).
cnf(t107,plain,
implies(not(X1),sF1) = implies(sF7,X1),
inference(orient,[status(thm)],[t45]) ).
cnf(u0,axiom,
or(or(X,Y),Z) = or(X,or(Y,Z)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t6,plain,
implies(not(implies(not(X1),X2)),X3) = implies(not(X1),implies(not(X2),X3)),
inference(definition_unfolding,[status(thm)],[u0,d0]) ).
cnf(t32,plain,
implies(not(implies(not(X1),X2)),X3) = implies(not(X1),implies(not(X2),X3)),
inference(orient,[status(thm)],[t6]) ).
cnf(t34,plain,
implies(not(x),implies(not(X1),X2)) = implies(not(implies(sF0,X1)),X2),
inference(cp,[status(thm)],[t32,t24]) ).
cnf(t1276,plain,
implies(sF0,implies(not(X1),X2)) = implies(not(implies(sF0,X1)),X2),
inference(step,[status(thm)],[t34,t24]) ).
cnf(t39,plain,
implies(not(implies(sF0,X1)),X2) = implies(sF0,implies(not(X1),X2)),
inference(orient,[status(thm)],[t1276]) ).
cnf(t110,plain,
implies(sF7,implies(sF0,X1)) = implies(sF0,implies(not(X1),sF1)),
inference(cp,[status(thm)],[t107,t39]) ).
cnf(t1285,plain,
implies(sF7,implies(sF0,X1)) = implies(sF0,implies(sF7,X1)),
inference(step,[status(thm)],[t110,t107]) ).
cnf(t300,plain,
implies(sF7,implies(sF0,X1)) = implies(sF0,implies(sF7,X1)),
inference(orient,[status(thm)],[t1285]) ).
cnf(t1307,plain,
implies(implies(sF3,X1),X1) = sF3,
inference(step,[status(thm)],[t305,t324]) ).
cnf(t341,plain,
implies(implies(sF3,X1),X1) = sF3,
inference(orient,[status(thm)],[t1307]) ).
cnf(t1318,plain,
implies(X1,X1) = sF3,
inference(step,[status(thm)],[t341,t349]) ).
cnf(t359,plain,
implies(X1,X1) = sF3,
inference(rw,[status(thm)],[t1318]) ).
cnf(t393,plain,
implies(X1,X1) = sF3,
inference(orient,[status(thm)],[t359]) ).
cnf(t409,plain,
implies(sF0,implies(sF7,sF0)) = implies(sF7,sF3),
inference(cp,[status(thm)],[t300,t393]) ).
cnf(t72,plain,
implies(sF1,sF1) = implies(sF7,sF0),
inference(cp,[status(thm)],[t70,t31]) ).
cnf(t96,plain,
implies(sF7,sF0) = implies(sF1,sF1),
inference(orient,[status(thm)],[t72]) ).
cnf(t1324,plain,
implies(sF7,sF0) = sF3,
inference(step,[status(thm)],[t96,t393]) ).
cnf(t396,plain,
implies(sF7,sF0) = sF3,
inference(orient,[status(thm)],[t1324]) ).
cnf(t1327,plain,
implies(sF0,sF3) = implies(sF7,sF3),
inference(step,[status(thm)],[t409,t396]) ).
cnf(t54,plain,
implies(sF2,sF1) = implies(sF7,truth),
inference(cp,[status(thm)],[t50,t31]) ).
cnf(t61,plain,
implies(sF7,truth) = implies(sF2,sF1),
inference(orient,[status(thm)],[t54]) ).
cnf(t1300,plain,
implies(sF7,sF3) = implies(sF2,sF1),
inference(step,[status(thm)],[t61,t324]) ).
cnf(t333,plain,
implies(sF7,sF3) = implies(sF2,sF1),
inference(rw,[status(thm)],[t1300]) ).
cnf(t366,plain,
implies(sF7,sF3) = implies(sF2,sF1),
inference(orient,[status(thm)],[t333]) ).
cnf(t1328,plain,
implies(sF0,sF3) = implies(sF2,sF1),
inference(step,[status(thm)],[t1327,t366]) ).
cnf(t411,plain,
implies(sF2,sF1) = implies(sF0,sF3),
inference(orient,[status(thm)],[t1328]) ).
cnf(t1339,plain,
implies(implies(sF0,sF3),sF1) = implies(sF0,sF2),
inference(step,[status(thm)],[t389,t411]) ).
cnf(t42,plain,
implies(not(X1),x) = implies(sF0,X1),
inference(cp,[status(thm)],[t40,t24]) ).
cnf(t62,plain,
implies(not(X1),x) = implies(sF0,X1),
inference(orient,[status(thm)],[t42]) ).
cnf(t64,plain,
implies(sF0,sF2) = implies(sF3,x),
inference(cp,[status(thm)],[t62,t30]) ).
cnf(t68,plain,
implies(sF3,x) = implies(sF0,sF2),
inference(orient,[status(thm)],[t64]) ).
cnf(t1311,plain,
x = implies(sF0,sF2),
inference(step,[status(thm)],[t68,t349]) ).
cnf(t350,plain,
x = implies(sF0,sF2),
inference(rw,[status(thm)],[t1311]) ).
cnf(t381,plain,
implies(sF0,sF2) = x,
inference(orient,[status(thm)],[t350]) ).
cnf(t1340,plain,
implies(implies(sF0,sF3),sF1) = x,
inference(step,[status(thm)],[t1339,t381]) ).
cnf(t451,plain,
implies(implies(sF0,sF3),sF1) = x,
inference(orient,[status(thm)],[t1340]) ).
cnf(t945,plain,
implies(sF3,sF1) = x,
inference(rw,[status(thm)],[t451]) ).
cnf(t1428,plain,
sF1 = x,
inference(step,[status(thm)],[t945,t349]) ).
cnf(t954,plain,
x = sF1,
inference(orient,[status(thm)],[t1428]) ).
cnf(t955,plain,
not(sF1) = sF0,
inference(rw,[status(thm)],[t24]) ).
cnf(t1433,plain,
sF7 = sF0,
inference(step,[status(thm)],[t955,t31]) ).
cnf(t967,plain,
sF7 = sF0,
inference(orient,[status(thm)],[t1433]) ).
cnf(t1434,plain,
not(sF1) = sF0,
inference(step,[status(thm)],[t31,t967]) ).
cnf(t968,plain,
not(sF1) = sF0,
inference(orient,[status(thm)],[t1434]) ).
cnf(t1293,plain,
not(sF3) = sF2,
inference(step,[status(thm)],[t26,t324]) ).
cnf(t325,plain,
not(sF3) = sF2,
inference(rw,[status(thm)],[t1293]) ).
cnf(t345,plain,
not(sF3) = sF2,
inference(orient,[status(thm)],[t325]) ).
cnf(t16,axiom,
sF4 = implies(not(not(x)),not(not(truth))),
introduced(definition) ).
cnf(t1366,plain,
sF4 = implies(not(sF0),not(not(truth))),
inference(step,[status(thm)],[t16,t24]) ).
cnf(t1367,plain,
sF4 = implies(sF1,not(not(truth))),
inference(step,[status(thm)],[t1366,t29]) ).
cnf(t1368,plain,
sF4 = implies(sF1,not(not(sF3))),
inference(step,[status(thm)],[t1367,t324]) ).
cnf(t1369,plain,
sF4 = implies(sF1,not(sF2)),
inference(step,[status(thm)],[t1368,t345]) ).
cnf(t1370,plain,
sF4 = implies(sF1,sF3),
inference(step,[status(thm)],[t1369,t30]) ).
cnf(t666,plain,
implies(sF1,sF3) = sF4,
inference(orient,[status(thm)],[t1370]) ).
cnf(t5,axiom,
implies(implies(X1,X2),implies(implies(X2,X3),implies(X1,X3))) = truth,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t188,plain,
implies(implies(X1,X2),implies(implies(X2,X3),implies(X1,X3))) = truth,
inference(orient,[status(thm)],[t5]) ).
cnf(t1305,plain,
implies(implies(X1,X2),implies(implies(X2,X3),implies(X1,X3))) = sF3,
inference(step,[status(thm)],[t188,t324]) ).
cnf(t339,plain,
implies(implies(X1,X2),implies(implies(X2,X3),implies(X1,X3))) = sF3,
inference(orient,[status(thm)],[t1305]) ).
cnf(t673,plain,
implies(implies(sF3,sF1),sF1) = implies(sF4,sF3),
inference(cp,[status(thm)],[t77,t666]) ).
cnf(t1377,plain,
implies(implies(sF1,sF3),sF3) = implies(sF4,sF3),
inference(step,[status(thm)],[t673,t77]) ).
cnf(t308,plain,
truth = implies(implies(X1,sF3),sF3),
inference(cp,[status(thm)],[t305,t77]) ).
cnf(t1336,plain,
sF3 = implies(implies(X1,sF3),sF3),
inference(step,[status(thm)],[t308,t324]) ).
cnf(t433,plain,
implies(implies(X1,sF3),sF3) = sF3,
inference(orient,[status(thm)],[t1336]) ).
cnf(t1378,plain,
sF3 = implies(sF4,sF3),
inference(step,[status(thm)],[t1377,t433]) ).
cnf(t694,plain,
implies(sF4,sF3) = sF3,
inference(orient,[status(thm)],[t1378]) ).
cnf(t697,plain,
sF3 = implies(implies(sF4,X1),implies(implies(X1,sF3),sF3)),
inference(cp,[status(thm)],[t339,t694]) ).
cnf(t1421,plain,
sF3 = implies(implies(sF4,X1),sF3),
inference(step,[status(thm)],[t697,t433]) ).
cnf(t933,plain,
implies(implies(sF4,X1),sF3) = sF3,
inference(orient,[status(thm)],[t1421]) ).
cnf(t99,plain,
implies(sF3,sF1) = implies(sF7,sF2),
inference(cp,[status(thm)],[t98,t31]) ).
cnf(t105,plain,
implies(sF7,sF2) = implies(sF3,sF1),
inference(orient,[status(thm)],[t99]) ).
cnf(t106,plain,
implies(implies(sF2,sF7),sF7) = implies(implies(sF3,sF1),sF2),
inference(cp,[status(thm)],[t77,t105]) ).
cnf(t185,plain,
implies(implies(sF3,sF1),sF2) = implies(implies(sF2,sF7),sF7),
inference(orient,[status(thm)],[t106]) ).
cnf(t1317,plain,
implies(sF1,sF2) = implies(implies(sF2,sF7),sF7),
inference(step,[status(thm)],[t185,t349]) ).
cnf(t358,plain,
implies(sF1,sF2) = implies(implies(sF2,sF7),sF7),
inference(rw,[status(thm)],[t1317]) ).
cnf(t1338,plain,
sF0 = implies(implies(sF2,sF7),sF7),
inference(step,[status(thm)],[t358,t387]) ).
cnf(t445,plain,
implies(implies(sF2,sF7),sF7) = sF0,
inference(orient,[status(thm)],[t1338]) ).
cnf(t35,plain,
implies(not(sF0),implies(not(X1),X2)) = implies(not(implies(sF1,X1)),X2),
inference(cp,[status(thm)],[t32,t29]) ).
cnf(t1355,plain,
implies(sF1,implies(not(X1),X2)) = implies(not(implies(sF1,X1)),X2),
inference(step,[status(thm)],[t35,t29]) ).
cnf(t537,plain,
implies(not(implies(sF1,X1)),X2) = implies(sF1,implies(not(X1),X2)),
inference(orient,[status(thm)],[t1355]) ).
cnf(t541,plain,
implies(sF1,implies(not(sF1),X1)) = implies(not(sF3),X1),
inference(cp,[status(thm)],[t537,t393]) ).
cnf(t1357,plain,
implies(sF1,implies(sF7,X1)) = implies(not(sF3),X1),
inference(step,[status(thm)],[t541,t31]) ).
cnf(t1358,plain,
implies(sF1,implies(sF7,X1)) = implies(sF2,X1),
inference(step,[status(thm)],[t1357,t345]) ).
cnf(t555,plain,
implies(sF1,implies(sF7,X1)) = implies(sF2,X1),
inference(orient,[status(thm)],[t1358]) ).
cnf(t558,plain,
implies(sF2,sF7) = implies(sF1,sF3),
inference(cp,[status(thm)],[t555,t393]) ).
cnf(t565,plain,
implies(sF2,sF7) = implies(sF1,sF3),
inference(orient,[status(thm)],[t558]) ).
cnf(t1361,plain,
implies(implies(sF1,sF3),sF7) = sF0,
inference(step,[status(thm)],[t445,t565]) ).
cnf(t566,plain,
implies(implies(sF1,sF3),sF7) = sF0,
inference(rw,[status(thm)],[t1361]) ).
cnf(t573,plain,
implies(implies(sF1,sF3),sF7) = sF0,
inference(orient,[status(thm)],[t566]) ).
cnf(t1376,plain,
implies(sF4,sF7) = sF0,
inference(step,[status(thm)],[t573,t666]) ).
cnf(t672,plain,
implies(sF4,sF7) = sF0,
inference(rw,[status(thm)],[t1376]) ).
cnf(t688,plain,
implies(sF4,sF7) = sF0,
inference(orient,[status(thm)],[t672]) ).
cnf(t934,plain,
sF3 = implies(sF0,sF3),
inference(cp,[status(thm)],[t933,t688]) ).
cnf(t938,plain,
implies(sF0,sF3) = sF3,
inference(orient,[status(thm)],[t934]) ).
cnf(t953,plain,
sF3 = implies(implies(sF0,X1),implies(implies(X1,sF3),sF3)),
inference(cp,[status(thm)],[t339,t938]) ).
cnf(t1506,plain,
sF3 = implies(implies(sF0,X1),sF3),
inference(step,[status(thm)],[t953,t433]) ).
cnf(t1226,plain,
implies(implies(sF0,X1),sF3) = sF3,
inference(orient,[status(thm)],[t1506]) ).
cnf(t1430,plain,
implies(sF0,sF2) = sF1,
inference(step,[status(thm)],[t381,t954]) ).
cnf(t960,plain,
implies(sF0,sF2) = sF1,
inference(orient,[status(thm)],[t1430]) ).
cnf(t1227,plain,
sF3 = implies(sF1,sF3),
inference(cp,[status(thm)],[t1226,t960]) ).
cnf(t1507,plain,
sF3 = sF4,
inference(step,[status(thm)],[t1227,t666]) ).
cnf(t1231,plain,
sF4 = sF3,
inference(orient,[status(thm)],[t1507]) ).
cnf(t1510,plain,
implies(sF1,sF3) = sF3,
inference(step,[status(thm)],[t666,t1231]) ).
cnf(t1234,plain,
implies(sF1,sF3) = sF3,
inference(orient,[status(thm)],[t1510]) ).
cnf(u8,negated_conjecture,
not(x) != xor(x,truth),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(u3,axiom,
xor(X,Y) = or(and(X,not(Y)),and(not(X),Y)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(u2,axiom,
and(X,Y) = not(or(not(X),not(Y))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(d1,axiom,
and(X,Y) = not(implies(not(not(X)),not(Y))),
inference(definition_unfolding,[status(thm)],[u2,d0]) ).
cnf(d2,axiom,
xor(X,Y) = implies(not(not(implies(not(not(X)),not(not(Y))))),not(implies(not(not(not(X))),not(Y)))),
inference(definition_unfolding,[status(thm)],[u3,d0,d1]) ).
cnf(goal_0,negated_conjecture,
implies(not(not(implies(not(not(x)),not(not(truth))))),not(implies(not(not(not(x))),not(truth)))) != not(x),
inference(definition_unfolding,[status(thm)],[u8,d2]) ).
cnf(g0_0,plain,
implies(not(not(implies(not(not(sF1)),not(not(truth))))),not(implies(not(not(not(x))),not(truth)))) != not(x),
inference(rw,[status(thm)],[goal_0,t954]) ).
cnf(g0_1,plain,
implies(not(not(implies(not(sF0),not(not(truth))))),not(implies(not(not(not(x))),not(truth)))) != not(x),
inference(rw,[status(thm)],[g0_0,t968]) ).
cnf(g0_2,plain,
implies(not(not(implies(sF1,not(not(truth))))),not(implies(not(not(not(x))),not(truth)))) != not(x),
inference(rw,[status(thm)],[g0_1,t29]) ).
cnf(g0_3,plain,
implies(not(not(implies(sF1,not(not(sF3))))),not(implies(not(not(not(x))),not(truth)))) != not(x),
inference(rw,[status(thm)],[g0_2,t324]) ).
cnf(g0_4,plain,
implies(not(not(implies(sF1,not(sF2)))),not(implies(not(not(not(x))),not(truth)))) != not(x),
inference(rw,[status(thm)],[g0_3,t345]) ).
cnf(g0_5,plain,
implies(not(not(implies(sF1,sF3))),not(implies(not(not(not(x))),not(truth)))) != not(x),
inference(rw,[status(thm)],[g0_4,t30]) ).
cnf(g0_6,plain,
implies(not(not(sF3)),not(implies(not(not(not(x))),not(truth)))) != not(x),
inference(rw,[status(thm)],[g0_5,t1234]) ).
cnf(g0_7,plain,
implies(not(sF2),not(implies(not(not(not(x))),not(truth)))) != not(x),
inference(rw,[status(thm)],[g0_6,t345]) ).
cnf(g0_8,plain,
implies(sF3,not(implies(not(not(not(x))),not(truth)))) != not(x),
inference(rw,[status(thm)],[g0_7,t30]) ).
cnf(g0_9,plain,
not(implies(not(not(not(x))),not(truth))) != not(x),
inference(rw,[status(thm)],[g0_8,t349]) ).
cnf(g0_10,plain,
not(implies(not(not(not(sF1))),not(truth))) != not(x),
inference(rw,[status(thm)],[g0_9,t954]) ).
cnf(g0_11,plain,
not(implies(not(not(sF0)),not(truth))) != not(x),
inference(rw,[status(thm)],[g0_10,t968]) ).
cnf(g0_12,plain,
not(implies(not(sF1),not(truth))) != not(x),
inference(rw,[status(thm)],[g0_11,t29]) ).
cnf(g0_13,plain,
not(implies(sF0,not(truth))) != not(x),
inference(rw,[status(thm)],[g0_12,t968]) ).
cnf(g0_14,plain,
not(implies(sF0,not(sF3))) != not(x),
inference(rw,[status(thm)],[g0_13,t324]) ).
cnf(g0_15,plain,
not(implies(sF0,sF2)) != not(x),
inference(rw,[status(thm)],[g0_14,t345]) ).
cnf(g0_16,plain,
not(sF1) != not(x),
inference(rw,[status(thm)],[g0_15,t960]) ).
cnf(g0_17,plain,
not(sF1) != not(sF1),
inference(rw,[status(thm)],[g0_16,t954]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_17]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : LCL153-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.07 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.19/0.45 % Computer : n014.cluster.edu
% 0.19/0.45 % Model : x86_64 x86_64
% 0.19/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.45 % Memory : 8046.5625MB
% 0.19/0.45 % OS : Linux 6.8.0-71-generic
% 0.19/0.45 % CPULimit : 300
% 0.19/0.45 % WCLimit : 300
% 0.19/0.45 % DateTime : Wed Sep 23 22:06:33 UTC 2026
% 0.19/0.45 % CPUTime :
% 0.19/0.45 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 8.33/1.73 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.33/1.73 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------