%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ARI607_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 : n003.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:57 AM UTC 2026
% Result : Theorem 8.57s 1.61s
% Output : Refutation 8.57s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : ARI607_1 : TPTP v9.3.1. Released v5.1.0.
% 0.00/0.07 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.24 % Computer : n003.cluster.edu
% 0.11/0.24 % Model : x86_64 x86_64
% 0.11/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.24 % Memory : 8046.5625MB
% 0.11/0.24 % OS : Linux 6.8.0-71-generic
% 0.11/0.24 % CPULimit : 300
% 0.11/0.24 % WCLimit : 300
% 0.11/0.24 % DateTime : Mon Sep 28 20:55:12 UTC 2026
% 0.11/0.25 % CPUTime :
% 0.11/0.25 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.11/0.28 Running first-order model finding
% 0.11/0.28 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
% 5.39/1.12 % (2003326)Will run a generic schedule for satisfiability detection.
% 5.39/1.12 % (2003334)dis+10_1_sil=32000:sp=arity:random_seed=2449960511:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 5.39/1.12 % (2003331)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1186488464_2999 on theBenchmark for (2999ds/0Mi)
% 5.39/1.12 % (2003331)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 5.39/1.12 % (2003331)Terminated due to inappropriate strategy.
% 5.39/1.12 % (2003331)------------------------------
% 5.39/1.12 % (2003331)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.39/1.12 % (2003331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.39/1.12 % (2003331)CaDiCaL version: 2.1.3
% 5.39/1.12 % (2003331)Termination reason: Inappropriate
% 5.39/1.12 % (2003331)Time elapsed: 0.0000 s
% 5.39/1.12 % (2003331)Peak memory usage: 10 MB
% 5.39/1.12 % (2003331)------------------------------
% 5.39/1.12 % (2003331)------------------------------
% 5.39/1.12 % (2003332)% WARNING: option uhcvi not known.
% 5.39/1.12 % (2003332)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=342438754:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 5.39/1.12 % (2003336)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2462193012:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 5.39/1.12 % (2003333)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3971982034:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 5.39/1.12 % (2003337)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=517137351:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 5.39/1.12 % (2003335)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2160172558:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 5.39/1.12 % (2003340)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=218978805:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 5.39/1.12 % (2003340)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 5.39/1.12 % (2003340)Terminated due to inappropriate strategy.
% 5.39/1.12 % (2003340)------------------------------
% 5.39/1.12 % (2003340)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.39/1.12 % (2003340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.39/1.12 % (2003340)CaDiCaL version: 2.1.3
% 5.39/1.12 % (2003340)Termination reason: Inappropriate
% 5.39/1.12 % (2003340)Time elapsed: 0.001 s
% 5.39/1.12 % (2003340)Peak memory usage: 10 MB
% 5.39/1.12 % (2003340)------------------------------
% 5.39/1.12 % (2003340)------------------------------
% 5.39/1.12 % (2003334)Instruction limit reached!
% 5.39/1.12 % (2003334)------------------------------
% 5.39/1.12 % (2003334)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.39/1.12 % (2003334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.39/1.12 % (2003334)CaDiCaL version: 2.1.3
% 5.39/1.12 % (2003334)Termination reason: Instruction limit
% 5.39/1.12 % (2003334)Termination phase: Saturation
% 5.39/1.12 % (2003334)Time elapsed: 0.055 s
% 5.39/1.12 % (2003334)Peak memory usage: 12 MB
% 5.39/1.12 % (2003334)Instructions burned: 104 (million)
% 5.39/1.12 % (2003347)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2467884328:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 5.39/1.12 % (2003348)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=3664572766:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 5.39/1.12 % (2003335)Instruction limit reached!
% 5.39/1.12 % (2003335)------------------------------
% 5.39/1.12 % (2003335)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.39/1.12 % (2003335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.39/1.12 % (2003335)CaDiCaL version: 2.1.3
% 5.39/1.12 % (2003335)Termination reason: Instruction limit
% 5.39/1.12 % (2003335)Termination phase: Saturation
% 5.39/1.12 % (2003335)Time elapsed: 0.112 s
% 5.39/1.12 % (2003335)Peak memory usage: 12 MB
% 5.39/1.12 % (2003335)Instructions burned: 116 (million)
% 5.39/1.12 % (2003336)Instruction limit reached!
% 5.39/1.12 % (2003336)------------------------------
% 5.39/1.12 % (2003336)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.39/1.12 % (2003336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.57/1.60 % (2003336)CaDiCaL version: 2.1.3
% 8.57/1.60 % (2003336)Termination reason: Instruction limit
% 8.57/1.60 % (2003336)Termination phase: Saturation
% 8.57/1.60 % (2003336)Time elapsed: 0.127 s
% 8.57/1.60 % (2003336)Peak memory usage: 12 MB
% 8.57/1.60 % (2003336)Instructions burned: 131 (million)
% 8.57/1.60 % (2003351)ott-21_1_sil=16000:fs=off:random_seed=3065137119:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 8.57/1.60 % (2003352)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1166804072:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 8.57/1.60 % (2003337)Instruction limit reached!
% 8.57/1.60 % (2003337)------------------------------
% 8.57/1.60 % (2003337)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.57/1.60 % (2003337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.57/1.60 % (2003337)CaDiCaL version: 2.1.3
% 8.57/1.60 % (2003337)Termination reason: Instruction limit
% 8.57/1.60 % (2003337)Termination phase: Saturation
% 8.57/1.60 % (2003337)Time elapsed: 0.166 s
% 8.57/1.61 % (2003337)Peak memory usage: 13 MB
% 8.57/1.61 % (2003337)Instructions burned: 159 (million)
% 8.57/1.61 % (2003355)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=657898012:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 8.57/1.61 % (2003355)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 8.57/1.61 % (2003355)Terminated due to inappropriate strategy.
% 8.57/1.61 % (2003355)------------------------------
% 8.57/1.61 % (2003355)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.57/1.61 % (2003355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.57/1.61 % (2003355)CaDiCaL version: 2.1.3
% 8.57/1.61 % (2003355)Termination reason: Inappropriate
% 8.57/1.61 % (2003355)Time elapsed: 0.0000 s
% 8.57/1.61 % (2003355)Peak memory usage: 10 MB
% 8.57/1.61 % (2003355)------------------------------
% 8.57/1.61 % (2003355)------------------------------
% 8.57/1.61 % (2003347)Instruction limit reached!
% 8.57/1.61 % (2003347)------------------------------
% 8.57/1.61 % (2003347)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.57/1.61 % (2003347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.57/1.61 % (2003347)CaDiCaL version: 2.1.3
% 8.57/1.61 % (2003347)Termination reason: Instruction limit
% 8.57/1.61 % (2003347)Termination phase: Saturation
% 8.57/1.61 % (2003347)Time elapsed: 0.136 s
% 8.57/1.61 % (2003347)Peak memory usage: 13 MB
% 8.57/1.61 % (2003347)Instructions burned: 131 (million)
% 8.57/1.61 % (2003357)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1725532797:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 8.57/1.61 % (2003358)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=475938809:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi)
% 8.57/1.61 % (2003358)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 8.57/1.61 % (2003358)Terminated due to inappropriate strategy.
% 8.57/1.61 % (2003358)------------------------------
% 8.57/1.61 % (2003358)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.57/1.61 % (2003358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.57/1.61 % (2003358)CaDiCaL version: 2.1.3
% 8.57/1.61 % (2003358)Termination reason: Inappropriate
% 8.57/1.61 % (2003358)Time elapsed: 0.0000 s
% 8.57/1.61 % (2003358)Peak memory usage: 10 MB
% 8.57/1.61 % (2003358)------------------------------
% 8.57/1.61 % (2003358)------------------------------
% 8.57/1.61 % (2003361)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=2346545851: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.57/1.61 % (2003351)Instruction limit reached!
% 8.57/1.61 % (2003351)------------------------------
% 8.57/1.61 % (2003351)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.57/1.61 % (2003351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.57/1.61 % (2003351)CaDiCaL version: 2.1.3
% 8.57/1.61 % (2003351)Termination reason: Instruction limit
% 8.57/1.61 % (2003351)Termination phase: Saturation
% 8.57/1.61 % (2003351)Time elapsed: 0.143 s
% 8.57/1.61 % (2003351)Peak memory usage: 12 MB
% 8.57/1.61 % (2003351)Instructions burned: 180 (million)
% 8.57/1.61 % (2003363)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3003652145:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi)
% 8.57/1.61 % (2003348)Instruction limit reached!
% 8.57/1.61 % (2003348)------------------------------
% 8.57/1.61 % (2003348)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.57/1.61 % (2003348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.57/1.61 % (2003348)CaDiCaL version: 2.1.3
% 8.57/1.61 % (2003348)Termination reason: Instruction limit
% 8.57/1.61 % (2003348)Termination phase: Saturation
% 8.57/1.61 % (2003348)Time elapsed: 0.332 s
% 8.57/1.61 % (2003348)Peak memory usage: 16 MB
% 8.57/1.61 % (2003348)Instructions burned: 685 (million)
% 8.57/1.61 % (2003365)fmb+10_1_sil=64000:random_seed=3506093164:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi)
% 8.57/1.61 % (2003365)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 8.57/1.61 % (2003365)Terminated due to inappropriate strategy.
% 8.57/1.61 % (2003365)------------------------------
% 8.57/1.61 % (2003365)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.57/1.61 % (2003365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.57/1.61 % (2003365)CaDiCaL version: 2.1.3
% 8.57/1.61 % (2003365)Termination reason: Inappropriate
% 8.57/1.61 % (2003365)Time elapsed: 0.001 s
% 8.57/1.61 % (2003365)Peak memory usage: 10 MB
% 8.57/1.61 % (2003365)------------------------------
% 8.57/1.61 % (2003365)------------------------------
% 8.57/1.61 % (2003367)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=406556765:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi)
% 8.57/1.61 % (2003367)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 8.57/1.61 % (2003367)Terminated due to inappropriate strategy.
% 8.57/1.61 % (2003367)------------------------------
% 8.57/1.61 % (2003367)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.57/1.61 % (2003367)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.57/1.61 % (2003367)CaDiCaL version: 2.1.3
% 8.57/1.61 % (2003367)Termination reason: Inappropriate
% 8.57/1.61 % (2003367)Time elapsed: 0.0000 s
% 8.57/1.61 % (2003367)Peak memory usage: 10 MB
% 8.57/1.61 % (2003367)------------------------------
% 8.57/1.61 % (2003367)------------------------------
% 8.57/1.61 % (2003369)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3986743576:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi)
% 8.57/1.61 % (2003369)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 8.57/1.61 % (2003369)Terminated due to inappropriate strategy.
% 8.57/1.61 % (2003369)------------------------------
% 8.57/1.61 % (2003369)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.57/1.61 % (2003369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.57/1.61 % (2003369)CaDiCaL version: 2.1.3
% 8.57/1.61 % (2003369)Termination reason: Inappropriate
% 8.57/1.61 % (2003369)Time elapsed: 0.001 s
% 8.57/1.61 % (2003369)Peak memory usage: 10 MB
% 8.57/1.61 % (2003369)------------------------------
% 8.57/1.61 % (2003369)------------------------------
% 8.57/1.61 % (2003371)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1816225552:i=5131_2994 on theBenchmark for (2994ds/5131Mi)
% 8.57/1.61 % (2003352)Instruction limit reached!
% 8.57/1.61 % (2003352)------------------------------
% 8.57/1.61 % (2003352)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.57/1.61 % (2003352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.57/1.61 % (2003352)CaDiCaL version: 2.1.3
% 8.57/1.61 % (2003352)Termination reason: Instruction limit
% 8.57/1.61 % (2003352)Termination phase: Saturation
% 8.57/1.61 % (2003352)Time elapsed: 0.488 s
% 8.57/1.61 % (2003352)Peak memory usage: 13 MB
% 8.57/1.61 % (2003352)Instructions burned: 477 (million)
% 8.57/1.61 % (2003373)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2831106287:i=1472:ins=7:fdi=8:gsp=on_2993 on theBenchmark for (2993ds/1472Mi)
% 8.57/1.61 % (2003363)Instruction limit reached!
% 8.57/1.61 % (2003363)------------------------------
% 8.57/1.61 % (2003363)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.57/1.61 % (2003363)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.57/1.61 % (2003363)CaDiCaL version: 2.1.3
% 8.57/1.61 % (2003363)Termination reason: Instruction limit
% 8.57/1.61 % (2003363)Termination phase: Saturation
% 8.57/1.61 % (2003363)Time elapsed: 0.469 s
% 8.57/1.61 % (2003363)Peak memory usage: 21 MB
% 8.57/1.61 % (2003363)Instructions burned: 881 (million)
% 8.57/1.61 % (2003375)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1577466367:i=6324_2991 on theBenchmark for (2991ds/6324Mi)
% 8.57/1.61 % (2003375)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 8.57/1.61 % (2003375)Terminated due to inappropriate strategy.
% 8.57/1.61 % (2003375)------------------------------
% 8.57/1.61 % (2003375)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.57/1.61 % (2003375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.57/1.61 % (2003375)CaDiCaL version: 2.1.3
% 8.57/1.61 % (2003375)Termination reason: Inappropriate
% 8.57/1.61 % (2003375)Time elapsed: 0.0000 s
% 8.57/1.61 % (2003375)Peak memory usage: 10 MB
% 8.57/1.61 % (2003375)------------------------------
% 8.57/1.61 % (2003375)------------------------------
% 8.57/1.61 % (2003377)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3404292122:fmbsr=2.30978:i=2174_2991 on theBenchmark for (2991ds/2174Mi)
% 8.57/1.61 % (2003377)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 8.57/1.61 % (2003377)Terminated due to inappropriate strategy.
% 8.57/1.61 % (2003377)------------------------------
% 8.57/1.61 % (2003377)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.57/1.61 % (2003377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.57/1.61 % (2003377)CaDiCaL version: 2.1.3
% 8.57/1.61 % (2003377)Termination reason: Inappropriate
% 8.57/1.61 % (2003377)Time elapsed: 0.0000 s
% 8.57/1.61 % (2003377)Peak memory usage: 10 MB
% 8.57/1.61 % (2003377)------------------------------
% 8.57/1.61 % (2003377)------------------------------
% 8.57/1.61 % (2003379)ott-2_1_sil=16000:newcnf=on:random_seed=2863535732:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2991 on theBenchmark for (2991ds/869Mi)
% 8.57/1.61 % (2003361)Instruction limit reached!
% 8.57/1.61 % (2003361)------------------------------
% 8.57/1.61 % (2003361)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.57/1.61 % (2003361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.57/1.61 % (2003361)CaDiCaL version: 2.1.3
% 8.57/1.61 % (2003361)Termination reason: Instruction limit
% 8.57/1.61 % (2003361)Termination phase: Saturation
% 8.57/1.61 % (2003361)Time elapsed: 0.646 s
% 8.57/1.61 % (2003361)Peak memory usage: 17 MB
% 8.57/1.61 % (2003361)Instructions burned: 692 (million)
% 8.57/1.61 % (2003381)ott+10_1_sil=32000:tgt=ground:random_seed=2878528810:i=5114:av=off_2990 on theBenchmark for (2990ds/5114Mi)
% 8.57/1.61 % (2003381) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2003326-2003381"...
% 8.57/1.61 % (2003381)...printing done.
% 8.57/1.61 % (2003381)Refutation found. Thanks to Tanya!
% 8.57/1.61 % SZS status Theorem for theBenchmark
% 8.57/1.61 % SZS output start Proof for theBenchmark
% 8.57/1.61 tff(func_def_0, type, f: $int > $int).
% 8.57/1.61 tff(func_def_9, type, sF0: $int).
% 8.57/1.61 tff(func_def_10, type, sF1: $int).
% 8.57/1.61 tff(func_def_11, type, sF2: $int).
% 8.57/1.61 tff(func_def_12, type, sF3: $int).
% 8.57/1.61 tff(func_def_13, type, sF4: $int).
% 8.57/1.61 tff(func_def_14, type, sF5: $int).
% 8.57/1.61 tff(f1,conjecture,(
% 8.57/1.61 ! [X0 : $int,X1 : $int] : ($lesseq(X0,X1) => $lesseq(f(X0),f(X1))) => $lesseq($sum(f(2),f(5)),$sum(f(7),f(3)))),
% 8.57/1.61 file('/export/starexec/sandbox/benchmark/theBenchmark.p',f_mon_implies_f2plusf5_gt_f7plusf3)).
% 8.57/1.61 tff(f2,negated_conjecture,(
% 8.57/1.61 ~(! [X0 : $int,X1 : $int] : ($lesseq(X0,X1) => $lesseq(f(X0),f(X1))) => $lesseq($sum(f(2),f(5)),$sum(f(7),f(3))))),
% 8.57/1.61 inference(negated_conjecture,[status(cth)],[f1])).
% 8.57/1.61 tff(f3,plain,(
% 8.57/1.61 ~(! [X0 : $int,X1 : $int] : (~$less(X1,X0) => ~$less(f(X1),f(X0))) => ~$less($sum(f(7),f(3)),$sum(f(2),f(5))))),
% 8.57/1.61 inference(theory_normalization,[],[f2])).
% 8.57/1.61 tff(f4,definition,(
% 8.57/1.61 ( ! [X0 : $int,X1 : $int] : ($sum(X0,X1) = $sum(X1,X0)) )),
% 8.57/1.61 introduced(theory,[tha_commutativity])).
% 8.57/1.61 tff(f9,definition,(
% 8.57/1.61 ( ! [X0 : $int] : (~$less(X0,X0)) )),
% 8.57/1.61 introduced(theory,[tha_non-reflexivity])).
% 8.57/1.61 tff(f10,definition,(
% 8.57/1.61 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~$less(X1,X2) | ~$less(X0,X1) | $less(X0,X2)) )),
% 8.57/1.61 introduced(theory,[tha_transitivity])).
% 8.57/1.61 tff(f11,definition,(
% 8.57/1.61 ( ! [X0 : $int,X1 : $int] : ($less(X1,X0) | $less(X0,X1) | X0 = X1) )),
% 8.57/1.61 introduced(theory,[tha_order_totality])).
% 8.57/1.61 tff(f12,definition,(
% 8.57/1.61 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($less($sum(X0,X2),$sum(X1,X2)) | ~$less(X0,X1)) )),
% 8.57/1.61 introduced(theory,[tha_order_monotonicity])).
% 8.57/1.61 tff(f16,plain,(
% 8.57/1.61 $less($sum(f(7),f(3)),$sum(f(2),f(5))) & ! [X0 : $int,X1 : $int] : (~$less(f(X1),f(X0)) | $less(X1,X0))),
% 8.57/1.61 inference(ennf_transformation,[],[f3])).
% 8.57/1.61 tff(f17,plain,(
% 8.57/1.61 ( ! [X0 : $int,X1 : $int] : (~$less(f(X1),f(X0)) | $less(X1,X0)) )),
% 8.57/1.61 inference(cnf_transformation,[],[f16])).
% 8.57/1.61 tff(f18,plain,(
% 8.57/1.61 $less($sum(f(7),f(3)),$sum(f(2),f(5)))),
% 8.57/1.61 inference(cnf_transformation,[],[f16])).
% 8.57/1.61 tff(f19,definition,(
% 8.57/1.61 sF0 = f(7)),
% 8.57/1.61 introduced(definition,[new_symbols(definition,[sF0])],[function_definition])).
% 8.57/1.61 tff(f20,plain,(
% 8.57/1.61 f(7) = sF0),
% 8.57/1.61 inference(reorient_equations,[],[f19])).
% 8.57/1.61 tff(f21,definition,(
% 8.57/1.61 sF1 = f(3)),
% 8.57/1.61 introduced(definition,[new_symbols(definition,[sF1])],[function_definition])).
% 8.57/1.61 tff(f22,plain,(
% 8.57/1.61 f(3) = sF1),
% 8.57/1.61 inference(reorient_equations,[],[f21])).
% 8.57/1.61 tff(f23,definition,(
% 8.57/1.61 sF2 = $sum(sF0,sF1)),
% 8.57/1.61 introduced(definition,[new_symbols(definition,[sF2])],[function_definition])).
% 8.57/1.61 tff(f24,plain,(
% 8.57/1.61 $sum(sF0,sF1) = sF2),
% 8.57/1.61 inference(reorient_equations,[],[f23])).
% 8.57/1.61 tff(f25,definition,(
% 8.57/1.61 sF3 = f(2)),
% 8.57/1.61 introduced(definition,[new_symbols(definition,[sF3])],[function_definition])).
% 8.57/1.61 tff(f26,plain,(
% 8.57/1.61 f(2) = sF3),
% 8.57/1.61 inference(reorient_equations,[],[f25])).
% 8.57/1.61 tff(f27,definition,(
% 8.57/1.61 sF4 = f(5)),
% 8.57/1.61 introduced(definition,[new_symbols(definition,[sF4])],[function_definition])).
% 8.57/1.61 tff(f28,plain,(
% 8.57/1.61 f(5) = sF4),
% 8.57/1.61 inference(reorient_equations,[],[f27])).
% 8.57/1.61 tff(f29,definition,(
% 8.57/1.61 sF5 = $sum(sF3,sF4)),
% 8.57/1.61 introduced(definition,[new_symbols(definition,[sF5])],[function_definition])).
% 8.57/1.61 tff(f30,plain,(
% 8.57/1.61 $sum(sF3,sF4) = sF5),
% 8.57/1.61 inference(reorient_equations,[],[f29])).
% 8.57/1.61 tff(f31,plain,(
% 8.57/1.61 $less(sF2,sF5)),
% 8.57/1.61 inference(definition_folding,[],[f18,f30,f28,f26,f24,f22,f20])).
% 8.57/1.61 tff(f45,plain,(
% 8.57/1.61 ( ! [X0 : $int] : (~$less(f(X0),sF3) | $less(X0,2)) )),
% 8.57/1.61 inference(superposition,[],[f17,f26])).
% 8.57/1.61 tff(f50,plain,(
% 8.57/1.61 ( ! [X0 : $int] : (~$less(f(X0),sF4) | $less(X0,5)) )),
% 8.57/1.61 inference(superposition,[],[f17,f28])).
% 8.57/1.61 tff(f91,plain,(
% 8.57/1.61 ( ! [X0 : $int] : (~$less(X0,sF2) | $less(X0,sF5)) )),
% 8.57/1.61 inference(resolution,[],[f10,f31])).
% 8.57/1.61 tff(f108,plain,(
% 8.57/1.61 ( ! [X0 : $int] : ($less(sF3,f(X0)) | f(X0) = sF3 | $less(X0,2)) )),
% 8.57/1.61 inference(resolution,[],[f11,f45])).
% 8.57/1.61 tff(f135,plain,(
% 8.57/1.61 ( ! [X0 : $int] : ($less(sF5,$sum(X0,sF4)) | ~$less(sF3,X0)) )),
% 8.57/1.61 inference(superposition,[],[f12,f30])).
% 8.57/1.61 tff(f139,plain,(
% 8.57/1.61 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($less($sum(X2,X0),$sum(X0,X1)) | ~$less(X2,X1)) )),
% 8.57/1.61 inference(superposition,[],[f12,f4])).
% 8.57/1.61 tff(f141,plain,(
% 8.57/1.61 ( ! [X0 : $int] : ($less($sum(X0,sF1),sF2) | ~$less(X0,sF0)) )),
% 8.57/1.61 inference(superposition,[],[f12,f24])).
% 8.57/1.61 tff(f146,plain,(
% 8.57/1.61 ( ! [X0 : $int] : ($less(sF4,f(X0)) | $less(X0,5) | f(X0) = sF4) )),
% 8.57/1.61 inference(resolution,[],[f50,f11])).
% 8.57/1.61 tff(f244,plain,(
% 8.57/1.61 ( ! [X0 : $int] : ($less(sF5,$sum(sF4,X0)) | ~$less(sF3,X0)) )),
% 8.57/1.61 inference(superposition,[],[f135,f4])).
% 8.57/1.61 tff(f254,plain,(
% 8.57/1.61 ( ! [X0 : $int] : ($less($sum(X0,sF1),sF5) | ~$less(X0,sF0)) )),
% 8.57/1.61 inference(resolution,[],[f141,f91])).
% 8.57/1.61 tff(f266,plain,(
% 8.57/1.61 ( ! [X0 : $int,X1 : $int] : (~$less(X1,$sum(X0,sF1)) | ~$less(X0,sF0) | $less(X1,sF5)) )),
% 8.57/1.61 inference(resolution,[],[f254,f10])).
% 8.57/1.61 tff(f268,plain,(
% 8.57/1.61 ( ! [X0 : $int] : ($less($sum(sF1,X0),sF5) | ~$less(X0,sF0)) )),
% 8.57/1.61 inference(superposition,[],[f254,f4])).
% 8.57/1.61 tff(f529,plain,(
% 8.57/1.61 ( ! [X0 : $int] : ($less($sum(X0,sF0),sF2) | ~$less(X0,sF1)) )),
% 8.57/1.61 inference(superposition,[],[f139,f24])).
% 8.57/1.61 tff(f667,plain,(
% 8.57/1.61 $less(sF3,sF1) | sF1 = sF3 | $less(3,2)),
% 8.57/1.61 inference(superposition,[],[f108,f22])).
% 8.57/1.61 tff(f668,plain,(
% 8.57/1.61 $less(sF3,sF1) | sF1 = sF3),
% 8.57/1.61 inference(evaluation,[],[f667])).
% 8.57/1.61 tff(f1524,plain,(
% 8.57/1.61 $less(sF4,sF0) | $less(7,5) | sF0 = sF4),
% 8.57/1.61 inference(superposition,[],[f146,f20])).
% 8.57/1.61 tff(f1526,plain,(
% 8.57/1.61 $less(sF4,sF0) | sF0 = sF4),
% 8.57/1.61 inference(evaluation,[],[f1524])).
% 8.57/1.61 tff(f2100,plain,(
% 8.57/1.61 ~$less(sF3,sF1) | ~$less(sF4,sF0) | $less(sF5,sF5)),
% 8.57/1.61 inference(resolution,[],[f244,f266])).
% 8.57/1.61 tff(f2113,plain,(
% 8.57/1.61 ~$less(sF4,sF0) | ~$less(sF3,sF1)),
% 8.57/1.61 inference(forward_subsumption_resolution,[],[f2100,f9])).
% 8.57/1.61 tff(f2114,plain,(
% 8.57/1.61 ~$less(sF3,sF1) | sF0 = sF4),
% 8.57/1.61 inference(resolution,[],[f2113,f1526])).
% 8.57/1.61 tff(f2139,plain,(
% 8.57/1.61 sF0 = sF4 | sF1 = sF3),
% 8.57/1.61 inference(resolution,[],[f2114,f668])).
% 8.57/1.61 tff(f2160,plain,(
% 8.57/1.61 sF5 = $sum(sF3,sF0) | sF1 = sF3),
% 8.57/1.61 inference(superposition,[],[f30,f2139])).
% 8.57/1.61 tff(f2185,plain,(
% 8.57/1.61 sF5 = $sum(sF0,sF3) | sF1 = sF3),
% 8.57/1.61 inference(forward_demodulation,[],[f2160,f4])).
% 8.57/1.61 tff(f2611,plain,(
% 8.57/1.61 ( ! [X0 : $int] : ($less($sum(X0,sF0),sF5) | ~$less(X0,sF1)) )),
% 8.57/1.61 inference(resolution,[],[f529,f91])).
% 8.57/1.61 tff(f3017,plain,(
% 8.57/1.61 ( ! [X0 : $int] : ($less($sum(sF0,X0),sF5) | ~$less(X0,sF1)) )),
% 8.57/1.61 inference(superposition,[],[f2611,f4])).
% 8.57/1.61 tff(f5590,plain,(
% 8.57/1.61 $less(sF5,sF5) | ~$less(sF3,sF1) | sF1 = sF3),
% 8.57/1.61 inference(superposition,[],[f3017,f2185])).
% 8.57/1.61 tff(f5635,plain,(
% 8.57/1.61 $less(sF5,sF5) | sF1 = sF3),
% 8.57/1.61 inference(forward_subsumption_resolution,[],[f5590,f668])).
% 8.57/1.61 tff(f5637,plain,(
% 8.57/1.61 sF1 = sF3),
% 8.57/1.61 inference(forward_subsumption_resolution,[],[f5635,f9])).
% 8.57/1.61 tff(f5770,plain,(
% 8.57/1.61 sF5 = $sum(sF1,sF4)),
% 8.57/1.61 inference(superposition,[],[f30,f5637])).
% 8.57/1.61 tff(f5913,plain,(
% 8.57/1.61 $less(sF5,sF5) | ~$less(sF4,sF0)),
% 8.57/1.61 inference(superposition,[],[f268,f5770])).
% 8.57/1.61 tff(f5963,plain,(
% 8.57/1.61 ~$less(sF4,sF0)),
% 8.57/1.61 inference(forward_subsumption_resolution,[],[f5913,f9])).
% 8.57/1.61 tff(f6084,plain,(
% 8.57/1.61 sF0 = sF4),
% 8.57/1.61 inference(resolution,[],[f5963,f1526])).
% 8.57/1.61 tff(f6570,plain,(
% 8.57/1.61 sF5 = $sum(sF1,sF0)),
% 8.57/1.61 inference(superposition,[],[f5770,f6084])).
% 8.57/1.61 tff(f6572,plain,(
% 8.57/1.61 $sum(sF0,sF1) = sF5),
% 8.57/1.61 inference(forward_demodulation,[],[f6570,f4])).
% 8.57/1.61 tff(f6595,plain,(
% 8.57/1.61 sF2 = sF5),
% 8.57/1.61 inference(forward_demodulation,[],[f6572,f24])).
% 8.57/1.61 tff(f7166,plain,(
% 8.57/1.61 $less(sF2,sF2)),
% 8.57/1.61 inference(superposition,[],[f31,f6595])).
% 8.57/1.61 tff(f7204,plain,(
% 8.57/1.61 $false),
% 8.57/1.61 inference(forward_subsumption_resolution,[],[f7166,f9])).
% 8.57/1.61 % SZS output end Proof for theBenchmark
% 8.57/1.61 % (2003381)------------------------------
% 8.57/1.61 % (2003381)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.57/1.61 % (2003381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.57/1.61 % (2003381)CaDiCaL version: 2.1.3
% 8.57/1.61 % (2003381)Termination reason: Refutation
% 8.57/1.61 % (2003381)Time elapsed: 0.326 s
% 8.57/1.61 % (2003381)Peak memory usage: 14 MB
% 8.57/1.61 % (2003381)Instructions burned: 332 (million)
% 8.57/1.61 % (2003326)Success in time 1.307 s
% 8.57/1.61 % Vampire exiting
%------------------------------------------------------------------------------