%------------------------------------------------------------------------------ % File : Vampire---5.0.1 % Problem : SWX123_1 : TPTP v9.3.1. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % Computer : n014.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Sep 29 01:45:55 PM UTC 2026 % Result : Timeout 289.51s 41.43s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : SWX123_1 : TPTP v9.3.1. Released v9.3.0. % 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.10/0.18 % Computer : n014.cluster.edu % 0.10/0.18 % Model : x86_64 x86_64 % 0.10/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.18 % Memory : 8046.5625MB % 0.10/0.18 % OS : Linux 6.8.0-71-generic % 0.10/0.18 % CPULimit : 300 % 0.10/0.18 % WCLimit : 300 % 0.10/0.18 % DateTime : Mon Sep 28 15:02:15 UTC 2026 % 0.10/0.18 % CPUTime : % 0.10/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM % 0.10/0.22 Running first-order theorem proving % 0.10/0.22 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 3.21/1.19 % (1835606)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule. % 3.21/1.19 % (1835751)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=4140281725:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi) % 3.21/1.19 % (1835751)Instruction limit reached! % 3.21/1.19 % (1835751)------------------------------ % 3.21/1.19 % (1835751)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.21/1.19 % (1835751)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.21/1.19 % (1835751)CaDiCaL version: 2.1.3 % 3.21/1.19 % (1835751)Termination reason: Instruction limit % 3.21/1.19 % (1835751)Termination phase: SInE selection % 3.21/1.19 % (1835751)Time elapsed: 0.002 s % 3.21/1.19 % (1835751)Peak memory usage: 85 MB % 3.21/1.19 % (1835751)Instructions burned: 8 (million) % 3.21/1.19 % (1835753)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=1386123888:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi) % 3.21/1.19 % (1835752)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=1809092367:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi) % 3.21/1.19 % (1835754)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=4237676385:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi) % 3.21/1.19 % (1835750)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=428365121:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi) % 3.21/1.19 % (1835748)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=4179230389:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi) % 3.21/1.19 % (1835749)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3401054900:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi) % 3.21/1.19 % (1835752)Instruction limit reached! % 3.21/1.19 % (1835752)------------------------------ % 3.21/1.19 % (1835752)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.21/1.19 % (1835752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.21/1.19 % (1835752)CaDiCaL version: 2.1.3 % 3.21/1.19 % (1835752)Termination reason: Instruction limit % 3.21/1.19 % (1835752)Termination phase: Including theory axioms % 3.21/1.19 % (1835752)Time elapsed: 0.002 s % 3.21/1.19 % (1835752)Peak memory usage: 85 MB % 3.21/1.19 % (1835752)Instructions burned: 4 (million) % 3.21/1.19 % (1835748)Instruction limit reached! % 3.21/1.19 % (1835748)------------------------------ % 3.21/1.19 % (1835748)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.21/1.19 % (1835748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.21/1.19 % (1835748)CaDiCaL version: 2.1.3 % 3.21/1.19 % (1835748)Termination reason: Instruction limit % 3.21/1.19 % (1835748)Termination phase: SInE selection % 3.21/1.19 % (1835748)Time elapsed: 0.005 s % 3.21/1.19 % (1835748)Peak memory usage: 85 MB % 3.21/1.19 % (1835748)Instructions burned: 12 (million) % 3.21/1.19 % (1835754)Instruction limit reached! % 3.21/1.19 % (1835754)------------------------------ % 3.21/1.19 % (1835754)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.21/1.19 % (1835754)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.21/1.20 % (1835754)CaDiCaL version: 2.1.3 % 3.21/1.20 % (1835754)Termination reason: Instruction limit % 3.21/1.20 % (1835754)Termination phase: Saturation % 3.21/1.20 % (1835754)Time elapsed: 0.036 s % 3.21/1.20 % (1835754)Peak memory usage: 112 MB % 3.21/1.20 % (1835754)Instructions burned: 34 (million) % 3.21/1.20 % (1835753)Instruction limit reached! % 3.21/1.20 % (1835753)------------------------------ % 3.21/1.20 % (1835753)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 3.21/1.20 % (1835753)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 3.21/1.20 % (1835753)CaDiCaL version: 2.1.3 % 3.21/1.20 % (1835753)Termination reason: Instruction limit % 3.21/1.20 % (1835753)Termination phase: Saturation % 3.21/1.20 % (1835753)Time elapsed: 0.043 s % 3.21/1.20 % (1835753)Peak memory usage: 111 MB % 3.21/1.20 % (1835753)Instructions burned: 48 (million) % 3.21/1.20 % (1835756)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=651036292:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi) % 3.21/1.20 % (1835756)Refutation not found, incomplete strategy % 3.21/1.20 % (1835756)------------------------------ % 4.51/1.40 % (1835756)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.51/1.40 % (1835756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.51/1.40 % (1835756)CaDiCaL version: 2.1.3 % 4.51/1.40 % (1835756)Termination reason: Refutation not found, incomplete strategy % 4.51/1.40 % (1835756)Time elapsed: 0.002 s % 4.51/1.40 % (1835756)Peak memory usage: 88 MB % 4.51/1.40 % (1835756)Instructions burned: 8 (million) % 4.51/1.40 % (1835750)Instruction limit reached! % 4.51/1.40 % (1835750)------------------------------ % 4.51/1.40 % (1835750)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.51/1.40 % (1835750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.51/1.40 % (1835750)CaDiCaL version: 2.1.3 % 4.51/1.40 % (1835750)Termination reason: Instruction limit % 4.51/1.40 % (1835750)Termination phase: Saturation % 4.51/1.40 % (1835750)Time elapsed: 0.107 s % 4.51/1.40 % (1835750)Peak memory usage: 117 MB % 4.51/1.40 % (1835750)Instructions burned: 202 (million) % 4.51/1.40 % (1835749)Instruction limit reached! % 4.51/1.40 % (1835749)------------------------------ % 4.51/1.40 % (1835749)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.51/1.40 % (1835749)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.51/1.40 % (1835749)CaDiCaL version: 2.1.3 % 4.51/1.40 % (1835749)Termination reason: Instruction limit % 4.51/1.40 % (1835749)Termination phase: Saturation % 4.51/1.40 % (1835749)Time elapsed: 0.152 s % 4.51/1.40 % (1835749)Peak memory usage: 116 MB % 4.51/1.40 % (1835749)Instructions burned: 311 (million) % 4.51/1.40 % (1835764)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2250826553:cond=on:i=16:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2998 on theBenchmark for (2998ds/16Mi) % 4.51/1.40 % (1835763)dis+1011_2:1_to=kbo:sil=128000:tgt=full:fde=none:si=on:norm_ineq=on:spb=goal_then_units:tha=some:nwc=2:sac=on:random_seed=3966663838:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi) % 4.51/1.40 % (1835764)Instruction limit reached! % 4.51/1.40 % (1835764)------------------------------ % 4.51/1.40 % (1835764)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.51/1.40 % (1835764)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.51/1.40 % (1835764)CaDiCaL version: 2.1.3 % 4.51/1.40 % (1835764)Termination reason: Instruction limit % 4.51/1.40 % (1835764)Termination phase: Saturation % 4.51/1.40 % (1835764)Time elapsed: 0.008 s % 4.51/1.40 % (1835764)Peak memory usage: 89 MB % 4.51/1.40 % (1835764)Instructions burned: 18 (million) % 4.51/1.40 % (1835763)Instruction limit reached! % 4.51/1.40 % (1835763)------------------------------ % 4.51/1.40 % (1835763)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.51/1.40 % (1835763)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.51/1.40 % (1835763)CaDiCaL version: 2.1.3 % 4.51/1.40 % (1835763)Termination reason: Instruction limit % 4.51/1.40 % (1835763)Termination phase: Saturation % 4.51/1.40 % (1835763)Time elapsed: 0.015 s % 4.51/1.40 % (1835763)Peak memory usage: 88 MB % 4.51/1.40 % (1835763)Instructions burned: 31 (million) % 4.51/1.40 % (1835765)dis+1011_1_prc=on:drc=off:si=on:sac=on:random_seed=1336785160:i=24:canc=force:rtra=on_2997 on theBenchmark for (2997ds/24Mi) % 4.51/1.40 % (1835766)ott+1010_8_to=lpo:sil=128000:si=on:norm_ineq=on:sp=unary_frequency:sos=on:gve=cautious:spb=goal_then_units:uwa=alasca_main_floor:tha=some:random_seed=3026278956:i=27:canc=cautious:fsr=off:rtra=on_2997 on theBenchmark for (2997ds/27Mi) % 4.51/1.40 % (1835765)Instruction limit reached! % 4.51/1.40 % (1835765)------------------------------ % 4.51/1.40 % (1835765)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.51/1.40 % (1835765)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 4.51/1.40 % (1835765)CaDiCaL version: 2.1.3 % 4.51/1.40 % (1835765)Termination reason: Instruction limit % 4.51/1.40 % (1835765)Termination phase: Saturation % 4.51/1.40 % (1835765)Time elapsed: 0.011 s % 4.51/1.40 % (1835765)Peak memory usage: 88 MB % 4.51/1.40 % (1835765)Instructions burned: 25 (million) % 4.51/1.40 % (1835766)Instruction limit reached! % 4.51/1.40 % (1835766)------------------------------ % 4.51/1.40 % (1835766)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 4.51/1.40 % (1835766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.81/1.56 % (1835766)CaDiCaL version: 2.1.3 % 5.81/1.56 % (1835766)Termination reason: Instruction limit % 5.81/1.56 % (1835766)Termination phase: Saturation % 5.81/1.56 % (1835766)Time elapsed: 0.012 s % 5.81/1.56 % (1835766)Peak memory usage: 88 MB % 5.81/1.56 % (1835766)Instructions burned: 27 (million) % 5.81/1.56 % (1835756)------------------------------ % 5.81/1.56 % (1835756)------------------------------ % 5.81/1.56 % (1835768)dis+1002_24_to=kbo:sil=128000:si=on:random_seed=2487784294:i=85:gtgl=4:rtra=on:gtg=exists_sym_2997 on theBenchmark for (2997ds/85Mi) % 5.81/1.56 % (1835769)ott+1002_1_si=on:sp=occurrence:spb=goal:lcm=predicate:random_seed=1988049181:i=2:bd=preordered:nm=2:ins=3:rtra=on:inst=on:tar=off_2996 on theBenchmark for (2996ds/2Mi) % 5.81/1.56 % (1835769)Instruction limit reached! % 5.81/1.56 % (1835769)------------------------------ % 5.81/1.56 % (1835769)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.81/1.56 % (1835769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.81/1.56 % (1835769)CaDiCaL version: 2.1.3 % 5.81/1.56 % (1835769)Termination reason: Instruction limit % 5.81/1.56 % (1835769)Termination phase: Property scanning % 5.81/1.56 % (1835769)Time elapsed: 0.002 s % 5.81/1.56 % (1835769)Peak memory usage: 85 MB % 5.81/1.56 % (1835769)Instructions burned: 4 (million) % 5.81/1.56 % (1835768)Instruction limit reached! % 5.81/1.56 % (1835768)------------------------------ % 5.81/1.56 % (1835768)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.81/1.56 % (1835768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.81/1.56 % (1835768)CaDiCaL version: 2.1.3 % 5.81/1.56 % (1835768)Termination reason: Instruction limit % 5.81/1.56 % (1835768)Termination phase: Saturation % 5.81/1.56 % (1835768)Time elapsed: 0.048 s % 5.81/1.56 % (1835768)Peak memory usage: 90 MB % 5.81/1.56 % (1835768)Instructions burned: 87 (million) % 5.81/1.56 % (1835773)lrs+10_2_to=lpo:sil=64000:si=on:sos=on:gve=force:lcm=reverse:uwa=one_side_interpreted:random_seed=3239144312:i=4:ep=RST:ins=2:rtra=on_2996 on theBenchmark for (2996ds/4Mi) % 5.81/1.56 % (1835772)dis+1010_1_to=kbo:sil=128000:tgt=full:si=on:tha=off:random_seed=2290947539:i=181:rtra=on:ss=axioms:ev=cautious_2996 on theBenchmark for (2996ds/181Mi) % 5.81/1.56 % (1835773)Instruction limit reached! % 5.81/1.56 % (1835773)------------------------------ % 5.81/1.56 % (1835773)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.81/1.56 % (1835773)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.81/1.56 % (1835773)CaDiCaL version: 2.1.3 % 5.81/1.56 % (1835773)Termination reason: Instruction limit % 5.81/1.56 % (1835773)Termination phase: Including theory axioms % 5.81/1.56 % (1835773)Time elapsed: 0.002 s % 5.81/1.56 % (1835773)Peak memory usage: 85 MB % 5.81/1.56 % (1835773)Instructions burned: 4 (million) % 5.81/1.56 % (1835772)Refutation not found, incomplete strategy % 5.81/1.56 % (1835772)------------------------------ % 5.81/1.56 % (1835772)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.81/1.56 % (1835772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.81/1.56 % (1835772)CaDiCaL version: 2.1.3 % 5.81/1.56 % (1835772)Termination reason: Refutation not found, incomplete strategy % 5.81/1.56 % (1835772)Time elapsed: 0.004 s % 5.81/1.56 % (1835772)Peak memory usage: 87 MB % 5.81/1.56 % (1835772)Instructions burned: 7 (million) % 5.81/1.56 % (1835778)ott+1011_1_to=kbo:plsq=on:drc=off:si=on:plsqr=32,1:sp=const_frequency:sos=all:uwa=one_side_interpreted:sac=on:random_seed=1492211664:i=8:ep=RST:nm=16:rtra=on:gtg=exists_top_2995 on theBenchmark for (2995ds/8Mi) % 5.81/1.56 % (1835778)Instruction limit reached! % 5.81/1.56 % (1835778)------------------------------ % 5.81/1.56 % (1835778)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 5.81/1.56 % (1835778)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 5.81/1.56 % (1835778)CaDiCaL version: 2.1.3 % 5.81/1.56 % (1835778)Termination reason: Instruction limit % 5.81/1.56 % (1835778)Termination phase: Property scanning % 5.81/1.56 % (1835778)Time elapsed: 0.002 s % 5.81/1.56 % (1835778)Peak memory usage: 85 MB % 5.81/1.56 % (1835778)Instructions burned: 9 (million) % 5.81/1.56 % (1835777)lrs+10_1_thi=all:si=on:fd=off:random_seed=2872549314:i=53:rtra=on:gtg=all_2996 on theBenchmark for (2996ds/53Mi) % 5.81/1.56 % (1835776)dis+1010_128_isp=bottom:to=lpo:thi=overlap:prc=on:sas=z3:si=on:fd=preordered:random_seed=1772346538:i=66:thsqd=64:thsqc=16:rtra=on:thsq=on:ev=force_2996 on theBenchmark for (2996ds/66Mi) % 6.83/1.75 % (1835777)Instruction limit reached! % 6.83/1.75 % (1835777)------------------------------ % 6.83/1.75 % (1835777)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.83/1.75 % (1835777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.83/1.75 % (1835777)CaDiCaL version: 2.1.3 % 6.83/1.75 % (1835777)Termination reason: Instruction limit % 6.83/1.75 % (1835777)Termination phase: Saturation % 6.83/1.75 % (1835777)Time elapsed: 0.048 s % 6.83/1.75 % (1835777)Peak memory usage: 116 MB % 6.83/1.75 % (1835777)Instructions burned: 54 (million) % 6.83/1.75 % (1835776)Instruction limit reached! % 6.83/1.75 % (1835776)------------------------------ % 6.83/1.75 % (1835776)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.83/1.75 % (1835776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.83/1.75 % (1835776)CaDiCaL version: 2.1.3 % 6.83/1.75 % (1835776)Termination reason: Instruction limit % 6.83/1.75 % (1835776)Termination phase: Saturation % 6.83/1.75 % (1835776)Time elapsed: 0.070 s % 6.83/1.75 % (1835776)Peak memory usage: 129 MB % 6.83/1.75 % (1835776)Instructions burned: 66 (million) % 6.83/1.75 % (1835781)lrs+10_1_to=lakbo:sil=128000:si=on:alasca=on:sp=occurrence:random_seed=1626706969:st=3:i=2:rtra=on:ss=axioms_2995 on theBenchmark for (2995ds/2Mi) % 6.83/1.75 % (1835782)dis+1002_1_to=lpo:sil=64000:si=on:flr=on:random_seed=3414477523:i=2:doe=on:canc=force:asg=cautious:rtra=on_2994 on theBenchmark for (2994ds/2Mi) % 6.83/1.75 % (1835781)Instruction limit reached! % 6.83/1.75 % (1835781)------------------------------ % 6.83/1.75 % (1835781)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.83/1.75 % (1835781)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.83/1.75 % (1835781)CaDiCaL version: 2.1.3 % 6.83/1.75 % (1835781)Termination reason: Instruction limit % 6.83/1.75 % (1835781)Termination phase: Property scanning % 6.83/1.75 % (1835781)Time elapsed: 0.002 s % 6.83/1.75 % (1835781)Peak memory usage: 84 MB % 6.83/1.75 % (1835781)Instructions burned: 4 (million) % 6.83/1.75 % (1835782)Instruction limit reached! % 6.83/1.75 % (1835782)------------------------------ % 6.83/1.75 % (1835782)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.83/1.75 % (1835782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.83/1.75 % (1835782)CaDiCaL version: 2.1.3 % 6.83/1.75 % (1835782)Termination reason: Instruction limit % 6.83/1.75 % (1835782)Termination phase: Property scanning % 6.83/1.75 % (1835782)Time elapsed: 0.002 s % 6.83/1.75 % (1835782)Peak memory usage: 85 MB % 6.83/1.75 % (1835782)Instructions burned: 4 (million) % 6.83/1.75 % (1835789)dis+10_1_si=on:random_seed=2507892394:i=10:ep=R:rtra=on_2994 on theBenchmark for (2994ds/10Mi) % 6.83/1.75 % (1835789)Instruction limit reached! % 6.83/1.75 % (1835789)------------------------------ % 6.83/1.75 % (1835789)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.83/1.75 % (1835789)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.83/1.75 % (1835789)CaDiCaL version: 2.1.3 % 6.83/1.75 % (1835789)Termination reason: Instruction limit % 6.83/1.75 % (1835789)Termination phase: Property scanning % 6.83/1.75 % (1835789)Time elapsed: 0.003 s % 6.83/1.75 % (1835789)Peak memory usage: 86 MB % 6.83/1.75 % (1835789)Instructions burned: 14 (million) % 6.83/1.75 % (1835785)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=4260800198:i=127:doe=on:rtra=on_2994 on theBenchmark for (2994ds/127Mi) % 6.83/1.75 % (1835790)lrs-1011_64_to=lpo:si=on:sp=unary_first:sos=on:br=off:random_seed=882754405:i=26:canc=cautious:av=off:rtra=on_2994 on theBenchmark for (2994ds/26Mi) % 6.83/1.75 % (1835785)Instruction limit reached! % 6.83/1.75 % (1835785)------------------------------ % 6.83/1.75 % (1835785)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 6.83/1.75 % (1835785)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 6.83/1.75 % (1835785)CaDiCaL version: 2.1.3 % 6.83/1.75 % (1835785)Termination reason: Instruction limit % 6.83/1.75 % (1835785)Termination phase: Saturation % 6.83/1.75 % (1835785)Time elapsed: 0.073 s % 6.83/1.75 % (1835785)Peak memory usage: 113 MB % 6.83/1.75 % (1835785)Instructions burned: 127 (million) % 6.83/1.75 % (1835790)Instruction limit reached! % 6.83/1.75 % (1835790)------------------------------ % 6.83/1.75 % (1835790)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.24/1.97 % (1835790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.24/1.97 % (1835790)CaDiCaL version: 2.1.3 % 8.24/1.97 % (1835790)Termination reason: Instruction limit % 8.24/1.97 % (1835790)Termination phase: Saturation % 8.24/1.97 % (1835790)Time elapsed: 0.012 s % 8.24/1.97 % (1835790)Peak memory usage: 88 MB % 8.24/1.97 % (1835790)Instructions burned: 26 (million) % 8.24/1.97 % (1835772)------------------------------ % 8.24/1.97 % (1835772)------------------------------ % 8.24/1.97 % (1835791)dis+1011_5_anc=all:tgt=full:si=on:sp=const_frequency:spb=non_intro:fd=preordered:sac=on:random_seed=811191348:avsq=on:i=35:doe=on:thsqd=64:nm=64:fsr=off:thsqc=32:rtra=on:tac=light:ss=included:thsq=on:ev=off:sgt=32_2993 on theBenchmark for (2993ds/35Mi) % 8.24/1.97 % (1835798)lrs-1011_1_to=kbo:sil=128000:prc=on:si=on:fs=off:tha=off:random_seed=1095278560:i=370:ep=RS:fsr=off:rtra=on_2993 on theBenchmark for (2993ds/370Mi) % 8.24/1.97 % (1835798)Refutation not found, incomplete strategy % 8.24/1.97 % (1835798)------------------------------ % 8.24/1.97 % (1835798)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.24/1.97 % (1835798)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.24/1.97 % (1835798)CaDiCaL version: 2.1.3 % 8.24/1.97 % (1835798)Termination reason: Refutation not found, incomplete strategy % 8.24/1.97 % (1835798)Time elapsed: 0.006 s % 8.24/1.97 % (1835798)Peak memory usage: 89 MB % 8.24/1.97 % (1835798)Instructions burned: 25 (million) % 8.24/1.97 % (1835791)Instruction limit reached! % 8.24/1.97 % (1835791)------------------------------ % 8.24/1.97 % (1835791)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.24/1.97 % (1835791)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.24/1.97 % (1835791)CaDiCaL version: 2.1.3 % 8.24/1.97 % (1835791)Termination reason: Instruction limit % 8.24/1.97 % (1835791)Termination phase: Saturation % 8.24/1.97 % (1835791)Time elapsed: 0.017 s % 8.24/1.97 % (1835791)Peak memory usage: 89 MB % 8.24/1.97 % (1835791)Instructions burned: 35 (million) % 8.24/1.97 % (1835794)ott+10_8:1_to=lpo:sil=128000:si=on:fs=off:spb=goal_then_units:uwa=alasca_main:random_seed=1468859350:i=2:fsr=off:rtra=on:inst=on_2993 on theBenchmark for (2993ds/2Mi) % 8.24/1.97 % (1835795)dis+21_1_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=off:s2agt=16:random_seed=1346655408:s2a=on:i=8:kws=inv_precedence:doe=on:rtra=on_2993 on theBenchmark for (2993ds/8Mi) % 8.24/1.97 % (1835794)Instruction limit reached! % 8.24/1.97 % (1835794)------------------------------ % 8.24/1.97 % (1835794)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.24/1.97 % (1835794)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.24/1.97 % (1835794)CaDiCaL version: 2.1.3 % 8.24/1.97 % (1835794)Termination reason: Instruction limit % 8.24/1.97 % (1835794)Termination phase: Including theory axioms % 8.24/1.97 % (1835794)Time elapsed: 0.002 s % 8.24/1.97 % (1835794)Peak memory usage: 85 MB % 8.24/1.97 % (1835794)Instructions burned: 4 (million) % 8.24/1.97 % (1835795)Instruction limit reached! % 8.24/1.97 % (1835795)------------------------------ % 8.24/1.97 % (1835795)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.24/1.97 % (1835795)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.24/1.97 % (1835795)CaDiCaL version: 2.1.3 % 8.24/1.97 % (1835795)Termination reason: Instruction limit % 8.24/1.97 % (1835795)Termination phase: Property scanning % 8.24/1.97 % (1835795)Time elapsed: 0.004 s % 8.24/1.97 % (1835795)Peak memory usage: 85 MB % 8.24/1.97 % (1835795)Instructions burned: 9 (million) % 8.24/1.97 % (1835800)ott+1002_1_to=lpo:thi=overlap:prc=on:bsd=on:si=on:gve=cautious:thigen=on:tha=some:random_seed=3869075400:i=13:av=off:rtra=on:gtg=exists_sym:ev=force_2992 on theBenchmark for (2992ds/13Mi) % 8.24/1.97 % (1835801)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=1591209620:i=226:rtra=on:gtg=position:ss=axioms_2992 on theBenchmark for (2992ds/226Mi) % 8.24/1.97 % (1835800)Instruction limit reached! % 8.24/1.97 % (1835800)------------------------------ % 8.24/1.97 % (1835800)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 8.24/1.97 % (1835800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 8.24/1.97 % (1835800)CaDiCaL version: 2.1.3 % 8.24/1.97 % (1835800)Termination reason: Instruction limit % 8.24/1.97 % (1835800)Termination phase: Property scanning % 10.62/2.29 % (1835800)Time elapsed: 0.006 s % 10.62/2.29 % (1835800)Peak memory usage: 85 MB % 10.62/2.29 % (1835800)Instructions burned: 15 (million) % 10.62/2.29 % (1835804)lrs+1010_5_to=lpo:sil=128000:si=on:sp=const_frequency:sos=theory:tha=off:random_seed=2674632324:i=10:rtra=on_2992 on theBenchmark for (2992ds/10Mi) % 10.62/2.29 % (1835804)Instruction limit reached! % 10.62/2.29 % (1835804)------------------------------ % 10.62/2.29 % (1835804)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.62/2.29 % (1835804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.62/2.29 % (1835804)CaDiCaL version: 2.1.3 % 10.62/2.29 % (1835804)Termination reason: Instruction limit % 10.62/2.29 % (1835804)Termination phase: Saturation % 10.62/2.29 % (1835804)Time elapsed: 0.005 s % 10.62/2.29 % (1835804)Peak memory usage: 87 MB % 10.62/2.29 % (1835804)Instructions burned: 12 (million) % 10.62/2.29 % (1835798)------------------------------ % 10.62/2.29 % (1835798)------------------------------ % 10.62/2.29 % (1835801)Refutation not found, incomplete strategy % 10.62/2.29 % (1835801)------------------------------ % 10.62/2.29 % (1835801)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.62/2.29 % (1835801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.62/2.29 % (1835801)CaDiCaL version: 2.1.3 % 10.62/2.29 % (1835801)Termination reason: Refutation not found, incomplete strategy % 10.62/2.29 % (1835801)Time elapsed: 0.031 s % 10.62/2.29 % (1835801)Peak memory usage: 111 MB % 10.62/2.29 % (1835801)Instructions burned: 16 (million) % 10.62/2.29 % (1835805)lrs+1002_1_to=lpo:thi=strong:sas=z3:si=on:sp=const_frequency:tha=off:random_seed=3544871954:i=71:rtra=on:gtg=exists_top_2992 on theBenchmark for (2992ds/71Mi) % 10.62/2.29 % (1835808)lrs+1010_1_to=lpo:prlc=on:sil=128000:prc=on:drc=off:si=on:sp=const_max:thsqr=8,1:tha=some:nwc=5:random_seed=1177212640:i=75:doe=on:thsqd=64:canc=force:thsqc=64:rtra=on:thsq=on_2991 on theBenchmark for (2991ds/75Mi) % 10.62/2.29 % (1835809)dis+1011_2:1_to=kbo:sil=128000:tgt=full:fde=none:si=on:norm_ineq=on:spb=goal_then_units:tha=some:nwc=2:sac=on:random_seed=1591941012:i=294:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2991 on theBenchmark for (2991ds/294Mi) % 10.62/2.29 % (1835808)Instruction limit reached! % 10.62/2.29 % (1835808)------------------------------ % 10.62/2.29 % (1835808)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.62/2.29 % (1835808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.62/2.29 % (1835808)CaDiCaL version: 2.1.3 % 10.62/2.29 % (1835808)Termination reason: Instruction limit % 10.62/2.29 % (1835808)Termination phase: Saturation % 10.62/2.29 % (1835808)Time elapsed: 0.034 s % 10.62/2.29 % (1835808)Peak memory usage: 89 MB % 10.62/2.29 % (1835808)Instructions burned: 76 (million) % 10.62/2.29 % (1835805)Instruction limit reached! % 10.62/2.29 % (1835805)------------------------------ % 10.62/2.29 % (1835805)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.62/2.29 % (1835805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.62/2.29 % (1835805)CaDiCaL version: 2.1.3 % 10.62/2.29 % (1835805)Termination reason: Instruction limit % 10.62/2.29 % (1835805)Termination phase: Saturation % 10.62/2.29 % (1835805)Time elapsed: 0.072 s % 10.62/2.29 % (1835805)Peak memory usage: 129 MB % 10.62/2.29 % (1835805)Instructions burned: 71 (million) % 10.62/2.29 % (1835815)dis+1010_16_to=lpo:sil=64000:thi=strong:sas=z3:si=on:nwc=5:random_seed=1304250313:i=40:gtgl=2:rtra=on:gtg=exists_sym:ev=force_2990 on theBenchmark for (2990ds/40Mi) % 10.62/2.29 % (1835812)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=1125511555:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2990 on theBenchmark for (2990ds/130Mi) % 10.62/2.29 % (1835814)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=368771838:i=131:rtra=on_2990 on theBenchmark for (2990ds/131Mi) % 10.62/2.29 % (1835815)Instruction limit reached! % 10.62/2.29 % (1835815)------------------------------ % 10.62/2.29 % (1835815)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 10.62/2.29 % (1835815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 10.62/2.29 % (1835815)CaDiCaL version: 2.1.3 % 10.62/2.29 % (1835815)Termination reason: Instruction limit % 10.62/2.29 % (1835815)Termination phase: Saturation % 10.62/2.29 % (1835815)Time elapsed: 0.036 s % 10.62/2.29 % (1835815)Peak memory usage: 129 MB % 10.62/2.29 % (1835815)Instructions burned: 44 (million) % 11.64/2.51 % (1835809)Instruction limit reached! % 11.64/2.51 % (1835809)------------------------------ % 11.64/2.51 % (1835809)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.64/2.51 % (1835809)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.64/2.51 % (1835809)CaDiCaL version: 2.1.3 % 11.64/2.51 % (1835809)Termination reason: Instruction limit % 11.64/2.51 % (1835809)Termination phase: Saturation % 11.64/2.51 % (1835809)Time elapsed: 0.124 s % 11.64/2.51 % (1835809)Peak memory usage: 89 MB % 11.64/2.51 % (1835809)Instructions burned: 294 (million) % 11.64/2.51 % (1835812)Instruction limit reached! % 11.64/2.51 % (1835812)------------------------------ % 11.64/2.51 % (1835812)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.64/2.51 % (1835812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.64/2.51 % (1835812)CaDiCaL version: 2.1.3 % 11.64/2.51 % (1835812)Termination reason: Instruction limit % 11.64/2.51 % (1835812)Termination phase: Saturation % 11.64/2.51 % (1835812)Time elapsed: 0.088 s % 11.64/2.51 % (1835812)Peak memory usage: 116 MB % 11.64/2.51 % (1835812)Instructions burned: 130 (million) % 11.64/2.51 % (1835819)lrs+10_1_to=lpo:sil=64000:si=on:sos=on:urr=on:random_seed=4015265532:i=307:rtra=on:gtg=exists_top_2989 on theBenchmark for (2989ds/307Mi) % 11.64/2.51 % (1835814)Instruction limit reached! % 11.64/2.51 % (1835814)------------------------------ % 11.64/2.51 % (1835814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.64/2.51 % (1835814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.64/2.51 % (1835814)CaDiCaL version: 2.1.3 % 11.64/2.51 % (1835814)Termination reason: Instruction limit % 11.64/2.51 % (1835814)Termination phase: Saturation % 11.64/2.51 % (1835814)Time elapsed: 0.101 s % 11.64/2.51 % (1835814)Peak memory usage: 133 MB % 11.64/2.51 % (1835814)Instructions burned: 131 (million) % 11.64/2.51 % (1835820)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=1051971660:s2a=on:i=598:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/598Mi) % 11.64/2.51 % (1835801)------------------------------ % 11.64/2.51 % (1835801)------------------------------ % 11.64/2.51 % (1835819)Refutation not found, incomplete strategy % 11.64/2.51 % (1835819)------------------------------ % 11.64/2.51 % (1835819)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.64/2.51 % (1835819)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.64/2.51 % (1835819)CaDiCaL version: 2.1.3 % 11.64/2.51 % (1835819)Termination reason: Refutation not found, incomplete strategy % 11.64/2.51 % (1835819)Time elapsed: 0.015 s % 11.64/2.51 % (1835819)Peak memory usage: 89 MB % 11.64/2.51 % (1835819)Instructions burned: 35 (million) % 11.64/2.51 % (1835824)lrs+1011_5:1_to=kbo:sil=64000:thi=all:si=on:uwa=ground:br=off:random_seed=1206178244:i=131:canc=cautious:fsr=off:rtra=on_2989 on theBenchmark for (2989ds/131Mi) % 11.64/2.51 % (1835825)dis+11_1_to=lpo:pum=on:sas=z3:si=on:sp=reverse_arity:sos=theory:thsqr=2,1:tha=some:s2agt=20:random_seed=3823911592:s2pl=no:i=259:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2989 on theBenchmark for (2989ds/259Mi) % 11.64/2.51 % (1835824)Instruction limit reached! % 11.64/2.51 % (1835824)------------------------------ % 11.64/2.51 % (1835824)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.64/2.51 % (1835824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.64/2.51 % (1835824)CaDiCaL version: 2.1.3 % 11.64/2.51 % (1835824)Termination reason: Instruction limit % 11.64/2.51 % (1835824)Termination phase: Saturation % 11.64/2.51 % (1835824)Time elapsed: 0.041 s % 11.64/2.51 % (1835824)Peak memory usage: 112 MB % 11.64/2.51 % (1835824)Instructions burned: 133 (million) % 11.64/2.51 % (1835825)Refutation not found, incomplete strategy % 11.64/2.51 % (1835825)------------------------------ % 11.64/2.51 % (1835825)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 11.64/2.51 % (1835825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 11.64/2.51 % (1835825)CaDiCaL version: 2.1.3 % 11.64/2.51 % (1835825)Termination reason: Refutation not found, incomplete strategy % 11.64/2.51 % (1835825)Time elapsed: 0.031 s % 11.64/2.51 % (1835825)Peak memory usage: 111 MB % 11.64/2.51 % (1835825)Instructions burned: 17 (million) % 11.64/2.51 % (1835826)dis+10_1_si=on:random_seed=381293285:s2a=on:i=1000:rtra=on:gtg=exists_all_2988 on theBenchmark for (2988ds/1000Mi) % 13.62/2.72 % (1835829)dis+1010_1_to=lpo:sil=128000:tgt=full:si=on:sp=const_frequency:uwa=off:tha=off:nwc=1:random_seed=966779483:i=383:fsr=off:rtra=on:ev=force_2988 on theBenchmark for (2988ds/383Mi) % 13.62/2.72 % (1835830)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=3831373289:i=141:doe=on:rtra=on_2988 on theBenchmark for (2988ds/141Mi) % 13.62/2.72 % (1835833)lrs+10_1024_to=kbo:sil=128000:fde=unused:sas=z3:si=on:norm_ineq=on:sos=on:tha=off:random_seed=545896720:i=65:nm=16:rtra=on_2987 on theBenchmark for (2987ds/65Mi) % 13.62/2.72 % (1835833)Refutation not found, incomplete strategy % 13.62/2.72 % (1835833)------------------------------ % 13.62/2.72 % (1835833)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.62/2.72 % (1835833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.62/2.72 % (1835833)CaDiCaL version: 2.1.3 % 13.62/2.72 % (1835833)Termination reason: Refutation not found, incomplete strategy % 13.62/2.72 % (1835833)Time elapsed: 0.023 s % 13.62/2.72 % (1835833)Peak memory usage: 113 MB % 13.62/2.72 % (1835833)Instructions burned: 37 (million) % 13.62/2.72 % (1835830)Instruction limit reached! % 13.62/2.72 % (1835830)------------------------------ % 13.62/2.72 % (1835830)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.62/2.72 % (1835830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.62/2.72 % (1835830)CaDiCaL version: 2.1.3 % 13.62/2.72 % (1835830)Termination reason: Instruction limit % 13.62/2.72 % (1835830)Termination phase: Saturation % 13.62/2.72 % (1835830)Time elapsed: 0.056 s % 13.62/2.72 % (1835830)Peak memory usage: 89 MB % 13.62/2.72 % (1835830)Instructions burned: 143 (million) % 13.62/2.72 % (1835819)------------------------------ % 13.62/2.72 % (1835819)------------------------------ % 13.62/2.72 % (1835820)Instruction limit reached! % 13.62/2.72 % (1835820)------------------------------ % 13.62/2.72 % (1835820)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.62/2.72 % (1835820)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.62/2.72 % (1835820)CaDiCaL version: 2.1.3 % 13.62/2.72 % (1835820)Termination reason: Instruction limit % 13.62/2.72 % (1835820)Termination phase: Saturation % 13.62/2.72 % (1835820)Time elapsed: 0.296 s % 13.62/2.72 % (1835820)Peak memory usage: 135 MB % 13.62/2.72 % (1835820)Instructions burned: 599 (million) % 13.62/2.72 % (1835829)Instruction limit reached! % 13.62/2.72 % (1835829)------------------------------ % 13.62/2.72 % (1835829)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.62/2.72 % (1835829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.62/2.72 % (1835829)CaDiCaL version: 2.1.3 % 13.62/2.72 % (1835829)Termination reason: Instruction limit % 13.62/2.72 % (1835829)Termination phase: Saturation % 13.62/2.72 % (1835829)Time elapsed: 0.152 s % 13.62/2.72 % (1835829)Peak memory usage: 90 MB % 13.62/2.72 % (1835829)Instructions burned: 385 (million) % 13.62/2.72 % (1835825)------------------------------ % 13.62/2.72 % (1835825)------------------------------ % 13.62/2.72 % (1835833)------------------------------ % 13.62/2.72 % (1835833)------------------------------ % 13.62/2.72 % (1835838)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=3366045690:i=121:nm=16:rtra=on_2985 on theBenchmark for (2985ds/121Mi) % 13.62/2.72 % (1835839)dis+1010_1_anc=none:to=kbo:sil=128000:sas=z3:si=on:sos=on:gve=force:urr=on:uwa=one_side_interpreted:random_seed=3271320414:s2a=on:i=128:s2at=5:ins=3:rtra=on_2985 on theBenchmark for (2985ds/128Mi) % 13.62/2.72 % (1835838)Instruction limit reached! % 13.62/2.72 % (1835838)------------------------------ % 13.62/2.72 % (1835838)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 13.62/2.72 % (1835838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 13.62/2.72 % (1835838)CaDiCaL version: 2.1.3 % 13.62/2.72 % (1835838)Termination reason: Instruction limit % 13.62/2.72 % (1835838)Termination phase: Saturation % 13.62/2.72 % (1835838)Time elapsed: 0.048 s % 13.62/2.72 % (1835838)Peak memory usage: 89 MB % 13.62/2.72 % (1835838)Instructions burned: 121 (million) % 13.62/2.72 % (1835840)ott-1_8:1_tgt=ground:plsq=on:plsqc=2:sas=z3:si=on:plsqr=3,1:sos=on:inw=on:flr=on:random_seed=3242342262:i=39:ins=3:rtra=on_2985 on theBenchmark for (2985ds/39Mi) % 13.62/2.72 % (1835841)dis+1010_1_to=kbo:si=on:random_seed=198032116:i=175:doe=on:nm=0:rtra=on:gtg=exists_sym:ss=axioms:ev=cautious_2985 on theBenchmark for (2985ds/175Mi) % 13.62/2.72 % (1835839)Refutation not found, incomplete strategy % 14.26/3.01 % (1835839)------------------------------ % 14.26/3.01 % (1835839)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.26/3.01 % (1835839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.26/3.01 % (1835839)CaDiCaL version: 2.1.3 % 14.26/3.01 % (1835839)Termination reason: Refutation not found, incomplete strategy % 14.26/3.01 % (1835839)Time elapsed: 0.043 s % 14.26/3.01 % (1835839)Peak memory usage: 113 MB % 14.26/3.01 % (1835839)Instructions burned: 46 (million) % 14.26/3.01 % (1835840)Instruction limit reached! % 14.26/3.01 % (1835840)------------------------------ % 14.26/3.01 % (1835840)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.26/3.01 % (1835840)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.26/3.01 % (1835840)CaDiCaL version: 2.1.3 % 14.26/3.01 % (1835840)Termination reason: Instruction limit % 14.26/3.01 % (1835840)Termination phase: Saturation % 14.26/3.01 % (1835840)Time elapsed: 0.017 s % 14.26/3.01 % (1835840)Peak memory usage: 89 MB % 14.26/3.01 % (1835840)Instructions burned: 39 (million) % 14.26/3.01 % (1835842)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=1130642832:i=329:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2984 on theBenchmark for (2984ds/329Mi) % 14.26/3.01 % (1835843)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=445587785:s2a=on:i=483:doe=on:nm=32:rtra=on_2984 on theBenchmark for (2984ds/483Mi) % 14.26/3.01 % (1835826)Instruction limit reached! % 14.26/3.01 % (1835826)------------------------------ % 14.26/3.01 % (1835826)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.26/3.01 % (1835826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.26/3.01 % (1835826)CaDiCaL version: 2.1.3 % 14.26/3.01 % (1835826)Termination reason: Instruction limit % 14.26/3.01 % (1835826)Termination phase: Saturation % 14.26/3.01 % (1835826)Time elapsed: 0.371 s % 14.26/3.01 % (1835826)Peak memory usage: 89 MB % 14.26/3.01 % (1835826)Instructions burned: 1002 (million) % 14.26/3.01 % (1835841)Instruction limit reached! % 14.26/3.01 % (1835841)------------------------------ % 14.26/3.01 % (1835841)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.26/3.01 % (1835841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.26/3.01 % (1835841)CaDiCaL version: 2.1.3 % 14.26/3.01 % (1835841)Termination reason: Instruction limit % 14.26/3.01 % (1835841)Termination phase: Saturation % 14.26/3.01 % (1835841)Time elapsed: 0.077 s % 14.26/3.01 % (1835841)Peak memory usage: 90 MB % 14.26/3.01 % (1835841)Instructions burned: 178 (million) % 14.26/3.01 % (1835850)lrs+1011_1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=unary_frequency:tha=off:random_seed=1378438875:i=349:rtra=on_2983 on theBenchmark for (2983ds/349Mi) % 14.26/3.01 % (1835847)lrs+10_40_anc=all:to=kbo:tgt=ground:thi=overlap:sas=z3:si=on:thigen=on:random_seed=3199208018:thitd=on:i=215:nm=0:rtra=on:ev=force_2983 on theBenchmark for (2983ds/215Mi) % 14.26/3.01 % (1835842)Instruction limit reached! % 14.26/3.01 % (1835842)------------------------------ % 14.26/3.01 % (1835842)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.26/3.01 % (1835842)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.26/3.01 % (1835842)CaDiCaL version: 2.1.3 % 14.26/3.01 % (1835842)Termination reason: Instruction limit % 14.26/3.01 % (1835842)Termination phase: Saturation % 14.26/3.01 % (1835842)Time elapsed: 0.156 s % 14.26/3.01 % (1835842)Peak memory usage: 117 MB % 14.26/3.01 % (1835842)Instructions burned: 330 (million) % 14.26/3.01 % (1835850)Instruction limit reached! % 14.26/3.01 % (1835850)------------------------------ % 14.26/3.01 % (1835850)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 14.26/3.01 % (1835850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 14.26/3.01 % (1835850)CaDiCaL version: 2.1.3 % 14.26/3.01 % (1835850)Termination reason: Instruction limit % 14.26/3.01 % (1835850)Termination phase: Saturation % 14.26/3.01 % (1835850)Time elapsed: 0.087 s % 14.26/3.01 % (1835850)Peak memory usage: 117 MB % 14.26/3.01 % (1835850)Instructions burned: 351 (million) % 14.26/3.01 % (1835853)dis+1011_1_to=kbo:sil=128000:drc=off:si=on:br=off:random_seed=4006729156:st=2:i=295:rtra=on:ss=axioms_2983 on theBenchmark for (2983ds/295Mi) % 14.26/3.01 % (1835854)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=1051411795:i=328:kws=inv_frequency:nm=20:rtra=on_2983 on theBenchmark for (2983ds/328Mi) % 17.86/3.28 % (1835853)Refutation not found, incomplete strategy % 17.86/3.28 % (1835853)------------------------------ % 17.86/3.28 % (1835853)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.86/3.28 % (1835853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.86/3.28 % (1835853)CaDiCaL version: 2.1.3 % 17.86/3.28 % (1835853)Termination reason: Refutation not found, incomplete strategy % 17.86/3.28 % (1835853)Time elapsed: 0.005 s % 17.86/3.28 % (1835853)Peak memory usage: 88 MB % 17.86/3.28 % (1835853)Instructions burned: 12 (million) % 17.86/3.28 % (1835839)------------------------------ % 17.86/3.28 % (1835839)------------------------------ % 17.86/3.28 % (1835847)Instruction limit reached! % 17.86/3.28 % (1835847)------------------------------ % 17.86/3.28 % (1835847)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.86/3.28 % (1835847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.86/3.28 % (1835847)CaDiCaL version: 2.1.3 % 17.86/3.28 % (1835847)Termination reason: Instruction limit % 17.86/3.28 % (1835847)Termination phase: Saturation % 17.86/3.28 % (1835847)Time elapsed: 0.143 s % 17.86/3.28 % (1835847)Peak memory usage: 135 MB % 17.86/3.28 % (1835847)Instructions burned: 215 (million) % 17.86/3.28 % (1835843)Instruction limit reached! % 17.86/3.28 % (1835843)------------------------------ % 17.86/3.28 % (1835843)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.86/3.28 % (1835843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.86/3.28 % (1835843)CaDiCaL version: 2.1.3 % 17.86/3.28 % (1835843)Termination reason: Instruction limit % 17.86/3.28 % (1835843)Termination phase: Saturation % 17.86/3.28 % (1835843)Time elapsed: 0.242 s % 17.86/3.28 % (1835843)Peak memory usage: 134 MB % 17.86/3.28 % (1835843)Instructions burned: 485 (million) % 17.86/3.28 % (1835857)dis+1010_1_to=lpo:sil=128000:sas=z3:si=on:nwc=5:random_seed=3162456923:i=281:gtgl=2:rtra=on:gtg=all_2981 on theBenchmark for (2981ds/281Mi) % 17.86/3.28 % (1835858)lrs+1010_1_to=kbo:sil=128000:si=on:sos=on:urr=on:uwa=alasca_main:random_seed=1273701798:i=484:doe=on:nm=0:av=off:rtra=on:ss=axioms_2981 on theBenchmark for (2981ds/484Mi) % 17.86/3.28 % (1835858)Refutation not found, incomplete strategy % 17.86/3.28 % (1835858)------------------------------ % 17.86/3.28 % (1835858)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.86/3.28 % (1835858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.86/3.28 % (1835858)CaDiCaL version: 2.1.3 % 17.86/3.28 % (1835858)Termination reason: Refutation not found, incomplete strategy % 17.86/3.28 % (1835858)Time elapsed: 0.005 s % 17.86/3.28 % (1835858)Peak memory usage: 87 MB % 17.86/3.28 % (1835858)Instructions burned: 11 (million) % 17.86/3.28 % (1835854)Instruction limit reached! % 17.86/3.28 % (1835854)------------------------------ % 17.86/3.28 % (1835854)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.86/3.28 % (1835854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.86/3.28 % (1835854)CaDiCaL version: 2.1.3 % 17.86/3.28 % (1835854)Termination reason: Instruction limit % 17.86/3.28 % (1835854)Termination phase: Saturation % 17.86/3.28 % (1835854)Time elapsed: 0.156 s % 17.86/3.28 % (1835854)Peak memory usage: 117 MB % 17.86/3.28 % (1835854)Instructions burned: 330 (million) % 17.86/3.28 % (1835861)lrs+21_1_to=kbo:sil=128000:thi=neg_eq:si=on:random_seed=2877631076:i=321:canc=force:rtra=on:tac=axiom:ss=axioms:ev=force_2981 on theBenchmark for (2981ds/321Mi) % 17.86/3.28 % (1835857)Instruction limit reached! % 17.86/3.28 % (1835857)------------------------------ % 17.86/3.28 % (1835857)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.86/3.28 % (1835857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.86/3.28 % (1835857)CaDiCaL version: 2.1.3 % 17.86/3.28 % (1835857)Termination reason: Instruction limit % 17.86/3.28 % (1835857)Termination phase: Saturation % 17.86/3.28 % (1835857)Time elapsed: 0.080 s % 17.86/3.28 % (1835857)Peak memory usage: 117 MB % 17.86/3.28 % (1835857)Instructions burned: 283 (million) % 17.86/3.28 % (1835861)Refutation not found, incomplete strategy % 17.86/3.28 % (1835861)------------------------------ % 17.86/3.28 % (1835861)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 17.86/3.28 % (1835861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 17.86/3.28 % (1835861)CaDiCaL version: 2.1.3 % 19.63/3.63 % (1835861)Termination reason: Refutation not found, incomplete strategy % 19.63/3.63 % (1835861)Time elapsed: 0.031 s % 19.63/3.63 % (1835861)Peak memory usage: 112 MB % 19.63/3.63 % (1835861)Instructions burned: 16 (million) % 19.63/3.63 % (1835862)lrs+1002_1_to=lpo:sil=128000:sas=z3:si=on:sos=on:urr=on:tha=off:random_seed=1390183092:i=416:rtra=on:gtg=position:ss=axioms_2981 on theBenchmark for (2981ds/416Mi) % 19.63/3.63 % (1835863)lrs+1010_1_to=kbo:tgt=ground:fde=unused:sas=z3:si=on:sp=unary_frequency:gve=force:spb=goal:tha=off:random_seed=3421257324:i=471:thf=on:kws=precedence:rtra=on_2980 on theBenchmark for (2980ds/471Mi) % 19.63/3.63 % (1835862)Refutation not found, incomplete strategy % 19.63/3.63 % (1835862)------------------------------ % 19.63/3.63 % (1835862)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.63/3.63 % (1835862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.63/3.63 % (1835862)CaDiCaL version: 2.1.3 % 19.63/3.63 % (1835862)Termination reason: Refutation not found, incomplete strategy % 19.63/3.63 % (1835862)Time elapsed: 0.031 s % 19.63/3.63 % (1835862)Peak memory usage: 111 MB % 19.63/3.63 % (1835862)Instructions burned: 16 (million) % 19.63/3.63 % (1835853)------------------------------ % 19.63/3.63 % (1835853)------------------------------ % 19.63/3.63 % (1835868)lrs+1010_2_to=kbo:sil=128000:tgt=ground:fde=unused:sas=z3:si=on:uwa=off:tha=off:nwc=1:random_seed=3304469015:i=375:kws=inv_arity_squared:rtra=on_2979 on theBenchmark for (2979ds/375Mi) % 19.63/3.63 % (1835866)lrs+1011_607:55_to=lpo:sil=64000:pum=on:thi=overlap:sas=z3:si=on:sp=const_min:spb=goal_then_units:tha=some:newcnf=on:random_seed=1136705772:avsq=on:i=276:avsqr=1,2:rtra=on_2979 on theBenchmark for (2979ds/276Mi) % 19.63/3.63 % (1835858)------------------------------ % 19.63/3.63 % (1835858)------------------------------ % 19.63/3.63 % (1835868)Instruction limit reached! % 19.63/3.63 % (1835868)------------------------------ % 19.63/3.63 % (1835868)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.63/3.63 % (1835868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.63/3.63 % (1835868)CaDiCaL version: 2.1.3 % 19.63/3.63 % (1835868)Termination reason: Instruction limit % 19.63/3.63 % (1835868)Termination phase: Saturation % 19.63/3.63 % (1835868)Time elapsed: 0.093 s % 19.63/3.63 % (1835868)Peak memory usage: 117 MB % 19.63/3.63 % (1835868)Instructions burned: 380 (million) % 19.63/3.63 % (1835871)lrs+10_1_to=kbo:sil=128000:tgt=full:sas=z3:si=on:uwa=func_ext:slsqc=1:flr=on:slsq=on:random_seed=747070514:i=387:bd=preordered:rtra=on:ss=axioms:sgt=8_2978 on theBenchmark for (2978ds/387Mi) % 19.63/3.63 % (1835863)Instruction limit reached! % 19.63/3.63 % (1835863)------------------------------ % 19.63/3.63 % (1835863)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.63/3.63 % (1835863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.63/3.63 % (1835863)CaDiCaL version: 2.1.3 % 19.63/3.63 % (1835863)Termination reason: Instruction limit % 19.63/3.63 % (1835863)Termination phase: Saturation % 19.63/3.63 % (1835863)Time elapsed: 0.204 s % 19.63/3.63 % (1835863)Peak memory usage: 112 MB % 19.63/3.63 % (1835863)Instructions burned: 472 (million) % 19.63/3.63 % (1835861)------------------------------ % 19.63/3.63 % (1835861)------------------------------ % 19.63/3.63 % (1835871)Refutation not found, incomplete strategy % 19.63/3.63 % (1835871)------------------------------ % 19.63/3.63 % (1835871)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.63/3.63 % (1835871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.63/3.63 % (1835871)CaDiCaL version: 2.1.3 % 19.63/3.63 % (1835871)Termination reason: Refutation not found, incomplete strategy % 19.63/3.63 % (1835871)Time elapsed: 0.031 s % 19.63/3.63 % (1835871)Peak memory usage: 111 MB % 19.63/3.63 % (1835871)Instructions burned: 17 (million) % 19.63/3.63 % (1835862)------------------------------ % 19.63/3.63 % (1835862)------------------------------ % 19.63/3.63 % (1835866)Instruction limit reached! % 19.63/3.63 % (1835866)------------------------------ % 19.63/3.63 % (1835866)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 19.63/3.63 % (1835866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 19.63/3.63 % (1835866)CaDiCaL version: 2.1.3 % 19.63/3.63 % (1835866)Termination reason: Instruction limit % 19.63/3.63 % (1835866)Termination phase: Saturation % 19.63/3.63 % (1835866)Time elapsed: 0.180 s % 19.63/3.63 % (1835866)Peak memory usage: 134 MB % 19.63/3.63 % (1835866)Instructions burned: 278 (million) % 21.73/3.98 % (1835875)lrs+21_1_to=kbo:sil=64000:thi=all:sas=z3:si=on:spb=goal_then_units:tha=off:nwc=3:random_seed=3850045401:i=334:rtra=on_2977 on theBenchmark for (2977ds/334Mi) % 21.73/3.98 % (1835874)lrs+10_1_to=kbo:sil=128000:fde=none:si=on:norm_ineq=on:urr=on:nwc=0.5:random_seed=1388291364:i=513:kws=frequency:bd=all:rtra=on:gtg=exists_all:ss=axioms:sgt=4_2977 on theBenchmark for (2977ds/513Mi) % 21.73/3.98 % (1835877)lrs+1010_1_to=kbo:sil=64000:sas=cadical:si=on:sos=on:bce=on:random_seed=1016975184:i=359:rtra=on:gtg=exists_top:ss=axioms_2977 on theBenchmark for (2977ds/359Mi) % 21.73/3.98 % (1835877)Refutation not found, incomplete strategy % 21.73/3.98 % (1835877)------------------------------ % 21.73/3.98 % (1835877)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.73/3.98 % (1835877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.73/3.98 % (1835877)CaDiCaL version: 2.1.3 % 21.73/3.98 % (1835877)Termination reason: Refutation not found, incomplete strategy % 21.73/3.98 % (1835877)Time elapsed: 0.007 s % 21.73/3.98 % (1835877)Peak memory usage: 88 MB % 21.73/3.98 % (1835877)Instructions burned: 15 (million) % 21.73/3.98 % (1835878)dis+1010_1_to=lpo:sil=128000:thi=all:fde=unused:si=on:sp=reverse_arity:tha=off:random_seed=750870346:i=341:gtgl=2:rtra=on:gtg=exists_sym:ev=force:fsd=on:fsdmm=1_2976 on theBenchmark for (2976ds/341Mi) % 21.73/3.98 % (1835875)Instruction limit reached! % 21.73/3.98 % (1835875)------------------------------ % 21.73/3.98 % (1835875)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.73/3.98 % (1835875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.73/3.98 % (1835875)CaDiCaL version: 2.1.3 % 21.73/3.98 % (1835875)Termination reason: Instruction limit % 21.73/3.98 % (1835875)Termination phase: Saturation % 21.73/3.98 % (1835875)Time elapsed: 0.109 s % 21.73/3.98 % (1835875)Peak memory usage: 134 MB % 21.73/3.98 % (1835875)Instructions burned: 334 (million) % 21.73/3.98 % (1835879)lrs-2_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_max:tha=off:random_seed=86041084:st=1.5:i=261:sd=1:kws=precedence:rtra=on:ss=axioms_2976 on theBenchmark for (2976ds/261Mi) % 21.73/3.98 % (1835880)dis+11_1_to=lpo:pum=on:sas=z3:si=on:sp=reverse_arity:sos=theory:thsqr=2,1:tha=some:s2agt=20:random_seed=1456784972:s2pl=no:i=235:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2976 on theBenchmark for (2976ds/235Mi) % 21.73/3.98 % (1835879)Refutation not found, incomplete strategy % 21.73/3.98 % (1835879)------------------------------ % 21.73/3.98 % (1835879)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.73/3.98 % (1835879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.73/3.98 % (1835879)CaDiCaL version: 2.1.3 % 21.73/3.98 % (1835879)Termination reason: Refutation not found, incomplete strategy % 21.73/3.98 % (1835879)Time elapsed: 0.029 s % 21.73/3.98 % (1835879)Peak memory usage: 111 MB % 21.73/3.98 % (1835879)Instructions burned: 13 (million) % 21.73/3.98 % (1835880)Refutation not found, incomplete strategy % 21.73/3.98 % (1835880)------------------------------ % 21.73/3.98 % (1835880)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.73/3.98 % (1835880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.73/3.98 % (1835880)CaDiCaL version: 2.1.3 % 21.73/3.98 % (1835880)Termination reason: Refutation not found, incomplete strategy % 21.73/3.98 % (1835880)Time elapsed: 0.031 s % 21.73/3.98 % (1835880)Peak memory usage: 111 MB % 21.73/3.98 % (1835880)Instructions burned: 17 (million) % 21.73/3.98 % (1835871)------------------------------ % 21.73/3.98 % (1835871)------------------------------ % 21.73/3.98 % (1835874)Instruction limit reached! % 21.73/3.98 % (1835874)------------------------------ % 21.73/3.98 % (1835874)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 21.73/3.98 % (1835874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 21.73/3.98 % (1835874)CaDiCaL version: 2.1.3 % 21.73/3.98 % (1835874)Termination reason: Instruction limit % 21.73/3.98 % (1835874)Termination phase: Saturation % 21.73/3.98 % (1835874)Time elapsed: 0.195 s % 21.73/3.98 % (1835874)Peak memory usage: 89 MB % 21.73/3.98 % (1835874)Instructions burned: 515 (million) % 21.73/3.98 % (1835885)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=2926383402:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2975 on theBenchmark for (2975ds/273Mi) % 25.90/4.40 % (1835878)Instruction limit reached! % 25.90/4.40 % (1835878)------------------------------ % 25.90/4.40 % (1835878)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.90/4.40 % (1835878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.90/4.40 % (1835878)CaDiCaL version: 2.1.3 % 25.90/4.40 % (1835878)Termination reason: Instruction limit % 25.90/4.40 % (1835878)Termination phase: Saturation % 25.90/4.40 % (1835878)Time elapsed: 0.161 s % 25.90/4.40 % (1835878)Peak memory usage: 117 MB % 25.90/4.40 % (1835878)Instructions burned: 343 (million) % 25.90/4.40 % (1835885)Instruction limit reached! % 25.90/4.40 % (1835885)------------------------------ % 25.90/4.40 % (1835885)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.90/4.40 % (1835885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.90/4.40 % (1835885)CaDiCaL version: 2.1.3 % 25.90/4.40 % (1835885)Termination reason: Instruction limit % 25.90/4.40 % (1835885)Termination phase: Saturation % 25.90/4.40 % (1835885)Time elapsed: 0.058 s % 25.90/4.40 % (1835885)Peak memory usage: 90 MB % 25.90/4.40 % (1835885)Instructions burned: 276 (million) % 25.90/4.40 % (1835877)------------------------------ % 25.90/4.40 % (1835877)------------------------------ % 25.90/4.40 % (1835888)lrs+10_1_to=kbo:sil=64000:si=on:norm_ineq=on:sp=unary_frequency:random_seed=324879590:i=146:doe=on:rtra=on_2974 on theBenchmark for (2974ds/146Mi) % 25.90/4.40 % (1835889)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=296897540:i=4428:doe=on:fsr=off:rtra=on_2973 on theBenchmark for (2973ds/4428Mi) % 25.90/4.40 % (1835879)------------------------------ % 25.90/4.40 % (1835879)------------------------------ % 25.90/4.40 % (1835888)Instruction limit reached! % 25.90/4.40 % (1835888)------------------------------ % 25.90/4.40 % (1835888)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.90/4.40 % (1835888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.90/4.40 % (1835888)CaDiCaL version: 2.1.3 % 25.90/4.40 % (1835888)Termination reason: Instruction limit % 25.90/4.40 % (1835888)Termination phase: Saturation % 25.90/4.40 % (1835888)Time elapsed: 0.058 s % 25.90/4.40 % (1835888)Peak memory usage: 89 MB % 25.90/4.40 % (1835888)Instructions burned: 147 (million) % 25.90/4.40 % (1835891)lrs+1011_607:55_to=lpo:sil=64000:pum=on:thi=overlap:sas=z3:si=on:sp=const_min:spb=goal_then_units:tha=some:newcnf=on:random_seed=3803215130:avsq=on:i=276:avsqr=1,2:rtra=on_2973 on theBenchmark for (2973ds/276Mi) % 25.90/4.40 % (1835892)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=3750779776:i=1052:rtra=on_2973 on theBenchmark for (2973ds/1052Mi) % 25.90/4.40 % (1835880)------------------------------ % 25.90/4.40 % (1835880)------------------------------ % 25.90/4.40 % (1835893)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=440907355:i=655:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2972 on theBenchmark for (2972ds/655Mi) % 25.90/4.40 % (1835899)lrs-1002_1_to=kbo:sas=z3:si=on:norm_ineq=on:sos=on:tha=some:random_seed=1582484113:i=107:rtra=on_2972 on theBenchmark for (2972ds/107Mi) % 25.90/4.40 % (1835897)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=4086197254:st=5:i=1054:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2972 on theBenchmark for (2972ds/1054Mi) % 25.90/4.40 % (1835897)Refutation not found, incomplete strategy % 25.90/4.40 % (1835897)------------------------------ % 25.90/4.40 % (1835897)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.90/4.40 % (1835897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.90/4.40 % (1835897)CaDiCaL version: 2.1.3 % 25.90/4.40 % (1835897)Termination reason: Refutation not found, incomplete strategy % 25.90/4.40 % (1835897)Time elapsed: 0.004 s % 25.90/4.40 % (1835897)Peak memory usage: 87 MB % 25.90/4.40 % (1835897)Instructions burned: 8 (million) % 25.90/4.40 % (1835900)lrs+1002_8_to=kbo:sil=128000:thi=all:drc=ordering:sas=z3:si=on:tha=off:rp=on:random_seed=3661163355:s2a=on:i=450:doe=on:nm=32:rtra=on_2971 on theBenchmark for (2971ds/450Mi) % 25.90/4.40 % (1835891)Instruction limit reached! % 25.90/4.40 % (1835891)------------------------------ % 25.90/4.40 % (1835891)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 25.90/4.40 % (1835891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 25.90/4.40 % (1835891)CaDiCaL version: 2.1.3 % 27.02/4.66 % (1835891)Termination reason: Instruction limit % 27.02/4.66 % (1835891)Termination phase: Saturation % 27.02/4.66 % (1835891)Time elapsed: 0.177 s % 27.02/4.66 % (1835891)Peak memory usage: 134 MB % 27.02/4.66 % (1835891)Instructions burned: 277 (million) % 27.02/4.66 % (1835899)Refutation not found, incomplete strategy % 27.02/4.66 % (1835899)------------------------------ % 27.02/4.66 % (1835899)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.02/4.66 % (1835899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.02/4.66 % (1835899)CaDiCaL version: 2.1.3 % 27.02/4.66 % (1835899)Termination reason: Refutation not found, incomplete strategy % 27.02/4.66 % (1835899)Time elapsed: 0.041 s % 27.02/4.66 % (1835899)Peak memory usage: 113 MB % 27.02/4.66 % (1835899)Instructions burned: 41 (million) % 27.02/4.66 % (1835893)Refutation not found, incomplete strategy % 27.02/4.66 % (1835893)------------------------------ % 27.02/4.66 % (1835893)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.02/4.66 % (1835893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.02/4.66 % (1835893)CaDiCaL version: 2.1.3 % 27.02/4.66 % (1835893)Termination reason: Refutation not found, incomplete strategy % 27.02/4.66 % (1835893)Time elapsed: 0.138 s % 27.02/4.66 % (1835893)Peak memory usage: 93 MB % 27.02/4.66 % (1835893)Instructions burned: 218 (million) % 27.02/4.66 % (1835892)Instruction limit reached! % 27.02/4.66 % (1835892)------------------------------ % 27.02/4.66 % (1835892)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.02/4.66 % (1835892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.02/4.66 % (1835892)CaDiCaL version: 2.1.3 % 27.02/4.66 % (1835892)Termination reason: Instruction limit % 27.02/4.66 % (1835892)Termination phase: Saturation % 27.02/4.66 % (1835892)Time elapsed: 0.224 s % 27.02/4.66 % (1835892)Peak memory usage: 92 MB % 27.02/4.66 % (1835892)Instructions burned: 1057 (million) % 27.02/4.66 % (1835905)WARNING Broken Constraint: if demodulation_redundancy_check(ordering) has been set then forward_demodulation(off) is not equal to off or backward_demodulation(off) is not equal to off or partial_redundancy_check(off) is not equal to off % 27.02/4.66 % (1835905)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=3055327478:i=1090:aac=none:nm=0:rtra=on:rawr=on_2970 on theBenchmark for (2970ds/1090Mi) % 27.02/4.66 % (1835906)ott+21_1_to=kbo:tgt=full:sas=z3:si=on:tha=off:random_seed=2138521650:i=130:kws=inv_frequency:nm=0:rtra=on:gtg=exists_all_2969 on theBenchmark for (2969ds/130Mi) % 27.02/4.66 % (1835897)------------------------------ % 27.02/4.66 % (1835897)------------------------------ % 27.02/4.66 % (1835900)Instruction limit reached! % 27.02/4.66 % (1835900)------------------------------ % 27.02/4.66 % (1835900)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.02/4.66 % (1835900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.02/4.66 % (1835900)CaDiCaL version: 2.1.3 % 27.02/4.66 % (1835900)Termination reason: Instruction limit % 27.02/4.66 % (1835900)Termination phase: Saturation % 27.02/4.66 % (1835900)Time elapsed: 0.228 s % 27.02/4.66 % (1835900)Peak memory usage: 134 MB % 27.02/4.66 % (1835900)Instructions burned: 450 (million) % 27.02/4.66 % (1835906)Instruction limit reached! % 27.02/4.66 % (1835906)------------------------------ % 27.02/4.66 % (1835906)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 27.02/4.66 % (1835906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 27.02/4.66 % (1835906)CaDiCaL version: 2.1.3 % 27.02/4.66 % (1835906)Termination reason: Instruction limit % 27.02/4.66 % (1835906)Termination phase: Saturation % 27.02/4.66 % (1835906)Time elapsed: 0.049 s % 27.02/4.66 % (1835906)Peak memory usage: 116 MB % 27.02/4.66 % (1835906)Instructions burned: 135 (million) % 27.02/4.66 % (1835899)------------------------------ % 27.02/4.66 % (1835899)------------------------------ % 27.02/4.66 % (1835893)------------------------------ % 27.02/4.66 % (1835893)------------------------------ % 27.02/4.66 % (1835911)ott+1011_4:1_to=lpo:sil=64000:si=on:spb=intro:random_seed=4115520802:s2a=on:i=835:s2at=2:rtra=on_2967 on theBenchmark for (2967ds/835Mi) % 27.02/4.66 % (1835910)ott+10_1_to=kbo:sil=64000:si=on:sp=reverse_frequency:sos=on:random_seed=2017578525:i=491:doe=on:rtra=on:gtg=position_2968 on theBenchmark for (2968ds/491Mi) % 27.02/4.66 % (1835909)dis+1010_1_to=kbo:sil=128000:tgt=ground:drc=ordering:sas=z3:si=on:spb=goal:nwc=5:br=off:random_seed=2936285379:i=312:kws=inv_frequency:nm=20:rtra=on_2968 on theBenchmark for (2968ds/312Mi) % 31.20/5.12 % (1835910)Refutation not found, incomplete strategy % 31.20/5.12 % (1835910)------------------------------ % 31.20/5.12 % (1835910)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.20/5.12 % (1835910)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.20/5.12 % (1835910)CaDiCaL version: 2.1.3 % 31.20/5.12 % (1835910)Termination reason: Refutation not found, incomplete strategy % 31.20/5.12 % (1835910)Time elapsed: 0.018 s % 31.20/5.12 % (1835910)Peak memory usage: 89 MB % 31.20/5.12 % (1835910)Instructions burned: 43 (million) % 31.20/5.12 % (1835912)ott+1011_2_to=lpo:sil=128000:si=on:sos=on:random_seed=3332472125:i=307:bd=preordered:av=off:rtra=on:ev=cautious_2967 on theBenchmark for (2967ds/307Mi) % 31.20/5.12 % (1835912)Refutation not found, incomplete strategy % 31.20/5.12 % (1835912)------------------------------ % 31.20/5.12 % (1835912)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.20/5.12 % (1835912)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.20/5.12 % (1835912)CaDiCaL version: 2.1.3 % 31.20/5.12 % (1835912)Termination reason: Refutation not found, incomplete strategy % 31.20/5.12 % (1835912)Time elapsed: 0.021 s % 31.20/5.12 % (1835912)Peak memory usage: 89 MB % 31.20/5.12 % (1835912)Instructions burned: 47 (million) % 31.20/5.12 % (1835913)lrs+1011_16:1_to=kbo:sil=128000:sas=z3:si=on:sos=theory:erd=off:urr=full:random_seed=2428904938:i=776:doe=on:rtra=on_2967 on theBenchmark for (2967ds/776Mi) % 31.20/5.12 % (1835909)Instruction limit reached! % 31.20/5.12 % (1835909)------------------------------ % 31.20/5.12 % (1835909)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.20/5.12 % (1835909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.20/5.12 % (1835909)CaDiCaL version: 2.1.3 % 31.20/5.12 % (1835909)Termination reason: Instruction limit % 31.20/5.12 % (1835909)Termination phase: Saturation % 31.20/5.12 % (1835909)Time elapsed: 0.147 s % 31.20/5.12 % (1835909)Peak memory usage: 117 MB % 31.20/5.12 % (1835909)Instructions burned: 314 (million) % 31.20/5.12 % (1835911)Instruction limit reached! % 31.20/5.12 % (1835911)------------------------------ % 31.20/5.12 % (1835911)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.20/5.12 % (1835911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.20/5.12 % (1835911)CaDiCaL version: 2.1.3 % 31.20/5.12 % (1835911)Termination reason: Instruction limit % 31.20/5.12 % (1835911)Termination phase: Saturation % 31.20/5.12 % (1835911)Time elapsed: 0.166 s % 31.20/5.12 % (1835911)Peak memory usage: 89 MB % 31.20/5.12 % (1835911)Instructions burned: 838 (million) % 31.20/5.12 % (1835910)------------------------------ % 31.20/5.12 % (1835910)------------------------------ % 31.20/5.12 % (1835905)Instruction limit reached! % 31.20/5.12 % (1835905)------------------------------ % 31.20/5.12 % (1835905)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.20/5.12 % (1835905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 31.20/5.12 % (1835905)CaDiCaL version: 2.1.3 % 31.20/5.12 % (1835905)Termination reason: Instruction limit % 31.20/5.12 % (1835905)Termination phase: Saturation % 31.20/5.12 % (1835905)Time elapsed: 0.457 s % 31.20/5.12 % (1835905)Peak memory usage: 117 MB % 31.20/5.12 % (1835905)Instructions burned: 1090 (million) % 31.20/5.12 % (1835920)lrs-1011_1_to=lpo:sil=128000:thi=overlap:fde=none:si=on:spb=non_intro:lcm=predicate:uwa=func_ext:slsq=on:random_seed=317180428:thitd=on:cond=fast:i=784:nm=30:rtra=on:gtg=all:tac=axiom_2965 on theBenchmark for (2965ds/784Mi) % 31.20/5.12 % (1835919)ott+1010_3:1_to=kbo:sil=128000:thi=overlap:sas=z3:si=on:urr=on:tha=off:s2agt=32:random_seed=3847285:s2a=on:i=646:doe=on:bs=on:canc=cautious:fsr=off:rtra=on_2965 on theBenchmark for (2965ds/646Mi) % 31.20/5.12 % (1835912)------------------------------ % 31.20/5.12 % (1835912)------------------------------ % 31.20/5.12 % (1835921)ott+1011_8:1_to=kbo:sil=128000:thi=overlap:si=on:sp=arity:lcm=reverse:uwa=func_ext:nwc=1:sac=on:random_seed=1164110053:thitd=on:s2a=on:i=1131:add=on:canc=force:bd=all:rtra=on:tac=axiom:ev=off_2964 on theBenchmark for (2964ds/1131Mi) % 31.20/5.12 % (1835913)Instruction limit reached! % 31.20/5.12 % (1835913)------------------------------ % 31.20/5.12 % (1835913)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 31.20/5.12 % (1835913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.21/5.76 % (1835913)CaDiCaL version: 2.1.3 % 34.21/5.76 % (1835913)Termination reason: Instruction limit % 34.21/5.76 % (1835913)Termination phase: Saturation % 34.21/5.76 % (1835913)Time elapsed: 0.311 s % 34.21/5.76 % (1835913)Peak memory usage: 113 MB % 34.21/5.76 % (1835913)Instructions burned: 778 (million) % 34.21/5.76 % (1835923)dis+11_1_to=lpo:pum=on:sas=z3:si=on:sp=reverse_arity:sos=theory:thsqr=2,1:tha=some:s2agt=20:random_seed=656628029:s2pl=no:i=246:sd=10:thsqd=64:thsqc=64:rtra=on:ss=axioms:thsq=on_2963 on theBenchmark for (2963ds/246Mi) % 34.21/5.76 % (1835920)Instruction limit reached! % 34.21/5.76 % (1835920)------------------------------ % 34.21/5.76 % (1835920)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.21/5.76 % (1835920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.21/5.76 % (1835920)CaDiCaL version: 2.1.3 % 34.21/5.76 % (1835920)Termination reason: Instruction limit % 34.21/5.76 % (1835920)Termination phase: Saturation % 34.21/5.76 % (1835920)Time elapsed: 0.168 s % 34.21/5.76 % (1835920)Peak memory usage: 113 MB % 34.21/5.76 % (1835920)Instructions burned: 787 (million) % 34.21/5.76 % (1835923)Refutation not found, incomplete strategy % 34.21/5.76 % (1835923)------------------------------ % 34.21/5.76 % (1835923)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.21/5.76 % (1835923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.21/5.76 % (1835923)CaDiCaL version: 2.1.3 % 34.21/5.76 % (1835923)Termination reason: Refutation not found, incomplete strategy % 34.21/5.76 % (1835923)Time elapsed: 0.030 s % 34.21/5.76 % (1835923)Peak memory usage: 111 MB % 34.21/5.76 % (1835923)Instructions burned: 17 (million) % 34.21/5.76 % (1835925)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=988770350:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2963 on theBenchmark for (2963ds/775Mi) % 34.21/5.76 % (1835925)Refutation not found, incomplete strategy % 34.21/5.76 % (1835925)------------------------------ % 34.21/5.76 % (1835925)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.21/5.76 % (1835925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.21/5.76 % (1835925)CaDiCaL version: 2.1.3 % 34.21/5.76 % (1835925)Termination reason: Refutation not found, incomplete strategy % 34.21/5.76 % (1835925)Time elapsed: 0.006 s % 34.21/5.76 % (1835925)Peak memory usage: 88 MB % 34.21/5.76 % (1835925)Instructions burned: 13 (million) % 34.21/5.76 % (1835928)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3357242232:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2962 on theBenchmark for (2962ds/273Mi) % 34.21/5.76 % (1835929)dis+10_1_to=kbo:sil=128000:tgt=ground:fde=unused:si=on:tha=some:sac=on:random_seed=461346785:i=102:nm=16:rtra=on_2962 on theBenchmark for (2962ds/102Mi) % 34.21/5.76 % (1835919)Instruction limit reached! % 34.21/5.76 % (1835919)------------------------------ % 34.21/5.76 % (1835919)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.21/5.76 % (1835919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.21/5.76 % (1835919)CaDiCaL version: 2.1.3 % 34.21/5.76 % (1835919)Termination reason: Instruction limit % 34.21/5.76 % (1835919)Termination phase: Saturation % 34.21/5.76 % (1835919)Time elapsed: 0.304 s % 34.21/5.76 % (1835919)Peak memory usage: 135 MB % 34.21/5.76 % (1835919)Instructions burned: 648 (million) % 34.21/5.76 % (1835929)Instruction limit reached! % 34.21/5.76 % (1835929)------------------------------ % 34.21/5.76 % (1835929)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.21/5.76 % (1835929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.21/5.76 % (1835929)CaDiCaL version: 2.1.3 % 34.21/5.76 % (1835929)Termination reason: Instruction limit % 34.21/5.76 % (1835929)Termination phase: Saturation % 34.21/5.76 % (1835929)Time elapsed: 0.022 s % 34.21/5.76 % (1835929)Peak memory usage: 89 MB % 34.21/5.76 % (1835929)Instructions burned: 103 (million) % 34.21/5.76 % (1835928)Instruction limit reached! % 34.21/5.76 % (1835928)------------------------------ % 34.21/5.76 % (1835928)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 34.21/5.76 % (1835928)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 34.21/5.76 % (1835928)CaDiCaL version: 2.1.3 % 34.21/5.76 % (1835928)Termination reason: Instruction limit % 34.21/5.76 % (1835928)Termination phase: Saturation % 34.21/5.76 % (1835928)Time elapsed: 0.110 s % 41.72/6.76 % (1835928)Peak memory usage: 90 MB % 41.72/6.76 % (1835928)Instructions burned: 274 (million) % 41.72/6.76 % (1835923)------------------------------ % 41.72/6.76 % (1835923)------------------------------ % 41.72/6.76 % (1835933)lrs+10_1_to=lpo:sil=128000:si=on:bsr=unit_only:tha=off:random_seed=2490830295:avsq=on:s2a=on:i=1094:s2at=5:avsqr=4463,131072:rtra=on_2960 on theBenchmark for (2960ds/1094Mi) % 41.72/6.76 % (1835925)------------------------------ % 41.72/6.76 % (1835925)------------------------------ % 41.72/6.76 % (1835934)dis+11_1_slsqr=1,2:to=lpo:plsq=on:si=on:norm_ineq=on:slsq=on:random_seed=4067580290:i=6400:doe=on:fsr=off:rtra=on_2960 on theBenchmark for (2960ds/6400Mi) % 41.72/6.76 % (1835935)dis+1011_12:1_to=lpo:sil=128000:tgt=full:sas=z3:si=on:sp=const_frequency:tha=off:slsqc=5:slsq=on:random_seed=1017018782:i=868:doe=on:nm=0:rtra=on:gtg=exists_sym_2960 on theBenchmark for (2960ds/868Mi) % 41.72/6.76 % (1835936)ott+1010_8_to=lpo:sil=128000:si=on:norm_ineq=on:sp=unary_frequency:sos=on:gve=cautious:spb=goal_then_units:uwa=alasca_main_floor:tha=some:random_seed=2550886605:i=1846:canc=cautious:fsr=off:rtra=on_2959 on theBenchmark for (2959ds/1846Mi) % 41.72/6.76 % (1835936)Refutation not found, incomplete strategy % 41.72/6.76 % (1835936)------------------------------ % 41.72/6.76 % (1835936)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.72/6.76 % (1835936)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.72/6.76 % (1835936)CaDiCaL version: 2.1.3 % 41.72/6.76 % (1835936)Termination reason: Refutation not found, incomplete strategy % 41.72/6.76 % (1835936)Time elapsed: 0.012 s % 41.72/6.76 % (1835936)Peak memory usage: 89 MB % 41.72/6.76 % (1835936)Instructions burned: 27 (million) % 41.72/6.76 % (1835921)Instruction limit reached! % 41.72/6.76 % (1835921)------------------------------ % 41.72/6.76 % (1835921)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.72/6.76 % (1835921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.72/6.76 % (1835921)CaDiCaL version: 2.1.3 % 41.72/6.76 % (1835921)Termination reason: Instruction limit % 41.72/6.76 % (1835921)Termination phase: Saturation % 41.72/6.76 % (1835921)Time elapsed: 0.465 s % 41.72/6.76 % (1835921)Peak memory usage: 113 MB % 41.72/6.76 % (1835921)Instructions burned: 1131 (million) % 41.72/6.76 % (1835938)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=876590028:s2a=on:i=36816:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2959 on theBenchmark for (2959ds/36816Mi) % 41.72/6.76 % (1835933)Instruction limit reached! % 41.72/6.76 % (1835933)------------------------------ % 41.72/6.76 % (1835933)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.72/6.76 % (1835933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.72/6.76 % (1835933)CaDiCaL version: 2.1.3 % 41.72/6.76 % (1835933)Termination reason: Instruction limit % 41.72/6.76 % (1835933)Termination phase: Saturation % 41.72/6.76 % (1835933)Time elapsed: 0.215 s % 41.72/6.76 % (1835933)Peak memory usage: 90 MB % 41.72/6.76 % (1835933)Instructions burned: 1094 (million) % 41.72/6.76 % (1835942)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=2883733439:i=273:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2958 on theBenchmark for (2958ds/273Mi) % 41.72/6.76 % (1835944)dis+1011_12:1_to=lpo:sil=128000:tgt=full:sas=z3:si=on:sp=const_frequency:tha=off:slsqc=5:slsq=on:random_seed=406815548:i=863:doe=on:nm=0:rtra=on:gtg=exists_sym_2957 on theBenchmark for (2957ds/863Mi) % 41.72/6.76 % (1835936)------------------------------ % 41.72/6.76 % (1835936)------------------------------ % 41.72/6.76 % (1835889)Instruction limit reached! % 41.72/6.76 % (1835889)------------------------------ % 41.72/6.76 % (1835889)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.72/6.76 % (1835889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 41.72/6.76 % (1835889)CaDiCaL version: 2.1.3 % 41.72/6.76 % (1835889)Termination reason: Instruction limit % 41.72/6.76 % (1835889)Termination phase: Saturation % 41.72/6.76 % (1835889)Time elapsed: 1.660 s % 41.72/6.76 % (1835889)Peak memory usage: 91 MB % 41.72/6.76 % (1835889)Instructions burned: 4428 (million) % 41.72/6.76 % (1835942)Instruction limit reached! % 41.72/6.76 % (1835942)------------------------------ % 41.72/6.76 % (1835942)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 41.72/6.76 % (1835942)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.85/7.65 % (1835942)CaDiCaL version: 2.1.3 % 48.85/7.65 % (1835942)Termination reason: Instruction limit % 48.85/7.65 % (1835942)Termination phase: Saturation % 48.85/7.65 % (1835942)Time elapsed: 0.109 s % 48.85/7.65 % (1835942)Peak memory usage: 90 MB % 48.85/7.65 % (1835942)Instructions burned: 273 (million) % 48.85/7.65 % (1835935)Instruction limit reached! % 48.85/7.65 % (1835935)------------------------------ % 48.85/7.65 % (1835935)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.85/7.65 % (1835935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.85/7.65 % (1835935)CaDiCaL version: 2.1.3 % 48.85/7.65 % (1835935)Termination reason: Instruction limit % 48.85/7.65 % (1835935)Termination phase: Saturation % 48.85/7.65 % (1835935)Time elapsed: 0.411 s % 48.85/7.65 % (1835935)Peak memory usage: 125 MB % 48.85/7.65 % (1835935)Instructions burned: 869 (million) % 48.85/7.65 % (1835947)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=3244082581:i=5811:kws=precedence:nm=0:rtra=on_2955 on theBenchmark for (2955ds/5811Mi) % 48.85/7.65 % (1835948)lrs+666_16:1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=reverse_arity:spb=goal_then_units:urr=on:uwa=off:tha=some:random_seed=142767009:i=2216:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2955 on theBenchmark for (2955ds/2216Mi) % 48.85/7.65 % (1835944)Instruction limit reached! % 48.85/7.65 % (1835944)------------------------------ % 48.85/7.65 % (1835944)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.85/7.65 % (1835944)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.85/7.65 % (1835944)CaDiCaL version: 2.1.3 % 48.85/7.65 % (1835944)Termination reason: Instruction limit % 48.85/7.65 % (1835944)Termination phase: Saturation % 48.85/7.65 % (1835944)Time elapsed: 0.213 s % 48.85/7.65 % (1835944)Peak memory usage: 123 MB % 48.85/7.65 % (1835944)Instructions burned: 866 (million) % 48.85/7.65 % (1835949)lrs+1011_12_to=kbo:tgt=ground:si=on:gve=force:acc=on:tha=off:random_seed=1652167263:i=801:kws=inv_arity_squared:rtra=on:gtg=exists_sym_2955 on theBenchmark for (2955ds/801Mi) % 48.85/7.65 % (1835951)dis+1011_14_to=kbo:tgt=ground:drc=ordering:fde=none:si=on:uwa=func_ext:tha=off:random_seed=661839638:st=5:i=1026:nm=32:av=off:rtra=on:ss=axioms:ev=cautious_2954 on theBenchmark for (2954ds/1026Mi) % 48.85/7.65 % (1835953)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=3490201541:i=3509:rtra=on_2954 on theBenchmark for (2954ds/3509Mi) % 48.85/7.65 % (1835951)Refutation not found, incomplete strategy % 48.85/7.65 % (1835951)------------------------------ % 48.85/7.65 % (1835951)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.85/7.65 % (1835951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.85/7.65 % (1835951)CaDiCaL version: 2.1.3 % 48.85/7.65 % (1835951)Termination reason: Refutation not found, incomplete strategy % 48.85/7.65 % (1835951)Time elapsed: 0.004 s % 48.85/7.65 % (1835951)Peak memory usage: 87 MB % 48.85/7.65 % (1835951)Instructions burned: 8 (million) % 48.85/7.65 % (1835949)Refutation not found, incomplete strategy % 48.85/7.65 % (1835949)------------------------------ % 48.85/7.65 % (1835949)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.85/7.65 % (1835949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.85/7.65 % (1835949)CaDiCaL version: 2.1.3 % 48.85/7.65 % (1835949)Termination reason: Refutation not found, incomplete strategy % 48.85/7.65 % (1835949)Time elapsed: 0.130 s % 48.85/7.65 % (1835949)Peak memory usage: 93 MB % 48.85/7.65 % (1835949)Instructions burned: 207 (million) % 48.85/7.65 % (1835951)------------------------------ % 48.85/7.65 % (1835951)------------------------------ % 48.85/7.65 % (1835949)------------------------------ % 48.85/7.65 % (1835949)------------------------------ % 48.85/7.65 % (1835957)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=2346960291:st=2:i=2127:sd=12:ep=R:rtra=on:ss=axioms_2950 on theBenchmark for (2950ds/2127Mi) % 48.85/7.65 % (1835957)Refutation not found, incomplete strategy % 48.85/7.65 % (1835957)------------------------------ % 48.85/7.65 % (1835957)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 48.85/7.65 % (1835957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 48.85/7.65 % (1835957)CaDiCaL version: 2.1.3 % 48.85/7.65 % (1835957)Termination reason: Refutation not found, incomplete strategy % 48.85/7.65 % (1835957)Time elapsed: 0.005 s % 48.85/7.65 % (1835957)Peak memory usage: 88 MB % 67.31/10.19 % (1835957)Instructions burned: 12 (million) % 67.31/10.19 % (1835958)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=1084914896:i=1959:rtra=on:fsd=on:proc=on_2950 on theBenchmark for (2950ds/1959Mi) % 67.31/10.19 % (1835957)------------------------------ % 67.31/10.19 % (1835957)------------------------------ % 67.31/10.19 % (1835953)Instruction limit reached! % 67.31/10.19 % (1835953)------------------------------ % 67.31/10.19 % (1835953)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.31/10.19 % (1835953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.31/10.19 % (1835953)CaDiCaL version: 2.1.3 % 67.31/10.19 % (1835953)Termination reason: Instruction limit % 67.31/10.19 % (1835953)Termination phase: Saturation % 67.31/10.19 % (1835953)Time elapsed: 0.675 s % 67.31/10.19 % (1835953)Peak memory usage: 90 MB % 67.31/10.19 % (1835953)Instructions burned: 3513 (million) % 67.31/10.19 % (1835961)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=2233654504:s2a=on:i=3553:nm=0:rtra=on_2946 on theBenchmark for (2946ds/3553Mi) % 67.31/10.19 % (1835948)Instruction limit reached! % 67.31/10.19 % (1835948)------------------------------ % 67.31/10.19 % (1835948)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.31/10.19 % (1835948)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.31/10.19 % (1835948)CaDiCaL version: 2.1.3 % 67.31/10.19 % (1835948)Termination reason: Instruction limit % 67.31/10.19 % (1835948)Termination phase: Saturation % 67.31/10.19 % (1835948)Time elapsed: 0.909 s % 67.31/10.19 % (1835948)Peak memory usage: 118 MB % 67.31/10.19 % (1835948)Instructions burned: 2216 (million) % 67.31/10.19 % (1835962)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2278855531:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2946 on theBenchmark for (2946ds/3201Mi) % 67.31/10.19 % (1835962)Refutation not found, incomplete strategy % 67.31/10.19 % (1835962)------------------------------ % 67.31/10.19 % (1835962)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.31/10.19 % (1835962)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.31/10.19 % (1835962)CaDiCaL version: 2.1.3 % 67.31/10.19 % (1835962)Termination reason: Refutation not found, incomplete strategy % 67.31/10.19 % (1835962)Time elapsed: 0.067 s % 67.31/10.19 % (1835962)Peak memory usage: 92 MB % 67.31/10.19 % (1835962)Instructions burned: 314 (million) % 67.31/10.19 % (1835965)lrs+1011_1_to=kbo:sil=64000:tgt=ground:thi=strong:plsq=on:sas=z3:si=on:plsqr=13711,262144:sp=const_max:sos=theory:thsqr=16,1:random_seed=81285907:thitd=on:cond=on:i=4093:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2945 on theBenchmark for (2945ds/4093Mi) % 67.31/10.19 % (1835962)------------------------------ % 67.31/10.19 % (1835962)------------------------------ % 67.31/10.19 % (1835967)lrs+1002_1_to=kbo:sil=128000:thi=neg_eq:sas=cadical:si=on:alasca=on:sp=occurrence:spb=intro:uwa=off:nwc=1:sac=on:random_seed=2325495995:cond=fast:i=21173:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2942 on theBenchmark for (2942ds/21173Mi) % 67.31/10.19 % (1835967)Refutation not found, incomplete strategy % 67.31/10.19 % (1835967)------------------------------ % 67.31/10.19 % (1835967)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.31/10.19 % (1835967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.31/10.19 % (1835967)CaDiCaL version: 2.1.3 % 67.31/10.19 % (1835967)Termination reason: Refutation not found, incomplete strategy % 67.31/10.19 % (1835967)Time elapsed: 0.017 s % 67.31/10.19 % (1835967)Peak memory usage: 112 MB % 67.31/10.19 % (1835967)Instructions burned: 10 (million) % 67.31/10.19 % (1835958)Instruction limit reached! % 67.31/10.19 % (1835958)------------------------------ % 67.31/10.19 % (1835958)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 67.31/10.19 % (1835958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 67.31/10.19 % (1835958)CaDiCaL version: 2.1.3 % 67.31/10.19 % (1835958)Termination reason: Instruction limit % 67.31/10.19 % (1835958)Termination phase: Saturation % 67.31/10.19 % (1835958)Time elapsed: 0.815 s % 67.31/10.19 % (1835958)Peak memory usage: 118 MB % 67.31/10.19 % (1835958)Instructions burned: 1959 (million) % 67.31/10.19 % (1835967)------------------------------ % 67.31/10.19 % (1835967)------------------------------ % 67.31/10.19 % (1835969)lrs+11_1_to=lpo:thi=all:sas=z3:si=on:fd=off:sac=on:slsq=on:random_seed=1646651459:avsq=on:i=10544:avsqr=17,4:canc=force:rtra=on:gtg=exists_top:er=filter_2940 on theBenchmark for (2940ds/10544Mi) % 77.21/11.63 % (1835970)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=832317576:avsq=on:i=1262:avsqr=1,16:rtra=on:rawr=on_2939 on theBenchmark for (2939ds/1262Mi) % 77.21/11.63 % (1835970)Instruction limit reached! % 77.21/11.63 % (1835970)------------------------------ % 77.21/11.63 % (1835970)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 77.21/11.63 % (1835970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.21/11.63 % (1835970)CaDiCaL version: 2.1.3 % 77.21/11.63 % (1835970)Termination reason: Instruction limit % 77.21/11.63 % (1835970)Termination phase: Saturation % 77.21/11.63 % (1835970)Time elapsed: 0.287 s % 77.21/11.63 % (1835970)Peak memory usage: 117 MB % 77.21/11.63 % (1835970)Instructions burned: 1267 (million) % 77.21/11.63 % (1835934)Instruction limit reached! % 77.21/11.63 % (1835934)------------------------------ % 77.21/11.63 % (1835934)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 77.21/11.63 % (1835934)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.21/11.63 % (1835934)CaDiCaL version: 2.1.3 % 77.21/11.63 % (1835934)Termination reason: Instruction limit % 77.21/11.63 % (1835934)Termination phase: Saturation % 77.21/11.63 % (1835934)Time elapsed: 2.365 s % 77.21/11.63 % (1835934)Peak memory usage: 92 MB % 77.21/11.63 % (1835934)Instructions burned: 6402 (million) % 77.21/11.63 % (1835973)lrs+1002_1_to=kbo:sil=64000:tgt=ground:si=on:random_seed=83455964:s2a=on:i=775:s2at=3:kws=precedence:doe=on:fsr=off:rtra=on:ss=axioms_2935 on theBenchmark for (2935ds/775Mi) % 77.21/11.63 % (1835973)Refutation not found, incomplete strategy % 77.21/11.63 % (1835973)------------------------------ % 77.21/11.63 % (1835973)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 77.21/11.63 % (1835973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.21/11.63 % (1835973)CaDiCaL version: 2.1.3 % 77.21/11.63 % (1835973)Termination reason: Refutation not found, incomplete strategy % 77.21/11.63 % (1835973)Time elapsed: 0.003 s % 77.21/11.63 % (1835973)Peak memory usage: 88 MB % 77.21/11.63 % (1835973)Instructions burned: 13 (million) % 77.21/11.63 % (1835974)dis+1011_2_to=kbo:sil=128000:tgt=full:irw=on:si=on:sp=unary_frequency:gve=cautious:nwc=5.53:random_seed=3468788880:i=270:kws=precedence:canc=cautious:nm=10:rtra=on:tar=off:rawr=on_2935 on theBenchmark for (2935ds/270Mi) % 77.21/11.63 % (1835974)Instruction limit reached! % 77.21/11.63 % (1835974)------------------------------ % 77.21/11.63 % (1835974)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 77.21/11.63 % (1835974)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.21/11.63 % (1835974)CaDiCaL version: 2.1.3 % 77.21/11.63 % (1835974)Termination reason: Instruction limit % 77.21/11.63 % (1835974)Termination phase: Saturation % 77.21/11.63 % (1835974)Time elapsed: 0.109 s % 77.21/11.63 % (1835974)Peak memory usage: 90 MB % 77.21/11.63 % (1835974)Instructions burned: 272 (million) % 77.21/11.63 % (1835973)------------------------------ % 77.21/11.63 % (1835973)------------------------------ % 77.21/11.63 % (1835961)Instruction limit reached! % 77.21/11.63 % (1835961)------------------------------ % 77.21/11.63 % (1835961)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 77.21/11.63 % (1835961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 77.21/11.63 % (1835961)CaDiCaL version: 2.1.3 % 77.21/11.63 % (1835961)Termination reason: Instruction limit % 77.21/11.63 % (1835961)Termination phase: Saturation % 77.21/11.63 % (1835961)Time elapsed: 1.343 s % 77.21/11.63 % (1835961)Peak memory usage: 91 MB % 77.21/11.63 % (1835961)Instructions burned: 3554 (million) % 77.21/11.63 % (1835978)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=2409355142:s2a=on:i=13094:s2at=-1:rtra=on_2932 on theBenchmark for (2932ds/13094Mi) % 77.21/11.63 % (1835977)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=1562254880:i=17165:aac=none:doe=on:rtra=on:gtg=exists_all_2933 on theBenchmark for (2933ds/17165Mi) % 77.21/11.63 % (1835979)lrs+10_1_to=lpo:sil=128000:si=on:sp=occurrence:random_seed=2333283079:st=2:i=12633:rtra=on:ss=axioms_2931 on theBenchmark for (2931ds/12633Mi) % 77.21/11.63 % (1835979)Refutation not found, incomplete strategy % 77.21/11.63 % (1835979)------------------------------ % 77.21/11.63 % (1835979)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 89.12/13.24 % (1835979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.12/13.24 % (1835979)CaDiCaL version: 2.1.3 % 89.12/13.24 % (1835979)Termination reason: Refutation not found, incomplete strategy % 89.12/13.24 % (1835979)Time elapsed: 0.005 s % 89.12/13.24 % (1835979)Peak memory usage: 88 MB % 89.12/13.24 % (1835979)Instructions burned: 9 (million) % 89.12/13.24 % (1835947)Instruction limit reached! % 89.12/13.24 % (1835947)------------------------------ % 89.12/13.24 % (1835947)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 89.12/13.24 % (1835947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.12/13.24 % (1835947)CaDiCaL version: 2.1.3 % 89.12/13.24 % (1835947)Termination reason: Instruction limit % 89.12/13.24 % (1835947)Termination phase: Saturation % 89.12/13.24 % (1835947)Time elapsed: 2.457 s % 89.12/13.24 % (1835947)Peak memory usage: 118 MB % 89.12/13.24 % (1835947)Instructions burned: 5813 (million) % 89.12/13.24 % (1835983)dis+1011_1_to=kbo:sil=64000:tgt=ground:sas=z3:si=on:sp=const_frequency:lsd=20:nwc=3:random_seed=3912014113:i=1783:rtra=on:gtg=position_2929 on theBenchmark for (2929ds/1783Mi) % 89.12/13.24 % (1835979)------------------------------ % 89.12/13.24 % (1835979)------------------------------ % 89.12/13.24 % (1835965)Instruction limit reached! % 89.12/13.24 % (1835965)------------------------------ % 89.12/13.24 % (1835965)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 89.12/13.24 % (1835965)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.12/13.24 % (1835965)CaDiCaL version: 2.1.3 % 89.12/13.24 % (1835965)Termination reason: Instruction limit % 89.12/13.24 % (1835965)Termination phase: Saturation % 89.12/13.24 % (1835965)Time elapsed: 1.615 s % 89.12/13.24 % (1835965)Peak memory usage: 137 MB % 89.12/13.24 % (1835965)Instructions burned: 4095 (million) % 89.12/13.24 % (1835985)dis+10_1_to=kbo:sil=128000:tgt=ground:plsq=on:plsqc=2:sas=z3:si=on:plsqr=2,1:norm_ineq=on:random_seed=1792182645:i=5451:aac=none:doe=on:nm=0:rtra=on:amm=off:gtg=position_2927 on theBenchmark for (2927ds/5451Mi) % 89.12/13.24 % (1835986)dis+1011_12:1_to=lpo:sil=128000:tgt=full:sas=z3:si=on:sp=const_frequency:tha=off:slsqc=5:slsq=on:random_seed=4112995480:i=4975:doe=on:nm=0:rtra=on:gtg=exists_sym_2927 on theBenchmark for (2927ds/4975Mi) % 89.12/13.24 % (1835983)Instruction limit reached! % 89.12/13.24 % (1835983)------------------------------ % 89.12/13.24 % (1835983)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 89.12/13.24 % (1835983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.12/13.24 % (1835983)CaDiCaL version: 2.1.3 % 89.12/13.24 % (1835983)Termination reason: Instruction limit % 89.12/13.24 % (1835983)Termination phase: Saturation % 89.12/13.24 % (1835983)Time elapsed: 0.709 s % 89.12/13.24 % (1835983)Peak memory usage: 119 MB % 89.12/13.24 % (1835983)Instructions burned: 1786 (million) % 89.12/13.24 % (1835989)lrs+666_16:1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=reverse_arity:spb=goal_then_units:urr=on:uwa=off:tha=some:random_seed=2771210070:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2920 on theBenchmark for (2920ds/2076Mi) % 89.12/13.24 % (1835989)Instruction limit reached! % 89.12/13.24 % (1835989)------------------------------ % 89.12/13.24 % (1835989)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 89.12/13.24 % (1835989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.12/13.24 % (1835989)CaDiCaL version: 2.1.3 % 89.12/13.24 % (1835989)Termination reason: Instruction limit % 89.12/13.24 % (1835989)Termination phase: Saturation % 89.12/13.24 % (1835989)Time elapsed: 0.840 s % 89.12/13.24 % (1835989)Peak memory usage: 118 MB % 89.12/13.24 % (1835989)Instructions burned: 2078 (million) % 89.12/13.24 % (1835991)dis+1011_1_to=kbo:sil=128000:tgt=full:si=on:spb=intro:lsd=50:tha=some:fd=preordered:sac=on:random_seed=419294456:i=5145:rtra=on_2910 on theBenchmark for (2910ds/5145Mi) % 89.12/13.24 % (1835978)Instruction limit reached! % 89.12/13.24 % (1835978)------------------------------ % 89.12/13.24 % (1835978)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 89.12/13.24 % (1835978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 89.12/13.24 % (1835978)CaDiCaL version: 2.1.3 % 89.12/13.24 % (1835978)Termination reason: Instruction limit % 89.12/13.24 % (1835978)Termination phase: Saturation % 89.12/13.24 % (1835978)Time elapsed: 2.550 s % 89.12/13.24 % (1835978)Peak memory usage: 103 MB % 89.12/13.24 % (1835978)Instructions burned: 13099 (million) % 89.12/13.24 % (1835993)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=2144152946:i=3509:rtra=on_2906 on theBenchmark for (2906ds/3509Mi) % 183.04/26.49 % (1835986)Instruction limit reached! % 183.04/26.49 % (1835986)------------------------------ % 183.04/26.49 % (1835986)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 183.04/26.49 % (1835986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.04/26.49 % (1835986)CaDiCaL version: 2.1.3 % 183.04/26.49 % (1835986)Termination reason: Instruction limit % 183.04/26.49 % (1835986)Termination phase: Saturation % 183.04/26.49 % (1835986)Time elapsed: 2.208 s % 183.04/26.49 % (1835986)Peak memory usage: 127 MB % 183.04/26.49 % (1835986)Instructions burned: 4975 (million) % 183.04/26.49 % (1835995)lrs+10_1_to=kbo:sil=128000:si=on:norm_ineq=on:random_seed=2960317537:st=2:i=13800:sd=12:ep=R:rtra=on:ss=axioms_2903 on theBenchmark for (2903ds/13800Mi) % 183.04/26.49 % (1835995)Refutation not found, incomplete strategy % 183.04/26.49 % (1835995)------------------------------ % 183.04/26.49 % (1835995)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 183.04/26.49 % (1835995)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.04/26.49 % (1835995)CaDiCaL version: 2.1.3 % 183.04/26.49 % (1835995)Termination reason: Refutation not found, incomplete strategy % 183.04/26.49 % (1835995)Time elapsed: 0.003 s % 183.04/26.49 % (1835995)Peak memory usage: 88 MB % 183.04/26.49 % (1835995)Instructions burned: 12 (million) % 183.04/26.49 % (1835985)Instruction limit reached! % 183.04/26.49 % (1835985)------------------------------ % 183.04/26.49 % (1835985)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 183.04/26.49 % (1835985)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.04/26.49 % (1835985)CaDiCaL version: 2.1.3 % 183.04/26.49 % (1835985)Termination reason: Instruction limit % 183.04/26.49 % (1835985)Termination phase: Saturation % 183.04/26.49 % (1835985)Time elapsed: 2.378 s % 183.04/26.49 % (1835985)Peak memory usage: 122 MB % 183.04/26.49 % (1835985)Instructions burned: 5452 (million) % 183.04/26.49 % (1835995)------------------------------ % 183.04/26.49 % (1835995)------------------------------ % 183.04/26.49 % (1835997)ott+1011_1_to=lpo:prc=on:sas=z3:si=on:taea=off:tha=off:gs=on:nwc=2:newcnf=on:random_seed=1962742893:i=1412:rtra=on:fsd=on:proc=on_2902 on theBenchmark for (2902ds/1412Mi) % 183.04/26.49 % (1835998)WARNING Broken Constraint: if demodulation_redundancy_check(ordering) has been set then forward_demodulation(off) is not equal to off or backward_demodulation(off) is not equal to off or partial_redundancy_check(off) is not equal to off % 183.04/26.49 % (1835998)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=2809145772:i=11747:aac=none:nm=0:rtra=on:rawr=on_2900 on theBenchmark for (2900ds/11747Mi) % 183.04/26.49 % (1835997)Instruction limit reached! % 183.04/26.49 % (1835997)------------------------------ % 183.04/26.49 % (1835997)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 183.04/26.49 % (1835997)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.04/26.49 % (1835997)CaDiCaL version: 2.1.3 % 183.04/26.49 % (1835997)Termination reason: Instruction limit % 183.04/26.49 % (1835997)Termination phase: Saturation % 183.04/26.49 % (1835997)Time elapsed: 0.605 s % 183.04/26.49 % (1835997)Peak memory usage: 118 MB % 183.04/26.49 % (1835997)Instructions burned: 1414 (million) % 183.04/26.49 % (1836001)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=1729298694:s2a=on:i=3553:nm=0:rtra=on_2894 on theBenchmark for (2894ds/3553Mi) % 183.04/26.49 % (1835993)Instruction limit reached! % 183.04/26.49 % (1835993)------------------------------ % 183.04/26.49 % (1835993)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 183.04/26.49 % (1835993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 183.04/26.49 % (1835993)CaDiCaL version: 2.1.3 % 183.04/26.49 % (1835993)Termination reason: Instruction limit % 183.04/26.49 % (1835993)Termination phase: Saturation % 183.04/26.49 % (1835993)Time elapsed: 1.185 s % 183.04/26.49 % (1835993)Peak memory usage: 90 MB % 183.04/26.49 % (1835993)Instructions burned: 3510 (million) % 183.04/26.49 % (1836003)ott+21_1024_to=lakbo:sil=128000:bsd=on:si=on:alasca=on:uwa=alasca_main:nwc=0.5:random_seed=2047777376:cond=on:i=3201:fgj=on:ep=RS:asg=force:nm=10:rtra=on:rawr=on_2892 on theBenchmark for (2892ds/3201Mi) % 183.04/26.49 % (1836003)Refutation not found, incomplete strategy % 183.04/26.49 % (1836003)------------------------------ % 183.04/26.49 % (1836003)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 225.31/32.47 % (1836003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.31/32.47 % (1836003)CaDiCaL version: 2.1.3 % 225.31/32.47 % (1836003)Termination reason: Refutation not found, incomplete strategy % 225.31/32.47 % (1836003)Time elapsed: 0.101 s % 225.31/32.47 % (1836003)Peak memory usage: 92 MB % 225.31/32.47 % (1836003)Instructions burned: 253 (million) % 225.31/32.47 % (1835991)Instruction limit reached! % 225.31/32.47 % (1835991)------------------------------ % 225.31/32.47 % (1835991)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 225.31/32.47 % (1835991)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.31/32.47 % (1835991)CaDiCaL version: 2.1.3 % 225.31/32.47 % (1835991)Termination reason: Instruction limit % 225.31/32.47 % (1835991)Termination phase: Saturation % 225.31/32.47 % (1835991)Time elapsed: 1.976 s % 225.31/32.47 % (1835991)Peak memory usage: 95 MB % 225.31/32.47 % (1835991)Instructions burned: 5146 (million) % 225.31/32.47 % (1836003)------------------------------ % 225.31/32.47 % (1836003)------------------------------ % 225.31/32.47 % (1836005)lrs+1011_1_to=kbo:sil=64000:tgt=ground:thi=strong:plsq=on:sas=z3:si=on:plsqr=13711,262144:sp=const_max:sos=theory:thsqr=16,1:random_seed=3209525021:thitd=on:cond=on:i=4081:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2889 on theBenchmark for (2889ds/4081Mi) % 225.31/32.47 % (1835969)Instruction limit reached! % 225.31/32.47 % (1835969)------------------------------ % 225.31/32.47 % (1835969)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 225.31/32.47 % (1835969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.31/32.47 % (1835969)CaDiCaL version: 2.1.3 % 225.31/32.47 % (1835969)Termination reason: Instruction limit % 225.31/32.47 % (1835969)Termination phase: Saturation % 225.31/32.47 % (1835969)Time elapsed: 5.242 s % 225.31/32.47 % (1835969)Peak memory usage: 191 MB % 225.31/32.47 % (1835969)Instructions burned: 10545 (million) % 225.31/32.47 % (1836006)lrs+1002_1_to=kbo:sil=128000:thi=neg_eq:sas=cadical:si=on:alasca=on:sp=occurrence:spb=intro:uwa=off:nwc=1:sac=on:random_seed=1428324373:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2887 on theBenchmark for (2887ds/20260Mi) % 225.31/32.47 % (1836006)Refutation not found, incomplete strategy % 225.31/32.47 % (1836006)------------------------------ % 225.31/32.47 % (1836006)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 225.31/32.47 % (1836006)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.31/32.47 % (1836006)CaDiCaL version: 2.1.3 % 225.31/32.47 % (1836006)Termination reason: Refutation not found, incomplete strategy % 225.31/32.47 % (1836006)Time elapsed: 0.028 s % 225.31/32.47 % (1836006)Peak memory usage: 112 MB % 225.31/32.47 % (1836006)Instructions burned: 10 (million) % 225.31/32.47 % (1836009)lrs+35_1_drc=ordering:si=on:norm_ineq=on:tha=off:random_seed=2729148253:s2a=on:i=58627:s2at=3:aac=none:rtra=on:amm=off:rawr=on_2886 on theBenchmark for (2886ds/58627Mi) % 225.31/32.47 % (1836006)------------------------------ % 225.31/32.47 % (1836006)------------------------------ % 225.31/32.47 % (1836011)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=461211603:avsq=on:i=6258:avsqr=1,16:rtra=on:rawr=on_2883 on theBenchmark for (2883ds/6258Mi) % 225.31/32.47 % (1836001)Instruction limit reached! % 225.31/32.47 % (1836001)------------------------------ % 225.31/32.47 % (1836001)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 225.31/32.47 % (1836001)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.31/32.47 % (1836001)CaDiCaL version: 2.1.3 % 225.31/32.47 % (1836001)Termination reason: Instruction limit % 225.31/32.47 % (1836001)Termination phase: Saturation % 225.31/32.47 % (1836001)Time elapsed: 1.299 s % 225.31/32.47 % (1836001)Peak memory usage: 91 MB % 225.31/32.47 % (1836001)Instructions burned: 3555 (million) % 225.31/32.47 % (1836013)ott+10_128_isp=bottom:to=lpo:sil=128000:si=on:urr=on:uwa=alasca_main:sac=on:slsq=on:random_seed=3967514836:i=34001:aac=none:doe=on:rtra=on:gtg=exists_all_2879 on theBenchmark for (2879ds/34001Mi) % 225.31/32.47 % (1835998)Instruction limit reached! % 225.31/32.47 % (1835998)------------------------------ % 225.31/32.47 % (1835998)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 225.31/32.47 % (1835998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 225.31/32.47 % (1835998)CaDiCaL version: 2.1.3 % 225.31/32.47 % (1835998)Termination reason: Instruction limit % 225.31/32.47 % (1835998)Termination phase: Saturation % 257.32/37.04 % (1835998)Time elapsed: 2.533 s % 257.32/37.04 % (1835998)Peak memory usage: 119 MB % 257.32/37.04 % (1835998)Instructions burned: 11749 (million) % 257.32/37.04 % (1836015)lrs+2_10_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_main:tha=some:random_seed=454788678:s2a=on:i=71622:s2at=-1:rtra=on_2874 on theBenchmark for (2874ds/71622Mi) % 257.32/37.04 % (1836005)Instruction limit reached! % 257.32/37.04 % (1836005)------------------------------ % 257.32/37.04 % (1836005)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 257.32/37.04 % (1836005)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.32/37.04 % (1836005)CaDiCaL version: 2.1.3 % 257.32/37.04 % (1836005)Termination reason: Instruction limit % 257.32/37.04 % (1836005)Termination phase: Saturation % 257.32/37.04 % (1836005)Time elapsed: 1.602 s % 257.32/37.04 % (1836005)Peak memory usage: 138 MB % 257.32/37.04 % (1836005)Instructions burned: 4081 (million) % 257.32/37.04 % (1836017)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=2460910336:i=24001:kws=precedence:nm=0:rtra=on_2871 on theBenchmark for (2871ds/24001Mi) % 257.32/37.04 % (1835977)Instruction limit reached! % 257.32/37.04 % (1835977)------------------------------ % 257.32/37.04 % (1835977)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 257.32/37.04 % (1835977)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.32/37.04 % (1835977)CaDiCaL version: 2.1.3 % 257.32/37.04 % (1835977)Termination reason: Instruction limit % 257.32/37.04 % (1835977)Termination phase: Saturation % 257.32/37.04 % (1835977)Time elapsed: 6.396 s % 257.32/37.04 % (1835977)Peak memory usage: 95 MB % 257.32/37.04 % (1835977)Instructions burned: 17165 (million) % 257.32/37.04 % (1836019)lrs+666_16:1_to=kbo:sil=128000:sas=z3:si=on:norm_ineq=on:sp=reverse_arity:spb=goal_then_units:urr=on:uwa=off:tha=some:random_seed=1231196704:i=2076:gtgl=2:aac=none:rtra=on:gtg=all:tac=axiom_2867 on theBenchmark for (2867ds/2076Mi) % 257.32/37.04 % (1836019)Instruction limit reached! % 257.32/37.04 % (1836019)------------------------------ % 257.32/37.04 % (1836019)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 257.32/37.04 % (1836019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.32/37.04 % (1836019)CaDiCaL version: 2.1.3 % 257.32/37.04 % (1836019)Termination reason: Instruction limit % 257.32/37.04 % (1836019)Termination phase: Saturation % 257.32/37.04 % (1836019)Time elapsed: 0.847 s % 257.32/37.04 % (1836019)Peak memory usage: 118 MB % 257.32/37.04 % (1836019)Instructions burned: 2078 (million) % 257.32/37.04 % (1836216)dis+21_20_to=lakbo:si=on:alasca=on:sp=const_max:uwa=alasca_main:sac=on:random_seed=3680638249:s2a=on:i=83971:s2at=4:bd=all:ins=1:rtra=on_2857 on theBenchmark for (2857ds/83971Mi) % 257.32/37.04 % (1836011)Instruction limit reached! % 257.32/37.04 % (1836011)------------------------------ % 257.32/37.04 % (1836011)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 257.32/37.04 % (1836011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.32/37.04 % (1836011)CaDiCaL version: 2.1.3 % 257.32/37.04 % (1836011)Termination reason: Instruction limit % 257.32/37.04 % (1836011)Termination phase: Saturation % 257.32/37.04 % (1836011)Time elapsed: 2.656 s % 257.32/37.04 % (1836011)Peak memory usage: 118 MB % 257.32/37.04 % (1836011)Instructions burned: 6260 (million) % 257.32/37.04 % (1836264)lrs+1011_5:1_to=lpo:sil=128000:sas=z3:si=on:norm_ineq=on:tha=some:random_seed=1443111842:i=83944:rtra=on_2855 on theBenchmark for (2855ds/83944Mi) % 257.32/37.04 % (1835938)Instruction limit reached! % 257.32/37.04 % (1835938)------------------------------ % 257.32/37.04 % (1835938)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 257.32/37.04 % (1835938)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 257.32/37.04 % (1835938)CaDiCaL version: 2.1.3 % 257.32/37.04 % (1835938)Termination reason: Instruction limit % 257.32/37.04 % (1835938)Termination phase: Saturation % 257.32/37.04 % (1835938)Time elapsed: 15.166 s % 257.32/37.04 % (1835938)Peak memory usage: 108 MB % 257.32/37.04 % (1835938)Instructions burned: 36817 (million) % 257.32/37.04 % (1836439)lrs+10_1_to=lpo:sil=64000:si=on:spb=goal_then_units:random_seed=1949074660:i=9201:rtra=on_2806 on theBenchmark for (2806ds/9201Mi) % 257.32/37.04 % (1836439)Instruction limit reached! % 257.32/37.04 % (1836439)------------------------------ % 257.32/37.04 % (1836439)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 257.32/37.04 % (1836439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.51/41.43 % (1836439)CaDiCaL version: 2.1.3 % 289.51/41.43 % (1836439)Termination reason: Instruction limit % 289.51/41.43 % (1836439)Termination phase: Saturation % 289.51/41.43 % (1836439)Time elapsed: 6.134 s % 289.51/41.43 % (1836439)Peak memory usage: 90 MB % 289.51/41.43 % (1836439)Instructions burned: 9201 (million) % 289.51/41.43 % (1836513)WARNING Broken Constraint: if demodulation_redundancy_check(ordering) has been set then forward_demodulation(off) is not equal to off or backward_demodulation(off) is not equal to off or partial_redundancy_check(off) is not equal to off % 289.51/41.43 % (1836513)lrs+1010_1_to=lpo:drc=ordering:sims=off:sas=z3:si=on:tha=off:fd=off:random_seed=1317696684:i=6806:aac=none:nm=0:rtra=on:rawr=on_2741 on theBenchmark for (2741ds/6806Mi) % 289.51/41.43 % (1836017)Instruction limit reached! % 289.51/41.43 % (1836017)------------------------------ % 289.51/41.43 % (1836017)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 289.51/41.43 % (1836017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.51/41.43 % (1836017)CaDiCaL version: 2.1.3 % 289.51/41.43 % (1836017)Termination reason: Instruction limit % 289.51/41.43 % (1836017)Termination phase: Saturation % 289.51/41.43 % (1836017)Time elapsed: 15.871 s % 289.51/41.43 % (1836017)Peak memory usage: 120 MB % 289.51/41.43 % (1836017)Instructions burned: 24001 (million) % 289.51/41.43 % (1836534)lrs+1010_1_to=kbo:sil=128000:si=on:newcnf=on:random_seed=114746505:s2a=on:i=3553:nm=0:rtra=on_2711 on theBenchmark for (2711ds/3553Mi) % 289.51/41.43 % (1836013)Instruction limit reached! % 289.51/41.43 % (1836013)------------------------------ % 289.51/41.43 % (1836013)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 289.51/41.43 % (1836013)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.51/41.43 % (1836013)CaDiCaL version: 2.1.3 % 289.51/41.43 % (1836013)Termination reason: Instruction limit % 289.51/41.43 % (1836013)Termination phase: Saturation % 289.51/41.43 % (1836013)Time elapsed: 18.952 s % 289.51/41.43 % (1836013)Peak memory usage: 99 MB % 289.51/41.43 % (1836013)Instructions burned: 34002 (million) % 289.51/41.43 % (1836538)lrs+1011_1_to=kbo:sil=64000:tgt=ground:thi=strong:plsq=on:sas=z3:si=on:plsqr=13711,262144:sp=const_max:sos=theory:thsqr=16,1:random_seed=4198184720:thitd=on:cond=on:i=2064:thsqd=32:asg=cautious:thsqc=32:rtra=on:sstl=2:thsq=on_2688 on theBenchmark for (2688ds/2064Mi) % 289.51/41.43 % (1836513)Instruction limit reached! % 289.51/41.43 % (1836513)------------------------------ % 289.51/41.43 % (1836513)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 289.51/41.43 % (1836513)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.51/41.43 % (1836513)CaDiCaL version: 2.1.3 % 289.51/41.43 % (1836513)Termination reason: Instruction limit % 289.51/41.43 % (1836513)Termination phase: Saturation % 289.51/41.43 % (1836513)Time elapsed: 5.375 s % 289.51/41.43 % (1836513)Peak memory usage: 119 MB % 289.51/41.43 % (1836513)Instructions burned: 6807 (million) % 289.51/41.43 % (1836534)Instruction limit reached! % 289.51/41.43 % (1836534)------------------------------ % 289.51/41.43 % (1836534)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 289.51/41.43 % (1836534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.51/41.43 % (1836534)CaDiCaL version: 2.1.3 % 289.51/41.43 % (1836534)Termination reason: Instruction limit % 289.51/41.43 % (1836534)Termination phase: Saturation % 289.51/41.43 % (1836534)Time elapsed: 2.417 s % 289.51/41.43 % (1836534)Peak memory usage: 91 MB % 289.51/41.43 % (1836534)Instructions burned: 3555 (million) % 289.51/41.43 % (1836541)lrs+1002_1_to=kbo:sil=128000:thi=neg_eq:sas=cadical:si=on:alasca=on:sp=occurrence:spb=intro:uwa=off:nwc=1:sac=on:random_seed=3818397163:cond=fast:i=20260:sd=10:alascaa=on:rtra=on:tac=axiom:ss=axioms:sgt=64_2685 on theBenchmark for (2685ds/20260Mi) % 289.51/41.43 % (1836541)Refutation not found, incomplete strategy % 289.51/41.43 % (1836541)------------------------------ % 289.51/41.43 % (1836541)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200) % 289.51/41.43 % (1836541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c % 289.51/41.43 % (1836541)CaDiCaL version: 2.1.3 % 289.51/41.43 % (1836541)Termination reason: Refutation not found, incomplete strategy % 289.51/41.43 % (1836541)Time elapsed: 0.042 s % 289.51/41.43 % (1836541)Peak memory usage: 112 MB % 289.51/41.43 % (1836541)Instructions burned: 10 (million) % 289.51/41.43 % (1836542)lrs+11_1_plsq=on:drc=ordering:sas=z3:si=on:avsql=on:norm_ineq=on:urr=on:tha=off:random_seed=2074936944:avsq=on:i=1244:avsqr=1,16:Terminated %------------------------------------------------------------------------------