%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LCL155-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 : n026.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 6.20s 1.37s
% Output : CNFRefutation 6.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 13
% Syntax : Number of clauses : 76 ( 76 unt; 0 nHn; 44 RR)
% Number of literals : 76 ( 75 equ; 12 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 : 12 ( 12 usr; 7 con; 0-2 aty)
% Number of variables : 49 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t5,axiom,
implies(implies(X1,X2),implies(implies(X2,X3),implies(X1,X3))) = truth,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t212,plain,
implies(implies(X1,X2),implies(implies(X2,X3),implies(X1,X3))) = truth,
inference(orient,[status(thm)],[t5]) ).
cnf(t1,axiom,
implies(truth,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t23,plain,
implies(truth,X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t213,plain,
truth = implies(X1,implies(implies(X1,X2),implies(truth,X2))),
inference(cp,[status(thm)],[t212,t23]) ).
cnf(t768,plain,
truth = implies(X1,implies(implies(X1,X2),X2)),
inference(step,[status(thm)],[t213,t23]) ).
cnf(t475,plain,
implies(X1,implies(implies(X1,X2),X2)) = truth,
inference(orient,[status(thm)],[t768]) ).
cnf(t476,plain,
truth = implies(implies(truth,X1),X1),
inference(cp,[status(thm)],[t475,t23]) ).
cnf(t769,plain,
truth = implies(X1,X1),
inference(step,[status(thm)],[t476,t23]) ).
cnf(t579,plain,
implies(X1,X1) = truth,
inference(orient,[status(thm)],[t769]) ).
cnf(t14,axiom,
sF2 = implies(not(not(x)),not(not(x))),
introduced(definition) ).
cnf(t12,axiom,
sF0 = not(x),
introduced(definition) ).
cnf(t22,plain,
not(x) = sF0,
inference(orient,[status(thm)],[t12]) ).
cnf(t744,plain,
sF2 = implies(not(sF0),not(not(x))),
inference(step,[status(thm)],[t14,t22]) ).
cnf(t13,axiom,
sF1 = not(not(x)),
introduced(definition) ).
cnf(t722,plain,
sF1 = not(sF0),
inference(step,[status(thm)],[t13,t22]) ).
cnf(t24,plain,
not(sF0) = sF1,
inference(orient,[status(thm)],[t722]) ).
cnf(t745,plain,
sF2 = implies(sF1,not(not(x))),
inference(step,[status(thm)],[t744,t24]) ).
cnf(t746,plain,
sF2 = implies(sF1,not(sF0)),
inference(step,[status(thm)],[t745,t22]) ).
cnf(t747,plain,
sF2 = implies(sF1,sF1),
inference(step,[status(thm)],[t746,t24]) ).
cnf(t370,plain,
implies(sF1,sF1) = sF2,
inference(orient,[status(thm)],[t747]) ).
cnf(t774,plain,
truth = sF2,
inference(step,[status(thm)],[t370,t579]) ).
cnf(t583,plain,
truth = sF2,
inference(rw,[status(thm)],[t774]) ).
cnf(t615,plain,
truth = sF2,
inference(orient,[status(thm)],[t583]) ).
cnf(t813,plain,
implies(X1,X1) = sF2,
inference(step,[status(thm)],[t579,t615]) ).
cnf(t655,plain,
implies(X1,X1) = sF2,
inference(orient,[status(thm)],[t813]) ).
cnf(t0,axiom,
not(truth) = falsehood,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t21,plain,
not(truth) = falsehood,
inference(orient,[status(thm)],[t0]) ).
cnf(t776,plain,
not(sF2) = falsehood,
inference(step,[status(thm)],[t21,t615]) ).
cnf(t616,plain,
not(sF2) = falsehood,
inference(rw,[status(thm)],[t776]) ).
cnf(t678,plain,
not(sF2) = falsehood,
inference(orient,[status(thm)],[t616]) ).
cnf(t4,axiom,
implies(implies(not(X1),not(X2)),implies(X2,X1)) = truth,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t109,plain,
implies(implies(not(X1),not(X2)),implies(X2,X1)) = truth,
inference(orient,[status(thm)],[t4]) ).
cnf(t111,plain,
truth = implies(implies(not(X1),falsehood),implies(truth,X1)),
inference(cp,[status(thm)],[t109,t21]) ).
cnf(t743,plain,
truth = implies(implies(not(X1),falsehood),X1),
inference(step,[status(thm)],[t111,t23]) ).
cnf(t325,plain,
implies(implies(not(X1),falsehood),X1) = truth,
inference(orient,[status(thm)],[t743]) ).
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(t35,plain,
implies(not(X1),X2) = implies(not(X2),X1),
inference(orient,[status(thm)],[t2]) ).
cnf(t335,plain,
truth = implies(implies(not(falsehood),X1),X1),
inference(cp,[status(thm)],[t325,t35]) ).
cnf(t363,plain,
implies(implies(not(falsehood),X1),X1) = truth,
inference(orient,[status(thm)],[t335]) ).
cnf(t608,plain,
truth = implies(truth,not(falsehood)),
inference(cp,[status(thm)],[t363,t579]) ).
cnf(t815,plain,
truth = not(falsehood),
inference(step,[status(thm)],[t608,t23]) ).
cnf(t816,plain,
sF2 = not(falsehood),
inference(step,[status(thm)],[t815,t615]) ).
cnf(t657,plain,
not(falsehood) = sF2,
inference(orient,[status(thm)],[t816]) ).
cnf(t777,plain,
implies(sF2,X1) = X1,
inference(step,[status(thm)],[t23,t615]) ).
cnf(t617,plain,
implies(sF2,X1) = X1,
inference(rw,[status(thm)],[t777]) ).
cnf(t719,plain,
implies(sF2,X1) = X1,
inference(orient,[status(thm)],[t617]) ).
cnf(t17,axiom,
sF5 = not(not(not(x))),
introduced(definition) ).
cnf(t723,plain,
sF5 = not(not(sF0)),
inference(step,[status(thm)],[t17,t22]) ).
cnf(t724,plain,
sF5 = not(sF1),
inference(step,[status(thm)],[t723,t24]) ).
cnf(t25,plain,
not(sF1) = sF5,
inference(orient,[status(thm)],[t724]) ).
cnf(t38,plain,
implies(not(X1),sF0) = implies(sF1,X1),
inference(cp,[status(thm)],[t35,t24]) ).
cnf(t65,plain,
implies(not(X1),sF0) = implies(sF1,X1),
inference(orient,[status(thm)],[t38]) ).
cnf(t66,plain,
implies(sF1,sF1) = implies(sF5,sF0),
inference(cp,[status(thm)],[t65,t25]) ).
cnf(t69,plain,
implies(sF5,sF0) = implies(sF1,sF1),
inference(orient,[status(thm)],[t66]) ).
cnf(t748,plain,
implies(sF5,sF0) = sF2,
inference(step,[status(thm)],[t69,t370]) ).
cnf(t371,plain,
implies(sF5,sF0) = sF2,
inference(orient,[status(thm)],[t748]) ).
cnf(u8,negated_conjecture,
xor(x,x) != falsehood,
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(x))))),not(implies(not(not(not(x))),not(x)))) != falsehood,
inference(definition_unfolding,[status(thm)],[u8,d2]) ).
cnf(g0_0,plain,
implies(not(not(sF2)),not(implies(not(not(not(x))),not(x)))) != falsehood,
inference(rw,[status(thm)],[goal_0,t655]) ).
cnf(g0_1,plain,
implies(not(falsehood),not(implies(not(not(not(x))),not(x)))) != falsehood,
inference(rw,[status(thm)],[g0_0,t678]) ).
cnf(g0_2,plain,
implies(sF2,not(implies(not(not(not(x))),not(x)))) != falsehood,
inference(rw,[status(thm)],[g0_1,t657]) ).
cnf(g0_3,plain,
not(implies(not(not(not(x))),not(x))) != falsehood,
inference(rw,[status(thm)],[g0_2,t719]) ).
cnf(g0_4,plain,
not(implies(not(not(sF0)),not(x))) != falsehood,
inference(rw,[status(thm)],[g0_3,t22]) ).
cnf(g0_5,plain,
not(implies(not(sF1),not(x))) != falsehood,
inference(rw,[status(thm)],[g0_4,t24]) ).
cnf(g0_6,plain,
not(implies(sF5,not(x))) != falsehood,
inference(rw,[status(thm)],[g0_5,t25]) ).
cnf(g0_7,plain,
not(implies(sF5,sF0)) != falsehood,
inference(rw,[status(thm)],[g0_6,t22]) ).
cnf(g0_8,plain,
not(sF2) != falsehood,
inference(rw,[status(thm)],[g0_7,t371]) ).
cnf(g0_9,plain,
falsehood != falsehood,
inference(rw,[status(thm)],[g0_8,t678]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_9]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL155-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n026.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Wed Sep 23 22:09:23 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 6.20/1.37 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.20/1.37 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------