%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : HWV020-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 : n019.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:38:02 PM UTC 2026
% Result : Unsatisfiable 8.70s 1.71s
% Output : Proof 8.70s
% Verified :
% Comments :
%------------------------------------------------------------------------------
cnf(t115,axiom,
sF0 = p_Empty(t_139),
introduced(definition) ).
cnf(f91,negated_conjecture,
p_Empty(t_139),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quest_2) ).
fof(f91_nnf,plain,
p_Empty(t_139),
inference(nnf_transformation,[status(thm)],[f91]) ).
cnf(c91,plain,
p_Empty(t_139),
inference(cnf_transformation,[status(esa)],[f91_nnf]) ).
cnf(t2,plain,
p_Empty(t_139) = true,
inference(equality_encoding,[status(esa)],[c91]) ).
cnf(t131,plain,
p_Empty(t_139) = true,
inference(orient,[status(thm)],[t2]) ).
cnf(t1565,plain,
sF0 = true,
inference(step,[status(thm)],[t115,t131]) ).
cnf(t135,plain,
true = sF0,
inference(orient,[status(thm)],[t1565]) ).
cnf(t117,axiom,
sF2 = p_Reset(t_139),
introduced(definition) ).
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(t1574,plain,
sF2 = false,
inference(step,[status(thm)],[t117,t133]) ).
cnf(t144,plain,
false = sF2,
inference(orient,[status(thm)],[t1574]) ).
cnf(f23,axiom,
( p_Empty(X_t_35)
| int_level(X_t_35) != n0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_24) ).
fof(f23_nnf,plain,
! [X_t_35] :
( p_Empty(X_t_35)
| int_level(X_t_35) != n0 ),
inference(nnf_transformation,[status(thm)],[f23]) ).
fof(f23_sk,plain,
! [X_t_35] :
( p_Empty(X_t_35)
| int_level(X_t_35) != n0 ),
inference(skolemisation,[status(esa)],[f23_nnf]) ).
cnf(c23,plain,
( p_Empty(X0)
| int_level(X0) != n0 ),
inference(cnf_transformation,[status(esa)],[f23_sk]) ).
cnf(t23,plain,
ifeq(int_level(X1),n0,p_Empty(X1),true) = true,
inference(equality_encoding,[status(esa)],[c23]) ).
cnf(t1619,plain,
ifeq(int_level(X1),n0,p_Empty(X1),sF0) = true,
inference(step,[status(thm)],[t23,t135]) ).
cnf(t1620,plain,
ifeq(int_level(X1),n0,p_Empty(X1),sF0) = sF0,
inference(step,[status(thm)],[t1619,t135]) ).
cnf(t193,plain,
ifeq(int_level(X1),n0,p_Empty(X1),sF0) = sF0,
inference(orient,[status(thm)],[t1620]) ).
cnf(t20,plain,
ifeq(eq(X1,X2),true,X1,X2) = X2,
introduced(definition) ).
cnf(t1616,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)],[t1616]) ).
cnf(f77,axiom,
( int_level(plus(X_t_42,n1)) = int_level(X_t_42)
| gt(int_level(X_t_42),n0)
| ~ p_Rd(X_t_42)
| p_Wr(X_t_42)
| p_Reset(X_t_42) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_78) ).
fof(f77_nnf,plain,
! [X_t_42] :
( int_level(plus(X_t_42,n1)) = int_level(X_t_42)
| gt(int_level(X_t_42),n0)
| ~ p_Rd(X_t_42)
| p_Wr(X_t_42)
| p_Reset(X_t_42) ),
inference(nnf_transformation,[status(thm)],[f77]) ).
fof(f77_sk,plain,
! [X_t_42] :
( int_level(plus(X_t_42,n1)) = int_level(X_t_42)
| gt(int_level(X_t_42),n0)
| ~ p_Rd(X_t_42)
| p_Wr(X_t_42)
| p_Reset(X_t_42) ),
inference(skolemisation,[status(esa)],[f77_nnf]) ).
cnf(c77,plain,
( int_level(plus(X0,n1)) = int_level(X0)
| gt(int_level(X0),n0)
| ~ p_Rd(X0)
| p_Wr(X0)
| p_Reset(X0) ),
inference(cnf_transformation,[status(esa)],[f77_sk]) ).
cnf(t77,plain,
ifeq(p_Rd(X1),true,or(p_Reset(X1),or(p_Wr(X1),or(gt(int_level(X1),n0),eq(int_level(plus(X1,n1)),int_level(X1))))),true) = true,
inference(equality_encoding,[status(esa)],[c77]) ).
cnf(t2065,plain,
ifeq(p_Rd(X1),sF0,or(p_Reset(X1),or(p_Wr(X1),or(gt(int_level(X1),n0),eq(int_level(plus(X1,n1)),int_level(X1))))),true) = true,
inference(step,[status(thm)],[t77,t135]) ).
cnf(t2066,plain,
ifeq(p_Rd(X1),sF0,or(p_Reset(X1),or(p_Wr(X1),or(gt(int_level(X1),n0),eq(int_level(plus(X1,n1)),int_level(X1))))),sF0) = true,
inference(step,[status(thm)],[t2065,t135]) ).
cnf(t2067,plain,
ifeq(p_Rd(X1),sF0,or(p_Reset(X1),or(p_Wr(X1),or(gt(int_level(X1),n0),eq(int_level(plus(X1,n1)),int_level(X1))))),sF0) = sF0,
inference(step,[status(thm)],[t2066,t135]) ).
cnf(t1428,plain,
ifeq(p_Rd(X1),sF0,or(p_Reset(X1),or(p_Wr(X1),or(gt(int_level(X1),n0),eq(int_level(plus(X1,n1)),int_level(X1))))),sF0) = sF0,
inference(orient,[status(thm)],[t2067]) ).
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]) ).
cnf(c90,plain,
p_Rd(t_139),
inference(cnf_transformation,[status(esa)],[f90_nnf]) ).
cnf(t3,plain,
p_Rd(t_139) = true,
inference(equality_encoding,[status(esa)],[c90]) ).
cnf(t132,plain,
p_Rd(t_139) = true,
inference(orient,[status(thm)],[t3]) ).
cnf(t1571,plain,
p_Rd(t_139) = sF0,
inference(step,[status(thm)],[t132,t135]) ).
cnf(t141,plain,
p_Rd(t_139) = sF0,
inference(orient,[status(thm)],[t1571]) ).
cnf(t1429,plain,
sF0 = ifeq(sF0,sF0,or(p_Reset(t_139),or(p_Wr(t_139),or(gt(int_level(t_139),n0),eq(int_level(plus(t_139,n1)),int_level(t_139))))),sF0),
inference(cp,[status(thm)],[t1428,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(t2068,plain,
sF0 = or(p_Reset(t_139),or(p_Wr(t_139),or(gt(int_level(t_139),n0),eq(int_level(plus(t_139,n1)),int_level(t_139))))),
inference(step,[status(thm)],[t1429,t173]) ).
cnf(t1576,plain,
p_Reset(t_139) = sF2,
inference(step,[status(thm)],[t133,t144]) ).
cnf(t146,plain,
p_Reset(t_139) = sF2,
inference(orient,[status(thm)],[t1576]) ).
cnf(t2069,plain,
sF0 = or(sF2,or(p_Wr(t_139),or(gt(int_level(t_139),n0),eq(int_level(plus(t_139,n1)),int_level(t_139))))),
inference(step,[status(thm)],[t2068,t146]) ).
cnf(t10,plain,
or(false,X1) = X1,
introduced(definition) ).
cnf(t1587,plain,
or(sF2,X1) = X1,
inference(step,[status(thm)],[t10,t144]) ).
cnf(t157,plain,
or(sF2,X1) = X1,
inference(orient,[status(thm)],[t1587]) ).
cnf(t2070,plain,
sF0 = or(p_Wr(t_139),or(gt(int_level(t_139),n0),eq(int_level(plus(t_139,n1)),int_level(t_139)))),
inference(step,[status(thm)],[t2069,t157]) ).
cnf(f92,negated_conjecture,
~ p_Wr(t_139),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quest_3) ).
fof(f92_nnf,plain,
~ p_Wr(t_139),
inference(nnf_transformation,[status(thm)],[f92]) ).
fof(f92_sk,plain,
~ p_Wr(t_139),
inference(skolemisation,[status(esa)],[f92_nnf]) ).
cnf(c92,plain,
~ p_Wr(t_139),
inference(cnf_transformation,[status(esa)],[f92_sk]) ).
cnf(t5,plain,
p_Wr(t_139) = false,
inference(equality_encoding,[status(esa)],[c92]) ).
cnf(t134,plain,
p_Wr(t_139) = false,
inference(orient,[status(thm)],[t5]) ).
cnf(t1578,plain,
p_Wr(t_139) = sF2,
inference(step,[status(thm)],[t134,t144]) ).
cnf(t148,plain,
p_Wr(t_139) = sF2,
inference(orient,[status(thm)],[t1578]) ).
cnf(t2071,plain,
sF0 = or(sF2,or(gt(int_level(t_139),n0),eq(int_level(plus(t_139,n1)),int_level(t_139)))),
inference(step,[status(thm)],[t2070,t148]) ).
cnf(t2072,plain,
sF0 = or(gt(int_level(t_139),n0),eq(int_level(plus(t_139,n1)),int_level(t_139))),
inference(step,[status(thm)],[t2071,t157]) ).
cnf(f24,axiom,
( ~ p_Empty(X_t_36)
| int_level(X_t_36) = n0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_25) ).
fof(f24_nnf,plain,
! [X_t_36] :
( ~ p_Empty(X_t_36)
| int_level(X_t_36) = n0 ),
inference(nnf_transformation,[status(thm)],[f24]) ).
fof(f24_sk,plain,
! [X_t_36] :
( ~ p_Empty(X_t_36)
| int_level(X_t_36) = n0 ),
inference(skolemisation,[status(esa)],[f24_nnf]) ).
cnf(c24,plain,
( ~ p_Empty(X0)
| int_level(X0) = n0 ),
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
cnf(t24,plain,
ifeq(p_Empty(X1),true,int_level(X1),n0) = n0,
inference(equality_encoding,[status(esa)],[c24]) ).
cnf(t1621,plain,
ifeq(p_Empty(X1),sF0,int_level(X1),n0) = n0,
inference(step,[status(thm)],[t24,t135]) ).
cnf(t198,plain,
ifeq(p_Empty(X1),sF0,int_level(X1),n0) = n0,
inference(orient,[status(thm)],[t1621]) ).
cnf(t1569,plain,
p_Empty(t_139) = sF0,
inference(step,[status(thm)],[t131,t135]) ).
cnf(t139,plain,
p_Empty(t_139) = sF0,
inference(orient,[status(thm)],[t1569]) ).
cnf(t199,plain,
n0 = ifeq(sF0,sF0,int_level(t_139),n0),
inference(cp,[status(thm)],[t198,t139]) ).
cnf(t1622,plain,
n0 = int_level(t_139),
inference(step,[status(thm)],[t199,t173]) ).
cnf(t201,plain,
int_level(t_139) = n0,
inference(orient,[status(thm)],[t1622]) ).
cnf(t2073,plain,
sF0 = or(gt(n0,n0),eq(int_level(plus(t_139,n1)),int_level(t_139))),
inference(step,[status(thm)],[t2072,t201]) ).
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(t1583,plain,
gt(X1,X1) = sF2,
inference(step,[status(thm)],[t7,t144]) ).
cnf(t154,plain,
gt(X1,X1) = sF2,
inference(orient,[status(thm)],[t1583]) ).
cnf(t2074,plain,
sF0 = or(sF2,eq(int_level(plus(t_139,n1)),int_level(t_139))),
inference(step,[status(thm)],[t2073,t154]) ).
cnf(t2075,plain,
sF0 = eq(int_level(plus(t_139,n1)),int_level(t_139)),
inference(step,[status(thm)],[t2074,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(t2076,plain,
sF0 = eq(int_level(sF6),int_level(t_139)),
inference(step,[status(thm)],[t2075,t160]) ).
cnf(t2077,plain,
sF0 = eq(int_level(sF6),n0),
inference(step,[status(thm)],[t2076,t201]) ).
cnf(t1431,plain,
eq(int_level(sF6),n0) = sF0,
inference(orient,[status(thm)],[t2077]) ).
cnf(t1432,plain,
n0 = ifeq(sF0,sF0,int_level(sF6),n0),
inference(cp,[status(thm)],[t186,t1431]) ).
cnf(t2078,plain,
n0 = int_level(sF6),
inference(step,[status(thm)],[t1432,t173]) ).
cnf(t1435,plain,
int_level(sF6) = n0,
inference(orient,[status(thm)],[t2078]) ).
cnf(t1441,plain,
sF0 = ifeq(n0,n0,p_Empty(sF6),sF0),
inference(cp,[status(thm)],[t193,t1435]) ).
cnf(t2080,plain,
sF0 = p_Empty(sF6),
inference(step,[status(thm)],[t1441,t173]) ).
cnf(t122,axiom,
sF7 = p_Empty(plus(t_139,n1)),
introduced(definition) ).
cnf(t1591,plain,
sF7 = p_Empty(sF6),
inference(step,[status(thm)],[t122,t160]) ).
cnf(t166,plain,
p_Empty(sF6) = sF7,
inference(orient,[status(thm)],[t1591]) ).
cnf(t17,plain,
ifeq(not(X1),true,X1,false) = false,
introduced(definition) ).
cnf(t1598,plain,
ifeq(not(X1),sF0,X1,false) = false,
inference(step,[status(thm)],[t17,t135]) ).
cnf(t1599,plain,
ifeq(not(X1),sF0,X1,sF2) = false,
inference(step,[status(thm)],[t1598,t144]) ).
cnf(t1600,plain,
ifeq(not(X1),sF0,X1,sF2) = sF2,
inference(step,[status(thm)],[t1599,t144]) ).
cnf(t176,plain,
ifeq(not(X1),sF0,X1,sF2) = sF2,
inference(orient,[status(thm)],[t1600]) ).
cnf(t123,axiom,
sF8 = not(p_Empty(plus(t_139,n1))),
introduced(definition) ).
cnf(t1594,plain,
sF8 = not(p_Empty(sF6)),
inference(step,[status(thm)],[t123,t160]) ).
cnf(t1595,plain,
sF8 = not(sF7),
inference(step,[status(thm)],[t1594,t166]) ).
cnf(t174,plain,
not(sF7) = sF8,
inference(orient,[status(thm)],[t1595]) ).
cnf(t178,plain,
sF2 = ifeq(sF8,sF0,sF7,sF2),
inference(cp,[status(thm)],[t176,t174]) ).
cnf(t181,plain,
ifeq(sF8,sF0,sF7,sF2) = sF2,
inference(orient,[status(thm)],[t178]) ).
cnf(t1130,plain,
ifeq(sF0,sF0,sF7,sF2) = sF2,
inference(rw,[status(thm)],[t181]) ).
cnf(t1995,plain,
sF7 = sF2,
inference(step,[status(thm)],[t1130,t173]) ).
cnf(t1134,plain,
sF7 = sF2,
inference(orient,[status(thm)],[t1995]) ).
cnf(t1996,plain,
p_Empty(sF6) = sF2,
inference(step,[status(thm)],[t166,t1134]) ).
cnf(t1135,plain,
p_Empty(sF6) = sF2,
inference(orient,[status(thm)],[t1996]) ).
cnf(t2081,plain,
sF0 = sF2,
inference(step,[status(thm)],[t2080,t1135]) ).
cnf(t1448,plain,
sF2 = sF0,
inference(orient,[status(thm)],[t2081]) ).
cnf(t2086,plain,
false = sF0,
inference(step,[status(thm)],[t144,t1448]) ).
cnf(t1453,plain,
false = sF0,
inference(orient,[status(thm)],[t2086]) ).
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_Rd_error(plus(t_139,n1))
| ~ p_Empty(plus(t_139,n1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quest_5) ).
fof(f94_nnf,plain,
( ~ p_Rd_error(plus(t_139,n1))
| ~ p_Empty(plus(t_139,n1)) ),
inference(nnf_transformation,[status(thm)],[f94]) ).
fof(f94_sk,plain,
( ~ p_Rd_error(plus(t_139,n1))
| ~ p_Empty(plus(t_139,n1)) ),
inference(skolemisation,[status(esa)],[f94_nnf]) ).
cnf(c94,plain,
( ~ p_Rd_error(plus(t_139,n1))
| ~ p_Empty(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,c92,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,t1453]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV020-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.38 % Computer : n019.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Wed Sep 23 16:26:19 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 8.70/1.71 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.70/1.71 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------