%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR063+5 : TPTP v9.3.1. Bugfixed v3.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n013.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:50 AM UTC 2026
% Result : Theorem 0.22s 46.23s
% Output : Refutation 0.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 4
% Syntax : Number of formulae : 17 ( 10 unt; 0 def)
% Number of atoms : 24 ( 0 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 19 ( 12 ~; 5 |; 1 &)
% ( 0 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 3 avg)
% Maximal term depth : 3 ( 2 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 2 con; 0-1 aty)
% Number of variables : 10 ( 10 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f117498,axiom,
! [X0] :
~ ( collection(X0)
& individual(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+4.ax',ax4_117519) ).
fof(f289015,axiom,
individual(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+4.ax',ax4_289056) ).
fof(f540089,axiom,
! [X0,X1] :
( disjointwith(X0,X1)
=> collection(X0) ),
file('/export/starexec/sandbox/benchmark/Axioms/CSR002+4.ax',ax4_540134) ).
fof(f540250,conjecture,
~ disjointwith(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_tptpcol_16_118949),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',query263) ).
fof(f540251,negated_conjecture,
~ ~ disjointwith(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_tptpcol_16_118949),
inference(negated_conjecture,[status(cth)],[f540250]) ).
fof(f540252,plain,
disjointwith(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_tptpcol_16_118949),
inference(flattening,[],[f540251]) ).
fof(f648061,plain,
! [X0] :
( ~ collection(X0)
| ~ individual(X0) ),
inference(ennf_transformation,[],[f117498]) ).
fof(f936314,plain,
! [X0,X1] :
( collection(X0)
| ~ disjointwith(X0,X1) ),
inference(ennf_transformation,[],[f540089]) ).
fof(f1044890,plain,
! [X0] :
( ~ individual(X0)
| ~ collection(X0) ),
inference(cnf_transformation,[],[f648061]) ).
fof(f1203120,plain,
individual(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))),
inference(cnf_transformation,[],[f289015]) ).
fof(f1426579,plain,
! [X0,X1] :
( ~ disjointwith(X0,X1)
| collection(X0) ),
inference(cnf_transformation,[],[f936314]) ).
fof(f1426738,plain,
disjointwith(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)),c_tptpcol_16_118949),
inference(cnf_transformation,[],[f540252]) ).
fof(f1472801,plain,
! [X0] :
( ~ collection(X0)
| individual(X0) ),
inference(consistent_polarity_flipping,[],[f1044890]) ).
fof(f1539806,plain,
~ individual(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))),
inference(consistent_polarity_flipping,[],[f1203120]) ).
fof(f2368516,plain,
collection(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))),
inference(resolution,[],[f1426579,f1426738]) ).
fof(f2375616,plain,
individual(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))),
inference(resolution,[],[f2368516,f1472801]) ).
fof(f2375617,plain,
$false,
inference(forward_subsumption_resolution,[],[f2375616,f1539806]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR063+5 : TPTP v9.3.1. Bugfixed v3.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.20 % Computer : n013.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:21:36 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.23 Running first-order model finding
% 0.09/0.23 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
% 62.37/19.93 % (1652658)Will run a generic schedule for satisfiability detection.
% 62.37/19.93 % (1652955)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1806885491_2873 on theBenchmark for (2873ds/0Mi)
% 62.37/19.93 % (1652957)% WARNING: option uhcvi not known.
% 62.37/19.93 % (1652957)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3706191341:i=135531:add=off:rawr=on_2873 on theBenchmark for (2873ds/135531Mi)
% 62.37/19.93 % (1652959)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2008236772:i=88024:add=on:rawr=on_2873 on theBenchmark for (2873ds/88024Mi)
% 62.37/19.93 % (1652961)dis+10_1_sil=32000:sp=arity:random_seed=1396079006:i=103:fgj=on_2873 on theBenchmark for (2873ds/103Mi)
% 62.37/19.93 % (1652963)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2449964805:i=116_2873 on theBenchmark for (2873ds/116Mi)
% 62.37/19.93 % (1652965)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2817509585:i=131_2873 on theBenchmark for (2873ds/131Mi)
% 62.37/19.93 % (1652966)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=374412601:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2873 on theBenchmark for (2873ds/159Mi)
% 62.37/19.93 % (1652961)Instruction limit reached!
% 62.37/19.93 % (1652961)------------------------------
% 62.37/19.93 % (1652961)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 62.37/19.93 % (1652961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.37/19.93 % (1652961)CaDiCaL version: 2.1.3
% 62.37/19.93 % (1652961)Termination reason: Instruction limit
% 62.37/19.93 % (1652961)Termination phase: Preprocessing 1
% 62.37/19.93 % (1652961)Time elapsed: 0.086 s
% 62.37/19.93 % (1652961)Peak memory usage: 639 MB
% 62.37/19.93 % (1652961)Instructions burned: 104 (million)
% 62.37/19.93 % (1652963)Instruction limit reached!
% 62.37/19.93 % (1652963)------------------------------
% 62.37/19.93 % (1652963)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 62.37/19.93 % (1652963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.37/19.93 % (1652963)CaDiCaL version: 2.1.3
% 62.37/19.93 % (1652963)Termination reason: Instruction limit
% 62.37/19.93 % (1652963)Termination phase: Preprocessing 1
% 62.37/19.93 % (1652963)Time elapsed: 0.110 s
% 62.37/19.93 % (1652963)Peak memory usage: 639 MB
% 62.37/19.93 % (1652963)Instructions burned: 117 (million)
% 62.37/19.93 % (1652969)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3654982010:i=714:nm=2_2871 on theBenchmark for (2871ds/714Mi)
% 62.37/19.93 % (1652965)Instruction limit reached!
% 62.37/19.93 % (1652965)------------------------------
% 62.37/19.93 % (1652965)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 62.37/19.93 % (1652965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.37/19.93 % (1652965)CaDiCaL version: 2.1.3
% 62.37/19.93 % (1652965)Termination reason: Instruction limit
% 62.37/19.93 % (1652965)Termination phase: Preprocessing 1
% 62.37/19.93 % (1652965)Time elapsed: 0.109 s
% 62.37/19.93 % (1652965)Peak memory usage: 639 MB
% 62.37/19.93 % (1652965)Instructions burned: 132 (million)
% 62.37/19.93 % (1652966)Instruction limit reached!
% 62.37/19.93 % (1652966)------------------------------
% 62.37/19.93 % (1652966)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 62.37/19.93 % (1652966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.37/19.93 % (1652966)CaDiCaL version: 2.1.3
% 62.37/19.93 % (1652966)Termination reason: Instruction limit
% 62.37/19.93 % (1652966)Termination phase: Preprocessing 1
% 62.37/19.93 % (1652966)Time elapsed: 0.132 s
% 62.37/19.93 % (1652966)Peak memory usage: 640 MB
% 62.37/19.93 % (1652966)Instructions burned: 159 (million)
% 62.37/19.93 % (1652971)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3830637160:i=131:bd=preordered:fsd=on_2870 on theBenchmark for (2870ds/131Mi)
% 62.37/19.93 % (1652973)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=904981271:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2870 on theBenchmark for (2870ds/684Mi)
% 62.37/19.93 % (1652975)ott-21_1_sil=16000:fs=off:random_seed=3688793982:i=180:av=off:fsr=off_2870 on theBenchmark for (2870ds/180Mi)
% 62.37/19.93 % (1652971)Instruction limit reached!
% 62.37/19.93 % (1652971)------------------------------
% 62.37/19.93 % (1652971)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 62.37/19.93 % (1652971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 103.47/25.80 % (1652971)CaDiCaL version: 2.1.3
% 103.47/25.80 % (1652971)Termination reason: Instruction limit
% 103.47/25.80 % (1652971)Termination phase: Preprocessing 1
% 103.47/25.80 % (1652971)Time elapsed: 0.108 s
% 103.47/25.80 % (1652971)Peak memory usage: 640 MB
% 103.47/25.80 % (1652971)Instructions burned: 131 (million)
% 103.47/25.80 % (1652977)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=288582365:i=477:bd=all_2869 on theBenchmark for (2869ds/477Mi)
% 103.47/25.80 % (1652975)Instruction limit reached!
% 103.47/25.80 % (1652975)------------------------------
% 103.47/25.80 % (1652975)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 103.47/25.80 % (1652975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 103.47/25.80 % (1652975)CaDiCaL version: 2.1.3
% 103.47/25.80 % (1652975)Termination reason: Instruction limit
% 103.47/25.80 % (1652975)Termination phase: Preprocessing 1
% 103.47/25.80 % (1652975)Time elapsed: 0.149 s
% 103.47/25.80 % (1652975)Peak memory usage: 640 MB
% 103.47/25.80 % (1652975)Instructions burned: 181 (million)
% 103.47/25.80 % (1652979)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4068795039:fmbsr=1.3:i=865:ins=25_2868 on theBenchmark for (2868ds/865Mi)
% 103.47/25.80 % (1652969)Instruction limit reached!
% 103.47/25.80 % (1652969)------------------------------
% 103.47/25.80 % (1652969)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 103.47/25.80 % (1652969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 103.47/25.80 % (1652969)CaDiCaL version: 2.1.3
% 103.47/25.80 % (1652969)Termination reason: Instruction limit
% 103.47/25.80 % (1652969)Termination phase: Preprocessing 1
% 103.47/25.80 % (1652969)Time elapsed: 0.525 s
% 103.47/25.80 % (1652969)Peak memory usage: 640 MB
% 103.47/25.80 % (1652969)Instructions burned: 714 (million)
% 103.47/25.80 % (1652973)Instruction limit reached!
% 103.47/25.80 % (1652973)------------------------------
% 103.47/25.80 % (1652973)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 103.47/25.80 % (1652973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 103.47/25.80 % (1652973)CaDiCaL version: 2.1.3
% 103.47/25.80 % (1652973)Termination reason: Instruction limit
% 103.47/25.80 % (1652973)Termination phase: SInE selection
% 103.47/25.80 % (1652973)Time elapsed: 0.471 s
% 103.47/25.80 % (1652973)Peak memory usage: 642 MB
% 103.47/25.80 % (1652973)Instructions burned: 685 (million)
% 103.47/25.80 % (1652977)Instruction limit reached!
% 103.47/25.80 % (1652977)------------------------------
% 103.47/25.80 % (1652977)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 103.47/25.80 % (1652977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 103.47/25.80 % (1652977)CaDiCaL version: 2.1.3
% 103.47/25.80 % (1652977)Termination reason: Instruction limit
% 103.47/25.80 % (1652977)Termination phase: Preprocessing 1
% 103.47/25.80 % (1652977)Time elapsed: 0.377 s
% 103.47/25.80 % (1652977)Peak memory usage: 640 MB
% 103.47/25.80 % (1652977)Instructions burned: 477 (million)
% 103.47/25.80 % (1652981)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1268053348:i=1179_2865 on theBenchmark for (2865ds/1179Mi)
% 103.47/25.80 % (1652982)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1150151663:i=889:ins=1_2865 on theBenchmark for (2865ds/889Mi)
% 103.47/25.80 % (1652985)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=975534360:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2864 on theBenchmark for (2864ds/692Mi)
% 103.47/25.80 % (1652979)Instruction limit reached!
% 103.47/25.80 % (1652979)------------------------------
% 103.47/25.80 % (1652979)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 103.47/25.80 % (1652979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 103.47/25.80 % (1652979)CaDiCaL version: 2.1.3
% 103.47/25.80 % (1652979)Termination reason: Instruction limit
% 103.47/25.80 % (1652979)Termination phase: Preprocessing 1
% 103.47/25.80 % (1652979)Time elapsed: 0.621 s
% 103.47/25.80 % (1652979)Peak memory usage: 640 MB
% 103.47/25.80 % (1652979)Instructions burned: 866 (million)
% 103.47/25.80 % (1653031)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3140125931:i=879:kws=inv_precedence:fsr=off_2861 on theBenchmark for (2861ds/879Mi)
% 103.47/25.80 % (1652985)Instruction limit reached!
% 103.47/25.80 % (1652985)------------------------------
% 103.47/25.80 % (1652985)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 103.47/25.80 % (1652985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 180.15/36.51 % (1652985)CaDiCaL version: 2.1.3
% 180.15/36.51 % (1652985)Termination reason: Instruction limit
% 180.15/36.51 % (1652985)Termination phase: SInE selection
% 180.15/36.51 % (1652985)Time elapsed: 0.483 s
% 180.15/36.51 % (1652985)Peak memory usage: 642 MB
% 180.15/36.51 % (1652985)Instructions burned: 692 (million)
% 180.15/36.51 % (1653119)fmb+10_1_sil=64000:random_seed=2712054783:i=22061:nm=2:gsp=on_2859 on theBenchmark for (2859ds/22061Mi)
% 180.15/36.51 % (1652982)Instruction limit reached!
% 180.15/36.51 % (1652982)------------------------------
% 180.15/36.51 % (1652982)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 180.15/36.51 % (1652982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 180.15/36.51 % (1652982)CaDiCaL version: 2.1.3
% 180.15/36.51 % (1652982)Termination reason: Instruction limit
% 180.15/36.51 % (1652982)Termination phase: Preprocessing 1
% 180.15/36.51 % (1652982)Time elapsed: 0.635 s
% 180.15/36.51 % (1652982)Peak memory usage: 640 MB
% 180.15/36.51 % (1652982)Instructions burned: 890 (million)
% 180.15/36.51 % (1653129)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=4220003059:i=9515:nm=5_2858 on theBenchmark for (2858ds/9515Mi)
% 180.15/36.51 % (1652981)Instruction limit reached!
% 180.15/36.51 % (1652981)------------------------------
% 180.15/36.51 % (1652981)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 180.15/36.51 % (1652981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 180.15/36.51 % (1652981)CaDiCaL version: 2.1.3
% 180.15/36.51 % (1652981)Termination reason: Instruction limit
% 180.15/36.51 % (1652981)Termination phase: Unused predicate definition removal
% 180.15/36.51 % (1652981)Time elapsed: 1.047 s
% 180.15/36.51 % (1652981)Peak memory usage: 717 MB
% 180.15/36.51 % (1652981)Instructions burned: 1179 (million)
% 180.15/36.51 % (1653169)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3083678673:fmbsr=1.7:i=920_2854 on theBenchmark for (2854ds/920Mi)
% 180.15/36.51 % (1653031)Instruction limit reached!
% 180.15/36.51 % (1653031)------------------------------
% 180.15/36.51 % (1653031)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 180.15/36.51 % (1653031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 180.15/36.51 % (1653031)CaDiCaL version: 2.1.3
% 180.15/36.51 % (1653031)Termination reason: Instruction limit
% 180.15/36.51 % (1653031)Termination phase: Unused predicate definition removal
% 180.15/36.51 % (1653031)Time elapsed: 0.816 s
% 180.15/36.51 % (1653031)Peak memory usage: 704 MB
% 180.15/36.51 % (1653031)Instructions burned: 879 (million)
% 180.15/36.51 % (1653227)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3792383282:i=5131_2852 on theBenchmark for (2852ds/5131Mi)
% 180.15/36.51 % (1653169)Instruction limit reached!
% 180.15/36.51 % (1653169)------------------------------
% 180.15/36.51 % (1653169)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 180.15/36.51 % (1653169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 180.15/36.51 % (1653169)CaDiCaL version: 2.1.3
% 180.15/36.51 % (1653169)Termination reason: Instruction limit
% 180.15/36.51 % (1653169)Termination phase: Preprocessing 1
% 180.15/36.51 % (1653169)Time elapsed: 0.890 s
% 180.15/36.51 % (1653169)Peak memory usage: 640 MB
% 180.15/36.51 % (1653169)Instructions burned: 920 (million)
% 180.15/36.51 % (1653289)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=999007074:i=1472:ins=7:fdi=8:gsp=on_2844 on theBenchmark for (2844ds/1472Mi)
% 180.15/36.51 % (1653289)Instruction limit reached!
% 180.15/36.51 % (1653289)------------------------------
% 180.15/36.51 % (1653289)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 180.15/36.51 % (1653289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 180.15/36.51 % (1653289)CaDiCaL version: 2.1.3
% 180.15/36.51 % (1653289)Termination reason: Instruction limit
% 180.15/36.51 % (1653289)Termination phase: Preprocessing 2
% 180.15/36.51 % (1653289)Time elapsed: 1.467 s
% 180.15/36.51 % (1653289)Peak memory usage: 724 MB
% 180.15/36.51 % (1653289)Instructions burned: 1473 (million)
% 180.15/36.51 % (1653448)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1479498461:i=6324_2828 on theBenchmark for (2828ds/6324Mi)
% 180.15/36.51 % (1653227)Instruction limit reached!
% 180.15/36.51 % (1653227)------------------------------
% 180.15/36.51 % (1653227)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 180.15/36.51 % (1653227)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 180.15/36.51 % (1653227)CaDiCaL version: 2.1.3
% 180.15/36.51 % (1653227)Termination reason: Instruction limit
% 0.22/46.22 % (1653227)Termination phase: Property scanning
% 0.22/46.22 % (1653227)Time elapsed: 4.841 s
% 0.22/46.22 % (1653227)Peak memory usage: 880 MB
% 0.22/46.22 % (1653227)Instructions burned: 5131 (million)
% 0.22/46.22 % (1653450)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2003826593:fmbsr=2.30978:i=2174_2802 on theBenchmark for (2802ds/2174Mi)
% 0.22/46.22 % (1653129)Instruction limit reached!
% 0.22/46.22 % (1653129)------------------------------
% 0.22/46.22 % (1653129)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/46.22 % (1653129)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/46.22 % (1653129)CaDiCaL version: 2.1.3
% 0.22/46.22 % (1653129)Termination reason: Instruction limit
% 0.22/46.22 % (1653129)Termination phase: Finite model building preprocessing
% 0.22/46.22 % (1653129)Time elapsed: 6.991 s
% 0.22/46.22 % (1653129)Peak memory usage: 864 MB
% 0.22/46.22 % (1653129)Instructions burned: 9515 (million)
% 0.22/46.22 % (1653452)ott-2_1_sil=16000:newcnf=on:random_seed=1496972043:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2786 on theBenchmark for (2786ds/869Mi)
% 0.22/46.22 % (1653450)Instruction limit reached!
% 0.22/46.22 % (1653450)------------------------------
% 0.22/46.22 % (1653450)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/46.22 % (1653450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/46.22 % (1653450)CaDiCaL version: 2.1.3
% 0.22/46.22 % (1653450)Termination reason: Instruction limit
% 0.22/46.22 % (1653450)Termination phase: Naming
% 0.22/46.22 % (1653450)Time elapsed: 1.875 s
% 0.22/46.22 % (1653450)Peak memory usage: 746 MB
% 0.22/46.22 % (1653450)Instructions burned: 2175 (million)
% 0.22/46.22 % (1653454)ott+10_1_sil=32000:tgt=ground:random_seed=3997673806:i=5114:av=off_2782 on theBenchmark for (2782ds/5114Mi)
% 0.22/46.22 % (1653448)Instruction limit reached!
% 0.22/46.22 % (1653448)------------------------------
% 0.22/46.22 % (1653448)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/46.22 % (1653448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/46.22 % (1653448)CaDiCaL version: 2.1.3
% 0.22/46.22 % (1653448)Termination reason: Instruction limit
% 0.22/46.22 % (1653448)Termination phase: Property scanning
% 0.22/46.22 % (1653448)Time elapsed: 4.664 s
% 0.22/46.22 % (1653448)Peak memory usage: 795 MB
% 0.22/46.22 % (1653448)Instructions burned: 6325 (million)
% 0.22/46.22 % (1653456)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2062105713:i=54282_2780 on theBenchmark for (2780ds/54282Mi)
% 0.22/46.22 % (1653452)Instruction limit reached!
% 0.22/46.22 % (1653452)------------------------------
% 0.22/46.22 % (1653452)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/46.22 % (1653452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/46.22 % (1653452)CaDiCaL version: 2.1.3
% 0.22/46.22 % (1653452)Termination reason: Instruction limit
% 0.22/46.22 % (1653452)Termination phase: Unused predicate definition removal
% 0.22/46.22 % (1653452)Time elapsed: 0.794 s
% 0.22/46.22 % (1653452)Peak memory usage: 702 MB
% 0.22/46.22 % (1653452)Instructions burned: 869 (million)
% 0.22/46.22 % (1653458)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2200622330:i=3512:aac=none_2777 on theBenchmark for (2777ds/3512Mi)
% 0.22/46.22 % (1653458)Instruction limit reached!
% 0.22/46.22 % (1653458)------------------------------
% 0.22/46.22 % (1653458)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/46.22 % (1653458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/46.22 % (1653458)CaDiCaL version: 2.1.3
% 0.22/46.22 % (1653458)Termination reason: Instruction limit
% 0.22/46.22 % (1653458)Termination phase: Preprocessing 3
% 0.22/46.22 % (1653458)Time elapsed: 2.449 s
% 0.22/46.22 % (1653458)Peak memory usage: 746 MB
% 0.22/46.22 % (1653458)Instructions burned: 3513 (million)
% 0.22/46.22 % (1653460)dis+21_1_sil=32000:sas=cadical:random_seed=2079091341:i=3773:amm=off_2752 on theBenchmark for (2752ds/3773Mi)
% 0.22/46.22 % (1653454)Instruction limit reached!
% 0.22/46.22 % (1653454)------------------------------
% 0.22/46.22 % (1653454)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/46.22 % (1653454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/46.22 % (1653454)CaDiCaL version: 2.1.3
% 0.22/46.22 % (1653454)Termination reason: Instruction limit
% 0.22/46.22 % (1653454)Termination phase: Property scanning
% 0.22/46.22 % (1653454)Time elapsed: 3.750 s
% 0.22/46.22 % (1653454)Peak memory usage: 795 MB
% 0.22/46.22 % (1653454)Instructions burned: 5115 (million)
% 0.22/46.22 % (1653462)ott+11_1_sil=16000:gs=on:random_seed=1040408877:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2743 on theBenchmark for (2743ds/2251Mi)
% 0.22/46.22 % (1653462)Instruction limit reached!
% 0.22/46.22 % (1653462)------------------------------
% 0.22/46.22 % (1653462)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/46.22 % (1653462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/46.22 % (1653462)CaDiCaL version: 2.1.3
% 0.22/46.22 % (1653462)Termination reason: Instruction limit
% 0.22/46.22 % (1653462)Termination phase: SInE selection
% 0.22/46.22 % (1653462)Time elapsed: 1.468 s
% 0.22/46.22 % (1653462)Peak memory usage: 660 MB
% 0.22/46.22 % (1653462)Instructions burned: 2252 (million)
% 0.22/46.22 % (1653464)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2480556692:fmbsr=1.6:i=67534_2728 on theBenchmark for (2728ds/67534Mi)
% 0.22/46.22 % (1653460)Instruction limit reached!
% 0.22/46.22 % (1653460)------------------------------
% 0.22/46.22 % (1653460)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/46.22 % (1653460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/46.22 % (1653460)CaDiCaL version: 2.1.3
% 0.22/46.22 % (1653460)Termination reason: Instruction limit
% 0.22/46.22 % (1653460)Termination phase: Preprocessing 3
% 0.22/46.22 % (1653460)Time elapsed: 2.557 s
% 0.22/46.22 % (1653460)Peak memory usage: 746 MB
% 0.22/46.22 % (1653460)Instructions burned: 3774 (million)
% 0.22/46.22 % (1653466)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2015336504:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2725 on theBenchmark for (2725ds/4591Mi)
% 0.22/46.22 % (1653119)Instruction limit reached!
% 0.22/46.22 % (1653119)------------------------------
% 0.22/46.22 % (1653119)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/46.22 % (1653119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/46.22 % (1653119)CaDiCaL version: 2.1.3
% 0.22/46.22 % (1653119)Termination reason: Instruction limit
% 0.22/46.22 % (1653119)Termination phase: Finite model building preprocessing
% 0.22/46.22 % (1653119)Time elapsed: 14.411 s
% 0.22/46.22 % (1653119)Peak memory usage: 1171 MB
% 0.22/46.22 % (1653119)Instructions burned: 22061 (million)
% 0.22/46.22 % (1653470)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1457869651:i=29340_2713 on theBenchmark for (2713ds/29340Mi)
% 0.22/46.22 % (1653466)Instruction limit reached!
% 0.22/46.22 % (1653466)------------------------------
% 0.22/46.22 % (1653466)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/46.22 % (1653466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/46.22 % (1653466)CaDiCaL version: 2.1.3
% 0.22/46.22 % (1653466)Termination reason: Instruction limit
% 0.22/46.22 % (1653466)Termination phase: Property scanning
% 0.22/46.22 % (1653466)Time elapsed: 3.801 s
% 0.22/46.22 % (1653466)Peak memory usage: 795 MB
% 0.22/46.22 % (1653466)Instructions burned: 4591 (million)
% 0.22/46.22 % (1653751)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2702921953:i=5211_2686 on theBenchmark for (2686ds/5211Mi)
% 0.22/46.22 % TRYING [1]
% 0.22/46.22 % (1653751)Instruction limit reached!
% 0.22/46.22 % (1653751)------------------------------
% 0.22/46.22 % (1653751)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/46.22 % (1653751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/46.22 % (1653751)CaDiCaL version: 2.1.3
% 0.22/46.22 % (1653751)Termination reason: Instruction limit
% 0.22/46.22 % (1653751)Termination phase: Property scanning
% 0.22/46.22 % (1653751)Time elapsed: 2.305 s
% 0.22/46.22 % (1653751)Peak memory usage: 795 MB
% 0.22/46.22 % (1653751)Instructions burned: 5211 (million)
% 0.22/46.22 % (1653906)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=1181377846:i=5497:nm=2_2662 on theBenchmark for (2662ds/5497Mi)
% 0.22/46.22 % TRYING [2]
% 0.22/46.22 % (1653906)Instruction limit reached!
% 0.22/46.22 % (1653906)------------------------------
% 0.22/46.22 % (1653906)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/46.22 % (1653906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/46.22 % (1653906)CaDiCaL version: 2.1.3
% 0.22/46.22 % (1653906)Termination reason: Instruction limit
% 0.22/46.22 % (1653906)Termination phase: Property scanning
% 0.22/46.23 % (1653906)Time elapsed: 2.486 s
% 0.22/46.23 % (1653906)Peak memory usage: 795 MB
% 0.22/46.23 % (1653906)Instructions burned: 5498 (million)
% 0.22/46.23 % (1653908)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3701270786:fmbsr=2:i=46332_2636 on theBenchmark for (2636ds/46332Mi)
% 0.22/46.23 % TRYING [3]
% 0.22/46.23 % TRYING [1]
% 0.22/46.23 % (1652957) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-1652658-1652957"...
% 0.22/46.23 % (1652957)...printing done.
% 0.22/46.23 % (1652957)Refutation found. Thanks to Tanya!
% 0.22/46.23 % SZS status Theorem for theBenchmark
% 0.22/46.23 % SZS output start Proof for theBenchmark
% See solution above
% 0.22/46.23 % (1652957)------------------------------
% 0.22/46.23 % (1652957)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.22/46.23 % (1652957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.22/46.23 % (1652957)CaDiCaL version: 2.1.3
% 0.22/46.23 % (1652957)Termination reason: Refutation
% 0.22/46.23 % (1652957)Time elapsed: 30.730 s
% 0.22/46.23 % (1652957)Peak memory usage: 1418 MB
% 0.22/46.23 % (1652957)Instructions burned: 60745 (million)
% 0.22/46.23 % (1652658)Success in time 45.018 s
% 0.22/46.23 % Vampire exiting
%------------------------------------------------------------------------------