%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWX093_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 : n009.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:52 PM UTC 2026
% Result : Theorem 3.76s 1.29s
% Output : Refutation 5.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 28
% Syntax : Number of formulae : 99 ( 26 unt; 0 typ; 23 def)
% Number of atoms : 241 ( 30 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 231 ( 89 ~; 69 |; 44 &)
% ( 21 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number arithmetic : 161 ( 41 atm; 54 fun; 39 num; 27 var)
% Number of types : 4 ( 2 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 33 ( 28 usr; 18 prp; 0-2 aty)
% Number of functors : 41 ( 37 usr; 16 con; 0-2 aty)
% Number of variables : 74 ( 65 !; 9 ?; 74 :)
% 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_9,type,
sK0: $int ).
tff(func_def_10,type,
sK1: general > $int ).
tff(func_def_11,type,
sK2: general > general ).
tff(func_def_12,type,
sK3: general > general ).
tff(func_def_13,type,
sK4: general > general ).
tff(func_def_14,type,
sK5: general > $int ).
tff(func_def_15,type,
sK6: general > $int ).
tff(func_def_16,type,
sK7: general > $int ).
tff(func_def_17,type,
sK8: general > $int ).
tff(func_def_18,type,
sK9: general > $int ).
tff(func_def_19,type,
sK10: general > $int ).
tff(func_def_20,type,
sK11: general > general ).
tff(func_def_21,type,
sK12: general > general ).
tff(func_def_22,type,
sK13: general > $int ).
tff(func_def_23,type,
sK14: general > $int ).
tff(func_def_24,type,
sK15: general > general ).
tff(func_def_25,type,
sK16: general > general ).
tff(func_def_26,type,
sK17: general > $int ).
tff(func_def_27,type,
sK18: general > $int ).
tff(func_def_28,type,
sK19: general > $int ).
tff(func_def_29,type,
sK20: $int > $int ).
tff(func_def_30,type,
sK21: $int ).
tff(func_def_31,type,
sK22: general ).
tff(func_def_32,type,
sK23: $int ).
tff(func_def_33,type,
sK24: general > symbol ).
tff(func_def_34,type,
sF25: $int ).
tff(func_def_35,type,
sF26: general ).
tff(func_def_36,type,
sF27: $int ).
tff(func_def_37,type,
sF28: general ).
tff(func_def_38,type,
sF29: $int ).
tff(func_def_39,type,
sF30: $int ).
tff(func_def_40,type,
sF31: general ).
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,
three: general > $o ).
tff(pred_def_9,type,
sqrt: general > $o ).
tff(pred_def_10,type,
three_p: general > $o ).
tff(pred_def_11,type,
more_than_three: general > $o ).
tff(pred_def_12,type,
sqrt: ( general * general ) > $o ).
tff(f6,axiom,
! [X1: $int,X0: $int] :
( $lesseq(X0,X1)
<=> p__less_equal__(f__integer__(X0),f__integer__(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',numeral_ordering_ax) ).
tff(f7,axiom,
! [X1: general,X0: general] :
( ( p__less_equal__(X1,X0)
& p__less_equal__(X0,X1) )
=> ( X0 = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',antisymmetric_ordering_ax) ).
tff(f8,axiom,
! [X2: general,X0: general,X1: general] :
( ( p__less_equal__(X0,X1)
& p__less_equal__(X1,X2) )
=> p__less_equal__(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',transitive_ordering_ax) ).
tff(f12,axiom,
! [X0: general,X1: general] :
( ( p__less_equal__(X1,X0)
& ( X0 != X1 ) )
<=> p__greater__(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p__greater__def_ax) ).
tff(f26,conjecture,
! [X1: $int,X0: $int,X2: general] :
( ( $greatereq(X0,0)
& p__less_equal__(f__integer__($product(X0,X0)),X2)
& $greatereq(X1,0)
& p__greater__(f__integer__($product($sum(X0,1),$sum(X0,1))),X2)
& p__less_equal__(f__integer__($product(X1,X1)),X2) )
=> $lesseq(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',formula_10_unnamed_formula) ).
tff(f27,negated_conjecture,
~ ! [X1: $int,X0: $int,X2: general] :
( ( $greatereq(X0,0)
& p__less_equal__(f__integer__($product(X0,X0)),X2)
& $greatereq(X1,0)
& p__greater__(f__integer__($product($sum(X0,1),$sum(X0,1))),X2)
& p__less_equal__(f__integer__($product(X1,X1)),X2) )
=> $lesseq(X1,X0) ),
inference(negated_conjecture,[status(cth)],[f26]) ).
tff(f29,plain,
! [X1: $int,X0: $int] :
( ~ $less(X1,X0)
<=> p__less_equal__(f__integer__(X0),f__integer__(X1)) ),
inference(theory_normalization,[],[f6]) ).
tff(f36,plain,
~ ! [X1: $int,X0: $int,X2: general] :
( ( ~ $less(X0,0)
& p__less_equal__(f__integer__($product(X0,X0)),X2)
& ~ $less(X1,0)
& p__greater__(f__integer__($product($sum(X0,1),$sum(X0,1))),X2)
& p__less_equal__(f__integer__($product(X1,X1)),X2) )
=> ~ $less(X0,X1) ),
inference(theory_normalization,[],[f27]) ).
tff(f39,plain,
! [X1: $int,X0: $int] :
( ~ $less(X0,X1)
<=> p__less_equal__(f__integer__(X1),f__integer__(X0)) ),
inference(rectify,[],[f29]) ).
tff(f40,plain,
! [X0: general,X1: general,X2: general] :
( ( p__less_equal__(X1,X2)
& p__less_equal__(X2,X0) )
=> p__less_equal__(X1,X0) ),
inference(rectify,[],[f8]) ).
tff(f48,plain,
~ ! [X2: general,X0: $int,X1: $int] :
( ( ~ $less(X0,0)
& p__greater__(f__integer__($product($sum(X1,1),$sum(X1,1))),X2)
& ~ $less(X1,0)
& p__less_equal__(f__integer__($product(X1,X1)),X2)
& p__less_equal__(f__integer__($product(X0,X0)),X2) )
=> ~ $less(X1,X0) ),
inference(rectify,[],[f36]) ).
tff(f50,plain,
! [X0: general,X1: general] :
( p__greater__(X0,X1)
=> ( p__less_equal__(X1,X0)
& ( X0 != X1 ) ) ),
inference(unused_predicate_definition_removal,[],[f12]) ).
tff(f55,plain,
! [X0: general,X1: general,X2: general] :
( p__less_equal__(X1,X0)
| ~ p__less_equal__(X1,X2)
| ~ p__less_equal__(X2,X0) ),
inference(ennf_transformation,[],[f40]) ).
tff(f56,plain,
! [X1: general,X0: general,X2: general] :
( p__less_equal__(X1,X0)
| ~ p__less_equal__(X2,X0)
| ~ p__less_equal__(X1,X2) ),
inference(flattening,[],[f55]) ).
tff(f59,plain,
? [X2: general,X0: $int,X1: $int] :
( $less(X1,X0)
& ~ $less(X0,0)
& p__greater__(f__integer__($product($sum(X1,1),$sum(X1,1))),X2)
& ~ $less(X1,0)
& p__less_equal__(f__integer__($product(X1,X1)),X2)
& p__less_equal__(f__integer__($product(X0,X0)),X2) ),
inference(ennf_transformation,[],[f48]) ).
tff(f60,plain,
? [X0: $int,X2: general,X1: $int] :
( $less(X1,X0)
& ~ $less(X0,0)
& p__less_equal__(f__integer__($product(X0,X0)),X2)
& ~ $less(X1,0)
& p__less_equal__(f__integer__($product(X1,X1)),X2)
& p__greater__(f__integer__($product($sum(X1,1),$sum(X1,1))),X2) ),
inference(flattening,[],[f59]) ).
tff(f61,plain,
! [X0: general,X1: general] :
( ~ p__greater__(X0,X1)
| ( p__less_equal__(X1,X0)
& ( X0 != X1 ) ) ),
inference(ennf_transformation,[],[f50]) ).
tff(f68,plain,
! [X1: general,X0: general] :
( ( X0 = X1 )
| ~ p__less_equal__(X1,X0)
| ~ p__less_equal__(X0,X1) ),
inference(ennf_transformation,[],[f7]) ).
tff(f69,plain,
! [X1: general,X0: general] :
( ( X0 = X1 )
| ~ p__less_equal__(X0,X1)
| ~ p__less_equal__(X1,X0) ),
inference(flattening,[],[f68]) ).
tff(f79,plain,
! [X0: general,X1: general] :
( ( X0 = X1 )
| ~ p__less_equal__(X1,X0)
| ~ p__less_equal__(X0,X1) ),
inference(rectify,[],[f69]) ).
tff(f83,plain,
! [X0: general,X1: general,X2: general] :
( p__less_equal__(X0,X1)
| ~ p__less_equal__(X2,X1)
| ~ p__less_equal__(X0,X2) ),
inference(rectify,[],[f56]) ).
tff(f84,plain,
! [X1: $int,X0: $int] :
( ( ~ $less(X0,X1)
| ~ p__less_equal__(f__integer__(X1),f__integer__(X0)) )
& ( p__less_equal__(f__integer__(X1),f__integer__(X0))
| $less(X0,X1) ) ),
inference(nnf_transformation,[],[f39]) ).
tff(f85,plain,
! [X0: $int,X1: $int] :
( ( ~ $less(X1,X0)
| ~ p__less_equal__(f__integer__(X0),f__integer__(X1)) )
& ( p__less_equal__(f__integer__(X0),f__integer__(X1))
| $less(X1,X0) ) ),
inference(rectify,[],[f84]) ).
tff(f87,plain,
? [X0: $int,X1: general,X2: $int] :
( $less(X2,X0)
& ~ $less(X0,0)
& p__less_equal__(f__integer__($product(X0,X0)),X1)
& ~ $less(X2,0)
& p__less_equal__(f__integer__($product(X2,X2)),X1)
& p__greater__(f__integer__($product($sum(X2,1),$sum(X2,1))),X1) ),
inference(rectify,[],[f60]) ).
tff(f88,plain,
( $less(sK23,sK21)
& ~ $less(sK21,0)
& p__less_equal__(f__integer__($product(sK21,sK21)),sK22)
& ~ $less(sK23,0)
& p__less_equal__(f__integer__($product(sK23,sK23)),sK22)
& p__greater__(f__integer__($product($sum(sK23,1),$sum(sK23,1))),sK22) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK21,sK22,sK23]),skolemize(X0,sK21),skolemize(X1,sK22),skolemize(X2,sK23)],[f87]) ).
tff(f97,plain,
! [X0: general,X1: general] :
( ~ p__greater__(X0,X1)
| ( X0 != X1 ) ),
inference(cnf_transformation,[],[f61]) ).
tff(f98,plain,
! [X0: general,X1: general] :
( ~ p__greater__(X0,X1)
| p__less_equal__(X1,X0) ),
inference(cnf_transformation,[],[f61]) ).
tff(f125,plain,
! [X0: general,X1: general] :
( ~ p__less_equal__(X1,X0)
| ~ p__less_equal__(X0,X1)
| ( X0 = X1 ) ),
inference(cnf_transformation,[],[f79]) ).
tff(f131,plain,
! [X2: general,X0: general,X1: general] :
( p__less_equal__(X0,X1)
| ~ p__less_equal__(X0,X2)
| ~ p__less_equal__(X2,X1) ),
inference(cnf_transformation,[],[f83]) ).
tff(f134,plain,
! [X0: $int,X1: $int] :
( p__less_equal__(f__integer__(X0),f__integer__(X1))
| $less(X1,X0) ),
inference(cnf_transformation,[],[f85]) ).
tff(f138,plain,
p__greater__(f__integer__($product($sum(sK23,1),$sum(sK23,1))),sK22),
inference(cnf_transformation,[],[f88]) ).
tff(f140,plain,
~ $less(sK23,0),
inference(cnf_transformation,[],[f88]) ).
tff(f141,plain,
p__less_equal__(f__integer__($product(sK21,sK21)),sK22),
inference(cnf_transformation,[],[f88]) ).
tff(f143,plain,
$less(sK23,sK21),
inference(cnf_transformation,[],[f88]) ).
tff(f148,plain,
! [X1: general] : ~ p__greater__(X1,X1),
inference(equality_resolution,[],[f97]) ).
tff(f150,definition,
sF25 = $product(sK21,sK21),
introduced(definition,[new_symbols(definition,[sF25])],[function_definition]) ).
tff(f151,plain,
$product(sK21,sK21) = sF25,
inference(reorient_equations,[],[f150]) ).
tff(f152,definition,
sF26 = f__integer__(sF25),
introduced(definition,[new_symbols(definition,[sF26])],[function_definition]) ).
tff(f153,plain,
p__less_equal__(sF26,sK22),
inference(definition_folding,[],[f141,f152,f151]) ).
tff(f154,definition,
sF27 = $product(sK23,sK23),
introduced(definition,[new_symbols(definition,[sF27])],[function_definition]) ).
tff(f157,definition,
sF29 = $sum(sK23,1),
introduced(definition,[new_symbols(definition,[sF29])],[function_definition]) ).
tff(f158,plain,
$sum(sK23,1) = sF29,
inference(reorient_equations,[],[f157]) ).
tff(f159,definition,
sF30 = $product(sF29,sF29),
introduced(definition,[new_symbols(definition,[sF30])],[function_definition]) ).
tff(f160,definition,
sF31 = f__integer__(sF30),
introduced(definition,[new_symbols(definition,[sF31])],[function_definition]) ).
tff(f161,plain,
p__greater__(sF31,sK22),
inference(definition_folding,[],[f138,f160,f159,f158,f158]) ).
tff(f163,definition,
( spl32_1
<=> ( sF30 = $product(sF29,sF29) ) ),
introduced(definition,[new_symbols(definition,[spl32_1])],[avatar_definition]) ).
tff(f166,plain,
spl32_1,
inference(avatar_split_clause,[],[f159,f163]) ).
tff(f168,definition,
( spl32_2
<=> ( $product(sK21,sK21) = sF25 ) ),
introduced(definition,[new_symbols(definition,[spl32_2])],[avatar_definition]) ).
tff(f171,plain,
spl32_2,
inference(avatar_split_clause,[],[f151,f168]) ).
tff(f173,definition,
( spl32_3
<=> $less(sK23,sK21) ),
introduced(definition,[new_symbols(definition,[spl32_3])],[avatar_definition]) ).
tff(f176,plain,
spl32_3,
inference(avatar_split_clause,[],[f143,f173]) ).
tff(f183,definition,
( spl32_5
<=> ( sF31 = f__integer__(sF30) ) ),
introduced(definition,[new_symbols(definition,[spl32_5])],[avatar_definition]) ).
tff(f185,plain,
( ( sF31 = f__integer__(sF30) )
| ~ spl32_5 ),
inference(avatar_component_clause,[],[f183]) ).
tff(f186,plain,
spl32_5,
inference(avatar_split_clause,[],[f160,f183]) ).
tff(f188,definition,
( spl32_6
<=> ( $sum(sK23,1) = sF29 ) ),
introduced(definition,[new_symbols(definition,[spl32_6])],[avatar_definition]) ).
tff(f191,plain,
spl32_6,
inference(avatar_split_clause,[],[f158,f188]) ).
tff(f198,definition,
( spl32_8
<=> p__less_equal__(sF26,sK22) ),
introduced(definition,[new_symbols(definition,[spl32_8])],[avatar_definition]) ).
tff(f200,plain,
( p__less_equal__(sF26,sK22)
| ~ spl32_8 ),
inference(avatar_component_clause,[],[f198]) ).
tff(f201,plain,
spl32_8,
inference(avatar_split_clause,[],[f153,f198]) ).
tff(f203,definition,
( spl32_9
<=> p__greater__(sF31,sK22) ),
introduced(definition,[new_symbols(definition,[spl32_9])],[avatar_definition]) ).
tff(f205,plain,
( p__greater__(sF31,sK22)
| ~ spl32_9 ),
inference(avatar_component_clause,[],[f203]) ).
tff(f206,plain,
spl32_9,
inference(avatar_split_clause,[],[f161,f203]) ).
tff(f208,definition,
( spl32_10
<=> $less(sK23,0) ),
introduced(definition,[new_symbols(definition,[spl32_10])],[avatar_definition]) ).
tff(f211,plain,
~ spl32_10,
inference(avatar_split_clause,[],[f140,f208]) ).
tff(f218,definition,
( spl32_12
<=> ( sF27 = $product(sK23,sK23) ) ),
introduced(definition,[new_symbols(definition,[spl32_12])],[avatar_definition]) ).
tff(f221,plain,
spl32_12,
inference(avatar_split_clause,[],[f154,f218]) ).
tff(f228,definition,
( spl32_14
<=> ( sF26 = f__integer__(sF25) ) ),
introduced(definition,[new_symbols(definition,[spl32_14])],[avatar_definition]) ).
tff(f230,plain,
( ( sF26 = f__integer__(sF25) )
| ~ spl32_14 ),
inference(avatar_component_clause,[],[f228]) ).
tff(f231,plain,
spl32_14,
inference(avatar_split_clause,[],[f152,f228]) ).
tff(f258,plain,
( p__less_equal__(sK22,sF31)
| ~ spl32_9 ),
inference(resolution,[],[f98,f205]) ).
tff(f260,definition,
( spl32_19
<=> p__less_equal__(sK22,sF31) ),
introduced(definition,[new_symbols(definition,[spl32_19])],[avatar_definition]) ).
tff(f262,plain,
( p__less_equal__(sK22,sF31)
| ~ spl32_19 ),
inference(avatar_component_clause,[],[f260]) ).
tff(f263,plain,
( spl32_19
| ~ spl32_9 ),
inference(avatar_split_clause,[],[f258,f203,f260]) ).
tff(f480,plain,
( ! [X0: $int] :
( p__less_equal__(sF31,f__integer__(X0))
| $less(X0,sF30) )
| ~ spl32_5 ),
inference(superposition,[],[f134,f185]) ).
tff(f529,plain,
( ( sF26 = sK22 )
| ~ p__less_equal__(sK22,sF26)
| ~ spl32_8 ),
inference(resolution,[],[f125,f200]) ).
tff(f533,plain,
( ( sF31 = sK22 )
| ~ p__less_equal__(sF31,sK22)
| ~ spl32_19 ),
inference(resolution,[],[f125,f262]) ).
tff(f536,definition,
( spl32_36
<=> ( sF26 = sK22 ) ),
introduced(definition,[new_symbols(definition,[spl32_36])],[avatar_definition]) ).
tff(f540,definition,
( spl32_37
<=> p__less_equal__(sK22,sF26) ),
introduced(definition,[new_symbols(definition,[spl32_37])],[avatar_definition]) ).
tff(f542,plain,
( ~ p__less_equal__(sK22,sF26)
| spl32_37 ),
inference(avatar_component_clause,[],[f540]) ).
tff(f543,plain,
( spl32_36
| ~ spl32_37
| ~ spl32_8 ),
inference(avatar_split_clause,[],[f529,f198,f540,f536]) ).
tff(f563,definition,
( spl32_42
<=> ( sF31 = sK22 ) ),
introduced(definition,[new_symbols(definition,[spl32_42])],[avatar_definition]) ).
tff(f565,plain,
( ( sF31 = sK22 )
| ~ spl32_42 ),
inference(avatar_component_clause,[],[f563]) ).
tff(f567,definition,
( spl32_43
<=> p__less_equal__(sF31,sK22) ),
introduced(definition,[new_symbols(definition,[spl32_43])],[avatar_definition]) ).
tff(f570,plain,
( spl32_42
| ~ spl32_43
| ~ spl32_19 ),
inference(avatar_split_clause,[],[f533,f260,f567,f563]) ).
tff(f623,plain,
( ! [X0: general] :
( ~ p__less_equal__(sK22,X0)
| ~ p__less_equal__(X0,sF26) )
| spl32_37 ),
inference(resolution,[],[f131,f542]) ).
tff(f644,plain,
( ~ p__less_equal__(sF31,sF26)
| ~ spl32_19
| spl32_37 ),
inference(resolution,[],[f623,f262]) ).
tff(f646,definition,
( spl32_53
<=> p__less_equal__(sF31,sF26) ),
introduced(definition,[new_symbols(definition,[spl32_53])],[avatar_definition]) ).
tff(f648,plain,
( ~ p__less_equal__(sF31,sF26)
| spl32_53 ),
inference(avatar_component_clause,[],[f646]) ).
tff(f649,plain,
( ~ spl32_53
| ~ spl32_19
| spl32_37 ),
inference(avatar_split_clause,[],[f644,f540,f260,f646]) ).
tff(f803,definition,
( spl32_68
<=> $less(sF25,sF30) ),
introduced(definition,[new_symbols(definition,[spl32_68])],[avatar_definition]) ).
tff(f805,plain,
( ~ $less(sF25,sF30)
| spl32_68 ),
inference(avatar_component_clause,[],[f803]) ).
tff(f887,plain,
( p__greater__(sK22,sK22)
| ~ spl32_9
| ~ spl32_42 ),
inference(superposition,[],[f205,f565]) ).
tff(f898,plain,
( $false
| ~ spl32_9
| ~ spl32_42 ),
inference(forward_subsumption_resolution,[],[f887,f148]) ).
tff(f899,plain,
( ~ spl32_9
| ~ spl32_42 ),
inference(avatar_contradiction_clause,[],[f898]) ).
tff(f1404,plain,
( p__less_equal__(sF31,sF26)
| $less(sF25,sF30)
| ~ spl32_5
| ~ spl32_14 ),
inference(superposition,[],[f480,f230]) ).
tff(f1408,plain,
( $less(sF25,sF30)
| ~ spl32_5
| ~ spl32_14
| spl32_53 ),
inference(forward_subsumption_resolution,[],[f1404,f648]) ).
tff(f1411,plain,
( $false
| ~ spl32_5
| ~ spl32_14
| spl32_53
| spl32_68 ),
inference(forward_subsumption_resolution,[],[f1408,f805]) ).
tff(f1412,plain,
( ~ spl32_5
| ~ spl32_14
| spl32_53
| spl32_68 ),
inference(avatar_contradiction_clause,[],[f1411]) ).
tff(f1414,plain,
$false,
inference(avatar_smt_refutation,[],[f1412,f899,f649,f570,f543,f263,f231,f221,f211,f206,f201,f191,f186,f176,f171,f166]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWX093_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.06/0.18 % Computer : n009.cluster.edu
% 0.06/0.18 % Model : x86_64 x86_64
% 0.06/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.18 % Memory : 8046.5625MB
% 0.06/0.18 % OS : Linux 6.8.0-71-generic
% 0.06/0.18 % CPULimit : 300
% 0.06/0.18 % WCLimit : 300
% 0.06/0.18 % DateTime : Mon Sep 28 15:01:00 UTC 2026
% 0.06/0.18 % CPUTime :
% 0.06/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.06/0.22 Running first-order theorem proving
% 0.06/0.22 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
% 3.76/1.21 % (3124074)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 3.76/1.21 % (3124081)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=3160105123:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 3.76/1.21 % (3124084)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=1757541418:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 3.76/1.21 % (3124083)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=1271478118:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 3.76/1.21 % (3124085)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=3620297843:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 3.76/1.21 % (3124082)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=2222486848:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 3.76/1.21 % (3124080)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=4136817358:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 3.76/1.21 % (3124079)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=842720873:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 3.76/1.21 % (3124083)Instruction limit reached!
% 3.76/1.21 % (3124083)------------------------------
% 3.76/1.21 % (3124083)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.76/1.21 % (3124083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.76/1.21 % (3124083)CaDiCaL version: 2.1.3
% 3.76/1.21 % (3124083)Termination reason: Instruction limit
% 3.76/1.21 % (3124083)Termination phase: Saturation
% 3.76/1.21 % (3124083)Time elapsed: 0.003 s
% 3.76/1.21 % (3124083)Peak memory usage: 88 MB
% 3.76/1.21 % (3124083)Instructions burned: 4 (million)
% 3.76/1.21 % (3124082)Instruction limit reached!
% 3.76/1.21 % (3124082)------------------------------
% 3.76/1.21 % (3124082)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.76/1.21 % (3124082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.76/1.21 % (3124082)CaDiCaL version: 2.1.3
% 3.76/1.21 % (3124082)Termination reason: Instruction limit
% 3.76/1.21 % (3124082)Termination phase: Saturation
% 3.76/1.21 % (3124082)Time elapsed: 0.005 s
% 3.76/1.21 % (3124082)Peak memory usage: 88 MB
% 3.76/1.21 % (3124082)Instructions burned: 8 (million)
% 3.76/1.21 % (3124079)Instruction limit reached!
% 3.76/1.21 % (3124079)------------------------------
% 3.76/1.21 % (3124079)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.76/1.21 % (3124079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.76/1.21 % (3124079)CaDiCaL version: 2.1.3
% 3.76/1.21 % (3124079)Termination reason: Instruction limit
% 3.76/1.21 % (3124079)Termination phase: Saturation
% 3.76/1.21 % (3124079)Time elapsed: 0.030 s
% 3.76/1.21 % (3124079)Peak memory usage: 116 MB
% 3.76/1.21 % (3124079)Instructions burned: 13 (million)
% 3.76/1.21 % (3124085)Instruction limit reached!
% 3.76/1.21 % (3124085)------------------------------
% 3.76/1.21 % (3124085)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.76/1.21 % (3124085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.76/1.21 % (3124085)CaDiCaL version: 2.1.3
% 3.76/1.21 % (3124085)Termination reason: Instruction limit
% 3.76/1.21 % (3124085)Termination phase: Saturation
% 3.76/1.21 % (3124085)Time elapsed: 0.047 s
% 3.76/1.21 % (3124085)Peak memory usage: 117 MB
% 3.76/1.21 % (3124085)Instructions burned: 34 (million)
% 3.76/1.21 % (3124081)Instruction limit reached!
% 3.76/1.21 % (3124081)------------------------------
% 3.76/1.21 % (3124081)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.76/1.21 % (3124081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.76/1.21 % (3124081)CaDiCaL version: 2.1.3
% 3.76/1.21 % (3124081)Termination reason: Instruction limit
% 3.76/1.21 % (3124081)Termination phase: Saturation
% 3.76/1.21 % (3124081)Time elapsed: 0.099 s
% 3.76/1.21 % (3124081)Peak memory usage: 118 MB
% 3.76/1.21 % (3124081)Instructions burned: 203 (million)
% 3.76/1.21 % (3124084)Instruction limit reached!
% 3.76/1.21 % (3124084)------------------------------
% 3.76/1.21 % (3124084)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.76/1.21 % (3124084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.76/1.29 % (3124084)CaDiCaL version: 2.1.3
% 3.76/1.29 % (3124084)Termination reason: Instruction limit
% 3.76/1.29 % (3124084)Termination phase: Saturation
% 3.76/1.29 % (3124084)Time elapsed: 0.057 s
% 3.76/1.29 % (3124084)Peak memory usage: 117 MB
% 3.76/1.29 % (3124084)Instructions burned: 47 (million)
% 3.76/1.29 % (3124093)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=1466444469:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 3.76/1.29 % (3124094)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=652665212:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi)
% 3.76/1.29 % (3124097)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=524487539:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi)
% 3.76/1.29 % (3124093)Instruction limit reached!
% 3.76/1.29 % (3124093)------------------------------
% 3.76/1.29 % (3124093)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.76/1.29 % (3124093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.76/1.29 % (3124093)CaDiCaL version: 2.1.3
% 3.76/1.29 % (3124093)Termination reason: Instruction limit
% 3.76/1.29 % (3124093)Termination phase: Saturation
% 3.76/1.29 % (3124093)Time elapsed: 0.012 s
% 3.76/1.29 % (3124093)Peak memory usage: 88 MB
% 3.76/1.29 % (3124093)Instructions burned: 15 (million)
% 3.76/1.29 % (3124097)Instruction limit reached!
% 3.76/1.29 % (3124097)------------------------------
% 3.76/1.29 % (3124097)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.76/1.29 % (3124097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.76/1.29 % (3124097)CaDiCaL version: 2.1.3
% 3.76/1.29 % (3124097)Termination reason: Instruction limit
% 3.76/1.29 % (3124097)Termination phase: Saturation
% 3.76/1.29 % (3124097)Time elapsed: 0.009 s
% 3.76/1.29 % (3124097)Peak memory usage: 89 MB
% 3.76/1.29 % (3124097)Instructions burned: 29 (million)
% 3.76/1.29 % (3124094)Instruction limit reached!
% 3.76/1.29 % (3124094)------------------------------
% 3.76/1.29 % (3124094)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.76/1.29 % (3124094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.76/1.29 % (3124094)CaDiCaL version: 2.1.3
% 3.76/1.29 % (3124094)Termination reason: Instruction limit
% 3.76/1.29 % (3124094)Termination phase: Saturation
% 3.76/1.29 % (3124094)Time elapsed: 0.021 s
% 3.76/1.29 % (3124094)Peak memory usage: 88 MB
% 3.76/1.29 % (3124094)Instructions burned: 29 (million)
% 3.76/1.29 % (3124095)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=3407212731:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi)
% 3.76/1.29 % (3124098)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=1350441526:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi)
% 3.76/1.29 % (3124095)Instruction limit reached!
% 3.76/1.29 % (3124095)------------------------------
% 3.76/1.29 % (3124095)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.76/1.29 % (3124095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.76/1.29 % (3124095)CaDiCaL version: 2.1.3
% 3.76/1.29 % (3124095)Termination reason: Instruction limit
% 3.76/1.29 % (3124095)Termination phase: Saturation
% 3.76/1.29 % (3124095)Time elapsed: 0.011 s
% 3.76/1.29 % (3124095)Peak memory usage: 90 MB
% 3.76/1.29 % (3124095)Instructions burned: 16 (million)
% 3.76/1.29 % (3124096)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=3599939430:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 3.76/1.29 % (3124096)Instruction limit reached!
% 3.76/1.29 % (3124096)------------------------------
% 3.76/1.29 % (3124096)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.76/1.29 % (3124096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.76/1.29 % (3124096)CaDiCaL version: 2.1.3
% 3.76/1.29 % (3124096)Termination reason: Instruction limit
% 3.76/1.29 % (3124096)Termination phase: Saturation
% 3.76/1.29 % (3124096)Time elapsed: 0.019 s
% 3.76/1.29 % (3124096)Peak memory usage: 89 MB
% 3.76/1.29 % (3124096)Instructions burned: 25 (million)
% 3.76/1.29 % (3124080)First to succeed.
% 3.76/1.29 % (3124080)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3124074"
% 3.76/1.29 % (3124098)Instruction limit reached!
% 3.76/1.29 % (3124098)------------------------------
% 3.76/1.29 % (3124098)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.76/1.29 % (3124098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.76/1.29 % (3124098)CaDiCaL version: 2.1.3
% 3.76/1.29 % (3124098)Termination reason: Instruction limit
% 3.76/1.29 % (3124098)Termination phase: Saturation
% 3.76/1.29 % (3124098)Time elapsed: 0.042 s
% 3.76/1.29 % (3124098)Peak memory usage: 89 MB
% 3.76/1.29 % (3124098)Instructions burned: 85 (million)
% 3.76/1.29 % (3124103)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=2346073971:i=181:rtra=on:ss=axioms:ev=cautious_2997 on theBenchmark for (2997ds/181Mi)
% 3.76/1.29 % (3124102)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=1468349809:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2997 on theBenchmark for (2997ds/2Mi)
% 3.76/1.29 % (3124102)Instruction limit reached!
% 3.76/1.29 % (3124102)------------------------------
% 3.76/1.29 % (3124102)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.76/1.29 % (3124102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.76/1.29 % (3124102)CaDiCaL version: 2.1.3
% 3.76/1.29 % (3124102)Termination reason: Instruction limit
% 3.76/1.29 % (3124102)Termination phase: Preprocessing 3
% 3.76/1.29 % (3124102)Time elapsed: 0.002 s
% 3.76/1.29 % (3124102)Peak memory usage: 86 MB
% 3.76/1.29 % (3124102)Instructions burned: 2 (million)
% 3.76/1.29 % (3124104)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=2781584342:i=4:ep=RST:ins=2:rtra=on_2997 on theBenchmark for (2997ds/4Mi)
% 3.76/1.29 % (3124104)Instruction limit reached!
% 3.76/1.29 % (3124104)------------------------------
% 3.76/1.29 % (3124104)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.76/1.29 % (3124104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.76/1.29 % (3124104)CaDiCaL version: 2.1.3
% 3.76/1.29 % (3124104)Termination reason: Instruction limit
% 3.76/1.29 % (3124104)Termination phase: Saturation
% 3.76/1.29 % (3124104)Time elapsed: 0.003 s
% 3.76/1.29 % (3124104)Peak memory usage: 88 MB
% 3.76/1.29 % (3124104)Instructions burned: 4 (million)
% 3.76/1.29 % (3124103)Instruction limit reached!
% 3.76/1.29 % (3124103)------------------------------
% 3.76/1.29 % (3124103)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.76/1.29 % (3124103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.76/1.29 % (3124103)CaDiCaL version: 2.1.3
% 3.76/1.29 % (3124103)Termination reason: Instruction limit
% 3.76/1.29 % (3124103)Termination phase: Saturation
% 3.76/1.29 % (3124103)Time elapsed: 0.071 s
% 3.76/1.29 % (3124103)Peak memory usage: 90 MB
% 3.76/1.29 % (3124103)Instructions burned: 181 (million)
% 3.76/1.29 % (3124108)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=1294228618:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2996 on theBenchmark for (2996ds/66Mi)
% 3.76/1.29 % (3124109)lrs+10_1_thi=all:si=on:fd=off:random_seed=1949418369:i=53:rtra=on:gtg=all_2996 on theBenchmark for (2996ds/53Mi)
% 3.76/1.29 % (3124110)ott+1011_1_to=kbo:plsq=on:drc=off:si=on:plsqr=32,1:sp=const_frequency:sos=all:uwa=one_side_interpreted:sac=on:random_seed=752325817:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2996 on theBenchmark for (2996ds/8Mi)
% 3.76/1.29 % (3124110)Instruction limit reached!
% 3.76/1.29 % (3124110)------------------------------
% 3.76/1.29 % (3124110)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.76/1.29 % (3124110)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.76/1.29 % (3124110)CaDiCaL version: 2.1.3
% 3.76/1.29 % (3124110)Termination reason: Instruction limit
% 3.76/1.29 % (3124110)Termination phase: Saturation
% 3.76/1.29 % (3124110)Time elapsed: 0.006 s
% 3.76/1.29 % (3124110)Peak memory usage: 88 MB
% 3.76/1.29 % (3124110)Instructions burned: 9 (million)
% 3.76/1.29 % (3124116)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=1412060683:i=127:doe=on:rtra=on_2995 on theBenchmark for (2995ds/127Mi)
% 3.76/1.29 % (3124113)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=1896928217:st=3:i=2:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/2Mi)
% 3.76/1.29 % (3124113)Instruction limit reached!
% 3.76/1.29 % (3124113)------------------------------
% 3.76/1.29 % (3124113)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.76/1.29 % (3124113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.76/1.29 % (3124113)CaDiCaL version: 2.1.3
% 3.76/1.29 % (3124113)Termination reason: Instruction limit
% 3.76/1.29 % (3124113)Termination phase: Property scanning
% 3.76/1.29 % (3124113)Time elapsed: 0.002 s
% 3.76/1.29 % (3124113)Peak memory usage: 86 MB
% 3.76/1.29 % (3124113)Instructions burned: 2 (million)
% 3.76/1.29 % (3124109)Instruction limit reached!
% 3.76/1.29 % (3124109)------------------------------
% 3.76/1.29 % (3124109)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.76/1.29 % (3124109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.76/1.29 % (3124109)CaDiCaL version: 2.1.3
% 3.76/1.29 % (3124109)Termination reason: Instruction limit
% 3.76/1.29 % (3124109)Termination phase: Saturation
% 3.76/1.29 % (3124109)Time elapsed: 0.066 s
% 3.76/1.29 % (3124109)Peak memory usage: 117 MB
% 3.76/1.29 % (3124109)Instructions burned: 54 (million)
% 3.76/1.29 % (3124108)Instruction limit reached!
% 3.76/1.29 % (3124108)------------------------------
% 3.76/1.29 % (3124108)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.76/1.29 % (3124108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.76/1.29 % (3124108)CaDiCaL version: 2.1.3
% 3.76/1.29 % (3124108)Termination reason: Instruction limit
% 3.76/1.29 % (3124108)Termination phase: Saturation
% 3.76/1.29 % (3124108)Time elapsed: 0.094 s
% 3.76/1.29 % (3124108)Peak memory usage: 134 MB
% 3.76/1.29 % (3124108)Instructions burned: 66 (million)
% 3.76/1.29 % (3124115)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=842519749:i=2:doe=on:canc=force:asg=cautious:rtra=on_2995 on theBenchmark for (2995ds/2Mi)
% 3.76/1.29 % (3124115)Instruction limit reached!
% 3.76/1.29 % (3124115)------------------------------
% 3.76/1.29 % (3124115)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.76/1.29 % (3124115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.76/1.29 % (3124115)CaDiCaL version: 2.1.3
% 3.76/1.29 % (3124115)Termination reason: Instruction limit
% 3.76/1.29 % (3124115)Termination phase: Property scanning
% 3.76/1.29 % (3124115)Time elapsed: 0.002 s
% 3.76/1.29 % (3124115)Peak memory usage: 86 MB
% 3.76/1.29 % (3124115)Instructions burned: 2 (million)
% 3.76/1.29 % (3124116)Instruction limit reached!
% 3.76/1.29 % (3124116)------------------------------
% 3.76/1.29 % (3124116)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.76/1.29 % (3124116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.76/1.29 % (3124116)CaDiCaL version: 2.1.3
% 3.76/1.29 % (3124116)Termination reason: Instruction limit
% 3.76/1.29 % (3124116)Termination phase: Saturation
% 3.76/1.29 % (3124116)Time elapsed: 0.057 s
% 3.76/1.29 % (3124116)Peak memory usage: 118 MB
% 3.76/1.29 % (3124116)Instructions burned: 128 (million)
% 3.76/1.29 % (3124120)dis+10_1_si=on:random_seed=3288558095:i=10:ep=R:rtra=on_2994 on theBenchmark for (2994ds/10Mi)
% 3.76/1.29 % (3124080)Refutation found. Thanks to Tanya!
% 3.76/1.29 % SZS status Theorem for theBenchmark
% 3.76/1.29 % SZS output start Proof for theBenchmark
% See solution above
% 5.06/1.49 % (3124080)------------------------------
% 5.06/1.49 % (3124080)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.06/1.49 % (3124080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.06/1.49 % (3124080)CaDiCaL version: 2.1.3
% 5.06/1.49 % (3124080)Termination reason: Refutation
% 5.06/1.49 % (3124080)Time elapsed: 0.218 s
% 5.06/1.49 % (3124080)Peak memory usage: 120 MB
% 5.06/1.49 % (3124080)Instructions burned: 306 (million)
% 5.06/1.49 % (3124080)------------------------------
% 5.06/1.49 % (3124080)------------------------------
% 5.06/1.49 % (3124074)Success in time 0.633 s
% 5.06/1.49 % Vampire exiting
%------------------------------------------------------------------------------