%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : HWV012-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n005.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:47 PM UTC 2026
% Result : Unsatisfiable 7.80s 1.50s
% Output : Proof 7.80s
% Verified :
% Comments :
%------------------------------------------------------------------------------
cnf(t110,axiom,
sF0 = p_Wr(t_139),
introduced(definition) ).
cnf(f91,negated_conjecture,
p_Wr(t_139),
file('/export/starexec/sandbox2/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(t2,plain,
p_Wr(t_139) = true,
inference(equality_encoding,[status(esa)],[c91]) ).
cnf(t117,plain,
p_Wr(t_139) = true,
inference(orient,[status(thm)],[t2]) ).
cnf(t1670,plain,
sF0 = true,
inference(step,[status(thm)],[t110,t117]) ).
cnf(t118,plain,
true = sF0,
inference(orient,[status(thm)],[t1670]) ).
cnf(f50,axiom,
( ~ p_Wr_error(plus(X_t_42,n1))
| ~ p_Rd(X_t_42)
| ~ p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_51) ).
fof(f50_nnf,plain,
! [X_t_42] :
( ~ p_Wr_error(plus(X_t_42,n1))
| ~ p_Rd(X_t_42)
| ~ p_Wr(X_t_42)
| p_Reset(X_t_42) ),
inference(nnf_transformation,[status(thm)],[f50]) ).
fof(f50_sk,plain,
! [X_t_42] :
( ~ p_Wr_error(plus(X_t_42,n1))
| ~ p_Rd(X_t_42)
| ~ p_Wr(X_t_42)
| p_Reset(X_t_42) ),
inference(skolemisation,[status(esa)],[f50_nnf]) ).
cnf(c50,plain,
( ~ p_Wr_error(plus(X0,n1))
| ~ p_Rd(X0)
| ~ p_Wr(X0)
| p_Reset(X0) ),
inference(cnf_transformation,[status(esa)],[f50_sk]) ).
cnf(t62,plain,
ifeq(p_Wr(X1),true,ifeq(p_Rd(X1),true,ifeq(p_Wr_error(plus(X1,n1)),true,p_Reset(X1),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c50]) ).
cnf(t1975,plain,
ifeq(p_Wr(X1),sF0,ifeq(p_Rd(X1),true,ifeq(p_Wr_error(plus(X1,n1)),true,p_Reset(X1),true),true),true) = true,
inference(step,[status(thm)],[t62,t118]) ).
cnf(t1976,plain,
ifeq(p_Wr(X1),sF0,ifeq(p_Rd(X1),sF0,ifeq(p_Wr_error(plus(X1,n1)),true,p_Reset(X1),true),true),true) = true,
inference(step,[status(thm)],[t1975,t118]) ).
cnf(t1977,plain,
ifeq(p_Wr(X1),sF0,ifeq(p_Rd(X1),sF0,ifeq(p_Wr_error(plus(X1,n1)),sF0,p_Reset(X1),true),true),true) = true,
inference(step,[status(thm)],[t1976,t118]) ).
cnf(t1978,plain,
ifeq(p_Wr(X1),sF0,ifeq(p_Rd(X1),sF0,ifeq(p_Wr_error(plus(X1,n1)),sF0,p_Reset(X1),sF0),true),true) = true,
inference(step,[status(thm)],[t1977,t118]) ).
cnf(t1979,plain,
ifeq(p_Wr(X1),sF0,ifeq(p_Rd(X1),sF0,ifeq(p_Wr_error(plus(X1,n1)),sF0,p_Reset(X1),sF0),sF0),true) = true,
inference(step,[status(thm)],[t1978,t118]) ).
cnf(t1980,plain,
ifeq(p_Wr(X1),sF0,ifeq(p_Rd(X1),sF0,ifeq(p_Wr_error(plus(X1,n1)),sF0,p_Reset(X1),sF0),sF0),sF0) = true,
inference(step,[status(thm)],[t1979,t118]) ).
cnf(t1981,plain,
ifeq(p_Wr(X1),sF0,ifeq(p_Rd(X1),sF0,ifeq(p_Wr_error(plus(X1,n1)),sF0,p_Reset(X1),sF0),sF0),sF0) = sF0,
inference(step,[status(thm)],[t1980,t118]) ).
cnf(t1037,plain,
ifeq(p_Wr(X1),sF0,ifeq(p_Rd(X1),sF0,ifeq(p_Wr_error(plus(X1,n1)),sF0,p_Reset(X1),sF0),sF0),sF0) = sF0,
inference(orient,[status(thm)],[t1981]) ).
cnf(f33,axiom,
( ~ p_Wr_error(plus(X_t_42,n1))
| ~ 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/sandbox2/benchmark/theBenchmark.p',axiom_34) ).
fof(f33_nnf,plain,
! [X_t_42] :
( ~ p_Wr_error(plus(X_t_42,n1))
| ~ 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)],[f33]) ).
fof(f33_sk,plain,
! [X_t_42] :
( ~ p_Wr_error(plus(X_t_42,n1))
| ~ 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)],[f33_nnf]) ).
cnf(c33,plain,
( ~ p_Wr_error(plus(X0,n1))
| ~ gt(fifo_length,int_level(X0))
| p_Rd(X0)
| ~ p_Wr(X0)
| p_Reset(X0) ),
inference(cnf_transformation,[status(esa)],[f33_sk]) ).
cnf(t77,plain,
ifeq(p_Wr(X1),true,ifeq(gt(fifo_length,int_level(X1)),true,ifeq(p_Wr_error(plus(X1,n1)),true,or(p_Reset(X1),p_Rd(X1)),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c33]) ).
cnf(t2146,plain,
ifeq(p_Wr(X1),sF0,ifeq(gt(fifo_length,int_level(X1)),true,ifeq(p_Wr_error(plus(X1,n1)),true,or(p_Reset(X1),p_Rd(X1)),true),true),true) = true,
inference(step,[status(thm)],[t77,t118]) ).
cnf(t2147,plain,
ifeq(p_Wr(X1),sF0,ifeq(gt(fifo_length,int_level(X1)),sF0,ifeq(p_Wr_error(plus(X1,n1)),true,or(p_Reset(X1),p_Rd(X1)),true),true),true) = true,
inference(step,[status(thm)],[t2146,t118]) ).
cnf(t2148,plain,
ifeq(p_Wr(X1),sF0,ifeq(gt(fifo_length,int_level(X1)),sF0,ifeq(p_Wr_error(plus(X1,n1)),sF0,or(p_Reset(X1),p_Rd(X1)),true),true),true) = true,
inference(step,[status(thm)],[t2147,t118]) ).
cnf(t2149,plain,
ifeq(p_Wr(X1),sF0,ifeq(gt(fifo_length,int_level(X1)),sF0,ifeq(p_Wr_error(plus(X1,n1)),sF0,or(p_Reset(X1),p_Rd(X1)),sF0),true),true) = true,
inference(step,[status(thm)],[t2148,t118]) ).
cnf(t2150,plain,
ifeq(p_Wr(X1),sF0,ifeq(gt(fifo_length,int_level(X1)),sF0,ifeq(p_Wr_error(plus(X1,n1)),sF0,or(p_Reset(X1),p_Rd(X1)),sF0),sF0),true) = true,
inference(step,[status(thm)],[t2149,t118]) ).
cnf(t2151,plain,
ifeq(p_Wr(X1),sF0,ifeq(gt(fifo_length,int_level(X1)),sF0,ifeq(p_Wr_error(plus(X1,n1)),sF0,or(p_Reset(X1),p_Rd(X1)),sF0),sF0),sF0) = true,
inference(step,[status(thm)],[t2150,t118]) ).
cnf(t2152,plain,
ifeq(p_Wr(X1),sF0,ifeq(gt(fifo_length,int_level(X1)),sF0,ifeq(p_Wr_error(plus(X1,n1)),sF0,or(p_Reset(X1),p_Rd(X1)),sF0),sF0),sF0) = sF0,
inference(step,[status(thm)],[t2151,t118]) ).
cnf(t1542,plain,
ifeq(p_Wr(X1),sF0,ifeq(gt(fifo_length,int_level(X1)),sF0,ifeq(p_Wr_error(plus(X1,n1)),sF0,or(p_Reset(X1),p_Rd(X1)),sF0),sF0),sF0) = sF0,
inference(orient,[status(thm)],[t2152]) ).
cnf(t1674,plain,
p_Wr(t_139) = sF0,
inference(step,[status(thm)],[t117,t118]) ).
cnf(t122,plain,
p_Wr(t_139) = sF0,
inference(orient,[status(thm)],[t1674]) ).
cnf(t1543,plain,
sF0 = ifeq(sF0,sF0,ifeq(gt(fifo_length,int_level(t_139)),sF0,ifeq(p_Wr_error(plus(t_139,n1)),sF0,or(p_Reset(t_139),p_Rd(t_139)),sF0),sF0),sF0),
inference(cp,[status(thm)],[t1542,t122]) ).
cnf(t15,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t148,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t15]) ).
cnf(t2153,plain,
sF0 = ifeq(gt(fifo_length,int_level(t_139)),sF0,ifeq(p_Wr_error(plus(t_139,n1)),sF0,or(p_Reset(t_139),p_Rd(t_139)),sF0),sF0),
inference(step,[status(thm)],[t1543,t148]) ).
cnf(t111,axiom,
sF1 = int_level(t_139),
introduced(definition) ).
cnf(t124,plain,
int_level(t_139) = sF1,
inference(orient,[status(thm)],[t111]) ).
cnf(t2154,plain,
sF0 = ifeq(gt(fifo_length,sF1),sF0,ifeq(p_Wr_error(plus(t_139,n1)),sF0,or(p_Reset(t_139),p_Rd(t_139)),sF0),sF0),
inference(step,[status(thm)],[t2153,t124]) ).
cnf(f90,negated_conjecture,
gt(fifo_length,level(t_139)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',quest_1) ).
fof(f90_nnf,plain,
gt(fifo_length,level(t_139)),
inference(nnf_transformation,[status(thm)],[f90]) ).
cnf(c90,plain,
gt(fifo_length,level(t_139)),
inference(cnf_transformation,[status(esa)],[f90_nnf]) ).
cnf(u0,axiom,
gt(fifo_length,level(t_139)) = true,
inference(equality_encoding,[status(esa)],[c90]) ).
cnf(f20,axiom,
level(X_t_32) = int_level(X_t_32),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_21) ).
fof(f20_nnf,plain,
! [X_t_32] : level(X_t_32) = int_level(X_t_32),
inference(nnf_transformation,[status(thm)],[f20]) ).
fof(f20_sk,plain,
! [X_t_32] : level(X_t_32) = int_level(X_t_32),
inference(skolemisation,[status(esa)],[f20_nnf]) ).
cnf(c20,plain,
level(X0) = int_level(X0),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(d0,axiom,
level(X0) = int_level(X0),
inference(equality_encoding,[status(esa)],[c20]) ).
cnf(t11,plain,
gt(fifo_length,int_level(t_139)) = true,
inference(definition_unfolding,[status(thm)],[u0,d0]) ).
cnf(t1681,plain,
gt(fifo_length,sF1) = true,
inference(step,[status(thm)],[t11,t124]) ).
cnf(t1682,plain,
gt(fifo_length,sF1) = sF0,
inference(step,[status(thm)],[t1681,t118]) ).
cnf(t134,plain,
gt(fifo_length,sF1) = sF0,
inference(orient,[status(thm)],[t1682]) ).
cnf(t2155,plain,
sF0 = ifeq(sF0,sF0,ifeq(p_Wr_error(plus(t_139,n1)),sF0,or(p_Reset(t_139),p_Rd(t_139)),sF0),sF0),
inference(step,[status(thm)],[t2154,t134]) ).
cnf(t2156,plain,
sF0 = ifeq(p_Wr_error(plus(t_139,n1)),sF0,or(p_Reset(t_139),p_Rd(t_139)),sF0),
inference(step,[status(thm)],[t2155,t148]) ).
cnf(t113,axiom,
sF3 = plus(t_139,n1),
introduced(definition) ).
cnf(t133,plain,
plus(t_139,n1) = sF3,
inference(orient,[status(thm)],[t113]) ).
cnf(t2157,plain,
sF0 = ifeq(p_Wr_error(sF3),sF0,or(p_Reset(t_139),p_Rd(t_139)),sF0),
inference(step,[status(thm)],[t2156,t133]) ).
cnf(f92,negated_conjecture,
p_Wr_error(plus(t_139,n1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',quest_3) ).
fof(f92_nnf,plain,
p_Wr_error(plus(t_139,n1)),
inference(nnf_transformation,[status(thm)],[f92]) ).
cnf(c92,plain,
p_Wr_error(plus(t_139,n1)),
inference(cnf_transformation,[status(esa)],[f92_nnf]) ).
cnf(t12,plain,
p_Wr_error(plus(t_139,n1)) = true,
inference(equality_encoding,[status(esa)],[c92]) ).
cnf(t1683,plain,
p_Wr_error(sF3) = true,
inference(step,[status(thm)],[t12,t133]) ).
cnf(t1684,plain,
p_Wr_error(sF3) = sF0,
inference(step,[status(thm)],[t1683,t118]) ).
cnf(t135,plain,
p_Wr_error(sF3) = sF0,
inference(orient,[status(thm)],[t1684]) ).
cnf(t2158,plain,
sF0 = ifeq(sF0,sF0,or(p_Reset(t_139),p_Rd(t_139)),sF0),
inference(step,[status(thm)],[t2157,t135]) ).
cnf(t2159,plain,
sF0 = or(p_Reset(t_139),p_Rd(t_139)),
inference(step,[status(thm)],[t2158,t148]) ).
cnf(t16,plain,
ifeq(not(X1),true,X1,false) = false,
introduced(definition) ).
cnf(t1690,plain,
ifeq(not(X1),sF0,X1,false) = false,
inference(step,[status(thm)],[t16,t118]) ).
cnf(t149,plain,
ifeq(not(X1),sF0,X1,false) = false,
inference(orient,[status(thm)],[t1690]) ).
cnf(f28,axiom,
( ~ p_Wr_error(plus(X_t_37,n1))
| ~ p_Reset(X_t_37) ),
file('/export/starexec/sandbox2/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(t32,plain,
or(not(p_Reset(X1)),not(p_Wr_error(plus(X1,n1)))) = true,
inference(equality_encoding,[status(esa)],[c28]) ).
cnf(t1726,plain,
or(not(p_Reset(X1)),not(p_Wr_error(plus(X1,n1)))) = sF0,
inference(step,[status(thm)],[t32,t118]) ).
cnf(t238,plain,
or(not(p_Reset(X1)),not(p_Wr_error(plus(X1,n1)))) = sF0,
inference(orient,[status(thm)],[t1726]) ).
cnf(t240,plain,
sF0 = or(not(p_Reset(t_139)),not(p_Wr_error(sF3))),
inference(cp,[status(thm)],[t238,t133]) ).
cnf(t1727,plain,
sF0 = or(not(p_Reset(t_139)),not(sF0)),
inference(step,[status(thm)],[t240,t135]) ).
cnf(t1,plain,
not(true) = false,
introduced(definition) ).
cnf(t116,plain,
not(true) = false,
inference(orient,[status(thm)],[t1]) ).
cnf(t1673,plain,
not(sF0) = false,
inference(step,[status(thm)],[t116,t118]) ).
cnf(t121,plain,
not(sF0) = false,
inference(rw,[status(thm)],[t1673]) ).
cnf(t125,plain,
not(sF0) = false,
inference(orient,[status(thm)],[t121]) ).
cnf(t1728,plain,
sF0 = or(not(p_Reset(t_139)),false),
inference(step,[status(thm)],[t1727,t125]) ).
cnf(t5,plain,
or(X1,false) = X1,
introduced(definition) ).
cnf(t128,plain,
or(X1,false) = X1,
inference(orient,[status(thm)],[t5]) ).
cnf(t1729,plain,
sF0 = not(p_Reset(t_139)),
inference(step,[status(thm)],[t1728,t128]) ).
cnf(t241,plain,
not(p_Reset(t_139)) = sF0,
inference(orient,[status(thm)],[t1729]) ).
cnf(t243,plain,
false = ifeq(sF0,sF0,p_Reset(t_139),false),
inference(cp,[status(thm)],[t149,t241]) ).
cnf(t1730,plain,
false = p_Reset(t_139),
inference(step,[status(thm)],[t243,t148]) ).
cnf(t244,plain,
p_Reset(t_139) = false,
inference(orient,[status(thm)],[t1730]) ).
cnf(t2160,plain,
sF0 = or(false,p_Rd(t_139)),
inference(step,[status(thm)],[t2159,t244]) ).
cnf(t7,plain,
or(false,X1) = X1,
introduced(definition) ).
cnf(t130,plain,
or(false,X1) = X1,
inference(orient,[status(thm)],[t7]) ).
cnf(t2161,plain,
sF0 = p_Rd(t_139),
inference(step,[status(thm)],[t2160,t130]) ).
cnf(t1545,plain,
p_Rd(t_139) = sF0,
inference(orient,[status(thm)],[t2161]) ).
cnf(t1552,plain,
sF0 = ifeq(p_Wr(t_139),sF0,ifeq(sF0,sF0,ifeq(p_Wr_error(plus(t_139,n1)),sF0,p_Reset(t_139),sF0),sF0),sF0),
inference(cp,[status(thm)],[t1037,t1545]) ).
cnf(t2162,plain,
sF0 = ifeq(sF0,sF0,ifeq(sF0,sF0,ifeq(p_Wr_error(plus(t_139,n1)),sF0,p_Reset(t_139),sF0),sF0),sF0),
inference(step,[status(thm)],[t1552,t122]) ).
cnf(t2163,plain,
sF0 = ifeq(sF0,sF0,ifeq(p_Wr_error(plus(t_139,n1)),sF0,p_Reset(t_139),sF0),sF0),
inference(step,[status(thm)],[t2162,t148]) ).
cnf(t2164,plain,
sF0 = ifeq(p_Wr_error(plus(t_139,n1)),sF0,p_Reset(t_139),sF0),
inference(step,[status(thm)],[t2163,t148]) ).
cnf(t2165,plain,
sF0 = ifeq(p_Wr_error(sF3),sF0,p_Reset(t_139),sF0),
inference(step,[status(thm)],[t2164,t133]) ).
cnf(t2166,plain,
sF0 = ifeq(sF0,sF0,p_Reset(t_139),sF0),
inference(step,[status(thm)],[t2165,t135]) ).
cnf(t2167,plain,
sF0 = p_Reset(t_139),
inference(step,[status(thm)],[t2166,t148]) ).
cnf(t2168,plain,
sF0 = false,
inference(step,[status(thm)],[t2167,t244]) ).
cnf(t1555,plain,
false = sF0,
inference(orient,[status(thm)],[t2168]) ).
cnf(f0,axiom,
plus(X_0,n1) != n0,
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/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(f16,axiom,
~ gt(X_28,X_28),
file('/export/starexec/sandbox2/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(f29,axiom,
( ~ p_Rd_error(plus(X_t_37,n1))
| ~ p_Reset(X_t_37) ),
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/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(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c0,c5,c6,c16,c28,c29,c30,c31]) ).
cnf(g0_0,plain,
sF0 != false,
inference(rw,[status(thm)],[goal_0,t118]) ).
cnf(g0_1,plain,
sF0 != sF0,
inference(rw,[status(thm)],[g0_0,t1555]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV012-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.37 % Computer : n005.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Wed Sep 23 16:22:49 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 7.80/1.50 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.80/1.50 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------