%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWC519_1 : TPTP v9.3.1. Bugfixed v9.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n002.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:06:11 PM UTC 2026
% Result : Theorem 5.75s 1.08s
% Output : Refutation 5.75s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWC519_1 : TPTP v9.3.1. Bugfixed v9.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.17 % Computer : n002.cluster.edu
% 0.09/0.17 % Model : x86_64 x86_64
% 0.09/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.17 % Memory : 8046.5625MB
% 0.09/0.17 % OS : Linux 6.8.0-71-generic
% 0.09/0.17 % CPULimit : 300
% 0.09/0.17 % WCLimit : 300
% 0.09/0.17 % DateTime : Mon Sep 28 09:44:22 UTC 2026
% 0.09/0.17 % CPUTime :
% 0.09/0.17 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.09/0.20 Running first-order model finding
% 0.09/0.20 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.33/0.70 % (236427)Will run a generic schedule for satisfiability detection.
% 3.33/0.70 % (236435)dis+10_1_sil=32000:sp=arity:random_seed=3372653801:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 3.33/0.70 % (236433)% WARNING: option uhcvi not known.
% 3.33/0.70 % (236432)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1304643152_2999 on theBenchmark for (2999ds/0Mi)
% 3.33/0.70 % (236433)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2873305058:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 3.33/0.70 % (236434)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=414446388:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 3.33/0.70 % (236436)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=744041681:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 3.33/0.70 % (236438)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=879161798:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 3.33/0.70 % (236437)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1920633071:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 3.33/0.70 % (236432)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 3.33/0.70 % (236432)Terminated due to inappropriate strategy.
% 3.33/0.70 % (236432)------------------------------
% 3.33/0.70 % (236432)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.33/0.70 % (236432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.33/0.70 % (236432)CaDiCaL version: 2.1.3
% 3.33/0.70 % (236432)Termination reason: Inappropriate
% 3.33/0.70 % (236432)Time elapsed: 0.015 s
% 3.33/0.70 % (236432)Peak memory usage: 11 MB
% 3.33/0.70 % (236432)Instructions burned: 31 (million)
% 3.33/0.70 % (236432)------------------------------
% 3.33/0.70 % (236432)------------------------------
% 3.33/0.70 % (236435)Instruction limit reached!
% 3.33/0.70 % (236435)------------------------------
% 3.33/0.70 % (236435)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.33/0.70 % (236435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.33/0.70 % (236435)CaDiCaL version: 2.1.3
% 3.33/0.70 % (236435)Termination reason: Instruction limit
% 3.33/0.70 % (236435)Termination phase: Saturation
% 3.33/0.70 % (236435)Time elapsed: 0.033 s
% 3.33/0.70 % (236435)Peak memory usage: 13 MB
% 3.33/0.70 % (236435)Instructions burned: 105 (million)
% 3.33/0.70 % (236447)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2790956697:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 3.33/0.70 % (236446)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=370686533:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 3.33/0.70 % (236446)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 3.33/0.70 % (236446)Terminated due to inappropriate strategy.
% 3.33/0.70 % (236446)------------------------------
% 3.33/0.70 % (236446)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.33/0.70 % (236446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.33/0.70 % (236446)CaDiCaL version: 2.1.3
% 3.33/0.70 % (236446)Termination reason: Inappropriate
% 3.33/0.70 % (236446)Time elapsed: 0.012 s
% 3.33/0.70 % (236446)Peak memory usage: 11 MB
% 3.33/0.70 % (236446)Instructions burned: 24 (million)
% 3.33/0.70 % (236446)------------------------------
% 3.33/0.70 % (236446)------------------------------
% 3.33/0.70 % (236436)Instruction limit reached!
% 3.33/0.70 % (236436)------------------------------
% 3.33/0.70 % (236436)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.33/0.70 % (236436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.33/0.70 % (236436)CaDiCaL version: 2.1.3
% 3.33/0.70 % (236436)Termination reason: Instruction limit
% 3.33/0.70 % (236436)Termination phase: Saturation
% 3.33/0.70 % (236436)Time elapsed: 0.060 s
% 3.33/0.70 % (236436)Peak memory usage: 14 MB
% 3.33/0.70 % (236436)Instructions burned: 116 (million)
% 3.33/0.70 % (236437)Instruction limit reached!
% 3.33/0.70 % (236437)------------------------------
% 3.33/0.70 % (236437)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 3.33/0.70 % (236437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.33/0.70 % (236437)CaDiCaL version: 2.1.3
% 3.33/0.70 % (236437)Termination reason: Instruction limit
% 3.33/0.70 % (236437)Termination phase: Saturation
% 5.75/1.06 % (236437)Time elapsed: 0.066 s
% 5.75/1.06 % (236437)Peak memory usage: 14 MB
% 5.75/1.06 % (236437)Instructions burned: 132 (million)
% 5.75/1.06 % (236450)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=1754851108:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 5.75/1.06 % (236447)Instruction limit reached!
% 5.75/1.06 % (236447)------------------------------
% 5.75/1.06 % (236447)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.75/1.06 % (236447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.75/1.06 % (236447)CaDiCaL version: 2.1.3
% 5.75/1.06 % (236447)Termination reason: Instruction limit
% 5.75/1.06 % (236447)Termination phase: Saturation
% 5.75/1.06 % (236447)Time elapsed: 0.039 s
% 5.75/1.06 % (236447)Peak memory usage: 14 MB
% 5.75/1.06 % (236447)Instructions burned: 133 (million)
% 5.75/1.06 % (236451)ott-21_1_sil=16000:fs=off:random_seed=631147656:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 5.75/1.06 % (236454)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=486904353:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 5.75/1.06 % (236452)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4268029295:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 5.75/1.06 % (236454)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 5.75/1.06 % (236438)Instruction limit reached!
% 5.75/1.06 % (236438)------------------------------
% 5.75/1.06 % (236438)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.75/1.06 % (236454)Terminated due to inappropriate strategy.
% 5.75/1.06 % (236454)------------------------------
% 5.75/1.06 % (236454)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.75/1.06 % (236454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.75/1.06 % (236438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.75/1.06 % (236454)CaDiCaL version: 2.1.3
% 5.75/1.06 % (236438)CaDiCaL version: 2.1.3
% 5.75/1.06 % (236438)Termination reason: Instruction limit
% 5.75/1.06 % (236438)Termination phase: Saturation
% 5.75/1.06 % (236438)Time elapsed: 0.091 s
% 5.75/1.06 % (236454)Termination reason: Inappropriate
% 5.75/1.06 % (236454)Time elapsed: 0.006 s
% 5.75/1.06 % (236438)Peak memory usage: 15 MB
% 5.75/1.06 % (236454)Peak memory usage: 11 MB
% 5.75/1.06 % (236438)Instructions burned: 160 (million)
% 5.75/1.06 % (236454)Instructions burned: 23 (million)
% 5.75/1.06 % (236454)------------------------------
% 5.75/1.06 % (236454)------------------------------
% 5.75/1.06 % (236459)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3439808386:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 5.75/1.06 % (236459)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 5.75/1.06 % (236459)Terminated due to inappropriate strategy.
% 5.75/1.06 % (236459)------------------------------
% 5.75/1.06 % (236459)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.75/1.06 % (236459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.75/1.06 % (236459)CaDiCaL version: 2.1.3
% 5.75/1.06 % (236459)Termination reason: Inappropriate
% 5.75/1.06 % (236459)Time elapsed: 0.006 s
% 5.75/1.06 % (236459)Peak memory usage: 11 MB
% 5.75/1.06 % (236459)Instructions burned: 24 (million)
% 5.75/1.06 % (236459)------------------------------
% 5.75/1.06 % (236459)------------------------------
% 5.75/1.06 % (236458)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=924278916:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 5.75/1.06 % (236461)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=2962101053: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)
% 5.75/1.06 % (236451)Instruction limit reached!
% 5.75/1.06 % (236451)------------------------------
% 5.75/1.06 % (236451)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.75/1.06 % (236451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.75/1.06 % (236451)CaDiCaL version: 2.1.3
% 5.75/1.06 % (236451)Termination reason: Instruction limit
% 5.75/1.06 % (236451)Termination phase: Saturation
% 5.75/1.06 % (236451)Time elapsed: 0.088 s
% 5.75/1.06 % (236451)Peak memory usage: 13 MB
% 5.75/1.06 % (236451)Instructions burned: 180 (million)
% 5.75/1.08 % (236464)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=763690090:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 5.75/1.08 % (236452)Instruction limit reached!
% 5.75/1.08 % (236452)------------------------------
% 5.75/1.08 % (236452)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.75/1.08 % (236452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.75/1.08 % (236452)CaDiCaL version: 2.1.3
% 5.75/1.08 % (236452)Termination reason: Instruction limit
% 5.75/1.08 % (236452)Termination phase: Saturation
% 5.75/1.08 % (236452)Time elapsed: 0.261 s
% 5.75/1.08 % (236452)Peak memory usage: 15 MB
% 5.75/1.08 % (236452)Instructions burned: 479 (million)
% 5.75/1.08 % (236461)Instruction limit reached!
% 5.75/1.08 % (236461)------------------------------
% 5.75/1.08 % (236461)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.75/1.08 % (236461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.75/1.08 % (236461)CaDiCaL version: 2.1.3
% 5.75/1.08 % (236461)Termination reason: Instruction limit
% 5.75/1.08 % (236461)Termination phase: Saturation
% 5.75/1.08 % (236461)Time elapsed: 0.228 s
% 5.75/1.08 % (236461)Peak memory usage: 21 MB
% 5.75/1.08 % (236461)Instructions burned: 693 (million)
% 5.75/1.08 % (236467)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2616136448:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi)
% 5.75/1.08 % (236466)fmb+10_1_sil=64000:random_seed=887773748:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi)
% 5.75/1.08 % (236467)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 5.75/1.08 % (236467)Terminated due to inappropriate strategy.
% 5.75/1.08 % (236467)------------------------------
% 5.75/1.08 % (236467)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.75/1.08 % (236467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.75/1.08 % (236467)CaDiCaL version: 2.1.3
% 5.75/1.08 % (236467)Termination reason: Inappropriate
% 5.75/1.08 % (236467)Time elapsed: 0.006 s
% 5.75/1.08 % (236467)Peak memory usage: 11 MB
% 5.75/1.08 % (236467)Instructions burned: 23 (million)
% 5.75/1.08 % (236467)------------------------------
% 5.75/1.08 % (236467)------------------------------
% 5.75/1.08 % (236466)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 5.75/1.08 % (236466)Terminated due to inappropriate strategy.
% 5.75/1.08 % (236466)------------------------------
% 5.75/1.08 % (236466)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.75/1.08 % (236466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.75/1.08 % (236466)CaDiCaL version: 2.1.3
% 5.75/1.08 % (236466)Termination reason: Inappropriate
% 5.75/1.08 % (236466)Time elapsed: 0.012 s
% 5.75/1.08 % (236466)Peak memory usage: 11 MB
% 5.75/1.08 % (236466)Instructions burned: 25 (million)
% 5.75/1.08 % (236470)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1291049693:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi)
% 5.75/1.08 % (236466)------------------------------
% 5.75/1.08 % (236466)------------------------------
% 5.75/1.08 % (236470)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 5.75/1.08 % (236470)Terminated due to inappropriate strategy.
% 5.75/1.08 % (236470)------------------------------
% 5.75/1.08 % (236470)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.75/1.08 % (236470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.75/1.08 % (236470)CaDiCaL version: 2.1.3
% 5.75/1.08 % (236470)Termination reason: Inappropriate
% 5.75/1.08 % (236470)Time elapsed: 0.006 s
% 5.75/1.08 % (236470)Peak memory usage: 11 MB
% 5.75/1.08 % (236470)Instructions burned: 24 (million)
% 5.75/1.08 % (236470)------------------------------
% 5.75/1.08 % (236470)------------------------------
% 5.75/1.08 % (236473)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=91429135:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi)
% 5.75/1.08 % (236472)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3503632856:i=5131_2995 on theBenchmark for (2995ds/5131Mi)
% 5.75/1.08 % (236450)Instruction limit reached!
% 5.75/1.08 % (236450)------------------------------
% 5.75/1.08 % (236450)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.75/1.08 % (236450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.75/1.08 % (236450)CaDiCaL version: 2.1.3
% 5.75/1.08 % (236450)Termination reason: Instruction limit
% 5.75/1.08 % (236450)Termination phase: Saturation
% 5.75/1.08 % (236450)Time elapsed: 0.387 s
% 5.75/1.08 % (236450)Peak memory usage: 19 MB
% 5.75/1.08 % (236450)Instructions burned: 685 (million)
% 5.75/1.08 % (236476)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3756183397:i=6324_2995 on theBenchmark for (2995ds/6324Mi)
% 5.75/1.08 % (236476)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 5.75/1.08 % (236476)Terminated due to inappropriate strategy.
% 5.75/1.08 % (236476)------------------------------
% 5.75/1.08 % (236476)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.75/1.08 % (236476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.75/1.08 % (236476)CaDiCaL version: 2.1.3
% 5.75/1.08 % (236476)Termination reason: Inappropriate
% 5.75/1.08 % (236476)Time elapsed: 0.015 s
% 5.75/1.08 % (236476)Peak memory usage: 11 MB
% 5.75/1.08 % (236476)Instructions burned: 31 (million)
% 5.75/1.08 % (236476)------------------------------
% 5.75/1.08 % (236476)------------------------------
% 5.75/1.08 % (236478)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3208066183:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi)
% 5.75/1.08 % (236478)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 5.75/1.08 % (236478)Terminated due to inappropriate strategy.
% 5.75/1.08 % (236478)------------------------------
% 5.75/1.08 % (236478)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.75/1.08 % (236478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.75/1.08 % (236478)CaDiCaL version: 2.1.3
% 5.75/1.08 % (236478)Termination reason: Inappropriate
% 5.75/1.08 % (236478)Time elapsed: 0.012 s
% 5.75/1.08 % (236478)Peak memory usage: 11 MB
% 5.75/1.08 % (236478)Instructions burned: 24 (million)
% 5.75/1.08 % (236478)------------------------------
% 5.75/1.08 % (236478)------------------------------
% 5.75/1.08 % (236480)ott-2_1_sil=16000:newcnf=on:random_seed=3928254510:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi)
% 5.75/1.08 % (236464)Instruction limit reached!
% 5.75/1.08 % (236464)------------------------------
% 5.75/1.08 % (236464)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.75/1.08 % (236464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.75/1.08 % (236464)CaDiCaL version: 2.1.3
% 5.75/1.08 % (236464)Termination reason: Instruction limit
% 5.75/1.08 % (236464)Termination phase: Saturation
% 5.75/1.08 % (236464)Time elapsed: 0.468 s
% 5.75/1.08 % (236464)Peak memory usage: 20 MB
% 5.75/1.08 % (236464)Instructions burned: 879 (million)
% 5.75/1.08 % (236482)ott+10_1_sil=32000:tgt=ground:random_seed=3035469465:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi)
% 5.75/1.08 % (236473)Instruction limit reached!
% 5.75/1.08 % (236473)------------------------------
% 5.75/1.08 % (236473)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.75/1.08 % (236473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.75/1.08 % (236473)CaDiCaL version: 2.1.3
% 5.75/1.08 % (236473)Termination reason: Instruction limit
% 5.75/1.08 % (236473)Termination phase: Saturation
% 5.75/1.08 % (236473)Time elapsed: 0.391 s
% 5.75/1.08 % (236473)Peak memory usage: 27 MB
% 5.75/1.08 % (236473)Instructions burned: 1474 (million)
% 5.75/1.08 % (236458)Instruction limit reached!
% 5.75/1.08 % (236458)------------------------------
% 5.75/1.08 % (236458)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.75/1.08 % (236458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.75/1.08 % (236458)CaDiCaL version: 2.1.3
% 5.75/1.08 % (236458)Termination reason: Instruction limit
% 5.75/1.08 % (236458)Termination phase: Saturation
% 5.75/1.08 % (236458)Time elapsed: 0.687 s
% 5.75/1.08 % (236458)Peak memory usage: 23 MB
% 5.75/1.08 % (236458)Instructions burned: 1181 (million)
% 5.75/1.08 % (236484)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3323717692:i=54282_2991 on theBenchmark for (2991ds/54282Mi)
% 5.75/1.08 % (236484)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 5.75/1.08 % (236484)Terminated due to inappropriate strategy.
% 5.75/1.08 % (236484)------------------------------
% 5.75/1.08 % (236484)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.75/1.08 % (236484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.75/1.08 % (236484)CaDiCaL version: 2.1.3
% 5.75/1.08 % (236484)Termination reason: Inappropriate
% 5.75/1.08 % (236484)Time elapsed: 0.008 s
% 5.75/1.08 % (236484)Peak memory usage: 11 MB
% 5.75/1.08 % (236484)Instructions burned: 31 (million)
% 5.75/1.08 % (236484)------------------------------
% 5.75/1.08 % (236484)------------------------------
% 5.75/1.08 % (236482) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-236427-236482"...
% 5.75/1.08 % (236486)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1752004487:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi)
% 5.75/1.08 % (236487)dis+21_1_sil=32000:sas=cadical:random_seed=100473883:i=3773:amm=off_2991 on theBenchmark for (2991ds/3773Mi)
% 5.75/1.08 % (236482)...printing done.
% 5.75/1.08 % (236482)Refutation found. Thanks to Tanya!
% 5.75/1.08 % SZS status Theorem for theBenchmark
% 5.75/1.08 % SZS output start Proof for theBenchmark
% 5.75/1.08 tff(type_def_5, type, set_0: $tType).
% 5.75/1.08 tff(type_def_6, type, set_2: $tType).
% 5.75/1.08 tff(type_def_7, type, set_3: $tType).
% 5.75/1.08 tff(type_def_8, type, set_4: $tType).
% 5.75/1.08 tff(func_def_0, type, min_int: $int).
% 5.75/1.08 tff(func_def_1, type, max_int: $int).
% 5.75/1.08 tff(func_def_5, type, g_s0_0: set_0).
% 5.75/1.08 tff(func_def_6, type, g_s1_1: $int).
% 5.75/1.08 tff(func_def_7, type, g_s2_2: $int).
% 5.75/1.08 tff(func_def_8, type, g_s3_3: set_0).
% 5.75/1.08 tff(func_def_9, type, g_s4_4: $int).
% 5.75/1.08 tff(func_def_10, type, g_s5_5: $int).
% 5.75/1.08 tff(func_def_11, type, g_s6_6: set_0).
% 5.75/1.08 tff(func_def_12, type, g_s7_7: $int).
% 5.75/1.08 tff(func_def_13, type, g_s8_8: $int).
% 5.75/1.08 tff(func_def_14, type, g_s9_9: set_0).
% 5.75/1.08 tff(func_def_15, type, g_s10_10: $int).
% 5.75/1.08 tff(func_def_16, type, g_s11_11: $int).
% 5.75/1.08 tff(func_def_17, type, g_s12_12: $int).
% 5.75/1.08 tff(func_def_18, type, g_s13_13: $int).
% 5.75/1.08 tff(func_def_19, type, g_s14_14: $int).
% 5.75/1.08 tff(func_def_20, type, g_s15_15: $int).
% 5.75/1.08 tff(func_def_21, type, g_s16_16: $int).
% 5.75/1.08 tff(func_def_22, type, g_s17_17: $int).
% 5.75/1.08 tff(func_def_23, type, g_s18_18: $int).
% 5.75/1.08 tff(func_def_24, type, g_s20_19: set_0).
% 5.75/1.08 tff(func_def_25, type, g_s19_20: $int).
% 5.75/1.08 tff(func_def_26, type, g_s22_21: set_0).
% 5.75/1.08 tff(func_def_27, type, g_s21_22: $int).
% 5.75/1.08 tff(func_def_28, type, g_s24_23: set_0).
% 5.75/1.08 tff(func_def_29, type, g_s23_24: $int).
% 5.75/1.08 tff(func_def_30, type, g_s25_25: $int).
% 5.75/1.08 tff(func_def_31, type, g_s26_26: $int).
% 5.75/1.08 tff(func_def_32, type, g_s27_27: set_0).
% 5.75/1.08 tff(func_def_33, type, set_2_empty: set_2).
% 5.75/1.08 tff(func_def_34, type, set_2_insert: set_2 > set_2).
% 5.75/1.08 tff(func_def_35, type, g_s28_28: set_2).
% 5.75/1.08 tff(func_def_36, type, g_s29_29: $int).
% 5.75/1.08 tff(func_def_37, type, g_s30_30: $int).
% 5.75/1.08 tff(func_def_38, type, g_s31_31: $int).
% 5.75/1.08 tff(func_def_39, type, g_s32_32: $int).
% 5.75/1.08 tff(func_def_40, type, g_s33_33: $int).
% 5.75/1.08 tff(func_def_41, type, g_s34_34: $int).
% 5.75/1.08 tff(func_def_42, type, g_s35_35: $int).
% 5.75/1.08 tff(func_def_43, type, g_s36_36: $int).
% 5.75/1.08 tff(func_def_44, type, g_s37_37: $int).
% 5.75/1.08 tff(func_def_45, type, g_s38_38: $int).
% 5.75/1.08 tff(func_def_46, type, g_s39_39: $int).
% 5.75/1.08 tff(func_def_47, type, g_s40_40: $int).
% 5.75/1.08 tff(func_def_48, type, g_s41_41: $int).
% 5.75/1.08 tff(func_def_49, type, g_s42_42: $int).
% 5.75/1.08 tff(func_def_50, type, g_s43_43: $int).
% 5.75/1.08 tff(func_def_51, type, g_s44_44: $int).
% 5.75/1.08 tff(func_def_52, type, g_s45_45: $int).
% 5.75/1.08 tff(func_def_53, type, g_s46_46: $int).
% 5.75/1.08 tff(func_def_54, type, g_s47_47: $int).
% 5.75/1.08 tff(func_def_55, type, g_s48_48: $int).
% 5.75/1.08 tff(func_def_56, type, g_s49_49: $int).
% 5.75/1.08 tff(func_def_57, type, g_s50_50: $int).
% 5.75/1.08 tff(func_def_58, type, g_s51_51: $int).
% 5.75/1.08 tff(func_def_59, type, g_s52_52: $int).
% 5.75/1.08 tff(func_def_60, type, g_s53_53: $int).
% 5.75/1.08 tff(func_def_61, type, g_s54_54: $int).
% 5.75/1.08 tff(func_def_62, type, g_s55_55: $int).
% 5.75/1.08 tff(func_def_63, type, g_s56_56: $int).
% 5.75/1.08 tff(func_def_64, type, g_s57_57: $int).
% 5.75/1.08 tff(func_def_65, type, g_s58_58: $int).
% 5.75/1.08 tff(func_def_66, type, g_s59_59: $int).
% 5.75/1.08 tff(func_def_67, type, g_s60_60: $int).
% 5.75/1.08 tff(func_def_68, type, g_s61_61: $int).
% 5.75/1.08 tff(func_def_69, type, g_s62_62: $int).
% 5.75/1.08 tff(func_def_70, type, g_s63_63: $int).
% 5.75/1.08 tff(func_def_71, type, g_s64_64: $int).
% 5.75/1.08 tff(func_def_72, type, g_s65_65: $int).
% 5.75/1.08 tff(func_def_73, type, g_s66_66: $int).
% 5.75/1.08 tff(func_def_74, type, g_s67_67: $int).
% 5.75/1.08 tff(func_def_75, type, g_s68_68: $int).
% 5.75/1.08 tff(func_def_76, type, g_s69_69: $int).
% 5.75/1.08 tff(func_def_77, type, g_s70_70: $int).
% 5.75/1.08 tff(func_def_78, type, g_s71_71: $int).
% 5.75/1.08 tff(func_def_79, type, g_s72_72: $int).
% 5.75/1.08 tff(func_def_80, type, g_s73_73: $int).
% 5.75/1.08 tff(func_def_81, type, g_s74_74: $int).
% 5.75/1.08 tff(func_def_82, type, g_s75_75: $int).
% 5.75/1.08 tff(func_def_83, type, g_s76_76: $int).
% 5.75/1.08 tff(func_def_84, type, g_s77_77: $int).
% 5.75/1.08 tff(func_def_85, type, g_s78_78: $int).
% 5.75/1.08 tff(func_def_86, type, g_s79_79: $int).
% 5.75/1.08 tff(func_def_87, type, g_s80_80: $int).
% 5.75/1.08 tff(func_def_88, type, g_s81_81: $int).
% 5.75/1.08 tff(func_def_89, type, g_s82_82: $int).
% 5.75/1.08 tff(func_def_90, type, g_s83_83: $int).
% 5.75/1.08 tff(func_def_91, type, g_s84_84: $int).
% 5.75/1.08 tff(func_def_92, type, g_s85_85: $int).
% 5.75/1.08 tff(func_def_93, type, g_s86_86: $int).
% 5.75/1.08 tff(func_def_94, type, g_s87_87: $int).
% 5.75/1.08 tff(func_def_95, type, g_s88_88: $int).
% 5.75/1.08 tff(func_def_96, type, g_s89_89: $int).
% 5.75/1.08 tff(func_def_97, type, g_s90_90: $int).
% 5.75/1.08 tff(func_def_98, type, g_s91_91: $int).
% 5.75/1.08 tff(func_def_99, type, g_s92_92: $int).
% 5.75/1.08 tff(func_def_100, type, g_s93_93: $int).
% 5.75/1.08 tff(func_def_101, type, g_s94_94: $int).
% 5.75/1.08 tff(func_def_102, type, g_s95_95: $int).
% 5.75/1.08 tff(func_def_103, type, g_s96_96: $int).
% 5.75/1.08 tff(func_def_104, type, g_s97_97: $int).
% 5.75/1.08 tff(func_def_105, type, g_s98_98: $int).
% 5.75/1.08 tff(func_def_106, type, g_s99_99: $int).
% 5.75/1.08 tff(func_def_107, type, g_s100_100: $int).
% 5.75/1.08 tff(func_def_108, type, g_s101_101: $int).
% 5.75/1.08 tff(func_def_109, type, g_s102_102: $int).
% 5.75/1.08 tff(func_def_110, type, g_s103_103: $int).
% 5.75/1.08 tff(func_def_111, type, g_s104_104: $int).
% 5.75/1.08 tff(func_def_112, type, g_s105_105: $int).
% 5.75/1.08 tff(func_def_113, type, g_s106_106: $int).
% 5.75/1.08 tff(func_def_114, type, g_s107_107: $int).
% 5.75/1.08 tff(func_def_115, type, g_s108_108: $int).
% 5.75/1.08 tff(func_def_116, type, g_s109_109: $int).
% 5.75/1.08 tff(func_def_117, type, g_s110_110: $int).
% 5.75/1.08 tff(func_def_118, type, g_s111_111: $int).
% 5.75/1.08 tff(func_def_119, type, g_s112_112: $int).
% 5.75/1.08 tff(func_def_120, type, g_s113_113: $int).
% 5.75/1.08 tff(func_def_121, type, g_s114_114: $int).
% 5.75/1.08 tff(func_def_122, type, g_s115_115: $int).
% 5.75/1.08 tff(func_def_123, type, g_s116_116: $int).
% 5.75/1.08 tff(func_def_124, type, g_s117_117: $int).
% 5.75/1.08 tff(func_def_125, type, g_s118_118: $int).
% 5.75/1.08 tff(func_def_126, type, g_s119_119: $int).
% 5.75/1.08 tff(func_def_127, type, g_s120_120: $int).
% 5.75/1.08 tff(func_def_128, type, g_s121_121: $int).
% 5.75/1.08 tff(func_def_129, type, g_s122_123: set_0).
% 5.75/1.08 tff(func_def_130, type, set_3_empty: set_3).
% 5.75/1.08 tff(func_def_131, type, set_3_insert: set_3 > set_3).
% 5.75/1.08 tff(func_def_132, type, g_s123_124: set_3).
% 5.75/1.08 tff(func_def_133, type, g_s124_125: set_3).
% 5.75/1.08 tff(func_def_134, type, g_s125_126: set_3).
% 5.75/1.08 tff(func_def_135, type, g_s126_127: set_3).
% 5.75/1.08 tff(func_def_136, type, g_s127_128: set_3).
% 5.75/1.08 tff(func_def_137, type, g_s128_129: set_3).
% 5.75/1.08 tff(func_def_138, type, g_s129_130: set_3).
% 5.75/1.08 tff(func_def_139, type, g_s130_131: set_3).
% 5.75/1.08 tff(func_def_140, type, g_s131_132: set_3).
% 5.75/1.08 tff(func_def_141, type, g_s132_133: set_3).
% 5.75/1.08 tff(func_def_142, type, g_s133_134: set_3).
% 5.75/1.08 tff(func_def_143, type, set_4_empty: set_4).
% 5.75/1.08 tff(func_def_144, type, set_4_insert: set_4 > set_4).
% 5.75/1.08 tff(func_def_145, type, g_s134_135: set_4).
% 5.75/1.08 tff(func_def_146, type, g_s135_136: set_3).
% 5.75/1.08 tff(func_def_147, type, g_s136_137: set_3).
% 5.75/1.08 tff(func_def_148, type, g_s137_138: set_0).
% 5.75/1.08 tff(func_def_149, type, g_s138_139: set_0).
% 5.75/1.08 tff(func_def_150, type, g_s139_140: set_0).
% 5.75/1.08 tff(func_def_151, type, g_s140_141: set_0).
% 5.75/1.08 tff(func_def_152, type, g_s141_142: set_0).
% 5.75/1.08 tff(func_def_153, type, g_s122_1_143: set_0).
% 5.75/1.08 tff(func_def_154, type, g_s139_1_144: set_0).
% 5.75/1.08 tff(func_def_155, type, g_s137_1_145: set_0).
% 5.75/1.08 tff(func_def_156, type, g_s138_1_146: set_0).
% 5.75/1.08 tff(func_def_157, type, g_s136_1_147: set_3).
% 5.75/1.08 tff(func_def_158, type, g_s143_1_148: set_0).
% 5.75/1.08 tff(func_def_159, type, g_s144_1_149: set_0).
% 5.75/1.08 tff(func_def_160, type, g_s145_1_150: set_0).
% 5.75/1.08 tff(func_def_161, type, g_s146_1_151: set_0).
% 5.75/1.08 tff(func_def_162, type, g_s147_1_152: set_0).
% 5.75/1.08 tff(func_def_163, type, g_s148_1_153: set_0).
% 5.75/1.08 tff(func_def_164, type, g_s149_1_154: set_0).
% 5.75/1.08 tff(func_def_165, type, g_s150_1_155: set_0).
% 5.75/1.08 tff(func_def_166, type, g_s151_1_156: set_0).
% 5.75/1.08 tff(func_def_167, type, g_s152_1_157: set_0).
% 5.75/1.08 tff(func_def_168, type, g_s153_1_158: set_0).
% 5.75/1.08 tff(func_def_169, type, g_s154_1_159: set_3).
% 5.75/1.08 tff(func_def_170, type, g_s155_1_160: set_3).
% 5.75/1.08 tff(func_def_171, type, g_s156_1_161: set_3).
% 5.75/1.08 tff(func_def_172, type, g_s157_1_162: set_3).
% 5.75/1.08 tff(func_def_173, type, g_s158_1_163: set_3).
% 5.75/1.08 tff(func_def_174, type, g_s159_1_164: set_3).
% 5.75/1.08 tff(func_def_175, type, g_s160_1_165: set_3).
% 5.75/1.08 tff(func_def_176, type, g_s161_1_166: set_3).
% 5.75/1.08 tff(func_def_177, type, g_s165_167: $int).
% 5.75/1.08 tff(func_def_178, type, g_s166_168: $int).
% 5.75/1.08 tff(func_def_179, type, g_s167_169: $int).
% 5.75/1.08 tff(func_def_180, type, g_s168_170: $int).
% 5.75/1.08 tff(func_def_181, type, g_s142_122: $int).
% 5.75/1.08 tff(func_def_193, type, bG0: $o > $o).
% 5.75/1.08 tff(func_def_194, type, bG1: $o > $o).
% 5.75/1.08 tff(func_def_195, type, bG2: $o > $o).
% 5.75/1.08 tff(func_def_196, type, bG3: $o > $o).
% 5.75/1.08 tff(func_def_197, type, bG4: $o > $o).
% 5.75/1.08 tff(func_def_198, type, bG5: $o > $o).
% 5.75/1.08 tff(func_def_199, type, bG6: $o > $o).
% 5.75/1.08 tff(func_def_200, type, bG7: $o > $o).
% 5.75/1.08 tff(func_def_201, type, bG8: $o > $o).
% 5.75/1.08 tff(func_def_202, type, bG9: $o > $o).
% 5.75/1.08 tff(func_def_203, type, sK12: set_3).
% 5.75/1.08 tff(func_def_204, type, sK13: $int > $int).
% 5.75/1.08 tff(func_def_205, type, sK14: set_3).
% 5.75/1.08 tff(func_def_206, type, sK15: $int > $int).
% 5.75/1.08 tff(func_def_207, type, sK16: set_3).
% 5.75/1.08 tff(func_def_208, type, sK17: $int > $int).
% 5.75/1.08 tff(func_def_209, type, sK18: set_3).
% 5.75/1.08 tff(func_def_210, type, sK19: $int > $int).
% 5.75/1.08 tff(func_def_211, type, sK20: set_3).
% 5.75/1.08 tff(func_def_212, type, sK21: $int > $int).
% 5.75/1.08 tff(func_def_213, type, sK22: set_3).
% 5.75/1.08 tff(func_def_214, type, sK23: $int > $int).
% 5.75/1.08 tff(func_def_215, type, sK24: set_3).
% 5.75/1.08 tff(func_def_216, type, sK25: $int > $int).
% 5.75/1.08 tff(func_def_217, type, sK26: set_3).
% 5.75/1.08 tff(func_def_218, type, sK27: $int > $int).
% 5.75/1.08 tff(func_def_219, type, sK28: set_3).
% 5.75/1.08 tff(func_def_220, type, sK29: $int > $int).
% 5.75/1.08 tff(func_def_221, type, sK30: set_3).
% 5.75/1.08 tff(func_def_222, type, sK31: $int > $int).
% 5.75/1.08 tff(func_def_223, type, sK32: set_3).
% 5.75/1.08 tff(func_def_224, type, sK33: $int > $int).
% 5.75/1.08 tff(func_def_225, type, sK34: set_3).
% 5.75/1.08 tff(func_def_226, type, sK35: $int > $int).
% 5.75/1.08 tff(func_def_227, type, sK36: set_3).
% 5.75/1.08 tff(func_def_228, type, sK37: $int > $int).
% 5.75/1.08 tff(func_def_229, type, sK38: set_3).
% 5.75/1.08 tff(func_def_230, type, sK39: $int > $int).
% 5.75/1.08 tff(func_def_231, type, sK40: set_3).
% 5.75/1.08 tff(func_def_232, type, sK41: $int > $int).
% 5.75/1.08 tff(func_def_233, type, sK42: set_3).
% 5.75/1.08 tff(func_def_234, type, sK43: $int > $int).
% 5.75/1.08 tff(func_def_235, type, sK44: set_3).
% 5.75/1.08 tff(func_def_236, type, sK45: $int > $int).
% 5.75/1.08 tff(func_def_237, type, sK46: set_3).
% 5.75/1.08 tff(func_def_238, type, sK47: $int > $int).
% 5.75/1.08 tff(func_def_239, type, sK48: set_3).
% 5.75/1.08 tff(func_def_240, type, sK49: $int > $int).
% 5.75/1.08 tff(func_def_241, type, sK50: set_3).
% 5.75/1.08 tff(func_def_242, type, sK51: $int > $int).
% 5.75/1.08 tff(func_def_243, type, sK52: set_3).
% 5.75/1.08 tff(func_def_244, type, sK53: $int > $int).
% 5.75/1.08 tff(func_def_245, type, sK54: set_3).
% 5.75/1.08 tff(func_def_246, type, sK55: $int > $int).
% 5.75/1.08 tff(func_def_247, type, sK56: set_3).
% 5.75/1.08 tff(func_def_248, type, sK57: $int > $int).
% 5.75/1.08 tff(func_def_249, type, sK58: set_3).
% 5.75/1.08 tff(func_def_250, type, sK59: $int > $int).
% 5.75/1.08 tff(func_def_251, type, sK60: set_3).
% 5.75/1.08 tff(func_def_252, type, sK61: $int > $int).
% 5.75/1.08 tff(func_def_253, type, sK62: set_3).
% 5.75/1.08 tff(func_def_254, type, sK63: $int > $int).
% 5.75/1.08 tff(func_def_255, type, sK64: $int > $int).
% 5.75/1.08 tff(func_def_256, type, sK65: $int > $int).
% 5.75/1.08 tff(func_def_257, type, sK66: $int > $int).
% 5.75/1.08 tff(func_def_258, type, sK67: ($int * $int) > $int).
% 5.75/1.08 tff(func_def_259, type, sK68: $int > $int).
% 5.75/1.08 tff(func_def_260, type, sK69: $int > $int).
% 5.75/1.08 tff(func_def_261, type, sK70: $int > $int).
% 5.75/1.08 tff(func_def_262, type, sK71: $int > $int).
% 5.75/1.08 tff(func_def_263, type, sK72: ($int * $int) > $int).
% 5.75/1.08 tff(func_def_264, type, sK73: $int > $int).
% 5.75/1.08 tff(func_def_265, type, sK74: $int > $int).
% 5.75/1.08 tff(func_def_266, type, sK75: $int > $int).
% 5.75/1.08 tff(func_def_267, type, sK76: $int > $int).
% 5.75/1.08 tff(func_def_268, type, sK77: ($int * $int) > $int).
% 5.75/1.08 tff(func_def_269, type, sK78: ($int * $int) > $int).
% 5.75/1.08 tff(func_def_270, type, sK79: ($int * $int) > $int).
% 5.75/1.08 tff(func_def_271, type, sK80: ($int * $int) > $int).
% 5.75/1.08 tff(func_def_272, type, sK81: ($int * $int) > $int).
% 5.75/1.08 tff(func_def_273, type, sK82: ($int * $int) > $int).
% 5.75/1.08 tff(func_def_274, type, sK83: $int > $int).
% 5.75/1.08 tff(func_def_275, type, sK84: ($int * $int) > $int).
% 5.75/1.08 tff(func_def_276, type, sK85: ($int * $int) > $int).
% 5.75/1.08 tff(func_def_277, type, sK86: ($int * $int) > $int).
% 5.75/1.08 tff(func_def_278, type, sK87: ($int * $int) > $int).
% 5.75/1.08 tff(func_def_279, type, sK88: ($int * $int) > $int).
% 5.75/1.08 tff(func_def_280, type, sK89: $int > $int).
% 5.75/1.08 tff(func_def_281, type, sK90: ($int * $int) > $int).
% 5.75/1.08 tff(func_def_282, type, sK91: ($int * $int) > $int).
% 5.75/1.08 tff(func_def_283, type, sK92: ($int * $int) > $int).
% 5.75/1.08 tff(func_def_284, type, sK93: $int > $int).
% 5.75/1.08 tff(func_def_285, type, sK94: ($int * $int) > $int).
% 5.75/1.08 tff(func_def_286, type, sK95: ($int * $int) > $int).
% 5.75/1.08 tff(func_def_287, type, sK96: ($int * $int) > $int).
% 5.75/1.08 tff(func_def_288, type, sK97: $int > $int).
% 5.75/1.08 tff(func_def_289, type, sK98: ($int * $int) > $int).
% 5.75/1.08 tff(func_def_290, type, sK99: ($int * $int) > $int).
% 5.75/1.08 tff(func_def_291, type, sK100: ($int * $int) > $int).
% 5.75/1.08 tff(func_def_292, type, sK101: ($int * $int) > $int).
% 5.75/1.08 tff(func_def_293, type, sK102: ($int * $int) > $int).
% 5.75/1.08 tff(func_def_294, type, sK103: $int > $int).
% 5.75/1.08 tff(func_def_295, type, sK104: ($int * $int) > $int).
% 5.75/1.08 tff(func_def_296, type, sK105: ($int * $int) > $int).
% 5.75/1.08 tff(func_def_297, type, sK106: ($int * $int) > $int).
% 5.75/1.08 tff(func_def_298, type, sK107: ($int * $int) > $int).
% 5.75/1.08 tff(func_def_299, type, sK108: ($int * $int) > $int).
% 5.75/1.08 tff(func_def_300, type, sK109: $int > $int).
% 5.75/1.08 tff(func_def_301, type, sK110: $int > $int).
% 5.75/1.08 tff(func_def_302, type, sK111: $int).
% 5.75/1.08 tff(func_def_303, type, sK112: $int).
% 5.75/1.08 tff(func_def_304, type, sK113: $int).
% 5.75/1.08 tff(func_def_305, type, sK114: $int).
% 5.75/1.08 tff(func_def_306, type, sK115: $int > $int).
% 5.75/1.08 tff(func_def_307, type, sF116: $int).
% 5.75/1.08 tff(pred_def_1, type, mem0: ($int * set_0) > $o).
% 5.75/1.08 tff(pred_def_2, type, mem2: ($o * $int * set_2) > $o).
% 5.75/1.08 tff(pred_def_3, type, mem3: ($int * $int * set_3) > $o).
% 5.75/1.08 tff(pred_def_4, type, mem4: ($int * $int * $int * set_4) > $o).
% 5.75/1.08 tff(pred_def_9, type, sP10: ($int * $int) > $o).
% 5.75/1.08 tff(pred_def_10, type, sP11: $int > $o).
% 5.75/1.08 tff(f6,axiom,(
% 5.75/1.08 ! [X0 : $int,X1 : $int] : (mem3(X1,X0,g_s133_134) => ($greatereq(X1,0) & $lesseq(X1,g_s51_51) & $greatereq(X0,0)))),
% 5.75/1.08 file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Define:abs:11')).
% 5.75/1.08 tff(f94,axiom,(
% 5.75/1.08 ! [X0 : $int] : (mem0(X0,g_s24_23) <=> ($greatereq(X0,0) & $lesseq(X0,255)))),
% 5.75/1.08 file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Define:ctx:19')).
% 5.75/1.08 tff(f136,axiom,(
% 5.75/1.08 $greatereq(g_s56_56,1)),
% 5.75/1.08 file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Define:ctx:57')).
% 5.75/1.08 tff(f213,axiom,(
% 5.75/1.08 ! [X0 : $int] : (($greatereq(X0,0) & $lesseq(X0,g_s51_51)) => ! [X1 : $int] : (mem3(X0,X1,g_s156_1_161) => $lesseq(X1,g_s56_56)))),
% 5.75/1.08 file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Define:inv:36')).
% 5.75/1.08 tff(f227,axiom,(
% 5.75/1.08 ! [X0 : $int] : (($greatereq(X0,0) & $lesseq(X0,g_s51_51)) => ! [X1 : $int,X2 : $int] : ((X2 = X0 & ! [X3 : $int,X4 : $int,X5 : $int] : ((mem3(X0,X3,g_s123_124) & mem3(X0,X4,g_s156_1_161) & mem3(X0,X5,g_s123_124)) => ($greatereq(X1,$sum($sum($difference(X3,g_s56_56),1),X4)) & $lesseq(X1,X5))) & mem3(X2,X1,g_s133_134)) <=> $false))),
% 5.75/1.08 file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Define:inv:49')).
% 5.75/1.08 tff(f246,axiom,(
% 5.75/1.08 $greatereq(g_s165_167,0) & $lesseq(g_s165_167,g_s51_51)),
% 5.75/1.08 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',gh_1_def)).
% 5.75/1.08 tff(f256,axiom,(
% 5.75/1.08 ! [X0 : $int] : (mem3(g_s165_167,X0,g_s156_1_161) => $lesseq(X0,0))),
% 5.75/1.08 file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Local_Hyp:20')).
% 5.75/1.08 tff(f258,axiom,(
% 5.75/1.08 ~ ! [X0 : $int,X1 : $int] : ((X1 = g_s165_167 & ! [X2 : $int,X3 : $int] : ((mem3(g_s165_167,X2,g_s123_124) & mem3(g_s165_167,X3,g_s123_124)) => ($greatereq(X0,$difference($sum(X2,1),g_s56_56)) & $lesseq(X0,$difference($sum(X3,1),1)))) & mem3(X1,X0,g_s133_134)) <=> $false)),
% 5.75/1.08 file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Local_Hyp:12')).
% 5.75/1.08 tff(f259,axiom,(
% 5.75/1.08 $greatereq(g_s142_122,0) & $lesseq(g_s142_122,g_s51_51)),
% 5.75/1.08 file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Local_Hyp:2')).
% 5.75/1.08 tff(f260,conjecture,(
% 5.75/1.08 ! [X0 : $int] : (((g_s142_122 = g_s165_167 & ! [X1 : $int] : (mem3(g_s165_167,X1,g_s156_1_161) => X0 = $difference(X1,1))) | (mem3(g_s142_122,X0,g_s156_1_161) & ~ ? [X2 : $int] : (g_s142_122 = g_s165_167 & ! [X3 : $int] : (mem3(g_s165_167,X3,g_s156_1_161) => X2 = $difference(X3,1))))) => $lesseq(X0,g_s56_56))),
% 5.75/1.08 file('/export/starexec/sandbox2/benchmark/theBenchmark.p','Goal')).
% 5.75/1.08 tff(f261,negated_conjecture,(
% 5.75/1.08 ~ ! [X0 : $int] : (((g_s142_122 = g_s165_167 & ! [X1 : $int] : (mem3(g_s165_167,X1,g_s156_1_161) => X0 = $difference(X1,1))) | (mem3(g_s142_122,X0,g_s156_1_161) & ~ ? [X2 : $int] : (g_s142_122 = g_s165_167 & ! [X3 : $int] : (mem3(g_s165_167,X3,g_s156_1_161) => X2 = $difference(X3,1))))) => $lesseq(X0,g_s56_56))),
% 5.75/1.08 inference(negated_conjecture,[status(cth)],[f260])).
% 5.75/1.08 tff(f265,plain,(
% 5.75/1.08 ! [X0 : $int,X1 : $int] : (mem3(X1,X0,g_s133_134) => (~$less(X1,0) & ~$less(g_s51_51,X1) & ~$less(X0,0)))),
% 5.75/1.08 inference(theory_normalization,[],[f6])).
% 5.75/1.08 tff(f313,plain,(
% 5.75/1.08 ! [X0 : $int] : (mem0(X0,g_s24_23) <=> (~$less(X0,0) & ~$less(255,X0)))),
% 5.75/1.08 inference(theory_normalization,[],[f94])).
% 5.75/1.08 tff(f328,plain,(
% 5.75/1.08 ~$less(g_s56_56,1)),
% 5.75/1.08 inference(theory_normalization,[],[f136])).
% 5.75/1.08 tff(f356,plain,(
% 5.75/1.08 ! [X0 : $int] : ((~$less(X0,0) & ~$less(g_s51_51,X0)) => ! [X1 : $int] : (mem3(X0,X1,g_s156_1_161) => ~$less(g_s56_56,X1)))),
% 5.75/1.08 inference(theory_normalization,[],[f213])).
% 5.75/1.08 tff(f369,plain,(
% 5.75/1.08 ! [X0 : $int] : ((~$less(X0,0) & ~$less(g_s51_51,X0)) => ! [X1 : $int,X2 : $int] : ((X2 = X0 & ! [X3 : $int,X4 : $int,X5 : $int] : ((mem3(X0,X3,g_s123_124) & mem3(X0,X4,g_s156_1_161) & mem3(X0,X5,g_s123_124)) => (~$less(X1,$sum($sum($sum(X3,$uminus(g_s56_56)),1),X4)) & ~$less(X5,X1))) & mem3(X2,X1,g_s133_134)) <=> $false))),
% 5.75/1.08 inference(theory_normalization,[],[f227])).
% 5.75/1.08 tff(f387,plain,(
% 5.75/1.08 ~$less(g_s165_167,0) & ~$less(g_s51_51,g_s165_167)),
% 5.75/1.08 inference(theory_normalization,[],[f246])).
% 5.75/1.08 tff(f390,plain,(
% 5.75/1.08 ! [X0 : $int] : (mem3(g_s165_167,X0,g_s156_1_161) => ~$less(0,X0))),
% 5.75/1.08 inference(theory_normalization,[],[f256])).
% 5.75/1.08 tff(f392,plain,(
% 5.75/1.08 ~ ! [X0 : $int,X1 : $int] : ((X1 = g_s165_167 & ! [X2 : $int,X3 : $int] : ((mem3(g_s165_167,X2,g_s123_124) & mem3(g_s165_167,X3,g_s123_124)) => (~$less(X0,$sum($sum(X2,1),$uminus(g_s56_56))) & ~$less($sum($sum(X3,1),$uminus(1)),X0))) & mem3(X1,X0,g_s133_134)) <=> $false)),
% 5.75/1.08 inference(theory_normalization,[],[f258])).
% 5.75/1.08 tff(f393,plain,(
% 5.75/1.08 ~$less(g_s142_122,0) & ~$less(g_s51_51,g_s142_122)),
% 5.75/1.08 inference(theory_normalization,[],[f259])).
% 5.75/1.08 tff(f394,plain,(
% 5.75/1.08 ~ ! [X0 : $int] : (((g_s142_122 = g_s165_167 & ! [X1 : $int] : (mem3(g_s165_167,X1,g_s156_1_161) => $sum(X1,$uminus(1)) = X0)) | (mem3(g_s142_122,X0,g_s156_1_161) & ~ ? [X2 : $int] : (g_s142_122 = g_s165_167 & ! [X3 : $int] : (mem3(g_s165_167,X3,g_s156_1_161) => $sum(X3,$uminus(1)) = X2)))) => ~$less(g_s56_56,X0))),
% 5.75/1.08 inference(theory_normalization,[],[f261])).
% 5.75/1.08 tff(f395,definition,(
% 5.75/1.08 ( ! [X0 : $int,X1 : $int] : ($sum(X0,X1) = $sum(X1,X0)) )),
% 5.75/1.08 introduced(theory,[tha_commutativity])).
% 5.75/1.08 tff(f396,definition,(
% 5.75/1.08 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($sum(X0,$sum(X1,X2)) = $sum($sum(X0,X1),X2)) )),
% 5.75/1.08 introduced(theory,[tha_associativity])).
% 5.75/1.08 tff(f397,definition,(
% 5.75/1.08 ( ! [X0 : $int] : ($sum(X0,0) = X0) )),
% 5.75/1.08 introduced(theory,[tha_right_identity])).
% 5.75/1.08 tff(f399,definition,(
% 5.75/1.08 ( ! [X0 : $int] : (0 = $sum(X0,$uminus(X0))) )),
% 5.75/1.08 introduced(theory,[tha_inverse_op_unit])).
% 5.75/1.08 tff(f400,definition,(
% 5.75/1.08 ( ! [X0 : $int] : (~$less(X0,X0)) )),
% 5.75/1.08 introduced(theory,[tha_non-reflexivity])).
% 5.75/1.08 tff(f401,definition,(
% 5.75/1.08 ( ! [X2 : $int,X0 : $int,X1 : $int] : (~$less(X1,X2) | ~$less(X0,X1) | $less(X0,X2)) )),
% 5.75/1.08 introduced(theory,[tha_transitivity])).
% 5.75/1.08 tff(f402,definition,(
% 5.75/1.08 ( ! [X0 : $int,X1 : $int] : ($less(X1,X0) | $less(X0,X1) | X0 = X1) )),
% 5.75/1.08 introduced(theory,[tha_order_totality])).
% 5.75/1.08 tff(f403,definition,(
% 5.75/1.08 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($less($sum(X0,X2),$sum(X1,X2)) | ~$less(X0,X1)) )),
% 5.75/1.08 introduced(theory,[tha_order_monotonicity])).
% 5.75/1.08 tff(f404,definition,(
% 5.75/1.08 ( ! [X0 : $int,X1 : $int] : ($less(X1,$sum(X0,1)) | $less(X0,X1)) )),
% 5.75/1.08 introduced(theory,[tha_order_plus_one_dichotomy])).
% 5.75/1.08 tff(f451,plain,(
% 5.75/1.08 ! [X0 : $int] : ((~$less(X0,0) & ~$less(g_s51_51,X0)) => ! [X1 : $int,X2 : $int] : ~(X2 = X0 & ! [X3 : $int,X4 : $int,X5 : $int] : ((mem3(X0,X3,g_s123_124) & mem3(X0,X4,g_s156_1_161) & mem3(X0,X5,g_s123_124)) => (~$less(X1,$sum($sum($sum(X3,$uminus(g_s56_56)),1),X4)) & ~$less(X5,X1))) & mem3(X2,X1,g_s133_134)))),
% 5.75/1.08 inference(true_and_false_elimination,[],[f369])).
% 5.75/1.08 tff(f456,plain,(
% 5.75/1.08 ~ ! [X0 : $int,X1 : $int] : ~(X1 = g_s165_167 & ! [X2 : $int,X3 : $int] : ((mem3(g_s165_167,X2,g_s123_124) & mem3(g_s165_167,X3,g_s123_124)) => (~$less(X0,$sum($sum(X2,1),$uminus(g_s56_56))) & ~$less($sum($sum(X3,1),$uminus(1)),X0))) & mem3(X1,X0,g_s133_134))),
% 5.75/1.08 inference(true_and_false_elimination,[],[f392])).
% 5.75/1.08 tff(f461,plain,(
% 5.75/1.08 ! [X0 : $int,X1 : $int] : ((~$less(X1,0) & ~$less(g_s51_51,X1) & ~$less(X0,0)) | ~mem3(X1,X0,g_s133_134))),
% 5.75/1.08 inference(ennf_transformation,[],[f265])).
% 5.75/1.08 tff(f552,plain,(
% 5.75/1.08 ! [X0 : $int] : (! [X1 : $int] : (~$less(g_s56_56,X1) | ~mem3(X0,X1,g_s156_1_161)) | ($less(X0,0) | $less(g_s51_51,X0)))),
% 5.75/1.08 inference(ennf_transformation,[],[f356])).
% 5.75/1.08 tff(f553,plain,(
% 5.75/1.08 ! [X0 : $int] : (! [X1 : $int] : (~$less(g_s56_56,X1) | ~mem3(X0,X1,g_s156_1_161)) | $less(X0,0) | $less(g_s51_51,X0))),
% 5.75/1.08 inference(flattening,[],[f552])).
% 5.75/1.08 tff(f568,plain,(
% 5.75/1.08 ! [X0 : $int] : (! [X1 : $int,X2 : $int] : (X0 != X2 | ? [X3 : $int,X4 : $int,X5 : $int] : (($less(X1,$sum($sum($sum(X3,$uminus(g_s56_56)),1),X4)) | $less(X5,X1)) & (mem3(X0,X3,g_s123_124) & mem3(X0,X4,g_s156_1_161) & mem3(X0,X5,g_s123_124))) | ~mem3(X2,X1,g_s133_134)) | ($less(X0,0) | $less(g_s51_51,X0)))),
% 5.75/1.08 inference(ennf_transformation,[],[f451])).
% 5.75/1.08 tff(f569,plain,(
% 5.75/1.08 ! [X0 : $int] : (! [X1 : $int,X2 : $int] : (X0 != X2 | ? [X3 : $int,X4 : $int,X5 : $int] : (($less(X1,$sum($sum($sum(X3,$uminus(g_s56_56)),1),X4)) | $less(X5,X1)) & mem3(X0,X3,g_s123_124) & mem3(X0,X4,g_s156_1_161) & mem3(X0,X5,g_s123_124)) | ~mem3(X2,X1,g_s133_134)) | $less(X0,0) | $less(g_s51_51,X0))),
% 5.75/1.08 inference(flattening,[],[f568])).
% 5.75/1.08 tff(f606,plain,(
% 5.75/1.08 ! [X0 : $int] : (~$less(0,X0) | ~mem3(g_s165_167,X0,g_s156_1_161))),
% 5.75/1.08 inference(ennf_transformation,[],[f390])).
% 5.75/1.08 tff(f608,plain,(
% 5.75/1.08 ? [X0 : $int,X1 : $int] : (X1 = g_s165_167 & ! [X2 : $int,X3 : $int] : ((~$less(X0,$sum($sum(X2,1),$uminus(g_s56_56))) & ~$less($sum($sum(X3,1),$uminus(1)),X0)) | (~mem3(g_s165_167,X2,g_s123_124) | ~mem3(g_s165_167,X3,g_s123_124))) & mem3(X1,X0,g_s133_134))),
% 5.75/1.08 inference(ennf_transformation,[],[f456])).
% 5.75/1.08 tff(f609,plain,(
% 5.75/1.08 ? [X0 : $int,X1 : $int] : (X1 = g_s165_167 & ! [X2 : $int,X3 : $int] : ((~$less(X0,$sum($sum(X2,1),$uminus(g_s56_56))) & ~$less($sum($sum(X3,1),$uminus(1)),X0)) | ~mem3(g_s165_167,X2,g_s123_124) | ~mem3(g_s165_167,X3,g_s123_124)) & mem3(X1,X0,g_s133_134))),
% 5.75/1.08 inference(flattening,[],[f608])).
% 5.75/1.08 tff(f610,plain,(
% 5.75/1.08 ? [X0 : $int] : ($less(g_s56_56,X0) & ((g_s142_122 = g_s165_167 & ! [X1 : $int] : ($sum(X1,$uminus(1)) = X0 | ~mem3(g_s165_167,X1,g_s156_1_161))) | (mem3(g_s142_122,X0,g_s156_1_161) & ! [X2 : $int] : (g_s165_167 != g_s142_122 | ? [X3 : $int] : ($sum(X3,$uminus(1)) != X2 & mem3(g_s165_167,X3,g_s156_1_161))))))),
% 5.75/1.08 inference(ennf_transformation,[],[f394])).
% 5.75/1.08 tff(f709,plain,(
% 5.75/1.08 ! [X0 : $int] : ((mem0(X0,g_s24_23) | ($less(X0,0) | $less(255,X0))) & ((~$less(X0,0) & ~$less(255,X0)) | ~mem0(X0,g_s24_23)))),
% 5.75/1.08 inference(nnf_transformation,[],[f313])).
% 5.75/1.08 tff(f710,plain,(
% 5.75/1.08 ! [X0 : $int] : ((mem0(X0,g_s24_23) | $less(X0,0) | $less(255,X0)) & ((~$less(X0,0) & ~$less(255,X0)) | ~mem0(X0,g_s24_23)))),
% 5.75/1.08 inference(flattening,[],[f709])).
% 5.75/1.08 tff(f792,plain,(
% 5.75/1.08 ! [X0 : $int] : (! [X1 : $int,X2 : $int] : (X0 != X2 | (($less(X1,$sum($sum($sum(sK84(X0,X1),$uminus(g_s56_56)),1),sK85(X0,X1))) | $less(sK86(X0,X1),X1)) & mem3(X0,sK84(X0,X1),g_s123_124) & mem3(X0,sK85(X0,X1),g_s156_1_161) & mem3(X0,sK86(X0,X1),g_s123_124)) | ~mem3(X2,X1,g_s133_134)) | $less(X0,0) | $less(g_s51_51,X0))),
% 5.75/1.08 inference(skolemize,[status(esa),new_symbols(skolem,[sK84,sK85,sK86]),skolemize(X3,sK84(X0,X1)),skolemize(X4,sK85(X0,X1)),skolemize(X5,sK86(X0,X1))],[f569])).
% 5.75/1.08 tff(f810,plain,(
% 5.75/1.08 g_s165_167 = sK113 & ! [X2 : $int,X3 : $int] : ((~$less(sK112,$sum($sum(X2,1),$uminus(g_s56_56))) & ~$less($sum($sum(X3,1),$uminus(1)),sK112)) | ~mem3(g_s165_167,X2,g_s123_124) | ~mem3(g_s165_167,X3,g_s123_124)) & mem3(sK113,sK112,g_s133_134)),
% 5.75/1.08 inference(skolemize,[status(esa),new_symbols(skolem,[sK112,sK113]),skolemize(X0,sK112),skolemize(X1,sK113)],[f609])).
% 5.75/1.08 tff(f811,plain,(
% 5.75/1.08 $less(g_s56_56,sK114) & ((g_s142_122 = g_s165_167 & ! [X1 : $int] : ($sum(X1,$uminus(1)) = sK114 | ~mem3(g_s165_167,X1,g_s156_1_161))) | (mem3(g_s142_122,sK114,g_s156_1_161) & ! [X2 : $int] : (g_s165_167 != g_s142_122 | ($sum(sK115(X2),$uminus(1)) != X2 & mem3(g_s165_167,sK115(X2),g_s156_1_161)))))),
% 5.75/1.08 inference(skolemize,[status(esa),new_symbols(skolem,[sK114,sK115]),skolemize(X0,sK114),skolemize(X3,sK115(X2))],[f610])).
% 5.75/1.08 tff(f847,plain,(
% 5.75/1.08 ( ! [X0 : $int,X1 : $int] : (~mem3(X1,X0,g_s133_134) | ~$less(g_s51_51,X1)) )),
% 5.75/1.08 inference(cnf_transformation,[],[f461])).
% 5.75/1.08 tff(f848,plain,(
% 5.75/1.08 ( ! [X0 : $int,X1 : $int] : (~mem3(X1,X0,g_s133_134) | ~$less(X1,0)) )),
% 5.75/1.08 inference(cnf_transformation,[],[f461])).
% 5.75/1.08 tff(f1072,plain,(
% 5.75/1.08 ( ! [X0 : $int] : (~$less(X0,0) | ~mem0(X0,g_s24_23)) )),
% 5.75/1.08 inference(cnf_transformation,[],[f710])).
% 5.75/1.08 tff(f1073,plain,(
% 5.75/1.08 ( ! [X0 : $int] : (mem0(X0,g_s24_23) | $less(X0,0) | $less(255,X0)) )),
% 5.75/1.08 inference(cnf_transformation,[],[f710])).
% 5.75/1.08 tff(f1135,plain,(
% 5.75/1.08 ~$less(g_s56_56,1)),
% 5.75/1.08 inference(cnf_transformation,[],[f328])).
% 5.75/1.08 tff(f1274,plain,(
% 5.75/1.08 ( ! [X0 : $int,X1 : $int] : (~mem3(X0,X1,g_s156_1_161) | ~$less(g_s56_56,X1) | $less(X0,0) | $less(g_s51_51,X0)) )),
% 5.75/1.08 inference(cnf_transformation,[],[f553])).
% 5.75/1.08 tff(f1336,plain,(
% 5.75/1.08 ( ! [X2 : $int,X0 : $int,X1 : $int] : (X0 != X2 | mem3(X0,sK85(X0,X1),g_s156_1_161) | ~mem3(X2,X1,g_s133_134) | $less(X0,0) | $less(g_s51_51,X0)) )),
% 5.75/1.08 inference(cnf_transformation,[],[f792])).
% 5.75/1.08 tff(f1398,plain,(
% 5.75/1.08 ~$less(g_s51_51,g_s165_167)),
% 5.75/1.08 inference(cnf_transformation,[],[f387])).
% 5.75/1.08 tff(f1399,plain,(
% 5.75/1.08 ~$less(g_s165_167,0)),
% 5.75/1.08 inference(cnf_transformation,[],[f387])).
% 5.75/1.08 tff(f1409,plain,(
% 5.75/1.08 ( ! [X0 : $int] : (~$less(0,X0) | ~mem3(g_s165_167,X0,g_s156_1_161)) )),
% 5.75/1.08 inference(cnf_transformation,[],[f606])).
% 5.75/1.08 tff(f1412,plain,(
% 5.75/1.08 mem3(sK113,sK112,g_s133_134)),
% 5.75/1.08 inference(cnf_transformation,[],[f810])).
% 5.75/1.08 tff(f1415,plain,(
% 5.75/1.08 g_s165_167 = sK113),
% 5.75/1.08 inference(cnf_transformation,[],[f810])).
% 5.75/1.08 tff(f1416,plain,(
% 5.75/1.08 ~$less(g_s51_51,g_s142_122)),
% 5.75/1.08 inference(cnf_transformation,[],[f393])).
% 5.75/1.08 tff(f1417,plain,(
% 5.75/1.08 ~$less(g_s142_122,0)),
% 5.75/1.08 inference(cnf_transformation,[],[f393])).
% 5.75/1.08 tff(f1420,plain,(
% 5.75/1.08 ( ! [X1 : $int] : ($sum(X1,$uminus(1)) = sK114 | ~mem3(g_s165_167,X1,g_s156_1_161) | mem3(g_s142_122,sK114,g_s156_1_161)) )),
% 5.75/1.08 inference(cnf_transformation,[],[f811])).
% 5.75/1.08 tff(f1423,plain,(
% 5.75/1.08 g_s165_167 = g_s142_122 | mem3(g_s142_122,sK114,g_s156_1_161)),
% 5.75/1.08 inference(cnf_transformation,[],[f811])).
% 5.75/1.08 tff(f1424,plain,(
% 5.75/1.08 $less(g_s56_56,sK114)),
% 5.75/1.08 inference(cnf_transformation,[],[f811])).
% 5.75/1.08 tff(f1434,plain,(
% 5.75/1.08 ~$less(sK113,0)),
% 5.75/1.08 inference(definition_unfolding,[],[f1399,f1415])).
% 5.75/1.08 tff(f1435,plain,(
% 5.75/1.08 ~$less(g_s51_51,sK113)),
% 5.75/1.08 inference(definition_unfolding,[],[f1398,f1415])).
% 5.75/1.08 tff(f1439,plain,(
% 5.75/1.08 ( ! [X0 : $int] : (~mem3(sK113,X0,g_s156_1_161) | ~$less(0,X0)) )),
% 5.75/1.08 inference(definition_unfolding,[],[f1409,f1415])).
% 5.75/1.08 tff(f1444,plain,(
% 5.75/1.08 mem3(g_s142_122,sK114,g_s156_1_161) | g_s142_122 = sK113),
% 5.75/1.08 inference(definition_unfolding,[],[f1423,f1415])).
% 5.75/1.08 tff(f1447,plain,(
% 5.75/1.08 ( ! [X1 : $int] : ($sum(X1,$uminus(1)) = sK114 | ~mem3(sK113,X1,g_s156_1_161) | mem3(g_s142_122,sK114,g_s156_1_161)) )),
% 5.75/1.08 inference(definition_unfolding,[],[f1420,f1415])).
% 5.75/1.08 tff(f1501,plain,(
% 5.75/1.08 ( ! [X2 : $int,X1 : $int] : (mem3(X2,sK85(X2,X1),g_s156_1_161) | ~mem3(X2,X1,g_s133_134) | $less(X2,0) | $less(g_s51_51,X2)) )),
% 5.75/1.08 inference(equality_resolution,[],[f1336])).
% 5.75/1.08 tff(f1518,definition,(
% 5.75/1.08 sF116 = $uminus(1)),
% 5.75/1.08 introduced(definition,[new_symbols(definition,[sF116])],[function_definition])).
% 5.75/1.08 tff(f1519,plain,(
% 5.75/1.08 $uminus(1) = sF116),
% 5.75/1.08 inference(reorient_equations,[],[f1518])).
% 5.75/1.08 tff(f1521,plain,(
% 5.75/1.08 ( ! [X1 : $int] : (~mem3(sK113,X1,g_s156_1_161) | sK114 = $sum(X1,sF116) | mem3(g_s142_122,sK114,g_s156_1_161)) )),
% 5.75/1.08 inference(definition_folding,[],[f1447,f1519])).
% 5.75/1.08 tff(f1540,plain,(
% 5.75/1.08 sF116 = -1),
% 5.75/1.08 inference(evaluation,[],[f1519])).
% 5.75/1.08 tff(f1661,plain,(
% 5.75/1.08 ( ! [X0 : $int] : ($less(X0,$sum(X0,1))) )),
% 5.75/1.08 inference(resolution,[],[f404,f400])).
% 5.75/1.08 tff(f1687,plain,(
% 5.75/1.08 ( ! [X0 : $int,X1 : $int] : ($less(X1,$sum(1,X0)) | $less(X0,X1)) )),
% 5.75/1.08 inference(superposition,[],[f404,f395])).
% 5.75/1.08 tff(f1713,plain,(
% 5.75/1.08 ( ! [X0 : $int] : ($less(X0,$sum(1,X0))) )),
% 5.75/1.08 inference(superposition,[],[f1661,f395])).
% 5.75/1.08 tff(f1923,plain,(
% 5.75/1.08 ( ! [X0 : $int] : (~$less(X0,g_s56_56) | $less(X0,sK114)) )),
% 5.75/1.08 inference(resolution,[],[f401,f1424])).
% 5.75/1.08 tff(f2006,plain,(
% 5.75/1.08 ( ! [X0 : $int] : ($less(g_s56_56,X0) | $less(X0,sK114) | g_s56_56 = X0) )),
% 5.75/1.08 inference(resolution,[],[f402,f1923])).
% 5.75/1.08 tff(f2083,plain,(
% 5.75/1.08 $less(1,sK114) | 1 = g_s56_56),
% 5.75/1.08 inference(resolution,[],[f2006,f1135])).
% 5.75/1.08 tff(f2113,plain,(
% 5.75/1.08 ( ! [X0 : $int] : (~$less(X0,1) | 1 = g_s56_56 | $less(X0,sK114)) )),
% 5.75/1.08 inference(resolution,[],[f2083,f401])).
% 5.75/1.08 tff(f2239,plain,(
% 5.75/1.08 ( ! [X0 : $int,X1 : $int] : ($sum(0,X1) = $sum(X0,$sum($uminus(X0),X1))) )),
% 5.75/1.08 inference(superposition,[],[f396,f399])).
% 5.75/1.08 tff(f2288,plain,(
% 5.75/1.08 ( ! [X0 : $int,X1 : $int] : ($sum(X0,$sum($uminus(X0),X1)) = X1) )),
% 5.75/1.08 inference(evaluation,[],[f2239])).
% 5.75/1.08 tff(f2348,plain,(
% 5.75/1.08 ( ! [X0 : $int] : ($less(1,X0) | $less(X0,sK114) | 1 = g_s56_56 | 1 = X0) )),
% 5.75/1.08 inference(resolution,[],[f2113,f402])).
% 5.75/1.08 tff(f2392,plain,(
% 5.75/1.08 $less(0,sK114) | 1 = g_s56_56 | 0 = 1 | ~mem0(1,g_s24_23)),
% 5.75/1.08 inference(resolution,[],[f2348,f1072])).
% 5.75/1.08 tff(f2450,plain,(
% 5.75/1.08 ~mem0(1,g_s24_23) | 1 = g_s56_56 | $less(0,sK114)),
% 5.75/1.08 inference(evaluation,[],[f2392])).
% 5.75/1.08 tff(f2515,plain,(
% 5.75/1.08 1 = g_s56_56 | $less(0,sK114) | $less(1,0) | $less(255,1)),
% 5.75/1.08 inference(resolution,[],[f2450,f1073])).
% 5.75/1.08 tff(f2516,plain,(
% 5.75/1.08 $less(0,sK114) | 1 = g_s56_56),
% 5.75/1.08 inference(evaluation,[],[f2515])).
% 5.75/1.08 tff(f2522,plain,(
% 5.75/1.08 ( ! [X0 : $int] : (~$less(X0,0) | 1 = g_s56_56 | $less(X0,sK114)) )),
% 5.75/1.08 inference(resolution,[],[f2516,f401])).
% 5.75/1.08 tff(f2693,plain,(
% 5.75/1.08 ~$less(g_s56_56,sK114) | $less(g_s142_122,0) | $less(g_s51_51,g_s142_122) | g_s142_122 = sK113),
% 5.75/1.08 inference(resolution,[],[f1274,f1444])).
% 5.75/1.08 tff(f2694,plain,(
% 5.75/1.08 $less(g_s142_122,0) | $less(g_s51_51,g_s142_122) | g_s142_122 = sK113),
% 5.75/1.08 inference(forward_subsumption_resolution,[],[f2693,f1424])).
% 5.75/1.08 tff(f2695,plain,(
% 5.75/1.08 $less(g_s51_51,g_s142_122) | g_s142_122 = sK113),
% 5.75/1.08 inference(forward_subsumption_resolution,[],[f2694,f1417])).
% 5.75/1.08 tff(f2696,plain,(
% 5.75/1.08 g_s142_122 = sK113),
% 5.75/1.08 inference(forward_subsumption_resolution,[],[f2695,f1416])).
% 5.75/1.08 tff(f2978,plain,(
% 5.75/1.08 ( ! [X0 : $int] : (~mem3(sK113,X0,g_s133_134) | $less(sK113,0) | $less(g_s51_51,sK113) | ~$less(0,sK85(sK113,X0))) )),
% 5.75/1.08 inference(resolution,[],[f1501,f1439])).
% 5.75/1.08 tff(f2979,plain,(
% 5.75/1.08 ( ! [X0 : $int] : (~mem3(sK113,X0,g_s133_134) | $less(sK113,0) | $less(g_s51_51,sK113) | sK114 = $sum(sK85(sK113,X0),sF116) | mem3(g_s142_122,sK114,g_s156_1_161)) )),
% 5.75/1.08 inference(resolution,[],[f1501,f1521])).
% 5.75/1.08 tff(f2985,plain,(
% 5.75/1.08 ( ! [X0 : $int] : (~mem3(sK113,X0,g_s133_134) | $less(g_s51_51,sK113) | sK114 = $sum(sK85(sK113,X0),sF116) | mem3(g_s142_122,sK114,g_s156_1_161)) )),
% 5.75/1.08 inference(forward_subsumption_resolution,[],[f2979,f848])).
% 5.75/1.08 tff(f2986,plain,(
% 5.75/1.08 ( ! [X0 : $int] : (~mem3(sK113,X0,g_s133_134) | $less(g_s51_51,sK113) | ~$less(0,sK85(sK113,X0))) )),
% 5.75/1.08 inference(forward_subsumption_resolution,[],[f2978,f848])).
% 5.75/1.08 tff(f2989,plain,(
% 5.75/1.08 ( ! [X0 : $int] : (~mem3(sK113,X0,g_s133_134) | sK114 = $sum(sK85(sK113,X0),sF116) | mem3(g_s142_122,sK114,g_s156_1_161)) )),
% 5.75/1.08 inference(forward_subsumption_resolution,[],[f2985,f847])).
% 5.75/1.08 tff(f2990,plain,(
% 5.75/1.08 ( ! [X0 : $int] : (~$less(0,sK85(sK113,X0)) | ~mem3(sK113,X0,g_s133_134)) )),
% 5.75/1.08 inference(forward_subsumption_resolution,[],[f2986,f847])).
% 5.75/1.08 tff(f2991,plain,(
% 5.75/1.08 ( ! [X0 : $int] : (sK114 = $sum(sF116,sK85(sK113,X0)) | ~mem3(sK113,X0,g_s133_134) | mem3(g_s142_122,sK114,g_s156_1_161)) )),
% 5.75/1.08 inference(forward_demodulation,[],[f2989,f395])).
% 5.75/1.08 tff(f2992,plain,(
% 5.75/1.08 ( ! [X0 : $int] : (sK114 = $sum(-1,sK85(sK113,X0)) | ~mem3(sK113,X0,g_s133_134) | mem3(g_s142_122,sK114,g_s156_1_161)) )),
% 5.75/1.08 inference(forward_demodulation,[],[f2991,f1540])).
% 5.75/1.08 tff(f2993,plain,(
% 5.75/1.08 ( ! [X0 : $int] : (~mem3(sK113,X0,g_s133_134) | sK114 = $sum(-1,sK85(sK113,X0)) | mem3(sK113,sK114,g_s156_1_161)) )),
% 5.75/1.08 inference(forward_demodulation,[],[f2992,f2696])).
% 5.75/1.08 tff(f3215,plain,(
% 5.75/1.08 mem3(sK113,sK114,g_s156_1_161) | sK114 = $sum(-1,sK85(sK113,sK112))),
% 5.75/1.08 inference(resolution,[],[f2993,f1412])).
% 5.75/1.08 tff(f3226,plain,(
% 5.75/1.08 sK114 = $sum(-1,sK85(sK113,sK112)) | ~$less(g_s56_56,sK114) | $less(sK113,0) | $less(g_s51_51,sK113)),
% 5.75/1.08 inference(resolution,[],[f3215,f1274])).
% 5.75/1.08 tff(f3228,plain,(
% 5.75/1.08 sK114 = $sum(-1,sK85(sK113,sK112)) | $less(sK113,0) | $less(g_s51_51,sK113)),
% 5.75/1.08 inference(forward_subsumption_resolution,[],[f3226,f1424])).
% 5.75/1.08 tff(f3231,plain,(
% 5.75/1.08 sK114 = $sum(-1,sK85(sK113,sK112)) | $less(g_s51_51,sK113)),
% 5.75/1.08 inference(forward_subsumption_resolution,[],[f3228,f1434])).
% 5.75/1.08 tff(f3233,plain,(
% 5.75/1.08 sK114 = $sum(-1,sK85(sK113,sK112))),
% 5.75/1.08 inference(forward_subsumption_resolution,[],[f3231,f1435])).
% 5.75/1.08 tff(f3244,plain,(
% 5.75/1.08 ( ! [X0 : $int] : ($sum(-1,$sum(sK85(sK113,sK112),X0)) = $sum(sK114,X0)) )),
% 5.75/1.08 inference(superposition,[],[f396,f3233])).
% 5.75/1.08 tff(f3246,plain,(
% 5.75/1.08 ( ! [X0 : $int] : ($less(sK114,$sum(X0,sK85(sK113,sK112))) | ~$less(-1,X0)) )),
% 5.75/1.08 inference(superposition,[],[f403,f3233])).
% 5.75/1.08 tff(f3276,plain,(
% 5.75/1.08 ( ! [X0 : $int] : ($less(sK114,$sum(sK85(sK113,sK112),X0)) | ~$less(-1,X0)) )),
% 5.75/1.08 inference(superposition,[],[f3246,f395])).
% 5.75/1.08 tff(f3340,plain,(
% 5.75/1.08 $less(sK114,sK85(sK113,sK112)) | ~$less(-1,0)),
% 5.75/1.08 inference(superposition,[],[f3276,f397])).
% 5.75/1.08 tff(f3344,plain,(
% 5.75/1.08 $less(sK114,sK85(sK113,sK112))),
% 5.75/1.08 inference(evaluation,[],[f3340])).
% 5.75/1.08 tff(f3380,plain,(
% 5.75/1.08 ( ! [X0 : $int] : ($less(X0,sK85(sK113,sK112)) | ~$less(X0,sK114)) )),
% 5.75/1.08 inference(resolution,[],[f3344,f401])).
% 5.75/1.08 tff(f3437,plain,(
% 5.75/1.08 ( ! [X0 : $int,X1 : $int] : (~$less(X1,X0) | ~$less(X0,sK114) | $less(X1,sK85(sK113,sK112))) )),
% 5.75/1.08 inference(resolution,[],[f3380,f401])).
% 5.75/1.08 tff(f4016,plain,(
% 5.75/1.08 ( ! [X0 : $int] : ($sum(sK114,X0) = $sum(-1,$sum(X0,sK85(sK113,sK112)))) )),
% 5.75/1.08 inference(superposition,[],[f3244,f395])).
% 5.75/1.08 tff(f4211,plain,(
% 5.75/1.08 ( ! [X0 : $int] : (~$less($sum(1,X0),sK114) | $less(X0,sK85(sK113,sK112))) )),
% 5.75/1.08 inference(resolution,[],[f3437,f1713])).
% 5.75/1.08 tff(f4275,plain,(
% 5.75/1.08 $less(0,sK85(sK113,sK112)) | ~$less(1,sK114)),
% 5.75/1.08 inference(superposition,[],[f4211,f397])).
% 5.75/1.08 tff(f5116,plain,(
% 5.75/1.08 sK85(sK113,sK112) = $sum(sK114,$uminus(-1))),
% 5.75/1.08 inference(superposition,[],[f4016,f2288])).
% 5.75/1.08 tff(f5117,plain,(
% 5.75/1.08 sK85(sK113,sK112) = $sum(sK114,1)),
% 5.75/1.08 inference(evaluation,[],[f5116])).
% 5.75/1.08 tff(f5126,plain,(
% 5.75/1.08 sK85(sK113,sK112) = $sum(1,sK114)),
% 5.75/1.08 inference(forward_demodulation,[],[f5117,f395])).
% 5.75/1.08 tff(f5273,plain,(
% 5.75/1.08 mem3(sK113,$sum(1,sK114),g_s156_1_161) | ~mem3(sK113,sK112,g_s133_134) | $less(sK113,0) | $less(g_s51_51,sK113)),
% 5.75/1.08 inference(superposition,[],[f1501,f5126])).
% 5.75/1.08 tff(f5274,plain,(
% 5.75/1.08 mem3(sK113,$sum(1,sK114),g_s156_1_161) | ~mem3(sK113,sK112,g_s133_134) | $less(g_s51_51,sK113)),
% 5.75/1.08 inference(forward_subsumption_resolution,[],[f5273,f848])).
% 5.75/1.08 tff(f5280,plain,(
% 5.75/1.08 mem3(sK113,$sum(1,sK114),g_s156_1_161) | ~mem3(sK113,sK112,g_s133_134)),
% 5.75/1.08 inference(forward_subsumption_resolution,[],[f5274,f847])).
% 5.75/1.08 tff(f5283,plain,(
% 5.75/1.08 mem3(sK113,$sum(1,sK114),g_s156_1_161)),
% 5.75/1.08 inference(forward_subsumption_resolution,[],[f5280,f1412])).
% 5.75/1.08 tff(f5296,plain,(
% 5.75/1.08 ~$less(0,$sum(1,sK114))),
% 5.75/1.08 inference(resolution,[],[f5283,f1439])).
% 5.75/1.08 tff(f5308,plain,(
% 5.75/1.08 $less(sK114,0)),
% 5.75/1.08 inference(resolution,[],[f5296,f1687])).
% 5.75/1.08 tff(f5334,plain,(
% 5.75/1.08 1 = g_s56_56 | $less(sK114,sK114)),
% 5.75/1.08 inference(resolution,[],[f5308,f2522])).
% 5.75/1.08 tff(f5340,plain,(
% 5.75/1.08 1 = g_s56_56),
% 5.75/1.08 inference(forward_subsumption_resolution,[],[f5334,f400])).
% 5.75/1.08 tff(f5470,plain,(
% 5.75/1.08 $less(1,sK114)),
% 5.75/1.08 inference(superposition,[],[f1424,f5340])).
% 5.75/1.08 tff(f5643,plain,(
% 5.75/1.08 ~mem3(sK113,sK112,g_s133_134) | ~$less(1,sK114)),
% 5.75/1.08 inference(resolution,[],[f2990,f4275])).
% 5.75/1.08 tff(f5657,plain,(
% 5.75/1.08 ~$less(1,sK114)),
% 5.75/1.08 inference(forward_subsumption_resolution,[],[f5643,f1412])).
% 5.75/1.08 tff(f5664,plain,(
% 5.75/1.08 $false),
% 5.75/1.08 inference(forward_subsumption_resolution,[],[f5657,f5470])).
% 5.75/1.08 % SZS output end Proof for theBenchmark
% 5.75/1.08 % (236482)------------------------------
% 5.75/1.08 % (236482)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.75/1.08 % (236482)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.75/1.08 % (236482)CaDiCaL version: 2.1.3
% 5.75/1.08 % (236482)Termination reason: Refutation
% 5.75/1.08 % (236482)Time elapsed: 0.142 s
% 5.75/1.08 % (236482)Peak memory usage: 15 MB
% 5.75/1.08 % (236482)Instructions burned: 251 (million)
% 5.75/1.08 % (236427)Success in time 0.864 s
% 5.75/1.08 % Vampire exiting
%------------------------------------------------------------------------------