%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CSR104+3 : TPTP v9.3.1. Bugfixed v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n006.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:43:04 AM UTC 2026
% Result : Theorem 18.84s 5.98s
% Output : Refutation 20.86s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 14
% Syntax : Number of formulae : 62 ( 26 unt; 2 def)
% Number of atoms : 150 ( 0 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 165 ( 77 ~; 71 |; 8 &)
% ( 2 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 7 ( 6 usr; 3 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 7 con; 0-0 aty)
% Number of variables : 54 ( 0 sgn 54 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f26456,axiom,
! [X0,X1] :
( s__subclass(X0,X1)
=> ( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kb_SUMO_26635) ).
fof(f26457,axiom,
! [X0,X1,X2] :
( ( s__instance(X1,s__SetOrClass)
& s__instance(X0,s__SetOrClass) )
=> ( ( s__subclass(X0,X1)
& s__instance(X2,X0) )
=> s__instance(X2,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kb_SUMO_26636) ).
fof(f26517,axiom,
! [X0,X1] :
( ( s__instance(X1,s__TimeInterval)
& s__instance(X0,s__TimeInterval) )
=> ( s__during(X0,X1)
=> s__temporalPart(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kb_SUMO_26696) ).
fof(f27595,axiom,
s__subclass(s__TimeInterval,s__TimePosition),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kb_SUMO_27777) ).
fof(f27599,axiom,
s__subclass(s__TimePoint,s__TimePosition),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kb_SUMO_27781) ).
fof(f28237,axiom,
! [X0,X1,X2] :
( ( s__instance(X2,s__TimePosition)
& s__instance(X1,s__TimePosition)
& s__instance(X0,s__TimePosition) )
=> ( ( s__temporalPart(X0,X1)
& s__temporalPart(X1,X2) )
=> s__temporalPart(X0,X2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',kb_SUMO_28419) ).
fof(f145102,axiom,
s__instance(s__TimePoint35_1,s__TimePoint),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_1) ).
fof(f145103,axiom,
s__instance(s__TimeInterval35_1,s__TimeInterval),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_2) ).
fof(f145104,axiom,
s__instance(s__TimeInterval35_2,s__TimeInterval),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_3) ).
fof(f145105,axiom,
s__temporalPart(s__TimePoint35_1,s__TimeInterval35_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_4) ).
fof(f145106,axiom,
s__during(s__TimeInterval35_1,s__TimeInterval35_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',local_5) ).
fof(f145107,conjecture,
s__temporalPart(s__TimePoint35_1,s__TimeInterval35_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_from_ALL) ).
fof(f145108,negated_conjecture,
~ s__temporalPart(s__TimePoint35_1,s__TimeInterval35_2),
inference(negated_conjecture,[status(cth)],[f145107]) ).
fof(f145109,plain,
~ s__temporalPart(s__TimePoint35_1,s__TimeInterval35_2),
inference(flattening,[],[f145108]) ).
fof(f145122,plain,
! [X0,X1,X2] :
( s__temporalPart(X0,X2)
| ~ s__temporalPart(X0,X1)
| ~ s__temporalPart(X1,X2)
| ~ s__instance(X2,s__TimePosition)
| ~ s__instance(X1,s__TimePosition)
| ~ s__instance(X0,s__TimePosition) ),
inference(ennf_transformation,[],[f28237]) ).
fof(f145123,plain,
! [X0,X1,X2] :
( s__temporalPart(X0,X2)
| ~ s__temporalPart(X0,X1)
| ~ s__temporalPart(X1,X2)
| ~ s__instance(X2,s__TimePosition)
| ~ s__instance(X1,s__TimePosition)
| ~ s__instance(X0,s__TimePosition) ),
inference(flattening,[],[f145122]) ).
fof(f145134,plain,
! [X0,X1] :
( s__temporalPart(X0,X1)
| ~ s__during(X0,X1)
| ~ s__instance(X1,s__TimeInterval)
| ~ s__instance(X0,s__TimeInterval) ),
inference(ennf_transformation,[],[f26517]) ).
fof(f145135,plain,
! [X0,X1] :
( s__temporalPart(X0,X1)
| ~ s__during(X0,X1)
| ~ s__instance(X1,s__TimeInterval)
| ~ s__instance(X0,s__TimeInterval) ),
inference(flattening,[],[f145134]) ).
fof(f145208,plain,
! [X0,X1,X2] :
( s__instance(X2,X1)
| ~ s__subclass(X0,X1)
| ~ s__instance(X2,X0)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(ennf_transformation,[],[f26457]) ).
fof(f145209,plain,
! [X0,X1,X2] :
( s__instance(X2,X1)
| ~ s__subclass(X0,X1)
| ~ s__instance(X2,X0)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(flattening,[],[f145208]) ).
fof(f145210,plain,
! [X0,X1] :
( ( s__instance(X0,s__SetOrClass)
& s__instance(X1,s__SetOrClass) )
| ~ s__subclass(X0,X1) ),
inference(ennf_transformation,[],[f26456]) ).
fof(f145256,plain,
s__instance(s__TimePoint35_1,s__TimePoint),
inference(cnf_transformation,[],[f145102]) ).
fof(f145257,plain,
s__instance(s__TimeInterval35_1,s__TimeInterval),
inference(cnf_transformation,[],[f145103]) ).
fof(f145258,plain,
s__instance(s__TimeInterval35_2,s__TimeInterval),
inference(cnf_transformation,[],[f145104]) ).
fof(f145259,plain,
s__temporalPart(s__TimePoint35_1,s__TimeInterval35_1),
inference(cnf_transformation,[],[f145105]) ).
fof(f145260,plain,
s__during(s__TimeInterval35_1,s__TimeInterval35_2),
inference(cnf_transformation,[],[f145106]) ).
fof(f145261,plain,
~ s__temporalPart(s__TimePoint35_1,s__TimeInterval35_2),
inference(cnf_transformation,[],[f145109]) ).
fof(f145267,plain,
s__subclass(s__TimePoint,s__TimePosition),
inference(cnf_transformation,[],[f27599]) ).
fof(f145280,plain,
! [X2,X0,X1] :
( ~ s__instance(X0,s__TimePosition)
| ~ s__temporalPart(X0,X1)
| ~ s__temporalPart(X1,X2)
| ~ s__instance(X2,s__TimePosition)
| ~ s__instance(X1,s__TimePosition)
| s__temporalPart(X0,X2) ),
inference(cnf_transformation,[],[f145123]) ).
fof(f145288,plain,
! [X0,X1] :
( ~ s__instance(X0,s__TimeInterval)
| ~ s__during(X0,X1)
| ~ s__instance(X1,s__TimeInterval)
| s__temporalPart(X0,X1) ),
inference(cnf_transformation,[],[f145135]) ).
fof(f145331,plain,
s__subclass(s__TimeInterval,s__TimePosition),
inference(cnf_transformation,[],[f27595]) ).
fof(f145376,plain,
! [X2,X0,X1] :
( s__instance(X2,X1)
| ~ s__subclass(X0,X1)
| ~ s__instance(X2,X0)
| ~ s__instance(X1,s__SetOrClass)
| ~ s__instance(X0,s__SetOrClass) ),
inference(cnf_transformation,[],[f145209]) ).
fof(f145377,plain,
! [X0,X1] :
( ~ s__subclass(X0,X1)
| s__instance(X1,s__SetOrClass) ),
inference(cnf_transformation,[],[f145210]) ).
fof(f145378,plain,
! [X0,X1] :
( ~ s__subclass(X0,X1)
| s__instance(X0,s__SetOrClass) ),
inference(cnf_transformation,[],[f145210]) ).
fof(f145462,plain,
! [X2,X0,X1] :
( s__instance(X2,X1)
| ~ s__subclass(X0,X1)
| ~ s__instance(X2,X0)
| ~ s__instance(X0,s__SetOrClass) ),
inference(forward_subsumption_resolution,[],[f145376,f145377]) ).
fof(f145466,plain,
! [X2,X0,X1] :
( ~ s__subclass(X0,X1)
| s__instance(X2,X1)
| ~ s__instance(X2,X0) ),
inference(forward_subsumption_resolution,[],[f145462,f145378]) ).
fof(f145472,plain,
! [X0] :
( ~ s__during(s__TimeInterval35_1,X0)
| ~ s__instance(X0,s__TimeInterval)
| s__temporalPart(s__TimeInterval35_1,X0) ),
inference(resolution,[],[f145257,f145288]) ).
fof(f145473,plain,
! [X0] :
( s__instance(X0,s__TimePosition)
| ~ s__instance(X0,s__TimeInterval) ),
inference(resolution,[],[f145331,f145466]) ).
fof(f145476,plain,
! [X0] :
( ~ s__instance(X0,s__TimePoint)
| s__instance(X0,s__TimePosition) ),
inference(resolution,[],[f145267,f145466]) ).
fof(f145477,plain,
s__instance(s__TimePoint35_1,s__TimePosition),
inference(resolution,[],[f145476,f145256]) ).
fof(f145479,plain,
! [X0,X1] :
( ~ s__temporalPart(s__TimePoint35_1,X0)
| ~ s__temporalPart(X0,X1)
| ~ s__instance(X1,s__TimePosition)
| ~ s__instance(X0,s__TimePosition)
| s__temporalPart(s__TimePoint35_1,X1) ),
inference(resolution,[],[f145477,f145280]) ).
fof(f145486,definition,
( spl3_2
<=> ! [X0] :
( ~ s__temporalPart(s__TimeInterval35_1,X0)
| s__temporalPart(s__TimePoint35_1,X0)
| ~ s__instance(X0,s__TimePosition) ) ),
introduced(definition,[new_symbols(definition,[spl3_2])],[avatar_definition]) ).
fof(f145487,plain,
( ! [X0] :
( ~ s__temporalPart(s__TimeInterval35_1,X0)
| s__temporalPart(s__TimePoint35_1,X0)
| ~ s__instance(X0,s__TimePosition) )
| ~ spl3_2 ),
inference(avatar_component_clause,[],[f145486]) ).
fof(f145489,plain,
! [X0] :
( ~ s__temporalPart(s__TimeInterval35_1,X0)
| ~ s__instance(X0,s__TimePosition)
| ~ s__instance(s__TimeInterval35_1,s__TimePosition)
| s__temporalPart(s__TimePoint35_1,X0) ),
inference(resolution,[],[f145479,f145259]) ).
fof(f145491,definition,
( spl3_3
<=> s__instance(s__TimeInterval35_1,s__TimePosition) ),
introduced(definition,[new_symbols(definition,[spl3_3])],[avatar_definition]) ).
fof(f145492,plain,
( ~ s__instance(s__TimeInterval35_1,s__TimePosition)
| spl3_3 ),
inference(avatar_component_clause,[],[f145491]) ).
fof(f145493,plain,
( ~ spl3_3
| spl3_2 ),
inference(avatar_split_clause,[],[f145489,f145486,f145491]) ).
fof(f145500,plain,
( ~ s__instance(s__TimeInterval35_2,s__TimeInterval)
| s__temporalPart(s__TimeInterval35_1,s__TimeInterval35_2) ),
inference(resolution,[],[f145472,f145260]) ).
fof(f145501,plain,
s__temporalPart(s__TimeInterval35_1,s__TimeInterval35_2),
inference(forward_subsumption_resolution,[],[f145500,f145258]) ).
fof(f145523,plain,
( ~ s__instance(s__TimeInterval35_1,s__TimeInterval)
| spl3_3 ),
inference(resolution,[],[f145492,f145473]) ).
fof(f145526,plain,
( $false
| spl3_3 ),
inference(forward_subsumption_resolution,[],[f145523,f145257]) ).
fof(f145527,plain,
spl3_3,
inference(avatar_contradiction_clause,[],[f145526]) ).
fof(f145528,plain,
( s__temporalPart(s__TimePoint35_1,s__TimeInterval35_2)
| ~ s__instance(s__TimeInterval35_2,s__TimePosition)
| ~ spl3_2 ),
inference(resolution,[],[f145487,f145501]) ).
fof(f145529,plain,
( ~ s__instance(s__TimeInterval35_2,s__TimePosition)
| ~ spl3_2 ),
inference(forward_subsumption_resolution,[],[f145528,f145261]) ).
fof(f145532,plain,
( ~ s__instance(s__TimeInterval35_2,s__TimeInterval)
| ~ spl3_2 ),
inference(resolution,[],[f145529,f145473]) ).
fof(f145535,plain,
( $false
| ~ spl3_2 ),
inference(forward_subsumption_resolution,[],[f145532,f145258]) ).
fof(f145536,plain,
~ spl3_2,
inference(avatar_contradiction_clause,[],[f145535]) ).
cnf(s2,plain,
( spl3_2
| ~ spl3_3 ),
inference(sat_conversion,[],[f145493]) ).
cnf(s5,plain,
spl3_3,
inference(sat_conversion,[],[f145527]) ).
cnf(s8,plain,
~ spl3_2,
inference(sat_conversion,[],[f145536]) ).
cnf(s9,plain,
$false,
inference(rat,[],[s2,s5,s8]) ).
fof(f145537,plain,
$false,
inference(avatar_sat_refutation,[],[s9]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : CSR104+3 : TPTP v9.3.1. Bugfixed v7.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.20 % Computer : n006.cluster.edu
% 0.07/0.20 % Model : x86_64 x86_64
% 0.07/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.20 % Memory : 8046.5625MB
% 0.07/0.20 % OS : Linux 6.8.0-71-generic
% 0.07/0.20 % CPULimit : 300
% 0.07/0.20 % WCLimit : 300
% 0.07/0.20 % DateTime : Mon Sep 28 22:53:40 UTC 2026
% 0.07/0.20 % CPUTime :
% 0.07/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.07/0.24 Running first-order theorem proving
% 0.07/0.24 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
% 16.20/5.45 % (296287)Detected formulas, will run a generic FOF schedule.
% 16.20/5.45 % (296296)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3064748960:i=119:av=off:ss=axioms_2971 on theBenchmark for (2971ds/119Mi)
% 16.20/5.45 % (296295)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3419383777:i=109:sd=1:ins=1:gsp=on:ss=axioms_2971 on theBenchmark for (2971ds/109Mi)
% 16.20/5.45 % (296293)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=2702075693:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2971 on theBenchmark for (2971ds/134677Mi)
% 16.20/5.45 % (296292)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=3469759901:i=141193_2971 on theBenchmark for (2971ds/141193Mi)
% 16.20/5.45 % (296294)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=991388032:i=141695:sd=1:nm=32:gsp=on:ss=included_2971 on theBenchmark for (2971ds/141695Mi)
% 16.20/5.45 % (296296)Instruction limit reached!
% 16.20/5.45 % (296296)------------------------------
% 16.20/5.45 % (296296)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.20/5.45 % (296296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.20/5.45 % (296296)CaDiCaL version: 2.1.3
% 16.20/5.45 % (296296)Termination reason: Instruction limit
% 16.20/5.45 % (296296)Termination phase: SInE selection
% 16.20/5.45 % (296296)Time elapsed: 0.044 s
% 16.20/5.45 % (296296)Peak memory usage: 165 MB
% 16.20/5.45 % (296296)Instructions burned: 119 (million)
% 16.20/5.45 % (296298)dis-21_1_sil=8000:lcm=predicate:random_seed=4057743943:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2971 on theBenchmark for (2971ds/129Mi)
% 16.20/5.45 % (296297)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1238281683:s2a=on:i=139:gtg=position_2971 on theBenchmark for (2971ds/139Mi)
% 16.20/5.45 % (296295)Instruction limit reached!
% 16.20/5.45 % (296295)------------------------------
% 16.20/5.45 % (296295)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.20/5.45 % (296295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.20/5.45 % (296295)CaDiCaL version: 2.1.3
% 16.20/5.45 % (296295)Termination reason: Instruction limit
% 16.20/5.45 % (296295)Termination phase: SInE selection
% 16.20/5.45 % (296295)Time elapsed: 0.066 s
% 16.20/5.45 % (296295)Peak memory usage: 164 MB
% 16.20/5.45 % (296295)Instructions burned: 109 (million)
% 16.20/5.45 % (296297)Instruction limit reached!
% 16.20/5.45 % (296297)------------------------------
% 16.20/5.45 % (296297)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.20/5.45 % (296297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.20/5.45 % (296297)CaDiCaL version: 2.1.3
% 16.20/5.45 % (296297)Termination reason: Instruction limit
% 16.20/5.45 % (296297)Termination phase: Property scanning
% 16.20/5.45 % (296297)Time elapsed: 0.077 s
% 16.20/5.45 % (296297)Peak memory usage: 165 MB
% 16.20/5.45 % (296297)Instructions burned: 141 (million)
% 16.20/5.45 % (296298)Instruction limit reached!
% 16.20/5.45 % (296298)------------------------------
% 16.20/5.45 % (296298)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.20/5.45 % (296298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.20/5.45 % (296298)CaDiCaL version: 2.1.3
% 16.20/5.45 % (296298)Termination reason: Instruction limit
% 16.20/5.45 % (296298)Termination phase: SInE selection
% 16.20/5.45 % (296298)Time elapsed: 0.078 s
% 16.20/5.45 % (296298)Peak memory usage: 164 MB
% 16.20/5.45 % (296298)Instructions burned: 129 (million)
% 16.20/5.45 % (296306)lrs+10_1_sil=8000:sp=occurrence:random_seed=1163118981:i=285:sd=3:ss=axioms:sgt=8_2969 on theBenchmark for (2969ds/285Mi)
% 16.20/5.45 % (296307)lrs+10_1_sil=32000:urr=on:br=off:random_seed=629021190:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2969 on theBenchmark for (2969ds/157Mi)
% 16.20/5.45 % (296306)Instruction limit reached!
% 16.20/5.45 % (296306)------------------------------
% 16.20/5.45 % (296306)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.20/5.45 % (296306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.20/5.45 % (296306)CaDiCaL version: 2.1.3
% 16.20/5.45 % (296306)Termination reason: Instruction limit
% 16.20/5.45 % (296306)Termination phase: SInE selection
% 18.84/5.98 % (296306)Time elapsed: 0.100 s
% 18.84/5.98 % (296306)Peak memory usage: 165 MB
% 18.84/5.98 % (296306)Instructions burned: 289 (million)
% 18.84/5.98 % (296309)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=3311789207:s2a=on:i=248:s2at=1.23:gtg=position_2969 on theBenchmark for (2969ds/248Mi)
% 18.84/5.98 % (296308)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3050939175:i=325:sd=1:ss=axioms:sgt=32_2969 on theBenchmark for (2969ds/325Mi)
% 18.84/5.98 % (296307)Instruction limit reached!
% 18.84/5.98 % (296307)------------------------------
% 18.84/5.98 % (296307)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.84/5.98 % (296307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.84/5.98 % (296307)CaDiCaL version: 2.1.3
% 18.84/5.98 % (296307)Termination reason: Instruction limit
% 18.84/5.98 % (296307)Termination phase: Property scanning
% 18.84/5.98 % (296307)Time elapsed: 0.085 s
% 18.84/5.98 % (296307)Peak memory usage: 165 MB
% 18.84/5.98 % (296307)Instructions burned: 158 (million)
% 18.84/5.98 % (296312)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2203610369:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2967 on theBenchmark for (2967ds/294Mi)
% 18.84/5.98 % (296309)Instruction limit reached!
% 18.84/5.98 % (296309)------------------------------
% 18.84/5.98 % (296309)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.84/5.98 % (296309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.84/5.98 % (296309)CaDiCaL version: 2.1.3
% 18.84/5.98 % (296309)Termination reason: Instruction limit
% 18.84/5.98 % (296309)Termination phase: Property scanning
% 18.84/5.98 % (296309)Time elapsed: 0.125 s
% 18.84/5.98 % (296309)Peak memory usage: 165 MB
% 18.84/5.98 % (296309)Instructions burned: 250 (million)
% 18.84/5.98 % (296308)Instruction limit reached!
% 18.84/5.98 % (296308)------------------------------
% 18.84/5.98 % (296308)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.84/5.98 % (296308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.84/5.98 % (296308)CaDiCaL version: 2.1.3
% 18.84/5.98 % (296308)Termination reason: Instruction limit
% 18.84/5.98 % (296308)Termination phase: SInE selection
% 18.84/5.98 % (296308)Time elapsed: 0.186 s
% 18.84/5.98 % (296308)Peak memory usage: 164 MB
% 18.84/5.98 % (296308)Instructions burned: 325 (million)
% 18.84/5.98 % (296312)Instruction limit reached!
% 18.84/5.98 % (296312)------------------------------
% 18.84/5.98 % (296312)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.84/5.98 % (296312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.84/5.98 % (296312)CaDiCaL version: 2.1.3
% 18.84/5.98 % (296312)Termination reason: Instruction limit
% 18.84/5.98 % (296312)Termination phase: SInE selection
% 18.84/5.98 % (296312)Time elapsed: 0.095 s
% 18.84/5.98 % (296312)Peak memory usage: 165 MB
% 18.84/5.98 % (296312)Instructions burned: 294 (million)
% 18.84/5.98 % (296315)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3762609032:i=2350_2966 on theBenchmark for (2966ds/2350Mi)
% 18.84/5.98 % (296317)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2410840547:cts=off:i=113:fsr=off:ss=included:sgt=4_2966 on theBenchmark for (2966ds/113Mi)
% 18.84/5.98 % (296318)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3152081529:i=127:av=off:fsr=off:sup=off_2965 on theBenchmark for (2965ds/127Mi)
% 18.84/5.98 % (296317)Instruction limit reached!
% 18.84/5.98 % (296317)------------------------------
% 18.84/5.98 % (296317)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.84/5.98 % (296317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.84/5.98 % (296317)CaDiCaL version: 2.1.3
% 18.84/5.98 % (296317)Termination reason: Instruction limit
% 18.84/5.98 % (296317)Termination phase: SInE selection
% 18.84/5.98 % (296317)Time elapsed: 0.067 s
% 18.84/5.98 % (296317)Peak memory usage: 165 MB
% 18.84/5.98 % (296317)Instructions burned: 115 (million)
% 18.84/5.98 % (296319)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3991043329:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2965 on theBenchmark for (2965ds/114Mi)
% 18.84/5.98 % (296318)Instruction limit reached!
% 18.84/5.98 % (296318)------------------------------
% 18.84/5.98 % (296318)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.84/5.98 % (296318)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.84/5.98 % (296318)CaDiCaL version: 2.1.3
% 18.84/5.98 % (296318)Termination reason: Instruction limit
% 18.84/5.98 % (296318)Termination phase: Preprocessing 1
% 18.84/5.98 % (296318)Time elapsed: 0.049 s
% 18.84/5.98 % (296318)Peak memory usage: 165 MB
% 18.84/5.98 % (296318)Instructions burned: 127 (million)
% 18.84/5.98 % (296319)Instruction limit reached!
% 18.84/5.98 % (296319)------------------------------
% 18.84/5.98 % (296319)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.84/5.98 % (296319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.84/5.98 % (296319)CaDiCaL version: 2.1.3
% 18.84/5.98 % (296319)Termination reason: Instruction limit
% 18.84/5.98 % (296319)Termination phase: Property scanning
% 18.84/5.98 % (296319)Time elapsed: 0.066 s
% 18.84/5.98 % (296319)Peak memory usage: 165 MB
% 18.84/5.98 % (296319)Instructions burned: 115 (million)
% 18.84/5.98 % (296325)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2120212927:i=437:sd=1:aac=none:ss=included_2963 on theBenchmark for (2963ds/437Mi)
% 18.84/5.98 % (296323)lrs+10_1_sil=8000:sp=occurrence:random_seed=1949755640:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2963 on theBenchmark for (2963ds/907Mi)
% 18.84/5.98 % (296326)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1650528351:i=5202:ss=axioms:sgt=16_2963 on theBenchmark for (2963ds/5202Mi)
% 18.84/5.98 % (296325)Refutation not found, incomplete strategy
% 18.84/5.98 % (296325)------------------------------
% 18.84/5.98 % (296325)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.84/5.98 % (296325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.84/5.98 % (296325)CaDiCaL version: 2.1.3
% 18.84/5.98 % (296325)Termination reason: Refutation not found, incomplete strategy
% 18.84/5.98 % (296325)Time elapsed: 0.141 s
% 18.84/5.98 % (296325)Peak memory usage: 169 MB
% 18.84/5.98 % (296325)Instructions burned: 397 (million)
% 18.84/5.98 % (296325)------------------------------
% 18.84/5.98 % (296325)------------------------------
% 18.84/5.98 % (296330)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=866540959:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2959 on theBenchmark for (2959ds/134Mi)
% 18.84/5.98 % (296330)Instruction limit reached!
% 18.84/5.98 % (296330)------------------------------
% 18.84/5.98 % (296330)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.84/5.98 % (296330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.84/5.98 % (296330)CaDiCaL version: 2.1.3
% 18.84/5.98 % (296330)Termination reason: Instruction limit
% 18.84/5.98 % (296330)Termination phase: SInE selection
% 18.84/5.98 % (296330)Time elapsed: 0.048 s
% 18.84/5.98 % (296330)Peak memory usage: 165 MB
% 18.84/5.98 % (296330)Instructions burned: 136 (million)
% 18.84/5.98 % (296323)Instruction limit reached!
% 18.84/5.98 % (296323)------------------------------
% 18.84/5.98 % (296323)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.84/5.98 % (296323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.84/5.98 % (296323)CaDiCaL version: 2.1.3
% 18.84/5.98 % (296323)Termination reason: Instruction limit
% 18.84/5.98 % (296323)Termination phase: Saturation
% 18.84/5.98 % (296323)Time elapsed: 0.544 s
% 18.84/5.98 % (296323)Peak memory usage: 174 MB
% 18.84/5.98 % (296323)Instructions burned: 908 (million)
% 18.84/5.98 % (296332)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3867591950:st=8:i=592:sd=3:ep=RST:ss=axioms_2957 on theBenchmark for (2957ds/592Mi)
% 18.84/5.98 % (296333)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=4149612885:st=3:i=13193:sd=3:ss=axioms_2956 on theBenchmark for (2956ds/13193Mi)
% 18.84/5.98 % (296332)Instruction limit reached!
% 18.84/5.98 % (296332)------------------------------
% 18.84/5.98 % (296332)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.84/5.98 % (296332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.84/5.98 % (296332)CaDiCaL version: 2.1.3
% 18.84/5.98 % (296332)Termination reason: Instruction limit
% 18.84/5.98 % (296332)Termination phase: Preprocessing 1
% 18.84/5.98 % (296332)Time elapsed: 0.198 s
% 18.84/5.98 % (296332)Peak memory usage: 167 MB
% 18.84/5.98 % (296332)Instructions burned: 592 (million)
% 18.84/5.98 % (296336)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=1642680642:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2953 on theBenchmark for (2953ds/125Mi)
% 18.84/5.98 % (296315)Instruction limit reached!
% 18.84/5.98 % (296315)------------------------------
% 18.84/5.98 % (296315)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.84/5.98 % (296315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.84/5.98 % (296315)CaDiCaL version: 2.1.3
% 18.84/5.98 % (296315)Termination reason: Instruction limit
% 18.84/5.98 % (296315)Termination phase: Property scanning
% 18.84/5.98 % (296315)Time elapsed: 1.306 s
% 18.84/5.98 % (296315)Peak memory usage: 194 MB
% 18.84/5.98 % (296315)Instructions burned: 2350 (million)
% 18.84/5.98 % (296294)Refutation not found, incomplete strategy
% 18.84/5.98 % (296294)------------------------------
% 18.84/5.98 % (296294)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.84/5.98 % (296294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.84/5.98 % (296294)CaDiCaL version: 2.1.3
% 18.84/5.98 % (296294)Termination reason: Refutation not found, incomplete strategy
% 18.84/5.98 % (296294)Time elapsed: 1.809 s
% 18.84/5.98 % (296294)Peak memory usage: 318 MB
% 18.84/5.98 % (296294)Instructions burned: 2533 (million)
% 18.84/5.98 % (296336)Instruction limit reached!
% 18.84/5.98 % (296336)------------------------------
% 18.84/5.98 % (296336)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.84/5.98 % (296336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.84/5.98 % (296336)CaDiCaL version: 2.1.3
% 18.84/5.98 % (296336)Termination reason: Instruction limit
% 18.84/5.98 % (296336)Termination phase: Property scanning
% 18.84/5.98 % (296336)Time elapsed: 0.040 s
% 18.84/5.98 % (296336)Peak memory usage: 165 MB
% 18.84/5.98 % (296336)Instructions burned: 126 (million)
% 18.84/5.98 % (296293)First to succeed.
% 18.84/5.98 % (296338)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2444665005:i=134:gtgl=5:slsql=off:gtg=exists_sym_2951 on theBenchmark for (2951ds/134Mi)
% 18.84/5.98 % (296293)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-296287"
% 18.84/5.98 % (296338)Instruction limit reached!
% 18.84/5.98 % (296338)------------------------------
% 18.84/5.98 % (296338)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.84/5.98 % (296338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.84/5.98 % (296338)CaDiCaL version: 2.1.3
% 18.84/5.98 % (296338)Termination reason: Instruction limit
% 18.84/5.98 % (296338)Termination phase: Property scanning
% 18.84/5.98 % (296338)Time elapsed: 0.042 s
% 18.84/5.98 % (296338)Peak memory usage: 165 MB
% 18.84/5.98 % (296338)Instructions burned: 138 (million)
% 18.84/5.98 % (296339)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3800078560:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2951 on theBenchmark for (2951ds/141Mi)
% 18.84/5.98 % (296339)Instruction limit reached!
% 18.84/5.98 % (296339)------------------------------
% 18.84/5.98 % (296339)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.84/5.98 % (296339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.84/5.98 % (296339)CaDiCaL version: 2.1.3
% 18.84/5.98 % (296339)Termination reason: Instruction limit
% 18.84/5.98 % (296339)Termination phase: SInE selection
% 18.84/5.98 % (296339)Time elapsed: 0.086 s
% 18.84/5.98 % (296339)Peak memory usage: 165 MB
% 18.84/5.98 % (296339)Instructions burned: 141 (million)
% 18.84/5.98 % (296294)------------------------------
% 18.84/5.98 % (296294)------------------------------
% 18.84/5.98 % (296342)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=734131961:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2950 on theBenchmark for (2950ds/431Mi)
% 18.84/5.98 % (296343)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=3168789452:i=6060:aac=none:ins=25_2949 on theBenchmark for (2949ds/6060Mi)
% 18.84/5.98 % (296293)Refutation found. Thanks to Tanya!
% 18.84/5.98 % SZS status Theorem for theBenchmark
% 18.84/5.98 % SZS output start Proof for theBenchmark
% See solution above
% 20.86/6.25 % (296293)------------------------------
% 20.86/6.25 % (296293)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.86/6.25 % (296293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.86/6.25 % (296293)CaDiCaL version: 2.1.3
% 20.86/6.25 % (296293)Termination reason: Refutation
% 20.86/6.25 % (296293)Time elapsed: 1.953 s
% 20.86/6.25 % (296293)Peak memory usage: 305 MB
% 20.86/6.25 % (296293)Instructions burned: 2769 (million)
% 20.86/6.25 % (296293)------------------------------
% 20.86/6.25 % (296293)------------------------------
% 20.86/6.25 % (296287)Success in time 5.298 s
% 20.86/6.25 % Vampire exiting
%------------------------------------------------------------------------------