%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWW610_2 : TPTP v9.3.1. Released v6.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n005.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 01:40:31 PM UTC 2026
% Result : Theorem 127.43s 18.30s
% Output : Refutation 127.80s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW610_2 : TPTP v9.3.1. Released v6.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.20 % Computer : n005.cluster.edu
% 0.08/0.20 % Model : x86_64 x86_64
% 0.08/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.20 % Memory : 8046.5625MB
% 0.08/0.20 % OS : Linux 6.8.0-71-generic
% 0.08/0.20 % CPULimit : 300
% 0.08/0.20 % WCLimit : 300
% 0.08/0.20 % DateTime : Mon Sep 28 14:21:31 UTC 2026
% 0.08/0.20 % CPUTime :
% 0.08/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.24 Running first-order model finding
% 0.08/0.24 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.61/0.85 % (814365)Will run a generic schedule for satisfiability detection.
% 3.61/0.85 % (814376)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3435586360:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 3.61/0.85 % (814371)% WARNING: option uhcvi not known.
% 3.61/0.85 % (814370)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3184800364_2999 on theBenchmark for (2999ds/0Mi)
% 3.61/0.85 % (814371)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3034002915:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 3.61/0.85 % (814372)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1811655861:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 3.61/0.85 % (814373)dis+10_1_sil=32000:sp=arity:random_seed=2713908304:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 3.61/0.85 % (814374)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=105805603:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 3.61/0.85 % (814375)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3878534805:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 3.61/0.85 % (814370)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 3.61/0.85 % (814370)Terminated due to inappropriate strategy.
% 3.61/0.85 % (814370)------------------------------
% 3.61/0.85 % (814370)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.61/0.85 % (814370)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.61/0.85 % (814370)CaDiCaL version: 2.1.3
% 3.61/0.85 % (814370)Termination reason: Inappropriate
% 3.61/0.85 % (814370)Time elapsed: 0.003 s
% 3.61/0.85 % (814370)Peak memory usage: 11 MB
% 3.61/0.85 % (814370)Instructions burned: 4 (million)
% 3.61/0.85 % (814370)------------------------------
% 3.61/0.85 % (814370)------------------------------
% 3.61/0.85 % (814384)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3855628132:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 3.61/0.85 % (814384)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 3.61/0.85 % (814384)Terminated due to inappropriate strategy.
% 3.61/0.85 % (814384)------------------------------
% 3.61/0.85 % (814384)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.61/0.85 % (814384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.61/0.85 % (814384)CaDiCaL version: 2.1.3
% 3.61/0.85 % (814384)Termination reason: Inappropriate
% 3.61/0.85 % (814384)Time elapsed: 0.002 s
% 3.61/0.85 % (814384)Peak memory usage: 10 MB
% 3.61/0.85 % (814384)Instructions burned: 3 (million)
% 3.61/0.85 % (814384)------------------------------
% 3.61/0.85 % (814384)------------------------------
% 3.61/0.85 % (814386)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3334946804:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 3.61/0.85 % (814376)Instruction limit reached!
% 3.61/0.85 % (814376)------------------------------
% 3.61/0.85 % (814376)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.61/0.85 % (814376)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.61/0.85 % (814376)CaDiCaL version: 2.1.3
% 3.61/0.85 % (814376)Termination reason: Instruction limit
% 3.61/0.85 % (814376)Termination phase: Saturation
% 3.61/0.85 % (814376)Time elapsed: 0.060 s
% 3.61/0.85 % (814376)Peak memory usage: 13 MB
% 3.61/0.85 % (814376)Instructions burned: 161 (million)
% 3.61/0.85 % (814388)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=1024554000:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 3.61/0.85 % (814373)Instruction limit reached!
% 3.61/0.85 % (814373)------------------------------
% 3.61/0.85 % (814373)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.61/0.85 % (814373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.61/0.85 % (814373)CaDiCaL version: 2.1.3
% 3.61/0.85 % (814373)Termination reason: Instruction limit
% 3.61/0.85 % (814373)Termination phase: Saturation
% 3.61/0.85 % (814373)Time elapsed: 0.065 s
% 3.61/0.85 % (814373)Peak memory usage: 13 MB
% 3.61/0.85 % (814373)Instructions burned: 104 (million)
% 3.61/0.85 % (814374)Instruction limit reached!
% 3.61/0.85 % (814374)------------------------------
% 3.61/0.85 % (814374)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.96/1.43 % (814374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.96/1.43 % (814374)CaDiCaL version: 2.1.3
% 7.96/1.43 % (814374)Termination reason: Instruction limit
% 7.96/1.43 % (814374)Termination phase: Saturation
% 7.96/1.43 % (814374)Time elapsed: 0.075 s
% 7.96/1.43 % (814374)Peak memory usage: 13 MB
% 7.96/1.43 % (814374)Instructions burned: 117 (million)
% 7.96/1.43 % (814375)Instruction limit reached!
% 7.96/1.43 % (814375)------------------------------
% 7.96/1.43 % (814375)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.96/1.43 % (814375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.96/1.43 % (814375)CaDiCaL version: 2.1.3
% 7.96/1.43 % (814375)Termination reason: Instruction limit
% 7.96/1.43 % (814375)Termination phase: Saturation
% 7.96/1.43 % (814375)Time elapsed: 0.086 s
% 7.96/1.43 % (814375)Peak memory usage: 13 MB
% 7.96/1.43 % (814375)Instructions burned: 132 (million)
% 7.96/1.43 % (814390)ott-21_1_sil=16000:fs=off:random_seed=2721804864:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 7.96/1.43 % (814391)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3534367347:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 7.96/1.43 % (814392)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2798301167:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 7.96/1.43 % (814392)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 7.96/1.43 % (814392)Terminated due to inappropriate strategy.
% 7.96/1.43 % (814392)------------------------------
% 7.96/1.43 % (814392)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.96/1.43 % (814392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.96/1.43 % (814392)CaDiCaL version: 2.1.3
% 7.96/1.43 % (814392)Termination reason: Inappropriate
% 7.96/1.43 % (814392)Time elapsed: 0.002 s
% 7.96/1.43 % (814392)Peak memory usage: 10 MB
% 7.96/1.43 % (814392)Instructions burned: 3 (million)
% 7.96/1.43 % (814392)------------------------------
% 7.96/1.43 % (814392)------------------------------
% 7.96/1.43 % (814396)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=682730098:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 7.96/1.43 % (814386)Instruction limit reached!
% 7.96/1.43 % (814386)------------------------------
% 7.96/1.43 % (814386)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.96/1.43 % (814386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.96/1.43 % (814386)CaDiCaL version: 2.1.3
% 7.96/1.43 % (814386)Termination reason: Instruction limit
% 7.96/1.43 % (814386)Termination phase: Saturation
% 7.96/1.43 % (814386)Time elapsed: 0.092 s
% 7.96/1.43 % (814386)Peak memory usage: 13 MB
% 7.96/1.43 % (814386)Instructions burned: 132 (million)
% 7.96/1.43 % (814398)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3144989702:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 7.96/1.43 % (814398)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 7.96/1.43 % (814398)Terminated due to inappropriate strategy.
% 7.96/1.43 % (814398)------------------------------
% 7.96/1.43 % (814398)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.96/1.43 % (814398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.96/1.43 % (814398)CaDiCaL version: 2.1.3
% 7.96/1.43 % (814398)Termination reason: Inappropriate
% 7.96/1.43 % (814398)Time elapsed: 0.002 s
% 7.96/1.43 % (814398)Peak memory usage: 10 MB
% 7.96/1.43 % (814398)Instructions burned: 3 (million)
% 7.96/1.43 % (814398)------------------------------
% 7.96/1.43 % (814398)------------------------------
% 7.96/1.43 % (814390)Instruction limit reached!
% 7.96/1.43 % (814390)------------------------------
% 7.96/1.43 % (814390)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.96/1.43 % (814390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.96/1.43 % (814390)CaDiCaL version: 2.1.3
% 7.96/1.43 % (814390)Termination reason: Instruction limit
% 7.96/1.43 % (814390)Termination phase: Saturation
% 7.96/1.43 % (814390)Time elapsed: 0.086 s
% 7.96/1.43 % (814390)Peak memory usage: 12 MB
% 7.96/1.43 % (814390)Instructions burned: 182 (million)
% 7.96/1.43 % (814400)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=2678932222: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)
% 20.87/3.27 % (814401)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2333691658:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 20.87/3.27 % (814388)Instruction limit reached!
% 20.87/3.27 % (814388)------------------------------
% 20.87/3.27 % (814388)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.87/3.27 % (814388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.87/3.27 % (814388)CaDiCaL version: 2.1.3
% 20.87/3.27 % (814388)Termination reason: Instruction limit
% 20.87/3.27 % (814388)Termination phase: Saturation
% 20.87/3.27 % (814388)Time elapsed: 0.185 s
% 20.87/3.27 % (814388)Peak memory usage: 15 MB
% 20.87/3.27 % (814388)Instructions burned: 685 (million)
% 20.87/3.27 % (814404)fmb+10_1_sil=64000:random_seed=3834217470:i=22061:nm=2:gsp=on_2997 on theBenchmark for (2997ds/22061Mi)
% 20.87/3.27 % (814404)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 20.87/3.27 % (814404)Terminated due to inappropriate strategy.
% 20.87/3.27 % (814404)------------------------------
% 20.87/3.27 % (814404)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.87/3.27 % (814404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.87/3.27 % (814404)CaDiCaL version: 2.1.3
% 20.87/3.27 % (814404)Termination reason: Inappropriate
% 20.87/3.27 % (814404)Time elapsed: 0.001 s
% 20.87/3.27 % (814404)Peak memory usage: 10 MB
% 20.87/3.27 % (814404)Instructions burned: 4 (million)
% 20.87/3.27 % (814404)------------------------------
% 20.87/3.27 % (814404)------------------------------
% 20.87/3.27 % (814406)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1773456584:i=9515:nm=5_2997 on theBenchmark for (2997ds/9515Mi)
% 20.87/3.27 % (814406)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 20.87/3.27 % (814406)Terminated due to inappropriate strategy.
% 20.87/3.27 % (814406)------------------------------
% 20.87/3.27 % (814406)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.87/3.27 % (814406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.87/3.27 % (814406)CaDiCaL version: 2.1.3
% 20.87/3.27 % (814406)Termination reason: Inappropriate
% 20.87/3.27 % (814406)Time elapsed: 0.001 s
% 20.87/3.27 % (814406)Peak memory usage: 11 MB
% 20.87/3.27 % (814406)Instructions burned: 4 (million)
% 20.87/3.27 % (814406)------------------------------
% 20.87/3.27 % (814406)------------------------------
% 20.87/3.27 % (814408)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=838311268:fmbsr=1.7:i=920_2996 on theBenchmark for (2996ds/920Mi)
% 20.87/3.27 % (814408)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 20.87/3.27 % (814408)Terminated due to inappropriate strategy.
% 20.87/3.27 % (814408)------------------------------
% 20.87/3.27 % (814408)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.87/3.27 % (814408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.87/3.27 % (814408)CaDiCaL version: 2.1.3
% 20.87/3.27 % (814408)Termination reason: Inappropriate
% 20.87/3.27 % (814408)Time elapsed: 0.001 s
% 20.87/3.27 % (814408)Peak memory usage: 11 MB
% 20.87/3.27 % (814408)Instructions burned: 3 (million)
% 20.87/3.27 % (814408)------------------------------
% 20.87/3.27 % (814408)------------------------------
% 20.87/3.27 % (814410)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=325683047:i=5131_2996 on theBenchmark for (2996ds/5131Mi)
% 20.87/3.27 % (814391)Instruction limit reached!
% 20.87/3.27 % (814391)------------------------------
% 20.87/3.27 % (814391)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.87/3.27 % (814391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.87/3.27 % (814391)CaDiCaL version: 2.1.3
% 20.87/3.27 % (814391)Termination reason: Instruction limit
% 20.87/3.27 % (814391)Termination phase: Saturation
% 20.87/3.27 % (814391)Time elapsed: 0.315 s
% 20.87/3.27 % (814391)Peak memory usage: 14 MB
% 20.87/3.27 % (814391)Instructions burned: 478 (million)
% 20.87/3.27 % (814412)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3263426971:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi)
% 20.87/3.27 % (814400)Instruction limit reached!
% 20.87/3.27 % (814400)------------------------------
% 20.87/3.27 % (814400)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.87/3.27 % (814400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.07/4.26 % (814400)CaDiCaL version: 2.1.3
% 28.07/4.26 % (814400)Termination reason: Instruction limit
% 28.07/4.26 % (814400)Termination phase: Saturation
% 28.07/4.26 % (814400)Time elapsed: 0.395 s
% 28.07/4.26 % (814400)Peak memory usage: 17 MB
% 28.07/4.26 % (814400)Instructions burned: 693 (million)
% 28.07/4.26 % (814414)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3587439380:i=6324_2993 on theBenchmark for (2993ds/6324Mi)
% 28.07/4.26 % (814414)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 28.07/4.26 % (814414)Terminated due to inappropriate strategy.
% 28.07/4.26 % (814414)------------------------------
% 28.07/4.26 % (814414)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.07/4.26 % (814414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.07/4.26 % (814414)CaDiCaL version: 2.1.3
% 28.07/4.26 % (814414)Termination reason: Inappropriate
% 28.07/4.26 % (814414)Time elapsed: 0.003 s
% 28.07/4.26 % (814414)Peak memory usage: 11 MB
% 28.07/4.26 % (814414)Instructions burned: 4 (million)
% 28.07/4.26 % (814414)------------------------------
% 28.07/4.26 % (814414)------------------------------
% 28.07/4.26 % (814416)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3149715429:fmbsr=2.30978:i=2174_2993 on theBenchmark for (2993ds/2174Mi)
% 28.07/4.26 % (814416)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 28.07/4.26 % (814416)Terminated due to inappropriate strategy.
% 28.07/4.26 % (814416)------------------------------
% 28.07/4.26 % (814416)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.07/4.26 % (814416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.07/4.26 % (814416)CaDiCaL version: 2.1.3
% 28.07/4.26 % (814416)Termination reason: Inappropriate
% 28.07/4.26 % (814416)Time elapsed: 0.002 s
% 28.07/4.26 % (814416)Peak memory usage: 10 MB
% 28.07/4.26 % (814416)Instructions burned: 3 (million)
% 28.07/4.26 % (814416)------------------------------
% 28.07/4.26 % (814416)------------------------------
% 28.07/4.26 % (814418)ott-2_1_sil=16000:newcnf=on:random_seed=3668990013:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi)
% 28.07/4.26 % (814401)Instruction limit reached!
% 28.07/4.26 % (814401)------------------------------
% 28.07/4.26 % (814401)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.07/4.26 % (814401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.07/4.26 % (814401)CaDiCaL version: 2.1.3
% 28.07/4.26 % (814401)Termination reason: Instruction limit
% 28.07/4.26 % (814401)Termination phase: Saturation
% 28.07/4.26 % (814401)Time elapsed: 0.495 s
% 28.07/4.26 % (814401)Peak memory usage: 17 MB
% 28.07/4.26 % (814401)Instructions burned: 879 (million)
% 28.07/4.26 % (814420)ott+10_1_sil=32000:tgt=ground:random_seed=2876362184:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi)
% 28.07/4.26 % (814396)Instruction limit reached!
% 28.07/4.26 % (814396)------------------------------
% 28.07/4.26 % (814396)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.07/4.26 % (814396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.07/4.26 % (814396)CaDiCaL version: 2.1.3
% 28.07/4.26 % (814396)Termination reason: Instruction limit
% 28.07/4.26 % (814396)Termination phase: Saturation
% 28.07/4.26 % (814396)Time elapsed: 0.714 s
% 28.07/4.26 % (814396)Peak memory usage: 19 MB
% 28.07/4.26 % (814396)Instructions burned: 1180 (million)
% 28.07/4.26 % (814422)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2773806385:i=54282_2991 on theBenchmark for (2991ds/54282Mi)
% 28.07/4.26 % (814422)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 28.07/4.26 % (814422)Terminated due to inappropriate strategy.
% 28.07/4.26 % (814422)------------------------------
% 28.07/4.26 % (814422)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 28.07/4.26 % (814422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.07/4.26 % (814422)CaDiCaL version: 2.1.3
% 28.07/4.26 % (814422)Termination reason: Inappropriate
% 28.07/4.26 % (814422)Time elapsed: 0.003 s
% 28.07/4.26 % (814422)Peak memory usage: 11 MB
% 28.07/4.26 % (814422)Instructions burned: 4 (million)
% 28.07/4.26 % (814422)------------------------------
% 28.07/4.26 % (814422)------------------------------
% 28.07/4.26 % (814424)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1755059709:i=3512:aac=none_2990 on theBenchmark for (2990ds/3512Mi)
% 28.07/4.26 % (814418)Instruction limit reached!
% 85.57/12.30 % (814418)------------------------------
% 85.57/12.30 % (814418)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 85.57/12.30 % (814418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.57/12.30 % (814418)CaDiCaL version: 2.1.3
% 85.57/12.30 % (814418)Termination reason: Instruction limit
% 85.57/12.30 % (814418)Termination phase: Saturation
% 85.57/12.30 % (814418)Time elapsed: 0.513 s
% 85.57/12.30 % (814418)Peak memory usage: 16 MB
% 85.57/12.30 % (814418)Instructions burned: 869 (million)
% 85.57/12.30 % (814426)dis+21_1_sil=32000:sas=cadical:random_seed=186568989:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi)
% 85.57/12.30 % (814412)Instruction limit reached!
% 85.57/12.30 % (814412)------------------------------
% 85.57/12.30 % (814412)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 85.57/12.30 % (814412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.57/12.30 % (814412)CaDiCaL version: 2.1.3
% 85.57/12.30 % (814412)Termination reason: Instruction limit
% 85.57/12.30 % (814412)Termination phase: Saturation
% 85.57/12.30 % (814412)Time elapsed: 0.836 s
% 85.57/12.30 % (814412)Peak memory usage: 22 MB
% 85.57/12.30 % (814412)Instructions burned: 1472 (million)
% 85.57/12.30 % (814428)ott+11_1_sil=16000:gs=on:random_seed=2885972342:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2986 on theBenchmark for (2986ds/2251Mi)
% 85.57/12.30 % (814410)Instruction limit reached!
% 85.57/12.30 % (814410)------------------------------
% 85.57/12.30 % (814410)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 85.57/12.30 % (814410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.57/12.30 % (814410)CaDiCaL version: 2.1.3
% 85.57/12.30 % (814410)Termination reason: Instruction limit
% 85.57/12.30 % (814410)Termination phase: Saturation
% 85.57/12.30 % (814410)Time elapsed: 1.522 s
% 85.57/12.30 % (814410)Peak memory usage: 43 MB
% 85.57/12.30 % (814410)Instructions burned: 5133 (million)
% 85.57/12.30 % (814430)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2064117068:fmbsr=1.6:i=67534_2981 on theBenchmark for (2981ds/67534Mi)
% 85.57/12.30 % (814430)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 85.57/12.30 % (814430)Terminated due to inappropriate strategy.
% 85.57/12.30 % (814430)------------------------------
% 85.57/12.30 % (814430)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 85.57/12.30 % (814430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.57/12.30 % (814430)CaDiCaL version: 2.1.3
% 85.57/12.30 % (814430)Termination reason: Inappropriate
% 85.57/12.30 % (814430)Time elapsed: 0.001 s
% 85.57/12.30 % (814430)Peak memory usage: 10 MB
% 85.57/12.30 % (814430)Instructions burned: 3 (million)
% 85.57/12.30 % (814430)------------------------------
% 85.57/12.30 % (814430)------------------------------
% 85.57/12.30 % (814432)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=204800539:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2981 on theBenchmark for (2981ds/4591Mi)
% 85.57/12.30 % (814428)Instruction limit reached!
% 85.57/12.30 % (814428)------------------------------
% 85.57/12.30 % (814428)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 85.57/12.30 % (814428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.57/12.30 % (814428)CaDiCaL version: 2.1.3
% 85.57/12.30 % (814428)Termination reason: Instruction limit
% 85.57/12.30 % (814428)Termination phase: Saturation
% 85.57/12.30 % (814428)Time elapsed: 1.347 s
% 85.57/12.30 % (814428)Peak memory usage: 24 MB
% 85.57/12.30 % (814428)Instructions burned: 2252 (million)
% 85.57/12.30 % (814434)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1985052406:i=29340_2973 on theBenchmark for (2973ds/29340Mi)
% 85.57/12.30 % (814424)Instruction limit reached!
% 85.57/12.30 % (814424)------------------------------
% 85.57/12.30 % (814424)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 85.57/12.30 % (814424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 85.57/12.30 % (814424)CaDiCaL version: 2.1.3
% 85.57/12.30 % (814424)Termination reason: Instruction limit
% 85.57/12.30 % (814424)Termination phase: Saturation
% 85.57/12.30 % (814424)Time elapsed: 1.927 s
% 85.57/12.30 % (814424)Peak memory usage: 43 MB
% 85.57/12.30 % (814424)Instructions burned: 3513 (million)
% 85.57/12.30 % (814436)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2795773264:i=5211_2971 on theBenchmark for (2971ds/5211Mi)
% 85.57/12.30 % (814432)Instruction limit reached!
% 115.41/17.88 % (814432)------------------------------
% 115.41/17.88 % (814432)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 115.41/17.88 % (814432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.41/17.88 % (814432)CaDiCaL version: 2.1.3
% 115.41/17.88 % (814432)Termination reason: Instruction limit
% 115.41/17.88 % (814432)Termination phase: Saturation
% 115.41/17.88 % (814432)Time elapsed: 1.147 s
% 115.41/17.88 % (814432)Peak memory usage: 38 MB
% 115.41/17.88 % (814432)Instructions burned: 4593 (million)
% 115.41/17.88 % (814438)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2470309349:i=5497:nm=2_2969 on theBenchmark for (2969ds/5497Mi)
% 115.41/17.88 % (814438)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 115.41/17.88 % (814438)Terminated due to inappropriate strategy.
% 115.41/17.88 % (814438)------------------------------
% 115.41/17.88 % (814438)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 115.41/17.88 % (814438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.41/17.88 % (814438)CaDiCaL version: 2.1.3
% 115.41/17.88 % (814438)Termination reason: Inappropriate
% 115.41/17.88 % (814438)Time elapsed: 0.001 s
% 115.41/17.88 % (814438)Peak memory usage: 11 MB
% 115.41/17.88 % (814438)Instructions burned: 4 (million)
% 115.41/17.88 % (814438)------------------------------
% 115.41/17.88 % (814438)------------------------------
% 115.41/17.88 % (814440)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3206248397:fmbsr=2:i=46332_2969 on theBenchmark for (2969ds/46332Mi)
% 115.41/17.88 % (814440)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 115.41/17.88 % (814440)Terminated due to inappropriate strategy.
% 115.41/17.88 % (814440)------------------------------
% 115.41/17.88 % (814440)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 115.41/17.88 % (814440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.41/17.88 % (814440)CaDiCaL version: 2.1.3
% 115.41/17.88 % (814440)Termination reason: Inappropriate
% 115.41/17.88 % (814440)Time elapsed: 0.001 s
% 115.41/17.88 % (814440)Peak memory usage: 10 MB
% 115.41/17.88 % (814440)Instructions burned: 3 (million)
% 115.41/17.88 % (814440)------------------------------
% 115.41/17.88 % (814440)------------------------------
% 115.41/17.88 % (814442)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2786451140:i=14071_2969 on theBenchmark for (2969ds/14071Mi)
% 115.41/17.88 % (814442)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 115.41/17.88 % (814442)Terminated due to inappropriate strategy.
% 115.41/17.88 % (814442)------------------------------
% 115.41/17.88 % (814442)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 115.41/17.88 % (814442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.41/17.88 % (814442)CaDiCaL version: 2.1.3
% 115.41/17.88 % (814442)Termination reason: Inappropriate
% 115.41/17.88 % (814442)Time elapsed: 0.001 s
% 115.41/17.88 % (814442)Peak memory usage: 11 MB
% 115.41/17.88 % (814442)Instructions burned: 3 (million)
% 115.41/17.88 % (814442)------------------------------
% 115.41/17.88 % (814442)------------------------------
% 115.41/17.88 % (814444)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2088527328:i=22565:add=on:rawr=on_2969 on theBenchmark for (2969ds/22565Mi)
% 115.41/17.88 % (814426)Instruction limit reached!
% 115.41/17.88 % (814426)------------------------------
% 115.41/17.88 % (814426)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 115.41/17.88 % (814426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.41/17.88 % (814426)CaDiCaL version: 2.1.3
% 115.41/17.88 % (814426)Termination reason: Instruction limit
% 115.41/17.88 % (814426)Termination phase: Saturation
% 115.41/17.88 % (814426)Time elapsed: 2.113 s
% 115.41/17.88 % (814426)Peak memory usage: 32 MB
% 115.41/17.88 % (814426)Instructions burned: 3774 (million)
% 115.41/17.88 % (814446)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3500439214:i=8173:av=off_2966 on theBenchmark for (2966ds/8173Mi)
% 115.41/17.88 % (814420)Instruction limit reached!
% 115.41/17.88 % (814420)------------------------------
% 115.41/17.88 % (814420)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 115.41/17.88 % (814420)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 115.41/17.88 % (814420)CaDiCaL version: 2.1.3
% 115.41/17.88 % (814420)Termination reason: Instruction limit
% 115.41/17.88 % (814420)Termination phase: Saturation
% 115.41/17.88 % (814420)Time elapsed: 3.275 s
% 126.97/18.18 % (814420)Peak memory usage: 34 MB
% 126.97/18.18 % (814420)Instructions burned: 5114 (million)
% 126.97/18.18 % (814448)dis+10_16:1_sil=16000:random_seed=3833671488:i=9155:fsr=off_2959 on theBenchmark for (2959ds/9155Mi)
% 126.97/18.18 % (814436)Instruction limit reached!
% 126.97/18.18 % (814436)------------------------------
% 126.97/18.18 % (814436)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 126.97/18.18 % (814436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 126.97/18.18 % (814436)CaDiCaL version: 2.1.3
% 126.97/18.18 % (814436)Termination reason: Instruction limit
% 126.97/18.18 % (814436)Termination phase: Saturation
% 126.97/18.18 % (814436)Time elapsed: 2.545 s
% 126.97/18.18 % (814436)Peak memory usage: 40 MB
% 126.97/18.18 % (814436)Instructions burned: 5211 (million)
% 126.97/18.18 % (814450)ott-3_8_sil=64000:random_seed=2385547192:i=20139:bs=on_2945 on theBenchmark for (2945ds/20139Mi)
% 126.97/18.18 % (814444)Instruction limit reached!
% 126.97/18.18 % (814444)------------------------------
% 126.97/18.18 % (814444)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 126.97/18.18 % (814444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 126.97/18.18 % (814444)CaDiCaL version: 2.1.3
% 126.97/18.18 % (814444)Termination reason: Instruction limit
% 126.97/18.18 % (814444)Termination phase: Saturation
% 126.97/18.18 % (814444)Time elapsed: 4.944 s
% 126.97/18.18 % (814444)Peak memory usage: 70 MB
% 126.97/18.18 % (814444)Instructions burned: 22568 (million)
% 126.97/18.18 % (814452)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3270416952:fmbsr=2:i=32576_2919 on theBenchmark for (2919ds/32576Mi)
% 126.97/18.18 % (814452)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 126.97/18.18 % (814452)Terminated due to inappropriate strategy.
% 126.97/18.18 % (814452)------------------------------
% 126.97/18.18 % (814452)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 126.97/18.18 % (814452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 126.97/18.18 % (814452)CaDiCaL version: 2.1.3
% 126.97/18.18 % (814452)Termination reason: Inappropriate
% 126.97/18.18 % (814452)Time elapsed: 0.001 s
% 126.97/18.18 % (814452)Peak memory usage: 11 MB
% 126.97/18.18 % (814452)Instructions burned: 4 (million)
% 126.97/18.18 % (814452)------------------------------
% 126.97/18.18 % (814452)------------------------------
% 126.97/18.18 % (814454)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3871743391:i=11404_2919 on theBenchmark for (2919ds/11404Mi)
% 126.97/18.18 % (814448)Instruction limit reached!
% 126.97/18.18 % (814448)------------------------------
% 126.97/18.18 % (814448)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 126.97/18.18 % (814448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 126.97/18.18 % (814448)CaDiCaL version: 2.1.3
% 126.97/18.18 % (814448)Termination reason: Instruction limit
% 126.97/18.18 % (814448)Termination phase: Saturation
% 126.97/18.18 % (814448)Time elapsed: 4.717 s
% 126.97/18.18 % (814448)Peak memory usage: 51 MB
% 126.97/18.18 % (814448)Instructions burned: 9157 (million)
% 126.97/18.18 % (814456)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=4269346093:i=14134_2912 on theBenchmark for (2912ds/14134Mi)
% 126.97/18.18 % (814446)Instruction limit reached!
% 126.97/18.18 % (814446)------------------------------
% 126.97/18.18 % (814446)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 126.97/18.18 % (814446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 126.97/18.18 % (814446)CaDiCaL version: 2.1.3
% 126.97/18.18 % (814446)Termination reason: Instruction limit
% 126.97/18.18 % (814446)Termination phase: Saturation
% 126.97/18.18 % (814446)Time elapsed: 5.438 s
% 126.97/18.18 % (814446)Peak memory usage: 54 MB
% 126.97/18.18 % (814446)Instructions burned: 8174 (million)
% 126.97/18.18 % (814458)dis+33_16_sil=32000:sac=on:random_seed=4103415:i=15851:nm=0_2912 on theBenchmark for (2912ds/15851Mi)
% 126.97/18.18 % (814454)Instruction limit reached!
% 126.97/18.18 % (814454)------------------------------
% 126.97/18.18 % (814454)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 126.97/18.18 % (814454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 126.97/18.18 % (814454)CaDiCaL version: 2.1.3
% 126.97/18.18 % (814454)Termination reason: Instruction limit
% 126.97/18.18 % (814454)Termination phase: Saturation
% 126.97/18.18 % (814454)Time elapsed: 3.990 s
% 126.97/18.18 % (814454)Peak memory usage: 62 MB
% 126.97/18.18 % (814454)Instructions burned: 11407 (million)
% 126.97/18.18 % (814460)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=4144016987:avsq=on:i=17627:add=on:amm=off_2879 on theBenchmark for (2879ds/17627Mi)
% 127.43/18.30 % (814434)Instruction limit reached!
% 127.43/18.30 % (814434)------------------------------
% 127.43/18.30 % (814434)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 127.43/18.30 % (814434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.43/18.30 % (814434)CaDiCaL version: 2.1.3
% 127.43/18.30 % (814434)Termination reason: Instruction limit
% 127.43/18.30 % (814434)Termination phase: Saturation
% 127.43/18.30 % (814434)Time elapsed: 14.480 s
% 127.43/18.30 % (814434)Peak memory usage: 131 MB
% 127.43/18.30 % (814434)Instructions burned: 29340 (million)
% 127.43/18.30 % (814462)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=600348052:s2a=on:i=53295_2828 on theBenchmark for (2828ds/53295Mi)
% 127.43/18.30 % (814458)Instruction limit reached!
% 127.43/18.30 % (814458)------------------------------
% 127.43/18.30 % (814458)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 127.43/18.30 % (814458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.43/18.30 % (814458)CaDiCaL version: 2.1.3
% 127.43/18.30 % (814458)Termination reason: Instruction limit
% 127.43/18.30 % (814458)Termination phase: Saturation
% 127.43/18.30 % (814458)Time elapsed: 8.730 s
% 127.43/18.30 % (814458)Peak memory usage: 144 MB
% 127.43/18.30 % (814458)Instructions burned: 15852 (million)
% 127.43/18.30 % (814460)Instruction limit reached!
% 127.43/18.30 % (814460)------------------------------
% 127.43/18.30 % (814460)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 127.43/18.30 % (814460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.43/18.30 % (814460)CaDiCaL version: 2.1.3
% 127.43/18.30 % (814460)Termination reason: Instruction limit
% 127.43/18.30 % (814460)Termination phase: Saturation
% 127.43/18.30 % (814460)Time elapsed: 5.514 s
% 127.43/18.30 % (814460)Peak memory usage: 118 MB
% 127.43/18.30 % (814460)Instructions burned: 17628 (million)
% 127.43/18.30 % (814464)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3398309618:i=26857:ins=20_2824 on theBenchmark for (2824ds/26857Mi)
% 127.43/18.30 % (814464)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 127.43/18.30 % (814464)Terminated due to inappropriate strategy.
% 127.43/18.30 % (814464)------------------------------
% 127.43/18.30 % (814464)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 127.43/18.30 % (814464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.43/18.30 % (814464)CaDiCaL version: 2.1.3
% 127.43/18.30 % (814464)Termination reason: Inappropriate
% 127.43/18.30 % (814464)Time elapsed: 0.002 s
% 127.43/18.30 % (814464)Peak memory usage: 10 MB
% 127.43/18.30 % (814464)Instructions burned: 3 (million)
% 127.43/18.30 % (814464)------------------------------
% 127.43/18.30 % (814464)------------------------------
% 127.43/18.30 % (814465)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=216194205:i=28120:bs=on:fsr=off_2824 on theBenchmark for (2824ds/28120Mi)
% 127.43/18.30 % (814467)fmb+10_1_sil=256000:fmbss=7:random_seed=3594878404:fmbsr=1.6:i=182295_2824 on theBenchmark for (2824ds/182295Mi)
% 127.43/18.30 % (814467)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 127.43/18.30 % (814467)Terminated due to inappropriate strategy.
% 127.43/18.30 % (814467)------------------------------
% 127.43/18.30 % (814467)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 127.43/18.30 % (814467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.43/18.30 % (814467)CaDiCaL version: 2.1.3
% 127.43/18.30 % (814467)Termination reason: Inappropriate
% 127.43/18.30 % (814467)Time elapsed: 0.002 s
% 127.43/18.30 % (814467)Peak memory usage: 10 MB
% 127.43/18.30 % (814467)Instructions burned: 3 (million)
% 127.43/18.30 % (814467)------------------------------
% 127.43/18.30 % (814467)------------------------------
% 127.43/18.30 % (814470)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=1967333780:i=44625:gsp=on_2823 on theBenchmark for (2823ds/44625Mi)
% 127.43/18.30 % (814470)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 127.43/18.30 % (814470)Terminated due to inappropriate strategy.
% 127.43/18.30 % (814470)------------------------------
% 127.43/18.30 % (814470)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 127.43/18.30 % (814470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.43/18.30 % (814470)CaDiCaL version: 2.1.3
% 127.43/18.30 % (814470)Termination reason: Inappropriate
% 127.43/18.30 % (814470)Time elapsed: 0.002 s
% 127.43/18.30 % (814470)Peak memory usage: 11 MB
% 127.43/18.30 % (814470)Instructions burned: 3 (million)
% 127.43/18.30 % (814470)------------------------------
% 127.43/18.30 % (814470)------------------------------
% 127.43/18.30 % (814472)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=2241775146:i=160505_2823 on theBenchmark for (2823ds/160505Mi)
% 127.43/18.30 % (814472)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 127.43/18.30 % (814472)Terminated due to inappropriate strategy.
% 127.43/18.30 % (814472)------------------------------
% 127.43/18.30 % (814472)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 127.43/18.30 % (814472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.43/18.30 % (814472)CaDiCaL version: 2.1.3
% 127.43/18.30 % (814472)Termination reason: Inappropriate
% 127.43/18.30 % (814472)Time elapsed: 0.003 s
% 127.43/18.30 % (814472)Peak memory usage: 11 MB
% 127.43/18.30 % (814472)Instructions burned: 3 (million)
% 127.43/18.30 % (814472)------------------------------
% 127.43/18.30 % (814472)------------------------------
% 127.43/18.30 % (814474)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=4246728424:fmbsr=1.3:i=225729_2823 on theBenchmark for (2823ds/225729Mi)
% 127.43/18.30 % (814474)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 127.43/18.30 % (814474)Terminated due to inappropriate strategy.
% 127.43/18.30 % (814474)------------------------------
% 127.43/18.30 % (814474)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 127.43/18.30 % (814474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.43/18.30 % (814474)CaDiCaL version: 2.1.3
% 127.43/18.30 % (814474)Termination reason: Inappropriate
% 127.43/18.30 % (814474)Time elapsed: 0.002 s
% 127.43/18.30 % (814474)Peak memory usage: 10 MB
% 127.43/18.30 % (814474)Instructions burned: 3 (million)
% 127.43/18.30 % (814474)------------------------------
% 127.43/18.30 % (814474)------------------------------
% 127.43/18.30 % (814476)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=1335756159:fmbsr=2:i=185024:ins=7_2823 on theBenchmark for (2823ds/185024Mi)
% 127.43/18.30 % (814476)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 127.43/18.30 % (814476)Terminated due to inappropriate strategy.
% 127.43/18.30 % (814476)------------------------------
% 127.43/18.30 % (814476)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 127.43/18.30 % (814476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.43/18.30 % (814476)CaDiCaL version: 2.1.3
% 127.43/18.30 % (814476)Termination reason: Inappropriate
% 127.43/18.30 % (814476)Time elapsed: 0.002 s
% 127.43/18.30 % (814476)Peak memory usage: 10 MB
% 127.43/18.30 % (814476)Instructions burned: 3 (million)
% 127.43/18.30 % (814476)------------------------------
% 127.43/18.30 % (814476)------------------------------
% 127.43/18.30 % (814478)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=1768208686:rtra=on_2822 on theBenchmark for (2822ds/0Mi)
% 127.43/18.30 % (814478)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 127.43/18.30 % (814478)Terminated due to inappropriate strategy.
% 127.43/18.30 % (814478)------------------------------
% 127.43/18.30 % (814478)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 127.43/18.30 % (814478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.43/18.30 % (814478)CaDiCaL version: 2.1.3
% 127.43/18.30 % (814478)Termination reason: Inappropriate
% 127.43/18.30 % (814478)Time elapsed: 0.003 s
% 127.43/18.30 % (814478)Peak memory usage: 11 MB
% 127.43/18.30 % (814478)Instructions burned: 4 (million)
% 127.43/18.30 % (814478)------------------------------
% 127.43/18.30 % (814478)------------------------------
% 127.43/18.30 % (814480)% WARNING: option uhcvi not known.
% 127.43/18.30 % (814480)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2724810946:i=271062:add=off:rtra=on:rawr=on_2822 on theBenchmark for (2822ds/271062Mi)
% 127.43/18.30 % (814456)Instruction limit reached!
% 127.43/18.30 % (814456)------------------------------
% 127.43/18.30 % (814456)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 127.43/18.30 % (814456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.43/18.30 % (814456)CaDiCaL version: 2.1.3
% 127.43/18.30 % (814456)Termination reason: Instruction limit
% 127.43/18.30 % (814456)Termination phase: Saturation
% 127.43/18.30 % (814456)Time elapsed: 9.121 s
% 127.43/18.30 % (814456)Peak memory usage: 71 MB
% 127.43/18.30 % (814456)Instructions burned: 14134 (million)
% 127.43/18.30 % (814482)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3724240294:i=176048:add=on:rtra=on:rawr=on_2820 on theBenchmark for (2820ds/176048Mi)
% 127.43/18.30 % (814480) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-814365-814480"...
% 127.43/18.30 % (814480)...printing done.
% 127.43/18.30 % (814480)Refutation found. Thanks to Tanya!
% 127.43/18.30 % SZS status Theorem for theBenchmark
% 127.43/18.30 % SZS output start Proof for theBenchmark
% 127.43/18.30 tff(type_def_5, type, uni: $tType).
% 127.43/18.30 tff(type_def_6, type, ty: $tType).
% 127.43/18.30 tff(type_def_7, type, bool1: $tType).
% 127.43/18.30 tff(type_def_8, type, tuple02: $tType).
% 127.43/18.30 tff(type_def_9, type, char1: $tType).
% 127.43/18.30 tff(type_def_10, type, array_char: $tType).
% 127.43/18.30 tff(func_def_0, type, witness1: ty > uni).
% 127.43/18.30 tff(func_def_1, type, int: ty).
% 127.43/18.30 tff(func_def_2, type, real: ty).
% 127.43/18.30 tff(func_def_3, type, bool: ty).
% 127.43/18.30 tff(func_def_4, type, true1: bool1).
% 127.43/18.30 tff(func_def_5, type, false1: bool1).
% 127.43/18.30 tff(func_def_6, type, match_bool1: (ty * bool1 * uni * uni) > uni).
% 127.43/18.30 tff(func_def_7, type, tuple0: ty).
% 127.43/18.30 tff(func_def_8, type, tuple03: tuple02).
% 127.43/18.30 tff(func_def_9, type, qtmark: ty).
% 127.43/18.30 tff(func_def_12, type, ref: ty > ty).
% 127.43/18.30 tff(func_def_13, type, mk_ref: (ty * uni) > uni).
% 127.43/18.30 tff(func_def_14, type, contents: (ty * uni) > uni).
% 127.43/18.30 tff(func_def_15, type, map: (ty * ty) > ty).
% 127.43/18.30 tff(func_def_16, type, get: (ty * ty * uni * uni) > uni).
% 127.43/18.30 tff(func_def_17, type, set: (ty * ty * uni * uni * uni) > uni).
% 127.43/18.30 tff(func_def_18, type, const: (ty * ty * uni) > uni).
% 127.43/18.30 tff(func_def_19, type, array: ty > ty).
% 127.43/18.30 tff(func_def_20, type, mk_array1: (ty * $int * uni) > uni).
% 127.43/18.30 tff(func_def_21, type, length1: (ty * uni) > $int).
% 127.43/18.30 tff(func_def_22, type, elts: (ty * uni) > uni).
% 127.43/18.30 tff(func_def_23, type, get2: (ty * uni * $int) > uni).
% 127.43/18.30 tff(func_def_24, type, t2tb: $int > uni).
% 127.43/18.30 tff(func_def_25, type, tb2t: uni > $int).
% 127.43/18.30 tff(func_def_26, type, set2: (ty * uni * $int * uni) > uni).
% 127.43/18.30 tff(func_def_27, type, make1: (ty * $int * uni) > uni).
% 127.43/18.30 tff(func_def_28, type, char: ty).
% 127.43/18.30 tff(func_def_29, type, t2tb1: array_char > uni).
% 127.43/18.30 tff(func_def_30, type, tb2t1: uni > array_char).
% 127.43/18.30 tff(func_def_31, type, t2tb2: char1 > uni).
% 127.43/18.30 tff(func_def_32, type, tb2t2: uni > char1).
% 127.43/18.30 tff(func_def_37, type, sK0: ($int * $int * $int * array_char * array_char) > $int).
% 127.43/18.30 tff(func_def_38, type, sK1: array_char).
% 127.43/18.30 tff(func_def_39, type, sK2: $int).
% 127.43/18.30 tff(func_def_40, type, sK3: array_char).
% 127.43/18.30 tff(func_def_41, type, sK4: $int).
% 127.43/18.30 tff(func_def_42, type, sK5: $int).
% 127.43/18.30 tff(func_def_43, type, sK6: $int).
% 127.43/18.30 tff(pred_def_1, type, sort1: (ty * uni) > $o).
% 127.43/18.30 tff(pred_def_3, type, matches1: (array_char * $int * array_char * $int * $int) > $o).
% 127.43/18.30 tff(f28,axiom,(
% 127.43/18.30 ! [X1 : uni,X2 : $int,X0 : ty] : get2(X0,X1,X2) = get(X0,int,elts(X0,X1),t2tb(X2))),
% 127.43/18.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p',get_def)).
% 127.43/18.30 tff(f39,axiom,(
% 127.43/18.30 ! [X3 : $int,X4 : $int,X1 : $int,X2 : array_char,X0 : array_char] : (($lesseq(X1,$difference(length1(char,t2tb1(X0)),X4)) & ! [X5 : $int] : (($less(X5,X4) & $lesseq(0,X5)) => tb2t2(get2(char,t2tb1(X0),$sum(X1,X5))) = tb2t2(get2(char,t2tb1(X2),$sum(X3,X5)))) & $lesseq(0,X1) & $lesseq(X3,$difference(length1(char,t2tb1(X2)),X4)) & $lesseq(0,X3)) <=> matches1(X0,X1,X2,X3,X4))),
% 127.43/18.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p',matches_def)).
% 127.43/18.30 tff(f44,conjecture,(
% 127.43/18.30 ! [X3 : $int,X4 : $int,X0 : array_char,X5 : $int,X1 : array_char,X2 : $int] : (matches1(X0,X2,X1,X3,X4) => ($less(X5,X4) => matches1(X0,X2,X1,X3,X5)))),
% 127.43/18.30 file('/export/starexec/sandbox/benchmark/theBenchmark.p',matches_right_weakening)).
% 127.43/18.30 tff(f45,negated_conjecture,(
% 127.43/18.30 ~ ! [X3 : $int,X4 : $int,X0 : array_char,X5 : $int,X1 : array_char,X2 : $int] : (matches1(X0,X2,X1,X3,X4) => ($less(X5,X4) => matches1(X0,X2,X1,X3,X5)))),
% 127.43/18.30 inference(negated_conjecture,[status(cth)],[f44])).
% 127.43/18.30 tff(f46,plain,(
% 127.43/18.30 ! [X3 : $int,X4 : $int,X1 : $int,X2 : array_char,X0 : array_char] : ((~$less($sum(length1(char,t2tb1(X0)),$uminus(X4)),X1) & ! [X5 : $int] : (($less(X5,X4) & ~$less(X5,0)) => tb2t2(get2(char,t2tb1(X0),$sum(X1,X5))) = tb2t2(get2(char,t2tb1(X2),$sum(X3,X5)))) & ~$less(X1,0) & ~$less($sum(length1(char,t2tb1(X2)),$uminus(X4)),X3) & ~$less(X3,0)) <=> matches1(X0,X1,X2,X3,X4))),
% 127.43/18.30 inference(theory_normalization,[],[f39])).
% 127.43/18.30 tff(f51,definition,(
% 127.43/18.30 ( ! [X0 : $int,X1 : $int] : ($sum(X1,X0) = $sum(X0,X1)) )),
% 127.43/18.30 introduced(theory,[tha_commutativity])).
% 127.43/18.30 tff(f52,definition,(
% 127.43/18.30 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($sum(X0,$sum(X1,X2)) = $sum($sum(X0,X1),X2)) )),
% 127.43/18.30 introduced(theory,[tha_associativity])).
% 127.43/18.30 tff(f55,definition,(
% 127.43/18.30 ( ! [X0 : $int] : (0 = $sum(X0,$uminus(X0))) )),
% 127.43/18.30 introduced(theory,[tha_inverse_op_unit])).
% 127.43/18.30 tff(f57,definition,(
% 127.43/18.30 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~$less(X1,X2) | $less(X0,X2) | ~$less(X0,X1)) )),
% 127.43/18.30 introduced(theory,[tha_transitivity])).
% 127.43/18.30 tff(f59,definition,(
% 127.43/18.30 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~$less(X0,X1) | $less($sum(X0,X2),$sum(X1,X2))) )),
% 127.43/18.30 introduced(theory,[tha_order_monotonicity])).
% 127.43/18.30 tff(f73,plain,(
% 127.43/18.30 ! [X0 : $int,X2 : $int,X4 : array_char,X1 : $int,X3 : array_char] : ((~$less(X0,0) & ~$less($sum(length1(char,t2tb1(X3)),$uminus(X1)),X0) & ! [X5 : $int] : ((~$less(X5,0) & $less(X5,X1)) => tb2t2(get2(char,t2tb1(X4),$sum(X2,X5))) = tb2t2(get2(char,t2tb1(X3),$sum(X0,X5)))) & ~$less(X2,0) & ~$less($sum(length1(char,t2tb1(X4)),$uminus(X1)),X2)) <=> matches1(X4,X2,X3,X0,X1))),
% 127.43/18.30 inference(rectify,[],[f46])).
% 127.43/18.30 tff(f85,plain,(
% 127.43/18.30 ! [X0 : uni,X1 : $int,X2 : ty] : get(X2,int,elts(X2,X0),t2tb(X1)) = get2(X2,X0,X1)),
% 127.43/18.30 inference(rectify,[],[f28])).
% 127.43/18.30 tff(f89,plain,(
% 127.43/18.30 ~ ! [X1 : $int,X3 : $int,X2 : array_char,X0 : $int,X5 : $int,X4 : array_char] : (matches1(X2,X5,X4,X0,X1) => ($less(X3,X1) => matches1(X2,X5,X4,X0,X3)))),
% 127.43/18.30 inference(rectify,[],[f45])).
% 127.43/18.30 tff(f93,plain,(
% 127.43/18.30 ! [X0 : $int,X2 : $int,X4 : array_char,X1 : $int,X3 : array_char] : ((~$less(X0,0) & ~$less($sum(length1(char,t2tb1(X3)),$uminus(X1)),X0) & ! [X5 : $int] : (tb2t2(get2(char,t2tb1(X4),$sum(X2,X5))) = tb2t2(get2(char,t2tb1(X3),$sum(X0,X5))) | ($less(X5,0) | ~$less(X5,X1))) & ~$less(X2,0) & ~$less($sum(length1(char,t2tb1(X4)),$uminus(X1)),X2)) <=> matches1(X4,X2,X3,X0,X1))),
% 127.43/18.30 inference(ennf_transformation,[],[f73])).
% 127.43/18.30 tff(f94,plain,(
% 127.43/18.30 ! [X2 : $int,X0 : $int,X4 : array_char,X3 : array_char,X1 : $int] : (matches1(X4,X2,X3,X0,X1) <=> (~$less(X2,0) & ! [X5 : $int] : (~$less(X5,X1) | $less(X5,0) | tb2t2(get2(char,t2tb1(X4),$sum(X2,X5))) = tb2t2(get2(char,t2tb1(X3),$sum(X0,X5)))) & ~$less($sum(length1(char,t2tb1(X3)),$uminus(X1)),X0) & ~$less(X0,0) & ~$less($sum(length1(char,t2tb1(X4)),$uminus(X1)),X2)))),
% 127.43/18.30 inference(flattening,[],[f93])).
% 127.43/18.30 tff(f97,plain,(
% 127.43/18.30 ? [X1 : $int,X3 : $int,X2 : array_char,X0 : $int,X5 : $int,X4 : array_char] : ((~matches1(X2,X5,X4,X0,X3) & $less(X3,X1)) & matches1(X2,X5,X4,X0,X1))),
% 127.43/18.30 inference(ennf_transformation,[],[f89])).
% 127.43/18.30 tff(f98,plain,(
% 127.43/18.30 ? [X4 : array_char,X1 : $int,X2 : array_char,X3 : $int,X0 : $int,X5 : $int] : ($less(X3,X1) & matches1(X2,X5,X4,X0,X1) & ~matches1(X2,X5,X4,X0,X3))),
% 127.43/18.30 inference(flattening,[],[f97])).
% 127.43/18.30 tff(f120,plain,(
% 127.43/18.30 ( ! [X2 : $int,X3 : array_char,X0 : $int,X1 : $int,X4 : array_char] : ($less($sum(length1(char,t2tb1(X4)),$uminus(X1)),X2) | $less(X0,0) | $less($sum(length1(char,t2tb1(X3)),$uminus(X1)),X0) | tb2t2(get2(char,t2tb1(X4),$sum(X2,sK0(X0,X1,X2,X3,X4)))) != tb2t2(get2(char,t2tb1(X3),$sum(X0,sK0(X0,X1,X2,X3,X4)))) | $less(X2,0) | matches1(X4,X2,X3,X0,X1)) )),
% 127.43/18.30 inference(cnf_transformation,[],[f94])).
% 127.43/18.30 tff(f121,plain,(
% 127.43/18.30 ( ! [X2 : $int,X3 : array_char,X0 : $int,X1 : $int,X4 : array_char] : (~$less(sK0(X0,X1,X2,X3,X4),0) | $less($sum(length1(char,t2tb1(X4)),$uminus(X1)),X2) | $less(X2,0) | $less($sum(length1(char,t2tb1(X3)),$uminus(X1)),X0) | matches1(X4,X2,X3,X0,X1) | $less(X0,0)) )),
% 127.43/18.30 inference(cnf_transformation,[],[f94])).
% 127.43/18.30 tff(f122,plain,(
% 127.43/18.30 ( ! [X2 : $int,X3 : array_char,X0 : $int,X1 : $int,X4 : array_char] : (matches1(X4,X2,X3,X0,X1) | $less($sum(length1(char,t2tb1(X3)),$uminus(X1)),X0) | $less(sK0(X0,X1,X2,X3,X4),X1) | $less($sum(length1(char,t2tb1(X4)),$uminus(X1)),X2) | $less(X0,0) | $less(X2,0)) )),
% 127.43/18.30 inference(cnf_transformation,[],[f94])).
% 127.43/18.30 tff(f123,plain,(
% 127.43/18.30 ( ! [X2 : $int,X3 : array_char,X0 : $int,X1 : $int,X4 : array_char,X5 : $int] : (tb2t2(get2(char,t2tb1(X4),$sum(X2,X5))) = tb2t2(get2(char,t2tb1(X3),$sum(X0,X5))) | $less(X5,0) | ~$less(X5,X1) | ~matches1(X4,X2,X3,X0,X1)) )),
% 127.43/18.30 inference(cnf_transformation,[],[f94])).
% 127.43/18.30 tff(f124,plain,(
% 127.43/18.30 ( ! [X2 : $int,X3 : array_char,X0 : $int,X1 : $int,X4 : array_char] : (~matches1(X4,X2,X3,X0,X1) | ~$less($sum(length1(char,t2tb1(X4)),$uminus(X1)),X2)) )),
% 127.43/18.30 inference(cnf_transformation,[],[f94])).
% 127.43/18.30 tff(f125,plain,(
% 127.43/18.30 ( ! [X2 : $int,X3 : array_char,X0 : $int,X1 : $int,X4 : array_char] : (~matches1(X4,X2,X3,X0,X1) | ~$less(X0,0)) )),
% 127.43/18.30 inference(cnf_transformation,[],[f94])).
% 127.43/18.30 tff(f126,plain,(
% 127.43/18.30 ( ! [X2 : $int,X3 : array_char,X0 : $int,X1 : $int,X4 : array_char] : (~matches1(X4,X2,X3,X0,X1) | ~$less($sum(length1(char,t2tb1(X3)),$uminus(X1)),X0)) )),
% 127.43/18.30 inference(cnf_transformation,[],[f94])).
% 127.43/18.30 tff(f127,plain,(
% 127.43/18.30 ( ! [X2 : $int,X3 : array_char,X0 : $int,X1 : $int,X4 : array_char] : (~matches1(X4,X2,X3,X0,X1) | ~$less(X2,0)) )),
% 127.43/18.30 inference(cnf_transformation,[],[f94])).
% 127.43/18.30 tff(f132,plain,(
% 127.43/18.30 ~matches1(sK3,sK6,sK1,sK5,sK4)),
% 127.43/18.30 inference(cnf_transformation,[],[f98])).
% 127.43/18.30 tff(f133,plain,(
% 127.43/18.30 matches1(sK3,sK6,sK1,sK5,sK2)),
% 127.43/18.30 inference(cnf_transformation,[],[f98])).
% 127.43/18.30 tff(f134,plain,(
% 127.43/18.30 $less(sK4,sK2)),
% 127.43/18.30 inference(cnf_transformation,[],[f98])).
% 127.43/18.30 tff(f157,plain,(
% 127.43/18.30 ( ! [X2 : ty,X0 : uni,X1 : $int] : (get(X2,int,elts(X2,X0),t2tb(X1)) = get2(X2,X0,X1)) )),
% 127.43/18.30 inference(cnf_transformation,[],[f85])).
% 127.43/18.30 tff(f172,plain,(
% 127.43/18.30 ( ! [X2 : $int,X3 : array_char,X0 : $int,X1 : $int,X4 : array_char,X5 : $int] : (~matches1(X4,X2,X3,X0,X1) | tb2t2(get(char,int,elts(char,t2tb1(X3)),t2tb($sum(X0,X5)))) = tb2t2(get(char,int,elts(char,t2tb1(X4)),t2tb($sum(X2,X5)))) | $less(X5,0) | ~$less(X5,X1)) )),
% 127.43/18.30 inference(definition_unfolding,[],[f123,f157,f157])).
% 127.43/18.30 tff(f173,plain,(
% 127.43/18.30 ( ! [X2 : $int,X3 : array_char,X0 : $int,X1 : $int,X4 : array_char] : (matches1(X4,X2,X3,X0,X1) | $less($sum(length1(char,t2tb1(X4)),$uminus(X1)),X2) | tb2t2(get(char,int,elts(char,t2tb1(X4)),t2tb($sum(X2,sK0(X0,X1,X2,X3,X4))))) != tb2t2(get(char,int,elts(char,t2tb1(X3)),t2tb($sum(X0,sK0(X0,X1,X2,X3,X4))))) | $less($sum(length1(char,t2tb1(X3)),$uminus(X1)),X0) | $less(X2,0) | $less(X0,0)) )),
% 127.43/18.30 inference(definition_unfolding,[],[f120,f157,f157])).
% 127.43/18.30 tff(f258,plain,(
% 127.43/18.30 ( ! [X0 : $int] : (~$less(X0,sK4) | $less(X0,sK2)) )),
% 127.43/18.30 inference(resolution,[],[f57,f134])).
% 127.43/18.30 tff(f267,plain,(
% 127.43/18.30 ~$less(sK5,0)),
% 127.43/18.30 inference(resolution,[],[f125,f133])).
% 127.43/18.30 tff(f268,plain,(
% 127.43/18.30 ~$less(sK6,0)),
% 127.43/18.30 inference(resolution,[],[f127,f133])).
% 127.43/18.30 tff(f285,plain,(
% 127.43/18.30 ( ! [X0 : $int] : ($less($sum(sK4,X0),$sum(sK2,X0))) )),
% 127.43/18.30 inference(resolution,[],[f59,f134])).
% 127.43/18.30 tff(f363,plain,(
% 127.43/18.30 ( ! [X0 : $int,X1 : $int] : ($sum(0,X1) = $sum(X0,$sum($uminus(X0),X1))) )),
% 127.43/18.30 inference(superposition,[],[f52,f55])).
% 127.43/18.30 tff(f371,plain,(
% 127.43/18.30 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($sum(X0,$sum(X1,X2)) = $sum(X1,$sum(X2,X0))) )),
% 127.43/18.30 inference(superposition,[],[f52,f51])).
% 127.43/18.30 tff(f381,plain,(
% 127.43/18.30 ( ! [X0 : $int,X1 : $int] : ($sum(X0,$sum($uminus(X0),X1)) = X1) )),
% 127.43/18.30 inference(evaluation,[],[f363])).
% 127.43/18.30 tff(f476,plain,(
% 127.43/18.30 ~$less($sum(length1(char,t2tb1(sK3)),$uminus(sK2)),sK6)),
% 127.43/18.30 inference(resolution,[],[f124,f133])).
% 127.43/18.30 tff(f479,plain,(
% 127.43/18.30 ~$less($sum(length1(char,t2tb1(sK1)),$uminus(sK2)),sK5)),
% 127.43/18.30 inference(resolution,[],[f126,f133])).
% 127.43/18.30 tff(f560,plain,(
% 127.43/18.30 ( ! [X0 : $int] : (~$less(X0,sK2) | tb2t2(get(char,int,elts(char,t2tb1(sK3)),t2tb($sum(sK6,X0)))) = tb2t2(get(char,int,elts(char,t2tb1(sK1)),t2tb($sum(sK5,X0)))) | $less(X0,0)) )),
% 127.43/18.30 inference(resolution,[],[f172,f133])).
% 127.43/18.30 tff(f570,plain,(
% 127.43/18.30 $less(sK5,0) | $less(sK0(sK5,sK4,sK6,sK1,sK3),sK4) | $less($sum(length1(char,t2tb1(sK3)),$uminus(sK4)),sK6) | $less($sum(length1(char,t2tb1(sK1)),$uminus(sK4)),sK5) | $less(sK6,0)),
% 127.43/18.30 inference(resolution,[],[f122,f132])).
% 127.43/18.30 tff(f580,plain,(
% 127.43/18.30 $less($sum(length1(char,t2tb1(sK1)),$uminus(sK4)),sK5) | $less(sK6,0) | $less($sum(length1(char,t2tb1(sK3)),$uminus(sK4)),sK6) | $less(sK0(sK5,sK4,sK6,sK1,sK3),sK4)),
% 127.43/18.30 inference(forward_subsumption_resolution,[],[f570,f267])).
% 127.43/18.30 tff(f582,plain,(
% 127.43/18.30 $less(sK0(sK5,sK4,sK6,sK1,sK3),sK4) | $less($sum(length1(char,t2tb1(sK1)),$uminus(sK4)),sK5) | $less($sum(length1(char,t2tb1(sK3)),$uminus(sK4)),sK6)),
% 127.43/18.30 inference(forward_subsumption_resolution,[],[f580,f268])).
% 127.43/18.30 tff(f608,plain,(
% 127.43/18.30 ~$less($sum($uminus(sK2),length1(char,t2tb1(sK1))),sK5)),
% 127.43/18.30 inference(forward_demodulation,[],[f479,f51])).
% 127.43/18.30 tff(f617,definition,(
% 127.43/18.30 spl7_11 <=> $less($sum($uminus(sK4),length1(char,t2tb1(sK1))),sK5)),
% 127.43/18.30 introduced(definition,[new_symbols(definition,[spl7_11])],[avatar_definition])).
% 127.43/18.30 tff(f618,plain,(
% 127.43/18.30 ~$less($sum($uminus(sK4),length1(char,t2tb1(sK1))),sK5) | spl7_11),
% 127.43/18.30 inference(avatar_component_clause,[],[f617])).
% 127.43/18.30 tff(f619,plain,(
% 127.43/18.30 $less($sum($uminus(sK4),length1(char,t2tb1(sK1))),sK5) | ~spl7_11),
% 127.43/18.30 inference(avatar_component_clause,[],[f617])).
% 127.43/18.30 tff(f658,plain,(
% 127.43/18.30 $less(sK5,0) | $less($sum(length1(char,t2tb1(sK1)),$uminus(sK4)),sK5) | $less(sK6,0) | tb2t2(get(char,int,elts(char,t2tb1(sK1)),t2tb($sum(sK5,sK0(sK5,sK4,sK6,sK1,sK3))))) != tb2t2(get(char,int,elts(char,t2tb1(sK3)),t2tb($sum(sK6,sK0(sK5,sK4,sK6,sK1,sK3))))) | $less($sum(length1(char,t2tb1(sK3)),$uminus(sK4)),sK6)),
% 127.43/18.30 inference(resolution,[],[f173,f132])).
% 127.43/18.30 tff(f666,plain,(
% 127.43/18.30 $less($sum(length1(char,t2tb1(sK3)),$uminus(sK4)),sK6) | tb2t2(get(char,int,elts(char,t2tb1(sK1)),t2tb($sum(sK5,sK0(sK5,sK4,sK6,sK1,sK3))))) != tb2t2(get(char,int,elts(char,t2tb1(sK3)),t2tb($sum(sK6,sK0(sK5,sK4,sK6,sK1,sK3))))) | $less($sum(length1(char,t2tb1(sK1)),$uminus(sK4)),sK5) | $less(sK6,0)),
% 127.43/18.30 inference(forward_subsumption_resolution,[],[f658,f267])).
% 127.43/18.30 tff(f667,plain,(
% 127.43/18.30 $less($sum(length1(char,t2tb1(sK1)),$uminus(sK4)),sK5) | $less($sum(length1(char,t2tb1(sK3)),$uminus(sK4)),sK6) | tb2t2(get(char,int,elts(char,t2tb1(sK1)),t2tb($sum(sK5,sK0(sK5,sK4,sK6,sK1,sK3))))) != tb2t2(get(char,int,elts(char,t2tb1(sK3)),t2tb($sum(sK6,sK0(sK5,sK4,sK6,sK1,sK3)))))),
% 127.43/18.30 inference(forward_subsumption_resolution,[],[f666,f268])).
% 127.43/18.30 tff(f668,plain,(
% 127.43/18.30 $less($sum($uminus(sK4),length1(char,t2tb1(sK1))),sK5) | $less($sum(length1(char,t2tb1(sK3)),$uminus(sK4)),sK6) | tb2t2(get(char,int,elts(char,t2tb1(sK1)),t2tb($sum(sK5,sK0(sK5,sK4,sK6,sK1,sK3))))) != tb2t2(get(char,int,elts(char,t2tb1(sK3)),t2tb($sum(sK6,sK0(sK5,sK4,sK6,sK1,sK3)))))),
% 127.43/18.30 inference(forward_demodulation,[],[f667,f51])).
% 127.43/18.30 tff(f706,plain,(
% 127.43/18.30 $less($sum(length1(char,t2tb1(sK3)),$uminus(sK4)),sK6) | $less($sum($uminus(sK4),length1(char,t2tb1(sK1))),sK5) | $less(sK0(sK5,sK4,sK6,sK1,sK3),sK4)),
% 127.43/18.30 inference(forward_demodulation,[],[f582,f51])).
% 127.43/18.30 tff(f708,plain,(
% 127.43/18.30 ~$less($sum($uminus(sK2),length1(char,t2tb1(sK3))),sK6)),
% 127.43/18.30 inference(forward_demodulation,[],[f476,f51])).
% 127.43/18.30 tff(f709,plain,(
% 127.43/18.30 $less($sum($uminus(sK4),length1(char,t2tb1(sK1))),sK5) | tb2t2(get(char,int,elts(char,t2tb1(sK1)),t2tb($sum(sK5,sK0(sK5,sK4,sK6,sK1,sK3))))) != tb2t2(get(char,int,elts(char,t2tb1(sK3)),t2tb($sum(sK6,sK0(sK5,sK4,sK6,sK1,sK3))))) | $less($sum($uminus(sK4),length1(char,t2tb1(sK3))),sK6)),
% 127.43/18.30 inference(forward_demodulation,[],[f668,f51])).
% 127.43/18.30 tff(f710,plain,(
% 127.43/18.30 $less(sK0(sK5,sK4,sK6,sK1,sK3),sK4) | $less($sum($uminus(sK4),length1(char,t2tb1(sK3))),sK6) | $less($sum($uminus(sK4),length1(char,t2tb1(sK1))),sK5)),
% 127.43/18.30 inference(forward_demodulation,[],[f706,f51])).
% 127.43/18.30 tff(f713,definition,(
% 127.43/18.30 spl7_20 <=> $less($sum($uminus(sK4),length1(char,t2tb1(sK3))),sK6)),
% 127.43/18.30 introduced(definition,[new_symbols(definition,[spl7_20])],[avatar_definition])).
% 127.43/18.30 tff(f715,plain,(
% 127.43/18.30 $less($sum($uminus(sK4),length1(char,t2tb1(sK3))),sK6) | ~spl7_20),
% 127.43/18.30 inference(avatar_component_clause,[],[f713])).
% 127.43/18.30 tff(f717,definition,(
% 127.43/18.30 spl7_21 <=> tb2t2(get(char,int,elts(char,t2tb1(sK1)),t2tb($sum(sK5,sK0(sK5,sK4,sK6,sK1,sK3))))) = tb2t2(get(char,int,elts(char,t2tb1(sK3)),t2tb($sum(sK6,sK0(sK5,sK4,sK6,sK1,sK3)))))),
% 127.43/18.30 introduced(definition,[new_symbols(definition,[spl7_21])],[avatar_definition])).
% 127.43/18.30 tff(f719,plain,(
% 127.43/18.30 tb2t2(get(char,int,elts(char,t2tb1(sK1)),t2tb($sum(sK5,sK0(sK5,sK4,sK6,sK1,sK3))))) != tb2t2(get(char,int,elts(char,t2tb1(sK3)),t2tb($sum(sK6,sK0(sK5,sK4,sK6,sK1,sK3))))) | spl7_21),
% 127.43/18.30 inference(avatar_component_clause,[],[f717])).
% 127.43/18.30 tff(f720,plain,(
% 127.43/18.30 spl7_20 | spl7_11 | ~spl7_21),
% 127.43/18.30 inference(avatar_split_clause,[],[f709,f717,f617,f713])).
% 127.43/18.30 tff(f722,definition,(
% 127.43/18.30 spl7_22 <=> $less(sK0(sK5,sK4,sK6,sK1,sK3),sK4)),
% 127.43/18.30 introduced(definition,[new_symbols(definition,[spl7_22])],[avatar_definition])).
% 127.43/18.30 tff(f724,plain,(
% 127.43/18.30 $less(sK0(sK5,sK4,sK6,sK1,sK3),sK4) | ~spl7_22),
% 127.43/18.30 inference(avatar_component_clause,[],[f722])).
% 127.43/18.30 tff(f725,plain,(
% 127.43/18.30 spl7_20 | spl7_11 | spl7_22),
% 127.43/18.30 inference(avatar_split_clause,[],[f710,f722,f617,f713])).
% 127.43/18.30 tff(f752,plain,(
% 127.43/18.30 ( ! [X0 : $int] : (~$less(X0,$sum($uminus(sK4),length1(char,t2tb1(sK1)))) | $less(X0,sK5)) ) | ~spl7_11),
% 127.43/18.30 inference(resolution,[],[f619,f57])).
% 127.43/18.30 tff(f880,plain,(
% 127.43/18.30 ( ! [X0 : $int] : ($less($sum(sK4,$sum($uminus(sK2),X0)),X0)) )),
% 127.43/18.30 inference(superposition,[],[f285,f381])).
% 127.43/18.30 tff(f5468,plain,(
% 127.43/18.30 $less($sum(sK4,$sum($uminus(sK2),$sum($uminus(sK4),length1(char,t2tb1(sK1))))),sK5) | ~spl7_11),
% 127.43/18.30 inference(resolution,[],[f752,f880])).
% 127.43/18.30 tff(f5477,plain,(
% 127.43/18.30 $less($sum(sK4,$sum($uminus(sK4),$sum(length1(char,t2tb1(sK1)),$uminus(sK2)))),sK5) | ~spl7_11),
% 127.43/18.30 inference(forward_demodulation,[],[f5468,f371])).
% 127.43/18.30 tff(f5483,plain,(
% 127.43/18.30 $less($sum(length1(char,t2tb1(sK1)),$uminus(sK2)),sK5) | ~spl7_11),
% 127.43/18.30 inference(forward_demodulation,[],[f5477,f381])).
% 127.43/18.30 tff(f5489,plain,(
% 127.43/18.30 $less($sum($uminus(sK2),length1(char,t2tb1(sK1))),sK5) | ~spl7_11),
% 127.80/18.30 inference(forward_demodulation,[],[f5483,f51])).
% 127.80/18.30 tff(f5494,plain,(
% 127.80/18.30 $false | ~spl7_11),
% 127.80/18.30 inference(forward_subsumption_resolution,[],[f5489,f608])).
% 127.80/18.30 tff(f5495,plain,(
% 127.80/18.30 ~spl7_11),
% 127.80/18.30 inference(avatar_contradiction_clause,[],[f5494])).
% 127.80/18.30 tff(f5786,plain,(
% 127.80/18.30 $less(sK0(sK5,sK4,sK6,sK1,sK3),sK2) | ~spl7_22),
% 127.80/18.30 inference(resolution,[],[f724,f258])).
% 127.80/18.30 tff(f5798,definition,(
% 127.80/18.30 spl7_87 <=> $less(sK0(sK5,sK4,sK6,sK1,sK3),0)),
% 127.80/18.30 introduced(definition,[new_symbols(definition,[spl7_87])],[avatar_definition])).
% 127.80/18.30 tff(f5800,plain,(
% 127.80/18.30 $less(sK0(sK5,sK4,sK6,sK1,sK3),0) | ~spl7_87),
% 127.80/18.30 inference(avatar_component_clause,[],[f5798])).
% 127.80/18.30 tff(f5825,plain,(
% 127.80/18.30 tb2t2(get(char,int,elts(char,t2tb1(sK1)),t2tb($sum(sK5,sK0(sK5,sK4,sK6,sK1,sK3))))) = tb2t2(get(char,int,elts(char,t2tb1(sK3)),t2tb($sum(sK6,sK0(sK5,sK4,sK6,sK1,sK3))))) | $less(sK0(sK5,sK4,sK6,sK1,sK3),0) | ~spl7_22),
% 127.80/18.30 inference(resolution,[],[f5786,f560])).
% 127.80/18.30 tff(f5831,plain,(
% 127.80/18.30 $less(sK0(sK5,sK4,sK6,sK1,sK3),0) | (spl7_21 | ~spl7_22)),
% 127.80/18.30 inference(forward_subsumption_resolution,[],[f5825,f719])).
% 127.80/18.30 tff(f5833,plain,(
% 127.80/18.30 spl7_87 | spl7_21 | ~spl7_22),
% 127.80/18.30 inference(avatar_split_clause,[],[f5831,f722,f717,f5798])).
% 127.80/18.30 tff(f5839,plain,(
% 127.80/18.30 $less(sK5,0) | $less($sum(length1(char,t2tb1(sK1)),$uminus(sK4)),sK5) | $less($sum(length1(char,t2tb1(sK3)),$uminus(sK4)),sK6) | matches1(sK3,sK6,sK1,sK5,sK4) | $less(sK6,0) | ~spl7_87),
% 127.80/18.30 inference(resolution,[],[f5800,f121])).
% 127.80/18.30 tff(f5847,plain,(
% 127.80/18.30 matches1(sK3,sK6,sK1,sK5,sK4) | $less($sum(length1(char,t2tb1(sK3)),$uminus(sK4)),sK6) | $less(sK6,0) | $less($sum(length1(char,t2tb1(sK1)),$uminus(sK4)),sK5) | ~spl7_87),
% 127.80/18.30 inference(forward_subsumption_resolution,[],[f5839,f267])).
% 127.80/18.30 tff(f5848,plain,(
% 127.80/18.30 $less($sum(length1(char,t2tb1(sK3)),$uminus(sK4)),sK6) | $less($sum(length1(char,t2tb1(sK1)),$uminus(sK4)),sK5) | $less(sK6,0) | ~spl7_87),
% 127.80/18.30 inference(forward_subsumption_resolution,[],[f5847,f132])).
% 127.80/18.30 tff(f5849,plain,(
% 127.80/18.30 $less($sum(length1(char,t2tb1(sK1)),$uminus(sK4)),sK5) | $less($sum(length1(char,t2tb1(sK3)),$uminus(sK4)),sK6) | ~spl7_87),
% 127.80/18.30 inference(forward_subsumption_resolution,[],[f5848,f268])).
% 127.80/18.30 tff(f5850,plain,(
% 127.80/18.30 $less($sum(length1(char,t2tb1(sK3)),$uminus(sK4)),sK6) | $less($sum($uminus(sK4),length1(char,t2tb1(sK1))),sK5) | ~spl7_87),
% 127.80/18.30 inference(forward_demodulation,[],[f5849,f51])).
% 127.80/18.30 tff(f5851,plain,(
% 127.80/18.30 $less($sum(length1(char,t2tb1(sK3)),$uminus(sK4)),sK6) | (spl7_11 | ~spl7_87)),
% 127.80/18.30 inference(forward_subsumption_resolution,[],[f5850,f618])).
% 127.80/18.30 tff(f5852,plain,(
% 127.80/18.30 $less($sum($uminus(sK4),length1(char,t2tb1(sK3))),sK6) | (spl7_11 | ~spl7_87)),
% 127.80/18.30 inference(forward_demodulation,[],[f5851,f51])).
% 127.80/18.30 tff(f5853,plain,(
% 127.80/18.30 spl7_20 | spl7_11 | ~spl7_87),
% 127.80/18.30 inference(avatar_split_clause,[],[f5852,f5798,f617,f713])).
% 127.80/18.30 tff(f5858,plain,(
% 127.80/18.30 ( ! [X0 : $int] : (~$less(X0,$sum($uminus(sK4),length1(char,t2tb1(sK3)))) | $less(X0,sK6)) ) | ~spl7_20),
% 127.80/18.30 inference(resolution,[],[f715,f57])).
% 127.80/18.30 tff(f5964,plain,(
% 127.80/18.30 $less($sum(sK4,$sum($uminus(sK2),$sum($uminus(sK4),length1(char,t2tb1(sK3))))),sK6) | ~spl7_20),
% 127.80/18.30 inference(resolution,[],[f5858,f880])).
% 127.80/18.30 tff(f5973,plain,(
% 127.80/18.30 $less($sum(sK4,$sum($uminus(sK4),$sum(length1(char,t2tb1(sK3)),$uminus(sK2)))),sK6) | ~spl7_20),
% 127.80/18.30 inference(forward_demodulation,[],[f5964,f371])).
% 127.80/18.30 tff(f5980,plain,(
% 127.80/18.30 $less($sum(length1(char,t2tb1(sK3)),$uminus(sK2)),sK6) | ~spl7_20),
% 127.80/18.30 inference(forward_demodulation,[],[f5973,f381])).
% 127.80/18.30 tff(f5987,plain,(
% 127.80/18.30 $less($sum($uminus(sK2),length1(char,t2tb1(sK3))),sK6) | ~spl7_20),
% 127.80/18.30 inference(forward_demodulation,[],[f5980,f51])).
% 127.80/18.30 tff(f5992,plain,(
% 127.80/18.30 $false | ~spl7_20),
% 127.80/18.30 inference(forward_subsumption_resolution,[],[f5987,f708])).
% 127.80/18.30 tff(f5993,plain,(
% 127.80/18.30 ~spl7_20),
% 127.80/18.30 inference(avatar_contradiction_clause,[],[f5992])).
% 127.80/18.30 cnf(s15, plain, spl7_11 | spl7_20 | ~spl7_21, inference(sat_conversion,[],[f720])).
% 127.80/18.30 cnf(s16, plain, spl7_11 | spl7_20 | spl7_22, inference(sat_conversion,[],[f725])).
% 127.80/18.30 cnf(s73, plain, ~spl7_11, inference(sat_conversion,[],[f5495])).
% 127.80/18.30 cnf(s90, plain, spl7_21 | ~spl7_22 | spl7_87, inference(sat_conversion,[],[f5833])).
% 127.80/18.30 cnf(s92, plain, spl7_11 | spl7_20 | ~spl7_87, inference(sat_conversion,[],[f5853])).
% 127.80/18.30 cnf(s94, plain, ~spl7_20, inference(sat_conversion,[],[f5993])).
% 127.80/18.30 cnf(s95, plain, spl7_11 | ~spl7_87, inference(rat,[],[s92,s94])).
% 127.80/18.30 cnf(s97, plain, ~spl7_87, inference(rat,[],[s95,s73])).
% 127.80/18.30 cnf(s98, plain, spl7_22, inference(rat,[],[s16,s94,s73])).
% 127.80/18.30 cnf(s100, plain, spl7_21, inference(rat,[],[s90,s97,s98])).
% 127.80/18.30 cnf(s102, plain, $false, inference(rat,[],[s15,s100,s94,s73])).
% 127.80/18.30 tff(f6002,plain,(
% 127.80/18.30 $false),
% 127.80/18.30 inference(avatar_sat_refutation,[],[s102])).
% 127.80/18.30 % SZS output end Proof for theBenchmark
% 127.80/18.30 % (814480)------------------------------
% 127.80/18.30 % (814480)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 127.80/18.30 % (814480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.80/18.30 % (814480)CaDiCaL version: 2.1.3
% 127.80/18.30 % (814480)Termination reason: Refutation
% 127.80/18.30 % (814480)Time elapsed: 0.217 s
% 127.80/18.30 % (814480)Peak memory usage: 16 MB
% 127.80/18.30 % (814480)Instructions burned: 345 (million)
% 127.80/18.30 % (814365)Success in time 18.053 s
% 127.80/18.30 % Vampire exiting
%------------------------------------------------------------------------------