%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LCL109-6 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n008.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:00:58 PM UTC 2026
% Result : Unsatisfiable 21.40s 18.34s
% Output : CNFRefutation 21.40s
% Verified :
% SZS Type : Refutation
% Derivation depth : 63
% Number of leaves : 13
% Syntax : Number of clauses : 176 ( 176 unt; 0 nHn; 12 RR)
% Number of literals : 176 ( 175 equ; 7 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 4 con; 0-2 aty)
% Number of variables : 324 ( 12 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t10,axiom,
xor(truth,and_star(X1,xor(truth,X2))) = implies(X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t28,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/sandbox2/benchmark/theBenchmark.p') ).
cnf(t24,plain,
xor(X1,truth) = not(X1),
inference(orient,[status(thm)],[t5]) ).
cnf(t8,axiom,
xor(X1,X2) = xor(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t15,plain,
xor(X1,X2) = xor(X2,X1),
inference(orient,[status(thm)],[t8]) ).
cnf(t26,plain,
not(X1) = xor(truth,X1),
inference(cp,[status(thm)],[t24,t15]) ).
cnf(t77,plain,
xor(truth,X1) = not(X1),
inference(orient,[status(thm)],[t26]) ).
cnf(t19451,plain,
not(and_star(X1,xor(truth,X2))) = implies(X1,X2),
inference(step,[status(thm)],[t28,t77]) ).
cnf(t19452,plain,
not(and_star(X1,not(X2))) = implies(X1,X2),
inference(step,[status(thm)],[t19451,t77]) ).
cnf(t80,plain,
not(and_star(X1,not(X2))) = implies(X1,X2),
inference(rw,[status(thm)],[t19452]) ).
cnf(t84,plain,
not(and_star(X1,not(X2))) = implies(X1,X2),
inference(orient,[status(thm)],[t80]) ).
cnf(t6,axiom,
and_star(X1,X2) = and_star(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t34,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/sandbox2/benchmark/theBenchmark.p') ).
cnf(t14,plain,
and_star(X1,truth) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t35,plain,
and_star(truth,X1) = X1,
inference(cp,[status(thm)],[t34,t14]) ).
cnf(t69,plain,
and_star(truth,X1) = X1,
inference(orient,[status(thm)],[t35]) ).
cnf(t85,plain,
implies(truth,X1) = not(not(X1)),
inference(cp,[status(thm)],[t84,t69]) ).
cnf(t94,plain,
not(not(X1)) = implies(truth,X1),
inference(orient,[status(thm)],[t85]) ).
cnf(t98,plain,
implies(X1,not(X2)) = not(and_star(X1,implies(truth,X2))),
inference(cp,[status(thm)],[t84,t94]) ).
cnf(t11,axiom,
xor(xor(X1,truth),X2) = xor(X1,xor(truth,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t18,plain,
xor(xor(X1,truth),X2) = xor(X1,xor(truth,X2)),
inference(orient,[status(thm)],[t11]) ).
cnf(t19440,plain,
xor(not(X1),X2) = xor(X1,xor(truth,X2)),
inference(step,[status(thm)],[t18,t24]) ).
cnf(t27,plain,
xor(not(X1),X2) = xor(X1,xor(truth,X2)),
inference(rw,[status(thm)],[t19440]) ).
cnf(t19459,plain,
xor(not(X1),X2) = xor(X1,not(X2)),
inference(step,[status(thm)],[t27,t77]) ).
cnf(t136,plain,
xor(not(X1),X2) = xor(X1,not(X2)),
inference(orient,[status(thm)],[t19459]) ).
cnf(t138,plain,
xor(X1,not(truth)) = not(not(X1)),
inference(cp,[status(thm)],[t136,t24]) ).
cnf(t0,axiom,
not(truth) = falsehood,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t65,plain,
not(truth) = falsehood,
inference(orient,[status(thm)],[t0]) ).
cnf(t19460,plain,
xor(X1,falsehood) = not(not(X1)),
inference(step,[status(thm)],[t138,t65]) ).
cnf(t4,axiom,
xor(X1,falsehood) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t13,plain,
xor(X1,falsehood) = X1,
inference(orient,[status(thm)],[t4]) ).
cnf(t19461,plain,
X1 = not(not(X1)),
inference(step,[status(thm)],[t19460,t13]) ).
cnf(t19462,plain,
X1 = implies(truth,X1),
inference(step,[status(thm)],[t19461,t94]) ).
cnf(t145,plain,
implies(truth,X1) = X1,
inference(orient,[status(thm)],[t19462]) ).
cnf(t19470,plain,
implies(X1,not(X2)) = not(and_star(X1,X2)),
inference(step,[status(thm)],[t98,t145]) ).
cnf(t169,plain,
not(and_star(X1,X2)) = implies(X1,not(X2)),
inference(orient,[status(thm)],[t19470]) ).
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/sandbox2/benchmark/theBenchmark.p') ).
cnf(t19441,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,t34]) ).
cnf(t19442,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)],[t19441,t24]) ).
cnf(t19443,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)],[t19442,t34]) ).
cnf(t19444,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)],[t19443,t24]) ).
cnf(t45,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)],[t19444]) ).
cnf(t19448,plain,
and_star(X1,not(and_star(not(X2),X1))) = and_star(X2,not(and_star(xor(truth,X1),X2))),
inference(step,[status(thm)],[t45,t77]) ).
cnf(t19449,plain,
and_star(X1,not(and_star(not(X2),X1))) = and_star(X2,not(and_star(not(X1),X2))),
inference(step,[status(thm)],[t19448,t77]) ).
cnf(t78,plain,
and_star(X1,not(and_star(not(X2),X1))) = and_star(X2,not(and_star(not(X1),X2))),
inference(rw,[status(thm)],[t19449]) ).
cnf(t19531,plain,
and_star(X1,implies(not(X2),not(X1))) = and_star(X2,not(and_star(not(X1),X2))),
inference(step,[status(thm)],[t78,t169]) ).
cnf(t87,plain,
implies(X1,X2) = not(and_star(not(X2),X1)),
inference(cp,[status(thm)],[t84,t34]) ).
cnf(t102,plain,
not(and_star(not(X1),X2)) = implies(X2,X1),
inference(orient,[status(thm)],[t87]) ).
cnf(t19471,plain,
implies(not(X1),not(X2)) = implies(X2,X1),
inference(step,[status(thm)],[t102,t169]) ).
cnf(t178,plain,
implies(not(X1),not(X2)) = implies(X2,X1),
inference(rw,[status(thm)],[t19471]) ).
cnf(t180,plain,
implies(not(X1),not(X2)) = implies(X2,X1),
inference(orient,[status(thm)],[t178]) ).
cnf(t19532,plain,
and_star(X1,implies(X1,X2)) = and_star(X2,not(and_star(not(X1),X2))),
inference(step,[status(thm)],[t19531,t180]) ).
cnf(t19533,plain,
and_star(X1,implies(X1,X2)) = and_star(X2,implies(not(X1),not(X2))),
inference(step,[status(thm)],[t19532,t169]) ).
cnf(t19534,plain,
and_star(X1,implies(X1,X2)) = and_star(X2,implies(X2,X1)),
inference(step,[status(thm)],[t19533,t180]) ).
cnf(t1306,plain,
and_star(X1,implies(X1,X2)) = and_star(X2,implies(X2,X1)),
inference(orient,[status(thm)],[t19534]) ).
cnf(t1312,plain,
and_star(not(X1),implies(not(X1),not(X2))) = and_star(not(X2),implies(X1,X2)),
inference(cp,[status(thm)],[t1306,t180]) ).
cnf(t19653,plain,
and_star(not(X1),implies(X2,X1)) = and_star(not(X2),implies(X1,X2)),
inference(step,[status(thm)],[t1312,t180]) ).
cnf(t6181,plain,
and_star(not(X1),implies(X2,X1)) = and_star(not(X2),implies(X1,X2)),
inference(orient,[status(thm)],[t19653]) ).
cnf(t6259,plain,
implies(not(X1),not(implies(X2,X1))) = not(and_star(not(X2),implies(X1,X2))),
inference(cp,[status(thm)],[t169,t6181]) ).
cnf(t19697,plain,
implies(implies(X2,X1),X1) = not(and_star(not(X2),implies(X1,X2))),
inference(step,[status(thm)],[t6259,t180]) ).
cnf(t19698,plain,
implies(implies(X2,X1),X1) = implies(not(X2),not(implies(X1,X2))),
inference(step,[status(thm)],[t19697,t169]) ).
cnf(t19699,plain,
implies(implies(X2,X1),X1) = implies(implies(X1,X2),X2),
inference(step,[status(thm)],[t19698,t180]) ).
cnf(t9602,plain,
implies(implies(X1,X2),X2) = implies(implies(X2,X1),X1),
inference(orient,[status(thm)],[t19699]) ).
cnf(t95,plain,
implies(truth,and_star(X1,not(X2))) = not(implies(X1,X2)),
inference(cp,[status(thm)],[t94,t84]) ).
cnf(t19469,plain,
and_star(X1,not(X2)) = not(implies(X1,X2)),
inference(step,[status(thm)],[t95,t145]) ).
cnf(t162,plain,
not(implies(X1,X2)) = and_star(X1,not(X2)),
inference(orient,[status(thm)],[t19469]) ).
cnf(t182,plain,
implies(X1,implies(X2,X3)) = implies(and_star(X2,not(X3)),not(X1)),
inference(cp,[status(thm)],[t180,t162]) ).
cnf(t9,axiom,
and_star(and_star(X1,X2),X3) = and_star(X1,and_star(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t37,plain,
and_star(and_star(X1,X2),X3) = and_star(X1,and_star(X2,X3)),
inference(orient,[status(thm)],[t9]) ).
cnf(t172,plain,
implies(and_star(X1,X2),not(X3)) = not(and_star(X1,and_star(X2,X3))),
inference(cp,[status(thm)],[t169,t37]) ).
cnf(t19495,plain,
implies(and_star(X1,X2),not(X3)) = implies(X1,not(and_star(X2,X3))),
inference(step,[status(thm)],[t172,t169]) ).
cnf(t19496,plain,
implies(and_star(X1,X2),not(X3)) = implies(X1,implies(X2,not(X3))),
inference(step,[status(thm)],[t19495,t169]) ).
cnf(t464,plain,
implies(and_star(X1,X2),not(X3)) = implies(X1,implies(X2,not(X3))),
inference(orient,[status(thm)],[t19496]) ).
cnf(t19498,plain,
implies(X1,implies(X2,X3)) = implies(X2,implies(not(X3),not(X1))),
inference(step,[status(thm)],[t182,t464]) ).
cnf(t19499,plain,
implies(X1,implies(X2,X3)) = implies(X2,implies(X1,X3)),
inference(step,[status(thm)],[t19498,t180]) ).
cnf(t562,plain,
implies(X1,implies(X2,X3)) = implies(X2,implies(X1,X3)),
inference(orient,[status(thm)],[t19499]) ).
cnf(t40,plain,
and_star(X1,and_star(X2,X3)) = and_star(and_star(X2,X1),X3),
inference(cp,[status(thm)],[t37,t34]) ).
cnf(t19505,plain,
and_star(X1,and_star(X2,X3)) = and_star(X2,and_star(X1,X3)),
inference(step,[status(thm)],[t40,t37]) ).
cnf(t826,plain,
and_star(X1,and_star(X2,X3)) = and_star(X2,and_star(X1,X3)),
inference(orient,[status(thm)],[t19505]) ).
cnf(t7,axiom,
and_star(xor(truth,X1),X1) = falsehood,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t19445,plain,
and_star(X1,xor(truth,X1)) = falsehood,
inference(step,[status(thm)],[t7,t34]) ).
cnf(t57,plain,
and_star(X1,xor(truth,X1)) = falsehood,
inference(orient,[status(thm)],[t19445]) ).
cnf(t19450,plain,
and_star(X1,not(X1)) = falsehood,
inference(step,[status(thm)],[t57,t77]) ).
cnf(t79,plain,
and_star(X1,not(X1)) = falsehood,
inference(rw,[status(thm)],[t19450]) ).
cnf(t81,plain,
and_star(X1,not(X1)) = falsehood,
inference(orient,[status(thm)],[t79]) ).
cnf(t83,plain,
and_star(X1,and_star(not(X1),X2)) = and_star(falsehood,X2),
inference(cp,[status(thm)],[t37,t81]) ).
cnf(t1,axiom,
and_star(X1,falsehood) = falsehood,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t42,plain,
and_star(X1,falsehood) = falsehood,
inference(orient,[status(thm)],[t1]) ).
cnf(t43,plain,
falsehood = and_star(falsehood,X1),
inference(cp,[status(thm)],[t42,t34]) ).
cnf(t72,plain,
and_star(falsehood,X1) = falsehood,
inference(orient,[status(thm)],[t43]) ).
cnf(t19458,plain,
and_star(X1,and_star(not(X1),X2)) = falsehood,
inference(step,[status(thm)],[t83,t72]) ).
cnf(t113,plain,
and_star(X1,and_star(not(X1),X2)) = falsehood,
inference(orient,[status(thm)],[t19458]) ).
cnf(t115,plain,
falsehood = and_star(X1,and_star(X2,not(X1))),
inference(cp,[status(thm)],[t113,t34]) ).
cnf(t127,plain,
and_star(X1,and_star(X2,not(X1))) = falsehood,
inference(orient,[status(thm)],[t115]) ).
cnf(t171,plain,
implies(X1,not(and_star(X2,not(X1)))) = not(falsehood),
inference(cp,[status(thm)],[t169,t127]) ).
cnf(t19472,plain,
implies(X1,implies(X2,X1)) = not(falsehood),
inference(step,[status(thm)],[t171,t84]) ).
cnf(t16,plain,
xor(falsehood,X1) = X1,
inference(cp,[status(thm)],[t15,t13]) ).
cnf(t66,plain,
xor(falsehood,X1) = X1,
inference(orient,[status(thm)],[t16]) ).
cnf(t67,plain,
truth = not(falsehood),
inference(cp,[status(thm)],[t66,t24]) ).
cnf(t68,plain,
not(falsehood) = truth,
inference(orient,[status(thm)],[t67]) ).
cnf(t19473,plain,
implies(X1,implies(X2,X1)) = truth,
inference(step,[status(thm)],[t19472,t68]) ).
cnf(t179,plain,
implies(X1,implies(X2,X1)) = truth,
inference(orient,[status(thm)],[t19473]) ).
cnf(t6216,plain,
and_star(not(X1),implies(implies(X2,X1),X1)) = and_star(not(implies(X2,X1)),truth),
inference(cp,[status(thm)],[t6181,t179]) ).
cnf(t19654,plain,
and_star(not(X1),implies(implies(X2,X1),X1)) = not(implies(X2,X1)),
inference(step,[status(thm)],[t6216,t14]) ).
cnf(t19655,plain,
and_star(not(X1),implies(implies(X2,X1),X1)) = and_star(X2,not(X1)),
inference(step,[status(thm)],[t19654,t162]) ).
cnf(t6316,plain,
and_star(not(X1),implies(implies(X2,X1),X1)) = and_star(X2,not(X1)),
inference(orient,[status(thm)],[t19655]) ).
cnf(t19463,plain,
not(not(X1)) = X1,
inference(step,[status(thm)],[t94,t145]) ).
cnf(t146,plain,
not(not(X1)) = X1,
inference(orient,[status(thm)],[t19463]) ).
cnf(t6319,plain,
and_star(X1,not(not(X2))) = and_star(X2,implies(implies(X1,not(X2)),not(X2))),
inference(cp,[status(thm)],[t6316,t146]) ).
cnf(t19656,plain,
and_star(X1,X2) = and_star(X2,implies(implies(X1,not(X2)),not(X2))),
inference(step,[status(thm)],[t6319,t146]) ).
cnf(t181,plain,
implies(X1,and_star(X2,X3)) = implies(implies(X2,not(X3)),not(X1)),
inference(cp,[status(thm)],[t180,t169]) ).
cnf(t540,plain,
implies(implies(X1,not(X2)),not(X3)) = implies(X3,and_star(X1,X2)),
inference(orient,[status(thm)],[t181]) ).
cnf(t19657,plain,
and_star(X1,X2) = and_star(X2,implies(X2,and_star(X1,X2))),
inference(step,[status(thm)],[t19656,t540]) ).
cnf(t6459,plain,
and_star(X1,implies(X1,and_star(X2,X1))) = and_star(X2,X1),
inference(orient,[status(thm)],[t19657]) ).
cnf(t6540,plain,
and_star(X1,and_star(X2,implies(X1,and_star(X3,X1)))) = and_star(X2,and_star(X3,X1)),
inference(cp,[status(thm)],[t826,t6459]) ).
cnf(t18545,plain,
and_star(X1,and_star(X2,implies(X1,and_star(X3,X1)))) = and_star(X2,and_star(X3,X1)),
inference(orient,[status(thm)],[t6540]) ).
cnf(t6405,plain,
implies(not(X1),not(implies(implies(X2,X1),X1))) = not(and_star(X2,not(X1))),
inference(cp,[status(thm)],[t169,t6316]) ).
cnf(t19661,plain,
implies(implies(implies(X2,X1),X1),X1) = not(and_star(X2,not(X1))),
inference(step,[status(thm)],[t6405,t180]) ).
cnf(t19662,plain,
implies(implies(implies(X2,X1),X1),X1) = implies(X2,X1),
inference(step,[status(thm)],[t19661,t84]) ).
cnf(t6646,plain,
implies(implies(implies(X1,X2),X2),X2) = implies(X1,X2),
inference(orient,[status(thm)],[t19662]) ).
cnf(t6677,plain,
implies(not(X1),not(X2)) = implies(implies(implies(X2,X1),not(X2)),not(X2)),
inference(cp,[status(thm)],[t6646,t180]) ).
cnf(t19663,plain,
implies(X2,X1) = implies(implies(implies(X2,X1),not(X2)),not(X2)),
inference(step,[status(thm)],[t6677,t180]) ).
cnf(t19664,plain,
implies(X2,X1) = implies(X2,and_star(implies(X2,X1),X2)),
inference(step,[status(thm)],[t19663,t540]) ).
cnf(t19665,plain,
implies(X2,X1) = implies(X2,and_star(X2,implies(X2,X1))),
inference(step,[status(thm)],[t19664,t34]) ).
cnf(t6760,plain,
implies(X1,and_star(X1,implies(X1,X2))) = implies(X1,X2),
inference(orient,[status(thm)],[t19665]) ).
cnf(t6765,plain,
implies(X1,X2) = implies(X1,and_star(X2,implies(X2,X1))),
inference(cp,[status(thm)],[t6760,t1306]) ).
cnf(t6826,plain,
implies(X1,and_star(X2,implies(X2,X1))) = implies(X1,X2),
inference(orient,[status(thm)],[t6765]) ).
cnf(t185,plain,
implies(implies(X1,X2),X3) = implies(not(X3),and_star(X1,not(X2))),
inference(cp,[status(thm)],[t180,t162]) ).
cnf(t613,plain,
implies(not(X1),and_star(X2,not(X3))) = implies(implies(X2,X3),X1),
inference(orient,[status(thm)],[t185]) ).
cnf(t618,plain,
implies(implies(X1,X2),X3) = implies(not(X3),and_star(not(X2),X1)),
inference(cp,[status(thm)],[t613,t34]) ).
cnf(t629,plain,
implies(not(X1),and_star(not(X2),X3)) = implies(implies(X3,X2),X1),
inference(orient,[status(thm)],[t618]) ).
cnf(t6828,plain,
implies(not(X1),not(X2)) = implies(implies(implies(not(X2),not(X1)),X2),X1),
inference(cp,[status(thm)],[t6826,t629]) ).
cnf(t19666,plain,
implies(X2,X1) = implies(implies(implies(not(X2),not(X1)),X2),X1),
inference(step,[status(thm)],[t6828,t180]) ).
cnf(t640,plain,
implies(implies(X1,not(X2)),X3) = implies(not(X3),and_star(X2,X1)),
inference(cp,[status(thm)],[t629,t146]) ).
cnf(t5859,plain,
implies(implies(X1,not(X2)),X3) = implies(not(X3),and_star(X2,X1)),
inference(orient,[status(thm)],[t640]) ).
cnf(t19667,plain,
implies(X2,X1) = implies(implies(not(X2),and_star(X1,not(X2))),X1),
inference(step,[status(thm)],[t19666,t5859]) ).
cnf(t19668,plain,
implies(X2,X1) = implies(implies(implies(X1,X2),X2),X1),
inference(step,[status(thm)],[t19667,t613]) ).
cnf(t6903,plain,
implies(implies(implies(X1,X2),X2),X1) = implies(X2,X1),
inference(orient,[status(thm)],[t19668]) ).
cnf(t7020,plain,
and_star(X1,implies(X1,implies(implies(X1,X2),X2))) = and_star(implies(implies(X1,X2),X2),implies(X2,X1)),
inference(cp,[status(thm)],[t1306,t6903]) ).
cnf(t164,plain,
falsehood = and_star(implies(X1,X2),and_star(X1,not(X2))),
inference(cp,[status(thm)],[t81,t162]) ).
cnf(t38,plain,
and_star(X1,and_star(X2,X3)) = and_star(X3,and_star(X1,X2)),
inference(cp,[status(thm)],[t37,t34]) ).
cnf(t251,plain,
and_star(X1,and_star(X2,X3)) = and_star(X3,and_star(X1,X2)),
inference(orient,[status(thm)],[t38]) ).
cnf(t19486,plain,
falsehood = and_star(X1,and_star(not(X2),implies(X1,X2))),
inference(step,[status(thm)],[t164,t251]) ).
cnf(t325,plain,
and_star(X1,and_star(not(X2),implies(X1,X2))) = falsehood,
inference(orient,[status(thm)],[t19486]) ).
cnf(t338,plain,
implies(X1,not(and_star(not(X2),implies(X1,X2)))) = not(falsehood),
inference(cp,[status(thm)],[t169,t325]) ).
cnf(t19487,plain,
implies(X1,implies(not(X2),not(implies(X1,X2)))) = not(falsehood),
inference(step,[status(thm)],[t338,t169]) ).
cnf(t19488,plain,
implies(X1,implies(implies(X1,X2),X2)) = not(falsehood),
inference(step,[status(thm)],[t19487,t180]) ).
cnf(t19489,plain,
implies(X1,implies(implies(X1,X2),X2)) = truth,
inference(step,[status(thm)],[t19488,t68]) ).
cnf(t343,plain,
implies(X1,implies(implies(X1,X2),X2)) = truth,
inference(orient,[status(thm)],[t19489]) ).
cnf(t19670,plain,
and_star(X1,truth) = and_star(implies(implies(X1,X2),X2),implies(X2,X1)),
inference(step,[status(thm)],[t7020,t343]) ).
cnf(t19671,plain,
X1 = and_star(implies(implies(X1,X2),X2),implies(X2,X1)),
inference(step,[status(thm)],[t19670,t14]) ).
cnf(t19672,plain,
X1 = and_star(implies(X2,X1),implies(implies(X1,X2),X2)),
inference(step,[status(thm)],[t19671,t34]) ).
cnf(t7222,plain,
and_star(implies(X1,X2),implies(implies(X2,X1),X1)) = X2,
inference(orient,[status(thm)],[t19672]) ).
cnf(t7274,plain,
not(X1) = and_star(implies(X1,X2),implies(implies(not(X1),not(X2)),not(X2))),
inference(cp,[status(thm)],[t7222,t180]) ).
cnf(t19767,plain,
not(X1) = and_star(implies(X1,X2),implies(X2,and_star(not(X1),X2))),
inference(step,[status(thm)],[t7274,t540]) ).
cnf(t14813,plain,
and_star(implies(X1,X2),implies(X2,and_star(not(X1),X2))) = not(X1),
inference(orient,[status(thm)],[t19767]) ).
cnf(t18563,plain,
and_star(implies(X1,X2),and_star(not(X1),X2)) = and_star(X2,not(X1)),
inference(cp,[status(thm)],[t18545,t14813]) ).
cnf(t274,plain,
and_star(X1,and_star(X2,X3)) = and_star(X3,and_star(X2,X1)),
inference(cp,[status(thm)],[t251,t34]) ).
cnf(t864,plain,
and_star(X1,and_star(X2,X3)) = and_star(X3,and_star(X2,X1)),
inference(orient,[status(thm)],[t274]) ).
cnf(t19800,plain,
and_star(X2,and_star(not(X1),implies(X1,X2))) = and_star(X2,not(X1)),
inference(step,[status(thm)],[t18563,t864]) ).
cnf(t19160,plain,
and_star(X1,and_star(not(X2),implies(X2,X1))) = and_star(X1,not(X2)),
inference(orient,[status(thm)],[t19800]) ).
cnf(t19198,plain,
implies(X1,not(and_star(not(X2),implies(X2,X1)))) = not(and_star(X1,not(X2))),
inference(cp,[status(thm)],[t169,t19160]) ).
cnf(t19801,plain,
implies(X1,implies(not(X2),not(implies(X2,X1)))) = not(and_star(X1,not(X2))),
inference(step,[status(thm)],[t19198,t169]) ).
cnf(t19802,plain,
implies(X1,implies(implies(X2,X1),X2)) = not(and_star(X1,not(X2))),
inference(step,[status(thm)],[t19801,t180]) ).
cnf(t19803,plain,
implies(X1,implies(implies(X2,X1),X2)) = implies(X1,X2),
inference(step,[status(thm)],[t19802,t84]) ).
cnf(t19294,plain,
implies(X1,implies(implies(X2,X1),X2)) = implies(X1,X2),
inference(orient,[status(thm)],[t19803]) ).
cnf(goal_0,negated_conjecture,
implies(implies(implies(a,b),implies(b,a)),implies(b,a)) != truth,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
implies(implies(implies(b,a),implies(a,b)),implies(a,b)) != truth,
inference(rw,[status(thm)],[goal_0,t9602]) ).
cnf(g0_1,plain,
implies(a,implies(implies(implies(b,a),implies(a,b)),b)) != truth,
inference(rw,[status(thm)],[g0_0,t562]) ).
cnf(g0_2,plain,
implies(a,implies(implies(a,implies(implies(b,a),b)),b)) != truth,
inference(rw,[status(thm)],[g0_1,t562]) ).
cnf(g0_3,plain,
implies(a,implies(implies(a,b),b)) != truth,
inference(rw,[status(thm)],[g0_2,t19294]) ).
cnf(g0_4,plain,
implies(a,implies(implies(b,a),a)) != truth,
inference(rw,[status(thm)],[g0_3,t9602]) ).
cnf(g0_5,plain,
truth != truth,
inference(rw,[status(thm)],[g0_4,t179]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_5]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL109-6 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.11/15.40 % Computer : n008.cluster.edu
% 0.11/15.40 % Model : x86_64 x86_64
% 0.11/15.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/15.40 % Memory : 8046.5625MB
% 0.11/15.40 % OS : Linux 6.8.0-71-generic
% 0.14/15.40 % CPULimit : 300
% 0.14/15.40 % WCLimit : 300
% 0.14/15.40 % DateTime : Wed Sep 23 21:58:28 UTC 2026
% 0.14/15.40 % CPUTime :
% 0.14/15.40 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 21.40/18.34 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 21.40/18.34 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------