%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CSR212+1 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n017.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:44:06 AM UTC 2026
% Result : Theorem 12.30s 2.68s
% Output : Refutation 13.95s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 17
% Syntax : Number of formulae : 90 ( 23 unt; 2 def)
% Number of atoms : 217 ( 0 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 237 ( 110 ~; 99 |; 21 &)
% ( 2 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 7 ( 6 usr; 3 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 13 con; 0-1 aty)
% Number of variables : 76 ( 0 sgn 66 !; 10 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [X0,X1,X2] :
( ( p__d__subclass(X0,X1)
& p__d__subclass(X1,X2) )
=> p__d__subclass(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',predefinitionsA8) ).
fof(f4,axiom,
! [X0,X1,X2] :
( ( p__d__instance(X0,X1)
& p__d__subclass(X1,X2) )
=> p__d__instance(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',predefinitionsA12) ).
fof(f110,axiom,
! [X0] :
( p__d__subclass(X0,c__Entity)
=> ? [X1] : p__d__instance(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA176) ).
fof(f112,axiom,
p__d__subclass(c__Physical,c__Entity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA178) ).
fof(f115,axiom,
p__d__subclass(c__Object,c__Physical),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA181) ).
fof(f225,axiom,
p__d__subclass(c__Agent,c__Object),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA312) ).
fof(f229,axiom,
p__d__subclass(c__LegalAgent,c__Agent),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA316) ).
fof(f1791,axiom,
p__d__subclass(c__Selling,c__FinancialTransaction),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA2559) ).
fof(f2336,axiom,
p__d__subclass(c__Corporation,c__LegalAgent),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA3224) ).
fof(f2338,axiom,
p__d__subclass(c__MercantileOrganization,c__Corporation),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',mergeA3227) ).
fof(f3598,axiom,
p__d__subclass(c__RetailStore,c__MercantileOrganization),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',miloA1186) ).
fof(f3602,axiom,
p__d__subclass(c__DrugStore,c__RetailStore),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',miloA1190) ).
fof(f3603,axiom,
! [X0] :
( p__d__instance(X0,c__DrugStore)
=> ? [X1,X2] :
( p__d__instance(X1,c__Selling)
& p__agent(X1,X0)
& p__patient(X1,X2)
& p__d__instance(X2,c__Medicine) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',miloA1191) ).
fof(f6883,axiom,
! [X0,X1] :
( p__agent(X0,X1)
=> ( p__d__instance(X1,c__Agent)
& p__d__instance(X0,c__Process) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',typeA30) ).
fof(f7433,conjecture,
? [X0,X1] :
( p__d__instance(X0,c__Process)
& p__d__instance(X1,c__Agent)
& p__d__instance(X0,c__FinancialTransaction)
& p__d__instance(X1,c__LegalAgent)
& p__agent(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',agentRelation0444) ).
fof(f7434,negated_conjecture,
~ ? [X0,X1] :
( p__d__instance(X0,c__Process)
& p__d__instance(X1,c__Agent)
& p__d__instance(X0,c__FinancialTransaction)
& p__d__instance(X1,c__LegalAgent)
& p__agent(X0,X1) ),
inference(negated_conjecture,[status(cth)],[f7433]) ).
fof(f7561,plain,
! [X0,X1] :
( ~ p__d__instance(X0,c__Process)
| ~ p__d__instance(X1,c__Agent)
| ~ p__d__instance(X0,c__FinancialTransaction)
| ~ p__d__instance(X1,c__LegalAgent)
| ~ p__agent(X0,X1) ),
inference(ennf_transformation,[],[f7434]) ).
fof(f7562,plain,
! [X0,X1,X2] :
( p__d__instance(X0,X2)
| ~ p__d__instance(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(ennf_transformation,[],[f4]) ).
fof(f7563,plain,
! [X0,X1,X2] :
( p__d__instance(X0,X2)
| ~ p__d__instance(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(flattening,[],[f7562]) ).
fof(f7564,plain,
! [X0,X1] :
( ( p__d__instance(X1,c__Agent)
& p__d__instance(X0,c__Process) )
| ~ p__agent(X0,X1) ),
inference(ennf_transformation,[],[f6883]) ).
fof(f7605,plain,
! [X0,X1,X2] :
( p__d__subclass(X0,X2)
| ~ p__d__subclass(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(ennf_transformation,[],[f2]) ).
fof(f7606,plain,
! [X0,X1,X2] :
( p__d__subclass(X0,X2)
| ~ p__d__subclass(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(flattening,[],[f7605]) ).
fof(f7920,plain,
! [X0] :
( ? [X1,X2] :
( p__d__instance(X1,c__Selling)
& p__agent(X1,X0)
& p__patient(X1,X2)
& p__d__instance(X2,c__Medicine) )
| ~ p__d__instance(X0,c__DrugStore) ),
inference(ennf_transformation,[],[f3603]) ).
fof(f8855,plain,
! [X0] :
( ? [X1] : p__d__instance(X1,X0)
| ~ p__d__subclass(X0,c__Entity) ),
inference(ennf_transformation,[],[f110]) ).
fof(f9221,plain,
! [X0] :
( ( p__d__instance(sK148(X0),c__Selling)
& p__agent(sK148(X0),X0)
& p__patient(sK148(X0),sK149(X0))
& p__d__instance(sK149(X0),c__Medicine) )
| ~ p__d__instance(X0,c__DrugStore) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK148,sK149]),skolemize(X1,sK148(X0)),skolemize(X2,sK149(X0))],[f7920]) ).
fof(f9637,plain,
! [X0] :
( p__d__instance(sK544(X0),X0)
| ~ p__d__subclass(X0,c__Entity) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK544]),skolemize(X1,sK544(X0))],[f8855]) ).
fof(f9726,plain,
! [X0,X1] :
( ~ p__d__instance(X0,c__Process)
| ~ p__d__instance(X1,c__Agent)
| ~ p__d__instance(X0,c__FinancialTransaction)
| ~ p__d__instance(X1,c__LegalAgent)
| ~ p__agent(X0,X1) ),
inference(cnf_transformation,[],[f7561]) ).
fof(f9727,plain,
! [X2,X0,X1] :
( p__d__instance(X0,X2)
| ~ p__d__instance(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(cnf_transformation,[],[f7563]) ).
fof(f9728,plain,
! [X0,X1] :
( ~ p__agent(X0,X1)
| p__d__instance(X0,c__Process) ),
inference(cnf_transformation,[],[f7564]) ).
fof(f9729,plain,
! [X0,X1] :
( ~ p__agent(X0,X1)
| p__d__instance(X1,c__Agent) ),
inference(cnf_transformation,[],[f7564]) ).
fof(f9777,plain,
p__d__subclass(c__Agent,c__Object),
inference(cnf_transformation,[],[f225]) ).
fof(f9780,plain,
p__d__subclass(c__Corporation,c__LegalAgent),
inference(cnf_transformation,[],[f2336]) ).
fof(f9781,plain,
p__d__subclass(c__LegalAgent,c__Agent),
inference(cnf_transformation,[],[f229]) ).
fof(f9792,plain,
p__d__subclass(c__Selling,c__FinancialTransaction),
inference(cnf_transformation,[],[f1791]) ).
fof(f9801,plain,
! [X2,X0,X1] :
( p__d__subclass(X0,X2)
| ~ p__d__subclass(X0,X1)
| ~ p__d__subclass(X1,X2) ),
inference(cnf_transformation,[],[f7606]) ).
fof(f9902,plain,
p__d__subclass(c__Object,c__Physical),
inference(cnf_transformation,[],[f115]) ).
fof(f10318,plain,
p__d__subclass(c__MercantileOrganization,c__Corporation),
inference(cnf_transformation,[],[f2338]) ).
fof(f10382,plain,
! [X0] :
( p__agent(sK148(X0),X0)
| ~ p__d__instance(X0,c__DrugStore) ),
inference(cnf_transformation,[],[f9221]) ).
fof(f10383,plain,
! [X0] :
( p__d__instance(sK148(X0),c__Selling)
| ~ p__d__instance(X0,c__DrugStore) ),
inference(cnf_transformation,[],[f9221]) ).
fof(f10510,plain,
p__d__subclass(c__DrugStore,c__RetailStore),
inference(cnf_transformation,[],[f3602]) ).
fof(f10512,plain,
p__d__subclass(c__RetailStore,c__MercantileOrganization),
inference(cnf_transformation,[],[f3598]) ).
fof(f12683,plain,
p__d__subclass(c__Physical,c__Entity),
inference(cnf_transformation,[],[f112]) ).
fof(f12684,plain,
! [X0] :
( p__d__instance(sK544(X0),X0)
| ~ p__d__subclass(X0,c__Entity) ),
inference(cnf_transformation,[],[f9637]) ).
fof(f13264,plain,
! [X0,X1] :
( ~ p__d__instance(X1,c__Agent)
| ~ p__d__instance(X0,c__FinancialTransaction)
| ~ p__d__instance(X1,c__LegalAgent)
| ~ p__agent(X0,X1) ),
inference(forward_subsumption_resolution,[],[f9726,f9728]) ).
fof(f13265,plain,
! [X0,X1] :
( ~ p__agent(X0,X1)
| ~ p__d__instance(X1,c__LegalAgent)
| ~ p__d__instance(X0,c__FinancialTransaction) ),
inference(forward_subsumption_resolution,[],[f13264,f9729]) ).
fof(f13295,plain,
! [X0] :
( ~ p__d__instance(sK148(X0),c__FinancialTransaction)
| ~ p__d__instance(X0,c__LegalAgent)
| ~ p__d__instance(X0,c__DrugStore) ),
inference(resolution,[],[f13265,f10382]) ).
fof(f13366,plain,
! [X0,X1] :
( ~ p__d__instance(sK148(X0),X1)
| ~ p__d__instance(X0,c__DrugStore)
| ~ p__d__instance(X0,c__LegalAgent)
| ~ p__d__subclass(X1,c__FinancialTransaction) ),
inference(resolution,[],[f13295,f9727]) ).
fof(f14311,plain,
! [X0] :
( ~ p__d__instance(X0,c__DrugStore)
| ~ p__d__instance(X0,c__LegalAgent)
| ~ p__d__subclass(c__Selling,c__FinancialTransaction)
| ~ p__d__instance(X0,c__DrugStore) ),
inference(resolution,[],[f13366,f10383]) ).
fof(f14323,plain,
! [X0] :
( ~ p__d__instance(X0,c__DrugStore)
| ~ p__d__instance(X0,c__LegalAgent)
| ~ p__d__subclass(c__Selling,c__FinancialTransaction) ),
inference(duplicate_literal_removal,[],[f14311]) ).
fof(f14324,plain,
! [X0] :
( ~ p__d__instance(X0,c__DrugStore)
| ~ p__d__instance(X0,c__LegalAgent) ),
inference(forward_subsumption_resolution,[],[f14323,f9792]) ).
fof(f14333,plain,
( ~ p__d__instance(sK544(c__DrugStore),c__LegalAgent)
| ~ p__d__subclass(c__DrugStore,c__Entity) ),
inference(resolution,[],[f14324,f12684]) ).
fof(f14351,definition,
( spl600_29
<=> p__d__subclass(c__DrugStore,c__Entity) ),
introduced(definition,[new_symbols(definition,[spl600_29])],[avatar_definition]) ).
fof(f14352,plain,
( p__d__subclass(c__DrugStore,c__Entity)
| ~ spl600_29 ),
inference(avatar_component_clause,[],[f14351]) ).
fof(f14353,plain,
( ~ p__d__subclass(c__DrugStore,c__Entity)
| spl600_29 ),
inference(avatar_component_clause,[],[f14351]) ).
fof(f14355,definition,
( spl600_30
<=> p__d__instance(sK544(c__DrugStore),c__LegalAgent) ),
introduced(definition,[new_symbols(definition,[spl600_30])],[avatar_definition]) ).
fof(f14357,plain,
( ~ p__d__instance(sK544(c__DrugStore),c__LegalAgent)
| spl600_30 ),
inference(avatar_component_clause,[],[f14355]) ).
fof(f14358,plain,
( ~ spl600_29
| ~ spl600_30 ),
inference(avatar_split_clause,[],[f14333,f14355,f14351]) ).
fof(f14359,plain,
( ! [X0] :
( ~ p__d__subclass(c__DrugStore,X0)
| ~ p__d__subclass(X0,c__Entity) )
| spl600_29 ),
inference(resolution,[],[f14353,f9801]) ).
fof(f14362,plain,
( ~ p__d__subclass(c__RetailStore,c__Entity)
| spl600_29 ),
inference(resolution,[],[f14359,f10510]) ).
fof(f14363,plain,
( ! [X0] :
( ~ p__d__subclass(c__RetailStore,X0)
| ~ p__d__subclass(X0,c__Entity) )
| spl600_29 ),
inference(resolution,[],[f14362,f9801]) ).
fof(f14366,plain,
( ~ p__d__subclass(c__MercantileOrganization,c__Entity)
| spl600_29 ),
inference(resolution,[],[f14363,f10512]) ).
fof(f14384,plain,
( ! [X0] :
( ~ p__d__subclass(c__MercantileOrganization,X0)
| ~ p__d__subclass(X0,c__Entity) )
| spl600_29 ),
inference(resolution,[],[f14366,f9801]) ).
fof(f14409,plain,
( ~ p__d__subclass(c__Corporation,c__Entity)
| spl600_29 ),
inference(resolution,[],[f14384,f10318]) ).
fof(f14410,plain,
( ! [X0] :
( ~ p__d__subclass(c__Corporation,X0)
| ~ p__d__subclass(X0,c__Entity) )
| spl600_29 ),
inference(resolution,[],[f14409,f9801]) ).
fof(f14413,plain,
( ~ p__d__subclass(c__LegalAgent,c__Entity)
| spl600_29 ),
inference(resolution,[],[f14410,f9780]) ).
fof(f14415,plain,
( ! [X0] :
( ~ p__d__subclass(c__LegalAgent,X0)
| ~ p__d__subclass(X0,c__Entity) )
| spl600_29 ),
inference(resolution,[],[f14413,f9801]) ).
fof(f14419,plain,
( ~ p__d__subclass(c__Agent,c__Entity)
| spl600_29 ),
inference(resolution,[],[f14415,f9781]) ).
fof(f14436,plain,
( ! [X0] :
( ~ p__d__subclass(c__Agent,X0)
| ~ p__d__subclass(X0,c__Entity) )
| spl600_29 ),
inference(resolution,[],[f14419,f9801]) ).
fof(f14466,plain,
( ~ p__d__subclass(c__Object,c__Entity)
| spl600_29 ),
inference(resolution,[],[f14436,f9777]) ).
fof(f14467,plain,
( ! [X0] :
( ~ p__d__subclass(c__Object,X0)
| ~ p__d__subclass(X0,c__Entity) )
| spl600_29 ),
inference(resolution,[],[f14466,f9801]) ).
fof(f14515,plain,
( ~ p__d__subclass(c__Physical,c__Entity)
| spl600_29 ),
inference(resolution,[],[f14467,f9902]) ).
fof(f14516,plain,
( $false
| spl600_29 ),
inference(forward_subsumption_resolution,[],[f14515,f12683]) ).
fof(f14517,plain,
spl600_29,
inference(avatar_contradiction_clause,[],[f14516]) ).
fof(f14518,plain,
( ! [X0] :
( ~ p__d__instance(sK544(c__DrugStore),X0)
| ~ p__d__subclass(X0,c__LegalAgent) )
| spl600_30 ),
inference(resolution,[],[f14357,f9727]) ).
fof(f14853,plain,
( ~ p__d__subclass(c__DrugStore,c__LegalAgent)
| ~ p__d__subclass(c__DrugStore,c__Entity)
| spl600_30 ),
inference(resolution,[],[f14518,f12684]) ).
fof(f14865,plain,
( ~ p__d__subclass(c__DrugStore,c__LegalAgent)
| ~ spl600_29
| spl600_30 ),
inference(forward_subsumption_resolution,[],[f14853,f14352]) ).
fof(f14879,plain,
( ! [X0] :
( ~ p__d__subclass(c__DrugStore,X0)
| ~ p__d__subclass(X0,c__LegalAgent) )
| ~ spl600_29
| spl600_30 ),
inference(resolution,[],[f14865,f9801]) ).
fof(f14883,plain,
( ~ p__d__subclass(c__RetailStore,c__LegalAgent)
| ~ spl600_29
| spl600_30 ),
inference(resolution,[],[f14879,f10510]) ).
fof(f14884,plain,
( ! [X0] :
( ~ p__d__subclass(c__RetailStore,X0)
| ~ p__d__subclass(X0,c__LegalAgent) )
| ~ spl600_29
| spl600_30 ),
inference(resolution,[],[f14883,f9801]) ).
fof(f14887,plain,
( ~ p__d__subclass(c__MercantileOrganization,c__LegalAgent)
| ~ spl600_29
| spl600_30 ),
inference(resolution,[],[f14884,f10512]) ).
fof(f14888,plain,
( ! [X0] :
( ~ p__d__subclass(c__MercantileOrganization,X0)
| ~ p__d__subclass(X0,c__LegalAgent) )
| ~ spl600_29
| spl600_30 ),
inference(resolution,[],[f14887,f9801]) ).
fof(f14891,plain,
( ~ p__d__subclass(c__Corporation,c__LegalAgent)
| ~ spl600_29
| spl600_30 ),
inference(resolution,[],[f14888,f10318]) ).
fof(f14892,plain,
( $false
| ~ spl600_29
| spl600_30 ),
inference(forward_subsumption_resolution,[],[f14891,f9780]) ).
fof(f14893,plain,
( ~ spl600_29
| spl600_30 ),
inference(avatar_contradiction_clause,[],[f14892]) ).
cnf(s20,plain,
( ~ spl600_29
| ~ spl600_30 ),
inference(sat_conversion,[],[f14358]) ).
cnf(s21,plain,
spl600_29,
inference(sat_conversion,[],[f14517]) ).
cnf(s30,plain,
( ~ spl600_29
| spl600_30 ),
inference(sat_conversion,[],[f14893]) ).
cnf(s35,plain,
spl600_30,
inference(rat,[],[s30,s21]) ).
cnf(s36,plain,
$false,
inference(rat,[],[s20,s35,s21]) ).
fof(f14894,plain,
$false,
inference(avatar_sat_refutation,[],[s36]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR212+1 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.18 % Computer : n017.cluster.edu
% 0.07/0.18 % Model : x86_64 x86_64
% 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.18 % Memory : 8046.5625MB
% 0.07/0.18 % OS : Linux 6.8.0-71-generic
% 0.07/0.18 % CPULimit : 300
% 0.07/0.18 % WCLimit : 300
% 0.07/0.18 % DateTime : Mon Sep 28 23:40:37 UTC 2026
% 0.07/0.18 % CPUTime :
% 0.07/0.18 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.22 Running first-order theorem proving
% 0.07/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
% 10.29/2.30 % (4135361)Detected formulas, will run a generic FOF schedule.
% 10.29/2.30 % (4135372)dis-21_1_sil=8000:lcm=predicate:random_seed=2192691864:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2998 on theBenchmark for (2998ds/129Mi)
% 10.29/2.30 % (4135372)Instruction limit reached!
% 10.29/2.30 % (4135372)------------------------------
% 10.29/2.30 % (4135372)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.29/2.30 % (4135372)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.29/2.30 % (4135372)CaDiCaL version: 2.1.3
% 10.29/2.30 % (4135372)Termination reason: Instruction limit
% 10.29/2.30 % (4135372)Termination phase: Saturation
% 10.29/2.30 % (4135372)Time elapsed: 0.042 s
% 10.29/2.30 % (4135372)Peak memory usage: 95 MB
% 10.29/2.30 % (4135372)Instructions burned: 130 (million)
% 10.29/2.30 % (4135371)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2562337302:s2a=on:i=139:gtg=position_2998 on theBenchmark for (2998ds/139Mi)
% 10.29/2.30 % (4135366)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=3584813843:i=141193_2998 on theBenchmark for (2998ds/141193Mi)
% 10.29/2.30 % (4135370)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1450295940:i=119:av=off:ss=axioms_2998 on theBenchmark for (2998ds/119Mi)
% 10.29/2.30 % (4135367)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=2573019641:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2998 on theBenchmark for (2998ds/134677Mi)
% 10.29/2.30 % (4135368)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=1216294274:i=141695:sd=1:nm=32:gsp=on:ss=included_2998 on theBenchmark for (2998ds/141695Mi)
% 10.29/2.30 % (4135369)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=854496005:i=109:sd=1:ins=1:gsp=on:ss=axioms_2998 on theBenchmark for (2998ds/109Mi)
% 10.29/2.30 % (4135369)Refutation not found, incomplete strategy
% 10.29/2.30 % (4135369)------------------------------
% 10.29/2.30 % (4135369)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.29/2.30 % (4135369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.29/2.30 % (4135369)CaDiCaL version: 2.1.3
% 10.29/2.30 % (4135369)Termination reason: Refutation not found, incomplete strategy
% 10.29/2.30 % (4135369)Time elapsed: 0.016 s
% 10.29/2.30 % (4135369)Peak memory usage: 93 MB
% 10.29/2.30 % (4135369)Instructions burned: 24 (million)
% 10.29/2.30 % (4135370)Instruction limit reached!
% 10.29/2.30 % (4135370)------------------------------
% 10.29/2.30 % (4135370)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.29/2.30 % (4135370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.29/2.30 % (4135370)CaDiCaL version: 2.1.3
% 10.29/2.30 % (4135370)Termination reason: Instruction limit
% 10.29/2.30 % (4135370)Termination phase: Saturation
% 10.29/2.30 % (4135370)Time elapsed: 0.069 s
% 10.29/2.30 % (4135370)Peak memory usage: 93 MB
% 10.29/2.30 % (4135370)Instructions burned: 121 (million)
% 10.29/2.30 % (4135380)lrs+10_1_sil=8000:sp=occurrence:random_seed=221196662:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi)
% 10.29/2.30 % (4135371)Instruction limit reached!
% 10.29/2.30 % (4135371)------------------------------
% 10.29/2.30 % (4135371)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.29/2.30 % (4135371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.29/2.30 % (4135371)CaDiCaL version: 2.1.3
% 10.29/2.30 % (4135371)Termination reason: Instruction limit
% 10.29/2.30 % (4135371)Termination phase: Preprocessing 3
% 10.29/2.30 % (4135371)Time elapsed: 0.095 s
% 10.29/2.30 % (4135371)Peak memory usage: 94 MB
% 10.29/2.30 % (4135371)Instructions burned: 140 (million)
% 10.29/2.30 % (4135380)Refutation not found, incomplete strategy
% 10.29/2.30 % (4135380)------------------------------
% 10.29/2.30 % (4135380)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.29/2.30 % (4135380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.29/2.30 % (4135380)CaDiCaL version: 2.1.3
% 10.29/2.30 % (4135380)Termination reason: Refutation not found, incomplete strategy
% 10.29/2.30 % (4135380)Time elapsed: 0.017 s
% 10.29/2.30 % (4135380)Peak memory usage: 95 MB
% 10.29/2.30 % (4135380)Instructions burned: 42 (million)
% 12.30/2.68 % (4135381)lrs+10_1_sil=32000:urr=on:br=off:random_seed=4091446141:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 12.30/2.68 % (4135383)lrs+1011_1_sil=32000:sp=occurrence:random_seed=287970554:i=325:sd=1:ss=axioms:sgt=32_2995 on theBenchmark for (2995ds/325Mi)
% 12.30/2.68 % (4135381)Refutation not found, incomplete strategy
% 12.30/2.68 % (4135381)------------------------------
% 12.30/2.68 % (4135381)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.30/2.68 % (4135381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.30/2.68 % (4135381)CaDiCaL version: 2.1.3
% 12.30/2.68 % (4135381)Termination reason: Refutation not found, incomplete strategy
% 12.30/2.68 % (4135381)Time elapsed: 0.032 s
% 12.30/2.68 % (4135381)Peak memory usage: 94 MB
% 12.30/2.68 % (4135381)Instructions burned: 60 (million)
% 12.30/2.68 % (4135380)------------------------------
% 12.30/2.68 % (4135380)------------------------------
% 12.30/2.68 % (4135383)Refutation not found, incomplete strategy
% 12.30/2.68 % (4135383)------------------------------
% 12.30/2.68 % (4135383)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.30/2.68 % (4135383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.30/2.68 % (4135383)CaDiCaL version: 2.1.3
% 12.30/2.68 % (4135383)Termination reason: Refutation not found, incomplete strategy
% 12.30/2.68 % (4135383)Time elapsed: 0.018 s
% 12.30/2.68 % (4135383)Peak memory usage: 94 MB
% 12.30/2.68 % (4135383)Instructions burned: 22 (million)
% 12.30/2.68 % (4135369)------------------------------
% 12.30/2.68 % (4135369)------------------------------
% 12.30/2.68 % (4135386)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=2990233717:s2a=on:i=248:s2at=1.23:gtg=position_2994 on theBenchmark for (2994ds/248Mi)
% 12.30/2.68 % (4135387)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2087040135:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 12.30/2.68 % (4135386)Instruction limit reached!
% 12.30/2.68 % (4135386)------------------------------
% 12.30/2.68 % (4135386)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.30/2.68 % (4135386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.30/2.68 % (4135386)CaDiCaL version: 2.1.3
% 12.30/2.68 % (4135386)Termination reason: Instruction limit
% 12.30/2.68 % (4135386)Termination phase: Saturation
% 12.30/2.68 % (4135386)Time elapsed: 0.076 s
% 12.30/2.68 % (4135386)Peak memory usage: 98 MB
% 12.30/2.68 % (4135386)Instructions burned: 250 (million)
% 12.30/2.68 % (4135381)------------------------------
% 12.30/2.68 % (4135381)------------------------------
% 12.30/2.68 % (4135383)------------------------------
% 12.30/2.68 % (4135383)------------------------------
% 12.30/2.68 % (4135390)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3321056382:i=2350_2992 on theBenchmark for (2992ds/2350Mi)
% 12.30/2.68 % (4135387)Instruction limit reached!
% 12.30/2.68 % (4135387)------------------------------
% 12.30/2.68 % (4135387)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.30/2.68 % (4135387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.30/2.68 % (4135387)CaDiCaL version: 2.1.3
% 12.30/2.68 % (4135387)Termination reason: Instruction limit
% 12.30/2.68 % (4135387)Termination phase: Saturation
% 12.30/2.68 % (4135387)Time elapsed: 0.153 s
% 12.30/2.68 % (4135387)Peak memory usage: 95 MB
% 12.30/2.68 % (4135387)Instructions burned: 294 (million)
% 12.30/2.68 % (4135391)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3038315272:cts=off:i=113:fsr=off:ss=included:sgt=4_2991 on theBenchmark for (2991ds/113Mi)
% 12.30/2.68 % (4135393)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1835679399:i=127:av=off:fsr=off:sup=off_2991 on theBenchmark for (2991ds/127Mi)
% 12.30/2.68 % (4135391)Instruction limit reached!
% 12.30/2.68 % (4135391)------------------------------
% 12.30/2.68 % (4135391)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.30/2.68 % (4135391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.30/2.68 % (4135391)CaDiCaL version: 2.1.3
% 12.30/2.68 % (4135391)Termination reason: Instruction limit
% 12.30/2.68 % (4135391)Termination phase: Saturation
% 12.30/2.68 % (4135391)Time elapsed: 0.059 s
% 12.30/2.68 % (4135391)Peak memory usage: 94 MB
% 12.30/2.68 % (4135391)Instructions burned: 114 (million)
% 12.30/2.68 % (4135368)Refutation not found, incomplete strategy
% 12.30/2.68 % (4135368)------------------------------
% 12.30/2.68 % (4135368)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.30/2.68 % (4135368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.30/2.68 % (4135368)CaDiCaL version: 2.1.3
% 12.30/2.68 % (4135368)Termination reason: Refutation not found, incomplete strategy
% 12.30/2.68 % (4135368)Time elapsed: 0.692 s
% 12.30/2.68 % (4135368)Peak memory usage: 144 MB
% 12.30/2.68 % (4135368)Instructions burned: 1024 (million)
% 12.30/2.68 % (4135394)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3618704564:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 12.30/2.68 % (4135393)Instruction limit reached!
% 12.30/2.68 % (4135393)------------------------------
% 12.30/2.68 % (4135393)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.30/2.68 % (4135393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.30/2.68 % (4135393)CaDiCaL version: 2.1.3
% 12.30/2.68 % (4135393)Termination reason: Instruction limit
% 12.30/2.68 % (4135393)Termination phase: Property scanning
% 12.30/2.68 % (4135393)Time elapsed: 0.076 s
% 12.30/2.68 % (4135393)Peak memory usage: 96 MB
% 12.30/2.68 % (4135393)Instructions burned: 127 (million)
% 12.30/2.68 % (4135394)Instruction limit reached!
% 12.30/2.68 % (4135394)------------------------------
% 12.30/2.68 % (4135394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.30/2.68 % (4135394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.30/2.68 % (4135394)CaDiCaL version: 2.1.3
% 12.30/2.68 % (4135394)Termination reason: Instruction limit
% 12.30/2.68 % (4135394)Termination phase: Property scanning
% 12.30/2.68 % (4135394)Time elapsed: 0.060 s
% 12.30/2.68 % (4135394)Peak memory usage: 92 MB
% 12.30/2.68 % (4135394)Instructions burned: 115 (million)
% 12.30/2.68 % (4135397)lrs+10_1_sil=8000:sp=occurrence:random_seed=825910075:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 12.30/2.68 % (4135399)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3559195761:i=437:sd=1:aac=none:ss=included_2989 on theBenchmark for (2989ds/437Mi)
% 12.30/2.68 % (4135399)Refutation not found, incomplete strategy
% 12.30/2.68 % (4135399)------------------------------
% 12.30/2.68 % (4135399)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.30/2.68 % (4135399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.30/2.68 % (4135399)CaDiCaL version: 2.1.3
% 12.30/2.68 % (4135399)Termination reason: Refutation not found, incomplete strategy
% 12.30/2.68 % (4135399)Time elapsed: 0.016 s
% 12.30/2.68 % (4135399)Peak memory usage: 94 MB
% 12.30/2.68 % (4135399)Instructions burned: 20 (million)
% 12.30/2.68 % (4135400)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2329288295:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 12.30/2.68 % (4135368)------------------------------
% 12.30/2.68 % (4135368)------------------------------
% 12.30/2.68 % (4135404)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2687555289:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2987 on theBenchmark for (2987ds/134Mi)
% 12.30/2.68 % (4135399)------------------------------
% 12.30/2.68 % (4135399)------------------------------
% 12.30/2.68 % (4135404)Refutation not found, incomplete strategy
% 12.30/2.68 % (4135404)------------------------------
% 12.30/2.68 % (4135404)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.30/2.68 % (4135404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.30/2.68 % (4135404)CaDiCaL version: 2.1.3
% 12.30/2.68 % (4135404)Termination reason: Refutation not found, incomplete strategy
% 12.30/2.68 % (4135404)Time elapsed: 0.020 s
% 12.30/2.68 % (4135404)Peak memory usage: 94 MB
% 12.30/2.68 % (4135404)Instructions burned: 25 (million)
% 12.30/2.68 % (4135406)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2789346140:st=8:i=592:sd=3:ep=RST:ss=axioms_2985 on theBenchmark for (2985ds/592Mi)
% 12.30/2.68 % (4135397)Instruction limit reached!
% 12.30/2.68 % (4135397)------------------------------
% 12.30/2.68 % (4135397)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.30/2.68 % (4135397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.30/2.68 % (4135397)CaDiCaL version: 2.1.3
% 12.30/2.68 % (4135397)Termination reason: Instruction limit
% 12.30/2.68 % (4135397)Termination phase: Saturation
% 12.30/2.68 % (4135397)Time elapsed: 0.518 s
% 12.30/2.68 % (4135397)Peak memory usage: 104 MB
% 12.30/2.68 % (4135397)Instructions burned: 908 (million)
% 12.30/2.68 % (4135390)Instruction limit reached!
% 12.30/2.68 % (4135390)------------------------------
% 12.30/2.68 % (4135390)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.30/2.68 % (4135390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.30/2.68 % (4135390)CaDiCaL version: 2.1.3
% 12.30/2.68 % (4135390)Termination reason: Instruction limit
% 12.30/2.68 % (4135390)Termination phase: Saturation
% 12.30/2.68 % (4135390)Time elapsed: 0.840 s
% 12.30/2.68 % (4135390)Peak memory usage: 205 MB
% 12.30/2.68 % (4135390)Instructions burned: 2352 (million)
% 12.30/2.68 % (4135404)------------------------------
% 12.30/2.68 % (4135404)------------------------------
% 12.30/2.68 % (4135406)First to succeed.
% 12.30/2.68 % (4135406)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-4135361"
% 12.30/2.68 % (4135409)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=2530420038:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/125Mi)
% 12.30/2.68 % (4135408)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2457937817:st=3:i=13193:sd=3:ss=axioms_2983 on theBenchmark for (2983ds/13193Mi)
% 12.30/2.68 % (4135409)Instruction limit reached!
% 12.30/2.68 % (4135409)------------------------------
% 12.30/2.68 % (4135409)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.30/2.68 % (4135409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.30/2.68 % (4135409)CaDiCaL version: 2.1.3
% 12.30/2.68 % (4135409)Termination reason: Instruction limit
% 12.30/2.68 % (4135409)Termination phase: Preprocessing 3
% 12.30/2.68 % (4135409)Time elapsed: 0.044 s
% 12.30/2.68 % (4135409)Peak memory usage: 93 MB
% 12.30/2.68 % (4135409)Instructions burned: 128 (million)
% 12.30/2.68 % (4135410)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3540002791:i=134:gtgl=5:slsql=off:gtg=exists_sym_2983 on theBenchmark for (2983ds/134Mi)
% 12.30/2.68 % (4135413)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=2806850884:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2981 on theBenchmark for (2981ds/141Mi)
% 12.30/2.68 % (4135410)Instruction limit reached!
% 12.30/2.68 % (4135410)------------------------------
% 12.30/2.68 % (4135410)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.30/2.68 % (4135410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.30/2.68 % (4135410)CaDiCaL version: 2.1.3
% 12.30/2.68 % (4135410)Termination reason: Instruction limit
% 12.30/2.68 % (4135410)Termination phase: Preprocessing 2
% 12.30/2.68 % (4135410)Time elapsed: 0.075 s
% 12.30/2.68 % (4135410)Peak memory usage: 92 MB
% 12.30/2.68 % (4135410)Instructions burned: 135 (million)
% 12.30/2.68 % (4135413)Refutation not found, incomplete strategy
% 12.30/2.68 % (4135413)------------------------------
% 12.30/2.68 % (4135413)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.30/2.68 % (4135413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.30/2.68 % (4135413)CaDiCaL version: 2.1.3
% 12.30/2.68 % (4135413)Termination reason: Refutation not found, incomplete strategy
% 12.30/2.68 % (4135413)Time elapsed: 0.009 s
% 12.30/2.68 % (4135413)Peak memory usage: 94 MB
% 12.30/2.68 % (4135413)Instructions burned: 24 (million)
% 12.30/2.68 % (4135406)Refutation found. Thanks to Tanya!
% 12.30/2.68 % SZS status Theorem for theBenchmark
% 12.30/2.68 % SZS output start Proof for theBenchmark
% See solution above
% 13.95/2.88 % (4135406)------------------------------
% 13.95/2.88 % (4135406)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.95/2.88 % (4135406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.95/2.88 % (4135406)CaDiCaL version: 2.1.3
% 13.95/2.88 % (4135406)Termination reason: Refutation
% 13.95/2.88 % (4135406)Time elapsed: 0.168 s
% 13.95/2.88 % (4135406)Peak memory usage: 100 MB
% 13.95/2.88 % (4135406)Instructions burned: 294 (million)
% 13.95/2.88 % (4135406)------------------------------
% 13.95/2.88 % (4135406)------------------------------
% 13.95/2.88 % (4135361)Success in time 2.027 s
% 13.95/2.88 % Vampire exiting
%------------------------------------------------------------------------------