%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : NUM841+1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n018.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 02:21:09 PM UTC 2026
% Result : Theorem 92.66s 12.26s
% Output : Proof 92.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 19
% Syntax : Number of formulae : 99 ( 51 unt; 0 def)
% Number of atoms : 170 ( 77 equ)
% Maximal formula atoms : 6 ( 1 avg)
% Number of connectives : 169 ( 98 ~; 56 |; 9 &)
% ( 1 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 7 con; 0-4 aty)
% Number of variables : 171 ( 6 sgn 107 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f22,axiom,
! [Vd208,Vd209] :
( greater(Vd208,Vd209)
=> less(Vd209,Vd208) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qtd22) ).
fof(f22_nnf,plain,
! [Vd208,Vd209] :
( less(Vd209,Vd208)
| ~ greater(Vd208,Vd209) ),
inference(nnf_transformation,[status(thm)],[f22]) ).
fof(f22_sk,plain,
! [Vd208,Vd209] :
( less(Vd209,Vd208)
| ~ greater(Vd208,Vd209) ),
inference(skolemisation,[status(esa)],[f22_nnf]) ).
cnf(c27,plain,
( less(X1,X0)
| ~ greater(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f22_sk]) ).
cnf(hi26,axiom,
ifeq(greater(X0,X1),true,less(X1,X0),true) = true,
inference(equality_encoding,[status(esa)],[c27]) ).
fof(f6,axiom,
greater(vd344,vd345),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qtd6) ).
fof(f6_nnf,plain,
greater(vd344,vd345),
inference(nnf_transformation,[status(thm)],[f6]) ).
cnf(c6,plain,
greater(vd344,vd345),
inference(cnf_transformation,[status(esa)],[f6_nnf]) ).
cnf(hi5,axiom,
greater(vd344,vd345) = true,
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(h20,plain,
less(vd345,vd344) = true,
inference(hyper_resolution,[status(thm)],[hi26,hi5]) ).
fof(f10,axiom,
! [Vd301,Vd302,Vd303] :
( less(Vd301,Vd302)
=> less(vplus(Vd301,Vd303),vplus(Vd302,Vd303)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qtd10) ).
fof(f10_nnf,plain,
! [Vd301,Vd302,Vd303] :
( less(vplus(Vd301,Vd303),vplus(Vd302,Vd303))
| ~ less(Vd301,Vd302) ),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [Vd301,Vd302,Vd303] :
( less(vplus(Vd301,Vd303),vplus(Vd302,Vd303))
| ~ less(Vd301,Vd302) ),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c10,plain,
( less(vplus(X0,X2),vplus(X1,X2))
| ~ less(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(hi9,axiom,
ifeq(less(X0,X1),true,less(vplus(X0,X2),vplus(X1,X2)),true) = true,
inference(equality_encoding,[status(esa)],[c10]) ).
cnf(h73,plain,
less(vplus(vd345,V0),vplus(vd344,V0)) = true,
inference(hyper_resolution,[status(thm)],[hi9,h20]) ).
fof(f19,axiom,
! [Vd249,Vd250] :
( leq(Vd250,Vd249)
<=> ( Vd250 = Vd249
| less(Vd250,Vd249) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qtd19) ).
fof(f19_nnf,plain,
! [Vd249,Vd250] :
( ( ( Vd250 != Vd249
& ~ less(Vd250,Vd249) )
| leq(Vd250,Vd249) )
& ( Vd250 = Vd249
| less(Vd250,Vd249)
| ~ leq(Vd250,Vd249) ) ),
inference(nnf_transformation,[status(thm)],[f19]) ).
fof(f19_sk,plain,
! [Vd250,Vd249] :
( ( ( Vd250 != Vd249
& ~ less(Vd250,Vd249) )
| leq(Vd250,Vd249) )
& ( Vd250 = Vd249
| less(Vd250,Vd249)
| ~ leq(Vd250,Vd249) ) ),
inference(skolemisation,[status(esa)],[f19_nnf]) ).
cnf(c22,plain,
( X1 != X0
| leq(X1,X0) ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(hi21,axiom,
ifeq(X0,X1,leq(X0,X1),true) = true,
inference(equality_encoding,[status(esa)],[c22]) ).
fof(f35,axiom,
! [Vd78,Vd79] : vplus(Vd79,Vd78) = vplus(Vd78,Vd79),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qtd35) ).
fof(f35_nnf,plain,
! [Vd78,Vd79] : vplus(Vd79,Vd78) = vplus(Vd78,Vd79),
inference(nnf_transformation,[status(thm)],[f35]) ).
fof(f35_sk,plain,
! [Vd79,Vd78] : vplus(Vd79,Vd78) = vplus(Vd78,Vd79),
inference(skolemisation,[status(esa)],[f35_nnf]) ).
cnf(c42,plain,
vplus(X1,X0) = vplus(X0,X1),
inference(cnf_transformation,[status(esa)],[f35_sk]) ).
cnf(hi34,axiom,
vplus(X0,X1) = vplus(X1,X0),
inference(equality_encoding,[status(esa)],[c42]) ).
cnf(h187,plain,
leq(vplus(V0,V1),vplus(V1,V0)) = true,
inference(hyper_resolution,[status(thm)],[hi21,hi34]) ).
fof(f15,axiom,
! [Vd281,Vd282,Vd283] :
( ( ( less(Vd281,Vd282)
& leq(Vd282,Vd283) )
| ( leq(Vd281,Vd282)
& less(Vd282,Vd283) ) )
=> less(Vd281,Vd283) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qtd15) ).
fof(f15_nnf,plain,
! [Vd281,Vd282,Vd283] :
( less(Vd281,Vd283)
| ( ( ~ less(Vd281,Vd282)
| ~ leq(Vd282,Vd283) )
& ( ~ leq(Vd281,Vd282)
| ~ less(Vd282,Vd283) ) ) ),
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
! [Vd282,Vd283,Vd281] :
( less(Vd281,Vd283)
| ( ( ~ less(Vd281,Vd282)
| ~ leq(Vd282,Vd283) )
& ( ~ leq(Vd281,Vd282)
| ~ less(Vd282,Vd283) ) ) ),
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c16,plain,
( less(X0,X2)
| ~ less(X0,X1)
| ~ leq(X1,X2) ),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(hi15,axiom,
ifeq(leq(X0,X1),true,ifeq(less(X2,X0),true,less(X2,X1),true),true) = true,
inference(equality_encoding,[status(esa)],[c16]) ).
cnf(h3785,plain,
less(vplus(vd345,V0),vplus(V0,vd344)) = true,
inference(hyper_resolution,[status(thm)],[hi15,h187,h73]) ).
fof(f5,axiom,
greater(vd347,vd348),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qtd5) ).
fof(f5_nnf,plain,
greater(vd347,vd348),
inference(nnf_transformation,[status(thm)],[f5]) ).
cnf(c5,plain,
greater(vd347,vd348),
inference(cnf_transformation,[status(esa)],[f5_nnf]) ).
cnf(hi4,axiom,
greater(vd347,vd348) = true,
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(h11,plain,
less(vd348,vd347) = true,
inference(hyper_resolution,[status(thm)],[hi26,hi4]) ).
cnf(h59,plain,
less(vplus(vd348,V0),vplus(vd347,V0)) = true,
inference(hyper_resolution,[status(thm)],[hi9,h11]) ).
cnf(h3786,plain,
less(vplus(vd348,V0),vplus(V0,vd347)) = true,
inference(hyper_resolution,[status(thm)],[hi15,h187,h59]) ).
fof(f16,axiom,
! [Vd262,Vd263,Vd265] :
( ( less(Vd262,Vd263)
& less(Vd263,Vd265) )
=> less(Vd262,Vd265) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qtd16) ).
fof(f16_nnf,plain,
! [Vd262,Vd263,Vd265] :
( less(Vd262,Vd265)
| ~ less(Vd262,Vd263)
| ~ less(Vd263,Vd265) ),
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
! [Vd263,Vd265,Vd262] :
( less(Vd262,Vd265)
| ~ less(Vd262,Vd263)
| ~ less(Vd263,Vd265) ),
inference(skolemisation,[status(esa)],[f16_nnf]) ).
cnf(c17,plain,
( less(X0,X2)
| ~ less(X0,X1)
| ~ less(X1,X2) ),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(hi16,axiom,
ifeq(less(X0,X1),true,ifeq(less(X2,X0),true,less(X2,X1),true),true) = true,
inference(equality_encoding,[status(esa)],[c17]) ).
cnf(h70811,plain,
less(vplus(vd345,vd348),vplus(vd344,vd347)) = true,
inference(hyper_resolution,[status(thm)],[hi16,h3786,h3785]) ).
fof(f21,axiom,
! [Vd226,Vd227] :
( less(Vd226,Vd227)
=> greater(Vd227,Vd226) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qtd21) ).
fof(f21_nnf,plain,
! [Vd226,Vd227] :
( greater(Vd227,Vd226)
| ~ less(Vd226,Vd227) ),
inference(nnf_transformation,[status(thm)],[f21]) ).
fof(f21_sk,plain,
! [Vd226,Vd227] :
( greater(Vd227,Vd226)
| ~ less(Vd226,Vd227) ),
inference(skolemisation,[status(esa)],[f21_nnf]) ).
cnf(c26,plain,
( greater(X1,X0)
| ~ less(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f21_sk]) ).
cnf(hi25,axiom,
ifeq(less(X0,X1),true,greater(X1,X0),true) = true,
inference(equality_encoding,[status(esa)],[c26]) ).
cnf(h83796,plain,
greater(vplus(vd344,vd347),vplus(vd345,vd348)) = true,
inference(hyper_resolution,[status(thm)],[hi25,h70811]) ).
fof(f0,conjecture,
greater(vplus(vd344,vd347),vplus(vd345,vd348)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qtd0) ).
fof(f0_neg,negated_conjecture,
~ greater(vplus(vd344,vd347),vplus(vd345,vd348)),
inference(negated_conjecture,[status(cth)],[f0]) ).
fof(f0_nnf,plain,
~ greater(vplus(vd344,vd347),vplus(vd345,vd348)),
inference(nnf_transformation,[status(thm)],[f0_neg]) ).
fof(f0_sk,plain,
~ greater(vplus(vd344,vd347),vplus(vd345,vd348)),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
~ greater(vplus(vd344,vd347),vplus(vd345,vd348)),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(hi43,negated_conjecture,
ifeq(greater(vplus(vd344,vd347),vplus(vd345,vd348)),true,false,true) = true,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t0,plain,
true = false,
inference(hyper_resolution,[status(thm)],[hi43,h83796]) ).
cnf(t263,plain,
false = true,
inference(orient,[status(thm)],[t0]) ).
fof(f24,axiom,
! [Vd203,Vd204] :
( ~ less(Vd203,Vd204)
| Vd203 != Vd204 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qtd24) ).
fof(f24_nnf,plain,
! [Vd203,Vd204] :
( ~ less(Vd203,Vd204)
| Vd203 != Vd204 ),
inference(nnf_transformation,[status(thm)],[f24]) ).
fof(f24_sk,plain,
! [Vd203,Vd204] :
( ~ less(Vd203,Vd204)
| Vd203 != Vd204 ),
inference(skolemisation,[status(esa)],[f24_nnf]) ).
cnf(c29,plain,
( ~ less(X0,X1)
| X0 != X1 ),
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
fof(f25,axiom,
! [Vd203,Vd204] :
( ~ less(Vd203,Vd204)
| ~ greater(Vd203,Vd204) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qtd25) ).
fof(f25_nnf,plain,
! [Vd203,Vd204] :
( ~ less(Vd203,Vd204)
| ~ greater(Vd203,Vd204) ),
inference(nnf_transformation,[status(thm)],[f25]) ).
fof(f25_sk,plain,
! [Vd203,Vd204] :
( ~ less(Vd203,Vd204)
| ~ greater(Vd203,Vd204) ),
inference(skolemisation,[status(esa)],[f25_nnf]) ).
cnf(c30,plain,
( ~ less(X0,X1)
| ~ greater(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f25_sk]) ).
fof(f26,axiom,
! [Vd203,Vd204] :
( ~ greater(Vd203,Vd204)
| Vd203 != Vd204 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qtd26) ).
fof(f26_nnf,plain,
! [Vd203,Vd204] :
( ~ greater(Vd203,Vd204)
| Vd203 != Vd204 ),
inference(nnf_transformation,[status(thm)],[f26]) ).
fof(f26_sk,plain,
! [Vd203,Vd204] :
( ~ greater(Vd203,Vd204)
| Vd203 != Vd204 ),
inference(skolemisation,[status(esa)],[f26_nnf]) ).
cnf(c31,plain,
( ~ greater(X0,X1)
| X0 != X1 ),
inference(cnf_transformation,[status(esa)],[f26_sk]) ).
fof(f30,axiom,
! [Vd120,Vd121] :
( ~ ? [Vd125] : Vd121 = vplus(Vd120,Vd125)
| Vd120 != Vd121 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qtd30) ).
fof(f30_nnf,plain,
! [Vd120,Vd121] :
( ! [Vd125] : Vd121 != vplus(Vd120,Vd125)
| Vd120 != Vd121 ),
inference(nnf_transformation,[status(thm)],[f30]) ).
fof(f30_sk,plain,
! [Vd120,Vd121,Vd125] :
( Vd121 != vplus(Vd120,Vd125)
| Vd120 != Vd121 ),
inference(skolemisation,[status(esa)],[f30_nnf]) ).
cnf(c37,plain,
( X1 != vplus(X0,X2)
| X0 != X1 ),
inference(cnf_transformation,[status(esa)],[f30_sk]) ).
fof(f31,axiom,
! [Vd120,Vd121] :
( ~ ? [Vd125] : Vd121 = vplus(Vd120,Vd125)
| ~ ? [Vd123] : Vd120 = vplus(Vd121,Vd123) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qtd31) ).
fof(f31_nnf,plain,
! [Vd120,Vd121] :
( ! [Vd125] : Vd121 != vplus(Vd120,Vd125)
| ! [Vd123] : Vd120 != vplus(Vd121,Vd123) ),
inference(nnf_transformation,[status(thm)],[f31]) ).
fof(f31_sk,plain,
! [Vd120,Vd121,Vd123,Vd125] :
( Vd121 != vplus(Vd120,Vd125)
| Vd120 != vplus(Vd121,Vd123) ),
inference(skolemisation,[status(esa)],[f31_nnf]) ).
cnf(c38,plain,
( X1 != vplus(X0,X3)
| X0 != vplus(X1,X2) ),
inference(cnf_transformation,[status(esa)],[f31_sk]) ).
fof(f32,axiom,
! [Vd120,Vd121] :
( ~ ? [Vd123] : Vd120 = vplus(Vd121,Vd123)
| Vd120 != Vd121 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qtd32) ).
fof(f32_nnf,plain,
! [Vd120,Vd121] :
( ! [Vd123] : Vd120 != vplus(Vd121,Vd123)
| Vd120 != Vd121 ),
inference(nnf_transformation,[status(thm)],[f32]) ).
fof(f32_sk,plain,
! [Vd120,Vd121,Vd123] :
( Vd120 != vplus(Vd121,Vd123)
| Vd120 != Vd121 ),
inference(skolemisation,[status(esa)],[f32_nnf]) ).
cnf(c39,plain,
( X0 != vplus(X1,X2)
| X0 != X1 ),
inference(cnf_transformation,[status(esa)],[f32_sk]) ).
fof(f34,axiom,
! [Vd92,Vd93] : Vd93 != vplus(Vd92,Vd93),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qtd34) ).
fof(f34_nnf,plain,
! [Vd92,Vd93] : Vd93 != vplus(Vd92,Vd93),
inference(nnf_transformation,[status(thm)],[f34]) ).
fof(f34_sk,plain,
! [Vd93,Vd92] : Vd93 != vplus(Vd92,Vd93),
inference(skolemisation,[status(esa)],[f34_nnf]) ).
cnf(c41,plain,
X1 != vplus(X0,X1),
inference(cnf_transformation,[status(esa)],[f34_sk]) ).
fof(f41,axiom,
! [Vd16] : vsucc(Vd16) != Vd16,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qtd41) ).
fof(f41_nnf,plain,
! [Vd16] : vsucc(Vd16) != Vd16,
inference(nnf_transformation,[status(thm)],[f41]) ).
fof(f41_sk,plain,
! [Vd16] : vsucc(Vd16) != Vd16,
inference(skolemisation,[status(esa)],[f41_nnf]) ).
cnf(c49,plain,
vsucc(X0) != X0,
inference(cnf_transformation,[status(esa)],[f41_sk]) ).
fof(f44,axiom,
! [Vd1] : vsucc(Vd1) != v1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qtd44) ).
fof(f44_nnf,plain,
! [Vd1] : vsucc(Vd1) != v1,
inference(nnf_transformation,[status(thm)],[f44]) ).
fof(f44_sk,plain,
! [Vd1] : vsucc(Vd1) != v1,
inference(skolemisation,[status(esa)],[f44_nnf]) ).
cnf(c52,plain,
vsucc(X0) != v1,
inference(cnf_transformation,[status(esa)],[f44_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c0,c29,c30,c31,c37,c38,c39,c41,c49,c52]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t263]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : NUM841+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.07/0.33 % Computer : n018.cluster.edu
% 0.07/0.33 % Model : x86_64 x86_64
% 0.07/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.33 % Memory : 8046.5625MB
% 0.07/0.33 % OS : Linux 6.8.0-71-generic
% 0.07/0.33 % CPULimit : 300
% 0.07/0.33 % WCLimit : 300
% 0.07/0.33 % DateTime : Thu Sep 24 05:35:48 UTC 2026
% 0.07/0.34 % CPUTime :
% 0.07/0.34 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 92.66/12.26 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 92.66/12.26 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------