%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LCL160-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 : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 02:01:06 PM UTC 2026
% Result : Unsatisfiable 26.83s 3.93s
% Output : CNFRefutation 26.83s
% Verified :
% SZS Type : Refutation
% Derivation depth : 81
% Number of leaves : 13
% Syntax : Number of clauses : 155 ( 155 unt; 0 nHn; 19 RR)
% Number of literals : 155 ( 154 equ; 16 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 : 10 ( 10 usr; 4 con; 0-2 aty)
% Number of variables : 244 ( 11 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t2,axiom,
and(X1,X2) = and(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t8,axiom,
not(or(not(X1),not(X2))) = and_star(X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t7,axiom,
not(or(not(X1),not(X2))) = and(X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t46,plain,
not(or(not(X1),not(X2))) = and(X1,X2),
inference(orient,[status(thm)],[t7]) ).
cnf(t6624,plain,
and(X1,X2) = and_star(X1,X2),
inference(step,[status(thm)],[t8,t46]) ).
cnf(t50,plain,
and(X1,X2) = and_star(X1,X2),
inference(orient,[status(thm)],[t6624]) ).
cnf(t6630,plain,
and_star(X1,X2) = and(X2,X1),
inference(step,[status(thm)],[t2,t50]) ).
cnf(t6631,plain,
and_star(X1,X2) = and_star(X2,X1),
inference(step,[status(thm)],[t6630,t50]) ).
cnf(t76,plain,
and_star(X1,X2) = and_star(X2,X1),
inference(orient,[status(thm)],[t6631]) ).
cnf(t15,axiom,
or(and(X1,not(X2)),and(not(X1),X2)) = xor(X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t6628,plain,
or(and_star(X1,not(X2)),and(not(X1),X2)) = xor(X1,X2),
inference(step,[status(thm)],[t15,t50]) ).
cnf(t6629,plain,
or(and_star(X1,not(X2)),and_star(not(X1),X2)) = xor(X1,X2),
inference(step,[status(thm)],[t6628,t50]) ).
cnf(t69,plain,
or(and_star(X1,not(X2)),and_star(not(X1),X2)) = xor(X1,X2),
inference(orient,[status(thm)],[t6629]) ).
cnf(t77,plain,
or(and_star(X1,not(X2)),and_star(not(X1),X2)) = xor(X1,X2),
inference(rw,[status(thm)],[t69]) ).
cnf(t6908,plain,
or(and_star(X1,not(X2)),and_star(X2,not(X1))) = xor(X1,X2),
inference(step,[status(thm)],[t77,t76]) ).
cnf(t6,axiom,
implies(not(X1),X2) = or(X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t40,plain,
implies(not(X1),X2) = or(X1,X2),
inference(orient,[status(thm)],[t6]) ).
cnf(t11,axiom,
implies(implies(X1,X2),X2) = implies(implies(X2,X1),X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t17,plain,
implies(implies(X1,X2),X2) = implies(implies(X2,X1),X1),
inference(orient,[status(thm)],[t11]) ).
cnf(t14,axiom,
implies(implies(X1,X2),implies(implies(X2,X3),implies(X1,X3))) = truth,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t19,plain,
implies(implies(X1,X2),implies(implies(X2,X3),implies(X1,X3))) = truth,
inference(orient,[status(thm)],[t14]) ).
cnf(t1,axiom,
implies(truth,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t16,plain,
implies(truth,X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t20,plain,
truth = implies(X1,implies(implies(X1,X2),implies(truth,X2))),
inference(cp,[status(thm)],[t19,t16]) ).
cnf(t6640,plain,
truth = implies(X1,implies(implies(X1,X2),X2)),
inference(step,[status(thm)],[t20,t16]) ).
cnf(t111,plain,
implies(X1,implies(implies(X1,X2),X2)) = truth,
inference(orient,[status(thm)],[t6640]) ).
cnf(t18,plain,
implies(implies(X1,truth),truth) = implies(X1,X1),
inference(cp,[status(thm)],[t17,t16]) ).
cnf(t115,plain,
truth = implies(implies(truth,X1),X1),
inference(cp,[status(thm)],[t111,t16]) ).
cnf(t6641,plain,
truth = implies(X1,X1),
inference(step,[status(thm)],[t115,t16]) ).
cnf(t127,plain,
implies(X1,X1) = truth,
inference(orient,[status(thm)],[t6641]) ).
cnf(t6655,plain,
implies(implies(X1,truth),truth) = truth,
inference(step,[status(thm)],[t18,t127]) ).
cnf(t190,plain,
implies(implies(X1,truth),truth) = truth,
inference(orient,[status(thm)],[t6655]) ).
cnf(t197,plain,
truth = implies(X1,truth),
inference(cp,[status(thm)],[t111,t190]) ).
cnf(t198,plain,
implies(X1,truth) = truth,
inference(orient,[status(thm)],[t197]) ).
cnf(t202,plain,
truth = implies(truth,implies(implies(truth,X1),implies(X2,X1))),
inference(cp,[status(thm)],[t19,t198]) ).
cnf(t6662,plain,
truth = implies(implies(truth,X1),implies(X2,X1)),
inference(step,[status(thm)],[t202,t16]) ).
cnf(t6663,plain,
truth = implies(X1,implies(X2,X1)),
inference(step,[status(thm)],[t6662,t16]) ).
cnf(t219,plain,
implies(X1,implies(X2,X1)) = truth,
inference(orient,[status(thm)],[t6663]) ).
cnf(t226,plain,
implies(implies(implies(X1,X2),X2),X2) = implies(truth,implies(X1,X2)),
inference(cp,[status(thm)],[t17,t219]) ).
cnf(t6667,plain,
implies(implies(implies(X1,X2),X2),X2) = implies(X1,X2),
inference(step,[status(thm)],[t226,t16]) ).
cnf(t279,plain,
implies(implies(implies(X1,X2),X2),X2) = implies(X1,X2),
inference(orient,[status(thm)],[t6667]) ).
cnf(t282,plain,
implies(not(X1),X2) = implies(implies(or(X1,X2),X2),X2),
inference(cp,[status(thm)],[t279,t40]) ).
cnf(t6669,plain,
or(X1,X2) = implies(implies(or(X1,X2),X2),X2),
inference(step,[status(thm)],[t282,t40]) ).
cnf(t298,plain,
implies(implies(or(X1,X2),X2),X2) = or(X1,X2),
inference(orient,[status(thm)],[t6669]) ).
cnf(t223,plain,
truth = implies(X1,or(X2,X1)),
inference(cp,[status(thm)],[t219,t40]) ).
cnf(t4,axiom,
or(X1,X2) = or(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t57,plain,
or(X1,X2) = or(X2,X1),
inference(orient,[status(thm)],[t4]) ).
cnf(t6664,plain,
truth = implies(X1,or(X1,X2)),
inference(step,[status(thm)],[t223,t57]) ).
cnf(t227,plain,
implies(X1,or(X1,X2)) = truth,
inference(orient,[status(thm)],[t6664]) ).
cnf(t236,plain,
implies(implies(or(X1,X2),X1),X1) = implies(truth,or(X1,X2)),
inference(cp,[status(thm)],[t17,t227]) ).
cnf(t6668,plain,
implies(implies(or(X1,X2),X1),X1) = or(X1,X2),
inference(step,[status(thm)],[t236,t16]) ).
cnf(t287,plain,
implies(implies(or(X1,X2),X1),X1) = or(X1,X2),
inference(orient,[status(thm)],[t6668]) ).
cnf(t12,axiom,
implies(implies(not(X1),not(X2)),implies(X2,X1)) = truth,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t31,plain,
implies(implies(not(X1),not(X2)),implies(X2,X1)) = truth,
inference(orient,[status(thm)],[t12]) ).
cnf(t6623,plain,
implies(or(X1,not(X2)),implies(X2,X1)) = truth,
inference(step,[status(thm)],[t31,t40]) ).
cnf(t45,plain,
implies(or(X1,not(X2)),implies(X2,X1)) = truth,
inference(rw,[status(thm)],[t6623]) ).
cnf(t309,plain,
implies(or(X1,not(X2)),implies(X2,X1)) = truth,
inference(orient,[status(thm)],[t45]) ).
cnf(t0,axiom,
not(truth) = falsehood,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t53,plain,
not(truth) = falsehood,
inference(orient,[status(thm)],[t0]) ).
cnf(t315,plain,
truth = implies(or(X1,falsehood),implies(truth,X1)),
inference(cp,[status(thm)],[t309,t53]) ).
cnf(t6670,plain,
truth = implies(or(X1,falsehood),X1),
inference(step,[status(thm)],[t315,t16]) ).
cnf(t325,plain,
implies(or(X1,falsehood),X1) = truth,
inference(orient,[status(thm)],[t6670]) ).
cnf(t330,plain,
or(X1,falsehood) = implies(truth,X1),
inference(cp,[status(thm)],[t287,t325]) ).
cnf(t6680,plain,
or(X1,falsehood) = X1,
inference(step,[status(thm)],[t330,t16]) ).
cnf(t340,plain,
or(X1,falsehood) = X1,
inference(orient,[status(thm)],[t6680]) ).
cnf(t344,plain,
or(X1,falsehood) = implies(implies(X1,falsehood),falsehood),
inference(cp,[status(thm)],[t298,t340]) ).
cnf(t6685,plain,
X1 = implies(implies(X1,falsehood),falsehood),
inference(step,[status(thm)],[t344,t340]) ).
cnf(t390,plain,
implies(implies(X1,falsehood),falsehood) = X1,
inference(orient,[status(thm)],[t6685]) ).
cnf(t392,plain,
not(X1) = implies(or(X1,falsehood),falsehood),
inference(cp,[status(thm)],[t390,t40]) ).
cnf(t6686,plain,
not(X1) = implies(X1,falsehood),
inference(step,[status(thm)],[t392,t340]) ).
cnf(t399,plain,
implies(X1,falsehood) = not(X1),
inference(orient,[status(thm)],[t6686]) ).
cnf(t402,plain,
not(implies(or(X1,falsehood),falsehood)) = or(X1,falsehood),
inference(cp,[status(thm)],[t399,t298]) ).
cnf(t6692,plain,
not(not(or(X1,falsehood))) = or(X1,falsehood),
inference(step,[status(thm)],[t402,t399]) ).
cnf(t6693,plain,
not(not(X1)) = or(X1,falsehood),
inference(step,[status(thm)],[t6692,t340]) ).
cnf(t6694,plain,
not(not(X1)) = X1,
inference(step,[status(thm)],[t6693,t340]) ).
cnf(t428,plain,
not(not(X1)) = X1,
inference(orient,[status(thm)],[t6694]) ).
cnf(t431,plain,
or(not(X1),X2) = implies(X1,X2),
inference(cp,[status(thm)],[t40,t428]) ).
cnf(t6699,plain,
or(X2,not(X1)) = implies(X1,X2),
inference(step,[status(thm)],[t431,t57]) ).
cnf(t453,plain,
or(X1,not(X2)) = implies(X2,X1),
inference(orient,[status(thm)],[t6699]) ).
cnf(t6625,plain,
not(or(not(X1),not(X2))) = and_star(X1,X2),
inference(step,[status(thm)],[t46,t50]) ).
cnf(t51,plain,
not(or(not(X1),not(X2))) = and_star(X1,X2),
inference(orient,[status(thm)],[t6625]) ).
cnf(t6707,plain,
not(implies(X2,not(X1))) = and_star(X1,X2),
inference(step,[status(thm)],[t51,t453]) ).
cnf(t463,plain,
not(implies(X2,not(X1))) = and_star(X1,X2),
inference(rw,[status(thm)],[t6707]) ).
cnf(t477,plain,
not(implies(X1,not(X2))) = and_star(X2,X1),
inference(orient,[status(thm)],[t463]) ).
cnf(t480,plain,
and_star(X1,not(X2)) = not(or(X2,not(X1))),
inference(cp,[status(thm)],[t477,t40]) ).
cnf(t6711,plain,
and_star(X1,not(X2)) = not(implies(X1,X2)),
inference(step,[status(thm)],[t480,t453]) ).
cnf(t493,plain,
not(implies(X1,X2)) = and_star(X1,not(X2)),
inference(orient,[status(thm)],[t6711]) ).
cnf(t506,plain,
implies(implies(X1,X2),X3) = or(X3,and_star(X1,not(X2))),
inference(cp,[status(thm)],[t453,t493]) ).
cnf(t820,plain,
or(X1,and_star(X2,not(X3))) = implies(implies(X2,X3),X1),
inference(orient,[status(thm)],[t506]) ).
cnf(t6909,plain,
implies(implies(X2,X1),and_star(X1,not(X2))) = xor(X1,X2),
inference(step,[status(thm)],[t6908,t820]) ).
cnf(t6514,plain,
implies(implies(X1,X2),and_star(X2,not(X1))) = xor(X2,X1),
inference(orient,[status(thm)],[t6909]) ).
cnf(t6533,plain,
xor(truth,X1) = implies(truth,and_star(truth,not(X1))),
inference(cp,[status(thm)],[t6514,t198]) ).
cnf(t5,axiom,
xor(X1,X2) = xor(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t88,plain,
xor(X1,X2) = xor(X2,X1),
inference(orient,[status(thm)],[t5]) ).
cnf(t6920,plain,
xor(X1,truth) = implies(truth,and_star(truth,not(X1))),
inference(step,[status(thm)],[t6533,t88]) ).
cnf(t6921,plain,
xor(X1,truth) = and_star(truth,not(X1)),
inference(step,[status(thm)],[t6920,t16]) ).
cnf(t500,plain,
and_star(truth,not(X1)) = not(X1),
inference(cp,[status(thm)],[t493,t16]) ).
cnf(t516,plain,
and_star(truth,not(X1)) = not(X1),
inference(orient,[status(thm)],[t500]) ).
cnf(t6922,plain,
xor(X1,truth) = not(X1),
inference(step,[status(thm)],[t6921,t516]) ).
cnf(t6621,plain,
xor(X1,truth) = not(X1),
inference(orient,[status(thm)],[t6922]) ).
cnf(t507,plain,
implies(X1,X2) = not(and_star(X1,not(X2))),
inference(cp,[status(thm)],[t428,t493]) ).
cnf(t521,plain,
not(and_star(X1,not(X2))) = implies(X1,X2),
inference(orient,[status(thm)],[t507]) ).
cnf(t524,plain,
implies(X1,not(X2)) = not(and_star(X1,X2)),
inference(cp,[status(thm)],[t521,t428]) ).
cnf(t542,plain,
not(and_star(X1,X2)) = implies(X1,not(X2)),
inference(orient,[status(thm)],[t524]) ).
cnf(t543,plain,
implies(X1,not(X2)) = not(and_star(X2,X1)),
inference(cp,[status(thm)],[t542,t76]) ).
cnf(t6725,plain,
implies(X1,not(X2)) = implies(X2,not(X1)),
inference(step,[status(thm)],[t543,t542]) ).
cnf(t687,plain,
implies(X1,not(X2)) = implies(X2,not(X1)),
inference(orient,[status(thm)],[t6725]) ).
cnf(t4544,plain,
implies(implies(or(X1,X2),X2),X2) = or(X1,X2),
inference(rw,[status(thm)],[t298]) ).
cnf(t691,plain,
implies(X1,not(implies(X2,not(X1)))) = implies(implies(not(X1),X2),X2),
inference(cp,[status(thm)],[t687,t17]) ).
cnf(t6858,plain,
implies(X1,and_star(X2,not(not(X1)))) = implies(implies(not(X1),X2),X2),
inference(step,[status(thm)],[t691,t493]) ).
cnf(t6859,plain,
implies(X1,and_star(X2,X1)) = implies(implies(not(X1),X2),X2),
inference(step,[status(thm)],[t6858,t428]) ).
cnf(t6860,plain,
implies(X1,and_star(X1,X2)) = implies(implies(not(X1),X2),X2),
inference(step,[status(thm)],[t6859,t76]) ).
cnf(t6861,plain,
implies(X1,and_star(X1,X2)) = implies(or(X1,X2),X2),
inference(step,[status(thm)],[t6860,t40]) ).
cnf(t4304,plain,
implies(X1,and_star(X1,X2)) = implies(or(X1,X2),X2),
inference(orient,[status(thm)],[t6861]) ).
cnf(t6862,plain,
implies(implies(X1,and_star(X1,X2)),X2) = or(X1,X2),
inference(step,[status(thm)],[t4544,t4304]) ).
cnf(t4643,plain,
implies(implies(X1,and_star(X1,X2)),X2) = or(X1,X2),
inference(orient,[status(thm)],[t6862]) ).
cnf(t4645,plain,
or(X1,not(X2)) = implies(X2,not(implies(X1,and_star(X1,not(X2))))),
inference(cp,[status(thm)],[t4643,t687]) ).
cnf(t6863,plain,
implies(X2,X1) = implies(X2,not(implies(X1,and_star(X1,not(X2))))),
inference(step,[status(thm)],[t4645,t453]) ).
cnf(t6864,plain,
implies(X2,X1) = implies(X2,and_star(X1,not(and_star(X1,not(X2))))),
inference(step,[status(thm)],[t6863,t493]) ).
cnf(t6865,plain,
implies(X2,X1) = implies(X2,and_star(X1,implies(X1,X2))),
inference(step,[status(thm)],[t6864,t521]) ).
cnf(t4759,plain,
implies(X1,and_star(X2,implies(X2,X1))) = implies(X1,X2),
inference(orient,[status(thm)],[t6865]) ).
cnf(t4828,plain,
implies(implies(and_star(X1,implies(X1,X2)),X2),X2) = implies(implies(X2,X1),and_star(X1,implies(X1,X2))),
inference(cp,[status(thm)],[t17,t4759]) ).
cnf(t548,plain,
implies(and_star(X1,X2),X3) = or(X3,implies(X1,not(X2))),
inference(cp,[status(thm)],[t453,t542]) ).
cnf(t899,plain,
or(X1,implies(X2,not(X3))) = implies(and_star(X2,X3),X1),
inference(orient,[status(thm)],[t548]) ).
cnf(t114,plain,
truth = or(X1,implies(implies(not(X1),X2),X2)),
inference(cp,[status(thm)],[t111,t40]) ).
cnf(t6650,plain,
truth = or(X1,implies(or(X1,X2),X2)),
inference(step,[status(thm)],[t114,t40]) ).
cnf(t174,plain,
or(X1,implies(or(X1,X2),X2)) = truth,
inference(orient,[status(thm)],[t6650]) ).
cnf(t901,plain,
implies(and_star(or(X1,not(X2)),X2),X1) = truth,
inference(cp,[status(thm)],[t899,t174]) ).
cnf(t6737,plain,
implies(and_star(X2,or(X1,not(X2))),X1) = truth,
inference(step,[status(thm)],[t901,t76]) ).
cnf(t6738,plain,
implies(and_star(X2,implies(X2,X1)),X1) = truth,
inference(step,[status(thm)],[t6737,t453]) ).
cnf(t950,plain,
implies(and_star(X1,implies(X1,X2)),X2) = truth,
inference(orient,[status(thm)],[t6738]) ).
cnf(t6870,plain,
implies(truth,X2) = implies(implies(X2,X1),and_star(X1,implies(X1,X2))),
inference(step,[status(thm)],[t4828,t950]) ).
cnf(t6871,plain,
X2 = implies(implies(X2,X1),and_star(X1,implies(X1,X2))),
inference(step,[status(thm)],[t6870,t16]) ).
cnf(t4975,plain,
implies(implies(X1,X2),and_star(X2,implies(X2,X1))) = X1,
inference(orient,[status(thm)],[t6871]) ).
cnf(t5015,plain,
and_star(X1,implies(X1,X2)) = implies(implies(and_star(X1,implies(X1,X2)),X2),and_star(X2,implies(X2,X1))),
inference(cp,[status(thm)],[t4975,t4759]) ).
cnf(t6906,plain,
and_star(X1,implies(X1,X2)) = implies(truth,and_star(X2,implies(X2,X1))),
inference(step,[status(thm)],[t5015,t950]) ).
cnf(t6907,plain,
and_star(X1,implies(X1,X2)) = and_star(X2,implies(X2,X1)),
inference(step,[status(thm)],[t6906,t16]) ).
cnf(t6465,plain,
and_star(X1,implies(X1,X2)) = and_star(X2,implies(X2,X1)),
inference(orient,[status(thm)],[t6907]) ).
cnf(goal_0,negated_conjecture,
and_star(xor(and_star(xor(truth,y),x),truth),x) != and_star(xor(and_star(xor(truth,x),y),truth),y),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
and_star(x,xor(and_star(xor(truth,y),x),truth)) != and_star(xor(and_star(xor(truth,x),y),truth),y),
inference(rw,[status(thm)],[goal_0,t76]) ).
cnf(g0_1,plain,
and_star(x,not(and_star(xor(truth,y),x))) != and_star(xor(and_star(xor(truth,x),y),truth),y),
inference(rw,[status(thm)],[g0_0,t6621]) ).
cnf(g0_2,plain,
and_star(x,implies(xor(truth,y),not(x))) != and_star(xor(and_star(xor(truth,x),y),truth),y),
inference(rw,[status(thm)],[g0_1,t542]) ).
cnf(g0_3,plain,
and_star(x,implies(x,not(xor(truth,y)))) != and_star(xor(and_star(xor(truth,x),y),truth),y),
inference(rw,[status(thm)],[g0_2,t687]) ).
cnf(g0_4,plain,
and_star(x,implies(x,not(xor(y,truth)))) != and_star(xor(and_star(xor(truth,x),y),truth),y),
inference(rw,[status(thm)],[g0_3,t88]) ).
cnf(g0_5,plain,
and_star(x,implies(x,not(not(y)))) != and_star(xor(and_star(xor(truth,x),y),truth),y),
inference(rw,[status(thm)],[g0_4,t6621]) ).
cnf(g0_6,plain,
and_star(x,implies(x,y)) != and_star(xor(and_star(xor(truth,x),y),truth),y),
inference(rw,[status(thm)],[g0_5,t428]) ).
cnf(g0_7,plain,
and_star(y,implies(y,x)) != and_star(xor(and_star(xor(truth,x),y),truth),y),
inference(rw,[status(thm)],[g0_6,t6465]) ).
cnf(g0_8,plain,
and_star(y,implies(y,x)) != and_star(y,xor(and_star(xor(truth,x),y),truth)),
inference(rw,[status(thm)],[g0_7,t76]) ).
cnf(g0_9,plain,
and_star(y,implies(y,x)) != and_star(y,not(and_star(xor(truth,x),y))),
inference(rw,[status(thm)],[g0_8,t6621]) ).
cnf(g0_10,plain,
and_star(y,implies(y,x)) != and_star(y,implies(xor(truth,x),not(y))),
inference(rw,[status(thm)],[g0_9,t542]) ).
cnf(g0_11,plain,
and_star(y,implies(y,x)) != and_star(y,implies(y,not(xor(truth,x)))),
inference(rw,[status(thm)],[g0_10,t687]) ).
cnf(g0_12,plain,
and_star(y,implies(y,x)) != and_star(y,implies(y,not(xor(x,truth)))),
inference(rw,[status(thm)],[g0_11,t88]) ).
cnf(g0_13,plain,
and_star(y,implies(y,x)) != and_star(y,implies(y,not(not(x)))),
inference(rw,[status(thm)],[g0_12,t6621]) ).
cnf(g0_14,plain,
and_star(y,implies(y,x)) != and_star(y,implies(y,x)),
inference(rw,[status(thm)],[g0_13,t428]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_14]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL160-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.13/0.38 % Computer : n015.cluster.edu
% 0.13/0.38 % Model : x86_64 x86_64
% 0.13/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.38 % Memory : 8046.5625MB
% 0.13/0.38 % OS : Linux 6.8.0-71-generic
% 0.13/0.38 % CPULimit : 300
% 0.13/0.38 % WCLimit : 300
% 0.13/0.38 % DateTime : Wed Sep 23 22:10:39 UTC 2026
% 0.13/0.38 % CPUTime :
% 0.13/0.38 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 26.83/3.93 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 26.83/3.93 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------