%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR051+5 : TPTP v9.3.1. Bugfixed v3.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/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:41 AM UTC 2026
% Result : Theorem 0.18s 27.18s
% Output : Refutation 0.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 4
% Syntax : Number of formulae : 22 ( 9 unt; 2 def)
% Number of atoms : 35 ( 0 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 25 ( 12 ~; 7 |; 1 &)
% ( 2 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 2 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 5 ( 4 usr; 3 prp; 0-1 aty)
% Number of functors : 2 ( 2 usr; 2 con; 0-0 aty)
% Number of variables : 4 ( 0 sgn 2 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f56259,axiom,
( mtvisible(c_tptp_member3356_mt)
=> marriagelicensedocument(c_tptpmarriagelicensedocument) ),
file('/export/starexec/sandbox2/benchmark/Axioms/CSR002+4.ax',ax4_56266) ).
fof(f540250,conjecture,
? [X0] :
( mtvisible(c_tptp_member3356_mt)
=> marriagelicensedocument(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',query251) ).
fof(f540251,negated_conjecture,
~ ? [X0] :
( mtvisible(c_tptp_member3356_mt)
=> marriagelicensedocument(X0) ),
inference(negated_conjecture,[status(cth)],[f540250]) ).
fof(f617850,plain,
( marriagelicensedocument(c_tptpmarriagelicensedocument)
| ~ mtvisible(c_tptp_member3356_mt) ),
inference(ennf_transformation,[],[f56259]) ).
fof(f936432,plain,
! [X0] :
( ~ marriagelicensedocument(X0)
& mtvisible(c_tptp_member3356_mt) ),
inference(ennf_transformation,[],[f540251]) ).
fof(f988376,plain,
( ~ mtvisible(c_tptp_member3356_mt)
| marriagelicensedocument(c_tptpmarriagelicensedocument) ),
inference(cnf_transformation,[],[f617850]) ).
fof(f1426738,plain,
mtvisible(c_tptp_member3356_mt),
inference(cnf_transformation,[],[f936432]) ).
fof(f1426739,plain,
! [X0] : ~ marriagelicensedocument(X0),
inference(cnf_transformation,[],[f936432]) ).
fof(f1465027,plain,
( mtvisible(c_tptp_member3356_mt)
| marriagelicensedocument(c_tptpmarriagelicensedocument) ),
inference(consistent_polarity_flipping,[],[f988376]) ).
fof(f1831172,plain,
~ mtvisible(c_tptp_member3356_mt),
inference(consistent_polarity_flipping,[],[f1426738]) ).
fof(f2036286,definition,
( spl0_41767
<=> marriagelicensedocument(c_tptpmarriagelicensedocument) ),
introduced(definition,[new_symbols(definition,[spl0_41767])],[avatar_definition]) ).
fof(f2036288,plain,
( marriagelicensedocument(c_tptpmarriagelicensedocument)
| ~ spl0_41767 ),
inference(avatar_component_clause,[],[f2036286]) ).
fof(f2036290,definition,
( spl0_41768
<=> mtvisible(c_tptp_member3356_mt) ),
introduced(definition,[new_symbols(definition,[spl0_41768])],[avatar_definition]) ).
fof(f2320487,plain,
( spl0_41767
| spl0_41768 ),
inference(avatar_split_clause,[],[f1465027,f2036290,f2036286]) ).
fof(f2423009,plain,
~ spl0_41768,
inference(avatar_split_clause,[],[f1831172,f2036290]) ).
fof(f2423020,plain,
( $false
| ~ spl0_41767 ),
inference(forward_subsumption_resolution,[],[f2036288,f1426739]) ).
fof(f2423021,plain,
~ spl0_41767,
inference(avatar_contradiction_clause,[],[f2423020]) ).
cnf(s96323,plain,
( spl0_41767
| spl0_41768 ),
inference(sat_conversion,[],[f2320487]) ).
cnf(s116912,plain,
~ spl0_41768,
inference(sat_conversion,[],[f2423009]) ).
cnf(s116923,plain,
~ spl0_41767,
inference(sat_conversion,[],[f2423021]) ).
cnf(s116924,plain,
$false,
inference(rat,[],[s96323,s116912,s116923]) ).
fof(f2423022,plain,
$false,
inference(avatar_sat_refutation,[],[s116924]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR051+5 : TPTP v9.3.1. Bugfixed v3.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.19 % Computer : n013.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 22:17:36 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.22 Running first-order model finding
% 0.09/0.22 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
% 57.74/18.29 % (1647745)Will run a generic schedule for satisfiability detection.
% 57.74/18.29 % (1647751)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=438892778_2885 on theBenchmark for (2885ds/0Mi)
% 57.74/18.29 % (1647753)% WARNING: option uhcvi not known.
% 57.74/18.29 % (1647753)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3653067768:i=135531:add=off:rawr=on_2885 on theBenchmark for (2885ds/135531Mi)
% 57.74/18.29 % (1647755)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3588590281:i=88024:add=on:rawr=on_2885 on theBenchmark for (2885ds/88024Mi)
% 57.74/18.29 % (1647757)dis+10_1_sil=32000:sp=arity:random_seed=2263955163:i=103:fgj=on_2885 on theBenchmark for (2885ds/103Mi)
% 57.74/18.29 % (1647759)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1905729728:i=116_2885 on theBenchmark for (2885ds/116Mi)
% 57.74/18.29 % (1647761)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3452456279:i=131_2885 on theBenchmark for (2885ds/131Mi)
% 57.74/18.29 % (1647763)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2035617066:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2885 on theBenchmark for (2885ds/159Mi)
% 57.74/18.29 % (1647757)Instruction limit reached!
% 57.74/18.29 % (1647757)------------------------------
% 57.74/18.29 % (1647757)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.74/18.29 % (1647757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.74/18.29 % (1647757)CaDiCaL version: 2.1.3
% 57.74/18.29 % (1647757)Termination reason: Instruction limit
% 57.74/18.29 % (1647757)Termination phase: Preprocessing 1
% 57.74/18.29 % (1647757)Time elapsed: 0.083 s
% 57.74/18.29 % (1647757)Peak memory usage: 639 MB
% 57.74/18.29 % (1647757)Instructions burned: 103 (million)
% 57.74/18.29 % (1647761)Instruction limit reached!
% 57.74/18.29 % (1647761)------------------------------
% 57.74/18.29 % (1647761)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.74/18.29 % (1647761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.74/18.29 % (1647761)CaDiCaL version: 2.1.3
% 57.74/18.29 % (1647761)Termination reason: Instruction limit
% 57.74/18.29 % (1647761)Termination phase: Preprocessing 1
% 57.74/18.29 % (1647761)Time elapsed: 0.063 s
% 57.74/18.29 % (1647761)Peak memory usage: 639 MB
% 57.74/18.29 % (1647761)Instructions burned: 133 (million)
% 57.74/18.29 % (1647759)Instruction limit reached!
% 57.74/18.29 % (1647759)------------------------------
% 57.74/18.29 % (1647759)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.74/18.29 % (1647759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.74/18.29 % (1647759)CaDiCaL version: 2.1.3
% 57.74/18.29 % (1647759)Termination reason: Instruction limit
% 57.74/18.29 % (1647759)Termination phase: Preprocessing 1
% 57.74/18.29 % (1647759)Time elapsed: 0.106 s
% 57.74/18.29 % (1647759)Peak memory usage: 639 MB
% 57.74/18.29 % (1647759)Instructions burned: 116 (million)
% 57.74/18.29 % (1647765)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3283409778:i=714:nm=2_2883 on theBenchmark for (2883ds/714Mi)
% 57.74/18.29 % (1647763)Instruction limit reached!
% 57.74/18.29 % (1647763)------------------------------
% 57.74/18.29 % (1647763)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.74/18.29 % (1647763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 57.74/18.29 % (1647763)CaDiCaL version: 2.1.3
% 57.74/18.29 % (1647763)Termination reason: Instruction limit
% 57.74/18.29 % (1647763)Termination phase: Preprocessing 1
% 57.74/18.29 % (1647763)Time elapsed: 0.128 s
% 57.74/18.29 % (1647763)Peak memory usage: 640 MB
% 57.74/18.29 % (1647763)Instructions burned: 159 (million)
% 57.74/18.29 % (1647767)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4179105831:i=131:bd=preordered:fsd=on_2883 on theBenchmark for (2883ds/131Mi)
% 57.74/18.29 % (1647769)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=1197240471:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2883 on theBenchmark for (2883ds/684Mi)
% 57.74/18.29 % (1647771)ott-21_1_sil=16000:fs=off:random_seed=753884240:i=180:av=off:fsr=off_2882 on theBenchmark for (2882ds/180Mi)
% 57.74/18.29 % (1647767)Instruction limit reached!
% 57.74/18.29 % (1647767)------------------------------
% 57.74/18.29 % (1647767)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 57.74/18.29 % (1647767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.43/23.53 % (1647767)CaDiCaL version: 2.1.3
% 95.43/23.53 % (1647767)Termination reason: Instruction limit
% 95.43/23.53 % (1647767)Termination phase: Preprocessing 1
% 95.43/23.53 % (1647767)Time elapsed: 0.106 s
% 95.43/23.53 % (1647767)Peak memory usage: 639 MB
% 95.43/23.53 % (1647767)Instructions burned: 131 (million)
% 95.43/23.53 % (1647773)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1016927028:i=477:bd=all_2881 on theBenchmark for (2881ds/477Mi)
% 95.43/23.53 % (1647771)Instruction limit reached!
% 95.43/23.53 % (1647771)------------------------------
% 95.43/23.53 % (1647771)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.43/23.53 % (1647771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.43/23.53 % (1647771)CaDiCaL version: 2.1.3
% 95.43/23.53 % (1647771)Termination reason: Instruction limit
% 95.43/23.53 % (1647771)Termination phase: Preprocessing 1
% 95.43/23.53 % (1647771)Time elapsed: 0.149 s
% 95.43/23.53 % (1647771)Peak memory usage: 639 MB
% 95.43/23.53 % (1647771)Instructions burned: 181 (million)
% 95.43/23.53 % (1647775)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=194675289:fmbsr=1.3:i=865:ins=25_2880 on theBenchmark for (2880ds/865Mi)
% 95.43/23.53 % (1647769)Instruction limit reached!
% 95.43/23.53 % (1647769)------------------------------
% 95.43/23.53 % (1647769)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.43/23.53 % (1647769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.43/23.53 % (1647769)CaDiCaL version: 2.1.3
% 95.43/23.53 % (1647769)Termination reason: Instruction limit
% 95.43/23.53 % (1647769)Termination phase: SInE selection
% 95.43/23.53 % (1647769)Time elapsed: 0.281 s
% 95.43/23.53 % (1647769)Peak memory usage: 642 MB
% 95.43/23.53 % (1647769)Instructions burned: 684 (million)
% 95.43/23.53 % (1647777)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2359679319:i=1179_2879 on theBenchmark for (2879ds/1179Mi)
% 95.43/23.53 % (1647765)Instruction limit reached!
% 95.43/23.53 % (1647765)------------------------------
% 95.43/23.53 % (1647765)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.43/23.53 % (1647765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.43/23.53 % (1647765)CaDiCaL version: 2.1.3
% 95.43/23.53 % (1647765)Termination reason: Instruction limit
% 95.43/23.53 % (1647765)Termination phase: Preprocessing 1
% 95.43/23.53 % (1647765)Time elapsed: 0.519 s
% 95.43/23.53 % (1647765)Peak memory usage: 639 MB
% 95.43/23.53 % (1647765)Instructions burned: 715 (million)
% 95.43/23.53 % (1647773)Instruction limit reached!
% 95.43/23.53 % (1647773)------------------------------
% 95.43/23.53 % (1647773)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.43/23.53 % (1647773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.43/23.53 % (1647773)CaDiCaL version: 2.1.3
% 95.43/23.53 % (1647773)Termination reason: Instruction limit
% 95.43/23.53 % (1647773)Termination phase: Preprocessing 1
% 95.43/23.53 % (1647773)Time elapsed: 0.374 s
% 95.43/23.53 % (1647773)Peak memory usage: 639 MB
% 95.43/23.53 % (1647773)Instructions burned: 479 (million)
% 95.43/23.53 % (1647779)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=288978119:i=889:ins=1_2877 on theBenchmark for (2877ds/889Mi)
% 95.43/23.53 % (1647781)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=1036221754:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2876 on theBenchmark for (2876ds/692Mi)
% 95.43/23.53 % (1647775)Instruction limit reached!
% 95.43/23.53 % (1647775)------------------------------
% 95.43/23.53 % (1647775)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.43/23.53 % (1647775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.43/23.53 % (1647775)CaDiCaL version: 2.1.3
% 95.43/23.53 % (1647775)Termination reason: Instruction limit
% 95.43/23.53 % (1647775)Termination phase: Preprocessing 1
% 95.43/23.53 % (1647775)Time elapsed: 0.613 s
% 95.43/23.53 % (1647775)Peak memory usage: 640 MB
% 95.43/23.53 % (1647775)Instructions burned: 865 (million)
% 95.43/23.53 % (1647777)Instruction limit reached!
% 95.43/23.53 % (1647777)------------------------------
% 95.43/23.53 % (1647777)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 95.43/23.53 % (1647777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.43/23.53 % (1647777)CaDiCaL version: 2.1.3
% 95.43/23.53 % (1647777)Termination reason: Instruction limit
% 95.43/23.53 % (1647777)Termination phase: Unused predicate definition removal
% 72.91/26.01 % (1647777)Time elapsed: 0.641 s
% 72.91/26.01 % (1647777)Peak memory usage: 718 MB
% 72.91/26.01 % (1647777)Instructions burned: 1179 (million)
% 72.91/26.01 % (1647783)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3227146514:i=879:kws=inv_precedence:fsr=off_2873 on theBenchmark for (2873ds/879Mi)
% 72.91/26.01 % (1647785)fmb+10_1_sil=64000:random_seed=3005369:i=22061:nm=2:gsp=on_2872 on theBenchmark for (2872ds/22061Mi)
% 72.91/26.01 % (1647781)Instruction limit reached!
% 72.91/26.01 % (1647781)------------------------------
% 72.91/26.01 % (1647781)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 72.91/26.01 % (1647781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.91/26.01 % (1647781)CaDiCaL version: 2.1.3
% 72.91/26.01 % (1647781)Termination reason: Instruction limit
% 72.91/26.01 % (1647781)Termination phase: SInE selection
% 72.91/26.01 % (1647781)Time elapsed: 0.483 s
% 72.91/26.01 % (1647781)Peak memory usage: 642 MB
% 72.91/26.01 % (1647781)Instructions burned: 692 (million)
% 72.91/26.01 % (1647779)Instruction limit reached!
% 72.91/26.01 % (1647779)------------------------------
% 72.91/26.01 % (1647779)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 72.91/26.01 % (1647779)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.91/26.01 % (1647779)CaDiCaL version: 2.1.3
% 72.91/26.01 % (1647779)Termination reason: Instruction limit
% 72.91/26.01 % (1647779)Termination phase: Preprocessing 1
% 72.91/26.01 % (1647779)Time elapsed: 0.624 s
% 72.91/26.01 % (1647779)Peak memory usage: 639 MB
% 72.91/26.01 % (1647779)Instructions burned: 890 (million)
% 72.91/26.01 % (1647787)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1618904102:i=9515:nm=5_2871 on theBenchmark for (2871ds/9515Mi)
% 72.91/26.01 % (1647789)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=4197084861:fmbsr=1.7:i=920_2870 on theBenchmark for (2870ds/920Mi)
% 72.91/26.01 % (1647783)Instruction limit reached!
% 72.91/26.01 % (1647783)------------------------------
% 72.91/26.01 % (1647783)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 72.91/26.01 % (1647783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.91/26.01 % (1647783)CaDiCaL version: 2.1.3
% 72.91/26.01 % (1647783)Termination reason: Instruction limit
% 72.91/26.01 % (1647783)Termination phase: Unused predicate definition removal
% 72.91/26.01 % (1647783)Time elapsed: 0.808 s
% 72.91/26.01 % (1647783)Peak memory usage: 704 MB
% 72.91/26.01 % (1647783)Instructions burned: 879 (million)
% 72.91/26.01 % (1647791)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1751505233:i=5131_2864 on theBenchmark for (2864ds/5131Mi)
% 72.91/26.01 % (1647789)Instruction limit reached!
% 72.91/26.01 % (1647789)------------------------------
% 72.91/26.01 % (1647789)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 72.91/26.01 % (1647789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.91/26.01 % (1647789)CaDiCaL version: 2.1.3
% 72.91/26.01 % (1647789)Termination reason: Instruction limit
% 72.91/26.01 % (1647789)Termination phase: Preprocessing 1
% 72.91/26.01 % (1647789)Time elapsed: 0.721 s
% 72.91/26.01 % (1647789)Peak memory usage: 640 MB
% 72.91/26.01 % (1647789)Instructions burned: 920 (million)
% 72.91/26.01 % (1647793)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1182490508:i=1472:ins=7:fdi=8:gsp=on_2862 on theBenchmark for (2862ds/1472Mi)
% 72.91/26.01 % (1647793)Instruction limit reached!
% 72.91/26.01 % (1647793)------------------------------
% 72.91/26.01 % (1647793)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 72.91/26.01 % (1647793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.91/26.01 % (1647793)CaDiCaL version: 2.1.3
% 72.91/26.01 % (1647793)Termination reason: Instruction limit
% 72.91/26.01 % (1647793)Termination phase: Preprocessing 2
% 72.91/26.01 % (1647793)Time elapsed: 1.477 s
% 72.91/26.01 % (1647793)Peak memory usage: 724 MB
% 72.91/26.01 % (1647793)Instructions burned: 1473 (million)
% 72.91/26.01 % (1647795)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3763505773:i=6324_2846 on theBenchmark for (2846ds/6324Mi)
% 72.91/26.01 % (1647791)Instruction limit reached!
% 72.91/26.01 % (1647791)------------------------------
% 72.91/26.01 % (1647791)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 72.91/26.01 % (1647791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.91/26.01 % (1647791)CaDiCaL version: 2.1.3
% 72.91/26.01 % (1647791)Termination reason: Instruction limit
% 0.18/27.18 % (1647791)Termination phase: Property scanning
% 0.18/27.18 % (1647791)Time elapsed: 4.433 s
% 0.18/27.18 % (1647791)Peak memory usage: 880 MB
% 0.18/27.18 % (1647791)Instructions burned: 5131 (million)
% 0.18/27.18 % (1647797)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2916807201:fmbsr=2.30978:i=2174_2818 on theBenchmark for (2818ds/2174Mi)
% 0.18/27.18 % (1647795)Instruction limit reached!
% 0.18/27.18 % (1647795)------------------------------
% 0.18/27.18 % (1647795)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/27.18 % (1647795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/27.18 % (1647795)CaDiCaL version: 2.1.3
% 0.18/27.18 % (1647795)Termination reason: Instruction limit
% 0.18/27.18 % (1647795)Termination phase: Property scanning
% 0.18/27.18 % (1647795)Time elapsed: 4.491 s
% 0.18/27.18 % (1647795)Peak memory usage: 795 MB
% 0.18/27.18 % (1647795)Instructions burned: 6325 (million)
% 0.18/27.18 % (1647799)ott-2_1_sil=16000:newcnf=on:random_seed=3987394387:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2800 on theBenchmark for (2800ds/869Mi)
% 0.18/27.18 % (1647797)Instruction limit reached!
% 0.18/27.18 % (1647797)------------------------------
% 0.18/27.18 % (1647797)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/27.18 % (1647797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/27.18 % (1647797)CaDiCaL version: 2.1.3
% 0.18/27.18 % (1647797)Termination reason: Instruction limit
% 0.18/27.18 % (1647797)Termination phase: Naming
% 0.18/27.18 % (1647797)Time elapsed: 1.864 s
% 0.18/27.18 % (1647797)Peak memory usage: 745 MB
% 0.18/27.18 % (1647797)Instructions burned: 2175 (million)
% 0.18/27.18 % (1647787)Instruction limit reached!
% 0.18/27.18 % (1647787)------------------------------
% 0.18/27.18 % (1647787)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/27.18 % (1647787)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/27.18 % (1647787)CaDiCaL version: 2.1.3
% 0.18/27.18 % (1647787)Termination reason: Instruction limit
% 0.18/27.18 % (1647787)Termination phase: Finite model building preprocessing
% 0.18/27.18 % (1647787)Time elapsed: 7.259 s
% 0.18/27.18 % (1647787)Peak memory usage: 864 MB
% 0.18/27.18 % (1647787)Instructions burned: 9516 (million)
% 0.18/27.18 % (1647801)ott+10_1_sil=32000:tgt=ground:random_seed=3434370593:i=5114:av=off_2798 on theBenchmark for (2798ds/5114Mi)
% 0.18/27.18 % (1647803)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=40002491:i=54282_2796 on theBenchmark for (2796ds/54282Mi)
% 0.18/27.18 % (1647799)Instruction limit reached!
% 0.18/27.18 % (1647799)------------------------------
% 0.18/27.18 % (1647799)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/27.18 % (1647799)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/27.18 % (1647799)CaDiCaL version: 2.1.3
% 0.18/27.18 % (1647799)Termination reason: Instruction limit
% 0.18/27.18 % (1647799)Termination phase: Unused predicate definition removal
% 0.18/27.18 % (1647799)Time elapsed: 0.787 s
% 0.18/27.18 % (1647799)Peak memory usage: 702 MB
% 0.18/27.18 % (1647799)Instructions burned: 869 (million)
% 0.18/27.18 % (1647805)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2237336325:i=3512:aac=none_2791 on theBenchmark for (2791ds/3512Mi)
% 0.18/27.18 % (1647785)Instruction limit reached!
% 0.18/27.18 % (1647785)------------------------------
% 0.18/27.18 % (1647785)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/27.18 % (1647785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/27.18 % (1647785)CaDiCaL version: 2.1.3
% 0.18/27.18 % (1647785)Termination reason: Instruction limit
% 0.18/27.18 % (1647785)Termination phase: Finite model building preprocessing
% 0.18/27.18 % (1647785)Time elapsed: 8.642 s
% 0.18/27.18 % (1647785)Peak memory usage: 1171 MB
% 0.18/27.18 % (1647785)Instructions burned: 22063 (million)
% 0.18/27.18 % (1647807)dis+21_1_sil=32000:sas=cadical:random_seed=1351740450:i=3773:amm=off_2784 on theBenchmark for (2784ds/3773Mi)
% 0.18/27.18 % (1647807)Instruction limit reached!
% 0.18/27.18 % (1647807)------------------------------
% 0.18/27.18 % (1647807)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/27.18 % (1647807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/27.18 % (1647807)CaDiCaL version: 2.1.3
% 0.18/27.18 % (1647807)Termination reason: Instruction limit
% 0.18/27.18 % (1647807)Termination phase: Preprocessing 3
% 0.18/27.18 % (1647807)Time elapsed: 1.742 s
% 0.18/27.18 % (1647807)Peak memory usage: 745 MB
% 0.18/27.18 % (1647807)Instructions burned: 3776 (million)
% 0.18/27.18 % (1647809)ott+11_1_sil=16000:gs=on:random_seed=3005488243:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2766 on theBenchmark for (2766ds/2251Mi)
% 0.18/27.18 % (1647805)Instruction limit reached!
% 0.18/27.18 % (1647805)------------------------------
% 0.18/27.18 % (1647805)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/27.18 % (1647805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/27.18 % (1647805)CaDiCaL version: 2.1.3
% 0.18/27.18 % (1647805)Termination reason: Instruction limit
% 0.18/27.18 % (1647805)Termination phase: Preprocessing 3
% 0.18/27.18 % (1647805)Time elapsed: 2.468 s
% 0.18/27.18 % (1647805)Peak memory usage: 745 MB
% 0.18/27.18 % (1647805)Instructions burned: 3512 (million)
% 0.18/27.18 % (1647811)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1669275100:fmbsr=1.6:i=67534_2765 on theBenchmark for (2765ds/67534Mi)
% 0.18/27.18 % (1647801)Instruction limit reached!
% 0.18/27.18 % (1647801)------------------------------
% 0.18/27.18 % (1647801)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/27.18 % (1647801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/27.18 % (1647801)CaDiCaL version: 2.1.3
% 0.18/27.18 % (1647801)Termination reason: Instruction limit
% 0.18/27.18 % (1647801)Termination phase: Property scanning
% 0.18/27.18 % (1647801)Time elapsed: 3.708 s
% 0.18/27.18 % (1647801)Peak memory usage: 795 MB
% 0.18/27.18 % (1647801)Instructions burned: 5114 (million)
% 0.18/27.18 % (1647813)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2201610220:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2760 on theBenchmark for (2760ds/4591Mi)
% 0.18/27.18 % (1647809)Instruction limit reached!
% 0.18/27.18 % (1647809)------------------------------
% 0.18/27.18 % (1647809)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/27.18 % (1647809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/27.18 % (1647809)CaDiCaL version: 2.1.3
% 0.18/27.18 % (1647809)Termination reason: Instruction limit
% 0.18/27.18 % (1647809)Termination phase: SInE selection
% 0.18/27.18 % (1647809)Time elapsed: 0.829 s
% 0.18/27.18 % (1647809)Peak memory usage: 660 MB
% 0.18/27.18 % (1647809)Instructions burned: 2254 (million)
% 0.18/27.18 % (1647815)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2339299339:i=29340_2757 on theBenchmark for (2757ds/29340Mi)
% 0.18/27.18 % (1647753) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1647745-1647753"...
% 0.18/27.18 % (1647753)...printing done.
% 0.18/27.18 % (1647753)Refutation found. Thanks to Tanya!
% 0.18/27.18 % SZS status Theorem for theBenchmark
% 0.18/27.18 % SZS output start Proof for theBenchmark
% See solution above
% 0.18/27.18 % (1647753)------------------------------
% 0.18/27.18 % (1647753)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.18/27.18 % (1647753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/27.18 % (1647753)CaDiCaL version: 2.1.3
% 0.18/27.18 % (1647753)Termination reason: Refutation
% 0.18/27.18 % (1647753)Time elapsed: 12.947 s
% 0.18/27.18 % (1647753)Peak memory usage: 1294 MB
% 0.18/27.18 % (1647753)Instructions burned: 16436 (million)
% 0.18/27.18 % (1647745)Success in time 25.78 s
% 0.18/27.18 % Vampire exiting
%------------------------------------------------------------------------------