%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR148^3 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n016.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 : Wed Sep 30 07:47:21 AM UTC 2026
% Result : Theorem 145.45s 21.01s
% Output : Refutation 145.45s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR148^3 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.18 % Computer : n016.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Tue Sep 29 18:02:05 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.21 Running first-order model finding
% 0.08/0.21 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
% 7.94/1.79 % (699095)Will run a generic schedule for satisfiability detection.
% 7.94/1.79 % (699102)% WARNING: option uhcvi not known.
% 7.94/1.79 % (699102)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2945121605:i=135531:add=off:rawr=on_2998 on theBenchmark for (2998ds/135531Mi)
% 7.94/1.79 % (699103)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2189549357:i=88024:add=on:rawr=on_2998 on theBenchmark for (2998ds/88024Mi)
% 7.94/1.79 % (699101)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=710048920_2998 on theBenchmark for (2998ds/0Mi)
% 7.94/1.79 % (699104)dis+10_1_sil=32000:sp=arity:random_seed=3887493263:i=103:fgj=on_2998 on theBenchmark for (2998ds/103Mi)
% 7.94/1.79 % (699105)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=871090971:i=116_2998 on theBenchmark for (2998ds/116Mi)
% 7.94/1.79 % (699107)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3545804579:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2998 on theBenchmark for (2998ds/159Mi)
% 7.94/1.79 % (699106)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3608932864:i=131_2998 on theBenchmark for (2998ds/131Mi)
% 7.94/1.79 % (699104)Instruction limit reached!
% 7.94/1.79 % (699104)------------------------------
% 7.94/1.79 % (699104)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.94/1.79 % (699104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.94/1.79 % (699104)CaDiCaL version: 2.1.3
% 7.94/1.79 % (699104)Termination reason: Instruction limit
% 7.94/1.79 % (699104)Termination phase: Initialization
% 7.94/1.79 % (699104)Time elapsed: 0.047 s
% 7.94/1.79 % (699104)Peak memory usage: 16 MB
% 7.94/1.79 % (699104)Instructions burned: 105 (million)
% 7.94/1.79 % (699106)Instruction limit reached!
% 7.94/1.79 % (699106)------------------------------
% 7.94/1.79 % (699106)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.94/1.79 % (699106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.94/1.79 % (699106)CaDiCaL version: 2.1.3
% 7.94/1.79 % (699106)Termination reason: Instruction limit
% 7.94/1.79 % (699106)Termination phase: Initialization
% 7.94/1.79 % (699106)Time elapsed: 0.056 s
% 7.94/1.79 % (699106)Peak memory usage: 16 MB
% 7.94/1.79 % (699106)Instructions burned: 133 (million)
% 7.94/1.79 % (699107)Instruction limit reached!
% 7.94/1.79 % (699107)------------------------------
% 7.94/1.79 % (699107)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.94/1.79 % (699105)Instruction limit reached!
% 7.94/1.79 % (699105)------------------------------
% 7.94/1.79 % (699105)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.94/1.79 % (699105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.94/1.79 % (699107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.94/1.79 % (699105)CaDiCaL version: 2.1.3
% 7.94/1.79 % (699105)Termination reason: Instruction limit
% 7.94/1.79 % (699105)Termination phase: Initialization
% 7.94/1.79 % (699105)Time elapsed: 0.065 s
% 7.94/1.79 % (699105)Peak memory usage: 16 MB
% 7.94/1.79 % (699105)Instructions burned: 116 (million)
% 7.94/1.79 % (699107)CaDiCaL version: 2.1.3
% 7.94/1.79 % (699107)Termination reason: Instruction limit
% 7.94/1.79 % (699107)Termination phase: Property scanning
% 7.94/1.79 % (699107)Time elapsed: 0.065 s
% 7.94/1.79 % (699107)Peak memory usage: 16 MB
% 7.94/1.79 % (699107)Instructions burned: 161 (million)
% 7.94/1.79 % (699115)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1501976293:i=714:nm=2_2997 on theBenchmark for (2997ds/714Mi)
% 7.94/1.79 % (699116)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=214677820:i=131:bd=preordered:fsd=on_2997 on theBenchmark for (2997ds/131Mi)
% 7.94/1.79 % (699118)ott-21_1_sil=16000:fs=off:random_seed=2539103111:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 7.94/1.79 % (699117)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=3061747612:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi)
% 7.94/1.79 % (699102)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 7.94/1.79 % (699116)Instruction limit reached!
% 7.94/1.79 % (699116)------------------------------
% 7.94/1.79 % (699116)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.94/1.79 % (699116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.59/3.62 % (699116)CaDiCaL version: 2.1.3
% 22.59/3.62 % (699116)Termination reason: Instruction limit
% 22.59/3.62 % (699116)Termination phase: Initialization
% 22.59/3.62 % (699116)Time elapsed: 0.079 s
% 22.59/3.62 % (699116)Peak memory usage: 15 MB
% 22.59/3.62 % (699116)Instructions burned: 133 (million)
% 22.59/3.62 % (699118)Instruction limit reached!
% 22.59/3.62 % (699118)------------------------------
% 22.59/3.62 % (699118)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.59/3.62 % (699118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.59/3.62 % (699118)CaDiCaL version: 2.1.3
% 22.59/3.62 % (699118)Termination reason: Instruction limit
% 22.59/3.62 % (699118)Termination phase: Property scanning
% 22.59/3.62 % (699118)Time elapsed: 0.094 s
% 22.59/3.62 % (699118)Peak memory usage: 16 MB
% 22.59/3.62 % (699118)Instructions burned: 180 (million)
% 22.59/3.62 % (699123)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4251867328:i=477:bd=all_2996 on theBenchmark for (2996ds/477Mi)
% 22.59/3.62 % (699124)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1458139362:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 22.59/3.62 % (699102)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 22.59/3.62 % Exception at run slice level
% 22.59/3.62 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 22.59/3.62 % (699127)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3666818740:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 22.59/3.62 % (699117)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 22.59/3.62 % Exception at run slice level
% 22.59/3.62 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 22.59/3.62 % (699123)Instruction limit reached!
% 22.59/3.62 % (699123)------------------------------
% 22.59/3.62 % (699123)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.59/3.62 % (699123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.59/3.62 % (699123)CaDiCaL version: 2.1.3
% 22.59/3.62 % (699123)Termination reason: Instruction limit
% 22.59/3.62 % (699123)Termination phase: Property scanning
% 22.59/3.62 % (699123)Time elapsed: 0.201 s
% 22.59/3.62 % (699123)Peak memory usage: 19 MB
% 22.59/3.62 % (699123)Instructions burned: 477 (million)
% 22.59/3.62 % (699129)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2877948777:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 22.59/3.62 % (699130)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=604675899:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 22.59/3.62 % Exception at run slice level
% 22.59/3.62 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 22.59/3.62 % (699117)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 22.59/3.62 % (699133)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1902670336:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 22.59/3.62 % (699117)Instruction limit reached!
% 22.59/3.62 % (699117)------------------------------
% 22.59/3.62 % (699117)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.59/3.62 % (699117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.59/3.62 % (699117)CaDiCaL version: 2.1.3
% 22.59/3.62 % (699117)Termination reason: Instruction limit
% 22.59/3.62 % (699117)Termination phase: Saturation
% 22.59/3.62 % (699117)Time elapsed: 0.423 s
% 22.59/3.62 % (699117)Peak memory usage: 21 MB
% 22.59/3.62 % (699117)Instructions burned: 685 (million)
% 22.59/3.62 % (699130)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 22.59/3.62 % (699135)fmb+10_1_sil=64000:random_seed=1718526225:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi)
% 22.59/3.62 % (699133)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 22.59/3.62 % (699130)Instruction limit reached!
% 22.59/3.62 % (699130)------------------------------
% 22.59/3.62 % (699130)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.59/3.62 % (699130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.92/7.75 % (699130)CaDiCaL version: 2.1.3
% 51.92/7.75 % (699130)Termination reason: Instruction limit
% 51.92/7.75 % (699130)Termination phase: Saturation
% 51.92/7.75 % (699130)Time elapsed: 0.328 s
% 51.92/7.75 % (699130)Peak memory usage: 22 MB
% 51.92/7.75 % (699130)Instructions burned: 693 (million)
% 51.92/7.75 % (699137)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2378060372:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 51.92/7.75 % (699127)Instruction limit reached!
% 51.92/7.75 % (699127)------------------------------
% 51.92/7.75 % (699127)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.92/7.75 % (699127)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.92/7.75 % (699127)CaDiCaL version: 2.1.3
% 51.92/7.75 % (699127)Termination reason: Instruction limit
% 51.92/7.75 % (699127)Termination phase: Saturation
% 51.92/7.75 % (699127)Time elapsed: 0.526 s
% 51.92/7.75 % (699127)Peak memory usage: 24 MB
% 51.92/7.75 % (699127)Instructions burned: 1181 (million)
% 51.92/7.75 % (699139)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=359468396:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 51.92/7.75 % Exception at run slice level
% 51.92/7.75 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 51.92/7.75 % (699141)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1153627895:i=5131_2990 on theBenchmark for (2990ds/5131Mi)
% 51.92/7.75 % (699135)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 51.92/7.75 % Exception at run slice level
% 51.92/7.75 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 51.92/7.75 % (699143)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3668763463:i=1472:ins=7:fdi=8:gsp=on_2989 on theBenchmark for (2989ds/1472Mi)
% 51.92/7.75 % (699141)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 51.92/7.75 % (699133)Instruction limit reached!
% 51.92/7.75 % (699133)------------------------------
% 51.92/7.75 % (699133)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.92/7.75 % (699133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.92/7.75 % (699133)CaDiCaL version: 2.1.3
% 51.92/7.75 % (699133)Termination reason: Instruction limit
% 51.92/7.75 % (699133)Termination phase: Saturation
% 51.92/7.75 % (699133)Time elapsed: 0.489 s
% 51.92/7.75 % (699133)Peak memory usage: 25 MB
% 51.92/7.75 % (699133)Instructions burned: 879 (million)
% 51.92/7.75 % Exception at run slice level
% 51.92/7.75 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 51.92/7.75 % (699147)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=326628949:i=6324_2988 on theBenchmark for (2988ds/6324Mi)
% 51.92/7.75 % (699151)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3259662847:fmbsr=2.30978:i=2174_2988 on theBenchmark for (2988ds/2174Mi)
% 51.92/7.75 % Exception at run slice level
% 51.92/7.75 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 51.92/7.75 % (699143)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 51.92/7.75 % (699154)ott-2_1_sil=16000:newcnf=on:random_seed=2299208012:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2987 on theBenchmark for (2987ds/869Mi)
% 51.92/7.75 % (699143)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 51.92/7.75 % (699154)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 51.92/7.75 % Exception at run slice level
% 51.92/7.75 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 51.92/7.75 % (699156)ott+10_1_sil=32000:tgt=ground:random_seed=3856711972:i=5114:av=off_2986 on theBenchmark for (2986ds/5114Mi)
% 51.92/7.75 % (699143)Instruction limit reached!
% 51.92/7.75 % (699143)------------------------------
% 51.92/7.75 % (699143)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 51.92/7.75 % (699143)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.92/7.75 % (699143)CaDiCaL version: 2.1.3
% 51.92/7.75 % (699143)Termination reason: Instruction limit
% 51.92/7.75 % (699143)Termination phase: Saturation
% 51.92/7.75 % (699143)Time elapsed: 0.461 s
% 51.92/7.75 % (699143)Peak memory usage: 27 MB
% 51.92/7.75 % (699143)Instructions burned: 1475 (million)
% 98.19/14.27 % (699158)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2354942795:i=54282_2984 on theBenchmark for (2984ds/54282Mi)
% 98.19/14.27 % Exception at run slice level
% 98.19/14.27 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 98.19/14.27 % (699154)Instruction limit reached!
% 98.19/14.27 % (699154)------------------------------
% 98.19/14.27 % (699154)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 98.19/14.27 % (699154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.19/14.27 % (699154)CaDiCaL version: 2.1.3
% 98.19/14.27 % (699154)Termination reason: Instruction limit
% 98.19/14.27 % (699154)Termination phase: Saturation
% 98.19/14.27 % (699154)Time elapsed: 0.387 s
% 98.19/14.27 % (699154)Peak memory usage: 24 MB
% 98.19/14.27 % (699154)Instructions burned: 869 (million)
% 98.19/14.27 % (699161)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3004626033:i=3512:aac=none_2983 on theBenchmark for (2983ds/3512Mi)
% 98.19/14.27 % (699162)dis+21_1_sil=32000:sas=cadical:random_seed=1287381589:i=3773:amm=off_2983 on theBenchmark for (2983ds/3773Mi)
% 98.19/14.27 % Exception at run slice level
% 98.19/14.27 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 98.19/14.27 % (699165)ott+11_1_sil=16000:gs=on:random_seed=3042452614:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2982 on theBenchmark for (2982ds/2251Mi)
% 98.19/14.27 % (699165)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 98.19/14.27 % (699161)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 98.19/14.27 % (699165)Instruction limit reached!
% 98.19/14.27 % (699165)------------------------------
% 98.19/14.27 % (699165)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 98.19/14.27 % (699165)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.19/14.27 % (699165)CaDiCaL version: 2.1.3
% 98.19/14.27 % (699165)Termination reason: Instruction limit
% 98.19/14.27 % (699165)Termination phase: Saturation
% 98.19/14.27 % (699165)Time elapsed: 0.541 s
% 98.19/14.27 % (699165)Peak memory usage: 27 MB
% 98.19/14.27 % (699165)Instructions burned: 2256 (million)
% 98.19/14.27 % (699167)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3036452051:fmbsr=1.6:i=67534_2977 on theBenchmark for (2977ds/67534Mi)
% 98.19/14.27 % Exception at run slice level
% 98.19/14.27 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 98.19/14.27 % (699169)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=46923213:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2976 on theBenchmark for (2976ds/4591Mi)
% 98.19/14.27 % (699161)Instruction limit reached!
% 98.19/14.27 % (699161)------------------------------
% 98.19/14.27 % (699161)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 98.19/14.27 % (699161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.19/14.27 % (699161)CaDiCaL version: 2.1.3
% 98.19/14.27 % (699161)Termination reason: Instruction limit
% 98.19/14.27 % (699161)Termination phase: Saturation
% 98.19/14.27 % (699161)Time elapsed: 1.417 s
% 98.19/14.27 % (699161)Peak memory usage: 22 MB
% 98.19/14.27 % (699161)Instructions burned: 3513 (million)
% 98.19/14.27 % (699171)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3614198026:i=29340_2969 on theBenchmark for (2969ds/29340Mi)
% 98.19/14.27 % (699141)Instruction limit reached!
% 98.19/14.27 % (699141)------------------------------
% 98.19/14.27 % (699141)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 98.19/14.27 % (699141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 98.19/14.27 % (699141)CaDiCaL version: 2.1.3
% 98.19/14.27 % (699141)Termination reason: Instruction limit
% 98.19/14.27 % (699141)Termination phase: Saturation
% 98.19/14.27 % (699141)Time elapsed: 2.247 s
% 98.19/14.27 % (699141)Peak memory usage: 22 MB
% 98.19/14.27 % (699141)Instructions burned: 5133 (million)
% 98.19/14.27 % (699173)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=1904911796:i=5211_2967 on theBenchmark for (2967ds/5211Mi)
% 98.19/14.27 % (699169)Instruction limit reached!
% 98.19/14.27 % (699169)------------------------------
% 98.19/14.27 % (699169)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 98.19/14.27 % (699169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 137.86/19.85 % (699169)CaDiCaL version: 2.1.3
% 137.86/19.85 % (699169)Termination reason: Instruction limit
% 137.86/19.85 % (699169)Termination phase: Saturation
% 137.86/19.85 % (699169)Time elapsed: 0.999 s
% 137.86/19.85 % (699169)Peak memory usage: 27 MB
% 137.86/19.85 % (699169)Instructions burned: 4593 (million)
% 137.86/19.85 % (699175)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2121747883:i=5497:nm=2_2966 on theBenchmark for (2966ds/5497Mi)
% 137.86/19.85 % (699156)Instruction limit reached!
% 137.86/19.85 % (699156)------------------------------
% 137.86/19.85 % (699156)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 137.86/19.85 % (699156)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 137.86/19.85 % (699156)CaDiCaL version: 2.1.3
% 137.86/19.85 % (699156)Termination reason: Instruction limit
% 137.86/19.85 % (699156)Termination phase: Saturation
% 137.86/19.85 % (699156)Time elapsed: 2.082 s
% 137.86/19.85 % (699156)Peak memory usage: 25 MB
% 137.86/19.85 % (699156)Instructions burned: 5116 (million)
% 137.86/19.85 % (699177)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3956792907:fmbsr=2:i=46332_2965 on theBenchmark for (2965ds/46332Mi)
% 137.86/19.85 % (699162)Instruction limit reached!
% 137.86/19.85 % (699162)------------------------------
% 137.86/19.85 % (699162)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 137.86/19.85 % (699162)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 137.86/19.85 % (699162)CaDiCaL version: 2.1.3
% 137.86/19.85 % (699162)Termination reason: Instruction limit
% 137.86/19.85 % (699162)Termination phase: Saturation
% 137.86/19.85 % (699162)Time elapsed: 1.865 s
% 137.86/19.85 % (699162)Peak memory usage: 22 MB
% 137.86/19.85 % (699162)Instructions burned: 3775 (million)
% 137.86/19.85 % Exception at run slice level
% 137.86/19.85 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 137.86/19.85 % (699179)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=1118093859:i=14071_2964 on theBenchmark for (2964ds/14071Mi)
% 137.86/19.85 % (699181)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3995768014:i=22565:add=on:rawr=on_2964 on theBenchmark for (2964ds/22565Mi)
% 137.86/19.85 % Exception at run slice level
% 137.86/19.85 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 137.86/19.85 % (699183)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1008801177:i=8173:av=off_2962 on theBenchmark for (2962ds/8173Mi)
% 137.86/19.85 % Exception at run slice level
% 137.86/19.85 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 137.86/19.85 % (699185)dis+10_16:1_sil=16000:random_seed=3765682155:i=9155:fsr=off_2962 on theBenchmark for (2962ds/9155Mi)
% 137.86/19.85 % (699173)Instruction limit reached!
% 137.86/19.85 % (699173)------------------------------
% 137.86/19.85 % (699173)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 137.86/19.85 % (699173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 137.86/19.85 % (699173)CaDiCaL version: 2.1.3
% 137.86/19.85 % (699173)Termination reason: Instruction limit
% 137.86/19.85 % (699173)Termination phase: Saturation
% 137.86/19.85 % (699173)Time elapsed: 2.151 s
% 137.86/19.85 % (699173)Peak memory usage: 27 MB
% 137.86/19.85 % (699173)Instructions burned: 5212 (million)
% 137.86/19.85 % (699187)ott-3_8_sil=64000:random_seed=387551714:i=20139:bs=on_2945 on theBenchmark for (2945ds/20139Mi)
% 137.86/19.85 % (699183)Instruction limit reached!
% 137.86/19.85 % (699183)------------------------------
% 137.86/19.85 % (699183)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 137.86/19.85 % (699183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 137.86/19.85 % (699183)CaDiCaL version: 2.1.3
% 137.86/19.85 % (699183)Termination reason: Instruction limit
% 137.86/19.85 % (699183)Termination phase: Saturation
% 137.86/19.85 % (699183)Time elapsed: 3.307 s
% 137.86/19.85 % (699183)Peak memory usage: 27 MB
% 137.86/19.85 % (699183)Instructions burned: 8175 (million)
% 137.86/19.85 % (699189)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=2855112987:fmbsr=2:i=32576_2929 on theBenchmark for (2929ds/32576Mi)
% 137.86/19.85 % Exception at run slice level
% 137.86/19.85 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 137.86/19.85 % (699191)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3169021846:i=11404_2927 on theBenchmark for (2927ds/11404Mi)
% 137.86/19.85 % (699185)Instruction limit reached!
% 145.45/21.00 % (699185)------------------------------
% 145.45/21.00 % (699185)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 145.45/21.00 % (699185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.45/21.00 % (699185)CaDiCaL version: 2.1.3
% 145.45/21.00 % (699185)Termination reason: Instruction limit
% 145.45/21.00 % (699185)Termination phase: Saturation
% 145.45/21.00 % (699185)Time elapsed: 3.750 s
% 145.45/21.00 % (699185)Peak memory usage: 23 MB
% 145.45/21.00 % (699185)Instructions burned: 9156 (million)
% 145.45/21.00 % (699193)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2558951086:i=14134_2924 on theBenchmark for (2924ds/14134Mi)
% 145.45/21.00 % (699193)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 145.45/21.00 % (699181)Instruction limit reached!
% 145.45/21.00 % (699181)------------------------------
% 145.45/21.00 % (699181)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 145.45/21.00 % (699181)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.45/21.00 % (699181)CaDiCaL version: 2.1.3
% 145.45/21.00 % (699181)Termination reason: Instruction limit
% 145.45/21.00 % (699181)Termination phase: Saturation
% 145.45/21.00 % (699181)Time elapsed: 5.179 s
% 145.45/21.00 % (699181)Peak memory usage: 27 MB
% 145.45/21.00 % (699181)Instructions burned: 22566 (million)
% 145.45/21.00 % (699195)dis+33_16_sil=32000:sac=on:random_seed=3515919393:i=15851:nm=0_2912 on theBenchmark for (2912ds/15851Mi)
% 145.45/21.00 % (699191)Instruction limit reached!
% 145.45/21.00 % (699191)------------------------------
% 145.45/21.00 % (699191)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 145.45/21.00 % (699191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.45/21.00 % (699191)CaDiCaL version: 2.1.3
% 145.45/21.00 % (699191)Termination reason: Instruction limit
% 145.45/21.00 % (699191)Termination phase: Saturation
% 145.45/21.00 % (699191)Time elapsed: 4.694 s
% 145.45/21.00 % (699191)Peak memory usage: 27 MB
% 145.45/21.00 % (699191)Instructions burned: 11406 (million)
% 145.45/21.00 % (699198)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=333911740:avsq=on:i=17627:add=on:amm=off_2879 on theBenchmark for (2879ds/17627Mi)
% 145.45/21.00 % (699195)Instruction limit reached!
% 145.45/21.00 % (699195)------------------------------
% 145.45/21.00 % (699195)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 145.45/21.00 % (699195)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.45/21.00 % (699195)CaDiCaL version: 2.1.3
% 145.45/21.00 % (699195)Termination reason: Instruction limit
% 145.45/21.00 % (699195)Termination phase: Saturation
% 145.45/21.00 % (699195)Time elapsed: 3.594 s
% 145.45/21.00 % (699195)Peak memory usage: 23 MB
% 145.45/21.00 % (699195)Instructions burned: 15852 (million)
% 145.45/21.00 % (699201)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=1208561981:s2a=on:i=53295_2876 on theBenchmark for (2876ds/53295Mi)
% 145.45/21.00 % (699193)Instruction limit reached!
% 145.45/21.00 % (699193)------------------------------
% 145.45/21.00 % (699193)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 145.45/21.00 % (699193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.45/21.00 % (699193)CaDiCaL version: 2.1.3
% 145.45/21.00 % (699193)Termination reason: Instruction limit
% 145.45/21.00 % (699193)Termination phase: Saturation
% 145.45/21.00 % (699193)Time elapsed: 5.849 s
% 145.45/21.00 % (699193)Peak memory usage: 26 MB
% 145.45/21.00 % (699193)Instructions burned: 14135 (million)
% 145.45/21.00 % (699204)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1693090933:i=26857:ins=20_2866 on theBenchmark for (2866ds/26857Mi)
% 145.45/21.00 % Exception at run slice level
% 145.45/21.00 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 145.45/21.00 % (699206)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3472112065:i=28120:bs=on:fsr=off_2863 on theBenchmark for (2863ds/28120Mi)
% 145.45/21.00 % (699187)Instruction limit reached!
% 145.45/21.00 % (699187)------------------------------
% 145.45/21.00 % (699187)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 145.45/21.00 % (699187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.45/21.00 % (699187)CaDiCaL version: 2.1.3
% 145.45/21.00 % (699187)Termination reason: Instruction limit
% 145.45/21.00 % (699187)Termination phase: Saturation
% 145.45/21.00 % (699187)Time elapsed: 8.597 s
% 145.45/21.00 % (699187)Peak memory usage: 28 MB
% 145.45/21.00 % (699187)Instructions burned: 20140 (million)
% 145.45/21.00 % (699208)fmb+10_1_sil=256000:fmbss=7:random_seed=1721793681:fmbsr=1.6:i=182295_2859 on theBenchmark for (2859ds/182295Mi)
% 145.45/21.00 % Exception at run slice level
% 145.45/21.00 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 145.45/21.00 % (699211)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=2181337774:i=44625:gsp=on_2857 on theBenchmark for (2857ds/44625Mi)
% 145.45/21.00 % (699211)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 145.45/21.00 % (699211)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 145.45/21.00 % (699171)Instruction limit reached!
% 145.45/21.00 % (699171)------------------------------
% 145.45/21.00 % (699171)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 145.45/21.00 % (699171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.45/21.00 % (699171)CaDiCaL version: 2.1.3
% 145.45/21.00 % (699171)Termination reason: Instruction limit
% 145.45/21.00 % (699171)Termination phase: Saturation
% 145.45/21.01 % (699171)Time elapsed: 11.436 s
% 145.45/21.01 % (699171)Peak memory usage: 25 MB
% 145.45/21.01 % (699171)Instructions burned: 29343 (million)
% 145.45/21.01 % (699213)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=747889595:i=160505_2854 on theBenchmark for (2854ds/160505Mi)
% 145.45/21.01 % Exception at run slice level
% 145.45/21.01 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 145.45/21.01 % (699215)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=2842708393:fmbsr=1.3:i=225729_2854 on theBenchmark for (2854ds/225729Mi)
% 145.45/21.01 % Exception at run slice level
% 145.45/21.01 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 145.45/21.01 % (699217)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=76550153:fmbsr=2:i=185024:ins=7_2853 on theBenchmark for (2853ds/185024Mi)
% 145.45/21.01 % Exception at run slice level
% 145.45/21.01 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 145.45/21.01 % Exception at run slice level
% 145.45/21.01 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 145.45/21.01 % (699219)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=2070155263:rtra=on_2852 on theBenchmark for (2852ds/0Mi)
% 145.45/21.01 % (699220)% WARNING: option uhcvi not known.
% 145.45/21.01 % (699220)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1465179233:i=271062:add=off:rtra=on:rawr=on_2852 on theBenchmark for (2852ds/271062Mi)
% 145.45/21.01 % (699220)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 145.45/21.01 % Exception at run slice level
% 145.45/21.01 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 145.45/21.01 % (699223)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2098200338:i=176048:add=on:rtra=on:rawr=on_2850 on theBenchmark for (2850ds/176048Mi)
% 145.45/21.01 % (699220)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 145.45/21.01 % (699198)Instruction limit reached!
% 145.45/21.01 % (699198)------------------------------
% 145.45/21.01 % (699198)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 145.45/21.01 % (699198)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.45/21.01 % (699198)CaDiCaL version: 2.1.3
% 145.45/21.01 % (699198)Termination reason: Instruction limit
% 145.45/21.01 % (699198)Termination phase: Saturation
% 145.45/21.01 % (699198)Time elapsed: 7.497 s
% 145.45/21.01 % (699198)Peak memory usage: 25 MB
% 145.45/21.01 % (699198)Instructions burned: 17627 (million)
% 145.45/21.01 % (699379)dis+10_1_sil=32000:si=on:sp=arity:random_seed=55905917:i=206:fgj=on:rtra=on_2804 on theBenchmark for (2804ds/206Mi)
% 145.45/21.01 % (699379)Instruction limit reached!
% 145.45/21.01 % (699379)------------------------------
% 145.45/21.01 % (699379)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 145.45/21.01 % (699379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.45/21.01 % (699379)CaDiCaL version: 2.1.3
% 145.45/21.01 % (699379)Termination reason: Instruction limit
% 145.45/21.01 % (699379)Termination phase: Property scanning
% 145.45/21.01 % (699379)Time elapsed: 0.085 s
% 145.45/21.01 % (699379)Peak memory usage: 16 MB
% 145.45/21.01 % (699379)Instructions burned: 206 (million)
% 145.45/21.01 % (699381)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=3967247743:i=232:rtra=on_2803 on theBenchmark for (2803ds/232Mi)
% 145.45/21.01 % (699381)Instruction limit reached!
% 145.45/21.01 % (699381)------------------------------
% 145.45/21.01 % (699381)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 145.45/21.01 % (699381)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.45/21.01 % (699381)CaDiCaL version: 2.1.3
% 145.45/21.01 % (699381)Termination reason: Instruction limit
% 145.45/21.01 % (699381)Termination phase: Property scanning
% 145.45/21.01 % (699381)Time elapsed: 0.096 s
% 145.45/21.01 % (699381)Peak memory usage: 16 MB
% 145.45/21.01 % (699381)Instructions burned: 234 (million)
% 145.45/21.01 % (699383)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=3427267322:i=262:rtra=on_2802 on theBenchmark for (2802ds/262Mi)
% 145.45/21.01 % (699383)Instruction limit reached!
% 145.45/21.01 % (699383)------------------------------
% 145.45/21.01 % (699383)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 145.45/21.01 % (699383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.45/21.01 % (699383)CaDiCaL version: 2.1.3
% 145.45/21.01 % (699383)Termination reason: Instruction limit
% 145.45/21.01 % (699383)Termination phase: shuffling
% 145.45/21.01 % (699383)Time elapsed: 0.110 s
% 145.45/21.01 % (699383)Peak memory usage: 17 MB
% 145.45/21.01 % (699383)Instructions burned: 263 (million)
% 145.45/21.01 % (699385)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=4179684386:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2801 on theBenchmark for (2801ds/318Mi)
% 145.45/21.01 % (699385)Instruction limit reached!
% 145.45/21.01 % (699385)------------------------------
% 145.45/21.01 % (699385)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 145.45/21.01 % (699385)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.45/21.01 % (699385)CaDiCaL version: 2.1.3
% 145.45/21.01 % (699385)Termination reason: Instruction limit
% 145.45/21.01 % (699385)Termination phase: Preprocessing 3
% 145.45/21.01 % (699385)Time elapsed: 0.136 s
% 145.45/21.01 % (699385)Peak memory usage: 19 MB
% 145.45/21.01 % (699385)Instructions burned: 319 (million)
% 145.45/21.01 % (699387)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=4079715769:i=1428:nm=2:rtra=on_2799 on theBenchmark for (2799ds/1428Mi)
% 145.45/21.01 % Exception at run slice level
% 145.45/21.01 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 145.45/21.01 % (699389)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=4099039247:i=262:bd=preordered:rtra=on:fsd=on_2797 on theBenchmark for (2797ds/262Mi)
% 145.45/21.01 % (699389)Instruction limit reached!
% 145.45/21.01 % (699389)------------------------------
% 145.45/21.01 % (699389)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 145.45/21.01 % (699389)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.45/21.01 % (699389)CaDiCaL version: 2.1.3
% 145.45/21.01 % (699389)Termination reason: Instruction limit
% 145.45/21.01 % (699389)Termination phase: Naming
% 145.45/21.01 % (699389)Time elapsed: 0.110 s
% 145.45/21.01 % (699389)Peak memory usage: 17 MB
% 145.45/21.01 % (699389)Instructions burned: 263 (million)
% 145.45/21.01 % (699391)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:si=on:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1601447522:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2795 on theBenchmark for (2795ds/1368Mi)
% 145.45/21.01 % (699391)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 145.45/21.01 % (699391)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 145.45/21.01 % (699391) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-699095-699391"...
% 145.45/21.01 % (699391)...printing done.
% 145.45/21.01 % (699391)Refutation found. Thanks to Tanya!
% 145.45/21.01 % SZS status Theorem for theBenchmark
% 145.45/21.01 % SZS output start Proof for theBenchmark
% 145.45/21.01 thf(type_def_5, type, num: $tType).
% 145.45/21.01 thf(type_def_6, type, sTfun: ($tType * $tType) > $tType).
% 145.45/21.01 thf(func_def_0, type, abstractCounterpart_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_2, type, age_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_3, type, agent_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_4, type, altitude_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 145.45/21.01 thf(func_def_5, type, ancestor_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_8, type, arcWeight_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_9, type, atomicNumber_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_10, type, attends_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_11, type, attribute_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_12, type, authors_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_13, type, average_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_14, type, barometricPressure_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_15, type, beforeOrEqual_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_16, type, before_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_17, type, believes_THFTYPE_IiooI: ($i > $o > $o)).
% 145.45/21.01 thf(func_def_18, type, between_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 145.45/21.01 thf(func_def_19, type, boilingPoint_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_20, type, bottom_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_22, type, capability_THFTYPE_IIioIIiioIioI: (($i > $o) > ($i > $i > $o) > $i > $o)).
% 145.45/21.01 thf(func_def_23, type, capability_THFTYPE_IiIiioIioI: ($i > ($i > $i > $o) > $i > $o)).
% 145.45/21.01 thf(func_def_24, type, causesProposition_THFTYPE_IoooI: ($o > $o > $o)).
% 145.45/21.01 thf(func_def_25, type, causesSubclass_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_26, type, causes_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_28, type, closedOn_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_29, type, color_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_30, type, completelyFills_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_31, type, component_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_32, type, conclusion_THFTYPE_IoooI: ($o > $o > $o)).
% 145.45/21.01 thf(func_def_33, type, conditionalProbability_THFTYPE_IooioI: ($o > $o > $i > $o)).
% 145.45/21.01 thf(func_def_34, type, confersNorm_THFTYPE_IioioI: ($i > $o > $i > $o)).
% 145.45/21.01 thf(func_def_35, type, confersObligation_THFTYPE_IoiioI: ($o > $i > $i > $o)).
% 145.45/21.01 thf(func_def_36, type, confersRight_THFTYPE_IoiioI: ($o > $i > $i > $o)).
% 145.45/21.01 thf(func_def_37, type, connectedEngineeringComponents_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_38, type, connected_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_39, type, connectsEngineeringComponents_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 145.45/21.01 thf(func_def_40, type, connects_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 145.45/21.01 thf(func_def_41, type, considers_THFTYPE_IiooI: ($i > $o > $o)).
% 145.45/21.01 thf(func_def_42, type, consistent_THFTYPE_IoooI: ($o > $o > $o)).
% 145.45/21.01 thf(func_def_43, type, containsInformation_THFTYPE_IiooI: ($i > $o > $o)).
% 145.45/21.01 thf(func_def_44, type, contains_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_45, type, contraryAttribute_THFTYPE_IiiiioI: ($i > $i > $i > $i > $o)).
% 145.45/21.01 thf(func_def_46, type, contraryAttribute_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_47, type, contraryAttribute_THFTYPE_IioI: ($i > $o)).
% 145.45/21.01 thf(func_def_48, type, contraryAttribute_THFTYPE_IoooI: ($o > $o > $o)).
% 145.45/21.01 thf(func_def_49, type, cooccur_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_50, type, copy_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_51, type, crosses_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_52, type, date_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_53, type, daughter_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_54, type, decreasesLikelihood_THFTYPE_IoooI: ($o > $o > $o)).
% 145.45/21.01 thf(func_def_55, type, deprivesNorm_THFTYPE_IioioI: ($i > $o > $i > $o)).
% 145.45/21.01 thf(func_def_56, type, depth_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 145.45/21.01 thf(func_def_57, type, desires_THFTYPE_IiooI: ($i > $o > $o)).
% 145.45/21.01 thf(func_def_58, type, destination_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_59, type, developmentalForm_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_60, type, diameter_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_61, type, direction_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_62, type, disjointDecomposition_THFTYPE_IiiiiiioI: ($i > $i > $i > $i > $i > $i > $o)).
% 145.45/21.01 thf(func_def_63, type, disjointDecomposition_THFTYPE_IiiiiioI: ($i > $i > $i > $i > $i > $o)).
% 145.45/21.01 thf(func_def_64, type, disjointDecomposition_THFTYPE_IiiiioI: ($i > $i > $i > $i > $o)).
% 145.45/21.01 thf(func_def_65, type, disjointDecomposition_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 145.45/21.01 thf(func_def_66, type, disjointDecomposition_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_67, type, disjointDecomposition_THFTYPE_IioI: ($i > $o)).
% 145.45/21.01 thf(func_def_68, type, disjointRelation_THFTYPE_IIiioIIiioIoI: (($i > $i > $o) > ($i > $i > $o) > $o)).
% 145.45/21.01 thf(func_def_69, type, disjointRelation_THFTYPE_IIioIIioIoI: (($i > $o) > ($i > $o) > $o)).
% 145.45/21.01 thf(func_def_70, type, disjointRelation_THFTYPE_IIioioIIioioIoI: (($i > $o > $i > $o) > ($i > $o > $i > $o) > $o)).
% 145.45/21.01 thf(func_def_71, type, disjointRelation_THFTYPE_IIoooIIoooIoI: (($o > $o > $o) > ($o > $o > $o) > $o)).
% 145.45/21.01 thf(func_def_72, type, disjointRelation_THFTYPE_IiIiioIoI: ($i > ($i > $i > $o) > $o)).
% 145.45/21.01 thf(func_def_73, type, disjointRelation_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_74, type, disjoint_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_75, type, distance_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 145.45/21.01 thf(func_def_76, type, distributes_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_77, type, div_THFTYPE_IiiiI: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_79, type, domainSubclass_THFTYPE_IIIioIIiioIioIiioI: ((($i > $o) > ($i > $i > $o) > $i > $o) > $i > $i > $o)).
% 145.45/21.01 thf(func_def_80, type, domainSubclass_THFTYPE_IIiiiIiioI: (($i > $i > $i) > $i > $i > $o)).
% 145.45/21.01 thf(func_def_81, type, domainSubclass_THFTYPE_IIiiiiiioIiioI: (($i > $i > $i > $i > $i > $i > $o) > $i > $i > $o)).
% 145.45/21.01 thf(func_def_82, type, domainSubclass_THFTYPE_IIiioIiioI: (($i > $i > $o) > $i > $i > $o)).
% 145.45/21.01 thf(func_def_83, type, domainSubclass_THFTYPE_IIioIiioI: (($i > $o) > $i > $i > $o)).
% 145.45/21.01 thf(func_def_84, type, domainSubclass_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 145.45/21.01 thf(func_def_85, type, domain_THFTYPE_IIIIioIIiioIioIiioIiioI: (((($i > $o) > ($i > $i > $o) > $i > $o) > $i > $i > $o) > $i > $i > $o)).
% 145.45/21.01 thf(func_def_86, type, domain_THFTYPE_IIIiiIioIiioI: ((($i > $i) > $i > $o) > $i > $i > $o)).
% 145.45/21.01 thf(func_def_87, type, domain_THFTYPE_IIIiioIIiioIoIiioI: ((($i > $i > $o) > ($i > $i > $o) > $o) > $i > $i > $o)).
% 145.45/21.01 thf(func_def_88, type, domain_THFTYPE_IIIiioIioIiioI: ((($i > $i > $o) > $i > $o) > $i > $i > $o)).
% 145.45/21.01 thf(func_def_89, type, domain_THFTYPE_IIIioIIiioIioIiioI: ((($i > $o) > ($i > $i > $o) > $i > $o) > $i > $i > $o)).
% 145.45/21.01 thf(func_def_90, type, domain_THFTYPE_IIIioIiIiioI: ((($i > $o) > $i) > $i > $i > $o)).
% 145.45/21.01 thf(func_def_91, type, domain_THFTYPE_IIIioIioIiioI: ((($i > $o) > $i > $o) > $i > $i > $o)).
% 145.45/21.01 thf(func_def_92, type, domain_THFTYPE_IIIoiIioIiioI: ((($o > $i) > $i > $o) > $i > $i > $o)).
% 145.45/21.01 thf(func_def_93, type, domain_THFTYPE_IIIoioIIiioIoIiioI: ((($o > $i > $o) > ($i > $i > $o) > $o) > $i > $i > $o)).
% 145.45/21.01 thf(func_def_94, type, domain_THFTYPE_IIiiIiioI: (($i > $i) > $i > $i > $o)).
% 145.45/21.01 thf(func_def_95, type, domain_THFTYPE_IIiiiIiioI: (($i > $i > $i) > $i > $i > $o)).
% 145.45/21.01 thf(func_def_96, type, domain_THFTYPE_IIiiiiiioIiioI: (($i > $i > $i > $i > $i > $i > $o) > $i > $i > $o)).
% 145.45/21.01 thf(func_def_97, type, domain_THFTYPE_IIiiiioIiioI: (($i > $i > $i > $i > $o) > $i > $i > $o)).
% 145.45/21.01 thf(func_def_98, type, domain_THFTYPE_IIiiioIiioI: (($i > $i > $i > $o) > $i > $i > $o)).
% 145.45/21.01 thf(func_def_99, type, domain_THFTYPE_IIiioIiioI: (($i > $i > $o) > $i > $i > $o)).
% 145.45/21.01 thf(func_def_100, type, domain_THFTYPE_IIioIiioI: (($i > $o) > $i > $i > $o)).
% 145.45/21.01 thf(func_def_101, type, domain_THFTYPE_IIioioIiioI: (($i > $o > $i > $o) > $i > $i > $o)).
% 145.45/21.01 thf(func_def_102, type, domain_THFTYPE_IIiooIiioI: (($i > $o > $o) > $i > $i > $o)).
% 145.45/21.01 thf(func_def_103, type, domain_THFTYPE_IIioooIiioI: (($i > $o > $o > $o) > $i > $i > $o)).
% 145.45/21.01 thf(func_def_104, type, domain_THFTYPE_IIoiIiioI: (($o > $i) > $i > $i > $o)).
% 145.45/21.01 thf(func_def_105, type, domain_THFTYPE_IIoiioIiioI: (($o > $i > $i > $o) > $i > $i > $o)).
% 145.45/21.01 thf(func_def_106, type, domain_THFTYPE_IIoioIiioI: (($o > $i > $o) > $i > $i > $o)).
% 145.45/21.01 thf(func_def_107, type, domain_THFTYPE_IIooIiioI: (($o > $o) > $i > $i > $o)).
% 145.45/21.01 thf(func_def_108, type, domain_THFTYPE_IIooioIiioI: (($o > $o > $i > $o) > $i > $i > $o)).
% 145.45/21.01 thf(func_def_109, type, domain_THFTYPE_IIoooIiioI: (($o > $o > $o) > $i > $i > $o)).
% 145.45/21.01 thf(func_def_110, type, domain_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 145.45/21.01 thf(func_def_111, type, duration_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_112, type, during_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_113, type, earlier_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_115, type, element_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_116, type, employs_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_117, type, engineeringSubcomponent_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_118, type, entails_THFTYPE_IoooI: ($o > $o > $o)).
% 145.45/21.01 thf(func_def_120, type, equivalenceRelationOn_THFTYPE_IIiioIioI: (($i > $i > $o) > $i > $o)).
% 145.45/21.01 thf(func_def_121, type, equivalentContentClass_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_122, type, equivalentContentInstance_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_123, type, exactlyLocated_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_124, type, exhaustiveAttribute_THFTYPE_IiiiiiioI: ($i > $i > $i > $i > $i > $i > $o)).
% 145.45/21.01 thf(func_def_125, type, exhaustiveAttribute_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 145.45/21.01 thf(func_def_126, type, exhaustiveAttribute_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_127, type, exhaustiveDecomposition_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_128, type, exhaustiveDecomposition_THFTYPE_IioI: ($i > $o)).
% 145.45/21.01 thf(func_def_129, type, experiencer_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_130, type, exploits_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_131, type, expressedInLanguage_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_133, type, faces_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_134, type, familyRelation_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_135, type, father_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_136, type, fills_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_137, type, finishes_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_138, type, frequency_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_140, type, geometricDistance_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 145.45/21.01 thf(func_def_142, type, geopoliticalSubdivision_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_143, type, graphMeasure_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_144, type, graphPart_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_145, type, grasps_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_146, type, greaterThanByQuality_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 145.45/21.01 thf(func_def_147, type, greaterThanOrEqualTo_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_148, type, greaterThan_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_149, type, gt_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_150, type, gtet_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_151, type, hasPurposeForAgent_THFTYPE_IioioI: ($i > $o > $i > $o)).
% 145.45/21.01 thf(func_def_152, type, hasPurpose_THFTYPE_IiooI: ($i > $o > $o)).
% 145.45/21.01 thf(func_def_153, type, hasPurpose_THFTYPE_IooI: ($o > $o)).
% 145.45/21.01 thf(func_def_154, type, hasSkill_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_155, type, height_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_156, type, holdsDuring_THFTYPE_IiooI: ($i > $o > $o)).
% 145.45/21.01 thf(func_def_157, type, holdsObligation_THFTYPE_IoioI: ($o > $i > $o)).
% 145.45/21.01 thf(func_def_158, type, holdsRight_THFTYPE_IoioI: ($o > $i > $o)).
% 145.45/21.01 thf(func_def_159, type, hole_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_160, type, home_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_161, type, husband_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_162, type, identicalListItems_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_163, type, identityElement_THFTYPE_IIiiiIioI: (($i > $i > $i) > $i > $o)).
% 145.45/21.01 thf(func_def_164, type, identityElement_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_165, type, immediateInstance_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_166, type, immediateSubclass_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_167, type, inList_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_168, type, inScopeOfInterest_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_169, type, increasesLikelihood_THFTYPE_IoooI: ($o > $o > $o)).
% 145.45/21.01 thf(func_def_170, type, independentProbability_THFTYPE_IoooI: ($o > $o > $o)).
% 145.45/21.01 thf(func_def_171, type, inhabits_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_172, type, inhibits_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_173, type, initialList_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_174, type, initialPart_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_175, type, instance_THFTYPE_IIIIioIIiioIioIiioIioI: (((($i > $o) > ($i > $i > $o) > $i > $o) > $i > $i > $o) > $i > $o)).
% 145.45/21.01 thf(func_def_176, type, instance_THFTYPE_IIIiiIioIioI: ((($i > $i) > $i > $o) > $i > $o)).
% 145.45/21.01 thf(func_def_177, type, instance_THFTYPE_IIIiioIIiioIoIioI: ((($i > $i > $o) > ($i > $i > $o) > $o) > $i > $o)).
% 145.45/21.01 thf(func_def_178, type, instance_THFTYPE_IIIiioIioIioI: ((($i > $i > $o) > $i > $o) > $i > $o)).
% 145.45/21.01 thf(func_def_179, type, instance_THFTYPE_IIIioIIiioIioIioI: ((($i > $o) > ($i > $i > $o) > $i > $o) > $i > $o)).
% 145.45/21.01 thf(func_def_180, type, instance_THFTYPE_IIIioIiIioI: ((($i > $o) > $i) > $i > $o)).
% 145.45/21.01 thf(func_def_181, type, instance_THFTYPE_IIIioIioIioI: ((($i > $o) > $i > $o) > $i > $o)).
% 145.45/21.01 thf(func_def_182, type, instance_THFTYPE_IIIioioIiioIioI: ((($i > $o > $i > $o) > $i > $i > $o) > $i > $o)).
% 145.45/21.01 thf(func_def_183, type, instance_THFTYPE_IIIoioIIiioIoIioI: ((($o > $i > $o) > ($i > $i > $o) > $o) > $i > $o)).
% 145.45/21.01 thf(func_def_184, type, instance_THFTYPE_IIiiIioI: (($i > $i) > $i > $o)).
% 145.45/21.01 thf(func_def_185, type, instance_THFTYPE_IIiiiIioI: (($i > $i > $i) > $i > $o)).
% 145.45/21.01 thf(func_def_186, type, instance_THFTYPE_IIiiiiiioIioI: (($i > $i > $i > $i > $i > $i > $o) > $i > $o)).
% 145.45/21.01 thf(func_def_187, type, instance_THFTYPE_IIiiiioIioI: (($i > $i > $i > $i > $o) > $i > $o)).
% 145.45/21.01 thf(func_def_188, type, instance_THFTYPE_IIiiioIioI: (($i > $i > $i > $o) > $i > $o)).
% 145.45/21.01 thf(func_def_189, type, instance_THFTYPE_IIiioIioI: (($i > $i > $o) > $i > $o)).
% 145.45/21.01 thf(func_def_190, type, instance_THFTYPE_IIioIioI: (($i > $o) > $i > $o)).
% 145.45/21.01 thf(func_def_191, type, instance_THFTYPE_IIioioIioI: (($i > $o > $i > $o) > $i > $o)).
% 145.45/21.01 thf(func_def_192, type, instance_THFTYPE_IIiooIioI: (($i > $o > $o) > $i > $o)).
% 145.45/21.01 thf(func_def_193, type, instance_THFTYPE_IIioooIioI: (($i > $o > $o > $o) > $i > $o)).
% 145.45/21.01 thf(func_def_194, type, instance_THFTYPE_IIoiIioI: (($o > $i) > $i > $o)).
% 145.45/21.01 thf(func_def_195, type, instance_THFTYPE_IIoiioIioI: (($o > $i > $i > $o) > $i > $o)).
% 145.45/21.01 thf(func_def_196, type, instance_THFTYPE_IIoioIioI: (($o > $i > $o) > $i > $o)).
% 145.45/21.01 thf(func_def_197, type, instance_THFTYPE_IIooIioI: (($o > $o) > $i > $o)).
% 145.45/21.01 thf(func_def_198, type, instance_THFTYPE_IIooioIioI: (($o > $o > $i > $o) > $i > $o)).
% 145.45/21.01 thf(func_def_199, type, instance_THFTYPE_IIoooIioI: (($o > $o > $o) > $i > $o)).
% 145.45/21.01 thf(func_def_200, type, instance_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_201, type, instance_THFTYPE_IoioI: ($o > $i > $o)).
% 145.45/21.01 thf(func_def_202, type, instrument_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_203, type, interiorPart_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_204, type, inverse_THFTYPE_IIiioIIiioIoI: (($i > $i > $o) > ($i > $i > $o) > $o)).
% 145.45/21.01 thf(func_def_205, type, involvedInEvent_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_206, type, irreflexiveOn_THFTYPE_IIiioIioI: (($i > $i > $o) > $i > $o)).
% 145.45/21.01 thf(func_def_207, type, knows_THFTYPE_IiooI: ($i > $o > $o)).
% 145.45/21.01 thf(func_def_210, type, lAbsoluteValueFn_THFTYPE_IiiI: ($i > $i)).
% 145.45/21.01 thf(func_def_213, type, lAbstractionFn_THFTYPE_IiiI: ($i > $i)).
% 145.45/21.01 thf(func_def_215, type, lAdditionFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_254, type, lAssignmentFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_255, type, lAssignmentFn_THFTYPE_IiiiiI: ($i > $i > $i > $i)).
% 145.45/21.01 thf(func_def_271, type, lBackFn_THFTYPE_IiiI: ($i > $i)).
% 145.45/21.01 thf(func_def_276, type, lBeginFn_THFTYPE_IiiI: ($i > $i)).
% 145.45/21.01 thf(func_def_278, type, lBeginNodeFn_THFTYPE_IiiI: ($i > $i)).
% 145.45/21.01 thf(func_def_319, type, lCardinalityFn_THFTYPE_IIioIiI: (($i > $o) > $i)).
% 145.45/21.01 thf(func_def_320, type, lCardinalityFn_THFTYPE_IiiI: ($i > $i)).
% 145.45/21.01 thf(func_def_325, type, lCeilingFn_THFTYPE_IiiI: ($i > $i)).
% 145.45/21.01 thf(func_def_329, type, lCenterOfCircleFn_THFTYPE_IiiI: ($i > $i)).
% 145.45/21.01 thf(func_def_387, type, lCosineFn_THFTYPE_IiiI: ($i > $i)).
% 145.45/21.01 thf(func_def_398, type, lCutSetFn_THFTYPE_IiiI: ($i > $i)).
% 145.45/21.01 thf(func_def_405, type, lDayFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_436, type, lDivisionFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_446, type, lEditionFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_458, type, lEndFn_THFTYPE_IiiI: ($i > $i)).
% 145.45/21.01 thf(func_def_460, type, lEndNodeFn_THFTYPE_IiiI: ($i > $i)).
% 145.45/21.01 thf(func_def_475, type, lExponentiationFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_478, type, lExtensionFn_THFTYPE_IiiI: ($i > $i)).
% 145.45/21.01 thf(func_def_499, type, lFloorFn_THFTYPE_IiiI: ($i > $i)).
% 145.45/21.01 thf(func_def_511, type, lFrontFn_THFTYPE_IiiI: ($i > $i)).
% 145.45/21.01 thf(func_def_519, type, lFutureFn_THFTYPE_IiiI: ($i > $i)).
% 145.45/21.01 thf(func_def_534, type, lGigaFn_THFTYPE_IiiI: ($i > $i)).
% 145.45/21.01 thf(func_def_539, type, lGovernmentFn_THFTYPE_IiiI: ($i > $i)).
% 145.45/21.01 thf(func_def_551, type, lGraphPathFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_556, type, lGreatestCommonDivisorFn_THFTYPE_IiiI: ($i > $i)).
% 145.45/21.01 thf(func_def_567, type, lHoleHostFn_THFTYPE_IiiI: ($i > $i)).
% 145.45/21.01 thf(func_def_569, type, lHoleSkinFn_THFTYPE_IiiI: ($i > $i)).
% 145.45/21.01 thf(func_def_578, type, lHourFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_588, type, lImaginaryPartFn_THFTYPE_IiiI: ($i > $i)).
% 145.45/21.01 thf(func_def_590, type, lImmediateFamilyFn_THFTYPE_IiiI: ($i > $i)).
% 145.45/21.01 thf(func_def_592, type, lImmediateFutureFn_THFTYPE_IiiI: ($i > $i)).
% 145.45/21.01 thf(func_def_594, type, lImmediatePastFn_THFTYPE_IiiI: ($i > $i)).
% 145.45/21.01 thf(func_def_605, type, lInitialNodeFn_THFTYPE_IiiI: ($i > $i)).
% 145.45/21.01 thf(func_def_620, type, lIntervalFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_642, type, lKiloFn_THFTYPE_IiiI: ($i > $i)).
% 145.45/21.01 thf(func_def_653, type, lLeastCommonMultipleFn_THFTYPE_IiiI: ($i > $i)).
% 145.45/21.01 thf(func_def_667, type, lListConcatenateFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_669, type, lListFn_THFTYPE_IiiI: ($i > $i)).
% 145.45/21.01 thf(func_def_670, type, lListFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_672, type, lListLengthFn_THFTYPE_IiiI: ($i > $i)).
% 145.45/21.01 thf(func_def_674, type, lListOrderFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_686, type, lMagnitudeFn_THFTYPE_IiiI: ($i > $i)).
% 145.45/21.01 thf(func_def_702, type, lMaxFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_704, type, lMaximalWeightedPathFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_707, type, lMeasureFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_714, type, lMegaFn_THFTYPE_IiiI: ($i > $i)).
% 145.45/21.01 thf(func_def_718, type, lMereologicalDifferenceFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_720, type, lMereologicalProductFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_722, type, lMereologicalSumFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_726, type, lMicroFn_THFTYPE_IiiI: ($i > $i)).
% 145.45/21.01 thf(func_def_733, type, lMilliFn_THFTYPE_IiiI: ($i > $i)).
% 145.45/21.01 thf(func_def_736, type, lMinFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_739, type, lMinimalCutSetFn_THFTYPE_IiiI: ($i > $i)).
% 145.45/21.01 thf(func_def_741, type, lMinimalWeightedPathFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_744, type, lMinuteFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_756, type, lMonthFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_767, type, lMultiplicationFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_776, type, lNanoFn_THFTYPE_IiiI: ($i > $i)).
% 145.45/21.01 thf(func_def_836, type, lPastFn_THFTYPE_IiiI: ($i > $i)).
% 145.45/21.01 thf(func_def_839, type, lPathWeightFn_THFTYPE_IiiI: ($i > $i)).
% 145.45/21.01 thf(func_def_845, type, lPeriodicalIssueFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_858, type, lPicoFn_THFTYPE_IiiI: ($i > $i)).
% 145.45/21.01 thf(func_def_886, type, lPredecessorFn_THFTYPE_IiiI: ($i > $i)).
% 145.45/21.01 thf(func_def_890, type, lPremisesFn_THFTYPE_IooI: ($o > $o)).
% 145.45/21.01 thf(func_def_898, type, lProbabilityFn_THFTYPE_IoiI: ($o > $i)).
% 145.45/21.01 thf(func_def_906, type, lPropertyFn_THFTYPE_IiiI: ($i > $i)).
% 145.45/21.01 thf(func_def_943, type, lRealNumberFn_THFTYPE_IiiI: ($i > $i)).
% 145.45/21.01 thf(func_def_947, type, lReciprocalFn_THFTYPE_IiiI: ($i > $i)).
% 145.45/21.01 thf(func_def_950, type, lRecurrentTimeIntervalFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_960, type, lRelativeTimeFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_965, type, lRemainderFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_983, type, lRoundFn_THFTYPE_IiiI: ($i > $i)).
% 145.45/21.01 thf(func_def_990, type, lSecondFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1003, type, lSeriesVolumeFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1018, type, lSignumFn_THFTYPE_IiiI: ($i > $i)).
% 145.45/21.01 thf(func_def_1020, type, lSineFn_THFTYPE_IiiI: ($i > $i)).
% 145.45/21.01 thf(func_def_1041, type, lSpeedFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1046, type, lSquareRootFn_THFTYPE_IiiI: ($i > $i)).
% 145.45/21.01 thf(func_def_1061, type, lSubtractionFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1063, type, lSuccessorFn_THFTYPE_IiiI: ($i > $i)).
% 145.45/21.01 thf(func_def_1078, type, lTangentFn_THFTYPE_IiiI: ($i > $i)).
% 145.45/21.01 thf(func_def_1083, type, lTemporalCompositionFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1087, type, lTeraFn_THFTYPE_IiiI: ($i > $i)).
% 145.45/21.01 thf(func_def_1089, type, lTerminalNodeFn_THFTYPE_IiiI: ($i > $i)).
% 145.45/21.01 thf(func_def_1103, type, lTimeIntervalFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1138, type, lUnionFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1141, type, lUnitFn_THFTYPE_IiiI: ($i > $i)).
% 145.45/21.01 thf(func_def_1164, type, lVelocityFn_THFTYPE_IiiiiiI: ($i > $i > $i > $i > $i)).
% 145.45/21.01 thf(func_def_1188, type, lWealthFn_THFTYPE_IiiI: ($i > $i)).
% 145.45/21.01 thf(func_def_1201, type, lWhenFn_THFTYPE_IiiI: ($i > $i)).
% 145.45/21.01 thf(func_def_1203, type, lWhereFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1212, type, lYearFn_THFTYPE_IiiI: ($i > $i)).
% 145.45/21.01 thf(func_def_1216, type, larger_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1217, type, leader_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1218, type, legalRelation_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1219, type, length_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1220, type, lessThanOrEqualTo_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1221, type, lessThan_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1223, type, linearExtent_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1224, type, links_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 145.45/21.01 thf(func_def_1225, type, located_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1226, type, lt_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1227, type, ltet_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1228, type, manner_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1229, type, material_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1230, type, measure_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1231, type, meetsSpatially_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1232, type, meetsTemporally_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1233, type, meltingPoint_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1234, type, member_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1236, type, minus_THFTYPE_IiiiI: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1237, type, modalAttribute_THFTYPE_IoioI: ($o > $i > $o)).
% 145.45/21.01 thf(func_def_1238, type, monetaryValue_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1239, type, mother_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1240, type, multiplicativeFactor_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1292, type, names_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1293, type, needs_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1294, type, occupiesPosition_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 145.45/21.01 thf(func_def_1295, type, orientation_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 145.45/21.01 thf(func_def_1296, type, origin_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1297, type, overlapsPartially_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1298, type, overlapsSpatially_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1299, type, overlapsTemporally_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1300, type, parallel_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1301, type, parent_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1302, type, part_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1303, type, partialOrderingOn_THFTYPE_IIiioIioI: (($i > $i > $o) > $i > $o)).
% 145.45/21.01 thf(func_def_1304, type, partiallyFills_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1305, type, partition_THFTYPE_IiiiiiiioI: ($i > $i > $i > $i > $i > $i > $i > $o)).
% 145.45/21.01 thf(func_def_1306, type, partition_THFTYPE_IiiiiiioI: ($i > $i > $i > $i > $i > $i > $o)).
% 145.45/21.01 thf(func_def_1307, type, partition_THFTYPE_IiiiiioI: ($i > $i > $i > $i > $i > $o)).
% 145.45/21.01 thf(func_def_1308, type, partition_THFTYPE_IiiiioI: ($i > $i > $i > $i > $o)).
% 145.45/21.01 thf(func_def_1309, type, partition_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 145.45/21.01 thf(func_def_1310, type, partition_THFTYPE_IioI: ($i > $o)).
% 145.45/21.01 thf(func_def_1311, type, partlyLocated_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1312, type, pathLength_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1313, type, path_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1314, type, patient_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1315, type, patient_THFTYPE_IiooI: ($i > $o > $o)).
% 145.45/21.01 thf(func_def_1316, type, penetrates_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1317, type, piece_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1318, type, plus_THFTYPE_IiiiI: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1319, type, pointOfFigure_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1320, type, pointOfIntersection_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 145.45/21.01 thf(func_def_1321, type, possesses_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1322, type, precondition_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1323, type, prefers_THFTYPE_IioooI: ($i > $o > $o > $o)).
% 145.45/21.01 thf(func_def_1324, type, premise_THFTYPE_IoooI: ($o > $o > $o)).
% 145.45/21.01 thf(func_def_1325, type, prevents_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1326, type, properPart_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1327, type, properlyFills_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1328, type, property_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1329, type, publishes_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1330, type, radius_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1331, type, rangeSubclass_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1332, type, range_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1333, type, realization_THFTYPE_IiooI: ($i > $o > $o)).
% 145.45/21.01 thf(func_def_1334, type, refers_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1335, type, reflexiveOn_THFTYPE_IIiioIioI: (($i > $i > $o) > $i > $o)).
% 145.45/21.01 thf(func_def_1336, type, relatedEvent_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1338, type, relatedInternalConcept_THFTYPE_IIIiioIIiioIoIIiioIoI: ((($i > $i > $o) > ($i > $i > $o) > $o) > ($i > $i > $o) > $o)).
% 145.45/21.01 thf(func_def_1339, type, relatedInternalConcept_THFTYPE_IIiiIioI: (($i > $i) > $i > $o)).
% 145.45/21.01 thf(func_def_1340, type, relatedInternalConcept_THFTYPE_IIiiiIioI: (($i > $i > $i) > $i > $o)).
% 145.45/21.01 thf(func_def_1341, type, relatedInternalConcept_THFTYPE_IIiiiiiioIIiioIoI: (($i > $i > $i > $i > $i > $i > $o) > ($i > $i > $o) > $o)).
% 145.45/21.01 thf(func_def_1342, type, relatedInternalConcept_THFTYPE_IIiioIIIoiIioIoI: (($i > $i > $o) > (($o > $i) > $i > $o) > $o)).
% 145.45/21.01 thf(func_def_1343, type, relatedInternalConcept_THFTYPE_IIiioIIiiiioIoI: (($i > $i > $o) > ($i > $i > $i > $i > $o) > $o)).
% 145.45/21.01 thf(func_def_1344, type, relatedInternalConcept_THFTYPE_IIiioIIiioIoI: (($i > $i > $o) > ($i > $i > $o) > $o)).
% 145.45/21.01 thf(func_def_1345, type, relatedInternalConcept_THFTYPE_IIiioIIiooIoI: (($i > $i > $o) > ($i > $o > $o) > $o)).
% 145.45/21.01 thf(func_def_1346, type, relatedInternalConcept_THFTYPE_IIiioIioI: (($i > $i > $o) > $i > $o)).
% 145.45/21.01 thf(func_def_1347, type, relatedInternalConcept_THFTYPE_IIiooIIiioIoI: (($i > $o > $o) > ($i > $i > $o) > $o)).
% 145.45/21.01 thf(func_def_1348, type, relatedInternalConcept_THFTYPE_IIiooIIiooIoI: (($i > $o > $o) > ($i > $o > $o) > $o)).
% 145.45/21.01 thf(func_def_1349, type, relatedInternalConcept_THFTYPE_IIoiioIIoiioIoI: (($o > $i > $i > $o) > ($o > $i > $i > $o) > $o)).
% 145.45/21.01 thf(func_def_1350, type, relatedInternalConcept_THFTYPE_IIoioIIoioIoI: (($o > $i > $o) > ($o > $i > $o) > $o)).
% 145.45/21.01 thf(func_def_1351, type, relatedInternalConcept_THFTYPE_IiIiiIoI: ($i > ($i > $i) > $o)).
% 145.45/21.01 thf(func_def_1352, type, relatedInternalConcept_THFTYPE_IiIiiiIoI: ($i > ($i > $i > $i) > $o)).
% 145.45/21.01 thf(func_def_1353, type, relatedInternalConcept_THFTYPE_IiIiioIoI: ($i > ($i > $i > $o) > $o)).
% 145.45/21.01 thf(func_def_1354, type, relatedInternalConcept_THFTYPE_IiIiooIoI: ($i > ($i > $o > $o) > $o)).
% 145.45/21.01 thf(func_def_1355, type, relatedInternalConcept_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1356, type, relative_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1357, type, representsForAgent_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 145.45/21.01 thf(func_def_1358, type, representsInLanguage_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 145.45/21.01 thf(func_def_1359, type, represents_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1360, type, resource_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1361, type, result_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1362, type, sibling_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1363, type, side_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1365, type, smaller_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1366, type, son_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1367, type, spouse_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1368, type, starts_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1370, type, subAttribute_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1371, type, subCollection_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1372, type, subGraph_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1373, type, subList_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1374, type, subOrganization_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1376, type, subProcess_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1377, type, subProposition_THFTYPE_IoooI: ($o > $o > $o)).
% 145.45/21.01 thf(func_def_1378, type, subSystem_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1379, type, subclass_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1380, type, subrelation_THFTYPE_IIiiioIIiiioIoI: (($i > $i > $i > $o) > ($i > $i > $i > $o) > $o)).
% 145.45/21.01 thf(func_def_1381, type, subrelation_THFTYPE_IIiioIIIoiIioIoI: (($i > $i > $o) > (($o > $i) > $i > $o) > $o)).
% 145.45/21.01 thf(func_def_1382, type, subrelation_THFTYPE_IIiioIIIooIioIoI: (($i > $i > $o) > (($o > $o) > $i > $o) > $o)).
% 145.45/21.01 thf(func_def_1383, type, subrelation_THFTYPE_IIiioIIiioIoI: (($i > $i > $o) > ($i > $i > $o) > $o)).
% 145.45/21.01 thf(func_def_1384, type, subrelation_THFTYPE_IIiioIIiooIoI: (($i > $i > $o) > ($i > $o > $o) > $o)).
% 145.45/21.01 thf(func_def_1385, type, subrelation_THFTYPE_IIiioIioI: (($i > $i > $o) > $i > $o)).
% 145.45/21.01 thf(func_def_1386, type, subrelation_THFTYPE_IIioIIioIoI: (($i > $o) > ($i > $o) > $o)).
% 145.45/21.01 thf(func_def_1387, type, subrelation_THFTYPE_IIiooIIiioIoI: (($i > $o > $o) > ($i > $i > $o) > $o)).
% 145.45/21.01 thf(func_def_1388, type, subrelation_THFTYPE_IIoioIIiioIoI: (($o > $i > $o) > ($i > $i > $o) > $o)).
% 145.45/21.01 thf(func_def_1389, type, subrelation_THFTYPE_IIoooIIiioIoI: (($o > $o > $o) > ($i > $i > $o) > $o)).
% 145.45/21.01 thf(func_def_1390, type, subrelation_THFTYPE_IiIiioIoI: ($i > ($i > $i > $o) > $o)).
% 145.45/21.01 thf(func_def_1391, type, subrelation_THFTYPE_IiIoooIoI: ($i > ($o > $o > $o) > $o)).
% 145.45/21.01 thf(func_def_1392, type, subrelation_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1393, type, subset_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1395, type, subsumesContentClass_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1396, type, subsumesContentInstance_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1397, type, subsumesContentInstance_THFTYPE_IiooI: ($i > $o > $o)).
% 145.45/21.01 thf(func_def_1399, type, successorAttributeClosure_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1400, type, successorAttribute_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1401, type, superficialPart_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1402, type, surface_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1404, type, systemPart_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1405, type, temporalPart_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1406, type, temporallyBetweenOrEqual_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 145.45/21.01 thf(func_def_1407, type, temporallyBetween_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 145.45/21.01 thf(func_def_1408, type, time_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1409, type, times_THFTYPE_IiiiI: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1410, type, top_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1411, type, totalOrderingOn_THFTYPE_IIiioIioI: (($i > $i > $o) > $i > $o)).
% 145.45/21.01 thf(func_def_1412, type, transactionAmount_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1413, type, traverses_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1414, type, trichotomizingOn_THFTYPE_IIiioIioI: (($i > $i > $o) > $i > $o)).
% 145.45/21.01 thf(func_def_1415, type, truth_THFTYPE_IoooI: ($o > $o > $o)).
% 145.45/21.01 thf(func_def_1416, type, typicalPart_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1417, type, typicallyContainsPart_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1419, type, uses_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1420, type, valence_THFTYPE_IIiioIioI: (($i > $i > $o) > $i > $o)).
% 145.45/21.01 thf(func_def_1421, type, valence_THFTYPE_IIioIioI: (($i > $o) > $i > $o)).
% 145.45/21.01 thf(func_def_1422, type, valence_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1423, type, version_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1424, type, wants_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1425, type, wears_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1427, type, width_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1428, type, wife_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1430, type, vNOT: ($o > $o)).
% 145.45/21.01 thf(func_def_1434, type, likes_THFTYPE_IiioI: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1438, type, vAND: ($o > $o > $o)).
% 145.45/21.01 thf(func_def_1439, type, db0: !>[X0: $tType]:(X0)).
% 145.45/21.01 thf(func_def_1440, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 145.45/21.01 thf(func_def_1441, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 145.45/21.01 thf(func_def_1442, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 145.45/21.01 thf(func_def_1443, type, db1: !>[X0: $tType]:(X0)).
% 145.45/21.01 thf(func_def_1444, type, db2: !>[X0: $tType]:(X0)).
% 145.45/21.01 thf(func_def_1445, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 145.45/21.01 thf(func_def_1446, type, vIMP: ($o > $o > $o)).
% 145.45/21.01 thf(func_def_1447, type, vOR: ($o > $o > $o)).
% 145.45/21.01 thf(func_def_1448, type, sP0: ($i > $o)).
% 145.45/21.01 thf(func_def_1449, type, sP1: ($i > $o)).
% 145.45/21.01 thf(func_def_1450, type, sP2: ($i > $o)).
% 145.45/21.01 thf(func_def_1451, type, sP3: (($i > $i > $o) > $i > $i > $o)).
% 145.45/21.01 thf(func_def_1452, type, sP4: (($i > $i > $o) > $i > $i > $o)).
% 145.45/21.01 thf(func_def_1453, type, sP5: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1454, type, sK6: ($i > $i)).
% 145.45/21.01 thf(func_def_1455, type, sK7: ($i > $i)).
% 145.45/21.01 thf(func_def_1456, type, sK8: ($i > $i)).
% 145.45/21.01 thf(func_def_1457, type, sK9: ($i > $i)).
% 145.45/21.01 thf(func_def_1458, type, sK10: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1459, type, sK11: ($i > $i)).
% 145.45/21.01 thf(func_def_1460, type, sK12: ($i > $i)).
% 145.45/21.01 thf(func_def_1461, type, sK13: ($i > $i)).
% 145.45/21.01 thf(func_def_1462, type, sK14: ($i > $i)).
% 145.45/21.01 thf(func_def_1463, type, sK15: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1464, type, sK16: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1465, type, sK17: ($i > $i)).
% 145.45/21.01 thf(func_def_1466, type, sK18: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1467, type, sK19: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1468, type, sK20: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1469, type, sK21: ($i > $i)).
% 145.45/21.01 thf(func_def_1470, type, sK22: ($i > $i)).
% 145.45/21.01 thf(func_def_1471, type, sK23: ($i > $o)).
% 145.45/21.01 thf(func_def_1472, type, sK24: ($i > $i)).
% 145.45/21.01 thf(func_def_1473, type, sK25: ($i > $i > $i > $i)).
% 145.45/21.01 thf(func_def_1474, type, sK26: ($i > $i)).
% 145.45/21.01 thf(func_def_1475, type, sK27: ($i > $i)).
% 145.45/21.01 thf(func_def_1476, type, sK28: ($i > $i > $i > $i)).
% 145.45/21.01 thf(func_def_1477, type, sK29: ($i > $i)).
% 145.45/21.01 thf(func_def_1478, type, sK30: ($i > $i)).
% 145.45/21.01 thf(func_def_1479, type, sK31: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1480, type, sK32: ($i > $i)).
% 145.45/21.01 thf(func_def_1481, type, sK33: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1482, type, sK34: ($i > $i)).
% 145.45/21.01 thf(func_def_1483, type, sK35: ($i > $i)).
% 145.45/21.01 thf(func_def_1484, type, sK36: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1485, type, sK37: ($i > $i)).
% 145.45/21.01 thf(func_def_1486, type, sK38: ($i > $i)).
% 145.45/21.01 thf(func_def_1487, type, sK39: ($i > $i)).
% 145.45/21.01 thf(func_def_1488, type, sK40: ($i > $i)).
% 145.45/21.01 thf(func_def_1489, type, sK41: ($i > $i)).
% 145.45/21.01 thf(func_def_1490, type, sK42: ($i > $i)).
% 145.45/21.01 thf(func_def_1491, type, sK43: ($i > $i)).
% 145.45/21.01 thf(func_def_1492, type, sK44: ($i > $i)).
% 145.45/21.01 thf(func_def_1493, type, sK45: ($i > $i)).
% 145.45/21.01 thf(func_def_1494, type, sK46: ($i > $i)).
% 145.45/21.01 thf(func_def_1495, type, sK47: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1496, type, sK48: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1497, type, sK49: ($i > $i)).
% 145.45/21.01 thf(func_def_1498, type, sK50: ($i > $i)).
% 145.45/21.01 thf(func_def_1499, type, sK51: ($i > $i)).
% 145.45/21.01 thf(func_def_1500, type, sK52: ($i > $i)).
% 145.45/21.01 thf(func_def_1501, type, sK53: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1502, type, sK54: ($i > $i)).
% 145.45/21.01 thf(func_def_1503, type, sK55: ($i > $i)).
% 145.45/21.01 thf(func_def_1504, type, sK56: ($i > $i)).
% 145.45/21.01 thf(func_def_1505, type, sK57: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1506, type, sK58: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1507, type, sK59: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1508, type, sK60: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1509, type, sK61: ($i > $i)).
% 145.45/21.01 thf(func_def_1510, type, sK62: ($i > $i)).
% 145.45/21.01 thf(func_def_1511, type, sK63: ($i > $i)).
% 145.45/21.01 thf(func_def_1512, type, sK64: ($i > $i)).
% 145.45/21.01 thf(func_def_1513, type, sK65: ($i > $i)).
% 145.45/21.01 thf(func_def_1514, type, sK66: ($i > $i)).
% 145.45/21.01 thf(func_def_1515, type, sK67: ($i > $i > $i > $i)).
% 145.45/21.01 thf(func_def_1516, type, sK68: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1517, type, sK69: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1518, type, sK70: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1519, type, sK71: ($i > $i)).
% 145.45/21.01 thf(func_def_1520, type, sK72: ($i > $i > $i > $i)).
% 145.45/21.01 thf(func_def_1521, type, sK73: ($i > $i)).
% 145.45/21.01 thf(func_def_1522, type, sK74: ($i > $o)).
% 145.45/21.01 thf(func_def_1523, type, sK75: ($i > $i)).
% 145.45/21.01 thf(func_def_1524, type, sK76: ($i > $i)).
% 145.45/21.01 thf(func_def_1525, type, sK77: ($i > $i)).
% 145.45/21.01 thf(func_def_1526, type, sK78: ($i > $i)).
% 145.45/21.01 thf(func_def_1527, type, sK79: ($i > $i)).
% 145.45/21.01 thf(func_def_1528, type, sK80: ($i > $i)).
% 145.45/21.01 thf(func_def_1529, type, sK81: ($i > $i > $i > $i)).
% 145.45/21.01 thf(func_def_1530, type, sK82: ($i > $i)).
% 145.45/21.01 thf(func_def_1531, type, sK83: ($i > $i)).
% 145.45/21.01 thf(func_def_1532, type, sK84: ($i > $i)).
% 145.45/21.01 thf(func_def_1533, type, sK85: ($o > $i)).
% 145.45/21.01 thf(func_def_1534, type, sK86: ($i > $i)).
% 145.45/21.01 thf(func_def_1535, type, sK87: ($i > $i)).
% 145.45/21.01 thf(func_def_1536, type, sK88: ($i > $i)).
% 145.45/21.01 thf(func_def_1537, type, sK89: ($i > $i)).
% 145.45/21.01 thf(func_def_1538, type, sK90: ($i > $i)).
% 145.45/21.01 thf(func_def_1539, type, sK91: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1540, type, sK92: ($i > $i)).
% 145.45/21.01 thf(func_def_1541, type, sK93: ($i > $i)).
% 145.45/21.01 thf(func_def_1542, type, sK94: ($i > $i)).
% 145.45/21.01 thf(func_def_1543, type, sK95: ($i > $i)).
% 145.45/21.01 thf(func_def_1544, type, sK96: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1545, type, sK97: ($i > $i)).
% 145.45/21.01 thf(func_def_1546, type, sK98: ($i > $i)).
% 145.45/21.01 thf(func_def_1547, type, sK99: ($i > $i > $i > $i > $i > $i)).
% 145.45/21.01 thf(func_def_1548, type, sK100: ($i > $i > $i > $i > $i)).
% 145.45/21.01 thf(func_def_1549, type, sK101: ($i > $i)).
% 145.45/21.01 thf(func_def_1550, type, sK102: ($i > $i)).
% 145.45/21.01 thf(func_def_1551, type, sK103: ($i > $i)).
% 145.45/21.01 thf(func_def_1552, type, sK104: ($i > $i)).
% 145.45/21.01 thf(func_def_1553, type, sK105: ($i > $i)).
% 145.45/21.01 thf(func_def_1554, type, sK106: ($i > $i)).
% 145.45/21.01 thf(func_def_1555, type, sK107: ($i > $i)).
% 145.45/21.01 thf(func_def_1556, type, sK108: ($i > $i)).
% 145.45/21.01 thf(func_def_1557, type, sK109: ($i > $i)).
% 145.45/21.01 thf(func_def_1558, type, sK110: ($i > $i > $i > $i > $i)).
% 145.45/21.01 thf(func_def_1559, type, sK111: ($i > $i)).
% 145.45/21.01 thf(func_def_1560, type, sK112: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1561, type, sK113: ($i > $o)).
% 145.45/21.01 thf(func_def_1562, type, sK114: ($i > $i)).
% 145.45/21.01 thf(func_def_1563, type, sK115: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1564, type, sK116: ($i > $i)).
% 145.45/21.01 thf(func_def_1565, type, sK117: ($i > $i)).
% 145.45/21.01 thf(func_def_1566, type, sK118: ($i > $i)).
% 145.45/21.01 thf(func_def_1567, type, sK119: ($i > $i)).
% 145.45/21.01 thf(func_def_1568, type, sK120: ($i > $i > $i > $i)).
% 145.45/21.01 thf(func_def_1569, type, sK121: ($i > $i)).
% 145.45/21.01 thf(func_def_1570, type, sK122: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1571, type, sK123: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1572, type, sK124: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1573, type, sK125: ($i > $i)).
% 145.45/21.01 thf(func_def_1574, type, sK126: ($i > $i > $i > $i)).
% 145.45/21.01 thf(func_def_1575, type, sK127: ($i > $i > $i > $i)).
% 145.45/21.01 thf(func_def_1576, type, sK128: ($i > $i)).
% 145.45/21.01 thf(func_def_1577, type, sK129: ($i > $i > $i > $i)).
% 145.45/21.01 thf(func_def_1578, type, sK130: ($i > $i)).
% 145.45/21.01 thf(func_def_1579, type, sK131: ($i > $i)).
% 145.45/21.01 thf(func_def_1580, type, sK132: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1581, type, sK133: ($i > $i > $i > $i)).
% 145.45/21.01 thf(func_def_1582, type, sK134: ($i > $i > $i > $i)).
% 145.45/21.01 thf(func_def_1583, type, sK135: ($i > $i)).
% 145.45/21.01 thf(func_def_1584, type, sK136: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1585, type, sK137: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1586, type, sK138: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1587, type, sK139: ($i > $i)).
% 145.45/21.01 thf(func_def_1588, type, sK140: ($i > $i > $i > $i)).
% 145.45/21.01 thf(func_def_1589, type, sK141: ($i > $i)).
% 145.45/21.01 thf(func_def_1590, type, sK142: ($i > $i)).
% 145.45/21.01 thf(func_def_1591, type, sK143: ($i > $i)).
% 145.45/21.01 thf(func_def_1592, type, sK144: ($i > $i)).
% 145.45/21.01 thf(func_def_1593, type, sK145: ($i > $i)).
% 145.45/21.01 thf(func_def_1594, type, sK146: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1595, type, sK147: ($i > $i)).
% 145.45/21.01 thf(func_def_1596, type, sK148: ($i > ($i > $i > $o) > $i)).
% 145.45/21.01 thf(func_def_1597, type, sK149: ($i > ($i > $i > $o) > $i)).
% 145.45/21.01 thf(func_def_1598, type, sK150: ($i > ($i > $i > $o) > $i)).
% 145.45/21.01 thf(func_def_1599, type, sK151: ($i > ($i > $i > $o) > $i)).
% 145.45/21.01 thf(func_def_1600, type, sK152: ($i > ($i > $i > $o) > $i)).
% 145.45/21.01 thf(func_def_1601, type, sK153: ($i > $i)).
% 145.45/21.01 thf(func_def_1602, type, sK154: ($i > $i)).
% 145.45/21.01 thf(func_def_1603, type, sK155: ($i > $i)).
% 145.45/21.01 thf(func_def_1604, type, sK156: ($i > $i)).
% 145.45/21.01 thf(func_def_1605, type, sK157: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1606, type, sK158: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1607, type, sK159: ($i > $i)).
% 145.45/21.01 thf(func_def_1608, type, sK160: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1609, type, sK161: (($i > $i > $o) > $i)).
% 145.45/21.01 thf(func_def_1610, type, sK162: (($i > $i > $o) > $i)).
% 145.45/21.01 thf(func_def_1611, type, sK163: (($i > $i > $o) > $i)).
% 145.45/21.01 thf(func_def_1612, type, sK164: ($i > $i)).
% 145.45/21.01 thf(func_def_1613, type, sK165: ($i > $i)).
% 145.45/21.01 thf(func_def_1614, type, sK166: ($i > $i)).
% 145.45/21.01 thf(func_def_1615, type, sK167: ($i > $i)).
% 145.45/21.01 thf(func_def_1616, type, sK168: ($i > $i)).
% 145.45/21.01 thf(func_def_1617, type, sK169: ($i > $i)).
% 145.45/21.01 thf(func_def_1618, type, sK170: ($i > $i)).
% 145.45/21.01 thf(func_def_1619, type, sK171: ($i > $i)).
% 145.45/21.01 thf(func_def_1620, type, sK172: ($i > $i)).
% 145.45/21.01 thf(func_def_1621, type, sK173: ($i > $i)).
% 145.45/21.01 thf(func_def_1622, type, sK174: ($i > $i)).
% 145.45/21.01 thf(func_def_1623, type, sK175: ($i > $i)).
% 145.45/21.01 thf(func_def_1624, type, sK176: ($i > $i)).
% 145.45/21.01 thf(func_def_1625, type, sK177: ($i > $i)).
% 145.45/21.01 thf(func_def_1626, type, sK178: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1627, type, sK179: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1628, type, sK180: ($i > $i)).
% 145.45/21.01 thf(func_def_1629, type, sK181: ($i > $i)).
% 145.45/21.01 thf(func_def_1630, type, sK182: ($i > $i)).
% 145.45/21.01 thf(func_def_1631, type, sK183: ($i > $i)).
% 145.45/21.01 thf(func_def_1632, type, sK184: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1633, type, sK185: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1634, type, sK186: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1635, type, sK187: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1636, type, sK188: ($i > $i)).
% 145.45/21.01 thf(func_def_1637, type, sK189: ($o > $i > $i > $i)).
% 145.45/21.01 thf(func_def_1638, type, sK190: ($o > $i > $i > $i)).
% 145.45/21.01 thf(func_def_1639, type, sK191: ($o > $i > $i > $i)).
% 145.45/21.01 thf(func_def_1640, type, sK192: ($i > $i)).
% 145.45/21.01 thf(func_def_1641, type, sK193: ($i > $i)).
% 145.45/21.01 thf(func_def_1642, type, sK194: ($i > $i)).
% 145.45/21.01 thf(func_def_1643, type, sK195: ($i > $i)).
% 145.45/21.01 thf(func_def_1644, type, sK196: ($i > $i)).
% 145.45/21.01 thf(func_def_1645, type, sK197: ($i > $i)).
% 145.45/21.01 thf(func_def_1646, type, sK198: ($i > $i)).
% 145.45/21.01 thf(func_def_1647, type, sK199: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1648, type, sK200: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1649, type, sK201: ($i > $i > $i > $i)).
% 145.45/21.01 thf(func_def_1650, type, sK202: (($i > $i > $o) > $i)).
% 145.45/21.01 thf(func_def_1651, type, sK203: ($i > $i)).
% 145.45/21.01 thf(func_def_1652, type, sK204: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1653, type, sK205: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1654, type, sK206: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1655, type, sK207: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1656, type, sK208: ($i > $i)).
% 145.45/21.01 thf(func_def_1657, type, sK209: ($i > $i > $i > $i)).
% 145.45/21.01 thf(func_def_1658, type, sK210: ($i > $i > $i > $i)).
% 145.45/21.01 thf(func_def_1659, type, sK211: ($i > $i)).
% 145.45/21.01 thf(func_def_1660, type, sK212: ($i > $i)).
% 145.45/21.01 thf(func_def_1661, type, sK213: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1662, type, sK214: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1663, type, sK215: ($o > $i > $i)).
% 145.45/21.01 thf(func_def_1664, type, sK216: ($i > $i)).
% 145.45/21.01 thf(func_def_1665, type, sK217: ($i > $i)).
% 145.45/21.01 thf(func_def_1666, type, sK218: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1667, type, sK219: ($i > $i)).
% 145.45/21.01 thf(func_def_1668, type, sK220: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1669, type, sK221: ($i > $i > $i > $i)).
% 145.45/21.01 thf(func_def_1670, type, sK222: ($i > $i)).
% 145.45/21.01 thf(func_def_1671, type, sK223: ($i > $i)).
% 145.45/21.01 thf(func_def_1672, type, sK224: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1673, type, sK225: ($i > $i)).
% 145.45/21.01 thf(func_def_1674, type, sK226: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1675, type, sK227: ($i > $i > $i > $i)).
% 145.45/21.01 thf(func_def_1676, type, sK228: ($i > $i > $i > $i)).
% 145.45/21.01 thf(func_def_1677, type, sK229: ($i > $i)).
% 145.45/21.01 thf(func_def_1678, type, sK230: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1679, type, sK231: ($i > $i)).
% 145.45/21.01 thf(func_def_1680, type, sK232: ($i > $i)).
% 145.45/21.01 thf(func_def_1681, type, sK233: ($i > $i)).
% 145.45/21.01 thf(func_def_1682, type, sK234: ($i > $i)).
% 145.45/21.01 thf(func_def_1683, type, sK235: ($i > $i)).
% 145.45/21.01 thf(func_def_1684, type, sK236: ($i > $i)).
% 145.45/21.01 thf(func_def_1685, type, sK237: ($i > $i)).
% 145.45/21.01 thf(func_def_1686, type, sK238: ($i > $i)).
% 145.45/21.01 thf(func_def_1687, type, sK239: ($i > $i)).
% 145.45/21.01 thf(func_def_1688, type, sK240: ($i > $i)).
% 145.45/21.01 thf(func_def_1689, type, sK241: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1690, type, sK242: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1691, type, sK243: ($i > $i)).
% 145.45/21.01 thf(func_def_1692, type, sK244: ($i > $i)).
% 145.45/21.01 thf(func_def_1693, type, sK245: ($i > $i)).
% 145.45/21.01 thf(func_def_1694, type, sK246: ($i > $i)).
% 145.45/21.01 thf(func_def_1695, type, sK247: ($i > $i)).
% 145.45/21.01 thf(func_def_1696, type, sK248: ($o > $i > $i)).
% 145.45/21.01 thf(func_def_1697, type, sK249: ($i > $i)).
% 145.45/21.01 thf(func_def_1698, type, sK250: ($i > $i)).
% 145.45/21.01 thf(func_def_1699, type, sK251: ($i > $i)).
% 145.45/21.01 thf(func_def_1700, type, sK252: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1701, type, sK253: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1702, type, sK254: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1703, type, sK255: ($i > $i > $i > $o)).
% 145.45/21.01 thf(func_def_1704, type, sK256: ($i > $i > $i > $i > $o)).
% 145.45/21.01 thf(func_def_1705, type, sK257: ($i > $i)).
% 145.45/21.01 thf(func_def_1706, type, sK258: ($i > $i)).
% 145.45/21.01 thf(func_def_1707, type, sK259: ($i > $i)).
% 145.45/21.01 thf(func_def_1708, type, sK260: ($i > $i > $i > $i)).
% 145.45/21.01 thf(func_def_1709, type, sK261: ($i > $i > $i > $i)).
% 145.45/21.01 thf(func_def_1710, type, sK262: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1711, type, sK263: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1712, type, sK264: ($i > $i)).
% 145.45/21.01 thf(func_def_1713, type, sK265: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1714, type, sK266: ($i > $i)).
% 145.45/21.01 thf(func_def_1715, type, sK267: ($i > $i)).
% 145.45/21.01 thf(func_def_1716, type, sK268: ($i > $i)).
% 145.45/21.01 thf(func_def_1717, type, sK269: ($i > $i)).
% 145.45/21.01 thf(func_def_1718, type, sK270: ($i > $i)).
% 145.45/21.01 thf(func_def_1719, type, sK271: ($i > $i)).
% 145.45/21.01 thf(func_def_1720, type, sK272: ($i > $i)).
% 145.45/21.01 thf(func_def_1721, type, sK273: ($i > $i)).
% 145.45/21.01 thf(func_def_1722, type, sK274: ($i > $i)).
% 145.45/21.01 thf(func_def_1723, type, sK275: ($i > $i > $i > $i)).
% 145.45/21.01 thf(func_def_1724, type, sK276: ($i > $i)).
% 145.45/21.01 thf(func_def_1725, type, sK277: ($i > $i)).
% 145.45/21.01 thf(func_def_1726, type, sK278: ($i > $i)).
% 145.45/21.01 thf(func_def_1727, type, sK279: ($i > $i)).
% 145.45/21.01 thf(func_def_1728, type, sK280: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1729, type, sK281: ($i > $i)).
% 145.45/21.01 thf(func_def_1730, type, sK282: ($i > $i)).
% 145.45/21.01 thf(func_def_1731, type, sK283: ($i > $i)).
% 145.45/21.01 thf(func_def_1732, type, sK284: (($i > $i > $o) > $i)).
% 145.45/21.01 thf(func_def_1733, type, sK285: (($i > $i > $o) > $i)).
% 145.45/21.01 thf(func_def_1734, type, sK286: ($i > $i)).
% 145.45/21.01 thf(func_def_1735, type, sK287: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1736, type, sK288: ($i > $i)).
% 145.45/21.01 thf(func_def_1737, type, sK289: ($i > $i)).
% 145.45/21.01 thf(func_def_1738, type, sK290: ($i > $i)).
% 145.45/21.01 thf(func_def_1739, type, sK291: ($i > $i)).
% 145.45/21.01 thf(func_def_1740, type, sK292: ($i > $i)).
% 145.45/21.01 thf(func_def_1741, type, sK293: ($i > $i)).
% 145.45/21.01 thf(func_def_1742, type, sK294: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1743, type, sK295: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1744, type, sK296: ($i > $i)).
% 145.45/21.01 thf(func_def_1745, type, sK297: ($i > $i)).
% 145.45/21.01 thf(func_def_1746, type, sK298: ($i > $i)).
% 145.45/21.01 thf(func_def_1747, type, sK299: ($i > $i)).
% 145.45/21.01 thf(func_def_1748, type, sK300: ($i > $i)).
% 145.45/21.01 thf(func_def_1749, type, sK301: ($i > $i)).
% 145.45/21.01 thf(func_def_1750, type, sK302: ($i > $i)).
% 145.45/21.01 thf(func_def_1751, type, sK303: ($i > $i > $i > $i)).
% 145.45/21.01 thf(func_def_1752, type, sK304: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1753, type, sK305: ($i > $o)).
% 145.45/21.01 thf(func_def_1754, type, sK306: ($i > $i > $i > $i)).
% 145.45/21.01 thf(func_def_1755, type, sK307: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1756, type, sK308: ($i > $i)).
% 145.45/21.01 thf(func_def_1757, type, sK309: ($i > $i)).
% 145.45/21.01 thf(func_def_1758, type, sK310: ($i > $i)).
% 145.45/21.01 thf(func_def_1759, type, sK311: (($i > $i > $o) > $i)).
% 145.45/21.01 thf(func_def_1760, type, sK312: (($i > $i > $o) > $i)).
% 145.45/21.01 thf(func_def_1761, type, sK313: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1762, type, sK314: ($i > $o)).
% 145.45/21.01 thf(func_def_1763, type, sK315: ($i > $i)).
% 145.45/21.01 thf(func_def_1764, type, sK316: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1765, type, sK317: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1766, type, sK318: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1767, type, sK319: ($i > $i)).
% 145.45/21.01 thf(func_def_1768, type, sK320: ($i > $i)).
% 145.45/21.01 thf(func_def_1769, type, sK321: ($i > $o)).
% 145.45/21.01 thf(func_def_1770, type, sK322: ($i > $i)).
% 145.45/21.01 thf(func_def_1771, type, sK323: ($i > $i)).
% 145.45/21.01 thf(func_def_1772, type, sK324: ($i > $o)).
% 145.45/21.01 thf(func_def_1773, type, sK325: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1774, type, sK326: ($i > $i)).
% 145.45/21.01 thf(func_def_1775, type, sK327: ($i > $o)).
% 145.45/21.01 thf(func_def_1776, type, sK328: ($i > $i)).
% 145.45/21.01 thf(func_def_1777, type, sK329: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1778, type, sK330: ($i > $i)).
% 145.45/21.01 thf(func_def_1779, type, sK331: ($i > $i)).
% 145.45/21.01 thf(func_def_1780, type, sK332: ($i > $i)).
% 145.45/21.01 thf(func_def_1781, type, sK333: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1782, type, sK334: ($i > $i > $i > $i)).
% 145.45/21.01 thf(func_def_1783, type, sK335: ($i > $i > $i > $i)).
% 145.45/21.01 thf(func_def_1784, type, sK336: ($i > $i)).
% 145.45/21.01 thf(func_def_1785, type, sK337: ($i > $i)).
% 145.45/21.01 thf(func_def_1786, type, sK338: ($i > $i)).
% 145.45/21.01 thf(func_def_1787, type, sK339: ($i > $i)).
% 145.45/21.01 thf(func_def_1788, type, sK340: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1789, type, sK341: ($i > $i)).
% 145.45/21.01 thf(func_def_1790, type, sK342: ($i > $i)).
% 145.45/21.01 thf(func_def_1791, type, sK343: ($i > $i)).
% 145.45/21.01 thf(func_def_1792, type, sK344: ($i > $i)).
% 145.45/21.01 thf(func_def_1793, type, sK345: ($i > $i)).
% 145.45/21.01 thf(func_def_1794, type, sK346: ($i > $i)).
% 145.45/21.01 thf(func_def_1795, type, sK347: ($i > $i)).
% 145.45/21.01 thf(func_def_1796, type, sK348: ($i > $i)).
% 145.45/21.01 thf(func_def_1797, type, sK349: ($i > $i)).
% 145.45/21.01 thf(func_def_1798, type, sK350: ($i > $i)).
% 145.45/21.01 thf(func_def_1799, type, sK351: ($i > $o)).
% 145.45/21.01 thf(func_def_1800, type, sK352: ($i > $i)).
% 145.45/21.01 thf(func_def_1801, type, sK353: ($i > $i > $i > $i)).
% 145.45/21.01 thf(func_def_1802, type, sK354: ($i > $i > $i > $i)).
% 145.45/21.01 thf(func_def_1803, type, sK355: ($i > $i)).
% 145.45/21.01 thf(func_def_1804, type, sK356: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1805, type, sK357: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1806, type, sK358: ($i > $i)).
% 145.45/21.01 thf(func_def_1807, type, sK359: ($i > $i)).
% 145.45/21.01 thf(func_def_1808, type, sK360: ($i > $i)).
% 145.45/21.01 thf(func_def_1809, type, sK361: ($i > $i)).
% 145.45/21.01 thf(func_def_1810, type, sK362: ($i > $i)).
% 145.45/21.01 thf(func_def_1811, type, sK363: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1812, type, sK364: ($i > $i)).
% 145.45/21.01 thf(func_def_1813, type, sK365: ($i > $i)).
% 145.45/21.01 thf(func_def_1814, type, sK366: ($i > $i)).
% 145.45/21.01 thf(func_def_1815, type, sK367: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1816, type, sK368: (($i > $i > $o) > $i)).
% 145.45/21.01 thf(func_def_1817, type, sK369: (($i > $i > $o) > $i)).
% 145.45/21.01 thf(func_def_1818, type, sK370: ($i > $i)).
% 145.45/21.01 thf(func_def_1819, type, sK371: ($i > $i)).
% 145.45/21.01 thf(func_def_1820, type, sK372: ($i > $o)).
% 145.45/21.01 thf(func_def_1821, type, sK373: ($i > $i)).
% 145.45/21.01 thf(func_def_1822, type, sK374: ($i > $i > $o)).
% 145.45/21.01 thf(func_def_1823, type, sK375: ($i > $i)).
% 145.45/21.01 thf(func_def_1824, type, sK376: ($i > $i)).
% 145.45/21.01 thf(func_def_1825, type, sK377: ($i > $i)).
% 145.45/21.01 thf(func_def_1826, type, sK378: ($i > $i)).
% 145.45/21.01 thf(func_def_1827, type, sK379: ($i > $i)).
% 145.45/21.01 thf(func_def_1828, type, sK380: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1829, type, sK381: ($i > $i)).
% 145.45/21.01 thf(func_def_1830, type, sK382: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1831, type, sK383: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1832, type, sK384: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1833, type, sK385: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1834, type, sK386: ($i > $i)).
% 145.45/21.01 thf(func_def_1835, type, sK387: ($i > $i)).
% 145.45/21.01 thf(func_def_1836, type, sK388: ($i > $i)).
% 145.45/21.01 thf(func_def_1837, type, sK389: ($i > $i)).
% 145.45/21.01 thf(func_def_1838, type, sK390: ($i > $i)).
% 145.45/21.01 thf(func_def_1839, type, sK391: ($i > $i)).
% 145.45/21.01 thf(func_def_1840, type, sK392: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1841, type, sK393: ($i > $i > $i > $i)).
% 145.45/21.01 thf(func_def_1842, type, sK394: ($i > $i > $i > $i)).
% 145.45/21.01 thf(func_def_1844, type, sK396: ($i > $i)).
% 145.45/21.01 thf(func_def_1845, type, sK397: (($i > $i > $o) > $i)).
% 145.45/21.01 thf(func_def_1846, type, sK398: (($i > $i > $o) > $i)).
% 145.45/21.01 thf(func_def_1847, type, sK399: (($i > $i > $o) > $i)).
% 145.45/21.01 thf(func_def_1848, type, sK400: ($i > $i)).
% 145.45/21.01 thf(func_def_1849, type, sK401: ($i > $i)).
% 145.45/21.01 thf(func_def_1850, type, sK402: ($i > $i)).
% 145.45/21.01 thf(func_def_1851, type, sK403: ($i > $i)).
% 145.45/21.01 thf(func_def_1852, type, sK404: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1853, type, sK405: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1854, type, sK406: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1855, type, sK407: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1856, type, sK408: ($o > $o > $i)).
% 145.45/21.01 thf(func_def_1857, type, sK409: ($o > $o > $i)).
% 145.45/21.01 thf(func_def_1858, type, sK410: ($i > $i)).
% 145.45/21.01 thf(func_def_1859, type, sK411: ($i > $o)).
% 145.45/21.01 thf(func_def_1860, type, sK412: ($i > $o)).
% 145.45/21.01 thf(func_def_1861, type, sK413: ($i > $i)).
% 145.45/21.01 thf(func_def_1862, type, sK414: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1863, type, sK415: ($i > $o)).
% 145.45/21.01 thf(func_def_1864, type, sK416: ($i > $i)).
% 145.45/21.01 thf(func_def_1865, type, sK417: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1866, type, sK418: ($i > $i)).
% 145.45/21.01 thf(func_def_1867, type, sK419: ($i > $i)).
% 145.45/21.01 thf(func_def_1868, type, sK420: ($i > $i)).
% 145.45/21.01 thf(func_def_1869, type, sK421: ($i > $i)).
% 145.45/21.01 thf(func_def_1870, type, sK422: ($i > $o)).
% 145.45/21.01 thf(func_def_1871, type, sK423: ($i > $i)).
% 145.45/21.01 thf(func_def_1872, type, sK424: ($i > $i)).
% 145.45/21.01 thf(func_def_1873, type, sK425: ($i > $i)).
% 145.45/21.01 thf(func_def_1874, type, sK426: ($i > $i)).
% 145.45/21.01 thf(func_def_1875, type, sK427: ($i > $i)).
% 145.45/21.01 thf(func_def_1876, type, sK428: ($i > $i)).
% 145.45/21.01 thf(func_def_1877, type, sK429: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1878, type, sK430: ($o > $i > $i)).
% 145.45/21.01 thf(func_def_1879, type, sK431: ($i > $i)).
% 145.45/21.01 thf(func_def_1880, type, sK432: ($i > $i)).
% 145.45/21.01 thf(func_def_1881, type, sK433: ($i > $o)).
% 145.45/21.01 thf(func_def_1882, type, sK434: ($i > $o > $i)).
% 145.45/21.01 thf(func_def_1883, type, sK435: ($i > $i)).
% 145.45/21.01 thf(func_def_1884, type, sK436: ($i > $i)).
% 145.45/21.01 thf(func_def_1885, type, sK437: ($i > $i)).
% 145.45/21.01 thf(func_def_1886, type, sK438: ($i > $i)).
% 145.45/21.01 thf(func_def_1887, type, sK439: ($i > $i)).
% 145.45/21.01 thf(func_def_1888, type, sK440: ($i > $i)).
% 145.45/21.01 thf(func_def_1889, type, sK441: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1890, type, sK442: ($i > $i)).
% 145.45/21.01 thf(func_def_1891, type, sK443: ($i > $i)).
% 145.45/21.01 thf(func_def_1892, type, sK444: (($i > $i > $o) > $i)).
% 145.45/21.01 thf(func_def_1893, type, sK445: (($i > $i > $o) > $i)).
% 145.45/21.01 thf(func_def_1894, type, sK446: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1895, type, sK447: ($o > $i > $i)).
% 145.45/21.01 thf(func_def_1896, type, sK448: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1897, type, sK449: ($i > $i)).
% 145.45/21.01 thf(func_def_1898, type, sK450: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1899, type, sK451: ($i > $i)).
% 145.45/21.01 thf(func_def_1900, type, sK452: ($i > $i)).
% 145.45/21.01 thf(func_def_1901, type, sK453: ($i > $i)).
% 145.45/21.01 thf(func_def_1902, type, sK454: ($i > $i)).
% 145.45/21.01 thf(func_def_1903, type, sK455: ($i > $i)).
% 145.45/21.01 thf(func_def_1904, type, sK456: ($i > $i)).
% 145.45/21.01 thf(func_def_1905, type, sK457: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1906, type, sK458: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1907, type, sK459: ($i > $i)).
% 145.45/21.01 thf(func_def_1908, type, sK460: ($i > $i)).
% 145.45/21.01 thf(func_def_1909, type, sK461: ($i > $i)).
% 145.45/21.01 thf(func_def_1910, type, sK462: ($i > $i)).
% 145.45/21.01 thf(func_def_1911, type, sK463: ($i > $i)).
% 145.45/21.01 thf(func_def_1912, type, sK464: ($i > $i)).
% 145.45/21.01 thf(func_def_1913, type, sK465: ($i > $i)).
% 145.45/21.01 thf(func_def_1914, type, sK466: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1915, type, sK467: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1916, type, sK468: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1917, type, sK469: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1918, type, sK470: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1919, type, sK471: ($i > $i)).
% 145.45/21.01 thf(func_def_1920, type, sK472: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1921, type, sK473: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1922, type, sK474: ($i > $i)).
% 145.45/21.01 thf(func_def_1923, type, sK475: ($i > $i)).
% 145.45/21.01 thf(func_def_1924, type, sK476: ($i > $i)).
% 145.45/21.01 thf(func_def_1925, type, sK477: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1926, type, sK478: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1927, type, sK479: ($i > $i > $i)).
% 145.45/21.01 thf(func_def_1928, type, sK480: ($i > $i > $i)).
% 145.45/21.01 thf(f182,axiom,(
% 145.45/21.01 ! [X1 : $o,X0 : $i] : ((holdsDuring_THFTYPE_IiooI @ X0 @ (~ X1)) => (~ (holdsDuring_THFTYPE_IiooI @ X0 @ X1)))),
% 145.45/21.01 file('/export/starexec/sandbox/benchmark/Axioms/CSR005^0.ax',ax182)).
% 145.45/21.01 thf(f3578,axiom,(
% 145.45/21.01 (likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i)),
% 145.45/21.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax)).
% 145.45/21.01 thf(f3579,axiom,(
% 145.45/21.01 (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ ! [X0 : $i] : ((likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ X0) => (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ X0)))),
% 145.45/21.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax_001)).
% 145.45/21.01 thf(f3580,axiom,(
% 145.45/21.01 ! [X0 : $o,X1 : $i] : (X0 => (holdsDuring_THFTYPE_IiooI @ X1 @ X0))),
% 145.45/21.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax_002)).
% 145.45/21.01 thf(f3581,conjecture,(
% 145.45/21.01 ? [X1 : $i,X0 : $i] : (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ X1) @ (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ X0))),
% 145.45/21.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p',con)).
% 145.45/21.01 thf(f3582,negated_conjecture,(
% 145.45/21.01 ~ ? [X1 : $i,X0 : $i] : (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ X1) @ (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ X0))),
% 145.45/21.01 inference(negated_conjecture,[status(cth)],[f3581])).
% 145.45/21.01 thf(f3647,plain,(
% 145.45/21.01 ~ ? [X0 : $i,X1 : $i] : (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ X0) @ (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ X1))),
% 145.45/21.01 inference(rectify,[],[f3582])).
% 145.45/21.01 thf(f3648,plain,(
% 145.45/21.01 ~ ? [X1 : $i,X0 : $i] : (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ X0) @ (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ X1))) = $true)),
% 145.45/21.01 inference(fool_elimination,[],[f3647])).
% 145.45/21.01 thf(f4343,plain,(
% 145.45/21.01 (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ ! [X0 : $i] : ((likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ X0) => (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ X0)))),
% 145.45/21.01 inference(rectify,[],[f3579])).
% 145.45/21.01 thf(f4344,plain,(
% 145.45/21.01 ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (!! @ $i @ (^[Y0 : $i]: ((likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ Y0) => (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ Y0)))))))),
% 145.45/21.01 inference(fool_elimination,[],[f4343])).
% 145.45/21.01 thf(f4431,plain,(
% 145.45/21.01 ! [X0 : $o,X1 : $i] : (X0 => (holdsDuring_THFTYPE_IiooI @ X1 @ X0))),
% 145.45/21.01 inference(rectify,[],[f3580])).
% 145.45/21.01 thf(f4432,plain,(
% 145.45/21.01 ! [X0 : $o,X1 : $i] : (($true = X0) => (((holdsDuring_THFTYPE_IiooI @ X1 @ X0)) = $true))),
% 145.45/21.01 inference(fool_elimination,[],[f4431])).
% 145.45/21.01 thf(f8497,plain,(
% 145.45/21.01 (likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i)),
% 145.45/21.01 inference(rectify,[],[f3578])).
% 145.45/21.01 thf(f8498,plain,(
% 145.45/21.01 (((likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i)) = $true)),
% 145.45/21.01 inference(fool_elimination,[],[f8497])).
% 145.45/21.01 thf(f10095,plain,(
% 145.45/21.01 ! [X0 : $o,X1 : $i] : ((holdsDuring_THFTYPE_IiooI @ X1 @ (~ X0)) => (~ (holdsDuring_THFTYPE_IiooI @ X1 @ X0)))),
% 145.45/21.01 inference(rectify,[],[f182])).
% 145.45/21.01 thf(f10096,plain,(
% 145.45/21.01 ! [X1 : $i,X0 : $o] : ((((holdsDuring_THFTYPE_IiooI @ X1 @ (~ X0))) = $true) => ($true = ((~ (holdsDuring_THFTYPE_IiooI @ X1 @ X0)))))),
% 145.45/21.01 inference(fool_elimination,[],[f10095])).
% 145.45/21.01 thf(f11249,plain,(
% 145.45/21.01 ! [X1 : $i,X0 : $i] : (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ X0) @ (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ X1))) != $true)),
% 145.45/21.01 inference(ennf_transformation,[],[f3648])).
% 145.45/21.01 thf(f11793,plain,(
% 145.45/21.01 ! [X0 : $o,X1 : $i] : (($true = ((~ (holdsDuring_THFTYPE_IiooI @ X1 @ X0)))) | (((holdsDuring_THFTYPE_IiooI @ X1 @ (~ X0))) != $true))),
% 145.45/21.01 inference(ennf_transformation,[],[f10096])).
% 145.45/21.01 thf(f11853,plain,(
% 145.45/21.01 ! [X1 : $i,X0 : $o] : (($true != X0) | (((holdsDuring_THFTYPE_IiooI @ X1 @ X0)) = $true))),
% 145.45/21.01 inference(ennf_transformation,[],[f4432])).
% 145.45/21.01 thf(f12693,plain,(
% 145.45/21.01 ! [X0 : $i,X1 : $i] : (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ X1) @ (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ X0))) != $true)),
% 145.45/21.01 inference(rectify,[],[f11249])).
% 145.45/21.01 thf(f12826,plain,(
% 145.45/21.01 ! [X0 : $i,X1 : $o] : (($true != X1) | (((holdsDuring_THFTYPE_IiooI @ X0 @ X1)) = $true))),
% 145.45/21.01 inference(rectify,[],[f11853])).
% 145.45/21.01 thf(f12893,plain,(
% 145.45/21.01 ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (!! @ $i @ (^[Y0 : $i]: ((likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ Y0) => (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ Y0)))))))),
% 145.45/21.01 inference(cnf_transformation,[],[f4344])).
% 145.45/21.01 thf(f16327,plain,(
% 145.45/21.01 ( ! [X0 : $o,X1 : $i] : ((((holdsDuring_THFTYPE_IiooI @ X1 @ (~ X0))) != $true) | ($true = ((~ (holdsDuring_THFTYPE_IiooI @ X1 @ X0))))) )),
% 145.45/21.01 inference(cnf_transformation,[],[f11793])).
% 145.45/21.01 thf(f16543,plain,(
% 145.45/21.01 ( ! [X0 : $i,X1 : $i] : ((((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ X1) @ (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ X0))) != $true)) )),
% 145.45/21.01 inference(cnf_transformation,[],[f12693])).
% 145.45/21.01 thf(f16807,plain,(
% 145.45/21.01 (((likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i)) = $true)),
% 145.45/21.01 inference(cnf_transformation,[],[f8498])).
% 145.45/21.01 thf(f17099,plain,(
% 145.45/21.01 ( ! [X0 : $i,X1 : $o] : (($true != X1) | (((holdsDuring_THFTYPE_IiooI @ X0 @ X1)) = $true)) )),
% 145.45/21.01 inference(cnf_transformation,[],[f12826])).
% 145.45/21.01 thf(f17118,definition,(
% 145.45/21.01 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 145.45/21.01 introduced(theory,[fool_exhaustiveness_axiom])).
% 145.45/21.01 thf(f17274,plain,(
% 145.45/21.01 ( ! [X0 : $i] : ((((holdsDuring_THFTYPE_IiooI @ X0 @ $true)) = $true)) )),
% 145.45/21.01 inference(equality_resolution,[],[f17099])).
% 145.45/21.01 thf(f17619,plain,(
% 145.45/21.01 ( ! [X0 : $o,X1 : $i] : ((((holdsDuring_THFTYPE_IiooI @ X1 @ (~ X0))) != $true) | (((holdsDuring_THFTYPE_IiooI @ X1 @ X0)) = $false)) )),
% 145.45/21.01 inference(not_proxy_clausification,[],[f16327])).
% 145.45/21.01 thf(f17787,plain,(
% 145.45/21.01 ( ! [X0 : $i,X1 : $i] : ((((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ X0) @ $true)) != $true) | ($false = ((likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ X1)))) )),
% 145.45/21.01 inference(constrained_superposition,[],[f16543,f17118])).
% 145.45/21.01 thf(f17796,definition,(
% 145.45/21.01 spl481_12 <=> ! [X1 : $i] : ($false = ((likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ X1)))),
% 145.45/21.01 introduced(definition,[new_symbols(definition,[spl481_12])],[avatar_definition])).
% 145.45/21.01 thf(f17797,plain,(
% 145.45/21.01 ( ! [X1 : $i] : (($false = ((likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ X1)))) ) | ~spl481_12),
% 145.45/21.01 inference(avatar_component_clause,[],[f17796])).
% 145.45/21.01 thf(f17799,definition,(
% 145.45/21.01 spl481_13 <=> ! [X0 : $i] : (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ X0) @ $true)) != $true)),
% 145.45/21.01 introduced(definition,[new_symbols(definition,[spl481_13])],[avatar_definition])).
% 145.45/21.01 thf(f17800,plain,(
% 145.45/21.01 ( ! [X0 : $i] : ((((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ X0) @ $true)) != $true)) ) | ~spl481_13),
% 145.45/21.01 inference(avatar_component_clause,[],[f17799])).
% 145.45/21.01 thf(f17801,plain,(
% 145.45/21.01 spl481_12 | spl481_13),
% 145.45/21.01 inference(avatar_split_clause,[],[f17787,f17799,f17796])).
% 145.45/21.01 thf(f17817,plain,(
% 145.45/21.01 ( ! [X0 : $i,X1 : $o] : ((((holdsDuring_THFTYPE_IiooI @ X0 @ X1)) = $false) | (((holdsDuring_THFTYPE_IiooI @ X0 @ $true)) != $true) | (((~ X1)) = $false)) )),
% 145.45/21.01 inference(constrained_superposition,[],[f17619,f17118])).
% 145.45/21.01 thf(f17821,plain,(
% 145.45/21.01 ( ! [X0 : $i,X1 : $o] : (($true = X1) | (((holdsDuring_THFTYPE_IiooI @ X0 @ $true)) != $true) | (((holdsDuring_THFTYPE_IiooI @ X0 @ X1)) = $false)) )),
% 145.45/21.01 inference(not_proxy_clausification,[],[f17817])).
% 145.45/21.01 thf(f17824,plain,(
% 145.45/21.01 ( ! [X0 : $i,X1 : $o] : ((((holdsDuring_THFTYPE_IiooI @ X0 @ X1)) = $false) | ($true = X1)) )),
% 145.45/21.01 inference(forward_subsumption_resolution,[],[f17821,f17274])).
% 145.45/21.01 thf(f17863,plain,(
% 145.45/21.01 ($false = $true) | (((!! @ $i @ (^[Y0 : $i]: ((likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ Y0) => (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ Y0))))) = $true)),
% 145.45/21.01 inference(constrained_superposition,[],[f17824,f12893])).
% 145.45/21.01 thf(f17868,plain,(
% 145.45/21.01 ( ! [X1 : $i] : (($false = $true) | ((((^[Y0 : $i]: ((likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ Y0) => (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ Y0))) @ X1)) = $true)) )),
% 145.45/21.01 inference(pi_proxy_clausification,[],[f17863])).
% 145.45/21.01 thf(f17869,plain,(
% 145.45/21.01 ( ! [X1 : $i] : (((((^[Y0 : $i]: ((likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ Y0) => (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ Y0))) @ X1)) = $true)) )),
% 145.45/21.01 inference(trivial_inequality_removal,[],[f17868])).
% 145.45/21.01 thf(f17870,plain,(
% 145.45/21.01 ( ! [X1 : $i] : (((((likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ X1) => (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ X1))) = $true)) )),
% 145.45/21.01 inference(beta-eta_normalization,[],[f17869])).
% 145.45/21.01 thf(f17871,plain,(
% 145.45/21.01 ( ! [X1 : $i] : (($false = ((likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ X1))) | (((likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ X1)) = $true)) )),
% 145.45/21.01 inference(imp_proxy_clausification,[],[f17870])).
% 145.45/21.01 thf(f17876,plain,(
% 145.45/21.01 ( ! [X1 : $i] : (($false = $true) | ($false = ((likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ X1)))) ) | ~spl481_12),
% 145.45/21.01 inference(forward_demodulation,[],[f17871,f17797])).
% 145.45/21.01 thf(f17877,plain,(
% 145.45/21.01 ( ! [X1 : $i] : (($false = ((likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ X1)))) ) | ~spl481_12),
% 145.45/21.01 inference(trivial_inequality_removal,[],[f17876])).
% 145.45/21.01 thf(f17880,plain,(
% 145.45/21.01 ($false = $true) | ~spl481_12),
% 145.45/21.01 inference(constrained_superposition,[],[f17877,f16807])).
% 145.45/21.01 thf(f17885,plain,(
% 145.45/21.01 $false | ~spl481_12),
% 145.45/21.01 inference(trivial_inequality_removal,[],[f17880])).
% 145.45/21.01 thf(f17886,plain,(
% 145.45/21.01 ~spl481_12),
% 145.45/21.01 inference(avatar_contradiction_clause,[],[f17885])).
% 145.45/21.01 thf(f17888,plain,(
% 145.45/21.01 $false | ~spl481_13),
% 145.45/21.01 inference(forward_subsumption_resolution,[],[f17800,f17274])).
% 145.45/21.01 thf(f17889,plain,(
% 145.45/21.01 ~spl481_13),
% 145.45/21.01 inference(avatar_contradiction_clause,[],[f17888])).
% 145.45/21.01 cnf(s7, plain, spl481_12 | spl481_13, inference(sat_conversion,[],[f17801])).
% 145.45/21.01 cnf(s9, plain, ~spl481_12, inference(sat_conversion,[],[f17886])).
% 145.45/21.01 cnf(s10, plain, ~spl481_13, inference(sat_conversion,[],[f17889])).
% 145.45/21.01 cnf(s11, plain, $false, inference(rat,[],[s7,s10,s9])).
% 145.45/21.01 thf(f17890,plain,(
% 145.45/21.01 $false),
% 145.45/21.01 inference(avatar_sat_refutation,[],[s11])).
% 145.45/21.01 % SZS output end Proof for theBenchmark
% 145.45/21.01 % (699391)------------------------------
% 145.45/21.01 % (699391)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 145.45/21.01 % (699391)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.45/21.01 % (699391)CaDiCaL version: 2.1.3
% 145.45/21.01 % (699391)Termination reason: Refutation
% 145.45/21.01 % (699391)Time elapsed: 0.321 s
% 145.45/21.01 % (699391)Peak memory usage: 23 MB
% 145.45/21.01 % (699391)Instructions burned: 734 (million)
% 145.45/21.01 % (699095)Success in time 20.784 s
% 145.45/21.01 % Vampire exiting
%------------------------------------------------------------------------------