%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWX230_1 : TPTP v9.3.1. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n009.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:46:48 PM UTC 2026 % Result : Timeout 295.72s 41.93s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWX230_1 : TPTP v9.3.1. Released v9.3.0. % 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.22 % Computer : n009.cluster.edu % 0.09/0.22 % Model : x86_64 x86_64 % 0.09/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.22 % Memory : 8046.5625MB % 0.09/0.22 % OS : Linux 6.8.0-71-generic % 0.09/0.22 % CPULimit : 300 % 0.09/0.22 % WCLimit : 300 % 0.09/0.22 % DateTime : Mon Sep 28 15:17:45 UTC 2026 % 0.09/0.22 % CPUTime : % 0.09/0.22 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.26 Running first-order model finding % 0.09/0.27 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 % 8.64/1.82 % (3139710)Will run a generic schedule for satisfiability detection. % 8.64/1.82 % (3139720)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1713085922:i=131_2999 on theBenchmark for (2999ds/131Mi) % 8.64/1.82 % (3139715)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=138000026_2999 on theBenchmark for (2999ds/0Mi) % 8.64/1.82 % (3139716)% WARNING: option uhcvi not known. % 8.64/1.82 % (3139719)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2962363235:i=116_2999 on theBenchmark for (2999ds/116Mi) % 8.64/1.82 % (3139718)dis+10_1_sil=32000:sp=arity:random_seed=3784536155:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 8.64/1.82 % (3139716)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3887310841:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 8.64/1.82 % (3139717)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2058772137:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 8.64/1.82 % (3139721)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2949156446:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 8.64/1.82 % Detected minimum model sizes of [1,1] % 8.64/1.82 % Detected maximum model sizes of [max,2] % 8.64/1.82 % TRYING [1,1] % 8.64/1.82 % TRYING [1,2] % 8.64/1.82 % TRYING [2,2] % 8.64/1.82 % TRYING [3,2] % 8.64/1.82 % TRYING [4,2] % 8.64/1.82 % (3139720)Instruction limit reached! % 8.64/1.82 % (3139720)------------------------------ % 8.64/1.82 % (3139720)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.64/1.82 % (3139720)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.64/1.82 % (3139720)CaDiCaL version: 2.1.3 % 8.64/1.82 % (3139720)Termination reason: Instruction limit % 8.64/1.82 % (3139720)Termination phase: Saturation % 8.64/1.82 % (3139720)Time elapsed: 0.069 s % 8.64/1.82 % (3139720)Peak memory usage: 13 MB % 8.64/1.82 % (3139720)Instructions burned: 132 (million) % 8.64/1.82 % (3139729)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=178312508:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi) % 8.64/1.82 % TRYING [1] % 8.64/1.82 % TRYING [2] % 8.64/1.82 % TRYING [3] % 8.64/1.82 % (3139718)Instruction limit reached! % 8.64/1.82 % (3139718)------------------------------ % 8.64/1.82 % (3139718)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.64/1.82 % (3139718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.64/1.82 % (3139718)CaDiCaL version: 2.1.3 % 8.64/1.82 % (3139718)Termination reason: Instruction limit % 8.64/1.82 % (3139718)Termination phase: Saturation % 8.64/1.82 % (3139718)Time elapsed: 0.101 s % 8.64/1.82 % (3139718)Peak memory usage: 13 MB % 8.64/1.82 % (3139718)Instructions burned: 103 (million) % 8.64/1.82 % (3139719)Instruction limit reached! % 8.64/1.82 % (3139719)------------------------------ % 8.64/1.82 % (3139719)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.64/1.82 % (3139719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.64/1.82 % (3139719)CaDiCaL version: 2.1.3 % 8.64/1.82 % (3139719)Termination reason: Instruction limit % 8.64/1.82 % (3139719)Termination phase: Saturation % 8.64/1.82 % (3139719)Time elapsed: 0.112 s % 8.64/1.82 % (3139719)Peak memory usage: 13 MB % 8.64/1.82 % (3139719)Instructions burned: 116 (million) % 8.64/1.82 % TRYING [4] % 8.64/1.82 % (3139731)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2423905310:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 8.64/1.82 % (3139732)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=1803908715:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 8.64/1.82 % (3139721)Instruction limit reached! % 8.64/1.82 % (3139721)------------------------------ % 8.64/1.82 % (3139721)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.64/1.82 % (3139721)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.64/1.82 % (3139721)CaDiCaL version: 2.1.3 % 8.64/1.82 % (3139721)Termination reason: Instruction limit % 8.64/1.82 % (3139721)Termination phase: Saturation % 8.64/1.82 % (3139721)Time elapsed: 0.151 s % 8.64/1.82 % (3139721)Peak memory usage: 13 MB % 8.64/1.82 % (3139721)Instructions burned: 159 (million) % 8.64/1.82 % TRYING [5,2] % 8.64/1.82 % TRYING [5] % 8.64/1.82 % (3139735)ott-21_1_sil=16000:fs=off:random_seed=3715728551:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 8.64/1.82 % (3139731)Instruction limit reached! % 8.64/1.82 % (3139731)------------------------------ % 41.03/6.05 % (3139731)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 41.03/6.05 % (3139731)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.03/6.05 % (3139731)CaDiCaL version: 2.1.3 % 41.03/6.05 % (3139731)Termination reason: Instruction limit % 41.03/6.05 % (3139731)Termination phase: Saturation % 41.03/6.05 % (3139731)Time elapsed: 0.158 s % 41.03/6.05 % (3139731)Peak memory usage: 13 MB % 41.03/6.05 % (3139731)Instructions burned: 132 (million) % 41.03/6.05 % (3139737)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3049175999:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi) % 41.03/6.05 % (3139735)Instruction limit reached! % 41.03/6.05 % (3139735)------------------------------ % 41.03/6.05 % (3139735)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 41.03/6.05 % (3139735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.03/6.05 % (3139735)CaDiCaL version: 2.1.3 % 41.03/6.05 % (3139735)Termination reason: Instruction limit % 41.03/6.05 % (3139735)Termination phase: Saturation % 41.03/6.05 % (3139735)Time elapsed: 0.156 s % 41.03/6.05 % (3139735)Peak memory usage: 13 MB % 41.03/6.05 % (3139735)Instructions burned: 180 (million) % 41.03/6.05 % (3139729)Instruction limit reached! % 41.03/6.05 % (3139729)------------------------------ % 41.03/6.05 % (3139729)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 41.03/6.05 % (3139729)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.03/6.05 % (3139729)CaDiCaL version: 2.1.3 % 41.03/6.05 % (3139729)Termination reason: Instruction limit % 41.03/6.05 % (3139729)Termination phase: Finite model building SAT solving % 41.03/6.05 % (3139729)Time elapsed: 0.291 s % 41.03/6.05 % (3139729)Peak memory usage: 42 MB % 41.03/6.05 % (3139729)Instructions burned: 715 (million) % 41.03/6.05 % (3139739)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3582777269:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi) % 41.03/6.05 % (3139740)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2157960064:i=1179_2995 on theBenchmark for (2995ds/1179Mi) % 41.03/6.05 % Detected minimum model sizes of [1,1] % 41.03/6.05 % Detected maximum model sizes of [max,2] % 41.03/6.05 % TRYING [1,1] % 41.03/6.05 % TRYING [1,2] % 41.03/6.05 % TRYING [2,2] % 41.03/6.05 % TRYING [3,2] % 41.03/6.05 % TRYING [4,2] % 41.03/6.05 % TRYING [6,2] % 41.03/6.05 % TRYING [5,2] % 41.03/6.05 % (3139732)Instruction limit reached! % 41.03/6.05 % (3139732)------------------------------ % 41.03/6.05 % (3139732)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 41.03/6.05 % (3139732)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.03/6.05 % (3139732)CaDiCaL version: 2.1.3 % 41.03/6.05 % (3139732)Termination reason: Instruction limit % 41.03/6.05 % (3139732)Termination phase: Saturation % 41.03/6.05 % (3139732)Time elapsed: 0.613 s % 41.03/6.05 % (3139732)Peak memory usage: 18 MB % 41.03/6.05 % (3139732)Instructions burned: 684 (million) % 41.03/6.05 % (3139737)Instruction limit reached! % 41.03/6.05 % (3139737)------------------------------ % 41.03/6.05 % (3139737)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 41.03/6.05 % (3139737)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.03/6.05 % (3139737)CaDiCaL version: 2.1.3 % 41.03/6.05 % (3139737)Termination reason: Instruction limit % 41.03/6.05 % (3139737)Termination phase: Saturation % 41.03/6.05 % (3139737)Time elapsed: 0.477 s % 41.03/6.05 % (3139737)Peak memory usage: 15 MB % 41.03/6.05 % (3139737)Instructions burned: 478 (million) % 41.03/6.05 % (3139743)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=407764365:i=889:ins=1_2992 on theBenchmark for (2992ds/889Mi) % 41.03/6.05 % (3139744)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=1173887366: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) % 41.03/6.05 % Detected minimum model sizes of [1,1] % 41.03/6.05 % Detected maximum model sizes of [max,2] % 41.03/6.05 % fmb_start_size (= 14) larger than a detected sort maximum size! % 41.03/6.05 % (3139743)Refutation not found, incomplete strategy % 41.03/6.05 % (3139743)------------------------------ % 41.03/6.05 % (3139743)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 41.03/6.05 % (3139743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.03/6.05 % (3139743)CaDiCaL version: 2.1.3 % 41.03/6.05 % (3139743)Termination reason: Refutation not found, incomplete strategy % 80.69/11.73 % (3139743)Time elapsed: 0.023 s % 80.69/11.73 % (3139743)Peak memory usage: 11 MB % 80.69/11.73 % (3139743)Instructions burned: 25 (million) % 80.69/11.73 % (3139743)------------------------------ % 80.69/11.73 % (3139743)------------------------------ % 80.69/11.73 % (3139747)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=783345708:i=879:kws=inv_precedence:fsr=off_2991 on theBenchmark for (2991ds/879Mi) % 80.69/11.73 % (3139740)Instruction limit reached! % 80.69/11.73 % (3139740)------------------------------ % 80.69/11.73 % (3139740)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 80.69/11.73 % (3139740)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.69/11.73 % (3139740)CaDiCaL version: 2.1.3 % 80.69/11.73 % (3139740)Termination reason: Instruction limit % 80.69/11.73 % (3139740)Termination phase: Saturation % 80.69/11.73 % (3139740)Time elapsed: 0.542 s % 80.69/11.73 % (3139740)Peak memory usage: 19 MB % 80.69/11.73 % (3139740)Instructions burned: 1181 (million) % 80.69/11.73 % (3139749)fmb+10_1_sil=64000:random_seed=1078719850:i=22061:nm=2:gsp=on_2990 on theBenchmark for (2990ds/22061Mi) % 80.69/11.73 % Detected minimum model sizes of [1,1] % 80.69/11.73 % Detected maximum model sizes of [max,2] % 80.69/11.73 % TRYING [1,1] % 80.69/11.73 % TRYING [1,2] % 80.69/11.73 % TRYING [2,2] % 80.69/11.73 % TRYING [3,2] % 80.69/11.73 % (3139739)Instruction limit reached! % 80.69/11.73 % (3139739)------------------------------ % 80.69/11.73 % (3139739)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 80.69/11.73 % (3139739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.69/11.73 % (3139739)CaDiCaL version: 2.1.3 % 80.69/11.73 % (3139739)Termination reason: Instruction limit % 80.69/11.73 % (3139739)Termination phase: Finite model building SAT solving % 80.69/11.73 % (3139739)Time elapsed: 0.649 s % 80.69/11.73 % (3139739)Peak memory usage: 34 MB % 80.69/11.73 % (3139739)Instructions burned: 865 (million) % 80.69/11.73 % TRYING [4,2] % 80.69/11.73 % (3139751)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3990625577:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi) % 80.69/11.73 % Detected minimum model sizes of [1,1] % 80.69/11.73 % Detected maximum model sizes of [max,2] % 80.69/11.73 % fmb_start_size (= 20) larger than a detected sort maximum size! % 80.69/11.73 % (3139751)Refutation not found, incomplete strategy % 80.69/11.73 % (3139751)------------------------------ % 80.69/11.73 % (3139751)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 80.69/11.73 % (3139751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.69/11.73 % (3139751)CaDiCaL version: 2.1.3 % 80.69/11.73 % (3139751)Termination reason: Refutation not found, incomplete strategy % 80.69/11.73 % (3139751)Time elapsed: 0.014 s % 80.69/11.73 % (3139751)Peak memory usage: 11 MB % 80.69/11.73 % (3139751)Instructions burned: 25 (million) % 80.69/11.73 % (3139751)------------------------------ % 80.69/11.73 % (3139751)------------------------------ % 80.69/11.73 % (3139753)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1680745107:fmbsr=1.7:i=920_2988 on theBenchmark for (2988ds/920Mi) % 80.69/11.73 % Detected minimum model sizes of [1,1] % 80.69/11.73 % Detected maximum model sizes of [max,2] % 80.69/11.73 % fmb_start_size (= 8) larger than a detected sort maximum size! % 80.69/11.73 % (3139753)Refutation not found, incomplete strategy % 80.69/11.73 % (3139753)------------------------------ % 80.69/11.73 % (3139753)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 80.69/11.73 % (3139753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.69/11.73 % (3139753)CaDiCaL version: 2.1.3 % 80.69/11.73 % (3139753)Termination reason: Refutation not found, incomplete strategy % 80.69/11.73 % (3139753)Time elapsed: 0.026 s % 80.69/11.73 % (3139753)Peak memory usage: 11 MB % 80.69/11.73 % (3139753)Instructions burned: 25 (million) % 80.69/11.73 % (3139753)------------------------------ % 80.69/11.73 % (3139753)------------------------------ % 80.69/11.73 % TRYING [5,2] % 80.69/11.73 % (3139755)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2583944908:i=5131_2988 on theBenchmark for (2988ds/5131Mi) % 80.69/11.73 % TRYING [7,2] % 80.69/11.73 % TRYING [6,2] % 80.69/11.73 % (3139744)Instruction limit reached! % 80.69/11.73 % (3139744)------------------------------ % 80.69/11.73 % (3139744)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 80.69/11.73 % (3139744)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 80.69/11.73 % (3139744)CaDiCaL version: 2.1.3 % 80.69/11.73 % (3139744)Termination reason: Instruction limit % 80.69/11.73 % (3139744)Termination phase: Saturation % 80.69/11.73 % (3139744)Time elapsed: 0.697 s % 80.69/11.73 % (3139744)Peak memory usage: 20 MB % 247.04/35.11 % (3139744)Instructions burned: 693 (million) % 247.04/35.11 % (3139757)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2728144002:i=1472:ins=7:fdi=8:gsp=on_2984 on theBenchmark for (2984ds/1472Mi) % 247.04/35.11 % (3139747)Instruction limit reached! % 247.04/35.11 % (3139747)------------------------------ % 247.04/35.11 % (3139747)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 247.04/35.11 % (3139747)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.04/35.11 % (3139747)CaDiCaL version: 2.1.3 % 247.04/35.11 % (3139747)Termination reason: Instruction limit % 247.04/35.11 % (3139747)Termination phase: Saturation % 247.04/35.11 % (3139747)Time elapsed: 0.771 s % 247.04/35.11 % (3139747)Peak memory usage: 16 MB % 247.04/35.11 % (3139747)Instructions burned: 879 (million) % 247.04/35.11 % (3139759)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3738309250:i=6324_2983 on theBenchmark for (2983ds/6324Mi) % 247.04/35.11 % Detected minimum model sizes of [1,1] % 247.04/35.11 % Detected maximum model sizes of [max,2] % 247.04/35.11 % fmb_start_size (= 77) larger than a detected sort maximum size! % 247.04/35.11 % (3139759)Refutation not found, incomplete strategy % 247.04/35.11 % (3139759)------------------------------ % 247.04/35.11 % (3139759)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 247.04/35.11 % (3139759)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.04/35.11 % (3139759)CaDiCaL version: 2.1.3 % 247.04/35.11 % (3139759)Termination reason: Refutation not found, incomplete strategy % 247.04/35.11 % (3139759)Time elapsed: 0.014 s % 247.04/35.11 % (3139759)Peak memory usage: 11 MB % 247.04/35.11 % (3139759)Instructions burned: 25 (million) % 247.04/35.11 % (3139759)------------------------------ % 247.04/35.11 % (3139759)------------------------------ % 247.04/35.11 % (3139761)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=459744212:fmbsr=2.30978:i=2174_2982 on theBenchmark for (2982ds/2174Mi) % 247.04/35.11 % TRYING [16] % 247.04/35.11 % TRYING [7,2] % 247.04/35.11 % (3139757)Instruction limit reached! % 247.04/35.11 % (3139757)------------------------------ % 247.04/35.11 % (3139757)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 247.04/35.11 % (3139757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.04/35.11 % (3139757)CaDiCaL version: 2.1.3 % 247.04/35.11 % (3139757)Termination reason: Instruction limit % 247.04/35.11 % (3139757)Termination phase: Saturation % 247.04/35.11 % (3139757)Time elapsed: 1.157 s % 247.04/35.11 % (3139757)Peak memory usage: 28 MB % 247.04/35.11 % (3139757)Instructions burned: 1474 (million) % 247.04/35.11 % (3139765)ott-2_1_sil=16000:newcnf=on:random_seed=3017217330:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2972 on theBenchmark for (2972ds/869Mi) % 247.04/35.11 % TRYING [8,2] % 247.04/35.11 % (3139761)Instruction limit reached! % 247.04/35.11 % (3139761)------------------------------ % 247.04/35.11 % (3139761)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 247.04/35.11 % (3139761)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.04/35.11 % (3139761)CaDiCaL version: 2.1.3 % 247.04/35.11 % (3139761)Termination reason: Instruction limit % 247.04/35.11 % (3139761)Termination phase: Finite model building constraint generation % 247.04/35.11 % (3139761)Time elapsed: 1.495 s % 247.04/35.11 % (3139761)Peak memory usage: 135 MB % 247.04/35.11 % (3139761)Instructions burned: 2175 (million) % 247.04/35.11 % (3139767)ott+10_1_sil=32000:tgt=ground:random_seed=3794706789:i=5114:av=off_2967 on theBenchmark for (2967ds/5114Mi) % 247.04/35.11 % (3139765)Instruction limit reached! % 247.04/35.11 % (3139765)------------------------------ % 247.04/35.11 % (3139765)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 247.04/35.11 % (3139765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 247.04/35.11 % (3139765)CaDiCaL version: 2.1.3 % 247.04/35.11 % (3139765)Termination reason: Instruction limit % 247.04/35.11 % (3139765)Termination phase: Saturation % 247.04/35.11 % (3139765)Time elapsed: 0.737 s % 247.04/35.11 % (3139765)Peak memory usage: 16 MB % 247.04/35.11 % (3139765)Instructions burned: 870 (million) % 247.04/35.11 % (3139769)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1419284307:i=54282_2964 on theBenchmark for (2964ds/54282Mi) % 247.04/35.11 % Detected minimum model sizes of [1,1] % 247.04/35.11 % Detected maximum model sizes of [max,2] % 247.04/35.11 % TRYING [1,1] % 247.04/35.11 % TRYING [1,2] % 247.04/35.11 % TRYING [2,2] % 247.04/35.11 % TRYING [3,2] % 247.04/35.11 % TRYING [4,2] % 247.04/35.11 % TRYING [5,2] % 247.04/35.11 % TRYING [6,2] % 247.04/35.11 % TRYING [8,2] % 247.04/35.11 % TRYING [7,2] % 247.04/35.11 % (3139755)Instruction limit reached! % 247.04/35.11 % (3139755)------------------------------ % 295.72/41.93 % (3139755)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 295.72/41.93 % (3139755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.72/41.93 % (3139755)CaDiCaL version: 2.1.3 % 295.72/41.93 % (3139755)Termination reason: Instruction limit % 295.72/41.93 % (3139755)Termination phase: Saturation % 295.72/41.93 % (3139755)Time elapsed: 4.586 s % 295.72/41.93 % (3139755)Peak memory usage: 53 MB % 295.72/41.93 % (3139755)Instructions burned: 5132 (million) % 295.72/41.93 % (3139775)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2672689769:i=3512:aac=none_2942 on theBenchmark for (2942ds/3512Mi) % 295.72/41.93 % TRYING [9,2] % 295.72/41.93 % TRYING [8,2] % 295.72/41.93 % (3139767)Instruction limit reached! % 295.72/41.93 % (3139767)------------------------------ % 295.72/41.93 % (3139767)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 295.72/41.93 % (3139767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.72/41.93 % (3139767)CaDiCaL version: 2.1.3 % 295.72/41.93 % (3139767)Termination reason: Instruction limit % 295.72/41.93 % (3139767)Termination phase: Saturation % 295.72/41.93 % (3139767)Time elapsed: 4.399 s % 295.72/41.93 % (3139767)Peak memory usage: 53 MB % 295.72/41.93 % (3139767)Instructions burned: 5115 (million) % 295.72/41.93 % (3139783)dis+21_1_sil=32000:sas=cadical:random_seed=1498521218:i=3773:amm=off_2923 on theBenchmark for (2923ds/3773Mi) % 295.72/41.93 % TRYING [9,2] % 295.72/41.93 % (3139775)Instruction limit reached! % 295.72/41.93 % (3139775)------------------------------ % 295.72/41.93 % (3139775)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 295.72/41.93 % (3139775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.72/41.93 % (3139775)CaDiCaL version: 2.1.3 % 295.72/41.93 % (3139775)Termination reason: Instruction limit % 295.72/41.93 % (3139775)Termination phase: Saturation % 295.72/41.93 % (3139775)Time elapsed: 3.147 s % 295.72/41.93 % (3139775)Peak memory usage: 39 MB % 295.72/41.93 % (3139775)Instructions burned: 3512 (million) % 295.72/41.93 % (3139795)ott+11_1_sil=16000:gs=on:random_seed=2222505366:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2910 on theBenchmark for (2910ds/2251Mi) % 295.72/41.93 % TRYING [9,2] % 295.72/41.93 % (3139749)Instruction limit reached! % 295.72/41.93 % (3139749)------------------------------ % 295.72/41.93 % (3139749)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 295.72/41.93 % (3139749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.72/41.93 % (3139749)CaDiCaL version: 2.1.3 % 295.72/41.93 % (3139749)Termination reason: Instruction limit % 295.72/41.93 % (3139749)Termination phase: Finite model building constraint generation % 295.72/41.93 % (3139749)Time elapsed: 9.329 s % 295.72/41.93 % (3139749)Peak memory usage: 313 MB % 295.72/41.93 % (3139749)Instructions burned: 22061 (million) % 295.72/41.93 % (3139799)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1559296941:fmbsr=1.6:i=67534_2896 on theBenchmark for (2896ds/67534Mi) % 295.72/41.93 % TRYING [7] % 295.72/41.93 % (3139783)Instruction limit reached! % 295.72/41.93 % (3139783)------------------------------ % 295.72/41.93 % (3139783)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 295.72/41.93 % (3139783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.72/41.93 % (3139783)CaDiCaL version: 2.1.3 % 295.72/41.93 % (3139783)Termination reason: Instruction limit % 295.72/41.93 % (3139783)Termination phase: Saturation % 295.72/41.93 % (3139783)Time elapsed: 3.383 s % 295.72/41.93 % (3139783)Peak memory usage: 40 MB % 295.72/41.93 % (3139783)Instructions burned: 3773 (million) % 295.72/41.93 % (3139801)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1006662955:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2888 on theBenchmark for (2888ds/4591Mi) % 295.72/41.93 % (3139795)Instruction limit reached! % 295.72/41.93 % (3139795)------------------------------ % 295.72/41.93 % (3139795)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 295.72/41.93 % (3139795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 295.72/41.93 % (3139795)CaDiCaL version: 2.1.3 % 295.72/41.93 % (3139795)Termination reason: Instruction limit % 295.72/41.93 % (3139795)Termination phase: Saturation % 295.72/41.93 % (3139795)Time elapsed: 2.193 s % 295.72/41.93 % (3139795)Peak memory usage: 33 MB % 295.72/41.93 % (3139795)Instructions burned: 2252 (million) % 295.72/41.93 % (3139803)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2065266975:i=29340_2888 on theBenchmark for (2888ds/29340Mi) % 295.72/41.93 % TRYING [10,2] % 300.43/42.63 % TRYING [8] % 300.43/42.63 % TRYING [10,2] % 300.43/42.63 % (3139801)Instruction limit reached! % 300.43/42.63 % (3139801)------------------------------ % 300.43/42.63 % (3139801)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.43/42.63 % (3139801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.43/42.63 % (3139801)CaDiCaL version: 2.1.3 % 300.43/42.63 % (3139801)Termination reason: Instruction limit % 300.43/42.63 % (3139801)Termination phase: Saturation % 300.43/42.63 % (3139801)Time elapsed: 3.962 s % 300.43/42.63 % (3139801)Peak memory usage: 51 MB % 300.43/42.63 % (3139801)Instructions burned: 4591 (million) % 300.43/42.63 % (3139813)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3179196273:i=5211_2848 on theBenchmark for (2848ds/5211Mi) % 300.43/42.63 % (3139813)Instruction limit reached! % 300.43/42.63 % (3139813)------------------------------ % 300.43/42.63 % (3139813)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.43/42.63 % (3139813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.43/42.63 % (3139813)CaDiCaL version: 2.1.3 % 300.43/42.63 % (3139813)Termination reason: Instruction limit % 300.43/42.63 % (3139813)Termination phase: Saturation % 300.43/42.63 % (3139813)Time elapsed: 4.547 s % 300.43/42.63 % (3139813)Peak memory usage: 53 MB % 300.43/42.63 % (3139813)Instructions burned: 5212 (million) % 300.43/42.63 % (3139821)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2182953224:i=5497:nm=2_2803 on theBenchmark for (2803ds/5497Mi) % 300.43/42.63 % Detected minimum model sizes of [1,1] % 300.43/42.63 % Detected maximum model sizes of [max,2] % 300.43/42.63 % fmb_start_size (= 17) larger than a detected sort maximum size! % 300.43/42.63 % (3139821)Refutation not found, incomplete strategy % 300.43/42.63 % (3139821)------------------------------ % 300.43/42.63 % (3139821)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.43/42.63 % (3139821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.43/42.63 % (3139821)CaDiCaL version: 2.1.3 % 300.43/42.63 % (3139821)Termination reason: Refutation not found, incomplete strategy % 300.43/42.63 % (3139821)Time elapsed: 0.029 s % 300.43/42.63 % (3139821)Peak memory usage: 11 MB % 300.43/42.63 % (3139821)Instructions burned: 25 (million) % 300.43/42.63 % (3139821)------------------------------ % 300.43/42.63 % (3139821)------------------------------ % 300.43/42.63 % (3139823)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=373586825:fmbsr=2:i=46332_2802 on theBenchmark for (2802ds/46332Mi) % 300.43/42.63 % TRYING [15] % 300.43/42.63 % TRYING [9] % 300.43/42.63 % TRYING [11,2] % 300.43/42.63 % TRYING [11,2] % 300.43/42.63 % TRYING [12,2] % 300.43/42.63 % (3139803)Instruction limit reached! % 300.43/42.63 % (3139803)------------------------------ % 300.43/42.63 % (3139803)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.43/42.63 % (3139803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.43/42.63 % (3139803)CaDiCaL version: 2.1.3 % 300.43/42.63 % (3139803)Termination reason: Instruction limit % 300.43/42.63 % (3139803)Termination phase: Saturation % 300.43/42.63 % (3139803)Time elapsed: 21.199 s % 300.43/42.63 % (3139803)Peak memory usage: 74 MB % 300.43/42.63 % (3139803)Instructions burned: 29341 (million) % 300.43/42.63 % (3139984)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3800035304:i=14071_2675 on theBenchmark for (2675ds/14071Mi) % 300.43/42.63 % Detected minimum model sizes of [1,1] % 300.43/42.63 % Detected maximum model sizes of [max,2] % 300.43/42.63 % fmb_start_size (= 12) larger than a detected sort maximum size! % 300.43/42.63 % (3139984)Refutation not found, incomplete strategy % 300.43/42.63 % (3139984)------------------------------ % 300.43/42.63 % (3139984)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.43/42.63 % (3139984)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.43/42.63 % (3139984)CaDiCaL version: 2.1.3 % 300.43/42.63 % (3139984)Termination reason: Refutation not found, incomplete strategy % 300.43/42.63 % (3139984)Time elapsed: 0.013 s % 300.43/42.63 % (3139984)Peak memory usage: 11 MB % 300.43/42.63 % (3139984)Instructions burned: 25 (million) % 300.43/42.63 % (3139984)------------------------------ % 300.43/42.63 % (3139984)------------------------------ % 300.43/42.63 % (3139986)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1179471228:i=22565:add=on:rawr=on_2675 on theBenchmark for (2675ds/22565Mi) % 300.43/42.63 % TRYING [10] % 300.43/42.63 % TRYING [12,2] % 300.43/42.63 % (3139799)Instruction limit reached! % 300.43/42.63 % (3139799)------------------------------ % 300.43/42.63 % (3139799)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16: % 300.43/42.63 Terminated % 300.43/42.63 % Vampire exiting % 300.43/42.64 Terminated %------------------------------------------------------------------------------