%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : HWV032-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 : n001.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:20 PM UTC 2026
% Result : Unsatisfiable 7.84s 1.60s
% Output : Proof 7.84s
% Verified :
% Comments :
%------------------------------------------------------------------------------
cnf(t111,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(t119,plain,
p_Reset(t_139) = true,
inference(orient,[status(thm)],[t2]) ).
cnf(t253,plain,
sF0 = true,
inference(step,[status(thm)],[t111,t119]) ).
cnf(t120,plain,
true = sF0,
inference(orient,[status(thm)],[t253]) ).
cnf(t115,axiom,
sF4 = gt(fifo_length,rd_level(plus(t_139,n1))),
introduced(definition) ).
cnf(t113,axiom,
sF2 = plus(t_139,n1),
introduced(definition) ).
cnf(t136,plain,
plus(t_139,n1) = sF2,
inference(orient,[status(thm)],[t113]) ).
cnf(t271,plain,
sF4 = gt(fifo_length,rd_level(sF2)),
inference(step,[status(thm)],[t115,t136]) ).
cnf(t114,axiom,
sF3 = rd_level(plus(t_139,n1)),
introduced(definition) ).
cnf(t266,plain,
sF3 = rd_level(sF2),
inference(step,[status(thm)],[t114,t136]) ).
cnf(t137,plain,
rd_level(sF2) = sF3,
inference(orient,[status(thm)],[t266]) ).
cnf(t272,plain,
sF4 = gt(fifo_length,sF3),
inference(step,[status(thm)],[t271,t137]) ).
cnf(f91,negated_conjecture,
~ gt(fifo_length,rd_level(plus(t_139,n1))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quest_2) ).
fof(f91_nnf,plain,
~ gt(fifo_length,rd_level(plus(t_139,n1))),
inference(nnf_transformation,[status(thm)],[f91]) ).
fof(f91_sk,plain,
~ gt(fifo_length,rd_level(plus(t_139,n1))),
inference(skolemisation,[status(esa)],[f91_nnf]) ).
cnf(c91,plain,
~ gt(fifo_length,rd_level(plus(t_139,n1))),
inference(cnf_transformation,[status(esa)],[f91_sk]) ).
cnf(t15,plain,
gt(fifo_length,rd_level(plus(t_139,n1))) = false,
inference(equality_encoding,[status(esa)],[c91]) ).
cnf(t268,plain,
gt(fifo_length,rd_level(sF2)) = false,
inference(step,[status(thm)],[t15,t136]) ).
cnf(t269,plain,
gt(fifo_length,sF3) = false,
inference(step,[status(thm)],[t268,t137]) ).
cnf(t149,plain,
gt(fifo_length,sF3) = false,
inference(orient,[status(thm)],[t269]) ).
cnf(t273,plain,
sF4 = false,
inference(step,[status(thm)],[t272,t149]) ).
cnf(t153,plain,
false = sF4,
inference(orient,[status(thm)],[t273]) ).
cnf(f92,negated_conjecture,
gt(fifo_length,n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quest_3) ).
fof(f92_nnf,plain,
gt(fifo_length,n0),
inference(nnf_transformation,[status(thm)],[f92]) ).
cnf(c92,plain,
gt(fifo_length,n0),
inference(cnf_transformation,[status(esa)],[f92_nnf]) ).
cnf(t5,plain,
gt(fifo_length,n0) = true,
inference(equality_encoding,[status(esa)],[c92]) ).
cnf(t260,plain,
gt(fifo_length,n0) = sF0,
inference(step,[status(thm)],[t5,t120]) ).
cnf(t129,plain,
gt(fifo_length,n0) = sF0,
inference(orient,[status(thm)],[t260]) ).
cnf(t213,plain,
gt(fifo_length,sF3) = sF0,
inference(rw,[status(thm)],[t129]) ).
cnf(t287,plain,
gt(fifo_length,sF3) = sF4,
inference(step,[status(thm)],[t149,t153]) ).
cnf(t167,plain,
gt(fifo_length,sF3) = sF4,
inference(orient,[status(thm)],[t287]) ).
cnf(t333,plain,
sF4 = sF0,
inference(step,[status(thm)],[t213,t167]) ).
cnf(t238,plain,
sF4 = sF0,
inference(orient,[status(thm)],[t333]) ).
cnf(t340,plain,
false = sF0,
inference(step,[status(thm)],[t153,t238]) ).
cnf(t245,plain,
false = sF0,
inference(orient,[status(thm)],[t340]) ).
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(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(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c0,c5,c6,c16,c28,c29,c30,c31,c91]) ).
cnf(g0_0,plain,
sF0 != false,
inference(rw,[status(thm)],[goal_0,t120]) ).
cnf(g0_1,plain,
sF0 != sF0,
inference(rw,[status(thm)],[g0_0,t245]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : HWV032-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.06 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.18/0.45 % Computer : n001.cluster.edu
% 0.18/0.45 % Model : x86_64 x86_64
% 0.18/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.45 % Memory : 8046.5625MB
% 0.18/0.45 % OS : Linux 6.8.0-71-generic
% 0.18/0.45 % CPULimit : 300
% 0.18/0.45 % WCLimit : 300
% 0.18/0.45 % DateTime : Wed Sep 23 16:35:50 UTC 2026
% 0.18/0.45 % CPUTime :
% 0.18/0.45 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 7.84/1.60 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 7.84/1.60 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------