%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LCL154-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n012.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 3.36s 0.81s
% Output : CNFRefutation 3.36s
% Verified :
% SZS Type : Refutation
% Derivation depth : 49
% Number of leaves : 18
% Syntax : Number of clauses : 216 ( 216 unt; 0 nHn; 147 RR)
% Number of literals : 216 ( 215 equ; 18 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 : 15 ( 15 usr; 10 con; 0-2 aty)
% Number of variables : 101 ( 8 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t12,axiom,
sF0 = not(x),
introduced(definition) ).
cnf(t24,plain,
not(x) = sF0,
inference(orient,[status(thm)],[t12]) ).
cnf(t13,axiom,
sF1 = not(not(x)),
introduced(definition) ).
cnf(t2018,plain,
sF1 = not(sF0),
inference(step,[status(thm)],[t13,t24]) ).
cnf(t27,plain,
not(sF0) = sF1,
inference(orient,[status(thm)],[t2018]) ).
cnf(t0,axiom,
not(truth) = falsehood,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t23,plain,
not(truth) = falsehood,
inference(orient,[status(thm)],[t0]) ).
cnf(t444,plain,
not(sF2) = falsehood,
inference(rw,[status(thm)],[t23]) ).
cnf(t15,axiom,
sF3 = not(not(falsehood)),
introduced(definition) ).
cnf(t14,axiom,
sF2 = not(falsehood),
introduced(definition) ).
cnf(t25,plain,
not(falsehood) = sF2,
inference(orient,[status(thm)],[t14]) ).
cnf(t2019,plain,
sF3 = not(sF2),
inference(step,[status(thm)],[t15,t25]) ).
cnf(t28,plain,
not(sF2) = sF3,
inference(orient,[status(thm)],[t2019]) ).
cnf(t2077,plain,
sF3 = falsehood,
inference(step,[status(thm)],[t444,t28]) ).
cnf(t479,plain,
falsehood = sF3,
inference(orient,[status(thm)],[t2077]) ).
cnf(t2078,plain,
not(sF3) = sF2,
inference(step,[status(thm)],[t25,t479]) ).
cnf(t480,plain,
not(sF3) = sF2,
inference(rw,[status(thm)],[t2078]) ).
cnf(t502,plain,
not(sF3) = sF2,
inference(orient,[status(thm)],[t480]) ).
cnf(u1,axiom,
or(X,Y) = or(Y,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(d0,axiom,
or(X,Y) = implies(not(X),Y),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t2,plain,
implies(not(X1),X2) = implies(not(X2),X1),
inference(definition_unfolding,[status(thm)],[u1,d0]) ).
cnf(t39,plain,
implies(not(X1),X2) = implies(not(X2),X1),
inference(orient,[status(thm)],[t2]) ).
cnf(t42,plain,
implies(not(X1),falsehood) = implies(sF2,X1),
inference(cp,[status(thm)],[t39,t25]) ).
cnf(t94,plain,
implies(not(X1),falsehood) = implies(sF2,X1),
inference(orient,[status(thm)],[t42]) ).
cnf(t95,plain,
implies(sF2,sF0) = implies(sF1,falsehood),
inference(cp,[status(thm)],[t94,t27]) ).
cnf(t103,plain,
implies(sF2,sF0) = implies(sF1,falsehood),
inference(orient,[status(thm)],[t95]) ).
cnf(t2083,plain,
implies(sF2,sF0) = implies(sF1,sF3),
inference(step,[status(thm)],[t103,t479]) ).
cnf(t490,plain,
implies(sF2,sF0) = implies(sF1,sF3),
inference(orient,[status(thm)],[t2083]) ).
cnf(t1,axiom,
implies(truth,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t26,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/sandbox2/benchmark/theBenchmark.p') ).
cnf(t130,plain,
implies(implies(not(X1),not(X2)),implies(X2,X1)) = truth,
inference(orient,[status(thm)],[t4]) ).
cnf(t132,plain,
truth = implies(implies(not(X1),falsehood),implies(truth,X1)),
inference(cp,[status(thm)],[t130,t23]) ).
cnf(t2031,plain,
truth = implies(implies(sF2,X1),implies(truth,X1)),
inference(step,[status(thm)],[t132,t94]) ).
cnf(t2032,plain,
truth = implies(implies(sF2,X1),X1),
inference(step,[status(thm)],[t2031,t26]) ).
cnf(t375,plain,
implies(implies(sF2,X1),X1) = truth,
inference(orient,[status(thm)],[t2032]) ).
cnf(t3,axiom,
implies(implies(X1,X2),X2) = implies(implies(X2,X1),X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t76,plain,
implies(implies(X1,X2),X2) = implies(implies(X2,X1),X1),
inference(orient,[status(thm)],[t3]) ).
cnf(t381,plain,
truth = implies(implies(X1,sF2),sF2),
inference(cp,[status(thm)],[t375,t76]) ).
cnf(t430,plain,
implies(implies(X1,sF2),sF2) = truth,
inference(orient,[status(thm)],[t381]) ).
cnf(t438,plain,
truth = implies(implies(implies(sF2,X1),X1),sF2),
inference(cp,[status(thm)],[t430,t76]) ).
cnf(t2050,plain,
truth = implies(truth,sF2),
inference(step,[status(thm)],[t438,t375]) ).
cnf(t2051,plain,
truth = sF2,
inference(step,[status(thm)],[t2050,t26]) ).
cnf(t443,plain,
truth = sF2,
inference(orient,[status(thm)],[t2051]) ).
cnf(t2052,plain,
implies(sF2,X1) = X1,
inference(step,[status(thm)],[t26,t443]) ).
cnf(t445,plain,
implies(sF2,X1) = X1,
inference(rw,[status(thm)],[t2052]) ).
cnf(t506,plain,
implies(sF2,X1) = X1,
inference(orient,[status(thm)],[t445]) ).
cnf(t2092,plain,
sF0 = implies(sF1,sF3),
inference(step,[status(thm)],[t490,t506]) ).
cnf(t508,plain,
sF0 = implies(sF1,sF3),
inference(rw,[status(thm)],[t2092]) ).
cnf(t558,plain,
implies(sF1,sF3) = sF0,
inference(orient,[status(thm)],[t508]) ).
cnf(t19,axiom,
sF7 = not(not(not(x))),
introduced(definition) ).
cnf(t2020,plain,
sF7 = not(not(sF0)),
inference(step,[status(thm)],[t19,t24]) ).
cnf(t2021,plain,
sF7 = not(sF1),
inference(step,[status(thm)],[t2020,t27]) ).
cnf(t29,plain,
not(sF1) = sF7,
inference(orient,[status(thm)],[t2021]) ).
cnf(t18,axiom,
sF6 = not(not(implies(not(not(x)),not(not(falsehood))))),
introduced(definition) ).
cnf(t2158,plain,
sF6 = not(not(implies(not(sF0),not(not(falsehood))))),
inference(step,[status(thm)],[t18,t24]) ).
cnf(t2159,plain,
sF6 = not(not(implies(sF1,not(not(falsehood))))),
inference(step,[status(thm)],[t2158,t27]) ).
cnf(t2160,plain,
sF6 = not(not(implies(sF1,not(not(sF3))))),
inference(step,[status(thm)],[t2159,t479]) ).
cnf(t2161,plain,
sF6 = not(not(implies(sF1,not(sF2)))),
inference(step,[status(thm)],[t2160,t502]) ).
cnf(t2162,plain,
sF6 = not(not(implies(sF1,sF3))),
inference(step,[status(thm)],[t2161,t28]) ).
cnf(t2163,plain,
sF6 = not(not(sF0)),
inference(step,[status(thm)],[t2162,t558]) ).
cnf(t2164,plain,
sF6 = not(sF1),
inference(step,[status(thm)],[t2163,t27]) ).
cnf(t2165,plain,
sF6 = sF7,
inference(step,[status(thm)],[t2164,t29]) ).
cnf(t807,plain,
sF7 = sF6,
inference(orient,[status(thm)],[t2165]) ).
cnf(t2166,plain,
not(sF1) = sF6,
inference(step,[status(thm)],[t29,t807]) ).
cnf(t808,plain,
not(sF1) = sF6,
inference(orient,[status(thm)],[t2166]) ).
cnf(t97,plain,
implies(sF2,sF1) = implies(sF7,falsehood),
inference(cp,[status(thm)],[t94,t29]) ).
cnf(t107,plain,
implies(sF7,falsehood) = implies(sF2,sF1),
inference(orient,[status(thm)],[t97]) ).
cnf(t2086,plain,
implies(sF7,sF3) = implies(sF2,sF1),
inference(step,[status(thm)],[t107,t479]) ).
cnf(t493,plain,
implies(sF7,sF3) = implies(sF2,sF1),
inference(rw,[status(thm)],[t2086]) ).
cnf(t2095,plain,
implies(sF7,sF3) = sF1,
inference(step,[status(thm)],[t493,t506]) ).
cnf(t516,plain,
implies(sF7,sF3) = sF1,
inference(orient,[status(thm)],[t2095]) ).
cnf(t517,plain,
implies(implies(sF3,sF7),sF7) = implies(sF1,sF3),
inference(cp,[status(thm)],[t76,t516]) ).
cnf(t2119,plain,
implies(implies(sF3,sF7),sF7) = sF0,
inference(step,[status(thm)],[t517,t558]) ).
cnf(t652,plain,
implies(implies(sF3,sF7),sF7) = sF0,
inference(orient,[status(thm)],[t2119]) ).
cnf(u0,axiom,
or(or(X,Y),Z) = or(X,or(Y,Z)),
file('/export/starexec/sandbox2/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(t30,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(sF0),implies(not(X1),X2)) = implies(not(implies(sF1,X1)),X2),
inference(cp,[status(thm)],[t30,t27]) ).
cnf(t2134,plain,
implies(sF1,implies(not(X1),X2)) = implies(not(implies(sF1,X1)),X2),
inference(step,[status(thm)],[t34,t27]) ).
cnf(t688,plain,
implies(not(implies(sF1,X1)),X2) = implies(sF1,implies(not(X1),X2)),
inference(orient,[status(thm)],[t2134]) ).
cnf(t2071,plain,
implies(implies(sF2,X1),X1) = sF2,
inference(step,[status(thm)],[t375,t443]) ).
cnf(t470,plain,
implies(implies(sF2,X1),X1) = sF2,
inference(orient,[status(thm)],[t2071]) ).
cnf(t2093,plain,
implies(X1,X1) = sF2,
inference(step,[status(thm)],[t470,t506]) ).
cnf(t510,plain,
implies(X1,X1) = sF2,
inference(rw,[status(thm)],[t2093]) ).
cnf(t563,plain,
implies(X1,X1) = sF2,
inference(orient,[status(thm)],[t510]) ).
cnf(t692,plain,
implies(sF1,implies(not(sF1),X1)) = implies(not(sF2),X1),
inference(cp,[status(thm)],[t688,t563]) ).
cnf(t2136,plain,
implies(sF1,implies(sF7,X1)) = implies(not(sF2),X1),
inference(step,[status(thm)],[t692,t29]) ).
cnf(t2137,plain,
implies(sF1,implies(sF7,X1)) = implies(sF3,X1),
inference(step,[status(thm)],[t2136,t28]) ).
cnf(t706,plain,
implies(sF1,implies(sF7,X1)) = implies(sF3,X1),
inference(orient,[status(thm)],[t2137]) ).
cnf(t710,plain,
implies(sF3,sF7) = implies(sF1,sF2),
inference(cp,[status(thm)],[t706,t563]) ).
cnf(t718,plain,
implies(sF3,sF7) = implies(sF1,sF2),
inference(orient,[status(thm)],[t710]) ).
cnf(t2140,plain,
implies(implies(sF1,sF2),sF7) = sF0,
inference(step,[status(thm)],[t652,t718]) ).
cnf(t719,plain,
implies(implies(sF1,sF2),sF7) = sF0,
inference(rw,[status(thm)],[t2140]) ).
cnf(t732,plain,
implies(implies(sF1,sF2),sF7) = sF0,
inference(orient,[status(thm)],[t719]) ).
cnf(t2181,plain,
implies(implies(sF1,sF2),sF6) = sF0,
inference(step,[status(thm)],[t732,t807]) ).
cnf(t823,plain,
implies(implies(sF1,sF2),sF6) = sF0,
inference(rw,[status(thm)],[t2181]) ).
cnf(t934,plain,
implies(implies(sF1,sF2),sF6) = sF0,
inference(orient,[status(thm)],[t823]) ).
cnf(t1867,plain,
implies(sF2,sF6) = sF0,
inference(rw,[status(thm)],[t934]) ).
cnf(t2356,plain,
sF6 = sF0,
inference(step,[status(thm)],[t1867,t506]) ).
cnf(t1989,plain,
sF6 = sF0,
inference(orient,[status(thm)],[t2356]) ).
cnf(t2357,plain,
not(sF1) = sF0,
inference(step,[status(thm)],[t808,t1989]) ).
cnf(t1990,plain,
not(sF1) = sF0,
inference(orient,[status(thm)],[t2357]) ).
cnf(t20,axiom,
sF8 = implies(not(not(not(x))),not(falsehood)),
introduced(definition) ).
cnf(t2183,plain,
sF8 = implies(not(not(falsehood)),not(not(x))),
inference(step,[status(thm)],[t20,t39]) ).
cnf(t2184,plain,
sF8 = implies(not(not(sF3)),not(not(x))),
inference(step,[status(thm)],[t2183,t479]) ).
cnf(t2185,plain,
sF8 = implies(not(sF2),not(not(x))),
inference(step,[status(thm)],[t2184,t502]) ).
cnf(t2186,plain,
sF8 = implies(sF3,not(not(x))),
inference(step,[status(thm)],[t2185,t28]) ).
cnf(t2187,plain,
sF8 = implies(sF3,not(sF0)),
inference(step,[status(thm)],[t2186,t24]) ).
cnf(t2188,plain,
sF8 = implies(sF3,sF1),
inference(step,[status(thm)],[t2187,t27]) ).
cnf(t45,plain,
implies(not(X1),sF1) = implies(sF7,X1),
inference(cp,[status(thm)],[t39,t29]) ).
cnf(t174,plain,
implies(not(X1),sF1) = implies(sF7,X1),
inference(orient,[status(thm)],[t45]) ).
cnf(t32,plain,
implies(not(x),implies(not(X1),X2)) = implies(not(implies(sF0,X1)),X2),
inference(cp,[status(thm)],[t30,t24]) ).
cnf(t2023,plain,
implies(sF0,implies(not(X1),X2)) = implies(not(implies(sF0,X1)),X2),
inference(step,[status(thm)],[t32,t24]) ).
cnf(t38,plain,
implies(not(implies(sF0,X1)),X2) = implies(sF0,implies(not(X1),X2)),
inference(orient,[status(thm)],[t2023]) ).
cnf(t177,plain,
implies(sF7,implies(sF0,X1)) = implies(sF0,implies(not(X1),sF1)),
inference(cp,[status(thm)],[t174,t38]) ).
cnf(t2038,plain,
implies(sF7,implies(sF0,X1)) = implies(sF0,implies(sF7,X1)),
inference(step,[status(thm)],[t177,t174]) ).
cnf(t398,plain,
implies(sF7,implies(sF0,X1)) = implies(sF0,implies(sF7,X1)),
inference(orient,[status(thm)],[t2038]) ).
cnf(t578,plain,
implies(sF0,implies(sF7,sF0)) = implies(sF7,sF2),
inference(cp,[status(thm)],[t398,t563]) ).
cnf(t43,plain,
implies(not(X1),sF0) = implies(sF1,X1),
inference(cp,[status(thm)],[t39,t27]) ).
cnf(t109,plain,
implies(not(X1),sF0) = implies(sF1,X1),
inference(orient,[status(thm)],[t43]) ).
cnf(t111,plain,
implies(sF1,sF1) = implies(sF7,sF0),
inference(cp,[status(thm)],[t109,t29]) ).
cnf(t119,plain,
implies(sF7,sF0) = implies(sF1,sF1),
inference(orient,[status(thm)],[t111]) ).
cnf(t2100,plain,
implies(sF7,sF0) = sF2,
inference(step,[status(thm)],[t119,t563]) ).
cnf(t566,plain,
implies(sF7,sF0) = sF2,
inference(orient,[status(thm)],[t2100]) ).
cnf(t2103,plain,
implies(sF0,sF2) = implies(sF7,sF2),
inference(step,[status(thm)],[t578,t566]) ).
cnf(t44,plain,
implies(not(X1),sF2) = implies(sF3,X1),
inference(cp,[status(thm)],[t39,t28]) ).
cnf(t121,plain,
implies(not(X1),sF2) = implies(sF3,X1),
inference(orient,[status(thm)],[t44]) ).
cnf(t122,plain,
implies(sF3,sF1) = implies(sF7,sF2),
inference(cp,[status(thm)],[t121,t29]) ).
cnf(t128,plain,
implies(sF7,sF2) = implies(sF3,sF1),
inference(orient,[status(thm)],[t122]) ).
cnf(t2104,plain,
implies(sF0,sF2) = implies(sF3,sF1),
inference(step,[status(thm)],[t2103,t128]) ).
cnf(t581,plain,
implies(sF3,sF1) = implies(sF0,sF2),
inference(orient,[status(thm)],[t2104]) ).
cnf(t2189,plain,
sF8 = implies(sF0,sF2),
inference(step,[status(thm)],[t2188,t581]) ).
cnf(t887,plain,
implies(sF0,sF2) = sF8,
inference(orient,[status(thm)],[t2189]) ).
cnf(t5,axiom,
implies(implies(X1,X2),implies(implies(X2,X3),implies(X1,X3))) = truth,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t196,plain,
implies(implies(X1,X2),implies(implies(X2,X3),implies(X1,X3))) = truth,
inference(orient,[status(thm)],[t5]) ).
cnf(t2065,plain,
implies(implies(X1,X2),implies(implies(X2,X3),implies(X1,X3))) = sF2,
inference(step,[status(thm)],[t196,t443]) ).
cnf(t464,plain,
implies(implies(X1,X2),implies(implies(X2,X3),implies(X1,X3))) = sF2,
inference(orient,[status(thm)],[t2065]) ).
cnf(t896,plain,
implies(implies(sF2,sF0),sF0) = implies(sF8,sF2),
inference(cp,[status(thm)],[t76,t887]) ).
cnf(t2197,plain,
implies(implies(sF0,sF2),sF2) = implies(sF8,sF2),
inference(step,[status(thm)],[t896,t76]) ).
cnf(t2075,plain,
implies(implies(X1,sF2),sF2) = sF2,
inference(step,[status(thm)],[t430,t443]) ).
cnf(t477,plain,
implies(implies(X1,sF2),sF2) = sF2,
inference(orient,[status(thm)],[t2075]) ).
cnf(t2198,plain,
sF2 = implies(sF8,sF2),
inference(step,[status(thm)],[t2197,t477]) ).
cnf(t910,plain,
implies(sF8,sF2) = sF2,
inference(orient,[status(thm)],[t2198]) ).
cnf(t913,plain,
sF2 = implies(implies(sF8,X1),implies(implies(X1,sF2),sF2)),
inference(cp,[status(thm)],[t464,t910]) ).
cnf(t2247,plain,
sF2 = implies(implies(sF8,X1),sF2),
inference(step,[status(thm)],[t913,t477]) ).
cnf(t1096,plain,
implies(implies(sF8,X1),sF2) = sF2,
inference(orient,[status(thm)],[t2247]) ).
cnf(t40,plain,
implies(not(X1),truth) = implies(falsehood,X1),
inference(cp,[status(thm)],[t39,t23]) ).
cnf(t50,plain,
implies(not(X1),truth) = implies(falsehood,X1),
inference(orient,[status(thm)],[t40]) ).
cnf(t55,plain,
implies(falsehood,sF1) = implies(sF7,truth),
inference(cp,[status(thm)],[t50,t29]) ).
cnf(t65,plain,
implies(falsehood,sF1) = implies(sF7,truth),
inference(orient,[status(thm)],[t55]) ).
cnf(t86,plain,
implies(implies(sF1,falsehood),falsehood) = implies(implies(sF7,truth),sF1),
inference(cp,[status(thm)],[t76,t65]) ).
cnf(t193,plain,
implies(implies(sF7,truth),sF1) = implies(implies(sF1,falsehood),falsehood),
inference(orient,[status(thm)],[t86]) ).
cnf(t463,plain,
implies(implies(sF7,sF2),sF1) = implies(implies(sF1,falsehood),falsehood),
inference(rw,[status(thm)],[t193]) ).
cnf(t2105,plain,
implies(sF7,sF2) = implies(sF0,sF2),
inference(step,[status(thm)],[t128,t581]) ).
cnf(t582,plain,
implies(sF7,sF2) = implies(sF0,sF2),
inference(orient,[status(thm)],[t2105]) ).
cnf(t2110,plain,
implies(implies(sF0,sF2),sF1) = implies(implies(sF1,falsehood),falsehood),
inference(step,[status(thm)],[t463,t582]) ).
cnf(t2111,plain,
implies(implies(sF0,sF2),sF1) = implies(implies(sF1,sF3),falsehood),
inference(step,[status(thm)],[t2110,t479]) ).
cnf(t2112,plain,
implies(implies(sF0,sF2),sF1) = implies(sF0,falsehood),
inference(step,[status(thm)],[t2111,t558]) ).
cnf(t2113,plain,
implies(implies(sF0,sF2),sF1) = implies(sF0,sF3),
inference(step,[status(thm)],[t2112,t479]) ).
cnf(t41,plain,
implies(not(X1),x) = implies(sF0,X1),
inference(cp,[status(thm)],[t39,t24]) ).
cnf(t67,plain,
implies(not(X1),x) = implies(sF0,X1),
inference(orient,[status(thm)],[t41]) ).
cnf(t68,plain,
implies(sF0,falsehood) = implies(sF2,x),
inference(cp,[status(thm)],[t67,t25]) ).
cnf(t73,plain,
implies(sF2,x) = implies(sF0,falsehood),
inference(orient,[status(thm)],[t68]) ).
cnf(t2080,plain,
implies(sF2,x) = implies(sF0,sF3),
inference(step,[status(thm)],[t73,t479]) ).
cnf(t487,plain,
implies(sF2,x) = implies(sF0,sF3),
inference(orient,[status(thm)],[t2080]) ).
cnf(t2091,plain,
x = implies(sF0,sF3),
inference(step,[status(thm)],[t487,t506]) ).
cnf(t507,plain,
x = implies(sF0,sF3),
inference(rw,[status(thm)],[t2091]) ).
cnf(t551,plain,
implies(sF0,sF3) = x,
inference(orient,[status(thm)],[t507]) ).
cnf(t2114,plain,
implies(implies(sF0,sF2),sF1) = x,
inference(step,[status(thm)],[t2113,t551]) ).
cnf(t601,plain,
implies(implies(sF0,sF2),sF1) = x,
inference(orient,[status(thm)],[t2114]) ).
cnf(t2194,plain,
implies(sF8,sF1) = x,
inference(step,[status(thm)],[t601,t887]) ).
cnf(t892,plain,
implies(sF8,sF1) = x,
inference(rw,[status(thm)],[t2194]) ).
cnf(t904,plain,
implies(sF8,sF1) = x,
inference(orient,[status(thm)],[t892]) ).
cnf(t1097,plain,
sF2 = implies(x,sF2),
inference(cp,[status(thm)],[t1096,t904]) ).
cnf(t1101,plain,
implies(x,sF2) = sF2,
inference(orient,[status(thm)],[t1097]) ).
cnf(t1104,plain,
sF2 = implies(implies(x,X1),implies(implies(X1,sF2),sF2)),
inference(cp,[status(thm)],[t464,t1101]) ).
cnf(t2261,plain,
sF2 = implies(implies(x,X1),sF2),
inference(step,[status(thm)],[t1104,t477]) ).
cnf(t1270,plain,
implies(implies(x,X1),sF2) = sF2,
inference(orient,[status(thm)],[t2261]) ).
cnf(t110,plain,
implies(sF1,sF2) = implies(sF3,sF0),
inference(cp,[status(thm)],[t109,t28]) ).
cnf(t117,plain,
implies(sF3,sF0) = implies(sF1,sF2),
inference(orient,[status(thm)],[t110]) ).
cnf(t118,plain,
implies(implies(sF0,sF3),sF3) = implies(implies(sF1,sF2),sF0),
inference(cp,[status(thm)],[t76,t117]) ).
cnf(t332,plain,
implies(implies(sF1,sF2),sF0) = implies(implies(sF0,sF3),sF3),
inference(orient,[status(thm)],[t118]) ).
cnf(t2096,plain,
implies(implies(sF1,sF2),sF0) = implies(x,sF3),
inference(step,[status(thm)],[t332,t551]) ).
cnf(t552,plain,
implies(implies(sF1,sF2),sF0) = implies(x,sF3),
inference(orient,[status(thm)],[t2096]) ).
cnf(t1864,plain,
implies(sF2,sF0) = implies(x,sF3),
inference(rw,[status(thm)],[t552]) ).
cnf(t2326,plain,
sF0 = implies(x,sF3),
inference(step,[status(thm)],[t1864,t506]) ).
cnf(t1882,plain,
implies(x,sF3) = sF0,
inference(orient,[status(thm)],[t2326]) ).
cnf(t1888,plain,
sF2 = implies(sF0,sF2),
inference(cp,[status(thm)],[t1270,t1882]) ).
cnf(t2327,plain,
sF2 = sF8,
inference(step,[status(thm)],[t1888,t887]) ).
cnf(t1890,plain,
sF8 = sF2,
inference(orient,[status(thm)],[t2327]) ).
cnf(t2334,plain,
implies(sF0,sF2) = sF2,
inference(step,[status(thm)],[t887,t1890]) ).
cnf(t1897,plain,
implies(sF0,sF2) = sF2,
inference(orient,[status(thm)],[t2334]) ).
cnf(u8,negated_conjecture,
xor(x,falsehood) != x,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(u3,axiom,
xor(X,Y) = or(and(X,not(Y)),and(not(X),Y)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(u2,axiom,
and(X,Y) = not(or(not(X),not(Y))),
file('/export/starexec/sandbox2/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(falsehood))))),not(implies(not(not(not(x))),not(falsehood)))) != x,
inference(definition_unfolding,[status(thm)],[u8,d2]) ).
cnf(g0_0,plain,
implies(not(not(implies(not(sF0),not(not(falsehood))))),not(implies(not(not(not(x))),not(falsehood)))) != x,
inference(rw,[status(thm)],[goal_0,t24]) ).
cnf(g0_1,plain,
implies(not(not(implies(sF1,not(not(falsehood))))),not(implies(not(not(not(x))),not(falsehood)))) != x,
inference(rw,[status(thm)],[g0_0,t27]) ).
cnf(g0_2,plain,
implies(not(not(implies(sF1,not(not(sF3))))),not(implies(not(not(not(x))),not(falsehood)))) != x,
inference(rw,[status(thm)],[g0_1,t479]) ).
cnf(g0_3,plain,
implies(not(not(implies(sF1,not(sF2)))),not(implies(not(not(not(x))),not(falsehood)))) != x,
inference(rw,[status(thm)],[g0_2,t502]) ).
cnf(g0_4,plain,
implies(not(not(implies(sF1,sF3))),not(implies(not(not(not(x))),not(falsehood)))) != x,
inference(rw,[status(thm)],[g0_3,t28]) ).
cnf(g0_5,plain,
implies(not(not(sF0)),not(implies(not(not(not(x))),not(falsehood)))) != x,
inference(rw,[status(thm)],[g0_4,t558]) ).
cnf(g0_6,plain,
implies(not(sF1),not(implies(not(not(not(x))),not(falsehood)))) != x,
inference(rw,[status(thm)],[g0_5,t27]) ).
cnf(g0_7,plain,
implies(sF0,not(implies(not(not(not(x))),not(falsehood)))) != x,
inference(rw,[status(thm)],[g0_6,t1990]) ).
cnf(g0_8,plain,
implies(sF0,not(implies(not(not(sF0)),not(falsehood)))) != x,
inference(rw,[status(thm)],[g0_7,t24]) ).
cnf(g0_9,plain,
implies(sF0,not(implies(not(sF1),not(falsehood)))) != x,
inference(rw,[status(thm)],[g0_8,t27]) ).
cnf(g0_10,plain,
implies(sF0,not(implies(sF0,not(falsehood)))) != x,
inference(rw,[status(thm)],[g0_9,t1990]) ).
cnf(g0_11,plain,
implies(sF0,not(implies(sF0,not(sF3)))) != x,
inference(rw,[status(thm)],[g0_10,t479]) ).
cnf(g0_12,plain,
implies(sF0,not(implies(sF0,sF2))) != x,
inference(rw,[status(thm)],[g0_11,t502]) ).
cnf(g0_13,plain,
implies(sF0,not(sF2)) != x,
inference(rw,[status(thm)],[g0_12,t1897]) ).
cnf(g0_14,plain,
implies(sF0,sF3) != x,
inference(rw,[status(thm)],[g0_13,t28]) ).
cnf(g0_15,plain,
x != x,
inference(rw,[status(thm)],[g0_14,t551]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_15]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : LCL154-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.02 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.04/0.30 % Computer : n012.cluster.edu
% 0.04/0.30 % Model : x86_64 x86_64
% 0.04/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/0.30 % Memory : 8046.5625MB
% 0.04/0.30 % OS : Linux 6.8.0-71-generic
% 0.04/0.30 % CPULimit : 300
% 0.04/0.30 % WCLimit : 300
% 0.04/0.30 % DateTime : Wed Sep 23 22:06:20 UTC 2026
% 0.04/0.30 % CPUTime :
% 0.04/0.30 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 3.36/0.81 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.36/0.81 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------