%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR049+3 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:44:39 AM UTC 2026
% Result : Theorem 57.59s 18.84s
% Output : Refutation 57.59s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 34
% Syntax : Number of formulae : 104 ( 93 unt; 0 def)
% Number of atoms : 123 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 63 ( 44 ~; 12 |; 3 &)
% ( 0 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 33 ( 33 usr; 33 con; 0-0 aty)
% Number of variables : 24 ( 24 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f79,axiom,
genls(c_tptpcol_10_26886,c_tptpcol_9_26885),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_79) ).
fof(f83,axiom,
genls(c_tptpcol_8_26629,c_tptpcol_7_26628),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_83) ).
fof(f244,axiom,
genls(c_tptpcol_15_26925,c_tptpcol_14_26921),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_244) ).
fof(f416,axiom,
genls(c_tptpcol_11_92230,c_tptpcol_10_92166),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_416) ).
fof(f460,axiom,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_460) ).
fof(f504,axiom,
genls(c_tptpcol_12_26919,c_tptpcol_11_26887),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_504) ).
fof(f569,axiom,
genls(c_tptpcol_7_92163,c_tptpcol_6_92162),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_569) ).
fof(f593,axiom,
genls(c_tptpcol_3_81921,c_tptpcol_2_65537),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_593) ).
fof(f696,axiom,
genls(c_tptpcol_13_26920,c_tptpcol_12_26919),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_696) ).
fof(f742,axiom,
genls(c_tptpcol_14_92264,c_tptpcol_13_92263),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_742) ).
fof(f867,axiom,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_867) ).
fof(f1009,axiom,
genls(c_tptpcol_5_24579,c_tptpcol_4_24578),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_1009) ).
fof(f1073,axiom,
genls(c_tptpcol_11_26887,c_tptpcol_10_26886),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_1073) ).
fof(f1145,axiom,
genls(c_tptpcol_10_92166,c_tptpcol_9_92165),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_1145) ).
fof(f1180,axiom,
genls(c_tptpcol_16_92269,c_tptpcol_15_92268),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_1180) ).
fof(f1200,axiom,
genls(c_tptpcol_16_26926,c_tptpcol_15_26925),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_1200) ).
fof(f1248,axiom,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_1248) ).
fof(f1553,axiom,
genls(c_tptpcol_7_26628,c_tptpcol_6_26627),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_1553) ).
fof(f1694,axiom,
genls(c_tptpcol_6_92162,c_tptpcol_5_90114),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_1694) ).
fof(f1715,axiom,
genls(c_tptpcol_15_92268,c_tptpcol_14_92264),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_1715) ).
fof(f1917,axiom,
genls(c_tptpcol_14_26921,c_tptpcol_13_26920),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_1917) ).
fof(f1942,axiom,
genls(c_tptpcol_5_90114,c_tptpcol_4_90113),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_1942) ).
fof(f2008,axiom,
genls(c_tptpcol_13_92263,c_tptpcol_12_92262),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_2008) ).
fof(f2022,axiom,
genls(c_tptpcol_8_92164,c_tptpcol_7_92163),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_2022) ).
fof(f2202,axiom,
genls(c_tptpcol_9_92165,c_tptpcol_8_92164),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_2202) ).
fof(f3013,axiom,
genls(c_tptpcol_6_26627,c_tptpcol_5_24579),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_3013) ).
fof(f3214,axiom,
genls(c_tptpcol_4_24578,c_tptpcol_3_16386),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_3214) ).
fof(f3253,axiom,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_3253) ).
fof(f3436,axiom,
genls(c_tptpcol_12_92262,c_tptpcol_11_92230),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_3436) ).
fof(f3513,axiom,
genls(c_tptpcol_9_26885,c_tptpcol_8_26629),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_3513) ).
fof(f3629,axiom,
genls(c_tptpcol_4_90113,c_tptpcol_3_81921),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_3629) ).
fof(f7585,axiom,
! [X0,X1,X2] :
( ( disjointwith(X0,X1)
& genls(X2,X1) )
=> disjointwith(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_7585) ).
fof(f7586,axiom,
! [X0,X1,X2] :
( ( disjointwith(X0,X1)
& genls(X2,X0) )
=> disjointwith(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+2.ax',ax2_7586) ).
fof(f8006,conjecture,
( mtvisible(c_unitedstatesgeographypeoplemt)
=> disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',query149) ).
fof(f8007,negated_conjecture,
~ ( mtvisible(c_unitedstatesgeographypeoplemt)
=> disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269) ),
inference(negated_conjecture,[status(cth)],[f8006]) ).
fof(f13088,plain,
! [X0,X1,X2] :
( disjointwith(X0,X2)
| ~ disjointwith(X0,X1)
| ~ genls(X2,X1) ),
inference(ennf_transformation,[],[f7585]) ).
fof(f13089,plain,
! [X0,X1,X2] :
( disjointwith(X0,X2)
| ~ disjointwith(X0,X1)
| ~ genls(X2,X1) ),
inference(flattening,[],[f13088]) ).
fof(f13090,plain,
! [X0,X1,X2] :
( disjointwith(X2,X1)
| ~ disjointwith(X0,X1)
| ~ genls(X2,X0) ),
inference(ennf_transformation,[],[f7586]) ).
fof(f13091,plain,
! [X0,X1,X2] :
( disjointwith(X2,X1)
| ~ disjointwith(X0,X1)
| ~ genls(X2,X0) ),
inference(flattening,[],[f13090]) ).
fof(f13400,plain,
( ~ disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269)
& mtvisible(c_unitedstatesgeographypeoplemt) ),
inference(ennf_transformation,[],[f8007]) ).
fof(f13477,plain,
genls(c_tptpcol_10_26886,c_tptpcol_9_26885),
inference(cnf_transformation,[],[f79]) ).
fof(f13481,plain,
genls(c_tptpcol_8_26629,c_tptpcol_7_26628),
inference(cnf_transformation,[],[f83]) ).
fof(f13639,plain,
genls(c_tptpcol_15_26925,c_tptpcol_14_26921),
inference(cnf_transformation,[],[f244]) ).
fof(f13808,plain,
genls(c_tptpcol_11_92230,c_tptpcol_10_92166),
inference(cnf_transformation,[],[f416]) ).
fof(f13852,plain,
genls(c_tptpcol_3_16386,c_tptpcol_2_2),
inference(cnf_transformation,[],[f460]) ).
fof(f13895,plain,
genls(c_tptpcol_12_26919,c_tptpcol_11_26887),
inference(cnf_transformation,[],[f504]) ).
fof(f13959,plain,
genls(c_tptpcol_7_92163,c_tptpcol_6_92162),
inference(cnf_transformation,[],[f569]) ).
fof(f13982,plain,
genls(c_tptpcol_3_81921,c_tptpcol_2_65537),
inference(cnf_transformation,[],[f593]) ).
fof(f14085,plain,
genls(c_tptpcol_13_26920,c_tptpcol_12_26919),
inference(cnf_transformation,[],[f696]) ).
fof(f14130,plain,
genls(c_tptpcol_14_92264,c_tptpcol_13_92263),
inference(cnf_transformation,[],[f742]) ).
fof(f14251,plain,
genls(c_tptpcol_2_65537,c_tptpcol_1_65536),
inference(cnf_transformation,[],[f867]) ).
fof(f14391,plain,
genls(c_tptpcol_5_24579,c_tptpcol_4_24578),
inference(cnf_transformation,[],[f1009]) ).
fof(f14452,plain,
genls(c_tptpcol_11_26887,c_tptpcol_10_26886),
inference(cnf_transformation,[],[f1073]) ).
fof(f14523,plain,
genls(c_tptpcol_10_92166,c_tptpcol_9_92165),
inference(cnf_transformation,[],[f1145]) ).
fof(f14557,plain,
genls(c_tptpcol_16_92269,c_tptpcol_15_92268),
inference(cnf_transformation,[],[f1180]) ).
fof(f14577,plain,
genls(c_tptpcol_16_26926,c_tptpcol_15_26925),
inference(cnf_transformation,[],[f1200]) ).
fof(f14623,plain,
disjointwith(c_tptpcol_1_1,c_tptpcol_1_65536),
inference(cnf_transformation,[],[f1248]) ).
fof(f14921,plain,
genls(c_tptpcol_7_26628,c_tptpcol_6_26627),
inference(cnf_transformation,[],[f1553]) ).
fof(f15060,plain,
genls(c_tptpcol_6_92162,c_tptpcol_5_90114),
inference(cnf_transformation,[],[f1694]) ).
fof(f15081,plain,
genls(c_tptpcol_15_92268,c_tptpcol_14_92264),
inference(cnf_transformation,[],[f1715]) ).
fof(f15279,plain,
genls(c_tptpcol_14_26921,c_tptpcol_13_26920),
inference(cnf_transformation,[],[f1917]) ).
fof(f15304,plain,
genls(c_tptpcol_5_90114,c_tptpcol_4_90113),
inference(cnf_transformation,[],[f1942]) ).
fof(f15370,plain,
genls(c_tptpcol_13_92263,c_tptpcol_12_92262),
inference(cnf_transformation,[],[f2008]) ).
fof(f15384,plain,
genls(c_tptpcol_8_92164,c_tptpcol_7_92163),
inference(cnf_transformation,[],[f2022]) ).
fof(f15561,plain,
genls(c_tptpcol_9_92165,c_tptpcol_8_92164),
inference(cnf_transformation,[],[f2202]) ).
fof(f16362,plain,
genls(c_tptpcol_6_26627,c_tptpcol_5_24579),
inference(cnf_transformation,[],[f3013]) ).
fof(f16560,plain,
genls(c_tptpcol_4_24578,c_tptpcol_3_16386),
inference(cnf_transformation,[],[f3214]) ).
fof(f16598,plain,
genls(c_tptpcol_2_2,c_tptpcol_1_1),
inference(cnf_transformation,[],[f3253]) ).
fof(f16778,plain,
genls(c_tptpcol_12_92262,c_tptpcol_11_92230),
inference(cnf_transformation,[],[f3436]) ).
fof(f16854,plain,
genls(c_tptpcol_9_26885,c_tptpcol_8_26629),
inference(cnf_transformation,[],[f3513]) ).
fof(f16969,plain,
genls(c_tptpcol_4_90113,c_tptpcol_3_81921),
inference(cnf_transformation,[],[f3629]) ).
fof(f20382,plain,
! [X2,X0,X1] :
( ~ disjointwith(X0,X1)
| disjointwith(X0,X2)
| ~ genls(X2,X1) ),
inference(cnf_transformation,[],[f13089]) ).
fof(f20383,plain,
! [X2,X0,X1] :
( ~ disjointwith(X0,X1)
| disjointwith(X2,X1)
| ~ genls(X2,X0) ),
inference(cnf_transformation,[],[f13091]) ).
fof(f20688,plain,
~ disjointwith(c_tptpcol_16_26926,c_tptpcol_16_92269),
inference(cnf_transformation,[],[f13400]) ).
fof(f679330,plain,
~ disjointwith(c_tptpcol_16_26926,c_tptpcol_15_92268),
inference(unit_resulting_resolution,[],[f20382,f14557,f20688]) ).
fof(f679539,plain,
~ disjointwith(c_tptpcol_16_26926,c_tptpcol_14_92264),
inference(unit_resulting_resolution,[],[f20382,f15081,f679330]) ).
fof(f679543,plain,
~ disjointwith(c_tptpcol_16_26926,c_tptpcol_13_92263),
inference(unit_resulting_resolution,[],[f20382,f14130,f679539]) ).
fof(f679551,plain,
~ disjointwith(c_tptpcol_16_26926,c_tptpcol_12_92262),
inference(unit_resulting_resolution,[],[f20382,f15370,f679543]) ).
fof(f679563,plain,
~ disjointwith(c_tptpcol_16_26926,c_tptpcol_11_92230),
inference(unit_resulting_resolution,[],[f20382,f16778,f679551]) ).
fof(f679579,plain,
~ disjointwith(c_tptpcol_16_26926,c_tptpcol_10_92166),
inference(unit_resulting_resolution,[],[f20382,f13808,f679563]) ).
fof(f679599,plain,
~ disjointwith(c_tptpcol_16_26926,c_tptpcol_9_92165),
inference(unit_resulting_resolution,[],[f20382,f14523,f679579]) ).
fof(f679623,plain,
~ disjointwith(c_tptpcol_16_26926,c_tptpcol_8_92164),
inference(unit_resulting_resolution,[],[f20382,f15561,f679599]) ).
fof(f679847,plain,
~ disjointwith(c_tptpcol_15_26925,c_tptpcol_8_92164),
inference(unit_resulting_resolution,[],[f20383,f14577,f679623]) ).
fof(f679901,plain,
~ disjointwith(c_tptpcol_14_26921,c_tptpcol_8_92164),
inference(unit_resulting_resolution,[],[f20383,f13639,f679847]) ).
fof(f679974,plain,
~ disjointwith(c_tptpcol_13_26920,c_tptpcol_8_92164),
inference(unit_resulting_resolution,[],[f20383,f15279,f679901]) ).
fof(f680052,plain,
~ disjointwith(c_tptpcol_12_26919,c_tptpcol_8_92164),
inference(unit_resulting_resolution,[],[f20383,f14085,f679974]) ).
fof(f680124,plain,
~ disjointwith(c_tptpcol_11_26887,c_tptpcol_8_92164),
inference(unit_resulting_resolution,[],[f20383,f13895,f680052]) ).
fof(f680202,plain,
~ disjointwith(c_tptpcol_10_26886,c_tptpcol_8_92164),
inference(unit_resulting_resolution,[],[f20383,f14452,f680124]) ).
fof(f680308,plain,
~ disjointwith(c_tptpcol_9_26885,c_tptpcol_8_92164),
inference(unit_resulting_resolution,[],[f20383,f13477,f680202]) ).
fof(f680398,plain,
~ disjointwith(c_tptpcol_8_26629,c_tptpcol_8_92164),
inference(unit_resulting_resolution,[],[f20383,f16854,f680308]) ).
fof(f680495,plain,
~ disjointwith(c_tptpcol_7_26628,c_tptpcol_8_92164),
inference(unit_resulting_resolution,[],[f20383,f13481,f680398]) ).
fof(f680600,plain,
~ disjointwith(c_tptpcol_6_26627,c_tptpcol_8_92164),
inference(unit_resulting_resolution,[],[f20383,f14921,f680495]) ).
fof(f680715,plain,
~ disjointwith(c_tptpcol_5_24579,c_tptpcol_8_92164),
inference(unit_resulting_resolution,[],[f20383,f16362,f680600]) ).
fof(f680844,plain,
~ disjointwith(c_tptpcol_4_24578,c_tptpcol_8_92164),
inference(unit_resulting_resolution,[],[f20383,f14391,f680715]) ).
fof(f680982,plain,
~ disjointwith(c_tptpcol_3_16386,c_tptpcol_8_92164),
inference(unit_resulting_resolution,[],[f20383,f16560,f680844]) ).
fof(f681121,plain,
~ disjointwith(c_tptpcol_2_2,c_tptpcol_8_92164),
inference(unit_resulting_resolution,[],[f20383,f13852,f680982]) ).
fof(f681297,plain,
~ disjointwith(c_tptpcol_1_1,c_tptpcol_8_92164),
inference(unit_resulting_resolution,[],[f20383,f16598,f681121]) ).
fof(f681514,plain,
~ disjointwith(c_tptpcol_1_1,c_tptpcol_7_92163),
inference(unit_resulting_resolution,[],[f20382,f15384,f681297]) ).
fof(f681663,plain,
~ disjointwith(c_tptpcol_1_1,c_tptpcol_6_92162),
inference(unit_resulting_resolution,[],[f20382,f13959,f681514]) ).
fof(f801467,plain,
~ disjointwith(c_tptpcol_1_1,c_tptpcol_5_90114),
inference(unit_resulting_resolution,[],[f20382,f15060,f681663]) ).
fof(f802049,plain,
~ disjointwith(c_tptpcol_1_1,c_tptpcol_4_90113),
inference(unit_resulting_resolution,[],[f20382,f15304,f801467]) ).
fof(f802658,plain,
~ disjointwith(c_tptpcol_1_1,c_tptpcol_3_81921),
inference(unit_resulting_resolution,[],[f20382,f16969,f802049]) ).
fof(f803196,plain,
~ disjointwith(c_tptpcol_1_1,c_tptpcol_2_65537),
inference(unit_resulting_resolution,[],[f20382,f13982,f802658]) ).
fof(f803798,plain,
$false,
inference(unit_resulting_resolution,[],[f20382,f14251,f14623,f803196]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR049+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.20 % Computer : n026.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Mon Sep 28 22:20:12 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.23 Running first-order model finding
% 0.09/0.23 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 17.79/2.98 % (152592)Will run a generic schedule for satisfiability detection.
% 17.79/2.98 % (152608)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=13634034:i=116_2998 on theBenchmark for (2998ds/116Mi)
% 17.79/2.98 % (152605)% WARNING: option uhcvi not known.
% 17.79/2.98 % (152605)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=683469195:i=135531:add=off:rawr=on_2998 on theBenchmark for (2998ds/135531Mi)
% 17.79/2.98 % (152607)dis+10_1_sil=32000:sp=arity:random_seed=869373113:i=103:fgj=on_2998 on theBenchmark for (2998ds/103Mi)
% 17.79/2.98 % (152606)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2303231814:i=88024:add=on:rawr=on_2998 on theBenchmark for (2998ds/88024Mi)
% 17.79/2.98 % (152610)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=638941243:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2998 on theBenchmark for (2998ds/159Mi)
% 17.79/2.98 % (152609)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4106482715:i=131_2998 on theBenchmark for (2998ds/131Mi)
% 17.79/2.98 % (152604)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=919096992_2998 on theBenchmark for (2998ds/0Mi)
% 17.79/2.98 % (152608)Instruction limit reached!
% 17.79/2.98 % (152608)------------------------------
% 17.79/2.98 % (152608)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.79/2.98 % (152608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.79/2.98 % (152608)CaDiCaL version: 2.1.3
% 17.79/2.98 % (152608)Termination reason: Instruction limit
% 17.79/2.98 % (152608)Termination phase: Blocked clause elimination
% 17.79/2.98 % (152608)Time elapsed: 0.076 s
% 17.79/2.98 % (152608)Peak memory usage: 24 MB
% 17.79/2.98 % (152608)Instructions burned: 117 (million)
% 17.79/2.98 % (152620)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1946597040:i=714:nm=2_2997 on theBenchmark for (2997ds/714Mi)
% 17.79/2.98 % (152607)Instruction limit reached!
% 17.79/2.98 % (152607)------------------------------
% 17.79/2.98 % (152607)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.79/2.98 % (152607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.79/2.98 % (152607)CaDiCaL version: 2.1.3
% 17.79/2.98 % (152607)Termination reason: Instruction limit
% 17.79/2.98 % (152607)Termination phase: Saturation
% 17.79/2.98 % (152607)Time elapsed: 0.100 s
% 17.79/2.98 % (152607)Peak memory usage: 22 MB
% 17.79/2.98 % (152607)Instructions burned: 103 (million)
% 17.79/2.98 % (152610)Instruction limit reached!
% 17.79/2.98 % (152610)------------------------------
% 17.79/2.98 % (152610)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.79/2.98 % (152610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.79/2.98 % (152610)CaDiCaL version: 2.1.3
% 17.79/2.98 % (152610)Termination reason: Instruction limit
% 17.79/2.98 % (152610)Termination phase: Saturation
% 17.79/2.98 % (152610)Time elapsed: 0.106 s
% 17.79/2.98 % (152610)Peak memory usage: 25 MB
% 17.79/2.98 % (152610)Instructions burned: 160 (million)
% 17.79/2.98 % (152609)Instruction limit reached!
% 17.79/2.98 % (152609)------------------------------
% 17.79/2.98 % (152609)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.79/2.98 % (152609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.79/2.98 % (152609)CaDiCaL version: 2.1.3
% 17.79/2.98 % (152609)Termination reason: Instruction limit
% 17.79/2.98 % (152609)Termination phase: Saturation
% 17.79/2.98 % (152609)Time elapsed: 0.131 s
% 17.79/2.98 % (152609)Peak memory usage: 23 MB
% 17.79/2.98 % (152609)Instructions burned: 131 (million)
% 17.79/2.98 % (152622)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1397797719:i=131:bd=preordered:fsd=on_2997 on theBenchmark for (2997ds/131Mi)
% 17.79/2.98 % (152623)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=3756357612:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi)
% 17.79/2.98 % (152625)ott-21_1_sil=16000:fs=off:random_seed=3536691231:i=180:av=off:fsr=off_2996 on theBenchmark for (2996ds/180Mi)
% 17.79/2.98 % (152622)Instruction limit reached!
% 17.79/2.98 % (152622)------------------------------
% 17.79/2.98 % (152622)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.79/2.98 % (152622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.79/2.98 % (152622)CaDiCaL version: 2.1.3
% 17.79/2.98 % (152622)Termination reason: Instruction limit
% 40.91/6.13 % (152622)Termination phase: Blocked clause elimination
% 40.91/6.13 % (152622)Time elapsed: 0.138 s
% 40.91/6.13 % (152622)Peak memory usage: 23 MB
% 40.91/6.13 % (152622)Instructions burned: 132 (million)
% 40.91/6.13 % TRYING [1]
% 40.91/6.13 % (152631)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=969327536:i=477:bd=all_2995 on theBenchmark for (2995ds/477Mi)
% 40.91/6.13 % TRYING [2]
% 40.91/6.13 % (152625)Instruction limit reached!
% 40.91/6.13 % (152625)------------------------------
% 40.91/6.13 % (152625)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.91/6.13 % (152625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.91/6.13 % (152625)CaDiCaL version: 2.1.3
% 40.91/6.13 % (152625)Termination reason: Instruction limit
% 40.91/6.13 % (152625)Termination phase: Saturation
% 40.91/6.13 % (152625)Time elapsed: 0.149 s
% 40.91/6.13 % (152625)Peak memory usage: 24 MB
% 40.91/6.13 % (152625)Instructions burned: 180 (million)
% 40.91/6.13 % (152633)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2927251738:fmbsr=1.3:i=865:ins=25_2994 on theBenchmark for (2994ds/865Mi)
% 40.91/6.13 % TRYING [1]
% 40.91/6.13 % TRYING [3]
% 40.91/6.13 % TRYING [2]
% 40.91/6.13 % (152620)Instruction limit reached!
% 40.91/6.13 % (152620)------------------------------
% 40.91/6.13 % (152620)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.91/6.13 % (152620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.91/6.13 % (152620)CaDiCaL version: 2.1.3
% 40.91/6.13 % (152620)Termination reason: Instruction limit
% 40.91/6.13 % (152620)Termination phase: Finite model building constraint generation
% 40.91/6.13 % (152620)Time elapsed: 0.286 s
% 40.91/6.13 % (152620)Peak memory usage: 41 MB
% 40.91/6.13 % (152620)Instructions burned: 730 (million)
% 40.91/6.13 % (152635)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=268621952:i=1179_2994 on theBenchmark for (2994ds/1179Mi)
% 40.91/6.13 % TRYING [3]
% 40.91/6.13 % (152631)Instruction limit reached!
% 40.91/6.13 % (152631)------------------------------
% 40.91/6.13 % (152631)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.91/6.13 % (152631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.91/6.13 % (152631)CaDiCaL version: 2.1.3
% 40.91/6.13 % (152631)Termination reason: Instruction limit
% 40.91/6.13 % (152631)Termination phase: Saturation
% 40.91/6.13 % (152631)Time elapsed: 0.246 s
% 40.91/6.13 % (152631)Peak memory usage: 28 MB
% 40.91/6.13 % (152631)Instructions burned: 477 (million)
% 40.91/6.13 % TRYING [4]
% 40.91/6.13 % TRYING [1]
% 40.91/6.13 % (152637)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3374661423:i=889:ins=1_2992 on theBenchmark for (2992ds/889Mi)
% 40.91/6.13 % TRYING [2]
% 40.91/6.13 % (152623)Instruction limit reached!
% 40.91/6.13 % (152623)------------------------------
% 40.91/6.13 % (152623)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.91/6.13 % (152623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.91/6.13 % (152623)CaDiCaL version: 2.1.3
% 40.91/6.13 % (152623)Termination reason: Instruction limit
% 40.91/6.13 % (152623)Termination phase: Saturation
% 40.91/6.13 % (152623)Time elapsed: 0.565 s
% 40.91/6.13 % (152623)Peak memory usage: 29 MB
% 40.91/6.13 % (152623)Instructions burned: 684 (million)
% 40.91/6.13 % (152635)Instruction limit reached!
% 40.91/6.13 % (152635)------------------------------
% 40.91/6.13 % (152635)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.91/6.13 % (152635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.91/6.13 % (152635)CaDiCaL version: 2.1.3
% 40.91/6.13 % (152635)Termination reason: Instruction limit
% 40.91/6.13 % (152635)Termination phase: Saturation
% 40.91/6.13 % (152635)Time elapsed: 0.342 s
% 40.91/6.13 % (152635)Peak memory usage: 46 MB
% 40.91/6.13 % (152635)Instructions burned: 1179 (million)
% 40.91/6.13 % (152640)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=3759854460:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2991 on theBenchmark for (2991ds/692Mi)
% 40.91/6.13 % (152642)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3653535030:i=879:kws=inv_precedence:fsr=off_2990 on theBenchmark for (2990ds/879Mi)
% 40.91/6.13 % (152633)Instruction limit reached!
% 40.91/6.13 % (152633)------------------------------
% 40.91/6.13 % (152633)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.91/6.13 % (152633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.99/14.03 % (152633)CaDiCaL version: 2.1.3
% 95.99/14.03 % (152633)Termination reason: Instruction limit
% 95.99/14.03 % (152633)Termination phase: Finite model building SAT solving
% 95.99/14.03 % (152633)Time elapsed: 0.422 s
% 95.99/14.03 % (152633)Peak memory usage: 41 MB
% 95.99/14.03 % (152633)Instructions burned: 865 (million)
% 95.99/14.03 % (152644)fmb+10_1_sil=64000:random_seed=3954310000:i=22061:nm=2:gsp=on_2990 on theBenchmark for (2990ds/22061Mi)
% 95.99/14.03 % TRYING [5]
% 95.99/14.03 % (152642)Instruction limit reached!
% 95.99/14.03 % (152642)------------------------------
% 95.99/14.03 % (152642)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.99/14.03 % (152642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.99/14.03 % (152642)CaDiCaL version: 2.1.3
% 95.99/14.03 % (152642)Termination reason: Instruction limit
% 95.99/14.03 % (152642)Termination phase: Saturation
% 95.99/14.03 % (152642)Time elapsed: 0.184 s
% 95.99/14.03 % (152642)Peak memory usage: 33 MB
% 95.99/14.03 % (152642)Instructions burned: 882 (million)
% 95.99/14.03 % (152692)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3795809169:i=9515:nm=5_2988 on theBenchmark for (2988ds/9515Mi)
% 95.99/14.03 % TRYING [1]
% 95.99/14.03 % (152637)Instruction limit reached!
% 95.99/14.03 % (152637)------------------------------
% 95.99/14.03 % (152637)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.99/14.03 % (152637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.99/14.03 % (152637)CaDiCaL version: 2.1.3
% 95.99/14.03 % (152637)Termination reason: Instruction limit
% 95.99/14.03 % (152637)Termination phase: Finite model building constraint generation
% 95.99/14.03 % (152637)Time elapsed: 0.441 s
% 95.99/14.03 % (152637)Peak memory usage: 90 MB
% 95.99/14.03 % (152637)Instructions burned: 889 (million)
% 95.99/14.03 % TRYING [2]
% 95.99/14.03 % (152723)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1223422179:fmbsr=1.7:i=920_2987 on theBenchmark for (2987ds/920Mi)
% 95.99/14.03 % TRYING [20]
% 95.99/14.03 % (152640)Instruction limit reached!
% 95.99/14.03 % (152640)------------------------------
% 95.99/14.03 % (152640)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.99/14.03 % (152640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.99/14.03 % (152640)CaDiCaL version: 2.1.3
% 95.99/14.03 % (152640)Termination reason: Instruction limit
% 95.99/14.03 % (152640)Termination phase: Saturation
% 95.99/14.03 % (152640)Time elapsed: 0.420 s
% 95.99/14.03 % (152640)Peak memory usage: 34 MB
% 95.99/14.03 % (152640)Instructions burned: 692 (million)
% 95.99/14.03 % (152747)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2228368506:i=5131_2986 on theBenchmark for (2986ds/5131Mi)
% 95.99/14.03 % TRYING [8]
% 95.99/14.03 % TRYING [3]
% 95.99/14.03 % (152723)Instruction limit reached!
% 95.99/14.03 % (152723)------------------------------
% 95.99/14.03 % (152723)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.99/14.03 % (152723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.99/14.03 % (152723)CaDiCaL version: 2.1.3
% 95.99/14.03 % (152723)Termination reason: Instruction limit
% 95.99/14.03 % (152723)Termination phase: Finite model building constraint generation
% 95.99/14.03 % (152723)Time elapsed: 0.382 s
% 95.99/14.03 % (152723)Peak memory usage: 61 MB
% 95.99/14.03 % (152723)Instructions burned: 923 (million)
% 95.99/14.03 % TRYING [6]
% 95.99/14.03 % (152804)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2907237323:i=1472:ins=7:fdi=8:gsp=on_2983 on theBenchmark for (2983ds/1472Mi)
% 95.99/14.03 % TRYING [4]
% 95.99/14.03 % (152804)Instruction limit reached!
% 95.99/14.03 % (152804)------------------------------
% 95.99/14.03 % (152804)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.99/14.03 % (152804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.99/14.03 % (152804)CaDiCaL version: 2.1.3
% 95.99/14.03 % (152804)Termination reason: Instruction limit
% 95.99/14.03 % (152804)Termination phase: Saturation
% 95.99/14.03 % (152804)Time elapsed: 0.829 s
% 95.99/14.03 % (152804)Peak memory usage: 49 MB
% 95.99/14.03 % (152804)Instructions burned: 1472 (million)
% 95.99/14.03 % (152806)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3134660323:i=6324_2975 on theBenchmark for (2975ds/6324Mi)
% 95.99/14.03 % (152806)Cannot represent all propositional literals internally
% 95.99/14.03 % (152806)Refutation not found, incomplete strategy
% 95.99/14.03 % (152806)------------------------------
% 95.99/14.03 % (152806)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.99/14.03 % (152806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.59/18.84 % (152806)CaDiCaL version: 2.1.3
% 57.59/18.84 % (152806)Termination reason: Refutation not found, incomplete strategy
% 57.59/18.84 % (152806)Time elapsed: 0.233 s
% 57.59/18.84 % (152806)Peak memory usage: 29 MB
% 57.59/18.84 % (152806)Instructions burned: 438 (million)
% 57.59/18.84 % (152806)------------------------------
% 57.59/18.84 % (152806)------------------------------
% 57.59/18.84 % (152808)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2857172925:fmbsr=2.30978:i=2174_2972 on theBenchmark for (2972ds/2174Mi)
% 57.59/18.84 % TRYING [7]
% 57.59/18.84 % (152692)Instruction limit reached!
% 57.59/18.84 % (152692)------------------------------
% 57.59/18.84 % (152692)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.59/18.84 % (152692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.59/18.84 % (152692)CaDiCaL version: 2.1.3
% 57.59/18.84 % (152692)Termination reason: Instruction limit
% 57.59/18.84 % (152692)Termination phase: Finite model building constraint generation
% 57.59/18.84 % (152692)Time elapsed: 1.838 s
% 57.59/18.84 % (152692)Peak memory usage: 537 MB
% 57.59/18.84 % (152692)Instructions burned: 9518 (million)
% 57.59/18.84 % TRYING [16]
% 57.59/18.84 % (152810)ott-2_1_sil=16000:newcnf=on:random_seed=1172757868:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2969 on theBenchmark for (2969ds/869Mi)
% 57.59/18.84 % (152810)Instruction limit reached!
% 57.59/18.84 % (152810)------------------------------
% 57.59/18.84 % (152810)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.59/18.84 % (152810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.59/18.84 % (152810)CaDiCaL version: 2.1.3
% 57.59/18.84 % (152810)Termination reason: Instruction limit
% 57.59/18.84 % (152810)Termination phase: Saturation
% 57.59/18.84 % (152810)Time elapsed: 0.266 s
% 57.59/18.84 % (152810)Peak memory usage: 43 MB
% 57.59/18.84 % (152810)Instructions burned: 872 (million)
% 57.59/18.84 % (152812)ott+10_1_sil=32000:tgt=ground:random_seed=2314048945:i=5114:av=off_2967 on theBenchmark for (2967ds/5114Mi)
% 57.59/18.84 % (152808)Instruction limit reached!
% 57.59/18.84 % (152808)------------------------------
% 57.59/18.84 % (152808)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.59/18.84 % (152808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.59/18.84 % (152808)CaDiCaL version: 2.1.3
% 57.59/18.84 % (152808)Termination reason: Instruction limit
% 57.59/18.84 % (152808)Termination phase: Finite model building constraint generation
% 57.59/18.84 % (152808)Time elapsed: 0.802 s
% 57.59/18.84 % (152808)Peak memory usage: 121 MB
% 57.59/18.84 % (152808)Instructions burned: 2174 (million)
% 57.59/18.84 % (152814)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2107716691:i=54282_2964 on theBenchmark for (2964ds/54282Mi)
% 57.59/18.84 % TRYING [1]
% 57.59/18.84 % TRYING [2]
% 57.59/18.84 % TRYING [3]
% 57.59/18.84 % TRYING [4]
% 57.59/18.84 % (152747)Instruction limit reached!
% 57.59/18.84 % (152747)------------------------------
% 57.59/18.84 % (152747)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.59/18.84 % (152747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.59/18.84 % (152747)CaDiCaL version: 2.1.3
% 57.59/18.84 % (152747)Termination reason: Instruction limit
% 57.59/18.84 % (152747)Termination phase: Saturation
% 57.59/18.84 % (152747)Time elapsed: 2.712 s
% 57.59/18.84 % (152747)Peak memory usage: 109 MB
% 57.59/18.84 % (152747)Instructions burned: 5132 (million)
% 57.59/18.84 % (152816)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2639387237:i=3512:aac=none_2959 on theBenchmark for (2959ds/3512Mi)
% 57.59/18.84 % TRYING [5]
% 57.59/18.84 % TRYING [5]
% 57.59/18.84 % (152812)Instruction limit reached!
% 57.59/18.84 % (152812)------------------------------
% 57.59/18.84 % (152812)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.59/18.84 % (152812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.59/18.84 % (152812)CaDiCaL version: 2.1.3
% 57.59/18.84 % (152812)Termination reason: Instruction limit
% 57.59/18.84 % (152812)Termination phase: Saturation
% 57.59/18.84 % (152812)Time elapsed: 1.467 s
% 57.59/18.84 % (152812)Peak memory usage: 72 MB
% 57.59/18.84 % (152812)Instructions burned: 5116 (million)
% 57.59/18.84 % (152818)dis+21_1_sil=32000:sas=cadical:random_seed=3088119975:i=3773:amm=off_2952 on theBenchmark for (2952ds/3773Mi)
% 57.59/18.84 % TRYING [6]
% 57.59/18.84 % TRYING [8]
% 57.59/18.84 % (152818)Instruction limit reached!
% 57.59/18.84 % (152818)------------------------------
% 57.59/18.84 % (152818)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.59/18.84 % (152818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.59/18.84 % (152818)CaDiCaL version: 2.1.3
% 57.59/18.84 % (152818)Termination reason: Instruction limit
% 57.59/18.84 % (152818)Termination phase: Saturation
% 57.59/18.84 % (152818)Time elapsed: 1.110 s
% 57.59/18.84 % (152818)Peak memory usage: 106 MB
% 57.59/18.84 % (152818)Instructions burned: 3773 (million)
% 57.59/18.84 % (152820)ott+11_1_sil=16000:gs=on:random_seed=1613115817:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2941 on theBenchmark for (2941ds/2251Mi)
% 57.59/18.84 % TRYING [7]
% 57.59/18.84 % (152816)Instruction limit reached!
% 57.59/18.84 % (152816)------------------------------
% 57.59/18.84 % (152816)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.59/18.84 % (152816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.59/18.84 % (152816)CaDiCaL version: 2.1.3
% 57.59/18.84 % (152816)Termination reason: Instruction limit
% 57.59/18.84 % (152816)Termination phase: Saturation
% 57.59/18.84 % (152816)Time elapsed: 2.087 s
% 57.59/18.84 % (152816)Peak memory usage: 181 MB
% 57.59/18.84 % (152816)Instructions burned: 3512 (million)
% 57.59/18.84 % (152822)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=486646430:fmbsr=1.6:i=67534_2937 on theBenchmark for (2937ds/67534Mi)
% 57.59/18.84 % TRYING [7]
% 57.59/18.84 % (152820)Instruction limit reached!
% 57.59/18.84 % (152820)------------------------------
% 57.59/18.84 % (152820)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.59/18.84 % (152820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.59/18.84 % (152820)CaDiCaL version: 2.1.3
% 57.59/18.84 % (152820)Termination reason: Instruction limit
% 57.59/18.84 % (152820)Termination phase: Saturation
% 57.59/18.84 % (152820)Time elapsed: 0.767 s
% 57.59/18.84 % (152820)Peak memory usage: 86 MB
% 57.59/18.84 % (152820)Instructions burned: 2253 (million)
% 57.59/18.84 % (152824)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=263614881:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2933 on theBenchmark for (2933ds/4591Mi)
% 57.59/18.84 % TRYING [6]
% 57.59/18.84 % (152824)Instruction limit reached!
% 57.59/18.84 % (152824)------------------------------
% 57.59/18.84 % (152824)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.59/18.84 % (152824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.59/18.84 % (152824)CaDiCaL version: 2.1.3
% 57.59/18.84 % (152824)Termination reason: Instruction limit
% 57.59/18.84 % (152824)Termination phase: Saturation
% 57.59/18.84 % (152824)Time elapsed: 1.545 s
% 57.59/18.84 % (152824)Peak memory usage: 134 MB
% 57.59/18.84 % (152824)Instructions burned: 4593 (million)
% 57.59/18.84 % (152826)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3034394719:i=29340_2917 on theBenchmark for (2917ds/29340Mi)
% 57.59/18.84 % TRYING [8]
% 57.59/18.84 % (152644)Instruction limit reached!
% 57.59/18.84 % (152644)------------------------------
% 57.59/18.84 % (152644)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.59/18.84 % (152644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.59/18.84 % (152644)CaDiCaL version: 2.1.3
% 57.59/18.84 % (152644)Termination reason: Instruction limit
% 57.59/18.84 % (152644)Termination phase: Finite model building SAT solving
% 57.59/18.84 % (152644)Time elapsed: 9.267 s
% 57.59/18.84 % (152644)Peak memory usage: 212 MB
% 57.59/18.84 % (152644)Instructions burned: 22062 (million)
% 57.59/18.84 % (152828)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=678031820:i=5211_2897 on theBenchmark for (2897ds/5211Mi)
% 57.59/18.84 % (152828)Instruction limit reached!
% 57.59/18.84 % (152828)------------------------------
% 57.59/18.84 % (152828)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.59/18.84 % (152828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.59/18.84 % (152828)CaDiCaL version: 2.1.3
% 57.59/18.84 % (152828)Termination reason: Instruction limit
% 57.59/18.84 % (152828)Termination phase: Saturation
% 57.59/18.84 % (152828)Time elapsed: 1.538 s
% 57.59/18.84 % (152828)Peak memory usage: 36 MB
% 57.59/18.84 % (152828)Instructions burned: 5211 (million)
% 57.59/18.84 % (152830)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=334989864:i=5497:nm=2_2881 on theBenchmark for (2881ds/5497Mi)
% 57.59/18.84 % TRYING [17]
% 57.59/18.84 % TRYING [9]
% 57.59/18.84 % (152830)Instruction limit reached!
% 57.59/18.84 % (152830)------------------------------
% 57.59/18.84 % (152830)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.59/18.84 % (152830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.59/18.84 % (152830)CaDiCaL version: 2.1.3
% 57.59/18.84 % (152830)Termination reason: Instruction limit
% 57.59/18.84 % (152830)Termination phase: Finite model building constraint generation
% 57.59/18.84 % (152830)Time elapsed: 1.935 s
% 57.59/18.84 % (152830)Peak memory usage: 290 MB
% 57.59/18.84 % (152830)Instructions burned: 5498 (million)
% 57.59/18.84 % (153058)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2414384903:fmbsr=2:i=46332_2861 on theBenchmark for (2861ds/46332Mi)
% 57.59/18.84 % TRYING [15]
% 57.59/18.84 % TRYING [9]
% 57.59/18.84 % (152826) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-152592-152826"...
% 57.59/18.84 % (152826)...printing done.
% 57.59/18.84 % (152826)Refutation found. Thanks to Tanya!
% 57.59/18.84 % SZS status Theorem for theBenchmark
% 57.59/18.84 % SZS output start Proof for theBenchmark
% See solution above
% 57.59/18.86 % (152826)------------------------------
% 57.59/18.86 % (152826)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.59/18.86 % (152826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.59/18.86 % (152826)CaDiCaL version: 2.1.3
% 57.59/18.86 % (152826)Termination reason: Refutation
% 57.59/18.86 % (152826)Time elapsed: 10.064 s
% 57.59/18.86 % (152826)Peak memory usage: 360 MB
% 57.59/18.86 % (152826)Instructions burned: 25479 (million)
% 57.59/18.86 % (152592)Success in time 18.6 s
% 57.59/18.86 % Vampire exiting
%------------------------------------------------------------------------------