%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYO595+1 : TPTP v9.3.1. Bugfixed v5.5.1.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n014.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 02:31:48 PM UTC 2026
% Result : Satisfiable 30.24s 4.91s
% Output : FiniteModel 30.24s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
tff('declare_$i1',type,
'fmb_$i_1': $i ).
tff('declare_$i2',type,
'fmb_$i_2': $i ).
tff('finite_domain_$i',axiom,
! [X: $i] :
( ( X = 'fmb_$i_1' )
| ( X = 'fmb_$i_2' ) ) ).
tff('distinct_domain_$i',axiom,
'fmb_$i_1' != 'fmb_$i_2' ).
tff(declare_true,type,
true: $i ).
tff(true_definition,axiom,
true = 'fmb_$i_1' ).
tff(declare_false,type,
false: $i ).
tff(false_definition,axiom,
false = 'fmb_$i_2' ).
tff(declare_p,type,
p: $i > $o ).
tff(predicate_p,axiom,
( p('fmb_$i_1')
& ~ p('fmb_$i_2') ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYO595+1 : TPTP v9.3.1. Bugfixed v5.5.1.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.19 % Computer : n014.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 17:51:46 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
% 14.06/2.33 % (1999034)Will run a generic schedule for satisfiability detection.
% 14.06/2.33 % (1999043)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2522003813:i=116_2998 on theBenchmark for (2998ds/116Mi)
% 14.06/2.33 % (1999040)% WARNING: option uhcvi not known.
% 14.06/2.33 % (1999039)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=175276565_2998 on theBenchmark for (2998ds/0Mi)
% 14.06/2.33 % (1999040)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3374254948:i=135531:add=off:rawr=on_2998 on theBenchmark for (2998ds/135531Mi)
% 14.06/2.33 % (1999041)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2906923321:i=88024:add=on:rawr=on_2998 on theBenchmark for (2998ds/88024Mi)
% 14.06/2.33 % (1999042)dis+10_1_sil=32000:sp=arity:random_seed=2605839191:i=103:fgj=on_2998 on theBenchmark for (2998ds/103Mi)
% 14.06/2.33 % (1999044)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2604765513:i=131_2998 on theBenchmark for (2998ds/131Mi)
% 14.06/2.33 % (1999045)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4057544454:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2998 on theBenchmark for (2998ds/159Mi)
% 14.06/2.33 % (1999043)Instruction limit reached!
% 14.06/2.33 % (1999043)------------------------------
% 14.06/2.33 % (1999043)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.06/2.33 % (1999043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.06/2.33 % (1999043)CaDiCaL version: 2.1.3
% 14.06/2.33 % (1999043)Termination reason: Instruction limit
% 14.06/2.33 % (1999043)Termination phase: Property scanning
% 14.06/2.33 % (1999043)Time elapsed: 0.030 s
% 14.06/2.33 % (1999043)Peak memory usage: 15 MB
% 14.06/2.33 % (1999043)Instructions burned: 117 (million)
% 14.06/2.33 % (1999053)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=529825890:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 14.06/2.33 % (1999042)Instruction limit reached!
% 14.06/2.33 % (1999042)------------------------------
% 14.06/2.33 % (1999042)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.06/2.33 % (1999042)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.06/2.33 % (1999042)CaDiCaL version: 2.1.3
% 14.06/2.33 % (1999042)Termination reason: Instruction limit
% 14.06/2.33 % (1999042)Termination phase: Property scanning
% 14.06/2.33 % (1999042)Time elapsed: 0.046 s
% 14.06/2.33 % (1999042)Peak memory usage: 14 MB
% 14.06/2.33 % (1999042)Instructions burned: 106 (million)
% 14.06/2.33 % (1999044)Instruction limit reached!
% 14.06/2.33 % (1999044)------------------------------
% 14.06/2.33 % (1999044)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.06/2.33 % (1999044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.06/2.33 % (1999044)CaDiCaL version: 2.1.3
% 14.06/2.33 % (1999044)Termination reason: Instruction limit
% 14.06/2.33 % (1999044)Termination phase: Saturation
% 14.06/2.33 % (1999044)Time elapsed: 0.057 s
% 14.06/2.33 % (1999044)Peak memory usage: 15 MB
% 14.06/2.33 % (1999044)Instructions burned: 133 (million)
% 14.06/2.33 % (1999055)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=476770161:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 14.06/2.33 % (1999045)Instruction limit reached!
% 14.06/2.33 % (1999045)------------------------------
% 14.06/2.33 % (1999045)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.06/2.33 % (1999045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.06/2.33 % (1999045)CaDiCaL version: 2.1.3
% 14.06/2.33 % (1999045)Termination reason: Instruction limit
% 14.06/2.33 % (1999045)Termination phase: Saturation
% 14.06/2.33 % (1999045)Time elapsed: 0.073 s
% 14.06/2.33 % (1999045)Peak memory usage: 17 MB
% 14.06/2.33 % (1999045)Instructions burned: 160 (million)
% 14.06/2.33 % (1999056)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=2879143900:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 14.06/2.33 % (1999058)ott-21_1_sil=16000:fs=off:random_seed=4020296262:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 14.06/2.33 % (1999055)Instruction limit reached!
% 14.06/2.33 % (1999055)------------------------------
% 14.06/2.33 % (1999055)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 14.06/2.33 % (1999055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.75/4.82 % (1999055)CaDiCaL version: 2.1.3
% 29.75/4.82 % (1999055)Termination reason: Instruction limit
% 29.75/4.82 % (1999055)Termination phase: Blocked clause elimination
% 29.75/4.82 % (1999055)Time elapsed: 0.056 s
% 29.75/4.82 % (1999055)Peak memory usage: 15 MB
% 29.75/4.82 % (1999055)Instructions burned: 132 (million)
% 29.75/4.82 % (1999061)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=184313763:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 29.75/4.82 % (1999058)Instruction limit reached!
% 29.75/4.82 % (1999058)------------------------------
% 29.75/4.82 % (1999058)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.75/4.82 % (1999058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.75/4.82 % (1999058)CaDiCaL version: 2.1.3
% 29.75/4.82 % (1999058)Termination reason: Instruction limit
% 29.75/4.82 % (1999058)Termination phase: Saturation
% 29.75/4.82 % (1999058)Time elapsed: 0.079 s
% 29.75/4.82 % (1999058)Peak memory usage: 16 MB
% 29.75/4.82 % (1999058)Instructions burned: 180 (million)
% 29.75/4.82 % (1999063)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3172242078:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 29.75/4.82 % (1999053)Instruction limit reached!
% 29.75/4.82 % (1999053)------------------------------
% 29.75/4.82 % (1999053)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.75/4.82 % (1999053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.75/4.82 % (1999053)CaDiCaL version: 2.1.3
% 29.75/4.82 % (1999053)Termination reason: Instruction limit
% 29.75/4.82 % (1999053)Termination phase: Finite model building preprocessing
% 29.75/4.82 % (1999053)Time elapsed: 0.166 s
% 29.75/4.82 % (1999053)Peak memory usage: 17 MB
% 29.75/4.82 % (1999053)Instructions burned: 722 (million)
% 29.75/4.82 % (1999065)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2083969060:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 29.75/4.82 % (1999061)Instruction limit reached!
% 29.75/4.82 % (1999061)------------------------------
% 29.75/4.82 % (1999061)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.75/4.82 % (1999061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.75/4.82 % (1999061)CaDiCaL version: 2.1.3
% 29.75/4.82 % (1999061)Termination reason: Instruction limit
% 29.75/4.82 % (1999061)Termination phase: Saturation
% 29.75/4.82 % (1999061)Time elapsed: 0.236 s
% 29.75/4.82 % (1999061)Peak memory usage: 19 MB
% 29.75/4.82 % (1999061)Instructions burned: 477 (million)
% 29.75/4.82 % (1999067)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2125305113:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 29.75/4.82 % (1999056)Instruction limit reached!
% 29.75/4.82 % (1999056)------------------------------
% 29.75/4.82 % (1999056)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.75/4.82 % (1999056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.75/4.82 % (1999056)CaDiCaL version: 2.1.3
% 29.75/4.82 % (1999056)Termination reason: Instruction limit
% 29.75/4.82 % (1999056)Termination phase: Saturation
% 29.75/4.82 % (1999056)Time elapsed: 0.368 s
% 29.75/4.82 % (1999056)Peak memory usage: 22 MB
% 29.75/4.82 % (1999056)Instructions burned: 684 (million)
% 29.75/4.82 % (1999069)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=3144738629:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 29.75/4.82 % (1999065)Instruction limit reached!
% 29.75/4.82 % (1999065)------------------------------
% 29.75/4.82 % (1999065)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.75/4.82 % (1999065)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.75/4.82 % (1999065)CaDiCaL version: 2.1.3
% 29.75/4.82 % (1999065)Termination reason: Instruction limit
% 29.75/4.82 % (1999065)Termination phase: Saturation
% 29.75/4.82 % (1999065)Time elapsed: 0.277 s
% 29.75/4.82 % (1999065)Peak memory usage: 21 MB
% 29.75/4.82 % (1999065)Instructions burned: 1184 (million)
% 29.75/4.82 % (1999071)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3085855744:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 29.75/4.82 % (1999063)Instruction limit reached!
% 29.75/4.82 % (1999063)------------------------------
% 29.75/4.82 % (1999063)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 29.75/4.82 % (1999063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.24/4.91 % (1999063)CaDiCaL version: 2.1.3
% 30.24/4.91 % (1999063)Termination reason: Instruction limit
% 30.24/4.91 % (1999063)Termination phase: Finite model building preprocessing
% 30.24/4.91 % (1999063)Time elapsed: 0.399 s
% 30.24/4.91 % (1999063)Peak memory usage: 17 MB
% 30.24/4.91 % (1999063)Instructions burned: 866 (million)
% 30.24/4.91 % (1999073)fmb+10_1_sil=64000:random_seed=1249407773:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi)
% 30.24/4.91 % (1999071)Instruction limit reached!
% 30.24/4.91 % (1999071)------------------------------
% 30.24/4.91 % (1999071)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.24/4.91 % (1999071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.24/4.91 % (1999071)CaDiCaL version: 2.1.3
% 30.24/4.91 % (1999071)Termination reason: Instruction limit
% 30.24/4.91 % (1999071)Termination phase: Saturation
% 30.24/4.91 % (1999071)Time elapsed: 0.255 s
% 30.24/4.91 % (1999071)Peak memory usage: 23 MB
% 30.24/4.91 % (1999071)Instructions burned: 881 (million)
% 30.24/4.91 % (1999075)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1928762215:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 30.24/4.91 % (1999067)Instruction limit reached!
% 30.24/4.91 % (1999067)------------------------------
% 30.24/4.91 % (1999067)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.24/4.91 % (1999067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.24/4.91 % (1999067)CaDiCaL version: 2.1.3
% 30.24/4.91 % (1999067)Termination reason: Instruction limit
% 30.24/4.91 % (1999067)Termination phase: Finite model building preprocessing
% 30.24/4.91 % (1999067)Time elapsed: 0.401 s
% 30.24/4.91 % (1999067)Peak memory usage: 17 MB
% 30.24/4.91 % (1999067)Instructions burned: 890 (million)
% 30.24/4.91 % (1999069)Instruction limit reached!
% 30.24/4.91 % (1999069)------------------------------
% 30.24/4.91 % (1999069)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.24/4.91 % (1999069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.24/4.91 % (1999069)CaDiCaL version: 2.1.3
% 30.24/4.91 % (1999069)Termination reason: Instruction limit
% 30.24/4.91 % (1999069)Termination phase: Saturation
% 30.24/4.91 % (1999069)Time elapsed: 0.337 s
% 30.24/4.91 % (1999069)Peak memory usage: 23 MB
% 30.24/4.91 % (1999069)Instructions burned: 694 (million)
% 30.24/4.91 % (1999077)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=224802005:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 30.24/4.91 % (1999078)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2684923204:i=5131_2990 on theBenchmark for (2990ds/5131Mi)
% 30.24/4.91 % TRYING [1]
% 30.24/4.91 % TRYING [2]
% 30.24/4.91 % (1999077)Instruction limit reached!
% 30.24/4.91 % (1999077)------------------------------
% 30.24/4.91 % (1999077)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.24/4.91 % (1999077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.24/4.91 % (1999077)CaDiCaL version: 2.1.3
% 30.24/4.91 % (1999077)Termination reason: Instruction limit
% 30.24/4.91 % (1999077)Termination phase: Finite model building preprocessing
% 30.24/4.91 % (1999077)Time elapsed: 0.420 s
% 30.24/4.91 % (1999077)Peak memory usage: 17 MB
% 30.24/4.91 % (1999077)Instructions burned: 921 (million)
% 30.24/4.91 % (1999081)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2680360061:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi)
% 30.24/4.91 % (1999075)Cannot represent all propositional literals internally
% 30.24/4.91 % (1999075)Refutation not found, incomplete strategy
% 30.24/4.91 % (1999075)------------------------------
% 30.24/4.91 % (1999075)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.24/4.91 % (1999075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.24/4.91 % (1999075)CaDiCaL version: 2.1.3
% 30.24/4.91 % (1999075)Termination reason: Refutation not found, incomplete strategy
% 30.24/4.91 % (1999075)Time elapsed: 0.581 s
% 30.24/4.91 % (1999075)Peak memory usage: 34 MB
% 30.24/4.91 % (1999075)Instructions burned: 2562 (million)
% 30.24/4.91 % (1999075)------------------------------
% 30.24/4.91 % (1999075)------------------------------
% 30.24/4.91 % (1999083)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3421517476:i=6324_2985 on theBenchmark for (2985ds/6324Mi)
% 30.24/4.91 % TRYING [1]
% 30.24/4.91 % (1999083)Cannot represent all propositional literals internally
% 30.24/4.91 % (1999083)Refutation not found, incomplete strategy
% 30.24/4.91 % (1999083)------------------------------
% 30.24/4.91 % (1999083)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.24/4.91 % (1999083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.24/4.91 % (1999083)CaDiCaL version: 2.1.3
% 30.24/4.91 % (1999083)Termination reason: Refutation not found, incomplete strategy
% 30.24/4.91 % (1999083)Time elapsed: 0.592 s
% 30.24/4.91 % (1999083)Peak memory usage: 35 MB
% 30.24/4.91 % (1999083)Instructions burned: 2598 (million)
% 30.24/4.91 % (1999083)------------------------------
% 30.24/4.91 % (1999083)------------------------------
% 30.24/4.91 % (1999085)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3557627376:fmbsr=2.30978:i=2174_2978 on theBenchmark for (2978ds/2174Mi)
% 30.24/4.91 % (1999081)Instruction limit reached!
% 30.24/4.91 % (1999081)------------------------------
% 30.24/4.91 % (1999081)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.24/4.91 % (1999081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.24/4.91 % (1999081)CaDiCaL version: 2.1.3
% 30.24/4.91 % (1999081)Termination reason: Instruction limit
% 30.24/4.91 % (1999081)Termination phase: Saturation
% 30.24/4.91 % (1999081)Time elapsed: 0.733 s
% 30.24/4.91 % (1999081)Peak memory usage: 29 MB
% 30.24/4.91 % (1999081)Instructions burned: 1473 (million)
% 30.24/4.91 % (1999087)ott-2_1_sil=16000:newcnf=on:random_seed=2394957757:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2978 on theBenchmark for (2978ds/869Mi)
% 30.24/4.91 % TRYING [2]
% 30.24/4.91 % (1999087)Instruction limit reached!
% 30.24/4.91 % (1999087)------------------------------
% 30.24/4.91 % (1999087)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.24/4.91 % (1999087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.24/4.91 % (1999087)CaDiCaL version: 2.1.3
% 30.24/4.91 % (1999087)Termination reason: Instruction limit
% 30.24/4.91 % (1999087)Termination phase: Saturation
% 30.24/4.91 % (1999087)Time elapsed: 0.408 s
% 30.24/4.91 % (1999087)Peak memory usage: 23 MB
% 30.24/4.91 % (1999087)Instructions burned: 870 (million)
% 30.24/4.91 % (1999089)ott+10_1_sil=32000:tgt=ground:random_seed=4072418789:i=5114:av=off_2974 on theBenchmark for (2974ds/5114Mi)
% 30.24/4.91 % (1999085)Instruction limit reached!
% 30.24/4.91 % (1999085)------------------------------
% 30.24/4.91 % (1999085)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.24/4.91 % (1999085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.24/4.91 % (1999085)CaDiCaL version: 2.1.3
% 30.24/4.91 % (1999085)Termination reason: Instruction limit
% 30.24/4.91 % (1999085)Termination phase: Finite model building preprocessing
% 30.24/4.91 % (1999085)Time elapsed: 0.503 s
% 30.24/4.91 % (1999085)Peak memory usage: 26 MB
% 30.24/4.91 % (1999085)Instructions burned: 2175 (million)
% 30.24/4.91 % (1999091)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=4029915769:i=54282_2973 on theBenchmark for (2973ds/54282Mi)
% 30.24/4.91 % TRYING [1]
% 30.24/4.91 % TRYING [2]
% 30.24/4.91 % (1999078)Instruction limit reached!
% 30.24/4.91 % (1999078)------------------------------
% 30.24/4.91 % (1999078)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.24/4.91 % (1999078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.24/4.91 % (1999078)CaDiCaL version: 2.1.3
% 30.24/4.91 % (1999078)Termination reason: Instruction limit
% 30.24/4.91 % (1999078)Termination phase: Saturation
% 30.24/4.91 % (1999078)Time elapsed: 2.306 s
% 30.24/4.91 % (1999078)Peak memory usage: 44 MB
% 30.24/4.91 % (1999078)Instructions burned: 5136 (million)
% 30.24/4.91 % (1999093)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1233266920:i=3512:aac=none_2967 on theBenchmark for (2967ds/3512Mi)
% 30.24/4.91 % Finite Model Found!
% 30.24/4.91 % SZS status Satisfiable for theBenchmark
% 30.24/4.91 % (1999089)Instruction limit reached!
% 30.24/4.91 % (1999089)------------------------------
% 30.24/4.91 % (1999089)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.24/4.91 % (1999089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.24/4.91 % (1999089)CaDiCaL version: 2.1.3
% 30.24/4.91 % (1999089)Termination reason: Instruction limit
% 30.24/4.91 % (1999089)Termination phase: Saturation
% 30.24/4.91 % (1999089)Time elapsed: 1.980 s
% 30.24/4.91 % (1999089)Peak memory usage: 25 MB
% 30.24/4.91 % (1999089)Instructions burned: 5116 (million)
% 30.24/4.91 % (1999039) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1999034-1999039"...
% 30.24/4.91 % (1999039)...printing done.
% 30.24/4.91 % (1999095)dis+21_1_sil=32000:sas=cadical:random_seed=3503490175:i=3773:amm=off_2954 on theBenchmark for (2954ds/3773Mi)
% 30.24/4.91 % SZS output start FiniteModel for theBenchmark
% See solution above
% 30.24/4.91 % (1999039)------------------------------
% 30.24/4.91 % (1999039)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 30.24/4.91 % (1999039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.24/4.91 % (1999039)CaDiCaL version: 2.1.3
% 30.24/4.91 % (1999039)Termination reason: Satisfiable
% 30.24/4.91 % (1999039)Time elapsed: 4.437 s
% 30.24/4.91 % (1999039)Peak memory usage: 434 MB
% 30.24/4.91 % (1999039)Instructions burned: 10715 (million)
% 30.24/4.91 % (1999034)Success in time 4.674 s
% 30.24/4.91 % Vampire exiting
%------------------------------------------------------------------------------