%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWC540_1 : TPTP v9.3.1. Bugfixed v9.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:06:14 PM UTC 2026
% Result : Theorem 12.82s 2.07s
% Output : Refutation 12.82s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWC540_1 : TPTP v9.3.1. Bugfixed v9.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.17 % Computer : n005.cluster.edu
% 0.10/0.17 % Model : x86_64 x86_64
% 0.10/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.17 % Memory : 8046.5625MB
% 0.10/0.17 % OS : Linux 6.8.0-71-generic
% 0.10/0.17 % CPULimit : 300
% 0.10/0.17 % WCLimit : 300
% 0.10/0.17 % DateTime : Mon Sep 28 09:41:46 UTC 2026
% 0.10/0.18 % CPUTime :
% 0.10/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.20 Running first-order model finding
% 0.10/0.20 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
% 2.92/0.65 % (673693)Will run a generic schedule for satisfiability detection.
% 2.92/0.65 % (673703)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4145583418:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 2.92/0.65 % (673699)% WARNING: option uhcvi not known.
% 2.92/0.65 % (673698)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=632263597_2999 on theBenchmark for (2999ds/0Mi)
% 2.92/0.65 % (673700)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=753096221:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 2.92/0.65 % (673701)dis+10_1_sil=32000:sp=arity:random_seed=1344676379:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 2.92/0.65 % (673699)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2746521973:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 2.92/0.65 % (673702)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3846997111:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 2.92/0.65 % (673704)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3601529272:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 2.92/0.65 % (673698)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 2.92/0.65 % (673698)Terminated due to inappropriate strategy.
% 2.92/0.65 % (673698)------------------------------
% 2.92/0.65 % (673698)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.92/0.65 % (673698)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.92/0.65 % (673698)CaDiCaL version: 2.1.3
% 2.92/0.65 % (673698)Termination reason: Inappropriate
% 2.92/0.65 % (673698)Time elapsed: 0.014 s
% 2.92/0.65 % (673698)Peak memory usage: 11 MB
% 2.92/0.65 % (673698)Instructions burned: 26 (million)
% 2.92/0.65 % (673698)------------------------------
% 2.92/0.65 % (673698)------------------------------
% 2.92/0.65 % (673712)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3643287249:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 2.92/0.65 % (673703)Instruction limit reached!
% 2.92/0.65 % (673703)------------------------------
% 2.92/0.65 % (673703)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.92/0.65 % (673703)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.92/0.65 % (673703)CaDiCaL version: 2.1.3
% 2.92/0.65 % (673703)Termination reason: Instruction limit
% 2.92/0.65 % (673703)Termination phase: Saturation
% 2.92/0.65 % (673703)Time elapsed: 0.045 s
% 2.92/0.65 % (673703)Peak memory usage: 14 MB
% 2.92/0.65 % (673703)Instructions burned: 133 (million)
% 2.92/0.65 % (673712)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 2.92/0.65 % (673712)Terminated due to inappropriate strategy.
% 2.92/0.65 % (673712)------------------------------
% 2.92/0.65 % (673712)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.92/0.65 % (673712)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.92/0.65 % (673712)CaDiCaL version: 2.1.3
% 2.92/0.65 % (673712)Termination reason: Inappropriate
% 2.92/0.65 % (673712)Time elapsed: 0.010 s
% 2.92/0.65 % (673712)Peak memory usage: 11 MB
% 2.92/0.65 % (673712)Instructions burned: 17 (million)
% 2.92/0.65 % (673712)------------------------------
% 2.92/0.65 % (673712)------------------------------
% 2.92/0.65 % (673714)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=959220725:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 2.92/0.65 % (673701)Instruction limit reached!
% 2.92/0.65 % (673701)------------------------------
% 2.92/0.65 % (673701)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.92/0.65 % (673701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.92/0.65 % (673701)CaDiCaL version: 2.1.3
% 2.92/0.65 % (673701)Termination reason: Instruction limit
% 2.92/0.65 % (673701)Termination phase: Saturation
% 2.92/0.65 % (673701)Time elapsed: 0.068 s
% 2.92/0.65 % (673701)Peak memory usage: 13 MB
% 2.92/0.65 % (673701)Instructions burned: 103 (million)
% 2.92/0.65 % (673716)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=180002708:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 2.92/0.65 % (673702)Instruction limit reached!
% 2.92/0.65 % (673702)------------------------------
% 2.92/0.65 % (673702)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.38/1.17 % (673702)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.38/1.17 % (673702)CaDiCaL version: 2.1.3
% 6.38/1.17 % (673702)Termination reason: Instruction limit
% 6.38/1.17 % (673702)Termination phase: Saturation
% 6.38/1.17 % (673702)Time elapsed: 0.069 s
% 6.38/1.17 % (673702)Peak memory usage: 13 MB
% 6.38/1.17 % (673702)Instructions burned: 116 (million)
% 6.38/1.17 % (673718)ott-21_1_sil=16000:fs=off:random_seed=2286252446:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 6.38/1.17 % (673719)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1325062669:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 6.38/1.17 % (673714)Instruction limit reached!
% 6.38/1.17 % (673714)------------------------------
% 6.38/1.17 % (673714)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.38/1.17 % (673714)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.38/1.17 % (673714)CaDiCaL version: 2.1.3
% 6.38/1.17 % (673714)Termination reason: Instruction limit
% 6.38/1.17 % (673714)Termination phase: Saturation
% 6.38/1.17 % (673714)Time elapsed: 0.044 s
% 6.38/1.17 % (673714)Peak memory usage: 14 MB
% 6.38/1.17 % (673714)Instructions burned: 134 (million)
% 6.38/1.17 % (673704)Instruction limit reached!
% 6.38/1.17 % (673704)------------------------------
% 6.38/1.17 % (673704)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.38/1.17 % (673704)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.38/1.17 % (673704)CaDiCaL version: 2.1.3
% 6.38/1.17 % (673704)Termination reason: Instruction limit
% 6.38/1.17 % (673704)Termination phase: Saturation
% 6.38/1.17 % (673704)Time elapsed: 0.103 s
% 6.38/1.17 % (673704)Peak memory usage: 15 MB
% 6.38/1.17 % (673704)Instructions burned: 159 (million)
% 6.38/1.17 % (673722)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=230928082:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 6.38/1.17 % (673722)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 6.38/1.17 % (673722)Terminated due to inappropriate strategy.
% 6.38/1.17 % (673722)------------------------------
% 6.38/1.17 % (673722)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.38/1.17 % (673722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.38/1.17 % (673722)CaDiCaL version: 2.1.3
% 6.38/1.17 % (673722)Termination reason: Inappropriate
% 6.38/1.17 % (673722)Time elapsed: 0.005 s
% 6.38/1.17 % (673722)Peak memory usage: 10 MB
% 6.38/1.17 % (673722)Instructions burned: 18 (million)
% 6.38/1.17 % (673722)------------------------------
% 6.38/1.17 % (673722)------------------------------
% 6.38/1.17 % (673723)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=214996308:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 6.38/1.17 % (673725)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=424469112:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 6.38/1.17 % (673725)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 6.38/1.17 % (673725)Terminated due to inappropriate strategy.
% 6.38/1.17 % (673725)------------------------------
% 6.38/1.17 % (673725)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.38/1.17 % (673725)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.38/1.17 % (673725)CaDiCaL version: 2.1.3
% 6.38/1.17 % (673725)Termination reason: Inappropriate
% 6.38/1.17 % (673725)Time elapsed: 0.005 s
% 6.38/1.17 % (673725)Peak memory usage: 11 MB
% 6.38/1.17 % (673725)Instructions burned: 18 (million)
% 6.38/1.17 % (673725)------------------------------
% 6.38/1.17 % (673725)------------------------------
% 6.38/1.17 % (673728)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=612087349: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)
% 6.38/1.17 % (673718)Instruction limit reached!
% 6.38/1.17 % (673718)------------------------------
% 6.38/1.17 % (673718)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 6.38/1.17 % (673718)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.38/1.17 % (673718)CaDiCaL version: 2.1.3
% 6.38/1.17 % (673718)Termination reason: Instruction limit
% 6.38/1.17 % (673718)Termination phase: Saturation
% 6.38/1.17 % (673718)Time elapsed: 0.094 s
% 6.38/1.17 % (673718)Peak memory usage: 13 MB
% 6.38/1.17 % (673718)Instructions burned: 180 (million)
% 12.82/2.07 % (673730)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2126679965:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 12.82/2.07 % (673719)Instruction limit reached!
% 12.82/2.07 % (673719)------------------------------
% 12.82/2.07 % (673719)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.82/2.07 % (673719)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.82/2.07 % (673719)CaDiCaL version: 2.1.3
% 12.82/2.07 % (673719)Termination reason: Instruction limit
% 12.82/2.07 % (673719)Termination phase: Saturation
% 12.82/2.07 % (673719)Time elapsed: 0.230 s
% 12.82/2.07 % (673719)Peak memory usage: 13 MB
% 12.82/2.07 % (673719)Instructions burned: 479 (million)
% 12.82/2.07 % (673746)fmb+10_1_sil=64000:random_seed=4250289043:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi)
% 12.82/2.07 % (673746)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 12.82/2.07 % (673746)Terminated due to inappropriate strategy.
% 12.82/2.07 % (673746)------------------------------
% 12.82/2.07 % (673746)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.82/2.07 % (673746)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.82/2.07 % (673746)CaDiCaL version: 2.1.3
% 12.82/2.07 % (673746)Termination reason: Inappropriate
% 12.82/2.07 % (673746)Time elapsed: 0.010 s
% 12.82/2.07 % (673746)Peak memory usage: 11 MB
% 12.82/2.07 % (673746)Instructions burned: 19 (million)
% 12.82/2.07 % (673746)------------------------------
% 12.82/2.07 % (673746)------------------------------
% 12.82/2.07 % (673755)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1137035771:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi)
% 12.82/2.07 % (673728)Instruction limit reached!
% 12.82/2.07 % (673728)------------------------------
% 12.82/2.07 % (673728)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.82/2.07 % (673728)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.82/2.07 % (673728)CaDiCaL version: 2.1.3
% 12.82/2.07 % (673728)Termination reason: Instruction limit
% 12.82/2.07 % (673728)Termination phase: Saturation
% 12.82/2.07 % (673728)Time elapsed: 0.232 s
% 12.82/2.07 % (673728)Peak memory usage: 20 MB
% 12.82/2.07 % (673728)Instructions burned: 694 (million)
% 12.82/2.07 % (673755)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 12.82/2.07 % (673755)Terminated due to inappropriate strategy.
% 12.82/2.07 % (673755)------------------------------
% 12.82/2.07 % (673755)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.82/2.07 % (673755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.82/2.07 % (673755)CaDiCaL version: 2.1.3
% 12.82/2.07 % (673755)Termination reason: Inappropriate
% 12.82/2.07 % (673755)Time elapsed: 0.009 s
% 12.82/2.07 % (673755)Peak memory usage: 11 MB
% 12.82/2.07 % (673755)Instructions burned: 17 (million)
% 12.82/2.07 % (673755)------------------------------
% 12.82/2.07 % (673755)------------------------------
% 12.82/2.07 % (673769)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3902465959:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi)
% 12.82/2.07 % (673769)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 12.82/2.07 % (673769)Terminated due to inappropriate strategy.
% 12.82/2.07 % (673769)------------------------------
% 12.82/2.07 % (673769)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.82/2.07 % (673769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.82/2.07 % (673769)CaDiCaL version: 2.1.3
% 12.82/2.07 % (673769)Termination reason: Inappropriate
% 12.82/2.07 % (673769)Time elapsed: 0.005 s
% 12.82/2.07 % (673769)Peak memory usage: 11 MB
% 12.82/2.07 % (673769)Instructions burned: 18 (million)
% 12.82/2.07 % (673769)------------------------------
% 12.82/2.07 % (673769)------------------------------
% 12.82/2.07 % (673716)Instruction limit reached!
% 12.82/2.07 % (673716)------------------------------
% 12.82/2.07 % (673716)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.82/2.07 % (673716)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.82/2.07 % (673716)CaDiCaL version: 2.1.3
% 12.82/2.07 % (673716)Termination reason: Instruction limit
% 12.82/2.07 % (673716)Termination phase: Saturation
% 12.82/2.07 % (673716)Time elapsed: 0.328 s
% 12.82/2.07 % (673716)Peak memory usage: 15 MB
% 12.82/2.07 % (673716)Instructions burned: 685 (million)
% 12.82/2.07 % (673772)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1268134218:i=5131_2995 on theBenchmark for (2995ds/5131Mi)
% 12.82/2.07 % (673780)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2361604255:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi)
% 12.82/2.07 % (673782)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2651412467:i=6324_2995 on theBenchmark for (2995ds/6324Mi)
% 12.82/2.07 % (673782)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 12.82/2.07 % (673782)Terminated due to inappropriate strategy.
% 12.82/2.07 % (673782)------------------------------
% 12.82/2.07 % (673782)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.82/2.07 % (673782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.82/2.07 % (673782)CaDiCaL version: 2.1.3
% 12.82/2.07 % (673782)Termination reason: Inappropriate
% 12.82/2.07 % (673782)Time elapsed: 0.014 s
% 12.82/2.07 % (673782)Peak memory usage: 11 MB
% 12.82/2.07 % (673782)Instructions burned: 25 (million)
% 12.82/2.07 % (673782)------------------------------
% 12.82/2.07 % (673782)------------------------------
% 12.82/2.07 % (673804)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1004019223:fmbsr=2.30978:i=2174_2995 on theBenchmark for (2995ds/2174Mi)
% 12.82/2.07 % (673804)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 12.82/2.07 % (673804)Terminated due to inappropriate strategy.
% 12.82/2.07 % (673804)------------------------------
% 12.82/2.07 % (673804)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.82/2.07 % (673804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.82/2.07 % (673804)CaDiCaL version: 2.1.3
% 12.82/2.07 % (673804)Termination reason: Inappropriate
% 12.82/2.07 % (673804)Time elapsed: 0.017 s
% 12.82/2.07 % (673804)Peak memory usage: 11 MB
% 12.82/2.07 % (673804)Instructions burned: 18 (million)
% 12.82/2.07 % (673804)------------------------------
% 12.82/2.07 % (673804)------------------------------
% 12.82/2.07 % (673812)ott-2_1_sil=16000:newcnf=on:random_seed=4253681406:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi)
% 12.82/2.07 % (673730)Instruction limit reached!
% 12.82/2.07 % (673730)------------------------------
% 12.82/2.07 % (673730)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.82/2.07 % (673730)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.82/2.07 % (673730)CaDiCaL version: 2.1.3
% 12.82/2.07 % (673730)Termination reason: Instruction limit
% 12.82/2.07 % (673730)Termination phase: Saturation
% 12.82/2.07 % (673730)Time elapsed: 0.446 s
% 12.82/2.07 % (673730)Peak memory usage: 21 MB
% 12.82/2.07 % (673730)Instructions burned: 879 (million)
% 12.82/2.07 % (673853)ott+10_1_sil=32000:tgt=ground:random_seed=2371771084:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi)
% 12.82/2.07 % (673780)Instruction limit reached!
% 12.82/2.07 % (673780)------------------------------
% 12.82/2.07 % (673780)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.82/2.07 % (673780)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.82/2.07 % (673780)CaDiCaL version: 2.1.3
% 12.82/2.07 % (673780)Termination reason: Instruction limit
% 12.82/2.07 % (673780)Termination phase: Saturation
% 12.82/2.07 % (673780)Time elapsed: 0.323 s
% 12.82/2.07 % (673780)Peak memory usage: 19 MB
% 12.82/2.07 % (673780)Instructions burned: 1477 (million)
% 12.82/2.07 % (673871)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2533482898:i=54282_2992 on theBenchmark for (2992ds/54282Mi)
% 12.82/2.07 % (673871)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 12.82/2.07 % (673871)Terminated due to inappropriate strategy.
% 12.82/2.07 % (673871)------------------------------
% 12.82/2.07 % (673871)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.82/2.07 % (673871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.82/2.07 % (673871)CaDiCaL version: 2.1.3
% 12.82/2.07 % (673871)Termination reason: Inappropriate
% 12.82/2.07 % (673871)Time elapsed: 0.007 s
% 12.82/2.07 % (673871)Peak memory usage: 11 MB
% 12.82/2.07 % (673871)Instructions burned: 25 (million)
% 12.82/2.07 % (673871)------------------------------
% 12.82/2.07 % (673871)------------------------------
% 12.82/2.07 % (673874)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1292725759:i=3512:aac=none_2992 on theBenchmark for (2992ds/3512Mi)
% 12.82/2.07 % (673723)Instruction limit reached!
% 12.82/2.07 % (673723)------------------------------
% 12.82/2.07 % (673723)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.82/2.07 % (673723)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.82/2.07 % (673723)CaDiCaL version: 2.1.3
% 12.82/2.07 % (673723)Termination reason: Instruction limit
% 12.82/2.07 % (673723)Termination phase: Saturation
% 12.82/2.07 % (673723)Time elapsed: 0.796 s
% 12.82/2.07 % (673723)Peak memory usage: 25 MB
% 12.82/2.07 % (673723)Instructions burned: 1181 (million)
% 12.82/2.07 % (673899)dis+21_1_sil=32000:sas=cadical:random_seed=3071054075:i=3773:amm=off_2990 on theBenchmark for (2990ds/3773Mi)
% 12.82/2.07 % (673812)Instruction limit reached!
% 12.82/2.07 % (673812)------------------------------
% 12.82/2.07 % (673812)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.82/2.07 % (673812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.82/2.07 % (673812)CaDiCaL version: 2.1.3
% 12.82/2.07 % (673812)Termination reason: Instruction limit
% 12.82/2.07 % (673812)Termination phase: Saturation
% 12.82/2.07 % (673812)Time elapsed: 0.451 s
% 12.82/2.07 % (673812)Peak memory usage: 16 MB
% 12.82/2.07 % (673812)Instructions burned: 875 (million)
% 12.82/2.07 % (673901)ott+11_1_sil=16000:gs=on:random_seed=1336289735:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2990 on theBenchmark for (2990ds/2251Mi)
% 12.82/2.07 % (673874) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-673693-673874"...
% 12.82/2.07 % (673874)...printing done.
% 12.82/2.07 % (673874)Refutation found. Thanks to Tanya!
% 12.82/2.07 % SZS status Theorem for theBenchmark
% 12.82/2.07 % SZS output start Proof for theBenchmark
% 12.82/2.07 tff(type_def_5, type, set_0: $tType).
% 12.82/2.07 tff(type_def_6, type, set_2: $tType).
% 12.82/2.07 tff(type_def_7, type, set_3: $tType).
% 12.82/2.07 tff(type_def_8, type, set_4: $tType).
% 12.82/2.07 tff(func_def_0, type, min_int: $int).
% 12.82/2.07 tff(func_def_1, type, max_int: $int).
% 12.82/2.07 tff(func_def_5, type, g_s0_0: set_0).
% 12.82/2.07 tff(func_def_6, type, g_s1_1: $int).
% 12.82/2.07 tff(func_def_7, type, g_s2_2: $int).
% 12.82/2.07 tff(func_def_8, type, g_s3_3: $int).
% 12.82/2.07 tff(func_def_9, type, g_s4_4: set_0).
% 12.82/2.07 tff(func_def_10, type, g_s5_5: $int).
% 12.82/2.07 tff(func_def_11, type, g_s6_6: $int).
% 12.82/2.07 tff(func_def_12, type, g_s7_7: $int).
% 12.82/2.07 tff(func_def_13, type, g_s8_8: set_0).
% 12.82/2.07 tff(func_def_14, type, g_s9_9: $int).
% 12.82/2.07 tff(func_def_15, type, g_s10_10: $int).
% 12.82/2.07 tff(func_def_16, type, g_s11_11: $int).
% 12.82/2.07 tff(func_def_17, type, g_s12_12: set_0).
% 12.82/2.07 tff(func_def_18, type, g_s13_13: $int).
% 12.82/2.07 tff(func_def_19, type, g_s14_14: $int).
% 12.82/2.07 tff(func_def_20, type, g_s15_15: set_0).
% 12.82/2.07 tff(func_def_21, type, g_s16_16: $int).
% 12.82/2.07 tff(func_def_22, type, g_s17_17: $int).
% 12.82/2.07 tff(func_def_23, type, g_s18_18: set_0).
% 12.82/2.07 tff(func_def_24, type, g_s19_19: $int).
% 12.82/2.07 tff(func_def_25, type, g_s20_20: $int).
% 12.82/2.07 tff(func_def_26, type, g_s21_21: $int).
% 12.82/2.07 tff(func_def_27, type, g_s22_22: set_0).
% 12.82/2.07 tff(func_def_28, type, g_s23_23: $int).
% 12.82/2.07 tff(func_def_29, type, g_s24_24: $int).
% 12.82/2.07 tff(func_def_30, type, g_s25_25: set_0).
% 12.82/2.07 tff(func_def_31, type, g_s26_26: $int).
% 12.82/2.07 tff(func_def_32, type, g_s27_27: $int).
% 12.82/2.07 tff(func_def_33, type, g_s28_28: $int).
% 12.82/2.07 tff(func_def_34, type, g_s29_29: set_0).
% 12.82/2.07 tff(func_def_35, type, set_2_empty: set_2).
% 12.82/2.07 tff(func_def_36, type, set_2_insert: set_2 > set_2).
% 12.82/2.07 tff(func_def_37, type, g_s30_30: set_0).
% 12.82/2.07 tff(func_def_38, type, g_s31_31: $int).
% 12.82/2.07 tff(func_def_39, type, g_s32_32: $int).
% 12.82/2.07 tff(func_def_40, type, g_s33_33: $int).
% 12.82/2.07 tff(func_def_41, type, g_s34_34: set_0).
% 12.82/2.07 tff(func_def_42, type, g_s35_35: set_0).
% 12.82/2.07 tff(func_def_43, type, g_s36_36: set_0).
% 12.82/2.07 tff(func_def_44, type, g_s37_37: set_0).
% 12.82/2.07 tff(func_def_45, type, g_s38_38: set_0).
% 12.82/2.07 tff(func_def_46, type, g_s39_39: set_0).
% 12.82/2.07 tff(func_def_47, type, g_s40_40: set_0).
% 12.82/2.07 tff(func_def_48, type, g_s41_41: $int).
% 12.82/2.07 tff(func_def_49, type, g_s42_42: set_2).
% 12.82/2.07 tff(func_def_50, type, g_s43_43: set_0).
% 12.82/2.07 tff(func_def_51, type, g_s44_44: set_2).
% 12.82/2.07 tff(func_def_52, type, g_s45_45: set_2).
% 12.82/2.07 tff(func_def_53, type, g_s46_46: set_0).
% 12.82/2.07 tff(func_def_54, type, g_s47_47: $int).
% 12.82/2.07 tff(func_def_55, type, g_s48_48: set_2).
% 12.82/2.07 tff(func_def_56, type, g_s49_49: set_0).
% 12.82/2.07 tff(func_def_57, type, g_s50_50: set_2).
% 12.82/2.07 tff(func_def_58, type, g_s51_51: $int).
% 12.82/2.07 tff(func_def_59, type, g_s52_52: set_0).
% 12.82/2.07 tff(func_def_60, type, g_s53_53: $int).
% 12.82/2.07 tff(func_def_61, type, g_s54_54: set_2).
% 12.82/2.07 tff(func_def_62, type, g_s55_55: set_0).
% 12.82/2.07 tff(func_def_63, type, g_s56_56: $int).
% 12.82/2.07 tff(func_def_64, type, g_s57_57: set_2).
% 12.82/2.07 tff(func_def_65, type, g_s58_58: set_0).
% 12.82/2.07 tff(func_def_66, type, g_s59_59: $int).
% 12.82/2.07 tff(func_def_67, type, g_s60_60: set_2).
% 12.82/2.07 tff(func_def_68, type, set_3_empty: set_3).
% 12.82/2.07 tff(func_def_69, type, set_3_insert: set_3 > set_3).
% 12.82/2.07 tff(func_def_70, type, g_s61_72: set_3).
% 12.82/2.07 tff(func_def_71, type, g_s62_73: set_2).
% 12.82/2.07 tff(func_def_72, type, g_s63_74: set_2).
% 12.82/2.07 tff(func_def_73, type, set_4_empty: set_4).
% 12.82/2.07 tff(func_def_74, type, set_4_insert: set_4 > set_4).
% 12.82/2.07 tff(func_def_75, type, g_s64_75: set_4).
% 12.82/2.07 tff(func_def_76, type, g_s65_76: set_2).
% 12.82/2.07 tff(func_def_77, type, g_s75_61: set_3).
% 12.82/2.07 tff(func_def_78, type, g_s76_67: set_2).
% 12.82/2.07 tff(func_def_79, type, g_s78_64: set_2).
% 12.82/2.07 tff(func_def_80, type, g_s79_65: set_2).
% 12.82/2.07 tff(func_def_81, type, g_s80_66: set_2).
% 12.82/2.07 tff(func_def_82, type, g_s82_62: set_3).
% 12.82/2.07 tff(func_def_83, type, g_s83_63: set_0).
% 12.82/2.07 tff(func_def_84, type, g_s84_68: set_3).
% 12.82/2.07 tff(func_def_85, type, g_s68_1_77: $int).
% 12.82/2.07 tff(func_def_86, type, g_s69_1_78: $int).
% 12.82/2.07 tff(func_def_87, type, g_s70_1_79: $int).
% 12.82/2.07 tff(func_def_88, type, g_s71_1_80: $int).
% 12.82/2.07 tff(func_def_89, type, g_s90_81: $int).
% 12.82/2.07 tff(func_def_93, type, sK12: set_4).
% 12.82/2.07 tff(func_def_94, type, sK13: $int > set_0).
% 12.82/2.07 tff(func_def_95, type, sK14: $int).
% 12.82/2.07 tff(func_def_96, type, sK15: set_2).
% 12.82/2.07 tff(func_def_97, type, sK16: $int > $int).
% 12.82/2.07 tff(func_def_98, type, sK17: ($int * $int) > $int).
% 12.82/2.07 tff(func_def_99, type, sK18: ($int * $int) > set_0).
% 12.82/2.07 tff(func_def_100, type, sK19: ($int * $int) > $int).
% 12.82/2.07 tff(func_def_101, type, sK20: $int > $int).
% 12.82/2.07 tff(func_def_102, type, sK21: ($int * $int) > set_0).
% 12.82/2.07 tff(func_def_103, type, sK22: ($int * $int) > set_0).
% 12.82/2.07 tff(func_def_104, type, sK23: ($int * $int) > set_0).
% 12.82/2.07 tff(func_def_105, type, sK24: ($int * $int) > set_0).
% 12.82/2.07 tff(func_def_106, type, sK25: ($int * $int) > set_0).
% 12.82/2.07 tff(func_def_107, type, sK26: ($int * $int) > set_0).
% 12.82/2.07 tff(func_def_108, type, sK27: ($int * set_0) > $int).
% 12.82/2.07 tff(func_def_109, type, sK28: ($int * $int) > $int).
% 12.82/2.07 tff(func_def_110, type, sK29: ($int * $int) > $int).
% 12.82/2.07 tff(func_def_111, type, sK30: ($int * $int) > set_0).
% 12.82/2.07 tff(func_def_112, type, sK31: ($int * $int) > set_0).
% 12.82/2.07 tff(func_def_113, type, sK32: ($int * $int) > $int).
% 12.82/2.07 tff(func_def_114, type, sK33: ($int * $int) > set_0).
% 12.82/2.07 tff(func_def_115, type, sK34: ($int * $int) > set_0).
% 12.82/2.07 tff(func_def_116, type, sK35: ($int * $int) > $int).
% 12.82/2.07 tff(func_def_117, type, sK36: set_0 > $int).
% 12.82/2.07 tff(func_def_118, type, sK37: $int).
% 12.82/2.07 tff(func_def_119, type, sK38: $int).
% 12.82/2.07 tff(func_def_120, type, sK39: set_2).
% 12.82/2.07 tff(func_def_121, type, sK40: set_2).
% 12.82/2.07 tff(func_def_122, type, sK41: $int > $int).
% 12.82/2.07 tff(func_def_123, type, sK42: $int > $int).
% 12.82/2.07 tff(func_def_124, type, sK43: $int).
% 12.82/2.07 tff(func_def_125, type, sK44: $int).
% 12.82/2.07 tff(func_def_126, type, sK45: set_2).
% 12.82/2.07 tff(func_def_127, type, sK46: set_2).
% 12.82/2.07 tff(func_def_128, type, sK47: $int > $int).
% 12.82/2.07 tff(func_def_129, type, sK48: $int > $int).
% 12.82/2.07 tff(func_def_130, type, sK49: $int).
% 12.82/2.07 tff(func_def_131, type, sK50: $int).
% 12.82/2.07 tff(func_def_132, type, sK51: set_2).
% 12.82/2.07 tff(func_def_133, type, sK52: set_2).
% 12.82/2.07 tff(func_def_134, type, sK53: $int > $int).
% 12.82/2.07 tff(func_def_135, type, sK54: $int > $int).
% 12.82/2.07 tff(func_def_136, type, sK55: $int).
% 12.82/2.07 tff(func_def_137, type, sK56: $int > $int).
% 12.82/2.07 tff(func_def_138, type, sK57: $int > $int).
% 12.82/2.07 tff(func_def_139, type, sK58: $int > $int).
% 12.82/2.07 tff(func_def_140, type, sK59: $int > $int).
% 12.82/2.07 tff(func_def_141, type, sK60: $int).
% 12.82/2.07 tff(func_def_142, type, sK61: $int).
% 12.82/2.07 tff(func_def_143, type, sK62: $int > $int).
% 12.82/2.07 tff(func_def_144, type, sK63: $int > $int).
% 12.82/2.07 tff(func_def_145, type, sK64: $int > $int).
% 12.82/2.07 tff(func_def_146, type, sK65: $int > $int).
% 12.82/2.07 tff(func_def_147, type, sK66: $int).
% 12.82/2.07 tff(func_def_148, type, sK67: $int).
% 12.82/2.07 tff(func_def_149, type, sK68: $int > $int).
% 12.82/2.07 tff(func_def_150, type, sK69: $int > $int).
% 12.82/2.07 tff(func_def_151, type, sK70: $int > $int).
% 12.82/2.07 tff(func_def_152, type, sK71: $int > $int).
% 12.82/2.07 tff(func_def_153, type, sK72: $int).
% 12.82/2.07 tff(func_def_154, type, sK73: $int).
% 12.82/2.07 tff(func_def_155, type, sK74: set_2).
% 12.82/2.07 tff(func_def_156, type, sK75: $int > $int).
% 12.82/2.07 tff(func_def_157, type, sK76: $int > $int).
% 12.82/2.07 tff(func_def_158, type, sK77: set_2).
% 12.82/2.07 tff(func_def_159, type, sK78: $int > $int).
% 12.82/2.07 tff(func_def_160, type, sK79: $int > $int).
% 12.82/2.07 tff(func_def_161, type, sK80: set_2).
% 12.82/2.07 tff(func_def_162, type, sK81: $int > $int).
% 12.82/2.07 tff(func_def_163, type, sK82: $int > $int).
% 12.82/2.07 tff(func_def_164, type, sK83: $int).
% 12.82/2.07 tff(func_def_165, type, sK84: set_2).
% 12.82/2.07 tff(func_def_166, type, sK85: $int > $int).
% 12.82/2.07 tff(func_def_167, type, sK86: $int > $int).
% 12.82/2.07 tff(func_def_168, type, sK87: set_2).
% 12.82/2.07 tff(func_def_169, type, sK88: $int > $int).
% 12.82/2.07 tff(func_def_170, type, sK89: $int > $int).
% 12.82/2.07 tff(func_def_171, type, sK90: $int).
% 12.82/2.07 tff(func_def_172, type, sK91: $int).
% 12.82/2.07 tff(func_def_173, type, sK92: set_2).
% 12.82/2.07 tff(func_def_174, type, sK93: $int > $int).
% 12.82/2.07 tff(func_def_175, type, sK94: $int > $int).
% 12.82/2.07 tff(func_def_176, type, sK95: $int).
% 12.82/2.07 tff(func_def_177, type, sK96: set_2).
% 12.82/2.07 tff(func_def_178, type, sK97: $int > $int).
% 12.82/2.07 tff(func_def_179, type, sK98: $int > $int).
% 12.82/2.07 tff(func_def_180, type, sK99: $int).
% 12.82/2.07 tff(func_def_181, type, sK100: set_2).
% 12.82/2.07 tff(func_def_182, type, sK101: $int > $int).
% 12.82/2.07 tff(func_def_183, type, sK102: $int > $int).
% 12.82/2.07 tff(func_def_184, type, sK103: $int).
% 12.82/2.07 tff(func_def_185, type, sK104: $int).
% 12.82/2.07 tff(func_def_186, type, sK105: set_2).
% 12.82/2.07 tff(func_def_187, type, sK106: set_2).
% 12.82/2.07 tff(func_def_188, type, sK107: $int > $int).
% 12.82/2.07 tff(func_def_189, type, sK108: $int > $int).
% 12.82/2.07 tff(func_def_190, type, sK109: ($int * set_0) > $int).
% 12.82/2.07 tff(func_def_191, type, sK110: ($int * set_0) > $int).
% 12.82/2.07 tff(func_def_192, type, sK111: ($int * set_0) > $int).
% 12.82/2.07 tff(func_def_193, type, sK112: ($int * $int) > $int).
% 12.82/2.07 tff(func_def_194, type, sK113: ($int * $int) > $int).
% 12.82/2.07 tff(func_def_195, type, sK114: ($int * $int) > $int).
% 12.82/2.07 tff(func_def_196, type, sK115: ($int * $int) > $int).
% 12.82/2.07 tff(func_def_197, type, sK116: ($int * $int) > $int).
% 12.82/2.07 tff(func_def_198, type, sK117: set_3).
% 12.82/2.07 tff(func_def_199, type, sK118: ($int * $int) > $int).
% 12.82/2.07 tff(func_def_200, type, sK119: set_3).
% 12.82/2.07 tff(func_def_201, type, sK120: ($int * $int) > $int).
% 12.82/2.07 tff(func_def_202, type, sK121: ($int * $int) > $int).
% 12.82/2.07 tff(func_def_203, type, sK122: ($int * $int) > $int).
% 12.82/2.07 tff(func_def_204, type, sK123: ($int * $int) > $int).
% 12.82/2.07 tff(func_def_205, type, sK124: ($int * $int) > $int).
% 12.82/2.07 tff(func_def_206, type, sK125: ($int * $int) > $int).
% 12.82/2.07 tff(func_def_207, type, sK126: ($int * $int) > $int).
% 12.82/2.07 tff(func_def_208, type, sK127: set_2).
% 12.82/2.07 tff(func_def_209, type, sK128: $int > $int).
% 12.82/2.07 tff(func_def_210, type, sK129: set_2).
% 12.82/2.07 tff(func_def_211, type, sK130: $int > $int).
% 12.82/2.07 tff(func_def_212, type, sK131: set_2).
% 12.82/2.07 tff(func_def_213, type, sK132: $int > $int).
% 12.82/2.07 tff(func_def_214, type, sK133: set_2).
% 12.82/2.07 tff(func_def_215, type, sK134: $int > $int).
% 12.82/2.07 tff(func_def_216, type, sK135: set_3).
% 12.82/2.07 tff(func_def_217, type, sK136: ($int * $int) > $int).
% 12.82/2.07 tff(func_def_218, type, sK137: $int).
% 12.82/2.07 tff(func_def_219, type, sK138: set_2).
% 12.82/2.07 tff(func_def_220, type, sK139: $int > $int).
% 12.82/2.07 tff(func_def_221, type, sK140: ($int * $int) > $int).
% 12.82/2.07 tff(func_def_222, type, sK141: ($int * $int) > $int).
% 12.82/2.07 tff(func_def_223, type, sK142: ($int * $int) > $int).
% 12.82/2.07 tff(func_def_224, type, sK143: ($int * $int) > $int).
% 12.82/2.07 tff(func_def_225, type, sK144: set_0).
% 12.82/2.07 tff(func_def_226, type, sK145: $int).
% 12.82/2.07 tff(func_def_227, type, sK146: $int).
% 12.82/2.07 tff(pred_def_1, type, mem0: ($int * set_0) > $o).
% 12.82/2.07 tff(pred_def_2, type, mem2: ($int * $int * set_2) > $o).
% 12.82/2.07 tff(pred_def_3, type, mem3: ($int * $int * $int * set_3) > $o).
% 12.82/2.07 tff(pred_def_4, type, mem4: ($int * set_0 * set_4) > $o).
% 12.82/2.07 tff(pred_def_8, type, sP0: $int > $o).
% 12.82/2.07 tff(pred_def_9, type, sP1: $int > $o).
% 12.82/2.07 tff(pred_def_10, type, sP2: ($int * $int) > $o).
% 12.82/2.07 tff(pred_def_11, type, sP3: ($int * $int) > $o).
% 12.82/2.07 tff(pred_def_12, type, sP4: ($int * $int) > $o).
% 12.82/2.07 tff(pred_def_13, type, sP5: ($int * set_0) > $o).
% 12.82/2.07 tff(pred_def_14, type, sP6: $int > $o).
% 12.82/2.07 tff(pred_def_15, type, sP7: $int > $o).
% 12.82/2.07 tff(pred_def_16, type, sP8: $int > $o).
% 12.82/2.07 tff(pred_def_17, type, sP9: ($int * set_0) > $o).
% 12.82/2.07 tff(pred_def_18, type, sP10: ($int * $int) > $o).
% 12.82/2.07 tff(pred_def_19, type, sP11: $int > $o).
% 12.82/2.07 tff(f72,axiom,(
% 12.82/2.07 ! [X0 : set_0,X1 : $int] : (mem4(X1,X0,g_s64_75) <=> (mem0(X1,g_s40_40) & ! [X2 : $int] : (mem0(X2,X0) <=> ! [X3 : $int,X4 : $int] : ((mem2(X1,X3,g_s78_64) & mem2(X1,X4,g_s79_65)) => ($greatereq(X2,X3) & $lesseq(X2,X4))))))),
% 12.82/2.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p','Define:imlprp:2')).
% 12.82/2.07 tff(f99,axiom,(
% 12.82/2.07 mem0(g_s90_81,g_s40_40)),
% 12.82/2.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p','Local_Hyp:1')).
% 12.82/2.07 tff(f100,axiom,(
% 12.82/2.07 ~ ! [X0 : set_0] : (! [X1 : $int] : (mem0(X1,X0) <=> $false) => mem4(g_s90_81,X0,g_s64_75))),
% 12.82/2.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p','Local_Hyp:2')).
% 12.82/2.07 tff(f101,conjecture,(
% 12.82/2.07 ! [X0 : $int,X1 : $int] : ((mem2(g_s90_81,X0,g_s78_64) & mem2(g_s90_81,X1,g_s79_65)) => $lesseq(X0,X1))),
% 12.82/2.07 file('/export/starexec/sandbox/benchmark/theBenchmark.p','Goal')).
% 12.82/2.07 tff(f102,negated_conjecture,(
% 12.82/2.07 ~ ! [X0 : $int,X1 : $int] : ((mem2(g_s90_81,X0,g_s78_64) & mem2(g_s90_81,X1,g_s79_65)) => $lesseq(X0,X1))),
% 12.82/2.07 inference(negated_conjecture,[status(cth)],[f101])).
% 12.82/2.07 tff(f125,plain,(
% 12.82/2.07 ! [X0 : set_0,X1 : $int] : (mem4(X1,X0,g_s64_75) <=> (mem0(X1,g_s40_40) & ! [X2 : $int] : (mem0(X2,X0) <=> ! [X3 : $int,X4 : $int] : ((mem2(X1,X3,g_s78_64) & mem2(X1,X4,g_s79_65)) => (~$less(X2,X3) & ~$less(X4,X2))))))),
% 12.82/2.07 inference(theory_normalization,[],[f72])).
% 12.82/2.07 tff(f137,plain,(
% 12.82/2.07 ~ ! [X0 : $int,X1 : $int] : ((mem2(g_s90_81,X0,g_s78_64) & mem2(g_s90_81,X1,g_s79_65)) => ~$less(X1,X0))),
% 12.82/2.07 inference(theory_normalization,[],[f102])).
% 12.82/2.07 tff(f143,definition,(
% 12.82/2.07 ( ! [X0 : $int] : (~$less(X0,X0)) )),
% 12.82/2.07 introduced(theory,[tha_non-reflexivity])).
% 12.82/2.07 tff(f144,definition,(
% 12.82/2.07 ( ! [X2 : $int,X0 : $int,X1 : $int] : ($less(X0,X2) | ~$less(X1,X2) | ~$less(X0,X1)) )),
% 12.82/2.07 introduced(theory,[tha_transitivity])).
% 12.82/2.07 tff(f145,definition,(
% 12.82/2.07 ( ! [X0 : $int,X1 : $int] : ($less(X1,X0) | $less(X0,X1) | X0 = X1) )),
% 12.82/2.07 introduced(theory,[tha_order_totality])).
% 12.82/2.07 tff(f169,plain,(
% 12.82/2.07 ~ ! [X0 : set_0] : (! [X1 : $int] : ~ mem0(X1,X0) => mem4(g_s90_81,X0,g_s64_75))),
% 12.82/2.07 inference(true_and_false_elimination,[],[f100])).
% 12.82/2.07 tff(f170,plain,(
% 12.82/2.07 ~ ! [X0 : set_0] : (! [X1 : $int] : ~mem0(X1,X0) => mem4(g_s90_81,X0,g_s64_75))),
% 12.82/2.07 inference(flattening,[],[f169])).
% 12.82/2.07 tff(f243,plain,(
% 12.82/2.07 ! [X0 : set_0,X1 : $int] : (mem4(X1,X0,g_s64_75) <=> (mem0(X1,g_s40_40) & ! [X2 : $int] : (mem0(X2,X0) <=> ! [X3 : $int,X4 : $int] : ((~$less(X2,X3) & ~$less(X4,X2)) | (~mem2(X1,X3,g_s78_64) | ~mem2(X1,X4,g_s79_65))))))),
% 12.82/2.07 inference(ennf_transformation,[],[f125])).
% 12.82/2.07 tff(f244,plain,(
% 12.82/2.07 ! [X0 : set_0,X1 : $int] : (mem4(X1,X0,g_s64_75) <=> (mem0(X1,g_s40_40) & ! [X2 : $int] : (mem0(X2,X0) <=> ! [X3 : $int,X4 : $int] : ((~$less(X2,X3) & ~$less(X4,X2)) | ~mem2(X1,X3,g_s78_64) | ~mem2(X1,X4,g_s79_65)))))),
% 12.82/2.07 inference(flattening,[],[f243])).
% 12.82/2.07 tff(f274,plain,(
% 12.82/2.07 ? [X0 : set_0] : (~mem4(g_s90_81,X0,g_s64_75) & ! [X1 : $int] : ~mem0(X1,X0))),
% 12.82/2.07 inference(ennf_transformation,[],[f170])).
% 12.82/2.07 tff(f275,plain,(
% 12.82/2.07 ? [X0 : $int,X1 : $int] : ($less(X1,X0) & (mem2(g_s90_81,X0,g_s78_64) & mem2(g_s90_81,X1,g_s79_65)))),
% 12.82/2.07 inference(ennf_transformation,[],[f137])).
% 12.82/2.07 tff(f276,plain,(
% 12.82/2.07 ? [X0 : $int,X1 : $int] : ($less(X1,X0) & mem2(g_s90_81,X0,g_s78_64) & mem2(g_s90_81,X1,g_s79_65))),
% 12.82/2.07 inference(flattening,[],[f275])).
% 12.82/2.07 tff(f291,definition,(
% 12.82/2.07 ! [X1 : $int,X0 : set_0] : (sP9(X1,X0) <=> (mem0(X1,g_s40_40) & ! [X2 : $int] : (mem0(X2,X0) <=> ! [X3 : $int,X4 : $int] : ((~$less(X2,X3) & ~$less(X4,X2)) | ~mem2(X1,X3,g_s78_64) | ~mem2(X1,X4,g_s79_65)))))),
% 12.82/2.07 introduced(definition,[new_symbols(definition,[sP9])],[predicate_definition_introduction])).
% 12.82/2.07 tff(f292,plain,(
% 12.82/2.07 ! [X0 : set_0,X1 : $int] : (mem4(X1,X0,g_s64_75) <=> sP9(X1,X0))),
% 12.82/2.07 inference(definition_folding,[],[f244,f291])).
% 12.82/2.07 tff(f418,plain,(
% 12.82/2.07 ! [X1 : $int,X0 : set_0] : ((sP9(X1,X0) | (~mem0(X1,g_s40_40) | ? [X2 : $int] : ((? [X3 : $int,X4 : $int] : (($less(X2,X3) | $less(X4,X2)) & mem2(X1,X3,g_s78_64) & mem2(X1,X4,g_s79_65)) | ~mem0(X2,X0)) & (! [X3 : $int,X4 : $int] : ((~$less(X2,X3) & ~$less(X4,X2)) | ~mem2(X1,X3,g_s78_64) | ~mem2(X1,X4,g_s79_65)) | mem0(X2,X0))))) & ((mem0(X1,g_s40_40) & ! [X2 : $int] : ((mem0(X2,X0) | ? [X3 : $int,X4 : $int] : (($less(X2,X3) | $less(X4,X2)) & mem2(X1,X3,g_s78_64) & mem2(X1,X4,g_s79_65))) & (! [X3 : $int,X4 : $int] : ((~$less(X2,X3) & ~$less(X4,X2)) | ~mem2(X1,X3,g_s78_64) | ~mem2(X1,X4,g_s79_65)) | ~mem0(X2,X0)))) | ~sP9(X1,X0)))),
% 12.82/2.07 inference(nnf_transformation,[],[f291])).
% 12.82/2.07 tff(f419,plain,(
% 12.82/2.07 ! [X1 : $int,X0 : set_0] : ((sP9(X1,X0) | ~mem0(X1,g_s40_40) | ? [X2 : $int] : ((? [X3 : $int,X4 : $int] : (($less(X2,X3) | $less(X4,X2)) & mem2(X1,X3,g_s78_64) & mem2(X1,X4,g_s79_65)) | ~mem0(X2,X0)) & (! [X3 : $int,X4 : $int] : ((~$less(X2,X3) & ~$less(X4,X2)) | ~mem2(X1,X3,g_s78_64) | ~mem2(X1,X4,g_s79_65)) | mem0(X2,X0)))) & ((mem0(X1,g_s40_40) & ! [X2 : $int] : ((mem0(X2,X0) | ? [X3 : $int,X4 : $int] : (($less(X2,X3) | $less(X4,X2)) & mem2(X1,X3,g_s78_64) & mem2(X1,X4,g_s79_65))) & (! [X3 : $int,X4 : $int] : ((~$less(X2,X3) & ~$less(X4,X2)) | ~mem2(X1,X3,g_s78_64) | ~mem2(X1,X4,g_s79_65)) | ~mem0(X2,X0)))) | ~sP9(X1,X0)))),
% 12.82/2.07 inference(flattening,[],[f418])).
% 12.82/2.07 tff(f420,plain,(
% 12.82/2.07 ! [X0 : $int,X1 : set_0] : ((sP9(X0,X1) | ~mem0(X0,g_s40_40) | ? [X2 : $int] : ((? [X3 : $int,X4 : $int] : (($less(X2,X3) | $less(X4,X2)) & mem2(X0,X3,g_s78_64) & mem2(X0,X4,g_s79_65)) | ~mem0(X2,X1)) & (! [X5 : $int,X6 : $int] : ((~$less(X2,X5) & ~$less(X6,X2)) | ~mem2(X0,X5,g_s78_64) | ~mem2(X0,X6,g_s79_65)) | mem0(X2,X1)))) & ((mem0(X0,g_s40_40) & ! [X7 : $int] : ((mem0(X7,X1) | ? [X8 : $int,X9 : $int] : (($less(X7,X8) | $less(X9,X7)) & mem2(X0,X8,g_s78_64) & mem2(X0,X9,g_s79_65))) & (! [X10 : $int,X11 : $int] : ((~$less(X7,X10) & ~$less(X11,X7)) | ~mem2(X0,X10,g_s78_64) | ~mem2(X0,X11,g_s79_65)) | ~mem0(X7,X1)))) | ~sP9(X0,X1)))),
% 12.82/2.07 inference(rectify,[],[f419])).
% 12.82/2.07 tff(f421,plain,(
% 12.82/2.07 ! [X0 : $int,X1 : set_0] : ((sP9(X0,X1) | ~mem0(X0,g_s40_40) | (((($less(sK109(X0,X1),sK110(X0,X1)) | $less(sK111(X0,X1),sK109(X0,X1))) & mem2(X0,sK110(X0,X1),g_s78_64) & mem2(X0,sK111(X0,X1),g_s79_65)) | ~mem0(sK109(X0,X1),X1)) & (! [X5 : $int,X6 : $int] : ((~$less(sK109(X0,X1),X5) & ~$less(X6,sK109(X0,X1))) | ~mem2(X0,X5,g_s78_64) | ~mem2(X0,X6,g_s79_65)) | mem0(sK109(X0,X1),X1)))) & ((mem0(X0,g_s40_40) & ! [X7 : $int] : ((mem0(X7,X1) | (($less(X7,sK112(X0,X7)) | $less(sK113(X0,X7),X7)) & mem2(X0,sK112(X0,X7),g_s78_64) & mem2(X0,sK113(X0,X7),g_s79_65))) & (! [X10 : $int,X11 : $int] : ((~$less(X7,X10) & ~$less(X11,X7)) | ~mem2(X0,X10,g_s78_64) | ~mem2(X0,X11,g_s79_65)) | ~mem0(X7,X1)))) | ~sP9(X0,X1)))),
% 12.82/2.07 inference(skolemize,[status(esa),new_symbols(skolem,[sK109,sK110,sK111,sK112,sK113]),skolemize(X2,sK109(X0,X1)),skolemize(X3,sK110(X0,X1)),skolemize(X4,sK111(X0,X1)),skolemize(X8,sK112(X0,X7)),skolemize(X9,sK113(X0,X7))],[f420])).
% 12.82/2.07 tff(f422,plain,(
% 12.82/2.07 ! [X0 : set_0,X1 : $int] : ((mem4(X1,X0,g_s64_75) | ~sP9(X1,X0)) & (sP9(X1,X0) | ~mem4(X1,X0,g_s64_75)))),
% 12.82/2.07 inference(nnf_transformation,[],[f292])).
% 12.82/2.07 tff(f467,plain,(
% 12.82/2.07 ~mem4(g_s90_81,sK144,g_s64_75) & ! [X1 : $int] : ~mem0(X1,sK144)),
% 12.82/2.07 inference(skolemize,[status(esa),new_symbols(skolem,[sK144]),skolemize(X0,sK144)],[f274])).
% 12.82/2.07 tff(f468,plain,(
% 12.82/2.07 $less(sK146,sK145) & mem2(g_s90_81,sK145,g_s78_64) & mem2(g_s90_81,sK146,g_s79_65)),
% 12.82/2.07 inference(skolemize,[status(esa),new_symbols(skolem,[sK145,sK146]),skolemize(X0,sK145),skolemize(X1,sK146)],[f276])).
% 12.82/2.07 tff(f813,plain,(
% 12.82/2.07 ( ! [X0 : $int,X1 : set_0,X6 : $int,X5 : $int] : (sP9(X0,X1) | ~mem0(X0,g_s40_40) | ~$less(X6,sK109(X0,X1)) | ~mem2(X0,X5,g_s78_64) | ~mem2(X0,X6,g_s79_65) | mem0(sK109(X0,X1),X1)) )),
% 12.82/2.07 inference(cnf_transformation,[],[f421])).
% 12.82/2.07 tff(f814,plain,(
% 12.82/2.07 ( ! [X0 : $int,X1 : set_0,X6 : $int,X5 : $int] : (sP9(X0,X1) | ~mem0(X0,g_s40_40) | ~$less(sK109(X0,X1),X5) | ~mem2(X0,X5,g_s78_64) | ~mem2(X0,X6,g_s79_65) | mem0(sK109(X0,X1),X1)) )),
% 12.82/2.07 inference(cnf_transformation,[],[f421])).
% 12.82/2.07 tff(f819,plain,(
% 12.82/2.07 ( ! [X0 : set_0,X1 : $int] : (mem4(X1,X0,g_s64_75) | ~sP9(X1,X0)) )),
% 12.82/2.07 inference(cnf_transformation,[],[f422])).
% 12.82/2.07 tff(f916,plain,(
% 12.82/2.07 mem0(g_s90_81,g_s40_40)),
% 12.82/2.07 inference(cnf_transformation,[],[f99])).
% 12.82/2.07 tff(f917,plain,(
% 12.82/2.07 ( ! [X1 : $int] : (~mem0(X1,sK144)) )),
% 12.82/2.07 inference(cnf_transformation,[],[f467])).
% 12.82/2.07 tff(f918,plain,(
% 12.82/2.07 ~mem4(g_s90_81,sK144,g_s64_75)),
% 12.82/2.07 inference(cnf_transformation,[],[f467])).
% 12.82/2.07 tff(f919,plain,(
% 12.82/2.07 mem2(g_s90_81,sK146,g_s79_65)),
% 12.82/2.07 inference(cnf_transformation,[],[f468])).
% 12.82/2.07 tff(f920,plain,(
% 12.82/2.07 mem2(g_s90_81,sK145,g_s78_64)),
% 12.82/2.07 inference(cnf_transformation,[],[f468])).
% 12.82/2.07 tff(f921,plain,(
% 12.82/2.07 $less(sK146,sK145)),
% 12.82/2.07 inference(cnf_transformation,[],[f468])).
% 12.82/2.07 tff(f1152,plain,(
% 12.82/2.07 ~sP9(g_s90_81,sK144)),
% 12.82/2.07 inference(resolution,[],[f819,f918])).
% 12.82/2.07 tff(f1346,plain,(
% 12.82/2.07 ( ! [X0 : $int,X1 : $int] : (~$less(X0,X1) | ~$less(X1,X0)) )),
% 12.82/2.07 inference(resolution,[],[f144,f143])).
% 12.82/2.07 tff(f3217,definition,(
% 12.82/2.07 spl147_186 <=> ! [X0 : $int] : ~mem2(g_s90_81,X0,g_s78_64)),
% 12.82/2.07 introduced(definition,[new_symbols(definition,[spl147_186])],[avatar_definition])).
% 12.82/2.07 tff(f3218,plain,(
% 12.82/2.07 ( ! [X0 : $int] : (~mem2(g_s90_81,X0,g_s78_64)) ) | ~spl147_186),
% 12.82/2.07 inference(avatar_component_clause,[],[f3217])).
% 12.82/2.07 tff(f3297,definition,(
% 12.82/2.07 spl147_188 <=> ! [X0 : $int] : ~mem2(g_s90_81,X0,g_s79_65)),
% 12.82/2.07 introduced(definition,[new_symbols(definition,[spl147_188])],[avatar_definition])).
% 12.82/2.07 tff(f3298,plain,(
% 12.82/2.07 ( ! [X0 : $int] : (~mem2(g_s90_81,X0,g_s79_65)) ) | ~spl147_188),
% 12.82/2.07 inference(avatar_component_clause,[],[f3297])).
% 12.82/2.07 tff(f3333,plain,(
% 12.82/2.07 $false | ~spl147_186),
% 12.82/2.07 inference(resolution,[],[f3218,f920])).
% 12.82/2.07 tff(f3338,plain,(
% 12.82/2.07 ~spl147_186),
% 12.82/2.07 inference(avatar_contradiction_clause,[],[f3333])).
% 12.82/2.07 tff(f3356,plain,(
% 12.82/2.07 $false | ~spl147_188),
% 12.82/2.07 inference(resolution,[],[f3298,f919])).
% 12.82/2.07 tff(f3361,plain,(
% 12.82/2.07 ~spl147_188),
% 12.82/2.07 inference(avatar_contradiction_clause,[],[f3356])).
% 12.82/2.07 tff(f3710,plain,(
% 12.82/2.07 ( ! [X0 : $int,X1 : $int] : (~mem0(g_s90_81,g_s40_40) | ~$less(X0,sK109(g_s90_81,sK144)) | ~mem2(g_s90_81,X1,g_s78_64) | ~mem2(g_s90_81,X0,g_s79_65) | mem0(sK109(g_s90_81,sK144),sK144)) )),
% 12.82/2.07 inference(resolution,[],[f813,f1152])).
% 12.82/2.07 tff(f3713,plain,(
% 12.82/2.07 ( ! [X0 : $int,X1 : $int] : (~$less(X0,sK109(g_s90_81,sK144)) | ~mem2(g_s90_81,X1,g_s78_64) | ~mem2(g_s90_81,X0,g_s79_65) | mem0(sK109(g_s90_81,sK144),sK144)) )),
% 12.82/2.07 inference(forward_subsumption_resolution,[],[f3710,f916])).
% 12.82/2.07 tff(f3714,plain,(
% 12.82/2.07 ( ! [X0 : $int,X1 : $int] : (~$less(X0,sK109(g_s90_81,sK144)) | ~mem2(g_s90_81,X1,g_s78_64) | ~mem2(g_s90_81,X0,g_s79_65)) )),
% 12.82/2.07 inference(forward_subsumption_resolution,[],[f3713,f917])).
% 12.82/2.07 tff(f3716,definition,(
% 12.82/2.07 spl147_217 <=> ! [X0 : $int] : (~$less(X0,sK109(g_s90_81,sK144)) | ~mem2(g_s90_81,X0,g_s79_65))),
% 12.82/2.07 introduced(definition,[new_symbols(definition,[spl147_217])],[avatar_definition])).
% 12.82/2.07 tff(f3717,plain,(
% 12.82/2.07 ( ! [X0 : $int] : (~mem2(g_s90_81,X0,g_s79_65) | ~$less(X0,sK109(g_s90_81,sK144))) ) | ~spl147_217),
% 12.82/2.07 inference(avatar_component_clause,[],[f3716])).
% 12.82/2.07 tff(f3718,plain,(
% 12.82/2.07 spl147_186 | spl147_217),
% 12.82/2.07 inference(avatar_split_clause,[],[f3714,f3716,f3217])).
% 12.82/2.07 tff(f3739,plain,(
% 12.82/2.07 ( ! [X0 : $int,X1 : $int] : (~mem0(g_s90_81,g_s40_40) | ~$less(sK109(g_s90_81,sK144),X0) | ~mem2(g_s90_81,X0,g_s78_64) | ~mem2(g_s90_81,X1,g_s79_65) | mem0(sK109(g_s90_81,sK144),sK144)) )),
% 12.82/2.07 inference(resolution,[],[f814,f1152])).
% 12.82/2.07 tff(f3742,plain,(
% 12.82/2.07 ( ! [X0 : $int,X1 : $int] : (~$less(sK109(g_s90_81,sK144),X0) | ~mem2(g_s90_81,X0,g_s78_64) | ~mem2(g_s90_81,X1,g_s79_65) | mem0(sK109(g_s90_81,sK144),sK144)) )),
% 12.82/2.07 inference(forward_subsumption_resolution,[],[f3739,f916])).
% 12.82/2.07 tff(f3743,plain,(
% 12.82/2.07 ( ! [X0 : $int,X1 : $int] : (~$less(sK109(g_s90_81,sK144),X0) | ~mem2(g_s90_81,X0,g_s78_64) | ~mem2(g_s90_81,X1,g_s79_65)) )),
% 12.82/2.07 inference(forward_subsumption_resolution,[],[f3742,f917])).
% 12.82/2.07 tff(f3745,definition,(
% 12.82/2.07 spl147_218 <=> ! [X0 : $int] : (~$less(sK109(g_s90_81,sK144),X0) | ~mem2(g_s90_81,X0,g_s78_64))),
% 12.82/2.07 introduced(definition,[new_symbols(definition,[spl147_218])],[avatar_definition])).
% 12.82/2.07 tff(f3746,plain,(
% 12.82/2.07 ( ! [X0 : $int] : (~mem2(g_s90_81,X0,g_s78_64) | ~$less(sK109(g_s90_81,sK144),X0)) ) | ~spl147_218),
% 12.82/2.07 inference(avatar_component_clause,[],[f3745])).
% 12.82/2.07 tff(f3747,plain,(
% 12.82/2.07 spl147_188 | spl147_218),
% 12.82/2.07 inference(avatar_split_clause,[],[f3743,f3745,f3297])).
% 12.82/2.07 tff(f5164,plain,(
% 12.82/2.07 ~$less(sK145,sK146)),
% 12.82/2.07 inference(resolution,[],[f1346,f921])).
% 12.82/2.07 tff(f12919,plain,(
% 12.82/2.07 ( ! [X0 : $int] : (~$less(X0,sK146) | ~$less(sK145,X0)) )),
% 12.82/2.07 inference(resolution,[],[f5164,f144])).
% 12.82/2.07 tff(f45642,plain,(
% 12.82/2.07 ~$less(sK146,sK109(g_s90_81,sK144)) | ~spl147_217),
% 12.82/2.07 inference(resolution,[],[f3717,f919])).
% 12.82/2.07 tff(f45664,plain,(
% 12.82/2.07 $less(sK109(g_s90_81,sK144),sK146) | sK146 = sK109(g_s90_81,sK144) | ~spl147_217),
% 12.82/2.07 inference(resolution,[],[f45642,f145])).
% 12.82/2.07 tff(f45667,definition,(
% 12.82/2.07 spl147_2578 <=> sK146 = sK109(g_s90_81,sK144)),
% 12.82/2.07 introduced(definition,[new_symbols(definition,[spl147_2578])],[avatar_definition])).
% 12.82/2.07 tff(f45668,plain,(
% 12.82/2.07 sK146 = sK109(g_s90_81,sK144) | ~spl147_2578),
% 12.82/2.07 inference(avatar_component_clause,[],[f45667])).
% 12.82/2.07 tff(f45670,definition,(
% 12.82/2.07 spl147_2579 <=> $less(sK109(g_s90_81,sK144),sK146)),
% 12.82/2.07 introduced(definition,[new_symbols(definition,[spl147_2579])],[avatar_definition])).
% 12.82/2.07 tff(f45671,plain,(
% 12.82/2.07 $less(sK109(g_s90_81,sK144),sK146) | ~spl147_2579),
% 12.82/2.07 inference(avatar_component_clause,[],[f45670])).
% 12.82/2.07 tff(f45672,plain,(
% 12.82/2.07 spl147_2578 | spl147_2579 | ~spl147_217),
% 12.82/2.07 inference(avatar_split_clause,[],[f45664,f3716,f45670,f45667])).
% 12.82/2.07 tff(f45677,plain,(
% 12.82/2.07 ~$less(sK109(g_s90_81,sK144),sK145) | ~spl147_218),
% 12.82/2.07 inference(resolution,[],[f3746,f920])).
% 12.82/2.07 tff(f45695,plain,(
% 12.82/2.07 $less(sK145,sK109(g_s90_81,sK144)) | sK145 = sK109(g_s90_81,sK144) | ~spl147_218),
% 12.82/2.07 inference(resolution,[],[f45677,f145])).
% 12.82/2.07 tff(f45698,definition,(
% 12.82/2.07 spl147_2582 <=> sK145 = sK109(g_s90_81,sK144)),
% 12.82/2.07 introduced(definition,[new_symbols(definition,[spl147_2582])],[avatar_definition])).
% 12.82/2.07 tff(f45699,plain,(
% 12.82/2.07 sK145 = sK109(g_s90_81,sK144) | ~spl147_2582),
% 12.82/2.07 inference(avatar_component_clause,[],[f45698])).
% 12.82/2.07 tff(f45701,definition,(
% 12.82/2.07 spl147_2583 <=> $less(sK145,sK109(g_s90_81,sK144))),
% 12.82/2.07 introduced(definition,[new_symbols(definition,[spl147_2583])],[avatar_definition])).
% 12.82/2.07 tff(f45702,plain,(
% 12.82/2.07 $less(sK145,sK109(g_s90_81,sK144)) | ~spl147_2583),
% 12.82/2.07 inference(avatar_component_clause,[],[f45701])).
% 12.82/2.07 tff(f45703,plain,(
% 12.82/2.07 spl147_2582 | spl147_2583 | ~spl147_218),
% 12.82/2.07 inference(avatar_split_clause,[],[f45695,f3745,f45701,f45698])).
% 12.82/2.07 tff(f45769,plain,(
% 12.82/2.07 ~$less(sK146,sK145) | (~spl147_218 | ~spl147_2578)),
% 12.82/2.07 inference(superposition,[],[f45677,f45668])).
% 12.82/2.07 tff(f45776,plain,(
% 12.82/2.07 $false | (~spl147_218 | ~spl147_2578)),
% 12.82/2.07 inference(forward_subsumption_resolution,[],[f45769,f921])).
% 12.82/2.07 tff(f45777,plain,(
% 12.82/2.07 ~spl147_218 | ~spl147_2578),
% 12.82/2.07 inference(avatar_contradiction_clause,[],[f45776])).
% 12.82/2.07 tff(f45839,plain,(
% 12.82/2.07 ~$less(sK145,sK109(g_s90_81,sK144)) | ~spl147_2579),
% 12.82/2.07 inference(resolution,[],[f45671,f12919])).
% 12.82/2.07 tff(f46233,plain,(
% 12.82/2.07 ~$less(sK146,sK145) | (~spl147_217 | ~spl147_2582)),
% 12.82/2.07 inference(superposition,[],[f45642,f45699])).
% 12.82/2.07 tff(f46239,plain,(
% 12.82/2.07 $false | (~spl147_217 | ~spl147_2582)),
% 12.82/2.07 inference(forward_subsumption_resolution,[],[f46233,f921])).
% 12.82/2.07 tff(f46240,plain,(
% 12.82/2.07 ~spl147_217 | ~spl147_2582),
% 12.82/2.07 inference(avatar_contradiction_clause,[],[f46239])).
% 12.82/2.07 tff(f46262,plain,(
% 12.82/2.07 $false | (~spl147_2579 | ~spl147_2583)),
% 12.82/2.07 inference(forward_subsumption_resolution,[],[f45839,f45702])).
% 12.82/2.07 tff(f46263,plain,(
% 12.82/2.07 ~spl147_2579 | ~spl147_2583),
% 12.82/2.07 inference(avatar_contradiction_clause,[],[f46262])).
% 12.82/2.07 cnf(s160, plain, ~spl147_186, inference(sat_conversion,[],[f3338])).
% 12.82/2.07 cnf(s162, plain, ~spl147_188, inference(sat_conversion,[],[f3361])).
% 12.82/2.07 cnf(s188, plain, spl147_186 | spl147_217, inference(sat_conversion,[],[f3718])).
% 12.82/2.07 cnf(s192, plain, spl147_188 | spl147_218, inference(sat_conversion,[],[f3747])).
% 12.82/2.07 cnf(s3580, plain, ~spl147_217 | spl147_2578 | spl147_2579, inference(sat_conversion,[],[f45672])).
% 12.82/2.07 cnf(s3583, plain, ~spl147_218 | spl147_2582 | spl147_2583, inference(sat_conversion,[],[f45703])).
% 12.82/2.07 cnf(s3584, plain, ~spl147_218 | ~spl147_2578, inference(sat_conversion,[],[f45777])).
% 12.82/2.07 cnf(s3585, plain, ~spl147_217 | ~spl147_2582, inference(sat_conversion,[],[f46240])).
% 12.82/2.07 cnf(s3587, plain, ~spl147_2579 | ~spl147_2583, inference(sat_conversion,[],[f46263])).
% 12.82/2.07 cnf(s3789, plain, spl147_218, inference(rat,[],[s192,s162])).
% 12.82/2.07 cnf(s3795, plain, ~spl147_2578, inference(rat,[],[s3584,s3789])).
% 12.82/2.07 cnf(s3861, plain, spl147_217, inference(rat,[],[s188,s160])).
% 12.82/2.07 cnf(s3862, plain, ~spl147_2582, inference(rat,[],[s3585,s3861])).
% 12.82/2.07 cnf(s3863, plain, spl147_2579, inference(rat,[],[s3580,s3795,s3861])).
% 12.82/2.07 cnf(s3866, plain, spl147_2583, inference(rat,[],[s3583,s3789,s3862])).
% 12.82/2.07 cnf(s3867, plain, $false, inference(rat,[],[s3587,s3866,s3863])).
% 12.82/2.07 tff(f46264,plain,(
% 12.82/2.07 $false),
% 12.82/2.07 inference(avatar_sat_refutation,[],[s3867])).
% 12.82/2.07 % SZS output end Proof for theBenchmark
% 12.82/2.07 % (673874)------------------------------
% 12.82/2.07 % (673874)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 12.82/2.07 % (673874)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.82/2.07 % (673874)CaDiCaL version: 2.1.3
% 12.82/2.07 % (673874)Termination reason: Refutation
% 12.82/2.07 % (673874)Time elapsed: 1.038 s
% 12.82/2.07 % (673874)Peak memory usage: 31 MB
% 12.82/2.07 % (673874)Instructions burned: 3405 (million)
% 12.82/2.07 % (673693)Success in time 1.853 s
% 12.82/2.07 % Vampire exiting
%------------------------------------------------------------------------------