%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWX034+1 : TPTP v9.3.1. Released v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:45:43 PM UTC 2026
% Result : Theorem 4.18s 1.13s
% Output : Refutation 5.41s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 12
% Syntax : Number of formulae : 79 ( 14 unt; 6 def)
% Number of atoms : 268 ( 40 equ)
% Maximal formula atoms : 10 ( 3 avg)
% Number of connectives : 296 ( 107 ~; 124 |; 41 &)
% ( 8 <=>; 16 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 13 ( 10 usr; 8 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 8 con; 0-3 aty)
% Number of variables : 133 ( 0 sgn 113 !; 20 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : '0' != s(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',id1) ).
fof(f2,axiom,
! [X0,X1] :
( s(X0) = s(X1)
=> X0 = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',id2) ).
fof(f17,axiom,
! [X0,X1,X2] :
( times_terminates(X0,X1,X2)
<=> ( ! [X3,X4] :
( $true
& ( X0 != s(X3)
| ( times_terminates(X3,X1,X4)
& ( times_fails(X3,X1,X4)
| plus_terminates(X1,X4,X2) ) ) ) )
& $true
& ( X0 != '0'
| $true ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',id17) ).
fof(f34,axiom,
! [X0,X1,X2] :
( nat_succeeds(X0)
=> plus_terminates(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','lemma-(plus:termination:1)') ).
fof(f57,axiom,
( ! [X0] :
( ( ? [X1] :
( X0 = s(X1)
& nat_succeeds(X1)
& ! [X2,X3] :
( nat_succeeds(X2)
=> times_terminates(X1,X2,X3) ) )
| X0 = '0' )
=> ! [X2,X3] :
( nat_succeeds(X2)
=> times_terminates(X0,X2,X3) ) )
=> ! [X0] :
( nat_succeeds(X0)
=> ! [X2,X3] :
( nat_succeeds(X2)
=> times_terminates(X0,X2,X3) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',induction) ).
fof(f58,conjecture,
! [X0,X1,X2] :
( ( nat_succeeds(X0)
& nat_succeeds(X1) )
=> times_terminates(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p','lemma-(times:termination)') ).
fof(f59,negated_conjecture,
~ ! [X0,X1,X2] :
( ( nat_succeeds(X0)
& nat_succeeds(X1) )
=> times_terminates(X0,X1,X2) ),
inference(negated_conjecture,[status(cth)],[f58]) ).
fof(f60,plain,
! [X0,X1,X2] :
( times_terminates(X0,X1,X2)
<=> ! [X3,X4] :
( X0 != s(X3)
| ( times_terminates(X3,X1,X4)
& ( times_fails(X3,X1,X4)
| plus_terminates(X1,X4,X2) ) ) ) ),
inference(true_and_false_elimination,[],[f17]) ).
fof(f69,plain,
( ! [X0] :
( ( ? [X1] :
( X0 = s(X1)
& nat_succeeds(X1)
& ! [X2,X3] :
( nat_succeeds(X2)
=> times_terminates(X1,X2,X3) ) )
| X0 = '0' )
=> ! [X4,X5] :
( nat_succeeds(X4)
=> times_terminates(X0,X4,X5) ) )
=> ! [X6] :
( nat_succeeds(X6)
=> ! [X7,X8] :
( nat_succeeds(X7)
=> times_terminates(X6,X7,X8) ) ) ),
inference(rectify,[],[f57]) ).
fof(f70,plain,
! [X0,X1] :
( X0 = X1
| s(X0) != s(X1) ),
inference(ennf_transformation,[],[f2]) ).
fof(f91,plain,
! [X0,X1,X2] :
( plus_terminates(X0,X1,X2)
| ~ nat_succeeds(X0) ),
inference(ennf_transformation,[],[f34]) ).
fof(f125,plain,
( ! [X6] :
( ! [X7,X8] :
( times_terminates(X6,X7,X8)
| ~ nat_succeeds(X7) )
| ~ nat_succeeds(X6) )
| ? [X0] :
( ? [X4,X5] :
( ~ times_terminates(X0,X4,X5)
& nat_succeeds(X4) )
& ( ? [X1] :
( X0 = s(X1)
& nat_succeeds(X1)
& ! [X2,X3] :
( times_terminates(X1,X2,X3)
| ~ nat_succeeds(X2) ) )
| X0 = '0' ) ) ),
inference(ennf_transformation,[],[f69]) ).
fof(f126,plain,
? [X0,X1,X2] :
( ~ times_terminates(X0,X1,X2)
& nat_succeeds(X0)
& nat_succeeds(X1) ),
inference(ennf_transformation,[],[f59]) ).
fof(f127,plain,
? [X0,X1,X2] :
( ~ times_terminates(X0,X1,X2)
& nat_succeeds(X0)
& nat_succeeds(X1) ),
inference(flattening,[],[f126]) ).
fof(f137,plain,
! [X0,X1,X2] :
( ( times_terminates(X0,X1,X2)
| ? [X3,X4] :
( s(X3) = X0
& ( ~ times_terminates(X3,X1,X4)
| ( ~ times_fails(X3,X1,X4)
& ~ plus_terminates(X1,X4,X2) ) ) ) )
& ( ! [X3,X4] :
( X0 != s(X3)
| ( times_terminates(X3,X1,X4)
& ( times_fails(X3,X1,X4)
| plus_terminates(X1,X4,X2) ) ) )
| ~ times_terminates(X0,X1,X2) ) ),
inference(nnf_transformation,[],[f60]) ).
fof(f138,plain,
! [X0,X1,X2] :
( ( times_terminates(X0,X1,X2)
| ? [X3,X4] :
( s(X3) = X0
& ( ~ times_terminates(X3,X1,X4)
| ( ~ times_fails(X3,X1,X4)
& ~ plus_terminates(X1,X4,X2) ) ) ) )
& ( ! [X5,X6] :
( s(X5) != X0
| ( times_terminates(X5,X1,X6)
& ( times_fails(X5,X1,X6)
| plus_terminates(X1,X6,X2) ) ) )
| ~ times_terminates(X0,X1,X2) ) ),
inference(rectify,[],[f137]) ).
fof(f139,plain,
! [X0,X1,X2] :
( ( times_terminates(X0,X1,X2)
| ( s(sK4(X0,X1,X2)) = X0
& ( ~ times_terminates(sK4(X0,X1,X2),X1,sK5(X0,X1,X2))
| ( ~ times_fails(sK4(X0,X1,X2),X1,sK5(X0,X1,X2))
& ~ plus_terminates(X1,sK5(X0,X1,X2),X2) ) ) ) )
& ( ! [X5,X6] :
( s(X5) != X0
| ( times_terminates(X5,X1,X6)
& ( times_fails(X5,X1,X6)
| plus_terminates(X1,X6,X2) ) ) )
| ~ times_terminates(X0,X1,X2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK5]),skolemize(X3,sK4(X0,X1,X2)),skolemize(X4,sK5(X0,X1,X2))],[f138]) ).
fof(f187,plain,
( ! [X0] :
( ! [X1,X2] :
( times_terminates(X0,X1,X2)
| ~ nat_succeeds(X1) )
| ~ nat_succeeds(X0) )
| ? [X3] :
( ? [X4,X5] :
( ~ times_terminates(X3,X4,X5)
& nat_succeeds(X4) )
& ( ? [X6] :
( s(X6) = X3
& nat_succeeds(X6)
& ! [X7,X8] :
( times_terminates(X6,X7,X8)
| ~ nat_succeeds(X7) ) )
| '0' = X3 ) ) ),
inference(rectify,[],[f125]) ).
fof(f188,plain,
( ! [X0] :
( ! [X1,X2] :
( times_terminates(X0,X1,X2)
| ~ nat_succeeds(X1) )
| ~ nat_succeeds(X0) )
| ( ~ times_terminates(sK30,sK31,sK32)
& nat_succeeds(sK31)
& ( ( sK30 = s(sK33)
& nat_succeeds(sK33)
& ! [X7,X8] :
( times_terminates(sK33,X7,X8)
| ~ nat_succeeds(X7) ) )
| '0' = sK30 ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK30,sK31,sK32,sK33]),skolemize(X3,sK30),skolemize(X4,sK31),skolemize(X5,sK32),skolemize(X6,sK33)],[f187]) ).
fof(f189,plain,
( ~ times_terminates(sK34,sK35,sK36)
& nat_succeeds(sK34)
& nat_succeeds(sK35) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK34,sK35,sK36]),skolemize(X0,sK34),skolemize(X1,sK35),skolemize(X2,sK36)],[f127]) ).
fof(f190,plain,
! [X0] : '0' != s(X0),
inference(cnf_transformation,[],[f1]) ).
fof(f191,plain,
! [X0,X1] :
( s(X0) != s(X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f70]) ).
fof(f223,plain,
! [X2,X0,X1] :
( ~ times_terminates(sK4(X0,X1,X2),X1,sK5(X0,X1,X2))
| times_terminates(X0,X1,X2)
| ~ plus_terminates(X1,sK5(X0,X1,X2),X2) ),
inference(cnf_transformation,[],[f139]) ).
fof(f225,plain,
! [X2,X0,X1] :
( times_terminates(X0,X1,X2)
| s(sK4(X0,X1,X2)) = X0 ),
inference(cnf_transformation,[],[f139]) ).
fof(f297,plain,
! [X2,X0,X1] :
( plus_terminates(X0,X1,X2)
| ~ nat_succeeds(X0) ),
inference(cnf_transformation,[],[f91]) ).
fof(f320,plain,
! [X2,X0,X1,X8,X7] :
( times_terminates(X0,X1,X2)
| ~ nat_succeeds(X1)
| ~ nat_succeeds(X0)
| times_terminates(sK33,X7,X8)
| ~ nat_succeeds(X7)
| '0' = sK30 ),
inference(cnf_transformation,[],[f188]) ).
fof(f322,plain,
! [X2,X0,X1] :
( times_terminates(X0,X1,X2)
| ~ nat_succeeds(X1)
| ~ nat_succeeds(X0)
| sK30 = s(sK33)
| '0' = sK30 ),
inference(cnf_transformation,[],[f188]) ).
fof(f323,plain,
! [X2,X0,X1] :
( times_terminates(X0,X1,X2)
| ~ nat_succeeds(X1)
| ~ nat_succeeds(X0)
| nat_succeeds(sK31) ),
inference(cnf_transformation,[],[f188]) ).
fof(f324,plain,
! [X2,X0,X1] :
( times_terminates(X0,X1,X2)
| ~ nat_succeeds(X1)
| ~ nat_succeeds(X0)
| ~ times_terminates(sK30,sK31,sK32) ),
inference(cnf_transformation,[],[f188]) ).
fof(f325,plain,
nat_succeeds(sK35),
inference(cnf_transformation,[],[f189]) ).
fof(f326,plain,
nat_succeeds(sK34),
inference(cnf_transformation,[],[f189]) ).
fof(f327,plain,
~ times_terminates(sK34,sK35,sK36),
inference(cnf_transformation,[],[f189]) ).
fof(f329,definition,
( spl37_1
<=> '0' = sK30 ),
introduced(definition,[new_symbols(definition,[spl37_1])],[avatar_definition]) ).
fof(f331,plain,
( '0' = sK30
| ~ spl37_1 ),
inference(avatar_component_clause,[],[f329]) ).
fof(f333,definition,
( spl37_2
<=> ! [X8,X7] :
( times_terminates(sK33,X7,X8)
| ~ nat_succeeds(X7) ) ),
introduced(definition,[new_symbols(definition,[spl37_2])],[avatar_definition]) ).
fof(f334,plain,
( ! [X8,X7] :
( times_terminates(sK33,X7,X8)
| ~ nat_succeeds(X7) )
| ~ spl37_2 ),
inference(avatar_component_clause,[],[f333]) ).
fof(f336,definition,
( spl37_3
<=> ! [X2,X0,X1] :
( times_terminates(X0,X1,X2)
| ~ nat_succeeds(X0)
| ~ nat_succeeds(X1) ) ),
introduced(definition,[new_symbols(definition,[spl37_3])],[avatar_definition]) ).
fof(f337,plain,
( ! [X2,X0,X1] :
( times_terminates(X0,X1,X2)
| ~ nat_succeeds(X0)
| ~ nat_succeeds(X1) )
| ~ spl37_3 ),
inference(avatar_component_clause,[],[f336]) ).
fof(f338,plain,
( spl37_1
| spl37_2
| spl37_3 ),
inference(avatar_split_clause,[],[f320,f336,f333,f329]) ).
fof(f345,definition,
( spl37_5
<=> sK30 = s(sK33) ),
introduced(definition,[new_symbols(definition,[spl37_5])],[avatar_definition]) ).
fof(f347,plain,
( sK30 = s(sK33)
| ~ spl37_5 ),
inference(avatar_component_clause,[],[f345]) ).
fof(f348,plain,
( spl37_1
| spl37_5
| spl37_3 ),
inference(avatar_split_clause,[],[f322,f336,f345,f329]) ).
fof(f350,definition,
( spl37_6
<=> nat_succeeds(sK31) ),
introduced(definition,[new_symbols(definition,[spl37_6])],[avatar_definition]) ).
fof(f352,plain,
( nat_succeeds(sK31)
| ~ spl37_6 ),
inference(avatar_component_clause,[],[f350]) ).
fof(f353,plain,
( spl37_6
| spl37_3 ),
inference(avatar_split_clause,[],[f323,f336,f350]) ).
fof(f355,definition,
( spl37_7
<=> times_terminates(sK30,sK31,sK32) ),
introduced(definition,[new_symbols(definition,[spl37_7])],[avatar_definition]) ).
fof(f357,plain,
( ~ times_terminates(sK30,sK31,sK32)
| spl37_7 ),
inference(avatar_component_clause,[],[f355]) ).
fof(f358,plain,
( ~ spl37_7
| spl37_3 ),
inference(avatar_split_clause,[],[f324,f336,f355]) ).
fof(f364,plain,
( ~ nat_succeeds(sK35)
| ~ spl37_3 ),
inference(unit_resulting_resolution,[],[f337,f326,f327]) ).
fof(f369,plain,
( $false
| ~ spl37_3 ),
inference(forward_subsumption_resolution,[],[f364,f325]) ).
fof(f370,plain,
~ spl37_3,
inference(avatar_contradiction_clause,[],[f369]) ).
fof(f371,plain,
( ~ times_terminates('0',sK31,sK32)
| ~ spl37_1
| spl37_7 ),
inference(superposition,[],[f357,f331]) ).
fof(f373,plain,
( sK30 = s(sK4(sK30,sK31,sK32))
| spl37_7 ),
inference(unit_resulting_resolution,[],[f225,f357]) ).
fof(f381,plain,
( '0' = s(sK4('0',sK31,sK32))
| ~ spl37_1
| spl37_7 ),
inference(unit_resulting_resolution,[],[f225,f371]) ).
fof(f384,plain,
( $false
| ~ spl37_1
| spl37_7 ),
inference(forward_subsumption_resolution,[],[f381,f190]) ).
fof(f385,plain,
( ~ spl37_1
| spl37_7 ),
inference(avatar_contradiction_clause,[],[f384]) ).
fof(f390,plain,
( ! [X0] : times_terminates(sK33,sK31,X0)
| ~ spl37_2
| ~ spl37_6 ),
inference(unit_resulting_resolution,[],[f334,f352]) ).
fof(f397,plain,
( ! [X0,X1] : plus_terminates(sK31,X0,X1)
| ~ spl37_6 ),
inference(unit_resulting_resolution,[],[f297,f352]) ).
fof(f419,plain,
( ! [X0] :
( s(X0) != sK30
| sK33 = X0 )
| ~ spl37_5 ),
inference(superposition,[],[f191,f347]) ).
fof(f760,plain,
( sK33 = sK4(sK30,sK31,sK32)
| ~ spl37_5
| spl37_7 ),
inference(unit_resulting_resolution,[],[f419,f373]) ).
fof(f5352,plain,
( ~ times_terminates(sK33,sK31,sK5(sK30,sK31,sK32))
| times_terminates(sK30,sK31,sK32)
| ~ plus_terminates(sK31,sK5(sK30,sK31,sK32),sK32)
| ~ spl37_5
| spl37_7 ),
inference(superposition,[],[f223,f760]) ).
fof(f5353,plain,
( times_terminates(sK30,sK31,sK32)
| ~ plus_terminates(sK31,sK5(sK30,sK31,sK32),sK32)
| ~ spl37_2
| ~ spl37_5
| ~ spl37_6
| spl37_7 ),
inference(forward_subsumption_resolution,[],[f5352,f390]) ).
fof(f5355,plain,
( ~ plus_terminates(sK31,sK5(sK30,sK31,sK32),sK32)
| ~ spl37_2
| ~ spl37_5
| ~ spl37_6
| spl37_7 ),
inference(forward_subsumption_resolution,[],[f5353,f357]) ).
fof(f5357,plain,
( $false
| ~ spl37_2
| ~ spl37_5
| ~ spl37_6
| spl37_7 ),
inference(forward_subsumption_resolution,[],[f5355,f397]) ).
fof(f5358,plain,
( ~ spl37_2
| ~ spl37_5
| ~ spl37_6
| spl37_7 ),
inference(avatar_contradiction_clause,[],[f5357]) ).
cnf(s1,plain,
( spl37_1
| spl37_2
| spl37_3 ),
inference(sat_conversion,[],[f338]) ).
cnf(s3,plain,
( spl37_1
| spl37_3
| spl37_5 ),
inference(sat_conversion,[],[f348]) ).
cnf(s4,plain,
( spl37_3
| spl37_6 ),
inference(sat_conversion,[],[f353]) ).
cnf(s5,plain,
( spl37_3
| ~ spl37_7 ),
inference(sat_conversion,[],[f358]) ).
cnf(s8,plain,
~ spl37_3,
inference(sat_conversion,[],[f370]) ).
cnf(s10,plain,
( ~ spl37_1
| spl37_7 ),
inference(sat_conversion,[],[f385]) ).
cnf(s31,plain,
( ~ spl37_2
| ~ spl37_5
| ~ spl37_6
| spl37_7 ),
inference(sat_conversion,[],[f5358]) ).
cnf(s32,plain,
~ spl37_7,
inference(rat,[],[s5,s8]) ).
cnf(s33,plain,
~ spl37_1,
inference(rat,[],[s10,s32]) ).
cnf(s34,plain,
spl37_6,
inference(rat,[],[s4,s8]) ).
cnf(s35,plain,
spl37_5,
inference(rat,[],[s3,s8,s33]) ).
cnf(s36,plain,
~ spl37_2,
inference(rat,[],[s31,s32,s34,s35]) ).
cnf(s42,plain,
$false,
inference(rat,[],[s1,s8,s36,s33]) ).
fof(f5359,plain,
$false,
inference(avatar_sat_refutation,[],[s42]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX034+1 : TPTP v9.3.1. Released v9.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.19 % Computer : n020.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 : Mon Sep 28 14:55:30 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.22 Running first-order theorem proving
% 0.08/0.22 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
% 4.18/1.13 % (220975)Detected formulas, will run a generic FOF schedule.
% 4.18/1.13 % (220986)dis-21_1_sil=8000:lcm=predicate:random_seed=2068049078:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 4.18/1.13 % (220986)Instruction limit reached!
% 4.18/1.13 % (220986)------------------------------
% 4.18/1.13 % (220986)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.18/1.13 % (220986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.18/1.13 % (220986)CaDiCaL version: 2.1.3
% 4.18/1.13 % (220986)Termination reason: Instruction limit
% 4.18/1.13 % (220986)Termination phase: Saturation
% 4.18/1.13 % (220986)Time elapsed: 0.031 s
% 4.18/1.13 % (220986)Peak memory usage: 89 MB
% 4.18/1.13 % (220986)Instructions burned: 130 (million)
% 4.18/1.13 % (220984)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2308979358:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 4.18/1.13 % (220985)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3761464420:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 4.18/1.13 % (220983)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1127619745:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 4.18/1.13 % (220982)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=1587203512:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 4.18/1.13 % (220980)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=150327448:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 4.18/1.13 % (220981)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=1908532552:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 4.18/1.13 % (220983)Refutation not found, incomplete strategy
% 4.18/1.13 % (220983)------------------------------
% 4.18/1.13 % (220983)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.18/1.13 % (220983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.18/1.13 % (220983)CaDiCaL version: 2.1.3
% 4.18/1.13 % (220983)Termination reason: Refutation not found, incomplete strategy
% 4.18/1.13 % (220983)Time elapsed: 0.002 s
% 4.18/1.13 % (220983)Peak memory usage: 88 MB
% 4.18/1.13 % (220983)Instructions burned: 1 (million)
% 4.18/1.13 % (220984)Instruction limit reached!
% 4.18/1.13 % (220984)------------------------------
% 4.18/1.13 % (220984)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.18/1.13 % (220984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.18/1.13 % (220984)CaDiCaL version: 2.1.3
% 4.18/1.13 % (220984)Termination reason: Instruction limit
% 4.18/1.13 % (220984)Termination phase: Saturation
% 4.18/1.13 % (220984)Time elapsed: 0.089 s
% 4.18/1.13 % (220984)Peak memory usage: 88 MB
% 4.18/1.13 % (220984)Instructions burned: 120 (million)
% 4.18/1.13 % (220985)Instruction limit reached!
% 4.18/1.13 % (220985)------------------------------
% 4.18/1.13 % (220985)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.18/1.13 % (220985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.18/1.13 % (220985)CaDiCaL version: 2.1.3
% 4.18/1.13 % (220985)Termination reason: Instruction limit
% 4.18/1.13 % (220985)Termination phase: Saturation
% 4.18/1.13 % (220985)Time elapsed: 0.093 s
% 4.18/1.13 % (220985)Peak memory usage: 90 MB
% 4.18/1.13 % (220985)Instructions burned: 139 (million)
% 4.18/1.13 % (220988)lrs+10_1_sil=8000:sp=occurrence:random_seed=493905514:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 4.18/1.13 % (220988)Instruction limit reached!
% 4.18/1.13 % (220988)------------------------------
% 4.18/1.13 % (220988)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.18/1.13 % (220988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.18/1.13 % (220988)CaDiCaL version: 2.1.3
% 4.18/1.13 % (220988)Termination reason: Instruction limit
% 4.18/1.13 % (220988)Termination phase: Saturation
% 4.18/1.13 % (220988)Time elapsed: 0.097 s
% 4.18/1.13 % (220988)Peak memory usage: 91 MB
% 4.18/1.13 % (220988)Instructions burned: 285 (million)
% 4.18/1.13 % (220983)------------------------------
% 4.18/1.13 % (220983)------------------------------
% 4.18/1.13 % (220996)lrs+1011_1_sil=32000:sp=occurrence:random_seed=176186891:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 4.18/1.13 % (220995)lrs+10_1_sil=32000:urr=on:br=off:random_seed=682793930:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 4.18/1.13 % (220998)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=1801638594:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 4.18/1.13 % (220995)Instruction limit reached!
% 4.18/1.13 % (220995)------------------------------
% 4.18/1.13 % (220995)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.18/1.13 % (220995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.18/1.13 % (220995)CaDiCaL version: 2.1.3
% 4.18/1.13 % (220995)Termination reason: Instruction limit
% 4.18/1.13 % (220995)Termination phase: Saturation
% 4.18/1.13 % (220995)Time elapsed: 0.073 s
% 4.18/1.13 % (220995)Peak memory usage: 89 MB
% 4.18/1.13 % (220995)Instructions burned: 157 (million)
% 4.18/1.13 % (220998)First to succeed.
% 4.18/1.13 % (220998)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-220975"
% 4.18/1.13 % (220999)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=84213180:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 4.18/1.13 % (220999)Refutation not found, incomplete strategy
% 4.18/1.13 % (220999)------------------------------
% 4.18/1.13 % (220999)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.18/1.13 % (220999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.18/1.13 % (220999)CaDiCaL version: 2.1.3
% 4.18/1.13 % (220999)Termination reason: Refutation not found, incomplete strategy
% 4.18/1.13 % (220999)Time elapsed: 0.011 s
% 4.18/1.13 % (220999)Peak memory usage: 89 MB
% 4.18/1.13 % (220999)Instructions burned: 15 (million)
% 4.18/1.13 % (220996)Instruction limit reached!
% 4.18/1.13 % (220996)------------------------------
% 4.18/1.13 % (220996)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.18/1.13 % (220996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.18/1.13 % (220996)CaDiCaL version: 2.1.3
% 4.18/1.13 % (220996)Termination reason: Instruction limit
% 4.18/1.13 % (220996)Termination phase: Saturation
% 4.18/1.13 % (220996)Time elapsed: 0.190 s
% 4.18/1.13 % (220996)Peak memory usage: 91 MB
% 4.18/1.13 % (220996)Instructions burned: 326 (million)
% 4.18/1.13 % (221003)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2241051788:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 4.18/1.13 % (220998)Refutation found. Thanks to Tanya!
% 4.18/1.13 % SZS status Theorem for theBenchmark
% 4.18/1.13 % SZS output start Proof for theBenchmark
% See solution above
% 5.41/1.33 % (220998)------------------------------
% 5.41/1.33 % (220998)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.41/1.33 % (220998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.41/1.33 % (220998)CaDiCaL version: 2.1.3
% 5.41/1.33 % (220998)Termination reason: Refutation
% 5.41/1.33 % (220998)Time elapsed: 0.051 s
% 5.41/1.33 % (220998)Peak memory usage: 92 MB
% 5.41/1.33 % (220998)Instructions burned: 151 (million)
% 5.41/1.33 % (220998)------------------------------
% 5.41/1.33 % (220998)------------------------------
% 5.41/1.33 % (220975)Success in time 0.714 s
% 5.41/1.33 % Vampire exiting
%------------------------------------------------------------------------------