%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LCL163-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 : n010.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:06 PM UTC 2026
% Result : Unsatisfiable 9.42s 1.97s
% Output : CNFRefutation 9.42s
% Verified :
% SZS Type : Refutation
% Derivation depth : 65
% Number of leaves : 17
% Syntax : Number of clauses : 237 ( 237 unt; 0 nHn; 133 RR)
% Number of literals : 237 ( 236 equ; 5 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 8 con; 0-2 aty)
% Number of variables : 165 ( 21 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t13,axiom,
sFlat0 = implies(y,x),
introduced(definition) ).
cnf(t73,plain,
implies(y,x) = sFlat0,
inference(orient,[status(thm)],[t13]) ).
cnf(t14,axiom,
sFlat1 = implies(implies(y,x),x),
introduced(definition) ).
cnf(t70,plain,
implies(implies(y,x),x) = sFlat1,
inference(orient,[status(thm)],[t14]) ).
cnf(t8856,plain,
implies(sFlat0,x) = sFlat1,
inference(step,[status(thm)],[t70,t73]) ).
cnf(t74,plain,
implies(sFlat0,x) = sFlat1,
inference(rw,[status(thm)],[t8856]) ).
cnf(t87,plain,
implies(sFlat0,x) = sFlat1,
inference(orient,[status(thm)],[t74]) ).
cnf(t15,axiom,
sFlat2 = implies(x,y),
introduced(definition) ).
cnf(t71,plain,
implies(x,y) = sFlat2,
inference(orient,[status(thm)],[t15]) ).
cnf(t16,axiom,
sFlat3 = implies(implies(x,y),y),
introduced(definition) ).
cnf(t69,plain,
implies(implies(x,y),y) = sFlat3,
inference(orient,[status(thm)],[t16]) ).
cnf(t8855,plain,
implies(sFlat2,y) = sFlat3,
inference(step,[status(thm)],[t69,t71]) ).
cnf(t72,plain,
implies(sFlat2,y) = sFlat3,
inference(rw,[status(thm)],[t8855]) ).
cnf(t86,plain,
implies(sFlat2,y) = sFlat3,
inference(orient,[status(thm)],[t72]) ).
cnf(t10,axiom,
xor(truth,and_star(X1,xor(truth,X2))) = implies(X1,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t32,plain,
xor(truth,and_star(X1,xor(truth,X2))) = implies(X1,X2),
inference(orient,[status(thm)],[t10]) ).
cnf(t5,axiom,
xor(X1,truth) = not(X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t28,plain,
xor(X1,truth) = not(X1),
inference(orient,[status(thm)],[t5]) ).
cnf(t8,axiom,
xor(X1,X2) = xor(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t19,plain,
xor(X1,X2) = xor(X2,X1),
inference(orient,[status(thm)],[t8]) ).
cnf(t30,plain,
not(X1) = xor(truth,X1),
inference(cp,[status(thm)],[t28,t19]) ).
cnf(t89,plain,
xor(truth,X1) = not(X1),
inference(orient,[status(thm)],[t30]) ).
cnf(t8862,plain,
not(and_star(X1,xor(truth,X2))) = implies(X1,X2),
inference(step,[status(thm)],[t32,t89]) ).
cnf(t8863,plain,
not(and_star(X1,not(X2))) = implies(X1,X2),
inference(step,[status(thm)],[t8862,t89]) ).
cnf(t92,plain,
not(and_star(X1,not(X2))) = implies(X1,X2),
inference(rw,[status(thm)],[t8863]) ).
cnf(t96,plain,
not(and_star(X1,not(X2))) = implies(X1,X2),
inference(orient,[status(thm)],[t92]) ).
cnf(t6,axiom,
and_star(X1,X2) = and_star(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t38,plain,
and_star(X1,X2) = and_star(X2,X1),
inference(orient,[status(thm)],[t6]) ).
cnf(t2,axiom,
and_star(X1,truth) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t18,plain,
and_star(X1,truth) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t39,plain,
and_star(truth,X1) = X1,
inference(cp,[status(thm)],[t38,t18]) ).
cnf(t79,plain,
and_star(truth,X1) = X1,
inference(orient,[status(thm)],[t39]) ).
cnf(t97,plain,
implies(truth,X1) = not(not(X1)),
inference(cp,[status(thm)],[t96,t79]) ).
cnf(t106,plain,
not(not(X1)) = implies(truth,X1),
inference(orient,[status(thm)],[t97]) ).
cnf(t11,axiom,
xor(xor(X1,truth),X2) = xor(X1,xor(truth,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t22,plain,
xor(xor(X1,truth),X2) = xor(X1,xor(truth,X2)),
inference(orient,[status(thm)],[t11]) ).
cnf(t8849,plain,
xor(not(X1),X2) = xor(X1,xor(truth,X2)),
inference(step,[status(thm)],[t22,t28]) ).
cnf(t31,plain,
xor(not(X1),X2) = xor(X1,xor(truth,X2)),
inference(rw,[status(thm)],[t8849]) ).
cnf(t8870,plain,
xor(not(X1),X2) = xor(X1,not(X2)),
inference(step,[status(thm)],[t31,t89]) ).
cnf(t148,plain,
xor(not(X1),X2) = xor(X1,not(X2)),
inference(orient,[status(thm)],[t8870]) ).
cnf(t150,plain,
xor(X1,not(truth)) = not(not(X1)),
inference(cp,[status(thm)],[t148,t28]) ).
cnf(t0,axiom,
not(truth) = falsehood,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t75,plain,
not(truth) = falsehood,
inference(orient,[status(thm)],[t0]) ).
cnf(t8871,plain,
xor(X1,falsehood) = not(not(X1)),
inference(step,[status(thm)],[t150,t75]) ).
cnf(t4,axiom,
xor(X1,falsehood) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t17,plain,
xor(X1,falsehood) = X1,
inference(orient,[status(thm)],[t4]) ).
cnf(t8872,plain,
X1 = not(not(X1)),
inference(step,[status(thm)],[t8871,t17]) ).
cnf(t8873,plain,
X1 = implies(truth,X1),
inference(step,[status(thm)],[t8872,t106]) ).
cnf(t157,plain,
implies(truth,X1) = X1,
inference(orient,[status(thm)],[t8873]) ).
cnf(t8874,plain,
not(not(X1)) = X1,
inference(step,[status(thm)],[t106,t157]) ).
cnf(t158,plain,
not(not(X1)) = X1,
inference(orient,[status(thm)],[t8874]) ).
cnf(t107,plain,
implies(truth,and_star(X1,not(X2))) = not(implies(X1,X2)),
inference(cp,[status(thm)],[t106,t96]) ).
cnf(t8880,plain,
and_star(X1,not(X2)) = not(implies(X1,X2)),
inference(step,[status(thm)],[t107,t157]) ).
cnf(t174,plain,
not(implies(X1,X2)) = and_star(X1,not(X2)),
inference(orient,[status(thm)],[t8880]) ).
cnf(t110,plain,
implies(X1,not(X2)) = not(and_star(X1,implies(truth,X2))),
inference(cp,[status(thm)],[t96,t106]) ).
cnf(t8926,plain,
implies(X1,not(X2)) = not(and_star(X1,X2)),
inference(step,[status(thm)],[t110,t157]) ).
cnf(t658,plain,
not(and_star(X1,X2)) = implies(X1,not(X2)),
inference(orient,[status(thm)],[t8926]) ).
cnf(t12,axiom,
and_star(xor(and_star(xor(truth,X1),X2),truth),X2) = and_star(xor(and_star(xor(truth,X2),X1),truth),X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t8850,plain,
and_star(X2,xor(and_star(xor(truth,X1),X2),truth)) = and_star(xor(and_star(xor(truth,X2),X1),truth),X1),
inference(step,[status(thm)],[t12,t38]) ).
cnf(t8851,plain,
and_star(X2,not(and_star(xor(truth,X1),X2))) = and_star(xor(and_star(xor(truth,X2),X1),truth),X1),
inference(step,[status(thm)],[t8850,t28]) ).
cnf(t8852,plain,
and_star(X2,not(and_star(xor(truth,X1),X2))) = and_star(X1,xor(and_star(xor(truth,X2),X1),truth)),
inference(step,[status(thm)],[t8851,t38]) ).
cnf(t8853,plain,
and_star(X2,not(and_star(xor(truth,X1),X2))) = and_star(X1,not(and_star(xor(truth,X2),X1))),
inference(step,[status(thm)],[t8852,t28]) ).
cnf(t49,plain,
and_star(X1,not(and_star(xor(truth,X2),X1))) = and_star(X2,not(and_star(xor(truth,X1),X2))),
inference(orient,[status(thm)],[t8853]) ).
cnf(t8859,plain,
and_star(X1,not(and_star(not(X2),X1))) = and_star(X2,not(and_star(xor(truth,X1),X2))),
inference(step,[status(thm)],[t49,t89]) ).
cnf(t8860,plain,
and_star(X1,not(and_star(not(X2),X1))) = and_star(X2,not(and_star(not(X1),X2))),
inference(step,[status(thm)],[t8859,t89]) ).
cnf(t90,plain,
and_star(X1,not(and_star(not(X2),X1))) = and_star(X2,not(and_star(not(X1),X2))),
inference(rw,[status(thm)],[t8860]) ).
cnf(t8960,plain,
and_star(X1,implies(not(X2),not(X1))) = and_star(X2,not(and_star(not(X1),X2))),
inference(step,[status(thm)],[t90,t658]) ).
cnf(t99,plain,
implies(X1,X2) = not(and_star(not(X2),X1)),
inference(cp,[status(thm)],[t96,t38]) ).
cnf(t114,plain,
not(and_star(not(X1),X2)) = implies(X2,X1),
inference(orient,[status(thm)],[t99]) ).
cnf(t8927,plain,
implies(not(X1),not(X2)) = implies(X2,X1),
inference(step,[status(thm)],[t114,t658]) ).
cnf(t692,plain,
implies(not(X1),not(X2)) = implies(X2,X1),
inference(rw,[status(thm)],[t8927]) ).
cnf(t698,plain,
implies(not(X1),not(X2)) = implies(X2,X1),
inference(orient,[status(thm)],[t692]) ).
cnf(t8961,plain,
and_star(X1,implies(X1,X2)) = and_star(X2,not(and_star(not(X1),X2))),
inference(step,[status(thm)],[t8960,t698]) ).
cnf(t8962,plain,
and_star(X1,implies(X1,X2)) = and_star(X2,implies(not(X1),not(X2))),
inference(step,[status(thm)],[t8961,t658]) ).
cnf(t8963,plain,
and_star(X1,implies(X1,X2)) = and_star(X2,implies(X2,X1)),
inference(step,[status(thm)],[t8962,t698]) ).
cnf(t761,plain,
and_star(X1,implies(X1,X2)) = and_star(X2,implies(X2,X1)),
inference(orient,[status(thm)],[t8963]) ).
cnf(t9,axiom,
and_star(and_star(X1,X2),X3) = and_star(X1,and_star(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t41,plain,
and_star(and_star(X1,X2),X3) = and_star(X1,and_star(X2,X3)),
inference(orient,[status(thm)],[t9]) ).
cnf(t7,axiom,
and_star(xor(truth,X1),X1) = falsehood,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t8854,plain,
and_star(X1,xor(truth,X1)) = falsehood,
inference(step,[status(thm)],[t7,t38]) ).
cnf(t61,plain,
and_star(X1,xor(truth,X1)) = falsehood,
inference(orient,[status(thm)],[t8854]) ).
cnf(t8861,plain,
and_star(X1,not(X1)) = falsehood,
inference(step,[status(thm)],[t61,t89]) ).
cnf(t91,plain,
and_star(X1,not(X1)) = falsehood,
inference(rw,[status(thm)],[t8861]) ).
cnf(t93,plain,
and_star(X1,not(X1)) = falsehood,
inference(orient,[status(thm)],[t91]) ).
cnf(t95,plain,
and_star(X1,and_star(not(X1),X2)) = and_star(falsehood,X2),
inference(cp,[status(thm)],[t41,t93]) ).
cnf(t1,axiom,
and_star(X1,falsehood) = falsehood,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t46,plain,
and_star(X1,falsehood) = falsehood,
inference(orient,[status(thm)],[t1]) ).
cnf(t47,plain,
falsehood = and_star(falsehood,X1),
inference(cp,[status(thm)],[t46,t38]) ).
cnf(t82,plain,
and_star(falsehood,X1) = falsehood,
inference(orient,[status(thm)],[t47]) ).
cnf(t8869,plain,
and_star(X1,and_star(not(X1),X2)) = falsehood,
inference(step,[status(thm)],[t95,t82]) ).
cnf(t125,plain,
and_star(X1,and_star(not(X1),X2)) = falsehood,
inference(orient,[status(thm)],[t8869]) ).
cnf(t132,plain,
implies(and_star(not(not(X1)),X2),X1) = not(falsehood),
inference(cp,[status(thm)],[t114,t125]) ).
cnf(t8877,plain,
implies(and_star(X1,X2),X1) = not(falsehood),
inference(step,[status(thm)],[t132,t158]) ).
cnf(t20,plain,
xor(falsehood,X1) = X1,
inference(cp,[status(thm)],[t19,t17]) ).
cnf(t76,plain,
xor(falsehood,X1) = X1,
inference(orient,[status(thm)],[t20]) ).
cnf(t77,plain,
truth = not(falsehood),
inference(cp,[status(thm)],[t76,t28]) ).
cnf(t78,plain,
not(falsehood) = truth,
inference(orient,[status(thm)],[t77]) ).
cnf(t8878,plain,
implies(and_star(X1,X2),X1) = truth,
inference(step,[status(thm)],[t8877,t78]) ).
cnf(t161,plain,
implies(and_star(X1,X2),X1) = truth,
inference(orient,[status(thm)],[t8878]) ).
cnf(t177,plain,
and_star(x,not(y)) = not(sFlat2),
inference(cp,[status(thm)],[t174,t71]) ).
cnf(t253,plain,
and_star(x,not(y)) = not(sFlat2),
inference(orient,[status(thm)],[t177]) ).
cnf(t256,plain,
truth = implies(not(sFlat2),x),
inference(cp,[status(thm)],[t161,t253]) ).
cnf(t262,plain,
implies(not(sFlat2),x) = truth,
inference(orient,[status(thm)],[t256]) ).
cnf(t263,plain,
and_star(not(sFlat2),not(x)) = not(truth),
inference(cp,[status(thm)],[t174,t262]) ).
cnf(t8891,plain,
and_star(not(sFlat2),not(x)) = falsehood,
inference(step,[status(thm)],[t263,t75]) ).
cnf(t305,plain,
and_star(not(sFlat2),not(x)) = falsehood,
inference(orient,[status(thm)],[t8891]) ).
cnf(t306,plain,
and_star(not(sFlat2),and_star(not(x),X1)) = and_star(falsehood,X1),
inference(cp,[status(thm)],[t41,t305]) ).
cnf(t8901,plain,
and_star(not(sFlat2),and_star(not(x),X1)) = falsehood,
inference(step,[status(thm)],[t306,t82]) ).
cnf(t421,plain,
and_star(not(sFlat2),and_star(not(x),X1)) = falsehood,
inference(orient,[status(thm)],[t8901]) ).
cnf(t425,plain,
implies(and_star(not(x),X1),sFlat2) = not(falsehood),
inference(cp,[status(thm)],[t114,t421]) ).
cnf(t8902,plain,
implies(and_star(not(x),X1),sFlat2) = truth,
inference(step,[status(thm)],[t425,t78]) ).
cnf(t427,plain,
implies(and_star(not(x),X1),sFlat2) = truth,
inference(orient,[status(thm)],[t8902]) ).
cnf(t428,plain,
truth = implies(and_star(X1,not(x)),sFlat2),
inference(cp,[status(thm)],[t427,t38]) ).
cnf(t432,plain,
implies(and_star(X1,not(x)),sFlat2) = truth,
inference(orient,[status(thm)],[t428]) ).
cnf(t175,plain,
and_star(sFlat0,not(x)) = not(sFlat1),
inference(cp,[status(thm)],[t174,t87]) ).
cnf(t185,plain,
and_star(sFlat0,not(x)) = not(sFlat1),
inference(orient,[status(thm)],[t175]) ).
cnf(t434,plain,
truth = implies(not(sFlat1),sFlat2),
inference(cp,[status(thm)],[t432,t185]) ).
cnf(t439,plain,
implies(not(sFlat1),sFlat2) = truth,
inference(orient,[status(thm)],[t434]) ).
cnf(t802,plain,
and_star(sFlat2,implies(sFlat2,not(sFlat1))) = and_star(not(sFlat1),truth),
inference(cp,[status(thm)],[t761,t439]) ).
cnf(t9037,plain,
and_star(sFlat2,implies(sFlat2,not(sFlat1))) = not(sFlat1),
inference(step,[status(thm)],[t802,t18]) ).
cnf(t1250,plain,
and_star(sFlat2,implies(sFlat2,not(sFlat1))) = not(sFlat1),
inference(orient,[status(thm)],[t9037]) ).
cnf(t1252,plain,
implies(sFlat2,not(implies(sFlat2,not(sFlat1)))) = not(not(sFlat1)),
inference(cp,[status(thm)],[t658,t1250]) ).
cnf(t9038,plain,
implies(sFlat2,and_star(sFlat2,not(not(sFlat1)))) = not(not(sFlat1)),
inference(step,[status(thm)],[t1252,t174]) ).
cnf(t9039,plain,
implies(sFlat2,and_star(sFlat2,sFlat1)) = not(not(sFlat1)),
inference(step,[status(thm)],[t9038,t158]) ).
cnf(t9040,plain,
implies(sFlat2,and_star(sFlat1,sFlat2)) = not(not(sFlat1)),
inference(step,[status(thm)],[t9039,t38]) ).
cnf(t9041,plain,
implies(sFlat2,and_star(sFlat1,sFlat2)) = sFlat1,
inference(step,[status(thm)],[t9040,t158]) ).
cnf(t1258,plain,
implies(sFlat2,and_star(sFlat1,sFlat2)) = sFlat1,
inference(orient,[status(thm)],[t9041]) ).
cnf(t1259,plain,
and_star(sFlat2,not(and_star(sFlat1,sFlat2))) = not(sFlat1),
inference(cp,[status(thm)],[t174,t1258]) ).
cnf(t9051,plain,
and_star(sFlat2,implies(sFlat1,not(sFlat2))) = not(sFlat1),
inference(step,[status(thm)],[t1259,t658]) ).
cnf(t1305,plain,
and_star(sFlat2,implies(sFlat1,not(sFlat2))) = not(sFlat1),
inference(orient,[status(thm)],[t9051]) ).
cnf(t162,plain,
truth = implies(and_star(X1,and_star(X2,X3)),and_star(X1,X2)),
inference(cp,[status(thm)],[t161,t41]) ).
cnf(t3557,plain,
implies(and_star(X1,and_star(X2,X3)),and_star(X1,X2)) = truth,
inference(orient,[status(thm)],[t162]) ).
cnf(t307,plain,
implies(not(x),sFlat2) = not(falsehood),
inference(cp,[status(thm)],[t114,t305]) ).
cnf(t8892,plain,
implies(not(x),sFlat2) = truth,
inference(step,[status(thm)],[t307,t78]) ).
cnf(t310,plain,
implies(not(x),sFlat2) = truth,
inference(orient,[status(thm)],[t8892]) ).
cnf(t793,plain,
and_star(sFlat2,implies(sFlat2,not(x))) = and_star(not(x),truth),
inference(cp,[status(thm)],[t761,t310]) ).
cnf(t811,plain,
and_star(y,implies(y,x)) = and_star(x,sFlat2),
inference(cp,[status(thm)],[t761,t71]) ).
cnf(t8968,plain,
and_star(y,sFlat0) = and_star(x,sFlat2),
inference(step,[status(thm)],[t811,t73]) ).
cnf(t8969,plain,
and_star(sFlat0,y) = and_star(x,sFlat2),
inference(step,[status(thm)],[t8968,t38]) ).
cnf(t8970,plain,
and_star(sFlat0,y) = and_star(sFlat2,x),
inference(step,[status(thm)],[t8969,t38]) ).
cnf(t867,plain,
and_star(sFlat2,x) = and_star(sFlat0,y),
inference(orient,[status(thm)],[t8970]) ).
cnf(t870,plain,
implies(sFlat2,not(x)) = not(and_star(sFlat0,y)),
inference(cp,[status(thm)],[t658,t867]) ).
cnf(t8974,plain,
implies(sFlat2,not(x)) = implies(sFlat0,not(y)),
inference(step,[status(thm)],[t870,t658]) ).
cnf(t948,plain,
implies(sFlat2,not(x)) = implies(sFlat0,not(y)),
inference(orient,[status(thm)],[t8974]) ).
cnf(t8984,plain,
and_star(sFlat2,implies(sFlat0,not(y))) = and_star(not(x),truth),
inference(step,[status(thm)],[t793,t948]) ).
cnf(t8985,plain,
and_star(sFlat2,implies(sFlat0,not(y))) = not(x),
inference(step,[status(thm)],[t8984,t18]) ).
cnf(t1062,plain,
and_star(sFlat2,implies(sFlat0,not(y))) = not(x),
inference(orient,[status(thm)],[t8985]) ).
cnf(t3613,plain,
truth = implies(and_star(X1,not(x)),and_star(X1,sFlat2)),
inference(cp,[status(thm)],[t3557,t1062]) ).
cnf(t8419,plain,
implies(and_star(X1,not(x)),and_star(X1,sFlat2)) = truth,
inference(orient,[status(thm)],[t3613]) ).
cnf(t188,plain,
truth = implies(not(sFlat1),sFlat0),
inference(cp,[status(thm)],[t161,t185]) ).
cnf(t192,plain,
implies(not(sFlat1),sFlat0) = truth,
inference(orient,[status(thm)],[t188]) ).
cnf(t193,plain,
and_star(not(sFlat1),not(sFlat0)) = not(truth),
inference(cp,[status(thm)],[t174,t192]) ).
cnf(t8885,plain,
and_star(not(sFlat0),not(sFlat1)) = not(truth),
inference(step,[status(thm)],[t193,t38]) ).
cnf(t8886,plain,
and_star(not(sFlat0),not(sFlat1)) = falsehood,
inference(step,[status(thm)],[t8885,t75]) ).
cnf(t289,plain,
and_star(not(sFlat0),not(sFlat1)) = falsehood,
inference(orient,[status(thm)],[t8886]) ).
cnf(t291,plain,
implies(not(sFlat0),sFlat1) = not(falsehood),
inference(cp,[status(thm)],[t96,t289]) ).
cnf(t8887,plain,
implies(not(sFlat0),sFlat1) = truth,
inference(step,[status(thm)],[t291,t78]) ).
cnf(t294,plain,
implies(not(sFlat0),sFlat1) = truth,
inference(orient,[status(thm)],[t8887]) ).
cnf(t797,plain,
and_star(sFlat1,implies(sFlat1,not(sFlat0))) = and_star(not(sFlat0),truth),
inference(cp,[status(thm)],[t761,t294]) ).
cnf(t9004,plain,
and_star(sFlat1,implies(sFlat1,not(sFlat0))) = not(sFlat0),
inference(step,[status(thm)],[t797,t18]) ).
cnf(t1121,plain,
and_star(sFlat1,implies(sFlat1,not(sFlat0))) = not(sFlat0),
inference(orient,[status(thm)],[t9004]) ).
cnf(t1124,plain,
implies(sFlat1,not(implies(sFlat1,not(sFlat0)))) = not(not(sFlat0)),
inference(cp,[status(thm)],[t658,t1121]) ).
cnf(t9005,plain,
implies(sFlat1,and_star(sFlat1,not(not(sFlat0)))) = not(not(sFlat0)),
inference(step,[status(thm)],[t1124,t174]) ).
cnf(t9006,plain,
implies(sFlat1,and_star(sFlat1,sFlat0)) = not(not(sFlat0)),
inference(step,[status(thm)],[t9005,t158]) ).
cnf(t9007,plain,
implies(sFlat1,and_star(sFlat0,sFlat1)) = not(not(sFlat0)),
inference(step,[status(thm)],[t9006,t38]) ).
cnf(t127,plain,
falsehood = and_star(X1,and_star(X2,not(X1))),
inference(cp,[status(thm)],[t125,t38]) ).
cnf(t139,plain,
and_star(X1,and_star(X2,not(X1))) = falsehood,
inference(orient,[status(thm)],[t127]) ).
cnf(t178,plain,
and_star(y,not(x)) = not(sFlat0),
inference(cp,[status(thm)],[t174,t73]) ).
cnf(t270,plain,
and_star(y,not(x)) = not(sFlat0),
inference(orient,[status(thm)],[t178]) ).
cnf(t276,plain,
falsehood = and_star(x,not(sFlat0)),
inference(cp,[status(thm)],[t139,t270]) ).
cnf(t281,plain,
and_star(x,not(sFlat0)) = falsehood,
inference(orient,[status(thm)],[t276]) ).
cnf(t283,plain,
implies(x,sFlat0) = not(falsehood),
inference(cp,[status(thm)],[t96,t281]) ).
cnf(t8884,plain,
implies(x,sFlat0) = truth,
inference(step,[status(thm)],[t283,t78]) ).
cnf(t286,plain,
implies(x,sFlat0) = truth,
inference(orient,[status(thm)],[t8884]) ).
cnf(t810,plain,
and_star(sFlat0,implies(sFlat0,x)) = and_star(x,truth),
inference(cp,[status(thm)],[t761,t286]) ).
cnf(t8964,plain,
and_star(sFlat0,sFlat1) = and_star(x,truth),
inference(step,[status(thm)],[t810,t87]) ).
cnf(t8965,plain,
and_star(sFlat0,sFlat1) = x,
inference(step,[status(thm)],[t8964,t18]) ).
cnf(t852,plain,
and_star(sFlat0,sFlat1) = x,
inference(orient,[status(thm)],[t8965]) ).
cnf(t9008,plain,
implies(sFlat1,x) = not(not(sFlat0)),
inference(step,[status(thm)],[t9007,t852]) ).
cnf(t9009,plain,
implies(sFlat1,x) = sFlat0,
inference(step,[status(thm)],[t9008,t158]) ).
cnf(t1130,plain,
implies(sFlat1,x) = sFlat0,
inference(orient,[status(thm)],[t9009]) ).
cnf(t1131,plain,
and_star(sFlat1,not(x)) = not(sFlat0),
inference(cp,[status(thm)],[t174,t1130]) ).
cnf(t1134,plain,
and_star(sFlat1,not(x)) = not(sFlat0),
inference(orient,[status(thm)],[t1131]) ).
cnf(t8420,plain,
truth = implies(not(sFlat0),and_star(sFlat1,sFlat2)),
inference(cp,[status(thm)],[t8419,t1134]) ).
cnf(t8432,plain,
implies(not(sFlat0),and_star(sFlat1,sFlat2)) = truth,
inference(orient,[status(thm)],[t8420]) ).
cnf(t8433,plain,
and_star(not(sFlat0),not(and_star(sFlat1,sFlat2))) = not(truth),
inference(cp,[status(thm)],[t174,t8432]) ).
cnf(t9568,plain,
and_star(not(sFlat0),implies(sFlat1,not(sFlat2))) = not(truth),
inference(step,[status(thm)],[t8433,t658]) ).
cnf(t9569,plain,
and_star(not(sFlat0),implies(sFlat1,not(sFlat2))) = falsehood,
inference(step,[status(thm)],[t9568,t75]) ).
cnf(t8680,plain,
and_star(not(sFlat0),implies(sFlat1,not(sFlat2))) = falsehood,
inference(orient,[status(thm)],[t9569]) ).
cnf(t8682,plain,
implies(not(sFlat0),not(implies(sFlat1,not(sFlat2)))) = not(falsehood),
inference(cp,[status(thm)],[t658,t8680]) ).
cnf(t9570,plain,
implies(implies(sFlat1,not(sFlat2)),sFlat0) = not(falsehood),
inference(step,[status(thm)],[t8682,t698]) ).
cnf(t9571,plain,
implies(implies(sFlat1,not(sFlat2)),sFlat0) = truth,
inference(step,[status(thm)],[t9570,t78]) ).
cnf(t8691,plain,
implies(implies(sFlat1,not(sFlat2)),sFlat0) = truth,
inference(orient,[status(thm)],[t9571]) ).
cnf(t8695,plain,
and_star(sFlat0,implies(sFlat0,implies(sFlat1,not(sFlat2)))) = and_star(implies(sFlat1,not(sFlat2)),truth),
inference(cp,[status(thm)],[t761,t8691]) ).
cnf(t853,plain,
and_star(sFlat0,and_star(sFlat1,X1)) = and_star(x,X1),
inference(cp,[status(thm)],[t41,t852]) ).
cnf(t951,plain,
and_star(sFlat0,and_star(sFlat1,X1)) = and_star(x,X1),
inference(orient,[status(thm)],[t853]) ).
cnf(t960,plain,
implies(sFlat0,not(and_star(sFlat1,X1))) = not(and_star(x,X1)),
inference(cp,[status(thm)],[t658,t951]) ).
cnf(t9121,plain,
implies(sFlat0,implies(sFlat1,not(X1))) = not(and_star(x,X1)),
inference(step,[status(thm)],[t960,t658]) ).
cnf(t9122,plain,
implies(sFlat0,implies(sFlat1,not(X1))) = implies(x,not(X1)),
inference(step,[status(thm)],[t9121,t658]) ).
cnf(t2307,plain,
implies(sFlat0,implies(sFlat1,not(X1))) = implies(x,not(X1)),
inference(orient,[status(thm)],[t9122]) ).
cnf(t9580,plain,
and_star(sFlat0,implies(x,not(sFlat2))) = and_star(implies(sFlat1,not(sFlat2)),truth),
inference(step,[status(thm)],[t8695,t2307]) ).
cnf(t684,plain,
implies(X1,not(X2)) = not(and_star(X2,X1)),
inference(cp,[status(thm)],[t658,t38]) ).
cnf(t9160,plain,
implies(X1,not(X2)) = implies(X2,not(X1)),
inference(step,[status(thm)],[t684,t658]) ).
cnf(t2712,plain,
implies(X1,not(X2)) = implies(X2,not(X1)),
inference(orient,[status(thm)],[t9160]) ).
cnf(t9581,plain,
and_star(sFlat0,implies(sFlat2,not(x))) = and_star(implies(sFlat1,not(sFlat2)),truth),
inference(step,[status(thm)],[t9580,t2712]) ).
cnf(t9582,plain,
and_star(sFlat0,implies(sFlat0,not(y))) = and_star(implies(sFlat1,not(sFlat2)),truth),
inference(step,[status(thm)],[t9581,t948]) ).
cnf(t273,plain,
truth = implies(not(sFlat0),y),
inference(cp,[status(thm)],[t161,t270]) ).
cnf(t279,plain,
implies(not(sFlat0),y) = truth,
inference(orient,[status(thm)],[t273]) ).
cnf(t280,plain,
and_star(not(sFlat0),not(y)) = not(truth),
inference(cp,[status(thm)],[t174,t279]) ).
cnf(t8893,plain,
and_star(not(sFlat0),not(y)) = falsehood,
inference(step,[status(thm)],[t280,t75]) ).
cnf(t314,plain,
and_star(not(sFlat0),not(y)) = falsehood,
inference(orient,[status(thm)],[t8893]) ).
cnf(t316,plain,
implies(not(y),sFlat0) = not(falsehood),
inference(cp,[status(thm)],[t114,t314]) ).
cnf(t8894,plain,
implies(not(y),sFlat0) = truth,
inference(step,[status(thm)],[t316,t78]) ).
cnf(t319,plain,
implies(not(y),sFlat0) = truth,
inference(orient,[status(thm)],[t8894]) ).
cnf(t792,plain,
and_star(sFlat0,implies(sFlat0,not(y))) = and_star(not(y),truth),
inference(cp,[status(thm)],[t761,t319]) ).
cnf(t8980,plain,
and_star(sFlat0,implies(sFlat0,not(y))) = not(y),
inference(step,[status(thm)],[t792,t18]) ).
cnf(t1054,plain,
and_star(sFlat0,implies(sFlat0,not(y))) = not(y),
inference(orient,[status(thm)],[t8980]) ).
cnf(t9583,plain,
not(y) = and_star(implies(sFlat1,not(sFlat2)),truth),
inference(step,[status(thm)],[t9582,t1054]) ).
cnf(t9584,plain,
not(y) = implies(sFlat1,not(sFlat2)),
inference(step,[status(thm)],[t9583,t18]) ).
cnf(t8728,plain,
implies(sFlat1,not(sFlat2)) = not(y),
inference(orient,[status(thm)],[t9584]) ).
cnf(t9588,plain,
and_star(sFlat2,not(y)) = not(sFlat1),
inference(step,[status(thm)],[t1305,t8728]) ).
cnf(t176,plain,
and_star(sFlat2,not(y)) = not(sFlat3),
inference(cp,[status(thm)],[t174,t86]) ).
cnf(t198,plain,
and_star(sFlat2,not(y)) = not(sFlat3),
inference(orient,[status(thm)],[t176]) ).
cnf(t9589,plain,
not(sFlat3) = not(sFlat1),
inference(step,[status(thm)],[t9588,t198]) ).
cnf(t8745,plain,
not(sFlat3) = not(sFlat1),
inference(rw,[status(thm)],[t9589]) ).
cnf(t8747,plain,
not(sFlat3) = not(sFlat1),
inference(orient,[status(thm)],[t8745]) ).
cnf(t8758,plain,
sFlat3 = not(not(sFlat1)),
inference(cp,[status(thm)],[t158,t8747]) ).
cnf(t9617,plain,
sFlat3 = sFlat1,
inference(step,[status(thm)],[t8758,t158]) ).
cnf(t8798,plain,
sFlat3 = sFlat1,
inference(orient,[status(thm)],[t9617]) ).
cnf(t9618,plain,
implies(sFlat2,y) = sFlat1,
inference(step,[status(thm)],[t86,t8798]) ).
cnf(t8799,plain,
implies(sFlat2,y) = sFlat1,
inference(orient,[status(thm)],[t9618]) ).
cnf(goal_0,negated_conjecture,
implies(implies(y,x),x) != implies(implies(x,y),y),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
implies(sFlat0,x) != implies(implies(x,y),y),
inference(rw,[status(thm)],[goal_0,t73]) ).
cnf(g0_1,plain,
sFlat1 != implies(implies(x,y),y),
inference(rw,[status(thm)],[g0_0,t87]) ).
cnf(g0_2,plain,
sFlat1 != implies(sFlat2,y),
inference(rw,[status(thm)],[g0_1,t71]) ).
cnf(g0_3,plain,
sFlat1 != sFlat1,
inference(rw,[status(thm)],[g0_2,t8799]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL163-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.11/0.38 % Computer : n010.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Wed Sep 23 22:07:57 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 9.42/1.97 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 9.42/1.97 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------