%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW588_2 : TPTP v9.3.1. Released v6.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n020.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:30:52 PM UTC 2026
% Result : Theorem 2.66s 1.53s
% Output : Refutation 4.83s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 32
% Syntax : Number of formulae : 104 ( 30 unt; 0 typ; 31 def)
% Number of atoms : 386 ( 124 equ)
% Maximal formula atoms : 17 ( 3 avg)
% Number of connectives : 426 ( 144 ~; 172 |; 64 &)
% ( 22 <=>; 24 =>; 0 <=; 0 <~>)
% Maximal formula depth : 21 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number arithmetic : 482 ( 152 atm; 148 fun; 129 num; 53 var)
% Number of types : 6 ( 4 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 27 ( 23 usr; 23 prp; 0-2 aty)
% Number of functors : 34 ( 28 usr; 25 con; 0-4 aty)
% Number of variables : 53 ( 37 !; 16 ?; 53 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
uni: $tType ).
tff(type_def_6,type,
ty: $tType ).
tff(type_def_7,type,
bool1: $tType ).
tff(type_def_8,type,
tuple02: $tType ).
tff(func_def_0,type,
witness1: ty > uni ).
tff(func_def_1,type,
int: ty ).
tff(func_def_2,type,
real: ty ).
tff(func_def_3,type,
bool: ty ).
tff(func_def_4,type,
true1: bool1 ).
tff(func_def_5,type,
false1: bool1 ).
tff(func_def_6,type,
match_bool1: ( ty * bool1 * uni * uni ) > uni ).
tff(func_def_7,type,
tuple0: ty ).
tff(func_def_8,type,
tuple03: tuple02 ).
tff(func_def_9,type,
qtmark: ty ).
tff(func_def_12,type,
ref: ty > ty ).
tff(func_def_13,type,
mk_ref: ( ty * uni ) > uni ).
tff(func_def_14,type,
contents: ( ty * uni ) > uni ).
tff(func_def_19,type,
sK0: $int ).
tff(func_def_20,type,
sK1: $int ).
tff(func_def_21,type,
sK2: $int ).
tff(func_def_22,type,
sK3: $int ).
tff(func_def_23,type,
sK4: $int ).
tff(func_def_24,type,
sK5: $int ).
tff(func_def_25,type,
sF6: $int ).
tff(func_def_26,type,
sF7: $int ).
tff(func_def_27,type,
sF8: $int ).
tff(func_def_28,type,
sF9: $int ).
tff(func_def_29,type,
sF10: $int ).
tff(func_def_30,type,
sF11: $int ).
tff(func_def_31,type,
sF12: $int ).
tff(func_def_32,type,
sF13: $int ).
tff(func_def_33,type,
sF14: $int ).
tff(pred_def_1,type,
sort1: ( ty * uni ) > $o ).
tff(f13,conjecture,
! [X1: $int,X0: $int] :
( ( $less(0,X1)
& $lesseq(0,X0) )
=> ( ! [X3: $int,X2: $int] :
( ( ( $sum($product(X3,X1),X2) = X0 )
& $lesseq(0,X2) )
=> ( ( ~ $lesseq(X1,X2)
=> ? [X5: $int] :
( $lesseq(0,X5)
& ( $sum($product(X3,X1),X5) = X0 )
& $less(X5,X1) ) )
& ( $lesseq(X1,X2)
=> ! [X4: $int] :
( ( X4 = $sum(X3,1) )
=> ! [X5: $int] :
( ( X5 = $difference(X2,X1) )
=> ( $less(X5,X2)
& ( $sum($product(X4,X1),X5) = X0 )
& $lesseq(0,X5)
& $lesseq(0,X2) ) ) ) ) ) )
& $lesseq(0,X0)
& ( $sum($product(0,X1),X0) = X0 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',wP_parameter_division) ).
tff(f14,negated_conjecture,
~ ! [X1: $int,X0: $int] :
( ( $less(0,X1)
& $lesseq(0,X0) )
=> ( ! [X3: $int,X2: $int] :
( ( ( $sum($product(X3,X1),X2) = X0 )
& $lesseq(0,X2) )
=> ( ( ~ $lesseq(X1,X2)
=> ? [X5: $int] :
( $lesseq(0,X5)
& ( $sum($product(X3,X1),X5) = X0 )
& $less(X5,X1) ) )
& ( $lesseq(X1,X2)
=> ! [X4: $int] :
( ( X4 = $sum(X3,1) )
=> ! [X5: $int] :
( ( X5 = $difference(X2,X1) )
=> ( $less(X5,X2)
& ( $sum($product(X4,X1),X5) = X0 )
& $lesseq(0,X5)
& $lesseq(0,X2) ) ) ) ) ) )
& $lesseq(0,X0)
& ( $sum($product(0,X1),X0) = X0 ) ) ),
inference(negated_conjecture,[status(cth)],[f13]) ).
tff(f16,plain,
~ ! [X1: $int,X0: $int] :
( ( $less(0,X1)
& ~ $less(X0,0) )
=> ( ! [X3: $int,X2: $int] :
( ( ( $sum($product(X3,X1),X2) = X0 )
& ~ $less(X2,0) )
=> ( ( $less(X2,X1)
=> ? [X5: $int] :
( ~ $less(X5,0)
& ( $sum($product(X3,X1),X5) = X0 )
& $less(X5,X1) ) )
& ( ~ $less(X2,X1)
=> ! [X4: $int] :
( ( X4 = $sum(X3,1) )
=> ! [X5: $int] :
( ( $sum(X2,$uminus(X1)) = X5 )
=> ( $less(X5,X2)
& ( $sum($product(X4,X1),X5) = X0 )
& ~ $less(X5,0)
& ~ $less(X2,0) ) ) ) ) ) )
& ~ $less(X0,0)
& ( $sum($product(0,X1),X0) = X0 ) ) ),
inference(theory_normalization,[],[f14]) ).
tff(f20,plain,
~ ! [X1: $int,X0: $int] :
( ( ~ $less(X1,0)
& $less(0,X0) )
=> ( ~ $less(X1,0)
& ! [X3: $int,X2: $int] :
( ( ~ $less(X3,0)
& ( $sum($product(X2,X0),X3) = X1 ) )
=> ( ( ~ $less(X3,X0)
=> ! [X5: $int] :
( ( $sum(X2,1) = X5 )
=> ! [X6: $int] :
( ( $sum(X3,$uminus(X0)) = X6 )
=> ( ~ $less(X6,0)
& ~ $less(X3,0)
& ( $sum($product(X5,X0),X6) = X1 )
& $less(X6,X3) ) ) ) )
& ( $less(X3,X0)
=> ? [X4: $int] :
( $less(X4,X0)
& ~ $less(X4,0)
& ( $sum($product(X2,X0),X4) = X1 ) ) ) ) )
& ( $sum($product(0,X0),X1) = X1 ) ) ),
inference(rectify,[],[f16]) ).
tff(f25,plain,
? [X1: $int,X0: $int] :
( ( $less(X1,0)
| ? [X3: $int,X2: $int] :
( ( ( ! [X4: $int] :
( ~ $less(X4,X0)
| ( $sum($product(X2,X0),X4) != X1 )
| $less(X4,0) )
& $less(X3,X0) )
| ( ~ $less(X3,X0)
& ? [X5: $int] :
( ( $sum(X2,1) = X5 )
& ? [X6: $int] :
( ( $sum(X3,$uminus(X0)) = X6 )
& ( ( $sum($product(X5,X0),X6) != X1 )
| ~ $less(X6,X3)
| $less(X3,0)
| $less(X6,0) ) ) ) ) )
& ~ $less(X3,0)
& ( $sum($product(X2,X0),X3) = X1 ) )
| ( $sum($product(0,X0),X1) != X1 ) )
& ~ $less(X1,0)
& $less(0,X0) ),
inference(ennf_transformation,[],[f20]) ).
tff(f26,plain,
? [X0: $int,X1: $int] :
( ( $less(X1,0)
| ? [X2: $int,X3: $int] :
( ( ( ! [X4: $int] :
( ~ $less(X4,X0)
| ( $sum($product(X2,X0),X4) != X1 )
| $less(X4,0) )
& $less(X3,X0) )
| ( ~ $less(X3,X0)
& ? [X5: $int] :
( ( $sum(X2,1) = X5 )
& ? [X6: $int] :
( ( $sum(X3,$uminus(X0)) = X6 )
& ( ( $sum($product(X5,X0),X6) != X1 )
| ~ $less(X6,X3)
| $less(X3,0)
| $less(X6,0) ) ) ) ) )
& ( $sum($product(X2,X0),X3) = X1 )
& ~ $less(X3,0) )
| ( $sum($product(0,X0),X1) != X1 ) )
& ~ $less(X1,0)
& $less(0,X0) ),
inference(flattening,[],[f25]) ).
tff(f31,plain,
( ( $less(sK1,0)
| ( ( ( ! [X4: $int] :
( ~ $less(X4,sK0)
| ( $sum($product(sK2,sK0),X4) != sK1 )
| $less(X4,0) )
& $less(sK3,sK0) )
| ( ~ $less(sK3,sK0)
& ( $sum(sK2,1) = sK4 )
& ( $sum(sK3,$uminus(sK0)) = sK5 )
& ( ( $sum($product(sK4,sK0),sK5) != sK1 )
| ~ $less(sK5,sK3)
| $less(sK3,0)
| $less(sK5,0) ) ) )
& ( $sum($product(sK2,sK0),sK3) = sK1 )
& ~ $less(sK3,0) )
| ( sK1 != $sum($product(0,sK0),sK1) ) )
& ~ $less(sK1,0)
& $less(0,sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3,sK4,sK5]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X3,sK3),skolemize(X5,sK4),skolemize(X6,sK5)],[f26]) ).
tff(f39,plain,
$less(0,sK0),
inference(cnf_transformation,[],[f31]) ).
tff(f40,plain,
~ $less(sK1,0),
inference(cnf_transformation,[],[f31]) ).
tff(f41,plain,
( $less(sK1,0)
| ~ $less(sK3,0)
| ( sK1 != $sum($product(0,sK0),sK1) ) ),
inference(cnf_transformation,[],[f31]) ).
tff(f42,plain,
( $less(sK1,0)
| ( $sum($product(sK2,sK0),sK3) = sK1 )
| ( sK1 != $sum($product(0,sK0),sK1) ) ),
inference(cnf_transformation,[],[f31]) ).
tff(f43,plain,
( $less(sK1,0)
| $less(sK3,sK0)
| ( $sum($product(sK4,sK0),sK5) != sK1 )
| ~ $less(sK5,sK3)
| $less(sK3,0)
| $less(sK5,0)
| ( sK1 != $sum($product(0,sK0),sK1) ) ),
inference(cnf_transformation,[],[f31]) ).
tff(f44,plain,
( $less(sK1,0)
| $less(sK3,sK0)
| ( $sum(sK3,$uminus(sK0)) = sK5 )
| ( sK1 != $sum($product(0,sK0),sK1) ) ),
inference(cnf_transformation,[],[f31]) ).
tff(f45,plain,
( $less(sK1,0)
| $less(sK3,sK0)
| ( $sum(sK2,1) = sK4 )
| ( sK1 != $sum($product(0,sK0),sK1) ) ),
inference(cnf_transformation,[],[f31]) ).
tff(f47,plain,
! [X4: $int] :
( $less(sK1,0)
| ~ $less(X4,sK0)
| ( $sum($product(sK2,sK0),X4) != sK1 )
| $less(X4,0)
| ( $sum($product(sK4,sK0),sK5) != sK1 )
| ~ $less(sK5,sK3)
| $less(sK3,0)
| $less(sK5,0)
| ( sK1 != $sum($product(0,sK0),sK1) ) ),
inference(cnf_transformation,[],[f31]) ).
tff(f48,plain,
! [X4: $int] :
( $less(sK1,0)
| ~ $less(X4,sK0)
| ( $sum($product(sK2,sK0),X4) != sK1 )
| $less(X4,0)
| ( $sum(sK3,$uminus(sK0)) = sK5 )
| ( sK1 != $sum($product(0,sK0),sK1) ) ),
inference(cnf_transformation,[],[f31]) ).
tff(f49,plain,
! [X4: $int] :
( $less(sK1,0)
| ~ $less(X4,sK0)
| ( $sum($product(sK2,sK0),X4) != sK1 )
| $less(X4,0)
| ( $sum(sK2,1) = sK4 )
| ( sK1 != $sum($product(0,sK0),sK1) ) ),
inference(cnf_transformation,[],[f31]) ).
tff(f50,plain,
! [X4: $int] :
( $less(sK1,0)
| ~ $less(X4,sK0)
| ( $sum($product(sK2,sK0),X4) != sK1 )
| $less(X4,0)
| ~ $less(sK3,sK0)
| ( sK1 != $sum($product(0,sK0),sK1) ) ),
inference(cnf_transformation,[],[f31]) ).
tff(f63,definition,
sF6 = $product(sK2,sK0),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
tff(f64,definition,
sF7 = $product(0,sK0),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
tff(f65,definition,
sF8 = $sum(sF7,sK1),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
tff(f66,plain,
$sum(sF7,sK1) = sF8,
inference(reorient_equations,[],[f65]) ).
tff(f67,plain,
! [X4: $int] :
( ( $sum(sF6,X4) != sK1 )
| ~ $less(X4,sK0)
| $less(sK1,0)
| ( sF8 != sK1 )
| $less(X4,0)
| ~ $less(sK3,sK0) ),
inference(definition_folding,[],[f50,f66,f64,f63]) ).
tff(f68,definition,
sF9 = $sum(sK2,1),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
tff(f69,plain,
$sum(sK2,1) = sF9,
inference(reorient_equations,[],[f68]) ).
tff(f70,plain,
! [X4: $int] :
( ~ $less(X4,sK0)
| $less(sK1,0)
| $less(X4,0)
| ( sF8 != sK1 )
| ( $sum(sF6,X4) != sK1 )
| ( sF9 = sK4 ) ),
inference(definition_folding,[],[f49,f66,f64,f69,f63]) ).
tff(f71,definition,
sF10 = $uminus(sK0),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
tff(f72,plain,
$uminus(sK0) = sF10,
inference(reorient_equations,[],[f71]) ).
tff(f73,definition,
sF11 = $sum(sK3,sF10),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
tff(f74,plain,
$sum(sK3,sF10) = sF11,
inference(reorient_equations,[],[f73]) ).
tff(f75,plain,
! [X4: $int] :
( ~ $less(X4,sK0)
| $less(sK1,0)
| ( sF8 != sK1 )
| ( sK5 = sF11 )
| $less(X4,0)
| ( $sum(sF6,X4) != sK1 ) ),
inference(definition_folding,[],[f48,f66,f64,f74,f72,f63]) ).
tff(f76,definition,
sF12 = $product(sK4,sK0),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
tff(f77,definition,
sF13 = $sum(sF12,sK5),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
tff(f78,plain,
$sum(sF12,sK5) = sF13,
inference(reorient_equations,[],[f77]) ).
tff(f79,plain,
! [X4: $int] :
( ( sF8 != sK1 )
| $less(sK1,0)
| $less(sK3,0)
| $less(sK5,0)
| ( $sum(sF6,X4) != sK1 )
| ( sF13 != sK1 )
| $less(X4,0)
| ~ $less(sK5,sK3)
| ~ $less(X4,sK0) ),
inference(definition_folding,[],[f47,f66,f64,f78,f76,f63]) ).
tff(f81,plain,
( ( sF8 != sK1 )
| $less(sK1,0)
| ( sF9 = sK4 )
| $less(sK3,sK0) ),
inference(definition_folding,[],[f45,f66,f64,f69]) ).
tff(f82,plain,
( $less(sK1,0)
| ( sK5 = sF11 )
| ( sF8 != sK1 )
| $less(sK3,sK0) ),
inference(definition_folding,[],[f44,f66,f64,f74,f72]) ).
tff(f83,plain,
( ( sF13 != sK1 )
| ~ $less(sK5,sK3)
| $less(sK5,0)
| $less(sK3,sK0)
| $less(sK3,0)
| $less(sK1,0)
| ( sF8 != sK1 ) ),
inference(definition_folding,[],[f43,f66,f64,f78,f76]) ).
tff(f84,definition,
sF14 = $sum(sF6,sK3),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
tff(f85,plain,
$sum(sF6,sK3) = sF14,
inference(reorient_equations,[],[f84]) ).
tff(f86,plain,
( ( sF8 != sK1 )
| ( sK1 = sF14 )
| $less(sK1,0) ),
inference(definition_folding,[],[f42,f66,f64,f85,f63]) ).
tff(f87,plain,
( ( sF8 != sK1 )
| ~ $less(sK3,0)
| $less(sK1,0) ),
inference(definition_folding,[],[f41,f66,f64]) ).
tff(f88,plain,
0 = sF7,
inference(evaluation,[],[f64]) ).
tff(f90,definition,
( spl15_1
<=> ( sF9 = sK4 ) ),
introduced(definition,[new_symbols(definition,[spl15_1])],[avatar_definition]) ).
tff(f94,definition,
( spl15_2
<=> $less(sK1,0) ),
introduced(definition,[new_symbols(definition,[spl15_2])],[avatar_definition]) ).
tff(f98,definition,
( spl15_3
<=> ! [X4: $int] :
( ~ $less(X4,sK0)
| ( $sum(sF6,X4) != sK1 )
| $less(X4,0) ) ),
introduced(definition,[new_symbols(definition,[spl15_3])],[avatar_definition]) ).
tff(f99,plain,
( ! [X4: $int] :
( ( $sum(sF6,X4) != sK1 )
| ~ $less(X4,sK0)
| $less(X4,0) )
| ~ spl15_3 ),
inference(avatar_component_clause,[],[f98]) ).
tff(f101,definition,
( spl15_4
<=> ( sF8 = sK1 ) ),
introduced(definition,[new_symbols(definition,[spl15_4])],[avatar_definition]) ).
tff(f104,plain,
( spl15_1
| spl15_2
| spl15_3
| ~ spl15_4 ),
inference(avatar_split_clause,[],[f70,f101,f98,f94,f90]) ).
tff(f106,definition,
( spl15_5
<=> ( $sum(sK2,1) = sF9 ) ),
introduced(definition,[new_symbols(definition,[spl15_5])],[avatar_definition]) ).
tff(f109,plain,
spl15_5,
inference(avatar_split_clause,[],[f69,f106]) ).
tff(f116,definition,
( spl15_7
<=> ( $sum(sF7,sK1) = sF8 ) ),
introduced(definition,[new_symbols(definition,[spl15_7])],[avatar_definition]) ).
tff(f118,plain,
( ( $sum(sF7,sK1) = sF8 )
| ~ spl15_7 ),
inference(avatar_component_clause,[],[f116]) ).
tff(f119,plain,
spl15_7,
inference(avatar_split_clause,[],[f66,f116]) ).
tff(f121,definition,
( spl15_8
<=> ( $sum(sF12,sK5) = sF13 ) ),
introduced(definition,[new_symbols(definition,[spl15_8])],[avatar_definition]) ).
tff(f124,plain,
spl15_8,
inference(avatar_split_clause,[],[f78,f121]) ).
tff(f126,definition,
( spl15_9
<=> ( sF12 = $product(sK4,sK0) ) ),
introduced(definition,[new_symbols(definition,[spl15_9])],[avatar_definition]) ).
tff(f129,plain,
spl15_9,
inference(avatar_split_clause,[],[f76,f126]) ).
tff(f131,definition,
( spl15_10
<=> ( sK5 = sF11 ) ),
introduced(definition,[new_symbols(definition,[spl15_10])],[avatar_definition]) ).
tff(f134,plain,
( spl15_2
| ~ spl15_4
| spl15_10
| spl15_3 ),
inference(avatar_split_clause,[],[f75,f98,f131,f101,f94]) ).
tff(f136,definition,
( spl15_11
<=> $less(sK5,0) ),
introduced(definition,[new_symbols(definition,[spl15_11])],[avatar_definition]) ).
tff(f140,definition,
( spl15_12
<=> ( sF13 = sK1 ) ),
introduced(definition,[new_symbols(definition,[spl15_12])],[avatar_definition]) ).
tff(f144,definition,
( spl15_13
<=> $less(sK3,sK0) ),
introduced(definition,[new_symbols(definition,[spl15_13])],[avatar_definition]) ).
tff(f146,plain,
( $less(sK3,sK0)
| ~ spl15_13 ),
inference(avatar_component_clause,[],[f144]) ).
tff(f148,definition,
( spl15_14
<=> $less(sK5,sK3) ),
introduced(definition,[new_symbols(definition,[spl15_14])],[avatar_definition]) ).
tff(f152,definition,
( spl15_15
<=> $less(sK3,0) ),
introduced(definition,[new_symbols(definition,[spl15_15])],[avatar_definition]) ).
tff(f153,plain,
( ~ $less(sK3,0)
| spl15_15 ),
inference(avatar_component_clause,[],[f152]) ).
tff(f155,plain,
( spl15_11
| ~ spl15_12
| ~ spl15_4
| spl15_13
| ~ spl15_14
| spl15_2
| spl15_15 ),
inference(avatar_split_clause,[],[f83,f152,f94,f148,f144,f101,f140,f136]) ).
tff(f157,definition,
( spl15_16
<=> ( $sum(sK3,sF10) = sF11 ) ),
introduced(definition,[new_symbols(definition,[spl15_16])],[avatar_definition]) ).
tff(f160,plain,
spl15_16,
inference(avatar_split_clause,[],[f74,f157]) ).
tff(f162,definition,
( spl15_17
<=> ( 0 = sF7 ) ),
introduced(definition,[new_symbols(definition,[spl15_17])],[avatar_definition]) ).
tff(f164,plain,
( ( 0 = sF7 )
| ~ spl15_17 ),
inference(avatar_component_clause,[],[f162]) ).
tff(f165,plain,
spl15_17,
inference(avatar_split_clause,[],[f88,f162]) ).
tff(f167,definition,
( spl15_18
<=> ( sK1 = sF14 ) ),
introduced(definition,[new_symbols(definition,[spl15_18])],[avatar_definition]) ).
tff(f169,plain,
( ( sK1 = sF14 )
| ~ spl15_18 ),
inference(avatar_component_clause,[],[f167]) ).
tff(f170,plain,
( spl15_18
| ~ spl15_4
| spl15_2 ),
inference(avatar_split_clause,[],[f86,f94,f101,f167]) ).
tff(f171,plain,
( spl15_1
| spl15_13
| ~ spl15_4
| spl15_2 ),
inference(avatar_split_clause,[],[f81,f94,f101,f144,f90]) ).
tff(f172,plain,
( ~ spl15_13
| spl15_2
| spl15_3
| ~ spl15_4 ),
inference(avatar_split_clause,[],[f67,f101,f98,f94,f144]) ).
tff(f173,plain,
( ~ spl15_4
| spl15_2
| ~ spl15_15 ),
inference(avatar_split_clause,[],[f87,f152,f94,f101]) ).
tff(f174,plain,
~ spl15_2,
inference(avatar_split_clause,[],[f40,f94]) ).
tff(f175,plain,
( spl15_2
| spl15_11
| ~ spl15_14
| ~ spl15_12
| spl15_3
| spl15_15
| ~ spl15_4 ),
inference(avatar_split_clause,[],[f79,f101,f152,f98,f140,f148,f136,f94]) ).
tff(f176,plain,
( spl15_13
| ~ spl15_4
| spl15_10
| spl15_2 ),
inference(avatar_split_clause,[],[f82,f94,f131,f101,f144]) ).
tff(f178,definition,
( spl15_19
<=> ( sF6 = $product(sK2,sK0) ) ),
introduced(definition,[new_symbols(definition,[spl15_19])],[avatar_definition]) ).
tff(f181,plain,
spl15_19,
inference(avatar_split_clause,[],[f63,f178]) ).
tff(f183,definition,
( spl15_20
<=> $less(0,sK0) ),
introduced(definition,[new_symbols(definition,[spl15_20])],[avatar_definition]) ).
tff(f186,plain,
spl15_20,
inference(avatar_split_clause,[],[f39,f183]) ).
tff(f188,definition,
( spl15_21
<=> ( $sum(sF6,sK3) = sF14 ) ),
introduced(definition,[new_symbols(definition,[spl15_21])],[avatar_definition]) ).
tff(f190,plain,
( ( $sum(sF6,sK3) = sF14 )
| ~ spl15_21 ),
inference(avatar_component_clause,[],[f188]) ).
tff(f191,plain,
spl15_21,
inference(avatar_split_clause,[],[f85,f188]) ).
tff(f193,definition,
( spl15_22
<=> ( $uminus(sK0) = sF10 ) ),
introduced(definition,[new_symbols(definition,[spl15_22])],[avatar_definition]) ).
tff(f196,plain,
spl15_22,
inference(avatar_split_clause,[],[f72,f193]) ).
tff(f200,plain,
( ( sF8 = $sum(0,sK1) )
| ~ spl15_7
| ~ spl15_17 ),
inference(forward_demodulation,[],[f118,f164]) ).
tff(f201,plain,
( ( sF8 = sK1 )
| ~ spl15_7
| ~ spl15_17 ),
inference(evaluation,[],[f200]) ).
tff(f202,plain,
( spl15_4
| ~ spl15_7
| ~ spl15_17 ),
inference(avatar_split_clause,[],[f201,f162,f116,f101]) ).
tff(f203,plain,
( ( $sum(sF6,sK3) = sK1 )
| ~ spl15_18
| ~ spl15_21 ),
inference(forward_demodulation,[],[f190,f169]) ).
tff(f205,definition,
( spl15_23
<=> ( $sum(sF6,sK3) = sK1 ) ),
introduced(definition,[new_symbols(definition,[spl15_23])],[avatar_definition]) ).
tff(f207,plain,
( ( $sum(sF6,sK3) = sK1 )
| ~ spl15_23 ),
inference(avatar_component_clause,[],[f205]) ).
tff(f208,plain,
( spl15_23
| ~ spl15_18
| ~ spl15_21 ),
inference(avatar_split_clause,[],[f203,f188,f167,f205]) ).
tff(f209,plain,
( $less(sK3,0)
| ~ $less(sK3,sK0)
| ( sK1 != sK1 )
| ~ spl15_3
| ~ spl15_23 ),
inference(superposition,[],[f99,f207]) ).
tff(f210,plain,
( $less(sK3,0)
| ~ $less(sK3,sK0)
| ~ spl15_3
| ~ spl15_23 ),
inference(trivial_inequality_removal,[],[f209]) ).
tff(f211,plain,
( ~ $less(sK3,sK0)
| ~ spl15_3
| spl15_15
| ~ spl15_23 ),
inference(forward_subsumption_resolution,[],[f210,f153]) ).
tff(f212,plain,
( $false
| ~ spl15_3
| ~ spl15_13
| spl15_15
| ~ spl15_23 ),
inference(forward_subsumption_resolution,[],[f211,f146]) ).
tff(f213,plain,
( ~ spl15_3
| ~ spl15_13
| spl15_15
| ~ spl15_23 ),
inference(avatar_contradiction_clause,[],[f212]) ).
tff(f214,plain,
$false,
inference(avatar_smt_refutation,[],[f213,f208,f202,f196,f191,f186,f181,f176,f175,f174,f173,f172,f171,f170,f165,f160,f155,f134,f129,f124,f119,f109,f104]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWW588_2 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.07 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.25 % Computer : n020.cluster.edu
% 0.10/0.25 % Model : x86_64 x86_64
% 0.10/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.25 % Memory : 8046.5625MB
% 0.10/0.25 % OS : Linux 6.8.0-71-generic
% 0.10/0.25 % CPULimit : 300
% 0.10/0.25 % WCLimit : 300
% 0.10/0.25 % DateTime : Mon Sep 28 14:20:49 UTC 2026
% 0.10/0.26 % CPUTime :
% 0.10/0.26 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.26/0.31 Running first-order theorem proving
% 0.26/0.31 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.66/1.53 % (194953)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 2.66/1.53 % (194963)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=1841608792:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 2.66/1.53 % (194968)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=3065028859:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 2.66/1.53 % (194968)Instruction limit reached!
% 2.66/1.53 % (194968)------------------------------
% 2.66/1.53 % (194968)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.66/1.53 % (194968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.66/1.53 % (194968)CaDiCaL version: 2.1.3
% 2.66/1.53 % (194968)Termination reason: Instruction limit
% 2.66/1.53 % (194968)Termination phase: Saturation
% 2.66/1.53 % (194968)Time elapsed: 0.073 s
% 2.66/1.53 % (194968)Peak memory usage: 117 MB
% 2.66/1.53 % (194968)Instructions burned: 33 (million)
% 2.66/1.53 % (194966)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=2985223727:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 2.66/1.53 % (194965)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=3233201458:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 2.66/1.53 % (194967)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=1101859863:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 2.66/1.53 % (194962)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=3619176630:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 2.66/1.53 % (194964)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=196545036:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 2.66/1.53 % (194966)Instruction limit reached!
% 2.66/1.53 % (194966)------------------------------
% 2.66/1.53 % (194966)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.66/1.53 % (194966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.66/1.53 % (194966)CaDiCaL version: 2.1.3
% 2.66/1.53 % (194966)Termination reason: Instruction limit
% 2.66/1.53 % (194966)Termination phase: Saturation
% 2.66/1.53 % (194966)Time elapsed: 0.006 s
% 2.66/1.53 % (194966)Peak memory usage: 89 MB
% 2.66/1.53 % (194966)Instructions burned: 4 (million)
% 2.66/1.53 % (194965)Instruction limit reached!
% 2.66/1.53 % (194965)------------------------------
% 2.66/1.53 % (194965)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.66/1.53 % (194965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.66/1.53 % (194965)CaDiCaL version: 2.1.3
% 2.66/1.53 % (194965)Termination reason: Instruction limit
% 2.66/1.53 % (194965)Termination phase: Saturation
% 2.66/1.53 % (194965)Time elapsed: 0.008 s
% 2.66/1.53 % (194965)Peak memory usage: 88 MB
% 2.66/1.53 % (194965)Instructions burned: 7 (million)
% 2.66/1.53 % (194963)First to succeed.
% 2.66/1.53 % (194963)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-194953"
% 2.66/1.53 % (194962)Instruction limit reached!
% 2.66/1.53 % (194962)------------------------------
% 2.66/1.53 % (194962)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.66/1.53 % (194962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.66/1.53 % (194962)CaDiCaL version: 2.1.3
% 2.66/1.53 % (194962)Termination reason: Instruction limit
% 2.66/1.53 % (194962)Termination phase: Saturation
% 2.66/1.53 % (194962)Time elapsed: 0.043 s
% 2.66/1.53 % (194962)Peak memory usage: 116 MB
% 2.66/1.53 % (194962)Instructions burned: 12 (million)
% 2.66/1.53 % (194967)Also succeeded, but the first one will report.
% 2.66/1.53 % (194978)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=2413765355:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2997 on theBenchmark for (2997ds/29Mi)
% 2.66/1.53 % (194964)Instruction limit reached!
% 2.66/1.53 % (194964)------------------------------
% 2.66/1.53 % (194964)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.66/1.53 % (194964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.66/1.53 % (194964)CaDiCaL version: 2.1.3
% 2.66/1.53 % (194964)Termination reason: Instruction limit
% 2.66/1.53 % (194964)Termination phase: Saturation
% 2.66/1.53 % (194964)Time elapsed: 0.186 s
% 2.66/1.53 % (194964)Peak memory usage: 117 MB
% 2.66/1.53 % (194964)Instructions burned: 202 (million)
% 2.66/1.53 % (194978)Instruction limit reached!
% 2.66/1.53 % (194978)------------------------------
% 2.66/1.53 % (194978)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.66/1.53 % (194978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.66/1.53 % (194978)CaDiCaL version: 2.1.3
% 2.66/1.53 % (194978)Termination reason: Instruction limit
% 2.66/1.53 % (194978)Termination phase: Saturation
% 2.66/1.53 % (194978)Time elapsed: 0.022 s
% 2.66/1.53 % (194978)Peak memory usage: 88 MB
% 2.66/1.53 % (194978)Instructions burned: 31 (million)
% 2.66/1.53 % (194963)Refutation found. Thanks to Tanya!
% 2.66/1.53 % SZS status Theorem for theBenchmark
% 2.66/1.53 % SZS output start Proof for theBenchmark
% See solution above
% 4.83/1.82 % (194963)------------------------------
% 4.83/1.82 % (194963)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.83/1.82 % (194963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.83/1.82 % (194963)CaDiCaL version: 2.1.3
% 4.83/1.82 % (194963)Termination reason: Refutation
% 4.83/1.82 % (194963)Time elapsed: 0.112 s
% 4.83/1.82 % (194963)Peak memory usage: 119 MB
% 4.83/1.82 % (194963)Instructions burned: 190 (million)
% 4.83/1.82 % (194963)------------------------------
% 4.83/1.82 % (194963)------------------------------
% 4.83/1.82 % (194953)Success in time 0.529 s
% 4.83/1.82 % Vampire exiting
%------------------------------------------------------------------------------