%------------------------------------------------------------------------------
% File : Vampire-SAT---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 SAT
% Computer : n009.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:33 AM UTC 2026
% Result : Theorem 9.60s 3.92s
% Output : Refutation 9.60s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 21
% Syntax : Number of formulae : 99 ( 12 unt; 0 def)
% Number of atoms : 186 ( 0 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 157 ( 70 ~; 65 |; 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 : 84 ( 84 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f318,axiom,
! [X0] :
( tptpcol_0_0(X0)
=> individual(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',ax3_318) ).
fof(f448,axiom,
! [X0] :
( tptpcol_10_109061(X0)
=> tptpcol_9_109060(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',ax3_448) ).
fof(f733,axiom,
! [X0] :
( tptpcol_9_109060(X0)
=> tptpcol_8_109059(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',ax3_733) ).
fof(f1291,axiom,
! [X0] :
( tptpcol_8_109059(X0)
=> tptpcol_7_108547(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',ax3_1291) ).
fof(f1714,axiom,
! [X0] :
( firstordercollection(X0)
=> fixedordercollection(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',ax3_1714) ).
fof(f3253,axiom,
! [X0] :
( tptpcol_6_108546(X0)
=> tptpcol_5_106498(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',ax3_3253) ).
fof(f3389,axiom,
! [X0] :
( tptpcol_12_109157(X0)
=> tptpcol_11_109125(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',ax3_3389) ).
fof(f4028,axiom,
! [X0] :
~ ( collection(X0)
& individual(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',ax3_4028) ).
fof(f5043,axiom,
! [X0] :
( tptpcol_1_65536(X0)
=> tptpcol_0_0(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',ax3_5043) ).
fof(f5511,axiom,
! [X0] :
( tptpcol_2_98304(X0)
=> tptpcol_1_65536(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',ax3_5511) ).
fof(f5949,axiom,
! [X0] :
( tptpcol_4_106497(X0)
=> tptpcol_3_98305(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',ax3_5949) ).
fof(f6733,axiom,
! [X0] :
( tptpcol_15_109185(X0)
=> tptpcol_14_109181(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',ax3_6733) ).
fof(f7614,axiom,
! [X0] :
( tptpcol_14_109181(X0)
=> tptpcol_13_109173(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',ax3_7614) ).
fof(f9044,axiom,
! [X0] :
( tptpcol_7_108547(X0)
=> tptpcol_6_108546(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',ax3_9044) ).
fof(f12015,axiom,
! [X0] :
( fixedordercollection(X0)
=> collection(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',ax3_12015) ).
fof(f15240,axiom,
! [X0] :
( tptpcol_5_106498(X0)
=> tptpcol_4_106497(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',ax3_15240) ).
fof(f15564,axiom,
! [X0] :
( tptpcol_13_109173(X0)
=> tptpcol_12_109157(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',ax3_15564) ).
fof(f20268,axiom,
firstordercollection(c_tptpcol_16_62187),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',ax3_20268) ).
fof(f22390,axiom,
! [X0] :
( tptpcol_3_98305(X0)
=> tptpcol_2_98304(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',ax3_22390) ).
fof(f24107,axiom,
! [X0] :
( tptpcol_11_109125(X0)
=> tptpcol_10_109061(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',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_10_109061(X0)
| tptpcol_9_109060(X0) ),
inference(cnf_transformation,[],[f46808]) ).
fof(f67039,plain,
! [X0] :
( ~ tptpcol_9_109060(X0)
| tptpcol_8_109059(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] :
( ~ firstordercollection(X0)
| fixedordercollection(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_12_109157(X0)
| tptpcol_11_109125(X0) ),
inference(cnf_transformation,[],[f47512]) ).
fof(f70265,plain,
! [X0] :
( ~ individual(X0)
| ~ collection(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_4_106497(X0)
| tptpcol_3_98305(X0) ),
inference(cnf_transformation,[],[f48161]) ).
fof(f72914,plain,
! [X0] :
( ~ tptpcol_15_109185(X0)
| tptpcol_14_109181(X0) ),
inference(cnf_transformation,[],[f48350]) ).
fof(f73780,plain,
! [X0] :
( ~ tptpcol_14_109181(X0)
| tptpcol_13_109173(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_5_106498(X0)
| tptpcol_4_106497(X0) ),
inference(cnf_transformation,[],[f50480]) ).
fof(f81583,plain,
! [X0] :
( ~ tptpcol_13_109173(X0)
| tptpcol_12_109157(X0) ),
inference(cnf_transformation,[],[f50551]) ).
fof(f86203,plain,
firstordercollection(c_tptpcol_16_62187),
inference(cnf_transformation,[],[f20268]) ).
fof(f88282,plain,
! [X0] :
( ~ tptpcol_3_98305(X0)
| tptpcol_2_98304(X0) ),
inference(cnf_transformation,[],[f52203]) ).
fof(f89959,plain,
! [X0] :
( ~ tptpcol_11_109125(X0)
| tptpcol_10_109061(X0) ),
inference(cnf_transformation,[],[f52611]) ).
fof(f108042,plain,
tptpcol_15_109185(c_tptpcol_16_62187),
inference(cnf_transformation,[],[f66315]) ).
fof(f108128,plain,
! [X0] :
( tptpcol_0_0(X0)
| individual(X0) ),
inference(consistent_polarity_flipping,[],[f66629]) ).
fof(f108161,plain,
! [X0] :
( ~ tptpcol_9_109060(X0)
| ~ tptpcol_10_109061(X0) ),
inference(consistent_polarity_flipping,[],[f66758]) ).
fof(f108249,plain,
! [X0] :
( tptpcol_8_109059(X0)
| tptpcol_9_109060(X0) ),
inference(consistent_polarity_flipping,[],[f67039]) ).
fof(f108539,plain,
! [X0] :
( ~ fixedordercollection(X0)
| firstordercollection(X0) ),
inference(consistent_polarity_flipping,[],[f68002]) ).
fof(f109003,plain,
! [X0] :
( ~ tptpcol_11_109125(X0)
| tptpcol_12_109157(X0) ),
inference(consistent_polarity_flipping,[],[f69640]) ).
fof(f109204,plain,
! [X0] :
( collection(X0)
| ~ individual(X0) ),
inference(consistent_polarity_flipping,[],[f70265]) ).
fof(f109485,plain,
! [X0] :
( ~ tptpcol_1_65536(X0)
| ~ tptpcol_0_0(X0) ),
inference(consistent_polarity_flipping,[],[f71258]) ).
fof(f109605,plain,
! [X0] :
( tptpcol_2_98304(X0)
| tptpcol_1_65536(X0) ),
inference(consistent_polarity_flipping,[],[f71715]) ).
fof(f109758,plain,
! [X0] :
( ~ tptpcol_4_106497(X0)
| ~ tptpcol_3_98305(X0) ),
inference(consistent_polarity_flipping,[],[f72143]) ).
fof(f109981,plain,
! [X0] :
( ~ tptpcol_14_109181(X0)
| ~ tptpcol_15_109185(X0) ),
inference(consistent_polarity_flipping,[],[f72914]) ).
fof(f110266,plain,
! [X0] :
( ~ tptpcol_13_109173(X0)
| tptpcol_14_109181(X0) ),
inference(consistent_polarity_flipping,[],[f73780]) ).
fof(f111521,plain,
! [X0] :
( fixedordercollection(X0)
| ~ collection(X0) ),
inference(consistent_polarity_flipping,[],[f78105]) ).
fof(f112541,plain,
! [X0] :
( ~ tptpcol_12_109157(X0)
| tptpcol_13_109173(X0) ),
inference(consistent_polarity_flipping,[],[f81583]) ).
fof(f113930,plain,
~ firstordercollection(c_tptpcol_16_62187),
inference(consistent_polarity_flipping,[],[f86203]) ).
fof(f114561,plain,
! [X0] :
( ~ tptpcol_2_98304(X0)
| tptpcol_3_98305(X0) ),
inference(consistent_polarity_flipping,[],[f88282]) ).
fof(f115042,plain,
! [X0] :
( tptpcol_11_109125(X0)
| tptpcol_10_109061(X0) ),
inference(consistent_polarity_flipping,[],[f89959]) ).
fof(f131685,plain,
! [X0] :
( ~ tptpcol_6_108546(X0)
| tptpcol_4_106497(X0) ),
inference(resolution,[],[f81265,f69508]) ).
fof(f131786,plain,
! [X0] :
( ~ collection(X0)
| firstordercollection(X0) ),
inference(resolution,[],[f111521,f108539]) ).
fof(f131825,plain,
! [X0] :
( tptpcol_3_98305(X0)
| tptpcol_1_65536(X0) ),
inference(resolution,[],[f114561,f109605]) ).
fof(f131835,plain,
! [X0] :
( tptpcol_12_109157(X0)
| tptpcol_10_109061(X0) ),
inference(resolution,[],[f115042,f109003]) ).
fof(f131876,plain,
! [X0] :
( ~ tptpcol_7_108547(X0)
| tptpcol_4_106497(X0) ),
inference(resolution,[],[f131685,f75181]) ).
fof(f131910,plain,
! [X0] :
( firstordercollection(X0)
| ~ individual(X0) ),
inference(resolution,[],[f131786,f109204]) ).
fof(f131932,plain,
! [X0] :
( tptpcol_13_109173(X0)
| tptpcol_10_109061(X0) ),
inference(resolution,[],[f131835,f112541]) ).
fof(f131954,plain,
! [X0] :
( ~ tptpcol_8_109059(X0)
| tptpcol_4_106497(X0) ),
inference(resolution,[],[f131876,f67587]) ).
fof(f132091,plain,
~ individual(c_tptpcol_16_62187),
inference(resolution,[],[f131910,f113930]) ).
fof(f132555,plain,
! [X0] :
( tptpcol_14_109181(X0)
| tptpcol_10_109061(X0) ),
inference(resolution,[],[f131932,f110266]) ).
fof(f132559,plain,
! [X0] :
( tptpcol_9_109060(X0)
| tptpcol_4_106497(X0) ),
inference(resolution,[],[f131954,f108249]) ).
fof(f132712,plain,
! [X0] :
( ~ tptpcol_15_109185(X0)
| tptpcol_10_109061(X0) ),
inference(resolution,[],[f132555,f109981]) ).
fof(f132714,plain,
! [X0] :
( ~ tptpcol_10_109061(X0)
| tptpcol_4_106497(X0) ),
inference(resolution,[],[f132559,f108161]) ).
fof(f132744,plain,
tptpcol_10_109061(c_tptpcol_16_62187),
inference(resolution,[],[f132712,f108042]) ).
fof(f132745,plain,
tptpcol_4_106497(c_tptpcol_16_62187),
inference(resolution,[],[f132714,f132744]) ).
fof(f132746,plain,
~ tptpcol_3_98305(c_tptpcol_16_62187),
inference(resolution,[],[f132745,f109758]) ).
fof(f132747,plain,
tptpcol_1_65536(c_tptpcol_16_62187),
inference(resolution,[],[f132746,f131825]) ).
fof(f132748,plain,
~ tptpcol_0_0(c_tptpcol_16_62187),
inference(resolution,[],[f132747,f109485]) ).
fof(f132750,plain,
individual(c_tptpcol_16_62187),
inference(resolution,[],[f132748,f108128]) ).
fof(f132751,plain,
$false,
inference(forward_subsumption_resolution,[],[f132750,f132091]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : CSR040+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.10 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.27/0.31 % Computer : n009.cluster.edu
% 0.27/0.31 % Model : x86_64 x86_64
% 0.27/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.27/0.31 % Memory : 8046.5625MB
% 0.27/0.31 % OS : Linux 6.8.0-71-generic
% 0.27/0.31 % CPULimit : 300
% 0.27/0.31 % WCLimit : 300
% 0.27/0.31 % DateTime : Mon Sep 28 22:15:00 UTC 2026
% 0.27/0.32 % CPUTime :
% 0.27/0.32 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.27/0.37 Running first-order model finding
% 0.27/0.37 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
% 9.60/3.92 % (3556213)Will run a generic schedule for satisfiability detection.
% 9.60/3.92 % (3556219)% WARNING: option uhcvi not known.
% 9.60/3.92 % (3556224)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1803699969:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2984 on theBenchmark for (2984ds/159Mi)
% 9.60/3.92 % (3556218)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2082047265_2984 on theBenchmark for (2984ds/0Mi)
% 9.60/3.92 % (3556219)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=497284507:i=135531:add=off:rawr=on_2984 on theBenchmark for (2984ds/135531Mi)
% 9.60/3.92 % (3556220)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2396429480:i=88024:add=on:rawr=on_2984 on theBenchmark for (2984ds/88024Mi)
% 9.60/3.92 % (3556221)dis+10_1_sil=32000:sp=arity:random_seed=3921095818:i=103:fgj=on_2984 on theBenchmark for (2984ds/103Mi)
% 9.60/3.92 % (3556222)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=4241766967:i=116_2984 on theBenchmark for (2984ds/116Mi)
% 9.60/3.92 % (3556223)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3979161366:i=131_2984 on theBenchmark for (2984ds/131Mi)
% 9.60/3.92 % (3556224)Instruction limit reached!
% 9.60/3.92 % (3556224)------------------------------
% 9.60/3.92 % (3556224)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.60/3.92 % (3556224)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.60/3.92 % (3556224)CaDiCaL version: 2.1.3
% 9.60/3.92 % (3556224)Termination reason: Instruction limit
% 9.60/3.92 % (3556224)Termination phase: Naming
% 9.60/3.92 % (3556224)Time elapsed: 0.128 s
% 9.60/3.92 % (3556224)Peak memory usage: 62 MB
% 9.60/3.92 % (3556224)Instructions burned: 159 (million)
% 9.60/3.92 % (3556221)Instruction limit reached!
% 9.60/3.92 % (3556221)------------------------------
% 9.60/3.92 % (3556221)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.60/3.92 % (3556221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.60/3.92 % (3556221)CaDiCaL version: 2.1.3
% 9.60/3.92 % (3556221)Termination reason: Instruction limit
% 9.60/3.92 % (3556221)Termination phase: Preprocessing 2
% 9.60/3.92 % (3556221)Time elapsed: 0.142 s
% 9.60/3.92 % (3556221)Peak memory usage: 61 MB
% 9.60/3.92 % (3556221)Instructions burned: 104 (million)
% 9.60/3.92 % (3556222)Instruction limit reached!
% 9.60/3.92 % (3556222)------------------------------
% 9.60/3.92 % (3556222)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.60/3.92 % (3556222)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.60/3.92 % (3556222)CaDiCaL version: 2.1.3
% 9.60/3.92 % (3556222)Termination reason: Instruction limit
% 9.60/3.92 % (3556222)Termination phase: Preprocessing 2
% 9.60/3.92 % (3556222)Time elapsed: 0.160 s
% 9.60/3.92 % (3556222)Peak memory usage: 61 MB
% 9.60/3.92 % (3556222)Instructions burned: 116 (million)
% 9.60/3.92 % (3556232)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=689963502:i=714:nm=2_2982 on theBenchmark for (2982ds/714Mi)
% 9.60/3.92 % (3556233)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1644378167:i=131:bd=preordered:fsd=on_2982 on theBenchmark for (2982ds/131Mi)
% 9.60/3.92 % (3556223)Instruction limit reached!
% 9.60/3.92 % (3556223)------------------------------
% 9.60/3.92 % (3556223)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.60/3.92 % (3556223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.60/3.92 % (3556223)CaDiCaL version: 2.1.3
% 9.60/3.92 % (3556223)Termination reason: Instruction limit
% 9.60/3.92 % (3556223)Termination phase: Preprocessing 2
% 9.60/3.92 % (3556223)Time elapsed: 0.194 s
% 9.60/3.92 % (3556223)Peak memory usage: 61 MB
% 9.60/3.92 % (3556223)Instructions burned: 131 (million)
% 9.60/3.92 % (3556234)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=3845264915:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2982 on theBenchmark for (2982ds/684Mi)
% 9.60/3.92 % (3556237)ott-21_1_sil=16000:fs=off:random_seed=870619808:i=180:av=off:fsr=off_2981 on theBenchmark for (2981ds/180Mi)
% 9.60/3.92 % (3556233)Instruction limit reached!
% 9.60/3.92 % (3556233)------------------------------
% 9.60/3.92 % (3556233)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.60/3.92 % (3556233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.60/3.92 % (3556233)CaDiCaL version: 2.1.3
% 9.60/3.92 % (3556233)Termination reason: Instruction limit
% 9.60/3.92 % (3556233)Termination phase: Preprocessing 2
% 9.60/3.92 % (3556233)Time elapsed: 0.175 s
% 9.60/3.92 % (3556233)Peak memory usage: 61 MB
% 9.60/3.92 % (3556233)Instructions burned: 131 (million)
% 9.60/3.92 % (3556240)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=23655394:i=477:bd=all_2980 on theBenchmark for (2980ds/477Mi)
% 9.60/3.92 % (3556237)Instruction limit reached!
% 9.60/3.92 % (3556237)------------------------------
% 9.60/3.92 % (3556237)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.60/3.92 % (3556237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.60/3.92 % (3556237)CaDiCaL version: 2.1.3
% 9.60/3.92 % (3556237)Termination reason: Instruction limit
% 9.60/3.92 % (3556237)Termination phase: Preprocessing 3
% 9.60/3.92 % (3556237)Time elapsed: 0.217 s
% 9.60/3.92 % (3556237)Peak memory usage: 62 MB
% 9.60/3.92 % (3556237)Instructions burned: 180 (million)
% 9.60/3.92 % (3556242)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=229866576:fmbsr=1.3:i=865:ins=25_2979 on theBenchmark for (2979ds/865Mi)
% 9.60/3.92 % (3556232)Instruction limit reached!
% 9.60/3.92 % (3556232)------------------------------
% 9.60/3.92 % (3556232)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.60/3.92 % (3556232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.60/3.92 % (3556232)CaDiCaL version: 2.1.3
% 9.60/3.92 % (3556232)Termination reason: Instruction limit
% 9.60/3.92 % (3556232)Termination phase: Finite model building preprocessing
% 9.60/3.92 % (3556232)Time elapsed: 0.433 s
% 9.60/3.92 % (3556232)Peak memory usage: 69 MB
% 9.60/3.92 % (3556232)Instructions burned: 716 (million)
% 9.60/3.92 % (3556244)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=844023474:i=1179_2977 on theBenchmark for (2977ds/1179Mi)
% 9.60/3.92 % (3556234)Instruction limit reached!
% 9.60/3.92 % (3556234)------------------------------
% 9.60/3.92 % (3556234)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.60/3.92 % (3556234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.60/3.92 % (3556234)CaDiCaL version: 2.1.3
% 9.60/3.92 % (3556234)Termination reason: Instruction limit
% 9.60/3.92 % (3556234)Termination phase: Property scanning
% 9.60/3.92 % (3556234)Time elapsed: 0.740 s
% 9.60/3.92 % (3556234)Peak memory usage: 73 MB
% 9.60/3.92 % (3556234)Instructions burned: 684 (million)
% 9.60/3.92 % (3556240)Instruction limit reached!
% 9.60/3.92 % (3556240)------------------------------
% 9.60/3.92 % (3556240)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.60/3.92 % (3556240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.60/3.92 % (3556240)CaDiCaL version: 2.1.3
% 9.60/3.92 % (3556240)Termination reason: Instruction limit
% 9.60/3.92 % (3556240)Termination phase: Property scanning
% 9.60/3.92 % (3556240)Time elapsed: 0.539 s
% 9.60/3.92 % (3556240)Peak memory usage: 66 MB
% 9.60/3.92 % (3556240)Instructions burned: 480 (million)
% 9.60/3.92 % (3556247)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=790353604:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2974 on theBenchmark for (2974ds/692Mi)
% 9.60/3.92 % (3556246)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1407496624:i=889:ins=1_2974 on theBenchmark for (2974ds/889Mi)
% 9.60/3.92 % (3556244)Instruction limit reached!
% 9.60/3.92 % (3556244)------------------------------
% 9.60/3.92 % (3556244)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.60/3.92 % (3556244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.60/3.92 % (3556244)CaDiCaL version: 2.1.3
% 9.60/3.92 % (3556244)Termination reason: Instruction limit
% 9.60/3.92 % (3556244)Termination phase: Saturation
% 9.60/3.92 % (3556244)Time elapsed: 0.665 s
% 9.60/3.92 % (3556244)Peak memory usage: 81 MB
% 9.60/3.92 % (3556244)Instructions burned: 1180 (million)
% 9.60/3.92 % (3556251)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1493555755:i=879:kws=inv_precedence:fsr=off_2970 on theBenchmark for (2970ds/879Mi)
% 9.60/3.92 % (3556242)Instruction limit reached!
% 9.60/3.92 % (3556242)------------------------------
% 9.60/3.92 % (3556242)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.60/3.92 % (3556242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.60/3.92 % (3556242)CaDiCaL version: 2.1.3
% 9.60/3.92 % (3556242)Termination reason: Instruction limit
% 9.60/3.92 % (3556242)Termination phase: Finite model building preprocessing
% 9.60/3.92 % (3556242)Time elapsed: 0.879 s
% 9.60/3.92 % (3556242)Peak memory usage: 86 MB
% 9.60/3.92 % (3556242)Instructions burned: 867 (million)
% 9.60/3.92 % (3556253)fmb+10_1_sil=64000:random_seed=830415677:i=22061:nm=2:gsp=on_2969 on theBenchmark for (2969ds/22061Mi)
% 9.60/3.92 % (3556219) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3556213-3556219"...
% 9.60/3.92 % (3556247)Instruction limit reached!
% 9.60/3.92 % (3556247)------------------------------
% 9.60/3.92 % (3556247)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.60/3.92 % (3556247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.60/3.92 % (3556247)CaDiCaL version: 2.1.3
% 9.60/3.92 % (3556247)Termination reason: Instruction limit
% 9.60/3.92 % (3556247)Termination phase: Property scanning
% 9.60/3.92 % (3556247)Time elapsed: 0.769 s
% 9.60/3.92 % (3556247)Peak memory usage: 79 MB
% 9.60/3.92 % (3556247)Instructions burned: 692 (million)
% 9.60/3.92 % (3556255)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1824922924:i=9515:nm=5_2965 on theBenchmark for (2965ds/9515Mi)
% 9.60/3.92 % (3556219)...printing done.
% 9.60/3.92 % (3556219)Refutation found. Thanks to Tanya!
% 9.60/3.92 % SZS status Theorem for theBenchmark
% 9.60/3.92 % SZS output start Proof for theBenchmark
% See solution above
% 9.60/4.02 % (3556219)------------------------------
% 9.60/4.02 % (3556219)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.60/4.02 % (3556219)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.60/4.02 % (3556219)CaDiCaL version: 2.1.3
% 9.60/4.02 % (3556219)Termination reason: Refutation
% 9.60/4.02 % (3556219)Time elapsed: 1.796 s
% 9.60/4.02 % (3556219)Peak memory usage: 94 MB
% 9.60/4.02 % (3556219)Instructions burned: 1708 (million)
% 9.60/4.02 % (3556213)Success in time 3.532 s
% 9.60/4.02 % Vampire exiting
%------------------------------------------------------------------------------