%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : NUM841+2 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n002.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 46.32s 11.24s
% Output : Proof 46.32s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 14
% Syntax : Number of formulae : 93 ( 68 unt; 0 def)
% Number of atoms : 122 ( 79 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 66 ( 37 ~; 23 |; 2 &)
% ( 1 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 6 con; 0-4 aty)
% Number of variables : 146 ( 12 sgn 58 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f14,axiom,
! [Vd226,Vd227] :
( less(Vd226,Vd227)
=> greater(Vd227,Vd226) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qtd14) ).
fof(f14_nnf,plain,
! [Vd226,Vd227] :
( greater(Vd227,Vd226)
| ~ less(Vd226,Vd227) ),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
! [Vd226,Vd227] :
( greater(Vd227,Vd226)
| ~ less(Vd226,Vd227) ),
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c14,plain,
( greater(X1,X0)
| ~ less(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(t51,plain,
ifeq(less(X1,X2),true,greater(X2,X1),true) = true,
inference(equality_encoding,[status(esa)],[c14]) ).
cnf(t1645,plain,
ifeq(less(X1,X2),true,greater(X2,X1),true) = true,
inference(orient,[status(thm)],[t51]) ).
fof(f11,axiom,
! [Vd301,Vd302,Vd303] :
( Vd301 = Vd302
=> vplus(Vd301,Vd303) = vplus(Vd302,Vd303) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qtd11) ).
fof(f11_nnf,plain,
! [Vd301,Vd302,Vd303] :
( vplus(Vd301,Vd303) = vplus(Vd302,Vd303)
| Vd301 != Vd302 ),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [Vd301,Vd302,Vd303] :
( vplus(Vd301,Vd303) = vplus(Vd302,Vd303)
| Vd301 != Vd302 ),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
( vplus(X0,X2) = vplus(X1,X2)
| X0 != X1 ),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(hi10,axiom,
ifeq(X0,X1,vplus(X0,X2),vplus(X1,X2)) = vplus(X1,X2),
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(hi34,axiom,
or(X0,false) = X0,
introduced(definition) ).
cnf(h54,plain,
vplus(or(V0,false),V1) = vplus(V0,V1),
inference(hyper_resolution,[status(thm)],[hi10,hi34]) ).
cnf(h219,plain,
vplus(vplus(or(V0,false),V1),V2) = vplus(vplus(V0,V1),V2),
inference(hyper_resolution,[status(thm)],[hi10,h54]) ).
fof(f18,axiom,
! [Vd193,Vd194] :
( greater(Vd194,Vd193)
<=> ? [Vd196] : Vd194 = vplus(Vd193,Vd196) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qtd18) ).
fof(f18_nnf,plain,
! [Vd193,Vd194] :
( ( ! [Vd196] : Vd194 != vplus(Vd193,Vd196)
| greater(Vd194,Vd193) )
& ( ? [Vd196] : Vd194 = vplus(Vd193,Vd196)
| ~ greater(Vd194,Vd193) ) ),
inference(nnf_transformation,[status(thm)],[f18]) ).
fof(f18_sk,plain,
! [Vd194,Vd193,Vd196] :
( ( Vd194 != vplus(Vd193,Vd196)
| greater(Vd194,Vd193) )
& ( Vd194 = vplus(Vd193,sk0(Vd193,Vd194))
| ~ greater(Vd194,Vd193) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0])],[f18_nnf]) ).
cnf(c19,plain,
( X1 != vplus(X0,X2)
| greater(X1,X0) ),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(hi17,axiom,
ifeq(X0,vplus(X1,X2),greater(X0,X1),true) = true,
inference(equality_encoding,[status(esa)],[c19]) ).
cnf(h763,plain,
greater(vplus(vplus(or(V0,false),V1),V2),vplus(V0,V1)) = true,
inference(hyper_resolution,[status(thm)],[hi17,h219]) ).
fof(f15,axiom,
! [Vd208,Vd209] :
( greater(Vd208,Vd209)
=> less(Vd209,Vd208) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qtd15) ).
fof(f15_nnf,plain,
! [Vd208,Vd209] :
( less(Vd209,Vd208)
| ~ greater(Vd208,Vd209) ),
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
! [Vd208,Vd209] :
( less(Vd209,Vd208)
| ~ greater(Vd208,Vd209) ),
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c15,plain,
( less(X1,X0)
| ~ greater(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(hi14,axiom,
ifeq(greater(X0,X1),true,less(X1,X0),true) = true,
inference(equality_encoding,[status(esa)],[c15]) ).
cnf(t102,plain,
less(vplus(X1,X2),vplus(vplus(or(X1,false),X2),X3)) = true,
inference(hyper_resolution,[status(thm)],[hi14,h763]) ).
fof(f23,axiom,
! [Vd46,Vd47,Vd48] : vplus(vplus(Vd46,Vd47),Vd48) = vplus(Vd46,vplus(Vd47,Vd48)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qtd23) ).
fof(f23_nnf,plain,
! [Vd46,Vd47,Vd48] : vplus(vplus(Vd46,Vd47),Vd48) = vplus(Vd46,vplus(Vd47,Vd48)),
inference(nnf_transformation,[status(thm)],[f23]) ).
fof(f23_sk,plain,
! [Vd46,Vd47,Vd48] : vplus(vplus(Vd46,Vd47),Vd48) = vplus(Vd46,vplus(Vd47,Vd48)),
inference(skolemisation,[status(esa)],[f23_nnf]) ).
cnf(c24,plain,
vplus(vplus(X0,X1),X2) = vplus(X0,vplus(X1,X2)),
inference(cnf_transformation,[status(esa)],[f23_sk]) ).
cnf(t55,plain,
vplus(vplus(X1,X2),X3) = vplus(X1,vplus(X2,X3)),
inference(equality_encoding,[status(esa)],[c24]) ).
cnf(t273,plain,
vplus(vplus(X1,X2),X3) = vplus(X1,vplus(X2,X3)),
inference(orient,[status(thm)],[t55]) ).
cnf(t24803,plain,
less(vplus(X1,X2),vplus(or(X1,false),vplus(X2,X3))) = true,
inference(step,[status(thm)],[t102,t273]) ).
cnf(t5,plain,
or(X1,false) = X1,
introduced(definition) ).
cnf(t256,plain,
or(X1,false) = X1,
inference(orient,[status(thm)],[t5]) ).
cnf(t24804,plain,
less(vplus(X1,X2),vplus(X1,vplus(X2,X3))) = true,
inference(step,[status(thm)],[t24803,t256]) ).
cnf(t1373,plain,
less(vplus(X1,X2),vplus(X1,vplus(X2,X3))) = true,
inference(orient,[status(thm)],[t24804]) ).
cnf(c18,plain,
( X1 = vplus(X0,sk0(X0,X1))
| ~ greater(X1,X0) ),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(hi16,axiom,
ifeq(greater(X0,X1),true,X0,vplus(X1,sk0(X1,X0))) = vplus(X1,sk0(X1,X0)),
inference(equality_encoding,[status(esa)],[c18]) ).
fof(f6,axiom,
greater(vd344,vd345),
file('/export/starexec/sandbox/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(t14,plain,
vplus(vd345,sk0(vd345,vd344)) = vd344,
inference(hyper_resolution,[status(thm)],[hi16,hi5]) ).
cnf(t1042,plain,
vplus(vd345,sk0(vd345,vd344)) = vd344,
inference(orient,[status(thm)],[t14]) ).
cnf(t1046,plain,
vplus(vd345,vplus(sk0(vd345,vd344),X1)) = vplus(vd344,X1),
inference(cp,[status(thm)],[t273,t1042]) ).
cnf(t4670,plain,
vplus(vd345,vplus(sk0(vd345,vd344),X1)) = vplus(vd344,X1),
inference(orient,[status(thm)],[t1046]) ).
cnf(t4716,plain,
true = less(vplus(X1,vd345),vplus(X1,vplus(vd344,X2))),
inference(cp,[status(thm)],[t1373,t4670]) ).
cnf(t23601,plain,
less(vplus(X1,vd345),vplus(X1,vplus(vd344,X2))) = true,
inference(orient,[status(thm)],[t4716]) ).
fof(f5,axiom,
greater(vd347,vd348),
file('/export/starexec/sandbox/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(t16,plain,
vplus(vd348,sk0(vd348,vd347)) = vd347,
inference(hyper_resolution,[status(thm)],[hi16,hi4]) ).
cnf(t1054,plain,
vplus(vd348,sk0(vd348,vd347)) = vd347,
inference(orient,[status(thm)],[t16]) ).
cnf(t1058,plain,
vplus(vd348,vplus(sk0(vd348,vd347),X1)) = vplus(vd347,X1),
inference(cp,[status(thm)],[t273,t1054]) ).
cnf(t4796,plain,
vplus(vd348,vplus(sk0(vd348,vd347),X1)) = vplus(vd347,X1),
inference(orient,[status(thm)],[t1058]) ).
fof(f20,axiom,
! [Vd78,Vd79] : vplus(Vd79,Vd78) = vplus(Vd78,Vd79),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qtd20) ).
fof(f20_nnf,plain,
! [Vd78,Vd79] : vplus(Vd79,Vd78) = vplus(Vd78,Vd79),
inference(nnf_transformation,[status(thm)],[f20]) ).
fof(f20_sk,plain,
! [Vd79,Vd78] : vplus(Vd79,Vd78) = vplus(Vd78,Vd79),
inference(skolemisation,[status(esa)],[f20_nnf]) ).
cnf(c21,plain,
vplus(X1,X0) = vplus(X0,X1),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(t13,plain,
vplus(X1,X2) = vplus(X2,X1),
inference(equality_encoding,[status(esa)],[c21]) ).
cnf(t261,plain,
vplus(X1,X2) = vplus(X2,X1),
inference(orient,[status(thm)],[t13]) ).
cnf(t4807,plain,
vplus(vd347,X1) = vplus(vd348,vplus(X1,sk0(vd348,vd347))),
inference(cp,[status(thm)],[t4796,t261]) ).
cnf(t5870,plain,
vplus(vd348,vplus(X1,sk0(vd348,vd347))) = vplus(vd347,X1),
inference(orient,[status(thm)],[t4807]) ).
cnf(t23611,plain,
true = less(vplus(vd348,vd345),vplus(vd347,vd344)),
inference(cp,[status(thm)],[t23601,t5870]) ).
cnf(t23632,plain,
less(vplus(vd348,vd345),vplus(vd347,vd344)) = true,
inference(orient,[status(thm)],[t23611]) ).
cnf(t23633,plain,
true = ifeq(true,true,greater(vplus(vd347,vd344),vplus(vd348,vd345)),true),
inference(cp,[status(thm)],[t1645,t23632]) ).
cnf(t12,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t258,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t12]) ).
cnf(t25144,plain,
true = greater(vplus(vd347,vd344),vplus(vd348,vd345)),
inference(step,[status(thm)],[t23633,t258]) ).
fof(f0,conjecture,
greater(vplus(vd344,vd347),vplus(vd345,vd348)),
file('/export/starexec/sandbox/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(t36,plain,
greater(vplus(vd344,vd347),vplus(vd345,vd348)) = false,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t24821,plain,
greater(vplus(vd347,vd344),vplus(vd345,vd348)) = false,
inference(step,[status(thm)],[t36,t261]) ).
cnf(t24822,plain,
greater(vplus(vd347,vd344),vplus(vd348,vd345)) = false,
inference(step,[status(thm)],[t24821,t261]) ).
cnf(t1721,plain,
greater(vplus(vd347,vd344),vplus(vd348,vd345)) = false,
inference(orient,[status(thm)],[t24822]) ).
cnf(t25145,plain,
true = false,
inference(step,[status(thm)],[t25144,t1721]) ).
cnf(t23637,plain,
false = true,
inference(orient,[status(thm)],[t25145]) ).
fof(f17,axiom,
! [Vd203,Vd204] :
( ~ less(Vd203,Vd204)
| ~ greater(Vd203,Vd204) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qtd17) ).
fof(f17_nnf,plain,
! [Vd203,Vd204] :
( ~ less(Vd203,Vd204)
| ~ greater(Vd203,Vd204) ),
inference(nnf_transformation,[status(thm)],[f17]) ).
fof(f17_sk,plain,
! [Vd203,Vd204] :
( ~ less(Vd203,Vd204)
| ~ greater(Vd203,Vd204) ),
inference(skolemisation,[status(esa)],[f17_nnf]) ).
cnf(c17,plain,
( ~ less(X0,X1)
| ~ greater(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
fof(f19,axiom,
! [Vd120,Vd121] :
( ~ ? [Vd123] : Vd120 = vplus(Vd121,Vd123)
| Vd120 != Vd121 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qtd19) ).
fof(f19_nnf,plain,
! [Vd120,Vd121] :
( ! [Vd123] : Vd120 != vplus(Vd121,Vd123)
| Vd120 != Vd121 ),
inference(nnf_transformation,[status(thm)],[f19]) ).
fof(f19_sk,plain,
! [Vd120,Vd121,Vd123] :
( Vd120 != vplus(Vd121,Vd123)
| Vd120 != Vd121 ),
inference(skolemisation,[status(esa)],[f19_nnf]) ).
cnf(c20,plain,
( X0 != vplus(X1,X2)
| X0 != X1 ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c0,c17,c20]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t23637]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NUM841+2 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/5.36 % Computer : n002.cluster.edu
% 0.10/5.36 % Model : x86_64 x86_64
% 0.10/5.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.36 % Memory : 8046.5625MB
% 0.10/5.36 % OS : Linux 6.8.0-71-generic
% 0.10/5.36 % CPULimit : 300
% 0.10/5.36 % WCLimit : 300
% 0.10/5.36 % DateTime : Thu Sep 24 05:36:25 UTC 2026
% 0.10/5.37 % CPUTime :
% 0.10/5.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 46.32/11.24 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 46.32/11.24 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------