%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : HWV009-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 : n016.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:38 PM UTC 2026
% Result : Unsatisfiable 6.56s 1.23s
% Output : Proof 6.56s
% Verified :
% Comments :
%------------------------------------------------------------------------------
cnf(t109,axiom,
sF0 = p_Reset(t_139),
introduced(definition) ).
cnf(f90,negated_conjecture,
p_Reset(t_139),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quest_1) ).
fof(f90_nnf,plain,
p_Reset(t_139),
inference(nnf_transformation,[status(thm)],[f90]) ).
cnf(c90,plain,
p_Reset(t_139),
inference(cnf_transformation,[status(esa)],[f90_nnf]) ).
cnf(t2,plain,
p_Reset(t_139) = true,
inference(equality_encoding,[status(esa)],[c90]) ).
cnf(t118,plain,
p_Reset(t_139) = true,
inference(orient,[status(thm)],[t2]) ).
cnf(t1035,plain,
sF0 = true,
inference(step,[status(thm)],[t109,t118]) ).
cnf(t119,plain,
true = sF0,
inference(orient,[status(thm)],[t1035]) ).
cnf(t14,plain,
ifeq(not(X1),true,X1,false) = false,
introduced(definition) ).
cnf(t1050,plain,
ifeq(not(X1),sF0,X1,false) = false,
inference(step,[status(thm)],[t14,t119]) ).
cnf(t148,plain,
ifeq(not(X1),sF0,X1,false) = false,
inference(orient,[status(thm)],[t1050]) ).
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(t29,plain,
or(not(p_Reset(X1)),not(p_Rd_error(plus(X1,n1)))) = true,
inference(equality_encoding,[status(esa)],[c29]) ).
cnf(t1105,plain,
or(not(p_Reset(X1)),not(p_Rd_error(plus(X1,n1)))) = sF0,
inference(step,[status(thm)],[t29,t119]) ).
cnf(t257,plain,
or(not(p_Reset(X1)),not(p_Rd_error(plus(X1,n1)))) = sF0,
inference(orient,[status(thm)],[t1105]) ).
cnf(t1039,plain,
p_Reset(t_139) = sF0,
inference(step,[status(thm)],[t118,t119]) ).
cnf(t123,plain,
p_Reset(t_139) = sF0,
inference(orient,[status(thm)],[t1039]) ).
cnf(t258,plain,
sF0 = or(not(sF0),not(p_Rd_error(plus(t_139,n1)))),
inference(cp,[status(thm)],[t257,t123]) ).
cnf(t1,plain,
not(true) = false,
introduced(definition) ).
cnf(t117,plain,
not(true) = false,
inference(orient,[status(thm)],[t1]) ).
cnf(t1038,plain,
not(sF0) = false,
inference(step,[status(thm)],[t117,t119]) ).
cnf(t122,plain,
not(sF0) = false,
inference(rw,[status(thm)],[t1038]) ).
cnf(t125,plain,
not(sF0) = false,
inference(orient,[status(thm)],[t122]) ).
cnf(t1106,plain,
sF0 = or(false,not(p_Rd_error(plus(t_139,n1)))),
inference(step,[status(thm)],[t258,t125]) ).
cnf(t7,plain,
or(false,X1) = X1,
introduced(definition) ).
cnf(t130,plain,
or(false,X1) = X1,
inference(orient,[status(thm)],[t7]) ).
cnf(t1107,plain,
sF0 = not(p_Rd_error(plus(t_139,n1))),
inference(step,[status(thm)],[t1106,t130]) ).
cnf(t110,axiom,
sF1 = plus(t_139,n1),
introduced(definition) ).
cnf(t133,plain,
plus(t_139,n1) = sF1,
inference(orient,[status(thm)],[t110]) ).
cnf(t1108,plain,
sF0 = not(p_Rd_error(sF1)),
inference(step,[status(thm)],[t1107,t133]) ).
cnf(t113,axiom,
sF4 = p_Rd_error(plus(t_139,n1)),
introduced(definition) ).
cnf(t1048,plain,
sF4 = p_Rd_error(sF1),
inference(step,[status(thm)],[t113,t133]) ).
cnf(t136,plain,
p_Rd_error(sF1) = sF4,
inference(orient,[status(thm)],[t1048]) ).
cnf(t1109,plain,
sF0 = not(sF4),
inference(step,[status(thm)],[t1108,t136]) ).
cnf(t260,plain,
not(sF4) = sF0,
inference(orient,[status(thm)],[t1109]) ).
cnf(t261,plain,
false = ifeq(sF0,sF0,sF4,false),
inference(cp,[status(thm)],[t148,t260]) ).
cnf(t13,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t145,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t13]) ).
cnf(t1110,plain,
false = sF4,
inference(step,[status(thm)],[t261,t145]) ).
cnf(t262,plain,
false = sF4,
inference(orient,[status(thm)],[t1110]) ).
cnf(t270,plain,
ifeq(not(X1),sF0,X1,sF4) = false,
inference(rw,[status(thm)],[t148]) ).
cnf(t1145,plain,
ifeq(not(X1),sF0,X1,sF4) = sF4,
inference(step,[status(thm)],[t270,t262]) ).
cnf(t303,plain,
ifeq(not(X1),sF0,X1,sF4) = sF4,
inference(orient,[status(thm)],[t1145]) ).
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(t30,plain,
or(not(p_Reset(X1)),not(p_Wr_error(plus(X1,n1)))) = true,
inference(equality_encoding,[status(esa)],[c28]) ).
cnf(t1138,plain,
or(not(p_Reset(X1)),not(p_Wr_error(plus(X1,n1)))) = sF0,
inference(step,[status(thm)],[t30,t119]) ).
cnf(t296,plain,
or(not(p_Reset(X1)),not(p_Wr_error(plus(X1,n1)))) = sF0,
inference(orient,[status(thm)],[t1138]) ).
cnf(t297,plain,
sF0 = or(not(sF0),not(p_Wr_error(plus(t_139,n1)))),
inference(cp,[status(thm)],[t296,t123]) ).
cnf(t1111,plain,
not(sF0) = sF4,
inference(step,[status(thm)],[t125,t262]) ).
cnf(t264,plain,
not(sF0) = sF4,
inference(orient,[status(thm)],[t1111]) ).
cnf(t1139,plain,
sF0 = or(sF4,not(p_Wr_error(plus(t_139,n1)))),
inference(step,[status(thm)],[t297,t264]) ).
cnf(t1116,plain,
or(sF4,X1) = X1,
inference(step,[status(thm)],[t130,t262]) ).
cnf(t269,plain,
or(sF4,X1) = X1,
inference(rw,[status(thm)],[t1116]) ).
cnf(t290,plain,
or(sF4,X1) = X1,
inference(orient,[status(thm)],[t269]) ).
cnf(t1140,plain,
sF0 = not(p_Wr_error(plus(t_139,n1))),
inference(step,[status(thm)],[t1139,t290]) ).
cnf(t1141,plain,
sF0 = not(p_Wr_error(sF1)),
inference(step,[status(thm)],[t1140,t133]) ).
cnf(t112,axiom,
sF3 = p_Wr_error(plus(t_139,n1)),
introduced(definition) ).
cnf(t1047,plain,
sF3 = p_Wr_error(sF1),
inference(step,[status(thm)],[t112,t133]) ).
cnf(t135,plain,
p_Wr_error(sF1) = sF3,
inference(orient,[status(thm)],[t1047]) ).
cnf(t1142,plain,
sF0 = not(sF3),
inference(step,[status(thm)],[t1141,t135]) ).
cnf(t299,plain,
not(sF3) = sF0,
inference(orient,[status(thm)],[t1142]) ).
cnf(t305,plain,
sF4 = ifeq(sF0,sF0,sF3,sF4),
inference(cp,[status(thm)],[t303,t299]) ).
cnf(t1146,plain,
sF4 = sF3,
inference(step,[status(thm)],[t305,t145]) ).
cnf(t307,plain,
sF4 = sF3,
inference(orient,[status(thm)],[t1146]) ).
cnf(t1163,plain,
false = sF3,
inference(step,[status(thm)],[t262,t307]) ).
cnf(t325,plain,
false = sF3,
inference(orient,[status(thm)],[t1163]) ).
cnf(f91,negated_conjecture,
( p_Rd_error(plus(t_139,n1))
| p_Wr_error(plus(t_139,n1))
| level(plus(t_139,n1)) != n0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quest_2) ).
fof(f91_nnf,plain,
( p_Rd_error(plus(t_139,n1))
| p_Wr_error(plus(t_139,n1))
| level(plus(t_139,n1)) != n0 ),
inference(nnf_transformation,[status(thm)],[f91]) ).
fof(f91_sk,plain,
( p_Rd_error(plus(t_139,n1))
| p_Wr_error(plus(t_139,n1))
| level(plus(t_139,n1)) != n0 ),
inference(skolemisation,[status(esa)],[f91_nnf]) ).
cnf(c91,plain,
( p_Rd_error(plus(t_139,n1))
| p_Wr_error(plus(t_139,n1))
| level(plus(t_139,n1)) != n0 ),
inference(cnf_transformation,[status(esa)],[f91_sk]) ).
cnf(u0,axiom,
ifeq(level(plus(t_139,n1)),n0,or(p_Wr_error(plus(t_139,n1)),p_Rd_error(plus(t_139,n1))),true) = true,
inference(equality_encoding,[status(esa)],[c91]) ).
cnf(f20,axiom,
level(X_t_32) = int_level(X_t_32),
file('/export/starexec/sandbox/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(t52,plain,
ifeq(int_level(plus(t_139,n1)),n0,or(p_Wr_error(plus(t_139,n1)),p_Rd_error(plus(t_139,n1))),true) = true,
inference(definition_unfolding,[status(thm)],[u0,d0]) ).
cnf(t1369,plain,
ifeq(int_level(sF1),n0,or(p_Wr_error(plus(t_139,n1)),p_Rd_error(plus(t_139,n1))),true) = true,
inference(step,[status(thm)],[t52,t133]) ).
cnf(t111,axiom,
sF2 = int_level(plus(t_139,n1)),
introduced(definition) ).
cnf(t1046,plain,
sF2 = int_level(sF1),
inference(step,[status(thm)],[t111,t133]) ).
cnf(t134,plain,
int_level(sF1) = sF2,
inference(orient,[status(thm)],[t1046]) ).
cnf(t1370,plain,
ifeq(sF2,n0,or(p_Wr_error(plus(t_139,n1)),p_Rd_error(plus(t_139,n1))),true) = true,
inference(step,[status(thm)],[t1369,t134]) ).
cnf(f25,axiom,
( int_level(plus(X_t_37,n1)) = n0
| ~ p_Reset(X_t_37) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_26) ).
fof(f25_nnf,plain,
! [X_t_37] :
( int_level(plus(X_t_37,n1)) = n0
| ~ p_Reset(X_t_37) ),
inference(nnf_transformation,[status(thm)],[f25]) ).
fof(f25_sk,plain,
! [X_t_37] :
( int_level(plus(X_t_37,n1)) = n0
| ~ p_Reset(X_t_37) ),
inference(skolemisation,[status(esa)],[f25_nnf]) ).
cnf(c25,plain,
( int_level(plus(X0,n1)) = n0
| ~ p_Reset(X0) ),
inference(cnf_transformation,[status(esa)],[f25_sk]) ).
cnf(t23,plain,
ifeq(p_Reset(X1),true,int_level(plus(X1,n1)),n0) = n0,
inference(equality_encoding,[status(esa)],[c25]) ).
cnf(t1065,plain,
ifeq(p_Reset(X1),sF0,int_level(plus(X1,n1)),n0) = n0,
inference(step,[status(thm)],[t23,t119]) ).
cnf(t177,plain,
ifeq(p_Reset(X1),sF0,int_level(plus(X1,n1)),n0) = n0,
inference(orient,[status(thm)],[t1065]) ).
cnf(t178,plain,
n0 = ifeq(sF0,sF0,int_level(plus(t_139,n1)),n0),
inference(cp,[status(thm)],[t177,t123]) ).
cnf(t1066,plain,
n0 = int_level(plus(t_139,n1)),
inference(step,[status(thm)],[t178,t145]) ).
cnf(t1067,plain,
n0 = int_level(sF1),
inference(step,[status(thm)],[t1066,t133]) ).
cnf(t1068,plain,
n0 = sF2,
inference(step,[status(thm)],[t1067,t134]) ).
cnf(t180,plain,
n0 = sF2,
inference(orient,[status(thm)],[t1068]) ).
cnf(t1371,plain,
ifeq(sF2,sF2,or(p_Wr_error(plus(t_139,n1)),p_Rd_error(plus(t_139,n1))),true) = true,
inference(step,[status(thm)],[t1370,t180]) ).
cnf(t1372,plain,
or(p_Wr_error(plus(t_139,n1)),p_Rd_error(plus(t_139,n1))) = true,
inference(step,[status(thm)],[t1371,t145]) ).
cnf(t1373,plain,
or(p_Wr_error(sF1),p_Rd_error(plus(t_139,n1))) = true,
inference(step,[status(thm)],[t1372,t133]) ).
cnf(t1374,plain,
or(sF3,p_Rd_error(plus(t_139,n1))) = true,
inference(step,[status(thm)],[t1373,t135]) ).
cnf(t1166,plain,
or(sF3,X1) = X1,
inference(step,[status(thm)],[t290,t307]) ).
cnf(t328,plain,
or(sF3,X1) = X1,
inference(rw,[status(thm)],[t1166]) ).
cnf(t337,plain,
or(sF3,X1) = X1,
inference(orient,[status(thm)],[t328]) ).
cnf(t1375,plain,
p_Rd_error(plus(t_139,n1)) = true,
inference(step,[status(thm)],[t1374,t337]) ).
cnf(t1376,plain,
p_Rd_error(sF1) = true,
inference(step,[status(thm)],[t1375,t133]) ).
cnf(t1151,plain,
p_Rd_error(sF1) = sF3,
inference(step,[status(thm)],[t136,t307]) ).
cnf(t312,plain,
p_Rd_error(sF1) = sF3,
inference(orient,[status(thm)],[t1151]) ).
cnf(t1377,plain,
sF3 = true,
inference(step,[status(thm)],[t1376,t312]) ).
cnf(t1378,plain,
sF3 = sF0,
inference(step,[status(thm)],[t1377,t119]) ).
cnf(t930,plain,
sF3 = sF0,
inference(orient,[status(thm)],[t1378]) ).
cnf(t1397,plain,
false = sF0,
inference(step,[status(thm)],[t325,t930]) ).
cnf(t949,plain,
false = sF0,
inference(orient,[status(thm)],[t1397]) ).
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(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(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(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,t119]) ).
cnf(g0_1,plain,
sF0 != sF0,
inference(rw,[status(thm)],[g0_0,t949]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV009-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.08/0.35 % Computer : n016.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Wed Sep 23 16:26:43 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 6.56/1.23 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.56/1.23 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------