%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ARI584_1 : TPTP v9.3.1. Released v5.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 09:34:55 AM UTC 2026
% Result : Theorem 13.37s 2.24s
% Output : Refutation 13.37s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : ARI584_1 : TPTP v9.3.1. Released v5.1.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.27 % Computer : n014.cluster.edu
% 0.10/0.27 % Model : x86_64 x86_64
% 0.10/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.27 % Memory : 8046.5625MB
% 0.10/0.27 % OS : Linux 6.8.0-71-generic
% 0.10/0.27 % CPULimit : 300
% 0.10/0.27 % WCLimit : 300
% 0.10/0.27 % DateTime : Mon Sep 28 20:52:45 UTC 2026
% 0.10/0.28 % CPUTime :
% 0.10/0.28 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.27/0.33 Running first-order model finding
% 0.27/0.33 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
% 6.16/1.27 % (2173594)Will run a generic schedule for satisfiability detection.
% 6.16/1.27 % (2173599)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1520273386_3000 on theBenchmark for (3000ds/0Mi)
% 6.16/1.27 % (2173599)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 6.16/1.27 % (2173599)Terminated due to inappropriate strategy.
% 6.16/1.27 % (2173599)------------------------------
% 6.16/1.27 % (2173599)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.16/1.27 % (2173599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.16/1.27 % (2173599)CaDiCaL version: 2.1.3
% 6.16/1.27 % (2173599)Termination reason: Inappropriate
% 6.16/1.27 % (2173599)Time elapsed: 0.0000 s
% 6.16/1.27 % (2173599)Peak memory usage: 10 MB
% 6.16/1.27 % (2173599)------------------------------
% 6.16/1.27 % (2173599)------------------------------
% 6.16/1.27 % (2173600)% WARNING: option uhcvi not known.
% 6.16/1.27 % (2173602)dis+10_1_sil=32000:sp=arity:random_seed=2749594699:i=103:fgj=on_3000 on theBenchmark for (3000ds/103Mi)
% 6.16/1.27 % (2173601)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2997574758:i=88024:add=on:rawr=on_3000 on theBenchmark for (3000ds/88024Mi)
% 6.16/1.27 % (2173603)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3586800418:i=116_3000 on theBenchmark for (3000ds/116Mi)
% 6.16/1.27 % (2173605)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=735458801:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_3000 on theBenchmark for (3000ds/159Mi)
% 6.16/1.27 % (2173604)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2567131722:i=131_3000 on theBenchmark for (3000ds/131Mi)
% 6.16/1.27 % (2173600)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1806518254:i=135531:add=off:rawr=on_3000 on theBenchmark for (3000ds/135531Mi)
% 6.16/1.27 % (2173607)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1985087845:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 6.16/1.27 % (2173607)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 6.16/1.27 % (2173607)Terminated due to inappropriate strategy.
% 6.16/1.27 % (2173607)------------------------------
% 6.16/1.27 % (2173607)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.16/1.27 % (2173607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.16/1.27 % (2173607)CaDiCaL version: 2.1.3
% 6.16/1.27 % (2173607)Termination reason: Inappropriate
% 6.16/1.27 % (2173607)Time elapsed: 0.0000 s
% 6.16/1.27 % (2173607)Peak memory usage: 10 MB
% 6.16/1.27 % (2173607)------------------------------
% 6.16/1.27 % (2173607)------------------------------
% 6.16/1.27 % (2173615)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2542073034:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 6.16/1.27 % (2173602)Instruction limit reached!
% 6.16/1.27 % (2173602)------------------------------
% 6.16/1.27 % (2173602)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.16/1.27 % (2173602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.16/1.27 % (2173602)CaDiCaL version: 2.1.3
% 6.16/1.27 % (2173602)Termination reason: Instruction limit
% 6.16/1.27 % (2173602)Termination phase: Saturation
% 6.16/1.27 % (2173602)Time elapsed: 0.106 s
% 6.16/1.27 % (2173602)Peak memory usage: 12 MB
% 6.16/1.27 % (2173602)Instructions burned: 104 (million)
% 6.16/1.27 % (2173603)Instruction limit reached!
% 6.16/1.27 % (2173603)------------------------------
% 6.16/1.27 % (2173603)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.16/1.27 % (2173603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.16/1.27 % (2173603)CaDiCaL version: 2.1.3
% 6.16/1.27 % (2173603)Termination reason: Instruction limit
% 6.16/1.27 % (2173603)Termination phase: Saturation
% 6.16/1.27 % (2173603)Time elapsed: 0.116 s
% 6.16/1.27 % (2173603)Peak memory usage: 12 MB
% 6.16/1.27 % (2173603)Instructions burned: 116 (million)
% 6.16/1.27 % (2173615)Instruction limit reached!
% 6.16/1.27 % (2173615)------------------------------
% 6.16/1.27 % (2173615)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.16/1.27 % (2173615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.16/1.27 % (2173615)CaDiCaL version: 2.1.3
% 6.16/1.27 % (2173615)Termination reason: Instruction limit
% 6.16/1.27 % (2173615)Termination phase: Saturation
% 6.16/1.27 % (2173615)Time elapsed: 0.087 s
% 13.37/2.24 % (2173615)Peak memory usage: 13 MB
% 13.37/2.24 % (2173615)Instructions burned: 132 (million)
% 13.37/2.24 % (2173604)Instruction limit reached!
% 13.37/2.24 % (2173604)------------------------------
% 13.37/2.24 % (2173604)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.37/2.24 % (2173604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.37/2.24 % (2173604)CaDiCaL version: 2.1.3
% 13.37/2.24 % (2173604)Termination reason: Instruction limit
% 13.37/2.24 % (2173604)Termination phase: Saturation
% 13.37/2.24 % (2173604)Time elapsed: 0.138 s
% 13.37/2.24 % (2173604)Peak memory usage: 12 MB
% 13.37/2.24 % (2173604)Instructions burned: 131 (million)
% 13.37/2.24 % (2173618)ott-21_1_sil=16000:fs=off:random_seed=2529779877:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 13.37/2.24 % (2173617)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=3346286215:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 13.37/2.24 % (2173619)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1509639690:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 13.37/2.24 % (2173622)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1074271220:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 13.37/2.24 % (2173622)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 13.37/2.24 % (2173622)Terminated due to inappropriate strategy.
% 13.37/2.24 % (2173622)------------------------------
% 13.37/2.24 % (2173622)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.37/2.24 % (2173622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.37/2.24 % (2173622)CaDiCaL version: 2.1.3
% 13.37/2.24 % (2173622)Termination reason: Inappropriate
% 13.37/2.24 % (2173622)Time elapsed: 0.001 s
% 13.37/2.24 % (2173622)Peak memory usage: 10 MB
% 13.37/2.24 % (2173622)------------------------------
% 13.37/2.24 % (2173622)------------------------------
% 13.37/2.24 % (2173605)Instruction limit reached!
% 13.37/2.24 % (2173605)------------------------------
% 13.37/2.24 % (2173605)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.37/2.24 % (2173605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.37/2.24 % (2173605)CaDiCaL version: 2.1.3
% 13.37/2.24 % (2173605)Termination reason: Instruction limit
% 13.37/2.24 % (2173605)Termination phase: Saturation
% 13.37/2.24 % (2173605)Time elapsed: 0.180 s
% 13.37/2.24 % (2173605)Peak memory usage: 13 MB
% 13.37/2.24 % (2173605)Instructions burned: 159 (million)
% 13.37/2.24 % (2173625)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2931630169:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 13.37/2.24 % (2173626)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3736217861:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi)
% 13.37/2.24 % (2173626)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 13.37/2.24 % (2173626)Terminated due to inappropriate strategy.
% 13.37/2.24 % (2173626)------------------------------
% 13.37/2.24 % (2173626)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.37/2.24 % (2173626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.37/2.24 % (2173626)CaDiCaL version: 2.1.3
% 13.37/2.24 % (2173626)Termination reason: Inappropriate
% 13.37/2.24 % (2173626)Time elapsed: 0.001 s
% 13.37/2.24 % (2173626)Peak memory usage: 10 MB
% 13.37/2.24 % (2173626)------------------------------
% 13.37/2.24 % (2173626)------------------------------
% 13.37/2.24 % (2173629)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=671519498: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)
% 13.37/2.24 % (2173618)Instruction limit reached!
% 13.37/2.24 % (2173618)------------------------------
% 13.37/2.24 % (2173618)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.37/2.24 % (2173618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.37/2.24 % (2173618)CaDiCaL version: 2.1.3
% 13.37/2.24 % (2173618)Termination reason: Instruction limit
% 13.37/2.24 % (2173618)Termination phase: Saturation
% 13.37/2.24 % (2173618)Time elapsed: 0.136 s
% 13.37/2.24 % (2173618)Peak memory usage: 12 MB
% 13.37/2.24 % (2173618)Instructions burned: 180 (million)
% 13.37/2.24 % (2173631)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1236618404:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi)
% 13.37/2.24 % (2173619)Instruction limit reached!
% 13.37/2.24 % (2173619)------------------------------
% 13.37/2.24 % (2173619)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.37/2.24 % (2173619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.37/2.24 % (2173619)CaDiCaL version: 2.1.3
% 13.37/2.24 % (2173619)Termination reason: Instruction limit
% 13.37/2.24 % (2173619)Termination phase: Saturation
% 13.37/2.24 % (2173619)Time elapsed: 0.251 s
% 13.37/2.24 % (2173619)Peak memory usage: 13 MB
% 13.37/2.24 % (2173619)Instructions burned: 479 (million)
% 13.37/2.24 % (2173633)fmb+10_1_sil=64000:random_seed=4264990052:i=22061:nm=2:gsp=on_2995 on theBenchmark for (2995ds/22061Mi)
% 13.37/2.24 % (2173633)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 13.37/2.24 % (2173633)Terminated due to inappropriate strategy.
% 13.37/2.24 % (2173633)------------------------------
% 13.37/2.24 % (2173633)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.37/2.24 % (2173633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.37/2.24 % (2173633)CaDiCaL version: 2.1.3
% 13.37/2.24 % (2173633)Termination reason: Inappropriate
% 13.37/2.24 % (2173633)Time elapsed: 0.001 s
% 13.37/2.24 % (2173633)Peak memory usage: 10 MB
% 13.37/2.24 % (2173633)------------------------------
% 13.37/2.24 % (2173633)------------------------------
% 13.37/2.24 % (2173635)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3428620251:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi)
% 13.37/2.24 % (2173635)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 13.37/2.24 % (2173635)Terminated due to inappropriate strategy.
% 13.37/2.24 % (2173635)------------------------------
% 13.37/2.24 % (2173635)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.37/2.24 % (2173635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.37/2.24 % (2173635)CaDiCaL version: 2.1.3
% 13.37/2.24 % (2173635)Termination reason: Inappropriate
% 13.37/2.24 % (2173635)Time elapsed: 0.0000 s
% 13.37/2.24 % (2173635)Peak memory usage: 10 MB
% 13.37/2.24 % (2173635)------------------------------
% 13.37/2.24 % (2173635)------------------------------
% 13.37/2.24 % (2173637)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3842878040:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi)
% 13.37/2.24 % (2173637)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 13.37/2.24 % (2173637)Terminated due to inappropriate strategy.
% 13.37/2.24 % (2173637)------------------------------
% 13.37/2.24 % (2173637)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.37/2.24 % (2173637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.37/2.24 % (2173637)CaDiCaL version: 2.1.3
% 13.37/2.24 % (2173637)Termination reason: Inappropriate
% 13.37/2.24 % (2173637)Time elapsed: 0.001 s
% 13.37/2.24 % (2173637)Peak memory usage: 10 MB
% 13.37/2.24 % (2173637)------------------------------
% 13.37/2.24 % (2173637)------------------------------
% 13.37/2.24 % (2173639)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3148753412:i=5131_2994 on theBenchmark for (2994ds/5131Mi)
% 13.37/2.24 % (2173617)Instruction limit reached!
% 13.37/2.24 % (2173617)------------------------------
% 13.37/2.24 % (2173617)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.37/2.24 % (2173617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.37/2.24 % (2173617)CaDiCaL version: 2.1.3
% 13.37/2.24 % (2173617)Termination reason: Instruction limit
% 13.37/2.24 % (2173617)Termination phase: Saturation
% 13.37/2.24 % (2173617)Time elapsed: 0.601 s
% 13.37/2.24 % (2173617)Peak memory usage: 16 MB
% 13.37/2.24 % (2173617)Instructions burned: 684 (million)
% 13.37/2.24 % (2173641)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2873448871:i=1472:ins=7:fdi=8:gsp=on_2992 on theBenchmark for (2992ds/1472Mi)
% 13.37/2.24 % (2173629)Instruction limit reached!
% 13.37/2.24 % (2173629)------------------------------
% 13.37/2.24 % (2173629)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.37/2.24 % (2173629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.37/2.24 % (2173629)CaDiCaL version: 2.1.3
% 13.37/2.24 % (2173629)Termination reason: Instruction limit
% 13.37/2.24 % (2173629)Termination phase: Saturation
% 13.37/2.24 % (2173629)Time elapsed: 0.628 s
% 13.37/2.24 % (2173629)Peak memory usage: 14 MB
% 13.37/2.24 % (2173629)Instructions burned: 692 (million)
% 13.37/2.24 % (2173643)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=445249834:i=6324_2990 on theBenchmark for (2990ds/6324Mi)
% 13.37/2.24 % (2173643)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 13.37/2.24 % (2173643)Terminated due to inappropriate strategy.
% 13.37/2.24 % (2173643)------------------------------
% 13.37/2.24 % (2173643)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.37/2.24 % (2173643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.37/2.24 % (2173643)CaDiCaL version: 2.1.3
% 13.37/2.24 % (2173643)Termination reason: Inappropriate
% 13.37/2.24 % (2173643)Time elapsed: 0.001 s
% 13.37/2.24 % (2173643)Peak memory usage: 10 MB
% 13.37/2.24 % (2173643)------------------------------
% 13.37/2.24 % (2173643)------------------------------
% 13.37/2.24 % (2173645)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2856030017:fmbsr=2.30978:i=2174_2990 on theBenchmark for (2990ds/2174Mi)
% 13.37/2.24 % (2173645)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 13.37/2.24 % (2173645)Terminated due to inappropriate strategy.
% 13.37/2.24 % (2173645)------------------------------
% 13.37/2.24 % (2173645)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.37/2.24 % (2173645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.37/2.24 % (2173645)CaDiCaL version: 2.1.3
% 13.37/2.24 % (2173645)Termination reason: Inappropriate
% 13.37/2.24 % (2173645)Time elapsed: 0.001 s
% 13.37/2.24 % (2173645)Peak memory usage: 10 MB
% 13.37/2.24 % (2173645)------------------------------
% 13.37/2.24 % (2173645)------------------------------
% 13.37/2.24 % (2173647)ott-2_1_sil=16000:newcnf=on:random_seed=853307065:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2990 on theBenchmark for (2990ds/869Mi)
% 13.37/2.24 % (2173631)Instruction limit reached!
% 13.37/2.24 % (2173631)------------------------------
% 13.37/2.24 % (2173631)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.37/2.24 % (2173631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.37/2.24 % (2173631)CaDiCaL version: 2.1.3
% 13.37/2.24 % (2173631)Termination reason: Instruction limit
% 13.37/2.24 % (2173631)Termination phase: Saturation
% 13.37/2.24 % (2173631)Time elapsed: 0.869 s
% 13.37/2.24 % (2173631)Peak memory usage: 19 MB
% 13.37/2.24 % (2173631)Instructions burned: 879 (million)
% 13.37/2.24 % (2173649)ott+10_1_sil=32000:tgt=ground:random_seed=1711775283:i=5114:av=off_2987 on theBenchmark for (2987ds/5114Mi)
% 13.37/2.24 % (2173625)Instruction limit reached!
% 13.37/2.24 % (2173625)------------------------------
% 13.37/2.24 % (2173625)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.37/2.24 % (2173625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.37/2.24 % (2173625)CaDiCaL version: 2.1.3
% 13.37/2.24 % (2173625)Termination reason: Instruction limit
% 13.37/2.24 % (2173625)Termination phase: Saturation
% 13.37/2.24 % (2173625)Time elapsed: 1.212 s
% 13.37/2.24 % (2173625)Peak memory usage: 16 MB
% 13.37/2.24 % (2173625)Instructions burned: 1179 (million)
% 13.37/2.24 % (2173651)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=212695916:i=54282_2985 on theBenchmark for (2985ds/54282Mi)
% 13.37/2.24 % (2173651)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 13.37/2.24 % (2173651)Terminated due to inappropriate strategy.
% 13.37/2.24 % (2173651)------------------------------
% 13.37/2.24 % (2173651)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.37/2.24 % (2173651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.37/2.24 % (2173651)CaDiCaL version: 2.1.3
% 13.37/2.24 % (2173651)Termination reason: Inappropriate
% 13.37/2.24 % (2173651)Time elapsed: 0.001 s
% 13.37/2.24 % (2173651)Peak memory usage: 10 MB
% 13.37/2.24 % (2173651)------------------------------
% 13.37/2.24 % (2173651)------------------------------
% 13.37/2.24 % (2173653)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1986360939:i=3512:aac=none_2984 on theBenchmark for (2984ds/3512Mi)
% 13.37/2.24 % (2173653) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2173594-2173653"...
% 13.37/2.24 % (2173653)...printing done.
% 13.37/2.24 % (2173653)Refutation found. Thanks to Tanya!
% 13.37/2.24 % SZS status Theorem for theBenchmark
% 13.37/2.24 % SZS output start Proof for theBenchmark
% 13.37/2.24 tff(func_def_6, type, sK0: $int).
% 13.37/2.24 tff(func_def_7, type, sK1: $int).
% 13.37/2.24 tff(f1,conjecture,(
% 13.37/2.24 ! [X0 : $int,X1 : $int] : ? [X2 : $int] : ($less(X0,X2) & $less(X2,$sum(X0,5)) & ~($less(X1,X2) & $less(X2,$sum(X1,3))))),
% 13.37/2.24 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',interv_3_cannot_cover_interv_5)).
% 13.37/2.24 tff(f2,negated_conjecture,(
% 13.37/2.24 ~ ! [X0 : $int,X1 : $int] : ? [X2 : $int] : ($less(X0,X2) & $less(X2,$sum(X0,5)) & ~($less(X1,X2) & $less(X2,$sum(X1,3))))),
% 13.37/2.24 inference(negated_conjecture,[status(cth)],[f1])).
% 13.37/2.24 tff(f3,definition,(
% 13.37/2.24 ( ! [X0 : $int,X1 : $int] : ($sum(X0,X1) = $sum(X1,X0)) )),
% 13.37/2.24 introduced(theory,[tha_commutativity])).
% 13.37/2.24 tff(f4,definition,(
% 13.37/2.24 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($sum(X0,$sum(X1,X2)) = $sum($sum(X0,X1),X2)) )),
% 13.37/2.24 introduced(theory,[tha_associativity])).
% 13.37/2.24 tff(f5,definition,(
% 13.37/2.24 ( ! [X0 : $int] : ($sum(X0,0) = X0) )),
% 13.37/2.24 introduced(theory,[tha_right_identity])).
% 13.37/2.24 tff(f6,definition,(
% 13.37/2.24 ( ! [X0 : $int,X1 : $int] : ($uminus($sum(X0,X1)) = $sum($uminus(X1),$uminus(X0))) )),
% 13.37/2.24 introduced(theory,[tha_inverse_op_op_inverses])).
% 13.37/2.24 tff(f7,definition,(
% 13.37/2.24 ( ! [X0 : $int] : (0 = $sum(X0,$uminus(X0))) )),
% 13.37/2.24 introduced(theory,[tha_inverse_op_unit])).
% 13.37/2.24 tff(f8,definition,(
% 13.37/2.24 ( ! [X0 : $int] : (~$less(X0,X0)) )),
% 13.37/2.24 introduced(theory,[tha_non-reflexivity])).
% 13.37/2.24 tff(f9,definition,(
% 13.37/2.24 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($less(X0,X2) | ~$less(X1,X2) | ~$less(X0,X1)) )),
% 13.37/2.24 introduced(theory,[tha_transitivity])).
% 13.37/2.24 tff(f10,definition,(
% 13.37/2.24 ( ! [X0 : $int,X1 : $int] : ($less(X1,X0) | $less(X0,X1) | X0 = X1) )),
% 13.37/2.24 introduced(theory,[tha_order_totality])).
% 13.37/2.24 tff(f11,definition,(
% 13.37/2.24 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($less($sum(X0,X2),$sum(X1,X2)) | ~$less(X0,X1)) )),
% 13.37/2.24 introduced(theory,[tha_order_monotonicity])).
% 13.37/2.24 tff(f12,definition,(
% 13.37/2.24 ( ! [X0 : $int,X1 : $int] : ($less(X1,$sum(X0,1)) | $less(X0,X1)) )),
% 13.37/2.24 introduced(theory,[tha_order_plus_one_dichotomy])).
% 13.37/2.24 tff(f14,definition,(
% 13.37/2.24 ( ! [X0 : $int,X1 : $int] : (~$less(X1,$sum(X0,1)) | ~$less(X0,X1)) )),
% 13.37/2.24 introduced(theory,[tha_extra_integer_ordering])).
% 13.37/2.24 tff(f15,plain,(
% 13.37/2.24 ? [X0 : $int,X1 : $int] : ! [X2 : $int] : (~$less(X0,X2) | ~$less(X2,$sum(X0,5)) | ($less(X1,X2) & $less(X2,$sum(X1,3))))),
% 13.37/2.24 inference(ennf_transformation,[],[f2])).
% 13.37/2.24 tff(f16,plain,(
% 13.37/2.24 ! [X2 : $int] : (~$less(sK0,X2) | ~$less(X2,$sum(sK0,5)) | ($less(sK1,X2) & $less(X2,$sum(sK1,3))))),
% 13.37/2.24 inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(X0,sK0),skolemize(X1,sK1)],[f15])).
% 13.37/2.24 tff(f17,plain,(
% 13.37/2.24 ( ! [X2 : $int] : ($less(X2,$sum(sK1,3)) | ~$less(X2,$sum(sK0,5)) | ~$less(sK0,X2)) )),
% 13.37/2.24 inference(cnf_transformation,[],[f16])).
% 13.37/2.24 tff(f18,plain,(
% 13.37/2.24 ( ! [X2 : $int] : ($less(sK1,X2) | ~$less(X2,$sum(sK0,5)) | ~$less(sK0,X2)) )),
% 13.37/2.24 inference(cnf_transformation,[],[f16])).
% 13.37/2.24 tff(f20,plain,(
% 13.37/2.24 ~$less($sum(sK1,3),$sum(sK0,5)) | ~$less(sK0,$sum(sK1,3))),
% 13.37/2.24 inference(resolution,[],[f8,f17])).
% 13.37/2.24 tff(f22,definition,(
% 13.37/2.24 spl2_1 <=> $less(sK0,$sum(sK1,3))),
% 13.37/2.24 introduced(definition,[new_symbols(definition,[spl2_1])],[avatar_definition])).
% 13.37/2.24 tff(f23,plain,(
% 13.37/2.24 ~$less(sK0,$sum(sK1,3)) | spl2_1),
% 13.37/2.24 inference(avatar_component_clause,[],[f22])).
% 13.37/2.24 tff(f25,definition,(
% 13.37/2.24 spl2_2 <=> $less($sum(sK1,3),$sum(sK0,5))),
% 13.37/2.24 introduced(definition,[new_symbols(definition,[spl2_2])],[avatar_definition])).
% 13.37/2.24 tff(f26,plain,(
% 13.37/2.24 ~$less($sum(sK1,3),$sum(sK0,5)) | spl2_2),
% 13.37/2.24 inference(avatar_component_clause,[],[f25])).
% 13.37/2.24 tff(f27,plain,(
% 13.37/2.24 ~spl2_1 | ~spl2_2),
% 13.37/2.24 inference(avatar_split_clause,[],[f20,f25,f22])).
% 13.37/2.24 tff(f29,definition,(
% 13.37/2.24 spl2_3 <=> $less(sK0,sK1)),
% 13.37/2.24 introduced(definition,[new_symbols(definition,[spl2_3])],[avatar_definition])).
% 13.37/2.24 tff(f30,plain,(
% 13.37/2.24 ~$less(sK0,sK1) | spl2_3),
% 13.37/2.24 inference(avatar_component_clause,[],[f29])).
% 13.37/2.24 tff(f54,plain,(
% 13.37/2.24 ( ! [X0 : $int] : ($less(X0,$sum(3,sK1)) | ~$less(X0,$sum(sK0,5)) | ~$less(sK0,X0)) )),
% 13.37/2.24 inference(superposition,[],[f17,f3])).
% 13.37/2.24 tff(f55,plain,(
% 13.37/2.24 ( ! [X0 : $int] : (~$less(X0,$sum(5,sK0)) | $less(X0,$sum(3,sK1)) | ~$less(sK0,X0)) )),
% 13.37/2.24 inference(forward_demodulation,[],[f54,f3])).
% 13.37/2.24 tff(f59,plain,(
% 13.37/2.24 ( ! [X0 : $int] : ($less(X0,$sum(X0,1))) )),
% 13.37/2.24 inference(resolution,[],[f12,f8])).
% 13.37/2.24 tff(f60,plain,(
% 13.37/2.24 ( ! [X0 : $int,X1 : $int] : ($less(X1,$sum(1,X0)) | $less(X0,X1)) )),
% 13.37/2.24 inference(superposition,[],[f12,f3])).
% 13.37/2.24 tff(f64,plain,(
% 13.37/2.24 ( ! [X0 : $int] : (~$less(X0,sK1) | ~$less($sum(X0,1),$sum(sK0,5)) | ~$less(sK0,$sum(X0,1))) )),
% 13.37/2.24 inference(resolution,[],[f14,f18])).
% 13.37/2.24 tff(f70,plain,(
% 13.37/2.24 ( ! [X0 : $int] : (~$less($sum(X0,1),$sum(5,sK0)) | ~$less(X0,sK1) | ~$less(sK0,$sum(X0,1))) )),
% 13.37/2.24 inference(forward_demodulation,[],[f64,f3])).
% 13.37/2.24 tff(f71,plain,(
% 13.37/2.24 ( ! [X0 : $int,X1 : $int] : (~$less(X0,X1) | ~$less(X1,X0)) )),
% 13.37/2.24 inference(resolution,[],[f9,f8])).
% 13.37/2.24 tff(f73,plain,(
% 13.37/2.24 ( ! [X0 : $int] : (~$less(X0,$sum(sK1,3)) | ~$less(sK0,X0)) ) | spl2_1),
% 13.37/2.24 inference(resolution,[],[f9,f23])).
% 13.37/2.24 tff(f78,plain,(
% 13.37/2.24 ( ! [X0 : $int] : (~$less(X0,$sum(3,sK1)) | ~$less(sK0,X0)) ) | spl2_1),
% 13.37/2.24 inference(forward_demodulation,[],[f73,f3])).
% 13.37/2.24 tff(f126,plain,(
% 13.37/2.24 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($less($sum(X0,X1),$sum(X2,X0)) | ~$less(X1,X2)) )),
% 13.37/2.24 inference(superposition,[],[f11,f3])).
% 13.37/2.24 tff(f142,plain,(
% 13.37/2.24 ( ! [X0 : $int,X1 : $int] : ($sum(0,X1) = $sum(X0,$sum($uminus(X0),X1))) )),
% 13.37/2.24 inference(superposition,[],[f4,f7])).
% 13.37/2.24 tff(f150,plain,(
% 13.37/2.24 ( ! [X0 : $int,X1 : $int] : (0 = $sum(X0,$sum(X1,$uminus($sum(X0,X1))))) )),
% 13.37/2.24 inference(superposition,[],[f4,f7])).
% 13.37/2.24 tff(f162,plain,(
% 13.37/2.24 ( ! [X0 : $int,X1 : $int] : ($sum(X0,$sum($uminus(X0),X1)) = X1) )),
% 13.37/2.24 inference(evaluation,[],[f142])).
% 13.37/2.24 tff(f182,plain,(
% 13.37/2.24 ( ! [X0 : $int] : (~$less(sK0,$sum(X0,sK1)) | ~$less(X0,3)) ) | spl2_1),
% 13.37/2.24 inference(resolution,[],[f78,f11])).
% 13.37/2.24 tff(f211,plain,(
% 13.37/2.24 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~$less($sum(X2,X1),$sum(X0,X1)) | ~$less(X0,X2)) )),
% 13.37/2.24 inference(resolution,[],[f71,f11])).
% 13.37/2.24 tff(f239,plain,(
% 13.37/2.24 $less(sK1,sK0) | ~$less(1,3) | spl2_1),
% 13.37/2.24 inference(resolution,[],[f60,f182])).
% 13.37/2.24 tff(f245,plain,(
% 13.37/2.24 $less(sK1,sK0) | spl2_1),
% 13.37/2.24 inference(evaluation,[],[f239])).
% 13.37/2.24 tff(f311,plain,(
% 13.37/2.24 ( ! [X0 : $int,X1 : $int] : ($uminus(X0) = $sum(X1,$uminus($sum(X0,X1)))) )),
% 13.37/2.24 inference(superposition,[],[f162,f6])).
% 13.37/2.24 tff(f431,plain,(
% 13.37/2.24 ~$less($sum(sK1,3),$sum(5,sK0)) | spl2_2),
% 13.37/2.24 inference(forward_demodulation,[],[f26,f3])).
% 13.37/2.24 tff(f554,plain,(
% 13.37/2.24 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~$less($sum(X1,X2),$sum(X2,X0)) | ~$less(X0,X1)) )),
% 13.37/2.24 inference(resolution,[],[f126,f71])).
% 13.37/2.24 tff(f559,plain,(
% 13.37/2.24 ( ! [X0 : $int,X1 : $int] : ($less(X0,$sum(X1,X0)) | ~$less(0,X1)) )),
% 13.37/2.24 inference(superposition,[],[f126,f5])).
% 13.37/2.24 tff(f1797,definition,(
% 13.37/2.24 spl2_15 <=> sK0 = sK1),
% 13.37/2.24 introduced(definition,[new_symbols(definition,[spl2_15])],[avatar_definition])).
% 13.37/2.24 tff(f1798,plain,(
% 13.37/2.24 sK0 = sK1 | ~spl2_15),
% 13.37/2.24 inference(avatar_component_clause,[],[f1797])).
% 13.37/2.24 tff(f1800,definition,(
% 13.37/2.24 spl2_16 <=> $less(sK1,sK0)),
% 13.37/2.24 introduced(definition,[new_symbols(definition,[spl2_16])],[avatar_definition])).
% 13.37/2.24 tff(f1801,plain,(
% 13.37/2.24 $less(sK1,sK0) | ~spl2_16),
% 13.37/2.24 inference(avatar_component_clause,[],[f1800])).
% 13.37/2.24 tff(f2644,plain,(
% 13.37/2.24 ~$less($sum(3,sK1),$sum(5,sK0)) | spl2_2),
% 13.37/2.24 inference(forward_demodulation,[],[f431,f3])).
% 13.37/2.24 tff(f4642,plain,(
% 13.37/2.24 spl2_16 | spl2_1),
% 13.37/2.24 inference(avatar_split_clause,[],[f245,f22,f1800])).
% 13.37/2.24 tff(f5843,plain,(
% 13.37/2.24 $less($sum(5,sK0),$sum(3,sK1)) | $sum(5,sK0) = $sum(3,sK1) | spl2_2),
% 13.37/2.24 inference(resolution,[],[f2644,f10])).
% 13.37/2.24 tff(f5846,definition,(
% 13.37/2.24 spl2_88 <=> $sum(5,sK0) = $sum(3,sK1)),
% 13.37/2.24 introduced(definition,[new_symbols(definition,[spl2_88])],[avatar_definition])).
% 13.37/2.24 tff(f5847,plain,(
% 13.37/2.24 $sum(5,sK0) = $sum(3,sK1) | ~spl2_88),
% 13.37/2.24 inference(avatar_component_clause,[],[f5846])).
% 13.37/2.24 tff(f5849,definition,(
% 13.37/2.24 spl2_89 <=> $less($sum(5,sK0),$sum(3,sK1))),
% 13.37/2.24 introduced(definition,[new_symbols(definition,[spl2_89])],[avatar_definition])).
% 13.37/2.24 tff(f5850,plain,(
% 13.37/2.24 $less($sum(5,sK0),$sum(3,sK1)) | ~spl2_89),
% 13.37/2.24 inference(avatar_component_clause,[],[f5849])).
% 13.37/2.24 tff(f5851,plain,(
% 13.37/2.24 spl2_88 | spl2_89 | spl2_2),
% 13.37/2.24 inference(avatar_split_clause,[],[f5843,f25,f5849,f5846])).
% 13.37/2.24 tff(f5868,plain,(
% 13.37/2.24 ( ! [X0 : $int] : ($less($sum(sK0,X0),$sum(3,sK1)) | ~$less(sK0,$sum(sK0,X0)) | ~$less(X0,5)) )),
% 13.37/2.24 inference(resolution,[],[f55,f126])).
% 13.37/2.24 tff(f5895,plain,(
% 13.37/2.24 ~$less(sK0,sK1) | ~$less(sK0,$sum(sK0,1)) | ~$less(1,5)),
% 13.37/2.24 inference(resolution,[],[f70,f126])).
% 13.37/2.24 tff(f5907,plain,(
% 13.37/2.24 ~$less(sK0,sK1) | ~$less(sK0,$sum(sK0,1))),
% 13.37/2.24 inference(evaluation,[],[f5895])).
% 13.37/2.24 tff(f8302,plain,(
% 13.37/2.24 ~$less(sK1,sK0) | ~$less(sK0,$sum(sK0,3)) | ~$less(3,5)),
% 13.37/2.24 inference(resolution,[],[f554,f5868])).
% 13.37/2.24 tff(f8353,plain,(
% 13.37/2.24 ~$less(sK1,sK0) | ~$less(sK0,$sum(sK0,3))),
% 13.37/2.24 inference(evaluation,[],[f8302])).
% 13.37/2.24 tff(f8362,plain,(
% 13.37/2.24 ~$less(sK0,$sum(sK0,3)) | ~spl2_16),
% 13.37/2.24 inference(forward_subsumption_resolution,[],[f8353,f1801])).
% 13.37/2.24 tff(f8364,plain,(
% 13.37/2.24 ~$less(sK0,$sum(3,sK0)) | ~spl2_16),
% 13.37/2.24 inference(forward_demodulation,[],[f8362,f3])).
% 13.37/2.24 tff(f8365,plain,(
% 13.37/2.24 ~$less(0,3) | ~spl2_16),
% 13.37/2.24 inference(resolution,[],[f8364,f559])).
% 13.37/2.24 tff(f8368,plain,(
% 13.37/2.24 $false | ~spl2_16),
% 13.37/2.24 inference(evaluation,[],[f8365])).
% 13.37/2.24 tff(f8369,plain,(
% 13.37/2.24 ~spl2_16),
% 13.37/2.24 inference(avatar_contradiction_clause,[],[f8368])).
% 13.37/2.24 tff(f8383,plain,(
% 13.37/2.24 ~$less(sK0,sK1)),
% 13.37/2.24 inference(forward_subsumption_resolution,[],[f5907,f59])).
% 13.37/2.24 tff(f8404,plain,(
% 13.37/2.24 ~spl2_3),
% 13.37/2.24 inference(avatar_split_clause,[],[f8383,f29])).
% 13.37/2.24 tff(f8446,plain,(
% 13.37/2.24 $less(sK1,sK0) | sK0 = sK1 | spl2_3),
% 13.37/2.24 inference(resolution,[],[f30,f10])).
% 13.37/2.24 tff(f8448,plain,(
% 13.37/2.24 spl2_15 | spl2_16 | spl2_3),
% 13.37/2.24 inference(avatar_split_clause,[],[f8446,f29,f1800,f1797])).
% 13.37/2.24 tff(f8491,plain,(
% 13.37/2.24 $less($sum(5,sK1),$sum(3,sK1)) | (~spl2_15 | ~spl2_89)),
% 13.37/2.24 inference(forward_demodulation,[],[f5850,f1798])).
% 13.37/2.24 tff(f8589,plain,(
% 13.37/2.24 ~$less(3,5) | (~spl2_15 | ~spl2_89)),
% 13.37/2.24 inference(resolution,[],[f8491,f211])).
% 13.37/2.24 tff(f8598,plain,(
% 13.37/2.24 $false | (~spl2_15 | ~spl2_89)),
% 13.37/2.24 inference(evaluation,[],[f8589])).
% 13.37/2.24 tff(f8599,plain,(
% 13.37/2.24 ~spl2_15 | ~spl2_89),
% 13.37/2.24 inference(avatar_contradiction_clause,[],[f8598])).
% 13.37/2.24 tff(f8603,plain,(
% 13.37/2.24 $sum(3,sK1) = $sum(5,sK1) | (~spl2_15 | ~spl2_88)),
% 13.37/2.24 inference(forward_demodulation,[],[f5847,f1798])).
% 13.37/2.24 tff(f8621,plain,(
% 13.37/2.24 0 = $sum(5,$sum(sK1,$uminus($sum(3,sK1)))) | (~spl2_15 | ~spl2_88)),
% 13.37/2.24 inference(superposition,[],[f150,f8603])).
% 13.37/2.24 tff(f8674,plain,(
% 13.37/2.24 0 = $sum(5,$uminus(3)) | (~spl2_15 | ~spl2_88)),
% 13.37/2.24 inference(forward_demodulation,[],[f8621,f311])).
% 13.37/2.24 tff(f8675,plain,(
% 13.37/2.24 $false | (~spl2_15 | ~spl2_88)),
% 13.37/2.24 inference(evaluation,[],[f8674])).
% 13.37/2.24 tff(f8676,plain,(
% 13.37/2.24 ~spl2_15 | ~spl2_88),
% 13.37/2.24 inference(avatar_contradiction_clause,[],[f8675])).
% 13.37/2.24 cnf(s1, plain, ~spl2_1 | ~spl2_2, inference(sat_conversion,[],[f27])).
% 13.37/2.24 cnf(s105, plain, spl2_1 | spl2_16, inference(sat_conversion,[],[f4642])).
% 13.37/2.24 cnf(s192, plain, spl2_2 | spl2_88 | spl2_89, inference(sat_conversion,[],[f5851])).
% 13.37/2.24 cnf(s339, plain, ~spl2_16, inference(sat_conversion,[],[f8369])).
% 13.37/2.24 cnf(s344, plain, ~spl2_3, inference(sat_conversion,[],[f8404])).
% 13.37/2.24 cnf(s353, plain, spl2_3 | spl2_15 | spl2_16, inference(sat_conversion,[],[f8448])).
% 13.37/2.24 cnf(s367, plain, ~spl2_15 | ~spl2_89, inference(sat_conversion,[],[f8599])).
% 13.37/2.24 cnf(s372, plain, ~spl2_15 | ~spl2_88, inference(sat_conversion,[],[f8676])).
% 13.37/2.24 cnf(s375, plain, spl2_15, inference(rat,[],[s353,s344,s339])).
% 13.37/2.24 cnf(s376, plain, ~spl2_88, inference(rat,[],[s372,s375])).
% 13.37/2.24 cnf(s377, plain, ~spl2_89, inference(rat,[],[s367,s375])).
% 13.37/2.24 cnf(s384, plain, spl2_2, inference(rat,[],[s192,s377,s376])).
% 13.37/2.24 cnf(s393, plain, spl2_1, inference(rat,[],[s105,s339])).
% 13.37/2.24 cnf(s417, plain, $false, inference(rat,[],[s1,s384,s393])).
% 13.37/2.24 tff(f8684,plain,(
% 13.37/2.24 $false),
% 13.37/2.24 inference(avatar_sat_refutation,[],[s417])).
% 13.37/2.24 % SZS output end Proof for theBenchmark
% 13.37/2.24 % (2173653)------------------------------
% 13.37/2.24 % (2173653)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.37/2.24 % (2173653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.37/2.24 % (2173653)CaDiCaL version: 2.1.3
% 13.37/2.24 % (2173653)Termination reason: Refutation
% 13.37/2.24 % (2173653)Time elapsed: 0.349 s
% 13.37/2.24 % (2173653)Peak memory usage: 15 MB
% 13.37/2.24 % (2173653)Instructions burned: 339 (million)
% 13.37/2.24 % (2173594)Success in time 1.906 s
% 13.37/2.24 % Vampire exiting
%------------------------------------------------------------------------------