%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR040+3 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n002.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 1.95s 0.64s
% Output : Refutation 2.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 21
% Syntax : Number of formulae : 83 ( 23 unt; 0 def)
% Number of atoms : 143 ( 0 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 105 ( 45 ~; 38 |; 2 &)
% ( 0 <=>; 20 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 22 ( 21 usr; 1 prp; 0-1 aty)
% Number of functors : 6 ( 6 usr; 3 con; 0-2 aty)
% Number of variables : 57 ( 57 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f119,axiom,
! [X0] :
( tptpcol_13_109173(X0)
=> tptpcol_12_109157(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+2.ax',ax2_119) ).
fof(f179,axiom,
! [X0] :
( tptpcol_0_0(X0)
=> individual(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+2.ax',ax2_179) ).
fof(f477,axiom,
! [X0] :
( fixedordercollection(X0)
=> collection(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+2.ax',ax2_477) ).
fof(f634,axiom,
! [X0] :
( tptpcol_15_109185(X0)
=> tptpcol_14_109181(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+2.ax',ax2_634) ).
fof(f645,axiom,
! [X0] :
( tptpcol_8_109059(X0)
=> tptpcol_7_108547(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+2.ax',ax2_645) ).
fof(f678,axiom,
! [X0] :
( tptpcol_1_65536(X0)
=> tptpcol_0_0(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+2.ax',ax2_678) ).
fof(f1096,axiom,
! [X0] :
( tptpcol_5_106498(X0)
=> tptpcol_4_106497(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+2.ax',ax2_1096) ).
fof(f1102,axiom,
! [X0] :
( tptpcol_11_109125(X0)
=> tptpcol_10_109061(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+2.ax',ax2_1102) ).
fof(f1247,axiom,
! [X0] :
( tptpcol_7_108547(X0)
=> tptpcol_6_108546(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+2.ax',ax2_1247) ).
fof(f1282,axiom,
! [X0] :
( tptpcol_2_98304(X0)
=> tptpcol_1_65536(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+2.ax',ax2_1282) ).
fof(f1400,axiom,
! [X0] :
( tptpcol_14_109181(X0)
=> tptpcol_13_109173(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+2.ax',ax2_1400) ).
fof(f1444,axiom,
! [X0] :
( tptpcol_3_98305(X0)
=> tptpcol_2_98304(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+2.ax',ax2_1444) ).
fof(f1981,axiom,
! [X0] :
( tptpcol_9_109060(X0)
=> tptpcol_8_109059(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+2.ax',ax2_1981) ).
fof(f2336,axiom,
! [X0] :
( tptpcol_12_109157(X0)
=> tptpcol_11_109125(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+2.ax',ax2_2336) ).
fof(f2475,axiom,
! [X0] :
( tptpcol_4_106497(X0)
=> tptpcol_3_98305(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+2.ax',ax2_2475) ).
fof(f3061,axiom,
! [X0] :
( tptpcol_6_108546(X0)
=> tptpcol_5_106498(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+2.ax',ax2_3061) ).
fof(f3081,axiom,
firstordercollection(c_tptpcol_16_62187),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+2.ax',ax2_3081) ).
fof(f3089,axiom,
! [X0] :
~ ( collection(X0)
& individual(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+2.ax',ax2_3089) ).
fof(f3241,axiom,
! [X0] :
( firstordercollection(X0)
=> fixedordercollection(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+2.ax',ax2_3241) ).
fof(f3252,axiom,
! [X0] :
( tptpcol_10_109061(X0)
=> tptpcol_9_109060(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+2.ax',ax2_3252) ).
fof(f8006,conjecture,
( mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwthedailybulletincompostcardsmar9chtm)),c_translation_14))
=> ~ tptpcol_15_109185(c_tptpcol_16_62187) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',query140) ).
fof(f8007,negated_conjecture,
~ ( mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwthedailybulletincompostcardsmar9chtm)),c_translation_14))
=> ~ tptpcol_15_109185(c_tptpcol_16_62187) ),
inference(negated_conjecture,[status(cth)],[f8006]) ).
fof(f8760,plain,
! [X0] :
( tptpcol_12_109157(X0)
| ~ tptpcol_13_109173(X0) ),
inference(ennf_transformation,[],[f119]) ).
fof(f8782,plain,
! [X0] :
( individual(X0)
| ~ tptpcol_0_0(X0) ),
inference(ennf_transformation,[],[f179]) ).
fof(f8902,plain,
! [X0] :
( collection(X0)
| ~ fixedordercollection(X0) ),
inference(ennf_transformation,[],[f477]) ).
fof(f8964,plain,
! [X0] :
( tptpcol_14_109181(X0)
| ~ tptpcol_15_109185(X0) ),
inference(ennf_transformation,[],[f634]) ).
fof(f8969,plain,
! [X0] :
( tptpcol_7_108547(X0)
| ~ tptpcol_8_109059(X0) ),
inference(ennf_transformation,[],[f645]) ).
fof(f8981,plain,
! [X0] :
( tptpcol_0_0(X0)
| ~ tptpcol_1_65536(X0) ),
inference(ennf_transformation,[],[f678]) ).
fof(f9170,plain,
! [X0] :
( tptpcol_4_106497(X0)
| ~ tptpcol_5_106498(X0) ),
inference(ennf_transformation,[],[f1096]) ).
fof(f9174,plain,
! [X0] :
( tptpcol_10_109061(X0)
| ~ tptpcol_11_109125(X0) ),
inference(ennf_transformation,[],[f1102]) ).
fof(f9227,plain,
! [X0] :
( tptpcol_6_108546(X0)
| ~ tptpcol_7_108547(X0) ),
inference(ennf_transformation,[],[f1247]) ).
fof(f9243,plain,
! [X0] :
( tptpcol_1_65536(X0)
| ~ tptpcol_2_98304(X0) ),
inference(ennf_transformation,[],[f1282]) ).
fof(f9291,plain,
! [X0] :
( tptpcol_13_109173(X0)
| ~ tptpcol_14_109181(X0) ),
inference(ennf_transformation,[],[f1400]) ).
fof(f9309,plain,
! [X0] :
( tptpcol_2_98304(X0)
| ~ tptpcol_3_98305(X0) ),
inference(ennf_transformation,[],[f1444]) ).
fof(f9530,plain,
! [X0] :
( tptpcol_8_109059(X0)
| ~ tptpcol_9_109060(X0) ),
inference(ennf_transformation,[],[f1981]) ).
fof(f9667,plain,
! [X0] :
( tptpcol_11_109125(X0)
| ~ tptpcol_12_109157(X0) ),
inference(ennf_transformation,[],[f2336]) ).
fof(f9722,plain,
! [X0] :
( tptpcol_3_98305(X0)
| ~ tptpcol_4_106497(X0) ),
inference(ennf_transformation,[],[f2475]) ).
fof(f9971,plain,
! [X0] :
( tptpcol_5_106498(X0)
| ~ tptpcol_6_108546(X0) ),
inference(ennf_transformation,[],[f3061]) ).
fof(f9979,plain,
! [X0] :
( ~ collection(X0)
| ~ individual(X0) ),
inference(ennf_transformation,[],[f3089]) ).
fof(f10026,plain,
! [X0] :
( fixedordercollection(X0)
| ~ firstordercollection(X0) ),
inference(ennf_transformation,[],[f3241]) ).
fof(f10031,plain,
! [X0] :
( tptpcol_9_109060(X0)
| ~ tptpcol_10_109061(X0) ),
inference(ennf_transformation,[],[f3252]) ).
fof(f13400,plain,
( tptpcol_15_109185(c_tptpcol_16_62187)
& mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwthedailybulletincompostcardsmar9chtm)),c_translation_14)) ),
inference(ennf_transformation,[],[f8007]) ).
fof(f13514,plain,
! [X0] :
( ~ tptpcol_13_109173(X0)
| tptpcol_12_109157(X0) ),
inference(cnf_transformation,[],[f8760]) ).
fof(f13574,plain,
! [X0] :
( ~ tptpcol_0_0(X0)
| individual(X0) ),
inference(cnf_transformation,[],[f8782]) ).
fof(f13869,plain,
! [X0] :
( ~ fixedordercollection(X0)
| collection(X0) ),
inference(cnf_transformation,[],[f8902]) ).
fof(f14023,plain,
! [X0] :
( ~ tptpcol_15_109185(X0)
| tptpcol_14_109181(X0) ),
inference(cnf_transformation,[],[f8964]) ).
fof(f14034,plain,
! [X0] :
( ~ tptpcol_8_109059(X0)
| tptpcol_7_108547(X0) ),
inference(cnf_transformation,[],[f8969]) ).
fof(f14067,plain,
! [X0] :
( ~ tptpcol_1_65536(X0)
| tptpcol_0_0(X0) ),
inference(cnf_transformation,[],[f8981]) ).
fof(f14474,plain,
! [X0] :
( ~ tptpcol_5_106498(X0)
| tptpcol_4_106497(X0) ),
inference(cnf_transformation,[],[f9170]) ).
fof(f14480,plain,
! [X0] :
( ~ tptpcol_11_109125(X0)
| tptpcol_10_109061(X0) ),
inference(cnf_transformation,[],[f9174]) ).
fof(f14622,plain,
! [X0] :
( ~ tptpcol_7_108547(X0)
| tptpcol_6_108546(X0) ),
inference(cnf_transformation,[],[f9227]) ).
fof(f14657,plain,
! [X0] :
( ~ tptpcol_2_98304(X0)
| tptpcol_1_65536(X0) ),
inference(cnf_transformation,[],[f9243]) ).
fof(f14773,plain,
! [X0] :
( ~ tptpcol_14_109181(X0)
| tptpcol_13_109173(X0) ),
inference(cnf_transformation,[],[f9291]) ).
fof(f14815,plain,
! [X0] :
( ~ tptpcol_3_98305(X0)
| tptpcol_2_98304(X0) ),
inference(cnf_transformation,[],[f9309]) ).
fof(f15343,plain,
! [X0] :
( ~ tptpcol_9_109060(X0)
| tptpcol_8_109059(X0) ),
inference(cnf_transformation,[],[f9530]) ).
fof(f15693,plain,
! [X0] :
( ~ tptpcol_12_109157(X0)
| tptpcol_11_109125(X0) ),
inference(cnf_transformation,[],[f9667]) ).
fof(f15832,plain,
! [X0] :
( ~ tptpcol_4_106497(X0)
| tptpcol_3_98305(X0) ),
inference(cnf_transformation,[],[f9722]) ).
fof(f16409,plain,
! [X0] :
( ~ tptpcol_6_108546(X0)
| tptpcol_5_106498(X0) ),
inference(cnf_transformation,[],[f9971]) ).
fof(f16429,plain,
firstordercollection(c_tptpcol_16_62187),
inference(cnf_transformation,[],[f3081]) ).
fof(f16436,plain,
! [X0] :
( ~ collection(X0)
| ~ individual(X0) ),
inference(cnf_transformation,[],[f9979]) ).
fof(f16586,plain,
! [X0] :
( ~ firstordercollection(X0)
| fixedordercollection(X0) ),
inference(cnf_transformation,[],[f10026]) ).
fof(f16597,plain,
! [X0] :
( ~ tptpcol_10_109061(X0)
| tptpcol_9_109060(X0) ),
inference(cnf_transformation,[],[f10031]) ).
fof(f20688,plain,
tptpcol_15_109185(c_tptpcol_16_62187),
inference(cnf_transformation,[],[f13400]) ).
fof(f22214,plain,
tptpcol_14_109181(c_tptpcol_16_62187),
inference(resolution,[],[f14023,f20688]) ).
fof(f22223,plain,
tptpcol_13_109173(c_tptpcol_16_62187),
inference(resolution,[],[f14773,f22214]) ).
fof(f22226,plain,
tptpcol_12_109157(c_tptpcol_16_62187),
inference(resolution,[],[f22223,f13514]) ).
fof(f23820,plain,
fixedordercollection(c_tptpcol_16_62187),
inference(resolution,[],[f16586,f16429]) ).
fof(f23926,plain,
collection(c_tptpcol_16_62187),
inference(resolution,[],[f23820,f13869]) ).
fof(f23955,plain,
~ individual(c_tptpcol_16_62187),
inference(resolution,[],[f23926,f16436]) ).
fof(f23998,plain,
tptpcol_11_109125(c_tptpcol_16_62187),
inference(resolution,[],[f15693,f22226]) ).
fof(f24001,plain,
tptpcol_10_109061(c_tptpcol_16_62187),
inference(resolution,[],[f23998,f14480]) ).
fof(f24018,plain,
tptpcol_9_109060(c_tptpcol_16_62187),
inference(resolution,[],[f16597,f24001]) ).
fof(f24021,plain,
tptpcol_8_109059(c_tptpcol_16_62187),
inference(resolution,[],[f24018,f15343]) ).
fof(f24022,plain,
tptpcol_7_108547(c_tptpcol_16_62187),
inference(resolution,[],[f24021,f14034]) ).
fof(f24031,plain,
tptpcol_6_108546(c_tptpcol_16_62187),
inference(resolution,[],[f14622,f24022]) ).
fof(f24042,plain,
tptpcol_5_106498(c_tptpcol_16_62187),
inference(resolution,[],[f16409,f24031]) ).
fof(f24045,plain,
tptpcol_4_106497(c_tptpcol_16_62187),
inference(resolution,[],[f24042,f14474]) ).
fof(f24048,plain,
tptpcol_3_98305(c_tptpcol_16_62187),
inference(resolution,[],[f24045,f15832]) ).
fof(f24049,plain,
tptpcol_2_98304(c_tptpcol_16_62187),
inference(resolution,[],[f24048,f14815]) ).
fof(f24051,plain,
tptpcol_1_65536(c_tptpcol_16_62187),
inference(resolution,[],[f24049,f14657]) ).
fof(f24052,plain,
tptpcol_0_0(c_tptpcol_16_62187),
inference(resolution,[],[f24051,f14067]) ).
fof(f24053,plain,
individual(c_tptpcol_16_62187),
inference(resolution,[],[f24052,f13574]) ).
fof(f24054,plain,
$false,
inference(forward_subsumption_resolution,[],[f24053,f23955]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR040+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.18 % Computer : n002.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 22:17:37 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.21 Running first-order model finding
% 0.08/0.21 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 1.95/0.63 % (840129)Will run a generic schedule for satisfiability detection.
% 1.95/0.63 % (840138)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=991128194:i=116_2998 on theBenchmark for (2998ds/116Mi)
% 1.95/0.63 % (840135)% WARNING: option uhcvi not known.
% 1.95/0.63 % (840136)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1974700809:i=88024:add=on:rawr=on_2998 on theBenchmark for (2998ds/88024Mi)
% 1.95/0.63 % (840134)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1911637941_2998 on theBenchmark for (2998ds/0Mi)
% 1.95/0.63 % (840135)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1278995424:i=135531:add=off:rawr=on_2998 on theBenchmark for (2998ds/135531Mi)
% 1.95/0.63 % (840137)dis+10_1_sil=32000:sp=arity:random_seed=3352408938:i=103:fgj=on_2998 on theBenchmark for (2998ds/103Mi)
% 1.95/0.63 % (840139)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1861942036:i=131_2998 on theBenchmark for (2998ds/131Mi)
% 1.95/0.63 % (840140)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1137284880:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2998 on theBenchmark for (2998ds/159Mi)
% 1.95/0.63 % (840138)Instruction limit reached!
% 1.95/0.63 % (840138)------------------------------
% 1.95/0.63 % (840138)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.95/0.63 % (840138)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.95/0.63 % (840138)CaDiCaL version: 2.1.3
% 1.95/0.63 % (840138)Termination reason: Instruction limit
% 1.95/0.63 % (840138)Termination phase: Blocked clause elimination
% 1.95/0.63 % (840138)Time elapsed: 0.045 s
% 1.95/0.63 % (840138)Peak memory usage: 24 MB
% 1.95/0.63 % (840138)Instructions burned: 119 (million)
% 1.95/0.63 % (840148)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2831964657:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 1.95/0.63 % (840137)Instruction limit reached!
% 1.95/0.63 % (840137)------------------------------
% 1.95/0.63 % (840137)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.95/0.63 % (840137)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.95/0.63 % (840137)CaDiCaL version: 2.1.3
% 1.95/0.64 % (840137)Termination reason: Instruction limit
% 1.95/0.64 % (840137)Termination phase: Saturation
% 1.95/0.64 % (840137)Time elapsed: 0.060 s
% 1.95/0.64 % (840137)Peak memory usage: 22 MB
% 1.95/0.64 % (840137)Instructions burned: 104 (million)
% 1.95/0.64 % (840150)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2126029664:i=131:bd=preordered:fsd=on_2997 on theBenchmark for (2997ds/131Mi)
% 1.95/0.64 % (840140)Instruction limit reached!
% 1.95/0.64 % (840140)------------------------------
% 1.95/0.64 % (840140)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.95/0.64 % (840140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.95/0.64 % (840140)CaDiCaL version: 2.1.3
% 1.95/0.64 % (840140)Termination reason: Instruction limit
% 1.95/0.64 % (840140)Termination phase: Saturation
% 1.95/0.64 % (840140)Time elapsed: 0.089 s
% 1.95/0.64 % (840140)Peak memory usage: 25 MB
% 1.95/0.64 % (840140)Instructions burned: 159 (million)
% 1.95/0.64 % (840139)Instruction limit reached!
% 1.95/0.64 % (840139)------------------------------
% 1.95/0.64 % (840139)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.95/0.64 % (840139)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.95/0.64 % (840139)CaDiCaL version: 2.1.3
% 1.95/0.64 % (840139)Termination reason: Instruction limit
% 1.95/0.64 % (840139)Termination phase: Saturation
% 1.95/0.64 % (840139)Time elapsed: 0.098 s
% 1.95/0.64 % (840139)Peak memory usage: 23 MB
% 1.95/0.64 % (840139)Instructions burned: 132 (million)
% 1.95/0.64 % (840152)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=693408087:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi)
% 1.95/0.64 % (840153)ott-21_1_sil=16000:fs=off:random_seed=1262833262:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 1.95/0.64 % (840150)Instruction limit reached!
% 1.95/0.64 % (840150)------------------------------
% 1.95/0.64 % (840150)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.95/0.64 % (840150)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.95/0.64 % (840150)CaDiCaL version: 2.1.3
% 1.95/0.64 % (840150)Termination reason: Instruction limit
% 1.95/0.64 % (840150)Termination phase: Blocked clause elimination
% 1.95/0.64 % (840150)Time elapsed: 0.078 s
% 1.95/0.64 % (840150)Peak memory usage: 23 MB
% 1.95/0.64 % (840150)Instructions burned: 132 (million)
% 1.95/0.64 % TRYING [1]
% 1.95/0.64 % TRYING [2]
% 1.95/0.64 % (840156)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2659995366:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 1.95/0.64 % TRYING [3]
% 1.95/0.64 % TRYING [1]
% 1.95/0.64 % (840136) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-840129-840136"...
% 1.95/0.64 % (840153)Instruction limit reached!
% 1.95/0.64 % (840153)------------------------------
% 1.95/0.64 % (840153)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.95/0.64 % (840153)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.95/0.64 % (840153)CaDiCaL version: 2.1.3
% 1.95/0.64 % (840153)Termination reason: Instruction limit
% 1.95/0.64 % (840153)Termination phase: Saturation
% 1.95/0.64 % (840153)Time elapsed: 0.109 s
% 1.95/0.64 % (840153)Peak memory usage: 23 MB
% 1.95/0.64 % (840153)Instructions burned: 181 (million)
% 1.95/0.64 % (840148)Instruction limit reached!
% 1.95/0.64 % (840148)------------------------------
% 1.95/0.64 % (840148)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.95/0.64 % (840148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.95/0.64 % (840148)CaDiCaL version: 2.1.3
% 1.95/0.64 % (840148)Termination reason: Instruction limit
% 1.95/0.64 % (840148)Termination phase: Finite model building constraint generation
% 1.95/0.64 % (840148)Time elapsed: 0.190 s
% 1.95/0.64 % (840148)Peak memory usage: 41 MB
% 1.95/0.64 % (840148)Instructions burned: 719 (million)
% 1.95/0.64 % (840136)...printing done.
% 1.95/0.64 % (840136)Refutation found. Thanks to Tanya!
% 1.95/0.64 % SZS status Theorem for theBenchmark
% 1.95/0.64 % SZS output start Proof for theBenchmark
% See solution above
% 2.18/0.65 % (840136)------------------------------
% 2.18/0.65 % (840136)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.18/0.65 % (840136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.18/0.65 % (840136)CaDiCaL version: 2.1.3
% 2.18/0.65 % (840136)Termination reason: Refutation
% 2.18/0.65 % (840136)Time elapsed: 0.237 s
% 2.18/0.65 % (840136)Peak memory usage: 29 MB
% 2.18/0.65 % (840136)Instructions burned: 479 (million)
% 2.18/0.65 % (840129)Success in time 0.413 s
% 2.18/0.65 % Vampire exiting
%------------------------------------------------------------------------------