%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : DAT330_1 : TPTP v9.3.1. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/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 09:47:47 AM UTC 2026
% Result : Unsatisfiable 14.19s 2.97s
% Output : Refutation 18.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 35
% Syntax : Number of formulae : 133 ( 19 unt; 0 typ; 25 def)
% Number of atoms : 305 ( 42 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 301 ( 129 ~; 128 |; 5 &)
% ( 28 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number arithmetic : 100 ( 42 atm; 0 fun; 17 num; 41 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 : 31 ( 26 usr; 26 prp; 0-2 aty)
% Number of functors : 21 ( 20 usr; 13 con; 0-3 aty)
% Number of variables : 60 ( 60 !; 0 ?; 60 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
'Set': $tType ).
tff(type_def_6,type,
'Array[Int,Int]': $tType ).
tff(func_def_0,type,
sup: 'Set' > $int ).
tff(func_def_1,type,
i3: $int ).
tff(func_def_2,type,
i2: $int ).
tff(func_def_3,type,
arr: 'Array[Int,Int]' ).
tff(func_def_4,type,
s1: 'Set' ).
tff(func_def_5,type,
i4: $int ).
tff(func_def_6,type,
i1: $int ).
tff(func_def_7,type,
delete: ( 'Set' * $int ) > 'Set' ).
tff(func_def_8,type,
'store:(Array[Int,Int]*Int*Int)>Array[Int,Int]': ( 'Array[Int,Int]' * $int * $int ) > 'Array[Int,Int]' ).
tff(func_def_9,type,
s4: 'Set' ).
tff(func_def_10,type,
'const:(Int)>Array[Int,Int]': $int > 'Array[Int,Int]' ).
tff(func_def_11,type,
g: $int > $int ).
tff(func_def_12,type,
s2: 'Set' ).
tff(func_def_13,type,
s0: 'Set' ).
tff(func_def_14,type,
s3: 'Set' ).
tff(func_def_15,type,
'select:(Array[Int,Int]*Int)>Int': ( 'Array[Int,Int]' * $int ) > $int ).
tff(func_def_16,type,
insert: ( 'Set' * $int ) > 'Set' ).
tff(func_def_18,type,
sK0: ( 'Array[Int,Int]' * 'Array[Int,Int]' ) > $int ).
tff(func_def_21,type,
'$inst2': $int ).
tff(func_def_22,type,
'$inst3': $int ).
tff(pred_def_1,type,
member: ( $int * 'Set' ) > $o ).
tff(f1,axiom,
! [X1: 'Set',X0: $int] : member(X0,insert(X1,X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_1) ).
tff(f2,axiom,
! [X1: $int,X0: $int,X2: 'Set'] :
( ( X0 != X1 )
=> ( member(X0,X2)
<=> member(X0,insert(X2,X1)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_2) ).
tff(f6,axiom,
! [X0: 'Set'] : member(sup(X0),X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_6) ).
tff(f7,axiom,
! [X1: $int,X0: 'Set'] :
( member(X1,X0)
=> $lesseq(X1,sup(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_7) ).
tff(f9,axiom,
! [X0: $int] :
( $greater(X0,0)
=> $less('select:(Array[Int,Int]*Int)>Int'(arr,X0),sup(s0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_9) ).
tff(f10,axiom,
! [X0: $int] : $greater(g(X0),0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_10) ).
tff(f11,axiom,
( ( $greater(i1,0)
=> ( s1 = insert(s0,'select:(Array[Int,Int]*Int)>Int'(arr,i1)) ) )
& ( ~ $greater(i1,0)
=> ( s1 = s0 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_11) ).
tff(f12,axiom,
s2 = insert(s1,'select:(Array[Int,Int]*Int)>Int'(arr,g(i2))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_12) ).
tff(f13,axiom,
s3 = insert(s2,'select:(Array[Int,Int]*Int)>Int'(arr,g(i3))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_13) ).
tff(f15,axiom,
sup(s3) != sup(s0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',formula_15) ).
tff(f20,plain,
! [X0: $int] : $less(0,g(X0)),
inference(theory_normalization,[],[f10]) ).
tff(f21,plain,
! [X1: $int,X0: 'Set'] :
( member(X1,X0)
=> ~ $less(sup(X0),X1) ),
inference(theory_normalization,[],[f7]) ).
tff(f22,plain,
! [X0: $int] :
( $less(0,X0)
=> $less('select:(Array[Int,Int]*Int)>Int'(arr,X0),sup(s0)) ),
inference(theory_normalization,[],[f9]) ).
tff(f23,plain,
( ( $less(0,i1)
=> ( s1 = insert(s0,'select:(Array[Int,Int]*Int)>Int'(arr,i1)) ) )
& ( ~ $less(0,i1)
=> ( s1 = s0 ) ) ),
inference(theory_normalization,[],[f11]) ).
tff(f25,plain,
! [X0: 'Set',X1: $int] : member(X1,insert(X0,X1)),
inference(rectify,[],[f1]) ).
tff(f26,plain,
! [X0: $int,X1: 'Set'] :
( member(X0,X1)
=> ~ $less(sup(X1),X0) ),
inference(rectify,[],[f21]) ).
tff(f29,plain,
! [X2: 'Set',X0: $int,X1: $int] :
( ( X0 != X1 )
=> ( member(X1,X2)
<=> member(X1,insert(X2,X0)) ) ),
inference(rectify,[],[f2]) ).
tff(f34,plain,
! [X0: $int] :
( $less('select:(Array[Int,Int]*Int)>Int'(arr,X0),sup(s0))
| ~ $less(0,X0) ),
inference(ennf_transformation,[],[f22]) ).
tff(f35,plain,
( ( ~ $less(0,i1)
| ( s1 = insert(s0,'select:(Array[Int,Int]*Int)>Int'(arr,i1)) ) )
& ( $less(0,i1)
| ( s1 = s0 ) ) ),
inference(ennf_transformation,[],[f23]) ).
tff(f40,plain,
! [X1: 'Set',X0: $int] :
( ~ member(X0,X1)
| ~ $less(sup(X1),X0) ),
inference(ennf_transformation,[],[f26]) ).
tff(f41,plain,
! [X2: 'Set',X1: $int,X0: $int] :
( ( member(X1,X2)
<=> member(X1,insert(X2,X0)) )
| ( X0 = X1 ) ),
inference(ennf_transformation,[],[f29]) ).
tff(f46,plain,
! [X0: 'Set',X1: $int] :
( ~ member(X1,X0)
| ~ $less(sup(X0),X1) ),
inference(rectify,[],[f40]) ).
tff(f48,plain,
! [X2: 'Set',X1: $int,X0: $int] :
( ( ( member(X1,X2)
| ~ member(X1,insert(X2,X0)) )
& ( member(X1,insert(X2,X0))
| ~ member(X1,X2) ) )
| ( X0 = X1 ) ),
inference(nnf_transformation,[],[f41]) ).
tff(f49,plain,
! [X0: 'Set',X1: $int,X2: $int] :
( ( ( member(X1,X0)
| ~ member(X1,insert(X0,X2)) )
& ( member(X1,insert(X0,X2))
| ~ member(X1,X0) ) )
| ( X1 = X2 ) ),
inference(rectify,[],[f48]) ).
tff(f52,plain,
sup(s0) != sup(s3),
inference(cnf_transformation,[],[f15]) ).
tff(f56,plain,
! [X0: 'Set',X1: $int] :
( ~ $less(sup(X0),X1)
| ~ member(X1,X0) ),
inference(cnf_transformation,[],[f46]) ).
tff(f57,plain,
! [X0: $int] : $less(0,g(X0)),
inference(cnf_transformation,[],[f20]) ).
tff(f58,plain,
! [X0: 'Set',X1: $int] : member(X1,insert(X0,X1)),
inference(cnf_transformation,[],[f25]) ).
tff(f61,plain,
! [X0: 'Set'] : member(sup(X0),X0),
inference(cnf_transformation,[],[f6]) ).
tff(f63,plain,
! [X2: $int,X0: 'Set',X1: $int] :
( member(X1,insert(X0,X2))
| ~ member(X1,X0)
| ( X1 = X2 ) ),
inference(cnf_transformation,[],[f49]) ).
tff(f64,plain,
! [X2: $int,X0: 'Set',X1: $int] :
( ~ member(X1,insert(X0,X2))
| member(X1,X0)
| ( X1 = X2 ) ),
inference(cnf_transformation,[],[f49]) ).
tff(f65,plain,
( ( s0 = s1 )
| $less(0,i1) ),
inference(cnf_transformation,[],[f35]) ).
tff(f66,plain,
( ( s1 = insert(s0,'select:(Array[Int,Int]*Int)>Int'(arr,i1)) )
| ~ $less(0,i1) ),
inference(cnf_transformation,[],[f35]) ).
tff(f67,plain,
s2 = insert(s1,'select:(Array[Int,Int]*Int)>Int'(arr,g(i2))),
inference(cnf_transformation,[],[f12]) ).
tff(f69,plain,
! [X0: $int] :
( $less('select:(Array[Int,Int]*Int)>Int'(arr,X0),sup(s0))
| ~ $less(0,X0) ),
inference(cnf_transformation,[],[f34]) ).
tff(f70,plain,
s3 = insert(s2,'select:(Array[Int,Int]*Int)>Int'(arr,g(i3))),
inference(cnf_transformation,[],[f13]) ).
tff(f73,definition,
( spl1_1
<=> ( s1 = insert(s0,'select:(Array[Int,Int]*Int)>Int'(arr,i1)) ) ),
introduced(definition,[new_symbols(definition,[spl1_1])],[avatar_definition]) ).
tff(f75,plain,
( ( s1 = insert(s0,'select:(Array[Int,Int]*Int)>Int'(arr,i1)) )
| ~ spl1_1 ),
inference(avatar_component_clause,[],[f73]) ).
tff(f77,definition,
( spl1_2
<=> $less(0,i1) ),
introduced(definition,[new_symbols(definition,[spl1_2])],[avatar_definition]) ).
tff(f78,plain,
( $less(0,i1)
| ~ spl1_2 ),
inference(avatar_component_clause,[],[f77]) ).
tff(f80,plain,
( spl1_1
| ~ spl1_2 ),
inference(avatar_split_clause,[],[f66,f77,f73]) ).
tff(f82,definition,
( spl1_3
<=> ( s0 = s1 ) ),
introduced(definition,[new_symbols(definition,[spl1_3])],[avatar_definition]) ).
tff(f84,plain,
( ( s0 = s1 )
| ~ spl1_3 ),
inference(avatar_component_clause,[],[f82]) ).
tff(f85,plain,
( spl1_2
| spl1_3 ),
inference(avatar_split_clause,[],[f65,f82,f77]) ).
tff(f87,definition,
( spl1_4
<=> ( s3 = insert(s2,'select:(Array[Int,Int]*Int)>Int'(arr,g(i3))) ) ),
introduced(definition,[new_symbols(definition,[spl1_4])],[avatar_definition]) ).
tff(f89,plain,
( ( s3 = insert(s2,'select:(Array[Int,Int]*Int)>Int'(arr,g(i3))) )
| ~ spl1_4 ),
inference(avatar_component_clause,[],[f87]) ).
tff(f90,plain,
spl1_4,
inference(avatar_split_clause,[],[f70,f87]) ).
tff(f97,definition,
( spl1_6
<=> ( sup(s0) = sup(s3) ) ),
introduced(definition,[new_symbols(definition,[spl1_6])],[avatar_definition]) ).
tff(f100,plain,
~ spl1_6,
inference(avatar_split_clause,[],[f52,f97]) ).
tff(f102,definition,
( spl1_7
<=> ( s2 = insert(s1,'select:(Array[Int,Int]*Int)>Int'(arr,g(i2))) ) ),
introduced(definition,[new_symbols(definition,[spl1_7])],[avatar_definition]) ).
tff(f104,plain,
( ( s2 = insert(s1,'select:(Array[Int,Int]*Int)>Int'(arr,g(i2))) )
| ~ spl1_7 ),
inference(avatar_component_clause,[],[f102]) ).
tff(f105,plain,
spl1_7,
inference(avatar_split_clause,[],[f67,f102]) ).
tff(f108,plain,
( member('select:(Array[Int,Int]*Int)>Int'(arr,i1),s1)
| ~ spl1_1 ),
inference(superposition,[],[f58,f75]) ).
tff(f110,definition,
( spl1_8
<=> member('select:(Array[Int,Int]*Int)>Int'(arr,i1),s1) ),
introduced(definition,[new_symbols(definition,[spl1_8])],[avatar_definition]) ).
tff(f112,plain,
( member('select:(Array[Int,Int]*Int)>Int'(arr,i1),s1)
| ~ spl1_8 ),
inference(avatar_component_clause,[],[f110]) ).
tff(f113,plain,
( spl1_8
| ~ spl1_1 ),
inference(avatar_split_clause,[],[f108,f73,f110]) ).
tff(f115,plain,
( member('select:(Array[Int,Int]*Int)>Int'(arr,g(i3)),s3)
| ~ spl1_4 ),
inference(superposition,[],[f58,f89]) ).
tff(f117,definition,
( spl1_9
<=> member('select:(Array[Int,Int]*Int)>Int'(arr,g(i3)),s3) ),
introduced(definition,[new_symbols(definition,[spl1_9])],[avatar_definition]) ).
tff(f119,plain,
( member('select:(Array[Int,Int]*Int)>Int'(arr,g(i3)),s3)
| ~ spl1_9 ),
inference(avatar_component_clause,[],[f117]) ).
tff(f120,plain,
( spl1_9
| ~ spl1_4 ),
inference(avatar_split_clause,[],[f115,f87,f117]) ).
tff(f133,plain,
( member('select:(Array[Int,Int]*Int)>Int'(arr,g(i2)),s2)
| ~ spl1_7 ),
inference(superposition,[],[f58,f104]) ).
tff(f135,definition,
( spl1_12
<=> member('select:(Array[Int,Int]*Int)>Int'(arr,g(i2)),s2) ),
introduced(definition,[new_symbols(definition,[spl1_12])],[avatar_definition]) ).
tff(f137,plain,
( member('select:(Array[Int,Int]*Int)>Int'(arr,g(i2)),s2)
| ~ spl1_12 ),
inference(avatar_component_clause,[],[f135]) ).
tff(f138,plain,
( spl1_12
| ~ spl1_7 ),
inference(avatar_split_clause,[],[f133,f102,f135]) ).
tff(f167,plain,
( $less('select:(Array[Int,Int]*Int)>Int'(arr,i1),sup(s0))
| ~ spl1_2 ),
inference(unit_resulting_resolution,[],[f69,f78]) ).
tff(f168,plain,
! [X0: $int] : $less('select:(Array[Int,Int]*Int)>Int'(arr,g(X0)),sup(s0)),
inference(unit_resulting_resolution,[],[f69,f57]) ).
tff(f170,definition,
( spl1_17
<=> $less('select:(Array[Int,Int]*Int)>Int'(arr,i1),sup(s0)) ),
introduced(definition,[new_symbols(definition,[spl1_17])],[avatar_definition]) ).
tff(f173,plain,
( spl1_17
| ~ spl1_2 ),
inference(avatar_split_clause,[],[f167,f77,f170]) ).
tff(f210,definition,
( spl1_23
<=> ( 'select:(Array[Int,Int]*Int)>Int'(arr,g(i3)) = sup(s3) ) ),
introduced(definition,[new_symbols(definition,[spl1_23])],[avatar_definition]) ).
tff(f212,plain,
( ( 'select:(Array[Int,Int]*Int)>Int'(arr,g(i3)) = sup(s3) )
| ~ spl1_23 ),
inference(avatar_component_clause,[],[f210]) ).
tff(f219,definition,
( spl1_25
<=> ( 'select:(Array[Int,Int]*Int)>Int'(arr,i1) = sup(s1) ) ),
introduced(definition,[new_symbols(definition,[spl1_25])],[avatar_definition]) ).
tff(f233,definition,
( spl1_28
<=> ( 'select:(Array[Int,Int]*Int)>Int'(arr,g(i2)) = sup(s2) ) ),
introduced(definition,[new_symbols(definition,[spl1_28])],[avatar_definition]) ).
tff(f235,plain,
( ( 'select:(Array[Int,Int]*Int)>Int'(arr,g(i2)) = sup(s2) )
| ~ spl1_28 ),
inference(avatar_component_clause,[],[f233]) ).
tff(f245,plain,
( ! [X0: $int] :
( ( 'select:(Array[Int,Int]*Int)>Int'(arr,g(i2)) = X0 )
| ~ member(X0,s1)
| member(X0,s2) )
| ~ spl1_7 ),
inference(superposition,[],[f63,f104]) ).
tff(f246,plain,
( ! [X0: $int] :
( ( 'select:(Array[Int,Int]*Int)>Int'(arr,g(i3)) = X0 )
| member(X0,s3)
| ~ member(X0,s2) )
| ~ spl1_4 ),
inference(superposition,[],[f63,f89]) ).
tff(f247,plain,
( ! [X0: $int] :
( ( 'select:(Array[Int,Int]*Int)>Int'(arr,i1) = X0 )
| member(X0,s1)
| ~ member(X0,s0) )
| ~ spl1_1 ),
inference(superposition,[],[f63,f75]) ).
tff(f259,plain,
! [X0: 'Set',X1: $int] :
( member(sup(insert(X0,X1)),X0)
| ( sup(insert(X0,X1)) = X1 ) ),
inference(resolution,[],[f64,f61]) ).
tff(f325,plain,
( ! [X0: $int] :
( member(X0,s1)
| ~ member(X0,s0)
| member(X0,s1) )
| ~ spl1_1
| ~ spl1_8 ),
inference(superposition,[],[f112,f247]) ).
tff(f331,plain,
( ! [X0: $int] :
( ~ member(X0,s0)
| member(X0,s1) )
| ~ spl1_1
| ~ spl1_8 ),
inference(duplicate_literal_removal,[],[f325]) ).
tff(f362,definition,
( spl1_38
<=> $less(sup(s3),sup(s0)) ),
introduced(definition,[new_symbols(definition,[spl1_38])],[avatar_definition]) ).
tff(f363,plain,
( $less(sup(s3),sup(s0))
| ~ spl1_38 ),
inference(avatar_component_clause,[],[f362]) ).
tff(f374,plain,
( ! [X0: $int] :
( member(X0,s2)
| member(X0,s2)
| ~ member(X0,s1) )
| ~ spl1_7
| ~ spl1_12 ),
inference(superposition,[],[f137,f245]) ).
tff(f378,plain,
( ! [X0: $int] :
( ~ member(X0,s1)
| member(X0,s2) )
| ~ spl1_7
| ~ spl1_12 ),
inference(duplicate_literal_removal,[],[f374]) ).
tff(f390,plain,
( ! [X0: $int] :
( ~ member(X0,s2)
| member(X0,s3)
| member(X0,s3) )
| ~ spl1_4
| ~ spl1_9 ),
inference(superposition,[],[f119,f246]) ).
tff(f394,plain,
( ! [X0: $int] :
( ~ member(X0,s2)
| member(X0,s3) )
| ~ spl1_4
| ~ spl1_9 ),
inference(duplicate_literal_removal,[],[f390]) ).
tff(f403,plain,
( member(sup(s0),s1)
| ~ spl1_1
| ~ spl1_8 ),
inference(resolution,[],[f331,f61]) ).
tff(f405,definition,
( spl1_42
<=> member(sup(s0),s1) ),
introduced(definition,[new_symbols(definition,[spl1_42])],[avatar_definition]) ).
tff(f407,plain,
( member(sup(s0),s1)
| ~ spl1_42 ),
inference(avatar_component_clause,[],[f405]) ).
tff(f408,plain,
( spl1_42
| ~ spl1_1
| ~ spl1_8 ),
inference(avatar_split_clause,[],[f403,f110,f73,f405]) ).
tff(f435,plain,
( member(sup(s1),s2)
| ~ spl1_7
| ~ spl1_12 ),
inference(resolution,[],[f378,f61]) ).
tff(f438,definition,
( spl1_47
<=> member(sup(s1),s2) ),
introduced(definition,[new_symbols(definition,[spl1_47])],[avatar_definition]) ).
tff(f440,plain,
( member(sup(s1),s2)
| ~ spl1_47 ),
inference(avatar_component_clause,[],[f438]) ).
tff(f441,plain,
( spl1_47
| ~ spl1_7
| ~ spl1_12 ),
inference(avatar_split_clause,[],[f435,f135,f102,f438]) ).
tff(f458,plain,
( ( 'select:(Array[Int,Int]*Int)>Int'(arr,g(i2)) = sup(s2) )
| member(sup(s2),s1)
| ~ spl1_7 ),
inference(superposition,[],[f259,f104]) ).
tff(f459,plain,
( member(sup(s3),s2)
| ( 'select:(Array[Int,Int]*Int)>Int'(arr,g(i3)) = sup(s3) )
| ~ spl1_4 ),
inference(superposition,[],[f259,f89]) ).
tff(f464,definition,
( spl1_49
<=> member(sup(s3),s2) ),
introduced(definition,[new_symbols(definition,[spl1_49])],[avatar_definition]) ).
tff(f466,plain,
( member(sup(s3),s2)
| ~ spl1_49 ),
inference(avatar_component_clause,[],[f464]) ).
tff(f467,plain,
( spl1_49
| spl1_23
| ~ spl1_4 ),
inference(avatar_split_clause,[],[f459,f87,f210,f464]) ).
tff(f469,definition,
( spl1_50
<=> member(sup(s2),s1) ),
introduced(definition,[new_symbols(definition,[spl1_50])],[avatar_definition]) ).
tff(f471,plain,
( member(sup(s2),s1)
| ~ spl1_50 ),
inference(avatar_component_clause,[],[f469]) ).
tff(f472,plain,
( spl1_28
| spl1_50
| ~ spl1_7 ),
inference(avatar_split_clause,[],[f458,f102,f469,f233]) ).
tff(f490,plain,
( $less(sup(s3),sup(s0))
| ~ spl1_23 ),
inference(superposition,[],[f168,f212]) ).
tff(f507,plain,
( spl1_38
| ~ spl1_23 ),
inference(avatar_split_clause,[],[f490,f210,f362]) ).
tff(f509,plain,
( member(sup(s0),s2)
| ~ spl1_3
| ~ spl1_47 ),
inference(superposition,[],[f440,f84]) ).
tff(f511,definition,
( spl1_57
<=> member(sup(s0),s2) ),
introduced(definition,[new_symbols(definition,[spl1_57])],[avatar_definition]) ).
tff(f513,plain,
( member(sup(s0),s2)
| ~ spl1_57 ),
inference(avatar_component_clause,[],[f511]) ).
tff(f514,plain,
( spl1_57
| ~ spl1_3
| ~ spl1_47 ),
inference(avatar_split_clause,[],[f509,f438,f82,f511]) ).
tff(f536,plain,
( member(sup(s1),s0)
| ( 'select:(Array[Int,Int]*Int)>Int'(arr,i1) = sup(s1) )
| ~ spl1_1 ),
inference(superposition,[],[f259,f75]) ).
tff(f538,definition,
( spl1_60
<=> member(sup(s1),s0) ),
introduced(definition,[new_symbols(definition,[spl1_60])],[avatar_definition]) ).
tff(f540,plain,
( member(sup(s1),s0)
| ~ spl1_60 ),
inference(avatar_component_clause,[],[f538]) ).
tff(f541,plain,
( spl1_25
| spl1_60
| ~ spl1_1 ),
inference(avatar_split_clause,[],[f536,f73,f538,f219]) ).
tff(f542,plain,
( member(sup(s0),s2)
| ~ spl1_7
| ~ spl1_12
| ~ spl1_42 ),
inference(unit_resulting_resolution,[],[f378,f407]) ).
tff(f546,plain,
( spl1_57
| ~ spl1_7
| ~ spl1_12
| ~ spl1_42 ),
inference(avatar_split_clause,[],[f542,f405,f135,f102,f511]) ).
tff(f566,plain,
( ~ $less(sup(s2),sup(s3))
| ~ spl1_49 ),
inference(unit_resulting_resolution,[],[f56,f466]) ).
tff(f573,definition,
( spl1_65
<=> $less(sup(s2),sup(s3)) ),
introduced(definition,[new_symbols(definition,[spl1_65])],[avatar_definition]) ).
tff(f576,plain,
( ~ spl1_65
| ~ spl1_49 ),
inference(avatar_split_clause,[],[f566,f464,f573]) ).
tff(f637,plain,
( $less(sup(s2),sup(s0))
| ~ spl1_28 ),
inference(superposition,[],[f168,f235]) ).
tff(f645,definition,
( spl1_75
<=> $less(sup(s1),sup(s2)) ),
introduced(definition,[new_symbols(definition,[spl1_75])],[avatar_definition]) ).
tff(f650,definition,
( spl1_76
<=> $less(sup(s2),sup(s0)) ),
introduced(definition,[new_symbols(definition,[spl1_76])],[avatar_definition]) ).
tff(f654,plain,
( spl1_76
| ~ spl1_28 ),
inference(avatar_split_clause,[],[f637,f233,f650]) ).
tff(f661,plain,
( ~ $less(sup(s1),sup(s2))
| ~ spl1_50 ),
inference(unit_resulting_resolution,[],[f56,f471]) ).
tff(f663,plain,
( ~ spl1_75
| ~ spl1_50 ),
inference(avatar_split_clause,[],[f661,f469,f645]) ).
tff(f701,plain,
( ~ $less(sup(s0),sup(s1))
| ~ spl1_60 ),
inference(unit_resulting_resolution,[],[f56,f540]) ).
tff(f703,definition,
( spl1_82
<=> $less(sup(s0),sup(s1)) ),
introduced(definition,[new_symbols(definition,[spl1_82])],[avatar_definition]) ).
tff(f706,plain,
( ~ spl1_82
| ~ spl1_60 ),
inference(avatar_split_clause,[],[f701,f538,f703]) ).
tff(f740,plain,
( ~ $less(sup(s2),sup(s0))
| ~ spl1_57 ),
inference(unit_resulting_resolution,[],[f56,f513]) ).
tff(f746,plain,
( ~ spl1_76
| ~ spl1_57 ),
inference(avatar_split_clause,[],[f740,f511,f650]) ).
tff(f782,plain,
( ~ member(sup(s0),s3)
| ~ spl1_38 ),
inference(unit_resulting_resolution,[],[f56,f363]) ).
tff(f787,definition,
( spl1_88
<=> member(sup(s0),s3) ),
introduced(definition,[new_symbols(definition,[spl1_88])],[avatar_definition]) ).
tff(f790,plain,
( ~ spl1_88
| ~ spl1_38 ),
inference(avatar_split_clause,[],[f782,f362,f787]) ).
tff(f1030,plain,
( member(sup(s0),s3)
| ~ spl1_4
| ~ spl1_9
| ~ spl1_57 ),
inference(resolution,[],[f394,f513]) ).
tff(f1040,plain,
( spl1_88
| ~ spl1_4
| ~ spl1_9
| ~ spl1_57 ),
inference(avatar_split_clause,[],[f1030,f511,f117,f87,f787]) ).
tff(f1051,plain,
$false,
inference(avatar_smt_refutation,[],[f1040,f790,f746,f706,f663,f654,f576,f546,f541,f514,f507,f472,f467,f441,f408,f173,f138,f120,f113,f105,f100,f90,f85,f80]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : DAT330_1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.18 % Computer : n020.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Tue Sep 29 00:20:34 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.21 Running first-order theorem proving
% 0.08/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
% 5.00/1.18 % (723177)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 5.00/1.18 % (723246)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=3068304900:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 5.00/1.18 % (723251)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=3059755733:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 5.00/1.18 % (723247)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=759408119:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 5.00/1.18 % (723249)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=1921025569:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 5.00/1.18 % (723248)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2936411251:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 5.00/1.18 % (723251)Instruction limit reached!
% 5.00/1.18 % (723251)------------------------------
% 5.00/1.18 % (723251)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.00/1.18 % (723251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.00/1.18 % (723251)CaDiCaL version: 2.1.3
% 5.00/1.18 % (723251)Termination reason: Instruction limit
% 5.00/1.18 % (723251)Termination phase: Saturation
% 5.00/1.18 % (723251)Time elapsed: 0.004 s
% 5.00/1.18 % (723251)Peak memory usage: 89 MB
% 5.00/1.18 % (723251)Instructions burned: 5 (million)
% 5.00/1.18 % (723249)Instruction limit reached!
% 5.00/1.18 % (723249)------------------------------
% 5.00/1.18 % (723249)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.00/1.18 % (723249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.00/1.18 % (723249)CaDiCaL version: 2.1.3
% 5.00/1.18 % (723249)Termination reason: Instruction limit
% 5.00/1.18 % (723249)Termination phase: Saturation
% 5.00/1.18 % (723249)Time elapsed: 0.005 s
% 5.00/1.18 % (723249)Peak memory usage: 88 MB
% 5.00/1.18 % (723249)Instructions burned: 7 (million)
% 5.00/1.18 % (723246)Refutation not found, incomplete strategy
% 5.00/1.18 % (723246)------------------------------
% 5.00/1.18 % (723246)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.00/1.18 % (723246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.00/1.18 % (723246)CaDiCaL version: 2.1.3
% 5.00/1.18 % (723246)Termination reason: Refutation not found, incomplete strategy
% 5.00/1.18 % (723246)Time elapsed: 0.017 s
% 5.00/1.18 % (723246)Peak memory usage: 111 MB
% 5.00/1.18 % (723246)Instructions burned: 5 (million)
% 5.00/1.18 % (723253)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=2780194559:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 5.00/1.18 % (723253)Instruction limit reached!
% 5.00/1.18 % (723253)------------------------------
% 5.00/1.18 % (723253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.00/1.18 % (723253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.00/1.18 % (723253)CaDiCaL version: 2.1.3
% 5.00/1.18 % (723253)Termination reason: Instruction limit
% 5.00/1.18 % (723253)Termination phase: Saturation
% 5.00/1.18 % (723253)Time elapsed: 0.048 s
% 5.00/1.18 % (723253)Peak memory usage: 115 MB
% 5.00/1.18 % (723253)Instructions burned: 34 (million)
% 5.00/1.18 % (723252)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=3534296210:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 5.00/1.18 % (723248)Instruction limit reached!
% 5.00/1.18 % (723248)------------------------------
% 5.00/1.18 % (723248)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.00/1.18 % (723248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.00/1.18 % (723248)CaDiCaL version: 2.1.3
% 5.00/1.18 % (723248)Termination reason: Instruction limit
% 5.00/1.18 % (723248)Termination phase: Saturation
% 5.00/1.18 % (723248)Time elapsed: 0.130 s
% 5.00/1.18 % (723248)Peak memory usage: 117 MB
% 5.00/1.18 % (723248)Instructions burned: 201 (million)
% 5.00/1.18 % (723246)------------------------------
% 5.00/1.18 % (723246)------------------------------
% 5.00/1.18 % (723263)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=3219128493:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 5.00/1.18 % (723264)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=3354352892:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi)
% 6.41/1.56 % (723263)Refutation not found, incomplete strategy
% 6.41/1.56 % (723263)------------------------------
% 6.41/1.56 % (723263)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.41/1.56 % (723263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.41/1.56 % (723263)CaDiCaL version: 2.1.3
% 6.41/1.56 % (723263)Termination reason: Refutation not found, incomplete strategy
% 6.41/1.56 % (723263)Time elapsed: 0.001 s
% 6.41/1.56 % (723263)Peak memory usage: 87 MB
% 6.41/1.56 % (723252)Instruction limit reached!
% 6.41/1.56 % (723252)------------------------------
% 6.41/1.56 % (723252)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.41/1.56 % (723252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.41/1.56 % (723252)CaDiCaL version: 2.1.3
% 6.41/1.56 % (723252)Termination reason: Instruction limit
% 6.41/1.56 % (723252)Termination phase: Saturation
% 6.41/1.56 % (723252)Time elapsed: 0.085 s
% 6.41/1.56 % (723252)Peak memory usage: 116 MB
% 6.41/1.56 % (723252)Instructions burned: 46 (million)
% 6.41/1.56 % (723264)Instruction limit reached!
% 6.41/1.56 % (723264)------------------------------
% 6.41/1.56 % (723264)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.41/1.56 % (723264)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.41/1.56 % (723264)CaDiCaL version: 2.1.3
% 6.41/1.56 % (723264)Termination reason: Instruction limit
% 6.41/1.56 % (723264)Termination phase: Saturation
% 6.41/1.56 % (723264)Time elapsed: 0.023 s
% 6.41/1.56 % (723264)Peak memory usage: 88 MB
% 6.41/1.56 % (723264)Instructions burned: 29 (million)
% 6.41/1.56 % (723247)Instruction limit reached!
% 6.41/1.56 % (723247)------------------------------
% 6.41/1.56 % (723247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.41/1.56 % (723247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.41/1.56 % (723247)CaDiCaL version: 2.1.3
% 6.41/1.56 % (723247)Termination reason: Instruction limit
% 6.41/1.56 % (723247)Termination phase: Saturation
% 6.41/1.56 % (723247)Time elapsed: 0.222 s
% 6.41/1.56 % (723247)Peak memory usage: 117 MB
% 6.41/1.56 % (723247)Instructions burned: 308 (million)
% 6.41/1.56 % (723266)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2286171059:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi)
% 6.41/1.56 % (723266)Instruction limit reached!
% 6.41/1.56 % (723266)------------------------------
% 6.41/1.56 % (723266)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.41/1.56 % (723266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.41/1.56 % (723266)CaDiCaL version: 2.1.3
% 6.41/1.56 % (723266)Termination reason: Instruction limit
% 6.41/1.56 % (723266)Termination phase: Saturation
% 6.41/1.56 % (723266)Time elapsed: 0.012 s
% 6.41/1.56 % (723266)Peak memory usage: 90 MB
% 6.41/1.56 % (723266)Instructions burned: 16 (million)
% 6.41/1.56 % (723268)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=866120159:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 6.41/1.56 % (723269)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=1330484157:i=27:canc=cautious:fsr=off:rtra=on_2996 on theBenchmark for (2996ds/27Mi)
% 6.41/1.56 % (723268)Instruction limit reached!
% 6.41/1.56 % (723268)------------------------------
% 6.41/1.56 % (723268)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.41/1.56 % (723268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.41/1.56 % (723268)CaDiCaL version: 2.1.3
% 6.41/1.56 % (723268)Termination reason: Instruction limit
% 6.41/1.56 % (723268)Termination phase: Saturation
% 6.41/1.56 % (723268)Time elapsed: 0.019 s
% 6.41/1.56 % (723268)Peak memory usage: 89 MB
% 6.41/1.56 % (723268)Instructions burned: 24 (million)
% 6.41/1.56 % (723269)Refutation not found, incomplete strategy
% 6.41/1.56 % (723269)------------------------------
% 6.41/1.56 % (723269)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.41/1.56 % (723269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.41/1.56 % (723269)CaDiCaL version: 2.1.3
% 6.41/1.56 % (723269)Termination reason: Refutation not found, incomplete strategy
% 8.28/1.89 % (723269)Time elapsed: 0.002 s
% 8.28/1.89 % (723269)Peak memory usage: 89 MB
% 8.28/1.89 % (723269)Instructions burned: 1 (million)
% 8.28/1.89 % (723272)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=2479512120:i=85:gtgl=4:rtra=on:gtg=exists_sym_2996 on theBenchmark for (2996ds/85Mi)
% 8.28/1.89 % (723272)Instruction limit reached!
% 8.28/1.89 % (723272)------------------------------
% 8.28/1.89 % (723272)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.28/1.89 % (723272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.28/1.89 % (723272)CaDiCaL version: 2.1.3
% 8.28/1.89 % (723272)Termination reason: Instruction limit
% 8.28/1.89 % (723272)Termination phase: Saturation
% 8.28/1.89 % (723272)Time elapsed: 0.029 s
% 8.28/1.89 % (723272)Peak memory usage: 89 MB
% 8.28/1.89 % (723272)Instructions burned: 86 (million)
% 8.28/1.89 % (723273)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=2141787572:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi)
% 8.28/1.89 % (723273)Instruction limit reached!
% 8.28/1.89 % (723273)------------------------------
% 8.28/1.89 % (723273)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.28/1.89 % (723273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.28/1.89 % (723273)CaDiCaL version: 2.1.3
% 8.28/1.89 % (723273)Termination reason: Instruction limit
% 8.28/1.89 % (723273)Termination phase: Saturation
% 8.28/1.89 % (723273)Time elapsed: 0.003 s
% 8.28/1.89 % (723273)Peak memory usage: 88 MB
% 8.28/1.89 % (723273)Instructions burned: 2 (million)
% 8.28/1.89 % (723275)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=4024300011:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi)
% 8.28/1.89 % (723276)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=768337388:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi)
% 8.28/1.89 % (723275)Refutation not found, incomplete strategy
% 8.28/1.89 % (723275)------------------------------
% 8.28/1.89 % (723275)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.28/1.89 % (723275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.28/1.89 % (723275)CaDiCaL version: 2.1.3
% 8.28/1.89 % (723275)Termination reason: Refutation not found, incomplete strategy
% 8.28/1.89 % (723275)Time elapsed: 0.001 s
% 8.28/1.89 % (723275)Peak memory usage: 87 MB
% 8.28/1.89 % (723276)Refutation not found, incomplete strategy
% 8.28/1.89 % (723276)------------------------------
% 8.28/1.89 % (723276)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.28/1.89 % (723276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.28/1.89 % (723276)CaDiCaL version: 2.1.3
% 8.28/1.89 % (723276)Termination reason: Refutation not found, incomplete strategy
% 8.28/1.89 % (723276)Time elapsed: 0.002 s
% 8.28/1.89 % (723276)Peak memory usage: 88 MB
% 8.28/1.89 % (723276)Instructions burned: 2 (million)
% 8.28/1.89 % (723263)------------------------------
% 8.28/1.89 % (723263)------------------------------
% 8.28/1.89 % (723282)lrs+10_1_thi=all:si=on:fd=off:random_seed=279879511:i=53:rtra=on:gtg=all_2995 on theBenchmark for (2995ds/53Mi)
% 8.28/1.89 % (723280)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=4281333790:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2995 on theBenchmark for (2995ds/66Mi)
% 8.28/1.89 % (723282)Instruction limit reached!
% 8.28/1.89 % (723282)------------------------------
% 8.28/1.89 % (723282)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.28/1.89 % (723282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.28/1.89 % (723282)CaDiCaL version: 2.1.3
% 8.28/1.89 % (723282)Termination reason: Instruction limit
% 8.28/1.89 % (723282)Termination phase: Saturation
% 8.28/1.89 % (723282)Time elapsed: 0.054 s
% 8.28/1.89 % (723282)Peak memory usage: 116 MB
% 8.28/1.89 % (723282)Instructions burned: 55 (million)
% 8.28/1.89 % (723269)------------------------------
% 8.28/1.89 % (723269)------------------------------
% 8.28/1.89 % (723283)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=4157877509:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2995 on theBenchmark for (2995ds/8Mi)
% 8.28/1.89 % (723283)Refutation not found, incomplete strategy
% 8.28/1.89 % (723283)------------------------------
% 12.30/2.24 % (723283)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.30/2.24 % (723283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.30/2.24 % (723283)CaDiCaL version: 2.1.3
% 12.30/2.24 % (723283)Termination reason: Refutation not found, incomplete strategy
% 12.30/2.24 % (723283)Time elapsed: 0.004 s
% 12.30/2.24 % (723283)Peak memory usage: 88 MB
% 12.30/2.24 % (723283)Instructions burned: 2 (million)
% 12.30/2.24 % (723280)Instruction limit reached!
% 12.30/2.24 % (723280)------------------------------
% 12.30/2.24 % (723280)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.30/2.24 % (723280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.30/2.24 % (723280)CaDiCaL version: 2.1.3
% 12.30/2.24 % (723280)Termination reason: Instruction limit
% 12.30/2.24 % (723280)Termination phase: Saturation
% 12.30/2.24 % (723280)Time elapsed: 0.134 s
% 12.30/2.24 % (723280)Peak memory usage: 134 MB
% 12.30/2.24 % (723280)Instructions burned: 66 (million)
% 12.30/2.24 % (723288)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=1046834247:st=3:i=2:rtra=on:ss=axioms_2994 on theBenchmark for (2994ds/2Mi)
% 12.30/2.24 % (723288)Refutation not found, incomplete strategy
% 12.30/2.24 % (723288)------------------------------
% 12.30/2.24 % (723288)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.30/2.24 % (723288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.30/2.24 % (723288)CaDiCaL version: 2.1.3
% 12.30/2.24 % (723288)Termination reason: Refutation not found, incomplete strategy
% 12.30/2.24 % (723288)Time elapsed: 0.002 s
% 12.30/2.24 % (723288)Peak memory usage: 87 MB
% 12.30/2.24 % (723275)------------------------------
% 12.30/2.24 % (723275)------------------------------
% 12.30/2.24 % (723276)------------------------------
% 12.30/2.24 % (723276)------------------------------
% 12.30/2.24 % (723297)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=2194103884:i=2:doe=on:canc=force:asg=cautious:rtra=on_2993 on theBenchmark for (2993ds/2Mi)
% 12.30/2.24 % (723297)Instruction limit reached!
% 12.30/2.24 % (723297)------------------------------
% 12.30/2.24 % (723297)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.30/2.24 % (723297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.30/2.24 % (723297)CaDiCaL version: 2.1.3
% 12.30/2.24 % (723297)Termination reason: Instruction limit
% 12.30/2.24 % (723297)Termination phase: Saturation
% 12.30/2.24 % (723297)Time elapsed: 0.003 s
% 12.30/2.24 % (723297)Peak memory usage: 89 MB
% 12.30/2.24 % (723297)Instructions burned: 3 (million)
% 12.30/2.24 % (723301)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=649706693:i=127:doe=on:rtra=on_2992 on theBenchmark for (2992ds/127Mi)
% 12.30/2.24 % (723303)dis+10_1_si=on:random_seed=3435208687:i=10:ep=R:rtra=on_2992 on theBenchmark for (2992ds/10Mi)
% 12.30/2.24 % (723303)Instruction limit reached!
% 12.30/2.24 % (723303)------------------------------
% 12.30/2.24 % (723303)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.30/2.24 % (723303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.30/2.24 % (723303)CaDiCaL version: 2.1.3
% 12.30/2.24 % (723303)Termination reason: Instruction limit
% 12.30/2.24 % (723303)Termination phase: Saturation
% 12.30/2.24 % (723303)Time elapsed: 0.013 s
% 12.30/2.24 % (723303)Peak memory usage: 88 MB
% 12.30/2.24 % (723303)Instructions burned: 11 (million)
% 12.30/2.24 % (723318)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=4073858679:i=2:fsr=off:rtra=on:inst=on_2990 on theBenchmark for (2990ds/2Mi)
% 12.30/2.24 % (723318)Instruction limit reached!
% 12.30/2.24 % (723318)------------------------------
% 12.30/2.24 % (723318)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.30/2.24 % (723318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.30/2.24 % (723318)CaDiCaL version: 2.1.3
% 12.30/2.24 % (723318)Termination reason: Instruction limit
% 12.30/2.24 % (723318)Termination phase: Saturation
% 12.30/2.24 % (723318)Time elapsed: 0.003 s
% 12.30/2.24 % (723318)Peak memory usage: 89 MB
% 12.30/2.24 % (723318)Instructions burned: 3 (million)
% 12.30/2.24 % (723301)Instruction limit reached!
% 12.30/2.24 % (723301)------------------------------
% 12.30/2.24 % (723301)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.30/2.24 % (723301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.47/2.59 % (723301)CaDiCaL version: 2.1.3
% 13.47/2.59 % (723301)Termination reason: Instruction limit
% 13.47/2.59 % (723301)Termination phase: Saturation
% 13.47/2.59 % (723301)Time elapsed: 0.176 s
% 13.47/2.59 % (723301)Peak memory usage: 116 MB
% 13.47/2.59 % (723301)Instructions burned: 127 (million)
% 13.47/2.59 % (723283)------------------------------
% 13.47/2.59 % (723283)------------------------------
% 13.47/2.59 % (723315)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=2042462855:i=26:canc=cautious:av=off:rtra=on_2990 on theBenchmark for (2990ds/26Mi)
% 13.47/2.59 % (723315)Refutation not found, incomplete strategy
% 13.47/2.59 % (723315)------------------------------
% 13.47/2.59 % (723315)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.47/2.59 % (723315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.47/2.59 % (723315)CaDiCaL version: 2.1.3
% 13.47/2.59 % (723315)Termination reason: Refutation not found, incomplete strategy
% 13.47/2.59 % (723315)Time elapsed: 0.003 s
% 13.47/2.59 % (723315)Peak memory usage: 88 MB
% 13.47/2.59 % (723315)Instructions burned: 2 (million)
% 13.47/2.59 % (723316)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=782391431:avsq=on:i=35:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2990 on theBenchmark for (2990ds/35Mi)
% 13.47/2.59 % (723288)------------------------------
% 13.47/2.59 % (723288)------------------------------
% 13.47/2.59 % (723316)Instruction limit reached!
% 13.47/2.59 % (723316)------------------------------
% 13.47/2.59 % (723316)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.47/2.59 % (723316)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.47/2.59 % (723316)CaDiCaL version: 2.1.3
% 13.47/2.59 % (723316)Termination reason: Instruction limit
% 13.47/2.59 % (723316)Termination phase: Saturation
% 13.47/2.59 % (723316)Time elapsed: 0.041 s
% 13.47/2.59 % (723316)Peak memory usage: 89 MB
% 13.47/2.59 % (723316)Instructions burned: 36 (million)
% 13.47/2.59 % (723326)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=896392349:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2989 on theBenchmark for (2989ds/8Mi)
% 13.47/2.59 % (723329)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=3071457071:i=370:ep=RS:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/370Mi)
% 13.47/2.59 % (723326)Instruction limit reached!
% 13.47/2.59 % (723326)------------------------------
% 13.47/2.59 % (723326)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.47/2.59 % (723326)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.47/2.59 % (723326)CaDiCaL version: 2.1.3
% 13.47/2.59 % (723326)Termination reason: Instruction limit
% 13.47/2.59 % (723326)Termination phase: Saturation
% 13.47/2.59 % (723326)Time elapsed: 0.006 s
% 13.47/2.59 % (723326)Peak memory usage: 88 MB
% 13.47/2.59 % (723326)Instructions burned: 8 (million)
% 13.47/2.59 % (723333)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=3485735971:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2988 on theBenchmark for (2988ds/13Mi)
% 13.47/2.59 % (723335)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=3923223835:i=226:rtra=on:gtg=position:ss=axioms_2988 on theBenchmark for (2988ds/226Mi)
% 13.47/2.59 % (723347)lrs+1010_1_to=lpo:prlc=on:sil=128000:prc=on:drc=off:si=on:sp=const_max:thsqr=8,1:tha=some:nwc=5:random_seed=252817702:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2987 on theBenchmark for (2987ds/75Mi)
% 13.47/2.59 % (723341)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=3533880758:i=71:rtra=on:gtg=exists_top_2987 on theBenchmark for (2987ds/71Mi)
% 13.47/2.59 % (723340)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=1483088081:i=10:rtra=on_2987 on theBenchmark for (2987ds/10Mi)
% 13.47/2.59 % (723333)Instruction limit reached!
% 13.47/2.59 % (723333)------------------------------
% 13.47/2.59 % (723333)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.47/2.59 % (723333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.47/2.59 % (723333)CaDiCaL version: 2.1.3
% 13.47/2.59 % (723333)Termination reason: Instruction limit
% 13.47/2.59 % (723333)Termination phase: Saturation
% 13.47/2.59 % (723333)Time elapsed: 0.046 s
% 13.47/2.59 % (723333)Peak memory usage: 116 MB
% 13.47/2.59 % (723333)Instructions burned: 14 (million)
% 14.19/2.97 % (723335)Refutation not found, incomplete strategy
% 14.19/2.97 % (723335)------------------------------
% 14.19/2.97 % (723335)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.19/2.97 % (723335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.19/2.97 % (723335)CaDiCaL version: 2.1.3
% 14.19/2.97 % (723335)Termination reason: Refutation not found, incomplete strategy
% 14.19/2.97 % (723335)Time elapsed: 0.037 s
% 14.19/2.97 % (723335)Peak memory usage: 111 MB
% 14.19/2.97 % (723335)Instructions burned: 5 (million)
% 14.19/2.97 % (723340)Instruction limit reached!
% 14.19/2.97 % (723340)------------------------------
% 14.19/2.97 % (723340)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.19/2.97 % (723340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.19/2.97 % (723340)CaDiCaL version: 2.1.3
% 14.19/2.97 % (723340)Termination reason: Instruction limit
% 14.19/2.97 % (723340)Termination phase: Saturation
% 14.19/2.97 % (723340)Time elapsed: 0.014 s
% 14.19/2.97 % (723340)Peak memory usage: 88 MB
% 14.19/2.97 % (723340)Instructions burned: 10 (million)
% 14.19/2.97 % (723347)Instruction limit reached!
% 14.19/2.97 % (723347)------------------------------
% 14.19/2.97 % (723347)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.19/2.97 % (723347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.19/2.97 % (723347)CaDiCaL version: 2.1.3
% 14.19/2.97 % (723347)Termination reason: Instruction limit
% 14.19/2.97 % (723347)Termination phase: Saturation
% 14.19/2.97 % (723347)Time elapsed: 0.047 s
% 14.19/2.97 % (723347)Peak memory usage: 90 MB
% 14.19/2.97 % (723347)Instructions burned: 76 (million)
% 14.19/2.97 % (723315)------------------------------
% 14.19/2.97 % (723315)------------------------------
% 14.19/2.97 % (723341)Instruction limit reached!
% 14.19/2.97 % (723341)------------------------------
% 14.19/2.97 % (723341)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.19/2.97 % (723341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.19/2.97 % (723341)CaDiCaL version: 2.1.3
% 14.19/2.97 % (723341)Termination reason: Instruction limit
% 14.19/2.97 % (723341)Termination phase: Saturation
% 14.19/2.97 % (723341)Time elapsed: 0.098 s
% 14.19/2.97 % (723341)Peak memory usage: 133 MB
% 14.19/2.97 % (723341)Instructions burned: 71 (million)
% 14.19/2.97 % (723329)Instruction limit reached!
% 14.19/2.97 % (723329)------------------------------
% 14.19/2.97 % (723329)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.19/2.97 % (723329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.19/2.97 % (723329)CaDiCaL version: 2.1.3
% 14.19/2.97 % (723329)Termination reason: Instruction limit
% 14.19/2.97 % (723329)Termination phase: Saturation
% 14.19/2.97 % (723329)Time elapsed: 0.299 s
% 14.19/2.97 % (723329)Peak memory usage: 91 MB
% 14.19/2.97 % (723329)Instructions burned: 370 (million)
% 14.19/2.97 % (723363)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=3461292533:i=131:rtra=on_2985 on theBenchmark for (2985ds/131Mi)
% 14.19/2.97 % (723360)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=3805416313:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2985 on theBenchmark for (2985ds/294Mi)
% 14.19/2.97 % (723361)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=2194972121:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2985 on theBenchmark for (2985ds/130Mi)
% 14.19/2.97 % (723366)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=3896635999:i=307:rtra=on:gtg=exists_top_2984 on theBenchmark for (2984ds/307Mi)
% 14.19/2.97 % (723366)Refutation not found, incomplete strategy
% 14.19/2.97 % (723366)------------------------------
% 14.19/2.97 % (723366)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.19/2.97 % (723366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.19/2.97 % (723366)CaDiCaL version: 2.1.3
% 14.19/2.97 % (723366)Termination reason: Refutation not found, incomplete strategy
% 14.19/2.97 % (723366)Time elapsed: 0.003 s
% 14.19/2.97 % (723366)Peak memory usage: 89 MB
% 14.19/2.97 % (723366)Instructions burned: 2 (million)
% 14.19/2.97 % (723365)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=2726235097:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2984 on theBenchmark for (2984ds/40Mi)
% 14.19/2.97 % (723363)Instruction limit reached!
% 14.19/2.97 % (723363)------------------------------
% 14.19/2.97 % (723363)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.19/2.97 % (723363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.19/2.97 % (723363)CaDiCaL version: 2.1.3
% 14.19/2.97 % (723363)Termination reason: Instruction limit
% 14.19/2.97 % (723363)Termination phase: Saturation
% 14.19/2.97 % (723363)Time elapsed: 0.103 s
% 14.19/2.97 % (723363)Peak memory usage: 133 MB
% 14.19/2.97 % (723363)Instructions burned: 132 (million)
% 14.19/2.97 % (723365)Instruction limit reached!
% 14.19/2.97 % (723365)------------------------------
% 14.19/2.97 % (723365)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.19/2.97 % (723365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.19/2.97 % (723365)CaDiCaL version: 2.1.3
% 14.19/2.97 % (723365)Termination reason: Instruction limit
% 14.19/2.97 % (723365)Termination phase: Saturation
% 14.19/2.97 % (723365)Time elapsed: 0.088 s
% 14.19/2.97 % (723365)Peak memory usage: 133 MB
% 14.19/2.97 % (723365)Instructions burned: 41 (million)
% 14.19/2.97 % (723335)------------------------------
% 14.19/2.97 % (723335)------------------------------
% 14.19/2.97 % (723367)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=2072898388:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2984 on theBenchmark for (2984ds/598Mi)
% 14.19/2.97 % (723361)Instruction limit reached!
% 14.19/2.97 % (723361)------------------------------
% 14.19/2.97 % (723361)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.19/2.97 % (723361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.19/2.97 % (723361)CaDiCaL version: 2.1.3
% 14.19/2.97 % (723361)Termination reason: Instruction limit
% 14.19/2.97 % (723361)Termination phase: Saturation
% 14.19/2.97 % (723361)Time elapsed: 0.158 s
% 14.19/2.97 % (723361)Peak memory usage: 116 MB
% 14.19/2.97 % (723361)Instructions burned: 130 (million)
% 14.19/2.97 % (723382)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=1893538378:i=131:canc=cautious:fsr=off:rtra=on_2981 on theBenchmark for (2981ds/131Mi)
% 14.19/2.97 % (723360)Instruction limit reached!
% 14.19/2.97 % (723360)------------------------------
% 14.19/2.97 % (723360)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.19/2.97 % (723360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.19/2.97 % (723360)CaDiCaL version: 2.1.3
% 14.19/2.97 % (723360)Termination reason: Instruction limit
% 14.19/2.97 % (723360)Termination phase: Saturation
% 14.19/2.97 % (723360)Time elapsed: 0.274 s
% 14.19/2.97 % (723360)Peak memory usage: 90 MB
% 14.19/2.97 % (723360)Instructions burned: 295 (million)
% 14.19/2.97 % (723382)Instruction limit reached!
% 14.19/2.97 % (723382)------------------------------
% 14.19/2.97 % (723382)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.19/2.97 % (723382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.19/2.97 % (723382)CaDiCaL version: 2.1.3
% 14.19/2.97 % (723382)Termination reason: Instruction limit
% 14.19/2.97 % (723382)Termination phase: Saturation
% 14.19/2.97 % (723382)Time elapsed: 0.072 s
% 14.19/2.97 % (723382)Peak memory usage: 117 MB
% 14.19/2.97 % (723382)Instructions burned: 134 (million)
% 14.19/2.97 % (723366)------------------------------
% 14.19/2.97 % (723366)------------------------------
% 14.19/2.97 % (723388)dis+11_1_to=lpo:pum=on:sas=z3:si=on:sp=reverse_arity:sos=theory:thsqr=2,1:tha=some:s2agt=20:random_seed=2778740640:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2981 on theBenchmark for (2981ds/259Mi)
% 14.19/2.97 % (723367)First to succeed.
% 14.19/2.97 % (723367)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-723177"
% 14.19/2.97 % (723390)dis+10_1_si=on:random_seed=4142321184:s2a=on:i=1000:rtra=on:gtg=exists_all_2981 on theBenchmark for (2981ds/1000Mi)
% 14.19/2.97 % (723388)Refutation not found, incomplete strategy
% 14.19/2.97 % (723388)------------------------------
% 14.19/2.97 % (723388)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.19/2.97 % (723388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.19/2.97 % (723388)CaDiCaL version: 2.1.3
% 14.19/2.97 % (723388)Termination reason: Refutation not found, incomplete strategy
% 14.19/2.97 % (723388)Time elapsed: 0.039 s
% 14.19/2.97 % (723388)Peak memory usage: 111 MB
% 14.19/2.97 % (723388)Instructions burned: 5 (million)
% 14.19/2.97 % (723391)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=162290814:i=383:fsr=off:rtra=on:ev=force_2981 on theBenchmark for (2981ds/383Mi)
% 14.19/2.97 % (723400)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=2747740338:i=65:nm=16:rtra=on_2979 on theBenchmark for (2979ds/65Mi)
% 14.19/2.97 % (723400)Refutation not found, incomplete strategy
% 14.19/2.97 % (723400)------------------------------
% 14.19/2.97 % (723400)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.19/2.97 % (723400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.19/2.97 % (723400)CaDiCaL version: 2.1.3
% 14.19/2.97 % (723400)Termination reason: Refutation not found, incomplete strategy
% 14.19/2.97 % (723400)Time elapsed: 0.017 s
% 14.19/2.97 % (723400)Peak memory usage: 112 MB
% 14.19/2.97 % (723400)Instructions burned: 6 (million)
% 14.19/2.97 % (723398)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=290766710:i=141:doe=on:rtra=on_2980 on theBenchmark for (2980ds/141Mi)
% 14.19/2.97 % (723400)------------------------------
% 14.19/2.97 % (723400)------------------------------
% 14.19/2.97 % (723398)Instruction limit reached!
% 14.19/2.97 % (723398)------------------------------
% 14.19/2.97 % (723398)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.19/2.97 % (723398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.19/2.97 % (723398)CaDiCaL version: 2.1.3
% 14.19/2.97 % (723398)Termination reason: Instruction limit
% 14.19/2.97 % (723398)Termination phase: Saturation
% 14.19/2.97 % (723398)Time elapsed: 0.136 s
% 14.19/2.97 % (723398)Peak memory usage: 90 MB
% 14.19/2.97 % (723398)Instructions burned: 143 (million)
% 14.19/2.97 % (723405)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=19397323:i=121:nm=16:rtra=on_2979 on theBenchmark for (2979ds/121Mi)
% 14.19/2.97 % (723405)Also succeeded, but the first one will report.
% 14.19/2.97 % (723391)Instruction limit reached!
% 14.19/2.97 % (723391)------------------------------
% 14.19/2.97 % (723391)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.19/2.97 % (723391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.19/2.97 % (723391)CaDiCaL version: 2.1.3
% 14.19/2.97 % (723391)Termination reason: Instruction limit
% 14.19/2.97 % (723391)Termination phase: Saturation
% 14.19/2.97 % (723391)Time elapsed: 0.357 s
% 14.19/2.97 % (723391)Peak memory usage: 92 MB
% 14.19/2.97 % (723391)Instructions burned: 383 (million)
% 14.19/2.97 % (723367)Refutation found. Thanks to Tanya!
% 14.19/2.97 % SZS status Unsatisfiable for theBenchmark
% 14.19/2.97 % SZS output start Proof for theBenchmark
% See solution above
% 18.14/3.22 % (723367)------------------------------
% 18.14/3.22 % (723367)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.14/3.22 % (723367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.14/3.22 % (723367)CaDiCaL version: 2.1.3
% 18.14/3.22 % (723367)Termination reason: Refutation
% 18.14/3.22 % (723367)Time elapsed: 0.261 s
% 18.14/3.22 % (723367)Peak memory usage: 135 MB
% 18.14/3.22 % (723367)Instructions burned: 180 (million)
% 18.14/3.22 % (723367)------------------------------
% 18.14/3.22 % (723367)------------------------------
% 18.14/3.22 % (723177)Success in time 2.525 s
% 18.14/3.22 % Vampire exiting
%------------------------------------------------------------------------------