%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWV401+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 : n005.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 34.94s 5.46s
% Output : Proof 34.94s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 6
% Syntax : Number of formulae : 60 ( 11 unt; 0 def)
% Number of atoms : 156 ( 47 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 142 ( 46 ~; 64 |; 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 : 143 ( 11 sgn 75 !; 6 ?)
% Comments :
%------------------------------------------------------------------------------
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]) ).
fof(f18,conjecture,
! [U] :
( ! [V,W,X] :
( ( less_than(X,W)
& pair_in_list(U,V,W) )
=> pair_in_list(update_slb(U,X),V,W) )
=> ! [Y,Z,X1,X2,X3] :
( ( less_than(X1,Z)
& pair_in_list(insert_slb(U,pair(X2,X3)),Y,Z) )
=> pair_in_list(update_slb(insert_slb(U,pair(X2,X3)),X1),Y,Z) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l37_co) ).
fof(f18_neg,negated_conjecture,
~ ! [U] :
( ! [V,W,X] :
( ( less_than(X,W)
& pair_in_list(U,V,W) )
=> pair_in_list(update_slb(U,X),V,W) )
=> ! [Y,Z,X1,X2,X3] :
( ( less_than(X1,Z)
& pair_in_list(insert_slb(U,pair(X2,X3)),Y,Z) )
=> pair_in_list(update_slb(insert_slb(U,pair(X2,X3)),X1),Y,Z) ) ),
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,Z)
& less_than(X1,Z)
& pair_in_list(insert_slb(U,pair(X2,X3)),Y,Z) )
& ! [V,W,X] :
( pair_in_list(update_slb(U,X),V,W)
| ~ less_than(X,W)
| ~ 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,sk2)
& less_than(sk3,sk2)
& pair_in_list(insert_slb(sk0,pair(sk4,sk5)),sk1,sk2)
& ( pair_in_list(update_slb(sk0,X),V,W)
| ~ less_than(X,W)
| ~ pair_in_list(sk0,V,W) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1,sk2,sk3,sk4,sk5])],[f18_nnf]) ).
cnf(c27,plain,
less_than(sk3,sk2),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(p95,plain,
update_slb(insert_slb(X0,pair(X1,sk2)),sk3) = insert_slb(update_slb(X0,sk3),pair(X1,sk2)),
inference(resolution,[status(thm)],[c24,c27]) ).
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(p36,plain,
( less_than(X1,X0)
| less_than(X1,X0)
| strictly_less_than(X0,X1) ),
inference(resolution,[status(thm)],[c5,c1]) ).
cnf(p45,plain,
( less_than(X1,X0)
| strictly_less_than(X0,X1) ),
inference(factoring,[status(thm)],[p36]) ).
cnf(p82,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,p45]) ).
cnf(c28,plain,
~ pair_in_list(update_slb(insert_slb(sk0,pair(sk4,sk5)),sk3),sk1,sk2),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(p196,plain,
( ~ pair_in_list(insert_slb(update_slb(sk0,sk3),pair(sk4,sk3)),sk1,sk2)
| less_than(sk3,sk5) ),
inference(superposition,[status(thm)],[p82,c28]) ).
cnf(c25,plain,
( pair_in_list(update_slb(sk0,X3),X1,X2)
| ~ less_than(X3,X2)
| ~ 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(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(c26,plain,
pair_in_list(insert_slb(sk0,pair(sk4,sk5)),sk1,sk2),
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(p44,plain,
( sk5 = sk2
| pair_in_list(sk0,sk1,sk2) ),
inference(resolution,[status(thm)],[c15,c26]) ).
cnf(p72,plain,
( sk5 = sk2
| pair_in_list(update_slb(sk0,X0),sk1,sk2)
| ~ less_than(X0,sk2) ),
inference(resolution,[status(thm)],[c25,p44]) ).
cnf(p86,plain,
( sk5 = sk2
| pair_in_list(update_slb(sk0,sk3),sk1,sk2) ),
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(p103,plain,
( pair_in_list(insert_slb(update_slb(sk0,sk3),pair(X0,X1)),sk1,sk2)
| sk5 = sk2 ),
inference(resolution,[status(thm)],[p86,c16]) ).
cnf(p239,plain,
( sk5 = sk2
| less_than(sk3,sk5) ),
inference(resolution,[status(thm)],[p196,p103]) ).
cnf(p261,plain,
( update_slb(insert_slb(X0,pair(X1,sk5)),sk3) = insert_slb(update_slb(X0,sk3),pair(X1,sk5))
| sk5 = sk2 ),
inference(resolution,[status(thm)],[p239,c24]) ).
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(p40,plain,
( sk4 = sk1
| pair_in_list(sk0,sk1,sk2) ),
inference(resolution,[status(thm)],[c14,c26]) ).
cnf(p71,plain,
( sk4 = sk1
| pair_in_list(update_slb(sk0,X0),sk1,sk2)
| ~ less_than(X0,sk2) ),
inference(resolution,[status(thm)],[c25,p40]) ).
cnf(p75,plain,
( sk4 = sk1
| pair_in_list(update_slb(sk0,sk3),sk1,sk2) ),
inference(resolution,[status(thm)],[p71,c27]) ).
cnf(p83,plain,
( pair_in_list(insert_slb(update_slb(sk0,sk3),pair(X0,X1)),sk1,sk2)
| sk4 = sk1 ),
inference(resolution,[status(thm)],[p75,c16]) ).
cnf(p238,plain,
( sk4 = sk1
| less_than(sk3,sk5) ),
inference(resolution,[status(thm)],[p196,p83]) ).
cnf(p243,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)],[p238,c24]) ).
cnf(p809,plain,
( ~ pair_in_list(insert_slb(update_slb(sk0,sk3),pair(sk4,sk5)),sk1,sk2)
| sk4 = sk1 ),
inference(superposition,[status(thm)],[p243,c28]) ).
cnf(p844,plain,
( sk4 = sk1
| sk4 = sk1 ),
inference(resolution,[status(thm)],[p809,p83]) ).
cnf(p846,plain,
sk4 = sk1,
inference(factoring,[status(thm)],[p844]) ).
cnf(p848,plain,
~ pair_in_list(update_slb(insert_slb(sk0,pair(sk1,sk5)),sk3),sk1,sk2),
inference(demodulation,[status(thm)],[p846,c28]) ).
cnf(p956,plain,
( ~ pair_in_list(insert_slb(update_slb(sk0,sk3),pair(sk1,sk5)),sk1,sk2)
| sk5 = sk2 ),
inference(superposition,[status(thm)],[p261,p848]) ).
cnf(p957,plain,
( sk5 = sk2
| sk5 = sk2 ),
inference(resolution,[status(thm)],[p956,p103]) ).
cnf(p958,plain,
sk5 = sk2,
inference(factoring,[status(thm)],[p957]) ).
cnf(p959,plain,
~ pair_in_list(update_slb(insert_slb(sk0,pair(sk1,sk2)),sk3),sk1,sk2),
inference(demodulation,[status(thm)],[p958,p848]) ).
cnf(p998,plain,
~ pair_in_list(insert_slb(update_slb(sk0,sk3),pair(sk1,sk2)),sk1,sk2),
inference(superposition,[status(thm)],[p95,p959]) ).
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(p66,plain,
pair_in_list(insert_slb(X0,pair(X1,X2)),X1,X2),
inference(equality_resolution,[status(thm)],[p58]) ).
cnf(p999,plain,
$false,
inference(resolution,[status(thm)],[p998,p66]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV401+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.07/0.35 % Computer : n005.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Thu Sep 24 19:29:32 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.07/0.35 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 34.94/5.46 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 34.94/5.46 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------