%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : CSR040+4 : TPTP v9.3.1. Released v3.4.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:42:12 AM UTC 2026
% Result : Theorem 48.51s 8.39s
% Output : Refutation 0.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 21
% Syntax : Number of formulae : 83 ( 6 unt; 0 def)
% Number of atoms : 160 ( 0 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 140 ( 63 ~; 55 |; 2 &)
% ( 0 <=>; 20 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 4 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 : 74 ( 74 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f318,axiom,
! [X0] :
( tptpcol_0_0(X0)
=> individual(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3_318) ).
fof(f448,axiom,
! [X0] :
( tptpcol_10_109061(X0)
=> tptpcol_9_109060(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3_448) ).
fof(f733,axiom,
! [X0] :
( tptpcol_9_109060(X0)
=> tptpcol_8_109059(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3_733) ).
fof(f1291,axiom,
! [X0] :
( tptpcol_8_109059(X0)
=> tptpcol_7_108547(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3_1291) ).
fof(f1714,axiom,
! [X0] :
( firstordercollection(X0)
=> fixedordercollection(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3_1714) ).
fof(f3253,axiom,
! [X0] :
( tptpcol_6_108546(X0)
=> tptpcol_5_106498(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3_3253) ).
fof(f3389,axiom,
! [X0] :
( tptpcol_12_109157(X0)
=> tptpcol_11_109125(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3_3389) ).
fof(f4028,axiom,
! [X0] :
~ ( collection(X0)
& individual(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3_4028) ).
fof(f5043,axiom,
! [X0] :
( tptpcol_1_65536(X0)
=> tptpcol_0_0(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3_5043) ).
fof(f5511,axiom,
! [X0] :
( tptpcol_2_98304(X0)
=> tptpcol_1_65536(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3_5511) ).
fof(f5949,axiom,
! [X0] :
( tptpcol_4_106497(X0)
=> tptpcol_3_98305(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3_5949) ).
fof(f6733,axiom,
! [X0] :
( tptpcol_15_109185(X0)
=> tptpcol_14_109181(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3_6733) ).
fof(f7614,axiom,
! [X0] :
( tptpcol_14_109181(X0)
=> tptpcol_13_109173(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3_7614) ).
fof(f9044,axiom,
! [X0] :
( tptpcol_7_108547(X0)
=> tptpcol_6_108546(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3_9044) ).
fof(f12015,axiom,
! [X0] :
( fixedordercollection(X0)
=> collection(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3_12015) ).
fof(f15240,axiom,
! [X0] :
( tptpcol_5_106498(X0)
=> tptpcol_4_106497(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3_15240) ).
fof(f15564,axiom,
! [X0] :
( tptpcol_13_109173(X0)
=> tptpcol_12_109157(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3_15564) ).
fof(f20268,axiom,
firstordercollection(c_tptpcol_16_62187),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3_20268) ).
fof(f22390,axiom,
! [X0] :
( tptpcol_3_98305(X0)
=> tptpcol_2_98304(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3_22390) ).
fof(f24107,axiom,
! [X0] :
( tptpcol_11_109125(X0)
=> tptpcol_10_109061(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3_24107) ).
fof(f44217,conjecture,
( mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwthedailybulletincompostcardsmar9chtm)),c_translation_14))
=> ~ tptpcol_15_109185(c_tptpcol_16_62187) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',query190) ).
fof(f44218,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)],[f44217]) ).
fof(f46782,plain,
! [X0] :
( individual(X0)
| ~ tptpcol_0_0(X0) ),
inference(ennf_transformation,[],[f318]) ).
fof(f46808,plain,
! [X0] :
( tptpcol_9_109060(X0)
| ~ tptpcol_10_109061(X0) ),
inference(ennf_transformation,[],[f448]) ).
fof(f46883,plain,
! [X0] :
( tptpcol_8_109059(X0)
| ~ tptpcol_9_109060(X0) ),
inference(ennf_transformation,[],[f733]) ).
fof(f47023,plain,
! [X0] :
( tptpcol_7_108547(X0)
| ~ tptpcol_8_109059(X0) ),
inference(ennf_transformation,[],[f1291]) ).
fof(f47131,plain,
! [X0] :
( fixedordercollection(X0)
| ~ firstordercollection(X0) ),
inference(ennf_transformation,[],[f1714]) ).
fof(f47489,plain,
! [X0] :
( tptpcol_5_106498(X0)
| ~ tptpcol_6_108546(X0) ),
inference(ennf_transformation,[],[f3253]) ).
fof(f47512,plain,
! [X0] :
( tptpcol_11_109125(X0)
| ~ tptpcol_12_109157(X0) ),
inference(ennf_transformation,[],[f3389]) ).
fof(f47681,plain,
! [X0] :
( ~ collection(X0)
| ~ individual(X0) ),
inference(ennf_transformation,[],[f4028]) ).
fof(f47928,plain,
! [X0] :
( tptpcol_0_0(X0)
| ~ tptpcol_1_65536(X0) ),
inference(ennf_transformation,[],[f5043]) ).
fof(f48039,plain,
! [X0] :
( tptpcol_1_65536(X0)
| ~ tptpcol_2_98304(X0) ),
inference(ennf_transformation,[],[f5511]) ).
fof(f48161,plain,
! [X0] :
( tptpcol_3_98305(X0)
| ~ tptpcol_4_106497(X0) ),
inference(ennf_transformation,[],[f5949]) ).
fof(f48350,plain,
! [X0] :
( tptpcol_14_109181(X0)
| ~ tptpcol_15_109185(X0) ),
inference(ennf_transformation,[],[f6733]) ).
fof(f48596,plain,
! [X0] :
( tptpcol_13_109173(X0)
| ~ tptpcol_14_109181(X0) ),
inference(ennf_transformation,[],[f7614]) ).
fof(f48963,plain,
! [X0] :
( tptpcol_6_108546(X0)
| ~ tptpcol_7_108547(X0) ),
inference(ennf_transformation,[],[f9044]) ).
fof(f49668,plain,
! [X0] :
( collection(X0)
| ~ fixedordercollection(X0) ),
inference(ennf_transformation,[],[f12015]) ).
fof(f50480,plain,
! [X0] :
( tptpcol_4_106497(X0)
| ~ tptpcol_5_106498(X0) ),
inference(ennf_transformation,[],[f15240]) ).
fof(f50551,plain,
! [X0] :
( tptpcol_12_109157(X0)
| ~ tptpcol_13_109173(X0) ),
inference(ennf_transformation,[],[f15564]) ).
fof(f52203,plain,
! [X0] :
( tptpcol_2_98304(X0)
| ~ tptpcol_3_98305(X0) ),
inference(ennf_transformation,[],[f22390]) ).
fof(f52611,plain,
! [X0] :
( tptpcol_10_109061(X0)
| ~ tptpcol_11_109125(X0) ),
inference(ennf_transformation,[],[f24107]) ).
fof(f66315,plain,
( tptpcol_15_109185(c_tptpcol_16_62187)
& mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwthedailybulletincompostcardsmar9chtm)),c_translation_14)) ),
inference(ennf_transformation,[],[f44218]) ).
fof(f66629,plain,
! [X0] :
( ~ tptpcol_0_0(X0)
| individual(X0) ),
inference(cnf_transformation,[],[f46782]) ).
fof(f66758,plain,
! [X0] :
( tptpcol_9_109060(X0)
| ~ tptpcol_10_109061(X0) ),
inference(cnf_transformation,[],[f46808]) ).
fof(f67039,plain,
! [X0] :
( tptpcol_8_109059(X0)
| ~ tptpcol_9_109060(X0) ),
inference(cnf_transformation,[],[f46883]) ).
fof(f67587,plain,
! [X0] :
( tptpcol_7_108547(X0)
| ~ tptpcol_8_109059(X0) ),
inference(cnf_transformation,[],[f47023]) ).
fof(f68002,plain,
! [X0] :
( fixedordercollection(X0)
| ~ firstordercollection(X0) ),
inference(cnf_transformation,[],[f47131]) ).
fof(f69508,plain,
! [X0] :
( tptpcol_5_106498(X0)
| ~ tptpcol_6_108546(X0) ),
inference(cnf_transformation,[],[f47489]) ).
fof(f69640,plain,
! [X0] :
( tptpcol_11_109125(X0)
| ~ tptpcol_12_109157(X0) ),
inference(cnf_transformation,[],[f47512]) ).
fof(f70265,plain,
! [X0] :
( ~ collection(X0)
| ~ individual(X0) ),
inference(cnf_transformation,[],[f47681]) ).
fof(f71258,plain,
! [X0] :
( ~ tptpcol_1_65536(X0)
| tptpcol_0_0(X0) ),
inference(cnf_transformation,[],[f47928]) ).
fof(f71715,plain,
! [X0] :
( ~ tptpcol_2_98304(X0)
| tptpcol_1_65536(X0) ),
inference(cnf_transformation,[],[f48039]) ).
fof(f72143,plain,
! [X0] :
( tptpcol_3_98305(X0)
| ~ tptpcol_4_106497(X0) ),
inference(cnf_transformation,[],[f48161]) ).
fof(f72914,plain,
! [X0] :
( tptpcol_14_109181(X0)
| ~ tptpcol_15_109185(X0) ),
inference(cnf_transformation,[],[f48350]) ).
fof(f73780,plain,
! [X0] :
( tptpcol_13_109173(X0)
| ~ tptpcol_14_109181(X0) ),
inference(cnf_transformation,[],[f48596]) ).
fof(f75181,plain,
! [X0] :
( tptpcol_6_108546(X0)
| ~ tptpcol_7_108547(X0) ),
inference(cnf_transformation,[],[f48963]) ).
fof(f78105,plain,
! [X0] :
( ~ fixedordercollection(X0)
| collection(X0) ),
inference(cnf_transformation,[],[f49668]) ).
fof(f81265,plain,
! [X0] :
( tptpcol_4_106497(X0)
| ~ tptpcol_5_106498(X0) ),
inference(cnf_transformation,[],[f50480]) ).
fof(f81583,plain,
! [X0] :
( tptpcol_12_109157(X0)
| ~ tptpcol_13_109173(X0) ),
inference(cnf_transformation,[],[f50551]) ).
fof(f86203,plain,
firstordercollection(c_tptpcol_16_62187),
inference(cnf_transformation,[],[f20268]) ).
fof(f88282,plain,
! [X0] :
( tptpcol_2_98304(X0)
| ~ tptpcol_3_98305(X0) ),
inference(cnf_transformation,[],[f52203]) ).
fof(f89959,plain,
! [X0] :
( tptpcol_10_109061(X0)
| ~ tptpcol_11_109125(X0) ),
inference(cnf_transformation,[],[f52611]) ).
fof(f108043,plain,
tptpcol_15_109185(c_tptpcol_16_62187),
inference(cnf_transformation,[],[f66315]) ).
fof(f108091,plain,
! [X0] :
( collection(X0)
| ~ firstordercollection(X0) ),
inference(resolution,[],[f78105,f68002]) ).
fof(f108103,plain,
! [X0] :
( tptpcol_1_65536(X0)
| ~ tptpcol_3_98305(X0) ),
inference(resolution,[],[f88282,f71715]) ).
fof(f108158,plain,
! [X0] :
( ~ firstordercollection(X0)
| ~ individual(X0) ),
inference(resolution,[],[f108091,f70265]) ).
fof(f108164,plain,
! [X0] :
( tptpcol_0_0(X0)
| ~ tptpcol_3_98305(X0) ),
inference(resolution,[],[f108103,f71258]) ).
fof(f108391,plain,
~ individual(c_tptpcol_16_62187),
inference(resolution,[],[f108158,f86203]) ).
fof(f108731,plain,
! [X0] :
( ~ tptpcol_3_98305(X0)
| individual(X0) ),
inference(resolution,[],[f108164,f66629]) ).
fof(f109014,plain,
! [X0] :
( ~ tptpcol_4_106497(X0)
| individual(X0) ),
inference(resolution,[],[f108731,f72143]) ).
fof(f109216,plain,
! [X0] :
( ~ tptpcol_5_106498(X0)
| individual(X0) ),
inference(resolution,[],[f109014,f81265]) ).
fof(f109374,plain,
! [X0] :
( ~ tptpcol_6_108546(X0)
| individual(X0) ),
inference(resolution,[],[f109216,f69508]) ).
fof(f109554,plain,
! [X0] :
( ~ tptpcol_7_108547(X0)
| individual(X0) ),
inference(resolution,[],[f109374,f75181]) ).
fof(f109591,plain,
! [X0] :
( ~ tptpcol_8_109059(X0)
| individual(X0) ),
inference(resolution,[],[f109554,f67587]) ).
fof(f109615,plain,
! [X0] :
( ~ tptpcol_9_109060(X0)
| individual(X0) ),
inference(resolution,[],[f109591,f67039]) ).
fof(f109633,plain,
! [X0] :
( ~ tptpcol_10_109061(X0)
| individual(X0) ),
inference(resolution,[],[f109615,f66758]) ).
fof(f109650,plain,
! [X0] :
( ~ tptpcol_11_109125(X0)
| individual(X0) ),
inference(resolution,[],[f109633,f89959]) ).
fof(f109666,plain,
! [X0] :
( ~ tptpcol_12_109157(X0)
| individual(X0) ),
inference(resolution,[],[f109650,f69640]) ).
fof(f109684,plain,
! [X0] :
( ~ tptpcol_13_109173(X0)
| individual(X0) ),
inference(resolution,[],[f109666,f81583]) ).
fof(f109695,plain,
! [X0] :
( ~ tptpcol_14_109181(X0)
| individual(X0) ),
inference(resolution,[],[f109684,f73780]) ).
fof(f109704,plain,
! [X0] :
( ~ tptpcol_15_109185(X0)
| individual(X0) ),
inference(resolution,[],[f109695,f72914]) ).
fof(f109711,plain,
individual(c_tptpcol_16_62187),
inference(resolution,[],[f109704,f108043]) ).
fof(f109712,plain,
$false,
inference(forward_subsumption_resolution,[],[f109711,f108391]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR040+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.20 % Computer : n017.cluster.edu
% 0.08/0.20 % Model : x86_64 x86_64
% 0.08/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.20 % Memory : 8046.5625MB
% 0.08/0.20 % OS : Linux 6.8.0-71-generic
% 0.08/0.20 % CPULimit : 300
% 0.08/0.20 % WCLimit : 300
% 0.08/0.20 % DateTime : Mon Sep 28 22:10:21 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.24 Running first-order theorem proving
% 0.08/0.24 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
% 13.67/3.40 % (4096205)Detected formulas, will run a generic FOF schedule.
% 13.67/3.40 % (4096216)dis-21_1_sil=8000:lcm=predicate:random_seed=3552714356:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2990 on theBenchmark for (2990ds/129Mi)
% 13.67/3.40 % (4096215)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2651812826:s2a=on:i=139:gtg=position_2990 on theBenchmark for (2990ds/139Mi)
% 13.67/3.40 % (4096213)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=614090370:i=109:sd=1:ins=1:gsp=on:ss=axioms_2990 on theBenchmark for (2990ds/109Mi)
% 13.67/3.40 % (4096212)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=3439761420:i=141695:sd=1:nm=32:gsp=on:ss=included_2990 on theBenchmark for (2990ds/141695Mi)
% 13.67/3.40 % (4096210)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=1745547881:i=141193_2990 on theBenchmark for (2990ds/141193Mi)
% 13.67/3.40 % (4096211)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=2887576655:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2990 on theBenchmark for (2990ds/134677Mi)
% 13.67/3.40 % (4096214)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=714473406:i=119:av=off:ss=axioms_2990 on theBenchmark for (2990ds/119Mi)
% 13.67/3.40 % (4096215)Instruction limit reached!
% 13.67/3.40 % (4096215)------------------------------
% 13.67/3.40 % (4096215)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.67/3.40 % (4096215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.67/3.40 % (4096215)CaDiCaL version: 2.1.3
% 13.67/3.40 % (4096215)Termination reason: Instruction limit
% 13.67/3.40 % (4096215)Termination phase: Property scanning
% 13.67/3.40 % (4096215)Time elapsed: 0.064 s
% 13.67/3.40 % (4096215)Peak memory usage: 110 MB
% 13.67/3.40 % (4096215)Instructions burned: 140 (million)
% 13.67/3.40 % (4096216)Instruction limit reached!
% 13.67/3.40 % (4096216)------------------------------
% 13.67/3.40 % (4096216)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.67/3.40 % (4096216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.67/3.40 % (4096216)CaDiCaL version: 2.1.3
% 13.67/3.40 % (4096216)Termination reason: Instruction limit
% 13.67/3.40 % (4096216)Termination phase: SInE selection
% 13.67/3.40 % (4096216)Time elapsed: 0.073 s
% 13.67/3.40 % (4096216)Peak memory usage: 111 MB
% 13.67/3.40 % (4096216)Instructions burned: 130 (million)
% 13.67/3.40 % (4096213)Instruction limit reached!
% 13.67/3.40 % (4096213)------------------------------
% 13.67/3.40 % (4096213)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.67/3.40 % (4096213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.67/3.40 % (4096213)CaDiCaL version: 2.1.3
% 13.67/3.40 % (4096213)Termination reason: Instruction limit
% 13.67/3.40 % (4096213)Termination phase: Saturation
% 13.67/3.40 % (4096213)Time elapsed: 0.078 s
% 13.67/3.40 % (4096213)Peak memory usage: 117 MB
% 13.67/3.40 % (4096213)Instructions burned: 109 (million)
% 13.67/3.40 % (4096214)Instruction limit reached!
% 13.67/3.40 % (4096214)------------------------------
% 13.67/3.40 % (4096214)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.67/3.40 % (4096214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.67/3.40 % (4096214)CaDiCaL version: 2.1.3
% 13.67/3.40 % (4096214)Termination reason: Instruction limit
% 13.67/3.40 % (4096214)Termination phase: Saturation
% 13.67/3.40 % (4096214)Time elapsed: 0.081 s
% 13.67/3.40 % (4096214)Peak memory usage: 116 MB
% 13.67/3.40 % (4096214)Instructions burned: 119 (million)
% 13.67/3.40 % (4096224)lrs+10_1_sil=8000:sp=occurrence:random_seed=3822941716:i=285:sd=3:ss=axioms:sgt=8_2988 on theBenchmark for (2988ds/285Mi)
% 13.67/3.40 % (4096225)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3036768199:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2988 on theBenchmark for (2988ds/157Mi)
% 13.67/3.40 % (4096226)lrs+1011_1_sil=32000:sp=occurrence:random_seed=537832737:i=325:sd=1:ss=axioms:sgt=32_2988 on theBenchmark for (2988ds/325Mi)
% 13.67/3.40 % (4096227)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=2321318382:s2a=on:i=248:s2at=1.23:gtg=position_2988 on theBenchmark for (2988ds/248Mi)
% 13.67/3.40 % (4096225)Instruction limit reached!
% 15.95/3.92 % (4096225)------------------------------
% 15.95/3.92 % (4096225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.95/3.92 % (4096225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.95/3.92 % (4096225)CaDiCaL version: 2.1.3
% 15.95/3.92 % (4096225)Termination reason: Instruction limit
% 15.95/3.92 % (4096225)Termination phase: Property scanning
% 15.95/3.92 % (4096225)Time elapsed: 0.072 s
% 15.95/3.92 % (4096225)Peak memory usage: 111 MB
% 15.95/3.92 % (4096225)Instructions burned: 157 (million)
% 15.95/3.92 % (4096224)Refutation not found, incomplete strategy
% 15.95/3.92 % (4096224)------------------------------
% 15.95/3.92 % (4096224)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.95/3.92 % (4096224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.95/3.92 % (4096224)CaDiCaL version: 2.1.3
% 15.95/3.92 % (4096224)Termination reason: Refutation not found, incomplete strategy
% 15.95/3.92 % (4096224)Time elapsed: 0.087 s
% 15.95/3.92 % (4096224)Peak memory usage: 119 MB
% 15.95/3.92 % (4096224)Instructions burned: 113 (million)
% 15.95/3.92 % (4096226)Refutation not found, incomplete strategy
% 15.95/3.92 % (4096226)------------------------------
% 15.95/3.92 % (4096226)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.95/3.92 % (4096226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.95/3.92 % (4096226)CaDiCaL version: 2.1.3
% 15.95/3.92 % (4096226)Termination reason: Refutation not found, incomplete strategy
% 15.95/3.92 % (4096226)Time elapsed: 0.087 s
% 15.95/3.92 % (4096226)Peak memory usage: 119 MB
% 15.95/3.92 % (4096226)Instructions burned: 113 (million)
% 15.95/3.92 % (4096227)Instruction limit reached!
% 15.95/3.92 % (4096227)------------------------------
% 15.95/3.92 % (4096227)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.95/3.92 % (4096227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.95/3.92 % (4096227)CaDiCaL version: 2.1.3
% 15.95/3.92 % (4096227)Termination reason: Instruction limit
% 15.95/3.92 % (4096227)Termination phase: SInE selection
% 15.95/3.92 % (4096227)Time elapsed: 0.143 s
% 15.95/3.92 % (4096227)Peak memory usage: 111 MB
% 15.95/3.92 % (4096227)Instructions burned: 248 (million)
% 15.95/3.92 % (4096232)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=263097639:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2986 on theBenchmark for (2986ds/294Mi)
% 15.95/3.92 % (4096224)------------------------------
% 15.95/3.92 % (4096224)------------------------------
% 15.95/3.92 % (4096226)------------------------------
% 15.95/3.92 % (4096226)------------------------------
% 15.95/3.92 % (4096233)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1853433296:i=2350_2985 on theBenchmark for (2985ds/2350Mi)
% 15.95/3.92 % (4096232)Refutation not found, incomplete strategy
% 15.95/3.92 % (4096232)------------------------------
% 15.95/3.92 % (4096232)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.95/3.92 % (4096232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.95/3.92 % (4096232)CaDiCaL version: 2.1.3
% 15.95/3.92 % (4096232)Termination reason: Refutation not found, incomplete strategy
% 15.95/3.92 % (4096232)Time elapsed: 0.141 s
% 15.95/3.92 % (4096232)Peak memory usage: 119 MB
% 15.95/3.92 % (4096232)Instructions burned: 221 (million)
% 15.95/3.92 % (4096235)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1717628189:cts=off:i=113:fsr=off:ss=included:sgt=4_2983 on theBenchmark for (2983ds/113Mi)
% 15.95/3.92 % (4096237)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=507157902:i=127:av=off:fsr=off:sup=off_2983 on theBenchmark for (2983ds/127Mi)
% 15.95/3.92 % (4096235)Instruction limit reached!
% 15.95/3.92 % (4096235)------------------------------
% 15.95/3.92 % (4096235)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.95/3.92 % (4096235)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.95/3.92 % (4096235)CaDiCaL version: 2.1.3
% 15.95/3.92 % (4096235)Termination reason: Instruction limit
% 15.95/3.92 % (4096235)Termination phase: Saturation
% 15.95/3.92 % (4096235)Time elapsed: 0.114 s
% 15.95/3.92 % (4096235)Peak memory usage: 116 MB
% 15.95/3.92 % (4096235)Instructions burned: 114 (million)
% 15.95/3.92 % (4096237)Instruction limit reached!
% 15.95/3.92 % (4096237)------------------------------
% 15.95/3.92 % (4096237)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.11/5.90 % (4096237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.11/5.90 % (4096237)CaDiCaL version: 2.1.3
% 31.11/5.90 % (4096237)Termination reason: Instruction limit
% 31.11/5.90 % (4096237)Termination phase: Preprocessing 2
% 31.11/5.90 % (4096237)Time elapsed: 0.106 s
% 31.11/5.90 % (4096237)Peak memory usage: 117 MB
% 31.11/5.90 % (4096237)Instructions burned: 128 (million)
% 31.11/5.90 % (4096232)------------------------------
% 31.11/5.90 % (4096232)------------------------------
% 31.11/5.90 % (4096240)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2659698087:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2980 on theBenchmark for (2980ds/114Mi)
% 31.11/5.90 % (4096241)lrs+10_1_sil=8000:sp=occurrence:random_seed=2979939847:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2980 on theBenchmark for (2980ds/907Mi)
% 31.11/5.90 % (4096242)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2259544867:i=437:sd=1:aac=none:ss=included_2980 on theBenchmark for (2980ds/437Mi)
% 31.11/5.90 % (4096240)Instruction limit reached!
% 31.11/5.90 % (4096240)------------------------------
% 31.11/5.90 % (4096240)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.11/5.90 % (4096240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.11/5.90 % (4096240)CaDiCaL version: 2.1.3
% 31.11/5.90 % (4096240)Termination reason: Instruction limit
% 31.11/5.90 % (4096240)Termination phase: Property scanning
% 31.11/5.90 % (4096240)Time elapsed: 0.058 s
% 31.11/5.90 % (4096240)Peak memory usage: 111 MB
% 31.11/5.90 % (4096240)Instructions burned: 115 (million)
% 31.11/5.90 % (4096242)Refutation not found, incomplete strategy
% 31.11/5.90 % (4096242)------------------------------
% 31.11/5.90 % (4096242)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.11/5.90 % (4096242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.11/5.90 % (4096242)CaDiCaL version: 2.1.3
% 31.11/5.90 % (4096242)Termination reason: Refutation not found, incomplete strategy
% 31.11/5.90 % (4096242)Time elapsed: 0.086 s
% 31.11/5.90 % (4096242)Peak memory usage: 118 MB
% 31.11/5.90 % (4096242)Instructions burned: 108 (million)
% 31.11/5.90 % (4096246)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1941302646:i=5202:ss=axioms:sgt=16_2978 on theBenchmark for (2978ds/5202Mi)
% 31.11/5.90 % (4096212)Refutation not found, incomplete strategy
% 31.11/5.90 % (4096212)------------------------------
% 31.11/5.90 % (4096212)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.11/5.90 % (4096212)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.11/5.90 % (4096212)CaDiCaL version: 2.1.3
% 31.11/5.90 % (4096212)Termination reason: Refutation not found, incomplete strategy
% 31.11/5.90 % (4096212)Time elapsed: 1.221 s
% 31.11/5.90 % (4096212)Peak memory usage: 233 MB
% 31.11/5.90 % (4096212)Instructions burned: 1627 (million)
% 31.11/5.90 % (4096241)Refutation not found, incomplete strategy
% 31.11/5.90 % (4096241)------------------------------
% 31.11/5.90 % (4096241)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.11/5.90 % (4096241)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.11/5.90 % (4096241)CaDiCaL version: 2.1.3
% 31.11/5.90 % (4096241)Termination reason: Refutation not found, incomplete strategy
% 31.11/5.90 % (4096241)Time elapsed: 0.305 s
% 31.11/5.90 % (4096241)Peak memory usage: 119 MB
% 31.11/5.90 % (4096241)Instructions burned: 598 (million)
% 31.11/5.90 % (4096242)------------------------------
% 31.11/5.90 % (4096242)------------------------------
% 31.11/5.90 % (4096248)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=461425772:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2975 on theBenchmark for (2975ds/134Mi)
% 31.11/5.90 % (4096241)------------------------------
% 31.11/5.90 % (4096241)------------------------------
% 31.11/5.90 % (4096248)Instruction limit reached!
% 31.11/5.90 % (4096248)------------------------------
% 31.11/5.90 % (4096248)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 31.11/5.90 % (4096248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.11/5.90 % (4096248)CaDiCaL version: 2.1.3
% 31.11/5.90 % (4096248)Termination reason: Instruction limit
% 31.11/5.90 % (4096248)Termination phase: Saturation
% 31.11/5.90 % (4096248)Time elapsed: 0.095 s
% 31.11/5.90 % (4096248)Peak memory usage: 117 MB
% 31.11/5.90 % (4096248)Instructions burned: 135 (million)
% 31.11/5.90 % (4096233)Instruction limit reached!
% 31.11/5.90 % (4096233)------------------------------
% 42.76/7.54 % (4096233)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.76/7.54 % (4096233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.76/7.54 % (4096233)CaDiCaL version: 2.1.3
% 42.76/7.54 % (4096233)Termination reason: Instruction limit
% 42.76/7.54 % (4096233)Termination phase: Saturation
% 42.76/7.54 % (4096233)Time elapsed: 1.052 s
% 42.76/7.54 % (4096233)Peak memory usage: 335 MB
% 42.76/7.54 % (4096233)Instructions burned: 2352 (million)
% 42.76/7.54 % (4096212)------------------------------
% 42.76/7.54 % (4096212)------------------------------
% 42.76/7.54 % (4096250)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3306067579:st=8:i=592:sd=3:ep=RST:ss=axioms_2973 on theBenchmark for (2973ds/592Mi)
% 42.76/7.54 % (4096252)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=3965521681:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2972 on theBenchmark for (2972ds/125Mi)
% 42.76/7.54 % (4096251)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=543551123:st=3:i=13193:sd=3:ss=axioms_2972 on theBenchmark for (2972ds/13193Mi)
% 42.76/7.54 % (4096252)Instruction limit reached!
% 42.76/7.54 % (4096252)------------------------------
% 42.76/7.54 % (4096252)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.76/7.54 % (4096252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.76/7.54 % (4096252)CaDiCaL version: 2.1.3
% 42.76/7.54 % (4096252)Termination reason: Instruction limit
% 42.76/7.54 % (4096252)Termination phase: Property scanning
% 42.76/7.54 % (4096252)Time elapsed: 0.035 s
% 42.76/7.54 % (4096252)Peak memory usage: 111 MB
% 42.76/7.54 % (4096252)Instructions burned: 127 (million)
% 42.76/7.54 % (4096253)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=4006291785:i=134:gtgl=5:slsql=off:gtg=exists_sym_2972 on theBenchmark for (2972ds/134Mi)
% 42.76/7.54 % (4096253)Instruction limit reached!
% 42.76/7.54 % (4096253)------------------------------
% 42.76/7.54 % (4096253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.76/7.54 % (4096253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.76/7.54 % (4096253)CaDiCaL version: 2.1.3
% 42.76/7.54 % (4096253)Termination reason: Instruction limit
% 42.76/7.54 % (4096253)Termination phase: Property scanning
% 42.76/7.54 % (4096253)Time elapsed: 0.064 s
% 42.76/7.54 % (4096253)Peak memory usage: 111 MB
% 42.76/7.54 % (4096253)Instructions burned: 135 (million)
% 42.76/7.54 % (4096250)Refutation not found, incomplete strategy
% 42.76/7.54 % (4096250)------------------------------
% 42.76/7.54 % (4096250)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.76/7.54 % (4096250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.76/7.54 % (4096250)CaDiCaL version: 2.1.3
% 42.76/7.54 % (4096250)Termination reason: Refutation not found, incomplete strategy
% 42.76/7.54 % (4096250)Time elapsed: 0.150 s
% 42.76/7.54 % (4096250)Peak memory usage: 119 MB
% 42.76/7.54 % (4096250)Instructions burned: 216 (million)
% 42.76/7.54 % (4096257)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1159781163:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2971 on theBenchmark for (2971ds/141Mi)
% 42.76/7.54 % (4096257)Refutation not found, incomplete strategy
% 42.76/7.54 % (4096257)------------------------------
% 42.76/7.54 % (4096257)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.76/7.54 % (4096257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.76/7.54 % (4096257)CaDiCaL version: 2.1.3
% 42.76/7.54 % (4096257)Termination reason: Refutation not found, incomplete strategy
% 42.76/7.54 % (4096257)Time elapsed: 0.055 s
% 42.76/7.54 % (4096257)Peak memory usage: 119 MB
% 42.76/7.54 % (4096257)Instructions burned: 140 (million)
% 42.76/7.54 % (4096259)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=2655949935:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2970 on theBenchmark for (2970ds/431Mi)
% 42.76/7.54 % (4096259)Refutation not found, incomplete strategy
% 42.76/7.54 % (4096259)------------------------------
% 42.76/7.54 % (4096259)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 42.76/7.54 % (4096259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 42.76/7.54 % (4096259)CaDiCaL version: 2.1.3
% 42.76/7.54 % (4096259)Termination reason: Refutation not found, incomplete strategy
% 48.51/8.39 % (4096259)Time elapsed: 0.089 s
% 48.51/8.39 % (4096259)Peak memory usage: 119 MB
% 48.51/8.39 % (4096259)Instructions burned: 113 (million)
% 48.51/8.39 % (4096257)------------------------------
% 48.51/8.39 % (4096257)------------------------------
% 48.51/8.39 % (4096250)------------------------------
% 48.51/8.39 % (4096250)------------------------------
% 48.51/8.39 % (4096262)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=933793137:i=6060:aac=none:ins=25_2967 on theBenchmark for (2967ds/6060Mi)
% 48.51/8.39 % (4096263)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=2035655858:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2967 on theBenchmark for (2967ds/150Mi)
% 48.51/8.39 % (4096259)------------------------------
% 48.51/8.39 % (4096259)------------------------------
% 48.51/8.39 % (4096263)Instruction limit reached!
% 48.51/8.39 % (4096263)------------------------------
% 48.51/8.39 % (4096263)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.51/8.39 % (4096263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.51/8.39 % (4096263)CaDiCaL version: 2.1.3
% 48.51/8.39 % (4096263)Termination reason: Instruction limit
% 48.51/8.39 % (4096263)Termination phase: Preprocessing 1
% 48.51/8.39 % (4096263)Time elapsed: 0.104 s
% 48.51/8.39 % (4096263)Peak memory usage: 112 MB
% 48.51/8.39 % (4096263)Instructions burned: 151 (million)
% 48.51/8.39 % (4096266)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1250177868:i=14155:bd=all_2964 on theBenchmark for (2964ds/14155Mi)
% 48.51/8.39 % (4096267)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=3799463759:i=667:av=off:fsr=off_2964 on theBenchmark for (2964ds/667Mi)
% 48.51/8.39 % (4096267)Instruction limit reached!
% 48.51/8.39 % (4096267)------------------------------
% 48.51/8.39 % (4096267)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.51/8.39 % (4096267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.51/8.39 % (4096267)CaDiCaL version: 2.1.3
% 48.51/8.39 % (4096267)Termination reason: Instruction limit
% 48.51/8.39 % (4096267)Termination phase: Saturation
% 48.51/8.39 % (4096267)Time elapsed: 0.375 s
% 48.51/8.39 % (4096267)Peak memory usage: 130 MB
% 48.51/8.39 % (4096267)Instructions burned: 667 (million)
% 48.51/8.39 % (4096270)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=1275038106:s2a=on:i=185:s2at=1.8:fdi=4_2959 on theBenchmark for (2959ds/185Mi)
% 48.51/8.39 % (4096270)Instruction limit reached!
% 48.51/8.39 % (4096270)------------------------------
% 48.51/8.39 % (4096270)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.51/8.39 % (4096270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.51/8.39 % (4096270)CaDiCaL version: 2.1.3
% 48.51/8.39 % (4096270)Termination reason: Instruction limit
% 48.51/8.39 % (4096270)Termination phase: Preprocessing 1
% 48.51/8.39 % (4096270)Time elapsed: 0.120 s
% 48.51/8.39 % (4096270)Peak memory usage: 112 MB
% 48.51/8.39 % (4096270)Instructions burned: 186 (million)
% 48.51/8.39 % (4096272)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2550524979:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2956 on theBenchmark for (2956ds/193Mi)
% 48.51/8.39 % (4096272)Instruction limit reached!
% 48.51/8.39 % (4096272)------------------------------
% 48.51/8.39 % (4096272)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.51/8.39 % (4096272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.51/8.39 % (4096272)CaDiCaL version: 2.1.3
% 48.51/8.39 % (4096272)Termination reason: Instruction limit
% 48.51/8.39 % (4096272)Termination phase: SInE selection
% 48.51/8.39 % (4096272)Time elapsed: 0.124 s
% 48.51/8.39 % (4096272)Peak memory usage: 112 MB
% 48.51/8.39 % (4096272)Instructions burned: 194 (million)
% 48.51/8.39 % (4096274)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=3980295816:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2953 on theBenchmark for (2953ds/4850Mi)
% 48.51/8.39 % (4096251)Refutation not found, incomplete strategy
% 48.51/8.39 % (4096251)------------------------------
% 48.51/8.39 % (4096251)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.51/8.39 % (4096251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.51/8.39 % (4096251)CaDiCaL version: 2.1.3
% 48.51/8.39 % (4096251)Termination reason: Refutation not found, incomplete strategy
% 48.51/8.39 % (4096251)Time elapsed: 2.357 s
% 48.51/8.39 % (4096251)Peak memory usage: 218 MB
% 48.51/8.39 % (4096251)Instructions burned: 3287 (million)
% 48.51/8.39 % (4096251)------------------------------
% 48.51/8.39 % (4096251)------------------------------
% 48.51/8.39 % (4096276)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3403275078:i=12111:sd=1:ss=included_2945 on theBenchmark for (2945ds/12111Mi)
% 48.51/8.39 % (4096262)Instruction limit reached!
% 48.51/8.39 % (4096262)------------------------------
% 48.51/8.39 % (4096262)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.51/8.39 % (4096262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.51/8.39 % (4096262)CaDiCaL version: 2.1.3
% 48.51/8.39 % (4096262)Termination reason: Instruction limit
% 48.51/8.39 % (4096262)Termination phase: Saturation
% 48.51/8.39 % (4096262)Time elapsed: 2.450 s
% 48.51/8.39 % (4096262)Peak memory usage: 388 MB
% 48.51/8.39 % (4096262)Instructions burned: 6060 (million)
% 48.51/8.39 % (4096278)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=835287894:i=319:kws=precedence:fsr=off_2941 on theBenchmark for (2941ds/319Mi)
% 48.51/8.39 % (4096278)Instruction limit reached!
% 48.51/8.39 % (4096278)------------------------------
% 48.51/8.39 % (4096278)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.51/8.39 % (4096278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.51/8.39 % (4096278)CaDiCaL version: 2.1.3
% 48.51/8.39 % (4096278)Termination reason: Instruction limit
% 48.51/8.39 % (4096278)Termination phase: Property scanning
% 48.51/8.39 % (4096278)Time elapsed: 0.116 s
% 48.51/8.39 % (4096278)Peak memory usage: 122 MB
% 48.51/8.39 % (4096278)Instructions burned: 321 (million)
% 48.51/8.39 % (4096280)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=4177689109:i=2064:ep=RST_2939 on theBenchmark for (2939ds/2064Mi)
% 48.51/8.39 % (4096274)Instruction limit reached!
% 48.51/8.39 % (4096274)------------------------------
% 48.51/8.39 % (4096274)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.51/8.39 % (4096274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.51/8.39 % (4096274)CaDiCaL version: 2.1.3
% 48.51/8.39 % (4096274)Termination reason: Instruction limit
% 48.51/8.39 % (4096274)Termination phase: Saturation
% 48.51/8.39 % (4096274)Time elapsed: 1.767 s
% 48.51/8.39 % (4096274)Peak memory usage: 118 MB
% 48.51/8.39 % (4096274)Instructions burned: 4850 (million)
% 48.51/8.39 % (4096280)Refutation not found, incomplete strategy
% 48.51/8.39 % (4096280)------------------------------
% 48.51/8.39 % (4096280)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.51/8.39 % (4096280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.51/8.39 % (4096280)CaDiCaL version: 2.1.3
% 48.51/8.39 % (4096280)Termination reason: Refutation not found, incomplete strategy
% 48.51/8.39 % (4096280)Time elapsed: 0.507 s
% 48.51/8.39 % (4096280)Peak memory usage: 142 MB
% 48.51/8.39 % (4096280)Instructions burned: 1240 (million)
% 48.51/8.39 % (4096282)dis-1011_128_sil=32000:random_seed=3114101007:i=3706:ep=RST:av=off_2934 on theBenchmark for (2934ds/3706Mi)
% 48.51/8.39 % (4096276)Refutation not found, incomplete strategy
% 48.51/8.39 % (4096276)------------------------------
% 48.51/8.39 % (4096276)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.51/8.39 % (4096276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.51/8.39 % (4096276)CaDiCaL version: 2.1.3
% 48.51/8.39 % (4096276)Termination reason: Refutation not found, incomplete strategy
% 48.51/8.39 % (4096276)Time elapsed: 1.122 s
% 48.51/8.39 % (4096276)Peak memory usage: 191 MB
% 48.51/8.39 % (4096276)Instructions burned: 1687 (million)
% 48.51/8.39 % (4096246)Instruction limit reached!
% 48.51/8.39 % (4096246)------------------------------
% 48.51/8.39 % (4096246)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.51/8.39 % (4096246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.51/8.39 % (4096246)CaDiCaL version: 2.1.3
% 48.51/8.39 % (4096246)Termination reason: Instruction limit
% 48.51/8.39 % (4096246)Termination phase: Saturation
% 48.51/8.39 % (4096246)Time elapsed: 4.554 s
% 48.51/8.39 % (4096246)Peak memory usage: 215 MB
% 48.51/8.39 % (4096246)Instructions burned: 5203 (million)
% 48.51/8.39 % (4096280)------------------------------
% 48.51/8.39 % (4096280)------------------------------
% 48.51/8.39 % (4096276)------------------------------
% 48.51/8.39 % (4096276)------------------------------
% 48.51/8.39 % (4096284)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=948098584:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2931 on theBenchmark for (2931ds/757Mi)
% 48.51/8.39 % (4096285)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=4106472793:i=13913:ss=axioms:sgt=8_2930 on theBenchmark for (2930ds/13913Mi)
% 48.51/8.39 % (4096284)Refutation not found, incomplete strategy
% 48.51/8.39 % (4096284)------------------------------
% 48.51/8.39 % (4096284)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 48.51/8.39 % (4096284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 48.51/8.39 % (4096284)CaDiCaL version: 2.1.3
% 48.51/8.39 % (4096284)Termination reason: Refutation not found, incomplete strategy
% 48.51/8.39 % (4096284)Time elapsed: 0.086 s
% 48.51/8.39 % (4096284)Peak memory usage: 119 MB
% 48.51/8.39 % (4096284)Instructions burned: 109 (million)
% 48.51/8.39 % (4096287)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=908971217:i=9925:aac=none_2929 on theBenchmark for (2929ds/9925Mi)
% 48.51/8.39 % (4096282)First to succeed.
% 48.51/8.39 % (4096282)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-4096205"
% 48.51/8.39 % (4096284)------------------------------
% 48.51/8.39 % (4096284)------------------------------
% 48.51/8.39 % (4096290)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=3960143373:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2925 on theBenchmark for (2925ds/2479Mi)
% 48.51/8.39 % (4096282)Refutation found. Thanks to Tanya!
% 48.51/8.39 % SZS status Theorem for theBenchmark
% 48.51/8.39 % SZS output start Proof for theBenchmark
% See solution above
% 0.21/8.60 % (4096282)------------------------------
% 0.21/8.60 % (4096282)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.21/8.60 % (4096282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.21/8.60 % (4096282)CaDiCaL version: 2.1.3
% 0.21/8.60 % (4096282)Termination reason: Refutation
% 0.21/8.60 % (4096282)Time elapsed: 0.640 s
% 0.21/8.60 % (4096282)Peak memory usage: 136 MB
% 0.21/8.60 % (4096282)Instructions burned: 1274 (million)
% 0.21/8.60 % (4096282)------------------------------
% 0.21/8.60 % (4096282)------------------------------
% 0.21/8.60 % (4096205)Success in time 7.709 s
% 0.21/8.60 % Vampire exiting
%------------------------------------------------------------------------------