%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CSR040+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 : 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:42:11 AM UTC 2026
% Result : Theorem 23.89s 5.72s
% Output : Refutation 0.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 21
% Syntax : Number of formulae : 83 ( 23 unt; 0 def)
% Number of atoms : 143 ( 0 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 105 ( 45 ~; 38 |; 2 &)
% ( 0 <=>; 20 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 22 ( 21 usr; 1 prp; 0-1 aty)
% Number of functors : 6 ( 6 usr; 3 con; 0-2 aty)
% Number of variables : 57 ( 57 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1425,axiom,
! [X0] :
( tptpcol_13_109173(X0)
=> tptpcol_12_109157(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_1425) ).
fof(f1632,axiom,
! [X0] :
( tptpcol_14_109181(X0)
=> tptpcol_13_109173(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_1632) ).
fof(f1910,axiom,
! [X0] :
( tptpcol_11_109125(X0)
=> tptpcol_10_109061(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_1910) ).
fof(f2076,axiom,
! [X0] :
( tptpcol_1_65536(X0)
=> tptpcol_0_0(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_2076) ).
fof(f2470,axiom,
! [X0] :
( tptpcol_3_98305(X0)
=> tptpcol_2_98304(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_2470) ).
fof(f2952,axiom,
! [X0] :
( tptpcol_8_109059(X0)
=> tptpcol_7_108547(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_2952) ).
fof(f2980,axiom,
! [X0] :
( tptpcol_2_98304(X0)
=> tptpcol_1_65536(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_2980) ).
fof(f3137,axiom,
firstordercollection(c_tptpcol_16_62187),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_3137) ).
fof(f3153,axiom,
! [X0] :
( tptpcol_6_108546(X0)
=> tptpcol_5_106498(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_3153) ).
fof(f3201,axiom,
! [X0] :
( tptpcol_12_109157(X0)
=> tptpcol_11_109125(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_3201) ).
fof(f3226,axiom,
! [X0] :
~ ( collection(X0)
& individual(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_3226) ).
fof(f3424,axiom,
! [X0] :
( tptpcol_9_109060(X0)
=> tptpcol_8_109059(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_3424) ).
fof(f3552,axiom,
! [X0] :
( tptpcol_15_109185(X0)
=> tptpcol_14_109181(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_3552) ).
fof(f3810,axiom,
! [X0] :
( tptpcol_7_108547(X0)
=> tptpcol_6_108546(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_3810) ).
fof(f3841,axiom,
! [X0] :
( firstordercollection(X0)
=> fixedordercollection(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_3841) ).
fof(f3890,axiom,
! [X0] :
( tptpcol_5_106498(X0)
=> tptpcol_4_106497(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_3890) ).
fof(f3934,axiom,
! [X0] :
( tptpcol_0_0(X0)
=> individual(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_3934) ).
fof(f3943,axiom,
! [X0] :
( tptpcol_10_109061(X0)
=> tptpcol_9_109060(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_3943) ).
fof(f4232,axiom,
! [X0] :
( tptpcol_4_106497(X0)
=> tptpcol_3_98305(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_4232) ).
fof(f4466,axiom,
! [X0] :
( fixedordercollection(X0)
=> collection(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2_4466) ).
fof(f8006,conjecture,
( mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwthedailybulletincompostcardsmar9chtm)),c_translation_14))
=> ~ tptpcol_15_109185(c_tptpcol_16_62187) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',query140) ).
fof(f8007,negated_conjecture,
~ ( mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwthedailybulletincompostcardsmar9chtm)),c_translation_14))
=> ~ tptpcol_15_109185(c_tptpcol_16_62187) ),
inference(negated_conjecture,[status(cth)],[f8006]) ).
fof(f9299,plain,
! [X0] :
( tptpcol_12_109157(X0)
| ~ tptpcol_13_109173(X0) ),
inference(ennf_transformation,[],[f1425]) ).
fof(f9385,plain,
! [X0] :
( tptpcol_13_109173(X0)
| ~ tptpcol_14_109181(X0) ),
inference(ennf_transformation,[],[f1632]) ).
fof(f9498,plain,
! [X0] :
( tptpcol_10_109061(X0)
| ~ tptpcol_11_109125(X0) ),
inference(ennf_transformation,[],[f1910]) ).
fof(f9563,plain,
! [X0] :
( tptpcol_0_0(X0)
| ~ tptpcol_1_65536(X0) ),
inference(ennf_transformation,[],[f2076]) ).
fof(f9721,plain,
! [X0] :
( tptpcol_2_98304(X0)
| ~ tptpcol_3_98305(X0) ),
inference(ennf_transformation,[],[f2470]) ).
fof(f9921,plain,
! [X0] :
( tptpcol_7_108547(X0)
| ~ tptpcol_8_109059(X0) ),
inference(ennf_transformation,[],[f2952]) ).
fof(f9931,plain,
! [X0] :
( tptpcol_1_65536(X0)
| ~ tptpcol_2_98304(X0) ),
inference(ennf_transformation,[],[f2980]) ).
fof(f9996,plain,
! [X0] :
( tptpcol_5_106498(X0)
| ~ tptpcol_6_108546(X0) ),
inference(ennf_transformation,[],[f3153]) ).
fof(f10014,plain,
! [X0] :
( tptpcol_11_109125(X0)
| ~ tptpcol_12_109157(X0) ),
inference(ennf_transformation,[],[f3201]) ).
fof(f10023,plain,
! [X0] :
( ~ collection(X0)
| ~ individual(X0) ),
inference(ennf_transformation,[],[f3226]) ).
fof(f10108,plain,
! [X0] :
( tptpcol_8_109059(X0)
| ~ tptpcol_9_109060(X0) ),
inference(ennf_transformation,[],[f3424]) ).
fof(f10156,plain,
! [X0] :
( tptpcol_14_109181(X0)
| ~ tptpcol_15_109185(X0) ),
inference(ennf_transformation,[],[f3552]) ).
fof(f10251,plain,
! [X0] :
( tptpcol_6_108546(X0)
| ~ tptpcol_7_108547(X0) ),
inference(ennf_transformation,[],[f3810]) ).
fof(f10267,plain,
! [X0] :
( fixedordercollection(X0)
| ~ firstordercollection(X0) ),
inference(ennf_transformation,[],[f3841]) ).
fof(f10285,plain,
! [X0] :
( tptpcol_4_106497(X0)
| ~ tptpcol_5_106498(X0) ),
inference(ennf_transformation,[],[f3890]) ).
fof(f10304,plain,
! [X0] :
( individual(X0)
| ~ tptpcol_0_0(X0) ),
inference(ennf_transformation,[],[f3934]) ).
fof(f10308,plain,
! [X0] :
( tptpcol_9_109060(X0)
| ~ tptpcol_10_109061(X0) ),
inference(ennf_transformation,[],[f3943]) ).
fof(f10431,plain,
! [X0] :
( tptpcol_3_98305(X0)
| ~ tptpcol_4_106497(X0) ),
inference(ennf_transformation,[],[f4232]) ).
fof(f10524,plain,
! [X0] :
( collection(X0)
| ~ fixedordercollection(X0) ),
inference(ennf_transformation,[],[f4466]) ).
fof(f13400,plain,
( tptpcol_15_109185(c_tptpcol_16_62187)
& mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwthedailybulletincompostcardsmar9chtm)),c_translation_14)) ),
inference(ennf_transformation,[],[f8007]) ).
fof(f14797,plain,
! [X0] :
( ~ tptpcol_13_109173(X0)
| tptpcol_12_109157(X0) ),
inference(cnf_transformation,[],[f9299]) ).
fof(f14999,plain,
! [X0] :
( ~ tptpcol_14_109181(X0)
| tptpcol_13_109173(X0) ),
inference(cnf_transformation,[],[f9385]) ).
fof(f15272,plain,
! [X0] :
( ~ tptpcol_11_109125(X0)
| tptpcol_10_109061(X0) ),
inference(cnf_transformation,[],[f9498]) ).
fof(f15437,plain,
! [X0] :
( ~ tptpcol_1_65536(X0)
| tptpcol_0_0(X0) ),
inference(cnf_transformation,[],[f9563]) ).
fof(f15827,plain,
! [X0] :
( ~ tptpcol_3_98305(X0)
| tptpcol_2_98304(X0) ),
inference(cnf_transformation,[],[f9721]) ).
fof(f16302,plain,
! [X0] :
( ~ tptpcol_8_109059(X0)
| tptpcol_7_108547(X0) ),
inference(cnf_transformation,[],[f9921]) ).
fof(f16330,plain,
! [X0] :
( ~ tptpcol_2_98304(X0)
| tptpcol_1_65536(X0) ),
inference(cnf_transformation,[],[f9931]) ).
fof(f16484,plain,
firstordercollection(c_tptpcol_16_62187),
inference(cnf_transformation,[],[f3137]) ).
fof(f16500,plain,
! [X0] :
( ~ tptpcol_6_108546(X0)
| tptpcol_5_106498(X0) ),
inference(cnf_transformation,[],[f9996]) ).
fof(f16547,plain,
! [X0] :
( ~ tptpcol_12_109157(X0)
| tptpcol_11_109125(X0) ),
inference(cnf_transformation,[],[f10014]) ).
fof(f16572,plain,
! [X0] :
( ~ collection(X0)
| ~ individual(X0) ),
inference(cnf_transformation,[],[f10023]) ).
fof(f16766,plain,
! [X0] :
( ~ tptpcol_9_109060(X0)
| tptpcol_8_109059(X0) ),
inference(cnf_transformation,[],[f10108]) ).
fof(f16893,plain,
! [X0] :
( ~ tptpcol_15_109185(X0)
| tptpcol_14_109181(X0) ),
inference(cnf_transformation,[],[f10156]) ).
fof(f17146,plain,
! [X0] :
( ~ tptpcol_7_108547(X0)
| tptpcol_6_108546(X0) ),
inference(cnf_transformation,[],[f10251]) ).
fof(f17177,plain,
! [X0] :
( ~ firstordercollection(X0)
| fixedordercollection(X0) ),
inference(cnf_transformation,[],[f10267]) ).
fof(f17226,plain,
! [X0] :
( ~ tptpcol_5_106498(X0)
| tptpcol_4_106497(X0) ),
inference(cnf_transformation,[],[f10285]) ).
fof(f17270,plain,
! [X0] :
( ~ tptpcol_0_0(X0)
| individual(X0) ),
inference(cnf_transformation,[],[f10304]) ).
fof(f17279,plain,
! [X0] :
( ~ tptpcol_10_109061(X0)
| tptpcol_9_109060(X0) ),
inference(cnf_transformation,[],[f10308]) ).
fof(f17561,plain,
! [X0] :
( ~ tptpcol_4_106497(X0)
| tptpcol_3_98305(X0) ),
inference(cnf_transformation,[],[f10431]) ).
fof(f17789,plain,
! [X0] :
( ~ fixedordercollection(X0)
| collection(X0) ),
inference(cnf_transformation,[],[f10524]) ).
fof(f20688,plain,
tptpcol_15_109185(c_tptpcol_16_62187),
inference(cnf_transformation,[],[f13400]) ).
fof(f24412,plain,
tptpcol_14_109181(c_tptpcol_16_62187),
inference(resolution,[],[f20688,f16893]) ).
fof(f24413,plain,
tptpcol_13_109173(c_tptpcol_16_62187),
inference(resolution,[],[f24412,f14999]) ).
fof(f24414,plain,
tptpcol_12_109157(c_tptpcol_16_62187),
inference(resolution,[],[f14797,f24413]) ).
fof(f24415,plain,
tptpcol_11_109125(c_tptpcol_16_62187),
inference(resolution,[],[f16547,f24414]) ).
fof(f24416,plain,
tptpcol_10_109061(c_tptpcol_16_62187),
inference(resolution,[],[f24415,f15272]) ).
fof(f24417,plain,
tptpcol_9_109060(c_tptpcol_16_62187),
inference(resolution,[],[f17279,f24416]) ).
fof(f24418,plain,
tptpcol_8_109059(c_tptpcol_16_62187),
inference(resolution,[],[f16766,f24417]) ).
fof(f24419,plain,
tptpcol_7_108547(c_tptpcol_16_62187),
inference(resolution,[],[f24418,f16302]) ).
fof(f24420,plain,
tptpcol_6_108546(c_tptpcol_16_62187),
inference(resolution,[],[f17146,f24419]) ).
fof(f24422,plain,
tptpcol_5_106498(c_tptpcol_16_62187),
inference(resolution,[],[f16500,f24420]) ).
fof(f24423,plain,
tptpcol_4_106497(c_tptpcol_16_62187),
inference(resolution,[],[f24422,f17226]) ).
fof(f24424,plain,
tptpcol_3_98305(c_tptpcol_16_62187),
inference(resolution,[],[f24423,f17561]) ).
fof(f25532,plain,
fixedordercollection(c_tptpcol_16_62187),
inference(resolution,[],[f17177,f16484]) ).
fof(f25875,plain,
collection(c_tptpcol_16_62187),
inference(resolution,[],[f17789,f25532]) ).
fof(f25876,plain,
~ individual(c_tptpcol_16_62187),
inference(resolution,[],[f25875,f16572]) ).
fof(f33487,plain,
tptpcol_2_98304(c_tptpcol_16_62187),
inference(resolution,[],[f15827,f24424]) ).
fof(f38897,plain,
tptpcol_1_65536(c_tptpcol_16_62187),
inference(resolution,[],[f16330,f33487]) ).
fof(f38898,plain,
tptpcol_0_0(c_tptpcol_16_62187),
inference(resolution,[],[f38897,f15437]) ).
fof(f38899,plain,
individual(c_tptpcol_16_62187),
inference(resolution,[],[f38898,f17270]) ).
fof(f38900,plain,
$false,
inference(forward_subsumption_resolution,[],[f38899,f25876]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR040+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n006.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 22:14:40 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.22 Running first-order theorem proving
% 0.09/0.22 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
% 13.25/2.93 % (268362)Detected formulas, will run a generic FOF schedule.
% 13.25/2.93 % (268498)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=1504429346:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2998 on theBenchmark for (2998ds/134677Mi)
% 13.25/2.93 % (268499)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=4095794758:i=141695:sd=1:nm=32:gsp=on:ss=included_2998 on theBenchmark for (2998ds/141695Mi)
% 13.25/2.93 % (268503)dis-21_1_sil=8000:lcm=predicate:random_seed=951411440: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)
% 13.25/2.93 % (268497)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=3599198654:i=141193_2998 on theBenchmark for (2998ds/141193Mi)
% 13.25/2.93 % (268500)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=3505021019:i=109:sd=1:ins=1:gsp=on:ss=axioms_2998 on theBenchmark for (2998ds/109Mi)
% 13.25/2.93 % (268501)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=2093455515:i=119:av=off:ss=axioms_2998 on theBenchmark for (2998ds/119Mi)
% 13.25/2.93 % (268500)Refutation not found, incomplete strategy
% 13.25/2.93 % (268500)------------------------------
% 13.25/2.93 % (268500)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.25/2.93 % (268500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.25/2.93 % (268500)CaDiCaL version: 2.1.3
% 13.25/2.93 % (268500)Termination reason: Refutation not found, incomplete strategy
% 13.25/2.93 % (268500)Time elapsed: 0.017 s
% 13.25/2.93 % (268500)Peak memory usage: 93 MB
% 13.25/2.93 % (268500)Instructions burned: 23 (million)
% 13.25/2.93 % (268503)Refutation not found, incomplete strategy
% 13.25/2.93 % (268503)------------------------------
% 13.25/2.93 % (268503)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.25/2.93 % (268503)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.25/2.93 % (268503)CaDiCaL version: 2.1.3
% 13.25/2.93 % (268503)Termination reason: Refutation not found, incomplete strategy
% 13.25/2.93 % (268503)Time elapsed: 0.023 s
% 13.25/2.93 % (268503)Peak memory usage: 94 MB
% 13.25/2.93 % (268503)Instructions burned: 35 (million)
% 13.25/2.93 % (268502)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2721692393:s2a=on:i=139:gtg=position_2998 on theBenchmark for (2998ds/139Mi)
% 13.25/2.93 % (268501)Instruction limit reached!
% 13.25/2.93 % (268501)------------------------------
% 13.25/2.93 % (268501)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.25/2.93 % (268501)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.25/2.93 % (268501)CaDiCaL version: 2.1.3
% 13.25/2.93 % (268501)Termination reason: Instruction limit
% 13.25/2.93 % (268501)Termination phase: Saturation
% 13.25/2.93 % (268501)Time elapsed: 0.062 s
% 13.25/2.93 % (268501)Peak memory usage: 93 MB
% 13.25/2.93 % (268501)Instructions burned: 121 (million)
% 13.25/2.93 % (268502)Instruction limit reached!
% 13.25/2.93 % (268502)------------------------------
% 13.25/2.93 % (268502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.25/2.93 % (268502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.25/2.93 % (268502)CaDiCaL version: 2.1.3
% 13.25/2.93 % (268502)Termination reason: Instruction limit
% 13.25/2.93 % (268502)Termination phase: Property scanning
% 13.25/2.93 % (268502)Time elapsed: 0.107 s
% 13.25/2.93 % (268502)Peak memory usage: 93 MB
% 13.25/2.93 % (268502)Instructions burned: 139 (million)
% 13.25/2.93 % (268511)lrs+10_1_sil=8000:sp=occurrence:random_seed=682625426:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi)
% 13.25/2.93 % (268520)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2602997968:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2995 on theBenchmark for (2995ds/157Mi)
% 13.25/2.93 % (268511)Refutation not found, incomplete strategy
% 13.25/2.93 % (268511)------------------------------
% 13.25/2.93 % (268511)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.25/2.93 % (268511)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.25/2.93 % (268511)CaDiCaL version: 2.1.3
% 13.25/2.93 % (268511)Termination reason: Refutation not found, incomplete strategy
% 13.25/2.93 % (268511)Time elapsed: 0.030 s
% 19.74/3.70 % (268511)Peak memory usage: 94 MB
% 19.74/3.70 % (268511)Instructions burned: 22 (million)
% 19.74/3.70 % (268500)------------------------------
% 19.74/3.70 % (268500)------------------------------
% 19.74/3.70 % (268520)Refutation not found, incomplete strategy
% 19.74/3.70 % (268520)------------------------------
% 19.74/3.70 % (268520)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.74/3.70 % (268520)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.74/3.70 % (268520)CaDiCaL version: 2.1.3
% 19.74/3.70 % (268520)Termination reason: Refutation not found, incomplete strategy
% 19.74/3.70 % (268520)Time elapsed: 0.027 s
% 19.74/3.70 % (268520)Peak memory usage: 94 MB
% 19.74/3.70 % (268520)Instructions burned: 57 (million)
% 19.74/3.70 % (268503)------------------------------
% 19.74/3.70 % (268503)------------------------------
% 19.74/3.70 % (268531)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3217860454:i=325:sd=1:ss=axioms:sgt=32_2993 on theBenchmark for (2993ds/325Mi)
% 19.74/3.70 % (268520)------------------------------
% 19.74/3.70 % (268520)------------------------------
% 19.74/3.70 % (268531)Refutation not found, incomplete strategy
% 19.74/3.70 % (268531)------------------------------
% 19.74/3.70 % (268531)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.74/3.70 % (268531)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.74/3.70 % (268531)CaDiCaL version: 2.1.3
% 19.74/3.70 % (268531)Termination reason: Refutation not found, incomplete strategy
% 19.74/3.70 % (268531)Time elapsed: 0.026 s
% 19.74/3.70 % (268531)Peak memory usage: 94 MB
% 19.74/3.70 % (268531)Instructions burned: 20 (million)
% 19.74/3.70 % (268533)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=310144935:s2a=on:i=248:s2at=1.23:gtg=position_2992 on theBenchmark for (2992ds/248Mi)
% 19.74/3.70 % (268511)------------------------------
% 19.74/3.70 % (268511)------------------------------
% 19.74/3.70 % (268536)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2753744822:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2990 on theBenchmark for (2990ds/294Mi)
% 19.74/3.70 % (268536)Refutation not found, incomplete strategy
% 19.74/3.70 % (268536)------------------------------
% 19.74/3.70 % (268536)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.74/3.70 % (268536)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.74/3.70 % (268536)CaDiCaL version: 2.1.3
% 19.74/3.70 % (268536)Termination reason: Refutation not found, incomplete strategy
% 19.74/3.70 % (268536)Time elapsed: 0.020 s
% 19.74/3.70 % (268536)Peak memory usage: 94 MB
% 19.74/3.70 % (268536)Instructions burned: 32 (million)
% 19.74/3.70 % (268533)Instruction limit reached!
% 19.74/3.70 % (268533)------------------------------
% 19.74/3.70 % (268533)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.74/3.70 % (268533)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.74/3.70 % (268533)CaDiCaL version: 2.1.3
% 19.74/3.70 % (268533)Termination reason: Instruction limit
% 19.74/3.70 % (268533)Termination phase: Saturation
% 19.74/3.70 % (268533)Time elapsed: 0.241 s
% 19.74/3.70 % (268533)Peak memory usage: 99 MB
% 19.74/3.70 % (268533)Instructions burned: 249 (million)
% 19.74/3.70 % (268531)------------------------------
% 19.74/3.70 % (268531)------------------------------
% 19.74/3.70 % (268499)Refutation not found, incomplete strategy
% 19.74/3.70 % (268499)------------------------------
% 19.74/3.70 % (268499)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.74/3.70 % (268499)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.74/3.70 % (268499)CaDiCaL version: 2.1.3
% 19.74/3.70 % (268499)Termination reason: Refutation not found, incomplete strategy
% 19.74/3.70 % (268499)Time elapsed: 1.029 s
% 19.74/3.70 % (268499)Peak memory usage: 141 MB
% 19.74/3.70 % (268499)Instructions burned: 1044 (million)
% 19.74/3.70 % (268542)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3298304540:i=2350_2989 on theBenchmark for (2989ds/2350Mi)
% 19.74/3.70 % (268536)------------------------------
% 19.74/3.70 % (268536)------------------------------
% 19.74/3.70 % (268547)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=587090043:cts=off:i=113:fsr=off:ss=included:sgt=4_2987 on theBenchmark for (2987ds/113Mi)
% 19.74/3.70 % (268551)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1073319750:i=127:av=off:fsr=off:sup=off_2986 on theBenchmark for (2986ds/127Mi)
% 26.37/4.57 % (268547)Instruction limit reached!
% 26.37/4.57 % (268547)------------------------------
% 26.37/4.57 % (268547)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.37/4.57 % (268547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.37/4.57 % (268547)CaDiCaL version: 2.1.3
% 26.37/4.57 % (268547)Termination reason: Instruction limit
% 26.37/4.57 % (268547)Termination phase: Saturation
% 26.37/4.57 % (268547)Time elapsed: 0.093 s
% 26.37/4.57 % (268547)Peak memory usage: 94 MB
% 26.37/4.57 % (268547)Instructions burned: 113 (million)
% 26.37/4.57 % (268553)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=23247342:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2985 on theBenchmark for (2985ds/114Mi)
% 26.37/4.57 % (268553)Instruction limit reached!
% 26.37/4.57 % (268553)------------------------------
% 26.37/4.57 % (268553)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.37/4.57 % (268553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.37/4.57 % (268553)CaDiCaL version: 2.1.3
% 26.37/4.57 % (268553)Termination reason: Instruction limit
% 26.37/4.57 % (268553)Termination phase: Saturation
% 26.37/4.57 % (268553)Time elapsed: 0.070 s
% 26.37/4.57 % (268553)Peak memory usage: 94 MB
% 26.37/4.57 % (268553)Instructions burned: 115 (million)
% 26.37/4.57 % (268499)------------------------------
% 26.37/4.57 % (268499)------------------------------
% 26.37/4.57 % (268551)Instruction limit reached!
% 26.37/4.57 % (268551)------------------------------
% 26.37/4.57 % (268551)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.37/4.57 % (268551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.37/4.57 % (268551)CaDiCaL version: 2.1.3
% 26.37/4.57 % (268551)Termination reason: Instruction limit
% 26.37/4.57 % (268551)Termination phase: Blocked clause elimination
% 26.37/4.57 % (268551)Time elapsed: 0.131 s
% 26.37/4.57 % (268551)Peak memory usage: 95 MB
% 26.37/4.57 % (268551)Instructions burned: 128 (million)
% 26.37/4.57 % (268561)lrs+10_1_sil=8000:sp=occurrence:random_seed=4231199170:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2983 on theBenchmark for (2983ds/907Mi)
% 26.37/4.57 % (268567)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2574288105:i=5202:ss=axioms:sgt=16_2982 on theBenchmark for (2982ds/5202Mi)
% 26.37/4.57 % (268561)Refutation not found, incomplete strategy
% 26.37/4.57 % (268561)------------------------------
% 26.37/4.57 % (268561)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.37/4.57 % (268561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.37/4.57 % (268561)CaDiCaL version: 2.1.3
% 26.37/4.57 % (268561)Termination reason: Refutation not found, incomplete strategy
% 26.37/4.57 % (268561)Time elapsed: 0.106 s
% 26.37/4.57 % (268561)Peak memory usage: 94 MB
% 26.37/4.57 % (268561)Instructions burned: 100 (million)
% 26.37/4.57 % (268566)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=4212073131:i=437:sd=1:aac=none:ss=included_2982 on theBenchmark for (2982ds/437Mi)
% 26.37/4.57 % (268566)Refutation not found, incomplete strategy
% 26.37/4.57 % (268566)------------------------------
% 26.37/4.57 % (268566)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.37/4.57 % (268566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.37/4.57 % (268566)CaDiCaL version: 2.1.3
% 26.37/4.57 % (268566)Termination reason: Refutation not found, incomplete strategy
% 26.37/4.57 % (268566)Time elapsed: 0.015 s
% 26.37/4.57 % (268566)Peak memory usage: 94 MB
% 26.37/4.57 % (268566)Instructions burned: 18 (million)
% 26.37/4.57 % (268568)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=4150311213:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2982 on theBenchmark for (2982ds/134Mi)
% 26.37/4.57 % (268568)Refutation not found, incomplete strategy
% 26.37/4.57 % (268568)------------------------------
% 26.37/4.57 % (268568)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 26.37/4.57 % (268568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.37/4.57 % (268568)CaDiCaL version: 2.1.3
% 26.37/4.57 % (268568)Termination reason: Refutation not found, incomplete strategy
% 26.37/4.57 % (268568)Time elapsed: 0.018 s
% 26.37/4.57 % (268568)Peak memory usage: 95 MB
% 26.37/4.57 % (268568)Instructions burned: 25 (million)
% 26.37/4.57 % (268561)------------------------------
% 26.37/4.57 % (268561)------------------------------
% 26.37/4.57 % (268566)------------------------------
% 26.37/4.57 % (268566)------------------------------
% 23.89/5.71 % (268568)------------------------------
% 23.89/5.71 % (268568)------------------------------
% 23.89/5.71 % (268577)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2438230497:st=8:i=592:sd=3:ep=RST:ss=axioms_2977 on theBenchmark for (2977ds/592Mi)
% 23.89/5.71 % (268577)Refutation not found, incomplete strategy
% 23.89/5.71 % (268577)------------------------------
% 23.89/5.71 % (268577)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.89/5.71 % (268577)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.89/5.71 % (268577)CaDiCaL version: 2.1.3
% 23.89/5.71 % (268577)Termination reason: Refutation not found, incomplete strategy
% 23.89/5.71 % (268577)Time elapsed: 0.023 s
% 23.89/5.71 % (268577)Peak memory usage: 94 MB
% 23.89/5.71 % (268577)Instructions burned: 31 (million)
% 23.89/5.71 % (268578)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1127189254:st=3:i=13193:sd=3:ss=axioms_2977 on theBenchmark for (2977ds/13193Mi)
% 23.89/5.71 % (268579)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=3827824946:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2976 on theBenchmark for (2976ds/125Mi)
% 23.89/5.71 % (268579)Instruction limit reached!
% 23.89/5.71 % (268579)------------------------------
% 23.89/5.71 % (268579)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.89/5.71 % (268579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.89/5.71 % (268579)CaDiCaL version: 2.1.3
% 23.89/5.71 % (268579)Termination reason: Instruction limit
% 23.89/5.71 % (268579)Termination phase: Saturation
% 23.89/5.71 % (268579)Time elapsed: 0.070 s
% 23.89/5.71 % (268579)Peak memory usage: 95 MB
% 23.89/5.71 % (268579)Instructions burned: 126 (million)
% 23.89/5.71 % (268577)------------------------------
% 23.89/5.71 % (268577)------------------------------
% 23.89/5.71 % (268610)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3409082518:i=134:gtgl=5:slsql=off:gtg=exists_sym_2974 on theBenchmark for (2974ds/134Mi)
% 23.89/5.71 % (268610)Instruction limit reached!
% 23.89/5.71 % (268610)------------------------------
% 23.89/5.71 % (268610)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.89/5.72 % (268610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.89/5.72 % (268610)CaDiCaL version: 2.1.3
% 23.89/5.72 % (268610)Termination reason: Instruction limit
% 23.89/5.72 % (268610)Termination phase: Preprocessing 3
% 23.89/5.72 % (268610)Time elapsed: 0.067 s
% 23.89/5.72 % (268610)Peak memory usage: 92 MB
% 23.89/5.72 % (268610)Instructions burned: 135 (million)
% 23.89/5.72 % (268644)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=134784376:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2973 on theBenchmark for (2973ds/141Mi)
% 23.89/5.72 % (268644)Refutation not found, incomplete strategy
% 23.89/5.72 % (268644)------------------------------
% 23.89/5.72 % (268644)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.89/5.72 % (268644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.89/5.72 % (268644)CaDiCaL version: 2.1.3
% 23.89/5.72 % (268644)Termination reason: Refutation not found, incomplete strategy
% 23.89/5.72 % (268644)Time elapsed: 0.017 s
% 23.89/5.72 % (268644)Peak memory usage: 94 MB
% 23.89/5.72 % (268644)Instructions burned: 24 (million)
% 23.89/5.72 % (268678)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=4250606933:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2972 on theBenchmark for (2972ds/431Mi)
% 23.89/5.72 % (268678)Refutation not found, incomplete strategy
% 23.89/5.72 % (268678)------------------------------
% 23.89/5.72 % (268678)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.89/5.72 % (268678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.89/5.72 % (268678)CaDiCaL version: 2.1.3
% 23.89/5.72 % (268678)Termination reason: Refutation not found, incomplete strategy
% 23.89/5.72 % (268678)Time elapsed: 0.015 s
% 23.89/5.72 % (268678)Peak memory usage: 94 MB
% 23.89/5.72 % (268678)Instructions burned: 20 (million)
% 23.89/5.72 % (268542)Instruction limit reached!
% 23.89/5.72 % (268542)------------------------------
% 23.89/5.72 % (268542)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.89/5.72 % (268542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.89/5.72 % (268542)CaDiCaL version: 2.1.3
% 23.89/5.72 % (268542)Termination reason: Instruction limit
% 23.89/5.72 % (268542)Termination phase: Saturation
% 23.89/5.72 % (268542)Time elapsed: 1.669 s
% 23.89/5.72 % (268542)Peak memory usage: 196 MB
% 23.89/5.72 % (268542)Instructions burned: 2350 (million)
% 23.89/5.72 % (268644)------------------------------
% 23.89/5.72 % (268644)------------------------------
% 23.89/5.72 % (268578)Refutation not found, incomplete strategy
% 23.89/5.72 % (268578)------------------------------
% 23.89/5.72 % (268578)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.89/5.72 % (268578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.89/5.72 % (268578)CaDiCaL version: 2.1.3
% 23.89/5.72 % (268578)Termination reason: Refutation not found, incomplete strategy
% 23.89/5.72 % (268578)Time elapsed: 0.737 s
% 23.89/5.72 % (268578)Peak memory usage: 142 MB
% 23.89/5.72 % (268578)Instructions burned: 1102 (million)
% 23.89/5.72 % (268729)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=2442951049:i=6060:aac=none:ins=25_2969 on theBenchmark for (2969ds/6060Mi)
% 23.89/5.72 % (268678)------------------------------
% 23.89/5.72 % (268678)------------------------------
% 23.89/5.72 % (268743)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=3680828973:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2969 on theBenchmark for (2969ds/150Mi)
% 23.89/5.72 % (268743)Instruction limit reached!
% 23.89/5.72 % (268743)------------------------------
% 23.89/5.72 % (268743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.89/5.72 % (268743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.89/5.72 % (268743)CaDiCaL version: 2.1.3
% 23.89/5.72 % (268743)Termination reason: Instruction limit
% 23.89/5.72 % (268743)Termination phase: Saturation
% 23.89/5.72 % (268743)Time elapsed: 0.081 s
% 23.89/5.72 % (268743)Peak memory usage: 97 MB
% 23.89/5.72 % (268743)Instructions burned: 150 (million)
% 23.89/5.72 % (268745)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2064037035:i=14155:bd=all_2967 on theBenchmark for (2967ds/14155Mi)
% 23.89/5.72 % (268578)------------------------------
% 23.89/5.72 % (268578)------------------------------
% 23.89/5.72 % (268747)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3037241546:i=667:av=off:fsr=off_2966 on theBenchmark for (2966ds/667Mi)
% 23.89/5.72 % (268747)Refutation not found, incomplete strategy
% 23.89/5.72 % (268747)------------------------------
% 23.89/5.72 % (268747)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.89/5.72 % (268747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.89/5.72 % (268747)CaDiCaL version: 2.1.3
% 23.89/5.72 % (268747)Termination reason: Refutation not found, incomplete strategy
% 23.89/5.72 % (268747)Time elapsed: 0.068 s
% 23.89/5.72 % (268747)Peak memory usage: 97 MB
% 23.89/5.72 % (268747)Instructions burned: 113 (million)
% 23.89/5.72 % (268749)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=1285292136:s2a=on:i=185:s2at=1.8:fdi=4_2965 on theBenchmark for (2965ds/185Mi)
% 23.89/5.72 % (268749)Instruction limit reached!
% 23.89/5.72 % (268749)------------------------------
% 23.89/5.72 % (268749)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.89/5.72 % (268749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.89/5.72 % (268749)CaDiCaL version: 2.1.3
% 23.89/5.72 % (268749)Termination reason: Instruction limit
% 23.89/5.72 % (268749)Termination phase: Saturation
% 23.89/5.72 % (268749)Time elapsed: 0.108 s
% 23.89/5.72 % (268749)Peak memory usage: 100 MB
% 23.89/5.72 % (268749)Instructions burned: 187 (million)
% 23.89/5.72 % (268747)------------------------------
% 23.89/5.72 % (268747)------------------------------
% 23.89/5.72 % (268752)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=1094328164:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2963 on theBenchmark for (2963ds/193Mi)
% 23.89/5.72 % (268752)Refutation not found, incomplete strategy
% 23.89/5.72 % (268752)------------------------------
% 23.89/5.72 % (268752)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.89/5.72 % (268752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.89/5.72 % (268752)CaDiCaL version: 2.1.3
% 23.89/5.72 % (268752)Termination reason: Refutation not found, incomplete strategy
% 23.89/5.72 % (268752)Time elapsed: 0.045 s
% 23.89/5.72 % (268752)Peak memory usage: 95 MB
% 23.89/5.72 % (268752)Instructions burned: 70 (million)
% 23.89/5.72 % (268753)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=2005949755:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2962 on theBenchmark for (2962ds/4850Mi)
% 23.89/5.72 % (268752)------------------------------
% 23.89/5.72 % (268752)------------------------------
% 23.89/5.72 % (268567)Instruction limit reached!
% 23.89/5.72 % (268567)------------------------------
% 23.89/5.72 % (268567)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.89/5.72 % (268567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.89/5.72 % (268567)CaDiCaL version: 2.1.3
% 23.89/5.72 % (268567)Termination reason: Instruction limit
% 23.89/5.72 % (268567)Termination phase: Saturation
% 23.89/5.72 % (268567)Time elapsed: 2.302 s
% 23.89/5.72 % (268567)Peak memory usage: 183 MB
% 23.89/5.72 % (268567)Instructions burned: 5203 (million)
% 23.89/5.72 % (268756)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=1484105364:i=12111:sd=1:ss=included_2958 on theBenchmark for (2958ds/12111Mi)
% 23.89/5.72 % (268757)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2418184744:i=319:kws=precedence:fsr=off_2957 on theBenchmark for (2957ds/319Mi)
% 23.89/5.72 % (268757)Instruction limit reached!
% 23.89/5.72 % (268757)------------------------------
% 23.89/5.72 % (268757)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.89/5.72 % (268757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.89/5.72 % (268757)CaDiCaL version: 2.1.3
% 23.89/5.72 % (268757)Termination reason: Instruction limit
% 23.89/5.72 % (268757)Termination phase: Saturation
% 23.89/5.72 % (268757)Time elapsed: 0.072 s
% 23.89/5.72 % (268757)Peak memory usage: 100 MB
% 23.89/5.72 % (268757)Instructions burned: 320 (million)
% 23.89/5.72 % (268760)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=2545314867:i=2064:ep=RST_2955 on theBenchmark for (2955ds/2064Mi)
% 23.89/5.72 % (268760)Refutation not found, incomplete strategy
% 23.89/5.72 % (268760)------------------------------
% 23.89/5.72 % (268760)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.89/5.72 % (268760)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.89/5.72 % (268760)CaDiCaL version: 2.1.3
% 23.89/5.72 % (268760)Termination reason: Refutation not found, incomplete strategy
% 23.89/5.72 % (268760)Time elapsed: 0.046 s
% 23.89/5.72 % (268760)Peak memory usage: 98 MB
% 23.89/5.72 % (268760)Instructions burned: 158 (million)
% 23.89/5.72 % (268760)------------------------------
% 23.89/5.72 % (268760)------------------------------
% 23.89/5.72 % (268497)First to succeed.
% 23.89/5.72 % (268497)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-268362"
% 23.89/5.72 % (268762)dis-1011_128_sil=32000:random_seed=1733482859:i=3706:ep=RST:av=off_2952 on theBenchmark for (2952ds/3706Mi)
% 23.89/5.72 % (268762)Also succeeded, but the first one will report.
% 23.89/5.72 % (268756)Refutation not found, incomplete strategy
% 23.89/5.72 % (268756)------------------------------
% 23.89/5.72 % (268756)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.89/5.72 % (268756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.89/5.72 % (268756)CaDiCaL version: 2.1.3
% 23.89/5.72 % (268756)Termination reason: Refutation not found, incomplete strategy
% 23.89/5.72 % (268756)Time elapsed: 0.694 s
% 23.89/5.72 % (268756)Peak memory usage: 148 MB
% 23.89/5.72 % (268756)Instructions burned: 1048 (million)
% 23.89/5.72 % (268497)Refutation found. Thanks to Tanya!
% 23.89/5.72 % SZS status Theorem for theBenchmark
% 23.89/5.72 % SZS output start Proof for theBenchmark
% See solution above
% 0.20/5.91 % (268497)------------------------------
% 0.20/5.91 % (268497)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.20/5.91 % (268497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/5.91 % (268497)CaDiCaL version: 2.1.3
% 0.20/5.91 % (268497)Termination reason: Refutation
% 0.20/5.91 % (268497)Time elapsed: 4.441 s
% 0.20/5.91 % (268497)Peak memory usage: 197 MB
% 0.20/5.91 % (268497)Instructions burned: 5736 (million)
% 0.20/5.91 % (268497)------------------------------
% 0.20/5.91 % (268497)------------------------------
% 0.20/5.91 % (268362)Success in time 5.044 s
% 0.20/5.91 % Vampire exiting
%------------------------------------------------------------------------------