%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWX072_1 : TPTP v9.3.1. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n014.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:49 PM UTC 2026
% Result : Theorem 3.73s 1.27s
% Output : Refutation 4.85s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 19
% Syntax : Number of formulae : 100 ( 7 unt; 0 typ; 11 def)
% Number of atoms : 358 ( 113 equ)
% Maximal formula atoms : 16 ( 3 avg)
% Number of connectives : 434 ( 176 ~; 173 |; 55 &)
% ( 16 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 15 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number arithmetic : 110 ( 14 atm; 0 fun; 82 num; 14 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 : 23 ( 18 usr; 12 prp; 0-2 aty)
% Number of functors : 11 ( 8 usr; 7 con; 0-1 aty)
% Number of variables : 144 ( 127 !; 17 ?; 144 :)
% 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_7,type,
sK0: general ).
tff(func_def_8,type,
sK1: general > $int ).
tff(func_def_9,type,
sK2: general > symbol ).
tff(func_def_10,type,
sF3: 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,
hp: general > $o ).
tff(pred_def_9,type,
tp: general > $o ).
tff(f6,axiom,
! [X0: $int,X1: $int] :
( $lesseq(X0,X1)
<=> p__less_equal__(f__integer__(X0),f__integer__(X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',numeral_ordering_ax) ).
tff(f8,axiom,
! [X1: general,X2: general,X0: general] :
( ( p__less_equal__(X1,X2)
& p__less_equal__(X0,X1) )
=> p__less_equal__(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',transitive_ordering_ax) ).
tff(f9,axiom,
! [X0: general,X1: general] :
( p__less_equal__(X1,X0)
| p__less_equal__(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',strongly_connected_ordering_ax) ).
tff(f10,axiom,
! [X1: general,X0: general] :
( p__less__(X0,X1)
<=> ( p__less_equal__(X0,X1)
& ( X0 != X1 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p__less__def_ax) ).
tff(f12,axiom,
! [X1: general,X0: general] :
( p__greater__(X0,X1)
<=> ( ( X0 != X1 )
& p__less_equal__(X1,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',p__greater__def_ax) ).
tff(f16,axiom,
! [X0: general] :
( hp(X0)
=> tp(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_0_transition_axiom_0) ).
tff(f17,axiom,
! [X1: general,X0: general] :
( ( ( ? [X2: general,X3: general] :
( ( X3 = f__integer__(3) )
& p__greater__(X2,X3)
& ( X2 = X1 ) )
& ( X0 = X1 )
& ? [X3: general,X2: general] :
( ( X2 = X1 )
& ( X3 = f__integer__(5) )
& p__less__(X2,X3) ) )
=> hp(X0) )
& ( ( ? [X2: general,X3: general] :
( ( X2 = X1 )
& p__less__(X2,X3)
& ( X3 = f__integer__(5) ) )
& ? [X2: general,X3: general] :
( ( X3 = f__integer__(3) )
& p__greater__(X2,X3)
& ( X2 = X1 ) )
& ( X0 = X1 ) )
=> tp(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_1_left_0) ).
tff(f18,conjecture,
! [X0: general] :
( ( ( ( X0 = f__integer__(4) )
& $true )
=> hp(X0) )
& ( ( ( X0 = f__integer__(4) )
& $true )
=> tp(X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_2_right_0) ).
tff(f19,negated_conjecture,
~ ! [X0: general] :
( ( ( ( X0 = f__integer__(4) )
& $true )
=> hp(X0) )
& ( ( ( X0 = f__integer__(4) )
& $true )
=> tp(X0) ) ),
inference(negated_conjecture,[status(cth)],[f18]) ).
tff(f20,plain,
! [X1: $int,X0: $int] :
( ~ $less(X1,X0)
<=> p__less_equal__(f__integer__(X0),f__integer__(X1)) ),
inference(theory_normalization,[],[f6]) ).
tff(f22,plain,
! [X1: general,X0: general] :
( p__less__(X1,X0)
<=> ( p__less_equal__(X1,X0)
& ( X0 != X1 ) ) ),
inference(rectify,[],[f10]) ).
tff(f24,plain,
~ ! [X0: general] :
( ( ( X0 = f__integer__(4) )
=> tp(X0) )
& ( ( X0 = f__integer__(4) )
=> hp(X0) ) ),
inference(true_and_false_elimination,[],[f19]) ).
tff(f25,plain,
! [X1: general,X0: general,X2: general] :
( ( p__less_equal__(X0,X1)
& p__less_equal__(X2,X0) )
=> p__less_equal__(X2,X1) ),
inference(rectify,[],[f8]) ).
tff(f26,plain,
! [X0: general,X1: general] :
( ( ( ( X0 = X1 )
& ? [X8: general,X9: general] :
( p__greater__(X8,X9)
& ( f__integer__(3) = X9 )
& ( X0 = X8 ) )
& ? [X7: general,X6: general] :
( p__less__(X6,X7)
& ( f__integer__(5) = X7 )
& ( X0 = X6 ) ) )
=> tp(X1) )
& ( ( ( X0 = X1 )
& ? [X4: general,X5: general] :
( ( X0 = X5 )
& ( f__integer__(5) = X4 )
& p__less__(X5,X4) )
& ? [X2: general,X3: general] :
( ( X3 = f__integer__(3) )
& ( X0 = X2 )
& p__greater__(X2,X3) ) )
=> hp(X1) ) ),
inference(rectify,[],[f17]) ).
tff(f28,plain,
! [X1: general,X0: general] :
( ( p__less_equal__(X0,X1)
& ( X0 != X1 ) )
<=> p__greater__(X1,X0) ),
inference(rectify,[],[f12]) ).
tff(f29,plain,
! [X1: general,X0: general] :
( ( p__less_equal__(X0,X1)
& ( X0 != X1 ) )
=> p__greater__(X1,X0) ),
inference(unused_predicate_definition_removal,[],[f28]) ).
tff(f32,plain,
? [X0: general] :
( ( ~ tp(X0)
& ( X0 = f__integer__(4) ) )
| ( ~ hp(X0)
& ( X0 = f__integer__(4) ) ) ),
inference(ennf_transformation,[],[f24]) ).
tff(f34,plain,
! [X0: general,X1: general] :
( ( tp(X1)
| ( X0 != X1 )
| ! [X9: general,X8: general] :
( ( X0 != X8 )
| ~ p__greater__(X8,X9)
| ( f__integer__(3) != X9 ) )
| ! [X7: general,X6: general] :
( ( X0 != X6 )
| ( f__integer__(5) != X7 )
| ~ p__less__(X6,X7) ) )
& ( hp(X1)
| ( X0 != X1 )
| ! [X5: general,X4: general] :
( ~ p__less__(X5,X4)
| ( f__integer__(5) != X4 )
| ( X0 != X5 ) )
| ! [X3: general,X2: general] :
( ( f__integer__(3) != X3 )
| ( X0 != X2 )
| ~ p__greater__(X2,X3) ) ) ),
inference(ennf_transformation,[],[f26]) ).
tff(f35,plain,
! [X0: general,X1: general] :
( ( ! [X3: general,X2: general] :
( ( f__integer__(3) != X3 )
| ( X0 != X2 )
| ~ p__greater__(X2,X3) )
| hp(X1)
| ! [X5: general,X4: general] :
( ~ p__less__(X5,X4)
| ( f__integer__(5) != X4 )
| ( X0 != X5 ) )
| ( X0 != X1 ) )
& ( tp(X1)
| ( X0 != X1 )
| ! [X7: general,X6: general] :
( ( X0 != X6 )
| ( f__integer__(5) != X7 )
| ~ p__less__(X6,X7) )
| ! [X9: general,X8: general] :
( ( X0 != X8 )
| ~ p__greater__(X8,X9)
| ( f__integer__(3) != X9 ) ) ) ),
inference(flattening,[],[f34]) ).
tff(f36,plain,
! [X0: general] :
( tp(X0)
| ~ hp(X0) ),
inference(ennf_transformation,[],[f16]) ).
tff(f37,plain,
! [X1: general,X0: general] :
( p__greater__(X1,X0)
| ~ p__less_equal__(X0,X1)
| ( X0 = X1 ) ),
inference(ennf_transformation,[],[f29]) ).
tff(f38,plain,
! [X1: general,X0: general] :
( ( X0 = X1 )
| p__greater__(X1,X0)
| ~ p__less_equal__(X0,X1) ),
inference(flattening,[],[f37]) ).
tff(f42,plain,
! [X1: general,X0: general,X2: general] :
( p__less_equal__(X2,X1)
| ~ p__less_equal__(X0,X1)
| ~ p__less_equal__(X2,X0) ),
inference(ennf_transformation,[],[f25]) ).
tff(f43,plain,
! [X2: general,X0: general,X1: general] :
( ~ p__less_equal__(X2,X0)
| p__less_equal__(X2,X1)
| ~ p__less_equal__(X0,X1) ),
inference(flattening,[],[f42]) ).
tff(f45,plain,
( ( ~ tp(sK0)
& ( f__integer__(4) = sK0 ) )
| ( ~ hp(sK0)
& ( f__integer__(4) = sK0 ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X0,sK0)],[f32]) ).
tff(f46,plain,
! [X1: general,X0: general] :
( ( p__less__(X1,X0)
| ~ p__less_equal__(X1,X0)
| ( X0 = X1 ) )
& ( ( p__less_equal__(X1,X0)
& ( X0 != X1 ) )
| ~ p__less__(X1,X0) ) ),
inference(nnf_transformation,[],[f22]) ).
tff(f47,plain,
! [X1: general,X0: general] :
( ( p__less__(X1,X0)
| ~ p__less_equal__(X1,X0)
| ( X0 = X1 ) )
& ( ( p__less_equal__(X1,X0)
& ( X0 != X1 ) )
| ~ p__less__(X1,X0) ) ),
inference(flattening,[],[f46]) ).
tff(f48,plain,
! [X0: general,X1: general] :
( ( p__less__(X0,X1)
| ~ p__less_equal__(X0,X1)
| ( X0 = X1 ) )
& ( ( p__less_equal__(X0,X1)
& ( X0 != X1 ) )
| ~ p__less__(X0,X1) ) ),
inference(rectify,[],[f47]) ).
tff(f53,plain,
! [X0: general,X1: general] :
( ( X0 = X1 )
| p__greater__(X0,X1)
| ~ p__less_equal__(X1,X0) ),
inference(rectify,[],[f38]) ).
tff(f54,plain,
! [X0: general,X1: general] :
( ( ! [X2: general,X3: general] :
( ( f__integer__(3) != X2 )
| ( X0 != X3 )
| ~ p__greater__(X3,X2) )
| hp(X1)
| ! [X4: general,X5: general] :
( ~ p__less__(X4,X5)
| ( f__integer__(5) != X5 )
| ( X0 != X4 ) )
| ( X0 != X1 ) )
& ( tp(X1)
| ( X0 != X1 )
| ! [X6: general,X7: general] :
( ( X0 != X7 )
| ( f__integer__(5) != X6 )
| ~ p__less__(X7,X6) )
| ! [X8: general,X9: general] :
( ( X0 != X9 )
| ~ p__greater__(X9,X8)
| ( f__integer__(3) != X8 ) ) ) ),
inference(rectify,[],[f35]) ).
tff(f56,plain,
! [X0: general,X1: general,X2: general] :
( ~ p__less_equal__(X0,X1)
| p__less_equal__(X0,X2)
| ~ p__less_equal__(X1,X2) ),
inference(rectify,[],[f43]) ).
tff(f57,plain,
! [X1: $int,X0: $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(nnf_transformation,[],[f20]) ).
tff(f58,plain,
! [X0: $int,X1: $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(rectify,[],[f57]) ).
tff(f62,plain,
( ( f__integer__(4) = sK0 )
| ( f__integer__(4) = sK0 ) ),
inference(cnf_transformation,[],[f45]) ).
tff(f65,plain,
( ~ tp(sK0)
| ~ hp(sK0) ),
inference(cnf_transformation,[],[f45]) ).
tff(f68,plain,
! [X0: general,X1: general] :
( p__less__(X0,X1)
| ~ p__less_equal__(X0,X1)
| ( X0 = X1 ) ),
inference(cnf_transformation,[],[f48]) ).
tff(f70,plain,
! [X0: general,X1: general] :
( p__less_equal__(X1,X0)
| p__less_equal__(X0,X1) ),
inference(cnf_transformation,[],[f9]) ).
tff(f75,plain,
! [X0: general,X1: general] :
( p__greater__(X0,X1)
| ( X0 = X1 )
| ~ p__less_equal__(X1,X0) ),
inference(cnf_transformation,[],[f53]) ).
tff(f76,plain,
! [X0: general] :
( tp(X0)
| ~ hp(X0) ),
inference(cnf_transformation,[],[f36]) ).
tff(f78,plain,
! [X2: general,X3: general,X0: general,X1: general,X4: general,X5: general] :
( ( f__integer__(3) != X2 )
| ( X0 != X3 )
| ~ p__greater__(X3,X2)
| hp(X1)
| ~ p__less__(X4,X5)
| ( f__integer__(5) != X5 )
| ( X0 != X4 )
| ( X0 != X1 ) ),
inference(cnf_transformation,[],[f54]) ).
tff(f81,plain,
! [X2: general,X0: general,X1: general] :
( p__less_equal__(X0,X2)
| ~ p__less_equal__(X0,X1)
| ~ p__less_equal__(X1,X2) ),
inference(cnf_transformation,[],[f56]) ).
tff(f84,plain,
! [X0: $int,X1: $int] :
( ~ p__less_equal__(f__integer__(X1),f__integer__(X0))
| ~ $less(X0,X1) ),
inference(cnf_transformation,[],[f58]) ).
tff(f88,plain,
! [X3: general,X0: general,X1: general,X4: general,X5: general] :
( ( X0 != X3 )
| ~ p__greater__(X3,f__integer__(3))
| hp(X1)
| ~ p__less__(X4,X5)
| ( f__integer__(5) != X5 )
| ( X0 != X4 )
| ( X0 != X1 ) ),
inference(equality_resolution,[],[f78]) ).
tff(f89,plain,
! [X3: general,X1: general,X4: general,X5: general] :
( ~ p__greater__(X3,f__integer__(3))
| hp(X1)
| ~ p__less__(X4,X5)
| ( f__integer__(5) != X5 )
| ( X3 != X4 )
| ( X1 != X3 ) ),
inference(equality_resolution,[],[f88]) ).
tff(f90,plain,
! [X3: general,X1: general,X4: general] :
( ~ p__greater__(X3,f__integer__(3))
| hp(X1)
| ~ p__less__(X4,f__integer__(5))
| ( X3 != X4 )
| ( X1 != X3 ) ),
inference(equality_resolution,[],[f89]) ).
tff(f91,plain,
! [X1: general,X4: general] :
( ~ p__greater__(X4,f__integer__(3))
| hp(X1)
| ~ p__less__(X4,f__integer__(5))
| ( X1 != X4 ) ),
inference(equality_resolution,[],[f90]) ).
tff(f92,plain,
! [X4: general] :
( ~ p__greater__(X4,f__integer__(3))
| hp(X4)
| ~ p__less__(X4,f__integer__(5)) ),
inference(equality_resolution,[],[f91]) ).
tff(f98,definition,
sF3 = f__integer__(4),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
tff(f99,plain,
f__integer__(4) = sF3,
inference(reorient_equations,[],[f98]) ).
tff(f102,plain,
( ( sK0 = sF3 )
| ( sK0 = sF3 ) ),
inference(definition_folding,[],[f62,f99,f99]) ).
tff(f103,plain,
sK0 = sF3,
inference(duplicate_literal_removal,[],[f102]) ).
tff(f105,definition,
( spl4_1
<=> hp(sK0) ),
introduced(definition,[new_symbols(definition,[spl4_1])],[avatar_definition]) ).
tff(f109,definition,
( spl4_2
<=> tp(sK0) ),
introduced(definition,[new_symbols(definition,[spl4_2])],[avatar_definition]) ).
tff(f111,plain,
( ~ tp(sK0)
| spl4_2 ),
inference(avatar_component_clause,[],[f109]) ).
tff(f112,plain,
( ~ spl4_1
| ~ spl4_2 ),
inference(avatar_split_clause,[],[f65,f109,f105]) ).
tff(f114,definition,
( spl4_3
<=> ( sK0 = sF3 ) ),
introduced(definition,[new_symbols(definition,[spl4_3])],[avatar_definition]) ).
tff(f116,plain,
( ( sK0 = sF3 )
| ~ spl4_3 ),
inference(avatar_component_clause,[],[f114]) ).
tff(f118,plain,
spl4_3,
inference(avatar_split_clause,[],[f103,f114]) ).
tff(f120,definition,
( spl4_4
<=> ( f__integer__(4) = sF3 ) ),
introduced(definition,[new_symbols(definition,[spl4_4])],[avatar_definition]) ).
tff(f122,plain,
( ( f__integer__(4) = sF3 )
| ~ spl4_4 ),
inference(avatar_component_clause,[],[f120]) ).
tff(f123,plain,
spl4_4,
inference(avatar_split_clause,[],[f99,f120]) ).
tff(f125,plain,
( ( f__integer__(4) = sK0 )
| ~ spl4_3
| ~ spl4_4 ),
inference(forward_demodulation,[],[f122,f116]) ).
tff(f127,definition,
( spl4_5
<=> ( f__integer__(4) = sK0 ) ),
introduced(definition,[new_symbols(definition,[spl4_5])],[avatar_definition]) ).
tff(f129,plain,
( ( f__integer__(4) = sK0 )
| ~ spl4_5 ),
inference(avatar_component_clause,[],[f127]) ).
tff(f130,plain,
( spl4_5
| ~ spl4_3
| ~ spl4_4 ),
inference(avatar_split_clause,[],[f125,f120,f114,f127]) ).
tff(f148,plain,
! [X0: general] : p__less_equal__(X0,X0),
inference(factoring,[],[f70]) ).
tff(f177,plain,
( ! [X0: $int] :
( ~ p__less_equal__(sK0,f__integer__(X0))
| ~ $less(X0,4) )
| ~ spl4_5 ),
inference(superposition,[],[f84,f129]) ).
tff(f179,plain,
( ! [X0: $int] :
( ~ p__less_equal__(f__integer__(X0),sK0)
| ~ $less(4,X0) )
| ~ spl4_5 ),
inference(superposition,[],[f84,f129]) ).
tff(f228,plain,
! [X0: general] :
( ~ p__less__(X0,f__integer__(5))
| hp(X0)
| ( f__integer__(3) = X0 )
| ~ p__less_equal__(f__integer__(3),X0) ),
inference(resolution,[],[f92,f75]) ).
tff(f251,plain,
( ! [X0: $int] :
( p__less_equal__(f__integer__(X0),sK0)
| ~ $less(X0,4) )
| ~ spl4_5 ),
inference(resolution,[],[f177,f70]) ).
tff(f255,plain,
( ! [X0: $int,X1: general] :
( ~ p__less_equal__(f__integer__(X0),X1)
| ~ p__less_equal__(X1,sK0)
| ~ $less(4,X0) )
| ~ spl4_5 ),
inference(resolution,[],[f179,f81]) ).
tff(f444,plain,
! [X0: general] :
( ~ p__less_equal__(f__integer__(3),X0)
| ( f__integer__(5) = X0 )
| ~ p__less_equal__(X0,f__integer__(5))
| ( f__integer__(3) = X0 )
| hp(X0) ),
inference(resolution,[],[f228,f68]) ).
tff(f479,definition,
( spl4_24
<=> p__less_equal__(f__integer__(3),sK0) ),
introduced(definition,[new_symbols(definition,[spl4_24])],[avatar_definition]) ).
tff(f480,plain,
( p__less_equal__(f__integer__(3),sK0)
| ~ spl4_24 ),
inference(avatar_component_clause,[],[f479]) ).
tff(f481,plain,
( ~ p__less_equal__(f__integer__(3),sK0)
| spl4_24 ),
inference(avatar_component_clause,[],[f479]) ).
tff(f483,definition,
( spl4_25
<=> ( f__integer__(3) = sK0 ) ),
introduced(definition,[new_symbols(definition,[spl4_25])],[avatar_definition]) ).
tff(f485,plain,
( ( f__integer__(3) = sK0 )
| ~ spl4_25 ),
inference(avatar_component_clause,[],[f483]) ).
tff(f2539,definition,
( spl4_75
<=> p__less_equal__(sK0,f__integer__(5)) ),
introduced(definition,[new_symbols(definition,[spl4_75])],[avatar_definition]) ).
tff(f2543,definition,
( spl4_76
<=> ( f__integer__(5) = sK0 ) ),
introduced(definition,[new_symbols(definition,[spl4_76])],[avatar_definition]) ).
tff(f2714,definition,
( spl4_101
<=> p__less_equal__(f__integer__(5),sK0) ),
introduced(definition,[new_symbols(definition,[spl4_101])],[avatar_definition]) ).
tff(f2715,plain,
( ~ p__less_equal__(f__integer__(5),sK0)
| spl4_101 ),
inference(avatar_component_clause,[],[f2714]) ).
tff(f2716,plain,
( p__less_equal__(f__integer__(5),sK0)
| ~ spl4_101 ),
inference(avatar_component_clause,[],[f2714]) ).
tff(f2746,plain,
( ~ $less(3,4)
| ~ spl4_5
| spl4_24 ),
inference(resolution,[],[f481,f251]) ).
tff(f2759,plain,
( $false
| ~ spl4_5
| spl4_24 ),
inference(evaluation,[],[f2746]) ).
tff(f2760,plain,
( ~ spl4_5
| spl4_24 ),
inference(avatar_contradiction_clause,[],[f2759]) ).
tff(f2886,plain,
( ( f__integer__(3) = sK0 )
| ( f__integer__(5) = sK0 )
| hp(sK0)
| ~ p__less_equal__(sK0,f__integer__(5))
| ~ spl4_24 ),
inference(resolution,[],[f480,f444]) ).
tff(f2940,plain,
( ~ $less(4,5)
| ~ p__less_equal__(sK0,sK0)
| ~ spl4_5
| ~ spl4_101 ),
inference(resolution,[],[f2716,f255]) ).
tff(f2950,plain,
( ~ p__less_equal__(sK0,sK0)
| ~ spl4_5
| ~ spl4_101 ),
inference(evaluation,[],[f2940]) ).
tff(f2955,plain,
( $false
| ~ spl4_5
| ~ spl4_101 ),
inference(forward_subsumption_resolution,[],[f2950,f148]) ).
tff(f2956,plain,
( ~ spl4_5
| ~ spl4_101 ),
inference(avatar_contradiction_clause,[],[f2955]) ).
tff(f2989,plain,
( p__less_equal__(sK0,f__integer__(5))
| spl4_101 ),
inference(resolution,[],[f2715,f70]) ).
tff(f2999,plain,
( spl4_75
| spl4_101 ),
inference(avatar_split_clause,[],[f2989,f2714,f2539]) ).
tff(f3002,plain,
( spl4_1
| spl4_76
| spl4_25
| ~ spl4_75
| ~ spl4_24 ),
inference(avatar_split_clause,[],[f2886,f479,f2539,f483,f2543,f105]) ).
tff(f3003,plain,
( ~ hp(sK0)
| spl4_2 ),
inference(resolution,[],[f111,f76]) ).
tff(f3006,plain,
( ~ spl4_1
| spl4_2 ),
inference(avatar_split_clause,[],[f3003,f109,f105]) ).
tff(f3032,plain,
( ~ p__less_equal__(sK0,sK0)
| ~ $less(3,4)
| ~ spl4_5
| ~ spl4_25 ),
inference(superposition,[],[f177,f485]) ).
tff(f3068,plain,
( ~ p__less_equal__(sK0,sK0)
| ~ spl4_5
| ~ spl4_25 ),
inference(evaluation,[],[f3032]) ).
tff(f3075,plain,
( $false
| ~ spl4_5
| ~ spl4_25 ),
inference(forward_subsumption_resolution,[],[f3068,f148]) ).
tff(f3076,plain,
( ~ spl4_5
| ~ spl4_25 ),
inference(avatar_contradiction_clause,[],[f3075]) ).
tff(f3084,plain,
$false,
inference(avatar_smt_refutation,[],[f3076,f3006,f3002,f2999,f2956,f2760,f130,f123,f118,f112]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX072_1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.18 % Computer : n014.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:00:15 UTC 2026
% 0.09/0.18 % CPUTime :
% 0.09/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.21 Running first-order theorem proving
% 0.09/0.21 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.73/1.26 % (1831824)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 3.73/1.26 % (1831832)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=3220647158:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 3.73/1.26 % (1831832)Instruction limit reached!
% 3.73/1.26 % (1831832)------------------------------
% 3.73/1.26 % (1831832)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.73/1.26 % (1831832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.73/1.26 % (1831832)CaDiCaL version: 2.1.3
% 3.73/1.26 % (1831832)Termination reason: Instruction limit
% 3.73/1.26 % (1831832)Termination phase: Saturation
% 3.73/1.26 % (1831832)Time elapsed: 0.004 s
% 3.73/1.26 % (1831832)Peak memory usage: 88 MB
% 3.73/1.26 % (1831832)Instructions burned: 10 (million)
% 3.73/1.26 % (1831833)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=2434036323:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 3.73/1.26 % (1831831)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2710339157:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 3.73/1.26 % (1831829)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=3727113201:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 3.73/1.26 % (1831830)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3322998221:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 3.73/1.26 % (1831833)Instruction limit reached!
% 3.73/1.26 % (1831833)------------------------------
% 3.73/1.26 % (1831833)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.73/1.26 % (1831833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.73/1.26 % (1831833)CaDiCaL version: 2.1.3
% 3.73/1.26 % (1831833)Termination reason: Instruction limit
% 3.73/1.26 % (1831833)Termination phase: Saturation
% 3.73/1.26 % (1831833)Time elapsed: 0.004 s
% 3.73/1.26 % (1831833)Peak memory usage: 88 MB
% 3.73/1.26 % (1831833)Instructions burned: 4 (million)
% 3.73/1.26 % (1831834)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=3060283336:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 3.73/1.26 % (1831835)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=4151123092:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 3.73/1.26 % (1831829)Instruction limit reached!
% 3.73/1.26 % (1831829)------------------------------
% 3.73/1.26 % (1831829)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.73/1.26 % (1831829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.73/1.26 % (1831829)CaDiCaL version: 2.1.3
% 3.73/1.26 % (1831829)Termination reason: Instruction limit
% 3.73/1.26 % (1831829)Termination phase: Saturation
% 3.73/1.26 % (1831829)Time elapsed: 0.032 s
% 3.73/1.26 % (1831829)Peak memory usage: 115 MB
% 3.73/1.26 % (1831829)Instructions burned: 13 (million)
% 3.73/1.26 % (1831835)Instruction limit reached!
% 3.73/1.26 % (1831835)------------------------------
% 3.73/1.26 % (1831835)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.73/1.26 % (1831835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.73/1.26 % (1831835)CaDiCaL version: 2.1.3
% 3.73/1.26 % (1831835)Termination reason: Instruction limit
% 3.73/1.26 % (1831835)Termination phase: Saturation
% 3.73/1.26 % (1831835)Time elapsed: 0.046 s
% 3.73/1.26 % (1831835)Peak memory usage: 115 MB
% 3.73/1.26 % (1831835)Instructions burned: 33 (million)
% 3.73/1.26 % (1831834)Instruction limit reached!
% 3.73/1.26 % (1831834)------------------------------
% 3.73/1.26 % (1831834)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.73/1.26 % (1831834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.73/1.26 % (1831834)CaDiCaL version: 2.1.3
% 3.73/1.26 % (1831834)Termination reason: Instruction limit
% 3.73/1.26 % (1831834)Termination phase: Saturation
% 3.73/1.26 % (1831834)Time elapsed: 0.053 s
% 3.73/1.26 % (1831834)Peak memory usage: 115 MB
% 3.73/1.26 % (1831834)Instructions burned: 46 (million)
% 3.73/1.26 % (1831837)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=1712514651:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 3.73/1.26 % (1831837)Instruction limit reached!
% 3.73/1.26 % (1831837)------------------------------
% 3.73/1.26 % (1831837)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.73/1.26 % (1831837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.73/1.26 % (1831837)CaDiCaL version: 2.1.3
% 3.73/1.26 % (1831837)Termination reason: Instruction limit
% 3.73/1.26 % (1831837)Termination phase: Saturation
% 3.73/1.26 % (1831837)Time elapsed: 0.006 s
% 3.73/1.26 % (1831837)Peak memory usage: 88 MB
% 3.73/1.26 % (1831837)Instructions burned: 15 (million)
% 3.73/1.26 % (1831831)Instruction limit reached!
% 3.73/1.26 % (1831831)------------------------------
% 3.73/1.26 % (1831831)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.73/1.26 % (1831831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.73/1.26 % (1831831)CaDiCaL version: 2.1.3
% 3.73/1.26 % (1831831)Termination reason: Instruction limit
% 3.73/1.26 % (1831831)Termination phase: Saturation
% 3.73/1.26 % (1831831)Time elapsed: 0.136 s
% 3.73/1.26 % (1831831)Peak memory usage: 116 MB
% 3.73/1.26 % (1831831)Instructions burned: 201 (million)
% 3.73/1.26 % (1831844)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=4155423158:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi)
% 3.73/1.26 % (1831830)First to succeed.
% 3.73/1.26 % (1831844)Instruction limit reached!
% 3.73/1.26 % (1831844)------------------------------
% 3.73/1.26 % (1831844)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.73/1.26 % (1831844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.73/1.26 % (1831844)CaDiCaL version: 2.1.3
% 3.73/1.26 % (1831844)Termination reason: Instruction limit
% 3.73/1.26 % (1831844)Termination phase: Saturation
% 3.73/1.26 % (1831844)Time elapsed: 0.023 s
% 3.73/1.26 % (1831844)Peak memory usage: 88 MB
% 3.73/1.26 % (1831844)Instructions burned: 30 (million)
% 3.73/1.26 % (1831830)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-1831824"
% 3.73/1.26 % (1831845)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=378277420:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi)
% 3.73/1.26 % (1831845)Instruction limit reached!
% 3.73/1.26 % (1831845)------------------------------
% 3.73/1.26 % (1831845)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.73/1.26 % (1831845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.73/1.26 % (1831845)CaDiCaL version: 2.1.3
% 3.73/1.26 % (1831845)Termination reason: Instruction limit
% 3.73/1.26 % (1831845)Termination phase: Saturation
% 3.73/1.26 % (1831845)Time elapsed: 0.013 s
% 3.73/1.26 % (1831845)Peak memory usage: 90 MB
% 3.73/1.26 % (1831845)Instructions burned: 17 (million)
% 3.73/1.26 % (1831846)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=1295583261:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 3.73/1.26 % (1831847)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=1898361322:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi)
% 3.73/1.26 % (1831849)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=288031525:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi)
% 3.73/1.26 % (1831846)Also succeeded, but the first one will report.
% 3.73/1.26 % (1831847)Instruction limit reached!
% 3.73/1.26 % (1831847)------------------------------
% 3.73/1.26 % (1831847)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.73/1.26 % (1831847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.73/1.26 % (1831847)CaDiCaL version: 2.1.3
% 3.73/1.26 % (1831847)Termination reason: Instruction limit
% 3.73/1.26 % (1831847)Termination phase: Saturation
% 3.73/1.26 % (1831847)Time elapsed: 0.021 s
% 3.73/1.26 % (1831847)Peak memory usage: 90 MB
% 3.73/1.26 % (1831847)Instructions burned: 28 (million)
% 3.73/1.26 % (1831849)Instruction limit reached!
% 3.73/1.26 % (1831849)------------------------------
% 3.73/1.26 % (1831849)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.73/1.26 % (1831849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.73/1.26 % (1831849)CaDiCaL version: 2.1.3
% 3.73/1.26 % (1831849)Termination reason: Instruction limit
% 3.73/1.26 % (1831849)Termination phase: Saturation
% 3.73/1.26 % (1831849)Time elapsed: 0.023 s
% 3.73/1.26 % (1831849)Peak memory usage: 88 MB
% 3.73/1.26 % (1831849)Instructions burned: 89 (million)
% 3.73/1.26 % (1831850)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=2274919411:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi)
% 3.73/1.26 % (1831850)Instruction limit reached!
% 3.73/1.26 % (1831850)------------------------------
% 3.73/1.26 % (1831850)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.73/1.26 % (1831850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.73/1.26 % (1831850)CaDiCaL version: 2.1.3
% 3.73/1.26 % (1831850)Termination reason: Instruction limit
% 3.73/1.26 % (1831850)Termination phase: Saturation
% 3.73/1.26 % (1831850)Time elapsed: 0.003 s
% 3.73/1.26 % (1831850)Peak memory usage: 89 MB
% 3.73/1.26 % (1831850)Instructions burned: 2 (million)
% 3.73/1.26 % (1831852)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=2565775371:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi)
% 3.73/1.26 % (1831852)Refutation not found, incomplete strategy
% 3.73/1.26 % (1831852)------------------------------
% 3.73/1.26 % (1831852)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.73/1.27 % (1831852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.73/1.27 % (1831852)CaDiCaL version: 2.1.3
% 3.73/1.27 % (1831852)Termination reason: Refutation not found, incomplete strategy
% 3.73/1.27 % (1831852)Time elapsed: 0.002 s
% 3.73/1.27 % (1831852)Peak memory usage: 89 MB
% 3.73/1.27 % (1831859)lrs+10_1_thi=all:si=on:fd=off:random_seed=2380393931:i=53:rtra=on:gtg=all_2995 on theBenchmark for (2995ds/53Mi)
% 3.73/1.27 % (1831854)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=2346350339:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi)
% 3.73/1.27 % (1831854)Instruction limit reached!
% 3.73/1.27 % (1831854)------------------------------
% 3.73/1.27 % (1831854)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.73/1.27 % (1831854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.73/1.27 % (1831854)CaDiCaL version: 2.1.3
% 3.73/1.27 % (1831854)Termination reason: Instruction limit
% 3.73/1.27 % (1831854)Termination phase: Saturation
% 3.73/1.27 % (1831854)Time elapsed: 0.004 s
% 3.73/1.27 % (1831854)Peak memory usage: 88 MB
% 3.73/1.27 % (1831854)Instructions burned: 4 (million)
% 3.73/1.27 % (1831859)Instruction limit reached!
% 3.73/1.27 % (1831859)------------------------------
% 3.73/1.27 % (1831859)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.73/1.27 % (1831859)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.73/1.27 % (1831859)CaDiCaL version: 2.1.3
% 3.73/1.27 % (1831859)Termination reason: Instruction limit
% 3.73/1.27 % (1831859)Termination phase: Saturation
% 3.73/1.27 % (1831859)Time elapsed: 0.037 s
% 3.73/1.27 % (1831859)Peak memory usage: 116 MB
% 3.73/1.27 % (1831859)Instructions burned: 53 (million)
% 3.73/1.27 % (1831858)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=1938424479:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2995 on theBenchmark for (2995ds/66Mi)
% 3.73/1.27 % (1831830)Refutation found. Thanks to Tanya!
% 3.73/1.27 % SZS status Theorem for theBenchmark
% 3.73/1.27 % SZS output start Proof for theBenchmark
% See solution above
% 4.85/1.45 % (1831830)------------------------------
% 4.85/1.45 % (1831830)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.85/1.45 % (1831830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.85/1.45 % (1831830)CaDiCaL version: 2.1.3
% 4.85/1.45 % (1831830)Termination reason: Refutation
% 4.85/1.45 % (1831830)Time elapsed: 0.171 s
% 4.85/1.45 % (1831830)Peak memory usage: 117 MB
% 4.85/1.45 % (1831830)Instructions burned: 215 (million)
% 4.85/1.45 % (1831830)------------------------------
% 4.85/1.45 % (1831830)------------------------------
% 4.85/1.45 % (1831824)Success in time 0.607 s
% 4.85/1.45 % Vampire exiting
%------------------------------------------------------------------------------