%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : DAT018_1 : TPTP v9.3.1. Released v5.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n018.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:06 AM UTC 2026
% Result : Theorem 2.94s 1.14s
% Output : Refutation 3.92s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 30
% Syntax : Number of formulae : 97 ( 28 unt; 0 typ; 27 def)
% Number of atoms : 228 ( 65 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 207 ( 76 ~; 79 |; 28 &)
% ( 20 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number arithmetic : 367 ( 72 atm; 93 fun; 157 num; 45 var)
% Number of types : 2 ( 1 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 24 ( 20 usr; 21 prp; 0-2 aty)
% Number of functors : 18 ( 13 usr; 15 con; 0-3 aty)
% Number of variables : 67 ( 51 !; 16 ?; 67 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
array: $tType ).
tff(func_def_0,type,
read: ( array * $int ) > $int ).
tff(func_def_1,type,
write: ( array * $int * $int ) > array ).
tff(func_def_7,type,
sK0: array ).
tff(func_def_8,type,
sK1: array ).
tff(func_def_9,type,
sK2: $int ).
tff(func_def_10,type,
sK3: $int ).
tff(func_def_11,type,
sF4: $int ).
tff(func_def_12,type,
sF5: array ).
tff(func_def_13,type,
sF6: $int ).
tff(func_def_14,type,
sF7: array ).
tff(func_def_15,type,
sF8: $int ).
tff(func_def_16,type,
sF9: array ).
tff(func_def_17,type,
sF10: $int ).
tff(f1,axiom,
! [X2: $int,X1: $int,X0: array] : ( read(write(X0,X1,X2),X1) = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1) ).
tff(f2,axiom,
! [X1: $int,X3: $int,X0: array,X2: $int] :
( ( read(write(X0,X1,X3),X2) = read(X0,X2) )
| ( X1 = X2 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax2) ).
tff(f3,conjecture,
! [X1: array,X2: $int,X3: $int,X0: array] :
( ( $lesseq(X3,$sum(X2,3))
& $lesseq(X2,X3)
& ( X0 = write(write(write(X1,X2,3),$sum(X2,2),2),$sum(X2,4),1) ) )
=> ? [X4: $int] :
( $lesseq(X3,X4)
& $lesseq(read(X0,X4),3)
& $lesseq(X4,$sum(X3,3)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1) ).
tff(f4,negated_conjecture,
~ ! [X1: array,X2: $int,X3: $int,X0: array] :
( ( $lesseq(X3,$sum(X2,3))
& $lesseq(X2,X3)
& ( X0 = write(write(write(X1,X2,3),$sum(X2,2),2),$sum(X2,4),1) ) )
=> ? [X4: $int] :
( $lesseq(X3,X4)
& $lesseq(read(X0,X4),3)
& $lesseq(X4,$sum(X3,3)) ) ),
inference(negated_conjecture,[status(cth)],[f3]) ).
tff(f5,plain,
~ ! [X1: array,X2: $int,X3: $int,X0: array] :
( ( ~ $less($sum(X2,3),X3)
& ~ $less(X3,X2)
& ( X0 = write(write(write(X1,X2,3),$sum(X2,2),2),$sum(X2,4),1) ) )
=> ? [X4: $int] :
( ~ $less(X4,X3)
& ~ $less(3,read(X0,X4))
& ~ $less($sum(X3,3),X4) ) ),
inference(theory_normalization,[],[f4]) ).
tff(f6,plain,
! [X1: $int,X0: $int,X2: array] : ( read(write(X2,X1,X0),X1) = X0 ),
inference(rectify,[],[f1]) ).
tff(f7,plain,
~ ! [X2: $int,X1: $int,X0: array,X3: array] :
( ( ~ $less($sum(X1,3),X2)
& ~ $less(X2,X1)
& ( write(write(write(X0,X1,3),$sum(X1,2),2),$sum(X1,4),1) = X3 ) )
=> ? [X4: $int] :
( ~ $less(X4,X2)
& ~ $less(3,read(X3,X4))
& ~ $less($sum(X2,3),X4) ) ),
inference(rectify,[],[f5]) ).
tff(f8,plain,
! [X3: $int,X2: array,X1: $int,X0: $int] :
( ( X0 = X3 )
| ( read(write(X2,X0,X1),X3) = read(X2,X3) ) ),
inference(rectify,[],[f2]) ).
tff(f9,plain,
? [X2: $int,X1: $int,X0: array,X3: array] :
( ! [X4: $int] :
( $less($sum(X2,3),X4)
| $less(X4,X2)
| $less(3,read(X3,X4)) )
& ~ $less($sum(X1,3),X2)
& ~ $less(X2,X1)
& ( write(write(write(X0,X1,3),$sum(X1,2),2),$sum(X1,4),1) = X3 ) ),
inference(ennf_transformation,[],[f7]) ).
tff(f10,plain,
? [X0: array,X3: array,X1: $int,X2: $int] :
( ! [X4: $int] :
( $less($sum(X2,3),X4)
| $less(X4,X2)
| $less(3,read(X3,X4)) )
& ( write(write(write(X0,X1,3),$sum(X1,2),2),$sum(X1,4),1) = X3 )
& ~ $less($sum(X1,3),X2)
& ~ $less(X2,X1) ),
inference(flattening,[],[f9]) ).
tff(f11,plain,
! [X0: $int,X1: $int,X2: array] : ( read(write(X2,X0,X1),X0) = X1 ),
inference(rectify,[],[f6]) ).
tff(f12,plain,
? [X0: array,X1: array,X2: $int,X3: $int] :
( ! [X4: $int] :
( $less($sum(X3,3),X4)
| $less(X4,X3)
| $less(3,read(X1,X4)) )
& ( write(write(write(X0,X2,3),$sum(X2,2),2),$sum(X2,4),1) = X1 )
& ~ $less($sum(X2,3),X3)
& ~ $less(X3,X2) ),
inference(rectify,[],[f10]) ).
tff(f13,plain,
( ! [X4: $int] :
( $less($sum(sK3,3),X4)
| $less(X4,sK3)
| $less(3,read(sK1,X4)) )
& ( sK1 = write(write(write(sK0,sK2,3),$sum(sK2,2),2),$sum(sK2,4),1) )
& ~ $less($sum(sK2,3),sK3)
& ~ $less(sK3,sK2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2,sK3]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2),skolemize(X3,sK3)],[f12]) ).
tff(f14,plain,
! [X0: $int,X1: array,X2: $int,X3: $int] :
( ( X0 = X3 )
| ( read(X1,X0) = read(write(X1,X3,X2),X0) ) ),
inference(rectify,[],[f8]) ).
tff(f15,plain,
! [X2: array,X0: $int,X1: $int] : ( read(write(X2,X0,X1),X0) = X1 ),
inference(cnf_transformation,[],[f11]) ).
tff(f16,plain,
~ $less(sK3,sK2),
inference(cnf_transformation,[],[f13]) ).
tff(f17,plain,
~ $less($sum(sK2,3),sK3),
inference(cnf_transformation,[],[f13]) ).
tff(f18,plain,
sK1 = write(write(write(sK0,sK2,3),$sum(sK2,2),2),$sum(sK2,4),1),
inference(cnf_transformation,[],[f13]) ).
tff(f19,plain,
! [X4: $int] :
( $less($sum(sK3,3),X4)
| $less(X4,sK3)
| $less(3,read(sK1,X4)) ),
inference(cnf_transformation,[],[f13]) ).
tff(f20,plain,
! [X2: $int,X3: $int,X0: $int,X1: array] :
( ( read(X1,X0) = read(write(X1,X3,X2),X0) )
| ( X0 = X3 ) ),
inference(cnf_transformation,[],[f14]) ).
tff(f21,definition,
sF4 = $sum(sK3,3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
tff(f22,plain,
! [X4: $int] :
( $less(3,read(sK1,X4))
| $less(X4,sK3)
| $less(sF4,X4) ),
inference(definition_folding,[],[f19,f21]) ).
tff(f23,definition,
sF5 = write(sK0,sK2,3),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
tff(f24,definition,
sF6 = $sum(sK2,2),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
tff(f25,definition,
sF7 = write(sF5,sF6,2),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
tff(f26,definition,
sF8 = $sum(sK2,4),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
tff(f27,plain,
$sum(sK2,4) = sF8,
inference(reorient_equations,[],[f26]) ).
tff(f28,definition,
sF9 = write(sF7,sF8,1),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
tff(f29,plain,
sF9 = sK1,
inference(definition_folding,[],[f18,f28,f27,f25,f24,f23]) ).
tff(f30,definition,
sF10 = $sum(sK2,3),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
tff(f31,plain,
$sum(sK2,3) = sF10,
inference(reorient_equations,[],[f30]) ).
tff(f32,plain,
~ $less(sF10,sK3),
inference(definition_folding,[],[f17,f31]) ).
tff(f34,definition,
( spl11_1
<=> $less(sK3,sK2) ),
introduced(definition,[new_symbols(definition,[spl11_1])],[avatar_definition]) ).
tff(f37,plain,
~ spl11_1,
inference(avatar_split_clause,[],[f16,f34]) ).
tff(f39,definition,
( spl11_2
<=> ( sF4 = $sum(sK3,3) ) ),
introduced(definition,[new_symbols(definition,[spl11_2])],[avatar_definition]) ).
tff(f41,plain,
( ( sF4 = $sum(sK3,3) )
| ~ spl11_2 ),
inference(avatar_component_clause,[],[f39]) ).
tff(f42,plain,
spl11_2,
inference(avatar_split_clause,[],[f21,f39]) ).
tff(f44,definition,
( spl11_3
<=> ( sF6 = $sum(sK2,2) ) ),
introduced(definition,[new_symbols(definition,[spl11_3])],[avatar_definition]) ).
tff(f46,plain,
( ( sF6 = $sum(sK2,2) )
| ~ spl11_3 ),
inference(avatar_component_clause,[],[f44]) ).
tff(f47,plain,
spl11_3,
inference(avatar_split_clause,[],[f24,f44]) ).
tff(f49,definition,
( spl11_4
<=> ( sF9 = sK1 ) ),
introduced(definition,[new_symbols(definition,[spl11_4])],[avatar_definition]) ).
tff(f51,plain,
( ( sF9 = sK1 )
| ~ spl11_4 ),
inference(avatar_component_clause,[],[f49]) ).
tff(f52,plain,
spl11_4,
inference(avatar_split_clause,[],[f29,f49]) ).
tff(f54,definition,
( spl11_5
<=> ( $sum(sK2,3) = sF10 ) ),
introduced(definition,[new_symbols(definition,[spl11_5])],[avatar_definition]) ).
tff(f56,plain,
( ( $sum(sK2,3) = sF10 )
| ~ spl11_5 ),
inference(avatar_component_clause,[],[f54]) ).
tff(f57,plain,
spl11_5,
inference(avatar_split_clause,[],[f31,f54]) ).
tff(f59,definition,
( spl11_6
<=> ( $sum(sK2,4) = sF8 ) ),
introduced(definition,[new_symbols(definition,[spl11_6])],[avatar_definition]) ).
tff(f61,plain,
( ( $sum(sK2,4) = sF8 )
| ~ spl11_6 ),
inference(avatar_component_clause,[],[f59]) ).
tff(f62,plain,
spl11_6,
inference(avatar_split_clause,[],[f27,f59]) ).
tff(f64,definition,
( spl11_7
<=> $less(sF10,sK3) ),
introduced(definition,[new_symbols(definition,[spl11_7])],[avatar_definition]) ).
tff(f66,plain,
( ~ $less(sF10,sK3)
| spl11_7 ),
inference(avatar_component_clause,[],[f64]) ).
tff(f67,plain,
~ spl11_7,
inference(avatar_split_clause,[],[f32,f64]) ).
tff(f69,definition,
( spl11_8
<=> ( sF9 = write(sF7,sF8,1) ) ),
introduced(definition,[new_symbols(definition,[spl11_8])],[avatar_definition]) ).
tff(f71,plain,
( ( sF9 = write(sF7,sF8,1) )
| ~ spl11_8 ),
inference(avatar_component_clause,[],[f69]) ).
tff(f72,plain,
spl11_8,
inference(avatar_split_clause,[],[f28,f69]) ).
tff(f79,definition,
( spl11_10
<=> ( sF7 = write(sF5,sF6,2) ) ),
introduced(definition,[new_symbols(definition,[spl11_10])],[avatar_definition]) ).
tff(f81,plain,
( ( sF7 = write(sF5,sF6,2) )
| ~ spl11_10 ),
inference(avatar_component_clause,[],[f79]) ).
tff(f82,plain,
spl11_10,
inference(avatar_split_clause,[],[f25,f79]) ).
tff(f83,plain,
( ~ $less($sum(sK2,3),sK3)
| ~ spl11_5
| spl11_7 ),
inference(superposition,[],[f66,f56]) ).
tff(f85,definition,
( spl11_11
<=> $less($sum(sK2,3),sK3) ),
introduced(definition,[new_symbols(definition,[spl11_11])],[avatar_definition]) ).
tff(f88,plain,
( ~ spl11_11
| ~ spl11_5
| spl11_7 ),
inference(avatar_split_clause,[],[f83,f64,f54,f85]) ).
tff(f89,plain,
( ( write(sF7,$sum(sK2,4),1) = sF9 )
| ~ spl11_6
| ~ spl11_8 ),
inference(forward_demodulation,[],[f71,f61]) ).
tff(f90,plain,
( ( write(sF7,$sum(sK2,4),1) = sK1 )
| ~ spl11_4
| ~ spl11_6
| ~ spl11_8 ),
inference(forward_demodulation,[],[f89,f51]) ).
tff(f92,definition,
( spl11_12
<=> ( write(sF7,$sum(sK2,4),1) = sK1 ) ),
introduced(definition,[new_symbols(definition,[spl11_12])],[avatar_definition]) ).
tff(f94,plain,
( ( write(sF7,$sum(sK2,4),1) = sK1 )
| ~ spl11_12 ),
inference(avatar_component_clause,[],[f92]) ).
tff(f95,plain,
( spl11_12
| ~ spl11_4
| ~ spl11_6
| ~ spl11_8 ),
inference(avatar_split_clause,[],[f90,f69,f59,f49,f92]) ).
tff(f96,plain,
( ( sF7 = write(sF5,$sum(sK2,2),2) )
| ~ spl11_3
| ~ spl11_10 ),
inference(forward_demodulation,[],[f81,f46]) ).
tff(f98,definition,
( spl11_13
<=> ( sF7 = write(sF5,$sum(sK2,2),2) ) ),
introduced(definition,[new_symbols(definition,[spl11_13])],[avatar_definition]) ).
tff(f100,plain,
( ( sF7 = write(sF5,$sum(sK2,2),2) )
| ~ spl11_13 ),
inference(avatar_component_clause,[],[f98]) ).
tff(f101,plain,
( spl11_13
| ~ spl11_3
| ~ spl11_10 ),
inference(avatar_split_clause,[],[f96,f79,f44,f98]) ).
tff(f102,plain,
( ( 1 = read(sK1,$sum(sK2,4)) )
| ~ spl11_12 ),
inference(superposition,[],[f15,f94]) ).
tff(f110,definition,
( spl11_15
<=> ( 1 = read(sK1,$sum(sK2,4)) ) ),
introduced(definition,[new_symbols(definition,[spl11_15])],[avatar_definition]) ).
tff(f112,plain,
( ( 1 = read(sK1,$sum(sK2,4)) )
| ~ spl11_15 ),
inference(avatar_component_clause,[],[f110]) ).
tff(f113,plain,
( spl11_15
| ~ spl11_12 ),
inference(avatar_split_clause,[],[f102,f92,f110]) ).
tff(f114,plain,
( $less(3,1)
| $less($sum(sK2,4),sK3)
| $less(sF4,$sum(sK2,4))
| ~ spl11_15 ),
inference(superposition,[],[f22,f112]) ).
tff(f115,plain,
( $less($sum(sK2,4),sK3)
| $less(sF4,$sum(sK2,4))
| ~ spl11_15 ),
inference(evaluation,[],[f114]) ).
tff(f116,plain,
( $less($sum(sK2,4),sK3)
| $less($sum(sK3,3),$sum(sK2,4))
| ~ spl11_2
| ~ spl11_15 ),
inference(forward_demodulation,[],[f115,f41]) ).
tff(f118,definition,
( spl11_16
<=> $less($sum(sK3,3),$sum(sK2,4)) ),
introduced(definition,[new_symbols(definition,[spl11_16])],[avatar_definition]) ).
tff(f122,definition,
( spl11_17
<=> $less($sum(sK2,4),sK3) ),
introduced(definition,[new_symbols(definition,[spl11_17])],[avatar_definition]) ).
tff(f125,plain,
( spl11_16
| spl11_17
| ~ spl11_2
| ~ spl11_15 ),
inference(avatar_split_clause,[],[f116,f110,f39,f122,f118]) ).
tff(f126,plain,
( ( 2 = read(sF7,$sum(sK2,2)) )
| ~ spl11_13 ),
inference(superposition,[],[f15,f100]) ).
tff(f128,definition,
( spl11_18
<=> ( 2 = read(sF7,$sum(sK2,2)) ) ),
introduced(definition,[new_symbols(definition,[spl11_18])],[avatar_definition]) ).
tff(f130,plain,
( ( 2 = read(sF7,$sum(sK2,2)) )
| ~ spl11_18 ),
inference(avatar_component_clause,[],[f128]) ).
tff(f131,plain,
( spl11_18
| ~ spl11_13 ),
inference(avatar_split_clause,[],[f126,f98,f128]) ).
tff(f132,plain,
( ! [X0: $int] :
( ( read(sK1,X0) = read(sF7,X0) )
| ( $sum(sK2,4) = X0 ) )
| ~ spl11_12 ),
inference(superposition,[],[f20,f94]) ).
tff(f136,plain,
( ( 2 = read(sK1,$sum(sK2,2)) )
| ( $sum(sK2,4) = $sum(sK2,2) )
| ~ spl11_12
| ~ spl11_18 ),
inference(superposition,[],[f132,f130]) ).
tff(f138,definition,
( spl11_19
<=> ( 2 = read(sK1,$sum(sK2,2)) ) ),
introduced(definition,[new_symbols(definition,[spl11_19])],[avatar_definition]) ).
tff(f140,plain,
( ( 2 = read(sK1,$sum(sK2,2)) )
| ~ spl11_19 ),
inference(avatar_component_clause,[],[f138]) ).
tff(f142,definition,
( spl11_20
<=> ( $sum(sK2,4) = $sum(sK2,2) ) ),
introduced(definition,[new_symbols(definition,[spl11_20])],[avatar_definition]) ).
tff(f146,plain,
( spl11_20
| spl11_19
| ~ spl11_12
| ~ spl11_18 ),
inference(avatar_split_clause,[],[f136,f128,f92,f138,f142]) ).
tff(f147,plain,
( $less(3,2)
| $less($sum(sK2,2),sK3)
| $less(sF4,$sum(sK2,2))
| ~ spl11_19 ),
inference(superposition,[],[f22,f140]) ).
tff(f148,plain,
( $less(sF4,$sum(sK2,2))
| $less($sum(sK2,2),sK3)
| ~ spl11_19 ),
inference(evaluation,[],[f147]) ).
tff(f149,plain,
( $less($sum(sK2,2),sK3)
| $less($sum(sK3,3),$sum(sK2,2))
| ~ spl11_2
| ~ spl11_19 ),
inference(forward_demodulation,[],[f148,f41]) ).
tff(f151,definition,
( spl11_21
<=> $less($sum(sK3,3),$sum(sK2,2)) ),
introduced(definition,[new_symbols(definition,[spl11_21])],[avatar_definition]) ).
tff(f155,definition,
( spl11_22
<=> $less($sum(sK2,2),sK3) ),
introduced(definition,[new_symbols(definition,[spl11_22])],[avatar_definition]) ).
tff(f158,plain,
( spl11_21
| spl11_22
| ~ spl11_2
| ~ spl11_19 ),
inference(avatar_split_clause,[],[f149,f138,f39,f155,f151]) ).
tff(f159,plain,
$false,
inference(avatar_smt_refutation,[],[f158,f146,f131,f125,f113,f101,f95,f88,f82,f72,f67,f62,f57,f52,f47,f42,f37]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : DAT018_1 : TPTP v9.3.1. Released v5.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.19 % Computer : n018.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Tue Sep 29 00:07:55 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.23 Running first-order theorem proving
% 0.08/0.23 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.94/1.14 % (3909686)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 2.94/1.14 % (3909693)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=3411233418:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 2.94/1.14 % (3909692)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2650214702:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 2.94/1.14 % (3909691)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=3035176312:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 2.94/1.14 % (3909694)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=753789217:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 2.94/1.14 % (3909695)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=798029946:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 2.94/1.14 % (3909697)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=2676462925:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 2.94/1.14 % (3909696)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=2082259760:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 2.94/1.14 % (3909695)Instruction limit reached!
% 2.94/1.14 % (3909695)------------------------------
% 2.94/1.14 % (3909695)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.94/1.14 % (3909695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.94/1.14 % (3909695)CaDiCaL version: 2.1.3
% 2.94/1.14 % (3909695)Termination reason: Instruction limit
% 2.94/1.14 % (3909695)Termination phase: Saturation
% 2.94/1.14 % (3909695)Time elapsed: 0.004 s
% 2.94/1.14 % (3909695)Peak memory usage: 88 MB
% 2.94/1.14 % (3909695)Instructions burned: 4 (million)
% 2.94/1.14 % (3909694)Instruction limit reached!
% 2.94/1.14 % (3909694)------------------------------
% 2.94/1.14 % (3909694)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.94/1.14 % (3909694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.94/1.14 % (3909694)CaDiCaL version: 2.1.3
% 2.94/1.14 % (3909694)Termination reason: Instruction limit
% 2.94/1.14 % (3909694)Termination phase: Saturation
% 2.94/1.14 % (3909694)Time elapsed: 0.006 s
% 2.94/1.14 % (3909694)Peak memory usage: 88 MB
% 2.94/1.14 % (3909694)Instructions burned: 8 (million)
% 2.94/1.14 % (3909691)Instruction limit reached!
% 2.94/1.14 % (3909691)------------------------------
% 2.94/1.14 % (3909691)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.94/1.14 % (3909691)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.94/1.14 % (3909691)CaDiCaL version: 2.1.3
% 2.94/1.14 % (3909691)Termination reason: Instruction limit
% 2.94/1.14 % (3909691)Termination phase: Saturation
% 2.94/1.14 % (3909691)Time elapsed: 0.032 s
% 2.94/1.14 % (3909691)Peak memory usage: 115 MB
% 2.94/1.14 % (3909691)Instructions burned: 12 (million)
% 2.94/1.14 % (3909696)Refutation not found, incomplete strategy
% 2.94/1.14 % (3909696)------------------------------
% 2.94/1.14 % (3909696)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.94/1.14 % (3909696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.94/1.14 % (3909696)CaDiCaL version: 2.1.3
% 2.94/1.14 % (3909696)Termination reason: Refutation not found, incomplete strategy
% 2.94/1.14 % (3909696)Time elapsed: 0.033 s
% 2.94/1.14 % (3909696)Peak memory usage: 115 MB
% 2.94/1.14 % (3909696)Instructions burned: 12 (million)
% 2.94/1.14 % (3909692)First to succeed.
% 2.94/1.14 % (3909692)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3909686"
% 2.94/1.14 % (3909693)Instruction limit reached!
% 2.94/1.14 % (3909693)------------------------------
% 2.94/1.14 % (3909693)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.94/1.14 % (3909693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.94/1.14 % (3909693)CaDiCaL version: 2.1.3
% 2.94/1.14 % (3909693)Termination reason: Instruction limit
% 2.94/1.14 % (3909693)Termination phase: Saturation
% 2.94/1.14 % (3909693)Time elapsed: 0.096 s
% 2.94/1.14 % (3909693)Peak memory usage: 117 MB
% 2.94/1.14 % (3909693)Instructions burned: 203 (million)
% 2.94/1.14 % (3909697)Instruction limit reached!
% 2.94/1.14 % (3909697)------------------------------
% 2.94/1.14 % (3909697)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.94/1.14 % (3909697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.94/1.14 % (3909697)CaDiCaL version: 2.1.3
% 2.94/1.14 % (3909697)Termination reason: Instruction limit
% 2.94/1.14 % (3909697)Termination phase: Saturation
% 2.94/1.14 % (3909697)Time elapsed: 0.047 s
% 2.94/1.14 % (3909697)Peak memory usage: 116 MB
% 2.94/1.14 % (3909697)Instructions burned: 33 (million)
% 2.94/1.14 % (3909708)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=3826150744:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 2.94/1.14 % (3909705)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=3269280012:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 2.94/1.14 % (3909707)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1026720836:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi)
% 2.94/1.14 % (3909706)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=1891179771:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi)
% 2.94/1.14 % (3909705)Refutation not found, incomplete strategy
% 2.94/1.14 % (3909705)------------------------------
% 2.94/1.14 % (3909705)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.94/1.14 % (3909705)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.94/1.14 % (3909705)CaDiCaL version: 2.1.3
% 2.94/1.14 % (3909705)Termination reason: Refutation not found, incomplete strategy
% 2.94/1.14 % (3909705)Time elapsed: 0.004 s
% 2.94/1.14 % (3909705)Peak memory usage: 89 MB
% 2.94/1.14 % (3909705)Instructions burned: 4 (million)
% 2.94/1.14 % (3909708)Instruction limit reached!
% 2.94/1.14 % (3909708)------------------------------
% 2.94/1.14 % (3909708)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.94/1.14 % (3909708)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.94/1.14 % (3909708)CaDiCaL version: 2.1.3
% 2.94/1.14 % (3909708)Termination reason: Instruction limit
% 2.94/1.14 % (3909708)Termination phase: Saturation
% 2.94/1.14 % (3909708)Time elapsed: 0.011 s
% 2.94/1.14 % (3909708)Peak memory usage: 89 MB
% 2.94/1.14 % (3909708)Instructions burned: 26 (million)
% 2.94/1.14 % (3909707)Refutation not found, incomplete strategy
% 2.94/1.14 % (3909707)------------------------------
% 2.94/1.14 % (3909707)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.94/1.14 % (3909707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.94/1.14 % (3909707)CaDiCaL version: 2.1.3
% 2.94/1.14 % (3909707)Termination reason: Refutation not found, incomplete strategy
% 2.94/1.14 % (3909707)Time elapsed: 0.010 s
% 2.94/1.14 % (3909707)Peak memory usage: 90 MB
% 2.94/1.14 % (3909707)Instructions burned: 15 (million)
% 2.94/1.14 % (3909706)Instruction limit reached!
% 2.94/1.14 % (3909706)------------------------------
% 2.94/1.14 % (3909706)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.94/1.14 % (3909706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.94/1.14 % (3909706)CaDiCaL version: 2.1.3
% 2.94/1.14 % (3909706)Termination reason: Instruction limit
% 2.94/1.14 % (3909706)Termination phase: Saturation
% 2.94/1.14 % (3909706)Time elapsed: 0.021 s
% 2.94/1.14 % (3909706)Peak memory usage: 88 MB
% 2.94/1.14 % (3909706)Instructions burned: 30 (million)
% 2.94/1.14 % (3909709)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=727139551:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi)
% 2.94/1.14 % (3909709)Instruction limit reached!
% 2.94/1.14 % (3909709)------------------------------
% 2.94/1.14 % (3909709)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.94/1.14 % (3909709)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.94/1.14 % (3909709)CaDiCaL version: 2.1.3
% 2.94/1.14 % (3909709)Termination reason: Instruction limit
% 2.94/1.14 % (3909709)Termination phase: Saturation
% 2.94/1.14 % (3909709)Time elapsed: 0.019 s
% 2.94/1.14 % (3909709)Peak memory usage: 89 MB
% 2.94/1.14 % (3909709)Instructions burned: 27 (million)
% 2.94/1.14 % (3909696)------------------------------
% 2.94/1.14 % (3909696)------------------------------
% 2.94/1.14 % (3909692)Refutation found. Thanks to Tanya!
% 2.94/1.14 % SZS status Theorem for theBenchmark
% 2.94/1.14 % SZS output start Proof for theBenchmark
% See solution above
% 3.92/1.34 % (3909692)------------------------------
% 3.92/1.34 % (3909692)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.92/1.34 % (3909692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.92/1.34 % (3909692)CaDiCaL version: 2.1.3
% 3.92/1.34 % (3909692)Termination reason: Refutation
% 3.92/1.34 % (3909692)Time elapsed: 0.045 s
% 3.92/1.34 % (3909692)Peak memory usage: 116 MB
% 3.92/1.34 % (3909692)Instructions burned: 28 (million)
% 3.92/1.34 % (3909692)------------------------------
% 3.92/1.34 % (3909692)------------------------------
% 3.92/1.34 % (3909686)Success in time 0.466 s
% 3.92/1.34 % Vampire exiting
%------------------------------------------------------------------------------