%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LDA002-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 : 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:10:49 PM UTC 2026
% Result : Unsatisfiable 7.00s 1.73s
% Output : CNFRefutation 7.00s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 14
% Syntax : Number of clauses : 131 ( 131 unt; 0 nHn; 103 RR)
% Number of literals : 131 ( 130 equ; 3 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 13 con; 0-2 aty)
% Number of variables : 32 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t11,axiom,
sFlat0 = f(b,v),
introduced(definition) ).
cnf(t46,plain,
f(b,v) = sFlat0,
inference(orient,[status(thm)],[t11]) ).
cnf(t12,axiom,
sFlat1 = f(a,v),
introduced(definition) ).
cnf(t49,plain,
f(a,v) = sFlat1,
inference(orient,[status(thm)],[t12]) ).
cnf(t10,axiom,
f(f(X1,X2),f(X1,X3)) = f(X1,f(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t13,plain,
f(f(X1,X2),f(X1,X3)) = f(X1,f(X2,X3)),
inference(orient,[status(thm)],[t10]) ).
cnf(t9,axiom,
f(f(n3,n2),u2) = a,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t16,plain,
f(f(n3,n2),u2) = a,
inference(orient,[status(thm)],[t9]) ).
cnf(t17,plain,
f(f(n3,n2),f(u2,X1)) = f(a,f(f(n3,n2),X1)),
inference(cp,[status(thm)],[t13,t16]) ).
cnf(t1574,plain,
f(f(n3,n2),f(u2,X1)) = f(a,f(f(n3,n2),X1)),
inference(orient,[status(thm)],[t17]) ).
cnf(t4,axiom,
f(u,n2) = u2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t22,plain,
f(u,n2) = u2,
inference(orient,[status(thm)],[t4]) ).
cnf(t23,plain,
f(u,f(n2,X1)) = f(u2,f(u,X1)),
inference(cp,[status(thm)],[t13,t22]) ).
cnf(t112,plain,
f(u,f(n2,X1)) = f(u2,f(u,X1)),
inference(orient,[status(thm)],[t23]) ).
cnf(t2,axiom,
f(n2,n2) = u,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t31,plain,
f(n2,n2) = u,
inference(orient,[status(thm)],[t2]) ).
cnf(t113,plain,
f(u2,f(u,n2)) = f(u,u),
inference(cp,[status(thm)],[t112,t31]) ).
cnf(t4488,plain,
f(u2,u2) = f(u,u),
inference(step,[status(thm)],[t113,t22]) ).
cnf(t6,axiom,
f(u,u) = uu,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t19,plain,
f(u,u) = uu,
inference(orient,[status(thm)],[t6]) ).
cnf(t4489,plain,
f(u2,u2) = uu,
inference(step,[status(thm)],[t4488,t19]) ).
cnf(t119,plain,
f(u2,u2) = uu,
inference(orient,[status(thm)],[t4489]) ).
cnf(t1586,plain,
f(a,f(f(n3,n2),u2)) = f(f(n3,n2),uu),
inference(cp,[status(thm)],[t1574,t119]) ).
cnf(t4656,plain,
f(a,a) = f(f(n3,n2),uu),
inference(step,[status(thm)],[t1586,t16]) ).
cnf(t1596,plain,
f(f(n3,n2),uu) = f(a,a),
inference(orient,[status(thm)],[t4656]) ).
cnf(t1,axiom,
f(n2,n1) = n3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t34,plain,
f(n2,n1) = n3,
inference(orient,[status(thm)],[t1]) ).
cnf(t35,plain,
f(n2,f(n1,X1)) = f(n3,f(n2,X1)),
inference(cp,[status(thm)],[t13,t34]) ).
cnf(t417,plain,
f(n2,f(n1,X1)) = f(n3,f(n2,X1)),
inference(orient,[status(thm)],[t35]) ).
cnf(t0,axiom,
f(n1,n1) = n2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t37,plain,
f(n1,n1) = n2,
inference(orient,[status(thm)],[t0]) ).
cnf(t38,plain,
f(n1,f(n1,X1)) = f(n2,f(n1,X1)),
inference(cp,[status(thm)],[t13,t37]) ).
cnf(t4525,plain,
f(n1,f(n1,X1)) = f(n3,f(n2,X1)),
inference(step,[status(thm)],[t38,t417]) ).
cnf(t483,plain,
f(n1,f(n1,X1)) = f(n3,f(n2,X1)),
inference(orient,[status(thm)],[t4525]) ).
cnf(t484,plain,
f(n3,f(n2,n1)) = f(n1,n2),
inference(cp,[status(thm)],[t483,t37]) ).
cnf(t4526,plain,
f(n3,n3) = f(n1,n2),
inference(step,[status(thm)],[t484,t34]) ).
cnf(t418,plain,
f(n3,f(n2,n1)) = f(n2,n2),
inference(cp,[status(thm)],[t417,t37]) ).
cnf(t4518,plain,
f(n3,n3) = f(n2,n2),
inference(step,[status(thm)],[t418,t34]) ).
cnf(t4519,plain,
f(n3,n3) = u,
inference(step,[status(thm)],[t4518,t31]) ).
cnf(t426,plain,
f(n3,n3) = u,
inference(orient,[status(thm)],[t4519]) ).
cnf(t4527,plain,
u = f(n1,n2),
inference(step,[status(thm)],[t4526,t426]) ).
cnf(t493,plain,
f(n1,n2) = u,
inference(orient,[status(thm)],[t4527]) ).
cnf(t497,plain,
f(n3,f(n2,n2)) = f(n2,u),
inference(cp,[status(thm)],[t417,t493]) ).
cnf(t4528,plain,
f(n3,u) = f(n2,u),
inference(step,[status(thm)],[t497,t31]) ).
cnf(t32,plain,
f(n2,f(n2,X1)) = f(u,f(n2,X1)),
inference(cp,[status(thm)],[t13,t31]) ).
cnf(t4494,plain,
f(n2,f(n2,X1)) = f(u2,f(u,X1)),
inference(step,[status(thm)],[t32,t112]) ).
cnf(t228,plain,
f(n2,f(n2,X1)) = f(u2,f(u,X1)),
inference(orient,[status(thm)],[t4494]) ).
cnf(t229,plain,
f(u2,f(u,n2)) = f(n2,u),
inference(cp,[status(thm)],[t228,t31]) ).
cnf(t4495,plain,
f(u2,u2) = f(n2,u),
inference(step,[status(thm)],[t229,t22]) ).
cnf(t4496,plain,
uu = f(n2,u),
inference(step,[status(thm)],[t4495,t119]) ).
cnf(t235,plain,
f(n2,u) = uu,
inference(orient,[status(thm)],[t4496]) ).
cnf(t4529,plain,
f(n3,u) = uu,
inference(step,[status(thm)],[t4528,t235]) ).
cnf(t501,plain,
f(n3,u) = uu,
inference(orient,[status(thm)],[t4529]) ).
cnf(t503,plain,
f(n3,f(X1,u)) = f(f(n3,X1),uu),
inference(cp,[status(thm)],[t13,t501]) ).
cnf(t2267,plain,
f(f(n3,X1),uu) = f(n3,f(X1,u)),
inference(orient,[status(thm)],[t503]) ).
cnf(t4699,plain,
f(n3,f(n2,u)) = f(a,a),
inference(step,[status(thm)],[t1596,t2267]) ).
cnf(t4700,plain,
f(n3,uu) = f(a,a),
inference(step,[status(thm)],[t4699,t235]) ).
cnf(t496,plain,
f(n3,f(n2,n2)) = f(n1,u),
inference(cp,[status(thm)],[t483,t493]) ).
cnf(t4536,plain,
f(n3,u) = f(n1,u),
inference(step,[status(thm)],[t496,t31]) ).
cnf(t4537,plain,
uu = f(n1,u),
inference(step,[status(thm)],[t4536,t501]) ).
cnf(t518,plain,
f(n1,u) = uu,
inference(orient,[status(thm)],[t4537]) ).
cnf(t522,plain,
f(n3,f(n2,u)) = f(n2,uu),
inference(cp,[status(thm)],[t417,t518]) ).
cnf(t4538,plain,
f(n3,uu) = f(n2,uu),
inference(step,[status(thm)],[t522,t235]) ).
cnf(t238,plain,
f(u2,f(u,u)) = f(n2,uu),
inference(cp,[status(thm)],[t228,t235]) ).
cnf(t4501,plain,
f(u2,uu) = f(n2,uu),
inference(step,[status(thm)],[t238,t19]) ).
cnf(t239,plain,
f(u2,f(u,u)) = f(u,uu),
inference(cp,[status(thm)],[t112,t235]) ).
cnf(t4499,plain,
f(u2,uu) = f(u,uu),
inference(step,[status(thm)],[t239,t19]) ).
cnf(t20,plain,
f(u,f(u,X1)) = f(uu,f(u,X1)),
inference(cp,[status(thm)],[t13,t19]) ).
cnf(t52,plain,
f(u,f(u,X1)) = f(uu,f(u,X1)),
inference(orient,[status(thm)],[t20]) ).
cnf(t55,plain,
f(uu,f(u,u)) = f(u,uu),
inference(cp,[status(thm)],[t52,t19]) ).
cnf(t4482,plain,
f(uu,uu) = f(u,uu),
inference(step,[status(thm)],[t55,t19]) ).
cnf(t8,axiom,
f(uu,uu) = v,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t40,plain,
f(uu,uu) = v,
inference(orient,[status(thm)],[t8]) ).
cnf(t4483,plain,
v = f(u,uu),
inference(step,[status(thm)],[t4482,t40]) ).
cnf(t60,plain,
f(u,uu) = v,
inference(orient,[status(thm)],[t4483]) ).
cnf(t4500,plain,
f(u2,uu) = v,
inference(step,[status(thm)],[t4499,t60]) ).
cnf(t245,plain,
f(u2,uu) = v,
inference(orient,[status(thm)],[t4500]) ).
cnf(t4502,plain,
v = f(n2,uu),
inference(step,[status(thm)],[t4501,t245]) ).
cnf(t248,plain,
f(n2,uu) = v,
inference(orient,[status(thm)],[t4502]) ).
cnf(t4539,plain,
f(n3,uu) = v,
inference(step,[status(thm)],[t4538,t248]) ).
cnf(t526,plain,
f(n3,uu) = v,
inference(orient,[status(thm)],[t4539]) ).
cnf(t4701,plain,
v = f(a,a),
inference(step,[status(thm)],[t4700,t526]) ).
cnf(t2283,plain,
v = f(a,a),
inference(rw,[status(thm)],[t4701]) ).
cnf(t2284,plain,
f(a,a) = v,
inference(orient,[status(thm)],[t2283]) ).
cnf(t2285,plain,
f(a,f(a,X1)) = f(v,f(a,X1)),
inference(cp,[status(thm)],[t13,t2284]) ).
cnf(t4457,plain,
f(a,f(a,X1)) = f(v,f(a,X1)),
inference(orient,[status(thm)],[t2285]) ).
cnf(t4459,plain,
f(v,f(a,a)) = f(a,v),
inference(cp,[status(thm)],[t4457,t2284]) ).
cnf(t4887,plain,
f(v,v) = f(a,v),
inference(step,[status(thm)],[t4459,t2284]) ).
cnf(t42,plain,
f(uu,f(X1,uu)) = f(f(uu,X1),v),
inference(cp,[status(thm)],[t13,t40]) ).
cnf(t704,plain,
f(f(uu,X1),v) = f(uu,f(X1,uu)),
inference(orient,[status(thm)],[t42]) ).
cnf(t3,axiom,
f(u,n1) = u1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t25,plain,
f(u,n1) = u1,
inference(orient,[status(thm)],[t3]) ).
cnf(t26,plain,
f(u,f(n1,X1)) = f(u1,f(u,X1)),
inference(cp,[status(thm)],[t13,t25]) ).
cnf(t158,plain,
f(u,f(n1,X1)) = f(u1,f(u,X1)),
inference(orient,[status(thm)],[t26]) ).
cnf(t39,plain,
f(n1,f(X1,n1)) = f(f(n1,X1),n2),
inference(cp,[status(thm)],[t13,t37]) ).
cnf(t571,plain,
f(f(n1,X1),n2) = f(n1,f(X1,n1)),
inference(orient,[status(thm)],[t39]) ).
cnf(t575,plain,
f(n1,f(n2,n1)) = f(u,n2),
inference(cp,[status(thm)],[t571,t493]) ).
cnf(t4553,plain,
f(n1,n3) = f(u,n2),
inference(step,[status(thm)],[t575,t34]) ).
cnf(t4554,plain,
f(n1,n3) = u2,
inference(step,[status(thm)],[t4553,t22]) ).
cnf(t580,plain,
f(n1,n3) = u2,
inference(orient,[status(thm)],[t4554]) ).
cnf(t586,plain,
f(u1,f(u,n3)) = f(u,u2),
inference(cp,[status(thm)],[t158,t580]) ).
cnf(t5,axiom,
f(u,n3) = u3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t28,plain,
f(u,n3) = u3,
inference(orient,[status(thm)],[t5]) ).
cnf(t4555,plain,
f(u1,u3) = f(u,u2),
inference(step,[status(thm)],[t586,t28]) ).
cnf(t7,axiom,
f(u1,u3) = b,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t43,plain,
f(u1,u3) = b,
inference(orient,[status(thm)],[t7]) ).
cnf(t4556,plain,
b = f(u,u2),
inference(step,[status(thm)],[t4555,t43]) ).
cnf(t56,plain,
f(uu,f(u,n2)) = f(u,u2),
inference(cp,[status(thm)],[t52,t22]) ).
cnf(t4486,plain,
f(uu,u2) = f(u,u2),
inference(step,[status(thm)],[t56,t22]) ).
cnf(t72,plain,
f(u,u2) = f(uu,u2),
inference(orient,[status(thm)],[t4486]) ).
cnf(t4557,plain,
b = f(uu,u2),
inference(step,[status(thm)],[t4556,t72]) ).
cnf(t589,plain,
f(uu,u2) = b,
inference(orient,[status(thm)],[t4557]) ).
cnf(t708,plain,
f(uu,f(u2,uu)) = f(b,v),
inference(cp,[status(thm)],[t704,t589]) ).
cnf(t4595,plain,
f(uu,v) = f(b,v),
inference(step,[status(thm)],[t708,t245]) ).
cnf(t41,plain,
f(uu,f(uu,X1)) = f(v,f(uu,X1)),
inference(cp,[status(thm)],[t13,t40]) ).
cnf(t670,plain,
f(uu,f(uu,X1)) = f(v,f(uu,X1)),
inference(orient,[status(thm)],[t41]) ).
cnf(t671,plain,
f(v,f(uu,uu)) = f(uu,v),
inference(cp,[status(thm)],[t670,t40]) ).
cnf(t4579,plain,
f(v,v) = f(uu,v),
inference(step,[status(thm)],[t671,t40]) ).
cnf(t678,plain,
f(uu,v) = f(v,v),
inference(orient,[status(thm)],[t4579]) ).
cnf(t4596,plain,
f(v,v) = f(b,v),
inference(step,[status(thm)],[t4595,t678]) ).
cnf(t4597,plain,
f(v,v) = sFlat0,
inference(step,[status(thm)],[t4596,t46]) ).
cnf(t712,plain,
f(v,v) = sFlat0,
inference(orient,[status(thm)],[t4597]) ).
cnf(t4888,plain,
sFlat0 = f(a,v),
inference(step,[status(thm)],[t4887,t712]) ).
cnf(t4889,plain,
sFlat0 = sFlat1,
inference(step,[status(thm)],[t4888,t49]) ).
cnf(t4471,plain,
sFlat1 = sFlat0,
inference(orient,[status(thm)],[t4889]) ).
cnf(t4890,plain,
f(a,v) = sFlat0,
inference(step,[status(thm)],[t49,t4471]) ).
cnf(t4472,plain,
f(a,v) = sFlat0,
inference(orient,[status(thm)],[t4890]) ).
cnf(goal_0,negated_conjecture,
f(b,v) != f(a,v),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
sFlat0 != f(a,v),
inference(rw,[status(thm)],[goal_0,t46]) ).
cnf(g0_1,plain,
sFlat0 != sFlat0,
inference(rw,[status(thm)],[g0_0,t4472]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LDA002-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.11/0.36 % Computer : n008.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Thu Sep 24 00:45:53 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 7.00/1.73 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.00/1.73 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------