%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : LAT286+3 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:46:32 AM UTC 2026
% Result : Theorem 10.68s 2.96s
% Output : Refutation 11.87s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 11
% Syntax : Number of formulae : 72 ( 15 unt; 4 def)
% Number of atoms : 211 ( 4 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 230 ( 91 ~; 102 |; 23 &)
% ( 7 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 12 ( 10 usr; 5 prp; 0-3 aty)
% Number of functors : 6 ( 6 usr; 1 con; 0-1 aty)
% Number of variables : 37 ( 0 sgn 35 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f471,axiom,
! [X0] : ~ v1_xboole_0(k1_zfmisc_1(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_subset_1) ).
fof(f556,axiom,
! [X0,X1] :
( ( ~ v1_xboole_0(X0)
& ~ v1_xboole_0(X1)
& m1_subset_1(X1,k1_zfmisc_1(X0)) )
=> ! [X2] :
( m2_subset_1(X2,X0,X1)
<=> m1_subset_1(X2,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',redefinition_m2_subset_1) ).
fof(f12331,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& l1_pre_topc(X0) )
=> m1_subset_1(k1_lopclset(X0),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(X0)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_k1_lopclset) ).
fof(f12353,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> ~ v1_xboole_0(k1_lopclset(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_lopclset) ).
fof(f12363,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> m2_subset_1(k2_pre_topc(X0),k1_zfmisc_1(u1_struct_0(X0)),k1_lopclset(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t8_lopclset) ).
fof(f12369,axiom,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> u1_struct_0(k6_lopclset(X0)) = k1_lopclset(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t13_lopclset) ).
fof(f12371,conjecture,
! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> m1_subset_1(k2_pre_topc(X0),u1_struct_0(k6_lopclset(X0))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t15_lopclset) ).
fof(f12372,negated_conjecture,
~ ! [X0] :
( ( ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) )
=> m1_subset_1(k2_pre_topc(X0),u1_struct_0(k6_lopclset(X0))) ),
inference(negated_conjecture,[status(cth)],[f12371]) ).
fof(f12433,plain,
! [X0] :
( m1_subset_1(k1_lopclset(X0),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(X0))))
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f12331]) ).
fof(f12434,plain,
! [X0] :
( m1_subset_1(k1_lopclset(X0),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(X0))))
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f12433]) ).
fof(f12475,plain,
! [X0] :
( ~ v1_xboole_0(k1_lopclset(X0))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f12353]) ).
fof(f12476,plain,
! [X0] :
( ~ v1_xboole_0(k1_lopclset(X0))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f12475]) ).
fof(f12493,plain,
! [X0] :
( m2_subset_1(k2_pre_topc(X0),k1_zfmisc_1(u1_struct_0(X0)),k1_lopclset(X0))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f12363]) ).
fof(f12494,plain,
! [X0] :
( m2_subset_1(k2_pre_topc(X0),k1_zfmisc_1(u1_struct_0(X0)),k1_lopclset(X0))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f12493]) ).
fof(f12505,plain,
! [X0] :
( u1_struct_0(k6_lopclset(X0)) = k1_lopclset(X0)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f12369]) ).
fof(f12506,plain,
! [X0] :
( u1_struct_0(k6_lopclset(X0)) = k1_lopclset(X0)
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(flattening,[],[f12505]) ).
fof(f12509,plain,
? [X0] :
( ~ m1_subset_1(k2_pre_topc(X0),u1_struct_0(k6_lopclset(X0)))
& ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) ),
inference(ennf_transformation,[],[f12372]) ).
fof(f12510,plain,
? [X0] :
( ~ m1_subset_1(k2_pre_topc(X0),u1_struct_0(k6_lopclset(X0)))
& ~ v3_struct_0(X0)
& v2_pre_topc(X0)
& l1_pre_topc(X0) ),
inference(flattening,[],[f12509]) ).
fof(f12553,plain,
! [X0,X1] :
( ! [X2] :
( m2_subset_1(X2,X0,X1)
<=> m1_subset_1(X2,X1) )
| v1_xboole_0(X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) ),
inference(ennf_transformation,[],[f556]) ).
fof(f12554,plain,
! [X0,X1] :
( ! [X2] :
( m2_subset_1(X2,X0,X1)
<=> m1_subset_1(X2,X1) )
| v1_xboole_0(X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) ),
inference(flattening,[],[f12553]) ).
fof(f12798,plain,
( ~ m1_subset_1(k2_pre_topc(sK5),u1_struct_0(k6_lopclset(sK5)))
& ~ v3_struct_0(sK5)
& v2_pre_topc(sK5)
& l1_pre_topc(sK5) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(X0,sK5)],[f12510]) ).
fof(f12826,plain,
! [X0,X1] :
( ! [X2] :
( ( m2_subset_1(X2,X0,X1)
| ~ m1_subset_1(X2,X1) )
& ( m1_subset_1(X2,X1)
| ~ m2_subset_1(X2,X0,X1) ) )
| v1_xboole_0(X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) ),
inference(nnf_transformation,[],[f12554]) ).
fof(f12922,plain,
! [X0] :
( m1_subset_1(k1_lopclset(X0),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(X0))))
| v3_struct_0(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f12434]) ).
fof(f12955,plain,
! [X0] :
( ~ v1_xboole_0(k1_lopclset(X0))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f12476]) ).
fof(f12970,plain,
! [X0] :
( m2_subset_1(k2_pre_topc(X0),k1_zfmisc_1(u1_struct_0(X0)),k1_lopclset(X0))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f12494]) ).
fof(f12978,plain,
! [X0] :
( k1_lopclset(X0) = u1_struct_0(k6_lopclset(X0))
| v3_struct_0(X0)
| ~ v2_pre_topc(X0)
| ~ l1_pre_topc(X0) ),
inference(cnf_transformation,[],[f12506]) ).
fof(f12980,plain,
l1_pre_topc(sK5),
inference(cnf_transformation,[],[f12798]) ).
fof(f12981,plain,
v2_pre_topc(sK5),
inference(cnf_transformation,[],[f12798]) ).
fof(f12982,plain,
~ v3_struct_0(sK5),
inference(cnf_transformation,[],[f12798]) ).
fof(f12983,plain,
~ m1_subset_1(k2_pre_topc(sK5),u1_struct_0(k6_lopclset(sK5))),
inference(cnf_transformation,[],[f12798]) ).
fof(f13009,plain,
! [X0] : ~ v1_xboole_0(k1_zfmisc_1(X0)),
inference(cnf_transformation,[],[f471]) ).
fof(f13048,plain,
! [X2,X0,X1] :
( m1_subset_1(X2,X1)
| ~ m2_subset_1(X2,X0,X1)
| v1_xboole_0(X0)
| v1_xboole_0(X1)
| ~ m1_subset_1(X1,k1_zfmisc_1(X0)) ),
inference(cnf_transformation,[],[f12826]) ).
fof(f13458,definition,
( spl90_1
<=> m1_subset_1(k2_pre_topc(sK5),u1_struct_0(k6_lopclset(sK5))) ),
introduced(definition,[new_symbols(definition,[spl90_1])],[avatar_definition]) ).
fof(f13460,plain,
( ~ m1_subset_1(k2_pre_topc(sK5),u1_struct_0(k6_lopclset(sK5)))
| spl90_1 ),
inference(avatar_component_clause,[],[f13458]) ).
fof(f13461,plain,
~ spl90_1,
inference(avatar_split_clause,[],[f12983,f13458]) ).
fof(f13471,plain,
( ~ m1_subset_1(k2_pre_topc(sK5),k1_lopclset(sK5))
| v3_struct_0(sK5)
| ~ v2_pre_topc(sK5)
| ~ l1_pre_topc(sK5)
| spl90_1 ),
inference(superposition,[],[f13460,f12978]) ).
fof(f13473,plain,
( ~ m1_subset_1(k2_pre_topc(sK5),k1_lopclset(sK5))
| ~ v2_pre_topc(sK5)
| ~ l1_pre_topc(sK5)
| spl90_1 ),
inference(forward_subsumption_resolution,[],[f13471,f12982]) ).
fof(f13476,plain,
( ~ m1_subset_1(k2_pre_topc(sK5),k1_lopclset(sK5))
| ~ l1_pre_topc(sK5)
| spl90_1 ),
inference(forward_subsumption_resolution,[],[f13473,f12981]) ).
fof(f13477,plain,
( ~ m1_subset_1(k2_pre_topc(sK5),k1_lopclset(sK5))
| spl90_1 ),
inference(forward_subsumption_resolution,[],[f13476,f12980]) ).
fof(f13479,definition,
( spl90_2
<=> v3_struct_0(sK5) ),
introduced(definition,[new_symbols(definition,[spl90_2])],[avatar_definition]) ).
fof(f13481,plain,
( ~ v3_struct_0(sK5)
| spl90_2 ),
inference(avatar_component_clause,[],[f13479]) ).
fof(f13482,plain,
~ spl90_2,
inference(avatar_split_clause,[],[f12982,f13479]) ).
fof(f13487,plain,
( m1_subset_1(k1_lopclset(sK5),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(sK5))))
| ~ l1_pre_topc(sK5)
| spl90_2 ),
inference(resolution,[],[f13481,f12922]) ).
fof(f13518,plain,
( ~ v1_xboole_0(k1_lopclset(sK5))
| ~ v2_pre_topc(sK5)
| ~ l1_pre_topc(sK5)
| spl90_2 ),
inference(resolution,[],[f13481,f12955]) ).
fof(f13529,plain,
( m2_subset_1(k2_pre_topc(sK5),k1_zfmisc_1(u1_struct_0(sK5)),k1_lopclset(sK5))
| ~ v2_pre_topc(sK5)
| ~ l1_pre_topc(sK5)
| spl90_2 ),
inference(resolution,[],[f13481,f12970]) ).
fof(f13670,plain,
( m2_subset_1(k2_pre_topc(sK5),k1_zfmisc_1(u1_struct_0(sK5)),k1_lopclset(sK5))
| ~ l1_pre_topc(sK5)
| spl90_2 ),
inference(forward_subsumption_resolution,[],[f13529,f12981]) ).
fof(f13681,plain,
( ~ v1_xboole_0(k1_lopclset(sK5))
| ~ l1_pre_topc(sK5)
| spl90_2 ),
inference(forward_subsumption_resolution,[],[f13518,f12981]) ).
fof(f13698,plain,
( m1_subset_1(k1_lopclset(sK5),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(sK5))))
| spl90_2 ),
inference(forward_subsumption_resolution,[],[f13487,f12980]) ).
fof(f13731,plain,
( m2_subset_1(k2_pre_topc(sK5),k1_zfmisc_1(u1_struct_0(sK5)),k1_lopclset(sK5))
| spl90_2 ),
inference(forward_subsumption_resolution,[],[f13670,f12980]) ).
fof(f13742,plain,
( ~ v1_xboole_0(k1_lopclset(sK5))
| spl90_2 ),
inference(forward_subsumption_resolution,[],[f13681,f12980]) ).
fof(f14114,definition,
( spl90_5
<=> m1_subset_1(k2_pre_topc(sK5),k1_lopclset(sK5)) ),
introduced(definition,[new_symbols(definition,[spl90_5])],[avatar_definition]) ).
fof(f14116,plain,
( ~ m1_subset_1(k2_pre_topc(sK5),k1_lopclset(sK5))
| spl90_5 ),
inference(avatar_component_clause,[],[f14114]) ).
fof(f14117,plain,
( ~ spl90_5
| spl90_1 ),
inference(avatar_split_clause,[],[f13477,f13458,f14114]) ).
fof(f16693,definition,
( spl90_25
<=> m2_subset_1(k2_pre_topc(sK5),k1_zfmisc_1(u1_struct_0(sK5)),k1_lopclset(sK5)) ),
introduced(definition,[new_symbols(definition,[spl90_25])],[avatar_definition]) ).
fof(f16695,plain,
( m2_subset_1(k2_pre_topc(sK5),k1_zfmisc_1(u1_struct_0(sK5)),k1_lopclset(sK5))
| ~ spl90_25 ),
inference(avatar_component_clause,[],[f16693]) ).
fof(f16696,plain,
( spl90_25
| spl90_2 ),
inference(avatar_split_clause,[],[f13731,f13479,f16693]) ).
fof(f16707,plain,
( m1_subset_1(k2_pre_topc(sK5),k1_lopclset(sK5))
| v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK5)))
| v1_xboole_0(k1_lopclset(sK5))
| ~ m1_subset_1(k1_lopclset(sK5),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(sK5))))
| ~ spl90_25 ),
inference(resolution,[],[f16695,f13048]) ).
fof(f16713,plain,
( v1_xboole_0(k1_zfmisc_1(u1_struct_0(sK5)))
| v1_xboole_0(k1_lopclset(sK5))
| ~ m1_subset_1(k1_lopclset(sK5),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(sK5))))
| spl90_5
| ~ spl90_25 ),
inference(forward_subsumption_resolution,[],[f16707,f14116]) ).
fof(f16724,plain,
( v1_xboole_0(k1_lopclset(sK5))
| ~ m1_subset_1(k1_lopclset(sK5),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(sK5))))
| spl90_5
| ~ spl90_25 ),
inference(forward_subsumption_resolution,[],[f16713,f13009]) ).
fof(f16735,plain,
( ~ m1_subset_1(k1_lopclset(sK5),k1_zfmisc_1(k1_zfmisc_1(u1_struct_0(sK5))))
| spl90_2
| spl90_5
| ~ spl90_25 ),
inference(forward_subsumption_resolution,[],[f16724,f13742]) ).
fof(f16746,plain,
( $false
| spl90_2
| spl90_5
| ~ spl90_25 ),
inference(forward_subsumption_resolution,[],[f16735,f13698]) ).
fof(f16747,plain,
( spl90_2
| spl90_5
| ~ spl90_25 ),
inference(avatar_contradiction_clause,[],[f16746]) ).
cnf(s1,plain,
~ spl90_1,
inference(sat_conversion,[],[f13461]) ).
cnf(s2,plain,
~ spl90_2,
inference(sat_conversion,[],[f13482]) ).
cnf(s5,plain,
( spl90_1
| ~ spl90_5 ),
inference(sat_conversion,[],[f14117]) ).
cnf(s24,plain,
( spl90_2
| spl90_25 ),
inference(sat_conversion,[],[f16696]) ).
cnf(s25,plain,
( spl90_2
| spl90_5
| ~ spl90_25 ),
inference(sat_conversion,[],[f16747]) ).
cnf(s31,plain,
spl90_25,
inference(rat,[],[s24,s2]) ).
cnf(s45,plain,
spl90_5,
inference(rat,[],[s25,s2,s31]) ).
cnf(s46,plain,
spl90_1,
inference(rat,[],[s5,s45]) ).
cnf(s47,plain,
$false,
inference(rat,[],[s1,s46]) ).
fof(f16776,plain,
$false,
inference(avatar_sat_refutation,[],[s47]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT286+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.36 % Computer : n011.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sun Sep 27 14:15:32 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.10/0.40 Running first-order theorem proving
% 0.10/0.40 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
% 10.68/2.96 % (2460578)Detected formulas, will run a generic FOF schedule.
% 10.68/2.96 % (2460589)dis-21_1_sil=8000:lcm=predicate:random_seed=409061545:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2993 on theBenchmark for (2993ds/129Mi)
% 10.68/2.96 % (2460585)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=1128748355:i=141695:sd=1:nm=32:gsp=on:ss=included_2993 on theBenchmark for (2993ds/141695Mi)
% 10.68/2.96 % (2460584)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=2001293848:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2993 on theBenchmark for (2993ds/134677Mi)
% 10.68/2.96 % (2460583)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=4059425535:i=141193_2993 on theBenchmark for (2993ds/141193Mi)
% 10.68/2.96 % (2460586)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=4051870616:i=109:sd=1:ins=1:gsp=on:ss=axioms_2993 on theBenchmark for (2993ds/109Mi)
% 10.68/2.96 % (2460587)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1700281680:i=119:av=off:ss=axioms_2993 on theBenchmark for (2993ds/119Mi)
% 10.68/2.96 % (2460588)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3014650012:s2a=on:i=139:gtg=position_2993 on theBenchmark for (2993ds/139Mi)
% 10.68/2.96 % (2460589)Instruction limit reached!
% 10.68/2.96 % (2460589)------------------------------
% 10.68/2.96 % (2460589)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.68/2.96 % (2460589)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.68/2.96 % (2460589)CaDiCaL version: 2.1.3
% 10.68/2.96 % (2460589)Termination reason: Instruction limit
% 10.68/2.96 % (2460589)Termination phase: Preprocessing 1
% 10.68/2.96 % (2460589)Time elapsed: 0.058 s
% 10.68/2.96 % (2460589)Peak memory usage: 102 MB
% 10.68/2.96 % (2460589)Instructions burned: 130 (million)
% 10.68/2.96 % (2460586)Refutation not found, incomplete strategy
% 10.68/2.96 % (2460586)------------------------------
% 10.68/2.96 % (2460586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.68/2.96 % (2460586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.68/2.96 % (2460586)CaDiCaL version: 2.1.3
% 10.68/2.96 % (2460586)Termination reason: Refutation not found, incomplete strategy
% 10.68/2.96 % (2460586)Time elapsed: 0.058 s
% 10.68/2.96 % (2460586)Peak memory usage: 105 MB
% 10.68/2.96 % (2460586)Instructions burned: 70 (million)
% 10.68/2.96 % (2460588)Instruction limit reached!
% 10.68/2.96 % (2460588)------------------------------
% 10.68/2.96 % (2460588)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.68/2.96 % (2460588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.68/2.96 % (2460588)CaDiCaL version: 2.1.3
% 10.68/2.96 % (2460588)Termination reason: Instruction limit
% 10.68/2.96 % (2460588)Termination phase: Property scanning
% 10.68/2.96 % (2460588)Time elapsed: 0.059 s
% 10.68/2.96 % (2460588)Peak memory usage: 101 MB
% 10.68/2.96 % (2460588)Instructions burned: 141 (million)
% 10.68/2.96 % (2460587)Instruction limit reached!
% 10.68/2.96 % (2460587)------------------------------
% 10.68/2.96 % (2460587)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.68/2.96 % (2460587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.68/2.96 % (2460587)CaDiCaL version: 2.1.3
% 10.68/2.96 % (2460587)Termination reason: Instruction limit
% 10.68/2.96 % (2460587)Termination phase: Saturation
% 10.68/2.96 % (2460587)Time elapsed: 0.088 s
% 10.68/2.96 % (2460587)Peak memory usage: 104 MB
% 10.68/2.96 % (2460587)Instructions burned: 121 (million)
% 10.68/2.96 % (2460597)lrs+10_1_sil=8000:sp=occurrence:random_seed=3273109045:i=285:sd=3:ss=axioms:sgt=8_2992 on theBenchmark for (2992ds/285Mi)
% 10.68/2.96 % (2460599)lrs+1011_1_sil=32000:sp=occurrence:random_seed=72120617:i=325:sd=1:ss=axioms:sgt=32_2991 on theBenchmark for (2991ds/325Mi)
% 10.68/2.96 % (2460598)lrs+10_1_sil=32000:urr=on:br=off:random_seed=328215906:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2991 on theBenchmark for (2991ds/157Mi)
% 10.68/2.96 % (2460597)Instruction limit reached!
% 10.68/2.96 % (2460597)------------------------------
% 10.68/2.96 % (2460597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.68/2.96 % (2460597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.68/2.96 % (2460597)CaDiCaL version: 2.1.3
% 10.68/2.96 % (2460597)Termination reason: Instruction limit
% 10.68/2.96 % (2460597)Termination phase: Saturation
% 10.68/2.96 % (2460597)Time elapsed: 0.113 s
% 10.68/2.96 % (2460597)Peak memory usage: 108 MB
% 10.68/2.96 % (2460597)Instructions burned: 286 (million)
% 10.68/2.96 % (2460598)Instruction limit reached!
% 10.68/2.96 % (2460598)------------------------------
% 10.68/2.96 % (2460598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.68/2.96 % (2460598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.68/2.96 % (2460598)CaDiCaL version: 2.1.3
% 10.68/2.96 % (2460598)Termination reason: Instruction limit
% 10.68/2.96 % (2460598)Termination phase: SInE selection
% 10.68/2.96 % (2460598)Time elapsed: 0.056 s
% 10.68/2.96 % (2460598)Peak memory usage: 101 MB
% 10.68/2.96 % (2460598)Instructions burned: 158 (million)
% 10.68/2.96 % (2460599)Refutation not found, incomplete strategy
% 10.68/2.96 % (2460599)------------------------------
% 10.68/2.96 % (2460599)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.68/2.96 % (2460599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.68/2.96 % (2460599)CaDiCaL version: 2.1.3
% 10.68/2.96 % (2460599)Termination reason: Refutation not found, incomplete strategy
% 10.68/2.96 % (2460599)Time elapsed: 0.059 s
% 10.68/2.96 % (2460586)------------------------------
% 10.68/2.96 % (2460586)------------------------------
% 10.68/2.96 % (2460599)Peak memory usage: 105 MB
% 10.68/2.96 % (2460599)Instructions burned: 68 (million)
% 10.68/2.96 % (2460603)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=2818790500:s2a=on:i=248:s2at=1.23:gtg=position_2989 on theBenchmark for (2989ds/248Mi)
% 10.68/2.96 % (2460604)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=285010180:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2989 on theBenchmark for (2989ds/294Mi)
% 10.68/2.96 % (2460605)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2953180907:i=2350_2989 on theBenchmark for (2989ds/2350Mi)
% 10.68/2.96 % (2460604)Instruction limit reached!
% 10.68/2.96 % (2460604)------------------------------
% 10.68/2.96 % (2460604)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.68/2.96 % (2460604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.68/2.96 % (2460604)CaDiCaL version: 2.1.3
% 10.68/2.96 % (2460604)Termination reason: Instruction limit
% 10.68/2.96 % (2460604)Termination phase: Saturation
% 10.68/2.96 % (2460604)Time elapsed: 0.102 s
% 10.68/2.96 % (2460604)Peak memory usage: 108 MB
% 10.68/2.96 % (2460604)Instructions burned: 295 (million)
% 10.68/2.96 % (2460599)------------------------------
% 10.68/2.96 % (2460599)------------------------------
% 10.68/2.96 % (2460603)Instruction limit reached!
% 10.68/2.96 % (2460603)------------------------------
% 10.68/2.96 % (2460603)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.68/2.96 % (2460603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.68/2.96 % (2460603)CaDiCaL version: 2.1.3
% 10.68/2.96 % (2460603)Termination reason: Instruction limit
% 10.68/2.96 % (2460603)Termination phase: SInE selection
% 10.68/2.96 % (2460603)Time elapsed: 0.134 s
% 10.68/2.96 % (2460603)Peak memory usage: 101 MB
% 10.68/2.96 % (2460603)Instructions burned: 248 (million)
% 10.68/2.96 % (2460609)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1330577585:cts=off:i=113:fsr=off:ss=included:sgt=4_2986 on theBenchmark for (2986ds/113Mi)
% 10.68/2.96 % (2460609)Instruction limit reached!
% 10.68/2.96 % (2460609)------------------------------
% 10.68/2.96 % (2460609)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.68/2.96 % (2460609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.68/2.96 % (2460609)CaDiCaL version: 2.1.3
% 10.68/2.96 % (2460609)Termination reason: Instruction limit
% 10.68/2.96 % (2460609)Termination phase: Preprocessing 3
% 10.68/2.96 % (2460609)Time elapsed: 0.058 s
% 10.68/2.96 % (2460609)Peak memory usage: 104 MB
% 10.68/2.96 % (2460609)Instructions burned: 115 (million)
% 10.68/2.96 % (2460611)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3932106962:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2986 on theBenchmark for (2986ds/114Mi)
% 10.68/2.96 % (2460610)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3091856972:i=127:av=off:fsr=off:sup=off_2986 on theBenchmark for (2986ds/127Mi)
% 10.68/2.96 % (2460611)Instruction limit reached!
% 10.68/2.96 % (2460611)------------------------------
% 10.68/2.96 % (2460611)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.68/2.96 % (2460611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.68/2.96 % (2460611)CaDiCaL version: 2.1.3
% 10.68/2.96 % (2460611)Termination reason: Instruction limit
% 10.68/2.96 % (2460611)Termination phase: Property scanning
% 10.68/2.96 % (2460611)Time elapsed: 0.049 s
% 10.68/2.96 % (2460611)Peak memory usage: 100 MB
% 10.68/2.96 % (2460611)Instructions burned: 116 (million)
% 10.68/2.96 % (2460610)Instruction limit reached!
% 10.68/2.96 % (2460610)------------------------------
% 10.68/2.96 % (2460610)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.68/2.96 % (2460610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.68/2.96 % (2460610)CaDiCaL version: 2.1.3
% 10.68/2.96 % (2460610)Termination reason: Instruction limit
% 10.68/2.96 % (2460610)Termination phase: Preprocessing 2
% 10.68/2.96 % (2460610)Time elapsed: 0.106 s
% 10.68/2.96 % (2460610)Peak memory usage: 107 MB
% 10.68/2.96 % (2460610)Instructions burned: 127 (million)
% 10.68/2.96 % (2460615)lrs+10_1_sil=8000:sp=occurrence:random_seed=2376762206:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2985 on theBenchmark for (2985ds/907Mi)
% 10.68/2.96 % (2460616)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1750640986:i=437:sd=1:aac=none:ss=included_2984 on theBenchmark for (2984ds/437Mi)
% 10.68/2.96 % (2460617)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=300625526:i=5202:ss=axioms:sgt=16_2984 on theBenchmark for (2984ds/5202Mi)
% 10.68/2.96 % (2460616)Refutation not found, incomplete strategy
% 10.68/2.96 % (2460616)------------------------------
% 10.68/2.96 % (2460616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.68/2.96 % (2460616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.68/2.96 % (2460616)CaDiCaL version: 2.1.3
% 10.68/2.96 % (2460616)Termination reason: Refutation not found, incomplete strategy
% 10.68/2.96 % (2460616)Time elapsed: 0.078 s
% 10.68/2.96 % (2460616)Peak memory usage: 106 MB
% 10.68/2.96 % (2460616)Instructions burned: 101 (million)
% 10.68/2.96 % (2460585)First to succeed.
% 10.68/2.96 % (2460585)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2460578"
% 10.68/2.96 % (2460615)Instruction limit reached!
% 10.68/2.96 % (2460615)------------------------------
% 10.68/2.96 % (2460615)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.68/2.96 % (2460615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.68/2.96 % (2460615)CaDiCaL version: 2.1.3
% 10.68/2.96 % (2460615)Termination reason: Instruction limit
% 10.68/2.96 % (2460615)Termination phase: Saturation
% 10.68/2.96 % (2460615)Time elapsed: 0.309 s
% 10.68/2.96 % (2460615)Peak memory usage: 119 MB
% 10.68/2.96 % (2460615)Instructions burned: 909 (million)
% 10.68/2.96 % (2460616)------------------------------
% 10.68/2.96 % (2460616)------------------------------
% 10.68/2.96 % (2460621)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3673786464:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2980 on theBenchmark for (2980ds/134Mi)
% 10.68/2.96 % (2460585)Refutation found. Thanks to Tanya!
% 10.68/2.96 % SZS status Theorem for theBenchmark
% 10.68/2.96 % SZS output start Proof for theBenchmark
% See solution above
% 11.87/3.16 % (2460585)------------------------------
% 11.87/3.16 % (2460585)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.87/3.16 % (2460585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.87/3.16 % (2460585)CaDiCaL version: 2.1.3
% 11.87/3.16 % (2460585)Termination reason: Refutation
% 11.87/3.16 % (2460585)Time elapsed: 1.066 s
% 11.87/3.16 % (2460585)Peak memory usage: 158 MB
% 11.87/3.16 % (2460585)Instructions burned: 1621 (million)
% 11.87/3.16 % (2460585)------------------------------
% 11.87/3.16 % (2460585)------------------------------
% 11.87/3.16 % (2460578)Success in time 2.115 s
% 11.87/3.16 % Vampire exiting
%------------------------------------------------------------------------------