%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR041+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:34 AM UTC 2026
% Result : Theorem 6.16s 3.00s
% Output : Refutation 6.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 4
% Syntax : Number of formulae : 17 ( 6 unt; 0 def)
% Number of atoms : 28 ( 0 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 21 ( 10 ~; 6 |; 1 &)
% ( 0 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 3 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 5 ( 4 usr; 1 prp; 0-1 aty)
% Number of functors : 6 ( 6 usr; 3 con; 0-2 aty)
% Number of variables : 12 ( 12 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3091,axiom,
! [X0] :
( aspatialinformationstore(X0)
=> aspatialthing(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',ax3_3091) ).
fof(f5173,axiom,
! [X0] :
( microtheory(X0)
=> aspatialinformationstore(X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',ax3_5173) ).
fof(f44207,axiom,
! [X0,X1] : microtheory(f_contentmtofcdafromeventfn(X0,X1)),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+3.ax',ax3_44207) ).
fof(f44217,conjecture,
( mtvisible(c_tptp_member2831_mt)
=> aspatialthing(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwinformationblastcomtechnical_university_of_munichhtml)),c_translation_3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',query191) ).
fof(f44218,negated_conjecture,
~ ( mtvisible(c_tptp_member2831_mt)
=> aspatialthing(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwinformationblastcomtechnical_university_of_munichhtml)),c_translation_3)) ),
inference(negated_conjecture,[status(cth)],[f44217]) ).
fof(f47450,plain,
! [X0] :
( aspatialthing(X0)
| ~ aspatialinformationstore(X0) ),
inference(ennf_transformation,[],[f3091]) ).
fof(f47954,plain,
! [X0] :
( aspatialinformationstore(X0)
| ~ microtheory(X0) ),
inference(ennf_transformation,[],[f5173]) ).
fof(f66315,plain,
( ~ aspatialthing(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwinformationblastcomtechnical_university_of_munichhtml)),c_translation_3))
& mtvisible(c_tptp_member2831_mt) ),
inference(ennf_transformation,[],[f44218]) ).
fof(f69349,plain,
! [X0] :
( ~ aspatialinformationstore(X0)
| aspatialthing(X0) ),
inference(cnf_transformation,[],[f47450]) ).
fof(f71386,plain,
! [X0] :
( ~ microtheory(X0)
| aspatialinformationstore(X0) ),
inference(cnf_transformation,[],[f47954]) ).
fof(f108031,plain,
! [X0,X1] : microtheory(f_contentmtofcdafromeventfn(X0,X1)),
inference(cnf_transformation,[],[f44207]) ).
fof(f108042,plain,
~ aspatialthing(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwinformationblastcomtechnical_university_of_munichhtml)),c_translation_3)),
inference(cnf_transformation,[],[f66315]) ).
fof(f110421,plain,
! [X0] :
( aspatialthing(X0)
| aspatialinformationstore(X0) ),
inference(consistent_polarity_flipping,[],[f69349]) ).
fof(f112025,plain,
! [X0] :
( ~ aspatialinformationstore(X0)
| ~ microtheory(X0) ),
inference(consistent_polarity_flipping,[],[f71386]) ).
fof(f151759,plain,
aspatialinformationstore(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwinformationblastcomtechnical_university_of_munichhtml)),c_translation_3)),
inference(resolution,[],[f110421,f108042]) ).
fof(f151782,plain,
~ microtheory(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwinformationblastcomtechnical_university_of_munichhtml)),c_translation_3)),
inference(resolution,[],[f112025,f151759]) ).
fof(f151783,plain,
$false,
inference(forward_subsumption_resolution,[],[f151782,f108031]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : CSR041+4 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.09 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.29 % Computer : n009.cluster.edu
% 0.12/0.29 % Model : x86_64 x86_64
% 0.12/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.29 % Memory : 8046.5625MB
% 0.12/0.29 % OS : Linux 6.8.0-71-generic
% 0.12/0.29 % CPULimit : 300
% 0.12/0.29 % WCLimit : 300
% 0.12/0.29 % DateTime : Mon Sep 28 22:15:15 UTC 2026
% 0.12/0.29 % CPUTime :
% 0.12/0.29 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.29/0.34 Running first-order model finding
% 0.29/0.34 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
% 6.16/3.00 % (3556673)Will run a generic schedule for satisfiability detection.
% 6.16/3.00 % (3556679)% WARNING: option uhcvi not known.
% 6.16/3.00 % (3556679)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3184215371:i=135531:add=off:rawr=on_2984 on theBenchmark for (2984ds/135531Mi)
% 6.16/3.00 % (3556678)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=205862981_2984 on theBenchmark for (2984ds/0Mi)
% 6.16/3.00 % (3556680)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3662961116:i=88024:add=on:rawr=on_2984 on theBenchmark for (2984ds/88024Mi)
% 6.16/3.00 % (3556681)dis+10_1_sil=32000:sp=arity:random_seed=1092934560:i=103:fgj=on_2984 on theBenchmark for (2984ds/103Mi)
% 6.16/3.00 % (3556682)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1084272638:i=116_2984 on theBenchmark for (2984ds/116Mi)
% 6.16/3.00 % (3556683)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=625552801:i=131_2984 on theBenchmark for (2984ds/131Mi)
% 6.16/3.00 % (3556684)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3516193773:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2984 on theBenchmark for (2984ds/159Mi)
% 6.16/3.00 % (3556681)Instruction limit reached!
% 6.16/3.00 % (3556681)------------------------------
% 6.16/3.00 % (3556681)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.16/3.00 % (3556681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.16/3.00 % (3556681)CaDiCaL version: 2.1.3
% 6.16/3.00 % (3556681)Termination reason: Instruction limit
% 6.16/3.00 % (3556681)Termination phase: Preprocessing 2
% 6.16/3.00 % (3556681)Time elapsed: 0.143 s
% 6.16/3.00 % (3556681)Peak memory usage: 61 MB
% 6.16/3.00 % (3556681)Instructions burned: 104 (million)
% 6.16/3.00 % (3556682)Instruction limit reached!
% 6.16/3.00 % (3556682)------------------------------
% 6.16/3.00 % (3556682)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.16/3.00 % (3556682)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.16/3.00 % (3556682)CaDiCaL version: 2.1.3
% 6.16/3.00 % (3556682)Termination reason: Instruction limit
% 6.16/3.00 % (3556682)Termination phase: Preprocessing 2
% 6.16/3.00 % (3556682)Time elapsed: 0.158 s
% 6.16/3.00 % (3556682)Peak memory usage: 61 MB
% 6.16/3.00 % (3556682)Instructions burned: 116 (million)
% 6.16/3.00 % (3556692)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3616224441:i=714:nm=2_2982 on theBenchmark for (2982ds/714Mi)
% 6.16/3.00 % (3556684)Instruction limit reached!
% 6.16/3.00 % (3556684)------------------------------
% 6.16/3.00 % (3556684)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.16/3.00 % (3556684)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.16/3.00 % (3556684)CaDiCaL version: 2.1.3
% 6.16/3.00 % (3556684)Termination reason: Instruction limit
% 6.16/3.00 % (3556684)Termination phase: Naming
% 6.16/3.00 % (3556684)Time elapsed: 0.196 s
% 6.16/3.00 % (3556684)Peak memory usage: 62 MB
% 6.16/3.00 % (3556684)Instructions burned: 160 (million)
% 6.16/3.00 % (3556693)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2130237797:i=131:bd=preordered:fsd=on_2982 on theBenchmark for (2982ds/131Mi)
% 6.16/3.00 % (3556683)Instruction limit reached!
% 6.16/3.00 % (3556683)------------------------------
% 6.16/3.00 % (3556683)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.16/3.00 % (3556683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.16/3.00 % (3556683)CaDiCaL version: 2.1.3
% 6.16/3.00 % (3556683)Termination reason: Instruction limit
% 6.16/3.00 % (3556683)Termination phase: Preprocessing 2
% 6.16/3.00 % (3556683)Time elapsed: 0.208 s
% 6.16/3.00 % (3556683)Peak memory usage: 61 MB
% 6.16/3.00 % (3556683)Instructions burned: 131 (million)
% 6.16/3.00 % (3556696)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=4071440797:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2981 on theBenchmark for (2981ds/684Mi)
% 6.16/3.00 % (3556697)ott-21_1_sil=16000:fs=off:random_seed=262997330:i=180:av=off:fsr=off_2981 on theBenchmark for (2981ds/180Mi)
% 6.16/3.00 % (3556693)Instruction limit reached!
% 6.16/3.00 % (3556693)------------------------------
% 6.16/3.00 % (3556693)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.16/3.00 % (3556693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.16/3.00 % (3556693)CaDiCaL version: 2.1.3
% 6.16/3.00 % (3556693)Termination reason: Instruction limit
% 6.16/3.00 % (3556693)Termination phase: Preprocessing 2
% 6.16/3.00 % (3556693)Time elapsed: 0.172 s
% 6.16/3.00 % (3556693)Peak memory usage: 61 MB
% 6.16/3.00 % (3556693)Instructions burned: 131 (million)
% 6.16/3.00 % (3556700)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3634964307:i=477:bd=all_2979 on theBenchmark for (2979ds/477Mi)
% 6.16/3.00 % (3556697)Instruction limit reached!
% 6.16/3.00 % (3556697)------------------------------
% 6.16/3.00 % (3556697)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.16/3.00 % (3556697)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.16/3.00 % (3556697)CaDiCaL version: 2.1.3
% 6.16/3.00 % (3556697)Termination reason: Instruction limit
% 6.16/3.00 % (3556697)Termination phase: Preprocessing 3
% 6.16/3.00 % (3556697)Time elapsed: 0.220 s
% 6.16/3.00 % (3556697)Peak memory usage: 62 MB
% 6.16/3.00 % (3556697)Instructions burned: 180 (million)
% 6.16/3.00 % (3556702)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2927505920:fmbsr=1.3:i=865:ins=25_2978 on theBenchmark for (2978ds/865Mi)
% 6.16/3.00 % (3556679) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3556673-3556679"...
% 6.16/3.00 % (3556679)...printing done.
% 6.16/3.00 % (3556692)Instruction limit reached!
% 6.16/3.00 % (3556692)------------------------------
% 6.16/3.00 % (3556692)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.16/3.00 % (3556692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.16/3.00 % (3556692)CaDiCaL version: 2.1.3
% 6.16/3.00 % (3556692)Termination reason: Instruction limit
% 6.16/3.00 % (3556692)Termination phase: Finite model building preprocessing
% 6.16/3.00 % (3556692)Time elapsed: 0.717 s
% 6.16/3.00 % (3556692)Peak memory usage: 68 MB
% 6.16/3.00 % (3556692)Instructions burned: 714 (million)
% 6.16/3.00 % (3556679)Refutation found. Thanks to Tanya!
% 6.16/3.00 % SZS status Theorem for theBenchmark
% 6.16/3.00 % SZS output start Proof for theBenchmark
% See solution above
% 6.16/3.00 % (3556679)------------------------------
% 6.16/3.00 % (3556679)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.16/3.00 % (3556679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.16/3.00 % (3556679)CaDiCaL version: 2.1.3
% 6.16/3.00 % (3556679)Termination reason: Refutation
% 6.16/3.00 % (3556679)Time elapsed: 0.880 s
% 6.16/3.00 % (3556679)Peak memory usage: 94 MB
% 6.16/3.00 % (3556679)Instructions burned: 1527 (million)
% 6.16/3.00 % (3556673)Success in time 2.58 s
% 6.16/3.00 % Vampire exiting
%------------------------------------------------------------------------------