%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : HWV023-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:07 PM UTC 2026
% Result : Unsatisfiable 13.40s 2.41s
% Output : Proof 13.40s
% Verified :
% Comments :
%------------------------------------------------------------------------------
cnf(t116,axiom,
sF1 = p_Rd(t_139),
introduced(definition) ).
cnf(f92,negated_conjecture,
p_Rd(t_139),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quest_3) ).
fof(f92_nnf,plain,
p_Rd(t_139),
inference(nnf_transformation,[status(thm)],[f92]) ).
cnf(c92,plain,
p_Rd(t_139),
inference(cnf_transformation,[status(esa)],[f92_nnf]) ).
cnf(t3,plain,
p_Rd(t_139) = true,
inference(equality_encoding,[status(esa)],[c92]) ).
cnf(t127,plain,
p_Rd(t_139) = true,
inference(orient,[status(thm)],[t3]) ).
cnf(t1858,plain,
sF1 = true,
inference(step,[status(thm)],[t116,t127]) ).
cnf(t133,plain,
true = sF1,
inference(orient,[status(thm)],[t1858]) ).
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(t128,plain,
p_Reset(t_139) = false,
inference(orient,[status(thm)],[t4]) ).
cnf(t1864,plain,
sF2 = false,
inference(step,[status(thm)],[t117,t128]) ).
cnf(t139,plain,
false = sF2,
inference(orient,[status(thm)],[t1864]) ).
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(t24,plain,
ifeq(int_level(X1),n0,p_Empty(X1),true) = true,
inference(equality_encoding,[status(esa)],[c23]) ).
cnf(t1912,plain,
ifeq(int_level(X1),n0,p_Empty(X1),sF1) = true,
inference(step,[status(thm)],[t24,t133]) ).
cnf(t1913,plain,
ifeq(int_level(X1),n0,p_Empty(X1),sF1) = sF1,
inference(step,[status(thm)],[t1912,t133]) ).
cnf(t184,plain,
ifeq(int_level(X1),n0,p_Empty(X1),sF1) = sF1,
inference(orient,[status(thm)],[t1913]) ).
cnf(t21,plain,
ifeq(eq(X1,X2),true,X1,X2) = X2,
introduced(definition) ).
cnf(t1909,plain,
ifeq(eq(X1,X2),sF1,X1,X2) = X2,
inference(step,[status(thm)],[t21,t133]) ).
cnf(t175,plain,
ifeq(eq(X1,X2),sF1,X1,X2) = X2,
inference(orient,[status(thm)],[t1909]) ).
cnf(f70,axiom,
( int_level(plus(X_t_42,n1)) = minus(int_level(X_t_42),n1)
| ~ 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_71) ).
fof(f70_nnf,plain,
! [X_t_42] :
( int_level(plus(X_t_42,n1)) = minus(int_level(X_t_42),n1)
| ~ 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)],[f70]) ).
fof(f70_sk,plain,
! [X_t_42] :
( int_level(plus(X_t_42,n1)) = minus(int_level(X_t_42),n1)
| ~ 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)],[f70_nnf]) ).
cnf(c70,plain,
( int_level(plus(X0,n1)) = minus(int_level(X0),n1)
| ~ gt(int_level(X0),n0)
| ~ p_Rd(X0)
| p_Wr(X0)
| p_Reset(X0) ),
inference(cnf_transformation,[status(esa)],[f70_sk]) ).
cnf(t88,plain,
ifeq(p_Rd(X1),true,ifeq(gt(int_level(X1),n0),true,or(p_Reset(X1),or(p_Wr(X1),eq(int_level(plus(X1,n1)),minus(int_level(X1),n1)))),true),true) = true,
inference(equality_encoding,[status(esa)],[c70]) ).
cnf(t2504,plain,
ifeq(p_Rd(X1),sF1,ifeq(gt(int_level(X1),n0),true,or(p_Reset(X1),or(p_Wr(X1),eq(int_level(plus(X1,n1)),minus(int_level(X1),n1)))),true),true) = true,
inference(step,[status(thm)],[t88,t133]) ).
cnf(t2505,plain,
ifeq(p_Rd(X1),sF1,ifeq(gt(int_level(X1),n0),sF1,or(p_Reset(X1),or(p_Wr(X1),eq(int_level(plus(X1,n1)),minus(int_level(X1),n1)))),true),true) = true,
inference(step,[status(thm)],[t2504,t133]) ).
cnf(t115,axiom,
sF0 = int_level(t_139),
introduced(definition) ).
cnf(f90,negated_conjecture,
level(t_139) = n1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quest_1) ).
fof(f90_nnf,plain,
level(t_139) = n1,
inference(nnf_transformation,[status(thm)],[f90]) ).
cnf(c90,plain,
level(t_139) = n1,
inference(cnf_transformation,[status(esa)],[f90_nnf]) ).
cnf(u0,axiom,
level(t_139) = n1,
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(t0,plain,
int_level(t_139) = n1,
inference(definition_unfolding,[status(thm)],[u0,d0]) ).
cnf(t124,plain,
int_level(t_139) = n1,
inference(orient,[status(thm)],[t0]) ).
cnf(t1855,plain,
sF0 = n1,
inference(step,[status(thm)],[t115,t124]) ).
cnf(t130,plain,
n1 = sF0,
inference(orient,[status(thm)],[t1855]) ).
cnf(t2506,plain,
ifeq(p_Rd(X1),sF1,ifeq(gt(int_level(X1),n0),sF1,or(p_Reset(X1),or(p_Wr(X1),eq(int_level(plus(X1,sF0)),minus(int_level(X1),n1)))),true),true) = true,
inference(step,[status(thm)],[t2505,t130]) ).
cnf(t2507,plain,
ifeq(p_Rd(X1),sF1,ifeq(gt(int_level(X1),n0),sF1,or(p_Reset(X1),or(p_Wr(X1),eq(int_level(plus(X1,sF0)),minus(int_level(X1),sF0)))),true),true) = true,
inference(step,[status(thm)],[t2506,t130]) ).
cnf(t2508,plain,
ifeq(p_Rd(X1),sF1,ifeq(gt(int_level(X1),n0),sF1,or(p_Reset(X1),or(p_Wr(X1),eq(int_level(plus(X1,sF0)),minus(int_level(X1),sF0)))),sF1),true) = true,
inference(step,[status(thm)],[t2507,t133]) ).
cnf(t2509,plain,
ifeq(p_Rd(X1),sF1,ifeq(gt(int_level(X1),n0),sF1,or(p_Reset(X1),or(p_Wr(X1),eq(int_level(plus(X1,sF0)),minus(int_level(X1),sF0)))),sF1),sF1) = true,
inference(step,[status(thm)],[t2508,t133]) ).
cnf(t2510,plain,
ifeq(p_Rd(X1),sF1,ifeq(gt(int_level(X1),n0),sF1,or(p_Reset(X1),or(p_Wr(X1),eq(int_level(plus(X1,sF0)),minus(int_level(X1),sF0)))),sF1),sF1) = sF1,
inference(step,[status(thm)],[t2509,t133]) ).
cnf(t1685,plain,
ifeq(p_Rd(X1),sF1,ifeq(gt(int_level(X1),n0),sF1,or(p_Reset(X1),or(p_Wr(X1),eq(int_level(plus(X1,sF0)),minus(int_level(X1),sF0)))),sF1),sF1) = sF1,
inference(orient,[status(thm)],[t2510]) ).
cnf(t1856,plain,
int_level(t_139) = sF0,
inference(step,[status(thm)],[t124,t130]) ).
cnf(t131,plain,
int_level(t_139) = sF0,
inference(orient,[status(thm)],[t1856]) ).
cnf(t1686,plain,
sF1 = ifeq(p_Rd(t_139),sF1,ifeq(gt(sF0,n0),sF1,or(p_Reset(t_139),or(p_Wr(t_139),eq(int_level(plus(t_139,sF0)),minus(int_level(t_139),sF0)))),sF1),sF1),
inference(cp,[status(thm)],[t1685,t131]) ).
cnf(t1862,plain,
p_Rd(t_139) = sF1,
inference(step,[status(thm)],[t127,t133]) ).
cnf(t137,plain,
p_Rd(t_139) = sF1,
inference(orient,[status(thm)],[t1862]) ).
cnf(t2511,plain,
sF1 = ifeq(sF1,sF1,ifeq(gt(sF0,n0),sF1,or(p_Reset(t_139),or(p_Wr(t_139),eq(int_level(plus(t_139,sF0)),minus(int_level(t_139),sF0)))),sF1),sF1),
inference(step,[status(thm)],[t1686,t137]) ).
cnf(t17,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t168,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t17]) ).
cnf(t2512,plain,
sF1 = ifeq(gt(sF0,n0),sF1,or(p_Reset(t_139),or(p_Wr(t_139),eq(int_level(plus(t_139,sF0)),minus(int_level(t_139),sF0)))),sF1),
inference(step,[status(thm)],[t2511,t168]) ).
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(t16,plain,
gt(plus(X1,n1),n0) = true,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t1889,plain,
gt(plus(X1,sF0),n0) = true,
inference(step,[status(thm)],[t16,t130]) ).
cnf(t1890,plain,
gt(plus(X1,sF0),n0) = sF1,
inference(step,[status(thm)],[t1889,t133]) ).
cnf(t163,plain,
gt(plus(X1,sF0),n0) = sF1,
inference(orient,[status(thm)],[t1890]) ).
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(t12,plain,
plus(n0,X1) = X1,
inference(equality_encoding,[status(esa)],[c18]) ).
cnf(t154,plain,
plus(n0,X1) = X1,
inference(orient,[status(thm)],[t12]) ).
cnf(t164,plain,
sF1 = gt(sF0,n0),
inference(cp,[status(thm)],[t163,t154]) ).
cnf(t166,plain,
gt(sF0,n0) = sF1,
inference(orient,[status(thm)],[t164]) ).
cnf(t2513,plain,
sF1 = ifeq(sF1,sF1,or(p_Reset(t_139),or(p_Wr(t_139),eq(int_level(plus(t_139,sF0)),minus(int_level(t_139),sF0)))),sF1),
inference(step,[status(thm)],[t2512,t166]) ).
cnf(t2514,plain,
sF1 = or(p_Reset(t_139),or(p_Wr(t_139),eq(int_level(plus(t_139,sF0)),minus(int_level(t_139),sF0)))),
inference(step,[status(thm)],[t2513,t168]) ).
cnf(t1866,plain,
p_Reset(t_139) = sF2,
inference(step,[status(thm)],[t128,t139]) ).
cnf(t141,plain,
p_Reset(t_139) = sF2,
inference(orient,[status(thm)],[t1866]) ).
cnf(t2515,plain,
sF1 = or(sF2,or(p_Wr(t_139),eq(int_level(plus(t_139,sF0)),minus(int_level(t_139),sF0)))),
inference(step,[status(thm)],[t2514,t141]) ).
cnf(t10,plain,
or(false,X1) = X1,
introduced(definition) ).
cnf(t1877,plain,
or(sF2,X1) = X1,
inference(step,[status(thm)],[t10,t139]) ).
cnf(t152,plain,
or(sF2,X1) = X1,
inference(orient,[status(thm)],[t1877]) ).
cnf(t2516,plain,
sF1 = or(p_Wr(t_139),eq(int_level(plus(t_139,sF0)),minus(int_level(t_139),sF0))),
inference(step,[status(thm)],[t2515,t152]) ).
cnf(f91,negated_conjecture,
~ p_Wr(t_139),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quest_2) ).
fof(f91_nnf,plain,
~ p_Wr(t_139),
inference(nnf_transformation,[status(thm)],[f91]) ).
fof(f91_sk,plain,
~ p_Wr(t_139),
inference(skolemisation,[status(esa)],[f91_nnf]) ).
cnf(c91,plain,
~ p_Wr(t_139),
inference(cnf_transformation,[status(esa)],[f91_sk]) ).
cnf(t5,plain,
p_Wr(t_139) = false,
inference(equality_encoding,[status(esa)],[c91]) ).
cnf(t129,plain,
p_Wr(t_139) = false,
inference(orient,[status(thm)],[t5]) ).
cnf(t1868,plain,
p_Wr(t_139) = sF2,
inference(step,[status(thm)],[t129,t139]) ).
cnf(t143,plain,
p_Wr(t_139) = sF2,
inference(orient,[status(thm)],[t1868]) ).
cnf(t2517,plain,
sF1 = or(sF2,eq(int_level(plus(t_139,sF0)),minus(int_level(t_139),sF0))),
inference(step,[status(thm)],[t2516,t143]) ).
cnf(t2518,plain,
sF1 = eq(int_level(plus(t_139,sF0)),minus(int_level(t_139),sF0)),
inference(step,[status(thm)],[t2517,t152]) ).
cnf(t119,axiom,
sF4 = plus(t_139,n1),
introduced(definition) ).
cnf(t1880,plain,
sF4 = plus(t_139,sF0),
inference(step,[status(thm)],[t119,t130]) ).
cnf(t155,plain,
plus(t_139,sF0) = sF4,
inference(orient,[status(thm)],[t1880]) ).
cnf(t2519,plain,
sF1 = eq(int_level(sF4),minus(int_level(t_139),sF0)),
inference(step,[status(thm)],[t2518,t155]) ).
cnf(t2520,plain,
sF1 = eq(int_level(sF4),minus(sF0,sF0)),
inference(step,[status(thm)],[t2519,t131]) ).
cnf(f4,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_5) ).
fof(f4_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)],[f4]) ).
fof(f4_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)],[f4_nnf]) ).
cnf(c4,plain,
( def_10(X1,X0)
| plus(X2,X1) != X0
| minus(X0,X1) = X2 ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(t58,plain,
ifeq(plus(X1,X2),X3,or(eq(minus(X3,X2),X1),def_10(X2,X3)),true) = true,
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t2145,plain,
ifeq(plus(X1,X2),X3,or(eq(minus(X3,X2),X1),def_10(X2,X3)),sF1) = true,
inference(step,[status(thm)],[t58,t133]) ).
cnf(t2146,plain,
ifeq(plus(X1,X2),X3,or(eq(minus(X3,X2),X1),def_10(X2,X3)),sF1) = sF1,
inference(step,[status(thm)],[t2145,t133]) ).
cnf(t762,plain,
ifeq(plus(X1,X2),X3,or(eq(minus(X3,X2),X1),def_10(X2,X3)),sF1) = sF1,
inference(orient,[status(thm)],[t2146]) ).
cnf(t18,plain,
ifeq(not(X1),true,X1,false) = false,
introduced(definition) ).
cnf(t1891,plain,
ifeq(not(X1),sF1,X1,false) = false,
inference(step,[status(thm)],[t18,t133]) ).
cnf(t1892,plain,
ifeq(not(X1),sF1,X1,sF2) = false,
inference(step,[status(thm)],[t1891,t139]) ).
cnf(t1893,plain,
ifeq(not(X1),sF1,X1,sF2) = sF2,
inference(step,[status(thm)],[t1892,t139]) ).
cnf(t169,plain,
ifeq(not(X1),sF1,X1,sF2) = sF2,
inference(orient,[status(thm)],[t1893]) ).
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(t34,plain,
or(not(def_10(X1,X2)),not(eq(X2,X1))) = true,
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t1938,plain,
or(not(def_10(X1,X2)),not(eq(X2,X1))) = sF1,
inference(step,[status(thm)],[t34,t133]) ).
cnf(t231,plain,
or(not(def_10(X1,X2)),not(eq(X2,X1))) = sF1,
inference(orient,[status(thm)],[t1938]) ).
cnf(t6,plain,
eq(X1,X1) = true,
introduced(definition) ).
cnf(t1871,plain,
eq(X1,X1) = sF1,
inference(step,[status(thm)],[t6,t133]) ).
cnf(t146,plain,
eq(X1,X1) = sF1,
inference(orient,[status(thm)],[t1871]) ).
cnf(t232,plain,
sF1 = or(not(def_10(X1,X1)),not(sF1)),
inference(cp,[status(thm)],[t231,t146]) ).
cnf(t2,plain,
not(true) = false,
introduced(definition) ).
cnf(t126,plain,
not(true) = false,
inference(orient,[status(thm)],[t2]) ).
cnf(t1861,plain,
not(sF1) = false,
inference(step,[status(thm)],[t126,t133]) ).
cnf(t136,plain,
not(sF1) = false,
inference(rw,[status(thm)],[t1861]) ).
cnf(t1872,plain,
not(sF1) = sF2,
inference(step,[status(thm)],[t136,t139]) ).
cnf(t147,plain,
not(sF1) = sF2,
inference(orient,[status(thm)],[t1872]) ).
cnf(t1939,plain,
sF1 = or(not(def_10(X1,X1)),sF2),
inference(step,[status(thm)],[t232,t147]) ).
cnf(t8,plain,
or(X1,false) = X1,
introduced(definition) ).
cnf(t1874,plain,
or(X1,sF2) = X1,
inference(step,[status(thm)],[t8,t139]) ).
cnf(t150,plain,
or(X1,sF2) = X1,
inference(orient,[status(thm)],[t1874]) ).
cnf(t1940,plain,
sF1 = not(def_10(X1,X1)),
inference(step,[status(thm)],[t1939,t150]) ).
cnf(t233,plain,
not(def_10(X1,X1)) = sF1,
inference(orient,[status(thm)],[t1940]) ).
cnf(t234,plain,
sF2 = ifeq(sF1,sF1,def_10(X1,X1),sF2),
inference(cp,[status(thm)],[t169,t233]) ).
cnf(t1941,plain,
sF2 = def_10(X1,X1),
inference(step,[status(thm)],[t234,t168]) ).
cnf(t235,plain,
def_10(X1,X1) = sF2,
inference(orient,[status(thm)],[t1941]) ).
cnf(t767,plain,
sF1 = ifeq(plus(X1,X2),X2,or(eq(minus(X2,X2),X1),sF2),sF1),
inference(cp,[status(thm)],[t762,t235]) ).
cnf(t2237,plain,
sF1 = ifeq(plus(X1,X2),X2,eq(minus(X2,X2),X1),sF1),
inference(step,[status(thm)],[t767,t150]) ).
cnf(t1019,plain,
ifeq(plus(X1,X2),X2,eq(minus(X2,X2),X1),sF1) = sF1,
inference(orient,[status(thm)],[t2237]) ).
cnf(t1020,plain,
sF1 = ifeq(X1,X1,eq(minus(X1,X1),n0),sF1),
inference(cp,[status(thm)],[t1019,t154]) ).
cnf(t2238,plain,
sF1 = eq(minus(X1,X1),n0),
inference(step,[status(thm)],[t1020,t168]) ).
cnf(t1023,plain,
eq(minus(X1,X1),n0) = sF1,
inference(orient,[status(thm)],[t2238]) ).
cnf(t1024,plain,
n0 = ifeq(sF1,sF1,minus(X1,X1),n0),
inference(cp,[status(thm)],[t175,t1023]) ).
cnf(t2239,plain,
n0 = minus(X1,X1),
inference(step,[status(thm)],[t1024,t168]) ).
cnf(t1027,plain,
minus(X1,X1) = n0,
inference(orient,[status(thm)],[t2239]) ).
cnf(t2521,plain,
sF1 = eq(int_level(sF4),n0),
inference(step,[status(thm)],[t2520,t1027]) ).
cnf(t1688,plain,
eq(int_level(sF4),n0) = sF1,
inference(orient,[status(thm)],[t2521]) ).
cnf(t1689,plain,
n0 = ifeq(sF1,sF1,int_level(sF4),n0),
inference(cp,[status(thm)],[t175,t1688]) ).
cnf(t2522,plain,
n0 = int_level(sF4),
inference(step,[status(thm)],[t1689,t168]) ).
cnf(t1692,plain,
int_level(sF4) = n0,
inference(orient,[status(thm)],[t2522]) ).
cnf(t1698,plain,
sF1 = ifeq(n0,n0,p_Empty(sF4),sF1),
inference(cp,[status(thm)],[t184,t1692]) ).
cnf(t2524,plain,
sF1 = p_Empty(sF4),
inference(step,[status(thm)],[t1698,t168]) ).
cnf(f94,negated_conjecture,
~ p_Empty(plus(t_139,n1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quest_5) ).
fof(f94_nnf,plain,
~ p_Empty(plus(t_139,n1)),
inference(nnf_transformation,[status(thm)],[f94]) ).
fof(f94_sk,plain,
~ p_Empty(plus(t_139,n1)),
inference(skolemisation,[status(esa)],[f94_nnf]) ).
cnf(c94,plain,
~ p_Empty(plus(t_139,n1)),
inference(cnf_transformation,[status(esa)],[f94_sk]) ).
cnf(t14,plain,
p_Empty(plus(t_139,n1)) = false,
inference(equality_encoding,[status(esa)],[c94]) ).
cnf(t1881,plain,
p_Empty(plus(t_139,sF0)) = false,
inference(step,[status(thm)],[t14,t130]) ).
cnf(t1882,plain,
p_Empty(sF4) = false,
inference(step,[status(thm)],[t1881,t155]) ).
cnf(t1883,plain,
p_Empty(sF4) = sF2,
inference(step,[status(thm)],[t1882,t139]) ).
cnf(t156,plain,
p_Empty(sF4) = sF2,
inference(orient,[status(thm)],[t1883]) ).
cnf(t2525,plain,
sF1 = sF2,
inference(step,[status(thm)],[t2524,t156]) ).
cnf(t1713,plain,
sF2 = sF1,
inference(orient,[status(thm)],[t2525]) ).
cnf(t2530,plain,
false = sF1,
inference(step,[status(thm)],[t139,t1713]) ).
cnf(t1718,plain,
false = sF1,
inference(orient,[status(thm)],[t2530]) ).
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(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,
sF1 != false,
inference(rw,[status(thm)],[goal_0,t133]) ).
cnf(g0_1,plain,
sF1 != sF1,
inference(rw,[status(thm)],[g0_0,t1718]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV023-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.11/0.38 % Computer : n026.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Wed Sep 23 16:29:53 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 13.40/2.41 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 13.40/2.41 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------