%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ARI185_1 : TPTP v9.3.1. Released v5.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n015.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:09 AM UTC 2026
% Result : Theorem 44.95s 10.05s
% Output : Refutation 44.95s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ARI185_1 : TPTP v9.3.1. Released v5.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.18 % Computer : n015.cluster.edu
% 0.09/0.18 % Model : x86_64 x86_64
% 0.09/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.18 % Memory : 8046.5625MB
% 0.09/0.18 % OS : Linux 6.8.0-71-generic
% 0.09/0.18 % CPULimit : 300
% 0.09/0.18 % WCLimit : 300
% 0.09/0.18 % DateTime : Mon Sep 28 20:47:47 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.21 Running first-order model finding
% 0.09/0.21 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.70/0.86 % (2988431)Will run a generic schedule for satisfiability detection.
% 3.70/0.86 % (2988440)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3089155223:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 3.70/0.86 % (2988437)% WARNING: option uhcvi not known.
% 3.70/0.86 % (2988436)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=67400233_2999 on theBenchmark for (2999ds/0Mi)
% 3.70/0.86 % (2988439)dis+10_1_sil=32000:sp=arity:random_seed=448053713:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 3.70/0.86 % (2988438)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=600468814:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 3.70/0.86 % (2988437)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3219394770:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 3.70/0.86 % (2988441)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2798584859:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 3.70/0.86 % (2988436)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 3.70/0.86 % (2988436)Terminated due to inappropriate strategy.
% 3.70/0.86 % (2988436)------------------------------
% 3.70/0.86 % (2988436)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.70/0.86 % (2988436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.70/0.86 % (2988436)CaDiCaL version: 2.1.3
% 3.70/0.86 % (2988442)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2006359116:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 3.70/0.86 % (2988436)Termination reason: Inappropriate
% 3.70/0.86 % (2988436)Time elapsed: 0.0000 s
% 3.70/0.86 % (2988436)Peak memory usage: 10 MB
% 3.70/0.86 % (2988436)------------------------------
% 3.70/0.86 % (2988436)------------------------------
% 3.70/0.86 % (2988450)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3222797905:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 3.70/0.86 % (2988450)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 3.70/0.86 % (2988450)Terminated due to inappropriate strategy.
% 3.70/0.86 % (2988450)------------------------------
% 3.70/0.86 % (2988450)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.70/0.86 % (2988450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.70/0.86 % (2988450)CaDiCaL version: 2.1.3
% 3.70/0.86 % (2988450)Termination reason: Inappropriate
% 3.70/0.86 % (2988450)Time elapsed: 0.0000 s
% 3.70/0.86 % (2988450)Peak memory usage: 10 MB
% 3.70/0.86 % (2988450)------------------------------
% 3.70/0.86 % (2988450)------------------------------
% 3.70/0.86 % (2988440)Instruction limit reached!
% 3.70/0.86 % (2988440)------------------------------
% 3.70/0.86 % (2988440)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.70/0.86 % (2988440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.70/0.86 % (2988440)CaDiCaL version: 2.1.3
% 3.70/0.86 % (2988440)Termination reason: Instruction limit
% 3.70/0.86 % (2988440)Termination phase: Saturation
% 3.70/0.86 % (2988440)Time elapsed: 0.039 s
% 3.70/0.86 % (2988440)Peak memory usage: 12 MB
% 3.70/0.86 % (2988440)Instructions burned: 118 (million)
% 3.70/0.86 % (2988452)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1903428952:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 3.70/0.86 % (2988453)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=181052672:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 3.70/0.86 % (2988439)Instruction limit reached!
% 3.70/0.86 % (2988439)------------------------------
% 3.70/0.86 % (2988439)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.70/0.86 % (2988439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.70/0.86 % (2988439)CaDiCaL version: 2.1.3
% 3.70/0.86 % (2988439)Termination reason: Instruction limit
% 3.70/0.86 % (2988439)Termination phase: Saturation
% 3.70/0.86 % (2988439)Time elapsed: 0.063 s
% 3.70/0.86 % (2988439)Peak memory usage: 12 MB
% 3.70/0.86 % (2988439)Instructions burned: 103 (million)
% 3.70/0.86 % (2988456)ott-21_1_sil=16000:fs=off:random_seed=4159370874:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 3.70/0.86 % (2988441)Instruction limit reached!
% 3.70/0.86 % (2988441)------------------------------
% 7.95/1.45 % (2988441)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.95/1.45 % (2988441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.95/1.45 % (2988441)CaDiCaL version: 2.1.3
% 7.95/1.45 % (2988441)Termination reason: Instruction limit
% 7.95/1.45 % (2988441)Termination phase: Saturation
% 7.95/1.45 % (2988441)Time elapsed: 0.082 s
% 7.95/1.45 % (2988441)Peak memory usage: 13 MB
% 7.95/1.45 % (2988441)Instructions burned: 132 (million)
% 7.95/1.45 % (2988442)Instruction limit reached!
% 7.95/1.45 % (2988442)------------------------------
% 7.95/1.45 % (2988442)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.95/1.45 % (2988458)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2740686953:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 7.95/1.45 % (2988442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.95/1.45 % (2988442)CaDiCaL version: 2.1.3
% 7.95/1.45 % (2988442)Termination reason: Instruction limit
% 7.95/1.45 % (2988442)Termination phase: Saturation
% 7.95/1.45 % (2988442)Time elapsed: 0.102 s
% 7.95/1.45 % (2988442)Peak memory usage: 13 MB
% 7.95/1.45 % (2988442)Instructions burned: 165 (million)
% 7.95/1.45 % (2988460)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=364039337:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 7.95/1.45 % (2988460)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 7.95/1.45 % (2988460)Terminated due to inappropriate strategy.
% 7.95/1.45 % (2988460)------------------------------
% 7.95/1.45 % (2988460)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.95/1.45 % (2988460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.95/1.45 % (2988460)CaDiCaL version: 2.1.3
% 7.95/1.45 % (2988460)Termination reason: Inappropriate
% 7.95/1.45 % (2988460)Time elapsed: 0.0000 s
% 7.95/1.45 % (2988460)Peak memory usage: 10 MB
% 7.95/1.45 % (2988460)------------------------------
% 7.95/1.45 % (2988460)------------------------------
% 7.95/1.45 % (2988452)Instruction limit reached!
% 7.95/1.45 % (2988452)------------------------------
% 7.95/1.45 % (2988452)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.95/1.45 % (2988452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.95/1.45 % (2988452)CaDiCaL version: 2.1.3
% 7.95/1.45 % (2988452)Termination reason: Instruction limit
% 7.95/1.45 % (2988452)Termination phase: Saturation
% 7.95/1.45 % (2988452)Time elapsed: 0.094 s
% 7.95/1.45 % (2988452)Peak memory usage: 13 MB
% 7.95/1.45 % (2988452)Instructions burned: 132 (million)
% 7.95/1.45 % (2988462)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3812058377:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 7.95/1.45 % (2988463)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4094004385:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 7.95/1.45 % (2988463)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 7.95/1.45 % (2988463)Terminated due to inappropriate strategy.
% 7.95/1.45 % (2988463)------------------------------
% 7.95/1.45 % (2988463)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.95/1.45 % (2988463)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.95/1.45 % (2988463)CaDiCaL version: 2.1.3
% 7.95/1.45 % (2988463)Termination reason: Inappropriate
% 7.95/1.45 % (2988463)Time elapsed: 0.0000 s
% 7.95/1.45 % (2988463)Peak memory usage: 10 MB
% 7.95/1.45 % (2988463)------------------------------
% 7.95/1.45 % (2988463)------------------------------
% 7.95/1.45 % (2988456)Instruction limit reached!
% 7.95/1.45 % (2988456)------------------------------
% 7.95/1.45 % (2988456)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.95/1.45 % (2988456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.95/1.45 % (2988456)CaDiCaL version: 2.1.3
% 7.95/1.45 % (2988456)Termination reason: Instruction limit
% 7.95/1.45 % (2988456)Termination phase: Saturation
% 7.95/1.45 % (2988456)Time elapsed: 0.080 s
% 7.95/1.45 % (2988456)Peak memory usage: 12 MB
% 7.95/1.45 % (2988456)Instructions burned: 181 (million)
% 7.95/1.45 % (2988466)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=3748132076:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi)
% 7.95/1.45 % (2988467)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=997613645:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi)
% 21.13/3.26 % (2988453)Instruction limit reached!
% 21.13/3.26 % (2988453)------------------------------
% 21.13/3.26 % (2988453)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.13/3.26 % (2988453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.13/3.26 % (2988453)CaDiCaL version: 2.1.3
% 21.13/3.26 % (2988453)Termination reason: Instruction limit
% 21.13/3.26 % (2988453)Termination phase: Saturation
% 21.13/3.26 % (2988453)Time elapsed: 0.202 s
% 21.13/3.26 % (2988453)Peak memory usage: 16 MB
% 21.13/3.26 % (2988453)Instructions burned: 684 (million)
% 21.13/3.26 % (2988470)fmb+10_1_sil=64000:random_seed=1804313839:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi)
% 21.13/3.26 % (2988470)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 21.13/3.26 % (2988470)Terminated due to inappropriate strategy.
% 21.13/3.26 % (2988470)------------------------------
% 21.13/3.26 % (2988470)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.13/3.26 % (2988470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.13/3.26 % (2988470)CaDiCaL version: 2.1.3
% 21.13/3.26 % (2988470)Termination reason: Inappropriate
% 21.13/3.26 % (2988470)Time elapsed: 0.0000 s
% 21.13/3.26 % (2988470)Peak memory usage: 10 MB
% 21.13/3.26 % (2988470)------------------------------
% 21.13/3.26 % (2988470)------------------------------
% 21.13/3.26 % (2988472)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2205701783:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi)
% 21.13/3.26 % (2988472)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 21.13/3.26 % (2988472)Terminated due to inappropriate strategy.
% 21.13/3.26 % (2988472)------------------------------
% 21.13/3.26 % (2988472)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.13/3.26 % (2988472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.13/3.26 % (2988472)CaDiCaL version: 2.1.3
% 21.13/3.26 % (2988472)Termination reason: Inappropriate
% 21.13/3.26 % (2988472)Time elapsed: 0.0000 s
% 21.13/3.26 % (2988472)Peak memory usage: 10 MB
% 21.13/3.26 % (2988472)------------------------------
% 21.13/3.26 % (2988472)------------------------------
% 21.13/3.26 % (2988474)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1558836383:fmbsr=1.7:i=920_2997 on theBenchmark for (2997ds/920Mi)
% 21.13/3.26 % (2988474)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 21.13/3.26 % (2988474)Terminated due to inappropriate strategy.
% 21.13/3.26 % (2988474)------------------------------
% 21.13/3.26 % (2988474)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.13/3.26 % (2988474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.13/3.26 % (2988474)CaDiCaL version: 2.1.3
% 21.13/3.26 % (2988474)Termination reason: Inappropriate
% 21.13/3.26 % (2988474)Time elapsed: 0.0000 s
% 21.13/3.26 % (2988474)Peak memory usage: 10 MB
% 21.13/3.26 % (2988474)------------------------------
% 21.13/3.26 % (2988474)------------------------------
% 21.13/3.26 % (2988476)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=327614491:i=5131_2996 on theBenchmark for (2996ds/5131Mi)
% 21.13/3.26 % (2988458)Instruction limit reached!
% 21.13/3.26 % (2988458)------------------------------
% 21.13/3.26 % (2988458)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.13/3.26 % (2988458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.13/3.26 % (2988458)CaDiCaL version: 2.1.3
% 21.13/3.26 % (2988458)Termination reason: Instruction limit
% 21.13/3.26 % (2988458)Termination phase: Saturation
% 21.13/3.26 % (2988458)Time elapsed: 0.305 s
% 21.13/3.26 % (2988458)Peak memory usage: 14 MB
% 21.13/3.26 % (2988458)Instructions burned: 478 (million)
% 21.13/3.26 % (2988478)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3509554077:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi)
% 21.13/3.26 % (2988466)Instruction limit reached!
% 21.13/3.26 % (2988466)------------------------------
% 21.13/3.26 % (2988466)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 21.13/3.26 % (2988466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.13/3.26 % (2988466)CaDiCaL version: 2.1.3
% 21.13/3.26 % (2988466)Termination reason: Instruction limit
% 28.21/4.23 % (2988466)Termination phase: Saturation
% 28.21/4.23 % (2988466)Time elapsed: 0.429 s
% 28.21/4.23 % (2988466)Peak memory usage: 18 MB
% 28.21/4.23 % (2988466)Instructions burned: 692 (million)
% 28.21/4.23 % (2988480)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2818743706:i=6324_2993 on theBenchmark for (2993ds/6324Mi)
% 28.21/4.23 % (2988480)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 28.21/4.23 % (2988480)Terminated due to inappropriate strategy.
% 28.21/4.23 % (2988480)------------------------------
% 28.21/4.23 % (2988480)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.21/4.23 % (2988480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.21/4.23 % (2988480)CaDiCaL version: 2.1.3
% 28.21/4.23 % (2988480)Termination reason: Inappropriate
% 28.21/4.23 % (2988480)Time elapsed: 0.0000 s
% 28.21/4.23 % (2988480)Peak memory usage: 10 MB
% 28.21/4.23 % (2988480)------------------------------
% 28.21/4.23 % (2988480)------------------------------
% 28.21/4.23 % (2988482)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2892328423:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi)
% 28.21/4.23 % (2988482)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 28.21/4.23 % (2988482)Terminated due to inappropriate strategy.
% 28.21/4.23 % (2988482)------------------------------
% 28.21/4.23 % (2988482)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.21/4.23 % (2988482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.21/4.23 % (2988482)CaDiCaL version: 2.1.3
% 28.21/4.23 % (2988482)Termination reason: Inappropriate
% 28.21/4.23 % (2988482)Time elapsed: 0.0000 s
% 28.21/4.23 % (2988482)Peak memory usage: 10 MB
% 28.21/4.23 % (2988482)------------------------------
% 28.21/4.23 % (2988482)------------------------------
% 28.21/4.23 % (2988484)ott-2_1_sil=16000:newcnf=on:random_seed=1614461822:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi)
% 28.21/4.23 % (2988467)Instruction limit reached!
% 28.21/4.23 % (2988467)------------------------------
% 28.21/4.23 % (2988467)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.21/4.23 % (2988467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.21/4.23 % (2988467)CaDiCaL version: 2.1.3
% 28.21/4.23 % (2988467)Termination reason: Instruction limit
% 28.21/4.23 % (2988467)Termination phase: Saturation
% 28.21/4.23 % (2988467)Time elapsed: 0.494 s
% 28.21/4.23 % (2988467)Peak memory usage: 19 MB
% 28.21/4.23 % (2988467)Instructions burned: 880 (million)
% 28.21/4.23 % (2988486)ott+10_1_sil=32000:tgt=ground:random_seed=4271547488:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi)
% 28.21/4.23 % (2988462)Instruction limit reached!
% 28.21/4.23 % (2988462)------------------------------
% 28.21/4.23 % (2988462)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.21/4.23 % (2988462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.21/4.23 % (2988462)CaDiCaL version: 2.1.3
% 28.21/4.23 % (2988462)Termination reason: Instruction limit
% 28.21/4.23 % (2988462)Termination phase: Saturation
% 28.21/4.23 % (2988462)Time elapsed: 0.593 s
% 28.21/4.23 % (2988462)Peak memory usage: 18 MB
% 28.21/4.23 % (2988462)Instructions burned: 1179 (million)
% 28.21/4.23 % (2988488)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2607282744:i=54282_2992 on theBenchmark for (2992ds/54282Mi)
% 28.21/4.23 % (2988488)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 28.21/4.23 % (2988488)Terminated due to inappropriate strategy.
% 28.21/4.23 % (2988488)------------------------------
% 28.21/4.23 % (2988488)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.21/4.23 % (2988488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.21/4.23 % (2988488)CaDiCaL version: 2.1.3
% 28.21/4.23 % (2988488)Termination reason: Inappropriate
% 28.21/4.23 % (2988488)Time elapsed: 0.0000 s
% 28.21/4.23 % (2988488)Peak memory usage: 10 MB
% 28.21/4.23 % (2988488)------------------------------
% 28.21/4.23 % (2988488)------------------------------
% 28.21/4.23 % (2988490)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=767558715:i=3512:aac=none_2992 on theBenchmark for (2992ds/3512Mi)
% 28.21/4.23 % (2988484)Instruction limit reached!
% 28.21/4.23 % (2988484)------------------------------
% 28.21/4.23 % (2988484)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.21/4.23 % (2988484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.95/10.05 % (2988484)CaDiCaL version: 2.1.3
% 44.95/10.05 % (2988484)Termination reason: Instruction limit
% 44.95/10.05 % (2988484)Termination phase: Saturation
% 44.95/10.05 % (2988484)Time elapsed: 0.529 s
% 44.95/10.05 % (2988484)Peak memory usage: 15 MB
% 44.95/10.05 % (2988484)Instructions burned: 870 (million)
% 44.95/10.05 % (2988492)dis+21_1_sil=32000:sas=cadical:random_seed=978208531:i=3773:amm=off_2987 on theBenchmark for (2987ds/3773Mi)
% 44.95/10.05 % (2988478)Instruction limit reached!
% 44.95/10.05 % (2988478)------------------------------
% 44.95/10.05 % (2988478)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.95/10.05 % (2988478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.95/10.05 % (2988478)CaDiCaL version: 2.1.3
% 44.95/10.05 % (2988478)Termination reason: Instruction limit
% 44.95/10.05 % (2988478)Termination phase: Saturation
% 44.95/10.05 % (2988478)Time elapsed: 0.790 s
% 44.95/10.05 % (2988478)Peak memory usage: 24 MB
% 44.95/10.05 % (2988478)Instructions burned: 1474 (million)
% 44.95/10.05 % (2988494)ott+11_1_sil=16000:gs=on:random_seed=2346828729:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2987 on theBenchmark for (2987ds/2251Mi)
% 44.95/10.05 % (2988476)Instruction limit reached!
% 44.95/10.05 % (2988476)------------------------------
% 44.95/10.05 % (2988476)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.95/10.05 % (2988476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.95/10.05 % (2988476)CaDiCaL version: 2.1.3
% 44.95/10.05 % (2988476)Termination reason: Instruction limit
% 44.95/10.05 % (2988476)Termination phase: Saturation
% 44.95/10.05 % (2988476)Time elapsed: 1.456 s
% 44.95/10.05 % (2988476)Peak memory usage: 41 MB
% 44.95/10.05 % (2988476)Instructions burned: 5143 (million)
% 44.95/10.05 % (2988496)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3966169087:fmbsr=1.6:i=67534_2982 on theBenchmark for (2982ds/67534Mi)
% 44.95/10.05 % (2988496)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 44.95/10.05 % (2988496)Terminated due to inappropriate strategy.
% 44.95/10.05 % (2988496)------------------------------
% 44.95/10.05 % (2988496)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.95/10.05 % (2988496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.95/10.05 % (2988496)CaDiCaL version: 2.1.3
% 44.95/10.05 % (2988496)Termination reason: Inappropriate
% 44.95/10.05 % (2988496)Time elapsed: 0.0000 s
% 44.95/10.05 % (2988496)Peak memory usage: 11 MB
% 44.95/10.05 % (2988496)------------------------------
% 44.95/10.05 % (2988496)------------------------------
% 44.95/10.05 % (2988498)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2644409139:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2982 on theBenchmark for (2982ds/4591Mi)
% 44.95/10.05 % (2988494)Instruction limit reached!
% 44.95/10.05 % (2988494)------------------------------
% 44.95/10.05 % (2988494)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.95/10.05 % (2988494)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.95/10.05 % (2988494)CaDiCaL version: 2.1.3
% 44.95/10.05 % (2988494)Termination reason: Instruction limit
% 44.95/10.05 % (2988494)Termination phase: Saturation
% 44.95/10.05 % (2988494)Time elapsed: 1.306 s
% 44.95/10.05 % (2988494)Peak memory usage: 24 MB
% 44.95/10.05 % (2988494)Instructions burned: 2253 (million)
% 44.95/10.05 % (2988500)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3730642200:i=29340_2974 on theBenchmark for (2974ds/29340Mi)
% 44.95/10.05 % (2988490)Instruction limit reached!
% 44.95/10.05 % (2988490)------------------------------
% 44.95/10.05 % (2988490)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.95/10.05 % (2988490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.95/10.05 % (2988490)CaDiCaL version: 2.1.3
% 44.95/10.05 % (2988490)Termination reason: Instruction limit
% 44.95/10.05 % (2988490)Termination phase: Saturation
% 44.95/10.05 % (2988490)Time elapsed: 1.841 s
% 44.95/10.05 % (2988490)Peak memory usage: 31 MB
% 44.95/10.05 % (2988490)Instructions burned: 3513 (million)
% 44.95/10.05 % (2988502)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2433756824:i=5211_2973 on theBenchmark for (2973ds/5211Mi)
% 44.95/10.05 % (2988498)Instruction limit reached!
% 44.95/10.05 % (2988498)------------------------------
% 44.95/10.05 % (2988498)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.95/10.05 % (2988498)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.95/10.05 % (2988498)CaDiCaL version: 2.1.3
% 44.95/10.05 % (2988498)Termination reason: Instruction limit
% 44.95/10.05 % (2988498)Termination phase: Saturation
% 44.95/10.05 % (2988498)Time elapsed: 1.230 s
% 44.95/10.05 % (2988498)Peak memory usage: 56 MB
% 44.95/10.05 % (2988498)Instructions burned: 4595 (million)
% 44.95/10.05 % (2988504)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=4222296037:i=5497:nm=2_2969 on theBenchmark for (2969ds/5497Mi)
% 44.95/10.05 % (2988504)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 44.95/10.05 % (2988504)Terminated due to inappropriate strategy.
% 44.95/10.05 % (2988504)------------------------------
% 44.95/10.05 % (2988504)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.95/10.05 % (2988504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.95/10.05 % (2988504)CaDiCaL version: 2.1.3
% 44.95/10.05 % (2988504)Termination reason: Inappropriate
% 44.95/10.05 % (2988504)Time elapsed: 0.0000 s
% 44.95/10.05 % (2988504)Peak memory usage: 10 MB
% 44.95/10.05 % (2988504)------------------------------
% 44.95/10.05 % (2988504)------------------------------
% 44.95/10.05 % (2988506)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2408222272:fmbsr=2:i=46332_2969 on theBenchmark for (2969ds/46332Mi)
% 44.95/10.05 % (2988506)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 44.95/10.05 % (2988506)Terminated due to inappropriate strategy.
% 44.95/10.05 % (2988506)------------------------------
% 44.95/10.05 % (2988506)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.95/10.05 % (2988506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.95/10.05 % (2988506)CaDiCaL version: 2.1.3
% 44.95/10.05 % (2988506)Termination reason: Inappropriate
% 44.95/10.05 % (2988506)Time elapsed: 0.0000 s
% 44.95/10.05 % (2988506)Peak memory usage: 10 MB
% 44.95/10.05 % (2988506)------------------------------
% 44.95/10.05 % (2988506)------------------------------
% 44.95/10.05 % (2988508)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2967306531:i=14071_2969 on theBenchmark for (2969ds/14071Mi)
% 44.95/10.05 % (2988508)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 44.95/10.05 % (2988508)Terminated due to inappropriate strategy.
% 44.95/10.05 % (2988508)------------------------------
% 44.95/10.05 % (2988508)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.95/10.05 % (2988508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.95/10.05 % (2988508)CaDiCaL version: 2.1.3
% 44.95/10.05 % (2988508)Termination reason: Inappropriate
% 44.95/10.05 % (2988508)Time elapsed: 0.0000 s
% 44.95/10.05 % (2988508)Peak memory usage: 10 MB
% 44.95/10.05 % (2988508)------------------------------
% 44.95/10.05 % (2988508)------------------------------
% 44.95/10.05 % (2988510)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1644447822:i=22565:add=on:rawr=on_2969 on theBenchmark for (2969ds/22565Mi)
% 44.95/10.05 % (2988492)Instruction limit reached!
% 44.95/10.05 % (2988492)------------------------------
% 44.95/10.05 % (2988492)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.95/10.05 % (2988492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.95/10.05 % (2988492)CaDiCaL version: 2.1.3
% 44.95/10.05 % (2988492)Termination reason: Instruction limit
% 44.95/10.05 % (2988492)Termination phase: Saturation
% 44.95/10.05 % (2988492)Time elapsed: 2.072 s
% 44.95/10.05 % (2988492)Peak memory usage: 37 MB
% 44.95/10.05 % (2988492)Instructions burned: 3774 (million)
% 44.95/10.05 % (2988512)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1130712775:i=8173:av=off_2966 on theBenchmark for (2966ds/8173Mi)
% 44.95/10.05 % (2988486)Instruction limit reached!
% 44.95/10.05 % (2988486)------------------------------
% 44.95/10.05 % (2988486)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.95/10.05 % (2988486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.95/10.05 % (2988486)CaDiCaL version: 2.1.3
% 44.95/10.05 % (2988486)Termination reason: Instruction limit
% 44.95/10.05 % (2988486)Termination phase: Saturation
% 44.95/10.05 % (2988486)Time elapsed: 3.253 s
% 44.95/10.05 % (2988486)Peak memory usage: 37 MB
% 44.95/10.05 % (2988486)Instructions burned: 5115 (million)
% 44.95/10.05 % (2988514)dis+10_16:1_sil=16000:random_seed=232652443:i=9155:fsr=off_2960 on theBenchmark for (2960ds/9155Mi)
% 44.95/10.05 % (2988502)Instruction limit reached!
% 44.95/10.05 % (2988502)------------------------------
% 44.95/10.05 % (2988502)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.95/10.05 % (2988502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.95/10.05 % (2988502)CaDiCaL version: 2.1.3
% 44.95/10.05 % (2988502)Termination reason: Instruction limit
% 44.95/10.05 % (2988502)Termination phase: Saturation
% 44.95/10.05 % (2988502)Time elapsed: 2.784 s
% 44.95/10.05 % (2988502)Peak memory usage: 50 MB
% 44.95/10.05 % (2988502)Instructions burned: 5212 (million)
% 44.95/10.05 % (2988516)ott-3_8_sil=64000:random_seed=3034801955:i=20139:bs=on_2945 on theBenchmark for (2945ds/20139Mi)
% 44.95/10.05 % (2988512)Instruction limit reached!
% 44.95/10.05 % (2988512)------------------------------
% 44.95/10.05 % (2988512)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.95/10.05 % (2988512)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.95/10.05 % (2988512)CaDiCaL version: 2.1.3
% 44.95/10.05 % (2988512)Termination reason: Instruction limit
% 44.95/10.05 % (2988512)Termination phase: Saturation
% 44.95/10.05 % (2988512)Time elapsed: 5.044 s
% 44.95/10.05 % (2988512)Peak memory usage: 54 MB
% 44.95/10.05 % (2988512)Instructions burned: 8174 (million)
% 44.95/10.05 % (2988518)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2446353841:fmbsr=2:i=32576_2916 on theBenchmark for (2916ds/32576Mi)
% 44.95/10.05 % (2988518)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 44.95/10.05 % (2988518)Terminated due to inappropriate strategy.
% 44.95/10.05 % (2988518)------------------------------
% 44.95/10.05 % (2988518)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.95/10.05 % (2988518)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.95/10.05 % (2988518)CaDiCaL version: 2.1.3
% 44.95/10.05 % (2988518)Termination reason: Inappropriate
% 44.95/10.05 % (2988518)Time elapsed: 0.0000 s
% 44.95/10.05 % (2988518)Peak memory usage: 10 MB
% 44.95/10.05 % (2988518)------------------------------
% 44.95/10.05 % (2988518)------------------------------
% 44.95/10.05 % (2988520)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=4214591304:i=11404_2915 on theBenchmark for (2915ds/11404Mi)
% 44.95/10.05 % (2988514)Instruction limit reached!
% 44.95/10.05 % (2988514)------------------------------
% 44.95/10.05 % (2988514)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.95/10.05 % (2988514)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.95/10.05 % (2988514)CaDiCaL version: 2.1.3
% 44.95/10.05 % (2988514)Termination reason: Instruction limit
% 44.95/10.05 % (2988514)Termination phase: Saturation
% 44.95/10.05 % (2988514)Time elapsed: 4.647 s
% 44.95/10.05 % (2988514)Peak memory usage: 52 MB
% 44.95/10.05 % (2988514)Instructions burned: 9155 (million)
% 44.95/10.05 % (2988522)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1177386023:i=14134_2913 on theBenchmark for (2913ds/14134Mi)
% 44.95/10.05 % (2988510)Instruction limit reached!
% 44.95/10.05 % (2988510)------------------------------
% 44.95/10.05 % (2988510)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.95/10.05 % (2988510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.95/10.05 % (2988510)CaDiCaL version: 2.1.3
% 44.95/10.05 % (2988510)Termination reason: Instruction limit
% 44.95/10.05 % (2988510)Termination phase: Saturation
% 44.95/10.05 % (2988510)Time elapsed: 6.180 s
% 44.95/10.05 % (2988510)Peak memory usage: 99 MB
% 44.95/10.05 % (2988510)Instructions burned: 22567 (million)
% 44.95/10.05 % (2988524)dis+33_16_sil=32000:sac=on:random_seed=2058801508:i=15851:nm=0_2907 on theBenchmark for (2907ds/15851Mi)
% 44.95/10.05 % (2988437) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2988431-2988437"...
% 44.95/10.05 % (2988437)...printing done.
% 44.95/10.05 % (2988437)Refutation found. Thanks to Tanya!
% 44.95/10.05 % SZS status Theorem for theBenchmark
% 44.95/10.05 % SZS output start Proof for theBenchmark
% 44.95/10.05 tff(func_def_0, type, f: $int > $int).
% 44.95/10.05 tff(f1,conjecture,(
% 44.95/10.05 ! [X0 : $int] : $greater(f(X0),1) => $less($difference(7,$product(2,f(3))),4)),
% 44.95/10.05 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1)).
% 44.95/10.05 tff(f2,negated_conjecture,(
% 44.95/10.05 ~(! [X0 : $int] : $greater(f(X0),1) => $less($difference(7,$product(2,f(3))),4))),
% 44.95/10.05 inference(negated_conjecture,[status(cth)],[f1])).
% 44.95/10.05 tff(f3,plain,(
% 44.95/10.05 ~(! [X0 : $int] : $less(1,f(X0)) => $less($sum(7,$uminus($product(2,f(3)))),4))),
% 44.95/10.05 inference(theory_normalization,[],[f2])).
% 44.95/10.05 tff(f4,definition,(
% 44.95/10.05 ( ! [X0 : $int,X1 : $int] : ($sum(X0,X1) = $sum(X1,X0)) )),
% 44.95/10.05 introduced(theory,[tha_commutativity])).
% 44.95/10.05 tff(f5,definition,(
% 44.95/10.05 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($sum(X0,$sum(X1,X2)) = $sum($sum(X0,X1),X2)) )),
% 44.95/10.05 introduced(theory,[tha_associativity])).
% 44.95/10.05 tff(f7,definition,(
% 44.95/10.05 ( ! [X0 : $int,X1 : $int] : ($uminus($sum(X0,X1)) = $sum($uminus(X1),$uminus(X0))) )),
% 44.95/10.05 introduced(theory,[tha_inverse_op_op_inverses])).
% 44.95/10.05 tff(f8,definition,(
% 44.95/10.05 ( ! [X0 : $int] : (0 = $sum(X0,$uminus(X0))) )),
% 44.95/10.05 introduced(theory,[tha_inverse_op_unit])).
% 44.95/10.05 tff(f10,definition,(
% 44.95/10.05 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~$less(X1,X2) | ~$less(X0,X1) | $less(X0,X2)) )),
% 44.95/10.05 introduced(theory,[tha_transitivity])).
% 44.95/10.05 tff(f11,definition,(
% 44.95/10.05 ( ! [X0 : $int,X1 : $int] : ($less(X1,X0) | $less(X0,X1) | X0 = X1) )),
% 44.95/10.05 introduced(theory,[tha_order_totality])).
% 44.95/10.05 tff(f12,definition,(
% 44.95/10.05 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($less($sum(X0,X2),$sum(X1,X2)) | ~$less(X0,X1)) )),
% 44.95/10.05 introduced(theory,[tha_order_monotonicity])).
% 44.95/10.05 tff(f14,definition,(
% 44.95/10.05 ( ! [X0 : $int] : ($uminus($uminus(X0)) = X0) )),
% 44.95/10.05 introduced(theory,[tha_minus_minus_x])).
% 44.95/10.05 tff(f15,definition,(
% 44.95/10.05 ( ! [X0 : $int,X1 : $int] : ($product(X0,X1) = $product(X1,X0)) )),
% 44.95/10.05 introduced(theory,[tha_commutativity])).
% 44.95/10.05 tff(f17,definition,(
% 44.95/10.05 ( ! [X0 : $int] : ($product(X0,1) = X0) )),
% 44.95/10.05 introduced(theory,[tha_right_identity])).
% 44.95/10.05 tff(f19,definition,(
% 44.95/10.05 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($product(X0,$sum(X1,X2)) = $sum($product(X0,X1),$product(X0,X2))) )),
% 44.95/10.05 introduced(theory,[tha_distributivity])).
% 44.95/10.05 tff(f21,definition,(
% 44.95/10.05 ( ! [X0 : $int,X1 : $int] : (~$less(X1,$sum(X0,1)) | ~$less(X0,X1)) )),
% 44.95/10.05 introduced(theory,[tha_extra_integer_ordering])).
% 44.95/10.05 tff(f22,plain,(
% 44.95/10.05 ~$less($sum(7,$uminus($product(2,f(3)))),4) & ! [X0 : $int] : $less(1,f(X0))),
% 44.95/10.05 inference(ennf_transformation,[],[f3])).
% 44.95/10.05 tff(f23,plain,(
% 44.95/10.05 ( ! [X0 : $int] : ($less(1,f(X0))) )),
% 44.95/10.05 inference(cnf_transformation,[],[f22])).
% 44.95/10.05 tff(f24,plain,(
% 44.95/10.05 ~$less($sum(7,$uminus($product(2,f(3)))),4)),
% 44.95/10.05 inference(cnf_transformation,[],[f22])).
% 44.95/10.05 tff(f56,plain,(
% 44.95/10.05 ( ! [X0 : $int,X1 : $int] : (~$less(X0,X1) | ~$less(X1,$sum(1,X0))) )),
% 44.95/10.05 inference(superposition,[],[f21,f4])).
% 44.95/10.05 tff(f60,plain,(
% 44.95/10.05 ( ! [X0 : $int,X1 : $int] : (~$less(X0,1) | $less(X0,f(X1))) )),
% 44.95/10.05 inference(resolution,[],[f10,f23])).
% 44.95/10.05 tff(f63,plain,(
% 44.95/10.05 $less(4,$sum(7,$uminus($product(2,f(3))))) | 4 = $sum(7,$uminus($product(2,f(3))))),
% 44.95/10.05 inference(resolution,[],[f11,f24])).
% 44.95/10.05 tff(f71,definition,(
% 44.95/10.05 spl0_1 <=> 4 = $sum(7,$uminus($product(2,f(3))))),
% 44.95/10.05 introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition])).
% 44.95/10.05 tff(f73,plain,(
% 44.95/10.05 4 = $sum(7,$uminus($product(2,f(3)))) | ~spl0_1),
% 44.95/10.05 inference(avatar_component_clause,[],[f71])).
% 44.95/10.05 tff(f75,definition,(
% 44.95/10.05 spl0_2 <=> $less(4,$sum(7,$uminus($product(2,f(3)))))),
% 44.95/10.05 introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition])).
% 44.95/10.05 tff(f77,plain,(
% 44.95/10.05 $less(4,$sum(7,$uminus($product(2,f(3))))) | ~spl0_2),
% 44.95/10.05 inference(avatar_component_clause,[],[f75])).
% 44.95/10.05 tff(f79,plain,(
% 44.95/10.05 spl0_1 | spl0_2),
% 44.95/10.05 inference(avatar_split_clause,[],[f63,f75,f71])).
% 44.95/10.05 tff(f80,plain,(
% 44.95/10.05 ( ! [X0 : $int,X1 : $int] : ($uminus($sum(X1,$uminus(X0))) = $sum(X0,$uminus(X1))) )),
% 44.95/10.05 inference(superposition,[],[f7,f14])).
% 44.95/10.05 tff(f101,plain,(
% 44.95/10.05 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~$less(X1,X2) | $less($sum(X0,X1),$sum(X2,X0))) )),
% 44.95/10.05 inference(superposition,[],[f12,f4])).
% 44.95/10.05 tff(f114,plain,(
% 44.95/10.05 ( ! [X0 : $int,X1 : $int] : ($sum(0,X1) = $sum(X0,$sum($uminus(X0),X1))) )),
% 44.95/10.05 inference(superposition,[],[f5,f8])).
% 44.95/10.05 tff(f122,plain,(
% 44.95/10.05 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($sum(X0,$sum(X1,X2)) = $sum(X1,$sum(X2,X0))) )),
% 44.95/10.05 inference(superposition,[],[f5,f4])).
% 44.95/10.05 tff(f125,plain,(
% 44.95/10.05 ( ! [X2 : $int,X3 : $int,X0 : $int,X1 : $int] : (~$less($sum(X0,X1),X3) | $less($sum(X0,$sum(X1,X2)),$sum(X3,X2))) )),
% 44.95/10.05 inference(superposition,[],[f12,f5])).
% 44.95/10.05 tff(f134,plain,(
% 44.95/10.05 ( ! [X0 : $int,X1 : $int] : ($sum(X0,$sum($uminus(X0),X1)) = X1) )),
% 44.95/10.05 inference(evaluation,[],[f114])).
% 44.95/10.05 tff(f137,plain,(
% 44.95/10.05 ( ! [X0 : $int,X1 : $int] : ($less(X0,f(X1)) | $less(1,X0) | 1 = X0) )),
% 44.95/10.05 inference(resolution,[],[f60,f11])).
% 44.95/10.05 tff(f155,plain,(
% 44.95/10.05 ( ! [X0 : $int,X1 : $int] : ($product(X0,$sum(1,X1)) = $sum(X0,$product(X0,X1))) )),
% 44.95/10.05 inference(superposition,[],[f19,f17])).
% 44.95/10.05 tff(f203,plain,(
% 44.95/10.05 ( ! [X0 : $int] : (~$less(f(X0),$sum(1,1))) )),
% 44.95/10.05 inference(resolution,[],[f56,f23])).
% 44.95/10.05 tff(f207,plain,(
% 44.95/10.05 ( ! [X0 : $int] : (~$less(f(X0),2)) )),
% 44.95/10.05 inference(evaluation,[],[f203])).
% 44.95/10.05 tff(f208,plain,(
% 44.95/10.05 ( ! [X0 : $int] : ($less(2,f(X0)) | f(X0) = 2) )),
% 44.95/10.05 inference(resolution,[],[f207,f11])).
% 44.95/10.05 tff(f213,plain,(
% 44.95/10.05 ( ! [X0 : $int,X1 : $int] : ($sum(X1,$sum(X0,$uminus(X1))) = X0) )),
% 44.95/10.05 inference(superposition,[],[f134,f4])).
% 44.95/10.05 tff(f226,plain,(
% 44.95/10.05 ( ! [X0 : $int] : (f(X0) = 2 | ~$less(f(X0),$sum(1,2))) )),
% 44.95/10.05 inference(resolution,[],[f208,f56])).
% 44.95/10.05 tff(f228,plain,(
% 44.95/10.05 ( ! [X0 : $int] : (~$less(f(X0),3) | f(X0) = 2) )),
% 44.95/10.05 inference(evaluation,[],[f226])).
% 44.95/10.05 tff(f385,plain,(
% 44.95/10.05 ( ! [X0 : $int,X1 : $int] : ($less($sum(X0,1),$sum(f(X1),X0))) )),
% 44.95/10.05 inference(resolution,[],[f101,f23])).
% 44.95/10.05 tff(f387,plain,(
% 44.95/10.05 ( ! [X0 : $int] : ($less($sum(X0,4),$sum($sum(7,$uminus($product(2,f(3)))),X0))) ) | ~spl0_2),
% 44.95/10.05 inference(resolution,[],[f101,f77])).
% 44.95/10.05 tff(f395,plain,(
% 44.95/10.05 ( ! [X0 : $int] : ($less($sum(X0,4),$sum(7,$sum($uminus($product(2,f(3))),X0)))) ) | ~spl0_2),
% 44.95/10.05 inference(forward_demodulation,[],[f387,f5])).
% 44.95/10.05 tff(f402,plain,(
% 44.95/10.05 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~$less(X0,$sum(X1,1)) | $less(X0,$sum(f(X2),X1))) )),
% 44.95/10.05 inference(resolution,[],[f385,f10])).
% 44.95/10.05 tff(f403,plain,(
% 44.95/10.05 ( ! [X0 : $int,X1 : $int] : ($less($sum(1,X0),$sum(f(X1),X0))) )),
% 44.95/10.05 inference(superposition,[],[f385,f4])).
% 44.95/10.05 tff(f672,plain,(
% 44.95/10.05 ( ! [X0 : $int,X1 : $int] : ($sum(X1,0) = $sum($uminus(X0),$sum(X1,X0))) )),
% 44.95/10.05 inference(superposition,[],[f122,f8])).
% 44.95/10.05 tff(f727,plain,(
% 44.95/10.05 ( ! [X0 : $int,X1 : $int] : ($sum($uminus(X0),$sum(X1,X0)) = X1) )),
% 44.95/10.05 inference(evaluation,[],[f672])).
% 44.95/10.05 tff(f848,plain,(
% 44.95/10.05 ( ! [X0 : $int] : ($product(X0,$sum(1,1)) = $sum(X0,X0)) )),
% 44.95/10.05 inference(superposition,[],[f155,f17])).
% 44.95/10.05 tff(f873,plain,(
% 44.95/10.05 ( ! [X0 : $int] : ($sum(X0,X0) = $product(X0,2)) )),
% 44.95/10.05 inference(evaluation,[],[f848])).
% 44.95/10.05 tff(f1647,plain,(
% 44.95/10.05 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~$less(0,X1) | $less($sum(X0,$sum($uminus(X0),X2)),$sum(X1,X2))) )),
% 44.95/10.05 inference(superposition,[],[f125,f8])).
% 44.95/10.05 tff(f1674,plain,(
% 44.95/10.05 ( ! [X2 : $int,X1 : $int] : (~$less(0,X1) | $less(X2,$sum(X1,X2))) )),
% 44.95/10.05 inference(forward_demodulation,[],[f1647,f134])).
% 44.95/10.05 tff(f2277,plain,(
% 44.95/10.05 ( ! [X0 : $int] : ($less($sum($sum($uminus($uminus($product(2,f(3)))),X0),4),$sum(7,X0))) ) | ~spl0_2),
% 44.95/10.05 inference(superposition,[],[f395,f134])).
% 44.95/10.05 tff(f2288,plain,(
% 44.95/10.05 ( ! [X0 : $int] : ($less($sum($sum($product(2,f(3)),X0),4),$sum(7,X0))) ) | ~spl0_2),
% 44.95/10.05 inference(evaluation,[],[f2277])).
% 44.95/10.05 tff(f2298,plain,(
% 44.95/10.05 ( ! [X0 : $int] : ($less($sum(4,$sum($product(2,f(3)),X0)),$sum(7,X0))) ) | ~spl0_2),
% 44.95/10.05 inference(forward_demodulation,[],[f2288,f4])).
% 44.95/10.05 tff(f3357,plain,(
% 44.95/10.05 $sum($product(2,f(3)),$uminus(7)) = $uminus(4) | ~spl0_1),
% 44.95/10.05 inference(superposition,[],[f80,f73])).
% 44.95/10.05 tff(f3375,plain,(
% 44.95/10.05 $sum($product(2,f(3)),-7) = -4 | ~spl0_1),
% 44.95/10.05 inference(evaluation,[],[f3357])).
% 44.95/10.05 tff(f3396,plain,(
% 44.95/10.05 $product(2,f(3)) = $sum($uminus(-7),-4) | ~spl0_1),
% 44.95/10.05 inference(superposition,[],[f727,f3375])).
% 44.95/10.05 tff(f3397,plain,(
% 44.95/10.05 3 = $product(2,f(3)) | ~spl0_1),
% 44.95/10.05 inference(evaluation,[],[f3396])).
% 44.95/10.05 tff(f3984,plain,(
% 44.95/10.05 ( ! [X0 : $int,X1 : $int] : ($less(X0,$sum(f(X1),X0)) | $less(1,0) | 1 = 0) )),
% 44.95/10.05 inference(resolution,[],[f1674,f137])).
% 44.95/10.05 tff(f3996,plain,(
% 44.95/10.05 ( ! [X0 : $int,X1 : $int] : ($less(X0,$sum(f(X1),X0))) )),
% 44.95/10.05 inference(evaluation,[],[f3984])).
% 44.95/10.05 tff(f4350,plain,(
% 44.95/10.05 ( ! [X0 : $int] : ($less(f(X0),$product(f(X0),2))) )),
% 44.95/10.05 inference(superposition,[],[f3996,f873])).
% 44.95/10.05 tff(f4364,plain,(
% 44.95/10.05 ( ! [X0 : $int] : ($less(f(X0),$product(2,f(X0)))) )),
% 44.95/10.05 inference(forward_demodulation,[],[f4350,f15])).
% 44.95/10.05 tff(f7536,plain,(
% 44.95/10.05 $less(f(3),3) | ~spl0_1),
% 44.95/10.05 inference(superposition,[],[f4364,f3397])).
% 44.95/10.05 tff(f7544,plain,(
% 44.95/10.05 2 = f(3) | ~spl0_1),
% 44.95/10.05 inference(resolution,[],[f7536,f228])).
% 44.95/10.05 tff(f7564,plain,(
% 44.95/10.05 ~$less($sum(7,$uminus($product(2,2))),4) | ~spl0_1),
% 44.95/10.05 inference(superposition,[],[f24,f7544])).
% 44.95/10.05 tff(f7620,plain,(
% 44.95/10.05 $false | ~spl0_1),
% 44.95/10.05 inference(evaluation,[],[f7564])).
% 44.95/10.05 tff(f7621,plain,(
% 44.95/10.05 ~spl0_1),
% 44.95/10.05 inference(avatar_contradiction_clause,[],[f7620])).
% 44.95/10.05 tff(f271829,plain,(
% 44.95/10.05 ( ! [X0 : $int,X1 : $int] : ($less($sum(1,1),$sum(f(X0),f(X1)))) )),
% 44.95/10.05 inference(resolution,[],[f402,f403])).
% 44.95/10.05 tff(f271867,plain,(
% 44.95/10.05 ( ! [X0 : $int,X1 : $int] : ($less(2,$sum(f(X0),f(X1)))) )),
% 44.95/10.05 inference(evaluation,[],[f271829])).
% 44.95/10.05 tff(f272265,plain,(
% 44.95/10.05 ( ! [X0 : $int] : ($less(2,$product(f(X0),2))) )),
% 44.95/10.05 inference(superposition,[],[f271867,f873])).
% 44.95/10.05 tff(f272279,plain,(
% 44.95/10.05 ( ! [X0 : $int] : ($less(2,$product(2,f(X0)))) )),
% 44.95/10.05 inference(forward_demodulation,[],[f272265,f15])).
% 44.95/10.05 tff(f272462,plain,(
% 44.95/10.05 ( ! [X0 : $int] : (~$less($product(2,f(X0)),$sum(1,2))) )),
% 44.95/10.05 inference(resolution,[],[f272279,f56])).
% 44.95/10.05 tff(f272499,plain,(
% 44.95/10.05 ( ! [X0 : $int] : (~$less($product(2,f(X0)),3)) )),
% 44.95/10.05 inference(evaluation,[],[f272462])).
% 44.95/10.05 tff(f288682,plain,(
% 44.95/10.05 $less($product(2,f(3)),$sum(7,$uminus(4))) | ~spl0_2),
% 44.95/10.05 inference(superposition,[],[f2298,f213])).
% 44.95/10.05 tff(f288745,plain,(
% 44.95/10.05 $less($product(2,f(3)),3) | ~spl0_2),
% 44.95/10.05 inference(evaluation,[],[f288682])).
% 44.95/10.05 tff(f288780,plain,(
% 44.95/10.05 $false | ~spl0_2),
% 44.95/10.05 inference(forward_subsumption_resolution,[],[f288745,f272499])).
% 44.95/10.05 tff(f288781,plain,(
% 44.95/10.05 ~spl0_2),
% 44.95/10.05 inference(avatar_contradiction_clause,[],[f288780])).
% 44.95/10.05 cnf(s2, plain, spl0_1 | spl0_2, inference(sat_conversion,[],[f79])).
% 44.95/10.05 cnf(s20, plain, ~spl0_1, inference(sat_conversion,[],[f7621])).
% 44.95/10.05 cnf(s1599, plain, ~spl0_2, inference(sat_conversion,[],[f288781])).
% 44.95/10.05 cnf(s1965, plain, $false, inference(rat,[],[s2,s1599,s20])).
% 44.95/10.05 tff(f288984,plain,(
% 44.95/10.05 $false),
% 44.95/10.05 inference(avatar_sat_refutation,[],[s1965])).
% 44.95/10.05 % SZS output end Proof for theBenchmark
% 44.95/10.05 % (2988437)------------------------------
% 44.95/10.05 % (2988437)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.95/10.05 % (2988437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.95/10.05 % (2988437)CaDiCaL version: 2.1.3
% 44.95/10.05 % (2988437)Termination reason: Refutation
% 44.95/10.05 % (2988437)Time elapsed: 9.754 s
% 44.95/10.05 % (2988437)Peak memory usage: 118 MB
% 44.95/10.05 % (2988437)Instructions burned: 18478 (million)
% 44.95/10.05 % (2988431)Success in time 9.826 s
% 44.95/10.05 % Vampire exiting
%------------------------------------------------------------------------------