%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : DAT051_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:48:02 AM UTC 2026
% Result : Theorem 15.14s 2.48s
% Output : Refutation 15.14s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : DAT051_1 : TPTP v9.3.1. Released v5.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.21 % Computer : n015.cluster.edu
% 0.08/0.21 % Model : x86_64 x86_64
% 0.08/0.21 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.21 % Memory : 8046.5625MB
% 0.08/0.21 % OS : Linux 6.8.0-71-generic
% 0.08/0.21 % CPULimit : 300
% 0.08/0.21 % WCLimit : 300
% 0.08/0.21 % DateTime : Tue Sep 29 00:10:34 UTC 2026
% 0.08/0.21 % CPUTime :
% 0.08/0.21 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.24 Running first-order model finding
% 0.08/0.24 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
% 4.40/0.98 % (3166285)Will run a generic schedule for satisfiability detection.
% 4.40/0.98 % (3166295)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1419839752:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 4.40/0.98 % (3166297)dis+10_1_sil=32000:sp=arity:random_seed=3583068334:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 4.40/0.98 % (3166303)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1651146608:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 4.40/0.98 % (3166293)% WARNING: option uhcvi not known.
% 4.40/0.98 % (3166293)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1612137385:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 4.40/0.98 % (3166301)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1466667999:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 4.40/0.98 % (3166291)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=47861938_2999 on theBenchmark for (2999ds/0Mi)
% 4.40/0.98 % (3166299)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1980823749:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 4.40/0.98 % (3166291)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 4.40/0.98 % (3166291)Terminated due to inappropriate strategy.
% 4.40/0.98 % (3166291)------------------------------
% 4.40/0.98 % (3166291)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.40/0.98 % (3166291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.40/0.98 % (3166291)CaDiCaL version: 2.1.3
% 4.40/0.98 % (3166291)Termination reason: Inappropriate
% 4.40/0.98 % (3166291)Time elapsed: 0.002 s
% 4.40/0.98 % (3166291)Peak memory usage: 11 MB
% 4.40/0.98 % (3166291)Instructions burned: 1 (million)
% 4.40/0.98 % (3166291)------------------------------
% 4.40/0.98 % (3166291)------------------------------
% 4.40/0.98 % (3166320)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=33545169:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 4.40/0.98 % (3166320)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 4.40/0.98 % (3166320)Terminated due to inappropriate strategy.
% 4.40/0.99 % (3166320)------------------------------
% 4.40/0.99 % (3166320)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.40/0.99 % (3166320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.40/0.99 % (3166320)CaDiCaL version: 2.1.3
% 4.40/0.99 % (3166320)Termination reason: Inappropriate
% 4.40/0.99 % (3166320)Time elapsed: 0.001 s
% 4.40/0.99 % (3166320)Peak memory usage: 10 MB
% 4.40/0.99 % (3166320)Instructions burned: 1 (million)
% 4.40/0.99 % (3166320)------------------------------
% 4.40/0.99 % (3166320)------------------------------
% 4.40/0.99 % (3166325)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=768818773:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 4.40/0.99 % (3166297)Instruction limit reached!
% 4.40/0.99 % (3166297)------------------------------
% 4.40/0.99 % (3166297)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.40/0.99 % (3166297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.40/0.99 % (3166297)CaDiCaL version: 2.1.3
% 4.40/0.99 % (3166297)Termination reason: Instruction limit
% 4.40/0.99 % (3166297)Termination phase: Saturation
% 4.40/0.99 % (3166297)Time elapsed: 0.106 s
% 4.40/0.99 % (3166297)Peak memory usage: 13 MB
% 4.40/0.99 % (3166297)Instructions burned: 103 (million)
% 4.40/0.99 % (3166330)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=640411705:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 4.40/0.99 % (3166299)Instruction limit reached!
% 4.40/0.99 % (3166299)------------------------------
% 4.40/0.99 % (3166299)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.40/0.99 % (3166299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.40/0.99 % (3166299)CaDiCaL version: 2.1.3
% 4.40/0.99 % (3166299)Termination reason: Instruction limit
% 4.40/0.99 % (3166299)Termination phase: Saturation
% 4.40/0.99 % (3166299)Time elapsed: 0.115 s
% 4.40/0.99 % (3166299)Peak memory usage: 13 MB
% 4.40/0.99 % (3166299)Instructions burned: 117 (million)
% 4.40/0.99 % (3166301)Instruction limit reached!
% 4.40/0.99 % (3166301)------------------------------
% 4.40/0.99 % (3166301)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.34/1.24 % (3166301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.34/1.24 % (3166301)CaDiCaL version: 2.1.3
% 6.34/1.24 % (3166301)Termination reason: Instruction limit
% 6.34/1.24 % (3166301)Termination phase: Saturation
% 6.34/1.24 % (3166301)Time elapsed: 0.135 s
% 6.34/1.24 % (3166301)Peak memory usage: 13 MB
% 6.34/1.24 % (3166301)Instructions burned: 131 (million)
% 6.34/1.24 % (3166334)ott-21_1_sil=16000:fs=off:random_seed=762863596:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 6.34/1.24 % (3166303)Instruction limit reached!
% 6.34/1.24 % (3166303)------------------------------
% 6.34/1.24 % (3166303)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.34/1.24 % (3166303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.34/1.24 % (3166303)CaDiCaL version: 2.1.3
% 6.34/1.24 % (3166303)Termination reason: Instruction limit
% 6.34/1.24 % (3166303)Termination phase: Saturation
% 6.34/1.24 % (3166303)Time elapsed: 0.180 s
% 6.34/1.24 % (3166303)Peak memory usage: 13 MB
% 6.34/1.24 % (3166303)Instructions burned: 159 (million)
% 6.34/1.24 % (3166341)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1048641500:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 6.34/1.24 % (3166335)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=944434239:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 6.34/1.24 % (3166341)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 6.34/1.24 % (3166341)Terminated due to inappropriate strategy.
% 6.34/1.24 % (3166341)------------------------------
% 6.34/1.24 % (3166341)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.34/1.24 % (3166341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.34/1.24 % (3166341)CaDiCaL version: 2.1.3
% 6.34/1.24 % (3166341)Termination reason: Inappropriate
% 6.34/1.24 % (3166341)Time elapsed: 0.001 s
% 6.34/1.24 % (3166341)Peak memory usage: 10 MB
% 6.34/1.24 % (3166341)Instructions burned: 1 (million)
% 6.34/1.24 % (3166341)------------------------------
% 6.34/1.24 % (3166341)------------------------------
% 6.34/1.24 % (3166325)Instruction limit reached!
% 6.34/1.24 % (3166325)------------------------------
% 6.34/1.24 % (3166325)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.34/1.24 % (3166325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.34/1.24 % (3166325)CaDiCaL version: 2.1.3
% 6.34/1.24 % (3166325)Termination reason: Instruction limit
% 6.34/1.24 % (3166325)Termination phase: Saturation
% 6.34/1.24 % (3166325)Time elapsed: 0.147 s
% 6.34/1.24 % (3166325)Peak memory usage: 13 MB
% 6.34/1.24 % (3166325)Instructions burned: 131 (million)
% 6.34/1.24 % (3166346)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=73614910:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 6.34/1.24 % (3166348)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3379797765:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi)
% 6.34/1.24 % (3166348)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 6.34/1.24 % (3166348)Terminated due to inappropriate strategy.
% 6.34/1.24 % (3166348)------------------------------
% 6.34/1.24 % (3166348)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.34/1.24 % (3166348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.34/1.24 % (3166348)CaDiCaL version: 2.1.3
% 6.34/1.24 % (3166348)Termination reason: Inappropriate
% 6.34/1.24 % (3166348)Time elapsed: 0.001 s
% 6.34/1.24 % (3166348)Peak memory usage: 10 MB
% 6.34/1.24 % (3166348)Instructions burned: 1 (million)
% 6.34/1.24 % (3166348)------------------------------
% 6.34/1.24 % (3166348)------------------------------
% 6.34/1.24 % (3166334)Instruction limit reached!
% 6.34/1.24 % (3166334)------------------------------
% 6.34/1.24 % (3166334)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.34/1.24 % (3166334)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.34/1.24 % (3166334)CaDiCaL version: 2.1.3
% 6.34/1.24 % (3166334)Termination reason: Instruction limit
% 6.34/1.24 % (3166334)Termination phase: Saturation
% 6.34/1.24 % (3166334)Time elapsed: 0.095 s
% 6.34/1.24 % (3166334)Peak memory usage: 12 MB
% 6.34/1.24 % (3166334)Instructions burned: 182 (million)
% 6.34/1.24 % (3166351)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=3268331803:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2996 on theBenchmark for (2996ds/692Mi)
% 15.14/2.48 % (3166352)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3922689802:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi)
% 15.14/2.48 % (3166330)Instruction limit reached!
% 15.14/2.48 % (3166330)------------------------------
% 15.14/2.48 % (3166330)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.14/2.48 % (3166330)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.14/2.48 % (3166330)CaDiCaL version: 2.1.3
% 15.14/2.48 % (3166330)Termination reason: Instruction limit
% 15.14/2.48 % (3166330)Termination phase: Saturation
% 15.14/2.48 % (3166330)Time elapsed: 0.349 s
% 15.14/2.48 % (3166330)Peak memory usage: 14 MB
% 15.14/2.48 % (3166330)Instructions burned: 685 (million)
% 15.14/2.48 % (3166398)fmb+10_1_sil=64000:random_seed=583407052:i=22061:nm=2:gsp=on_2994 on theBenchmark for (2994ds/22061Mi)
% 15.14/2.48 % (3166398)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 15.14/2.48 % (3166398)Terminated due to inappropriate strategy.
% 15.14/2.48 % (3166398)------------------------------
% 15.14/2.48 % (3166398)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.14/2.48 % (3166398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.14/2.48 % (3166398)CaDiCaL version: 2.1.3
% 15.14/2.48 % (3166398)Termination reason: Inappropriate
% 15.14/2.48 % (3166398)Time elapsed: 0.001 s
% 15.14/2.48 % (3166398)Peak memory usage: 10 MB
% 15.14/2.48 % (3166398)Instructions burned: 1 (million)
% 15.14/2.48 % (3166398)------------------------------
% 15.14/2.48 % (3166398)------------------------------
% 15.14/2.48 % (3166403)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=68307490:i=9515:nm=5_2994 on theBenchmark for (2994ds/9515Mi)
% 15.14/2.48 % (3166403)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 15.14/2.48 % (3166403)Terminated due to inappropriate strategy.
% 15.14/2.48 % (3166403)------------------------------
% 15.14/2.48 % (3166403)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.14/2.48 % (3166403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.14/2.48 % (3166403)CaDiCaL version: 2.1.3
% 15.14/2.48 % (3166403)Termination reason: Inappropriate
% 15.14/2.48 % (3166403)Time elapsed: 0.001 s
% 15.14/2.48 % (3166403)Peak memory usage: 10 MB
% 15.14/2.48 % (3166403)Instructions burned: 1 (million)
% 15.14/2.48 % (3166403)------------------------------
% 15.14/2.48 % (3166403)------------------------------
% 15.14/2.48 % (3166410)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=503094903:fmbsr=1.7:i=920_2994 on theBenchmark for (2994ds/920Mi)
% 15.14/2.48 % (3166335)Instruction limit reached!
% 15.14/2.48 % (3166335)------------------------------
% 15.14/2.48 % (3166335)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.14/2.48 % (3166335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.14/2.48 % (3166335)CaDiCaL version: 2.1.3
% 15.14/2.48 % (3166335)Termination reason: Instruction limit
% 15.14/2.48 % (3166335)Termination phase: Saturation
% 15.14/2.48 % (3166335)Time elapsed: 0.330 s
% 15.14/2.48 % (3166335)Peak memory usage: 14 MB
% 15.14/2.48 % (3166335)Instructions burned: 477 (million)
% 15.14/2.48 % (3166410)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 15.14/2.48 % (3166410)Terminated due to inappropriate strategy.
% 15.14/2.48 % (3166410)------------------------------
% 15.14/2.48 % (3166410)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.14/2.48 % (3166410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.14/2.48 % (3166410)CaDiCaL version: 2.1.3
% 15.14/2.48 % (3166410)Termination reason: Inappropriate
% 15.14/2.48 % (3166410)Time elapsed: 0.001 s
% 15.14/2.48 % (3166410)Peak memory usage: 10 MB
% 15.14/2.48 % (3166410)Instructions burned: 1 (million)
% 15.14/2.48 % (3166410)------------------------------
% 15.14/2.48 % (3166410)------------------------------
% 15.14/2.48 % (3166416)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2856780765:i=5131_2994 on theBenchmark for (2994ds/5131Mi)
% 15.14/2.48 % (3166418)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3408481870:i=1472:ins=7:fdi=8:gsp=on_2994 on theBenchmark for (2994ds/1472Mi)
% 15.14/2.48 % (3166351)Instruction limit reached!
% 15.14/2.48 % (3166351)------------------------------
% 15.14/2.48 % (3166351)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.14/2.48 % (3166351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.14/2.48 % (3166351)CaDiCaL version: 2.1.3
% 15.14/2.48 % (3166351)Termination reason: Instruction limit
% 15.14/2.48 % (3166351)Termination phase: Saturation
% 15.14/2.48 % (3166351)Time elapsed: 0.411 s
% 15.14/2.48 % (3166351)Peak memory usage: 18 MB
% 15.14/2.48 % (3166351)Instructions burned: 692 (million)
% 15.14/2.48 % (3166446)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2868179890:i=6324_2992 on theBenchmark for (2992ds/6324Mi)
% 15.14/2.48 % (3166446)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 15.14/2.48 % (3166446)Terminated due to inappropriate strategy.
% 15.14/2.48 % (3166446)------------------------------
% 15.14/2.48 % (3166446)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.14/2.48 % (3166446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.14/2.48 % (3166446)CaDiCaL version: 2.1.3
% 15.14/2.48 % (3166446)Termination reason: Inappropriate
% 15.14/2.48 % (3166446)Time elapsed: 0.001 s
% 15.14/2.48 % (3166446)Peak memory usage: 10 MB
% 15.14/2.48 % (3166446)Instructions burned: 1 (million)
% 15.14/2.48 % (3166446)------------------------------
% 15.14/2.48 % (3166446)------------------------------
% 15.14/2.48 % (3166452)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=194401753:fmbsr=2.30978:i=2174_2992 on theBenchmark for (2992ds/2174Mi)
% 15.14/2.48 % (3166452)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 15.14/2.48 % (3166452)Terminated due to inappropriate strategy.
% 15.14/2.48 % (3166452)------------------------------
% 15.14/2.48 % (3166452)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.14/2.48 % (3166452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.14/2.48 % (3166452)CaDiCaL version: 2.1.3
% 15.14/2.48 % (3166452)Termination reason: Inappropriate
% 15.14/2.48 % (3166452)Time elapsed: 0.001 s
% 15.14/2.48 % (3166452)Peak memory usage: 10 MB
% 15.14/2.48 % (3166452)Instructions burned: 1 (million)
% 15.14/2.48 % (3166452)------------------------------
% 15.14/2.48 % (3166452)------------------------------
% 15.14/2.48 % (3166459)ott-2_1_sil=16000:newcnf=on:random_seed=1243482825:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2992 on theBenchmark for (2992ds/869Mi)
% 15.14/2.48 % (3166352)Instruction limit reached!
% 15.14/2.48 % (3166352)------------------------------
% 15.14/2.48 % (3166352)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.14/2.48 % (3166352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.14/2.48 % (3166352)CaDiCaL version: 2.1.3
% 15.14/2.48 % (3166352)Termination reason: Instruction limit
% 15.14/2.48 % (3166352)Termination phase: Saturation
% 15.14/2.48 % (3166352)Time elapsed: 0.502 s
% 15.14/2.48 % (3166352)Peak memory usage: 22 MB
% 15.14/2.48 % (3166352)Instructions burned: 880 (million)
% 15.14/2.48 % (3166466)ott+10_1_sil=32000:tgt=ground:random_seed=108007045:i=5114:av=off_2991 on theBenchmark for (2991ds/5114Mi)
% 15.14/2.48 % (3166346)Instruction limit reached!
% 15.14/2.48 % (3166346)------------------------------
% 15.14/2.48 % (3166346)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.14/2.48 % (3166346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.14/2.48 % (3166346)CaDiCaL version: 2.1.3
% 15.14/2.48 % (3166346)Termination reason: Instruction limit
% 15.14/2.48 % (3166346)Termination phase: Saturation
% 15.14/2.48 % (3166346)Time elapsed: 0.670 s
% 15.14/2.48 % (3166346)Peak memory usage: 18 MB
% 15.14/2.48 % (3166346)Instructions burned: 1180 (million)
% 15.14/2.48 % (3166478)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=4179660060:i=54282_2990 on theBenchmark for (2990ds/54282Mi)
% 15.14/2.48 % (3166478)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 15.14/2.48 % (3166478)Terminated due to inappropriate strategy.
% 15.14/2.48 % (3166478)------------------------------
% 15.14/2.48 % (3166478)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.14/2.48 % (3166478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.14/2.48 % (3166478)CaDiCaL version: 2.1.3
% 15.14/2.48 % (3166478)Termination reason: Inappropriate
% 15.14/2.48 % (3166478)Time elapsed: 0.001 s
% 15.14/2.48 % (3166478)Peak memory usage: 10 MB
% 15.14/2.48 % (3166478)Instructions burned: 1 (million)
% 15.14/2.48 % (3166478)------------------------------
% 15.14/2.48 % (3166478)------------------------------
% 15.14/2.48 % (3166480)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=796773581:i=3512:aac=none_2990 on theBenchmark for (2990ds/3512Mi)
% 15.14/2.48 % (3166459)Instruction limit reached!
% 15.14/2.48 % (3166459)------------------------------
% 15.14/2.48 % (3166459)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.14/2.48 % (3166459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.14/2.48 % (3166459)CaDiCaL version: 2.1.3
% 15.14/2.48 % (3166459)Termination reason: Instruction limit
% 15.14/2.48 % (3166459)Termination phase: Saturation
% 15.14/2.48 % (3166459)Time elapsed: 0.504 s
% 15.14/2.48 % (3166459)Peak memory usage: 16 MB
% 15.14/2.48 % (3166459)Instructions burned: 869 (million)
% 15.14/2.48 % (3166526)dis+21_1_sil=32000:sas=cadical:random_seed=1497539095:i=3773:amm=off_2986 on theBenchmark for (2986ds/3773Mi)
% 15.14/2.48 % (3166418)Instruction limit reached!
% 15.14/2.48 % (3166418)------------------------------
% 15.14/2.48 % (3166418)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.14/2.48 % (3166418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.14/2.48 % (3166418)CaDiCaL version: 2.1.3
% 15.14/2.48 % (3166418)Termination reason: Instruction limit
% 15.14/2.48 % (3166418)Termination phase: Saturation
% 15.14/2.48 % (3166418)Time elapsed: 0.915 s
% 15.14/2.48 % (3166418)Peak memory usage: 25 MB
% 15.14/2.48 % (3166418)Instructions burned: 1472 (million)
% 15.14/2.48 % (3166531)ott+11_1_sil=16000:gs=on:random_seed=1811509985:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2984 on theBenchmark for (2984ds/2251Mi)
% 15.14/2.48 % (3166416) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3166285-3166416"...
% 15.14/2.48 % (3166416)...printing done.
% 15.14/2.48 % (3166416)Refutation found. Thanks to Tanya!
% 15.14/2.48 % SZS status Theorem for theBenchmark
% 15.14/2.48 % SZS output start Proof for theBenchmark
% 15.14/2.48 tff(type_def_5, type, record: $tType).
% 15.14/2.48 tff(func_def_0, type, length: record > $int).
% 15.14/2.48 tff(func_def_1, type, next: record > record).
% 15.14/2.48 tff(func_def_2, type, data: record > $int).
% 15.14/2.48 tff(func_def_3, type, split1: record > record).
% 15.14/2.48 tff(func_def_4, type, split2: record > record).
% 15.14/2.48 tff(func_def_12, type, sK0: record).
% 15.14/2.48 tff(func_def_13, type, sK1: record).
% 15.14/2.48 tff(pred_def_1, type, isrecord: record > $o).
% 15.14/2.48 tff(f3,axiom,(
% 15.14/2.48 ! [X0 : record] : (isrecord(X0) => length(X0) = $sum(length(next(X0)),1))),
% 15.14/2.48 file('/export/starexec/sandbox2/benchmark/Axioms/DAT003_0.ax',ax3)).
% 15.14/2.48 tff(f11,axiom,(
% 15.14/2.48 ! [X0 : record] : ((isrecord(X0) & isrecord(next(X0))) => isrecord(split2(X0)))),
% 15.14/2.48 file('/export/starexec/sandbox2/benchmark/Axioms/DAT003_0.ax',ax11)).
% 15.14/2.48 tff(f13,axiom,(
% 15.14/2.48 ! [X0 : record] : ((isrecord(X0) & isrecord(next(X0))) => next(split2(X0)) = split2(next(next(X0))))),
% 15.14/2.48 file('/export/starexec/sandbox2/benchmark/Axioms/DAT003_0.ax',ax13)).
% 15.14/2.48 tff(f14,conjecture,(
% 15.14/2.48 ! [X0 : record,X1 : record] : ((isrecord(X0) & isrecord(next(X0)) & X1 = next(next(X0)) & ($product(2,length(split2(X1))) = $difference(length(X1),1) | $product(2,length(split2(X1))) = length(X1))) => ($product(2,length(split2(X0))) = $difference(length(X0),1) | $product(2,length(split2(X0))) = length(X0)))),
% 15.14/2.48 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1)).
% 15.14/2.48 tff(f15,negated_conjecture,(
% 15.14/2.48 ~ ! [X0 : record,X1 : record] : ((isrecord(X0) & isrecord(next(X0)) & X1 = next(next(X0)) & ($product(2,length(split2(X1))) = $difference(length(X1),1) | $product(2,length(split2(X1))) = length(X1))) => ($product(2,length(split2(X0))) = $difference(length(X0),1) | $product(2,length(split2(X0))) = length(X0)))),
% 15.14/2.48 inference(negated_conjecture,[status(cth)],[f14])).
% 15.14/2.48 tff(f17,plain,(
% 15.14/2.48 ~ ! [X0 : record,X1 : record] : ((isrecord(X0) & isrecord(next(X0)) & X1 = next(next(X0)) & ($product(2,length(split2(X1))) = $sum(length(X1),$uminus(1)) | $product(2,length(split2(X1))) = length(X1))) => ($product(2,length(split2(X0))) = $sum(length(X0),$uminus(1)) | $product(2,length(split2(X0))) = length(X0)))),
% 15.14/2.48 inference(theory_normalization,[],[f15])).
% 15.14/2.48 tff(f18,definition,(
% 15.14/2.48 ( ! [X0 : $int,X1 : $int] : ($sum(X0,X1) = $sum(X1,X0)) )),
% 15.14/2.48 introduced(theory,[tha_commutativity])).
% 15.14/2.48 tff(f19,definition,(
% 15.14/2.48 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($sum(X0,$sum(X1,X2)) = $sum($sum(X0,X1),X2)) )),
% 15.14/2.48 introduced(theory,[tha_associativity])).
% 15.14/2.48 tff(f22,definition,(
% 15.14/2.48 ( ! [X0 : $int] : (0 = $sum(X0,$uminus(X0))) )),
% 15.14/2.48 introduced(theory,[tha_inverse_op_unit])).
% 15.14/2.48 tff(f31,definition,(
% 15.14/2.48 ( ! [X0 : $int] : ($product(X0,1) = X0) )),
% 15.14/2.48 introduced(theory,[tha_right_identity])).
% 15.14/2.48 tff(f33,definition,(
% 15.14/2.48 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($product(X0,$sum(X1,X2)) = $sum($product(X0,X1),$product(X0,X2))) )),
% 15.14/2.48 introduced(theory,[tha_distributivity])).
% 15.14/2.48 tff(f38,plain,(
% 15.14/2.48 ! [X0 : record] : (length(X0) = $sum(length(next(X0)),1) | ~isrecord(X0))),
% 15.14/2.48 inference(ennf_transformation,[],[f3])).
% 15.14/2.48 tff(f48,plain,(
% 15.14/2.48 ! [X0 : record] : (isrecord(split2(X0)) | (~isrecord(X0) | ~isrecord(next(X0))))),
% 15.14/2.48 inference(ennf_transformation,[],[f11])).
% 15.14/2.48 tff(f49,plain,(
% 15.14/2.48 ! [X0 : record] : (isrecord(split2(X0)) | ~isrecord(X0) | ~isrecord(next(X0)))),
% 15.14/2.48 inference(flattening,[],[f48])).
% 15.14/2.48 tff(f52,plain,(
% 15.14/2.48 ! [X0 : record] : (next(split2(X0)) = split2(next(next(X0))) | (~isrecord(X0) | ~isrecord(next(X0))))),
% 15.14/2.48 inference(ennf_transformation,[],[f13])).
% 15.14/2.48 tff(f53,plain,(
% 15.14/2.48 ! [X0 : record] : (next(split2(X0)) = split2(next(next(X0))) | ~isrecord(X0) | ~isrecord(next(X0)))),
% 15.14/2.48 inference(flattening,[],[f52])).
% 15.14/2.48 tff(f54,plain,(
% 15.14/2.48 ? [X0 : record,X1 : record] : (($product(2,length(split2(X0))) != $sum(length(X0),$uminus(1)) & length(X0) != $product(2,length(split2(X0)))) & (isrecord(X0) & isrecord(next(X0)) & X1 = next(next(X0)) & ($product(2,length(split2(X1))) = $sum(length(X1),$uminus(1)) | $product(2,length(split2(X1))) = length(X1))))),
% 15.14/2.48 inference(ennf_transformation,[],[f17])).
% 15.14/2.48 tff(f55,plain,(
% 15.14/2.48 ? [X0 : record,X1 : record] : ($product(2,length(split2(X0))) != $sum(length(X0),$uminus(1)) & length(X0) != $product(2,length(split2(X0))) & isrecord(X0) & isrecord(next(X0)) & X1 = next(next(X0)) & ($product(2,length(split2(X1))) = $sum(length(X1),$uminus(1)) | $product(2,length(split2(X1))) = length(X1)))),
% 15.14/2.48 inference(flattening,[],[f54])).
% 15.14/2.48 tff(f58,plain,(
% 15.14/2.48 ( ! [X0 : record] : (~isrecord(X0) | length(X0) = $sum(length(next(X0)),1)) )),
% 15.14/2.48 inference(cnf_transformation,[],[f38])).
% 15.14/2.48 tff(f66,plain,(
% 15.14/2.48 ( ! [X0 : record] : (isrecord(split2(X0)) | ~isrecord(X0) | ~isrecord(next(X0))) )),
% 15.14/2.48 inference(cnf_transformation,[],[f49])).
% 15.14/2.48 tff(f68,plain,(
% 15.14/2.48 ( ! [X0 : record] : (~isrecord(next(X0)) | ~isrecord(X0) | next(split2(X0)) = split2(next(next(X0)))) )),
% 15.14/2.48 inference(cnf_transformation,[],[f53])).
% 15.14/2.48 tff(f69,plain,(
% 15.14/2.48 $product(2,length(split2(sK1))) = length(sK1) | $product(2,length(split2(sK1))) = $sum(length(sK1),$uminus(1))),
% 15.14/2.48 inference(cnf_transformation,[],[f55])).
% 15.14/2.48 tff(f70,plain,(
% 15.14/2.48 sK1 = next(next(sK0))),
% 15.14/2.48 inference(cnf_transformation,[],[f55])).
% 15.14/2.48 tff(f71,plain,(
% 15.14/2.48 isrecord(next(sK0))),
% 15.14/2.48 inference(cnf_transformation,[],[f55])).
% 15.14/2.48 tff(f72,plain,(
% 15.14/2.48 isrecord(sK0)),
% 15.14/2.48 inference(cnf_transformation,[],[f55])).
% 15.14/2.48 tff(f73,plain,(
% 15.14/2.48 length(sK0) != $product(2,length(split2(sK0)))),
% 15.14/2.48 inference(cnf_transformation,[],[f55])).
% 15.14/2.48 tff(f74,plain,(
% 15.14/2.48 $product(2,length(split2(sK0))) != $sum(length(sK0),$uminus(1))),
% 15.14/2.48 inference(cnf_transformation,[],[f55])).
% 15.14/2.48 tff(f76,plain,(
% 15.14/2.48 $product(2,length(split2(sK1))) = length(sK1) | $product(2,length(split2(sK1))) = $sum(length(sK1),-1)),
% 15.14/2.48 inference(evaluation,[],[f69])).
% 15.14/2.48 tff(f77,plain,(
% 15.14/2.48 $product(2,length(split2(sK0))) != $sum(length(sK0),-1)),
% 15.14/2.48 inference(evaluation,[],[f74])).
% 15.14/2.48 tff(f79,definition,(
% 15.14/2.48 spl2_1 <=> $product(2,length(split2(sK1))) = $sum(length(sK1),-1)),
% 15.14/2.48 introduced(definition,[new_symbols(definition,[spl2_1])],[avatar_definition])).
% 15.14/2.48 tff(f81,plain,(
% 15.14/2.48 $product(2,length(split2(sK1))) = $sum(length(sK1),-1) | ~spl2_1),
% 15.14/2.48 inference(avatar_component_clause,[],[f79])).
% 15.14/2.48 tff(f83,definition,(
% 15.14/2.48 spl2_2 <=> $product(2,length(split2(sK1))) = length(sK1)),
% 15.14/2.48 introduced(definition,[new_symbols(definition,[spl2_2])],[avatar_definition])).
% 15.14/2.48 tff(f85,plain,(
% 15.14/2.48 $product(2,length(split2(sK1))) = length(sK1) | ~spl2_2),
% 15.14/2.48 inference(avatar_component_clause,[],[f83])).
% 15.14/2.48 tff(f86,plain,(
% 15.14/2.48 spl2_1 | spl2_2),
% 15.14/2.48 inference(avatar_split_clause,[],[f76,f83,f79])).
% 15.14/2.48 tff(f184,plain,(
% 15.14/2.48 ( ! [X0 : record] : (~isrecord(X0) | length(X0) = $sum(1,length(next(X0)))) )),
% 15.14/2.48 inference(forward_demodulation,[],[f58,f18])).
% 15.14/2.48 tff(f191,plain,(
% 15.14/2.48 length(next(sK0)) = $sum(1,length(next(next(sK0))))),
% 15.14/2.48 inference(resolution,[],[f184,f71])).
% 15.14/2.48 tff(f194,plain,(
% 15.14/2.48 ( ! [X0 : record] : (~isrecord(next(X0)) | ~isrecord(X0) | length(split2(X0)) = $sum(1,length(next(split2(X0))))) )),
% 15.14/2.48 inference(resolution,[],[f184,f66])).
% 15.14/2.48 tff(f195,plain,(
% 15.14/2.48 length(sK0) = $sum(1,length(next(sK0)))),
% 15.14/2.48 inference(resolution,[],[f184,f72])).
% 15.14/2.48 tff(f196,plain,(
% 15.14/2.48 length(next(sK0)) = $sum(1,length(sK1))),
% 15.14/2.48 inference(forward_demodulation,[],[f191,f70])).
% 15.14/2.48 tff(f202,plain,(
% 15.14/2.48 ( ! [X0 : $int,X1 : $int] : ($sum(0,X1) = $sum(X0,$sum($uminus(X0),X1))) )),
% 15.14/2.48 inference(superposition,[],[f19,f22])).
% 15.14/2.48 tff(f209,plain,(
% 15.14/2.48 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($sum(X0,$sum(X1,X2)) = $sum(X1,$sum(X2,X0))) )),
% 15.14/2.48 inference(superposition,[],[f19,f18])).
% 15.14/2.48 tff(f220,plain,(
% 15.14/2.48 ( ! [X0 : $int,X1 : $int] : ($sum(X0,$sum($uminus(X0),X1)) = X1) )),
% 15.14/2.48 inference(evaluation,[],[f202])).
% 15.14/2.48 tff(f293,plain,(
% 15.14/2.48 ~isrecord(sK0) | next(split2(sK0)) = split2(next(next(sK0)))),
% 15.14/2.48 inference(resolution,[],[f68,f71])).
% 15.14/2.48 tff(f298,plain,(
% 15.14/2.48 next(split2(sK0)) = split2(next(next(sK0)))),
% 15.14/2.48 inference(forward_subsumption_resolution,[],[f293,f72])).
% 15.14/2.48 tff(f299,plain,(
% 15.14/2.48 split2(sK1) = next(split2(sK0))),
% 15.14/2.48 inference(forward_demodulation,[],[f298,f70])).
% 15.14/2.48 tff(f963,plain,(
% 15.14/2.48 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($sum(X1,X0) = $sum(X2,$sum($sum($uminus(X2),X0),X1))) )),
% 15.14/2.48 inference(superposition,[],[f209,f220])).
% 15.14/2.48 tff(f1080,plain,(
% 15.14/2.48 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($sum(X1,X0) = $sum(X2,$sum($uminus(X2),$sum(X0,X1)))) )),
% 15.14/2.48 inference(forward_demodulation,[],[f963,f19])).
% 15.14/2.48 tff(f2453,plain,(
% 15.14/2.48 ~isrecord(sK0) | length(split2(sK0)) = $sum(1,length(next(split2(sK0))))),
% 15.14/2.48 inference(resolution,[],[f194,f71])).
% 15.14/2.48 tff(f2463,plain,(
% 15.14/2.48 length(split2(sK0)) = $sum(1,length(next(split2(sK0))))),
% 15.14/2.48 inference(forward_subsumption_resolution,[],[f2453,f72])).
% 15.14/2.48 tff(f2464,plain,(
% 15.14/2.48 length(split2(sK0)) = $sum(1,length(split2(sK1)))),
% 15.14/2.48 inference(forward_demodulation,[],[f2463,f299])).
% 15.14/2.48 tff(f2494,plain,(
% 15.14/2.48 $product(2,length(split2(sK1))) = $sum(-1,length(sK1)) | ~spl2_1),
% 15.14/2.48 inference(forward_demodulation,[],[f81,f18])).
% 15.14/2.48 tff(f2500,plain,(
% 15.14/2.48 ( ! [X0 : $int] : ($product(2,$sum(length(split2(sK1)),X0)) = $sum($sum(-1,length(sK1)),$product(2,X0))) ) | ~spl2_1),
% 15.14/2.48 inference(superposition,[],[f33,f2494])).
% 15.14/2.48 tff(f2542,plain,(
% 15.14/2.48 ( ! [X0 : $int] : ($sum(1,$sum(length(next(sK0)),X0)) = $sum(X0,length(sK0))) )),
% 15.14/2.48 inference(superposition,[],[f209,f195])).
% 15.14/2.48 tff(f2608,plain,(
% 15.14/2.48 ( ! [X0 : $int] : ($sum(length(next(sK0)),X0) = $sum(1,$sum(length(sK1),X0))) )),
% 15.14/2.48 inference(superposition,[],[f19,f196])).
% 15.14/2.48 tff(f3577,plain,(
% 15.14/2.48 $product(2,$sum(length(split2(sK1)),1)) = $sum($sum(-1,length(sK1)),2) | ~spl2_1),
% 15.14/2.48 inference(superposition,[],[f2500,f31])).
% 15.14/2.48 tff(f3615,plain,(
% 15.14/2.48 $product(2,$sum(length(split2(sK1)),1)) = $sum(2,$sum(-1,length(sK1))) | ~spl2_1),
% 15.14/2.48 inference(forward_demodulation,[],[f3577,f18])).
% 15.14/2.48 tff(f3620,plain,(
% 15.14/2.48 $product(2,$sum(length(split2(sK1)),1)) = $sum(-1,$sum(length(sK1),2)) | ~spl2_1),
% 15.14/2.48 inference(forward_demodulation,[],[f3615,f209])).
% 15.14/2.48 tff(f3624,plain,(
% 15.14/2.48 $product(2,$sum(length(split2(sK1)),1)) = $sum(-1,$sum(2,length(sK1))) | ~spl2_1),
% 15.14/2.48 inference(forward_demodulation,[],[f3620,f18])).
% 15.14/2.48 tff(f3625,plain,(
% 15.14/2.48 $product(2,$sum(1,length(split2(sK1)))) = $sum(-1,$sum(2,length(sK1))) | ~spl2_1),
% 15.14/2.48 inference(forward_demodulation,[],[f3624,f18])).
% 15.14/2.48 tff(f4860,plain,(
% 15.14/2.48 $sum(1,0) = $sum(length(next(sK0)),$uminus(length(sK1)))),
% 15.14/2.48 inference(superposition,[],[f2608,f22])).
% 15.14/2.48 tff(f4898,plain,(
% 15.14/2.48 1 = $sum(length(next(sK0)),$uminus(length(sK1)))),
% 15.14/2.48 inference(evaluation,[],[f4860])).
% 15.14/2.48 tff(f5342,plain,(
% 15.14/2.48 $product(2,length(split2(sK0))) = $sum(-1,$sum(2,length(sK1))) | ~spl2_1),
% 15.14/2.48 inference(forward_demodulation,[],[f3625,f2464])).
% 15.14/2.48 tff(f14831,plain,(
% 15.14/2.48 $sum(1,1) = $sum($uminus(length(sK1)),length(sK0))),
% 15.14/2.48 inference(superposition,[],[f2542,f4898])).
% 15.14/2.48 tff(f14869,plain,(
% 15.14/2.48 2 = $sum($uminus(length(sK1)),length(sK0))),
% 15.14/2.48 inference(evaluation,[],[f14831])).
% 15.14/2.48 tff(f15239,plain,(
% 15.14/2.48 length(sK0) = $sum(length(sK1),2)),
% 15.14/2.48 inference(superposition,[],[f220,f14869])).
% 15.14/2.48 tff(f15537,plain,(
% 15.14/2.48 length(sK0) = $sum(2,length(sK1))),
% 15.14/2.48 inference(superposition,[],[f15239,f18])).
% 15.14/2.48 tff(f53290,plain,(
% 15.14/2.48 ( ! [X0 : $int] : ($sum($sum(2,length(sK1)),-1) = $sum(X0,$sum($uminus(X0),$product(2,length(split2(sK0)))))) ) | ~spl2_1),
% 15.14/2.48 inference(superposition,[],[f1080,f5342])).
% 15.14/2.48 tff(f53653,plain,(
% 15.14/2.48 $product(2,length(split2(sK0))) = $sum($sum(2,length(sK1)),-1) | ~spl2_1),
% 15.14/2.48 inference(forward_demodulation,[],[f53290,f220])).
% 15.14/2.48 tff(f53826,plain,(
% 15.14/2.48 $product(2,length(split2(sK0))) = $sum(length(sK0),-1) | ~spl2_1),
% 15.14/2.48 inference(forward_demodulation,[],[f53653,f15537])).
% 15.14/2.48 tff(f53874,plain,(
% 15.14/2.48 $false | ~spl2_1),
% 15.14/2.48 inference(forward_subsumption_resolution,[],[f53826,f77])).
% 15.14/2.48 tff(f53875,plain,(
% 15.14/2.48 ~spl2_1),
% 15.14/2.48 inference(avatar_contradiction_clause,[],[f53874])).
% 15.14/2.48 tff(f54008,plain,(
% 15.14/2.48 ( ! [X0 : $int] : ($product(2,$sum(X0,length(split2(sK1)))) = $sum($product(2,X0),length(sK1))) ) | ~spl2_2),
% 15.14/2.48 inference(superposition,[],[f33,f85])).
% 15.14/2.48 tff(f54057,plain,(
% 15.14/2.48 ( ! [X0 : $int] : ($sum(length(sK1),$product(2,X0)) = $product(2,$sum(X0,length(split2(sK1))))) ) | ~spl2_2),
% 15.14/2.48 inference(forward_demodulation,[],[f54008,f18])).
% 15.14/2.48 tff(f54512,plain,(
% 15.14/2.48 $product(2,length(split2(sK0))) = $sum(length(sK1),$product(2,1)) | ~spl2_2),
% 15.14/2.48 inference(superposition,[],[f54057,f2464])).
% 15.14/2.48 tff(f54593,plain,(
% 15.14/2.48 $product(2,length(split2(sK0))) = $sum(length(sK1),2) | ~spl2_2),
% 15.14/2.48 inference(evaluation,[],[f54512])).
% 15.14/2.48 tff(f54619,plain,(
% 15.14/2.48 $product(2,length(split2(sK0))) = $sum(2,length(sK1)) | ~spl2_2),
% 15.14/2.48 inference(forward_demodulation,[],[f54593,f18])).
% 15.14/2.48 tff(f54635,plain,(
% 15.14/2.48 length(sK0) = $product(2,length(split2(sK0))) | ~spl2_2),
% 15.14/2.48 inference(forward_demodulation,[],[f54619,f15537])).
% 15.14/2.48 tff(f54647,plain,(
% 15.14/2.48 $false | ~spl2_2),
% 15.14/2.48 inference(forward_subsumption_resolution,[],[f54635,f73])).
% 15.14/2.48 tff(f54648,plain,(
% 15.14/2.48 ~spl2_2),
% 15.14/2.48 inference(avatar_contradiction_clause,[],[f54647])).
% 15.14/2.48 cnf(s1, plain, spl2_1 | spl2_2, inference(sat_conversion,[],[f86])).
% 15.14/2.48 cnf(s52, plain, ~spl2_1, inference(sat_conversion,[],[f53875])).
% 15.14/2.48 cnf(s53, plain, ~spl2_2, inference(sat_conversion,[],[f54648])).
% 15.14/2.48 cnf(s78, plain, $false, inference(rat,[],[s1,s53,s52])).
% 15.14/2.48 tff(f54655,plain,(
% 15.14/2.48 $false),
% 15.14/2.48 inference(avatar_sat_refutation,[],[s78])).
% 15.14/2.48 % SZS output end Proof for theBenchmark
% 15.14/2.48 % (3166416)------------------------------
% 15.14/2.48 % (3166416)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.14/2.48 % (3166416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.14/2.48 % (3166416)CaDiCaL version: 2.1.3
% 15.14/2.48 % (3166416)Termination reason: Refutation
% 15.14/2.48 % (3166416)Time elapsed: 1.608 s
% 15.14/2.48 % (3166416)Peak memory usage: 30 MB
% 15.14/2.48 % (3166416)Instructions burned: 3008 (million)
% 15.14/2.48 % (3166285)Success in time 2.231 s
% 15.14/2.48 % Vampire exiting
%------------------------------------------------------------------------------