%------------------------------------------------------------------------------ % File : Vampire-SAT---5.0.1 % Problem : SWV977-1 : TPTP v9.3.1. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n006.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:26:45 PM UTC 2026 % Result : Timeout 300.33s 42.54s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWV977-1 : TPTP v9.3.1. Released v4.1.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.17 % Computer : n006.cluster.edu % 0.09/0.17 % Model : x86_64 x86_64 % 0.09/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.17 % Memory : 8046.5625MB % 0.09/0.17 % OS : Linux 6.8.0-71-generic % 0.09/0.17 % CPULimit : 300 % 0.09/0.17 % WCLimit : 300 % 0.09/0.17 % DateTime : Mon Sep 28 13:03:25 UTC 2026 % 0.09/0.17 % CPUTime : % 0.09/0.17 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.09/0.20 Running first-order model finding % 0.09/0.20 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.61/1.51 % (3945784)Will run a generic schedule for satisfiability detection. % 8.61/1.51 % (3945791)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2913105223:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi) % 8.61/1.51 % (3945790)% WARNING: option uhcvi not known. % 8.61/1.51 % (3945789)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2037918152_2999 on theBenchmark for (2999ds/0Mi) % 8.61/1.51 % (3945793)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1228832832:i=116_2999 on theBenchmark for (2999ds/116Mi) % 8.61/1.51 % (3945790)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1356268854:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi) % 8.61/1.51 % (3945792)dis+10_1_sil=32000:sp=arity:random_seed=690243342:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi) % 8.61/1.51 % (3945794)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1164834464:i=131_2999 on theBenchmark for (2999ds/131Mi) % 8.61/1.51 % (3945795)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2289027305:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi) % 8.61/1.51 % (3945793)Instruction limit reached! % 8.61/1.51 % (3945793)------------------------------ % 8.61/1.51 % (3945793)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.61/1.51 % (3945793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.61/1.51 % (3945793)CaDiCaL version: 2.1.3 % 8.61/1.51 % (3945793)Termination reason: Instruction limit % 8.61/1.51 % (3945793)Termination phase: Saturation % 8.61/1.51 % (3945793)Time elapsed: 0.057 s % 8.61/1.51 % (3945793)Peak memory usage: 12 MB % 8.61/1.51 % (3945793)Instructions burned: 116 (million) % 8.61/1.51 % (3945792)Instruction limit reached! % 8.61/1.51 % (3945792)------------------------------ % 8.61/1.51 % (3945792)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.61/1.51 % (3945792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.61/1.51 % (3945792)CaDiCaL version: 2.1.3 % 8.61/1.51 % (3945792)Termination reason: Instruction limit % 8.61/1.51 % (3945792)Termination phase: Saturation % 8.61/1.51 % (3945792)Time elapsed: 0.069 s % 8.61/1.51 % (3945792)Peak memory usage: 12 MB % 8.61/1.51 % (3945792)Instructions burned: 104 (million) % 8.61/1.51 % (3945795)Instruction limit reached! % 8.61/1.51 % (3945795)------------------------------ % 8.61/1.51 % (3945795)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.61/1.51 % (3945795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.61/1.51 % (3945795)CaDiCaL version: 2.1.3 % 8.61/1.51 % (3945795)Termination reason: Instruction limit % 8.61/1.51 % (3945795)Termination phase: Saturation % 8.61/1.51 % (3945795)Time elapsed: 0.065 s % 8.61/1.51 % (3945795)Peak memory usage: 12 MB % 8.61/1.51 % (3945795)Instructions burned: 159 (million) % 8.61/1.51 % (3945803)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3156625512:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi) % 8.61/1.51 % TRYING [1] % 8.61/1.51 % TRYING [2] % 8.61/1.51 % (3945794)Instruction limit reached! % 8.61/1.51 % (3945794)------------------------------ % 8.61/1.51 % (3945794)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.61/1.51 % (3945794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.61/1.51 % (3945794)CaDiCaL version: 2.1.3 % 8.61/1.51 % (3945794)Termination reason: Instruction limit % 8.61/1.51 % (3945794)Termination phase: Saturation % 8.61/1.51 % (3945794)Time elapsed: 0.083 s % 8.61/1.51 % (3945794)Peak memory usage: 13 MB % 8.61/1.51 % (3945794)Instructions burned: 132 (million) % 8.61/1.51 % (3945804)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2759546647:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi) % 8.61/1.51 % (3945805)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=1341232789:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi) % 8.61/1.51 % (3945807)ott-21_1_sil=16000:fs=off:random_seed=2969401379:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi) % 8.61/1.51 % (3945804)Instruction limit reached! % 8.61/1.51 % (3945804)------------------------------ % 8.61/1.51 % (3945804)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 8.61/1.51 % (3945804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.83/7.49 % (3945804)CaDiCaL version: 2.1.3 % 50.83/7.49 % (3945804)Termination reason: Instruction limit % 50.83/7.49 % (3945804)Termination phase: Saturation % 50.83/7.49 % (3945804)Time elapsed: 0.077 s % 50.83/7.49 % (3945804)Peak memory usage: 13 MB % 50.83/7.49 % (3945804)Instructions burned: 136 (million) % 50.83/7.49 % (3945825)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1234032609:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi) % 50.83/7.49 % TRYING [1] % 50.83/7.49 % (3945807)Instruction limit reached! % 50.83/7.49 % (3945807)------------------------------ % 50.83/7.49 % (3945807)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 50.83/7.49 % (3945807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.83/7.49 % (3945807)CaDiCaL version: 2.1.3 % 50.83/7.49 % (3945807)Termination reason: Instruction limit % 50.83/7.49 % (3945807)Termination phase: Saturation % 50.83/7.49 % (3945807)Time elapsed: 0.082 s % 50.83/7.49 % (3945807)Peak memory usage: 12 MB % 50.83/7.49 % (3945807)Instructions burned: 180 (million) % 50.83/7.49 % TRYING [2] % 50.83/7.49 % (3945834)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1830843768:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi) % 50.83/7.49 % TRYING [1] % 50.83/7.49 % (3945803)Instruction limit reached! % 50.83/7.49 % (3945803)------------------------------ % 50.83/7.49 % (3945803)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 50.83/7.49 % (3945803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.83/7.49 % (3945803)CaDiCaL version: 2.1.3 % 50.83/7.49 % (3945803)Termination reason: Instruction limit % 50.83/7.49 % (3945803)Termination phase: Finite model building constraint generation % 50.83/7.49 % (3945803)Time elapsed: 0.261 s % 50.83/7.49 % (3945803)Peak memory usage: 19 MB % 50.83/7.49 % (3945803)Instructions burned: 717 (million) % 50.83/7.49 % (3945886)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1534108190:i=1179_2995 on theBenchmark for (2995ds/1179Mi) % 50.83/7.49 % (3945805)Instruction limit reached! % 50.83/7.49 % (3945805)------------------------------ % 50.83/7.49 % (3945805)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 50.83/7.49 % (3945805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.83/7.49 % (3945805)CaDiCaL version: 2.1.3 % 50.83/7.49 % (3945805)Termination reason: Instruction limit % 50.83/7.49 % (3945805)Termination phase: Saturation % 50.83/7.49 % (3945805)Time elapsed: 0.303 s % 50.83/7.49 % (3945805)Peak memory usage: 16 MB % 50.83/7.49 % (3945805)Instructions burned: 686 (million) % 50.83/7.49 % (3945902)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=563121838:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi) % 50.83/7.49 % (3945825)Instruction limit reached! % 50.83/7.49 % (3945825)------------------------------ % 50.83/7.49 % (3945825)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 50.83/7.49 % (3945825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.83/7.49 % (3945825)CaDiCaL version: 2.1.3 % 50.83/7.49 % (3945825)Termination reason: Instruction limit % 50.83/7.49 % (3945825)Termination phase: Saturation % 50.83/7.49 % (3945825)Time elapsed: 0.270 s % 50.83/7.49 % (3945825)Peak memory usage: 13 MB % 50.83/7.49 % (3945825)Instructions burned: 477 (million) % 50.83/7.49 % (3945918)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=3527090751: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) % 50.83/7.49 % (3945902)Cannot represent all propositional literals internally % 50.83/7.49 % (3945902)Refutation not found, incomplete strategy % 50.83/7.49 % (3945902)------------------------------ % 50.83/7.49 % (3945902)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 50.83/7.49 % (3945902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 50.83/7.49 % (3945902)CaDiCaL version: 2.1.3 % 50.83/7.49 % (3945902)Termination reason: Refutation not found, incomplete strategy % 50.83/7.49 % (3945902)Time elapsed: 0.103 s % 50.83/7.49 % (3945902)Peak memory usage: 13 MB % 50.83/7.49 % (3945902)Instructions burned: 189 (million) % 50.83/7.49 % (3945902)------------------------------ % 50.83/7.49 % (3945902)------------------------------ % 50.83/7.49 % (3945935)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1908436034:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi) % 50.83/7.49 % (3945834)Instruction limit reached! % 50.83/7.49 % (3945834)------------------------------ % 101.27/14.59 % (3945834)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.27/14.59 % (3945834)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.27/14.59 % (3945834)CaDiCaL version: 2.1.3 % 101.27/14.59 % (3945834)Termination reason: Instruction limit % 101.27/14.59 % (3945834)Termination phase: Finite model building constraint generation % 101.27/14.59 % (3945834)Time elapsed: 0.439 s % 101.27/14.59 % (3945834)Peak memory usage: 93 MB % 101.27/14.59 % (3945834)Instructions burned: 867 (million) % 101.27/14.59 % (3945953)fmb+10_1_sil=64000:random_seed=896176444:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi) % 101.27/14.59 % TRYING [1] % 101.27/14.59 % (3945918)Instruction limit reached! % 101.27/14.59 % (3945918)------------------------------ % 101.27/14.59 % (3945918)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.27/14.59 % (3945918)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.27/14.59 % (3945918)CaDiCaL version: 2.1.3 % 101.27/14.59 % (3945918)Termination reason: Instruction limit % 101.27/14.59 % (3945918)Termination phase: Saturation % 101.27/14.59 % (3945918)Time elapsed: 0.359 s % 101.27/14.59 % (3945918)Peak memory usage: 15 MB % 101.27/14.59 % (3945918)Instructions burned: 693 (million) % 101.27/14.59 % (3945955)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3659839020:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi) % 101.27/14.59 % (3945955)Cannot represent all propositional literals internally % 101.27/14.59 % (3945955)Refutation not found, incomplete strategy % 101.27/14.59 % (3945955)------------------------------ % 101.27/14.59 % (3945955)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.27/14.59 % (3945955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.27/14.59 % (3945955)CaDiCaL version: 2.1.3 % 101.27/14.59 % (3945955)Termination reason: Refutation not found, incomplete strategy % 101.27/14.59 % (3945955)Time elapsed: 0.094 s % 101.27/14.59 % (3945955)Peak memory usage: 13 MB % 101.27/14.59 % (3945955)Instructions burned: 185 (million) % 101.27/14.59 % (3945955)------------------------------ % 101.27/14.59 % (3945955)------------------------------ % 101.27/14.59 % (3945957)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=571161774:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi) % 101.27/14.59 % (3945957)Cannot represent all propositional literals internally % 101.27/14.59 % (3945957)Refutation not found, incomplete strategy % 101.27/14.59 % (3945957)------------------------------ % 101.27/14.59 % (3945957)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.27/14.59 % (3945957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.27/14.59 % (3945957)CaDiCaL version: 2.1.3 % 101.27/14.59 % (3945957)Termination reason: Refutation not found, incomplete strategy % 101.27/14.59 % (3945957)Time elapsed: 0.094 s % 101.27/14.59 % (3945957)Peak memory usage: 13 MB % 101.27/14.59 % (3945957)Instructions burned: 185 (million) % 101.27/14.59 % (3945957)------------------------------ % 101.27/14.59 % (3945957)------------------------------ % 101.27/14.59 % (3945886)Instruction limit reached! % 101.27/14.59 % (3945886)------------------------------ % 101.27/14.59 % (3945886)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.27/14.59 % (3945886)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.27/14.59 % (3945886)CaDiCaL version: 2.1.3 % 101.27/14.59 % (3945886)Termination reason: Instruction limit % 101.27/14.59 % (3945886)Termination phase: Saturation % 101.27/14.59 % (3945886)Time elapsed: 0.715 s % 101.27/14.59 % (3945886)Peak memory usage: 27 MB % 101.27/14.59 % (3945886)Instructions burned: 1180 (million) % 101.27/14.59 % (3945959)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=4082649159:i=5131_2988 on theBenchmark for (2988ds/5131Mi) % 101.27/14.59 % (3945960)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3278762746:i=1472:ins=7:fdi=8:gsp=on_2988 on theBenchmark for (2988ds/1472Mi) % 101.27/14.59 % (3945935)Instruction limit reached! % 101.27/14.59 % (3945935)------------------------------ % 101.27/14.59 % (3945935)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 101.27/14.59 % (3945935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 101.27/14.59 % (3945935)CaDiCaL version: 2.1.3 % 101.27/14.59 % (3945935)Termination reason: Instruction limit % 101.27/14.59 % (3945935)Termination phase: Saturation % 101.27/14.59 % (3945935)Time elapsed: 0.623 s % 101.27/14.59 % (3945935)Peak memory usage: 19 MB % 101.27/14.59 % (3945935)Instructions burned: 880 (million) % 101.27/14.59 % (3945971)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2835683352:i=6324_2987 on theBenchmark for (2987ds/6324Mi) % 196.51/27.92 % (3945971)Cannot represent all propositional literals internally % 196.51/27.92 % (3945971)Refutation not found, incomplete strategy % 196.51/27.92 % (3945971)------------------------------ % 196.51/27.92 % (3945971)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 196.51/27.92 % (3945971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.51/27.92 % (3945971)CaDiCaL version: 2.1.3 % 196.51/27.92 % (3945971)Termination reason: Refutation not found, incomplete strategy % 196.51/27.92 % (3945971)Time elapsed: 0.133 s % 196.51/27.92 % (3945971)Peak memory usage: 13 MB % 196.51/27.92 % (3945971)Instructions burned: 162 (million) % 196.51/27.92 % (3945971)------------------------------ % 196.51/27.92 % (3945971)------------------------------ % 196.51/27.92 % (3945975)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2597466857:fmbsr=2.30978:i=2174_2985 on theBenchmark for (2985ds/2174Mi) % 196.51/27.92 % (3945960)Instruction limit reached! % 196.51/27.92 % (3945960)------------------------------ % 196.51/27.92 % (3945960)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 196.51/27.92 % (3945960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.51/27.92 % (3945960)CaDiCaL version: 2.1.3 % 196.51/27.92 % (3945960)Termination reason: Instruction limit % 196.51/27.92 % (3945960)Termination phase: Saturation % 196.51/27.92 % (3945960)Time elapsed: 1.087 s % 196.51/27.92 % (3945960)Peak memory usage: 24 MB % 196.51/27.92 % (3945960)Instructions burned: 1472 (million) % 196.51/27.92 % (3945999)ott-2_1_sil=16000:newcnf=on:random_seed=1617748723:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2977 on theBenchmark for (2977ds/869Mi) % 196.51/27.92 % (3945975)Cannot represent all propositional literals internally % 196.51/27.92 % (3945975)Refutation not found, incomplete strategy % 196.51/27.92 % (3945975)------------------------------ % 196.51/27.92 % (3945975)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 196.51/27.92 % (3945975)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.51/27.92 % (3945975)CaDiCaL version: 2.1.3 % 196.51/27.92 % (3945975)Termination reason: Refutation not found, incomplete strategy % 196.51/27.92 % (3945975)Time elapsed: 1.026 s % 196.51/27.92 % (3945975)Peak memory usage: 19 MB % 196.51/27.92 % (3945975)Instructions burned: 1217 (million) % 196.51/27.92 % (3945975)------------------------------ % 196.51/27.92 % (3945975)------------------------------ % 196.51/27.92 % (3946006)ott+10_1_sil=32000:tgt=ground:random_seed=3229757856:i=5114:av=off_2975 on theBenchmark for (2975ds/5114Mi) % 196.51/27.92 % (3945999)Instruction limit reached! % 196.51/27.92 % (3945999)------------------------------ % 196.51/27.92 % (3945999)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 196.51/27.92 % (3945999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.51/27.92 % (3945999)CaDiCaL version: 2.1.3 % 196.51/27.92 % (3945999)Termination reason: Instruction limit % 196.51/27.92 % (3945999)Termination phase: Saturation % 196.51/27.92 % (3945999)Time elapsed: 0.812 s % 196.51/27.92 % (3945999)Peak memory usage: 18 MB % 196.51/27.92 % (3945999)Instructions burned: 869 (million) % 196.51/27.92 % (3946013)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=4086428559:i=54282_2968 on theBenchmark for (2968ds/54282Mi) % 196.51/27.92 % TRYING [1] % 196.51/27.92 % TRYING [2] % 196.51/27.92 % (3945959)Instruction limit reached! % 196.51/27.92 % (3945959)------------------------------ % 196.51/27.92 % (3945959)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 196.51/27.92 % (3945959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.51/27.92 % (3945959)CaDiCaL version: 2.1.3 % 196.51/27.92 % (3945959)Termination reason: Instruction limit % 196.51/27.92 % (3945959)Termination phase: Saturation % 196.51/27.92 % (3945959)Time elapsed: 4.330 s % 196.51/27.92 % (3945959)Peak memory usage: 48 MB % 196.51/27.92 % (3945959)Instructions burned: 5131 (million) % 196.51/27.92 % (3946032)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2496773345:i=3512:aac=none_2945 on theBenchmark for (2945ds/3512Mi) % 196.51/27.92 % (3946006)Instruction limit reached! % 196.51/27.92 % (3946006)------------------------------ % 196.51/27.92 % (3946006)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 196.51/27.92 % (3946006)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 196.51/27.92 % (3946006)CaDiCaL version: 2.1.3 % 196.51/27.92 % (3946006)Termination reason: Instruction limit % 196.51/27.92 % (3946006)Termination phase: Saturation % 300.33/42.54 % (3946006)Time elapsed: 4.758 s % 300.33/42.54 % (3946006)Peak memory usage: 86 MB % 300.33/42.54 % (3946006)Instructions burned: 5115 (million) % 300.33/42.54 % (3946035)dis+21_1_sil=32000:sas=cadical:random_seed=2999402964:i=3773:amm=off_2927 on theBenchmark for (2927ds/3773Mi) % 300.33/42.54 % (3946032)Instruction limit reached! % 300.33/42.54 % (3946032)------------------------------ % 300.33/42.54 % (3946032)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.33/42.54 % (3946032)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.33/42.54 % (3946032)CaDiCaL version: 2.1.3 % 300.33/42.54 % (3946032)Termination reason: Instruction limit % 300.33/42.54 % (3946032)Termination phase: Saturation % 300.33/42.54 % (3946032)Time elapsed: 3.087 s % 300.33/42.54 % (3946032)Peak memory usage: 38 MB % 300.33/42.54 % (3946032)Instructions burned: 3513 (million) % 300.33/42.54 % (3946046)ott+11_1_sil=16000:gs=on:random_seed=1943065163:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2913 on theBenchmark for (2913ds/2251Mi) % 300.33/42.54 % (3946046)Instruction limit reached! % 300.33/42.54 % (3946046)------------------------------ % 300.33/42.54 % (3946046)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.33/42.54 % (3946046)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.33/42.54 % (3946046)CaDiCaL version: 2.1.3 % 300.33/42.54 % (3946046)Termination reason: Instruction limit % 300.33/42.54 % (3946046)Termination phase: Saturation % 300.33/42.54 % (3946046)Time elapsed: 1.693 s % 300.33/42.54 % (3946046)Peak memory usage: 16 MB % 300.33/42.54 % (3946046)Instructions burned: 2252 (million) % 300.33/42.54 % (3946050)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3099678138:fmbsr=1.6:i=67534_2896 on theBenchmark for (2896ds/67534Mi) % 300.33/42.54 % (3946050)Cannot represent all propositional literals internally % 300.33/42.54 % (3946050)Refutation not found, incomplete strategy % 300.33/42.54 % (3946050)------------------------------ % 300.33/42.54 % (3946050)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.33/42.54 % (3946050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.33/42.54 % (3946050)CaDiCaL version: 2.1.3 % 300.33/42.54 % (3946050)Termination reason: Refutation not found, incomplete strategy % 300.33/42.54 % (3946050)Time elapsed: 0.191 s % 300.33/42.54 % (3946050)Peak memory usage: 13 MB % 300.33/42.54 % (3946050)Instructions burned: 225 (million) % 300.33/42.54 % (3946050)------------------------------ % 300.33/42.54 % (3946050)------------------------------ % 300.33/42.54 % (3946052)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1283825838:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2894 on theBenchmark for (2894ds/4591Mi) % 300.33/42.54 % (3946035)Instruction limit reached! % 300.33/42.54 % (3946035)------------------------------ % 300.33/42.54 % (3946035)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.33/42.54 % (3946035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.33/42.54 % (3946035)CaDiCaL version: 2.1.3 % 300.33/42.54 % (3946035)Termination reason: Instruction limit % 300.33/42.54 % (3946035)Termination phase: Saturation % 300.33/42.54 % (3946035)Time elapsed: 3.316 s % 300.33/42.54 % (3946035)Peak memory usage: 42 MB % 300.33/42.54 % (3946035)Instructions burned: 3774 (million) % 300.33/42.54 % (3946054)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2912006422:i=29340_2893 on theBenchmark for (2893ds/29340Mi) % 300.33/42.54 % (3946052)Instruction limit reached! % 300.33/42.54 % (3946052)------------------------------ % 300.33/42.54 % (3946052)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.33/42.54 % (3946052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.33/42.54 % (3946052)CaDiCaL version: 2.1.3 % 300.33/42.54 % (3946052)Termination reason: Instruction limit % 300.33/42.54 % (3946052)Termination phase: Saturation % 300.33/42.54 % (3946052)Time elapsed: 1.556 s % 300.33/42.54 % (3946052)Peak memory usage: 28 MB % 300.33/42.54 % (3946052)Instructions burned: 4593 (million) % 300.33/42.54 % (3946066)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3593062238:i=5211_2878 on theBenchmark for (2878ds/5211Mi) % 300.33/42.54 % (3946066)Instruction limit reached! % 300.33/42.54 % (3946066)------------------------------ % 300.33/42.54 % (3946066)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.33/42.54 % (3946066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.33/42.54 % (3946066)CaDiCaL version: 2.1.3 % 300.33/42.54 % (3946066)Termination reason: Instruction limit % 300.33/42.54 % (3946066)Termination phase: Saturation % 300.33/42.54 % (3946066)Time elapsed: 2.227 s % 300.33/42.54 % (3946066)Peak memory usage: 50 MB % 300.33/42.54 % (3946066)Instructions burned: 5212 (million) % 300.33/42.54 % (3946074)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3586599384:i=5497:nm=2_2856 on theBenchmark for (2856ds/5497Mi) % 300.33/42.54 % (3946074)Cannot represent all propositional literals internally % 300.33/42.54 % (3946074)Refutation not found, incomplete strategy % 300.33/42.54 % (3946074)------------------------------ % 300.33/42.54 % (3946074)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.33/42.54 % (3946074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.33/42.54 % (3946074)CaDiCaL version: 2.1.3 % 300.33/42.54 % (3946074)Termination reason: Refutation not found, incomplete strategy % 300.33/42.54 % (3946074)Time elapsed: 0.075 s % 300.33/42.54 % (3946074)Peak memory usage: 13 MB % 300.33/42.54 % (3946074)Instructions burned: 162 (million) % 300.33/42.54 % (3946074)------------------------------ % 300.33/42.54 % (3946074)------------------------------ % 300.33/42.54 % (3946077)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3741943663:fmbsr=2:i=46332_2855 on theBenchmark for (2855ds/46332Mi) % 300.33/42.54 % (3946077)Cannot represent all propositional literals internally % 300.33/42.54 % (3946077)Refutation not found, incomplete strategy % 300.33/42.54 % (3946077)------------------------------ % 300.33/42.54 % (3946077)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.33/42.54 % (3946077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.33/42.54 % (3946077)CaDiCaL version: 2.1.3 % 300.33/42.54 % (3946077)Termination reason: Refutation not found, incomplete strategy % 300.33/42.54 % (3946077)Time elapsed: 0.178 s % 300.33/42.54 % (3946077)Peak memory usage: 13 MB % 300.33/42.54 % (3946077)Instructions burned: 225 (million) % 300.33/42.54 % (3946077)------------------------------ % 300.33/42.54 % (3946077)------------------------------ % 300.33/42.54 % (3946080)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2083729677:i=14071_2853 on theBenchmark for (2853ds/14071Mi) % 300.33/42.54 % (3946080)Cannot represent all propositional literals internally % 300.33/42.54 % (3946080)Refutation not found, incomplete strategy % 300.33/42.54 % (3946080)------------------------------ % 300.33/42.54 % (3946080)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.33/42.54 % (3946080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.33/42.54 % (3946080)CaDiCaL version: 2.1.3 % 300.33/42.54 % (3946080)Termination reason: Refutation not found, incomplete strategy % 300.33/42.54 % (3946080)Time elapsed: 0.186 s % 300.33/42.54 % (3946080)Peak memory usage: 13 MB % 300.33/42.54 % (3946080)Instructions burned: 193 (million) % 300.33/42.54 % (3946080)------------------------------ % 300.33/42.54 % (3946080)------------------------------ % 300.33/42.54 % (3946082)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=980280710:i=22565:add=on:rawr=on_2850 on theBenchmark for (2850ds/22565Mi) % 300.33/42.54 % (3945953)Instruction limit reached! % 300.33/42.54 % (3945953)------------------------------ % 300.33/42.54 % (3945953)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.33/42.54 % (3945953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.33/42.54 % (3945953)CaDiCaL version: 2.1.3 % 300.33/42.54 % (3945953)Termination reason: Instruction limit % 300.33/42.54 % (3945953)Termination phase: Finite model building constraint generation % 300.33/42.54 % (3945953)Time elapsed: 18.290 s % 300.33/42.54 % (3945953)Peak memory usage: 2123 MB % 300.33/42.54 % (3945953)Instructions burned: 22062 (million) % 300.33/42.54 % (3946090)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1157955045:i=8173:av=off_2803 on theBenchmark for (2803ds/8173Mi) % 300.33/42.54 % (3946090)Instruction limit reached! % 300.33/42.54 % (3946090)------------------------------ % 300.33/42.54 % (3946090)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200) % 300.33/42.54 % (3946090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 300.33/42.54 % (3946090)CaDiCaL version: 2.1.3 % 300.33/42.54 % (3946090)Termination reason: Instruction limit % 300.33/42.54 % (3946090)Termination phase: Saturation % 300.33/42.54 % (3946090)Time elapsed: 8.017 s % 300.33/42.54 % (3946090)Peak memory usage: 132 MB % 300.33/42.54 % (3946090)Instructions burned: 8173 (million) % 300.33/42.54 % (3946114)dis+10_16:1_sil=16000:random_seed=1519881331:i=9155:fsr=of % 300.33/42.54 Terminated % 300.33/42.54 % Vampire exiting % 300.33/42.54 Terminated %------------------------------------------------------------------------------