%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : HWV022-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 : n026.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:06 PM UTC 2026
% Result : Unsatisfiable 17.64s 2.73s
% Output : Proof 17.64s
% Verified :
% Comments :
%------------------------------------------------------------------------------
cnf(t117,axiom,
sF2 = p_Wr(t_139),
introduced(definition) ).
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]) ).
cnf(c92,plain,
p_Wr(t_139),
inference(cnf_transformation,[status(esa)],[f92_nnf]) ).
cnf(t4,plain,
p_Wr(t_139) = true,
inference(equality_encoding,[status(esa)],[c92]) ).
cnf(t130,plain,
p_Wr(t_139) = true,
inference(orient,[status(thm)],[t4]) ).
cnf(t2516,plain,
sF2 = true,
inference(step,[status(thm)],[t117,t130]) ).
cnf(t140,plain,
true = sF2,
inference(orient,[status(thm)],[t2516]) ).
cnf(f34,axiom,
( int_level(plus(X_t_42,n1)) = plus(int_level(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/sandbox/benchmark/theBenchmark.p',axiom_35) ).
fof(f34_nnf,plain,
! [X_t_42] :
( int_level(plus(X_t_42,n1)) = plus(int_level(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)],[f34]) ).
fof(f34_sk,plain,
! [X_t_42] :
( int_level(plus(X_t_42,n1)) = plus(int_level(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)],[f34_nnf]) ).
cnf(c34,plain,
( int_level(plus(X0,n1)) = plus(int_level(X0),n1)
| ~ gt(fifo_length,int_level(X0))
| p_Rd(X0)
| ~ p_Wr(X0)
| p_Reset(X0) ),
inference(cnf_transformation,[status(esa)],[f34_sk]) ).
cnf(t91,plain,
ifeq(p_Wr(X1),true,ifeq(gt(fifo_length,int_level(X1)),true,or(p_Reset(X1),or(p_Rd(X1),eq(int_level(plus(X1,n1)),plus(int_level(X1),n1)))),true),true) = true,
inference(equality_encoding,[status(esa)],[c34]) ).
cnf(t3188,plain,
ifeq(p_Wr(X1),sF2,ifeq(gt(fifo_length,int_level(X1)),true,or(p_Reset(X1),or(p_Rd(X1),eq(int_level(plus(X1,n1)),plus(int_level(X1),n1)))),true),true) = true,
inference(step,[status(thm)],[t91,t140]) ).
cnf(t119,axiom,
sF4 = plus(int_level(t_139),n1),
introduced(definition) ).
cnf(t118,axiom,
sF3 = int_level(t_139),
introduced(definition) ).
cnf(t144,plain,
int_level(t_139) = sF3,
inference(orient,[status(thm)],[t118]) ).
cnf(t2531,plain,
sF4 = plus(sF3,n1),
inference(step,[status(thm)],[t119,t144]) ).
cnf(f90,negated_conjecture,
plus(level(t_139),n1) = fifo_length,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quest_1) ).
fof(f90_nnf,plain,
plus(level(t_139),n1) = fifo_length,
inference(nnf_transformation,[status(thm)],[f90]) ).
cnf(c90,plain,
plus(level(t_139),n1) = fifo_length,
inference(cnf_transformation,[status(esa)],[f90_nnf]) ).
cnf(u0,axiom,
plus(level(t_139),n1) = fifo_length,
inference(equality_encoding,[status(esa)],[c90]) ).
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(t13,plain,
plus(int_level(t_139),n1) = fifo_length,
inference(definition_unfolding,[status(thm)],[u0,d0]) ).
cnf(t2529,plain,
plus(sF3,n1) = fifo_length,
inference(step,[status(thm)],[t13,t144]) ).
cnf(t155,plain,
plus(sF3,n1) = fifo_length,
inference(orient,[status(thm)],[t2529]) ).
cnf(t2532,plain,
sF4 = fifo_length,
inference(step,[status(thm)],[t2531,t155]) ).
cnf(t163,plain,
fifo_length = sF4,
inference(orient,[status(thm)],[t2532]) ).
cnf(t3189,plain,
ifeq(p_Wr(X1),sF2,ifeq(gt(sF4,int_level(X1)),true,or(p_Reset(X1),or(p_Rd(X1),eq(int_level(plus(X1,n1)),plus(int_level(X1),n1)))),true),true) = true,
inference(step,[status(thm)],[t3188,t163]) ).
cnf(t3190,plain,
ifeq(p_Wr(X1),sF2,ifeq(gt(sF4,int_level(X1)),sF2,or(p_Reset(X1),or(p_Rd(X1),eq(int_level(plus(X1,n1)),plus(int_level(X1),n1)))),true),true) = true,
inference(step,[status(thm)],[t3189,t140]) ).
cnf(t3191,plain,
ifeq(p_Wr(X1),sF2,ifeq(gt(sF4,int_level(X1)),sF2,or(p_Reset(X1),or(p_Rd(X1),eq(int_level(plus(X1,n1)),plus(int_level(X1),n1)))),sF2),true) = true,
inference(step,[status(thm)],[t3190,t140]) ).
cnf(t3192,plain,
ifeq(p_Wr(X1),sF2,ifeq(gt(sF4,int_level(X1)),sF2,or(p_Reset(X1),or(p_Rd(X1),eq(int_level(plus(X1,n1)),plus(int_level(X1),n1)))),sF2),sF2) = true,
inference(step,[status(thm)],[t3191,t140]) ).
cnf(t3193,plain,
ifeq(p_Wr(X1),sF2,ifeq(gt(sF4,int_level(X1)),sF2,or(p_Reset(X1),or(p_Rd(X1),eq(int_level(plus(X1,n1)),plus(int_level(X1),n1)))),sF2),sF2) = sF2,
inference(step,[status(thm)],[t3192,t140]) ).
cnf(t2077,plain,
ifeq(p_Wr(X1),sF2,ifeq(gt(sF4,int_level(X1)),sF2,or(p_Reset(X1),or(p_Rd(X1),eq(int_level(plus(X1,n1)),plus(int_level(X1),n1)))),sF2),sF2) = sF2,
inference(orient,[status(thm)],[t3193]) ).
cnf(f91,negated_conjecture,
~ p_Rd(t_139),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quest_2) ).
fof(f91_nnf,plain,
~ p_Rd(t_139),
inference(nnf_transformation,[status(thm)],[f91]) ).
fof(f91_sk,plain,
~ p_Rd(t_139),
inference(skolemisation,[status(esa)],[f91_nnf]) ).
cnf(c91,plain,
~ p_Rd(t_139),
inference(cnf_transformation,[status(esa)],[f91_sk]) ).
cnf(t2,plain,
p_Rd(t_139) = false,
inference(equality_encoding,[status(esa)],[c91]) ).
cnf(t128,plain,
p_Rd(t_139) = false,
inference(orient,[status(thm)],[t2]) ).
cnf(t115,axiom,
sF0 = p_Rd(t_139),
introduced(definition) ).
cnf(t2507,plain,
sF0 = false,
inference(step,[status(thm)],[t115,t128]) ).
cnf(t131,plain,
false = sF0,
inference(orient,[status(thm)],[t2507]) ).
cnf(t2511,plain,
p_Rd(t_139) = sF0,
inference(step,[status(thm)],[t128,t131]) ).
cnf(t135,plain,
p_Rd(t_139) = sF0,
inference(orient,[status(thm)],[t2511]) ).
cnf(t2078,plain,
sF2 = ifeq(p_Wr(t_139),sF2,ifeq(gt(sF4,int_level(t_139)),sF2,or(p_Reset(t_139),or(sF0,eq(int_level(plus(t_139,n1)),plus(int_level(t_139),n1)))),sF2),sF2),
inference(cp,[status(thm)],[t2077,t135]) ).
cnf(t2518,plain,
p_Wr(t_139) = sF2,
inference(step,[status(thm)],[t130,t140]) ).
cnf(t142,plain,
p_Wr(t_139) = sF2,
inference(orient,[status(thm)],[t2518]) ).
cnf(t3194,plain,
sF2 = ifeq(sF2,sF2,ifeq(gt(sF4,int_level(t_139)),sF2,or(p_Reset(t_139),or(sF0,eq(int_level(plus(t_139,n1)),plus(int_level(t_139),n1)))),sF2),sF2),
inference(step,[status(thm)],[t2078,t142]) ).
cnf(t16,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t176,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t16]) ).
cnf(t3195,plain,
sF2 = ifeq(gt(sF4,int_level(t_139)),sF2,or(p_Reset(t_139),or(sF0,eq(int_level(plus(t_139,n1)),plus(int_level(t_139),n1)))),sF2),
inference(step,[status(thm)],[t3194,t176]) ).
cnf(t3196,plain,
sF2 = ifeq(gt(sF4,sF3),sF2,or(p_Reset(t_139),or(sF0,eq(int_level(plus(t_139,n1)),plus(int_level(t_139),n1)))),sF2),
inference(step,[status(thm)],[t3195,t144]) ).
cnf(f8,axiom,
( ~ gt(plus(Y_12,n1),plus(X_11,n1))
| gt(Y_12,X_11) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_9) ).
fof(f8_nnf,plain,
! [Y_12,X_11] :
( ~ gt(plus(Y_12,n1),plus(X_11,n1))
| gt(Y_12,X_11) ),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [Y_12,X_11] :
( ~ gt(plus(Y_12,n1),plus(X_11,n1))
| gt(Y_12,X_11) ),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
( ~ gt(plus(X0,n1),plus(X1,n1))
| gt(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(t46,plain,
ifeq(gt(plus(X1,n1),plus(X2,n1)),true,gt(X1,X2),true) = true,
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(t2681,plain,
ifeq(gt(plus(X1,n1),plus(X2,n1)),sF2,gt(X1,X2),true) = true,
inference(step,[status(thm)],[t46,t140]) ).
cnf(t2682,plain,
ifeq(gt(plus(X1,n1),plus(X2,n1)),sF2,gt(X1,X2),sF2) = true,
inference(step,[status(thm)],[t2681,t140]) ).
cnf(t2683,plain,
ifeq(gt(plus(X1,n1),plus(X2,n1)),sF2,gt(X1,X2),sF2) = sF2,
inference(step,[status(thm)],[t2682,t140]) ).
cnf(t519,plain,
ifeq(gt(plus(X1,n1),plus(X2,n1)),sF2,gt(X1,X2),sF2) = sF2,
inference(orient,[status(thm)],[t2683]) ).
cnf(t2533,plain,
plus(sF3,n1) = sF4,
inference(step,[status(thm)],[t155,t163]) ).
cnf(t164,plain,
plus(sF3,n1) = sF4,
inference(orient,[status(thm)],[t2533]) ).
cnf(t525,plain,
sF2 = ifeq(gt(plus(X1,n1),sF4),sF2,gt(X1,sF3),sF2),
inference(cp,[status(thm)],[t519,t164]) ).
cnf(t950,plain,
ifeq(gt(plus(X1,n1),sF4),sF2,gt(X1,sF3),sF2) = sF2,
inference(orient,[status(thm)],[t525]) ).
cnf(f2,axiom,
( gt(X_2,minus(X_2,n1))
| ~ gt(X_2,n0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_3) ).
fof(f2_nnf,plain,
! [X_2] :
( gt(X_2,minus(X_2,n1))
| ~ gt(X_2,n0) ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [X_2] :
( gt(X_2,minus(X_2,n1))
| ~ gt(X_2,n0) ),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
( gt(X0,minus(X0,n1))
| ~ gt(X0,n0) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(t41,plain,
ifeq(gt(X1,n0),true,gt(X1,minus(X1,n1)),true) = true,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t2635,plain,
ifeq(gt(X1,n0),sF2,gt(X1,minus(X1,n1)),true) = true,
inference(step,[status(thm)],[t41,t140]) ).
cnf(t2636,plain,
ifeq(gt(X1,n0),sF2,gt(X1,minus(X1,n1)),sF2) = true,
inference(step,[status(thm)],[t2635,t140]) ).
cnf(t2637,plain,
ifeq(gt(X1,n0),sF2,gt(X1,minus(X1,n1)),sF2) = sF2,
inference(step,[status(thm)],[t2636,t140]) ).
cnf(t407,plain,
ifeq(gt(X1,n0),sF2,gt(X1,minus(X1,n1)),sF2) = sF2,
inference(orient,[status(thm)],[t2637]) ).
cnf(f17,axiom,
( X_29 = Y_30
| plus(X_29,n1) != plus(Y_30,n1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_18) ).
fof(f17_nnf,plain,
! [X_29,Y_30] :
( X_29 = Y_30
| plus(X_29,n1) != plus(Y_30,n1) ),
inference(nnf_transformation,[status(thm)],[f17]) ).
fof(f17_sk,plain,
! [X_29,Y_30] :
( X_29 = Y_30
| plus(X_29,n1) != plus(Y_30,n1) ),
inference(skolemisation,[status(esa)],[f17_nnf]) ).
cnf(c17,plain,
( X0 = X1
| plus(X0,n1) != plus(X1,n1) ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(t33,plain,
ifeq(plus(X1,n1),plus(X2,n1),X1,X2) = X2,
inference(equality_encoding,[status(esa)],[c17]) ).
cnf(t244,plain,
ifeq(plus(X1,n1),plus(X2,n1),X1,X2) = X2,
inference(orient,[status(thm)],[t33]) ).
cnf(t21,plain,
ifeq(eq(X1,X2),true,X1,X2) = X2,
introduced(definition) ).
cnf(t2564,plain,
ifeq(eq(X1,X2),sF2,X1,X2) = X2,
inference(step,[status(thm)],[t21,t140]) ).
cnf(t185,plain,
ifeq(eq(X1,X2),sF2,X1,X2) = X2,
inference(orient,[status(thm)],[t2564]) ).
cnf(f15,axiom,
( X_26 = plus(y_27(X_26),n1)
| X_26 = n0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_16) ).
fof(f15_nnf,plain,
! [X_26] :
( X_26 = plus(y_27(X_26),n1)
| X_26 = n0 ),
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
! [X_26] :
( X_26 = plus(y_27(X_26),n1)
| X_26 = n0 ),
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c15,plain,
( X0 = plus(y_27(X0),n1)
| X0 = n0 ),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(t38,plain,
or(eq(X1,n0),eq(X1,plus(y_27(X1),n1))) = true,
inference(equality_encoding,[status(esa)],[c15]) ).
cnf(t2616,plain,
or(eq(X1,n0),eq(X1,plus(y_27(X1),n1))) = sF2,
inference(step,[status(thm)],[t38,t140]) ).
cnf(t309,plain,
or(eq(X1,n0),eq(X1,plus(y_27(X1),n1))) = sF2,
inference(orient,[status(thm)],[t2616]) ).
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(t14,plain,
eq(plus(X1,n1),n0) = false,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t2530,plain,
eq(plus(X1,n1),n0) = sF0,
inference(step,[status(thm)],[t14,t131]) ).
cnf(t156,plain,
eq(plus(X1,n1),n0) = sF0,
inference(orient,[status(thm)],[t2530]) ).
cnf(t310,plain,
sF2 = or(sF0,eq(plus(X1,n1),plus(y_27(plus(X1,n1)),n1))),
inference(cp,[status(thm)],[t309,t156]) ).
cnf(t9,plain,
or(false,X1) = X1,
introduced(definition) ).
cnf(t2526,plain,
or(sF0,X1) = X1,
inference(step,[status(thm)],[t9,t131]) ).
cnf(t151,plain,
or(sF0,X1) = X1,
inference(orient,[status(thm)],[t2526]) ).
cnf(t2633,plain,
sF2 = eq(plus(X1,n1),plus(y_27(plus(X1,n1)),n1)),
inference(step,[status(thm)],[t310,t151]) ).
cnf(t388,plain,
eq(plus(X1,n1),plus(y_27(plus(X1,n1)),n1)) = sF2,
inference(orient,[status(thm)],[t2633]) ).
cnf(t389,plain,
plus(y_27(plus(X1,n1)),n1) = ifeq(sF2,sF2,plus(X1,n1),plus(y_27(plus(X1,n1)),n1)),
inference(cp,[status(thm)],[t185,t388]) ).
cnf(t2634,plain,
plus(y_27(plus(X1,n1)),n1) = plus(X1,n1),
inference(step,[status(thm)],[t389,t176]) ).
cnf(t391,plain,
plus(y_27(plus(X1,n1)),n1) = plus(X1,n1),
inference(orient,[status(thm)],[t2634]) ).
cnf(t396,plain,
X1 = ifeq(plus(X2,n1),plus(X1,n1),y_27(plus(X2,n1)),X1),
inference(cp,[status(thm)],[t244,t391]) ).
cnf(t465,plain,
ifeq(plus(X1,n1),plus(X2,n1),y_27(plus(X1,n1)),X2) = X2,
inference(orient,[status(thm)],[t396]) ).
cnf(t466,plain,
X1 = y_27(plus(X1,n1)),
inference(cp,[status(thm)],[t465,t176]) ).
cnf(t468,plain,
y_27(plus(X1,n1)) = X1,
inference(orient,[status(thm)],[t466]) ).
cnf(f3,axiom,
( def_10(Y_4,X_3)
| plus(Z_5,Y_4) = X_3
| minus(X_3,Y_4) != Z_5 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_4) ).
fof(f3_nnf,plain,
! [X_3,Y_4,Z_5] :
( def_10(Y_4,X_3)
| plus(Z_5,Y_4) = X_3
| minus(X_3,Y_4) != Z_5 ),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [X_3,Y_4,Z_5] :
( def_10(Y_4,X_3)
| plus(Z_5,Y_4) = X_3
| minus(X_3,Y_4) != Z_5 ),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
( def_10(X1,X0)
| plus(X2,X1) = X0
| minus(X0,X1) != X2 ),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(t54,plain,
ifeq(minus(X1,X2),X3,or(eq(plus(X3,X2),X1),def_10(X2,X1)),true) = true,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t2761,plain,
ifeq(minus(X1,X2),X3,or(eq(plus(X3,X2),X1),def_10(X2,X1)),sF2) = true,
inference(step,[status(thm)],[t54,t140]) ).
cnf(t2762,plain,
ifeq(minus(X1,X2),X3,or(eq(plus(X3,X2),X1),def_10(X2,X1)),sF2) = sF2,
inference(step,[status(thm)],[t2761,t140]) ).
cnf(t792,plain,
ifeq(minus(X1,X2),X3,or(eq(plus(X3,X2),X1),def_10(X2,X1)),sF2) = sF2,
inference(orient,[status(thm)],[t2762]) ).
cnf(t798,plain,
sF2 = or(eq(plus(minus(X1,X2),X2),X1),def_10(X2,X1)),
inference(cp,[status(thm)],[t792,t176]) ).
cnf(t1182,plain,
or(eq(plus(minus(X1,X2),X2),X1),def_10(X2,X1)) = sF2,
inference(orient,[status(thm)],[t798]) ).
cnf(t18,plain,
ifeq(not(X1),true,X1,false) = false,
introduced(definition) ).
cnf(t2542,plain,
ifeq(not(X1),sF2,X1,false) = false,
inference(step,[status(thm)],[t18,t140]) ).
cnf(t2543,plain,
ifeq(not(X1),sF2,X1,sF0) = false,
inference(step,[status(thm)],[t2542,t131]) ).
cnf(t2544,plain,
ifeq(not(X1),sF2,X1,sF0) = sF0,
inference(step,[status(thm)],[t2543,t131]) ).
cnf(t178,plain,
ifeq(not(X1),sF2,X1,sF0) = sF0,
inference(orient,[status(thm)],[t2544]) ).
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(t35,plain,
or(not(def_10(X1,X2)),not(gt(X2,X1))) = true,
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(t2601,plain,
or(not(def_10(X1,X2)),not(gt(X2,X1))) = sF2,
inference(step,[status(thm)],[t35,t140]) ).
cnf(t278,plain,
or(not(def_10(X1,X2)),not(gt(X2,X1))) = sF2,
inference(orient,[status(thm)],[t2601]) ).
cnf(f7,axiom,
( gt(plus(Y_12,n1),plus(X_11,n1))
| ~ gt(Y_12,X_11) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_8) ).
fof(f7_nnf,plain,
! [Y_12,X_11] :
( gt(plus(Y_12,n1),plus(X_11,n1))
| ~ gt(Y_12,X_11) ),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [Y_12,X_11] :
( gt(plus(Y_12,n1),plus(X_11,n1))
| ~ gt(Y_12,X_11) ),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
( gt(plus(X0,n1),plus(X1,n1))
| ~ gt(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(t45,plain,
ifeq(gt(X1,X2),true,gt(plus(X1,n1),plus(X2,n1)),true) = true,
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(t2664,plain,
ifeq(gt(X1,X2),sF2,gt(plus(X1,n1),plus(X2,n1)),true) = true,
inference(step,[status(thm)],[t45,t140]) ).
cnf(t2665,plain,
ifeq(gt(X1,X2),sF2,gt(plus(X1,n1),plus(X2,n1)),sF2) = true,
inference(step,[status(thm)],[t2664,t140]) ).
cnf(t2666,plain,
ifeq(gt(X1,X2),sF2,gt(plus(X1,n1),plus(X2,n1)),sF2) = sF2,
inference(step,[status(thm)],[t2665,t140]) ).
cnf(t480,plain,
ifeq(gt(X1,X2),sF2,gt(plus(X1,n1),plus(X2,n1)),sF2) = sF2,
inference(orient,[status(thm)],[t2666]) ).
cnf(f1,axiom,
gt(plus(X_1,n1),n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_2) ).
fof(f1_nnf,plain,
! [X_1] : gt(plus(X_1,n1),n0),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [X_1] : gt(plus(X_1,n1),n0),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
gt(plus(X0,n1),n0),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(t15,plain,
gt(plus(X1,n1),n0) = true,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t2537,plain,
gt(plus(X1,n1),n0) = sF2,
inference(step,[status(thm)],[t15,t140]) ).
cnf(t169,plain,
gt(plus(X1,n1),n0) = sF2,
inference(orient,[status(thm)],[t2537]) ).
cnf(t172,plain,
sF2 = gt(sF4,n0),
inference(cp,[status(thm)],[t169,t164]) ).
cnf(t175,plain,
gt(sF4,n0) = sF2,
inference(orient,[status(thm)],[t172]) ).
cnf(t490,plain,
sF2 = ifeq(sF2,sF2,gt(plus(sF4,n1),plus(n0,n1)),sF2),
inference(cp,[status(thm)],[t480,t175]) ).
cnf(t2671,plain,
sF2 = gt(plus(sF4,n1),plus(n0,n1)),
inference(step,[status(thm)],[t490,t176]) ).
cnf(f18,axiom,
plus(n0,X_31) = X_31,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_19) ).
fof(f18_nnf,plain,
! [X_31] : plus(n0,X_31) = X_31,
inference(nnf_transformation,[status(thm)],[f18]) ).
fof(f18_sk,plain,
! [X_31] : plus(n0,X_31) = X_31,
inference(skolemisation,[status(esa)],[f18_nnf]) ).
cnf(c18,plain,
plus(n0,X0) = X0,
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(t11,plain,
plus(n0,X1) = X1,
inference(equality_encoding,[status(esa)],[c18]) ).
cnf(t153,plain,
plus(n0,X1) = X1,
inference(orient,[status(thm)],[t11]) ).
cnf(t2672,plain,
sF2 = gt(plus(sF4,n1),n1),
inference(step,[status(thm)],[t2671,t153]) ).
cnf(t503,plain,
gt(plus(sF4,n1),n1) = sF2,
inference(orient,[status(thm)],[t2672]) ).
cnf(t504,plain,
sF2 = or(not(def_10(n1,plus(sF4,n1))),not(sF2)),
inference(cp,[status(thm)],[t278,t503]) ).
cnf(t1,plain,
not(true) = false,
introduced(definition) ).
cnf(t127,plain,
not(true) = false,
inference(orient,[status(thm)],[t1]) ).
cnf(t2509,plain,
not(true) = sF0,
inference(step,[status(thm)],[t127,t131]) ).
cnf(t133,plain,
not(true) = sF0,
inference(orient,[status(thm)],[t2509]) ).
cnf(t2517,plain,
not(sF2) = sF0,
inference(step,[status(thm)],[t133,t140]) ).
cnf(t141,plain,
not(sF2) = sF0,
inference(rw,[status(thm)],[t2517]) ).
cnf(t147,plain,
not(sF2) = sF0,
inference(orient,[status(thm)],[t141]) ).
cnf(t2679,plain,
sF2 = or(not(def_10(n1,plus(sF4,n1))),sF0),
inference(step,[status(thm)],[t504,t147]) ).
cnf(t7,plain,
or(X1,false) = X1,
introduced(definition) ).
cnf(t2523,plain,
or(X1,sF0) = X1,
inference(step,[status(thm)],[t7,t131]) ).
cnf(t149,plain,
or(X1,sF0) = X1,
inference(orient,[status(thm)],[t2523]) ).
cnf(t2680,plain,
sF2 = not(def_10(n1,plus(sF4,n1))),
inference(step,[status(thm)],[t2679,t149]) ).
cnf(t517,plain,
not(def_10(n1,plus(sF4,n1))) = sF2,
inference(orient,[status(thm)],[t2680]) ).
cnf(t518,plain,
sF0 = ifeq(sF2,sF2,def_10(n1,plus(sF4,n1)),sF0),
inference(cp,[status(thm)],[t178,t517]) ).
cnf(t2684,plain,
sF0 = def_10(n1,plus(sF4,n1)),
inference(step,[status(thm)],[t518,t176]) ).
cnf(t534,plain,
def_10(n1,plus(sF4,n1)) = sF0,
inference(orient,[status(thm)],[t2684]) ).
cnf(t1194,plain,
sF2 = or(eq(plus(minus(plus(sF4,n1),n1),n1),plus(sF4,n1)),sF0),
inference(cp,[status(thm)],[t1182,t534]) ).
cnf(t3172,plain,
sF2 = eq(plus(minus(plus(sF4,n1),n1),n1),plus(sF4,n1)),
inference(step,[status(thm)],[t1194,t149]) ).
cnf(t1937,plain,
eq(plus(minus(plus(sF4,n1),n1),n1),plus(sF4,n1)) = sF2,
inference(orient,[status(thm)],[t3172]) ).
cnf(t1938,plain,
plus(sF4,n1) = ifeq(sF2,sF2,plus(minus(plus(sF4,n1),n1),n1),plus(sF4,n1)),
inference(cp,[status(thm)],[t185,t1937]) ).
cnf(t3173,plain,
plus(sF4,n1) = plus(minus(plus(sF4,n1),n1),n1),
inference(step,[status(thm)],[t1938,t176]) ).
cnf(t1940,plain,
plus(minus(plus(sF4,n1),n1),n1) = plus(sF4,n1),
inference(orient,[status(thm)],[t3173]) ).
cnf(t1957,plain,
minus(plus(sF4,n1),n1) = y_27(plus(sF4,n1)),
inference(cp,[status(thm)],[t468,t1940]) ).
cnf(t3174,plain,
minus(plus(sF4,n1),n1) = sF4,
inference(step,[status(thm)],[t1957,t468]) ).
cnf(t2019,plain,
minus(plus(sF4,n1),n1) = sF4,
inference(orient,[status(thm)],[t3174]) ).
cnf(t2022,plain,
sF2 = ifeq(gt(plus(sF4,n1),n0),sF2,gt(plus(sF4,n1),sF4),sF2),
inference(cp,[status(thm)],[t407,t2019]) ).
cnf(t3176,plain,
sF2 = ifeq(sF2,sF2,gt(plus(sF4,n1),sF4),sF2),
inference(step,[status(thm)],[t2022,t169]) ).
cnf(t3177,plain,
sF2 = gt(plus(sF4,n1),sF4),
inference(step,[status(thm)],[t3176,t176]) ).
cnf(t2027,plain,
gt(plus(sF4,n1),sF4) = sF2,
inference(orient,[status(thm)],[t3177]) ).
cnf(t2034,plain,
sF2 = ifeq(sF2,sF2,gt(sF4,sF3),sF2),
inference(cp,[status(thm)],[t950,t2027]) ).
cnf(t3178,plain,
sF2 = gt(sF4,sF3),
inference(step,[status(thm)],[t2034,t176]) ).
cnf(t2036,plain,
gt(sF4,sF3) = sF2,
inference(orient,[status(thm)],[t3178]) ).
cnf(t3197,plain,
sF2 = ifeq(sF2,sF2,or(p_Reset(t_139),or(sF0,eq(int_level(plus(t_139,n1)),plus(int_level(t_139),n1)))),sF2),
inference(step,[status(thm)],[t3196,t2036]) ).
cnf(t3198,plain,
sF2 = or(p_Reset(t_139),or(sF0,eq(int_level(plus(t_139,n1)),plus(int_level(t_139),n1)))),
inference(step,[status(thm)],[t3197,t176]) ).
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(t3,plain,
p_Reset(t_139) = false,
inference(equality_encoding,[status(esa)],[c93]) ).
cnf(t129,plain,
p_Reset(t_139) = false,
inference(orient,[status(thm)],[t3]) ).
cnf(t2513,plain,
p_Reset(t_139) = sF0,
inference(step,[status(thm)],[t129,t131]) ).
cnf(t137,plain,
p_Reset(t_139) = sF0,
inference(orient,[status(thm)],[t2513]) ).
cnf(t3199,plain,
sF2 = or(sF0,or(sF0,eq(int_level(plus(t_139,n1)),plus(int_level(t_139),n1)))),
inference(step,[status(thm)],[t3198,t137]) ).
cnf(t3200,plain,
sF2 = or(sF0,eq(int_level(plus(t_139,n1)),plus(int_level(t_139),n1))),
inference(step,[status(thm)],[t3199,t151]) ).
cnf(t3201,plain,
sF2 = eq(int_level(plus(t_139,n1)),plus(int_level(t_139),n1)),
inference(step,[status(thm)],[t3200,t151]) ).
cnf(t120,axiom,
sF5 = plus(t_139,n1),
introduced(definition) ).
cnf(t154,plain,
plus(t_139,n1) = sF5,
inference(orient,[status(thm)],[t120]) ).
cnf(t3202,plain,
sF2 = eq(int_level(sF5),plus(int_level(t_139),n1)),
inference(step,[status(thm)],[t3201,t154]) ).
cnf(t121,axiom,
sF6 = int_level(plus(t_139,n1)),
introduced(definition) ).
cnf(t2536,plain,
sF6 = int_level(sF5),
inference(step,[status(thm)],[t121,t154]) ).
cnf(t168,plain,
int_level(sF5) = sF6,
inference(orient,[status(thm)],[t2536]) ).
cnf(t3203,plain,
sF2 = eq(sF6,plus(int_level(t_139),n1)),
inference(step,[status(thm)],[t3202,t168]) ).
cnf(t3204,plain,
sF2 = eq(sF6,plus(sF3,n1)),
inference(step,[status(thm)],[t3203,t144]) ).
cnf(t3205,plain,
sF2 = eq(sF6,sF4),
inference(step,[status(thm)],[t3204,t164]) ).
cnf(f94,negated_conjecture,
level(plus(t_139,n1)) != fifo_length,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quest_5) ).
fof(f94_nnf,plain,
level(plus(t_139,n1)) != fifo_length,
inference(nnf_transformation,[status(thm)],[f94]) ).
fof(f94_sk,plain,
level(plus(t_139,n1)) != fifo_length,
inference(skolemisation,[status(esa)],[f94_nnf]) ).
cnf(c94,plain,
level(plus(t_139,n1)) != fifo_length,
inference(cnf_transformation,[status(esa)],[f94_sk]) ).
cnf(u2,axiom,
eq(level(plus(t_139,n1)),fifo_length) = false,
inference(equality_encoding,[status(esa)],[c94]) ).
cnf(t17,plain,
eq(int_level(plus(t_139,n1)),fifo_length) = false,
inference(definition_unfolding,[status(thm)],[u2,d0]) ).
cnf(t2538,plain,
eq(int_level(sF5),fifo_length) = false,
inference(step,[status(thm)],[t17,t154]) ).
cnf(t2539,plain,
eq(sF6,fifo_length) = false,
inference(step,[status(thm)],[t2538,t168]) ).
cnf(t2540,plain,
eq(sF6,sF4) = false,
inference(step,[status(thm)],[t2539,t163]) ).
cnf(t2541,plain,
eq(sF6,sF4) = sF0,
inference(step,[status(thm)],[t2540,t131]) ).
cnf(t177,plain,
eq(sF6,sF4) = sF0,
inference(orient,[status(thm)],[t2541]) ).
cnf(t3206,plain,
sF2 = sF0,
inference(step,[status(thm)],[t3205,t177]) ).
cnf(t2082,plain,
sF2 = sF0,
inference(orient,[status(thm)],[t3206]) ).
cnf(t3209,plain,
true = sF0,
inference(step,[status(thm)],[t140,t2082]) ).
cnf(t2085,plain,
true = sF0,
inference(orient,[status(thm)],[t3209]) ).
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,c93,c94]) ).
cnf(g0_0,plain,
sF0 != false,
inference(rw,[status(thm)],[goal_0,t2085]) ).
cnf(g0_1,plain,
sF0 != sF0,
inference(rw,[status(thm)],[g0_0,t131]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV022-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 : n026.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:29:40 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 17.64/2.73 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 17.64/2.73 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------