%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : DAT053_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 : n008.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:11 AM UTC 2026
% Result : Theorem 3.86s 1.30s
% Output : Refutation 5.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 18
% Syntax : Number of formulae : 65 ( 11 unt; 0 typ; 14 def)
% Number of atoms : 151 ( 54 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 136 ( 50 ~; 50 |; 17 &)
% ( 14 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 6 ( 2 avg)
% Number arithmetic : 102 ( 0 atm; 51 fun; 51 num; 0 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 : 17 ( 15 usr; 15 prp; 0-2 aty)
% Number of functors : 11 ( 7 usr; 4 con; 0-2 aty)
% Number of variables : 10 ( 10 !; 0 ?; 10 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
record: $tType ).
tff(func_def_0,type,
length: record > $int ).
tff(func_def_1,type,
next: record > record ).
tff(func_def_2,type,
data: record > $int ).
tff(func_def_3,type,
split1: record > record ).
tff(func_def_4,type,
split2: record > record ).
tff(func_def_8,type,
a: record ).
tff(func_def_9,type,
b: record ).
tff(pred_def_1,type,
isrecord: record > $o ).
tff(f3,axiom,
! [X0: record] :
( isrecord(X0)
=> ( length(X0) = $sum(length(next(X0)),1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3) ).
tff(f5,axiom,
! [X0: record] :
( isrecord(X0)
=> isrecord(split1(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
tff(f8,axiom,
! [X0: record] :
( ( isrecord(X0)
& isrecord(next(X0)) )
=> ( next(split1(X0)) = split1(next(next(X0))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
tff(f14,conjecture,
( ( ( ( $product(2,length(split1(a))) = $sum(length(a),1) )
| ( $product(2,length(split1(a))) = length(a) ) )
& isrecord(next(b))
& isrecord(b)
& ( next(next(b)) = a ) )
=> ( ( $product(2,length(split1(b))) = $sum(length(b),1) )
| ( $product(2,length(split1(b))) = length(b) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1) ).
tff(f15,negated_conjecture,
~ ( ( ( ( $product(2,length(split1(a))) = $sum(length(a),1) )
| ( $product(2,length(split1(a))) = length(a) ) )
& isrecord(next(b))
& isrecord(b)
& ( next(next(b)) = a ) )
=> ( ( $product(2,length(split1(b))) = $sum(length(b),1) )
| ( $product(2,length(split1(b))) = length(b) ) ) ),
inference(negated_conjecture,[status(cth)],[f14]) ).
tff(f21,plain,
! [X0: record] :
( ~ isrecord(X0)
| ( length(X0) = $sum(length(next(X0)),1) ) ),
inference(ennf_transformation,[],[f3]) ).
tff(f22,plain,
( ( $product(2,length(split1(b))) != $sum(length(b),1) )
& ( $product(2,length(split1(b))) != length(b) )
& ( ( $product(2,length(split1(a))) = $sum(length(a),1) )
| ( $product(2,length(split1(a))) = length(a) ) )
& isrecord(next(b))
& isrecord(b)
& ( next(next(b)) = a ) ),
inference(ennf_transformation,[],[f15]) ).
tff(f23,plain,
( isrecord(b)
& ( ( $product(2,length(split1(a))) = $sum(length(a),1) )
| ( $product(2,length(split1(a))) = length(a) ) )
& isrecord(next(b))
& ( $product(2,length(split1(b))) != $sum(length(b),1) )
& ( next(next(b)) = a )
& ( $product(2,length(split1(b))) != length(b) ) ),
inference(flattening,[],[f22]) ).
tff(f26,plain,
! [X0: record] :
( isrecord(split1(X0))
| ~ isrecord(X0) ),
inference(ennf_transformation,[],[f5]) ).
tff(f30,plain,
! [X0: record] :
( ( next(split1(X0)) = split1(next(next(X0))) )
| ~ isrecord(X0)
| ~ isrecord(next(X0)) ),
inference(ennf_transformation,[],[f8]) ).
tff(f31,plain,
! [X0: record] :
( ~ isrecord(next(X0))
| ~ isrecord(X0)
| ( next(split1(X0)) = split1(next(next(X0))) ) ),
inference(flattening,[],[f30]) ).
tff(f37,plain,
! [X0: record] :
( ~ isrecord(X0)
| ( length(X0) = $sum(length(next(X0)),1) ) ),
inference(cnf_transformation,[],[f21]) ).
tff(f38,plain,
$product(2,length(split1(b))) != length(b),
inference(cnf_transformation,[],[f23]) ).
tff(f39,plain,
next(next(b)) = a,
inference(cnf_transformation,[],[f23]) ).
tff(f40,plain,
$product(2,length(split1(b))) != $sum(length(b),1),
inference(cnf_transformation,[],[f23]) ).
tff(f41,plain,
isrecord(next(b)),
inference(cnf_transformation,[],[f23]) ).
tff(f42,plain,
( ( $product(2,length(split1(a))) = $sum(length(a),1) )
| ( $product(2,length(split1(a))) = length(a) ) ),
inference(cnf_transformation,[],[f23]) ).
tff(f43,plain,
isrecord(b),
inference(cnf_transformation,[],[f23]) ).
tff(f48,plain,
! [X0: record] :
( ~ isrecord(next(X0))
| ( next(split1(X0)) = split1(next(next(X0))) )
| ~ isrecord(X0) ),
inference(cnf_transformation,[],[f31]) ).
tff(f51,plain,
! [X0: record] :
( isrecord(split1(X0))
| ~ isrecord(X0) ),
inference(cnf_transformation,[],[f26]) ).
tff(f57,definition,
( spl0_1
<=> ( next(next(b)) = a ) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
tff(f59,plain,
( ( next(next(b)) = a )
| ~ spl0_1 ),
inference(avatar_component_clause,[],[f57]) ).
tff(f60,plain,
spl0_1,
inference(avatar_split_clause,[],[f39,f57]) ).
tff(f62,definition,
( spl0_2
<=> ( $product(2,length(split1(b))) = $sum(length(b),1) ) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
tff(f65,plain,
~ spl0_2,
inference(avatar_split_clause,[],[f40,f62]) ).
tff(f67,definition,
( spl0_3
<=> isrecord(next(b)) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
tff(f69,plain,
( isrecord(next(b))
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f67]) ).
tff(f70,plain,
spl0_3,
inference(avatar_split_clause,[],[f41,f67]) ).
tff(f72,definition,
( spl0_4
<=> isrecord(b) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
tff(f74,plain,
( isrecord(b)
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f72]) ).
tff(f75,plain,
spl0_4,
inference(avatar_split_clause,[],[f43,f72]) ).
tff(f77,definition,
( spl0_5
<=> ( $product(2,length(split1(a))) = $sum(length(a),1) ) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
tff(f81,definition,
( spl0_6
<=> ( $product(2,length(split1(a))) = length(a) ) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
tff(f83,plain,
( ( $product(2,length(split1(a))) = length(a) )
| ~ spl0_6 ),
inference(avatar_component_clause,[],[f81]) ).
tff(f84,plain,
( spl0_5
| spl0_6 ),
inference(avatar_split_clause,[],[f42,f81,f77]) ).
tff(f86,definition,
( spl0_7
<=> ( $product(2,length(split1(b))) = length(b) ) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
tff(f89,plain,
~ spl0_7,
inference(avatar_split_clause,[],[f38,f86]) ).
tff(f90,plain,
( ( length(next(next(b))) = $product(2,length(split1(next(next(b))))) )
| ~ spl0_1
| ~ spl0_6 ),
inference(forward_demodulation,[],[f83,f59]) ).
tff(f92,definition,
( spl0_8
<=> ( length(next(next(b))) = $product(2,length(split1(next(next(b))))) ) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
tff(f94,plain,
( ( length(next(next(b))) = $product(2,length(split1(next(next(b))))) )
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f92]) ).
tff(f95,plain,
( spl0_8
| ~ spl0_1
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f90,f81,f57,f92]) ).
tff(f139,plain,
( ( $sum(length(next(next(b))),1) = length(next(b)) )
| ~ spl0_3 ),
inference(resolution,[],[f37,f69]) ).
tff(f142,plain,
( ( length(b) = $sum(length(next(b)),1) )
| ~ spl0_4 ),
inference(resolution,[],[f37,f74]) ).
tff(f149,definition,
( spl0_14
<=> ( $sum(length(next(next(b))),1) = length(next(b)) ) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
tff(f152,plain,
( spl0_14
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f139,f67,f149]) ).
tff(f154,definition,
( spl0_15
<=> ( length(b) = $sum(length(next(b)),1) ) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
tff(f157,plain,
( spl0_15
| ~ spl0_4 ),
inference(avatar_split_clause,[],[f142,f72,f154]) ).
tff(f167,plain,
( ( split1(next(next(b))) = next(split1(b)) )
| ~ isrecord(b)
| ~ spl0_3 ),
inference(resolution,[],[f48,f69]) ).
tff(f170,plain,
( ( split1(next(next(b))) = next(split1(b)) )
| ~ spl0_3
| ~ spl0_4 ),
inference(forward_subsumption_resolution,[],[f167,f74]) ).
tff(f172,definition,
( spl0_17
<=> ( split1(next(next(b))) = next(split1(b)) ) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
tff(f174,plain,
( ( split1(next(next(b))) = next(split1(b)) )
| ~ spl0_17 ),
inference(avatar_component_clause,[],[f172]) ).
tff(f175,plain,
( spl0_17
| ~ spl0_3
| ~ spl0_4 ),
inference(avatar_split_clause,[],[f170,f72,f67,f172]) ).
tff(f176,plain,
( ( length(next(next(b))) = $product(2,length(next(split1(b)))) )
| ~ spl0_8
| ~ spl0_17 ),
inference(superposition,[],[f94,f174]) ).
tff(f190,definition,
( spl0_20
<=> ( length(next(next(b))) = $product(2,length(next(split1(b)))) ) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
tff(f193,plain,
( spl0_20
| ~ spl0_8
| ~ spl0_17 ),
inference(avatar_split_clause,[],[f176,f172,f92,f190]) ).
tff(f240,definition,
( spl0_27
<=> isrecord(split1(b)) ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
tff(f241,plain,
( isrecord(split1(b))
| ~ spl0_27 ),
inference(avatar_component_clause,[],[f240]) ).
tff(f242,plain,
( ~ isrecord(split1(b))
| spl0_27 ),
inference(avatar_component_clause,[],[f240]) ).
tff(f318,plain,
( ~ isrecord(b)
| spl0_27 ),
inference(resolution,[],[f242,f51]) ).
tff(f332,plain,
( $false
| ~ spl0_4
| spl0_27 ),
inference(forward_subsumption_resolution,[],[f318,f74]) ).
tff(f333,plain,
( ~ spl0_4
| spl0_27 ),
inference(avatar_contradiction_clause,[],[f332]) ).
tff(f346,plain,
( ( length(split1(b)) = $sum(length(next(split1(b))),1) )
| ~ spl0_27 ),
inference(resolution,[],[f241,f37]) ).
tff(f349,definition,
( spl0_41
<=> ( length(split1(b)) = $sum(length(next(split1(b))),1) ) ),
introduced(definition,[new_symbols(definition,[spl0_41])],[avatar_definition]) ).
tff(f352,plain,
( spl0_41
| ~ spl0_27 ),
inference(avatar_split_clause,[],[f346,f240,f349]) ).
tff(f359,plain,
$false,
inference(avatar_smt_refutation,[],[f352,f333,f193,f175,f157,f152,f95,f89,f84,f75,f70,f65,f60]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : DAT053_1 : TPTP v9.3.1. Released v5.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.18 % Computer : n008.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:07:54 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.21 Running first-order theorem proving
% 0.08/0.21 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
% 3.86/1.30 % (2780441)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 3.86/1.30 % (2780493)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=1170863402:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 3.86/1.30 % (2780493)Instruction limit reached!
% 3.86/1.30 % (2780493)------------------------------
% 3.86/1.30 % (2780493)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.86/1.30 % (2780493)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.86/1.30 % (2780493)CaDiCaL version: 2.1.3
% 3.86/1.30 % (2780493)Termination reason: Instruction limit
% 3.86/1.30 % (2780493)Termination phase: Saturation
% 3.86/1.30 % (2780493)Time elapsed: 0.004 s
% 3.86/1.30 % (2780493)Peak memory usage: 88 MB
% 3.86/1.30 % (2780493)Instructions burned: 9 (million)
% 3.86/1.30 % (2780488)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=3470937129:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 3.86/1.30 % (2780491)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1002685951:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 3.86/1.30 % (2780490)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=508957069:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 3.86/1.30 % (2780497)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=1362389021:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 3.86/1.30 % (2780494)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=759232489:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 3.86/1.30 % (2780496)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=3784933193:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 3.86/1.30 % (2780494)Instruction limit reached!
% 3.86/1.30 % (2780494)------------------------------
% 3.86/1.30 % (2780494)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.86/1.30 % (2780494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.86/1.30 % (2780494)CaDiCaL version: 2.1.3
% 3.86/1.30 % (2780494)Termination reason: Instruction limit
% 3.86/1.30 % (2780494)Termination phase: Saturation
% 3.86/1.30 % (2780494)Time elapsed: 0.004 s
% 3.86/1.30 % (2780494)Peak memory usage: 88 MB
% 3.86/1.30 % (2780494)Instructions burned: 4 (million)
% 3.86/1.30 % (2780488)Instruction limit reached!
% 3.86/1.30 % (2780488)------------------------------
% 3.86/1.30 % (2780488)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.86/1.30 % (2780488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.86/1.30 % (2780488)CaDiCaL version: 2.1.3
% 3.86/1.30 % (2780488)Termination reason: Instruction limit
% 3.86/1.30 % (2780488)Termination phase: Saturation
% 3.86/1.30 % (2780488)Time elapsed: 0.032 s
% 3.86/1.30 % (2780488)Peak memory usage: 115 MB
% 3.86/1.30 % (2780488)Instructions burned: 13 (million)
% 3.86/1.30 % (2780497)Instruction limit reached!
% 3.86/1.30 % (2780497)------------------------------
% 3.86/1.30 % (2780497)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.86/1.30 % (2780497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.86/1.30 % (2780497)CaDiCaL version: 2.1.3
% 3.86/1.30 % (2780497)Termination reason: Instruction limit
% 3.86/1.30 % (2780497)Termination phase: Saturation
% 3.86/1.30 % (2780497)Time elapsed: 0.047 s
% 3.86/1.30 % (2780497)Peak memory usage: 116 MB
% 3.86/1.30 % (2780497)Instructions burned: 34 (million)
% 3.86/1.30 % (2780496)First to succeed.
% 3.86/1.30 % (2780496)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2780441"
% 3.86/1.30 % (2780537)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=1137012665:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 3.86/1.30 % (2780537)Instruction limit reached!
% 3.86/1.30 % (2780537)------------------------------
% 3.86/1.30 % (2780537)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.86/1.30 % (2780537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.86/1.30 % (2780537)CaDiCaL version: 2.1.3
% 3.86/1.30 % (2780537)Termination reason: Instruction limit
% 3.86/1.30 % (2780537)Termination phase: Saturation
% 3.86/1.30 % (2780537)Time elapsed: 0.006 s
% 3.86/1.30 % (2780537)Peak memory usage: 88 MB
% 3.86/1.30 % (2780537)Instructions burned: 16 (million)
% 3.86/1.30 % (2780491)Instruction limit reached!
% 3.86/1.30 % (2780491)------------------------------
% 3.86/1.30 % (2780491)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.86/1.30 % (2780491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.86/1.30 % (2780491)CaDiCaL version: 2.1.3
% 3.86/1.30 % (2780491)Termination reason: Instruction limit
% 3.86/1.30 % (2780491)Termination phase: Saturation
% 3.86/1.30 % (2780491)Time elapsed: 0.148 s
% 3.86/1.30 % (2780491)Peak memory usage: 117 MB
% 3.86/1.30 % (2780491)Instructions burned: 201 (million)
% 3.86/1.30 % (2780555)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=389424803:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi)
% 3.86/1.30 % (2780561)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=1812115324:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2997 on theBenchmark for (2997ds/16Mi)
% 3.86/1.30 % (2780555)Instruction limit reached!
% 3.86/1.30 % (2780555)------------------------------
% 3.86/1.30 % (2780555)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.86/1.30 % (2780555)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.86/1.30 % (2780555)CaDiCaL version: 2.1.3
% 3.86/1.30 % (2780555)Termination reason: Instruction limit
% 3.86/1.30 % (2780555)Termination phase: Saturation
% 3.86/1.30 % (2780555)Time elapsed: 0.023 s
% 3.86/1.30 % (2780555)Peak memory usage: 88 MB
% 3.86/1.30 % (2780555)Instructions burned: 29 (million)
% 3.86/1.30 % (2780561)Instruction limit reached!
% 3.86/1.30 % (2780561)------------------------------
% 3.86/1.30 % (2780561)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.86/1.30 % (2780561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.86/1.30 % (2780561)CaDiCaL version: 2.1.3
% 3.86/1.30 % (2780561)Termination reason: Instruction limit
% 3.86/1.30 % (2780561)Termination phase: Saturation
% 3.86/1.30 % (2780561)Time elapsed: 0.011 s
% 3.86/1.30 % (2780561)Peak memory usage: 90 MB
% 3.86/1.30 % (2780561)Instructions burned: 16 (million)
% 3.86/1.30 % (2780490)Instruction limit reached!
% 3.86/1.30 % (2780490)------------------------------
% 3.86/1.30 % (2780490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.86/1.30 % (2780490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.86/1.30 % (2780490)CaDiCaL version: 2.1.3
% 3.86/1.30 % (2780490)Termination reason: Instruction limit
% 3.86/1.30 % (2780490)Termination phase: Saturation
% 3.86/1.30 % (2780490)Time elapsed: 0.216 s
% 3.86/1.30 % (2780490)Peak memory usage: 116 MB
% 3.86/1.30 % (2780490)Instructions burned: 314 (million)
% 3.86/1.30 % (2780576)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=262105041:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi)
% 3.86/1.30 % (2780566)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=189917547:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi)
% 3.86/1.30 % (2780576)Instruction limit reached!
% 3.86/1.30 % (2780576)------------------------------
% 3.86/1.30 % (2780576)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.86/1.30 % (2780576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.86/1.30 % (2780576)CaDiCaL version: 2.1.3
% 3.86/1.30 % (2780576)Termination reason: Instruction limit
% 3.86/1.30 % (2780576)Termination phase: Saturation
% 3.86/1.30 % (2780576)Time elapsed: 0.011 s
% 3.86/1.30 % (2780576)Peak memory usage: 89 MB
% 3.86/1.30 % (2780576)Instructions burned: 30 (million)
% 3.86/1.30 % (2780566)Instruction limit reached!
% 3.86/1.30 % (2780566)------------------------------
% 3.86/1.30 % (2780566)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.86/1.30 % (2780566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.86/1.30 % (2780566)CaDiCaL version: 2.1.3
% 3.86/1.30 % (2780566)Termination reason: Instruction limit
% 3.86/1.30 % (2780566)Termination phase: Saturation
% 3.86/1.30 % (2780566)Time elapsed: 0.020 s
% 3.86/1.30 % (2780566)Peak memory usage: 89 MB
% 3.86/1.30 % (2780566)Instructions burned: 24 (million)
% 3.86/1.30 % (2780588)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=216848105:i=85:gtgl=4:rtra=on:gtg=exists_sym_2996 on theBenchmark for (2996ds/85Mi)
% 3.86/1.30 % (2780599)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=3507551704:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi)
% 3.86/1.30 % (2780604)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=3658817866:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2996 on theBenchmark for (2996ds/66Mi)
% 3.86/1.30 % (2780599)Instruction limit reached!
% 3.86/1.30 % (2780599)------------------------------
% 3.86/1.30 % (2780599)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.86/1.30 % (2780599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.86/1.30 % (2780599)CaDiCaL version: 2.1.3
% 3.86/1.30 % (2780599)Termination reason: Instruction limit
% 3.86/1.30 % (2780599)Termination phase: Saturation
% 3.86/1.30 % (2780599)Time elapsed: 0.003 s
% 3.86/1.30 % (2780599)Peak memory usage: 89 MB
% 3.86/1.30 % (2780599)Instructions burned: 3 (million)
% 3.86/1.30 % (2780600)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=4213183077:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi)
% 3.86/1.30 % (2780588)Instruction limit reached!
% 3.86/1.30 % (2780588)------------------------------
% 3.86/1.30 % (2780588)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.86/1.30 % (2780588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.86/1.30 % (2780588)CaDiCaL version: 2.1.3
% 3.86/1.30 % (2780588)Termination reason: Instruction limit
% 3.86/1.30 % (2780588)Termination phase: Saturation
% 3.86/1.30 % (2780588)Time elapsed: 0.062 s
% 3.86/1.30 % (2780588)Peak memory usage: 90 MB
% 3.86/1.30 % (2780588)Instructions burned: 86 (million)
% 3.86/1.30 % (2780603)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=1768587861:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi)
% 3.86/1.30 % (2780603)Instruction limit reached!
% 3.86/1.30 % (2780603)------------------------------
% 3.86/1.30 % (2780603)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.86/1.30 % (2780603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.86/1.30 % (2780603)CaDiCaL version: 2.1.3
% 3.86/1.30 % (2780603)Termination reason: Instruction limit
% 3.86/1.30 % (2780603)Termination phase: Saturation
% 3.86/1.30 % (2780603)Time elapsed: 0.004 s
% 3.86/1.30 % (2780603)Peak memory usage: 88 MB
% 3.86/1.30 % (2780603)Instructions burned: 4 (million)
% 3.86/1.30 % (2780605)lrs+10_1_thi=all:si=on:fd=off:random_seed=2251604308:i=53:rtra=on:gtg=all_2995 on theBenchmark for (2995ds/53Mi)
% 3.86/1.30 % (2780604)Instruction limit reached!
% 3.86/1.30 % (2780604)------------------------------
% 3.86/1.30 % (2780604)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.86/1.30 % (2780604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.86/1.30 % (2780604)CaDiCaL version: 2.1.3
% 3.86/1.30 % (2780604)Termination reason: Instruction limit
% 3.86/1.30 % (2780604)Termination phase: Saturation
% 3.86/1.30 % (2780604)Time elapsed: 0.053 s
% 3.86/1.30 % (2780604)Peak memory usage: 133 MB
% 3.86/1.30 % (2780604)Instructions burned: 68 (million)
% 3.86/1.30 % (2780600)Instruction limit reached!
% 3.86/1.30 % (2780600)------------------------------
% 3.86/1.30 % (2780600)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.86/1.30 % (2780600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.86/1.30 % (2780600)CaDiCaL version: 2.1.3
% 3.86/1.30 % (2780600)Termination reason: Instruction limit
% 3.86/1.30 % (2780600)Termination phase: Saturation
% 3.86/1.30 % (2780600)Time elapsed: 0.100 s
% 3.86/1.30 % (2780600)Peak memory usage: 90 MB
% 3.86/1.30 % (2780600)Instructions burned: 182 (million)
% 3.86/1.30 % (2780605)Instruction limit reached!
% 3.86/1.30 % (2780605)------------------------------
% 3.86/1.30 % (2780605)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.86/1.30 % (2780605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.86/1.30 % (2780605)CaDiCaL version: 2.1.3
% 3.86/1.30 % (2780605)Termination reason: Instruction limit
% 3.86/1.30 % (2780605)Termination phase: Saturation
% 3.86/1.30 % (2780605)Time elapsed: 0.058 s
% 3.86/1.30 % (2780605)Peak memory usage: 113 MB
% 3.86/1.30 % (2780605)Instructions burned: 53 (million)
% 3.86/1.30 % (2780496)Refutation found. Thanks to Tanya!
% 3.86/1.30 % SZS status Theorem for theBenchmark
% 3.86/1.30 % SZS output start Proof for theBenchmark
% See solution above
% 5.09/1.49 % (2780496)------------------------------
% 5.09/1.49 % (2780496)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.09/1.49 % (2780496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.09/1.49 % (2780496)CaDiCaL version: 2.1.3
% 5.09/1.49 % (2780496)Termination reason: Refutation
% 5.09/1.49 % (2780496)Time elapsed: 0.079 s
% 5.09/1.49 % (2780496)Peak memory usage: 117 MB
% 5.09/1.49 % (2780496)Instructions burned: 48 (million)
% 5.09/1.49 % (2780496)------------------------------
% 5.09/1.49 % (2780496)------------------------------
% 5.09/1.49 % (2780441)Success in time 0.647 s
% 5.09/1.49 % Vampire exiting
%------------------------------------------------------------------------------