%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWW677_1 : TPTP v9.3.1. Released v6.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n011.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:31:07 PM UTC 2026
% Result : Theorem 3.04s 1.12s
% Output : Refutation 3.90s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 22
% Syntax : Number of formulae : 70 ( 27 unt; 0 typ; 20 def)
% Number of atoms : 303 ( 72 equ)
% Maximal formula atoms : 20 ( 4 avg)
% Number of connectives : 366 ( 133 ~; 91 |; 94 &)
% ( 15 <=>; 33 =>; 0 <=; 0 <~>)
% Maximal formula depth : 19 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number arithmetic : 566 ( 143 atm; 163 fun; 187 num; 73 var)
% Number of types : 3 ( 1 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 20 ( 14 usr; 15 prp; 0-3 aty)
% Number of functors : 28 ( 20 usr; 16 con; 0-3 aty)
% Number of variables : 81 ( 54 !; 27 ?; 81 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
'Array[Int,Int]': $tType ).
tff(func_def_0,type,
'select:(Array[Int,Int]*Int)>Int': ( 'Array[Int,Int]' * $int ) > $int ).
tff(func_def_1,type,
'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]': ( 'Array[Int,Int]' * $int * $int ) > 'Array[Int,Int]' ).
tff(func_def_2,type,
'const:(Int)>Array[Int,Int]': $int > 'Array[Int,Int]' ).
tff(func_def_3,type,
length: 'Array[Int,Int]' > $int ).
tff(func_def_4,type,
div2: $int > $int ).
tff(func_def_12,type,
sK0: ( 'Array[Int,Int]' * $int * $int ) > $int ).
tff(func_def_13,type,
sK1: ( 'Array[Int,Int]' * $int * $int ) > $int ).
tff(func_def_14,type,
sK2: ( 'Array[Int,Int]' * 'Array[Int,Int]' ) > $int ).
tff(func_def_15,type,
sK3: $int ).
tff(func_def_16,type,
sK4: $int ).
tff(func_def_17,type,
sK5: $int ).
tff(func_def_18,type,
sK6: 'Array[Int,Int]' ).
tff(func_def_19,type,
sF7: $int ).
tff(func_def_20,type,
sF8: $int ).
tff(func_def_21,type,
sF9: $int ).
tff(func_def_22,type,
sF10: $int ).
tff(func_def_23,type,
sF11: $int ).
tff(func_def_24,type,
sF12: $int ).
tff(func_def_25,type,
sF13: $int ).
tff(func_def_26,type,
sF14: $int ).
tff(pred_def_1,type,
sorted: ( 'Array[Int,Int]' * $int * $int ) > $o ).
tff(f5,axiom,
! [X0: $int,X1: $int] :
( ( div2(X0) = X1 )
<=> ( $greater($product(2,$sum(X1,1)),X0)
& $lesseq($product(2,X1),X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_004) ).
tff(f8,conjecture,
! [X1: $int,X0: $int,X3: $int,X2: 'Array[Int,Int]'] :
( ( $less(X1,length(X2))
& $lesseq(0,X0)
& sorted(X2,0,$difference(length(X2),1)) )
=> ( ( ~ $greater(X0,X1)
=> ? [X4: $int] :
( ( X4 = div2($sum(X0,X1)) )
& ( ( 'select:(Array[Int,Int]*Int)>Int'(X2,X4) = X3 )
=> $true )
& ( ( 'select:(Array[Int,Int]*Int)>Int'(X2,X4) != X3 )
=> ( ( $less('select:(Array[Int,Int]*Int)>Int'(X2,X4),X3)
=> ? [X5: $int] :
( sorted(X2,0,$difference(length(X2),1))
& $less(X1,length(X2))
& $lesseq(0,X5)
& ( X5 = $sum(X4,1) ) ) )
& ( ~ $less('select:(Array[Int,Int]*Int)>Int'(X2,X4),X3)
=> ? [X6: $int] :
( $less(X6,length(X2))
& $lesseq(0,X0)
& sorted(X2,0,$difference(length(X2),1))
& ( X6 = $difference(X4,1) ) ) ) ) ) ) )
& ( $greater(X0,X1)
=> $true ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_007) ).
tff(f9,negated_conjecture,
~ ! [X1: $int,X0: $int,X3: $int,X2: 'Array[Int,Int]'] :
( ( $less(X1,length(X2))
& $lesseq(0,X0)
& sorted(X2,0,$difference(length(X2),1)) )
=> ( ( ~ $greater(X0,X1)
=> ? [X4: $int] :
( ( X4 = div2($sum(X0,X1)) )
& ( ( 'select:(Array[Int,Int]*Int)>Int'(X2,X4) = X3 )
=> $true )
& ( ( 'select:(Array[Int,Int]*Int)>Int'(X2,X4) != X3 )
=> ( ( $less('select:(Array[Int,Int]*Int)>Int'(X2,X4),X3)
=> ? [X5: $int] :
( sorted(X2,0,$difference(length(X2),1))
& $less(X1,length(X2))
& $lesseq(0,X5)
& ( X5 = $sum(X4,1) ) ) )
& ( ~ $less('select:(Array[Int,Int]*Int)>Int'(X2,X4),X3)
=> ? [X6: $int] :
( $less(X6,length(X2))
& $lesseq(0,X0)
& sorted(X2,0,$difference(length(X2),1))
& ( X6 = $difference(X4,1) ) ) ) ) ) ) )
& ( $greater(X0,X1)
=> $true ) ) ),
inference(negated_conjecture,[status(cth)],[f8]) ).
tff(f12,plain,
~ ! [X1: $int,X0: $int,X3: $int,X2: 'Array[Int,Int]'] :
( ( $less(X1,length(X2))
& ~ $less(X0,0)
& sorted(X2,0,$sum(length(X2),$uminus(1))) )
=> ( ( ~ $less(X1,X0)
=> ? [X4: $int] :
( ( X4 = div2($sum(X0,X1)) )
& ( ( 'select:(Array[Int,Int]*Int)>Int'(X2,X4) = X3 )
=> $true )
& ( ( 'select:(Array[Int,Int]*Int)>Int'(X2,X4) != X3 )
=> ( ( $less('select:(Array[Int,Int]*Int)>Int'(X2,X4),X3)
=> ? [X5: $int] :
( sorted(X2,0,$sum(length(X2),$uminus(1)))
& $less(X1,length(X2))
& ~ $less(X5,0)
& ( X5 = $sum(X4,1) ) ) )
& ( ~ $less('select:(Array[Int,Int]*Int)>Int'(X2,X4),X3)
=> ? [X6: $int] :
( $less(X6,length(X2))
& ~ $less(X0,0)
& sorted(X2,0,$sum(length(X2),$uminus(1)))
& ( $sum(X4,$uminus(1)) = X6 ) ) ) ) ) ) )
& ( $less(X1,X0)
=> $true ) ) ),
inference(theory_normalization,[],[f9]) ).
tff(f13,plain,
! [X1: $int,X0: $int] :
( ( div2(X0) = X1 )
<=> ( ~ $less(X0,$product(2,X1))
& $less(X0,$product(2,$sum(X1,1))) ) ),
inference(theory_normalization,[],[f5]) ).
tff(f18,plain,
~ ! [X0: $int,X1: $int,X2: $int,X3: 'Array[Int,Int]'] :
( ( ~ $less(X1,0)
& $less(X0,length(X3))
& sorted(X3,0,$sum(length(X3),$uminus(1))) )
=> ( ( ~ $less(X0,X1)
=> ? [X4: $int] :
( ( div2($sum(X1,X0)) = X4 )
& ( ( 'select:(Array[Int,Int]*Int)>Int'(X3,X4) = X2 )
=> $true )
& ( ( 'select:(Array[Int,Int]*Int)>Int'(X3,X4) != X2 )
=> ( ( $less('select:(Array[Int,Int]*Int)>Int'(X3,X4),X2)
=> ? [X5: $int] :
( $less(X0,length(X3))
& ~ $less(X5,0)
& sorted(X3,0,$sum(length(X3),$uminus(1)))
& ( X5 = $sum(X4,1) ) ) )
& ( ~ $less('select:(Array[Int,Int]*Int)>Int'(X3,X4),X2)
=> ? [X6: $int] :
( sorted(X3,0,$sum(length(X3),$uminus(1)))
& ~ $less(X1,0)
& $less(X6,length(X3))
& ( $sum(X4,$uminus(1)) = X6 ) ) ) ) ) ) )
& ( $less(X0,X1)
=> $true ) ) ),
inference(rectify,[],[f12]) ).
tff(f19,plain,
~ ! [X0: $int,X3: 'Array[Int,Int]',X2: $int,X1: $int] :
( ( ~ $less(X1,0)
& $less(X0,length(X3))
& sorted(X3,0,$sum(length(X3),$uminus(1))) )
=> ( ~ $less(X0,X1)
=> ? [X4: $int] :
( ( div2($sum(X1,X0)) = X4 )
& ( ( 'select:(Array[Int,Int]*Int)>Int'(X3,X4) != X2 )
=> ( ( $less('select:(Array[Int,Int]*Int)>Int'(X3,X4),X2)
=> ? [X5: $int] :
( $less(X0,length(X3))
& ~ $less(X5,0)
& sorted(X3,0,$sum(length(X3),$uminus(1)))
& ( X5 = $sum(X4,1) ) ) )
& ( ~ $less('select:(Array[Int,Int]*Int)>Int'(X3,X4),X2)
=> ? [X6: $int] :
( sorted(X3,0,$sum(length(X3),$uminus(1)))
& ~ $less(X1,0)
& $less(X6,length(X3))
& ( $sum(X4,$uminus(1)) = X6 ) ) ) ) ) ) ) ),
inference(true_and_false_elimination,[],[f18]) ).
tff(f21,plain,
? [X0: $int,X3: 'Array[Int,Int]',X2: $int,X1: $int] :
( ! [X4: $int] :
( ( ( ( ! [X6: $int] :
( ~ $less(X6,length(X3))
| ( $sum(X4,$uminus(1)) != X6 )
| $less(X1,0)
| ~ sorted(X3,0,$sum(length(X3),$uminus(1))) )
& ~ $less('select:(Array[Int,Int]*Int)>Int'(X3,X4),X2) )
| ( $less('select:(Array[Int,Int]*Int)>Int'(X3,X4),X2)
& ! [X5: $int] :
( ( $sum(X4,1) != X5 )
| ~ $less(X0,length(X3))
| $less(X5,0)
| ~ sorted(X3,0,$sum(length(X3),$uminus(1))) ) ) )
& ( 'select:(Array[Int,Int]*Int)>Int'(X3,X4) != X2 ) )
| ( div2($sum(X1,X0)) != X4 ) )
& ~ $less(X0,X1)
& ~ $less(X1,0)
& $less(X0,length(X3))
& sorted(X3,0,$sum(length(X3),$uminus(1))) ),
inference(ennf_transformation,[],[f19]) ).
tff(f22,plain,
? [X0: $int,X2: $int,X1: $int,X3: 'Array[Int,Int]'] :
( $less(X0,length(X3))
& ! [X4: $int] :
( ( ( ( ! [X6: $int] :
( ~ $less(X6,length(X3))
| ( $sum(X4,$uminus(1)) != X6 )
| $less(X1,0)
| ~ sorted(X3,0,$sum(length(X3),$uminus(1))) )
& ~ $less('select:(Array[Int,Int]*Int)>Int'(X3,X4),X2) )
| ( $less('select:(Array[Int,Int]*Int)>Int'(X3,X4),X2)
& ! [X5: $int] :
( ( $sum(X4,1) != X5 )
| ~ $less(X0,length(X3))
| $less(X5,0)
| ~ sorted(X3,0,$sum(length(X3),$uminus(1))) ) ) )
& ( 'select:(Array[Int,Int]*Int)>Int'(X3,X4) != X2 ) )
| ( div2($sum(X1,X0)) != X4 ) )
& ~ $less(X0,X1)
& sorted(X3,0,$sum(length(X3),$uminus(1)))
& ~ $less(X1,0) ),
inference(flattening,[],[f21]) ).
tff(f30,plain,
! [X1: $int,X0: $int] :
( ( ( div2(X0) = X1 )
| $less(X0,$product(2,X1))
| ~ $less(X0,$product(2,$sum(X1,1))) )
& ( ( ~ $less(X0,$product(2,X1))
& $less(X0,$product(2,$sum(X1,1))) )
| ( div2(X0) != X1 ) ) ),
inference(nnf_transformation,[],[f13]) ).
tff(f31,plain,
! [X1: $int,X0: $int] :
( ( ( div2(X0) = X1 )
| $less(X0,$product(2,X1))
| ~ $less(X0,$product(2,$sum(X1,1))) )
& ( ( ~ $less(X0,$product(2,X1))
& $less(X0,$product(2,$sum(X1,1))) )
| ( div2(X0) != X1 ) ) ),
inference(flattening,[],[f30]) ).
tff(f32,plain,
! [X0: $int,X1: $int] :
( ( ( div2(X1) = X0 )
| $less(X1,$product(2,X0))
| ~ $less(X1,$product(2,$sum(X0,1))) )
& ( ( ~ $less(X1,$product(2,X0))
& $less(X1,$product(2,$sum(X0,1))) )
| ( div2(X1) != X0 ) ) ),
inference(rectify,[],[f31]) ).
tff(f35,plain,
? [X0: $int,X1: $int,X2: $int,X3: 'Array[Int,Int]'] :
( $less(X0,length(X3))
& ! [X4: $int] :
( ( ( ( ! [X5: $int] :
( ~ $less(X5,length(X3))
| ( $sum(X4,$uminus(1)) != X5 )
| $less(X2,0)
| ~ sorted(X3,0,$sum(length(X3),$uminus(1))) )
& ~ $less('select:(Array[Int,Int]*Int)>Int'(X3,X4),X1) )
| ( $less('select:(Array[Int,Int]*Int)>Int'(X3,X4),X1)
& ! [X6: $int] :
( ( $sum(X4,1) != X6 )
| ~ $less(X0,length(X3))
| $less(X6,0)
| ~ sorted(X3,0,$sum(length(X3),$uminus(1))) ) ) )
& ( 'select:(Array[Int,Int]*Int)>Int'(X3,X4) != X1 ) )
| ( div2($sum(X2,X0)) != X4 ) )
& ~ $less(X0,X2)
& sorted(X3,0,$sum(length(X3),$uminus(1)))
& ~ $less(X2,0) ),
inference(rectify,[],[f22]) ).
tff(f36,plain,
( $less(sK3,length(sK6))
& ! [X4: $int] :
( ( ( ( ! [X5: $int] :
( ~ $less(X5,length(sK6))
| ( $sum(X4,$uminus(1)) != X5 )
| $less(sK5,0)
| ~ sorted(sK6,0,$sum(length(sK6),$uminus(1))) )
& ~ $less('select:(Array[Int,Int]*Int)>Int'(sK6,X4),sK4) )
| ( $less('select:(Array[Int,Int]*Int)>Int'(sK6,X4),sK4)
& ! [X6: $int] :
( ( $sum(X4,1) != X6 )
| ~ $less(sK3,length(sK6))
| $less(X6,0)
| ~ sorted(sK6,0,$sum(length(sK6),$uminus(1))) ) ) )
& ( sK4 != 'select:(Array[Int,Int]*Int)>Int'(sK6,X4) ) )
| ( div2($sum(sK5,sK3)) != X4 ) )
& ~ $less(sK3,sK5)
& sorted(sK6,0,$sum(length(sK6),$uminus(1)))
& ~ $less(sK5,0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3,sK4,sK5,sK6]),skolemize(X0,sK3),skolemize(X1,sK4),skolemize(X2,sK5),skolemize(X3,sK6)],[f35]) ).
tff(f43,plain,
! [X0: $int,X1: $int] :
( $less(X1,$product(2,$sum(X0,1)))
| ( div2(X1) != X0 ) ),
inference(cnf_transformation,[],[f32]) ).
tff(f44,plain,
! [X0: $int,X1: $int] :
( ~ $less(X1,$product(2,X0))
| ( div2(X1) != X0 ) ),
inference(cnf_transformation,[],[f32]) ).
tff(f50,plain,
~ $less(sK5,0),
inference(cnf_transformation,[],[f36]) ).
tff(f51,plain,
sorted(sK6,0,$sum(length(sK6),$uminus(1))),
inference(cnf_transformation,[],[f36]) ).
tff(f52,plain,
~ $less(sK3,sK5),
inference(cnf_transformation,[],[f36]) ).
tff(f56,plain,
! [X6: $int,X4: $int,X5: $int] :
( ~ $less(X5,length(sK6))
| ( $sum(X4,$uminus(1)) != X5 )
| $less(sK5,0)
| ~ sorted(sK6,0,$sum(length(sK6),$uminus(1)))
| ( $sum(X4,1) != X6 )
| ~ $less(sK3,length(sK6))
| $less(X6,0)
| ~ sorted(sK6,0,$sum(length(sK6),$uminus(1)))
| ( div2($sum(sK5,sK3)) != X4 ) ),
inference(cnf_transformation,[],[f36]) ).
tff(f58,plain,
$less(sK3,length(sK6)),
inference(cnf_transformation,[],[f36]) ).
tff(f59,plain,
! [X1: $int] : ~ $less(X1,$product(2,div2(X1))),
inference(equality_resolution,[],[f44]) ).
tff(f60,plain,
! [X1: $int] : $less(X1,$product(2,$sum(div2(X1),1))),
inference(equality_resolution,[],[f43]) ).
tff(f63,plain,
! [X6: $int,X4: $int] :
( ~ $less($sum(X4,$uminus(1)),length(sK6))
| $less(sK5,0)
| ~ sorted(sK6,0,$sum(length(sK6),$uminus(1)))
| ( $sum(X4,1) != X6 )
| ~ $less(sK3,length(sK6))
| $less(X6,0)
| ~ sorted(sK6,0,$sum(length(sK6),$uminus(1)))
| ( div2($sum(sK5,sK3)) != X4 ) ),
inference(equality_resolution,[],[f56]) ).
tff(f64,plain,
! [X4: $int] :
( ~ $less($sum(X4,$uminus(1)),length(sK6))
| $less(sK5,0)
| ~ sorted(sK6,0,$sum(length(sK6),$uminus(1)))
| ~ $less(sK3,length(sK6))
| $less($sum(X4,1),0)
| ~ sorted(sK6,0,$sum(length(sK6),$uminus(1)))
| ( div2($sum(sK5,sK3)) != X4 ) ),
inference(equality_resolution,[],[f63]) ).
tff(f65,plain,
( ~ $less($sum(div2($sum(sK5,sK3)),$uminus(1)),length(sK6))
| $less(sK5,0)
| ~ sorted(sK6,0,$sum(length(sK6),$uminus(1)))
| ~ $less(sK3,length(sK6))
| $less($sum(div2($sum(sK5,sK3)),1),0)
| ~ sorted(sK6,0,$sum(length(sK6),$uminus(1))) ),
inference(equality_resolution,[],[f64]) ).
tff(f70,definition,
sF7 = length(sK6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
tff(f71,plain,
$less(sK3,sF7),
inference(definition_folding,[],[f58,f70]) ).
tff(f72,definition,
sF8 = $sum(sK5,sK3),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
tff(f73,plain,
$sum(sK5,sK3) = sF8,
inference(reorient_equations,[],[f72]) ).
tff(f74,definition,
sF9 = div2(sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
tff(f75,definition,
sF10 = $uminus(1),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
tff(f76,definition,
sF11 = $sum(sF9,sF10),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
tff(f77,definition,
sF12 = $sum(sF7,sF10),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
tff(f81,definition,
sF14 = $sum(sF9,1),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
tff(f82,plain,
( ~ sorted(sK6,0,sF12)
| $less(sK5,0)
| ~ $less(sF11,sF7)
| $less(sF14,0)
| ~ $less(sK3,sF7)
| ~ sorted(sK6,0,sF12) ),
inference(definition_folding,[],[f65,f77,f75,f70,f81,f74,f73,f70,f77,f75,f70,f70,f76,f75,f74,f73]) ).
tff(f86,plain,
sorted(sK6,0,sF12),
inference(definition_folding,[],[f51,f77,f75,f70]) ).
tff(f87,plain,
( $less(sK5,0)
| ~ $less(sF11,sF7)
| ~ $less(sK3,sF7)
| ~ sorted(sK6,0,sF12)
| $less(sF14,0) ),
inference(duplicate_literal_removal,[],[f82]) ).
tff(f88,plain,
sF10 = -1,
inference(evaluation,[],[f75]) ).
tff(f90,definition,
( spl15_1
<=> $less(sF14,0) ),
introduced(definition,[new_symbols(definition,[spl15_1])],[avatar_definition]) ).
tff(f94,definition,
( spl15_2
<=> sorted(sK6,0,sF12) ),
introduced(definition,[new_symbols(definition,[spl15_2])],[avatar_definition]) ).
tff(f98,definition,
( spl15_3
<=> $less(sK5,0) ),
introduced(definition,[new_symbols(definition,[spl15_3])],[avatar_definition]) ).
tff(f102,definition,
( spl15_4
<=> $less(sK3,sF7) ),
introduced(definition,[new_symbols(definition,[spl15_4])],[avatar_definition]) ).
tff(f106,definition,
( spl15_5
<=> $less(sF11,sF7) ),
introduced(definition,[new_symbols(definition,[spl15_5])],[avatar_definition]) ).
tff(f109,plain,
( spl15_1
| ~ spl15_2
| spl15_3
| ~ spl15_4
| ~ spl15_5 ),
inference(avatar_split_clause,[],[f87,f106,f102,f98,f94,f90]) ).
tff(f111,definition,
( spl15_6
<=> ( sF14 = $sum(sF9,1) ) ),
introduced(definition,[new_symbols(definition,[spl15_6])],[avatar_definition]) ).
tff(f113,plain,
( ( sF14 = $sum(sF9,1) )
| ~ spl15_6 ),
inference(avatar_component_clause,[],[f111]) ).
tff(f114,plain,
spl15_6,
inference(avatar_split_clause,[],[f81,f111]) ).
tff(f136,definition,
( spl15_11
<=> ( sF11 = $sum(sF9,sF10) ) ),
introduced(definition,[new_symbols(definition,[spl15_11])],[avatar_definition]) ).
tff(f139,plain,
spl15_11,
inference(avatar_split_clause,[],[f76,f136]) ).
tff(f147,definition,
( spl15_13
<=> ( $sum(sK5,sK3) = sF8 ) ),
introduced(definition,[new_symbols(definition,[spl15_13])],[avatar_definition]) ).
tff(f150,plain,
spl15_13,
inference(avatar_split_clause,[],[f73,f147]) ).
tff(f151,plain,
spl15_4,
inference(avatar_split_clause,[],[f71,f102]) ).
tff(f152,plain,
spl15_2,
inference(avatar_split_clause,[],[f86,f94]) ).
tff(f154,definition,
( spl15_14
<=> ( sF9 = div2(sF8) ) ),
introduced(definition,[new_symbols(definition,[spl15_14])],[avatar_definition]) ).
tff(f156,plain,
( ( sF9 = div2(sF8) )
| ~ spl15_14 ),
inference(avatar_component_clause,[],[f154]) ).
tff(f157,plain,
spl15_14,
inference(avatar_split_clause,[],[f74,f154]) ).
tff(f158,plain,
~ spl15_3,
inference(avatar_split_clause,[],[f50,f98]) ).
tff(f160,definition,
( spl15_15
<=> $less(sK3,sK5) ),
introduced(definition,[new_symbols(definition,[spl15_15])],[avatar_definition]) ).
tff(f163,plain,
~ spl15_15,
inference(avatar_split_clause,[],[f52,f160]) ).
tff(f165,definition,
( spl15_16
<=> ( sF10 = -1 ) ),
introduced(definition,[new_symbols(definition,[spl15_16])],[avatar_definition]) ).
tff(f168,plain,
spl15_16,
inference(avatar_split_clause,[],[f88,f165]) ).
tff(f187,plain,
( ~ $less(sF8,$product(2,sF9))
| ~ spl15_14 ),
inference(superposition,[],[f59,f156]) ).
tff(f189,definition,
( spl15_20
<=> $less(sF8,$product(2,sF9)) ),
introduced(definition,[new_symbols(definition,[spl15_20])],[avatar_definition]) ).
tff(f192,plain,
( ~ spl15_20
| ~ spl15_14 ),
inference(avatar_split_clause,[],[f187,f154,f189]) ).
tff(f193,plain,
( $less(sF8,$product(2,$sum(sF9,1)))
| ~ spl15_14 ),
inference(superposition,[],[f60,f156]) ).
tff(f194,plain,
( $less(sF8,$product(2,sF14))
| ~ spl15_6
| ~ spl15_14 ),
inference(forward_demodulation,[],[f193,f113]) ).
tff(f196,definition,
( spl15_21
<=> $less(sF8,$product(2,sF14)) ),
introduced(definition,[new_symbols(definition,[spl15_21])],[avatar_definition]) ).
tff(f199,plain,
( spl15_21
| ~ spl15_6
| ~ spl15_14 ),
inference(avatar_split_clause,[],[f194,f154,f111,f196]) ).
tff(f200,plain,
$false,
inference(avatar_smt_refutation,[],[f199,f192,f168,f163,f158,f157,f152,f151,f150,f139,f114,f109]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW677_1 : TPTP v9.3.1. Released v6.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.18 % Computer : n011.cluster.edu
% 0.07/0.18 % Model : x86_64 x86_64
% 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.18 % Memory : 8046.5625MB
% 0.07/0.18 % OS : Linux 6.8.0-71-generic
% 0.07/0.18 % CPULimit : 300
% 0.07/0.18 % WCLimit : 300
% 0.07/0.18 % DateTime : Mon Sep 28 14:25:01 UTC 2026
% 0.07/0.19 % CPUTime :
% 0.07/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.22 Running first-order theorem proving
% 0.07/0.22 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.04/1.12 % (3420559)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 3.04/1.12 % (3420564)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=1420512337:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 3.04/1.12 % (3420564)Instruction limit reached!
% 3.04/1.12 % (3420564)------------------------------
% 3.04/1.12 % (3420564)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.04/1.12 % (3420564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/1.12 % (3420564)CaDiCaL version: 2.1.3
% 3.04/1.12 % (3420564)Termination reason: Instruction limit
% 3.04/1.12 % (3420564)Termination phase: Saturation
% 3.04/1.12 % (3420564)Time elapsed: 0.019 s
% 3.04/1.12 % (3420564)Peak memory usage: 116 MB
% 3.04/1.12 % (3420564)Instructions burned: 13 (million)
% 3.04/1.12 % (3420570)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=1067339532:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 3.04/1.12 % (3420565)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=374714629:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 3.04/1.12 % (3420568)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=1824403527:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 3.04/1.12 % (3420567)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=2798884551:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 3.04/1.12 % (3420566)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=640815243:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 3.04/1.12 % (3420569)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=1295710375:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 3.04/1.12 % (3420568)Instruction limit reached!
% 3.04/1.12 % (3420568)------------------------------
% 3.04/1.12 % (3420568)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.04/1.12 % (3420568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/1.12 % (3420568)CaDiCaL version: 2.1.3
% 3.04/1.12 % (3420568)Termination reason: Instruction limit
% 3.04/1.12 % (3420568)Termination phase: Saturation
% 3.04/1.12 % (3420568)Time elapsed: 0.004 s
% 3.04/1.12 % (3420568)Peak memory usage: 89 MB
% 3.04/1.12 % (3420568)Instructions burned: 5 (million)
% 3.04/1.12 % (3420567)Instruction limit reached!
% 3.04/1.12 % (3420567)------------------------------
% 3.04/1.12 % (3420567)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.04/1.12 % (3420567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/1.12 % (3420567)CaDiCaL version: 2.1.3
% 3.04/1.12 % (3420567)Termination reason: Instruction limit
% 3.04/1.12 % (3420567)Termination phase: Saturation
% 3.04/1.12 % (3420567)Time elapsed: 0.005 s
% 3.04/1.12 % (3420567)Peak memory usage: 88 MB
% 3.04/1.12 % (3420567)Instructions burned: 8 (million)
% 3.04/1.12 % (3420565)First to succeed.
% 3.04/1.12 % (3420565)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3420559"
% 3.04/1.12 % (3420570)Also succeeded, but the first one will report.
% 3.04/1.12 % (3420569)Instruction limit reached!
% 3.04/1.12 % (3420569)------------------------------
% 3.04/1.12 % (3420569)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.04/1.12 % (3420569)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/1.12 % (3420569)CaDiCaL version: 2.1.3
% 3.04/1.12 % (3420569)Termination reason: Instruction limit
% 3.04/1.12 % (3420569)Termination phase: Saturation
% 3.04/1.12 % (3420569)Time elapsed: 0.053 s
% 3.04/1.12 % (3420569)Peak memory usage: 116 MB
% 3.04/1.12 % (3420569)Instructions burned: 47 (million)
% 3.04/1.12 % (3420572)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=2173778884:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 3.04/1.12 % (3420572)Instruction limit reached!
% 3.04/1.12 % (3420572)------------------------------
% 3.04/1.12 % (3420572)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.04/1.12 % (3420572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/1.12 % (3420572)CaDiCaL version: 2.1.3
% 3.04/1.12 % (3420572)Termination reason: Instruction limit
% 3.04/1.12 % (3420572)Termination phase: Saturation
% 3.04/1.12 % (3420572)Time elapsed: 0.006 s
% 3.04/1.12 % (3420572)Peak memory usage: 88 MB
% 3.04/1.12 % (3420572)Instructions burned: 16 (million)
% 3.04/1.12 % (3420580)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=877537835:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi)
% 3.04/1.12 % (3420579)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=3437658325:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi)
% 3.04/1.12 % (3420580)Instruction limit reached!
% 3.04/1.12 % (3420580)------------------------------
% 3.04/1.12 % (3420580)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.04/1.12 % (3420580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/1.12 % (3420580)CaDiCaL version: 2.1.3
% 3.04/1.12 % (3420580)Termination reason: Instruction limit
% 3.04/1.12 % (3420580)Termination phase: Saturation
% 3.04/1.12 % (3420580)Time elapsed: 0.011 s
% 3.04/1.12 % (3420580)Peak memory usage: 90 MB
% 3.04/1.12 % (3420580)Instructions burned: 17 (million)
% 3.04/1.12 % (3420579)Instruction limit reached!
% 3.04/1.12 % (3420579)------------------------------
% 3.04/1.12 % (3420579)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.04/1.12 % (3420579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/1.12 % (3420579)CaDiCaL version: 2.1.3
% 3.04/1.12 % (3420579)Termination reason: Instruction limit
% 3.04/1.12 % (3420579)Termination phase: Saturation
% 3.04/1.12 % (3420579)Time elapsed: 0.024 s
% 3.04/1.12 % (3420579)Peak memory usage: 88 MB
% 3.04/1.12 % (3420579)Instructions burned: 30 (million)
% 3.04/1.12 % (3420583)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=2839815463:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi)
% 3.04/1.12 % (3420566)Instruction limit reached!
% 3.04/1.12 % (3420566)------------------------------
% 3.04/1.12 % (3420566)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.04/1.12 % (3420566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/1.12 % (3420566)CaDiCaL version: 2.1.3
% 3.04/1.12 % (3420566)Termination reason: Instruction limit
% 3.04/1.12 % (3420566)Termination phase: Saturation
% 3.04/1.12 % (3420566)Time elapsed: 0.173 s
% 3.04/1.12 % (3420566)Peak memory usage: 118 MB
% 3.04/1.12 % (3420566)Instructions burned: 202 (million)
% 3.04/1.12 % (3420583)Instruction limit reached!
% 3.04/1.12 % (3420583)------------------------------
% 3.04/1.12 % (3420583)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.04/1.12 % (3420583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/1.12 % (3420583)CaDiCaL version: 2.1.3
% 3.04/1.12 % (3420583)Termination reason: Instruction limit
% 3.04/1.12 % (3420583)Termination phase: Saturation
% 3.04/1.12 % (3420583)Time elapsed: 0.009 s
% 3.04/1.12 % (3420583)Peak memory usage: 89 MB
% 3.04/1.12 % (3420583)Instructions burned: 30 (million)
% 3.04/1.12 % (3420581)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=214840211:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 3.04/1.12 % (3420581)Instruction limit reached!
% 3.04/1.12 % (3420581)------------------------------
% 3.04/1.12 % (3420581)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.04/1.12 % (3420581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/1.12 % (3420581)CaDiCaL version: 2.1.3
% 3.04/1.12 % (3420581)Termination reason: Instruction limit
% 3.04/1.12 % (3420581)Termination phase: Saturation
% 3.04/1.12 % (3420581)Time elapsed: 0.019 s
% 3.04/1.12 % (3420581)Peak memory usage: 89 MB
% 3.04/1.12 % (3420581)Instructions burned: 24 (million)
% 3.04/1.12 % (3420591)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=2841231069:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi)
% 3.04/1.12 % (3420591)Instruction limit reached!
% 3.04/1.12 % (3420591)------------------------------
% 3.04/1.12 % (3420591)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.04/1.12 % (3420591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/1.12 % (3420591)CaDiCaL version: 2.1.3
% 3.04/1.12 % (3420591)Termination reason: Instruction limit
% 3.04/1.12 % (3420591)Termination phase: Saturation
% 3.04/1.12 % (3420591)Time elapsed: 0.002 s
% 3.04/1.12 % (3420591)Peak memory usage: 88 MB
% 3.04/1.12 % (3420591)Instructions burned: 4 (million)
% 3.04/1.12 % (3420586)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=3950802075:i=85:gtgl=4:rtra=on:gtg=exists_sym_2996 on theBenchmark for (2996ds/85Mi)
% 3.04/1.12 % (3420587)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=864105129:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi)
% 3.04/1.12 % (3420587)Instruction limit reached!
% 3.04/1.12 % (3420587)------------------------------
% 3.04/1.12 % (3420587)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.04/1.12 % (3420587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.04/1.12 % (3420587)CaDiCaL version: 2.1.3
% 3.04/1.12 % (3420587)Termination reason: Instruction limit
% 3.04/1.12 % (3420587)Termination phase: Saturation
% 3.04/1.12 % (3420587)Time elapsed: 0.002 s
% 3.04/1.12 % (3420587)Peak memory usage: 88 MB
% 3.04/1.12 % (3420587)Instructions burned: 2 (million)
% 3.04/1.12 % (3420565)Refutation found. Thanks to Tanya!
% 3.04/1.12 % SZS status Theorem for theBenchmark
% 3.04/1.12 % SZS output start Proof for theBenchmark
% See solution above
% 3.90/1.31 % (3420565)------------------------------
% 3.90/1.31 % (3420565)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.90/1.31 % (3420565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.90/1.31 % (3420565)CaDiCaL version: 2.1.3
% 3.90/1.31 % (3420565)Termination reason: Refutation
% 3.90/1.31 % (3420565)Time elapsed: 0.044 s
% 3.90/1.31 % (3420565)Peak memory usage: 116 MB
% 3.90/1.31 % (3420565)Instructions burned: 26 (million)
% 3.90/1.31 % (3420565)------------------------------
% 3.90/1.31 % (3420565)------------------------------
% 3.90/1.31 % (3420559)Success in time 0.46 s
% 3.90/1.31 % Vampire exiting
%------------------------------------------------------------------------------