%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWW366+1 : TPTP v9.3.1. Released v5.2.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n001.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 01:39:53 PM UTC 2026 % Result : Timeout 300.15s 42.93s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWW366+1 : TPTP v9.3.1. Released v5.2.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.10/0.21 % Computer : n001.cluster.edu % 0.10/0.21 % Model : x86_64 x86_64 % 0.10/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.21 % Memory : 8046.5625MB % 0.10/0.21 % OS : Linux 6.8.0-71-generic % 0.10/0.21 % CPULimit : 300 % 0.10/0.21 % WCLimit : 300 % 0.10/0.21 % DateTime : Mon Sep 28 13:48:18 UTC 2026 % 0.10/0.21 % CPUTime : % 0.10/0.21 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.10/0.24 Running first-order model finding % 0.10/0.25 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 % 29.36/4.71 % (356988)Will run a generic schedule for satisfiability detection. % 29.36/4.71 % (356994)% WARNING: option uhcvi not known. % 29.36/4.71 % (356994)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2335393395:i=135531:add=off:rawr=on_2996 on theBenchmark for (2996ds/135531Mi) % 29.36/4.71 % (356993)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3939777652_2996 on theBenchmark for (2996ds/0Mi) % 29.36/4.71 % (356995)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1041426939:i=88024:add=on:rawr=on_2996 on theBenchmark for (2996ds/88024Mi) % 29.36/4.71 % (356996)dis+10_1_sil=32000:sp=arity:random_seed=1433535517:i=103:fgj=on_2996 on theBenchmark for (2996ds/103Mi) % 29.36/4.71 % (356997)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=876528190:i=116_2996 on theBenchmark for (2996ds/116Mi) % 29.36/4.71 % (356998)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2243469273:i=131_2996 on theBenchmark for (2996ds/131Mi) % 29.36/4.71 % (356999)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1785000838:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2996 on theBenchmark for (2996ds/159Mi) % 29.36/4.71 % (356996)Instruction limit reached! % 29.36/4.71 % (356996)------------------------------ % 29.36/4.71 % (356996)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.36/4.71 % (356996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.36/4.71 % (356996)CaDiCaL version: 2.1.3 % 29.36/4.71 % (356996)Termination reason: Instruction limit % 29.36/4.71 % (356996)Termination phase: Preprocessing 3 % 29.36/4.71 % (356996)Time elapsed: 0.066 s % 29.36/4.71 % (356996)Peak memory usage: 20 MB % 29.36/4.71 % (356996)Instructions burned: 104 (million) % 29.36/4.71 % (356997)Instruction limit reached! % 29.36/4.71 % (356997)------------------------------ % 29.36/4.71 % (356997)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.36/4.71 % (356997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.36/4.71 % (356997)CaDiCaL version: 2.1.3 % 29.36/4.71 % (356997)Termination reason: Instruction limit % 29.36/4.71 % (356997)Termination phase: NewCNF % 29.36/4.71 % (356997)Time elapsed: 0.077 s % 29.36/4.71 % (356997)Peak memory usage: 21 MB % 29.36/4.71 % (356997)Instructions burned: 116 (million) % 29.36/4.71 % (357007)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=60115892:i=714:nm=2_2995 on theBenchmark for (2995ds/714Mi) % 29.36/4.71 % (356998)Instruction limit reached! % 29.36/4.71 % (356998)------------------------------ % 29.36/4.71 % (356998)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.36/4.71 % (356998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.36/4.71 % (356998)CaDiCaL version: 2.1.3 % 29.36/4.71 % (356998)Termination reason: Instruction limit % 29.36/4.71 % (356998)Termination phase: Preprocessing 3 % 29.36/4.71 % (356998)Time elapsed: 0.089 s % 29.36/4.71 % (356998)Peak memory usage: 20 MB % 29.36/4.71 % (356998)Instructions burned: 131 (million) % 29.36/4.71 % (356999)Instruction limit reached! % 29.36/4.71 % (356999)------------------------------ % 29.36/4.71 % (356999)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.36/4.71 % (356999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.36/4.71 % (356999)CaDiCaL version: 2.1.3 % 29.36/4.71 % (356999)Termination reason: Instruction limit % 29.36/4.71 % (356999)Termination phase: Clausification % 29.36/4.71 % (356999)Time elapsed: 0.097 s % 29.36/4.71 % (356999)Peak memory usage: 21 MB % 29.36/4.71 % (356999)Instructions burned: 160 (million) % 29.36/4.71 % (357008)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3713537422:i=131:bd=preordered:fsd=on_2995 on theBenchmark for (2995ds/131Mi) % 29.36/4.71 % (357010)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=1066919865:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2995 on theBenchmark for (2995ds/684Mi) % 29.36/4.71 % (357012)ott-21_1_sil=16000:fs=off:random_seed=2233964165:i=180:av=off:fsr=off_2995 on theBenchmark for (2995ds/180Mi) % 29.36/4.71 % (357008)Instruction limit reached! % 29.36/4.71 % (357008)------------------------------ % 29.36/4.71 % (357008)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 29.36/4.71 % (357008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 29.36/4.71 % (357008)CaDiCaL version: 2.1.3 % 29.36/4.71 % (357008)Termination reason: Instruction limit % 69.80/10.41 % (357008)Termination phase: Preprocessing 3 % 69.80/10.41 % (357008)Time elapsed: 0.079 s % 69.80/10.41 % (357008)Peak memory usage: 20 MB % 69.80/10.41 % (357008)Instructions burned: 132 (million) % 69.80/10.41 % (357015)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2960847790:i=477:bd=all_2994 on theBenchmark for (2994ds/477Mi) % 69.80/10.41 % (357012)Instruction limit reached! % 69.80/10.41 % (357012)------------------------------ % 69.80/10.41 % (357012)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 69.80/10.41 % (357012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.80/10.41 % (357012)CaDiCaL version: 2.1.3 % 69.80/10.41 % (357012)Termination reason: Instruction limit % 69.80/10.41 % (357012)Termination phase: Property scanning % 69.80/10.41 % (357012)Time elapsed: 0.105 s % 69.80/10.41 % (357012)Peak memory usage: 22 MB % 69.80/10.41 % (357012)Instructions burned: 182 (million) % 69.80/10.41 % (357017)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2664474784:fmbsr=1.3:i=865:ins=25_2993 on theBenchmark for (2993ds/865Mi) % 69.80/10.41 % (357007)Instruction limit reached! % 69.80/10.41 % (357007)------------------------------ % 69.80/10.41 % (357007)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 69.80/10.41 % (357007)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.80/10.41 % (357007)CaDiCaL version: 2.1.3 % 69.80/10.41 % (357007)Termination reason: Instruction limit % 69.80/10.41 % (357007)Termination phase: Finite model building preprocessing % 69.80/10.41 % (357007)Time elapsed: 0.329 s % 69.80/10.41 % (357007)Peak memory usage: 25 MB % 69.80/10.41 % (357007)Instructions burned: 715 (million) % 69.80/10.41 % (357015)Instruction limit reached! % 69.80/10.41 % (357015)------------------------------ % 69.80/10.41 % (357015)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 69.80/10.41 % (357015)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.80/10.41 % (357015)CaDiCaL version: 2.1.3 % 69.80/10.41 % (357015)Termination reason: Instruction limit % 69.80/10.41 % (357015)Termination phase: Property scanning % 69.80/10.41 % (357015)Time elapsed: 0.225 s % 69.80/10.41 % (357015)Peak memory usage: 23 MB % 69.80/10.41 % (357015)Instructions burned: 479 (million) % 69.80/10.41 % (357010)Instruction limit reached! % 69.80/10.41 % (357010)------------------------------ % 69.80/10.41 % (357010)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 69.80/10.41 % (357010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.80/10.41 % (357010)CaDiCaL version: 2.1.3 % 69.80/10.41 % (357010)Termination reason: Instruction limit % 69.80/10.41 % (357010)Termination phase: Saturation % 69.80/10.41 % (357010)Time elapsed: 0.320 s % 69.80/10.41 % (357010)Peak memory usage: 25 MB % 69.80/10.41 % (357010)Instructions burned: 686 (million) % 69.80/10.41 % (357019)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1844429010:i=1179_2991 on theBenchmark for (2991ds/1179Mi) % 69.80/10.41 % (357020)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1238368086:i=889:ins=1_2991 on theBenchmark for (2991ds/889Mi) % 69.80/10.41 % (357021)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=3185504197:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2991 on theBenchmark for (2991ds/692Mi) % 69.80/10.41 % (357017)Instruction limit reached! % 69.80/10.41 % (357017)------------------------------ % 69.80/10.41 % (357017)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 69.80/10.41 % (357017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.80/10.41 % (357017)CaDiCaL version: 2.1.3 % 69.80/10.41 % (357017)Termination reason: Instruction limit % 69.80/10.41 % (357017)Termination phase: Finite model building preprocessing % 69.80/10.41 % (357017)Time elapsed: 0.407 s % 69.80/10.41 % (357017)Peak memory usage: 30 MB % 69.80/10.41 % (357017)Instructions burned: 866 (million) % 69.80/10.41 % (357025)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1926989746:i=879:kws=inv_precedence:fsr=off_2989 on theBenchmark for (2989ds/879Mi) % 69.80/10.41 % (357021)Instruction limit reached! % 69.80/10.41 % (357021)------------------------------ % 69.80/10.41 % (357021)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 69.80/10.41 % (357021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 69.80/10.41 % (357021)CaDiCaL version: 2.1.3 % 69.80/10.41 % (357021)Termination reason: Instruction limit % 157.76/22.82 % (357021)Termination phase: Saturation % 157.76/22.82 % (357021)Time elapsed: 0.343 s % 157.76/22.82 % (357021)Peak memory usage: 28 MB % 157.76/22.82 % (357021)Instructions burned: 693 (million) % 157.76/22.82 % (357027)fmb+10_1_sil=64000:random_seed=3627514823:i=22061:nm=2:gsp=on_2988 on theBenchmark for (2988ds/22061Mi) % 157.76/22.82 % (357020)Instruction limit reached! % 157.76/22.82 % (357020)------------------------------ % 157.76/22.82 % (357020)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.76/22.82 % (357020)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.76/22.82 % (357020)CaDiCaL version: 2.1.3 % 157.76/22.82 % (357020)Termination reason: Instruction limit % 157.76/22.82 % (357020)Termination phase: Finite model building preprocessing % 157.76/22.82 % (357020)Time elapsed: 0.424 s % 157.76/22.82 % (357020)Peak memory usage: 31 MB % 157.76/22.82 % (357020)Instructions burned: 890 (million) % 157.76/22.82 % (357029)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=170207241:i=9515:nm=5_2987 on theBenchmark for (2987ds/9515Mi) % 157.76/22.82 % (357019)Instruction limit reached! % 157.76/22.82 % (357019)------------------------------ % 157.76/22.82 % (357019)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.76/22.82 % (357019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.76/22.82 % (357019)CaDiCaL version: 2.1.3 % 157.76/22.82 % (357019)Termination reason: Instruction limit % 157.76/22.82 % (357019)Termination phase: Saturation % 157.76/22.82 % (357019)Time elapsed: 0.634 s % 157.76/22.82 % (357019)Peak memory usage: 30 MB % 157.76/22.82 % (357019)Instructions burned: 1179 (million) % 157.76/22.82 % (357031)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=278543941:fmbsr=1.7:i=920_2985 on theBenchmark for (2985ds/920Mi) % 157.76/22.82 % (357025)Instruction limit reached! % 157.76/22.82 % (357025)------------------------------ % 157.76/22.82 % (357025)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.76/22.82 % (357025)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.76/22.82 % (357025)CaDiCaL version: 2.1.3 % 157.76/22.82 % (357025)Termination reason: Instruction limit % 157.76/22.82 % (357025)Termination phase: Saturation % 157.76/22.82 % (357025)Time elapsed: 0.421 s % 157.76/22.82 % (357025)Peak memory usage: 30 MB % 157.76/22.82 % (357025)Instructions burned: 879 (million) % 157.76/22.82 % (357033)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=898914392:i=5131_2985 on theBenchmark for (2985ds/5131Mi) % 157.76/22.82 % (357031)Instruction limit reached! % 157.76/22.82 % (357031)------------------------------ % 157.76/22.82 % (357031)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.76/22.82 % (357031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.76/22.82 % (357031)CaDiCaL version: 2.1.3 % 157.76/22.82 % (357031)Termination reason: Instruction limit % 157.76/22.82 % (357031)Termination phase: Finite model building preprocessing % 157.76/22.82 % (357031)Time elapsed: 0.435 s % 157.76/22.82 % (357031)Peak memory usage: 31 MB % 157.76/22.82 % (357031)Instructions burned: 921 (million) % 157.76/22.82 % (357035)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3981438199:i=1472:ins=7:fdi=8:gsp=on_2980 on theBenchmark for (2980ds/1472Mi) % 157.76/22.82 % (357035)Instruction limit reached! % 157.76/22.82 % (357035)------------------------------ % 157.76/22.82 % (357035)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.76/22.82 % (357035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.76/22.82 % (357035)CaDiCaL version: 2.1.3 % 157.76/22.82 % (357035)Termination reason: Instruction limit % 157.76/22.82 % (357035)Termination phase: Saturation % 157.76/22.82 % (357035)Time elapsed: 0.634 s % 157.76/22.82 % (357035)Peak memory usage: 28 MB % 157.76/22.82 % (357035)Instructions burned: 1474 (million) % 157.76/22.82 % (357037)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=4090404346:i=6324_2974 on theBenchmark for (2974ds/6324Mi) % 157.76/22.82 % (357033)Instruction limit reached! % 157.76/22.82 % (357033)------------------------------ % 157.76/22.82 % (357033)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 157.76/22.82 % (357033)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 157.76/22.82 % (357033)CaDiCaL version: 2.1.3 % 157.76/22.82 % (357033)Termination reason: Instruction limit % 157.76/22.82 % (357033)Termination phase: Saturation % 157.76/22.82 % (357033)Time elapsed: 2.909 s % 157.76/22.82 % (357033)Peak memory usage: 61 MB % 157.76/22.82 % (357033)Instructions burned: 5132 (million) % 157.76/22.82 % (357039)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=343921593:fmbsr=2.30978:i=2174_2955 on theBenchmark for (2955ds/2174Mi) % 241.94/35.42 % (357039)Instruction limit reached! % 241.94/35.42 % (357039)------------------------------ % 241.94/35.42 % (357039)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 241.94/35.42 % (357039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 241.94/35.42 % (357039)CaDiCaL version: 2.1.3 % 241.94/35.42 % (357039)Termination reason: Instruction limit % 241.94/35.42 % (357039)Termination phase: Finite model building preprocessing % 241.94/35.42 % (357039)Time elapsed: 1.012 s % 241.94/35.42 % (357039)Peak memory usage: 48 MB % 241.94/35.42 % (357039)Instructions burned: 2176 (million) % 241.94/35.42 % (357041)ott-2_1_sil=16000:newcnf=on:random_seed=3719427242:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2945 on theBenchmark for (2945ds/869Mi) % 241.94/35.42 % (357037)Instruction limit reached! % 241.94/35.42 % (357037)------------------------------ % 241.94/35.42 % (357037)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 241.94/35.42 % (357037)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 241.94/35.42 % (357037)CaDiCaL version: 2.1.3 % 241.94/35.42 % (357037)Termination reason: Instruction limit % 241.94/35.42 % (357037)Termination phase: Finite model building preprocessing % 241.94/35.42 % (357037)Time elapsed: 3.179 s % 241.94/35.42 % (357037)Peak memory usage: 67 MB % 241.94/35.42 % (357037)Instructions burned: 6325 (million) % 241.94/35.42 % (357043)ott+10_1_sil=32000:tgt=ground:random_seed=4075688505:i=5114:av=off_2942 on theBenchmark for (2942ds/5114Mi) % 241.94/35.42 % (357041)Instruction limit reached! % 241.94/35.42 % (357041)------------------------------ % 241.94/35.42 % (357041)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 241.94/35.42 % (357041)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 241.94/35.42 % (357041)CaDiCaL version: 2.1.3 % 241.94/35.42 % (357041)Termination reason: Instruction limit % 241.94/35.42 % (357041)Termination phase: Saturation % 241.94/35.42 % (357041)Time elapsed: 0.442 s % 241.94/35.42 % (357041)Peak memory usage: 28 MB % 241.94/35.42 % (357041)Instructions burned: 870 (million) % 241.94/35.42 % (357045)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3473232081:i=54282_2940 on theBenchmark for (2940ds/54282Mi) % 241.94/35.42 % (357029)Instruction limit reached! % 241.94/35.42 % (357029)------------------------------ % 241.94/35.42 % (357029)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 241.94/35.42 % (357029)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 241.94/35.42 % (357029)CaDiCaL version: 2.1.3 % 241.94/35.42 % (357029)Termination reason: Instruction limit % 241.94/35.42 % (357029)Termination phase: Finite model building preprocessing % 241.94/35.42 % (357029)Time elapsed: 4.882 s % 241.94/35.42 % (357029)Peak memory usage: 88 MB % 241.94/35.42 % (357029)Instructions burned: 9515 (million) % 241.94/35.42 % (357047)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1994920471:i=3512:aac=none_2938 on theBenchmark for (2938ds/3512Mi) % 241.94/35.42 % (357047)Instruction limit reached! % 241.94/35.42 % (357047)------------------------------ % 241.94/35.42 % (357047)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 241.94/35.42 % (357047)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 241.94/35.42 % (357047)CaDiCaL version: 2.1.3 % 241.94/35.42 % (357047)Termination reason: Instruction limit % 241.94/35.42 % (357047)Termination phase: Saturation % 241.94/35.42 % (357047)Time elapsed: 1.962 s % 241.94/35.42 % (357047)Peak memory usage: 51 MB % 241.94/35.42 % (357047)Instructions burned: 3513 (million) % 241.94/35.42 % (357049)dis+21_1_sil=32000:sas=cadical:random_seed=1330456467:i=3773:amm=off_2918 on theBenchmark for (2918ds/3773Mi) % 241.94/35.42 % (357043)Instruction limit reached! % 241.94/35.42 % (357043)------------------------------ % 241.94/35.42 % (357043)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 241.94/35.42 % (357043)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 241.94/35.42 % (357043)CaDiCaL version: 2.1.3 % 241.94/35.42 % (357043)Termination reason: Instruction limit % 241.94/35.42 % (357043)Termination phase: Saturation % 241.94/35.42 % (357043)Time elapsed: 3.121 s % 241.94/35.42 % (357043)Peak memory usage: 65 MB % 241.94/35.42 % (357043)Instructions burned: 5115 (million) % 241.94/35.42 % (357051)ott+11_1_sil=16000:gs=on:random_seed=3629084629:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2910 on theBenchmark for (2910ds/2251Mi) % 241.94/35.42 % (357051)Instruction limit reached! % 300.15/42.93 % (357051)------------------------------ % 300.15/42.93 % (357051)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.15/42.93 % (357051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.15/42.93 % (357051)CaDiCaL version: 2.1.3 % 300.15/42.93 % (357051)Termination reason: Instruction limit % 300.15/42.93 % (357051)Termination phase: Saturation % 300.15/42.93 % (357051)Time elapsed: 1.195 s % 300.15/42.93 % (357051)Peak memory usage: 34 MB % 300.15/42.93 % (357051)Instructions burned: 2252 (million) % 300.15/42.93 % (357053)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3104820408:fmbsr=1.6:i=67534_2898 on theBenchmark for (2898ds/67534Mi) % 300.15/42.93 % (357049)Instruction limit reached! % 300.15/42.93 % (357049)------------------------------ % 300.15/42.93 % (357049)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.15/42.93 % (357049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.15/42.93 % (357049)CaDiCaL version: 2.1.3 % 300.15/42.93 % (357049)Termination reason: Instruction limit % 300.15/42.93 % (357049)Termination phase: Saturation % 300.15/42.93 % (357049)Time elapsed: 2.126 s % 300.15/42.93 % (357049)Peak memory usage: 56 MB % 300.15/42.93 % (357049)Instructions burned: 3773 (million) % 300.15/42.93 % (357055)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=720178874:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2896 on theBenchmark for (2896ds/4591Mi) % 300.15/42.93 % (357055)Instruction limit reached! % 300.15/42.93 % (357055)------------------------------ % 300.15/42.93 % (357055)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.15/42.93 % (357055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.15/42.93 % (357055)CaDiCaL version: 2.1.3 % 300.15/42.93 % (357055)Termination reason: Instruction limit % 300.15/42.93 % (357055)Termination phase: Saturation % 300.15/42.93 % (357055)Time elapsed: 1.716 s % 300.15/42.93 % (357055)Peak memory usage: 31 MB % 300.15/42.93 % (357055)Instructions burned: 4594 (million) % 300.15/42.93 % (357057)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=4155819740:i=29340_2879 on theBenchmark for (2879ds/29340Mi) % 300.15/42.93 % (357027)Instruction limit reached! % 300.15/42.93 % (357027)------------------------------ % 300.15/42.93 % (357027)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.15/42.93 % (357027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.15/42.93 % (357027)CaDiCaL version: 2.1.3 % 300.15/42.93 % (357027)Termination reason: Instruction limit % 300.15/42.93 % (357027)Termination phase: Finite model building preprocessing % 300.15/42.93 % (357027)Time elapsed: 11.500 s % 300.15/42.93 % (357027)Peak memory usage: 216 MB % 300.15/42.93 % (357027)Instructions burned: 22062 (million) % 300.15/42.93 % (357059)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2425627349:i=5211_2872 on theBenchmark for (2872ds/5211Mi) % 300.15/42.93 % TRYING [1] % 300.15/42.93 % TRYING [2] % 300.15/42.93 % (357059)Instruction limit reached! % 300.15/42.93 % (357059)------------------------------ % 300.15/42.93 % (357059)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.15/42.93 % (357059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.15/42.93 % (357059)CaDiCaL version: 2.1.3 % 300.15/42.93 % (357059)Termination reason: Instruction limit % 300.15/42.93 % (357059)Termination phase: Saturation % 300.15/42.93 % (357059)Time elapsed: 2.143 s % 300.15/42.93 % (357059)Peak memory usage: 47 MB % 300.15/42.93 % (357059)Instructions burned: 5212 (million) % 300.15/42.93 % (357061)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=4226344871:i=5497:nm=2_2850 on theBenchmark for (2850ds/5497Mi) % 300.15/42.93 % TRYING [3] % 300.15/42.93 % (357061)Instruction limit reached! % 300.15/42.93 % (357061)------------------------------ % 300.15/42.93 % (357061)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.15/42.93 % (357061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.15/42.93 % (357061)CaDiCaL version: 2.1.3 % 300.15/42.93 % (357061)Termination reason: Instruction limit % 300.15/42.93 % (357061)Termination phase: Finite model building preprocessing % 300.15/42.93 % (357061)Time elapsed: 2.800 s % 300.15/42.93 % (357061)Peak memory usage: 64 MB % 300.15/42.93 % (357061)Instructions burned: 5498 (million) % 300.15/42.93 % (357063)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1408285623:fmbsr=2:i=46332_2822 on theBenchmark for (2822ds/46332Mi) % 300.15/42.93 % TRYING [1] % 300.15/42.93 % TRYING [2] % 300.15/42.93 % TRYING [3] % 300.15/42.93 % (357053)Canno % 300.15/42.93 Terminated % 300.15/42.93 % Vampire exiting % 300.15/42.93 Terminated %------------------------------------------------------------------------------