%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ITP376_1 : TPTP v9.3.1. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n012.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 11:39:28 AM UTC 2026
% Result : Theorem 91.90s 13.48s
% Output : Refutation 91.90s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ITP376_1 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.04 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.34 % Computer : n012.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.02/0.34 % CPULimit : 300
% 0.02/0.34 % WCLimit : 300
% 0.02/0.34 % DateTime : Sun Sep 27 12:55:49 UTC 2026
% 0.02/0.34 % CPUTime :
% 0.02/0.34 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.02/0.36 Running first-order model finding
% 0.02/0.36 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.92 % (2367602)Will run a generic schedule for satisfiability detection.
% 2.92/0.92 % (2367608)% WARNING: option uhcvi not known.
% 2.92/0.92 % (2367608)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2204523019:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 2.92/0.92 % (2367612)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4210152094:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 2.92/0.92 % (2367610)dis+10_1_sil=32000:sp=arity:random_seed=2976474020:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 2.92/0.92 % (2367607)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4161837972_2999 on theBenchmark for (2999ds/0Mi)
% 2.92/0.92 % (2367611)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3370088011:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 2.92/0.92 % (2367613)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=134079397:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 2.92/0.92 % (2367609)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=98141156:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 2.92/0.92 % (2367607)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 2.92/0.92 % (2367607)Terminated due to inappropriate strategy.
% 2.92/0.92 % (2367607)------------------------------
% 2.92/0.92 % (2367607)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.92/0.92 % (2367607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.92/0.92 % (2367607)CaDiCaL version: 2.1.3
% 2.92/0.92 % (2367607)Termination reason: Inappropriate
% 2.92/0.92 % (2367607)Time elapsed: 0.038 s
% 2.92/0.92 % (2367607)Peak memory usage: 12 MB
% 2.92/0.92 % (2367607)Instructions burned: 84 (million)
% 2.92/0.92 % (2367607)------------------------------
% 2.92/0.92 % (2367607)------------------------------
% 2.92/0.92 % (2367610)Instruction limit reached!
% 2.92/0.92 % (2367610)------------------------------
% 2.92/0.92 % (2367610)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.92/0.92 % (2367610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.92/0.92 % (2367610)CaDiCaL version: 2.1.3
% 2.92/0.92 % (2367610)Termination reason: Instruction limit
% 2.92/0.92 % (2367610)Termination phase: Saturation
% 2.92/0.92 % (2367610)Time elapsed: 0.049 s
% 2.92/0.92 % (2367610)Peak memory usage: 13 MB
% 2.92/0.92 % (2367610)Instructions burned: 104 (million)
% 2.92/0.92 % (2367621)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3519790467:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 2.92/0.92 % (2367611)Instruction limit reached!
% 2.92/0.92 % (2367611)------------------------------
% 2.92/0.92 % (2367611)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.92/0.92 % (2367611)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.92/0.92 % (2367611)CaDiCaL version: 2.1.3
% 2.92/0.92 % (2367611)Termination reason: Instruction limit
% 2.92/0.92 % (2367611)Termination phase: Saturation
% 2.92/0.92 % (2367611)Time elapsed: 0.054 s
% 2.92/0.92 % (2367611)Peak memory usage: 13 MB
% 2.92/0.92 % (2367611)Instructions burned: 117 (million)
% 2.92/0.92 % (2367612)Instruction limit reached!
% 2.92/0.92 % (2367612)------------------------------
% 2.92/0.92 % (2367612)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.92/0.92 % (2367612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.92/0.92 % (2367612)CaDiCaL version: 2.1.3
% 2.92/0.92 % (2367612)Termination reason: Instruction limit
% 2.92/0.92 % (2367612)Termination phase: Saturation
% 2.92/0.92 % (2367612)Time elapsed: 0.061 s
% 2.92/0.92 % (2367612)Peak memory usage: 14 MB
% 2.92/0.92 % (2367612)Instructions burned: 131 (million)
% 2.92/0.92 % (2367622)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=509629710:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 2.92/0.92 % (2367621)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 2.92/0.92 % (2367621)Terminated due to inappropriate strategy.
% 2.92/0.92 % (2367621)------------------------------
% 2.92/0.92 % (2367621)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.92/0.92 % (2367621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.92/0.92 % (2367621)CaDiCaL version: 2.1.3
% 2.92/0.92 % (2367621)Termination reason: Inappropriate
% 2.92/0.92 % (2367621)Time elapsed: 0.019 s
% 5.52/1.21 % (2367621)Peak memory usage: 12 MB
% 5.52/1.21 % (2367621)Instructions burned: 75 (million)
% 5.52/1.21 % (2367621)------------------------------
% 5.52/1.21 % (2367621)------------------------------
% 5.52/1.21 % (2367624)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=1779046181:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 5.52/1.21 % (2367625)ott-21_1_sil=16000:fs=off:random_seed=4005843325:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 5.52/1.21 % (2367613)Instruction limit reached!
% 5.52/1.21 % (2367613)------------------------------
% 5.52/1.21 % (2367613)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.52/1.21 % (2367613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.52/1.21 % (2367613)CaDiCaL version: 2.1.3
% 5.52/1.21 % (2367613)Termination reason: Instruction limit
% 5.52/1.21 % (2367613)Termination phase: Saturation
% 5.52/1.21 % (2367613)Time elapsed: 0.080 s
% 5.52/1.21 % (2367613)Peak memory usage: 14 MB
% 5.52/1.21 % (2367613)Instructions burned: 160 (million)
% 5.52/1.21 % (2367627)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3428389108:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 5.52/1.21 % (2367630)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2599858517:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 5.52/1.21 % (2367630)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 5.52/1.21 % (2367630)Terminated due to inappropriate strategy.
% 5.52/1.21 % (2367630)------------------------------
% 5.52/1.21 % (2367630)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.52/1.21 % (2367630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.52/1.21 % (2367630)CaDiCaL version: 2.1.3
% 5.52/1.21 % (2367630)Termination reason: Inappropriate
% 5.52/1.21 % (2367630)Time elapsed: 0.015 s
% 5.52/1.21 % (2367630)Peak memory usage: 12 MB
% 5.52/1.21 % (2367630)Instructions burned: 58 (million)
% 5.52/1.21 % (2367630)------------------------------
% 5.52/1.21 % (2367630)------------------------------
% 5.52/1.21 % (2367633)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=597330224:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 5.52/1.21 % (2367622)Instruction limit reached!
% 5.52/1.21 % (2367622)------------------------------
% 5.52/1.21 % (2367622)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.52/1.21 % (2367622)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.52/1.21 % (2367622)CaDiCaL version: 2.1.3
% 5.52/1.21 % (2367622)Termination reason: Instruction limit
% 5.52/1.21 % (2367622)Termination phase: Saturation
% 5.52/1.21 % (2367622)Time elapsed: 0.064 s
% 5.52/1.21 % (2367622)Peak memory usage: 14 MB
% 5.52/1.21 % (2367622)Instructions burned: 132 (million)
% 5.52/1.21 % (2367635)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3324669399:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 5.52/1.21 % (2367625)Instruction limit reached!
% 5.52/1.21 % (2367625)------------------------------
% 5.52/1.21 % (2367625)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.52/1.21 % (2367625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.52/1.21 % (2367625)CaDiCaL version: 2.1.3
% 5.52/1.21 % (2367625)Termination reason: Instruction limit
% 5.52/1.21 % (2367625)Termination phase: Saturation
% 5.52/1.21 % (2367625)Time elapsed: 0.084 s
% 5.52/1.21 % (2367625)Peak memory usage: 14 MB
% 5.52/1.21 % (2367625)Instructions burned: 180 (million)
% 5.52/1.21 % (2367635)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 5.52/1.21 % (2367635)Terminated due to inappropriate strategy.
% 5.52/1.21 % (2367635)------------------------------
% 5.52/1.21 % (2367635)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 5.52/1.21 % (2367635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.52/1.21 % (2367635)CaDiCaL version: 2.1.3
% 5.52/1.21 % (2367635)Termination reason: Inappropriate
% 5.52/1.21 % (2367635)Time elapsed: 0.021 s
% 5.52/1.21 % (2367635)Peak memory usage: 12 MB
% 5.52/1.21 % (2367635)Instructions burned: 76 (million)
% 5.52/1.21 % (2367635)------------------------------
% 5.52/1.21 % (2367635)------------------------------
% 5.52/1.21 % (2367638)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1020543602:i=879:kws=inv_precedence:fsr=off_2997 on theBenchmark for (2997ds/879Mi)
% 20.58/3.39 % (2367637)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=1533254125:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2997 on theBenchmark for (2997ds/692Mi)
% 20.58/3.39 % (2367627)Instruction limit reached!
% 20.58/3.39 % (2367627)------------------------------
% 20.58/3.39 % (2367627)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.58/3.39 % (2367627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.58/3.39 % (2367627)CaDiCaL version: 2.1.3
% 20.58/3.39 % (2367627)Termination reason: Instruction limit
% 20.58/3.39 % (2367627)Termination phase: Saturation
% 20.58/3.39 % (2367627)Time elapsed: 0.253 s
% 20.58/3.39 % (2367627)Peak memory usage: 15 MB
% 20.58/3.39 % (2367627)Instructions burned: 478 (million)
% 20.58/3.39 % (2367641)fmb+10_1_sil=64000:random_seed=3309954530:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi)
% 20.58/3.39 % (2367641)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 20.58/3.39 % (2367641)Terminated due to inappropriate strategy.
% 20.58/3.39 % (2367641)------------------------------
% 20.58/3.39 % (2367641)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.58/3.39 % (2367641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.58/3.39 % (2367641)CaDiCaL version: 2.1.3
% 20.58/3.39 % (2367641)Termination reason: Inappropriate
% 20.58/3.39 % (2367641)Time elapsed: 0.021 s
% 20.58/3.39 % (2367641)Peak memory usage: 12 MB
% 20.58/3.39 % (2367641)Instructions burned: 79 (million)
% 20.58/3.39 % (2367641)------------------------------
% 20.58/3.39 % (2367641)------------------------------
% 20.58/3.39 % (2367624)Instruction limit reached!
% 20.58/3.39 % (2367624)------------------------------
% 20.58/3.39 % (2367624)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.58/3.39 % (2367624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.58/3.39 % (2367624)CaDiCaL version: 2.1.3
% 20.58/3.39 % (2367624)Termination reason: Instruction limit
% 20.58/3.39 % (2367624)Termination phase: Saturation
% 20.58/3.39 % (2367624)Time elapsed: 0.315 s
% 20.58/3.39 % (2367624)Peak memory usage: 17 MB
% 20.58/3.39 % (2367624)Instructions burned: 685 (million)
% 20.58/3.39 % (2367644)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2945756413:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi)
% 20.58/3.39 % (2367646)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3438159090:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi)
% 20.58/3.39 % (2367644)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 20.58/3.39 % (2367644)Terminated due to inappropriate strategy.
% 20.58/3.39 % (2367644)------------------------------
% 20.58/3.39 % (2367644)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.58/3.39 % (2367644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.58/3.39 % (2367644)CaDiCaL version: 2.1.3
% 20.58/3.39 % (2367644)Termination reason: Inappropriate
% 20.58/3.39 % (2367644)Time elapsed: 0.020 s
% 20.58/3.39 % (2367644)Peak memory usage: 12 MB
% 20.58/3.39 % (2367644)Instructions burned: 75 (million)
% 20.58/3.39 % (2367644)------------------------------
% 20.58/3.39 % (2367644)------------------------------
% 20.58/3.39 % (2367648)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=32135638:i=5131_2995 on theBenchmark for (2995ds/5131Mi)
% 20.58/3.39 % (2367646)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 20.58/3.39 % (2367646)Terminated due to inappropriate strategy.
% 20.58/3.39 % (2367646)------------------------------
% 20.58/3.39 % (2367646)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 20.58/3.39 % (2367646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.58/3.39 % (2367646)CaDiCaL version: 2.1.3
% 20.58/3.39 % (2367646)Termination reason: Inappropriate
% 20.58/3.39 % (2367646)Time elapsed: 0.034 s
% 20.58/3.39 % (2367646)Peak memory usage: 12 MB
% 20.58/3.39 % (2367646)Instructions burned: 75 (million)
% 20.58/3.39 % (2367646)------------------------------
% 20.58/3.39 % (2367646)------------------------------
% 20.58/3.39 % (2367650)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3100621589:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi)
% 20.58/3.39 % (2367637)Instruction limit reached!
% 20.58/3.39 % (2367637)------------------------------
% 31.14/4.88 % (2367637)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.14/4.88 % (2367637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.14/4.88 % (2367637)CaDiCaL version: 2.1.3
% 31.14/4.88 % (2367637)Termination reason: Instruction limit
% 31.14/4.88 % (2367637)Termination phase: Saturation
% 31.14/4.88 % (2367637)Time elapsed: 0.327 s
% 31.14/4.88 % (2367637)Peak memory usage: 18 MB
% 31.14/4.88 % (2367637)Instructions burned: 693 (million)
% 31.14/4.88 % (2367652)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2702528275:i=6324_2994 on theBenchmark for (2994ds/6324Mi)
% 31.14/4.88 % (2367652)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 31.14/4.88 % (2367652)Terminated due to inappropriate strategy.
% 31.14/4.88 % (2367652)------------------------------
% 31.14/4.88 % (2367652)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.14/4.88 % (2367652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.14/4.88 % (2367652)CaDiCaL version: 2.1.3
% 31.14/4.88 % (2367652)Termination reason: Inappropriate
% 31.14/4.88 % (2367652)Time elapsed: 0.031 s
% 31.14/4.88 % (2367652)Peak memory usage: 13 MB
% 31.14/4.88 % (2367652)Instructions burned: 84 (million)
% 31.14/4.88 % (2367652)------------------------------
% 31.14/4.88 % (2367652)------------------------------
% 31.14/4.88 % (2367654)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3875346032:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi)
% 31.14/4.88 % (2367638)Instruction limit reached!
% 31.14/4.88 % (2367638)------------------------------
% 31.14/4.88 % (2367638)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.14/4.88 % (2367638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.14/4.88 % (2367638)CaDiCaL version: 2.1.3
% 31.14/4.88 % (2367638)Termination reason: Instruction limit
% 31.14/4.88 % (2367638)Termination phase: Saturation
% 31.14/4.88 % (2367638)Time elapsed: 0.404 s
% 31.14/4.88 % (2367638)Peak memory usage: 21 MB
% 31.14/4.88 % (2367638)Instructions burned: 879 (million)
% 31.14/4.88 % (2367654)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 31.14/4.88 % (2367654)Terminated due to inappropriate strategy.
% 31.14/4.88 % (2367654)------------------------------
% 31.14/4.88 % (2367654)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.14/4.88 % (2367654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.14/4.88 % (2367654)CaDiCaL version: 2.1.3
% 31.14/4.88 % (2367654)Termination reason: Inappropriate
% 31.14/4.88 % (2367654)Time elapsed: 0.021 s
% 31.14/4.88 % (2367654)Peak memory usage: 12 MB
% 31.14/4.88 % (2367654)Instructions burned: 75 (million)
% 31.14/4.88 % (2367654)------------------------------
% 31.14/4.88 % (2367654)------------------------------
% 31.14/4.88 % (2367657)ott-2_1_sil=16000:newcnf=on:random_seed=1112702771:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2993 on theBenchmark for (2993ds/869Mi)
% 31.14/4.88 % (2367658)ott+10_1_sil=32000:tgt=ground:random_seed=3202041407:i=5114:av=off_2993 on theBenchmark for (2993ds/5114Mi)
% 31.14/4.88 % (2367633)Instruction limit reached!
% 31.14/4.88 % (2367633)------------------------------
% 31.14/4.88 % (2367633)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.14/4.88 % (2367633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.14/4.88 % (2367633)CaDiCaL version: 2.1.3
% 31.14/4.88 % (2367633)Termination reason: Instruction limit
% 31.14/4.88 % (2367633)Termination phase: Saturation
% 31.14/4.88 % (2367633)Time elapsed: 0.612 s
% 31.14/4.88 % (2367633)Peak memory usage: 22 MB
% 31.14/4.88 % (2367633)Instructions burned: 1180 (million)
% 31.14/4.88 % (2367661)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1711700795:i=54282_2992 on theBenchmark for (2992ds/54282Mi)
% 31.14/4.88 % (2367661)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 31.14/4.88 % (2367661)Terminated due to inappropriate strategy.
% 31.14/4.88 % (2367661)------------------------------
% 31.14/4.88 % (2367661)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 31.14/4.88 % (2367661)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 31.14/4.88 % (2367661)CaDiCaL version: 2.1.3
% 31.14/4.88 % (2367661)Termination reason: Inappropriate
% 31.14/4.88 % (2367661)Time elapsed: 0.043 s
% 31.14/4.88 % (2367661)Peak memory usage: 13 MB
% 31.14/4.88 % (2367661)Instructions burned: 84 (million)
% 91.90/13.48 % (2367661)------------------------------
% 91.90/13.48 % (2367661)------------------------------
% 91.90/13.48 % (2367663)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=250007044:i=3512:aac=none_2991 on theBenchmark for (2991ds/3512Mi)
% 91.90/13.48 % (2367657)Instruction limit reached!
% 91.90/13.48 % (2367657)------------------------------
% 91.90/13.48 % (2367657)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 91.90/13.48 % (2367657)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.90/13.48 % (2367657)CaDiCaL version: 2.1.3
% 91.90/13.48 % (2367657)Termination reason: Instruction limit
% 91.90/13.48 % (2367657)Termination phase: Saturation
% 91.90/13.48 % (2367657)Time elapsed: 0.475 s
% 91.90/13.48 % (2367657)Peak memory usage: 20 MB
% 91.90/13.48 % (2367657)Instructions burned: 870 (million)
% 91.90/13.48 % (2367665)dis+21_1_sil=32000:sas=cadical:random_seed=2110782502:i=3773:amm=off_2988 on theBenchmark for (2988ds/3773Mi)
% 91.90/13.48 % (2367650)Instruction limit reached!
% 91.90/13.48 % (2367650)------------------------------
% 91.90/13.48 % (2367650)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 91.90/13.48 % (2367650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.90/13.48 % (2367650)CaDiCaL version: 2.1.3
% 91.90/13.48 % (2367650)Termination reason: Instruction limit
% 91.90/13.48 % (2367650)Termination phase: Saturation
% 91.90/13.48 % (2367650)Time elapsed: 0.692 s
% 91.90/13.48 % (2367650)Peak memory usage: 25 MB
% 91.90/13.48 % (2367650)Instructions burned: 1473 (million)
% 91.90/13.48 % (2367667)ott+11_1_sil=16000:gs=on:random_seed=44666547:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2988 on theBenchmark for (2988ds/2251Mi)
% 91.90/13.48 % (2367667)Instruction limit reached!
% 91.90/13.48 % (2367667)------------------------------
% 91.90/13.48 % (2367667)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 91.90/13.48 % (2367667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.90/13.48 % (2367667)CaDiCaL version: 2.1.3
% 91.90/13.48 % (2367667)Termination reason: Instruction limit
% 91.90/13.48 % (2367667)Termination phase: Saturation
% 91.90/13.48 % (2367667)Time elapsed: 1.110 s
% 91.90/13.48 % (2367667)Peak memory usage: 27 MB
% 91.90/13.48 % (2367667)Instructions burned: 2252 (million)
% 91.90/13.48 % (2367671)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2353253391:fmbsr=1.6:i=67534_2976 on theBenchmark for (2976ds/67534Mi)
% 91.90/13.48 % (2367671)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 91.90/13.48 % (2367671)Terminated due to inappropriate strategy.
% 91.90/13.48 % (2367671)------------------------------
% 91.90/13.48 % (2367671)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 91.90/13.48 % (2367671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.90/13.48 % (2367671)CaDiCaL version: 2.1.3
% 91.90/13.48 % (2367671)Termination reason: Inappropriate
% 91.90/13.48 % (2367671)Time elapsed: 0.036 s
% 91.90/13.48 % (2367671)Peak memory usage: 12 MB
% 91.90/13.48 % (2367671)Instructions burned: 75 (million)
% 91.90/13.48 % (2367671)------------------------------
% 91.90/13.48 % (2367671)------------------------------
% 91.90/13.48 % (2367673)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1615774894:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2976 on theBenchmark for (2976ds/4591Mi)
% 91.90/13.48 % (2367663)Instruction limit reached!
% 91.90/13.48 % (2367663)------------------------------
% 91.90/13.48 % (2367663)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 91.90/13.48 % (2367663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.90/13.48 % (2367663)CaDiCaL version: 2.1.3
% 91.90/13.48 % (2367663)Termination reason: Instruction limit
% 91.90/13.48 % (2367663)Termination phase: Saturation
% 91.90/13.48 % (2367663)Time elapsed: 1.700 s
% 91.90/13.48 % (2367663)Peak memory usage: 37 MB
% 91.90/13.48 % (2367663)Instructions burned: 3513 (million)
% 91.90/13.48 % (2367675)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1324399721:i=29340_2974 on theBenchmark for (2974ds/29340Mi)
% 91.90/13.48 % (2367665)Instruction limit reached!
% 91.90/13.48 % (2367665)------------------------------
% 91.90/13.48 % (2367665)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 91.90/13.48 % (2367665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.90/13.48 % (2367665)CaDiCaL version: 2.1.3
% 91.90/13.48 % (2367665)Termination reason: Instruction limit
% 91.90/13.48 % (2367665)Termination phase: Saturation
% 91.90/13.48 % (2367665)Time elapsed: 1.886 s
% 91.90/13.48 % (2367665)Peak memory usage: 32 MB
% 91.90/13.48 % (2367665)Instructions burned: 3773 (million)
% 91.90/13.48 % (2367677)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3359204:i=5211_2969 on theBenchmark for (2969ds/5211Mi)
% 91.90/13.48 % (2367648)Instruction limit reached!
% 91.90/13.48 % (2367648)------------------------------
% 91.90/13.48 % (2367648)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 91.90/13.48 % (2367648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.90/13.48 % (2367648)CaDiCaL version: 2.1.3
% 91.90/13.48 % (2367648)Termination reason: Instruction limit
% 91.90/13.48 % (2367648)Termination phase: Saturation
% 91.90/13.48 % (2367648)Time elapsed: 2.619 s
% 91.90/13.48 % (2367648)Peak memory usage: 36 MB
% 91.90/13.48 % (2367648)Instructions burned: 5132 (million)
% 91.90/13.48 % (2367679)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2683851823:i=5497:nm=2_2969 on theBenchmark for (2969ds/5497Mi)
% 91.90/13.48 % (2367679)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 91.90/13.48 % (2367679)Terminated due to inappropriate strategy.
% 91.90/13.48 % (2367679)------------------------------
% 91.90/13.48 % (2367679)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 91.90/13.48 % (2367679)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.90/13.48 % (2367679)CaDiCaL version: 2.1.3
% 91.90/13.48 % (2367679)Termination reason: Inappropriate
% 91.90/13.48 % (2367679)Time elapsed: 0.023 s
% 91.90/13.48 % (2367679)Peak memory usage: 13 MB
% 91.90/13.48 % (2367679)Instructions burned: 82 (million)
% 91.90/13.48 % (2367679)------------------------------
% 91.90/13.48 % (2367679)------------------------------
% 91.90/13.48 % (2367681)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1605873553:fmbsr=2:i=46332_2968 on theBenchmark for (2968ds/46332Mi)
% 91.90/13.48 % (2367681)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 91.90/13.48 % (2367681)Terminated due to inappropriate strategy.
% 91.90/13.48 % (2367681)------------------------------
% 91.90/13.48 % (2367681)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 91.90/13.48 % (2367681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.90/13.48 % (2367681)CaDiCaL version: 2.1.3
% 91.90/13.48 % (2367681)Termination reason: Inappropriate
% 91.90/13.48 % (2367681)Time elapsed: 0.021 s
% 91.90/13.48 % (2367681)Peak memory usage: 12 MB
% 91.90/13.48 % (2367681)Instructions burned: 75 (million)
% 91.90/13.48 % (2367681)------------------------------
% 91.90/13.48 % (2367681)------------------------------
% 91.90/13.48 % (2367683)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=879487362:i=14071_2968 on theBenchmark for (2968ds/14071Mi)
% 91.90/13.48 % (2367683)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 91.90/13.48 % (2367683)Terminated due to inappropriate strategy.
% 91.90/13.48 % (2367683)------------------------------
% 91.90/13.48 % (2367683)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 91.90/13.48 % (2367683)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.90/13.48 % (2367683)CaDiCaL version: 2.1.3
% 91.90/13.48 % (2367683)Termination reason: Inappropriate
% 91.90/13.48 % (2367683)Time elapsed: 0.021 s
% 91.90/13.48 % (2367683)Peak memory usage: 12 MB
% 91.90/13.48 % (2367683)Instructions burned: 75 (million)
% 91.90/13.48 % (2367683)------------------------------
% 91.90/13.48 % (2367683)------------------------------
% 91.90/13.48 % (2367685)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3379746056:i=22565:add=on:rawr=on_2968 on theBenchmark for (2968ds/22565Mi)
% 91.90/13.48 % (2367658)Instruction limit reached!
% 91.90/13.48 % (2367658)------------------------------
% 91.90/13.48 % (2367658)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 91.90/13.48 % (2367658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.90/13.48 % (2367658)CaDiCaL version: 2.1.3
% 91.90/13.48 % (2367658)Termination reason: Instruction limit
% 91.90/13.48 % (2367658)Termination phase: Saturation
% 91.90/13.48 % (2367658)Time elapsed: 2.753 s
% 91.90/13.48 % (2367658)Peak memory usage: 41 MB
% 91.90/13.48 % (2367658)Instructions burned: 5115 (million)
% 91.90/13.48 % (2367687)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=87666868:i=8173:av=off_2965 on theBenchmark for (2965ds/8173Mi)
% 91.90/13.48 % (2367673)Instruction limit reached!
% 91.90/13.48 % (2367673)------------------------------
% 91.90/13.48 % (2367673)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 91.90/13.48 % (2367673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.90/13.48 % (2367673)CaDiCaL version: 2.1.3
% 91.90/13.48 % (2367673)Termination reason: Instruction limit
% 91.90/13.48 % (2367673)Termination phase: Saturation
% 91.90/13.48 % (2367673)Time elapsed: 2.118 s
% 91.90/13.48 % (2367673)Peak memory usage: 38 MB
% 91.90/13.48 % (2367673)Instructions burned: 4594 (million)
% 91.90/13.48 % (2367689)dis+10_16:1_sil=16000:random_seed=3412393361:i=9155:fsr=off_2954 on theBenchmark for (2954ds/9155Mi)
% 91.90/13.48 % (2367677)Instruction limit reached!
% 91.90/13.48 % (2367677)------------------------------
% 91.90/13.48 % (2367677)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 91.90/13.48 % (2367677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.90/13.48 % (2367677)CaDiCaL version: 2.1.3
% 91.90/13.48 % (2367677)Termination reason: Instruction limit
% 91.90/13.48 % (2367677)Termination phase: Saturation
% 91.90/13.48 % (2367677)Time elapsed: 2.492 s
% 91.90/13.48 % (2367677)Peak memory usage: 51 MB
% 91.90/13.48 % (2367677)Instructions burned: 5211 (million)
% 91.90/13.48 % (2367692)ott-3_8_sil=64000:random_seed=2710560349:i=20139:bs=on_2944 on theBenchmark for (2944ds/20139Mi)
% 91.90/13.48 % (2367687)Instruction limit reached!
% 91.90/13.48 % (2367687)------------------------------
% 91.90/13.48 % (2367687)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 91.90/13.48 % (2367687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.90/13.48 % (2367687)CaDiCaL version: 2.1.3
% 91.90/13.48 % (2367687)Termination reason: Instruction limit
% 91.90/13.48 % (2367687)Termination phase: Saturation
% 91.90/13.48 % (2367687)Time elapsed: 4.402 s
% 91.90/13.48 % (2367687)Peak memory usage: 82 MB
% 91.90/13.48 % (2367687)Instructions burned: 8174 (million)
% 91.90/13.48 % (2367695)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1238258312:fmbsr=2:i=32576_2921 on theBenchmark for (2921ds/32576Mi)
% 91.90/13.48 % (2367695)WARNING: trying to run FMB on interpreted or otherwise provably infinite-domain problem!
% 91.90/13.48 % (2367695)Terminated due to inappropriate strategy.
% 91.90/13.48 % (2367695)------------------------------
% 91.90/13.48 % (2367695)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 91.90/13.48 % (2367695)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.90/13.48 % (2367695)CaDiCaL version: 2.1.3
% 91.90/13.48 % (2367695)Termination reason: Inappropriate
% 91.90/13.48 % (2367695)Time elapsed: 0.023 s
% 91.90/13.48 % (2367695)Peak memory usage: 13 MB
% 91.90/13.48 % (2367695)Instructions burned: 84 (million)
% 91.90/13.48 % (2367695)------------------------------
% 91.90/13.48 % (2367695)------------------------------
% 91.90/13.48 % (2367697)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2829850683:i=11404_2921 on theBenchmark for (2921ds/11404Mi)
% 91.90/13.48 % (2367689)Instruction limit reached!
% 91.90/13.48 % (2367689)------------------------------
% 91.90/13.48 % (2367689)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 91.90/13.48 % (2367689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.90/13.48 % (2367689)CaDiCaL version: 2.1.3
% 91.90/13.48 % (2367689)Termination reason: Instruction limit
% 91.90/13.48 % (2367689)Termination phase: Saturation
% 91.90/13.48 % (2367689)Time elapsed: 4.268 s
% 91.90/13.48 % (2367689)Peak memory usage: 57 MB
% 91.90/13.48 % (2367689)Instructions burned: 9157 (million)
% 91.90/13.48 % (2367701)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=938063044:i=14134_2912 on theBenchmark for (2912ds/14134Mi)
% 91.90/13.48 % (2367701) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2367602-2367701"...
% 91.90/13.48 % (2367701)...printing done.
% 91.90/13.48 % (2367701)Refutation found. Thanks to Tanya!
% 91.90/13.48 % SZS status Theorem for theBenchmark
% 91.90/13.48 % SZS output start Proof for theBenchmark
% 91.90/13.48 tff(type_def_5, type, 'Real_real_bool_fun_fun$': $tType).
% 91.90/13.48 tff(type_def_6, type, 'Int_bool_fun$': $tType).
% 91.90/13.48 tff(type_def_7, type, 'Real_num_fun$': $tType).
% 91.90/13.48 tff(type_def_8, type, 'Nat_nat_bool_fun_fun$': $tType).
% 91.90/13.48 tff(type_def_9, type, 'A_ltln_list$': $tType).
% 91.90/13.48 tff(type_def_10, type, 'Num_num_fun$': $tType).
% 91.90/13.48 tff(type_def_11, type, 'Nat_enat_fun$': $tType).
% 91.90/13.48 tff(type_def_12, type, 'Int_real_fun$': $tType).
% 91.90/13.48 tff(type_def_13, type, 'Num_enat_fun$': $tType).
% 91.90/13.48 tff(type_def_14, type, 'Enat$': $tType).
% 91.90/13.48 tff(type_def_15, type, 'Int_int_fun$': $tType).
% 91.90/13.48 tff(type_def_16, type, 'Enat_int_fun$': $tType).
% 91.90/13.48 tff(type_def_17, type, 'Num_bool_fun$': $tType).
% 91.90/13.48 tff(type_def_18, type, 'Nat_nat_fun$': $tType).
% 91.90/13.48 tff(type_def_19, type, 'Num_real_fun$': $tType).
% 91.90/13.48 tff(type_def_20, type, 'Nat$': $tType).
% 91.90/13.48 tff(type_def_21, type, 'Num$': $tType).
% 91.90/13.48 tff(type_def_22, type, tlbool: $tType).
% 91.90/13.48 tff(type_def_23, type, 'Enat_bool_fun$': $tType).
% 91.90/13.48 tff(type_def_24, type, 'Int_enat_fun$': $tType).
% 91.90/13.48 tff(type_def_25, type, 'Nat_num_fun$': $tType).
% 91.90/13.48 tff(type_def_26, type, 'Enat_num_fun$': $tType).
% 91.90/13.48 tff(type_def_27, type, 'Nat_real_fun$': $tType).
% 91.90/13.48 tff(type_def_28, type, 'Real_int_fun$': $tType).
% 91.90/13.48 tff(type_def_29, type, 'Enat_enat_bool_fun_fun$': $tType).
% 91.90/13.48 tff(type_def_30, type, 'Int_int_bool_fun_fun$': $tType).
% 91.90/13.48 tff(type_def_31, type, 'Nat_bool_fun$': $tType).
% 91.90/13.48 tff(type_def_32, type, 'Real_bool_fun$': $tType).
% 91.90/13.48 tff(type_def_33, type, 'Real_set$': $tType).
% 91.90/13.48 tff(type_def_34, type, 'Nat_int_fun$': $tType).
% 91.90/13.48 tff(type_def_35, type, 'Int_num_fun$': $tType).
% 91.90/13.48 tff(type_def_36, type, 'Num_int_fun$': $tType).
% 91.90/13.48 tff(type_def_37, type, 'Num_num_bool_fun_fun$': $tType).
% 91.90/13.48 tff(func_def_0, type, 'less_eq$': 'Num_num_bool_fun_fun$').
% 91.90/13.48 tff(func_def_1, type, 'less_eq$a': 'Enat_enat_bool_fun_fun$').
% 91.90/13.48 tff(func_def_2, type, 'fun_app$p': ('Int_int_fun$' * $int) > $int).
% 91.90/13.48 tff(func_def_3, type, 'dbl$': 'Int_int_fun$').
% 91.90/13.48 tff(func_def_4, type, 'zero$': 'Nat$').
% 91.90/13.48 tff(func_def_5, type, 'zero$a': 'Enat$').
% 91.90/13.48 tff(func_def_6, type, 'numeral$b': 'Num_real_fun$').
% 91.90/13.48 tff(func_def_7, type, 'power$c': $real > 'Nat_real_fun$').
% 91.90/13.48 tff(func_def_8, type, 'n$': 'Nat$').
% 91.90/13.48 tff(func_def_9, type, 'size$a': 'Num$' > 'Nat$').
% 91.90/13.48 tff(func_def_10, type, 'of_nat$a': 'Nat_nat_fun$').
% 91.90/13.48 tff(func_def_11, type, 'fun_app$z': ('Int_real_fun$' * $int) > $real).
% 91.90/13.48 tff(func_def_12, type, 'times$b': $int > 'Int_int_fun$').
% 91.90/13.48 tff(func_def_13, type, 'fun_app$v': ('Int_num_fun$' * $int) > 'Num$').
% 91.90/13.48 tff(func_def_14, type, 'fun_app$f': ('Num_num_bool_fun_fun$' * 'Num$') > 'Num_bool_fun$').
% 91.90/13.48 tff(func_def_15, type, 'ys$': 'A_ltln_list$').
% 91.90/13.48 tff(func_def_16, type, 'of_nat$': 'Nat_int_fun$').
% 91.90/13.48 tff(func_def_17, type, 'times$': 'Nat$' > 'Nat_nat_fun$').
% 91.90/13.48 tff(func_def_18, type, 'less$': 'Num_num_bool_fun_fun$').
% 91.90/13.48 tff(func_def_19, type, 'dbl$a': $real > $real).
% 91.90/13.48 tff(func_def_20, type, 'less_eq$b': 'Nat_nat_bool_fun_fun$').
% 91.90/13.48 tff(func_def_21, type, tltrue: tlbool).
% 91.90/13.48 tff(func_def_22, type, 'fun_app$w': ('Enat_num_fun$' * 'Enat$') > 'Num$').
% 91.90/13.48 tff(func_def_23, type, 'uu$': 'Real_set$' > 'Real_bool_fun$').
% 91.90/13.48 tff(func_def_24, type, 'fun_app$j': ('Num_real_fun$' * 'Num$') > $real).
% 91.90/13.48 tff(func_def_25, type, 'fun_app$r': ('Int_int_bool_fun_fun$' * $int) > 'Int_bool_fun$').
% 91.90/13.48 tff(func_def_26, type, 'fun_app$a': ('Nat_int_fun$' * 'Nat$') > $int).
% 91.90/13.48 tff(func_def_27, type, 'pow$': 'Num$' > 'Num_num_fun$').
% 91.90/13.48 tff(func_def_28, type, 'numeral$c': 'Num$' > 'Nat$').
% 91.90/13.48 tff(func_def_29, type, 'fun_app$m': ('Nat_real_fun$' * 'Nat$') > $real).
% 91.90/13.48 tff(func_def_30, type, 'less$a': 'Enat_enat_bool_fun_fun$').
% 91.90/13.48 tff(func_def_31, type, 'power$a': $int > 'Nat_int_fun$').
% 91.90/13.48 tff(func_def_32, type, 'fun_app$x': ('Real_num_fun$' * $real) > 'Num$').
% 91.90/13.48 tff(func_def_33, type, 'numeral$': 'Num_int_fun$').
% 91.90/13.48 tff(func_def_34, type, 'power$b': 'Enat$' > 'Nat_enat_fun$').
% 91.90/13.48 tff(func_def_35, type, 'numeral$a': 'Num_enat_fun$').
% 91.90/13.48 tff(func_def_36, type, 'fun_app$s': ('Real_real_bool_fun_fun$' * $real) > 'Real_bool_fun$').
% 91.90/13.48 tff(func_def_37, type, 'fun_app$i': ('Num_enat_fun$' * 'Num$') > 'Enat$').
% 91.90/13.48 tff(func_def_38, type, 'times$c': ('Enat$' * 'Enat$') > 'Enat$').
% 91.90/13.48 tff(func_def_39, type, 'fun_app$t': ('Enat_int_fun$' * 'Enat$') > $int).
% 91.90/13.48 tff(func_def_40, type, 'one$': 'Num$').
% 91.90/13.48 tff(func_def_41, type, 'fun_app$d': ('Num_int_fun$' * 'Num$') > $int).
% 91.90/13.48 tff(func_def_42, type, 'less$b': 'Nat_nat_bool_fun_fun$').
% 91.90/13.48 tff(func_def_43, type, tlfalse: tlbool).
% 91.90/13.48 tff(func_def_44, type, 'nat$': $int > 'Nat$').
% 91.90/13.48 tff(func_def_45, type, 'fun_app$u': ('Real_int_fun$' * $real) > $int).
% 91.90/13.48 tff(func_def_46, type, 'fun_app$o': ('Nat_nat_bool_fun_fun$' * 'Nat$') > 'Nat_bool_fun$').
% 91.90/13.48 tff(func_def_47, type, 'fun_app$c': ('Num_num_fun$' * 'Num$') > 'Num$').
% 91.90/13.48 tff(func_def_48, type, 'fun_app$l': ('Nat_enat_fun$' * 'Nat$') > 'Enat$').
% 91.90/13.48 tff(func_def_49, type, 'size$': 'A_ltln_list$' > 'Nat$').
% 91.90/13.48 tff(func_def_50, type, 'of_nat$c': 'Nat_enat_fun$').
% 91.90/13.48 tff(func_def_51, type, 'fun_app$k': ('Nat_num_fun$' * 'Nat$') > 'Num$').
% 91.90/13.48 tff(func_def_52, type, 'fun_app$h': ('Enat_enat_bool_fun_fun$' * 'Enat$') > 'Enat_bool_fun$').
% 91.90/13.48 tff(func_def_53, type, 'times$a': 'Num$' > 'Num_num_fun$').
% 91.90/13.48 tff(func_def_54, type, 'of_nat$b': 'Nat_real_fun$').
% 91.90/13.48 tff(func_def_55, type, 'fun_app$y': ('Int_enat_fun$' * $int) > 'Enat$').
% 91.90/13.48 tff(func_def_56, type, 'times$d': ($real * $real) > $real).
% 91.90/13.48 tff(func_def_57, type, 'collect$': 'Real_bool_fun$' > 'Real_set$').
% 91.90/13.48 tff(func_def_58, type, 'power$': 'Nat$' > 'Nat_nat_fun$').
% 91.90/13.48 tff(func_def_59, type, 'bit0$': 'Num_num_fun$').
% 91.90/13.48 tff(func_def_60, type, 'fun_app$b': ('Nat_nat_fun$' * 'Nat$') > 'Nat$').
% 91.90/13.48 tff(func_def_74, type, sK12: 'Nat_int_fun$' > 'Nat$').
% 91.90/13.48 tff(func_def_75, type, sK13: 'Nat_num_fun$' > 'Nat$').
% 91.90/13.48 tff(func_def_76, type, sK14: 'Nat_enat_fun$' > 'Nat$').
% 91.90/13.48 tff(func_def_77, type, sK15: 'Nat_real_fun$' > 'Nat$').
% 91.90/13.48 tff(func_def_78, type, sK16: 'Nat_int_fun$' > 'Nat$').
% 91.90/13.48 tff(func_def_79, type, sK17: 'Nat_num_fun$' > 'Nat$').
% 91.90/13.48 tff(func_def_80, type, sK18: 'Nat_enat_fun$' > 'Nat$').
% 91.90/13.48 tff(func_def_81, type, sK19: 'Nat_real_fun$' > 'Nat$').
% 91.90/13.48 tff(func_def_82, type, sK20: 'Nat_bool_fun$' > 'Nat$').
% 91.90/13.48 tff(func_def_83, type, sK21: ('Nat_bool_fun$' * 'Nat$') > 'Nat$').
% 91.90/13.48 tff(func_def_84, type, sK22: 'Nat_nat_bool_fun_fun$' > 'Nat$').
% 91.90/13.48 tff(func_def_85, type, sK23: 'Nat_nat_bool_fun_fun$' > 'Nat$').
% 91.90/13.48 tff(func_def_86, type, sK24: 'Nat_nat_bool_fun_fun$' > 'Nat$').
% 91.90/13.48 tff(func_def_87, type, sK25: 'Nat_nat_bool_fun_fun$' > 'Nat$').
% 91.90/13.48 tff(func_def_88, type, sK26: 'Nat_nat_bool_fun_fun$' > 'Nat$').
% 91.90/13.48 tff(func_def_89, type, sK27: ('Nat$' * 'Nat_bool_fun$') > 'Nat$').
% 91.90/13.48 tff(func_def_90, type, sK28: 'Nat_bool_fun$' > 'Nat$').
% 91.90/13.48 tff(func_def_91, type, sK29: 'Nat$' > 'Nat$').
% 91.90/13.48 tff(func_def_92, type, sK30: 'Nat$' > 'Nat$').
% 91.90/13.48 tff(func_def_93, type, sK31: 'Nat_bool_fun$' > 'Nat$').
% 91.90/13.48 tff(func_def_94, type, sK32: 'Nat_nat_bool_fun_fun$' > 'Nat$').
% 91.90/13.48 tff(func_def_95, type, sK33: 'Nat_nat_bool_fun_fun$' > 'Nat$').
% 91.90/13.48 tff(func_def_96, type, sK34: 'Nat_nat_bool_fun_fun$' > 'Nat$').
% 91.90/13.48 tff(func_def_97, type, sK35: 'Nat_nat_bool_fun_fun$' > 'Nat$').
% 91.90/13.48 tff(func_def_98, type, sK36: 'Nat_bool_fun$' > 'Nat$').
% 91.90/13.48 tff(func_def_99, type, sK37: 'Nat$' > 'Nat$').
% 91.90/13.48 tff(func_def_100, type, sK38: 'Int_int_bool_fun_fun$' > $int).
% 91.90/13.48 tff(func_def_101, type, sK39: 'Int_int_bool_fun_fun$' > $int).
% 91.90/13.48 tff(func_def_102, type, sK40: 'Int_int_bool_fun_fun$' > $int).
% 91.90/13.48 tff(func_def_103, type, sK41: 'Int_int_bool_fun_fun$' > $int).
% 91.90/13.48 tff(func_def_104, type, sK42: 'Num_num_bool_fun_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_105, type, sK43: 'Num_num_bool_fun_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_106, type, sK44: 'Num_num_bool_fun_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_107, type, sK45: 'Num_num_bool_fun_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_108, type, sK46: 'Enat_enat_bool_fun_fun$' > 'Enat$').
% 91.90/13.48 tff(func_def_109, type, sK47: 'Enat_enat_bool_fun_fun$' > 'Enat$').
% 91.90/13.48 tff(func_def_110, type, sK48: 'Enat_enat_bool_fun_fun$' > 'Enat$').
% 91.90/13.48 tff(func_def_111, type, sK49: 'Enat_enat_bool_fun_fun$' > 'Enat$').
% 91.90/13.48 tff(func_def_112, type, sK50: 'Real_real_bool_fun_fun$' > $real).
% 91.90/13.48 tff(func_def_113, type, sK51: 'Real_real_bool_fun_fun$' > $real).
% 91.90/13.48 tff(func_def_114, type, sK52: 'Real_real_bool_fun_fun$' > $real).
% 91.90/13.48 tff(func_def_115, type, sK53: 'Real_real_bool_fun_fun$' > $real).
% 91.90/13.48 tff(func_def_116, type, sK54: 'Int_int_fun$' > $int).
% 91.90/13.48 tff(func_def_117, type, sK55: 'Int_int_fun$' > $int).
% 91.90/13.48 tff(func_def_118, type, sK56: 'Num_int_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_119, type, sK57: 'Num_int_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_120, type, sK58: 'Enat_int_fun$' > 'Enat$').
% 91.90/13.48 tff(func_def_121, type, sK59: 'Enat_int_fun$' > 'Enat$').
% 91.90/13.48 tff(func_def_122, type, sK60: 'Real_int_fun$' > $real).
% 91.90/13.48 tff(func_def_123, type, sK61: 'Real_int_fun$' > $real).
% 91.90/13.48 tff(func_def_124, type, sK62: 'Int_num_fun$' > $int).
% 91.90/13.48 tff(func_def_125, type, sK63: 'Int_num_fun$' > $int).
% 91.90/13.48 tff(func_def_126, type, sK64: 'Num_num_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_127, type, sK65: 'Num_num_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_128, type, sK66: 'Enat_num_fun$' > 'Enat$').
% 91.90/13.48 tff(func_def_129, type, sK67: 'Enat_num_fun$' > 'Enat$').
% 91.90/13.48 tff(func_def_130, type, sK68: 'Real_num_fun$' > $real).
% 91.90/13.48 tff(func_def_131, type, sK69: 'Real_num_fun$' > $real).
% 91.90/13.48 tff(func_def_132, type, sK70: 'Int_enat_fun$' > $int).
% 91.90/13.48 tff(func_def_133, type, sK71: 'Int_enat_fun$' > $int).
% 91.90/13.48 tff(func_def_134, type, sK72: 'Num_enat_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_135, type, sK73: 'Num_enat_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_136, type, sK74: 'Int_int_fun$' > $int).
% 91.90/13.48 tff(func_def_137, type, sK75: 'Int_int_fun$' > $int).
% 91.90/13.48 tff(func_def_138, type, sK76: 'Int_num_fun$' > $int).
% 91.90/13.48 tff(func_def_139, type, sK77: 'Int_num_fun$' > $int).
% 91.90/13.48 tff(func_def_140, type, sK78: 'Int_enat_fun$' > $int).
% 91.90/13.48 tff(func_def_141, type, sK79: 'Int_enat_fun$' > $int).
% 91.90/13.48 tff(func_def_142, type, sK80: 'Int_real_fun$' > $int).
% 91.90/13.48 tff(func_def_143, type, sK81: 'Int_real_fun$' > $int).
% 91.90/13.48 tff(func_def_144, type, sK82: 'Num_int_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_145, type, sK83: 'Num_int_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_146, type, sK84: 'Num_num_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_147, type, sK85: 'Num_num_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_148, type, sK86: 'Num_enat_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_149, type, sK87: 'Num_enat_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_150, type, sK88: 'Num_real_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_151, type, sK89: 'Num_real_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_152, type, sK90: 'Enat_int_fun$' > 'Enat$').
% 91.90/13.48 tff(func_def_153, type, sK91: 'Enat_int_fun$' > 'Enat$').
% 91.90/13.48 tff(func_def_154, type, sK92: 'Enat_num_fun$' > 'Enat$').
% 91.90/13.48 tff(func_def_155, type, sK93: 'Enat_num_fun$' > 'Enat$').
% 91.90/13.48 tff(func_def_156, type, sK94: 'Int_int_fun$' > $int).
% 91.90/13.48 tff(func_def_157, type, sK95: 'Int_int_fun$' > $int).
% 91.90/13.48 tff(func_def_158, type, sK96: 'Int_num_fun$' > $int).
% 91.90/13.48 tff(func_def_159, type, sK97: 'Int_num_fun$' > $int).
% 91.90/13.48 tff(func_def_160, type, sK98: 'Int_enat_fun$' > $int).
% 91.90/13.48 tff(func_def_161, type, sK99: 'Int_enat_fun$' > $int).
% 91.90/13.48 tff(func_def_162, type, sK100: 'Int_real_fun$' > $int).
% 91.90/13.48 tff(func_def_163, type, sK101: 'Int_real_fun$' > $int).
% 91.90/13.48 tff(func_def_164, type, sK102: 'Num_int_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_165, type, sK103: 'Num_int_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_166, type, sK104: 'Num_num_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_167, type, sK105: 'Num_num_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_168, type, sK106: 'Num_enat_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_169, type, sK107: 'Num_enat_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_170, type, sK108: 'Num_real_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_171, type, sK109: 'Num_real_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_172, type, sK110: 'Enat_int_fun$' > 'Enat$').
% 91.90/13.48 tff(func_def_173, type, sK111: 'Enat_int_fun$' > 'Enat$').
% 91.90/13.48 tff(func_def_174, type, sK112: 'Enat_num_fun$' > 'Enat$').
% 91.90/13.48 tff(func_def_175, type, sK113: 'Enat_num_fun$' > 'Enat$').
% 91.90/13.48 tff(func_def_176, type, sK114: 'Int_int_fun$' > $int).
% 91.90/13.48 tff(func_def_177, type, sK115: 'Int_int_fun$' > $int).
% 91.90/13.48 tff(func_def_178, type, sK116: 'Int_num_fun$' > $int).
% 91.90/13.48 tff(func_def_179, type, sK117: 'Int_num_fun$' > $int).
% 91.90/13.48 tff(func_def_180, type, sK118: 'Int_enat_fun$' > $int).
% 91.90/13.48 tff(func_def_181, type, sK119: 'Int_enat_fun$' > $int).
% 91.90/13.48 tff(func_def_182, type, sK120: 'Int_real_fun$' > $int).
% 91.90/13.48 tff(func_def_183, type, sK121: 'Int_real_fun$' > $int).
% 91.90/13.48 tff(func_def_184, type, sK122: 'Num_int_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_185, type, sK123: 'Num_int_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_186, type, sK124: 'Num_num_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_187, type, sK125: 'Num_num_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_188, type, sK126: 'Num_enat_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_189, type, sK127: 'Num_enat_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_190, type, sK128: 'Num_real_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_191, type, sK129: 'Num_real_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_192, type, sK130: 'Enat_int_fun$' > 'Enat$').
% 91.90/13.48 tff(func_def_193, type, sK131: 'Enat_int_fun$' > 'Enat$').
% 91.90/13.48 tff(func_def_194, type, sK132: 'Enat_num_fun$' > 'Enat$').
% 91.90/13.48 tff(func_def_195, type, sK133: 'Enat_num_fun$' > 'Enat$').
% 91.90/13.48 tff(func_def_196, type, sK134: $real > 'Nat$').
% 91.90/13.48 tff(func_def_197, type, sK135: 'Real_set$' > $real).
% 91.90/13.48 tff(func_def_198, type, sK136: ('Real_set$' * $real) > $real).
% 91.90/13.48 tff(func_def_199, type, sK137: ('Real_set$' * $real) > $real).
% 91.90/13.48 tff(func_def_200, type, sK138: $int > 'Nat$').
% 91.90/13.48 tff(func_def_201, type, sK139: 'Nat_bool_fun$' > 'Nat$').
% 91.90/13.48 tff(func_def_202, type, sK140: $int > 'Nat$').
% 91.90/13.48 tff(func_def_203, type, sK141: 'Num_num_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_204, type, sK142: 'Num_num_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_205, type, sK143: 'Num_int_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_206, type, sK144: 'Num_int_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_207, type, sK145: 'Num_enat_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_208, type, sK146: 'Num_enat_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_209, type, sK147: 'Num_real_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_210, type, sK148: 'Num_real_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_211, type, sK149: 'Int_num_fun$' > $int).
% 91.90/13.48 tff(func_def_212, type, sK150: 'Int_num_fun$' > $int).
% 91.90/13.48 tff(func_def_213, type, sK151: 'Int_int_fun$' > $int).
% 91.90/13.48 tff(func_def_214, type, sK152: 'Int_int_fun$' > $int).
% 91.90/13.48 tff(func_def_215, type, sK153: 'Int_enat_fun$' > $int).
% 91.90/13.48 tff(func_def_216, type, sK154: 'Int_enat_fun$' > $int).
% 91.90/13.48 tff(func_def_217, type, sK155: 'Int_real_fun$' > $int).
% 91.90/13.48 tff(func_def_218, type, sK156: 'Int_real_fun$' > $int).
% 91.90/13.48 tff(func_def_219, type, sK157: 'Enat_num_fun$' > 'Enat$').
% 91.90/13.48 tff(func_def_220, type, sK158: 'Enat_num_fun$' > 'Enat$').
% 91.90/13.48 tff(func_def_221, type, sK159: 'Enat_int_fun$' > 'Enat$').
% 91.90/13.48 tff(func_def_222, type, sK160: 'Enat_int_fun$' > 'Enat$').
% 91.90/13.48 tff(func_def_223, type, sK161: 'Num_num_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_224, type, sK162: 'Num_num_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_225, type, sK163: 'Int_num_fun$' > $int).
% 91.90/13.48 tff(func_def_226, type, sK164: 'Int_num_fun$' > $int).
% 91.90/13.48 tff(func_def_227, type, sK165: 'Enat_num_fun$' > 'Enat$').
% 91.90/13.48 tff(func_def_228, type, sK166: 'Enat_num_fun$' > 'Enat$').
% 91.90/13.48 tff(func_def_229, type, sK167: 'Real_num_fun$' > $real).
% 91.90/13.48 tff(func_def_230, type, sK168: 'Real_num_fun$' > $real).
% 91.90/13.48 tff(func_def_231, type, sK169: 'Num_int_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_232, type, sK170: 'Num_int_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_233, type, sK171: 'Int_int_fun$' > $int).
% 91.90/13.48 tff(func_def_234, type, sK172: 'Int_int_fun$' > $int).
% 91.90/13.48 tff(func_def_235, type, sK173: 'Enat_int_fun$' > 'Enat$').
% 91.90/13.48 tff(func_def_236, type, sK174: 'Enat_int_fun$' > 'Enat$').
% 91.90/13.48 tff(func_def_237, type, sK175: 'Real_int_fun$' > $real).
% 91.90/13.48 tff(func_def_238, type, sK176: 'Real_int_fun$' > $real).
% 91.90/13.48 tff(func_def_239, type, sK177: 'Num_enat_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_240, type, sK178: 'Num_enat_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_241, type, sK179: 'Int_enat_fun$' > $int).
% 91.90/13.48 tff(func_def_242, type, sK180: 'Int_enat_fun$' > $int).
% 91.90/13.48 tff(func_def_243, type, sK181: 'Num_num_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_244, type, sK182: 'Num_num_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_245, type, sK183: 'Num_int_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_246, type, sK184: 'Num_int_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_247, type, sK185: 'Num_enat_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_248, type, sK186: 'Num_enat_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_249, type, sK187: 'Num_real_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_250, type, sK188: 'Num_real_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_251, type, sK189: 'Int_num_fun$' > $int).
% 91.90/13.48 tff(func_def_252, type, sK190: 'Int_num_fun$' > $int).
% 91.90/13.48 tff(func_def_253, type, sK191: 'Int_int_fun$' > $int).
% 91.90/13.48 tff(func_def_254, type, sK192: 'Int_int_fun$' > $int).
% 91.90/13.48 tff(func_def_255, type, sK193: 'Int_enat_fun$' > $int).
% 91.90/13.48 tff(func_def_256, type, sK194: 'Int_enat_fun$' > $int).
% 91.90/13.48 tff(func_def_257, type, sK195: 'Int_real_fun$' > $int).
% 91.90/13.48 tff(func_def_258, type, sK196: 'Int_real_fun$' > $int).
% 91.90/13.48 tff(func_def_259, type, sK197: 'Enat_num_fun$' > 'Enat$').
% 91.90/13.48 tff(func_def_260, type, sK198: 'Enat_num_fun$' > 'Enat$').
% 91.90/13.48 tff(func_def_261, type, sK199: 'Enat_int_fun$' > 'Enat$').
% 91.90/13.48 tff(func_def_262, type, sK200: 'Enat_int_fun$' > 'Enat$').
% 91.90/13.48 tff(func_def_263, type, sK201: 'Num_num_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_264, type, sK202: 'Num_num_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_265, type, sK203: 'Num_int_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_266, type, sK204: 'Num_int_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_267, type, sK205: 'Num_enat_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_268, type, sK206: 'Num_enat_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_269, type, sK207: 'Num_real_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_270, type, sK208: 'Num_real_fun$' > 'Num$').
% 91.90/13.48 tff(func_def_271, type, sK209: 'Int_num_fun$' > $int).
% 91.90/13.48 tff(func_def_272, type, sK210: 'Int_num_fun$' > $int).
% 91.90/13.48 tff(func_def_273, type, sK211: 'Int_int_fun$' > $int).
% 91.90/13.48 tff(func_def_274, type, sK212: 'Int_int_fun$' > $int).
% 91.90/13.48 tff(func_def_275, type, sK213: 'Int_enat_fun$' > $int).
% 91.90/13.48 tff(func_def_276, type, sK214: 'Int_enat_fun$' > $int).
% 91.90/13.48 tff(func_def_277, type, sK215: 'Int_real_fun$' > $int).
% 91.90/13.48 tff(func_def_278, type, sK216: 'Int_real_fun$' > $int).
% 91.90/13.48 tff(func_def_279, type, sK217: 'Enat_num_fun$' > 'Enat$').
% 91.90/13.48 tff(func_def_280, type, sK218: 'Enat_num_fun$' > 'Enat$').
% 91.90/13.48 tff(func_def_281, type, sK219: 'Enat_int_fun$' > 'Enat$').
% 91.90/13.48 tff(func_def_282, type, sK220: 'Enat_int_fun$' > 'Enat$').
% 91.90/13.48 tff(func_def_283, type, sK221: $int > 'Nat$').
% 91.90/13.48 tff(func_def_284, type, sK222: $int > 'Nat$').
% 91.90/13.48 tff(func_def_285, type, sK223: ('Nat$' * 'Nat_bool_fun$') > 'Nat$').
% 91.90/13.48 tff(func_def_286, type, sK224: ('Nat$' * 'Nat_bool_fun$') > 'Nat$').
% 91.90/13.48 tff(func_def_287, type, sK225: 'Nat_nat_bool_fun_fun$' > 'Nat$').
% 91.90/13.48 tff(func_def_288, type, sK226: 'Nat_nat_bool_fun_fun$' > 'Nat$').
% 91.90/13.48 tff(func_def_289, type, sK227: 'Nat_nat_bool_fun_fun$' > 'Nat$').
% 91.90/13.48 tff(func_def_290, type, sK228: 'Nat_nat_bool_fun_fun$' > 'Nat$').
% 91.90/13.48 tff(func_def_291, type, sK229: ('Nat$' * 'Nat$') > 'Nat$').
% 91.90/13.48 tff(func_def_292, type, sK230: ('Nat$' * 'Nat_bool_fun$') > 'Nat$').
% 91.90/13.48 tff(func_def_293, type, sK231: ('Nat$' * 'Nat_bool_fun$') > 'Nat$').
% 91.90/13.48 tff(func_def_294, type, sK232: ('Nat$' * 'Nat_bool_fun$') > 'Nat$').
% 91.90/13.48 tff(func_def_295, type, sK233: ('Nat$' * 'Nat_bool_fun$') > 'Nat$').
% 91.90/13.48 tff(func_def_296, type, sK234: ('Nat$' * 'Nat$') > 'Nat$').
% 91.90/13.48 tff(func_def_297, type, sK235: ('Nat$' * 'Nat$') > 'Nat$').
% 91.90/13.48 tff(func_def_298, type, sK236: ('Nat$' * 'Nat_bool_fun$') > 'Nat$').
% 91.90/13.48 tff(func_def_299, type, sK237: ('Nat$' * 'Nat_bool_fun$') > 'Nat$').
% 91.90/13.48 tff(func_def_300, type, sK238: 'Nat$' > 'Nat$').
% 91.90/13.48 tff(func_def_301, type, sK239: ('Nat$' * 'Nat_bool_fun$') > 'Nat$').
% 91.90/13.48 tff(func_def_302, type, sK240: ('Nat$' * 'Nat_bool_fun$') > 'Nat$').
% 91.90/13.48 tff(func_def_303, type, sK241: 'Nat$' > 'Nat$').
% 91.90/13.48 tff(func_def_304, type, sK242: ('Nat$' * 'Nat$') > 'Nat$').
% 91.90/13.48 tff(func_def_305, type, sK243: 'Nat_nat_fun$' > 'Nat$').
% 91.90/13.48 tff(func_def_306, type, sK244: 'Nat_nat_fun$' > 'Nat$').
% 91.90/13.48 tff(func_def_307, type, sK245: ('Nat_bool_fun$' * 'Nat$') > 'Nat$').
% 91.90/13.48 tff(func_def_308, type, sK246: 'Nat_bool_fun$' > 'Nat$').
% 91.90/13.48 tff(func_def_309, type, sK247: 'Nat_bool_fun$' > 'Nat$').
% 91.90/13.48 tff(func_def_310, type, sK248: ('Nat$' * 'Nat$' * 'Nat_bool_fun$') > 'Nat$').
% 91.90/13.48 tff(func_def_311, type, sK249: ('Nat$' * 'Nat$' * 'Nat_bool_fun$') > 'Nat$').
% 91.90/13.48 tff(func_def_312, type, sK250: ('Nat_bool_fun$' * 'Nat$') > 'Nat$').
% 91.90/13.48 tff(func_def_313, type, sK251: 'Nat_bool_fun$' > 'Nat$').
% 91.90/13.48 tff(func_def_314, type, sK252: 'Enat_bool_fun$' > 'Enat$').
% 91.90/13.48 tff(func_def_315, type, sK253: 'Nat_bool_fun$' > 'Nat$').
% 91.90/13.48 tff(func_def_316, type, sK254: 'Nat_bool_fun$' > 'Nat$').
% 91.90/13.48 tff(func_def_317, type, sK255: ($real * $real) > 'Nat$').
% 91.90/13.48 tff(func_def_318, type, sK256: ($real * $real) > 'Nat$').
% 91.90/13.48 tff(func_def_319, type, sK257: ($real * 'Nat$') > $real).
% 91.90/13.48 tff(func_def_320, type, sK258: ('Nat$' * $real) > $real).
% 91.90/13.48 tff(func_def_321, type, sK259: ('Nat$' * $real) > $real).
% 91.90/13.48 tff(pred_def_1, type, 'fun_app$q': ('Int_bool_fun$' * $int) > $o).
% 91.90/13.48 tff(pred_def_2, type, 'fun_app$n': ('Nat_bool_fun$' * 'Nat$') > $o).
% 91.90/13.48 tff(pred_def_3, type, 'fun_app$': ('Real_bool_fun$' * $real) > $o).
% 91.90/13.48 tff(pred_def_4, type, 'fun_app$e': ('Num_bool_fun$' * 'Num$') > $o).
% 91.90/13.48 tff(pred_def_5, type, 'member$': ($real * 'Real_set$') > $o).
% 91.90/13.48 tff(pred_def_6, type, 'fun_app$g': ('Enat_bool_fun$' * 'Enat$') > $o).
% 91.90/13.48 tff(pred_def_11, type, sP0: ($int * $int * $int) > $o).
% 91.90/13.48 tff(pred_def_12, type, sP1: ($int * $int * $int) > $o).
% 91.90/13.48 tff(pred_def_13, type, sP2: ($int * $int * $int) > $o).
% 91.90/13.48 tff(pred_def_14, type, sP3: ('Num$' * 'Num$' * 'Num$') > $o).
% 91.90/13.48 tff(pred_def_15, type, sP4: ('Num$' * 'Num$' * 'Num$') > $o).
% 91.90/13.48 tff(pred_def_16, type, sP5: ('Num$' * 'Num$' * 'Num$') > $o).
% 91.90/13.48 tff(pred_def_17, type, sP6: ('Enat$' * 'Enat$' * 'Enat$') > $o).
% 91.90/13.48 tff(pred_def_18, type, sP7: ('Enat$' * 'Enat$' * 'Enat$') > $o).
% 91.90/13.48 tff(pred_def_19, type, sP8: ('Enat$' * 'Enat$' * 'Enat$') > $o).
% 91.90/13.48 tff(pred_def_20, type, sP9: ($real * $real * $real) > $o).
% 91.90/13.48 tff(pred_def_21, type, sP10: ($real * $real * $real) > $o).
% 91.90/13.48 tff(pred_def_22, type, sP11: ($real * $real * $real) > $o).
% 91.90/13.48 tff(f2,conjecture,(
% 91.90/13.48 $lesseq('fun_app$a'('of_nat$','fun_app$b'('power$'('fun_app$b'('power$'('nat$'(2)),'fun_app$b'('power$'('nat$'(2)),'nat$'($sum('fun_app$a'('of_nat$','n$'),1))))),'size$'('ys$'))),'fun_app$a'('of_nat$','fun_app$b'('power$'('fun_app$b'('power$'('nat$'(2)),'fun_app$b'('power$'('nat$'(2)),'nat$'($sum('fun_app$a'('of_nat$','n$'),1))))),'n$')))),
% 91.90/13.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p',conjecture1)).
% 91.90/13.48 tff(f3,negated_conjecture,(
% 91.90/13.48 ~ $lesseq('fun_app$a'('of_nat$','fun_app$b'('power$'('fun_app$b'('power$'('nat$'(2)),'fun_app$b'('power$'('nat$'(2)),'nat$'($sum('fun_app$a'('of_nat$','n$'),1))))),'size$'('ys$'))),'fun_app$a'('of_nat$','fun_app$b'('power$'('fun_app$b'('power$'('nat$'(2)),'fun_app$b'('power$'('nat$'(2)),'nat$'($sum('fun_app$a'('of_nat$','n$'),1))))),'n$')))),
% 91.90/13.48 inference(negated_conjecture,[status(cth)],[f2])).
% 91.90/13.48 tff(f4,axiom,(
% 91.90/13.48 $lesseq('fun_app$a'('of_nat$','size$'('ys$')),'fun_app$a'('of_nat$','n$'))),
% 91.90/13.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom2)).
% 91.90/13.48 tff(f121,axiom,(
% 91.90/13.48 ! [X0 : 'Nat$',X1 : 'Nat$'] : 'fun_app$a'('of_nat$','fun_app$b'('power$'(X0),X1)) = 'fun_app$a'('power$a'('fun_app$a'('of_nat$',X0)),X1)),
% 91.90/13.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom119)).
% 91.90/13.48 tff(f345,axiom,(
% 91.90/13.48 ! [X0 : 'Nat$'] : ~$lesseq('fun_app$a'('power$a'(2),X0),0)),
% 91.90/13.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom343)).
% 91.90/13.48 tff(f529,axiom,(
% 91.90/13.48 ! [X0 : $int,X1 : $int] : (X0 != X1 <=> ($less(X0,X1) | $less(X1,X0)))),
% 91.90/13.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom527)).
% 91.90/13.48 tff(f533,axiom,(
% 91.90/13.48 ! [X0 : $int,X1 : $int] : (($less(X0,X1) & $less(X1,X0)) => $false)),
% 91.90/13.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom531)).
% 91.90/13.48 tff(f536,axiom,(
% 91.90/13.48 ! [X0 : $int] : ($less(0,X0) => ? [X1 : 'Nat$'] : ($less(0,'fun_app$a'('of_nat$',X1)) & X0 = 'fun_app$a'('of_nat$',X1)))),
% 91.90/13.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom534)).
% 91.90/13.48 tff(f587,axiom,(
% 91.90/13.48 ! [X0 : 'Nat$',X1 : 'Nat$',X2 : 'Nat$'] : (($less(0,'fun_app$a'('of_nat$',X0)) & $less('fun_app$a'('of_nat$','fun_app$b'('power$'(X0),X1)),'fun_app$a'('of_nat$','fun_app$b'('power$'(X0),X2)))) => $less('fun_app$a'('of_nat$',X1),'fun_app$a'('of_nat$',X2)))),
% 91.90/13.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom585)).
% 91.90/13.48 tff(f638,axiom,(
% 91.90/13.48 ! [X0 : 'Nat$'] : 'nat$'('fun_app$a'('of_nat$',X0)) = X0),
% 91.90/13.48 file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom636)).
% 91.90/13.48 tff(f642,plain,(
% 91.90/13.48 ~ ~$less('fun_app$a'('of_nat$','fun_app$b'('power$'('fun_app$b'('power$'('nat$'(2)),'fun_app$b'('power$'('nat$'(2)),'nat$'($sum('fun_app$a'('of_nat$','n$'),1))))),'n$')),'fun_app$a'('of_nat$','fun_app$b'('power$'('fun_app$b'('power$'('nat$'(2)),'fun_app$b'('power$'('nat$'(2)),'nat$'($sum('fun_app$a'('of_nat$','n$'),1))))),'size$'('ys$'))))),
% 91.90/13.48 inference(theory_normalization,[],[f3])).
% 91.90/13.48 tff(f643,plain,(
% 91.90/13.48 ~$less('fun_app$a'('of_nat$','n$'),'fun_app$a'('of_nat$','size$'('ys$')))),
% 91.90/13.48 inference(theory_normalization,[],[f4])).
% 91.90/13.48 tff(f805,plain,(
% 91.90/13.48 ! [X0 : 'Nat$'] : $less(0,'fun_app$a'('power$a'(2),X0))),
% 91.90/13.48 inference(theory_normalization,[],[f345])).
% 91.90/13.48 tff(f848,definition,(
% 91.90/13.48 ( ! [X0 : $int,X1 : $int] : ($sum(X0,X1) = $sum(X1,X0)) )),
% 91.90/13.48 introduced(theory,[tha_commutativity])).
% 91.90/13.48 tff(f857,definition,(
% 91.90/13.48 ( ! [X0 : $int,X1 : $int] : ($less(X1,$sum(X0,1)) | $less(X0,X1)) )),
% 91.90/13.48 introduced(theory,[tha_order_plus_one_dichotomy])).
% 91.90/13.48 tff(f883,plain,(
% 91.90/13.48 $less('fun_app$a'('of_nat$','fun_app$b'('power$'('fun_app$b'('power$'('nat$'(2)),'fun_app$b'('power$'('nat$'(2)),'nat$'($sum('fun_app$a'('of_nat$','n$'),1))))),'n$')),'fun_app$a'('of_nat$','fun_app$b'('power$'('fun_app$b'('power$'('nat$'(2)),'fun_app$b'('power$'('nat$'(2)),'nat$'($sum('fun_app$a'('of_nat$','n$'),1))))),'size$'('ys$'))))),
% 91.90/13.48 inference(flattening,[],[f642])).
% 91.90/13.48 tff(f964,plain,(
% 91.90/13.48 ! [X0 : $int,X1 : $int] : ~($less(X0,X1) & $less(X1,X0))),
% 91.90/13.48 inference(true_and_false_elimination,[],[f533])).
% 91.90/13.48 tff(f1412,plain,(
% 91.90/13.48 ! [X0 : $int,X1 : $int] : (~$less(X0,X1) | ~$less(X1,X0))),
% 91.90/13.48 inference(ennf_transformation,[],[f964])).
% 91.90/13.48 tff(f1415,plain,(
% 91.90/13.48 ! [X0 : $int] : (? [X1 : 'Nat$'] : ($less(0,'fun_app$a'('of_nat$',X1)) & X0 = 'fun_app$a'('of_nat$',X1)) | ~$less(0,X0))),
% 91.90/13.48 inference(ennf_transformation,[],[f536])).
% 91.90/13.48 tff(f1456,plain,(
% 91.90/13.48 ! [X0 : 'Nat$',X1 : 'Nat$',X2 : 'Nat$'] : ($less('fun_app$a'('of_nat$',X1),'fun_app$a'('of_nat$',X2)) | (~$less(0,'fun_app$a'('of_nat$',X0)) | ~$less('fun_app$a'('of_nat$','fun_app$b'('power$'(X0),X1)),'fun_app$a'('of_nat$','fun_app$b'('power$'(X0),X2)))))),
% 91.90/13.48 inference(ennf_transformation,[],[f587])).
% 91.90/13.48 tff(f1457,plain,(
% 91.90/13.48 ! [X0 : 'Nat$',X1 : 'Nat$',X2 : 'Nat$'] : ($less('fun_app$a'('of_nat$',X1),'fun_app$a'('of_nat$',X2)) | ~$less(0,'fun_app$a'('of_nat$',X0)) | ~$less('fun_app$a'('of_nat$','fun_app$b'('power$'(X0),X1)),'fun_app$a'('of_nat$','fun_app$b'('power$'(X0),X2))))),
% 91.90/13.48 inference(flattening,[],[f1456])).
% 91.90/13.48 tff(f1840,plain,(
% 91.90/13.48 ! [X0 : $int,X1 : $int] : ((X0 != X1 | (~$less(X0,X1) & ~$less(X1,X0))) & (($less(X0,X1) | $less(X1,X0)) | X0 = X1))),
% 91.90/13.48 inference(nnf_transformation,[],[f529])).
% 91.90/13.48 tff(f1841,plain,(
% 91.90/13.48 ! [X0 : $int,X1 : $int] : ((X0 != X1 | (~$less(X0,X1) & ~$less(X1,X0))) & ($less(X0,X1) | $less(X1,X0) | X0 = X1))),
% 91.90/13.48 inference(flattening,[],[f1840])).
% 91.90/13.48 tff(f1846,plain,(
% 91.90/13.48 ! [X0 : $int] : (($less(0,'fun_app$a'('of_nat$',sK221(X0))) & 'fun_app$a'('of_nat$',sK221(X0)) = X0) | ~$less(0,X0))),
% 91.90/13.48 inference(skolemize,[status(esa),new_symbols(skolem,[sK221]),skolemize(X1,sK221(X0))],[f1415])).
% 91.90/13.48 tff(f1925,plain,(
% 91.90/13.48 $less('fun_app$a'('of_nat$','fun_app$b'('power$'('fun_app$b'('power$'('nat$'(2)),'fun_app$b'('power$'('nat$'(2)),'nat$'($sum('fun_app$a'('of_nat$','n$'),1))))),'n$')),'fun_app$a'('of_nat$','fun_app$b'('power$'('fun_app$b'('power$'('nat$'(2)),'fun_app$b'('power$'('nat$'(2)),'nat$'($sum('fun_app$a'('of_nat$','n$'),1))))),'size$'('ys$'))))),
% 91.90/13.48 inference(cnf_transformation,[],[f883])).
% 91.90/13.48 tff(f1926,plain,(
% 91.90/13.48 ~$less('fun_app$a'('of_nat$','n$'),'fun_app$a'('of_nat$','size$'('ys$')))),
% 91.90/13.48 inference(cnf_transformation,[],[f643])).
% 91.90/13.48 tff(f2097,plain,(
% 91.90/13.48 ( ! [X0 : 'Nat$',X1 : 'Nat$'] : ('fun_app$a'('of_nat$','fun_app$b'('power$'(X0),X1)) = 'fun_app$a'('power$a'('fun_app$a'('of_nat$',X0)),X1)) )),
% 91.90/13.48 inference(cnf_transformation,[],[f121])).
% 91.90/13.48 tff(f2494,plain,(
% 91.90/13.48 ( ! [X0 : 'Nat$'] : ($less(0,'fun_app$a'('power$a'(2),X0))) )),
% 91.90/13.48 inference(cnf_transformation,[],[f805])).
% 91.90/13.48 tff(f2808,plain,(
% 91.90/13.48 ( ! [X0 : $int,X1 : $int] : (X0 != X1 | ~$less(X1,X0)) )),
% 91.90/13.48 inference(cnf_transformation,[],[f1841])).
% 91.90/13.48 tff(f2817,plain,(
% 91.90/13.48 ( ! [X0 : $int,X1 : $int] : (~$less(X0,X1) | ~$less(X1,X0)) )),
% 91.90/13.48 inference(cnf_transformation,[],[f1412])).
% 91.90/13.48 tff(f2820,plain,(
% 91.90/13.48 ( ! [X0 : $int] : (~$less(0,X0) | 'fun_app$a'('of_nat$',sK221(X0)) = X0) )),
% 91.90/13.48 inference(cnf_transformation,[],[f1846])).
% 91.90/13.48 tff(f2930,plain,(
% 91.90/13.48 ( ! [X2 : 'Nat$',X0 : 'Nat$',X1 : 'Nat$'] : ($less('fun_app$a'('of_nat$',X1),'fun_app$a'('of_nat$',X2)) | ~$less(0,'fun_app$a'('of_nat$',X0)) | ~$less('fun_app$a'('of_nat$','fun_app$b'('power$'(X0),X1)),'fun_app$a'('of_nat$','fun_app$b'('power$'(X0),X2)))) )),
% 91.90/13.48 inference(cnf_transformation,[],[f1457])).
% 91.90/13.48 tff(f3018,plain,(
% 91.90/13.48 ( ! [X0 : 'Nat$'] : ('nat$'('fun_app$a'('of_nat$',X0)) = X0) )),
% 91.90/13.48 inference(cnf_transformation,[],[f638])).
% 91.90/13.48 tff(f3186,plain,(
% 91.90/13.48 ( ! [X1 : $int] : (~$less(X1,X1)) )),
% 91.90/13.48 inference(equality_resolution,[],[f2808])).
% 91.90/13.48 tff(f3267,plain,(
% 91.90/13.48 $less('fun_app$a'('of_nat$','fun_app$b'('power$'('fun_app$b'('power$'('nat$'(2)),'fun_app$b'('power$'('nat$'(2)),'nat$'($sum(1,'fun_app$a'('of_nat$','n$')))))),'n$')),'fun_app$a'('of_nat$','fun_app$b'('power$'('fun_app$b'('power$'('nat$'(2)),'fun_app$b'('power$'('nat$'(2)),'nat$'($sum(1,'fun_app$a'('of_nat$','n$')))))),'size$'('ys$'))))),
% 91.90/13.48 inference(superposition,[],[f1925,f848])).
% 91.90/13.48 tff(f3313,plain,(
% 91.90/13.48 ( ! [X0 : $int] : ($less(X0,$sum(X0,1))) )),
% 91.90/13.48 inference(resolution,[],[f857,f3186])).
% 91.90/13.48 tff(f3315,plain,(
% 91.90/13.48 ( ! [X0 : $int,X1 : $int] : (~$less($sum(X0,1),X1) | $less(X0,X1)) )),
% 91.90/13.48 inference(resolution,[],[f857,f2817])).
% 91.90/13.48 tff(f3319,plain,(
% 91.90/13.48 ( ! [X0 : $int] : ($less(X0,$sum(1,X0))) )),
% 91.90/13.48 inference(superposition,[],[f3313,f848])).
% 91.90/13.48 tff(f3361,plain,(
% 91.90/13.48 ( ! [X0 : $int] : ($less(X0,$sum(1,$sum(X0,1)))) )),
% 91.90/13.48 inference(resolution,[],[f3315,f3319])).
% 91.90/13.48 tff(f3367,plain,(
% 91.90/13.48 ( ! [X0 : $int] : ($less(X0,$sum(1,$sum(1,X0)))) )),
% 91.90/13.48 inference(superposition,[],[f3361,f848])).
% 91.90/13.48 tff(f3548,plain,(
% 91.90/13.48 $sum(1,$sum(1,0)) = 'fun_app$a'('of_nat$',sK221($sum(1,$sum(1,0))))),
% 91.90/13.48 inference(resolution,[],[f2820,f3367])).
% 91.90/13.48 tff(f3551,plain,(
% 91.90/13.48 2 = 'fun_app$a'('of_nat$',sK221(2))),
% 91.90/13.48 inference(evaluation,[],[f3548])).
% 91.90/13.48 tff(f3616,plain,(
% 91.90/13.48 'nat$'(2) = sK221(2)),
% 91.90/13.48 inference(superposition,[],[f3018,f3551])).
% 91.90/13.48 tff(f3646,plain,(
% 91.90/13.48 2 = 'fun_app$a'('of_nat$','nat$'(2))),
% 91.90/13.48 inference(superposition,[],[f3551,f3616])).
% 91.90/13.48 tff(f5162,plain,(
% 91.90/13.48 ( ! [X0 : 'Nat$'] : ('fun_app$a'('power$a'(2),X0) = 'fun_app$a'('of_nat$','fun_app$b'('power$'('nat$'(2)),X0))) )),
% 91.90/13.48 inference(superposition,[],[f2097,f3646])).
% 91.90/13.48 tff(f21518,plain,(
% 91.90/13.48 ( ! [X0 : 'Nat$'] : (~$less('fun_app$a'('of_nat$','fun_app$b'('power$'(X0),'n$')),'fun_app$a'('of_nat$','fun_app$b'('power$'(X0),'size$'('ys$')))) | ~$less(0,'fun_app$a'('of_nat$',X0))) )),
% 91.90/13.48 inference(resolution,[],[f2930,f1926])).
% 91.90/13.48 tff(f155538,plain,(
% 91.90/13.48 ~$less(0,'fun_app$a'('of_nat$','fun_app$b'('power$'('nat$'(2)),'fun_app$b'('power$'('nat$'(2)),'nat$'($sum(1,'fun_app$a'('of_nat$','n$')))))))),
% 91.90/13.48 inference(resolution,[],[f21518,f3267])).
% 91.90/13.48 tff(f155653,plain,(
% 91.90/13.48 ~$less(0,'fun_app$a'('power$a'(2),'fun_app$b'('power$'('nat$'(2)),'nat$'($sum(1,'fun_app$a'('of_nat$','n$'))))))),
% 91.90/13.48 inference(forward_demodulation,[],[f155538,f5162])).
% 91.90/13.48 tff(f155700,plain,(
% 91.90/13.48 $false),
% 91.90/13.48 inference(forward_subsumption_resolution,[],[f155653,f2494])).
% 91.90/13.48 % SZS output end Proof for theBenchmark
% 91.90/13.48 % (2367701)------------------------------
% 91.90/13.48 % (2367701)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 91.90/13.48 % (2367701)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 91.90/13.48 % (2367701)CaDiCaL version: 2.1.3
% 91.90/13.48 % (2367701)Termination reason: Refutation
% 91.90/13.48 % (2367701)Time elapsed: 4.232 s
% 91.90/13.48 % (2367701)Peak memory usage: 64 MB
% 91.90/13.48 % (2367701)Instructions burned: 8601 (million)
% 91.90/13.48 % (2367602)Success in time 13.107 s
% 91.90/13.48 % Vampire exiting
%------------------------------------------------------------------------------