%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : HWC001-1 : TPTP v9.3.1. Bugfixed v1.1.1.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n011.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 01:37:32 PM UTC 2026
% Result : Unsatisfiable 4.53s 16.17s
% Output : Proof 4.53s
% Verified :
% Comments :
%------------------------------------------------------------------------------
cnf(t14,axiom,
sF6 = output(n0,n1,n1,n1),
introduced(definition) ).
cnf(t47,plain,
output(n0,n1,n1,n1) = sF6,
inference(orient,[status(thm)],[t14]) ).
cnf(t12,axiom,
sF4(X1,X2,X3,X4,X5,X6,X7,X8) = ifeq(output(X1,X2,X3,X4),true,output(not(and(X5,X1)),not(and(X6,X2)),not(and(X7,X3)),not(and(X8,X4))),true),
introduced(definition) ).
cnf(t8,axiom,
sF0 = output(n0,n0,n1,n1),
introduced(definition) ).
cnf(f6,negated_conjecture,
output(n0,n0,n1,n1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',input1) ).
fof(f6_nnf,plain,
output(n0,n0,n1,n1),
inference(nnf_transformation,[status(thm)],[f6]) ).
cnf(c6,plain,
output(n0,n0,n1,n1),
inference(cnf_transformation,[status(esa)],[f6_nnf]) ).
cnf(t5,plain,
output(n0,n0,n1,n1) = true,
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t25,plain,
output(n0,n0,n1,n1) = true,
inference(orient,[status(thm)],[t5]) ).
cnf(t475,plain,
sF0 = true,
inference(step,[status(thm)],[t8,t25]) ).
cnf(t40,plain,
true = sF0,
inference(orient,[status(thm)],[t475]) ).
cnf(t485,plain,
sF4(X1,X2,X3,X4,X5,X6,X7,X8) = ifeq(output(X1,X2,X3,X4),sF0,output(not(and(X5,X1)),not(and(X6,X2)),not(and(X7,X3)),not(and(X8,X4))),true),
inference(step,[status(thm)],[t12,t40]) ).
cnf(t10,axiom,
sF2(X1,X2) = not(and(X1,X2)),
introduced(definition) ).
cnf(t19,plain,
not(and(X1,X2)) = sF2(X1,X2),
inference(orient,[status(thm)],[t10]) ).
cnf(t486,plain,
sF4(X1,X2,X3,X4,X5,X6,X7,X8) = ifeq(output(X1,X2,X3,X4),sF0,output(sF2(X5,X1),not(and(X6,X2)),not(and(X7,X3)),not(and(X8,X4))),true),
inference(step,[status(thm)],[t485,t19]) ).
cnf(t487,plain,
sF4(X1,X2,X3,X4,X5,X6,X7,X8) = ifeq(output(X1,X2,X3,X4),sF0,output(sF2(X5,X1),sF2(X6,X2),not(and(X7,X3)),not(and(X8,X4))),true),
inference(step,[status(thm)],[t486,t19]) ).
cnf(t488,plain,
sF4(X1,X2,X3,X4,X5,X6,X7,X8) = ifeq(output(X1,X2,X3,X4),sF0,output(sF2(X5,X1),sF2(X6,X2),sF2(X7,X3),not(and(X8,X4))),true),
inference(step,[status(thm)],[t487,t19]) ).
cnf(t489,plain,
sF4(X1,X2,X3,X4,X5,X6,X7,X8) = ifeq(output(X1,X2,X3,X4),sF0,output(sF2(X5,X1),sF2(X6,X2),sF2(X7,X3),sF2(X8,X4)),true),
inference(step,[status(thm)],[t488,t19]) ).
cnf(t11,axiom,
sF3(X1,X2,X3,X4,X5,X6,X7,X8) = output(not(and(X1,X2)),not(and(X3,X4)),not(and(X5,X6)),not(and(X7,X8))),
introduced(definition) ).
cnf(t481,plain,
sF3(X1,X2,X3,X4,X5,X6,X7,X8) = output(sF2(X1,X2),not(and(X3,X4)),not(and(X5,X6)),not(and(X7,X8))),
inference(step,[status(thm)],[t11,t19]) ).
cnf(t482,plain,
sF3(X1,X2,X3,X4,X5,X6,X7,X8) = output(sF2(X1,X2),sF2(X3,X4),not(and(X5,X6)),not(and(X7,X8))),
inference(step,[status(thm)],[t481,t19]) ).
cnf(t483,plain,
sF3(X1,X2,X3,X4,X5,X6,X7,X8) = output(sF2(X1,X2),sF2(X3,X4),sF2(X5,X6),not(and(X7,X8))),
inference(step,[status(thm)],[t482,t19]) ).
cnf(t484,plain,
sF3(X1,X2,X3,X4,X5,X6,X7,X8) = output(sF2(X1,X2),sF2(X3,X4),sF2(X5,X6),sF2(X7,X8)),
inference(step,[status(thm)],[t483,t19]) ).
cnf(t48,plain,
output(sF2(X1,X2),sF2(X3,X4),sF2(X5,X6),sF2(X7,X8)) = sF3(X1,X2,X3,X4,X5,X6,X7,X8),
inference(orient,[status(thm)],[t484]) ).
cnf(t490,plain,
sF4(X1,X2,X3,X4,X5,X6,X7,X8) = ifeq(output(X1,X2,X3,X4),sF0,sF3(X5,X1,X6,X2,X7,X3,X8,X4),true),
inference(step,[status(thm)],[t489,t48]) ).
cnf(t491,plain,
sF4(X1,X2,X3,X4,X5,X6,X7,X8) = ifeq(output(X1,X2,X3,X4),sF0,sF3(X5,X1,X6,X2,X7,X3,X8,X4),sF0),
inference(step,[status(thm)],[t490,t40]) ).
cnf(t93,plain,
ifeq(output(X1,X2,X3,X4),sF0,sF3(X5,X1,X6,X2,X7,X3,X8,X4),sF0) = sF4(X1,X2,X3,X4,X5,X6,X7,X8),
inference(orient,[status(thm)],[t491]) ).
cnf(t13,axiom,
sF5(X1,X2,X3,X4,X5,X6,X7,X8) = ifeq(output(X1,X2,X3,X4),true,ifeq(output(X5,X6,X7,X8),true,output(not(and(X1,X5)),not(and(X2,X6)),not(and(X3,X7)),not(and(X4,X8))),true),true),
introduced(definition) ).
cnf(t492,plain,
sF5(X1,X2,X3,X4,X5,X6,X7,X8) = ifeq(output(X1,X2,X3,X4),sF0,ifeq(output(X5,X6,X7,X8),true,output(not(and(X1,X5)),not(and(X2,X6)),not(and(X3,X7)),not(and(X4,X8))),true),true),
inference(step,[status(thm)],[t13,t40]) ).
cnf(t493,plain,
sF5(X1,X2,X3,X4,X5,X6,X7,X8) = ifeq(output(X1,X2,X3,X4),sF0,ifeq(output(X5,X6,X7,X8),sF0,output(not(and(X1,X5)),not(and(X2,X6)),not(and(X3,X7)),not(and(X4,X8))),true),true),
inference(step,[status(thm)],[t492,t40]) ).
cnf(t494,plain,
sF5(X1,X2,X3,X4,X5,X6,X7,X8) = ifeq(output(X1,X2,X3,X4),sF0,ifeq(output(X5,X6,X7,X8),sF0,output(sF2(X1,X5),not(and(X2,X6)),not(and(X3,X7)),not(and(X4,X8))),true),true),
inference(step,[status(thm)],[t493,t19]) ).
cnf(t495,plain,
sF5(X1,X2,X3,X4,X5,X6,X7,X8) = ifeq(output(X1,X2,X3,X4),sF0,ifeq(output(X5,X6,X7,X8),sF0,output(sF2(X1,X5),sF2(X2,X6),not(and(X3,X7)),not(and(X4,X8))),true),true),
inference(step,[status(thm)],[t494,t19]) ).
cnf(t496,plain,
sF5(X1,X2,X3,X4,X5,X6,X7,X8) = ifeq(output(X1,X2,X3,X4),sF0,ifeq(output(X5,X6,X7,X8),sF0,output(sF2(X1,X5),sF2(X2,X6),sF2(X3,X7),not(and(X4,X8))),true),true),
inference(step,[status(thm)],[t495,t19]) ).
cnf(t497,plain,
sF5(X1,X2,X3,X4,X5,X6,X7,X8) = ifeq(output(X1,X2,X3,X4),sF0,ifeq(output(X5,X6,X7,X8),sF0,output(sF2(X1,X5),sF2(X2,X6),sF2(X3,X7),sF2(X4,X8)),true),true),
inference(step,[status(thm)],[t496,t19]) ).
cnf(t498,plain,
sF5(X1,X2,X3,X4,X5,X6,X7,X8) = ifeq(output(X1,X2,X3,X4),sF0,ifeq(output(X5,X6,X7,X8),sF0,sF3(X1,X5,X2,X6,X3,X7,X4,X8),true),true),
inference(step,[status(thm)],[t497,t48]) ).
cnf(t499,plain,
sF5(X1,X2,X3,X4,X5,X6,X7,X8) = ifeq(output(X1,X2,X3,X4),sF0,ifeq(output(X5,X6,X7,X8),sF0,sF3(X1,X5,X2,X6,X3,X7,X4,X8),sF0),true),
inference(step,[status(thm)],[t498,t40]) ).
cnf(t500,plain,
sF5(X1,X2,X3,X4,X5,X6,X7,X8) = ifeq(output(X1,X2,X3,X4),sF0,sF4(X5,X6,X7,X8,X1,X2,X3,X4),true),
inference(step,[status(thm)],[t499,t93]) ).
cnf(t501,plain,
sF5(X1,X2,X3,X4,X5,X6,X7,X8) = ifeq(output(X1,X2,X3,X4),sF0,sF4(X5,X6,X7,X8,X1,X2,X3,X4),sF0),
inference(step,[status(thm)],[t500,t40]) ).
cnf(t125,plain,
ifeq(output(X1,X2,X3,X4),sF0,sF4(X5,X6,X7,X8,X1,X2,X3,X4),sF0) = sF5(X1,X2,X3,X4,X5,X6,X7,X8),
inference(orient,[status(thm)],[t501]) ).
cnf(f7,negated_conjecture,
output(n0,n1,n0,n1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',input2) ).
fof(f7_nnf,plain,
output(n0,n1,n0,n1),
inference(nnf_transformation,[status(thm)],[f7]) ).
cnf(c7,plain,
output(n0,n1,n0,n1),
inference(cnf_transformation,[status(esa)],[f7_nnf]) ).
cnf(t6,plain,
output(n0,n1,n0,n1) = true,
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(t26,plain,
output(n0,n1,n0,n1) = true,
inference(orient,[status(thm)],[t6]) ).
cnf(t478,plain,
output(n0,n1,n0,n1) = sF0,
inference(step,[status(thm)],[t26,t40]) ).
cnf(t43,plain,
output(n0,n1,n0,n1) = sF0,
inference(orient,[status(thm)],[t478]) ).
cnf(t127,plain,
sF5(n0,n1,n0,n1,X1,X2,X3,X4) = ifeq(sF0,sF0,sF4(X1,X2,X3,X4,n0,n1,n0,n1),sF0),
inference(cp,[status(thm)],[t125,t43]) ).
cnf(t4,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t24,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t4]) ).
cnf(t505,plain,
sF5(n0,n1,n0,n1,X1,X2,X3,X4) = sF4(X1,X2,X3,X4,n0,n1,n0,n1),
inference(step,[status(thm)],[t127,t24]) ).
cnf(t154,plain,
sF5(n0,n1,n0,n1,X1,X2,X3,X4) = sF4(X1,X2,X3,X4,n0,n1,n0,n1),
inference(orient,[status(thm)],[t505]) ).
cnf(f5,negated_conjecture,
( output(nand(X1,Y1),nand(X2,Y2),nand(X3,Y3),nand(X4,Y4))
| ~ output(Y1,Y2,Y3,Y4)
| ~ output(X1,X2,X3,X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',nand_table_definition) ).
fof(f5_nnf,plain,
! [X1,X2,X3,X4,Y1,Y2,Y3,Y4] :
( output(nand(X1,Y1),nand(X2,Y2),nand(X3,Y3),nand(X4,Y4))
| ~ output(Y1,Y2,Y3,Y4)
| ~ output(X1,X2,X3,X4) ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [X1,X2,X3,X4,Y1,Y2,Y3,Y4] :
( output(nand(X1,Y1),nand(X2,Y2),nand(X3,Y3),nand(X4,Y4))
| ~ output(Y1,Y2,Y3,Y4)
| ~ output(X1,X2,X3,X4) ),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
( output(nand(X0,X4),nand(X1,X5),nand(X2,X6),nand(X3,X7))
| ~ output(X4,X5,X6,X7)
| ~ output(X0,X1,X2,X3) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(u0,axiom,
ifeq(output(X0,X1,X2,X3),true,ifeq(output(X4,X5,X6,X7),true,output(nand(X0,X4),nand(X1,X5),nand(X2,X6),nand(X3,X7)),true),true) = true,
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(f0,axiom,
nand(X,Y) = not(and(X,Y)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',nand_definition) ).
fof(f0_nnf,plain,
! [X,Y] : nand(X,Y) = not(and(X,Y)),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X,Y] : nand(X,Y) = not(and(X,Y)),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
nand(X0,X1) = not(and(X0,X1)),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(d0,axiom,
nand(X0,X1) = not(and(X0,X1)),
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t7,plain,
ifeq(output(X1,X2,X3,X4),true,ifeq(output(X5,X6,X7,X8),true,output(not(and(X1,X5)),not(and(X2,X6)),not(and(X3,X7)),not(and(X4,X8))),true),true) = true,
inference(definition_unfolding,[status(thm)],[u0,d0]) ).
cnf(t471,plain,
ifeq(output(X1,X2,X3,X4),true,ifeq(output(X5,X6,X7,X8),true,output(sF2(X1,X5),not(and(X2,X6)),not(and(X3,X7)),not(and(X4,X8))),true),true) = true,
inference(step,[status(thm)],[t7,t19]) ).
cnf(t472,plain,
ifeq(output(X1,X2,X3,X4),true,ifeq(output(X5,X6,X7,X8),true,output(sF2(X1,X5),sF2(X2,X6),not(and(X3,X7)),not(and(X4,X8))),true),true) = true,
inference(step,[status(thm)],[t471,t19]) ).
cnf(t473,plain,
ifeq(output(X1,X2,X3,X4),true,ifeq(output(X5,X6,X7,X8),true,output(sF2(X1,X5),sF2(X2,X6),sF2(X3,X7),not(and(X4,X8))),true),true) = true,
inference(step,[status(thm)],[t472,t19]) ).
cnf(t474,plain,
ifeq(output(X1,X2,X3,X4),true,ifeq(output(X5,X6,X7,X8),true,output(sF2(X1,X5),sF2(X2,X6),sF2(X3,X7),sF2(X4,X8)),true),true) = true,
inference(step,[status(thm)],[t473,t19]) ).
cnf(t27,plain,
ifeq(output(X1,X2,X3,X4),true,ifeq(output(X5,X6,X7,X8),true,output(sF2(X1,X5),sF2(X2,X6),sF2(X3,X7),sF2(X4,X8)),true),true) = true,
inference(orient,[status(thm)],[t474]) ).
cnf(t45,plain,
ifeq(output(X1,X2,X3,X4),sF0,ifeq(output(X5,X6,X7,X8),sF0,output(sF2(X1,X5),sF2(X2,X6),sF2(X3,X7),sF2(X4,X8)),sF0),sF0) = true,
inference(rw,[status(thm)],[t27]) ).
cnf(t506,plain,
ifeq(output(X1,X2,X3,X4),sF0,ifeq(output(X5,X6,X7,X8),sF0,sF3(X1,X5,X2,X6,X3,X7,X4,X8),sF0),sF0) = true,
inference(step,[status(thm)],[t45,t48]) ).
cnf(t507,plain,
ifeq(output(X1,X2,X3,X4),sF0,sF4(X5,X6,X7,X8,X1,X2,X3,X4),sF0) = true,
inference(step,[status(thm)],[t506,t93]) ).
cnf(t508,plain,
sF5(X1,X2,X3,X4,X5,X6,X7,X8) = true,
inference(step,[status(thm)],[t507,t125]) ).
cnf(t509,plain,
sF5(X1,X2,X3,X4,X5,X6,X7,X8) = sF0,
inference(step,[status(thm)],[t508,t40]) ).
cnf(t155,plain,
sF5(X1,X2,X3,X4,X5,X6,X7,X8) = sF0,
inference(orient,[status(thm)],[t509]) ).
cnf(t513,plain,
sF0 = sF4(X1,X2,X3,X4,n0,n1,n0,n1),
inference(step,[status(thm)],[t154,t155]) ).
cnf(t159,plain,
sF0 = sF4(X1,X2,X3,X4,n0,n1,n0,n1),
inference(rw,[status(thm)],[t513]) ).
cnf(t163,plain,
sF4(X1,X2,X3,X4,n0,n1,n0,n1) = sF0,
inference(orient,[status(thm)],[t159]) ).
cnf(t95,plain,
sF4(n0,n1,n0,n1,X1,X2,X3,X4) = ifeq(sF0,sF0,sF3(X1,n0,X2,n1,X3,n0,X4,n1),sF0),
inference(cp,[status(thm)],[t93,t43]) ).
cnf(t503,plain,
sF4(n0,n1,n0,n1,X1,X2,X3,X4) = sF3(X1,n0,X2,n1,X3,n0,X4,n1),
inference(step,[status(thm)],[t95,t24]) ).
cnf(t141,plain,
sF4(n0,n1,n0,n1,X1,X2,X3,X4) = sF3(X1,n0,X2,n1,X3,n0,X4,n1),
inference(orient,[status(thm)],[t503]) ).
cnf(t165,plain,
sF0 = sF3(n0,n0,n1,n1,n0,n0,n1,n1),
inference(cp,[status(thm)],[t163,t141]) ).
cnf(t169,plain,
sF3(n0,n0,n1,n1,n0,n0,n1,n1) = sF0,
inference(orient,[status(thm)],[t165]) ).
cnf(f1,axiom,
and(X,n0) = n0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_definition1) ).
fof(f1_nnf,plain,
! [X] : and(X,n0) = n0,
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [X] : and(X,n0) = n0,
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
and(X0,n0) = n0,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(t2,plain,
and(X1,n0) = n0,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t17,plain,
and(X1,n0) = n0,
inference(orient,[status(thm)],[t2]) ).
cnf(t20,plain,
sF2(X1,n0) = not(n0),
inference(cp,[status(thm)],[t19,t17]) ).
cnf(f3,axiom,
not(n0) = n1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_definition1) ).
fof(f3_nnf,plain,
not(n0) = n1,
inference(nnf_transformation,[status(thm)],[f3]) ).
cnf(c3,plain,
not(n0) = n1,
inference(cnf_transformation,[status(esa)],[f3_nnf]) ).
cnf(t0,plain,
not(n0) = n1,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t15,plain,
not(n0) = n1,
inference(orient,[status(thm)],[t0]) ).
cnf(t470,plain,
sF2(X1,n0) = n1,
inference(step,[status(thm)],[t20,t15]) ).
cnf(t22,plain,
sF2(X1,n0) = n1,
inference(orient,[status(thm)],[t470]) ).
cnf(t49,plain,
sF3(X1,n0,X2,X3,X4,X5,X6,X7) = output(n1,sF2(X2,X3),sF2(X4,X5),sF2(X6,X7)),
inference(cp,[status(thm)],[t48,t22]) ).
cnf(f2,axiom,
and(X,n1) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_definition2) ).
fof(f2_nnf,plain,
! [X] : and(X,n1) = X,
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [X] : and(X,n1) = X,
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
and(X0,n1) = X0,
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(t3,plain,
and(X1,n1) = X1,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t18,plain,
and(X1,n1) = X1,
inference(orient,[status(thm)],[t3]) ).
cnf(t21,plain,
sF2(X1,n1) = not(X1),
inference(cp,[status(thm)],[t19,t18]) ).
cnf(t23,plain,
sF2(X1,n1) = not(X1),
inference(orient,[status(thm)],[t21]) ).
cnf(t53,plain,
sF3(X1,n1,X2,X3,X4,X5,X6,X7) = output(not(X1),sF2(X2,X3),sF2(X4,X5),sF2(X6,X7)),
inference(cp,[status(thm)],[t48,t23]) ).
cnf(t57,plain,
output(not(X1),sF2(X2,X3),sF2(X4,X5),sF2(X6,X7)) = sF3(X1,n1,X2,X3,X4,X5,X6,X7),
inference(orient,[status(thm)],[t53]) ).
cnf(t58,plain,
sF3(n0,n1,X1,X2,X3,X4,X5,X6) = output(n1,sF2(X1,X2),sF2(X3,X4),sF2(X5,X6)),
inference(cp,[status(thm)],[t57,t15]) ).
cnf(t67,plain,
output(n1,sF2(X1,X2),sF2(X3,X4),sF2(X5,X6)) = sF3(n0,n1,X1,X2,X3,X4,X5,X6),
inference(orient,[status(thm)],[t58]) ).
cnf(t514,plain,
sF3(X1,n0,X2,X3,X4,X5,X6,X7) = sF3(n0,n1,X2,X3,X4,X5,X6,X7),
inference(step,[status(thm)],[t49,t67]) ).
cnf(t193,plain,
sF3(X1,n0,X2,X3,X4,X5,X6,X7) = sF3(n0,n1,X2,X3,X4,X5,X6,X7),
inference(orient,[status(thm)],[t514]) ).
cnf(t540,plain,
sF3(n0,n1,n1,n1,n0,n0,n1,n1) = sF0,
inference(step,[status(thm)],[t169,t193]) ).
cnf(t541,plain,
sF3(f1,n0,n1,n1,n0,n0,n1,n1) = sF0,
inference(step,[status(thm)],[t540,t193]) ).
cnf(t220,plain,
sF3(f1,n0,n1,n1,n0,n0,n1,n1) = sF0,
inference(rw,[status(thm)],[t541]) ).
cnf(t71,plain,
sF3(n0,n1,X1,n1,X2,X3,X4,X5) = output(n1,not(X1),sF2(X2,X3),sF2(X4,X5)),
inference(cp,[status(thm)],[t67,t23]) ).
cnf(t74,plain,
output(n1,not(X1),sF2(X2,X3),sF2(X4,X5)) = sF3(n0,n1,X1,n1,X2,X3,X4,X5),
inference(orient,[status(thm)],[t71]) ).
cnf(t78,plain,
sF3(n0,n1,X1,n1,X2,n0,X3,X4) = output(n1,not(X1),n1,sF2(X3,X4)),
inference(cp,[status(thm)],[t74,t22]) ).
cnf(t92,plain,
sF3(n0,n1,X1,n1,X2,n0,X3,X4) = output(n1,not(X1),n1,sF2(X3,X4)),
inference(orient,[status(thm)],[t78]) ).
cnf(t523,plain,
sF3(f1,n0,X1,n1,X2,n0,X3,X4) = output(n1,not(X1),n1,sF2(X3,X4)),
inference(step,[status(thm)],[t92,t193]) ).
cnf(t202,plain,
sF3(f1,n0,X1,n1,X2,n0,X3,X4) = output(n1,not(X1),n1,sF2(X3,X4)),
inference(rw,[status(thm)],[t523]) ).
cnf(t254,plain,
sF3(f1,n0,X1,n1,X2,n0,X3,X4) = output(n1,not(X1),n1,sF2(X3,X4)),
inference(orient,[status(thm)],[t202]) ).
cnf(t562,plain,
output(n1,not(n1),n1,sF2(n1,n1)) = sF0,
inference(step,[status(thm)],[t220,t254]) ).
cnf(f4,axiom,
not(n1) = n0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_definition2) ).
fof(f4_nnf,plain,
not(n1) = n0,
inference(nnf_transformation,[status(thm)],[f4]) ).
cnf(c4,plain,
not(n1) = n0,
inference(cnf_transformation,[status(esa)],[f4_nnf]) ).
cnf(t1,plain,
not(n1) = n0,
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t16,plain,
not(n1) = n0,
inference(orient,[status(thm)],[t1]) ).
cnf(t563,plain,
output(n1,n0,n1,sF2(n1,n1)) = sF0,
inference(step,[status(thm)],[t562,t16]) ).
cnf(t564,plain,
output(n1,n0,n1,not(n1)) = sF0,
inference(step,[status(thm)],[t563,t23]) ).
cnf(t565,plain,
output(n1,n0,n1,n0) = sF0,
inference(step,[status(thm)],[t564,t16]) ).
cnf(t301,plain,
output(n1,n0,n1,n0) = sF0,
inference(orient,[status(thm)],[t565]) ).
cnf(t302,plain,
sF4(n1,n0,n1,n0,X1,X2,X3,X4) = ifeq(sF0,sF0,sF3(X1,n1,X2,n0,X3,n1,X4,n0),sF0),
inference(cp,[status(thm)],[t93,t301]) ).
cnf(t582,plain,
sF4(n1,n0,n1,n0,X1,X2,X3,X4) = sF3(X1,n1,X2,n0,X3,n1,X4,n0),
inference(step,[status(thm)],[t302,t24]) ).
cnf(t367,plain,
sF4(n1,n0,n1,n0,X1,X2,X3,X4) = sF3(X1,n1,X2,n0,X3,n1,X4,n0),
inference(orient,[status(thm)],[t582]) ).
cnf(t510,plain,
ifeq(output(X1,X2,X3,X4),sF0,sF4(X5,X6,X7,X8,X1,X2,X3,X4),sF0) = sF0,
inference(step,[status(thm)],[t125,t155]) ).
cnf(t156,plain,
ifeq(output(X1,X2,X3,X4),sF0,sF4(X5,X6,X7,X8,X1,X2,X3,X4),sF0) = sF0,
inference(orient,[status(thm)],[t510]) ).
cnf(t476,plain,
output(n0,n0,n1,n1) = sF0,
inference(step,[status(thm)],[t25,t40]) ).
cnf(t41,plain,
output(n0,n0,n1,n1) = sF0,
inference(orient,[status(thm)],[t476]) ).
cnf(t126,plain,
sF5(n0,n0,n1,n1,X1,X2,X3,X4) = ifeq(sF0,sF0,sF4(X1,X2,X3,X4,n0,n0,n1,n1),sF0),
inference(cp,[status(thm)],[t125,t41]) ).
cnf(t504,plain,
sF5(n0,n0,n1,n1,X1,X2,X3,X4) = sF4(X1,X2,X3,X4,n0,n0,n1,n1),
inference(step,[status(thm)],[t126,t24]) ).
cnf(t153,plain,
sF5(n0,n0,n1,n1,X1,X2,X3,X4) = sF4(X1,X2,X3,X4,n0,n0,n1,n1),
inference(orient,[status(thm)],[t504]) ).
cnf(t512,plain,
sF0 = sF4(X1,X2,X3,X4,n0,n0,n1,n1),
inference(step,[status(thm)],[t153,t155]) ).
cnf(t158,plain,
sF0 = sF4(X1,X2,X3,X4,n0,n0,n1,n1),
inference(rw,[status(thm)],[t512]) ).
cnf(t160,plain,
sF4(X1,X2,X3,X4,n0,n0,n1,n1) = sF0,
inference(orient,[status(thm)],[t158]) ).
cnf(t94,plain,
sF4(n0,n0,n1,n1,X1,X2,X3,X4) = ifeq(sF0,sF0,sF3(X1,n0,X2,n0,X3,n1,X4,n1),sF0),
inference(cp,[status(thm)],[t93,t41]) ).
cnf(t502,plain,
sF4(n0,n0,n1,n1,X1,X2,X3,X4) = sF3(X1,n0,X2,n0,X3,n1,X4,n1),
inference(step,[status(thm)],[t94,t24]) ).
cnf(t139,plain,
sF4(n0,n0,n1,n1,X1,X2,X3,X4) = sF3(X1,n0,X2,n0,X3,n1,X4,n1),
inference(orient,[status(thm)],[t502]) ).
cnf(t161,plain,
sF0 = sF3(n0,n0,n0,n0,n1,n1,n1,n1),
inference(cp,[status(thm)],[t160,t139]) ).
cnf(t166,plain,
sF3(n0,n0,n0,n0,n1,n1,n1,n1) = sF0,
inference(orient,[status(thm)],[t161]) ).
cnf(t217,plain,
sF3(f1,n0,n0,n0,n1,n1,n1,n1) = sF0,
inference(rw,[status(thm)],[t166]) ).
cnf(t72,plain,
sF3(n0,n1,X1,X2,X3,n1,X4,X5) = output(n1,sF2(X1,X2),not(X3),sF2(X4,X5)),
inference(cp,[status(thm)],[t67,t23]) ).
cnf(t170,plain,
output(n1,sF2(X1,X2),not(X3),sF2(X4,X5)) = sF3(n0,n1,X1,X2,X3,n1,X4,X5),
inference(orient,[status(thm)],[t72]) ).
cnf(t172,plain,
sF3(n0,n1,X1,X2,n1,n1,X3,X4) = output(n1,sF2(X1,X2),n0,sF2(X3,X4)),
inference(cp,[status(thm)],[t170,t16]) ).
cnf(t185,plain,
output(n1,sF2(X1,X2),n0,sF2(X3,X4)) = sF3(n0,n1,X1,X2,n1,n1,X3,X4),
inference(orient,[status(thm)],[t172]) ).
cnf(t186,plain,
sF3(n0,n1,X1,n0,n1,n1,X2,X3) = output(n1,n1,n0,sF2(X2,X3)),
inference(cp,[status(thm)],[t185,t22]) ).
cnf(t553,plain,
sF3(f1,n0,X1,n0,n1,n1,X2,X3) = output(n1,n1,n0,sF2(X2,X3)),
inference(step,[status(thm)],[t186,t193]) ).
cnf(t248,plain,
sF3(f1,n0,X1,n0,n1,n1,X2,X3) = output(n1,n1,n0,sF2(X2,X3)),
inference(orient,[status(thm)],[t553]) ).
cnf(t555,plain,
output(n1,n1,n0,sF2(n1,n1)) = sF0,
inference(step,[status(thm)],[t217,t248]) ).
cnf(t556,plain,
output(n1,n1,n0,not(n1)) = sF0,
inference(step,[status(thm)],[t555,t23]) ).
cnf(t557,plain,
output(n1,n1,n0,n0) = sF0,
inference(step,[status(thm)],[t556,t16]) ).
cnf(t292,plain,
output(n1,n1,n0,n0) = sF0,
inference(orient,[status(thm)],[t557]) ).
cnf(t294,plain,
sF0 = ifeq(sF0,sF0,sF4(X1,X2,X3,X4,n1,n1,n0,n0),sF0),
inference(cp,[status(thm)],[t156,t292]) ).
cnf(t573,plain,
sF0 = sF4(X1,X2,X3,X4,n1,n1,n0,n0),
inference(step,[status(thm)],[t294,t24]) ).
cnf(t343,plain,
sF4(X1,X2,X3,X4,n1,n1,n0,n0) = sF0,
inference(orient,[status(thm)],[t573]) ).
cnf(t370,plain,
sF3(n1,n1,n1,n0,n0,n1,n0,n0) = sF0,
inference(cp,[status(thm)],[t367,t343]) ).
cnf(t465,plain,
sF3(n1,n1,n1,n0,n0,n1,n0,n0) = sF0,
inference(orient,[status(thm)],[t370]) ).
cnf(t50,plain,
sF3(X1,X2,X3,n0,X4,X5,X6,X7) = output(sF2(X1,X2),n1,sF2(X4,X5),sF2(X6,X7)),
inference(cp,[status(thm)],[t48,t22]) ).
cnf(t260,plain,
sF3(X1,X2,X3,n0,X4,X5,X6,X7) = output(sF2(X1,X2),n1,sF2(X4,X5),sF2(X6,X7)),
inference(orient,[status(thm)],[t50]) ).
cnf(t466,plain,
sF0 = output(sF2(n1,n1),n1,sF2(n0,n1),sF2(n0,n0)),
inference(cp,[status(thm)],[t465,t260]) ).
cnf(t611,plain,
sF0 = output(not(n1),n1,sF2(n0,n1),sF2(n0,n0)),
inference(step,[status(thm)],[t466,t23]) ).
cnf(t612,plain,
sF0 = output(n0,n1,sF2(n0,n1),sF2(n0,n0)),
inference(step,[status(thm)],[t611,t16]) ).
cnf(t613,plain,
sF0 = output(n0,n1,not(n0),sF2(n0,n0)),
inference(step,[status(thm)],[t612,t23]) ).
cnf(t614,plain,
sF0 = output(n0,n1,n1,sF2(n0,n0)),
inference(step,[status(thm)],[t613,t15]) ).
cnf(t615,plain,
sF0 = output(n0,n1,n1,n1),
inference(step,[status(thm)],[t614,t22]) ).
cnf(t616,plain,
sF0 = sF6,
inference(step,[status(thm)],[t615,t47]) ).
cnf(t467,plain,
sF6 = sF0,
inference(orient,[status(thm)],[t616]) ).
cnf(t617,plain,
output(n0,n1,n1,n1) = sF0,
inference(step,[status(thm)],[t47,t467]) ).
cnf(t468,plain,
output(n0,n1,n1,n1) = sF0,
inference(orient,[status(thm)],[t617]) ).
cnf(f8,negated_conjecture,
~ output(n0,n1,n1,n1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_cannot_make_or) ).
fof(f8_nnf,plain,
~ output(n0,n1,n1,n1),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
~ output(n0,n1,n1,n1),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
~ output(n0,n1,n1,n1),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(goal_0,negated_conjecture,
output(n0,n1,n1,n1) != true,
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(g0_0,plain,
sF0 != true,
inference(rw,[status(thm)],[goal_0,t468]) ).
cnf(g0_1,plain,
sF0 != sF0,
inference(rw,[status(thm)],[g0_0,t40]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : HWC001-1 : TPTP v9.3.1. Bugfixed v1.1.1.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.08/0.34 % Computer : n011.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/15.42 % CPULimit : 300
% 0.07/15.42 % WCLimit : 300
% 0.07/15.42 % DateTime : Wed Sep 23 16:18:59 UTC 2026
% 0.07/15.42 % CPUTime :
% 0.07/15.42 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 4.53/16.17 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.53/16.17 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------