%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ARI585_1 : TPTP v9.3.1. Released v5.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:34:55 AM UTC 2026
% Result : Theorem 8.71s 1.84s
% Output : Refutation 8.71s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ARI585_1 : TPTP v9.3.1. Released v5.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.22 % Computer : n006.cluster.edu
% 0.09/0.22 % Model : x86_64 x86_64
% 0.09/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.22 % Memory : 8046.5625MB
% 0.09/0.22 % OS : Linux 6.8.0-71-generic
% 0.09/0.22 % CPULimit : 300
% 0.09/0.22 % WCLimit : 300
% 0.09/0.22 % DateTime : Mon Sep 28 20:52:40 UTC 2026
% 0.09/0.22 % CPUTime :
% 0.09/0.22 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.27 Running first-order model finding
% 0.09/0.27 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 7.00/1.32 % (183354)Will run a generic schedule for satisfiability detection.
% 7.00/1.32 % (183360)% WARNING: option uhcvi not known.
% 7.00/1.32 % (183360)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3187181038:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 7.00/1.32 % (183359)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2605345299_2999 on theBenchmark for (2999ds/0Mi)
% 7.00/1.32 % (183359)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 7.00/1.32 % (183359)Terminated due to inappropriate strategy.
% 7.00/1.32 % (183359)------------------------------
% 7.00/1.32 % (183359)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.00/1.32 % (183359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.00/1.32 % (183359)CaDiCaL version: 2.1.3
% 7.00/1.32 % (183359)Termination reason: Inappropriate
% 7.00/1.32 % (183359)Time elapsed: 0.0000 s
% 7.00/1.32 % (183359)Peak memory usage: 10 MB
% 7.00/1.32 % (183359)------------------------------
% 7.00/1.32 % (183359)------------------------------
% 7.00/1.32 % (183363)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2463336910:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 7.00/1.32 % (183362)dis+10_1_sil=32000:sp=arity:random_seed=2268608409:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 7.00/1.32 % (183361)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3893758472:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 7.00/1.32 % (183364)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4217967927:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 7.00/1.32 % (183365)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=356925392:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 7.00/1.32 % (183368)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2628591598:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 7.00/1.32 % (183368)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 7.00/1.32 % (183368)Terminated due to inappropriate strategy.
% 7.00/1.32 % (183368)------------------------------
% 7.00/1.32 % (183368)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.00/1.32 % (183368)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.00/1.32 % (183368)CaDiCaL version: 2.1.3
% 7.00/1.32 % (183368)Termination reason: Inappropriate
% 7.00/1.32 % (183368)Time elapsed: 0.0000 s
% 7.00/1.32 % (183368)Peak memory usage: 10 MB
% 7.00/1.32 % (183368)------------------------------
% 7.00/1.32 % (183368)------------------------------
% 7.00/1.32 % (183375)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=873429275:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 7.00/1.32 % (183362)Instruction limit reached!
% 7.00/1.32 % (183362)------------------------------
% 7.00/1.32 % (183362)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.00/1.32 % (183362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.00/1.32 % (183362)CaDiCaL version: 2.1.3
% 7.00/1.32 % (183362)Termination reason: Instruction limit
% 7.00/1.32 % (183362)Termination phase: Saturation
% 7.00/1.32 % (183362)Time elapsed: 0.108 s
% 7.00/1.32 % (183362)Peak memory usage: 12 MB
% 7.00/1.32 % (183362)Instructions burned: 104 (million)
% 7.00/1.32 % (183363)Instruction limit reached!
% 7.00/1.32 % (183363)------------------------------
% 7.00/1.32 % (183363)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.00/1.32 % (183363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.00/1.32 % (183363)CaDiCaL version: 2.1.3
% 7.00/1.32 % (183363)Termination reason: Instruction limit
% 7.00/1.32 % (183363)Termination phase: Saturation
% 7.00/1.32 % (183363)Time elapsed: 0.109 s
% 7.00/1.32 % (183363)Peak memory usage: 13 MB
% 7.00/1.32 % (183363)Instructions burned: 117 (million)
% 7.00/1.32 % (183377)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=2354145788:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 7.00/1.32 % (183364)Instruction limit reached!
% 7.00/1.32 % (183364)------------------------------
% 7.00/1.32 % (183364)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.00/1.32 % (183364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.71/1.83 % (183364)CaDiCaL version: 2.1.3
% 8.71/1.83 % (183364)Termination reason: Instruction limit
% 8.71/1.83 % (183364)Termination phase: Saturation
% 8.71/1.83 % (183364)Time elapsed: 0.135 s
% 8.71/1.83 % (183364)Peak memory usage: 12 MB
% 8.71/1.83 % (183364)Instructions burned: 131 (million)
% 8.71/1.83 % (183378)ott-21_1_sil=16000:fs=off:random_seed=3325289418:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 8.71/1.83 % (183380)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=38291847:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 8.71/1.83 % (183375)Instruction limit reached!
% 8.71/1.83 % (183375)------------------------------
% 8.71/1.83 % (183375)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.71/1.83 % (183375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.71/1.83 % (183375)CaDiCaL version: 2.1.3
% 8.71/1.83 % (183375)Termination reason: Instruction limit
% 8.71/1.83 % (183375)Termination phase: Saturation
% 8.71/1.83 % (183375)Time elapsed: 0.130 s
% 8.71/1.83 % (183375)Peak memory usage: 13 MB
% 8.71/1.83 % (183375)Instructions burned: 131 (million)
% 8.71/1.83 % (183365)Instruction limit reached!
% 8.71/1.83 % (183365)------------------------------
% 8.71/1.83 % (183365)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.71/1.83 % (183365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.71/1.83 % (183365)CaDiCaL version: 2.1.3
% 8.71/1.83 % (183365)Termination reason: Instruction limit
% 8.71/1.83 % (183365)Termination phase: Saturation
% 8.71/1.83 % (183365)Time elapsed: 0.180 s
% 8.71/1.83 % (183365)Peak memory usage: 13 MB
% 8.71/1.83 % (183365)Instructions burned: 159 (million)
% 8.71/1.83 % (183384)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3844086561:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 8.71/1.83 % (183383)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1808532307:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 8.71/1.83 % (183383)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 8.71/1.83 % (183383)Terminated due to inappropriate strategy.
% 8.71/1.83 % (183383)------------------------------
% 8.71/1.83 % (183383)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.71/1.83 % (183383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.71/1.83 % (183383)CaDiCaL version: 2.1.3
% 8.71/1.83 % (183383)Termination reason: Inappropriate
% 8.71/1.83 % (183383)Time elapsed: 0.001 s
% 8.71/1.83 % (183383)Peak memory usage: 9 MB
% 8.71/1.83 % (183383)------------------------------
% 8.71/1.83 % (183383)------------------------------
% 8.71/1.83 % (183387)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3612124426:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi)
% 8.71/1.83 % (183387)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 8.71/1.83 % (183387)Terminated due to inappropriate strategy.
% 8.71/1.83 % (183387)------------------------------
% 8.71/1.83 % (183387)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.71/1.83 % (183387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.71/1.83 % (183387)CaDiCaL version: 2.1.3
% 8.71/1.83 % (183387)Termination reason: Inappropriate
% 8.71/1.83 % (183387)Time elapsed: 0.001 s
% 8.71/1.83 % (183387)Peak memory usage: 10 MB
% 8.71/1.83 % (183387)------------------------------
% 8.71/1.83 % (183387)------------------------------
% 8.71/1.83 % (183378)Instruction limit reached!
% 8.71/1.83 % (183378)------------------------------
% 8.71/1.83 % (183378)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.71/1.83 % (183378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.71/1.83 % (183378)CaDiCaL version: 2.1.3
% 8.71/1.83 % (183378)Termination reason: Instruction limit
% 8.71/1.83 % (183378)Termination phase: Saturation
% 8.71/1.83 % (183378)Time elapsed: 0.139 s
% 8.71/1.83 % (183378)Peak memory usage: 12 MB
% 8.71/1.83 % (183378)Instructions burned: 180 (million)
% 8.71/1.83 % (183389)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=1997104639:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi)
% 8.71/1.83 % (183390)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1185890029:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi)
% 8.71/1.83 % (183380)Instruction limit reached!
% 8.71/1.83 % (183380)------------------------------
% 8.71/1.83 % (183380)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.71/1.83 % (183380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.71/1.83 % (183380)CaDiCaL version: 2.1.3
% 8.71/1.83 % (183380)Termination reason: Instruction limit
% 8.71/1.83 % (183380)Termination phase: Saturation
% 8.71/1.83 % (183380)Time elapsed: 0.515 s
% 8.71/1.83 % (183380)Peak memory usage: 15 MB
% 8.71/1.83 % (183380)Instructions burned: 477 (million)
% 8.71/1.83 % (183393)fmb+10_1_sil=64000:random_seed=2739724109:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi)
% 8.71/1.83 % (183393)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 8.71/1.83 % (183393)Terminated due to inappropriate strategy.
% 8.71/1.83 % (183393)------------------------------
% 8.71/1.83 % (183393)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.71/1.83 % (183393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.71/1.83 % (183393)CaDiCaL version: 2.1.3
% 8.71/1.83 % (183393)Termination reason: Inappropriate
% 8.71/1.83 % (183393)Time elapsed: 0.001 s
% 8.71/1.83 % (183393)Peak memory usage: 10 MB
% 8.71/1.83 % (183393)------------------------------
% 8.71/1.83 % (183393)------------------------------
% 8.71/1.83 % (183395)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=825375737:i=9515:nm=5_2992 on theBenchmark for (2992ds/9515Mi)
% 8.71/1.83 % (183395)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 8.71/1.83 % (183395)Terminated due to inappropriate strategy.
% 8.71/1.83 % (183395)------------------------------
% 8.71/1.83 % (183395)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.71/1.83 % (183395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.71/1.83 % (183395)CaDiCaL version: 2.1.3
% 8.71/1.83 % (183395)Termination reason: Inappropriate
% 8.71/1.83 % (183395)Time elapsed: 0.0000 s
% 8.71/1.83 % (183395)Peak memory usage: 10 MB
% 8.71/1.83 % (183395)------------------------------
% 8.71/1.83 % (183395)------------------------------
% 8.71/1.83 % (183377)Instruction limit reached!
% 8.71/1.83 % (183377)------------------------------
% 8.71/1.83 % (183377)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.71/1.83 % (183377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.71/1.83 % (183377)CaDiCaL version: 2.1.3
% 8.71/1.83 % (183377)Termination reason: Instruction limit
% 8.71/1.83 % (183377)Termination phase: Saturation
% 8.71/1.83 % (183377)Time elapsed: 0.625 s
% 8.71/1.83 % (183377)Peak memory usage: 16 MB
% 8.71/1.83 % (183377)Instructions burned: 685 (million)
% 8.71/1.83 % (183398)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1294200565:i=5131_2992 on theBenchmark for (2992ds/5131Mi)
% 8.71/1.83 % (183397)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1258006337:fmbsr=1.7:i=920_2992 on theBenchmark for (2992ds/920Mi)
% 8.71/1.83 % (183397)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 8.71/1.83 % (183397)Terminated due to inappropriate strategy.
% 8.71/1.83 % (183397)------------------------------
% 8.71/1.83 % (183397)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.71/1.83 % (183397)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.71/1.83 % (183397)CaDiCaL version: 2.1.3
% 8.71/1.83 % (183397)Termination reason: Inappropriate
% 8.71/1.83 % (183397)Time elapsed: 0.001 s
% 8.71/1.83 % (183397)Peak memory usage: 10 MB
% 8.71/1.83 % (183397)------------------------------
% 8.71/1.83 % (183397)------------------------------
% 8.71/1.83 % (183401)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2218075999:i=1472:ins=7:fdi=8:gsp=on_2991 on theBenchmark for (2991ds/1472Mi)
% 8.71/1.83 % (183389)Instruction limit reached!
% 8.71/1.83 % (183389)------------------------------
% 8.71/1.83 % (183389)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.71/1.83 % (183389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.71/1.83 % (183389)CaDiCaL version: 2.1.3
% 8.71/1.83 % (183389)Termination reason: Instruction limit
% 8.71/1.83 % (183389)Termination phase: Saturation
% 8.71/1.83 % (183389)Time elapsed: 0.689 s
% 8.71/1.83 % (183389)Peak memory usage: 18 MB
% 8.71/1.83 % (183389)Instructions burned: 693 (million)
% 8.71/1.83 % (183403)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1115167126:i=6324_2989 on theBenchmark for (2989ds/6324Mi)
% 8.71/1.84 % (183403)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 8.71/1.84 % (183403)Terminated due to inappropriate strategy.
% 8.71/1.84 % (183403)------------------------------
% 8.71/1.84 % (183403)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.71/1.84 % (183403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.71/1.84 % (183403)CaDiCaL version: 2.1.3
% 8.71/1.84 % (183403)Termination reason: Inappropriate
% 8.71/1.84 % (183403)Time elapsed: 0.0000 s
% 8.71/1.84 % (183403)Peak memory usage: 10 MB
% 8.71/1.84 % (183403)------------------------------
% 8.71/1.84 % (183403)------------------------------
% 8.71/1.84 % (183405)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1844114662:fmbsr=2.30978:i=2174_2989 on theBenchmark for (2989ds/2174Mi)
% 8.71/1.84 % (183405)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 8.71/1.84 % (183405)Terminated due to inappropriate strategy.
% 8.71/1.84 % (183405)------------------------------
% 8.71/1.84 % (183405)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.71/1.84 % (183405)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.71/1.84 % (183405)CaDiCaL version: 2.1.3
% 8.71/1.84 % (183405)Termination reason: Inappropriate
% 8.71/1.84 % (183405)Time elapsed: 0.0000 s
% 8.71/1.84 % (183405)Peak memory usage: 10 MB
% 8.71/1.84 % (183405)------------------------------
% 8.71/1.84 % (183405)------------------------------
% 8.71/1.84 % (183407)ott-2_1_sil=16000:newcnf=on:random_seed=1140076959:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2989 on theBenchmark for (2989ds/869Mi)
% 8.71/1.84 % (183390)Instruction limit reached!
% 8.71/1.84 % (183390)------------------------------
% 8.71/1.84 % (183390)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.71/1.84 % (183390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.71/1.84 % (183390)CaDiCaL version: 2.1.3
% 8.71/1.84 % (183390)Termination reason: Instruction limit
% 8.71/1.84 % (183390)Termination phase: Saturation
% 8.71/1.84 % (183390)Time elapsed: 0.811 s
% 8.71/1.84 % (183390)Peak memory usage: 20 MB
% 8.71/1.84 % (183390)Instructions burned: 879 (million)
% 8.71/1.84 % (183409)ott+10_1_sil=32000:tgt=ground:random_seed=2577753047:i=5114:av=off_2988 on theBenchmark for (2988ds/5114Mi)
% 8.71/1.84 % (183384)Instruction limit reached!
% 8.71/1.84 % (183384)------------------------------
% 8.71/1.84 % (183384)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.71/1.84 % (183384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.71/1.84 % (183384)CaDiCaL version: 2.1.3
% 8.71/1.84 % (183384)Termination reason: Instruction limit
% 8.71/1.84 % (183384)Termination phase: Saturation
% 8.71/1.84 % (183384)Time elapsed: 1.233 s
% 8.71/1.84 % (183384)Peak memory usage: 17 MB
% 8.71/1.84 % (183384)Instructions burned: 1179 (million)
% 8.71/1.84 % (183411)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3100934430:i=54282_2985 on theBenchmark for (2985ds/54282Mi)
% 8.71/1.84 % (183411)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 8.71/1.84 % (183411)Terminated due to inappropriate strategy.
% 8.71/1.84 % (183411)------------------------------
% 8.71/1.84 % (183411)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.71/1.84 % (183411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.71/1.84 % (183411)CaDiCaL version: 2.1.3
% 8.71/1.84 % (183411)Termination reason: Inappropriate
% 8.71/1.84 % (183411)Time elapsed: 0.0000 s
% 8.71/1.84 % (183411)Peak memory usage: 10 MB
% 8.71/1.84 % (183411)------------------------------
% 8.71/1.84 % (183411)------------------------------
% 8.71/1.84 % (183413)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1447576435:i=3512:aac=none_2985 on theBenchmark for (2985ds/3512Mi)
% 8.71/1.84 % (183409) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-183354-183409"...
% 8.71/1.84 % (183409)...printing done.
% 8.71/1.84 % (183409)Refutation found. Thanks to Tanya!
% 8.71/1.84 % SZS status Theorem for theBenchmark
% 8.71/1.84 % SZS output start Proof for theBenchmark
% 8.71/1.84 tff(func_def_7, type, sK0: $int).
% 8.71/1.84 tff(func_def_8, type, sK1: $int > $int).
% 8.71/1.84 tff(func_def_9, type, sF2: $int).
% 8.71/1.84 tff(func_def_10, type, sF3: $int).
% 8.71/1.84 tff(f1,conjecture,(
% 8.71/1.84 ! [X0 : $int] : ? [X1 : $int] : ! [X2 : $int] : (($less($sum(X0,5),X2) & $less(X2,$sum(X0,8))) => ($less(X1,X2) & $less(X2,$sum(X1,4))))),
% 8.71/1.84 file('/export/starexec/sandbox/benchmark/theBenchmark.p',interv_4_can_cover_interv_3)).
% 8.71/1.84 tff(f2,negated_conjecture,(
% 8.71/1.84 ~ ! [X0 : $int] : ? [X1 : $int] : ! [X2 : $int] : (($less($sum(X0,5),X2) & $less(X2,$sum(X0,8))) => ($less(X1,X2) & $less(X2,$sum(X1,4))))),
% 8.71/1.84 inference(negated_conjecture,[status(cth)],[f1])).
% 8.71/1.84 tff(f3,definition,(
% 8.71/1.84 ( ! [X0 : $int,X1 : $int] : ($sum(X0,X1) = $sum(X1,X0)) )),
% 8.71/1.84 introduced(theory,[tha_commutativity])).
% 8.71/1.84 tff(f4,definition,(
% 8.71/1.84 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($sum(X0,$sum(X1,X2)) = $sum($sum(X0,X1),X2)) )),
% 8.71/1.84 introduced(theory,[tha_associativity])).
% 8.71/1.84 tff(f9,definition,(
% 8.71/1.84 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~$less(X1,X2) | ~$less(X0,X1) | $less(X0,X2)) )),
% 8.71/1.84 introduced(theory,[tha_transitivity])).
% 8.71/1.84 tff(f11,definition,(
% 8.71/1.84 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($less($sum(X0,X2),$sum(X1,X2)) | ~$less(X0,X1)) )),
% 8.71/1.84 introduced(theory,[tha_order_monotonicity])).
% 8.71/1.84 tff(f15,plain,(
% 8.71/1.84 ? [X0 : $int] : ! [X1 : $int] : ? [X2 : $int] : ((~$less(X1,X2) | ~$less(X2,$sum(X1,4))) & ($less($sum(X0,5),X2) & $less(X2,$sum(X0,8))))),
% 8.71/1.84 inference(ennf_transformation,[],[f2])).
% 8.71/1.84 tff(f16,plain,(
% 8.71/1.84 ? [X0 : $int] : ! [X1 : $int] : ? [X2 : $int] : ((~$less(X1,X2) | ~$less(X2,$sum(X1,4))) & $less($sum(X0,5),X2) & $less(X2,$sum(X0,8)))),
% 8.71/1.84 inference(flattening,[],[f15])).
% 8.71/1.84 tff(f17,plain,(
% 8.71/1.84 ! [X1 : $int] : ((~$less(X1,sK1(X1)) | ~$less(sK1(X1),$sum(X1,4))) & $less($sum(sK0,5),sK1(X1)) & $less(sK1(X1),$sum(sK0,8)))),
% 8.71/1.84 inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(X0,sK0),skolemize(X2,sK1(X1))],[f16])).
% 8.71/1.84 tff(f18,plain,(
% 8.71/1.84 ( ! [X1 : $int] : ($less(sK1(X1),$sum(sK0,8))) )),
% 8.71/1.84 inference(cnf_transformation,[],[f17])).
% 8.71/1.84 tff(f19,plain,(
% 8.71/1.84 ( ! [X1 : $int] : ($less($sum(sK0,5),sK1(X1))) )),
% 8.71/1.84 inference(cnf_transformation,[],[f17])).
% 8.71/1.84 tff(f20,plain,(
% 8.71/1.84 ( ! [X1 : $int] : (~$less(sK1(X1),$sum(X1,4)) | ~$less(X1,sK1(X1))) )),
% 8.71/1.84 inference(cnf_transformation,[],[f17])).
% 8.71/1.84 tff(f21,definition,(
% 8.71/1.84 sF2 = $sum(sK0,5)),
% 8.71/1.84 introduced(definition,[new_symbols(definition,[sF2])],[function_definition])).
% 8.71/1.84 tff(f22,plain,(
% 8.71/1.84 $sum(sK0,5) = sF2),
% 8.71/1.84 inference(reorient_equations,[],[f21])).
% 8.71/1.84 tff(f23,plain,(
% 8.71/1.84 ( ! [X1 : $int] : ($less(sF2,sK1(X1))) )),
% 8.71/1.84 inference(definition_folding,[],[f19,f22])).
% 8.71/1.84 tff(f24,definition,(
% 8.71/1.84 sF3 = $sum(sK0,8)),
% 8.71/1.84 introduced(definition,[new_symbols(definition,[sF3])],[function_definition])).
% 8.71/1.84 tff(f25,plain,(
% 8.71/1.84 $sum(sK0,8) = sF3),
% 8.71/1.84 inference(reorient_equations,[],[f24])).
% 8.71/1.84 tff(f26,plain,(
% 8.71/1.84 ( ! [X1 : $int] : ($less(sK1(X1),sF3)) )),
% 8.71/1.84 inference(definition_folding,[],[f18,f25])).
% 8.71/1.84 tff(f27,plain,(
% 8.71/1.84 sF2 = $sum(5,sK0)),
% 8.71/1.84 inference(forward_demodulation,[],[f22,f3])).
% 8.71/1.84 tff(f28,plain,(
% 8.71/1.84 sF3 = $sum(8,sK0)),
% 8.71/1.84 inference(forward_demodulation,[],[f25,f3])).
% 8.71/1.84 tff(f88,plain,(
% 8.71/1.84 ( ! [X0 : $int] : ($less(sF3,$sum(X0,sK0)) | ~$less(8,X0)) )),
% 8.71/1.84 inference(superposition,[],[f11,f28])).
% 8.71/1.84 tff(f116,plain,(
% 8.71/1.84 ( ! [X0 : $int,X1 : $int] : (~$less(sK1($sum(X0,X1)),$sum(X0,$sum(X1,4))) | ~$less($sum(X0,X1),sK1($sum(X0,X1)))) )),
% 8.71/1.84 inference(superposition,[],[f20,f4])).
% 8.71/1.84 tff(f129,plain,(
% 8.71/1.84 ( ! [X0 : $int,X1 : $int] : (~$less(sK1($sum(X0,X1)),$sum(X1,$sum(X0,4))) | ~$less($sum(X0,X1),sK1($sum(X0,X1)))) )),
% 8.71/1.84 inference(superposition,[],[f116,f3])).
% 8.71/1.84 tff(f195,plain,(
% 8.71/1.84 ( ! [X0 : $int,X1 : $int] : ($less(X1,$sum(X0,sK0)) | ~$less(X1,sF3) | ~$less(8,X0)) )),
% 8.71/1.84 inference(resolution,[],[f88,f9])).
% 8.71/1.84 tff(f1937,plain,(
% 8.71/1.84 ~$less(sK1(sF2),$sum(sK0,$sum(5,4))) | ~$less(sF2,sK1(sF2))),
% 8.71/1.84 inference(superposition,[],[f129,f27])).
% 8.71/1.84 tff(f1963,plain,(
% 8.71/1.84 ~$less(sK1(sF2),$sum(sK0,9)) | ~$less(sF2,sK1(sF2))),
% 8.71/1.84 inference(evaluation,[],[f1937])).
% 8.71/1.84 tff(f1981,plain,(
% 8.71/1.84 ~$less(sK1(sF2),$sum(sK0,9))),
% 8.71/1.84 inference(forward_subsumption_resolution,[],[f1963,f23])).
% 8.71/1.84 tff(f1996,plain,(
% 8.71/1.84 ~$less(sK1(sF2),$sum(9,sK0))),
% 8.71/1.84 inference(forward_demodulation,[],[f1981,f3])).
% 8.71/1.84 tff(f7818,plain,(
% 8.71/1.84 ~$less(sK1(sF2),sF3) | ~$less(8,9)),
% 8.71/1.84 inference(resolution,[],[f195,f1996])).
% 8.71/1.84 tff(f7828,plain,(
% 8.71/1.84 ~$less(sK1(sF2),sF3)),
% 8.71/1.84 inference(evaluation,[],[f7818])).
% 8.71/1.84 tff(f7829,plain,(
% 8.71/1.84 $false),
% 8.71/1.84 inference(forward_subsumption_resolution,[],[f7828,f26])).
% 8.71/1.84 % SZS output end Proof for theBenchmark
% 8.71/1.84 % (183409)------------------------------
% 8.71/1.84 % (183409)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.71/1.84 % (183409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.71/1.84 % (183409)CaDiCaL version: 2.1.3
% 8.71/1.84 % (183409)Termination reason: Refutation
% 8.71/1.84 % (183409)Time elapsed: 0.355 s
% 8.71/1.84 % (183409)Peak memory usage: 14 MB
% 8.71/1.84 % (183409)Instructions burned: 367 (million)
% 8.71/1.84 % (183354)Success in time 1.551 s
% 8.71/1.84 % Vampire exiting
%------------------------------------------------------------------------------