%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV403+1 : TPTP v9.3.1. Released v3.3.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 03:13:10 PM UTC 2026
% Result : Theorem 92.81s 14.15s
% Output : Proof 92.81s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 6
% Syntax : Number of formulae : 60 ( 13 unt; 0 def)
% Number of atoms : 154 ( 41 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 141 ( 47 ~; 62 |; 22 &)
% ( 2 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 6 con; 0-2 aty)
% Number of variables : 147 ( 12 sgn 75 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f16,axiom,
! [U,V,W,X] :
( strictly_less_than(X,W)
=> update_slb(insert_slb(U,pair(V,X)),W) = insert_slb(update_slb(U,W),pair(V,W)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax29) ).
fof(f16_nnf,plain,
! [U,V,W,X] :
( update_slb(insert_slb(U,pair(V,X)),W) = insert_slb(update_slb(U,W),pair(V,W))
| ~ strictly_less_than(X,W) ),
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
! [X,W,U,V] :
( update_slb(insert_slb(U,pair(V,X)),W) = insert_slb(update_slb(U,W),pair(V,W))
| ~ strictly_less_than(X,W) ),
inference(skolemisation,[status(esa)],[f16_nnf]) ).
cnf(c23,plain,
( update_slb(insert_slb(X0,pair(X1,X3)),X2) = insert_slb(update_slb(X0,X2),pair(X1,X2))
| ~ strictly_less_than(X3,X2) ),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
fof(f3,axiom,
! [U,V] :
( strictly_less_than(U,V)
<=> ( ~ less_than(V,U)
& less_than(U,V) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',stricly_smaller_definition) ).
fof(f3_nnf,plain,
! [U,V] :
( ( less_than(V,U)
| ~ less_than(U,V)
| strictly_less_than(U,V) )
& ( ( ~ less_than(V,U)
& less_than(U,V) )
| ~ strictly_less_than(U,V) ) ),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [U,V] :
( ( less_than(V,U)
| ~ less_than(U,V)
| strictly_less_than(U,V) )
& ( ( ~ less_than(V,U)
& less_than(U,V) )
| ~ strictly_less_than(U,V) ) ),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c5,plain,
( less_than(X1,X0)
| ~ less_than(X0,X1)
| strictly_less_than(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
fof(f1,axiom,
! [U,V] :
( less_than(V,U)
| less_than(U,V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',totality) ).
fof(f1_nnf,plain,
! [U,V] :
( less_than(V,U)
| less_than(U,V) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [U,V] :
( less_than(V,U)
| less_than(U,V) ),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
( less_than(X1,X0)
| less_than(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(p34,plain,
( less_than(X1,X0)
| less_than(X1,X0)
| strictly_less_than(X0,X1) ),
inference(resolution,[status(thm)],[c5,c1]) ).
cnf(p44,plain,
( less_than(X1,X0)
| strictly_less_than(X0,X1) ),
inference(factoring,[status(thm)],[p34]) ).
cnf(p78,plain,
( less_than(X3,X2)
| update_slb(insert_slb(X0,pair(X1,X2)),X3) = insert_slb(update_slb(X0,X3),pair(X1,X3)) ),
inference(resolution,[status(thm)],[c23,p44]) ).
fof(f18,conjecture,
! [U] :
( ! [V,W,X] :
( ( strictly_less_than(W,X)
& pair_in_list(U,V,W) )
=> pair_in_list(update_slb(U,X),V,X) )
=> ! [Y,Z,X1,X2,X3] :
( ( strictly_less_than(Z,X1)
& pair_in_list(insert_slb(U,pair(X2,X3)),Y,Z) )
=> pair_in_list(update_slb(insert_slb(U,pair(X2,X3)),X1),Y,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l39_co) ).
fof(f18_neg,negated_conjecture,
~ ! [U] :
( ! [V,W,X] :
( ( strictly_less_than(W,X)
& pair_in_list(U,V,W) )
=> pair_in_list(update_slb(U,X),V,X) )
=> ! [Y,Z,X1,X2,X3] :
( ( strictly_less_than(Z,X1)
& pair_in_list(insert_slb(U,pair(X2,X3)),Y,Z) )
=> pair_in_list(update_slb(insert_slb(U,pair(X2,X3)),X1),Y,X1) ) ),
inference(negated_conjecture,[status(cth)],[f18]) ).
fof(f18_nnf,plain,
? [U] :
( ? [Y,Z,X1,X2,X3] :
( ~ pair_in_list(update_slb(insert_slb(U,pair(X2,X3)),X1),Y,X1)
& strictly_less_than(Z,X1)
& pair_in_list(insert_slb(U,pair(X2,X3)),Y,Z) )
& ! [V,W,X] :
( pair_in_list(update_slb(U,X),V,X)
| ~ strictly_less_than(W,X)
| ~ pair_in_list(U,V,W) ) ),
inference(nnf_transformation,[status(thm)],[f18_neg]) ).
fof(f18_sk,plain,
! [V,W,X] :
( ~ pair_in_list(update_slb(insert_slb(sk0,pair(sk4,sk5)),sk3),sk1,sk3)
& strictly_less_than(sk2,sk3)
& pair_in_list(insert_slb(sk0,pair(sk4,sk5)),sk1,sk2)
& ( pair_in_list(update_slb(sk0,X),V,X)
| ~ strictly_less_than(W,X)
| ~ pair_in_list(sk0,V,W) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1,sk2,sk3,sk4,sk5])],[f18_nnf]) ).
cnf(c28,plain,
~ pair_in_list(update_slb(insert_slb(sk0,pair(sk4,sk5)),sk3),sk1,sk3),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(p136,plain,
( ~ pair_in_list(insert_slb(update_slb(sk0,sk3),pair(sk4,sk3)),sk1,sk3)
| less_than(sk3,sk5) ),
inference(superposition,[status(thm)],[p78,c28]) ).
cnf(c25,plain,
( pair_in_list(update_slb(sk0,X3),X1,X3)
| ~ strictly_less_than(X2,X3)
| ~ pair_in_list(sk0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
fof(f10,axiom,
! [U,V,W,X,Y] :
( pair_in_list(insert_slb(U,pair(V,X)),W,Y)
<=> ( ( X = Y
& V = W )
| pair_in_list(U,W,Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax23) ).
fof(f10_nnf,plain,
! [U,V,W,X,Y] :
( ( ( ( X != Y
| V != W )
& ~ pair_in_list(U,W,Y) )
| pair_in_list(insert_slb(U,pair(V,X)),W,Y) )
& ( ( X = Y
& V = W )
| pair_in_list(U,W,Y)
| ~ pair_in_list(insert_slb(U,pair(V,X)),W,Y) ) ),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [U,V,X,W,Y] :
( ( ( ( X != Y
| V != W )
& ~ pair_in_list(U,W,Y) )
| pair_in_list(insert_slb(U,pair(V,X)),W,Y) )
& ( ( X = Y
& V = W )
| pair_in_list(U,W,Y)
| ~ pair_in_list(insert_slb(U,pair(V,X)),W,Y) ) ),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c14,plain,
( X1 = X2
| pair_in_list(X0,X2,X4)
| ~ pair_in_list(insert_slb(X0,pair(X1,X3)),X2,X4) ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(c26,plain,
pair_in_list(insert_slb(sk0,pair(sk4,sk5)),sk1,sk2),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(p45,plain,
( sk4 = sk1
| pair_in_list(sk0,sk1,sk2) ),
inference(resolution,[status(thm)],[c14,c26]) ).
cnf(p72,plain,
( sk4 = sk1
| pair_in_list(update_slb(sk0,X0),sk1,X0)
| ~ strictly_less_than(sk2,X0) ),
inference(resolution,[status(thm)],[c25,p45]) ).
cnf(c27,plain,
strictly_less_than(sk2,sk3),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(p74,plain,
( sk4 = sk1
| pair_in_list(update_slb(sk0,sk3),sk1,sk3) ),
inference(resolution,[status(thm)],[p72,c27]) ).
cnf(c16,plain,
( ~ pair_in_list(X0,X2,X4)
| pair_in_list(insert_slb(X0,pair(X1,X3)),X2,X4) ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(p76,plain,
( pair_in_list(insert_slb(update_slb(sk0,sk3),pair(X0,X1)),sk1,sk3)
| sk4 = sk1 ),
inference(resolution,[status(thm)],[p74,c16]) ).
cnf(p183,plain,
( sk4 = sk1
| less_than(sk3,sk5) ),
inference(resolution,[status(thm)],[p136,p76]) ).
fof(f17,axiom,
! [U,V,W,X] :
( less_than(W,X)
=> update_slb(insert_slb(U,pair(V,X)),W) = insert_slb(update_slb(U,W),pair(V,X)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax30) ).
fof(f17_nnf,plain,
! [U,V,W,X] :
( update_slb(insert_slb(U,pair(V,X)),W) = insert_slb(update_slb(U,W),pair(V,X))
| ~ less_than(W,X) ),
inference(nnf_transformation,[status(thm)],[f17]) ).
fof(f17_sk,plain,
! [W,X,U,V] :
( update_slb(insert_slb(U,pair(V,X)),W) = insert_slb(update_slb(U,W),pair(V,X))
| ~ less_than(W,X) ),
inference(skolemisation,[status(esa)],[f17_nnf]) ).
cnf(c24,plain,
( update_slb(insert_slb(X0,pair(X1,X3)),X2) = insert_slb(update_slb(X0,X2),pair(X1,X3))
| ~ less_than(X2,X3) ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(p190,plain,
( update_slb(insert_slb(X0,pair(X1,sk5)),sk3) = insert_slb(update_slb(X0,sk3),pair(X1,sk5))
| sk4 = sk1 ),
inference(resolution,[status(thm)],[p183,c24]) ).
cnf(p703,plain,
( ~ pair_in_list(insert_slb(update_slb(sk0,sk3),pair(sk4,sk5)),sk1,sk3)
| sk4 = sk1 ),
inference(superposition,[status(thm)],[p190,c28]) ).
cnf(p757,plain,
( sk4 = sk1
| sk4 = sk1 ),
inference(resolution,[status(thm)],[p703,p76]) ).
cnf(p759,plain,
sk4 = sk1,
inference(factoring,[status(thm)],[p757]) ).
cnf(p761,plain,
~ pair_in_list(update_slb(insert_slb(sk0,pair(sk1,sk5)),sk3),sk1,sk3),
inference(demodulation,[status(thm)],[p759,c28]) ).
cnf(c17,plain,
( X3 != X4
| X1 != X2
| pair_in_list(insert_slb(X0,pair(X1,X3)),X2,X4) ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(p58,plain,
( X2 != X3
| pair_in_list(insert_slb(X0,pair(X1,X2)),X1,X3) ),
inference(equality_resolution,[status(thm)],[c17]) ).
cnf(p67,plain,
pair_in_list(insert_slb(X0,pair(X1,X2)),X1,X2),
inference(equality_resolution,[status(thm)],[p58]) ).
cnf(p145,plain,
( pair_in_list(update_slb(insert_slb(X2,pair(X3,X1)),X0),X3,X0)
| less_than(X0,X1) ),
inference(superposition,[status(thm)],[p78,p67]) ).
cnf(p800,plain,
less_than(sk3,sk5),
inference(resolution,[status(thm)],[p761,p145]) ).
cnf(p805,plain,
update_slb(insert_slb(X0,pair(X1,sk5)),sk3) = insert_slb(update_slb(X0,sk3),pair(X1,sk5)),
inference(resolution,[status(thm)],[p800,c24]) ).
cnf(p806,plain,
~ pair_in_list(insert_slb(update_slb(sk0,sk3),pair(sk1,sk5)),sk1,sk3),
inference(demodulation,[status(thm)],[p805,p761]) ).
cnf(c15,plain,
( X3 = X4
| pair_in_list(X0,X2,X4)
| ~ pair_in_list(insert_slb(X0,pair(X1,X3)),X2,X4) ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(p47,plain,
( sk5 = sk2
| pair_in_list(sk0,sk1,sk2) ),
inference(resolution,[status(thm)],[c15,c26]) ).
cnf(p73,plain,
( sk5 = sk2
| pair_in_list(update_slb(sk0,X0),sk1,X0)
| ~ strictly_less_than(sk2,X0) ),
inference(resolution,[status(thm)],[c25,p47]) ).
cnf(p79,plain,
( sk5 = sk2
| pair_in_list(update_slb(sk0,sk3),sk1,sk3) ),
inference(resolution,[status(thm)],[p73,c27]) ).
cnf(p81,plain,
( pair_in_list(insert_slb(update_slb(sk0,sk3),pair(X0,X1)),sk1,sk3)
| sk5 = sk2 ),
inference(resolution,[status(thm)],[p79,c16]) ).
cnf(p870,plain,
sk5 = sk2,
inference(resolution,[status(thm)],[p806,p81]) ).
cnf(p871,plain,
less_than(sk3,sk2),
inference(demodulation,[status(thm)],[p870,p800]) ).
cnf(c4,plain,
( ~ less_than(X1,X0)
| ~ strictly_less_than(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(p32,plain,
~ less_than(sk3,sk2),
inference(resolution,[status(thm)],[c4,c27]) ).
cnf(p922,plain,
$false,
inference(resolution,[status(thm)],[p871,p32]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV403+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.08/0.33 % Computer : n018.cluster.edu
% 0.08/0.33 % Model : x86_64 x86_64
% 0.08/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.33 % Memory : 8046.5625MB
% 0.08/0.33 % OS : Linux 6.8.0-71-generic
% 0.08/0.33 % CPULimit : 300
% 0.08/0.33 % WCLimit : 300
% 0.08/0.33 % DateTime : Thu Sep 24 19:31:33 UTC 2026
% 0.08/0.34 % CPUTime :
% 0.08/0.34 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 92.81/14.15 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 92.81/14.15 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------