%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : TOP045+1 : TPTP v9.3.1. Released v3.4.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n008.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:34:29 PM UTC 2026 % Result : Timeout 300.44s 42.64s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : TOP045+1 : TPTP v9.3.1. Released v3.4.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.19 % Computer : n008.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 19:06:30 UTC 2026 % 0.09/0.19 % CPUTime : % 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.22 Running first-order model finding % 0.09/0.22 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 % 14.61/2.36 % (2534685)Will run a generic schedule for satisfiability detection. % 14.61/2.36 % (2534693)dis+10_1_sil=32000:sp=arity:random_seed=1383587934:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 14.61/2.36 % (2534691)% WARNING: option uhcvi not known. % 14.61/2.36 % (2534690)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=54179450_2999 on theBenchmark for (2999ds/0Mi) % 14.61/2.36 % (2534691)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3394562445:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 14.61/2.36 % (2534692)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1731235789:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 14.61/2.36 % (2534694)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2863638639:i=116_2999 on theBenchmark for (2999ds/116Mi) % 14.61/2.36 % (2534695)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=402166678:i=131_2999 on theBenchmark for (2999ds/131Mi) % 14.61/2.36 % (2534696)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=323322516:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 14.61/2.36 % TRYING [1] % 14.61/2.36 % TRYING [2] % 14.61/2.36 % (2534693)Instruction limit reached! % 14.61/2.36 % (2534693)------------------------------ % 14.61/2.36 % (2534693)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.61/2.36 % (2534693)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.61/2.36 % (2534693)CaDiCaL version: 2.1.3 % 14.61/2.36 % (2534693)Termination reason: Instruction limit % 14.61/2.36 % (2534693)Termination phase: Saturation % 14.61/2.36 % (2534693)Time elapsed: 0.037 s % 14.61/2.36 % (2534693)Peak memory usage: 13 MB % 14.61/2.36 % (2534693)Instructions burned: 103 (million) % 14.61/2.36 % TRYING [3] % 14.61/2.36 % (2534704)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3477168754:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 14.61/2.36 % TRYING [1] % 14.61/2.36 % TRYING [2] % 14.61/2.36 % TRYING [3] % 14.61/2.36 % (2534694)Instruction limit reached! % 14.61/2.36 % (2534694)------------------------------ % 14.61/2.36 % (2534694)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.61/2.36 % (2534694)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.61/2.36 % (2534694)CaDiCaL version: 2.1.3 % 14.61/2.36 % (2534694)Termination reason: Instruction limit % 14.61/2.36 % (2534694)Termination phase: Saturation % 14.61/2.36 % (2534694)Time elapsed: 0.069 s % 14.61/2.36 % (2534694)Peak memory usage: 13 MB % 14.61/2.36 % (2534694)Instructions burned: 117 (million) % 14.61/2.36 % (2534695)Instruction limit reached! % 14.61/2.36 % (2534695)------------------------------ % 14.61/2.36 % (2534695)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.61/2.36 % (2534695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.61/2.36 % (2534695)CaDiCaL version: 2.1.3 % 14.61/2.36 % (2534695)Termination reason: Instruction limit % 14.61/2.36 % (2534695)Termination phase: Saturation % 14.61/2.36 % (2534695)Time elapsed: 0.073 s % 14.61/2.36 % (2534695)Peak memory usage: 13 MB % 14.61/2.36 % (2534695)Instructions burned: 131 (million) % 14.61/2.36 % TRYING [4] % 14.61/2.36 % (2534706)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=4019783906:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 14.61/2.36 % (2534707)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=2500440120:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 14.61/2.36 % (2534696)Instruction limit reached! % 14.61/2.36 % (2534696)------------------------------ % 14.61/2.36 % (2534696)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.61/2.36 % (2534696)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.61/2.36 % (2534696)CaDiCaL version: 2.1.3 % 14.61/2.36 % (2534696)Termination reason: Instruction limit % 14.61/2.36 % (2534696)Termination phase: Saturation % 14.61/2.36 % (2534696)Time elapsed: 0.101 s % 14.61/2.36 % (2534696)Peak memory usage: 16 MB % 14.61/2.36 % (2534696)Instructions burned: 159 (million) % 14.61/2.36 % TRYING [4] % 14.61/2.36 % (2534710)ott-21_1_sil=16000:fs=off:random_seed=1291776212:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 14.61/2.36 % (2534706)Instruction limit reached! % 14.61/2.36 % (2534706)------------------------------ % 14.61/2.36 % (2534706)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 14.61/2.36 % (2534706)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.55/4.89 % (2534706)CaDiCaL version: 2.1.3 % 31.55/4.89 % (2534706)Termination reason: Instruction limit % 31.55/4.89 % (2534706)Termination phase: Saturation % 31.55/4.89 % (2534706)Time elapsed: 0.079 s % 31.55/4.89 % (2534706)Peak memory usage: 14 MB % 31.55/4.89 % (2534706)Instructions burned: 131 (million) % 31.55/4.89 % (2534704)Instruction limit reached! % 31.55/4.89 % (2534704)------------------------------ % 31.55/4.89 % (2534704)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.55/4.89 % (2534704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.55/4.89 % (2534704)CaDiCaL version: 2.1.3 % 31.55/4.89 % (2534704)Termination reason: Instruction limit % 31.55/4.89 % (2534704)Termination phase: Finite model building constraint generation % 31.55/4.89 % (2534704)Time elapsed: 0.128 s % 31.55/4.89 % (2534704)Peak memory usage: 25 MB % 31.55/4.89 % (2534704)Instructions burned: 714 (million) % 31.55/4.89 % (2534713)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=66922445:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 31.55/4.89 % (2534712)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3942673835:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi) % 31.55/4.89 % TRYING [1] % 31.55/4.89 % TRYING [2] % 31.55/4.89 % TRYING [3] % 31.55/4.89 % (2534710)Instruction limit reached! % 31.55/4.89 % (2534710)------------------------------ % 31.55/4.89 % (2534710)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.55/4.89 % (2534710)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.55/4.89 % (2534710)CaDiCaL version: 2.1.3 % 31.55/4.89 % (2534710)Termination reason: Instruction limit % 31.55/4.89 % (2534710)Termination phase: Saturation % 31.55/4.89 % (2534710)Time elapsed: 0.098 s % 31.55/4.89 % (2534710)Peak memory usage: 13 MB % 31.55/4.89 % (2534710)Instructions burned: 181 (million) % 31.55/4.89 % (2534716)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2964669111:i=1179_2997 on theBenchmark for (2997ds/1179Mi) % 31.55/4.89 % TRYING [4] % 31.55/4.89 % (2534713)Instruction limit reached! % 31.55/4.89 % (2534713)------------------------------ % 31.55/4.89 % (2534713)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.55/4.89 % (2534713)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.55/4.89 % (2534713)CaDiCaL version: 2.1.3 % 31.55/4.89 % (2534713)Termination reason: Instruction limit % 31.55/4.89 % (2534713)Termination phase: Finite model building constraint generation % 31.55/4.89 % (2534713)Time elapsed: 0.183 s % 31.55/4.89 % (2534713)Peak memory usage: 30 MB % 31.55/4.89 % (2534713)Instructions burned: 868 (million) % 31.55/4.89 % (2534718)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2733054555:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi) % 31.55/4.89 % TRYING [5] % 31.55/4.89 % (2534712)Instruction limit reached! % 31.55/4.89 % (2534712)------------------------------ % 31.55/4.89 % (2534712)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.55/4.89 % (2534712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.55/4.89 % (2534712)CaDiCaL version: 2.1.3 % 31.55/4.89 % (2534712)Termination reason: Instruction limit % 31.55/4.89 % (2534712)Termination phase: Saturation % 31.55/4.89 % (2534712)Time elapsed: 0.312 s % 31.55/4.89 % (2534712)Peak memory usage: 16 MB % 31.55/4.89 % (2534712)Instructions burned: 477 (million) % 31.55/4.89 % (2534720)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=3542002343: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) % 31.55/4.89 % (2534707)Instruction limit reached! % 31.55/4.89 % (2534707)------------------------------ % 31.55/4.89 % (2534707)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 31.55/4.89 % (2534707)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.55/4.89 % (2534707)CaDiCaL version: 2.1.3 % 31.55/4.89 % (2534707)Termination reason: Instruction limit % 31.55/4.89 % (2534707)Termination phase: Saturation % 31.55/4.89 % (2534707)Time elapsed: 0.431 s % 31.55/4.89 % (2534707)Peak memory usage: 20 MB % 31.55/4.89 % (2534707)Instructions burned: 684 (million) % 31.55/4.89 % (2534722)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2489173234:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi) % 31.55/4.89 % (2534718)Instruction limit reached! % 31.55/4.89 % (2534718)------------------------------ % 78.45/11.37 % (2534718)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 78.45/11.37 % (2534718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 78.45/11.37 % (2534718)CaDiCaL version: 2.1.3 % 78.45/11.37 % (2534718)Termination reason: Instruction limit % 78.45/11.37 % (2534718)Termination phase: Finite model building constraint generation % 78.45/11.37 % (2534718)Time elapsed: 0.238 s % 78.45/11.37 % (2534718)Peak memory usage: 111 MB % 78.45/11.37 % (2534718)Instructions burned: 892 (million) % 78.45/11.37 % (2534724)fmb+10_1_sil=64000:random_seed=3979424086:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi) % 78.45/11.37 % TRYING [1] % 78.45/11.37 % TRYING [2] % 78.45/11.37 % TRYING [3] % 78.45/11.37 % TRYING [4] % 78.45/11.37 % (2534720)Instruction limit reached! % 78.45/11.37 % (2534720)------------------------------ % 78.45/11.37 % (2534720)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 78.45/11.37 % (2534720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 78.45/11.37 % (2534720)CaDiCaL version: 2.1.3 % 78.45/11.37 % (2534720)Termination reason: Instruction limit % 78.45/11.37 % (2534720)Termination phase: Saturation % 78.45/11.37 % (2534720)Time elapsed: 0.411 s % 78.45/11.37 % (2534720)Peak memory usage: 25 MB % 78.45/11.37 % (2534720)Instructions burned: 693 (million) % 78.45/11.37 % (2534726)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1053758486:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi) % 78.45/11.37 % (2534716)Instruction limit reached! % 78.45/11.37 % (2534716)------------------------------ % 78.45/11.37 % (2534716)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 78.45/11.37 % (2534716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 78.45/11.37 % (2534716)CaDiCaL version: 2.1.3 % 78.45/11.37 % (2534716)Termination reason: Instruction limit % 78.45/11.37 % (2534716)Termination phase: Saturation % 78.45/11.37 % (2534716)Time elapsed: 0.727 s % 78.45/11.37 % (2534716)Peak memory usage: 27 MB % 78.45/11.37 % (2534716)Instructions burned: 1179 (million) % 78.45/11.37 % TRYING [20] % 78.45/11.37 % (2534728)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=4005982186:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi) % 78.45/11.37 % TRYING [8] % 78.45/11.37 % (2534722)Instruction limit reached! % 78.45/11.37 % (2534722)------------------------------ % 78.45/11.37 % (2534722)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 78.45/11.37 % (2534722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 78.45/11.37 % (2534722)CaDiCaL version: 2.1.3 % 78.45/11.37 % (2534722)Termination reason: Instruction limit % 78.45/11.37 % (2534722)Termination phase: Saturation % 78.45/11.37 % (2534722)Time elapsed: 0.483 s % 78.45/11.37 % (2534722)Peak memory usage: 20 MB % 78.45/11.37 % (2534722)Instructions burned: 879 (million) % 78.45/11.37 % (2534730)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=4132900527:i=5131_2989 on theBenchmark for (2989ds/5131Mi) % 78.45/11.37 % (2534728)Instruction limit reached! % 78.45/11.37 % (2534728)------------------------------ % 78.45/11.37 % (2534728)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 78.45/11.37 % (2534728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 78.45/11.37 % (2534728)CaDiCaL version: 2.1.3 % 78.45/11.37 % (2534728)Termination reason: Instruction limit % 78.45/11.37 % (2534728)Termination phase: Finite model building constraint generation % 78.45/11.37 % (2534728)Time elapsed: 0.304 s % 78.45/11.37 % (2534728)Peak memory usage: 47 MB % 78.45/11.37 % (2534728)Instructions burned: 920 (million) % 78.45/11.37 % (2534732)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=511035492:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi) % 78.45/11.37 % TRYING [6] % 78.45/11.37 % (2534732)Instruction limit reached! % 78.45/11.37 % (2534732)------------------------------ % 78.45/11.37 % (2534732)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 78.45/11.37 % (2534732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 78.45/11.37 % (2534732)CaDiCaL version: 2.1.3 % 78.45/11.37 % (2534732)Termination reason: Instruction limit % 78.45/11.37 % (2534732)Termination phase: Saturation % 78.45/11.37 % (2534732)Time elapsed: 0.717 s % 78.45/11.37 % (2534732)Peak memory usage: 27 MB % 78.45/11.37 % (2534732)Instructions burned: 1474 (million) % 78.45/11.37 % (2534734)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2173033704:i=6324_2979 on theBenchmark for (2979ds/6324Mi) % 78.45/11.37 % (2534734)Cannot represent all propositional literals internally % 78.45/11.37 % (2534734)Refutation not found, incomplete strategy % 202.58/28.83 % (2534734)------------------------------ % 202.58/28.83 % (2534734)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.58/28.83 % (2534734)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.58/28.83 % (2534734)CaDiCaL version: 2.1.3 % 202.58/28.83 % (2534734)Termination reason: Refutation not found, incomplete strategy % 202.58/28.83 % (2534734)Time elapsed: 0.023 s % 202.58/28.83 % (2534734)Peak memory usage: 11 MB % 202.58/28.83 % (2534734)Instructions burned: 47 (million) % 202.58/28.83 % (2534734)------------------------------ % 202.58/28.83 % (2534734)------------------------------ % 202.58/28.83 % (2534736)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1501958500:fmbsr=2.30978:i=2174_2978 on theBenchmark for (2978ds/2174Mi) % 202.58/28.83 % TRYING [16] % 202.58/28.83 % (2534736)Instruction limit reached! % 202.58/28.83 % (2534736)------------------------------ % 202.58/28.83 % (2534736)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.58/28.83 % (2534736)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.58/28.83 % (2534736)CaDiCaL version: 2.1.3 % 202.58/28.83 % (2534736)Termination reason: Instruction limit % 202.58/28.83 % (2534736)Termination phase: Finite model building constraint generation % 202.58/28.83 % (2534736)Time elapsed: 0.720 s % 202.58/28.83 % (2534736)Peak memory usage: 120 MB % 202.58/28.83 % (2534736)Instructions burned: 2176 (million) % 202.58/28.83 % (2534738)ott-2_1_sil=16000:newcnf=on:random_seed=2538849183:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2971 on theBenchmark for (2971ds/869Mi) % 202.58/28.83 % (2534738)Instruction limit reached! % 202.58/28.83 % (2534738)------------------------------ % 202.58/28.83 % (2534738)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.58/28.83 % (2534738)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.58/28.83 % (2534738)CaDiCaL version: 2.1.3 % 202.58/28.83 % (2534738)Termination reason: Instruction limit % 202.58/28.83 % (2534738)Termination phase: Saturation % 202.58/28.83 % (2534738)Time elapsed: 0.526 s % 202.58/28.83 % (2534738)Peak memory usage: 19 MB % 202.58/28.83 % (2534738)Instructions burned: 870 (million) % 202.58/28.83 % (2534740)ott+10_1_sil=32000:tgt=ground:random_seed=237260449:i=5114:av=off_2965 on theBenchmark for (2965ds/5114Mi) % 202.58/28.83 % (2534730)Instruction limit reached! % 202.58/28.83 % (2534730)------------------------------ % 202.58/28.83 % (2534730)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.58/28.83 % (2534730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.58/28.83 % (2534730)CaDiCaL version: 2.1.3 % 202.58/28.83 % (2534730)Termination reason: Instruction limit % 202.58/28.83 % (2534730)Termination phase: Saturation % 202.58/28.83 % (2534730)Time elapsed: 2.903 s % 202.58/28.83 % (2534730)Peak memory usage: 57 MB % 202.58/28.83 % (2534730)Instructions burned: 5132 (million) % 202.58/28.83 % (2534742)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=365655750:i=54282_2959 on theBenchmark for (2959ds/54282Mi) % 202.58/28.83 % TRYING [1] % 202.58/28.83 % TRYING [2] % 202.58/28.83 % TRYING [3] % 202.58/28.83 % TRYING [4] % 202.58/28.83 % (2534726)Instruction limit reached! % 202.58/28.83 % (2534726)------------------------------ % 202.58/28.83 % (2534726)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.58/28.83 % (2534726)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.58/28.83 % (2534726)CaDiCaL version: 2.1.3 % 202.58/28.83 % (2534726)Termination reason: Instruction limit % 202.58/28.83 % (2534726)Termination phase: Finite model building constraint generation % 202.58/28.83 % (2534726)Time elapsed: 3.246 s % 202.58/28.83 % (2534726)Peak memory usage: 570 MB % 202.58/28.83 % (2534726)Instructions burned: 9518 (million) % 202.58/28.83 % (2534744)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1490971620:i=3512:aac=none_2956 on theBenchmark for (2956ds/3512Mi) % 202.58/28.83 % TRYING [5] % 202.58/28.83 % (2534724)Instruction limit reached! % 202.58/28.83 % (2534724)------------------------------ % 202.58/28.83 % (2534724)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 202.58/28.83 % (2534724)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 202.58/28.83 % (2534724)CaDiCaL version: 2.1.3 % 202.58/28.83 % (2534724)Termination reason: Instruction limit % 202.58/28.83 % (2534724)Termination phase: Finite model building SAT solving % 202.58/28.83 % (2534724)Time elapsed: 3.957 s % 202.58/28.83 % (2534724)Peak memory usage: 104 MB % 202.58/28.83 % (2534724)Instructions burned: 22064 (million) % 202.58/28.83 % (2534747)dis+21_1_sil=32000:sas=cadical:random_seed=1915941901:i=3773:amm=off_2953 on theBenchmark for (2953ds/3773Mi) % 276.80/40.52 % TRYING [6] % 276.80/40.52 % (2534747)Instruction limit reached! % 276.80/40.52 % (2534747)------------------------------ % 276.80/40.52 % (2534747)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 276.80/40.52 % (2534747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.80/40.52 % (2534747)CaDiCaL version: 2.1.3 % 276.80/40.52 % (2534747)Termination reason: Instruction limit % 276.80/40.52 % (2534747)Termination phase: Saturation % 276.80/40.52 % (2534747)Time elapsed: 1.101 s % 276.80/40.52 % (2534747)Peak memory usage: 33 MB % 276.80/40.52 % (2534747)Instructions burned: 3776 (million) % 276.80/40.52 % (2534749)ott+11_1_sil=16000:gs=on:random_seed=3128988745:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2942 on theBenchmark for (2942ds/2251Mi) % 276.80/40.52 % (2534749)Instruction limit reached! % 276.80/40.52 % (2534749)------------------------------ % 276.80/40.52 % (2534749)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 276.80/40.52 % (2534749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.80/40.52 % (2534749)CaDiCaL version: 2.1.3 % 276.80/40.52 % (2534749)Termination reason: Instruction limit % 276.80/40.52 % (2534749)Termination phase: Saturation % 276.80/40.52 % (2534749)Time elapsed: 0.564 s % 276.80/40.52 % (2534749)Peak memory usage: 20 MB % 276.80/40.52 % (2534749)Instructions burned: 2252 (million) % 276.80/40.52 % (2534751)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2083689567:fmbsr=1.6:i=67534_2936 on theBenchmark for (2936ds/67534Mi) % 276.80/40.52 % (2534744)Instruction limit reached! % 276.80/40.52 % (2534744)------------------------------ % 276.80/40.52 % (2534744)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 276.80/40.52 % (2534744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.80/40.52 % (2534744)CaDiCaL version: 2.1.3 % 276.80/40.52 % (2534744)Termination reason: Instruction limit % 276.80/40.52 % (2534744)Termination phase: Saturation % 276.80/40.52 % (2534744)Time elapsed: 2.039 s % 276.80/40.52 % (2534744)Peak memory usage: 31 MB % 276.80/40.52 % (2534744)Instructions burned: 3513 (million) % 276.80/40.52 % (2534740)Instruction limit reached! % 276.80/40.52 % (2534740)------------------------------ % 276.80/40.52 % (2534740)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 276.80/40.52 % (2534740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.80/40.52 % (2534740)CaDiCaL version: 2.1.3 % 276.80/40.52 % (2534740)Termination reason: Instruction limit % 276.80/40.52 % (2534740)Termination phase: Saturation % 276.80/40.52 % (2534740)Time elapsed: 2.946 s % 276.80/40.52 % (2534740)Peak memory usage: 59 MB % 276.80/40.52 % (2534740)Instructions burned: 5114 (million) % 276.80/40.52 % (2534753)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=517296578:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2936 on theBenchmark for (2936ds/4591Mi) % 276.80/40.52 % TRYING [7] % 276.80/40.52 % (2534755)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2498036118:i=29340_2935 on theBenchmark for (2935ds/29340Mi) % 276.80/40.52 % (2534753)Instruction limit reached! % 276.80/40.52 % (2534753)------------------------------ % 276.80/40.52 % (2534753)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 276.80/40.52 % (2534753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.80/40.52 % (2534753)CaDiCaL version: 2.1.3 % 276.80/40.52 % (2534753)Termination reason: Instruction limit % 276.80/40.52 % (2534753)Termination phase: Saturation % 276.80/40.52 % (2534753)Time elapsed: 1.995 s % 276.80/40.52 % (2534753)Peak memory usage: 38 MB % 276.80/40.52 % (2534753)Instructions burned: 4591 (million) % 276.80/40.52 % (2534757)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2173226959:i=5211_2915 on theBenchmark for (2915ds/5211Mi) % 276.80/40.52 % TRYING [7] % 276.80/40.52 % (2534757)Instruction limit reached! % 276.80/40.52 % (2534757)------------------------------ % 276.80/40.52 % (2534757)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 276.80/40.52 % (2534757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 276.80/40.52 % (2534757)CaDiCaL version: 2.1.3 % 276.80/40.52 % (2534757)Termination reason: Instruction limit % 276.80/40.52 % (2534757)Termination phase: Saturation % 276.80/40.52 % (2534757)Time elapsed: 2.682 s % 276.80/40.52 % (2534757)Peak memory usage: 44 MB % 276.80/40.52 % (2534757)Instructions burned: 5213 (million) % 276.80/40.52 % (2534759)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2718749839:i=5Terminated % 300.44/42.64 % Vampire exiting %------------------------------------------------------------------------------