%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : HWV018-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n002.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:56 PM UTC 2026
% Result : Unsatisfiable 8.83s 1.66s
% Output : Proof 8.83s
% Verified :
% Comments :
%------------------------------------------------------------------------------
cnf(t115,axiom,
sF0 = p_Full(t_139),
introduced(definition) ).
cnf(f92,negated_conjecture,
p_Full(t_139),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quest_3) ).
fof(f92_nnf,plain,
p_Full(t_139),
inference(nnf_transformation,[status(thm)],[f92]) ).
cnf(c92,plain,
p_Full(t_139),
inference(cnf_transformation,[status(esa)],[f92_nnf]) ).
cnf(t2,plain,
p_Full(t_139) = true,
inference(equality_encoding,[status(esa)],[c92]) ).
cnf(t131,plain,
p_Full(t_139) = true,
inference(orient,[status(thm)],[t2]) ).
cnf(t1630,plain,
sF0 = true,
inference(step,[status(thm)],[t115,t131]) ).
cnf(t135,plain,
true = sF0,
inference(orient,[status(thm)],[t1630]) ).
cnf(t116,axiom,
sF1 = p_Rd(t_139),
introduced(definition) ).
cnf(f90,negated_conjecture,
~ p_Rd(t_139),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quest_1) ).
fof(f90_nnf,plain,
~ p_Rd(t_139),
inference(nnf_transformation,[status(thm)],[f90]) ).
fof(f90_sk,plain,
~ p_Rd(t_139),
inference(skolemisation,[status(esa)],[f90_nnf]) ).
cnf(c90,plain,
~ p_Rd(t_139),
inference(cnf_transformation,[status(esa)],[f90_sk]) ).
cnf(t3,plain,
p_Rd(t_139) = false,
inference(equality_encoding,[status(esa)],[c90]) ).
cnf(t132,plain,
p_Rd(t_139) = false,
inference(orient,[status(thm)],[t3]) ).
cnf(t1638,plain,
sF1 = false,
inference(step,[status(thm)],[t116,t132]) ).
cnf(t143,plain,
false = sF1,
inference(orient,[status(thm)],[t1638]) ).
cnf(f21,axiom,
( p_Full(X_t_33)
| int_level(X_t_33) != fifo_length ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_22) ).
fof(f21_nnf,plain,
! [X_t_33] :
( p_Full(X_t_33)
| int_level(X_t_33) != fifo_length ),
inference(nnf_transformation,[status(thm)],[f21]) ).
fof(f21_sk,plain,
! [X_t_33] :
( p_Full(X_t_33)
| int_level(X_t_33) != fifo_length ),
inference(skolemisation,[status(esa)],[f21_nnf]) ).
cnf(c21,plain,
( p_Full(X0)
| int_level(X0) != fifo_length ),
inference(cnf_transformation,[status(esa)],[f21_sk]) ).
cnf(t22,plain,
ifeq(int_level(X1),fifo_length,p_Full(X1),true) = true,
inference(equality_encoding,[status(esa)],[c21]) ).
cnf(t1682,plain,
ifeq(int_level(X1),fifo_length,p_Full(X1),sF0) = true,
inference(step,[status(thm)],[t22,t135]) ).
cnf(t1683,plain,
ifeq(int_level(X1),fifo_length,p_Full(X1),sF0) = sF0,
inference(step,[status(thm)],[t1682,t135]) ).
cnf(t192,plain,
ifeq(int_level(X1),fifo_length,p_Full(X1),sF0) = sF0,
inference(orient,[status(thm)],[t1683]) ).
cnf(t20,plain,
ifeq(eq(X1,X2),true,X1,X2) = X2,
introduced(definition) ).
cnf(t1681,plain,
ifeq(eq(X1,X2),sF0,X1,X2) = X2,
inference(step,[status(thm)],[t20,t135]) ).
cnf(t186,plain,
ifeq(eq(X1,X2),sF0,X1,X2) = X2,
inference(orient,[status(thm)],[t1681]) ).
cnf(f43,axiom,
( int_level(plus(X_t_42,n1)) = int_level(X_t_42)
| gt(fifo_length,int_level(X_t_42))
| p_Rd(X_t_42)
| ~ p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_44) ).
fof(f43_nnf,plain,
! [X_t_42] :
( int_level(plus(X_t_42,n1)) = int_level(X_t_42)
| gt(fifo_length,int_level(X_t_42))
| p_Rd(X_t_42)
| ~ p_Wr(X_t_42)
| p_Reset(X_t_42) ),
inference(nnf_transformation,[status(thm)],[f43]) ).
fof(f43_sk,plain,
! [X_t_42] :
( int_level(plus(X_t_42,n1)) = int_level(X_t_42)
| gt(fifo_length,int_level(X_t_42))
| p_Rd(X_t_42)
| ~ p_Wr(X_t_42)
| p_Reset(X_t_42) ),
inference(skolemisation,[status(esa)],[f43_nnf]) ).
cnf(c43,plain,
( int_level(plus(X0,n1)) = int_level(X0)
| gt(fifo_length,int_level(X0))
| p_Rd(X0)
| ~ p_Wr(X0)
| p_Reset(X0) ),
inference(cnf_transformation,[status(esa)],[f43_sk]) ).
cnf(t79,plain,
ifeq(p_Wr(X1),true,or(p_Reset(X1),or(p_Rd(X1),or(gt(fifo_length,int_level(X1)),eq(int_level(plus(X1,n1)),int_level(X1))))),true) = true,
inference(equality_encoding,[status(esa)],[c43]) ).
cnf(t2172,plain,
ifeq(p_Wr(X1),sF0,or(p_Reset(X1),or(p_Rd(X1),or(gt(fifo_length,int_level(X1)),eq(int_level(plus(X1,n1)),int_level(X1))))),true) = true,
inference(step,[status(thm)],[t79,t135]) ).
cnf(t2173,plain,
ifeq(p_Wr(X1),sF0,or(p_Reset(X1),or(p_Rd(X1),or(gt(fifo_length,int_level(X1)),eq(int_level(plus(X1,n1)),int_level(X1))))),sF0) = true,
inference(step,[status(thm)],[t2172,t135]) ).
cnf(t2174,plain,
ifeq(p_Wr(X1),sF0,or(p_Reset(X1),or(p_Rd(X1),or(gt(fifo_length,int_level(X1)),eq(int_level(plus(X1,n1)),int_level(X1))))),sF0) = sF0,
inference(step,[status(thm)],[t2173,t135]) ).
cnf(t1485,plain,
ifeq(p_Wr(X1),sF0,or(p_Reset(X1),or(p_Rd(X1),or(gt(fifo_length,int_level(X1)),eq(int_level(plus(X1,n1)),int_level(X1))))),sF0) = sF0,
inference(orient,[status(thm)],[t2174]) ).
cnf(t1640,plain,
p_Rd(t_139) = sF1,
inference(step,[status(thm)],[t132,t143]) ).
cnf(t145,plain,
p_Rd(t_139) = sF1,
inference(orient,[status(thm)],[t1640]) ).
cnf(t1486,plain,
sF0 = ifeq(p_Wr(t_139),sF0,or(p_Reset(t_139),or(sF1,or(gt(fifo_length,int_level(t_139)),eq(int_level(plus(t_139,n1)),int_level(t_139))))),sF0),
inference(cp,[status(thm)],[t1485,t145]) ).
cnf(f91,negated_conjecture,
p_Wr(t_139),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quest_2) ).
fof(f91_nnf,plain,
p_Wr(t_139),
inference(nnf_transformation,[status(thm)],[f91]) ).
cnf(c91,plain,
p_Wr(t_139),
inference(cnf_transformation,[status(esa)],[f91_nnf]) ).
cnf(t5,plain,
p_Wr(t_139) = true,
inference(equality_encoding,[status(esa)],[c91]) ).
cnf(t134,plain,
p_Wr(t_139) = true,
inference(orient,[status(thm)],[t5]) ).
cnf(t1636,plain,
p_Wr(t_139) = sF0,
inference(step,[status(thm)],[t134,t135]) ).
cnf(t141,plain,
p_Wr(t_139) = sF0,
inference(orient,[status(thm)],[t1636]) ).
cnf(t2175,plain,
sF0 = ifeq(sF0,sF0,or(p_Reset(t_139),or(sF1,or(gt(fifo_length,int_level(t_139)),eq(int_level(plus(t_139,n1)),int_level(t_139))))),sF0),
inference(step,[status(thm)],[t1486,t141]) ).
cnf(t16,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t173,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t16]) ).
cnf(t2176,plain,
sF0 = or(p_Reset(t_139),or(sF1,or(gt(fifo_length,int_level(t_139)),eq(int_level(plus(t_139,n1)),int_level(t_139))))),
inference(step,[status(thm)],[t2175,t173]) ).
cnf(f93,negated_conjecture,
~ p_Reset(t_139),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quest_4) ).
fof(f93_nnf,plain,
~ p_Reset(t_139),
inference(nnf_transformation,[status(thm)],[f93]) ).
fof(f93_sk,plain,
~ p_Reset(t_139),
inference(skolemisation,[status(esa)],[f93_nnf]) ).
cnf(c93,plain,
~ p_Reset(t_139),
inference(cnf_transformation,[status(esa)],[f93_sk]) ).
cnf(t4,plain,
p_Reset(t_139) = false,
inference(equality_encoding,[status(esa)],[c93]) ).
cnf(t133,plain,
p_Reset(t_139) = false,
inference(orient,[status(thm)],[t4]) ).
cnf(t1642,plain,
p_Reset(t_139) = sF1,
inference(step,[status(thm)],[t133,t143]) ).
cnf(t147,plain,
p_Reset(t_139) = sF1,
inference(orient,[status(thm)],[t1642]) ).
cnf(t2177,plain,
sF0 = or(sF1,or(sF1,or(gt(fifo_length,int_level(t_139)),eq(int_level(plus(t_139,n1)),int_level(t_139))))),
inference(step,[status(thm)],[t2176,t147]) ).
cnf(t10,plain,
or(false,X1) = X1,
introduced(definition) ).
cnf(t1652,plain,
or(sF1,X1) = X1,
inference(step,[status(thm)],[t10,t143]) ).
cnf(t157,plain,
or(sF1,X1) = X1,
inference(orient,[status(thm)],[t1652]) ).
cnf(t2178,plain,
sF0 = or(sF1,or(gt(fifo_length,int_level(t_139)),eq(int_level(plus(t_139,n1)),int_level(t_139)))),
inference(step,[status(thm)],[t2177,t157]) ).
cnf(t2179,plain,
sF0 = or(gt(fifo_length,int_level(t_139)),eq(int_level(plus(t_139,n1)),int_level(t_139))),
inference(step,[status(thm)],[t2178,t157]) ).
cnf(f22,axiom,
( ~ p_Full(X_t_34)
| int_level(X_t_34) = fifo_length ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_23) ).
fof(f22_nnf,plain,
! [X_t_34] :
( ~ p_Full(X_t_34)
| int_level(X_t_34) = fifo_length ),
inference(nnf_transformation,[status(thm)],[f22]) ).
fof(f22_sk,plain,
! [X_t_34] :
( ~ p_Full(X_t_34)
| int_level(X_t_34) = fifo_length ),
inference(skolemisation,[status(esa)],[f22_nnf]) ).
cnf(c22,plain,
( ~ p_Full(X0)
| int_level(X0) = fifo_length ),
inference(cnf_transformation,[status(esa)],[f22_sk]) ).
cnf(t25,plain,
ifeq(p_Full(X1),true,int_level(X1),fifo_length) = fifo_length,
inference(equality_encoding,[status(esa)],[c22]) ).
cnf(t1687,plain,
ifeq(p_Full(X1),sF0,int_level(X1),fifo_length) = fifo_length,
inference(step,[status(thm)],[t25,t135]) ).
cnf(t199,plain,
ifeq(p_Full(X1),sF0,int_level(X1),fifo_length) = fifo_length,
inference(orient,[status(thm)],[t1687]) ).
cnf(t1634,plain,
p_Full(t_139) = sF0,
inference(step,[status(thm)],[t131,t135]) ).
cnf(t139,plain,
p_Full(t_139) = sF0,
inference(orient,[status(thm)],[t1634]) ).
cnf(t200,plain,
fifo_length = ifeq(sF0,sF0,int_level(t_139),fifo_length),
inference(cp,[status(thm)],[t199,t139]) ).
cnf(t1688,plain,
fifo_length = int_level(t_139),
inference(step,[status(thm)],[t200,t173]) ).
cnf(t202,plain,
int_level(t_139) = fifo_length,
inference(orient,[status(thm)],[t1688]) ).
cnf(t2180,plain,
sF0 = or(gt(fifo_length,fifo_length),eq(int_level(plus(t_139,n1)),int_level(t_139))),
inference(step,[status(thm)],[t2179,t202]) ).
cnf(f16,axiom,
~ gt(X_28,X_28),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_17) ).
fof(f16_nnf,plain,
! [X_28] : ~ gt(X_28,X_28),
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
! [X_28] : ~ gt(X_28,X_28),
inference(skolemisation,[status(esa)],[f16_nnf]) ).
cnf(c16,plain,
~ gt(X0,X0),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(t7,plain,
gt(X1,X1) = false,
inference(equality_encoding,[status(esa)],[c16]) ).
cnf(t1648,plain,
gt(X1,X1) = sF1,
inference(step,[status(thm)],[t7,t143]) ).
cnf(t154,plain,
gt(X1,X1) = sF1,
inference(orient,[status(thm)],[t1648]) ).
cnf(t2181,plain,
sF0 = or(sF1,eq(int_level(plus(t_139,n1)),int_level(t_139))),
inference(step,[status(thm)],[t2180,t154]) ).
cnf(t2182,plain,
sF0 = eq(int_level(plus(t_139,n1)),int_level(t_139)),
inference(step,[status(thm)],[t2181,t157]) ).
cnf(t121,axiom,
sF6 = plus(t_139,n1),
introduced(definition) ).
cnf(t160,plain,
plus(t_139,n1) = sF6,
inference(orient,[status(thm)],[t121]) ).
cnf(t2183,plain,
sF0 = eq(int_level(sF6),int_level(t_139)),
inference(step,[status(thm)],[t2182,t160]) ).
cnf(t2184,plain,
sF0 = eq(int_level(sF6),fifo_length),
inference(step,[status(thm)],[t2183,t202]) ).
cnf(t1488,plain,
eq(int_level(sF6),fifo_length) = sF0,
inference(orient,[status(thm)],[t2184]) ).
cnf(t1489,plain,
fifo_length = ifeq(sF0,sF0,int_level(sF6),fifo_length),
inference(cp,[status(thm)],[t186,t1488]) ).
cnf(t2185,plain,
fifo_length = int_level(sF6),
inference(step,[status(thm)],[t1489,t173]) ).
cnf(t1493,plain,
int_level(sF6) = fifo_length,
inference(orient,[status(thm)],[t2185]) ).
cnf(t1499,plain,
sF0 = ifeq(fifo_length,fifo_length,p_Full(sF6),sF0),
inference(cp,[status(thm)],[t192,t1493]) ).
cnf(t2188,plain,
sF0 = p_Full(sF6),
inference(step,[status(thm)],[t1499,t173]) ).
cnf(t122,axiom,
sF7 = p_Full(plus(t_139,n1)),
introduced(definition) ).
cnf(t1656,plain,
sF7 = p_Full(sF6),
inference(step,[status(thm)],[t122,t160]) ).
cnf(t166,plain,
p_Full(sF6) = sF7,
inference(orient,[status(thm)],[t1656]) ).
cnf(t17,plain,
ifeq(not(X1),true,X1,false) = false,
introduced(definition) ).
cnf(t1663,plain,
ifeq(not(X1),sF0,X1,false) = false,
inference(step,[status(thm)],[t17,t135]) ).
cnf(t1664,plain,
ifeq(not(X1),sF0,X1,sF1) = false,
inference(step,[status(thm)],[t1663,t143]) ).
cnf(t1665,plain,
ifeq(not(X1),sF0,X1,sF1) = sF1,
inference(step,[status(thm)],[t1664,t143]) ).
cnf(t176,plain,
ifeq(not(X1),sF0,X1,sF1) = sF1,
inference(orient,[status(thm)],[t1665]) ).
cnf(t123,axiom,
sF8 = not(p_Full(plus(t_139,n1))),
introduced(definition) ).
cnf(t1659,plain,
sF8 = not(p_Full(sF6)),
inference(step,[status(thm)],[t123,t160]) ).
cnf(t1660,plain,
sF8 = not(sF7),
inference(step,[status(thm)],[t1659,t166]) ).
cnf(t174,plain,
not(sF7) = sF8,
inference(orient,[status(thm)],[t1660]) ).
cnf(t178,plain,
sF1 = ifeq(sF8,sF0,sF7,sF1),
inference(cp,[status(thm)],[t176,t174]) ).
cnf(t181,plain,
ifeq(sF8,sF0,sF7,sF1) = sF1,
inference(orient,[status(thm)],[t178]) ).
cnf(t1323,plain,
ifeq(sF0,sF0,sF7,sF1) = sF1,
inference(rw,[status(thm)],[t181]) ).
cnf(t2100,plain,
sF7 = sF1,
inference(step,[status(thm)],[t1323,t173]) ).
cnf(t1327,plain,
sF7 = sF1,
inference(orient,[status(thm)],[t2100]) ).
cnf(t2101,plain,
p_Full(sF6) = sF1,
inference(step,[status(thm)],[t166,t1327]) ).
cnf(t1328,plain,
p_Full(sF6) = sF1,
inference(orient,[status(thm)],[t2101]) ).
cnf(t2189,plain,
sF0 = sF1,
inference(step,[status(thm)],[t2188,t1328]) ).
cnf(t1509,plain,
sF1 = sF0,
inference(orient,[status(thm)],[t2189]) ).
cnf(t2194,plain,
false = sF0,
inference(step,[status(thm)],[t143,t1509]) ).
cnf(t1514,plain,
false = sF0,
inference(orient,[status(thm)],[t2194]) ).
cnf(f0,axiom,
plus(X_0,n1) != n0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_1) ).
fof(f0_nnf,plain,
! [X_0] : plus(X_0,n1) != n0,
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X_0] : plus(X_0,n1) != n0,
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
plus(X0,n1) != n0,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(f5,axiom,
( ~ gt(X_3,Y_4)
| ~ def_10(Y_4,X_3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_6) ).
fof(f5_nnf,plain,
! [Y_4,X_3] :
( ~ gt(X_3,Y_4)
| ~ def_10(Y_4,X_3) ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [Y_4,X_3] :
( ~ gt(X_3,Y_4)
| ~ def_10(Y_4,X_3) ),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
( ~ gt(X1,X0)
| ~ def_10(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(f6,axiom,
( X_3 != Y_4
| ~ def_10(Y_4,X_3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_7) ).
fof(f6_nnf,plain,
! [Y_4,X_3] :
( X_3 != Y_4
| ~ def_10(Y_4,X_3) ),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [Y_4,X_3] :
( X_3 != Y_4
| ~ def_10(Y_4,X_3) ),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
( X1 != X0
| ~ def_10(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(f28,axiom,
( ~ p_Wr_error(plus(X_t_37,n1))
| ~ p_Reset(X_t_37) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_29) ).
fof(f28_nnf,plain,
! [X_t_37] :
( ~ p_Wr_error(plus(X_t_37,n1))
| ~ p_Reset(X_t_37) ),
inference(nnf_transformation,[status(thm)],[f28]) ).
fof(f28_sk,plain,
! [X_t_37] :
( ~ p_Wr_error(plus(X_t_37,n1))
| ~ p_Reset(X_t_37) ),
inference(skolemisation,[status(esa)],[f28_nnf]) ).
cnf(c28,plain,
( ~ p_Wr_error(plus(X0,n1))
| ~ p_Reset(X0) ),
inference(cnf_transformation,[status(esa)],[f28_sk]) ).
cnf(f29,axiom,
( ~ p_Rd_error(plus(X_t_37,n1))
| ~ p_Reset(X_t_37) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_30) ).
fof(f29_nnf,plain,
! [X_t_37] :
( ~ p_Rd_error(plus(X_t_37,n1))
| ~ p_Reset(X_t_37) ),
inference(nnf_transformation,[status(thm)],[f29]) ).
fof(f29_sk,plain,
! [X_t_37] :
( ~ p_Rd_error(plus(X_t_37,n1))
| ~ p_Reset(X_t_37) ),
inference(skolemisation,[status(esa)],[f29_nnf]) ).
cnf(c29,plain,
( ~ p_Rd_error(plus(X0,n1))
| ~ p_Reset(X0) ),
inference(cnf_transformation,[status(esa)],[f29_sk]) ).
cnf(f30,axiom,
( ~ p_Mem(X_k1_38,X_k2_39,plus(X_t_37,n1))
| ~ p_Reset(X_t_37) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_31) ).
fof(f30_nnf,plain,
! [X_t_37,X_k1_38,X_k2_39] :
( ~ p_Mem(X_k1_38,X_k2_39,plus(X_t_37,n1))
| ~ p_Reset(X_t_37) ),
inference(nnf_transformation,[status(thm)],[f30]) ).
fof(f30_sk,plain,
! [X_t_37,X_k1_38,X_k2_39] :
( ~ p_Mem(X_k1_38,X_k2_39,plus(X_t_37,n1))
| ~ p_Reset(X_t_37) ),
inference(skolemisation,[status(esa)],[f30_nnf]) ).
cnf(c30,plain,
( ~ p_Mem(X1,X2,plus(X0,n1))
| ~ p_Reset(X0) ),
inference(cnf_transformation,[status(esa)],[f30_sk]) ).
cnf(f31,axiom,
( ~ p_Data_out(X_k1_40,plus(X_t_37,n1))
| ~ p_Reset(X_t_37) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_32) ).
fof(f31_nnf,plain,
! [X_t_37,X_k1_40] :
( ~ p_Data_out(X_k1_40,plus(X_t_37,n1))
| ~ p_Reset(X_t_37) ),
inference(nnf_transformation,[status(thm)],[f31]) ).
fof(f31_sk,plain,
! [X_t_37,X_k1_40] :
( ~ p_Data_out(X_k1_40,plus(X_t_37,n1))
| ~ p_Reset(X_t_37) ),
inference(skolemisation,[status(esa)],[f31_nnf]) ).
cnf(c31,plain,
( ~ p_Data_out(X1,plus(X0,n1))
| ~ p_Reset(X0) ),
inference(cnf_transformation,[status(esa)],[f31_sk]) ).
cnf(f94,negated_conjecture,
( ~ p_Wr_error(plus(t_139,n1))
| ~ p_Full(plus(t_139,n1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quest_5) ).
fof(f94_nnf,plain,
( ~ p_Wr_error(plus(t_139,n1))
| ~ p_Full(plus(t_139,n1)) ),
inference(nnf_transformation,[status(thm)],[f94]) ).
fof(f94_sk,plain,
( ~ p_Wr_error(plus(t_139,n1))
| ~ p_Full(plus(t_139,n1)) ),
inference(skolemisation,[status(esa)],[f94_nnf]) ).
cnf(c94,plain,
( ~ p_Wr_error(plus(t_139,n1))
| ~ p_Full(plus(t_139,n1)) ),
inference(cnf_transformation,[status(esa)],[f94_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c0,c5,c6,c16,c28,c29,c30,c31,c90,c93,c94]) ).
cnf(g0_0,plain,
sF0 != false,
inference(rw,[status(thm)],[goal_0,t135]) ).
cnf(g0_1,plain,
sF0 != sF0,
inference(rw,[status(thm)],[g0_0,t1514]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV018-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.38 % Computer : n002.cluster.edu
% 0.09/0.38 % Model : x86_64 x86_64
% 0.09/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.38 % Memory : 8046.5625MB
% 0.09/0.38 % OS : Linux 6.8.0-71-generic
% 0.09/0.38 % CPULimit : 300
% 0.09/0.38 % WCLimit : 300
% 0.09/0.38 % DateTime : Wed Sep 23 16:28:07 UTC 2026
% 0.09/0.38 % CPUTime :
% 0.09/0.38 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 8.83/1.66 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.83/1.66 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------