%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWX077_1 : TPTP v9.3.1. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n001.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 : Tue Sep 29 01:45:50 PM UTC 2026
% Result : Theorem 2.93s 1.14s
% Output : Refutation 4.02s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 15
% Syntax : Number of formulae : 97 ( 27 unt; 0 typ; 11 def)
% Number of atoms : 415 ( 168 equ)
% Maximal formula atoms : 14 ( 4 avg)
% Number of connectives : 518 ( 200 ~; 176 |; 125 &)
% ( 12 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 25 ( 5 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 4 ( 2 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 23 ( 21 usr; 12 prp; 0-2 aty)
% Number of functors : 26 ( 26 usr; 14 con; 0-1 aty)
% Number of variables : 204 ( 126 !; 78 ?; 204 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
general: $tType ).
tff(type_def_6,type,
symbol: $tType ).
tff(func_def_0,type,
f__integer__: $int > general ).
tff(func_def_1,type,
f__symbolic__: symbol > general ).
tff(func_def_2,type,
c__infimum__: general ).
tff(func_def_3,type,
c__supremum__: general ).
tff(func_def_4,type,
n_i: $int ).
tff(func_def_7,type,
sK0: general > general ).
tff(func_def_8,type,
sK1: general > general ).
tff(func_def_9,type,
sK2: general > general ).
tff(func_def_10,type,
sK3: general > general ).
tff(func_def_11,type,
sK4: general > general ).
tff(func_def_12,type,
sK5: general ).
tff(func_def_13,type,
sK6: general ).
tff(func_def_14,type,
sK7: general ).
tff(func_def_15,type,
sK8: general ).
tff(func_def_16,type,
sK9: general ).
tff(func_def_17,type,
sK10: general ).
tff(func_def_18,type,
sK11: general ).
tff(func_def_19,type,
sK12: general ).
tff(func_def_20,type,
sK13: general ).
tff(func_def_21,type,
sK14: general ).
tff(func_def_22,type,
sK15: general ).
tff(func_def_23,type,
sK16: general > symbol ).
tff(func_def_24,type,
sK17: general > $int ).
tff(func_def_25,type,
sK18: general > $int ).
tff(func_def_26,type,
sK19: general > $int ).
tff(func_def_27,type,
sK20: general > $int ).
tff(pred_def_1,type,
p__is_integer__: general > $o ).
tff(pred_def_2,type,
p__is_symbolic__: general > $o ).
tff(pred_def_3,type,
p__less_equal__: ( general * general ) > $o ).
tff(pred_def_4,type,
p__less__: ( general * general ) > $o ).
tff(pred_def_5,type,
p__greater_equal__: ( general * general ) > $o ).
tff(pred_def_6,type,
p__greater__: ( general * general ) > $o ).
tff(pred_def_8,type,
covered: general > $o ).
tff(pred_def_9,type,
in_cover: general > $o ).
tff(pred_def_10,type,
s: ( general * general ) > $o ).
tff(pred_def_11,type,
covered_p: general > $o ).
tff(f9,axiom,
! [X1: general,X0: general] :
( p__less_equal__(X0,X1)
| p__less_equal__(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',strongly_connected_ordering_ax) ).
tff(f10,axiom,
! [X0: general,X1: general] :
( p__less__(X0,X1)
<=> ( ( X0 != X1 )
& p__less_equal__(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p__less__def_ax) ).
tff(f19,axiom,
! [X0: general,X2: general,X1: general] :
( ( ? [X3: general] :
( ( X3 = X1 )
& in_cover(X3) )
& ? [X3: general] :
( in_cover(X3)
& ( X3 = X0 ) )
& ? [X3: general,X4: general] :
( s(X3,X4)
& ( X3 = X2 )
& ( X4 = X0 ) )
& ? [X3: general,X4: general] :
( s(X3,X4)
& ( X4 = X1 )
& ( X3 = X2 ) )
& ? [X3: general,X4: general] :
( ( X4 = X1 )
& p__less__(X3,X4)
& ( X3 = X0 ) ) )
=> $false ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',formula_3_constraint_0) ).
tff(f22,conjecture,
! [X1: general,X0: general,X2: general] :
( ( ? [X3: general] :
( ( X3 = X0 )
& in_cover(X3) )
& ? [X3: general] :
( ( X3 = X1 )
& in_cover(X3) )
& ? [X4: general,X3: general] :
( ( X4 = X1 )
& s(X3,X4)
& ( X3 = X2 ) )
& ? [X3: general,X4: general] :
( ( X3 = X0 )
& ( X4 = X1 )
& ( X3 != X4 ) )
& ? [X3: general,X4: general] :
( s(X3,X4)
& ( X3 = X2 )
& ( X4 = X0 ) ) )
=> $false ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',formula_6_constraint_0) ).
tff(f23,negated_conjecture,
~ ! [X1: general,X0: general,X2: general] :
( ( ? [X3: general] :
( ( X3 = X0 )
& in_cover(X3) )
& ? [X3: general] :
( ( X3 = X1 )
& in_cover(X3) )
& ? [X4: general,X3: general] :
( ( X4 = X1 )
& s(X3,X4)
& ( X3 = X2 ) )
& ? [X3: general,X4: general] :
( ( X3 = X0 )
& ( X4 = X1 )
& ( X3 != X4 ) )
& ? [X3: general,X4: general] :
( s(X3,X4)
& ( X3 = X2 )
& ( X4 = X0 ) ) )
=> $false ),
inference(negated_conjecture,[status(cth)],[f22]) ).
tff(f27,plain,
~ ! [X0: general,X1: general,X2: general] :
( ( ? [X10: general,X9: general] :
( s(X9,X10)
& ( X1 = X10 )
& ( X2 = X9 ) )
& ? [X6: general,X5: general] :
( ( X2 = X6 )
& ( X0 = X5 )
& s(X6,X5) )
& ? [X4: general] :
( ( X0 = X4 )
& in_cover(X4) )
& ? [X8: general,X7: general] :
( ( X1 = X7 )
& ( X7 != X8 )
& ( X0 = X8 ) )
& ? [X3: general] :
( ( X1 = X3 )
& in_cover(X3) ) )
=> $false ),
inference(rectify,[],[f23]) ).
tff(f28,plain,
~ ! [X1: general,X0: general,X2: general] :
~ ( ? [X10: general,X9: general] :
( s(X9,X10)
& ( X1 = X10 )
& ( X2 = X9 ) )
& ? [X6: general,X5: general] :
( ( X2 = X6 )
& ( X0 = X5 )
& s(X6,X5) )
& ? [X4: general] :
( ( X0 = X4 )
& in_cover(X4) )
& ? [X8: general,X7: general] :
( ( X1 = X7 )
& ( X7 != X8 )
& ( X0 = X8 ) )
& ? [X3: general] :
( ( X1 = X3 )
& in_cover(X3) ) ),
inference(true_and_false_elimination,[],[f27]) ).
tff(f33,plain,
! [X0: general,X1: general,X2: general] :
( ( ? [X9: general,X10: general] :
( ( X2 = X10 )
& p__less__(X9,X10)
& ( X0 = X9 ) )
& ? [X4: general] :
( ( X0 = X4 )
& in_cover(X4) )
& ? [X7: general,X8: general] :
( s(X7,X8)
& ( X2 = X8 )
& ( X1 = X7 ) )
& ? [X3: general] :
( ( X2 = X3 )
& in_cover(X3) )
& ? [X6: general,X5: general] :
( ( X0 = X6 )
& ( X1 = X5 )
& s(X5,X6) ) )
=> $false ),
inference(rectify,[],[f19]) ).
tff(f34,plain,
! [X2: general,X0: general,X1: general] :
~ ( ? [X9: general,X10: general] :
( ( X2 = X10 )
& p__less__(X9,X10)
& ( X0 = X9 ) )
& ? [X4: general] :
( ( X0 = X4 )
& in_cover(X4) )
& ? [X7: general,X8: general] :
( s(X7,X8)
& ( X2 = X8 )
& ( X1 = X7 ) )
& ? [X3: general] :
( ( X2 = X3 )
& in_cover(X3) )
& ? [X6: general,X5: general] :
( ( X0 = X6 )
& ( X1 = X5 )
& s(X5,X6) ) ),
inference(true_and_false_elimination,[],[f33]) ).
tff(f41,plain,
! [X1: general,X0: general] :
( p__less_equal__(X1,X0)
| p__less_equal__(X0,X1) ),
inference(rectify,[],[f9]) ).
tff(f52,plain,
? [X1: general,X0: general,X2: general] :
( ? [X10: general,X9: general] :
( s(X9,X10)
& ( X1 = X10 )
& ( X2 = X9 ) )
& ? [X6: general,X5: general] :
( ( X2 = X6 )
& ( X0 = X5 )
& s(X6,X5) )
& ? [X4: general] :
( ( X0 = X4 )
& in_cover(X4) )
& ? [X8: general,X7: general] :
( ( X1 = X7 )
& ( X7 != X8 )
& ( X0 = X8 ) )
& ? [X3: general] :
( ( X1 = X3 )
& in_cover(X3) ) ),
inference(ennf_transformation,[],[f28]) ).
tff(f55,plain,
! [X0: general,X2: general,X1: general] :
( ! [X6: general,X5: general] :
( ( X1 != X5 )
| ( X0 != X6 )
| ~ s(X5,X6) )
| ! [X4: general] :
( ~ in_cover(X4)
| ( X0 != X4 ) )
| ! [X8: general,X7: general] :
( ( X1 != X7 )
| ( X2 != X8 )
| ~ s(X7,X8) )
| ! [X3: general] :
( ( X2 != X3 )
| ~ in_cover(X3) )
| ! [X10: general,X9: general] :
( ( X2 != X10 )
| ~ p__less__(X9,X10)
| ( X0 != X9 ) ) ),
inference(ennf_transformation,[],[f34]) ).
tff(f56,plain,
! [X0: general,X1: general,X2: general] :
( ! [X3: general,X4: general] :
( ( X2 != X4 )
| ( X0 != X3 )
| ~ s(X4,X3) )
| ! [X5: general] :
( ~ in_cover(X5)
| ( X0 != X5 ) )
| ! [X6: general,X7: general] :
( ( X2 != X7 )
| ( X1 != X6 )
| ~ s(X7,X6) )
| ! [X8: general] :
( ( X1 != X8 )
| ~ in_cover(X8) )
| ! [X9: general,X10: general] :
( ( X1 != X9 )
| ~ p__less__(X10,X9)
| ( X0 != X10 ) ) ),
inference(rectify,[],[f55]) ).
tff(f67,plain,
? [X0: general,X1: general,X2: general] :
( ? [X3: general,X4: general] :
( s(X4,X3)
& ( X0 = X3 )
& ( X2 = X4 ) )
& ? [X5: general,X6: general] :
( ( X2 = X5 )
& ( X1 = X6 )
& s(X5,X6) )
& ? [X7: general] :
( ( X1 = X7 )
& in_cover(X7) )
& ? [X8: general,X9: general] :
( ( X0 = X9 )
& ( X8 != X9 )
& ( X1 = X8 ) )
& ? [X10: general] :
( ( X0 = X10 )
& in_cover(X10) ) ),
inference(rectify,[],[f52]) ).
tff(f68,plain,
( s(sK9,sK8)
& ( sK8 = sK5 )
& ( sK9 = sK7 )
& ( sK10 = sK7 )
& ( sK11 = sK6 )
& s(sK10,sK11)
& ( sK6 = sK12 )
& in_cover(sK12)
& ( sK14 = sK5 )
& ( sK14 != sK13 )
& ( sK6 = sK13 )
& ( sK5 = sK15 )
& in_cover(sK15) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5,sK6,sK7,sK8,sK9,sK10,sK11,sK12,sK13,sK14,sK15]),skolemize(X0,sK5),skolemize(X1,sK6),skolemize(X2,sK7),skolemize(X3,sK8),skolemize(X4,sK9),skolemize(X5,sK10),skolemize(X6,sK11),skolemize(X7,sK12),skolemize(X8,sK13),skolemize(X9,sK14),skolemize(X10,sK15)],[f67]) ).
tff(f71,plain,
! [X0: general,X1: general] :
( ( p__less__(X0,X1)
| ( X0 = X1 )
| ~ p__less_equal__(X0,X1) )
& ( ( ( X0 != X1 )
& p__less_equal__(X0,X1) )
| ~ p__less__(X0,X1) ) ),
inference(nnf_transformation,[],[f10]) ).
tff(f72,plain,
! [X0: general,X1: general] :
( ( p__less__(X0,X1)
| ( X0 = X1 )
| ~ p__less_equal__(X0,X1) )
& ( ( ( X0 != X1 )
& p__less_equal__(X0,X1) )
| ~ p__less__(X0,X1) ) ),
inference(flattening,[],[f71]) ).
tff(f80,plain,
! [X0: general,X1: general] :
( p__less_equal__(X0,X1)
| p__less_equal__(X1,X0) ),
inference(rectify,[],[f41]) ).
tff(f82,plain,
! [X2: general,X3: general,X10: general,X0: general,X1: general,X8: general,X6: general,X9: general,X7: general,X4: general,X5: general] :
( ( X2 != X4 )
| ( X0 != X3 )
| ~ s(X4,X3)
| ~ in_cover(X5)
| ( X0 != X5 )
| ( X2 != X7 )
| ( X1 != X6 )
| ~ s(X7,X6)
| ( X1 != X8 )
| ~ in_cover(X8)
| ( X1 != X9 )
| ~ p__less__(X10,X9)
| ( X0 != X10 ) ),
inference(cnf_transformation,[],[f56]) ).
tff(f100,plain,
in_cover(sK15),
inference(cnf_transformation,[],[f68]) ).
tff(f101,plain,
sK5 = sK15,
inference(cnf_transformation,[],[f68]) ).
tff(f102,plain,
sK6 = sK13,
inference(cnf_transformation,[],[f68]) ).
tff(f103,plain,
sK14 != sK13,
inference(cnf_transformation,[],[f68]) ).
tff(f104,plain,
sK14 = sK5,
inference(cnf_transformation,[],[f68]) ).
tff(f105,plain,
in_cover(sK12),
inference(cnf_transformation,[],[f68]) ).
tff(f106,plain,
sK6 = sK12,
inference(cnf_transformation,[],[f68]) ).
tff(f107,plain,
s(sK10,sK11),
inference(cnf_transformation,[],[f68]) ).
tff(f108,plain,
sK11 = sK6,
inference(cnf_transformation,[],[f68]) ).
tff(f109,plain,
sK10 = sK7,
inference(cnf_transformation,[],[f68]) ).
tff(f110,plain,
sK9 = sK7,
inference(cnf_transformation,[],[f68]) ).
tff(f111,plain,
sK8 = sK5,
inference(cnf_transformation,[],[f68]) ).
tff(f112,plain,
s(sK9,sK8),
inference(cnf_transformation,[],[f68]) ).
tff(f118,plain,
! [X0: general,X1: general] :
( p__less__(X0,X1)
| ~ p__less_equal__(X0,X1)
| ( X0 = X1 ) ),
inference(cnf_transformation,[],[f72]) ).
tff(f129,plain,
! [X0: general,X1: general] :
( p__less_equal__(X1,X0)
| p__less_equal__(X0,X1) ),
inference(cnf_transformation,[],[f80]) ).
tff(f130,plain,
sK8 = sK15,
inference(definition_unfolding,[],[f111,f101]) ).
tff(f131,plain,
sK11 = sK12,
inference(definition_unfolding,[],[f108,f106]) ).
tff(f132,plain,
sK14 = sK15,
inference(definition_unfolding,[],[f104,f101]) ).
tff(f133,plain,
s(sK7,sK15),
inference(definition_unfolding,[],[f112,f110,f130]) ).
tff(f134,plain,
s(sK7,sK12),
inference(definition_unfolding,[],[f107,f109,f131]) ).
tff(f135,plain,
sK13 != sK15,
inference(definition_unfolding,[],[f103,f132]) ).
tff(f136,plain,
sK12 = sK13,
inference(definition_unfolding,[],[f102,f106]) ).
tff(f137,plain,
! [X3: general,X10: general,X0: general,X1: general,X8: general,X6: general,X9: general,X7: general,X4: general,X5: general] :
( ( X0 != X3 )
| ~ s(X4,X3)
| ~ in_cover(X5)
| ( X0 != X5 )
| ( X4 != X7 )
| ( X1 != X6 )
| ~ s(X7,X6)
| ( X1 != X8 )
| ~ in_cover(X8)
| ( X1 != X9 )
| ~ p__less__(X10,X9)
| ( X0 != X10 ) ),
inference(equality_resolution,[],[f82]) ).
tff(f138,plain,
! [X3: general,X10: general,X1: general,X8: general,X6: general,X9: general,X7: general,X4: general,X5: general] :
( ~ s(X4,X3)
| ~ in_cover(X5)
| ( X3 != X5 )
| ( X4 != X7 )
| ( X1 != X6 )
| ~ s(X7,X6)
| ( X1 != X8 )
| ~ in_cover(X8)
| ( X1 != X9 )
| ~ p__less__(X10,X9)
| ( X3 != X10 ) ),
inference(equality_resolution,[],[f137]) ).
tff(f139,plain,
! [X10: general,X1: general,X8: general,X6: general,X9: general,X7: general,X4: general,X5: general] :
( ~ s(X4,X5)
| ~ in_cover(X5)
| ( X4 != X7 )
| ( X1 != X6 )
| ~ s(X7,X6)
| ( X1 != X8 )
| ~ in_cover(X8)
| ( X1 != X9 )
| ~ p__less__(X10,X9)
| ( X5 != X10 ) ),
inference(equality_resolution,[],[f138]) ).
tff(f140,plain,
! [X10: general,X1: general,X8: general,X6: general,X9: general,X7: general,X5: general] :
( ~ s(X7,X5)
| ~ in_cover(X5)
| ( X1 != X6 )
| ~ s(X7,X6)
| ( X1 != X8 )
| ~ in_cover(X8)
| ( X1 != X9 )
| ~ p__less__(X10,X9)
| ( X5 != X10 ) ),
inference(equality_resolution,[],[f139]) ).
tff(f141,plain,
! [X10: general,X8: general,X6: general,X9: general,X7: general,X5: general] :
( ~ s(X7,X5)
| ~ in_cover(X5)
| ~ s(X7,X6)
| ( X6 != X8 )
| ~ in_cover(X8)
| ( X6 != X9 )
| ~ p__less__(X10,X9)
| ( X5 != X10 ) ),
inference(equality_resolution,[],[f140]) ).
tff(f142,plain,
! [X10: general,X8: general,X9: general,X7: general,X5: general] :
( ~ s(X7,X5)
| ~ in_cover(X5)
| ~ s(X7,X8)
| ~ in_cover(X8)
| ( X8 != X9 )
| ~ p__less__(X10,X9)
| ( X5 != X10 ) ),
inference(equality_resolution,[],[f141]) ).
tff(f143,plain,
! [X10: general,X9: general,X7: general,X5: general] :
( ~ s(X7,X5)
| ~ in_cover(X5)
| ~ s(X7,X9)
| ~ in_cover(X9)
| ~ p__less__(X10,X9)
| ( X5 != X10 ) ),
inference(equality_resolution,[],[f142]) ).
tff(f144,plain,
! [X10: general,X9: general,X7: general] :
( ~ s(X7,X10)
| ~ p__less__(X10,X9)
| ~ in_cover(X10)
| ~ in_cover(X9)
| ~ s(X7,X9) ),
inference(equality_resolution,[],[f143]) ).
tff(f155,definition,
( spl21_1
<=> ( sK12 = sK13 ) ),
introduced(definition,[new_symbols(definition,[spl21_1])],[avatar_definition]) ).
tff(f157,plain,
( ( sK12 = sK13 )
| ~ spl21_1 ),
inference(avatar_component_clause,[],[f155]) ).
tff(f158,plain,
spl21_1,
inference(avatar_split_clause,[],[f136,f155]) ).
tff(f160,definition,
( spl21_2
<=> in_cover(sK12) ),
introduced(definition,[new_symbols(definition,[spl21_2])],[avatar_definition]) ).
tff(f162,plain,
( in_cover(sK12)
| ~ spl21_2 ),
inference(avatar_component_clause,[],[f160]) ).
tff(f163,plain,
spl21_2,
inference(avatar_split_clause,[],[f105,f160]) ).
tff(f165,definition,
( spl21_3
<=> s(sK7,sK15) ),
introduced(definition,[new_symbols(definition,[spl21_3])],[avatar_definition]) ).
tff(f167,plain,
( s(sK7,sK15)
| ~ spl21_3 ),
inference(avatar_component_clause,[],[f165]) ).
tff(f168,plain,
spl21_3,
inference(avatar_split_clause,[],[f133,f165]) ).
tff(f170,definition,
( spl21_4
<=> s(sK7,sK12) ),
introduced(definition,[new_symbols(definition,[spl21_4])],[avatar_definition]) ).
tff(f172,plain,
( s(sK7,sK12)
| ~ spl21_4 ),
inference(avatar_component_clause,[],[f170]) ).
tff(f173,plain,
spl21_4,
inference(avatar_split_clause,[],[f134,f170]) ).
tff(f175,definition,
( spl21_5
<=> ( sK13 = sK15 ) ),
introduced(definition,[new_symbols(definition,[spl21_5])],[avatar_definition]) ).
tff(f177,plain,
( ( sK13 != sK15 )
| spl21_5 ),
inference(avatar_component_clause,[],[f175]) ).
tff(f178,plain,
~ spl21_5,
inference(avatar_split_clause,[],[f135,f175]) ).
tff(f180,definition,
( spl21_6
<=> in_cover(sK15) ),
introduced(definition,[new_symbols(definition,[spl21_6])],[avatar_definition]) ).
tff(f182,plain,
( in_cover(sK15)
| ~ spl21_6 ),
inference(avatar_component_clause,[],[f180]) ).
tff(f183,plain,
spl21_6,
inference(avatar_split_clause,[],[f100,f180]) ).
tff(f189,plain,
( ( sK12 != sK15 )
| ~ spl21_1
| spl21_5 ),
inference(forward_demodulation,[],[f177,f157]) ).
tff(f191,definition,
( spl21_8
<=> ( sK12 = sK15 ) ),
introduced(definition,[new_symbols(definition,[spl21_8])],[avatar_definition]) ).
tff(f193,plain,
( ( sK12 != sK15 )
| spl21_8 ),
inference(avatar_component_clause,[],[f191]) ).
tff(f194,plain,
( ~ spl21_8
| ~ spl21_1
| spl21_5 ),
inference(avatar_split_clause,[],[f189,f175,f155,f191]) ).
tff(f309,plain,
( ! [X0: general] :
( ~ p__less__(sK15,X0)
| ~ in_cover(sK15)
| ~ in_cover(X0)
| ~ s(sK7,X0) )
| ~ spl21_3 ),
inference(resolution,[],[f144,f167]) ).
tff(f310,plain,
( ! [X0: general] :
( ~ in_cover(X0)
| ~ s(sK7,X0)
| ~ p__less__(sK12,X0)
| ~ in_cover(sK12) )
| ~ spl21_4 ),
inference(resolution,[],[f144,f172]) ).
tff(f312,plain,
( ! [X0: general] :
( ~ s(sK7,X0)
| ~ p__less__(sK15,X0)
| ~ in_cover(X0) )
| ~ spl21_3
| ~ spl21_6 ),
inference(forward_subsumption_resolution,[],[f309,f182]) ).
tff(f313,plain,
( ! [X0: general] :
( ~ s(sK7,X0)
| ~ in_cover(X0)
| ~ p__less__(sK12,X0) )
| ~ spl21_2
| ~ spl21_4 ),
inference(forward_subsumption_resolution,[],[f310,f162]) ).
tff(f315,plain,
( ~ in_cover(sK12)
| ~ p__less__(sK15,sK12)
| ~ spl21_3
| ~ spl21_4
| ~ spl21_6 ),
inference(resolution,[],[f312,f172]) ).
tff(f316,plain,
( ~ p__less__(sK15,sK12)
| ~ spl21_2
| ~ spl21_3
| ~ spl21_4
| ~ spl21_6 ),
inference(forward_subsumption_resolution,[],[f315,f162]) ).
tff(f318,definition,
( spl21_15
<=> p__less__(sK15,sK12) ),
introduced(definition,[new_symbols(definition,[spl21_15])],[avatar_definition]) ).
tff(f320,plain,
( ~ p__less__(sK15,sK12)
| spl21_15 ),
inference(avatar_component_clause,[],[f318]) ).
tff(f321,plain,
( ~ spl21_15
| ~ spl21_2
| ~ spl21_3
| ~ spl21_4
| ~ spl21_6 ),
inference(avatar_split_clause,[],[f316,f180,f170,f165,f160,f318]) ).
tff(f322,plain,
( ~ in_cover(sK15)
| ~ p__less__(sK12,sK15)
| ~ spl21_2
| ~ spl21_3
| ~ spl21_4 ),
inference(resolution,[],[f313,f167]) ).
tff(f324,plain,
( ~ p__less__(sK12,sK15)
| ~ spl21_2
| ~ spl21_3
| ~ spl21_4
| ~ spl21_6 ),
inference(forward_subsumption_resolution,[],[f322,f182]) ).
tff(f326,definition,
( spl21_16
<=> p__less__(sK12,sK15) ),
introduced(definition,[new_symbols(definition,[spl21_16])],[avatar_definition]) ).
tff(f328,plain,
( ~ p__less__(sK12,sK15)
| spl21_16 ),
inference(avatar_component_clause,[],[f326]) ).
tff(f329,plain,
( ~ spl21_16
| ~ spl21_2
| ~ spl21_3
| ~ spl21_4
| ~ spl21_6 ),
inference(avatar_split_clause,[],[f324,f180,f170,f165,f160,f326]) ).
tff(f330,plain,
( ( sK12 = sK15 )
| ~ p__less_equal__(sK15,sK12)
| spl21_15 ),
inference(resolution,[],[f320,f118]) ).
tff(f331,plain,
( ~ p__less_equal__(sK15,sK12)
| spl21_8
| spl21_15 ),
inference(forward_subsumption_resolution,[],[f330,f193]) ).
tff(f333,definition,
( spl21_17
<=> p__less_equal__(sK15,sK12) ),
introduced(definition,[new_symbols(definition,[spl21_17])],[avatar_definition]) ).
tff(f335,plain,
( ~ p__less_equal__(sK15,sK12)
| spl21_17 ),
inference(avatar_component_clause,[],[f333]) ).
tff(f336,plain,
( ~ spl21_17
| spl21_8
| spl21_15 ),
inference(avatar_split_clause,[],[f331,f318,f191,f333]) ).
tff(f337,plain,
( ~ p__less_equal__(sK12,sK15)
| ( sK12 = sK15 )
| spl21_16 ),
inference(resolution,[],[f328,f118]) ).
tff(f338,plain,
( ~ p__less_equal__(sK12,sK15)
| spl21_8
| spl21_16 ),
inference(forward_subsumption_resolution,[],[f337,f193]) ).
tff(f340,definition,
( spl21_18
<=> p__less_equal__(sK12,sK15) ),
introduced(definition,[new_symbols(definition,[spl21_18])],[avatar_definition]) ).
tff(f343,plain,
( ~ spl21_18
| spl21_8
| spl21_16 ),
inference(avatar_split_clause,[],[f338,f326,f191,f340]) ).
tff(f349,plain,
( p__less_equal__(sK12,sK15)
| spl21_17 ),
inference(resolution,[],[f335,f129]) ).
tff(f350,plain,
( spl21_18
| spl21_17 ),
inference(avatar_split_clause,[],[f349,f333,f340]) ).
tff(f351,plain,
$false,
inference(avatar_smt_refutation,[],[f350,f343,f336,f329,f321,f194,f183,f178,f173,f168,f163,f158]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX077_1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.18 % Computer : n001.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Mon Sep 28 15:06:03 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.21 Running first-order theorem proving
% 0.09/0.21 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.93/1.14 % (414012)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 2.93/1.14 % (414017)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=1017694324:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 2.93/1.14 % (414017)Instruction limit reached!
% 2.93/1.14 % (414017)------------------------------
% 2.93/1.14 % (414017)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.93/1.14 % (414017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.93/1.14 % (414017)CaDiCaL version: 2.1.3
% 2.93/1.14 % (414017)Termination reason: Instruction limit
% 2.93/1.14 % (414017)Termination phase: Saturation
% 2.93/1.14 % (414017)Time elapsed: 0.019 s
% 2.93/1.14 % (414017)Peak memory usage: 115 MB
% 2.93/1.14 % (414017)Instructions burned: 12 (million)
% 2.93/1.14 % (414021)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=915453267:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 2.93/1.14 % (414020)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=3018231968:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 2.93/1.14 % (414019)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=4201948733:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 2.93/1.14 % (414023)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=1802362596:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 2.93/1.14 % (414018)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=625875238:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 2.93/1.14 % (414022)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=1172685464:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 2.93/1.14 % (414021)Instruction limit reached!
% 2.93/1.14 % (414021)------------------------------
% 2.93/1.14 % (414021)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.93/1.14 % (414021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.93/1.14 % (414021)CaDiCaL version: 2.1.3
% 2.93/1.14 % (414021)Termination reason: Instruction limit
% 2.93/1.14 % (414021)Termination phase: Saturation
% 2.93/1.14 % (414021)Time elapsed: 0.004 s
% 2.93/1.14 % (414021)Peak memory usage: 89 MB
% 2.93/1.14 % (414021)Instructions burned: 4 (million)
% 2.93/1.14 % (414020)Instruction limit reached!
% 2.93/1.14 % (414020)------------------------------
% 2.93/1.14 % (414020)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.93/1.14 % (414020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.93/1.14 % (414020)CaDiCaL version: 2.1.3
% 2.93/1.14 % (414020)Termination reason: Instruction limit
% 2.93/1.14 % (414020)Termination phase: Saturation
% 2.93/1.14 % (414020)Time elapsed: 0.006 s
% 2.93/1.14 % (414020)Peak memory usage: 88 MB
% 2.93/1.14 % (414020)Instructions burned: 8 (million)
% 2.93/1.14 % (414018)First to succeed.
% 2.93/1.14 % (414018)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-414012"
% 2.93/1.14 % (414023)Instruction limit reached!
% 2.93/1.14 % (414023)------------------------------
% 2.93/1.14 % (414023)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.93/1.14 % (414023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.93/1.14 % (414023)CaDiCaL version: 2.1.3
% 2.93/1.14 % (414023)Termination reason: Instruction limit
% 2.93/1.14 % (414023)Termination phase: Saturation
% 2.93/1.14 % (414023)Time elapsed: 0.047 s
% 2.93/1.14 % (414023)Peak memory usage: 116 MB
% 2.93/1.14 % (414023)Instructions burned: 33 (million)
% 2.93/1.14 % (414022)Instruction limit reached!
% 2.93/1.14 % (414022)------------------------------
% 2.93/1.14 % (414022)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.93/1.14 % (414022)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.93/1.14 % (414022)CaDiCaL version: 2.1.3
% 2.93/1.14 % (414022)Termination reason: Instruction limit
% 2.93/1.14 % (414022)Termination phase: Saturation
% 2.93/1.14 % (414022)Time elapsed: 0.056 s
% 2.93/1.14 % (414022)Peak memory usage: 116 MB
% 2.93/1.14 % (414022)Instructions burned: 47 (million)
% 2.93/1.14 % (414025)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=4059399604:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 2.93/1.14 % (414025)Instruction limit reached!
% 2.93/1.14 % (414025)------------------------------
% 2.93/1.14 % (414025)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.93/1.14 % (414025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.93/1.14 % (414025)CaDiCaL version: 2.1.3
% 2.93/1.14 % (414025)Termination reason: Instruction limit
% 2.93/1.14 % (414025)Termination phase: Saturation
% 2.93/1.14 % (414025)Time elapsed: 0.007 s
% 2.93/1.14 % (414025)Peak memory usage: 89 MB
% 2.93/1.14 % (414025)Instructions burned: 15 (million)
% 2.93/1.14 % (414019)Instruction limit reached!
% 2.93/1.14 % (414019)------------------------------
% 2.93/1.14 % (414019)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.93/1.14 % (414019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.93/1.14 % (414019)CaDiCaL version: 2.1.3
% 2.93/1.14 % (414019)Termination reason: Instruction limit
% 2.93/1.14 % (414019)Termination phase: Saturation
% 2.93/1.14 % (414019)Time elapsed: 0.131 s
% 2.93/1.14 % (414019)Peak memory usage: 114 MB
% 2.93/1.14 % (414019)Instructions burned: 202 (million)
% 2.93/1.14 % (414033)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1625680479:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi)
% 2.93/1.14 % (414032)dis+1011_2:1_to=kbo:sil=128000:tgt=full:fde=none:si=on:norm_ineq=on:spb=goal_then_units:tha=some:nwc=2:sac=on:random_seed=3121705239:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi)
% 2.93/1.14 % (414032)Also succeeded, but the first one will report.
% 2.93/1.14 % (414033)Instruction limit reached!
% 2.93/1.14 % (414033)------------------------------
% 2.93/1.14 % (414033)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.93/1.14 % (414033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.93/1.14 % (414033)CaDiCaL version: 2.1.3
% 2.93/1.14 % (414033)Termination reason: Instruction limit
% 2.93/1.14 % (414033)Termination phase: Saturation
% 2.93/1.14 % (414033)Time elapsed: 0.012 s
% 2.93/1.14 % (414033)Peak memory usage: 90 MB
% 2.93/1.14 % (414033)Instructions burned: 17 (million)
% 2.93/1.14 % (414037)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=2659996164:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi)
% 2.93/1.14 % (414034)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=3954435897:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 2.93/1.14 % (414035)ott+1010_8_to=lpo:sil=128000:si=on:norm_ineq=on:sp=unary_frequency:sos=on:gve=cautious:spb=goal_then_units:uwa=alasca_main_floor:tha=some:random_seed=714023422:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi)
% 2.93/1.14 % (414035)Refutation not found, incomplete strategy
% 2.93/1.14 % (414035)------------------------------
% 2.93/1.14 % (414035)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.93/1.14 % (414035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.93/1.14 % (414035)CaDiCaL version: 2.1.3
% 2.93/1.14 % (414035)Termination reason: Refutation not found, incomplete strategy
% 2.93/1.14 % (414035)Time elapsed: 0.004 s
% 2.93/1.14 % (414035)Peak memory usage: 89 MB
% 2.93/1.14 % (414035)Instructions burned: 3 (million)
% 2.93/1.14 % (414034)Also succeeded, but the first one will report.
% 2.93/1.14 % (414037)Instruction limit reached!
% 2.93/1.14 % (414037)------------------------------
% 2.93/1.14 % (414037)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.93/1.14 % (414037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.93/1.14 % (414037)CaDiCaL version: 2.1.3
% 2.93/1.14 % (414037)Termination reason: Instruction limit
% 2.93/1.14 % (414037)Termination phase: Saturation
% 2.93/1.14 % (414037)Time elapsed: 0.023 s
% 2.93/1.14 % (414037)Peak memory usage: 89 MB
% 2.93/1.14 % (414037)Instructions burned: 89 (million)
% 2.93/1.14 % (414038)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=1523992015:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi)
% 2.93/1.14 % (414038)Instruction limit reached!
% 2.93/1.14 % (414038)------------------------------
% 2.93/1.14 % (414038)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.93/1.14 % (414038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.93/1.14 % (414038)CaDiCaL version: 2.1.3
% 2.93/1.14 % (414038)Termination reason: Instruction limit
% 2.93/1.14 % (414038)Termination phase: Saturation
% 2.93/1.14 % (414038)Time elapsed: 0.002 s
% 2.93/1.14 % (414038)Peak memory usage: 88 MB
% 2.93/1.14 % (414038)Instructions burned: 2 (million)
% 2.93/1.14 % (414018)Refutation found. Thanks to Tanya!
% 2.93/1.14 % SZS status Theorem for theBenchmark
% 2.93/1.14 % SZS output start Proof for theBenchmark
% See solution above
% 4.02/1.34 % (414018)------------------------------
% 4.02/1.34 % (414018)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.02/1.34 % (414018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.02/1.34 % (414018)CaDiCaL version: 2.1.3
% 4.02/1.34 % (414018)Termination reason: Refutation
% 4.02/1.34 % (414018)Time elapsed: 0.046 s
% 4.02/1.34 % (414018)Peak memory usage: 116 MB
% 4.02/1.34 % (414018)Instructions burned: 27 (million)
% 4.02/1.34 % (414018)------------------------------
% 4.02/1.34 % (414018)------------------------------
% 4.02/1.34 % (414012)Success in time 0.482 s
% 4.02/1.34 % Vampire exiting
%------------------------------------------------------------------------------