%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR149^3 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n007.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:22 AM UTC 2026
% Result : Theorem 81.90s 20.61s
% Output : Refutation 81.90s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR149^3 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.19 % Computer : n007.cluster.edu
% 0.11/0.19 % Model : x86_64 x86_64
% 0.11/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.19 % Memory : 8046.5625MB
% 0.11/0.19 % OS : Linux 6.8.0-71-generic
% 0.11/0.19 % CPULimit : 300
% 0.11/0.19 % WCLimit : 300
% 0.11/0.19 % DateTime : Tue Sep 29 17:55:26 UTC 2026
% 0.11/0.19 % CPUTime :
% 0.11/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.22 Running first-order model finding
% 0.11/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.14/1.53 % (3719890)Will run a generic schedule for satisfiability detection.
% 7.14/1.53 % (3719953)dis+10_1_sil=32000:sp=arity:random_seed=598808729:i=103:fgj=on_2998 on theBenchmark for (2998ds/103Mi)
% 7.14/1.53 % (3719951)% WARNING: option uhcvi not known.
% 7.14/1.53 % (3719949)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3000474013_2998 on theBenchmark for (2998ds/0Mi)
% 7.14/1.53 % (3719951)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1703745607:i=135531:add=off:rawr=on_2998 on theBenchmark for (2998ds/135531Mi)
% 7.14/1.53 % (3719952)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2433013865:i=88024:add=on:rawr=on_2998 on theBenchmark for (2998ds/88024Mi)
% 7.14/1.53 % (3719954)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2424264959:i=116_2998 on theBenchmark for (2998ds/116Mi)
% 7.14/1.53 % (3719955)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2922441212:i=131_2998 on theBenchmark for (2998ds/131Mi)
% 7.14/1.53 % (3719957)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1488979466:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2998 on theBenchmark for (2998ds/159Mi)
% 7.14/1.53 % (3719953)Instruction limit reached!
% 7.14/1.53 % (3719953)------------------------------
% 7.14/1.53 % (3719953)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.14/1.53 % (3719953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.14/1.53 % (3719953)CaDiCaL version: 2.1.3
% 7.14/1.53 % (3719953)Termination reason: Instruction limit
% 7.14/1.53 % (3719953)Termination phase: Initialization
% 7.14/1.53 % (3719953)Time elapsed: 0.024 s
% 7.14/1.53 % (3719953)Peak memory usage: 16 MB
% 7.14/1.53 % (3719953)Instructions burned: 104 (million)
% 7.14/1.53 % (3719981)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=791661850:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 7.14/1.53 % (3719954)Instruction limit reached!
% 7.14/1.53 % (3719954)------------------------------
% 7.14/1.53 % (3719954)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.14/1.53 % (3719954)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.14/1.53 % (3719954)CaDiCaL version: 2.1.3
% 7.14/1.53 % (3719954)Termination reason: Instruction limit
% 7.14/1.53 % (3719954)Termination phase: Initialization
% 7.14/1.53 % (3719954)Time elapsed: 0.048 s
% 7.14/1.53 % (3719954)Peak memory usage: 16 MB
% 7.14/1.53 % (3719954)Instructions burned: 118 (million)
% 7.14/1.53 % (3719955)Instruction limit reached!
% 7.14/1.53 % (3719955)------------------------------
% 7.14/1.53 % (3719955)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.14/1.53 % (3719955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.14/1.53 % (3719955)CaDiCaL version: 2.1.3
% 7.14/1.53 % (3719955)Termination reason: Instruction limit
% 7.14/1.53 % (3719955)Termination phase: Initialization
% 7.14/1.53 % (3719955)Time elapsed: 0.055 s
% 7.14/1.53 % (3719955)Peak memory usage: 16 MB
% 7.14/1.53 % (3719955)Instructions burned: 137 (million)
% 7.14/1.53 % (3719957)Instruction limit reached!
% 7.14/1.53 % (3719957)------------------------------
% 7.14/1.53 % (3719957)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.14/1.53 % (3719957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.14/1.53 % (3719957)CaDiCaL version: 2.1.3
% 7.14/1.53 % (3719957)Termination reason: Instruction limit
% 7.14/1.53 % (3719957)Termination phase: Property scanning
% 7.14/1.53 % (3719957)Time elapsed: 0.064 s
% 7.14/1.53 % (3719957)Peak memory usage: 16 MB
% 7.14/1.53 % (3719957)Instructions burned: 160 (million)
% 7.14/1.53 % (3719989)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2567357173:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 7.14/1.53 % (3719994)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=1990385311:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi)
% 7.14/1.53 % (3719999)ott-21_1_sil=16000:fs=off:random_seed=3788751823:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 7.14/1.53 % (3719951)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 7.14/1.53 % (3719989)Instruction limit reached!
% 7.14/1.53 % (3719989)------------------------------
% 7.14/1.53 % (3719989)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.93/3.17 % (3719989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.93/3.17 % (3719989)CaDiCaL version: 2.1.3
% 19.93/3.17 % (3719989)Termination reason: Instruction limit
% 19.93/3.17 % (3719989)Termination phase: Initialization
% 19.93/3.17 % (3719989)Time elapsed: 0.054 s
% 19.93/3.17 % (3719989)Peak memory usage: 16 MB
% 19.93/3.17 % (3719989)Instructions burned: 131 (million)
% 19.93/3.17 % (3720003)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2444511372:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 19.93/3.17 % (3719999)Instruction limit reached!
% 19.93/3.17 % (3719999)------------------------------
% 19.93/3.17 % (3719999)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.93/3.17 % (3719999)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.93/3.17 % (3719999)CaDiCaL version: 2.1.3
% 19.93/3.17 % (3719999)Termination reason: Instruction limit
% 19.93/3.17 % (3719999)Termination phase: Property scanning
% 19.93/3.17 % (3719999)Time elapsed: 0.074 s
% 19.93/3.17 % (3719999)Peak memory usage: 16 MB
% 19.93/3.17 % (3719999)Instructions burned: 182 (million)
% 19.93/3.17 % Exception at run slice level
% 19.93/3.17 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 19.93/3.17 % (3720005)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2385389953:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 19.93/3.17 % (3720006)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=224522939:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 19.93/3.17 % (3719994)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 19.93/3.17 % Exception at run slice level
% 19.93/3.17 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 19.93/3.17 % (3719951)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 19.93/3.17 % (3720027)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3407970707:i=889:ins=1_2996 on theBenchmark for (2996ds/889Mi)
% 19.93/3.17 % (3719994)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 19.93/3.17 % (3720003)Instruction limit reached!
% 19.93/3.17 % (3720003)------------------------------
% 19.93/3.17 % (3720003)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.93/3.17 % (3720003)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.93/3.17 % (3720003)CaDiCaL version: 2.1.3
% 19.93/3.17 % (3720003)Termination reason: Instruction limit
% 19.93/3.17 % (3720003)Termination phase: Property scanning
% 19.93/3.17 % (3720003)Time elapsed: 0.199 s
% 19.93/3.17 % (3720003)Peak memory usage: 19 MB
% 19.93/3.17 % (3720003)Instructions burned: 480 (million)
% 19.93/3.17 % Exception at run slice level
% 19.93/3.17 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 19.93/3.17 % (3720058)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=498601012:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi)
% 19.93/3.17 % (3719994)Instruction limit reached!
% 19.93/3.17 % (3719994)------------------------------
% 19.93/3.17 % (3719994)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.93/3.17 % (3719994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.93/3.17 % (3719994)CaDiCaL version: 2.1.3
% 19.93/3.17 % (3719994)Termination reason: Instruction limit
% 19.93/3.17 % (3719994)Termination phase: Saturation
% 19.93/3.17 % (3719994)Time elapsed: 0.293 s
% 19.93/3.17 % (3719994)Peak memory usage: 21 MB
% 19.93/3.17 % (3719994)Instructions burned: 686 (million)
% 19.93/3.17 % (3720059)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=165412662:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 19.93/3.17 % (3720061)fmb+10_1_sil=64000:random_seed=1963274471:i=22061:nm=2:gsp=on_2994 on theBenchmark for (2994ds/22061Mi)
% 19.93/3.17 % (3720006)Instruction limit reached!
% 19.93/3.17 % (3720006)------------------------------
% 19.93/3.17 % (3720006)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.93/3.17 % (3720006)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.93/3.17 % (3720006)CaDiCaL version: 2.1.3
% 19.93/3.17 % (3720006)Termination reason: Instruction limit
% 46.54/7.00 % (3720006)Termination phase: Saturation
% 46.54/7.00 % (3720006)Time elapsed: 0.270 s
% 46.54/7.00 % (3720006)Peak memory usage: 25 MB
% 46.54/7.00 % (3720006)Instructions burned: 1179 (million)
% 46.54/7.00 % (3720064)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=755069085:i=9515:nm=5_2994 on theBenchmark for (2994ds/9515Mi)
% 46.54/7.00 % (3720059)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 46.54/7.00 % (3720058)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 46.54/7.00 % Exception at run slice level
% 46.54/7.00 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 46.54/7.00 % (3720066)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=4250531129:fmbsr=1.7:i=920_2993 on theBenchmark for (2993ds/920Mi)
% 46.54/7.00 % (3720061)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 46.54/7.00 % Exception at run slice level
% 46.54/7.00 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 46.54/7.00 % (3720068)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=510450569:i=5131_2992 on theBenchmark for (2992ds/5131Mi)
% 46.54/7.00 % Exception at run slice level
% 46.54/7.00 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 46.54/7.00 % (3720070)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2690095494:i=1472:ins=7:fdi=8:gsp=on_2992 on theBenchmark for (2992ds/1472Mi)
% 46.54/7.00 % (3720068)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 46.54/7.00 % (3720058)Instruction limit reached!
% 46.54/7.00 % (3720058)------------------------------
% 46.54/7.00 % (3720058)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.54/7.00 % (3720058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.54/7.00 % (3720058)CaDiCaL version: 2.1.3
% 46.54/7.00 % (3720058)Termination reason: Instruction limit
% 46.54/7.00 % (3720058)Termination phase: Saturation
% 46.54/7.00 % (3720058)Time elapsed: 0.294 s
% 46.54/7.00 % (3720058)Peak memory usage: 22 MB
% 46.54/7.00 % (3720058)Instructions burned: 693 (million)
% 46.54/7.00 % (3720072)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3058975119:i=6324_2991 on theBenchmark for (2991ds/6324Mi)
% 46.54/7.00 % Exception at run slice level
% 46.54/7.00 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 46.54/7.00 % (3720059)Instruction limit reached!
% 46.54/7.00 % (3720059)------------------------------
% 46.54/7.00 % (3720059)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 46.54/7.00 % (3720059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.54/7.00 % (3720059)CaDiCaL version: 2.1.3
% 46.54/7.00 % (3720059)Termination reason: Instruction limit
% 46.54/7.00 % (3720059)Termination phase: Saturation
% 46.54/7.00 % (3720059)Time elapsed: 0.380 s
% 46.54/7.00 % (3720059)Peak memory usage: 25 MB
% 46.54/7.00 % (3720059)Instructions burned: 880 (million)
% 46.54/7.00 % (3720074)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1160586907:fmbsr=2.30978:i=2174_2990 on theBenchmark for (2990ds/2174Mi)
% 46.54/7.00 % (3720075)ott-2_1_sil=16000:newcnf=on:random_seed=137115195:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2990 on theBenchmark for (2990ds/869Mi)
% 46.54/7.00 % (3720070)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 46.54/7.00 % (3720070)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 46.54/7.00 % (3720075)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 46.54/7.00 % Exception at run slice level
% 46.54/7.00 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 46.54/7.00 % (3720078)ott+10_1_sil=32000:tgt=ground:random_seed=4260487152:i=5114:av=off_2989 on theBenchmark for (2989ds/5114Mi)
% 46.54/7.00 % Exception at run slice level
% 46.54/7.00 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 46.54/7.00 % (3720080)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2181276352:i=54282_2988 on theBenchmark for (2988ds/54282Mi)
% 46.54/7.00 % (3720075)Instruction limit reached!
% 46.54/7.00 % (3720075)------------------------------
% 46.54/7.00 % (3720075)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.78/13.78 % (3720075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.78/13.78 % (3720075)CaDiCaL version: 2.1.3
% 94.78/13.78 % (3720075)Termination reason: Instruction limit
% 94.78/13.78 % (3720075)Termination phase: Saturation
% 94.78/13.78 % (3720075)Time elapsed: 0.374 s
% 94.78/13.78 % (3720075)Peak memory usage: 24 MB
% 94.78/13.78 % (3720075)Instructions burned: 870 (million)
% 94.78/13.78 % (3720082)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=4139933813:i=3512:aac=none_2986 on theBenchmark for (2986ds/3512Mi)
% 94.78/13.78 % Exception at run slice level
% 94.78/13.78 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 94.78/13.78 % (3720084)dis+21_1_sil=32000:sas=cadical:random_seed=499725627:i=3773:amm=off_2986 on theBenchmark for (2986ds/3773Mi)
% 94.78/13.78 % (3720070)Instruction limit reached!
% 94.78/13.78 % (3720070)------------------------------
% 94.78/13.78 % (3720070)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.78/13.78 % (3720070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.78/13.78 % (3720070)CaDiCaL version: 2.1.3
% 94.78/13.78 % (3720070)Termination reason: Instruction limit
% 94.78/13.78 % (3720070)Termination phase: Saturation
% 94.78/13.78 % (3720070)Time elapsed: 0.683 s
% 94.78/13.78 % (3720070)Peak memory usage: 28 MB
% 94.78/13.78 % (3720070)Instructions burned: 1473 (million)
% 94.78/13.78 % (3720086)ott+11_1_sil=16000:gs=on:random_seed=989539996:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2985 on theBenchmark for (2985ds/2251Mi)
% 94.78/13.78 % (3720082)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 94.78/13.78 % (3720086)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 94.78/13.78 % (3720068)Instruction limit reached!
% 94.78/13.78 % (3720068)------------------------------
% 94.78/13.78 % (3720068)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.78/13.78 % (3720068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.78/13.78 % (3720068)CaDiCaL version: 2.1.3
% 94.78/13.78 % (3720068)Termination reason: Instruction limit
% 94.78/13.78 % (3720068)Termination phase: Saturation
% 94.78/13.78 % (3720068)Time elapsed: 1.117 s
% 94.78/13.78 % (3720068)Peak memory usage: 22 MB
% 94.78/13.78 % (3720068)Instructions burned: 5134 (million)
% 94.78/13.78 % (3720088)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=4220848149:fmbsr=1.6:i=67534_2981 on theBenchmark for (2981ds/67534Mi)
% 94.78/13.78 % Exception at run slice level
% 94.78/13.78 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 94.78/13.78 % (3720090)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3114038999:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2980 on theBenchmark for (2980ds/4591Mi)
% 94.78/13.78 % (3720086)Instruction limit reached!
% 94.78/13.78 % (3720086)------------------------------
% 94.78/13.78 % (3720086)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.78/13.78 % (3720086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.78/13.78 % (3720086)CaDiCaL version: 2.1.3
% 94.78/13.78 % (3720086)Termination reason: Instruction limit
% 94.78/13.78 % (3720086)Termination phase: Saturation
% 94.78/13.78 % (3720086)Time elapsed: 1.010 s
% 94.78/13.78 % (3720086)Peak memory usage: 27 MB
% 94.78/13.78 % (3720086)Instructions burned: 2253 (million)
% 94.78/13.78 % (3720092)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1013331582:i=29340_2974 on theBenchmark for (2974ds/29340Mi)
% 94.78/13.78 % (3720082)Instruction limit reached!
% 94.78/13.78 % (3720082)------------------------------
% 94.78/13.78 % (3720082)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 94.78/13.78 % (3720082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.78/13.78 % (3720082)CaDiCaL version: 2.1.3
% 94.78/13.78 % (3720082)Termination reason: Instruction limit
% 94.78/13.78 % (3720082)Termination phase: Saturation
% 94.78/13.78 % (3720082)Time elapsed: 1.424 s
% 94.78/13.78 % (3720082)Peak memory usage: 22 MB
% 94.78/13.78 % (3720082)Instructions burned: 3512 (million)
% 94.78/13.78 % (3720094)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3436401530:i=5211_2972 on theBenchmark for (2972ds/5211Mi)
% 94.78/13.78 % (3720084)Instruction limit reached!
% 134.67/19.37 % (3720084)------------------------------
% 134.67/19.37 % (3720084)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.67/19.37 % (3720084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.67/19.37 % (3720084)CaDiCaL version: 2.1.3
% 134.67/19.37 % (3720084)Termination reason: Instruction limit
% 134.67/19.37 % (3720084)Termination phase: Saturation
% 134.67/19.37 % (3720084)Time elapsed: 1.527 s
% 134.67/19.37 % (3720084)Peak memory usage: 23 MB
% 134.67/19.37 % (3720084)Instructions burned: 3776 (million)
% 134.67/19.37 % (3720096)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=757888957:i=5497:nm=2_2970 on theBenchmark for (2970ds/5497Mi)
% 134.67/19.37 % (3720090)Instruction limit reached!
% 134.67/19.37 % (3720090)------------------------------
% 134.67/19.37 % (3720090)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.67/19.37 % (3720090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.67/19.37 % (3720090)CaDiCaL version: 2.1.3
% 134.67/19.37 % (3720090)Termination reason: Instruction limit
% 134.67/19.37 % (3720090)Termination phase: Saturation
% 134.67/19.37 % (3720090)Time elapsed: 1.044 s
% 134.67/19.37 % (3720090)Peak memory usage: 27 MB
% 134.67/19.37 % (3720090)Instructions burned: 4594 (million)
% 134.67/19.37 % (3720098)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=2621956339:fmbsr=2:i=46332_2969 on theBenchmark for (2969ds/46332Mi)
% 134.67/19.37 % (3720078)Instruction limit reached!
% 134.67/19.37 % (3720078)------------------------------
% 134.67/19.37 % (3720078)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.67/19.37 % (3720078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.67/19.37 % (3720078)CaDiCaL version: 2.1.3
% 134.67/19.37 % (3720078)Termination reason: Instruction limit
% 134.67/19.37 % (3720078)Termination phase: Saturation
% 134.67/19.37 % (3720078)Time elapsed: 2.070 s
% 134.67/19.37 % (3720078)Peak memory usage: 25 MB
% 134.67/19.37 % (3720078)Instructions burned: 5114 (million)
% 134.67/19.37 % (3720100)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2479741891:i=14071_2968 on theBenchmark for (2968ds/14071Mi)
% 134.67/19.37 % Exception at run slice level
% 134.67/19.37 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 134.67/19.37 % Exception at run slice level
% 134.67/19.37 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 134.67/19.37 % (3720102)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=911210421:i=22565:add=on:rawr=on_2968 on theBenchmark for (2968ds/22565Mi)
% 134.67/19.37 % (3720103)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2680757997:i=8173:av=off_2968 on theBenchmark for (2968ds/8173Mi)
% 134.67/19.37 % Exception at run slice level
% 134.67/19.37 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 134.67/19.37 % (3720106)dis+10_16:1_sil=16000:random_seed=2479029635:i=9155:fsr=off_2966 on theBenchmark for (2966ds/9155Mi)
% 134.67/19.37 % (3720094)Instruction limit reached!
% 134.67/19.37 % (3720094)------------------------------
% 134.67/19.37 % (3720094)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.67/19.37 % (3720094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.67/19.37 % (3720094)CaDiCaL version: 2.1.3
% 134.67/19.37 % (3720094)Termination reason: Instruction limit
% 134.67/19.37 % (3720094)Termination phase: Saturation
% 134.67/19.37 % (3720094)Time elapsed: 2.149 s
% 134.67/19.37 % (3720094)Peak memory usage: 27 MB
% 134.67/19.37 % (3720094)Instructions burned: 5211 (million)
% 134.67/19.37 % (3720108)ott-3_8_sil=64000:random_seed=3182900191:i=20139:bs=on_2950 on theBenchmark for (2950ds/20139Mi)
% 134.67/19.37 % (3720103)Instruction limit reached!
% 134.67/19.37 % (3720103)------------------------------
% 134.67/19.37 % (3720103)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 134.67/19.37 % (3720103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.67/19.37 % (3720103)CaDiCaL version: 2.1.3
% 134.67/19.37 % (3720103)Termination reason: Instruction limit
% 134.67/19.37 % (3720103)Termination phase: Saturation
% 134.67/19.37 % (3720103)Time elapsed: 3.314 s
% 134.67/19.37 % (3720103)Peak memory usage: 26 MB
% 134.67/19.37 % (3720103)Instructions burned: 8175 (million)
% 134.67/19.37 % (3720110)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=4267072361:fmbsr=2:i=32576_2934 on theBenchmark for (2934ds/32576Mi)
% 134.67/19.37 % Exception at run slice level
% 81.90/20.61 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 81.90/20.61 % (3720112)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=555161663:i=11404_2932 on theBenchmark for (2932ds/11404Mi)
% 81.90/20.61 % (3720106)Instruction limit reached!
% 81.90/20.61 % (3720106)------------------------------
% 81.90/20.61 % (3720106)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 81.90/20.61 % (3720106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.90/20.61 % (3720106)CaDiCaL version: 2.1.3
% 81.90/20.61 % (3720106)Termination reason: Instruction limit
% 81.90/20.61 % (3720106)Termination phase: Saturation
% 81.90/20.61 % (3720106)Time elapsed: 3.749 s
% 81.90/20.61 % (3720106)Peak memory usage: 23 MB
% 81.90/20.61 % (3720106)Instructions burned: 9155 (million)
% 81.90/20.61 % (3720114)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2116844888:i=14134_2928 on theBenchmark for (2928ds/14134Mi)
% 81.90/20.61 % (3720114)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 81.90/20.61 % (3720102)Instruction limit reached!
% 81.90/20.61 % (3720102)------------------------------
% 81.90/20.61 % (3720102)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 81.90/20.61 % (3720102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.90/20.61 % (3720102)CaDiCaL version: 2.1.3
% 81.90/20.61 % (3720102)Termination reason: Instruction limit
% 81.90/20.61 % (3720102)Termination phase: Saturation
% 81.90/20.61 % (3720102)Time elapsed: 5.305 s
% 81.90/20.61 % (3720102)Peak memory usage: 27 MB
% 81.90/20.61 % (3720102)Instructions burned: 22566 (million)
% 81.90/20.61 % (3720116)dis+33_16_sil=32000:sac=on:random_seed=1668879339:i=15851:nm=0_2914 on theBenchmark for (2914ds/15851Mi)
% 81.90/20.61 % (3720112)Instruction limit reached!
% 81.90/20.61 % (3720112)------------------------------
% 81.90/20.61 % (3720112)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 81.90/20.61 % (3720112)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.90/20.61 % (3720112)CaDiCaL version: 2.1.3
% 81.90/20.61 % (3720112)Termination reason: Instruction limit
% 81.90/20.61 % (3720112)Termination phase: Saturation
% 81.90/20.61 % (3720112)Time elapsed: 4.688 s
% 81.90/20.61 % (3720112)Peak memory usage: 27 MB
% 81.90/20.61 % (3720112)Instructions burned: 11404 (million)
% 81.90/20.61 % (3720118)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1491360053:avsq=on:i=17627:add=on:amm=off_2885 on theBenchmark for (2885ds/17627Mi)
% 81.90/20.61 % (3720116)Instruction limit reached!
% 81.90/20.61 % (3720116)------------------------------
% 81.90/20.61 % (3720116)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 81.90/20.61 % (3720116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.90/20.61 % (3720116)CaDiCaL version: 2.1.3
% 81.90/20.61 % (3720116)Termination reason: Instruction limit
% 81.90/20.61 % (3720116)Termination phase: Saturation
% 81.90/20.61 % (3720116)Time elapsed: 3.552 s
% 81.90/20.61 % (3720116)Peak memory usage: 23 MB
% 81.90/20.61 % (3720116)Instructions burned: 15852 (million)
% 81.90/20.61 % (3720120)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=2498287935:s2a=on:i=53295_2879 on theBenchmark for (2879ds/53295Mi)
% 81.90/20.61 % (3720114)Instruction limit reached!
% 81.90/20.61 % (3720114)------------------------------
% 81.90/20.61 % (3720114)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 81.90/20.61 % (3720114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.90/20.61 % (3720114)CaDiCaL version: 2.1.3
% 81.90/20.61 % (3720114)Termination reason: Instruction limit
% 81.90/20.61 % (3720114)Termination phase: Saturation
% 81.90/20.61 % (3720114)Time elapsed: 5.884 s
% 81.90/20.61 % (3720114)Peak memory usage: 26 MB
% 81.90/20.61 % (3720114)Instructions burned: 14136 (million)
% 81.90/20.61 % (3720122)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=3002727519:i=26857:ins=20_2869 on theBenchmark for (2869ds/26857Mi)
% 81.90/20.61 % Exception at run slice level
% 81.90/20.61 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 81.90/20.61 % (3720125)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=2049713027:i=28120:bs=on:fsr=off_2866 on theBenchmark for (2866ds/28120Mi)
% 81.90/20.61 % (3720108)Instruction limit reached!
% 81.90/20.61 % (3720108)------------------------------
% 81.90/20.61 % (3720108)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 81.90/20.61 % (3720108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.90/20.61 % (3720108)CaDiCaL version: 2.1.3
% 81.90/20.61 % (3720108)Termination reason: Instruction limit
% 81.90/20.61 % (3720108)Termination phase: Saturation
% 81.90/20.61 % (3720108)Time elapsed: 8.607 s
% 81.90/20.61 % (3720108)Peak memory usage: 27 MB
% 81.90/20.61 % (3720108)Instructions burned: 20141 (million)
% 81.90/20.61 % (3720199)fmb+10_1_sil=256000:fmbss=7:random_seed=2479169887:fmbsr=1.6:i=182295_2864 on theBenchmark for (2864ds/182295Mi)
% 81.90/20.61 % Exception at run slice level
% 81.90/20.61 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 81.90/20.61 % (3720244)fmb+10_1_sil=128000:fmbss=21:newcnf=on:random_seed=515420719:i=44625:gsp=on_2862 on theBenchmark for (2862ds/44625Mi)
% 81.90/20.61 % (3720244)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 81.90/20.61 % (3720244)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 81.90/20.61 % Exception at run slice level
% 81.90/20.61 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 81.90/20.61 % (3720258)fmb+10_1_sil=256000:sas=cadical:fmbss=15:random_seed=1364877127:i=160505_2859 on theBenchmark for (2859ds/160505Mi)
% 81.90/20.61 % Exception at run slice level
% 81.90/20.61 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 81.90/20.61 % (3720347)fmb+10_1_sil=256000:tgt=full:fmbss=10:random_seed=1119604628:fmbsr=1.3:i=225729_2857 on theBenchmark for (2857ds/225729Mi)
% 81.90/20.61 % Exception at run slice level
% 81.90/20.61 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 81.90/20.61 % (3720399)fmb+10_1_sil=256000:tgt=full:sas=cadical:fmbss=10:random_seed=345956792:fmbsr=2:i=185024:ins=7_2854 on theBenchmark for (2854ds/185024Mi)
% 81.90/20.61 % Exception at run slice level
% 81.90/20.61 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 81.90/20.61 % (3720468)fmb+10_1_sas=cadical:si=on:bce=on:rp=on:random_seed=3111124005:rtra=on_2851 on theBenchmark for (2851ds/0Mi)
% 81.90/20.61 % (3720092)Instruction limit reached!
% 81.90/20.61 % (3720092)------------------------------
% 81.90/20.61 % (3720092)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 81.90/20.61 % (3720092)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.90/20.61 % (3720092)CaDiCaL version: 2.1.3
% 81.90/20.61 % (3720092)Termination reason: Instruction limit
% 81.90/20.61 % (3720092)Termination phase: Saturation
% 81.90/20.61 % (3720092)Time elapsed: 12.531 s
% 81.90/20.61 % (3720092)Peak memory usage: 25 MB
% 81.90/20.61 % (3720092)Instructions burned: 29342 (million)
% 81.90/20.61 % (3720508)% WARNING: option uhcvi not known.
% 81.90/20.61 % (3720508)dis+11_61:31_drc=ordering:si=on:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=361614927:i=271062:add=off:rtra=on:rawr=on_2849 on theBenchmark for (2849ds/271062Mi)
% 81.90/20.61 % Exception at run slice level
% 81.90/20.61 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 81.90/20.61 % (3720523)dis+10_161_sil=256000:plsq=on:si=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2431761348:i=176048:add=on:rtra=on:rawr=on_2849 on theBenchmark for (2849ds/176048Mi)
% 81.90/20.61 % (3720508)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 81.90/20.61 % (3720508)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 81.90/20.61 % (3720118)Instruction limit reached!
% 81.90/20.61 % (3720118)------------------------------
% 81.90/20.61 % (3720118)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 81.90/20.61 % (3720118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.90/20.61 % (3720118)CaDiCaL version: 2.1.3
% 81.90/20.61 % (3720118)Termination reason: Instruction limit
% 81.90/20.61 % (3720118)Termination phase: Saturation
% 81.90/20.61 % (3720118)Time elapsed: 7.532 s
% 81.90/20.61 % (3720118)Peak memory usage: 25 MB
% 81.90/20.61 % (3720118)Instructions burned: 17628 (million)
% 81.90/20.61 % (3720559)dis+10_1_sil=32000:si=on:sp=arity:random_seed=559692911:i=206:fgj=on:rtra=on_2809 on theBenchmark for (2809ds/206Mi)
% 81.90/20.61 % (3720559)Instruction limit reached!
% 81.90/20.61 % (3720559)------------------------------
% 81.90/20.61 % (3720559)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 81.90/20.61 % (3720559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.90/20.61 % (3720559)CaDiCaL version: 2.1.3
% 81.90/20.61 % (3720559)Termination reason: Instruction limit
% 81.90/20.61 % (3720559)Termination phase: Property scanning
% 81.90/20.61 % (3720559)Time elapsed: 0.086 s
% 81.90/20.61 % (3720559)Peak memory usage: 16 MB
% 81.90/20.61 % (3720559)Instructions burned: 207 (million)
% 81.90/20.61 % (3720561)ott+31_1_sil=16000:si=on:lcm=predicate:bce=on:newcnf=on:random_seed=1204471865:i=232:rtra=on_2808 on theBenchmark for (2808ds/232Mi)
% 81.90/20.61 % (3720561)Instruction limit reached!
% 81.90/20.61 % (3720561)------------------------------
% 81.90/20.61 % (3720561)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 81.90/20.61 % (3720561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.90/20.61 % (3720561)CaDiCaL version: 2.1.3
% 81.90/20.61 % (3720561)Termination reason: Instruction limit
% 81.90/20.61 % (3720561)Termination phase: Property scanning
% 81.90/20.61 % (3720561)Time elapsed: 0.096 s
% 81.90/20.61 % (3720561)Peak memory usage: 16 MB
% 81.90/20.61 % (3720561)Instructions burned: 233 (million)
% 81.90/20.61 % (3720564)ott+1_1_to=lpo:sil=16000:si=on:sp=reverse_arity:erd=off:random_seed=2155669621:i=262:rtra=on_2807 on theBenchmark for (2807ds/262Mi)
% 81.90/20.61 % (3720564)Instruction limit reached!
% 81.90/20.61 % (3720564)------------------------------
% 81.90/20.61 % (3720564)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 81.90/20.61 % (3720564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.90/20.61 % (3720564)CaDiCaL version: 2.1.3
% 81.90/20.61 % (3720564)Termination reason: Instruction limit
% 81.90/20.61 % (3720564)Termination phase: shuffling
% 81.90/20.61 % (3720564)Time elapsed: 0.110 s
% 81.90/20.61 % (3720564)Peak memory usage: 17 MB
% 81.90/20.61 % (3720564)Instructions burned: 262 (million)
% 81.90/20.61 % (3720566)ott-3_16_to=lpo:sil=16000:si=on:sp=arity:fd=off:rp=on:random_seed=686771646:i=318:bs=unit_only:nicw=on:fsr=off:rtra=on:amm=off_2806 on theBenchmark for (2806ds/318Mi)
% 81.90/20.61 % (3720566)Instruction limit reached!
% 81.90/20.61 % (3720566)------------------------------
% 81.90/20.61 % (3720566)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 81.90/20.61 % (3720566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.90/20.61 % (3720566)CaDiCaL version: 2.1.3
% 81.90/20.61 % (3720566)Termination reason: Instruction limit
% 81.90/20.61 % (3720566)Termination phase: Preprocessing 3
% 81.90/20.61 % (3720566)Time elapsed: 0.138 s
% 81.90/20.61 % (3720566)Peak memory usage: 19 MB
% 81.90/20.61 % (3720566)Instructions burned: 319 (million)
% 81.90/20.61 % (3720568)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:si=on:random_seed=3712508372:i=1428:nm=2:rtra=on_2804 on theBenchmark for (2804ds/1428Mi)
% 81.90/20.61 % Exception at run slice level
% 81.90/20.61 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 81.90/20.61 % (3720570)ott+32_1_sil=16000:bsd=on:si=on:sp=const_max:bce=on:random_seed=781980299:i=262:bd=preordered:rtra=on:fsd=on_2801 on theBenchmark for (2801ds/262Mi)
% 81.90/20.61 % (3720570)Instruction limit reached!
% 81.90/20.61 % (3720570)------------------------------
% 81.90/20.61 % (3720570)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 81.90/20.61 % (3720570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.90/20.61 % (3720570)CaDiCaL version: 2.1.3
% 81.90/20.61 % (3720570)Termination reason: Instruction limit
% 81.90/20.61 % (3720570)Termination phase: shuffling
% 81.90/20.61 % (3720570)Time elapsed: 0.109 s
% 81.90/20.61 % (3720570)Peak memory usage: 17 MB
% 81.90/20.61 % (3720570)Instructions burned: 262 (million)
% 81.90/20.61 % (3720572)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=2800000442:i=1368:slsql=off:bs=unit_only:nicw=on:rtra=on:rawr=on_2800 on theBenchmark for (2800ds/1368Mi)
% 81.90/20.61 % (3720572)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 81.90/20.61 % (3720572)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 81.90/20.61 % (3720572) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3719890-3720572"...
% 81.90/20.61 % (3720572)...printing done.
% 81.90/20.61 % (3720572)Refutation found. Thanks to Tanya!
% 81.90/20.61 % SZS status Theorem for theBenchmark
% 81.90/20.61 % SZS output start Proof for theBenchmark
% 81.90/20.61 thf(type_def_5, type, num: $tType).
% 81.90/20.61 thf(type_def_6, type, sTfun: ($tType * $tType) > $tType).
% 81.90/20.61 thf(func_def_0, type, abstractCounterpart_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_2, type, age_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_3, type, agent_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_4, type, altitude_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 81.90/20.61 thf(func_def_5, type, ancestor_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_8, type, arcWeight_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_9, type, atomicNumber_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_10, type, attends_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_11, type, attribute_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_12, type, authors_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_13, type, average_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_14, type, barometricPressure_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_15, type, beforeOrEqual_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_16, type, before_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_17, type, believes_THFTYPE_IiooI: ($i > $o > $o)).
% 81.90/20.61 thf(func_def_18, type, between_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 81.90/20.61 thf(func_def_19, type, boilingPoint_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_20, type, bottom_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_22, type, capability_THFTYPE_IIioIIiioIioI: (($i > $o) > ($i > $i > $o) > $i > $o)).
% 81.90/20.61 thf(func_def_23, type, capability_THFTYPE_IiIiioIioI: ($i > ($i > $i > $o) > $i > $o)).
% 81.90/20.61 thf(func_def_24, type, causesProposition_THFTYPE_IoooI: ($o > $o > $o)).
% 81.90/20.61 thf(func_def_25, type, causesSubclass_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_26, type, causes_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_28, type, closedOn_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_29, type, color_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_30, type, completelyFills_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_31, type, component_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_32, type, conclusion_THFTYPE_IoooI: ($o > $o > $o)).
% 81.90/20.61 thf(func_def_33, type, conditionalProbability_THFTYPE_IooioI: ($o > $o > $i > $o)).
% 81.90/20.61 thf(func_def_34, type, confersNorm_THFTYPE_IioioI: ($i > $o > $i > $o)).
% 81.90/20.61 thf(func_def_35, type, confersObligation_THFTYPE_IoiioI: ($o > $i > $i > $o)).
% 81.90/20.61 thf(func_def_36, type, confersRight_THFTYPE_IoiioI: ($o > $i > $i > $o)).
% 81.90/20.61 thf(func_def_37, type, connectedEngineeringComponents_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_38, type, connected_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_39, type, connectsEngineeringComponents_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 81.90/20.61 thf(func_def_40, type, connects_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 81.90/20.61 thf(func_def_41, type, considers_THFTYPE_IiooI: ($i > $o > $o)).
% 81.90/20.61 thf(func_def_42, type, consistent_THFTYPE_IoooI: ($o > $o > $o)).
% 81.90/20.61 thf(func_def_43, type, containsInformation_THFTYPE_IiooI: ($i > $o > $o)).
% 81.90/20.61 thf(func_def_44, type, contains_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_45, type, contraryAttribute_THFTYPE_IiiiioI: ($i > $i > $i > $i > $o)).
% 81.90/20.61 thf(func_def_46, type, contraryAttribute_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_47, type, contraryAttribute_THFTYPE_IioI: ($i > $o)).
% 81.90/20.61 thf(func_def_48, type, contraryAttribute_THFTYPE_IoooI: ($o > $o > $o)).
% 81.90/20.61 thf(func_def_49, type, cooccur_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_50, type, copy_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_51, type, crosses_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_52, type, date_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_53, type, daughter_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_54, type, decreasesLikelihood_THFTYPE_IoooI: ($o > $o > $o)).
% 81.90/20.61 thf(func_def_55, type, deprivesNorm_THFTYPE_IioioI: ($i > $o > $i > $o)).
% 81.90/20.61 thf(func_def_56, type, depth_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 81.90/20.61 thf(func_def_57, type, desires_THFTYPE_IiooI: ($i > $o > $o)).
% 81.90/20.61 thf(func_def_58, type, destination_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_59, type, developmentalForm_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_60, type, diameter_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_61, type, direction_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_62, type, disjointDecomposition_THFTYPE_IiiiiiioI: ($i > $i > $i > $i > $i > $i > $o)).
% 81.90/20.61 thf(func_def_63, type, disjointDecomposition_THFTYPE_IiiiiioI: ($i > $i > $i > $i > $i > $o)).
% 81.90/20.61 thf(func_def_64, type, disjointDecomposition_THFTYPE_IiiiioI: ($i > $i > $i > $i > $o)).
% 81.90/20.61 thf(func_def_65, type, disjointDecomposition_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 81.90/20.61 thf(func_def_66, type, disjointDecomposition_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_67, type, disjointDecomposition_THFTYPE_IioI: ($i > $o)).
% 81.90/20.61 thf(func_def_68, type, disjointRelation_THFTYPE_IIiioIIiioIoI: (($i > $i > $o) > ($i > $i > $o) > $o)).
% 81.90/20.61 thf(func_def_69, type, disjointRelation_THFTYPE_IIioIIioIoI: (($i > $o) > ($i > $o) > $o)).
% 81.90/20.61 thf(func_def_70, type, disjointRelation_THFTYPE_IIioioIIioioIoI: (($i > $o > $i > $o) > ($i > $o > $i > $o) > $o)).
% 81.90/20.61 thf(func_def_71, type, disjointRelation_THFTYPE_IIoooIIoooIoI: (($o > $o > $o) > ($o > $o > $o) > $o)).
% 81.90/20.61 thf(func_def_72, type, disjointRelation_THFTYPE_IiIiioIoI: ($i > ($i > $i > $o) > $o)).
% 81.90/20.61 thf(func_def_73, type, disjointRelation_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_74, type, disjoint_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_75, type, distance_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 81.90/20.61 thf(func_def_76, type, distributes_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_77, type, div_THFTYPE_IiiiI: ($i > $i > $i)).
% 81.90/20.61 thf(func_def_79, type, domainSubclass_THFTYPE_IIIioIIiioIioIiioI: ((($i > $o) > ($i > $i > $o) > $i > $o) > $i > $i > $o)).
% 81.90/20.61 thf(func_def_80, type, domainSubclass_THFTYPE_IIiiiIiioI: (($i > $i > $i) > $i > $i > $o)).
% 81.90/20.61 thf(func_def_81, type, domainSubclass_THFTYPE_IIiiiiiioIiioI: (($i > $i > $i > $i > $i > $i > $o) > $i > $i > $o)).
% 81.90/20.61 thf(func_def_82, type, domainSubclass_THFTYPE_IIiioIiioI: (($i > $i > $o) > $i > $i > $o)).
% 81.90/20.61 thf(func_def_83, type, domainSubclass_THFTYPE_IIioIiioI: (($i > $o) > $i > $i > $o)).
% 81.90/20.61 thf(func_def_84, type, domainSubclass_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 81.90/20.61 thf(func_def_85, type, domain_THFTYPE_IIIIioIIiioIioIiioIiioI: (((($i > $o) > ($i > $i > $o) > $i > $o) > $i > $i > $o) > $i > $i > $o)).
% 81.90/20.61 thf(func_def_86, type, domain_THFTYPE_IIIiiIioIiioI: ((($i > $i) > $i > $o) > $i > $i > $o)).
% 81.90/20.61 thf(func_def_87, type, domain_THFTYPE_IIIiioIIiioIoIiioI: ((($i > $i > $o) > ($i > $i > $o) > $o) > $i > $i > $o)).
% 81.90/20.61 thf(func_def_88, type, domain_THFTYPE_IIIiioIioIiioI: ((($i > $i > $o) > $i > $o) > $i > $i > $o)).
% 81.90/20.61 thf(func_def_89, type, domain_THFTYPE_IIIioIIiioIioIiioI: ((($i > $o) > ($i > $i > $o) > $i > $o) > $i > $i > $o)).
% 81.90/20.61 thf(func_def_90, type, domain_THFTYPE_IIIioIiIiioI: ((($i > $o) > $i) > $i > $i > $o)).
% 81.90/20.61 thf(func_def_91, type, domain_THFTYPE_IIIioIioIiioI: ((($i > $o) > $i > $o) > $i > $i > $o)).
% 81.90/20.61 thf(func_def_92, type, domain_THFTYPE_IIIoiIioIiioI: ((($o > $i) > $i > $o) > $i > $i > $o)).
% 81.90/20.61 thf(func_def_93, type, domain_THFTYPE_IIIoioIIiioIoIiioI: ((($o > $i > $o) > ($i > $i > $o) > $o) > $i > $i > $o)).
% 81.90/20.61 thf(func_def_94, type, domain_THFTYPE_IIiiIiioI: (($i > $i) > $i > $i > $o)).
% 81.90/20.61 thf(func_def_95, type, domain_THFTYPE_IIiiiIiioI: (($i > $i > $i) > $i > $i > $o)).
% 81.90/20.61 thf(func_def_96, type, domain_THFTYPE_IIiiiiiioIiioI: (($i > $i > $i > $i > $i > $i > $o) > $i > $i > $o)).
% 81.90/20.61 thf(func_def_97, type, domain_THFTYPE_IIiiiioIiioI: (($i > $i > $i > $i > $o) > $i > $i > $o)).
% 81.90/20.61 thf(func_def_98, type, domain_THFTYPE_IIiiioIiioI: (($i > $i > $i > $o) > $i > $i > $o)).
% 81.90/20.61 thf(func_def_99, type, domain_THFTYPE_IIiioIiioI: (($i > $i > $o) > $i > $i > $o)).
% 81.90/20.61 thf(func_def_100, type, domain_THFTYPE_IIioIiioI: (($i > $o) > $i > $i > $o)).
% 81.90/20.61 thf(func_def_101, type, domain_THFTYPE_IIioioIiioI: (($i > $o > $i > $o) > $i > $i > $o)).
% 81.90/20.61 thf(func_def_102, type, domain_THFTYPE_IIiooIiioI: (($i > $o > $o) > $i > $i > $o)).
% 81.90/20.61 thf(func_def_103, type, domain_THFTYPE_IIioooIiioI: (($i > $o > $o > $o) > $i > $i > $o)).
% 81.90/20.61 thf(func_def_104, type, domain_THFTYPE_IIoiIiioI: (($o > $i) > $i > $i > $o)).
% 81.90/20.61 thf(func_def_105, type, domain_THFTYPE_IIoiioIiioI: (($o > $i > $i > $o) > $i > $i > $o)).
% 81.90/20.61 thf(func_def_106, type, domain_THFTYPE_IIoioIiioI: (($o > $i > $o) > $i > $i > $o)).
% 81.90/20.61 thf(func_def_107, type, domain_THFTYPE_IIooIiioI: (($o > $o) > $i > $i > $o)).
% 81.90/20.61 thf(func_def_108, type, domain_THFTYPE_IIooioIiioI: (($o > $o > $i > $o) > $i > $i > $o)).
% 81.90/20.61 thf(func_def_109, type, domain_THFTYPE_IIoooIiioI: (($o > $o > $o) > $i > $i > $o)).
% 81.90/20.61 thf(func_def_110, type, domain_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 81.90/20.61 thf(func_def_111, type, duration_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_112, type, during_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_113, type, earlier_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_115, type, element_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_116, type, employs_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_117, type, engineeringSubcomponent_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_118, type, entails_THFTYPE_IoooI: ($o > $o > $o)).
% 81.90/20.61 thf(func_def_120, type, equivalenceRelationOn_THFTYPE_IIiioIioI: (($i > $i > $o) > $i > $o)).
% 81.90/20.61 thf(func_def_121, type, equivalentContentClass_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_122, type, equivalentContentInstance_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_123, type, exactlyLocated_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_124, type, exhaustiveAttribute_THFTYPE_IiiiiiioI: ($i > $i > $i > $i > $i > $i > $o)).
% 81.90/20.61 thf(func_def_125, type, exhaustiveAttribute_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 81.90/20.61 thf(func_def_126, type, exhaustiveAttribute_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_127, type, exhaustiveDecomposition_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_128, type, exhaustiveDecomposition_THFTYPE_IioI: ($i > $o)).
% 81.90/20.61 thf(func_def_129, type, experiencer_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_130, type, exploits_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_131, type, expressedInLanguage_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_133, type, faces_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_134, type, familyRelation_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_135, type, father_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_136, type, fills_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_137, type, finishes_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_138, type, frequency_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_140, type, geometricDistance_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 81.90/20.61 thf(func_def_142, type, geopoliticalSubdivision_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_143, type, graphMeasure_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_144, type, graphPart_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_145, type, grasps_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_146, type, greaterThanByQuality_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 81.90/20.61 thf(func_def_147, type, greaterThanOrEqualTo_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_148, type, greaterThan_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_149, type, gt_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_150, type, gtet_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_151, type, hasPurposeForAgent_THFTYPE_IioioI: ($i > $o > $i > $o)).
% 81.90/20.61 thf(func_def_152, type, hasPurpose_THFTYPE_IiooI: ($i > $o > $o)).
% 81.90/20.61 thf(func_def_153, type, hasPurpose_THFTYPE_IooI: ($o > $o)).
% 81.90/20.61 thf(func_def_154, type, hasSkill_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_155, type, height_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_156, type, holdsDuring_THFTYPE_IiooI: ($i > $o > $o)).
% 81.90/20.61 thf(func_def_157, type, holdsObligation_THFTYPE_IoioI: ($o > $i > $o)).
% 81.90/20.61 thf(func_def_158, type, holdsRight_THFTYPE_IoioI: ($o > $i > $o)).
% 81.90/20.61 thf(func_def_159, type, hole_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_160, type, home_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_161, type, husband_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_162, type, identicalListItems_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_163, type, identityElement_THFTYPE_IIiiiIioI: (($i > $i > $i) > $i > $o)).
% 81.90/20.61 thf(func_def_164, type, identityElement_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_165, type, immediateInstance_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_166, type, immediateSubclass_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_167, type, inList_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_168, type, inScopeOfInterest_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_169, type, increasesLikelihood_THFTYPE_IoooI: ($o > $o > $o)).
% 81.90/20.61 thf(func_def_170, type, independentProbability_THFTYPE_IoooI: ($o > $o > $o)).
% 81.90/20.61 thf(func_def_171, type, inhabits_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_172, type, inhibits_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_173, type, initialList_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_174, type, initialPart_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_175, type, instance_THFTYPE_IIIIioIIiioIioIiioIioI: (((($i > $o) > ($i > $i > $o) > $i > $o) > $i > $i > $o) > $i > $o)).
% 81.90/20.61 thf(func_def_176, type, instance_THFTYPE_IIIiiIioIioI: ((($i > $i) > $i > $o) > $i > $o)).
% 81.90/20.61 thf(func_def_177, type, instance_THFTYPE_IIIiioIIiioIoIioI: ((($i > $i > $o) > ($i > $i > $o) > $o) > $i > $o)).
% 81.90/20.61 thf(func_def_178, type, instance_THFTYPE_IIIiioIioIioI: ((($i > $i > $o) > $i > $o) > $i > $o)).
% 81.90/20.61 thf(func_def_179, type, instance_THFTYPE_IIIioIIiioIioIioI: ((($i > $o) > ($i > $i > $o) > $i > $o) > $i > $o)).
% 81.90/20.61 thf(func_def_180, type, instance_THFTYPE_IIIioIiIioI: ((($i > $o) > $i) > $i > $o)).
% 81.90/20.61 thf(func_def_181, type, instance_THFTYPE_IIIioIioIioI: ((($i > $o) > $i > $o) > $i > $o)).
% 81.90/20.61 thf(func_def_182, type, instance_THFTYPE_IIIioioIiioIioI: ((($i > $o > $i > $o) > $i > $i > $o) > $i > $o)).
% 81.90/20.61 thf(func_def_183, type, instance_THFTYPE_IIIoioIIiioIoIioI: ((($o > $i > $o) > ($i > $i > $o) > $o) > $i > $o)).
% 81.90/20.61 thf(func_def_184, type, instance_THFTYPE_IIiiIioI: (($i > $i) > $i > $o)).
% 81.90/20.61 thf(func_def_185, type, instance_THFTYPE_IIiiiIioI: (($i > $i > $i) > $i > $o)).
% 81.90/20.61 thf(func_def_186, type, instance_THFTYPE_IIiiiiiioIioI: (($i > $i > $i > $i > $i > $i > $o) > $i > $o)).
% 81.90/20.61 thf(func_def_187, type, instance_THFTYPE_IIiiiioIioI: (($i > $i > $i > $i > $o) > $i > $o)).
% 81.90/20.61 thf(func_def_188, type, instance_THFTYPE_IIiiioIioI: (($i > $i > $i > $o) > $i > $o)).
% 81.90/20.61 thf(func_def_189, type, instance_THFTYPE_IIiioIioI: (($i > $i > $o) > $i > $o)).
% 81.90/20.61 thf(func_def_190, type, instance_THFTYPE_IIioIioI: (($i > $o) > $i > $o)).
% 81.90/20.61 thf(func_def_191, type, instance_THFTYPE_IIioioIioI: (($i > $o > $i > $o) > $i > $o)).
% 81.90/20.61 thf(func_def_192, type, instance_THFTYPE_IIiooIioI: (($i > $o > $o) > $i > $o)).
% 81.90/20.61 thf(func_def_193, type, instance_THFTYPE_IIioooIioI: (($i > $o > $o > $o) > $i > $o)).
% 81.90/20.61 thf(func_def_194, type, instance_THFTYPE_IIoiIioI: (($o > $i) > $i > $o)).
% 81.90/20.61 thf(func_def_195, type, instance_THFTYPE_IIoiioIioI: (($o > $i > $i > $o) > $i > $o)).
% 81.90/20.61 thf(func_def_196, type, instance_THFTYPE_IIoioIioI: (($o > $i > $o) > $i > $o)).
% 81.90/20.61 thf(func_def_197, type, instance_THFTYPE_IIooIioI: (($o > $o) > $i > $o)).
% 81.90/20.61 thf(func_def_198, type, instance_THFTYPE_IIooioIioI: (($o > $o > $i > $o) > $i > $o)).
% 81.90/20.61 thf(func_def_199, type, instance_THFTYPE_IIoooIioI: (($o > $o > $o) > $i > $o)).
% 81.90/20.61 thf(func_def_200, type, instance_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_201, type, instance_THFTYPE_IoioI: ($o > $i > $o)).
% 81.90/20.61 thf(func_def_202, type, instrument_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_203, type, interiorPart_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_204, type, inverse_THFTYPE_IIiioIIiioIoI: (($i > $i > $o) > ($i > $i > $o) > $o)).
% 81.90/20.61 thf(func_def_205, type, involvedInEvent_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_206, type, irreflexiveOn_THFTYPE_IIiioIioI: (($i > $i > $o) > $i > $o)).
% 81.90/20.61 thf(func_def_207, type, knows_THFTYPE_IiooI: ($i > $o > $o)).
% 81.90/20.61 thf(func_def_210, type, lAbsoluteValueFn_THFTYPE_IiiI: ($i > $i)).
% 81.90/20.61 thf(func_def_213, type, lAbstractionFn_THFTYPE_IiiI: ($i > $i)).
% 81.90/20.61 thf(func_def_215, type, lAdditionFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 81.90/20.61 thf(func_def_254, type, lAssignmentFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 81.90/20.61 thf(func_def_255, type, lAssignmentFn_THFTYPE_IiiiiI: ($i > $i > $i > $i)).
% 81.90/20.61 thf(func_def_271, type, lBackFn_THFTYPE_IiiI: ($i > $i)).
% 81.90/20.61 thf(func_def_276, type, lBeginFn_THFTYPE_IiiI: ($i > $i)).
% 81.90/20.61 thf(func_def_278, type, lBeginNodeFn_THFTYPE_IiiI: ($i > $i)).
% 81.90/20.61 thf(func_def_319, type, lCardinalityFn_THFTYPE_IIioIiI: (($i > $o) > $i)).
% 81.90/20.61 thf(func_def_320, type, lCardinalityFn_THFTYPE_IiiI: ($i > $i)).
% 81.90/20.61 thf(func_def_325, type, lCeilingFn_THFTYPE_IiiI: ($i > $i)).
% 81.90/20.61 thf(func_def_329, type, lCenterOfCircleFn_THFTYPE_IiiI: ($i > $i)).
% 81.90/20.61 thf(func_def_387, type, lCosineFn_THFTYPE_IiiI: ($i > $i)).
% 81.90/20.61 thf(func_def_398, type, lCutSetFn_THFTYPE_IiiI: ($i > $i)).
% 81.90/20.61 thf(func_def_405, type, lDayFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 81.90/20.61 thf(func_def_436, type, lDivisionFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 81.90/20.61 thf(func_def_446, type, lEditionFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 81.90/20.61 thf(func_def_458, type, lEndFn_THFTYPE_IiiI: ($i > $i)).
% 81.90/20.61 thf(func_def_460, type, lEndNodeFn_THFTYPE_IiiI: ($i > $i)).
% 81.90/20.61 thf(func_def_475, type, lExponentiationFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 81.90/20.61 thf(func_def_478, type, lExtensionFn_THFTYPE_IiiI: ($i > $i)).
% 81.90/20.61 thf(func_def_499, type, lFloorFn_THFTYPE_IiiI: ($i > $i)).
% 81.90/20.61 thf(func_def_511, type, lFrontFn_THFTYPE_IiiI: ($i > $i)).
% 81.90/20.61 thf(func_def_519, type, lFutureFn_THFTYPE_IiiI: ($i > $i)).
% 81.90/20.61 thf(func_def_534, type, lGigaFn_THFTYPE_IiiI: ($i > $i)).
% 81.90/20.61 thf(func_def_539, type, lGovernmentFn_THFTYPE_IiiI: ($i > $i)).
% 81.90/20.61 thf(func_def_551, type, lGraphPathFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 81.90/20.61 thf(func_def_556, type, lGreatestCommonDivisorFn_THFTYPE_IiiI: ($i > $i)).
% 81.90/20.61 thf(func_def_567, type, lHoleHostFn_THFTYPE_IiiI: ($i > $i)).
% 81.90/20.61 thf(func_def_569, type, lHoleSkinFn_THFTYPE_IiiI: ($i > $i)).
% 81.90/20.61 thf(func_def_578, type, lHourFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 81.90/20.61 thf(func_def_588, type, lImaginaryPartFn_THFTYPE_IiiI: ($i > $i)).
% 81.90/20.61 thf(func_def_590, type, lImmediateFamilyFn_THFTYPE_IiiI: ($i > $i)).
% 81.90/20.61 thf(func_def_592, type, lImmediateFutureFn_THFTYPE_IiiI: ($i > $i)).
% 81.90/20.61 thf(func_def_594, type, lImmediatePastFn_THFTYPE_IiiI: ($i > $i)).
% 81.90/20.61 thf(func_def_605, type, lInitialNodeFn_THFTYPE_IiiI: ($i > $i)).
% 81.90/20.61 thf(func_def_620, type, lIntervalFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 81.90/20.61 thf(func_def_642, type, lKiloFn_THFTYPE_IiiI: ($i > $i)).
% 81.90/20.61 thf(func_def_653, type, lLeastCommonMultipleFn_THFTYPE_IiiI: ($i > $i)).
% 81.90/20.61 thf(func_def_667, type, lListConcatenateFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 81.90/20.61 thf(func_def_669, type, lListFn_THFTYPE_IiiI: ($i > $i)).
% 81.90/20.61 thf(func_def_670, type, lListFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 81.90/20.61 thf(func_def_672, type, lListLengthFn_THFTYPE_IiiI: ($i > $i)).
% 81.90/20.61 thf(func_def_674, type, lListOrderFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 81.90/20.61 thf(func_def_686, type, lMagnitudeFn_THFTYPE_IiiI: ($i > $i)).
% 81.90/20.61 thf(func_def_702, type, lMaxFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 81.90/20.61 thf(func_def_704, type, lMaximalWeightedPathFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 81.90/20.61 thf(func_def_707, type, lMeasureFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 81.90/20.61 thf(func_def_714, type, lMegaFn_THFTYPE_IiiI: ($i > $i)).
% 81.90/20.61 thf(func_def_718, type, lMereologicalDifferenceFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 81.90/20.61 thf(func_def_720, type, lMereologicalProductFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 81.90/20.61 thf(func_def_722, type, lMereologicalSumFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 81.90/20.61 thf(func_def_726, type, lMicroFn_THFTYPE_IiiI: ($i > $i)).
% 81.90/20.61 thf(func_def_733, type, lMilliFn_THFTYPE_IiiI: ($i > $i)).
% 81.90/20.61 thf(func_def_736, type, lMinFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 81.90/20.61 thf(func_def_739, type, lMinimalCutSetFn_THFTYPE_IiiI: ($i > $i)).
% 81.90/20.61 thf(func_def_741, type, lMinimalWeightedPathFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 81.90/20.61 thf(func_def_744, type, lMinuteFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 81.90/20.61 thf(func_def_756, type, lMonthFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 81.90/20.61 thf(func_def_767, type, lMultiplicationFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 81.90/20.61 thf(func_def_776, type, lNanoFn_THFTYPE_IiiI: ($i > $i)).
% 81.90/20.61 thf(func_def_836, type, lPastFn_THFTYPE_IiiI: ($i > $i)).
% 81.90/20.61 thf(func_def_839, type, lPathWeightFn_THFTYPE_IiiI: ($i > $i)).
% 81.90/20.61 thf(func_def_845, type, lPeriodicalIssueFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 81.90/20.61 thf(func_def_858, type, lPicoFn_THFTYPE_IiiI: ($i > $i)).
% 81.90/20.61 thf(func_def_886, type, lPredecessorFn_THFTYPE_IiiI: ($i > $i)).
% 81.90/20.61 thf(func_def_890, type, lPremisesFn_THFTYPE_IooI: ($o > $o)).
% 81.90/20.61 thf(func_def_898, type, lProbabilityFn_THFTYPE_IoiI: ($o > $i)).
% 81.90/20.61 thf(func_def_906, type, lPropertyFn_THFTYPE_IiiI: ($i > $i)).
% 81.90/20.61 thf(func_def_943, type, lRealNumberFn_THFTYPE_IiiI: ($i > $i)).
% 81.90/20.61 thf(func_def_947, type, lReciprocalFn_THFTYPE_IiiI: ($i > $i)).
% 81.90/20.61 thf(func_def_950, type, lRecurrentTimeIntervalFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 81.90/20.61 thf(func_def_960, type, lRelativeTimeFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 81.90/20.61 thf(func_def_965, type, lRemainderFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 81.90/20.61 thf(func_def_983, type, lRoundFn_THFTYPE_IiiI: ($i > $i)).
% 81.90/20.61 thf(func_def_990, type, lSecondFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 81.90/20.61 thf(func_def_1003, type, lSeriesVolumeFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 81.90/20.61 thf(func_def_1018, type, lSignumFn_THFTYPE_IiiI: ($i > $i)).
% 81.90/20.61 thf(func_def_1020, type, lSineFn_THFTYPE_IiiI: ($i > $i)).
% 81.90/20.61 thf(func_def_1041, type, lSpeedFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 81.90/20.61 thf(func_def_1046, type, lSquareRootFn_THFTYPE_IiiI: ($i > $i)).
% 81.90/20.61 thf(func_def_1061, type, lSubtractionFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 81.90/20.61 thf(func_def_1063, type, lSuccessorFn_THFTYPE_IiiI: ($i > $i)).
% 81.90/20.61 thf(func_def_1078, type, lTangentFn_THFTYPE_IiiI: ($i > $i)).
% 81.90/20.61 thf(func_def_1083, type, lTemporalCompositionFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 81.90/20.61 thf(func_def_1087, type, lTeraFn_THFTYPE_IiiI: ($i > $i)).
% 81.90/20.61 thf(func_def_1089, type, lTerminalNodeFn_THFTYPE_IiiI: ($i > $i)).
% 81.90/20.61 thf(func_def_1103, type, lTimeIntervalFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 81.90/20.61 thf(func_def_1138, type, lUnionFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 81.90/20.61 thf(func_def_1141, type, lUnitFn_THFTYPE_IiiI: ($i > $i)).
% 81.90/20.61 thf(func_def_1164, type, lVelocityFn_THFTYPE_IiiiiiI: ($i > $i > $i > $i > $i)).
% 81.90/20.61 thf(func_def_1188, type, lWealthFn_THFTYPE_IiiI: ($i > $i)).
% 81.90/20.61 thf(func_def_1201, type, lWhenFn_THFTYPE_IiiI: ($i > $i)).
% 81.90/20.61 thf(func_def_1203, type, lWhereFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 81.90/20.61 thf(func_def_1212, type, lYearFn_THFTYPE_IiiI: ($i > $i)).
% 81.90/20.61 thf(func_def_1216, type, larger_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_1217, type, leader_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_1218, type, legalRelation_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_1219, type, length_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_1220, type, lessThanOrEqualTo_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_1221, type, lessThan_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_1223, type, linearExtent_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_1224, type, links_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 81.90/20.61 thf(func_def_1225, type, located_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_1226, type, lt_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_1227, type, ltet_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_1228, type, manner_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_1229, type, material_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_1230, type, measure_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_1231, type, meetsSpatially_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_1232, type, meetsTemporally_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_1233, type, meltingPoint_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_1234, type, member_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_1236, type, minus_THFTYPE_IiiiI: ($i > $i > $i)).
% 81.90/20.61 thf(func_def_1237, type, modalAttribute_THFTYPE_IoioI: ($o > $i > $o)).
% 81.90/20.61 thf(func_def_1238, type, monetaryValue_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_1239, type, mother_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_1240, type, multiplicativeFactor_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_1292, type, names_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_1293, type, needs_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_1294, type, occupiesPosition_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 81.90/20.61 thf(func_def_1295, type, orientation_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 81.90/20.61 thf(func_def_1296, type, origin_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_1297, type, overlapsPartially_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_1298, type, overlapsSpatially_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_1299, type, overlapsTemporally_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_1300, type, parallel_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_1301, type, parent_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_1302, type, part_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_1303, type, partialOrderingOn_THFTYPE_IIiioIioI: (($i > $i > $o) > $i > $o)).
% 81.90/20.61 thf(func_def_1304, type, partiallyFills_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.61 thf(func_def_1305, type, partition_THFTYPE_IiiiiiiioI: ($i > $i > $i > $i > $i > $i > $i > $o)).
% 81.90/20.61 thf(func_def_1306, type, partition_THFTYPE_IiiiiiioI: ($i > $i > $i > $i > $i > $i > $o)).
% 81.90/20.61 thf(func_def_1307, type, partition_THFTYPE_IiiiiioI: ($i > $i > $i > $i > $i > $o)).
% 81.90/20.61 thf(func_def_1308, type, partition_THFTYPE_IiiiioI: ($i > $i > $i > $i > $o)).
% 81.90/20.61 thf(func_def_1309, type, partition_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 81.90/20.62 thf(func_def_1310, type, partition_THFTYPE_IioI: ($i > $o)).
% 81.90/20.62 thf(func_def_1311, type, partlyLocated_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1312, type, pathLength_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1313, type, path_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1314, type, patient_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1315, type, patient_THFTYPE_IiooI: ($i > $o > $o)).
% 81.90/20.62 thf(func_def_1316, type, penetrates_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1317, type, piece_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1318, type, plus_THFTYPE_IiiiI: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1319, type, pointOfFigure_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1320, type, pointOfIntersection_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 81.90/20.62 thf(func_def_1321, type, possesses_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1322, type, precondition_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1323, type, prefers_THFTYPE_IioooI: ($i > $o > $o > $o)).
% 81.90/20.62 thf(func_def_1324, type, premise_THFTYPE_IoooI: ($o > $o > $o)).
% 81.90/20.62 thf(func_def_1325, type, prevents_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1326, type, properPart_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1327, type, properlyFills_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1328, type, property_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1329, type, publishes_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1330, type, radius_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1331, type, rangeSubclass_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1332, type, range_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1333, type, realization_THFTYPE_IiooI: ($i > $o > $o)).
% 81.90/20.62 thf(func_def_1334, type, refers_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1335, type, reflexiveOn_THFTYPE_IIiioIioI: (($i > $i > $o) > $i > $o)).
% 81.90/20.62 thf(func_def_1336, type, relatedEvent_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1338, type, relatedInternalConcept_THFTYPE_IIIiioIIiioIoIIiioIoI: ((($i > $i > $o) > ($i > $i > $o) > $o) > ($i > $i > $o) > $o)).
% 81.90/20.62 thf(func_def_1339, type, relatedInternalConcept_THFTYPE_IIiiIioI: (($i > $i) > $i > $o)).
% 81.90/20.62 thf(func_def_1340, type, relatedInternalConcept_THFTYPE_IIiiiIioI: (($i > $i > $i) > $i > $o)).
% 81.90/20.62 thf(func_def_1341, type, relatedInternalConcept_THFTYPE_IIiiiiiioIIiioIoI: (($i > $i > $i > $i > $i > $i > $o) > ($i > $i > $o) > $o)).
% 81.90/20.62 thf(func_def_1342, type, relatedInternalConcept_THFTYPE_IIiioIIIoiIioIoI: (($i > $i > $o) > (($o > $i) > $i > $o) > $o)).
% 81.90/20.62 thf(func_def_1343, type, relatedInternalConcept_THFTYPE_IIiioIIiiiioIoI: (($i > $i > $o) > ($i > $i > $i > $i > $o) > $o)).
% 81.90/20.62 thf(func_def_1344, type, relatedInternalConcept_THFTYPE_IIiioIIiioIoI: (($i > $i > $o) > ($i > $i > $o) > $o)).
% 81.90/20.62 thf(func_def_1345, type, relatedInternalConcept_THFTYPE_IIiioIIiooIoI: (($i > $i > $o) > ($i > $o > $o) > $o)).
% 81.90/20.62 thf(func_def_1346, type, relatedInternalConcept_THFTYPE_IIiioIioI: (($i > $i > $o) > $i > $o)).
% 81.90/20.62 thf(func_def_1347, type, relatedInternalConcept_THFTYPE_IIiooIIiioIoI: (($i > $o > $o) > ($i > $i > $o) > $o)).
% 81.90/20.62 thf(func_def_1348, type, relatedInternalConcept_THFTYPE_IIiooIIiooIoI: (($i > $o > $o) > ($i > $o > $o) > $o)).
% 81.90/20.62 thf(func_def_1349, type, relatedInternalConcept_THFTYPE_IIoiioIIoiioIoI: (($o > $i > $i > $o) > ($o > $i > $i > $o) > $o)).
% 81.90/20.62 thf(func_def_1350, type, relatedInternalConcept_THFTYPE_IIoioIIoioIoI: (($o > $i > $o) > ($o > $i > $o) > $o)).
% 81.90/20.62 thf(func_def_1351, type, relatedInternalConcept_THFTYPE_IiIiiIoI: ($i > ($i > $i) > $o)).
% 81.90/20.62 thf(func_def_1352, type, relatedInternalConcept_THFTYPE_IiIiiiIoI: ($i > ($i > $i > $i) > $o)).
% 81.90/20.62 thf(func_def_1353, type, relatedInternalConcept_THFTYPE_IiIiioIoI: ($i > ($i > $i > $o) > $o)).
% 81.90/20.62 thf(func_def_1354, type, relatedInternalConcept_THFTYPE_IiIiooIoI: ($i > ($i > $o > $o) > $o)).
% 81.90/20.62 thf(func_def_1355, type, relatedInternalConcept_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1356, type, relative_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1357, type, representsForAgent_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 81.90/20.62 thf(func_def_1358, type, representsInLanguage_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 81.90/20.62 thf(func_def_1359, type, represents_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1360, type, resource_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1361, type, result_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1362, type, sibling_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1363, type, side_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1365, type, smaller_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1366, type, son_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1367, type, spouse_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1368, type, starts_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1370, type, subAttribute_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1371, type, subCollection_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1372, type, subGraph_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1373, type, subList_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1374, type, subOrganization_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1376, type, subProcess_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1377, type, subProposition_THFTYPE_IoooI: ($o > $o > $o)).
% 81.90/20.62 thf(func_def_1378, type, subSystem_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1379, type, subclass_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1380, type, subrelation_THFTYPE_IIiiioIIiiioIoI: (($i > $i > $i > $o) > ($i > $i > $i > $o) > $o)).
% 81.90/20.62 thf(func_def_1381, type, subrelation_THFTYPE_IIiioIIIoiIioIoI: (($i > $i > $o) > (($o > $i) > $i > $o) > $o)).
% 81.90/20.62 thf(func_def_1382, type, subrelation_THFTYPE_IIiioIIIooIioIoI: (($i > $i > $o) > (($o > $o) > $i > $o) > $o)).
% 81.90/20.62 thf(func_def_1383, type, subrelation_THFTYPE_IIiioIIiioIoI: (($i > $i > $o) > ($i > $i > $o) > $o)).
% 81.90/20.62 thf(func_def_1384, type, subrelation_THFTYPE_IIiioIIiooIoI: (($i > $i > $o) > ($i > $o > $o) > $o)).
% 81.90/20.62 thf(func_def_1385, type, subrelation_THFTYPE_IIiioIioI: (($i > $i > $o) > $i > $o)).
% 81.90/20.62 thf(func_def_1386, type, subrelation_THFTYPE_IIioIIioIoI: (($i > $o) > ($i > $o) > $o)).
% 81.90/20.62 thf(func_def_1387, type, subrelation_THFTYPE_IIiooIIiioIoI: (($i > $o > $o) > ($i > $i > $o) > $o)).
% 81.90/20.62 thf(func_def_1388, type, subrelation_THFTYPE_IIoioIIiioIoI: (($o > $i > $o) > ($i > $i > $o) > $o)).
% 81.90/20.62 thf(func_def_1389, type, subrelation_THFTYPE_IIoooIIiioIoI: (($o > $o > $o) > ($i > $i > $o) > $o)).
% 81.90/20.62 thf(func_def_1390, type, subrelation_THFTYPE_IiIiioIoI: ($i > ($i > $i > $o) > $o)).
% 81.90/20.62 thf(func_def_1391, type, subrelation_THFTYPE_IiIoooIoI: ($i > ($o > $o > $o) > $o)).
% 81.90/20.62 thf(func_def_1392, type, subrelation_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1393, type, subset_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1395, type, subsumesContentClass_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1396, type, subsumesContentInstance_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1397, type, subsumesContentInstance_THFTYPE_IiooI: ($i > $o > $o)).
% 81.90/20.62 thf(func_def_1399, type, successorAttributeClosure_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1400, type, successorAttribute_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1401, type, superficialPart_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1402, type, surface_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1404, type, systemPart_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1405, type, temporalPart_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1406, type, temporallyBetweenOrEqual_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 81.90/20.62 thf(func_def_1407, type, temporallyBetween_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 81.90/20.62 thf(func_def_1408, type, time_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1409, type, times_THFTYPE_IiiiI: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1410, type, top_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1411, type, totalOrderingOn_THFTYPE_IIiioIioI: (($i > $i > $o) > $i > $o)).
% 81.90/20.62 thf(func_def_1412, type, transactionAmount_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1413, type, traverses_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1414, type, trichotomizingOn_THFTYPE_IIiioIioI: (($i > $i > $o) > $i > $o)).
% 81.90/20.62 thf(func_def_1415, type, truth_THFTYPE_IoooI: ($o > $o > $o)).
% 81.90/20.62 thf(func_def_1416, type, typicalPart_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1417, type, typicallyContainsPart_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1419, type, uses_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1420, type, valence_THFTYPE_IIiioIioI: (($i > $i > $o) > $i > $o)).
% 81.90/20.62 thf(func_def_1421, type, valence_THFTYPE_IIioIioI: (($i > $o) > $i > $o)).
% 81.90/20.62 thf(func_def_1422, type, valence_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1423, type, version_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1424, type, wants_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1425, type, wears_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1427, type, width_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1428, type, wife_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1430, type, vNOT: ($o > $o)).
% 81.90/20.62 thf(func_def_1434, type, likes_THFTYPE_IiioI: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1438, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 81.90/20.62 thf(func_def_1439, type, db0: !>[X0: $tType]:(X0)).
% 81.90/20.62 thf(func_def_1440, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 81.90/20.62 thf(func_def_1441, type, vAND: ($o > $o > $o)).
% 81.90/20.62 thf(func_def_1442, type, db1: !>[X0: $tType]:(X0)).
% 81.90/20.62 thf(func_def_1443, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 81.90/20.62 thf(func_def_1444, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 81.90/20.62 thf(func_def_1445, type, vIMP: ($o > $o > $o)).
% 81.90/20.62 thf(func_def_1446, type, db2: !>[X0: $tType]:(X0)).
% 81.90/20.62 thf(func_def_1447, type, vOR: ($o > $o > $o)).
% 81.90/20.62 thf(func_def_1448, type, sP0: ($i > $o)).
% 81.90/20.62 thf(func_def_1449, type, sP1: (($i > $i > $o) > $i > $i > $o)).
% 81.90/20.62 thf(func_def_1450, type, sP2: (($i > $i > $o) > $i > $i > $o)).
% 81.90/20.62 thf(func_def_1451, type, sP3: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1452, type, sP4: ($i > $o)).
% 81.90/20.62 thf(func_def_1453, type, sP5: ($i > $o)).
% 81.90/20.62 thf(func_def_1454, type, sK6: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1455, type, sK7: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1456, type, sK8: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1457, type, sK9: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1458, type, sK10: ($i > $i)).
% 81.90/20.62 thf(func_def_1459, type, sK11: ($i > $i)).
% 81.90/20.62 thf(func_def_1460, type, sK12: ($i > $i)).
% 81.90/20.62 thf(func_def_1461, type, sK13: ($i > $i)).
% 81.90/20.62 thf(func_def_1462, type, sK14: ($i > $i)).
% 81.90/20.62 thf(func_def_1463, type, sK15: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1464, type, sK16: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1465, type, sK17: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1466, type, sK18: ($i > $i > $i > $i)).
% 81.90/20.62 thf(func_def_1467, type, sK19: ($i > $i)).
% 81.90/20.62 thf(func_def_1468, type, sK20: ($i > $i)).
% 81.90/20.62 thf(func_def_1469, type, sK21: ($i > $i)).
% 81.90/20.62 thf(func_def_1470, type, sK22: ($i > $i)).
% 81.90/20.62 thf(func_def_1471, type, sK23: ($i > $i)).
% 81.90/20.62 thf(func_def_1472, type, sK24: ($i > $i)).
% 81.90/20.62 thf(func_def_1473, type, sK25: ($i > $i)).
% 81.90/20.62 thf(func_def_1474, type, sK26: ($i > $i)).
% 81.90/20.62 thf(func_def_1475, type, sK27: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1476, type, sK28: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1477, type, sK29: ($i > $i)).
% 81.90/20.62 thf(func_def_1478, type, sK30: ($i > $i)).
% 81.90/20.62 thf(func_def_1479, type, sK31: ($i > $i)).
% 81.90/20.62 thf(func_def_1480, type, sK32: ($i > $i)).
% 81.90/20.62 thf(func_def_1481, type, sK33: ($i > $o)).
% 81.90/20.62 thf(func_def_1482, type, sK34: ($i > $i)).
% 81.90/20.62 thf(func_def_1483, type, sK35: ($i > $i)).
% 81.90/20.62 thf(func_def_1484, type, sK36: ($i > $i)).
% 81.90/20.62 thf(func_def_1485, type, sK37: ($i > $o)).
% 81.90/20.62 thf(func_def_1486, type, sK38: ($i > $i)).
% 81.90/20.62 thf(func_def_1487, type, sK39: ($i > $i > $i > $i)).
% 81.90/20.62 thf(func_def_1488, type, sK40: ($i > $i)).
% 81.90/20.62 thf(func_def_1489, type, sK41: ($i > $i)).
% 81.90/20.62 thf(func_def_1490, type, sK42: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1491, type, sK43: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1492, type, sK44: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1493, type, sK45: ($i > $i)).
% 81.90/20.62 thf(func_def_1494, type, sK46: ($i > $i)).
% 81.90/20.62 thf(func_def_1495, type, sK47: ($i > $i > $i > $i)).
% 81.90/20.62 thf(func_def_1496, type, sK48: ($i > $i)).
% 81.90/20.62 thf(func_def_1497, type, sK49: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1498, type, sK50: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1499, type, sK51: ($i > $i)).
% 81.90/20.62 thf(func_def_1500, type, sK52: ($i > $o)).
% 81.90/20.62 thf(func_def_1501, type, sK53: ($i > $o)).
% 81.90/20.62 thf(func_def_1502, type, sK54: ($i > $i)).
% 81.90/20.62 thf(func_def_1503, type, sK55: ($i > $i)).
% 81.90/20.62 thf(func_def_1504, type, sK56: ($i > $i)).
% 81.90/20.62 thf(func_def_1505, type, sK57: ($i > $i)).
% 81.90/20.62 thf(func_def_1506, type, sK58: ($i > $i)).
% 81.90/20.62 thf(func_def_1507, type, sK59: ($i > $i)).
% 81.90/20.62 thf(func_def_1508, type, sK60: ($i > $i)).
% 81.90/20.62 thf(func_def_1509, type, sK61: ($i > $i > $i > $i)).
% 81.90/20.62 thf(func_def_1510, type, sK62: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1511, type, sK63: ($i > $i)).
% 81.90/20.62 thf(func_def_1512, type, sK64: ($i > $o)).
% 81.90/20.62 thf(func_def_1513, type, sK65: ($i > $i > $i > $i)).
% 81.90/20.62 thf(func_def_1514, type, sK66: ($i > $i > $i > $i)).
% 81.90/20.62 thf(func_def_1515, type, sK67: (($i > $i > $o) > $i)).
% 81.90/20.62 thf(func_def_1516, type, sK68: (($i > $i > $o) > $i)).
% 81.90/20.62 thf(func_def_1517, type, sK69: ($i > $i)).
% 81.90/20.62 thf(func_def_1518, type, sK70: ($i > $i > $i > $i)).
% 81.90/20.62 thf(func_def_1519, type, sK71: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1520, type, sK72: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1521, type, sK73: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1522, type, sK74: ($i > $i)).
% 81.90/20.62 thf(func_def_1523, type, sK75: ($i > $i)).
% 81.90/20.62 thf(func_def_1524, type, sK76: ($i > $i)).
% 81.90/20.62 thf(func_def_1525, type, sK77: ($i > $i)).
% 81.90/20.62 thf(func_def_1526, type, sK78: ($i > $i)).
% 81.90/20.62 thf(func_def_1527, type, sK79: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1528, type, sK80: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1529, type, sK81: ($i > $i)).
% 81.90/20.62 thf(func_def_1530, type, sK82: ($i > $i)).
% 81.90/20.62 thf(func_def_1531, type, sK83: ($i > $i)).
% 81.90/20.62 thf(func_def_1532, type, sK84: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1533, type, sK85: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1534, type, sK86: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1535, type, sK87: ($i > $i > $i > $i)).
% 81.90/20.62 thf(func_def_1536, type, sK88: ($i > $i > $i > $i)).
% 81.90/20.62 thf(func_def_1537, type, sK89: ($i > $i)).
% 81.90/20.62 thf(func_def_1538, type, sK90: ($i > $i)).
% 81.90/20.62 thf(func_def_1539, type, sK91: ($i > $i)).
% 81.90/20.62 thf(func_def_1540, type, sK92: ($i > $i)).
% 81.90/20.62 thf(func_def_1541, type, sK93: ($i > $i)).
% 81.90/20.62 thf(func_def_1542, type, sK94: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1543, type, sK95: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1544, type, sK96: ($i > $i)).
% 81.90/20.62 thf(func_def_1545, type, sK97: ($i > $i)).
% 81.90/20.62 thf(func_def_1546, type, sK98: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1547, type, sK99: ($i > $o > $i > $i)).
% 81.90/20.62 thf(func_def_1548, type, sK100: ($i > $o > $i > $i)).
% 81.90/20.62 thf(func_def_1549, type, sK101: ($i > $o > $i > $i)).
% 81.90/20.62 thf(func_def_1550, type, sK102: (($i > $i > $o) > $i)).
% 81.90/20.62 thf(func_def_1551, type, sK103: (($i > $i > $o) > $i)).
% 81.90/20.62 thf(func_def_1552, type, sK104: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1553, type, sK105: ($i > $i)).
% 81.90/20.62 thf(func_def_1554, type, sK106: ($i > $i)).
% 81.90/20.62 thf(func_def_1555, type, sK107: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1556, type, sK108: ($i > $i)).
% 81.90/20.62 thf(func_def_1557, type, sK109: ($i > $i)).
% 81.90/20.62 thf(func_def_1558, type, sK110: ($i > $i)).
% 81.90/20.62 thf(func_def_1559, type, sK111: ($i > $i)).
% 81.90/20.62 thf(func_def_1560, type, sK112: ($i > $i > $i > $i)).
% 81.90/20.62 thf(func_def_1561, type, sK113: ($i > $i)).
% 81.90/20.62 thf(func_def_1562, type, sK114: ($i > $i)).
% 81.90/20.62 thf(func_def_1563, type, sK115: ($i > $i)).
% 81.90/20.62 thf(func_def_1564, type, sK116: ($i > $i)).
% 81.90/20.62 thf(func_def_1565, type, sK117: ($i > $i)).
% 81.90/20.62 thf(func_def_1566, type, sK118: ($i > $i > $i > $i)).
% 81.90/20.62 thf(func_def_1567, type, sK119: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1568, type, sK120: ($i > $i > $i > $i)).
% 81.90/20.62 thf(func_def_1569, type, sK121: ($i > $i > $i > $i)).
% 81.90/20.62 thf(func_def_1570, type, sK122: ($i > $i)).
% 81.90/20.62 thf(func_def_1571, type, sK123: ($i > $i)).
% 81.90/20.62 thf(func_def_1572, type, sK124: ($i > $i)).
% 81.90/20.62 thf(func_def_1573, type, sK125: ($i > $i)).
% 81.90/20.62 thf(func_def_1574, type, sK126: ($i > $i)).
% 81.90/20.62 thf(func_def_1575, type, sK127: ($i > $i)).
% 81.90/20.62 thf(func_def_1576, type, sK128: ($i > $o)).
% 81.90/20.62 thf(func_def_1577, type, sK129: ($i > $i)).
% 81.90/20.62 thf(func_def_1578, type, sK130: ($i > $i)).
% 81.90/20.62 thf(func_def_1579, type, sK131: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1580, type, sK132: ($i > $i)).
% 81.90/20.62 thf(func_def_1581, type, sK133: ($i > $i)).
% 81.90/20.62 thf(func_def_1582, type, sK134: ($i > $i)).
% 81.90/20.62 thf(func_def_1583, type, sK135: ($i > $i)).
% 81.90/20.62 thf(func_def_1584, type, sK136: ($i > $i)).
% 81.90/20.62 thf(func_def_1585, type, sK137: ($i > $o)).
% 81.90/20.62 thf(func_def_1586, type, sK138: ($i > $o)).
% 81.90/20.62 thf(func_def_1587, type, sK139: ($i > $i)).
% 81.90/20.62 thf(func_def_1588, type, sK140: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1589, type, sK141: ($i > $i)).
% 81.90/20.62 thf(func_def_1590, type, sK142: ($i > $i)).
% 81.90/20.62 thf(func_def_1591, type, sK143: ($i > $i)).
% 81.90/20.62 thf(func_def_1592, type, sK144: ($i > $i)).
% 81.90/20.62 thf(func_def_1593, type, sK145: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1594, type, sK146: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1595, type, sK147: ($i > $i)).
% 81.90/20.62 thf(func_def_1596, type, sK148: ($i > $i)).
% 81.90/20.62 thf(func_def_1597, type, sK149: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1598, type, sK150: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1599, type, sK151: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1600, type, sK152: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1601, type, sK153: ($i > $o)).
% 81.90/20.62 thf(func_def_1602, type, sK154: ($i > $i)).
% 81.90/20.62 thf(func_def_1603, type, sK155: ($i > $o)).
% 81.90/20.62 thf(func_def_1604, type, sK156: ($i > $i)).
% 81.90/20.62 thf(func_def_1605, type, sK157: ($i > $i)).
% 81.90/20.62 thf(func_def_1606, type, sK158: ($i > $i)).
% 81.90/20.62 thf(func_def_1607, type, sK159: ($i > $i)).
% 81.90/20.62 thf(func_def_1608, type, sK160: ($i > $i)).
% 81.90/20.62 thf(func_def_1609, type, sK161: ($i > $i)).
% 81.90/20.62 thf(func_def_1610, type, sK162: ($i > $i)).
% 81.90/20.62 thf(func_def_1611, type, sK163: ($i > $i > $i > $i > $o)).
% 81.90/20.62 thf(func_def_1612, type, sK164: ($i > $i)).
% 81.90/20.62 thf(func_def_1613, type, sK165: ($i > $i)).
% 81.90/20.62 thf(func_def_1614, type, sK166: ($i > $i)).
% 81.90/20.62 thf(func_def_1615, type, sK167: ($i > $i)).
% 81.90/20.62 thf(func_def_1616, type, sK168: ($i > $i > $i > $i)).
% 81.90/20.62 thf(func_def_1617, type, sK169: ($i > $i > $i > $i)).
% 81.90/20.62 thf(func_def_1618, type, sK170: ($i > $i)).
% 81.90/20.62 thf(func_def_1619, type, sK171: ($i > $i)).
% 81.90/20.62 thf(func_def_1620, type, sK172: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1621, type, sK173: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1622, type, sK174: ($i > $i)).
% 81.90/20.62 thf(func_def_1623, type, sK175: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1624, type, sK176: ($i > $i)).
% 81.90/20.62 thf(func_def_1625, type, sK177: ($i > $i)).
% 81.90/20.62 thf(func_def_1626, type, sK178: ($i > $i)).
% 81.90/20.62 thf(func_def_1627, type, sK179: ($i > $i)).
% 81.90/20.62 thf(func_def_1628, type, sK180: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1629, type, sK181: ($i > $i)).
% 81.90/20.62 thf(func_def_1630, type, sK182: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1631, type, sK183: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1632, type, sK184: ($i > $i)).
% 81.90/20.62 thf(func_def_1633, type, sK185: ($i > $i)).
% 81.90/20.62 thf(func_def_1634, type, sK186: ($i > $i)).
% 81.90/20.62 thf(func_def_1635, type, sK187: ($i > $i)).
% 81.90/20.62 thf(func_def_1636, type, sK188: ($i > $i)).
% 81.90/20.62 thf(func_def_1637, type, sK189: ($i > $i)).
% 81.90/20.62 thf(func_def_1638, type, sK190: ($i > $i)).
% 81.90/20.62 thf(func_def_1639, type, sK191: ($i > $i)).
% 81.90/20.62 thf(func_def_1640, type, sK192: ($i > $i)).
% 81.90/20.62 thf(func_def_1641, type, sK193: ($i > $i)).
% 81.90/20.62 thf(func_def_1642, type, sK194: ($i > $i)).
% 81.90/20.62 thf(func_def_1643, type, sK195: ($i > $i)).
% 81.90/20.62 thf(func_def_1644, type, sK196: ($i > $i)).
% 81.90/20.62 thf(func_def_1645, type, sK197: ($i > $i)).
% 81.90/20.62 thf(func_def_1646, type, sK198: ($i > $i)).
% 81.90/20.62 thf(func_def_1647, type, sK199: ($i > $i)).
% 81.90/20.62 thf(func_def_1648, type, sK200: ($i > $i)).
% 81.90/20.62 thf(func_def_1649, type, sK201: ($i > $i)).
% 81.90/20.62 thf(func_def_1650, type, sK202: ($i > $i)).
% 81.90/20.62 thf(func_def_1651, type, sK203: (($i > $i > $o) > $i > $i)).
% 81.90/20.62 thf(func_def_1652, type, sK204: (($i > $i > $o) > $i > $i)).
% 81.90/20.62 thf(func_def_1653, type, sK205: (($i > $i > $o) > $i > $i)).
% 81.90/20.62 thf(func_def_1654, type, sK206: (($i > $i > $o) > $i > $i)).
% 81.90/20.62 thf(func_def_1655, type, sK207: (($i > $i > $o) > $i > $i)).
% 81.90/20.62 thf(func_def_1656, type, sK208: ($i > $i)).
% 81.90/20.62 thf(func_def_1657, type, sK209: ($i > $o > $i)).
% 81.90/20.62 thf(func_def_1658, type, sK210: ($i > $i)).
% 81.90/20.62 thf(func_def_1659, type, sK211: ($i > $i)).
% 81.90/20.62 thf(func_def_1660, type, sK212: ($i > $i)).
% 81.90/20.62 thf(func_def_1661, type, sK213: ($i > $i)).
% 81.90/20.62 thf(func_def_1662, type, sK214: ($i > $i)).
% 81.90/20.62 thf(func_def_1663, type, sK215: ($i > $i)).
% 81.90/20.62 thf(func_def_1664, type, sK216: ($i > $i > $i > $o)).
% 81.90/20.62 thf(func_def_1665, type, sK217: ($o > $i > $i)).
% 81.90/20.62 thf(func_def_1666, type, sK218: ($i > $i)).
% 81.90/20.62 thf(func_def_1667, type, sK219: ($i > $i)).
% 81.90/20.62 thf(func_def_1668, type, sK220: ($i > $i)).
% 81.90/20.62 thf(func_def_1669, type, sK221: ($i > $i)).
% 81.90/20.62 thf(func_def_1670, type, sK222: ($o > $i > $i)).
% 81.90/20.62 thf(func_def_1671, type, sK223: ($i > $i > $i > $i)).
% 81.90/20.62 thf(func_def_1672, type, sK224: ($i > $i)).
% 81.90/20.62 thf(func_def_1673, type, sK225: ($i > $i)).
% 81.90/20.62 thf(func_def_1674, type, sK226: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1675, type, sK227: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1676, type, sK228: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1677, type, sK229: ($i > $i)).
% 81.90/20.62 thf(func_def_1678, type, sK230: ($i > $i)).
% 81.90/20.62 thf(func_def_1679, type, sK231: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1680, type, sK232: ($i > $i)).
% 81.90/20.62 thf(func_def_1681, type, sK233: ($i > $i)).
% 81.90/20.62 thf(func_def_1682, type, sK234: ($i > $i)).
% 81.90/20.62 thf(func_def_1683, type, sK235: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1684, type, sK236: ($i > $i > $i > $i > $i)).
% 81.90/20.62 thf(func_def_1685, type, sK237: ($i > $i)).
% 81.90/20.62 thf(func_def_1686, type, sK238: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1687, type, sK239: ($i > $i)).
% 81.90/20.62 thf(func_def_1688, type, sK240: ($i > $i)).
% 81.90/20.62 thf(func_def_1689, type, sK241: ($i > $o)).
% 81.90/20.62 thf(func_def_1690, type, sK242: ($i > $i)).
% 81.90/20.62 thf(func_def_1691, type, sK243: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1692, type, sK244: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1693, type, sK245: ($i > $i)).
% 81.90/20.62 thf(func_def_1694, type, sK246: ($i > $i)).
% 81.90/20.62 thf(func_def_1695, type, sK247: ($i > $i)).
% 81.90/20.62 thf(func_def_1696, type, sK248: ($i > $i)).
% 81.90/20.62 thf(func_def_1697, type, sK249: ($i > $i)).
% 81.90/20.62 thf(func_def_1698, type, sK250: ($i > $i)).
% 81.90/20.62 thf(func_def_1699, type, sK251: ($i > $o)).
% 81.90/20.62 thf(func_def_1700, type, sK252: ($i > $i)).
% 81.90/20.62 thf(func_def_1701, type, sK253: ($i > $i > $o)).
% 81.90/20.62 thf(func_def_1702, type, sK254: ($i > $i)).
% 81.90/20.62 thf(func_def_1703, type, sK255: ($i > $i)).
% 81.90/20.62 thf(func_def_1704, type, sK256: ($i > $i)).
% 81.90/20.62 thf(func_def_1705, type, sK257: ($i > $i)).
% 81.90/20.62 thf(func_def_1706, type, sK258: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1707, type, sK259: ($i > $o)).
% 81.90/20.62 thf(func_def_1708, type, sK260: ($i > $i)).
% 81.90/20.62 thf(func_def_1709, type, sK261: ($i > $i)).
% 81.90/20.62 thf(func_def_1710, type, sK262: ($i > $i)).
% 81.90/20.62 thf(func_def_1711, type, sK263: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1712, type, sK264: ($i > $i)).
% 81.90/20.62 thf(func_def_1713, type, sK265: ($i > $i)).
% 81.90/20.62 thf(func_def_1714, type, sK266: ($i > $i)).
% 81.90/20.62 thf(func_def_1715, type, sK267: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1716, type, sK268: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1717, type, sK269: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1718, type, sK270: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1719, type, sK271: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1720, type, sK272: ($i > $i > $i > $i)).
% 81.90/20.62 thf(func_def_1721, type, sK273: ($i > $i > $i > $i)).
% 81.90/20.62 thf(func_def_1722, type, sK274: ($i > $i)).
% 81.90/20.62 thf(func_def_1723, type, sK275: ($i > $i)).
% 81.90/20.62 thf(func_def_1724, type, sK276: ($i > $i)).
% 81.90/20.62 thf(func_def_1725, type, sK277: ($i > $i)).
% 81.90/20.62 thf(func_def_1726, type, sK278: ($i > $i)).
% 81.90/20.62 thf(func_def_1727, type, sK279: ($i > $i)).
% 81.90/20.62 thf(func_def_1728, type, sK280: ($i > $i)).
% 81.90/20.62 thf(func_def_1729, type, sK281: ($i > $i)).
% 81.90/20.62 thf(func_def_1730, type, sK282: ($i > $i)).
% 81.90/20.62 thf(func_def_1731, type, sK283: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1732, type, sK284: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1733, type, sK285: ($i > $i)).
% 81.90/20.62 thf(func_def_1734, type, sK286: ($i > $i)).
% 81.90/20.62 thf(func_def_1735, type, sK287: ($i > $i)).
% 81.90/20.62 thf(func_def_1736, type, sK288: ($i > $i)).
% 81.90/20.62 thf(func_def_1737, type, sK289: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1738, type, sK290: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1739, type, sK291: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1740, type, sK292: (($i > $i > $o) > $i)).
% 81.90/20.62 thf(func_def_1741, type, sK293: (($i > $i > $o) > $i)).
% 81.90/20.62 thf(func_def_1742, type, sK294: ($i > $i)).
% 81.90/20.62 thf(func_def_1743, type, sK295: (($i > $i > $o) > $i)).
% 81.90/20.62 thf(func_def_1744, type, sK296: (($i > $i > $o) > $i)).
% 81.90/20.62 thf(func_def_1745, type, sK297: (($i > $i > $o) > $i)).
% 81.90/20.62 thf(func_def_1746, type, sK298: ($i > $i)).
% 81.90/20.62 thf(func_def_1747, type, sK299: ($i > $i)).
% 81.90/20.62 thf(func_def_1748, type, sK300: ($i > $i)).
% 81.90/20.62 thf(func_def_1749, type, sK301: ($i > $i)).
% 81.90/20.62 thf(func_def_1750, type, sK302: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1751, type, sK303: ($i > $i)).
% 81.90/20.62 thf(func_def_1752, type, sK304: ($i > $i)).
% 81.90/20.62 thf(func_def_1753, type, sK305: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1754, type, sK306: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1755, type, sK307: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1756, type, sK308: ($i > $o)).
% 81.90/20.62 thf(func_def_1757, type, sK309: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1758, type, sK310: ($i > $i)).
% 81.90/20.62 thf(func_def_1759, type, sK311: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1760, type, sK312: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1761, type, sK313: ($i > $i)).
% 81.90/20.62 thf(func_def_1762, type, sK314: ($i > $i)).
% 81.90/20.62 thf(func_def_1763, type, sK315: ($i > $o)).
% 81.90/20.62 thf(func_def_1764, type, sK316: ($i > $i)).
% 81.90/20.62 thf(func_def_1765, type, sK317: ($i > $i)).
% 81.90/20.62 thf(func_def_1766, type, sK318: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1767, type, sK319: ($i > $i)).
% 81.90/20.62 thf(func_def_1768, type, sK320: ($i > $i)).
% 81.90/20.62 thf(func_def_1769, type, sK321: ($i > $i)).
% 81.90/20.62 thf(func_def_1770, type, sK322: ($i > $i)).
% 81.90/20.62 thf(func_def_1771, type, sK323: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1772, type, sK324: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1773, type, sK325: ($i > $i)).
% 81.90/20.62 thf(func_def_1774, type, sK326: ($i > $i)).
% 81.90/20.62 thf(func_def_1775, type, sK327: ($i > $i)).
% 81.90/20.62 thf(func_def_1776, type, sK328: ($o > $i > $i)).
% 81.90/20.62 thf(func_def_1777, type, sK329: ($i > $i)).
% 81.90/20.62 thf(func_def_1778, type, sK330: ($i > $i)).
% 81.90/20.62 thf(func_def_1779, type, sK331: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1781, type, sK333: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1782, type, sK334: ($i > $i > $i > $i)).
% 81.90/20.62 thf(func_def_1783, type, sK335: ($i > $i > $i > $i)).
% 81.90/20.62 thf(func_def_1784, type, sK336: ($i > $i)).
% 81.90/20.62 thf(func_def_1785, type, sK337: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1786, type, sK338: ($i > $i)).
% 81.90/20.62 thf(func_def_1787, type, sK339: ($i > $i)).
% 81.90/20.62 thf(func_def_1788, type, sK340: ($i > $i)).
% 81.90/20.62 thf(func_def_1789, type, sK341: ($i > $i)).
% 81.90/20.62 thf(func_def_1790, type, sK342: ($i > $i)).
% 81.90/20.62 thf(func_def_1791, type, sK343: ($i > $i > $i > $i)).
% 81.90/20.62 thf(func_def_1792, type, sK344: ($i > $i)).
% 81.90/20.62 thf(func_def_1793, type, sK345: ($i > $i > $i > $i > $i)).
% 81.90/20.62 thf(func_def_1794, type, sK346: ($i > $i)).
% 81.90/20.62 thf(func_def_1795, type, sK347: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1796, type, sK348: ($i > $i)).
% 81.90/20.62 thf(func_def_1797, type, sK349: ($i > $i)).
% 81.90/20.62 thf(func_def_1798, type, sK350: ($i > $i > $i > $i)).
% 81.90/20.62 thf(func_def_1799, type, sK351: ($i > $i > $i > $i)).
% 81.90/20.62 thf(func_def_1800, type, sK352: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1801, type, sK353: ($i > $i > $i > $i)).
% 81.90/20.62 thf(func_def_1802, type, sK354: ($i > $i)).
% 81.90/20.62 thf(func_def_1803, type, sK355: ($i > $i)).
% 81.90/20.62 thf(func_def_1804, type, sK356: ($i > $i)).
% 81.90/20.62 thf(func_def_1805, type, sK357: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1806, type, sK358: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1807, type, sK359: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1808, type, sK360: ($i > $i)).
% 81.90/20.62 thf(func_def_1809, type, sK361: ($i > $i)).
% 81.90/20.62 thf(func_def_1810, type, sK362: ($i > $i)).
% 81.90/20.62 thf(func_def_1811, type, sK363: ($i > $i > $i > $i > $i > $i)).
% 81.90/20.62 thf(func_def_1812, type, sK364: ($i > $i > $i > $i)).
% 81.90/20.62 thf(func_def_1813, type, sK365: ($i > $i)).
% 81.90/20.62 thf(func_def_1814, type, sK366: ($i > $i)).
% 81.90/20.62 thf(func_def_1815, type, sK367: ($i > $i > $i > $i)).
% 81.90/20.62 thf(func_def_1816, type, sK368: ($i > $i)).
% 81.90/20.62 thf(func_def_1817, type, sK369: ($i > $i)).
% 81.90/20.62 thf(func_def_1818, type, sK370: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1819, type, sK371: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1820, type, sK372: ($i > $i)).
% 81.90/20.62 thf(func_def_1821, type, sK373: ($i > $i)).
% 81.90/20.62 thf(func_def_1822, type, sK374: ($i > $i)).
% 81.90/20.62 thf(func_def_1823, type, sK375: ($i > $i)).
% 81.90/20.62 thf(func_def_1824, type, sK376: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1825, type, sK377: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1826, type, sK378: ($i > $i)).
% 81.90/20.62 thf(func_def_1827, type, sK379: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1828, type, sK380: ($i > $i)).
% 81.90/20.62 thf(func_def_1829, type, sK381: ($i > $i)).
% 81.90/20.62 thf(func_def_1830, type, sK382: ($i > $i)).
% 81.90/20.62 thf(func_def_1831, type, sK383: (($i > $i > $o) > $i)).
% 81.90/20.62 thf(func_def_1832, type, sK384: ($i > $i > $i > $i)).
% 81.90/20.62 thf(func_def_1833, type, sK385: ($i > $i)).
% 81.90/20.62 thf(func_def_1834, type, sK386: ($i > $i)).
% 81.90/20.62 thf(func_def_1835, type, sK387: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1836, type, sK388: ($i > $i > $i > $i)).
% 81.90/20.62 thf(func_def_1837, type, sK389: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1838, type, sK390: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1839, type, sK391: ($i > $i)).
% 81.90/20.62 thf(func_def_1840, type, sK392: ($i > $i)).
% 81.90/20.62 thf(func_def_1841, type, sK393: ($i > $i)).
% 81.90/20.62 thf(func_def_1842, type, sK394: ($i > $i)).
% 81.90/20.62 thf(func_def_1843, type, sK395: ($i > $i)).
% 81.90/20.62 thf(func_def_1844, type, sK396: ($i > $i)).
% 81.90/20.62 thf(func_def_1845, type, sK397: ($i > $i)).
% 81.90/20.62 thf(func_def_1846, type, sK398: ($i > $i)).
% 81.90/20.62 thf(func_def_1847, type, sK399: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1848, type, sK400: ($i > $i)).
% 81.90/20.62 thf(func_def_1849, type, sK401: ($i > $i)).
% 81.90/20.62 thf(func_def_1850, type, sK402: ($i > $i)).
% 81.90/20.62 thf(func_def_1851, type, sK403: ($i > $i)).
% 81.90/20.62 thf(func_def_1852, type, sK404: ($i > $i)).
% 81.90/20.62 thf(func_def_1853, type, sK405: ($i > $i)).
% 81.90/20.62 thf(func_def_1854, type, sK406: ($i > $i)).
% 81.90/20.62 thf(func_def_1855, type, sK407: ($i > $i)).
% 81.90/20.62 thf(func_def_1856, type, sK408: ($i > $i)).
% 81.90/20.62 thf(func_def_1857, type, sK409: ($i > $i)).
% 81.90/20.62 thf(func_def_1858, type, sK410: ($i > $i)).
% 81.90/20.62 thf(func_def_1859, type, sK411: ($i > $i)).
% 81.90/20.62 thf(func_def_1860, type, sK412: ($i > $i)).
% 81.90/20.62 thf(func_def_1861, type, sK413: ($i > $i)).
% 81.90/20.62 thf(func_def_1862, type, sK414: ($i > $i > $i > $i)).
% 81.90/20.62 thf(func_def_1863, type, sK415: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1864, type, sK416: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1865, type, sK417: ($i > $o > $i)).
% 81.90/20.62 thf(func_def_1866, type, sK418: ($i > $i)).
% 81.90/20.62 thf(func_def_1867, type, sK419: ($i > $i)).
% 81.90/20.62 thf(func_def_1868, type, sK420: ($i > $i)).
% 81.90/20.62 thf(func_def_1869, type, sK421: ($i > $i)).
% 81.90/20.62 thf(func_def_1870, type, sK422: ($i > $i)).
% 81.90/20.62 thf(func_def_1871, type, sK423: ($o > $o > $i)).
% 81.90/20.62 thf(func_def_1872, type, sK424: ($o > $o > $i)).
% 81.90/20.62 thf(func_def_1873, type, sK425: (($i > $i > $o) > $i)).
% 81.90/20.62 thf(func_def_1874, type, sK426: (($i > $i > $o) > $i)).
% 81.90/20.62 thf(func_def_1875, type, sK427: (($i > $i > $o) > $i)).
% 81.90/20.62 thf(func_def_1876, type, sK428: (($i > $i > $o) > $i)).
% 81.90/20.62 thf(func_def_1877, type, sK429: (($i > $i > $o) > $i)).
% 81.90/20.62 thf(func_def_1878, type, sK430: ($i > $i)).
% 81.90/20.62 thf(func_def_1879, type, sK431: ($i > $i)).
% 81.90/20.62 thf(func_def_1880, type, sK432: ($i > $i)).
% 81.90/20.62 thf(func_def_1881, type, sK433: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1882, type, sK434: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1883, type, sK435: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1884, type, sK436: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1885, type, sK437: ($i > $i)).
% 81.90/20.62 thf(func_def_1886, type, sK438: ($i > $i)).
% 81.90/20.62 thf(func_def_1887, type, sK439: ($i > $i)).
% 81.90/20.62 thf(func_def_1888, type, sK440: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1889, type, sK441: ($i > $i)).
% 81.90/20.62 thf(func_def_1890, type, sK442: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1891, type, sK443: ($i > $i)).
% 81.90/20.62 thf(func_def_1892, type, sK444: ($i > $i)).
% 81.90/20.62 thf(func_def_1893, type, sK445: ($i > $i)).
% 81.90/20.62 thf(func_def_1894, type, sK446: ($i > $i)).
% 81.90/20.62 thf(func_def_1895, type, sK447: ($i > $i)).
% 81.90/20.62 thf(func_def_1896, type, sK448: ($i > $i)).
% 81.90/20.62 thf(func_def_1897, type, sK449: ($i > $i)).
% 81.90/20.62 thf(func_def_1898, type, sK450: ($i > $i)).
% 81.90/20.62 thf(func_def_1899, type, sK451: ($i > $i)).
% 81.90/20.62 thf(func_def_1900, type, sK452: ($i > $i)).
% 81.90/20.62 thf(func_def_1901, type, sK453: ($i > $i)).
% 81.90/20.62 thf(func_def_1902, type, sK454: ($i > $i)).
% 81.90/20.62 thf(func_def_1903, type, sK455: ($i > $i)).
% 81.90/20.62 thf(func_def_1904, type, sK456: ($o > $i)).
% 81.90/20.62 thf(func_def_1905, type, sK457: ($i > $i)).
% 81.90/20.62 thf(func_def_1906, type, sK458: ($i > $i)).
% 81.90/20.62 thf(func_def_1907, type, sK459: ($i > $i)).
% 81.90/20.62 thf(func_def_1908, type, sK460: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1909, type, sK461: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1910, type, sK462: ($i > $i)).
% 81.90/20.62 thf(func_def_1911, type, sK463: ($i > $i)).
% 81.90/20.62 thf(func_def_1912, type, sK464: ($i > $i)).
% 81.90/20.62 thf(func_def_1913, type, sK465: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1914, type, sK466: ($i > $i)).
% 81.90/20.62 thf(func_def_1915, type, sK467: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1916, type, sK468: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1917, type, sK469: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1918, type, sK470: ($i > $i)).
% 81.90/20.62 thf(func_def_1919, type, sK471: ($i > $i)).
% 81.90/20.62 thf(func_def_1920, type, sK472: ($i > $i)).
% 81.90/20.62 thf(func_def_1921, type, sK473: ($i > $i)).
% 81.90/20.62 thf(func_def_1922, type, sK474: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1923, type, sK475: ($i > $i)).
% 81.90/20.62 thf(func_def_1924, type, sK476: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1925, type, sK477: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1926, type, sK478: ($i > $i > $i)).
% 81.90/20.62 thf(func_def_1927, type, sK479: ($i > $i)).
% 81.90/20.62 thf(func_def_1928, type, sK480: ($i > $i > $i)).
% 81.90/20.62 thf(f182,axiom,(
% 81.90/20.62 ! [X1 : $o,X0 : $i] : ((holdsDuring_THFTYPE_IiooI @ X0 @ (~ X1)) => (~ (holdsDuring_THFTYPE_IiooI @ X0 @ X1)))),
% 81.90/20.62 file('/export/starexec/sandbox2/benchmark/Axioms/CSR005^0.ax',ax182)).
% 81.90/20.62 thf(f3578,axiom,(
% 81.90/20.62 (likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i)),
% 81.90/20.62 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax)).
% 81.90/20.62 thf(f3579,axiom,(
% 81.90/20.62 ! [X0 : $i] : (holdsDuring_THFTYPE_IiooI @ X0 @ $true)),
% 81.90/20.62 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax_001)).
% 81.90/20.62 thf(f3580,axiom,(
% 81.90/20.62 (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)))),
% 81.90/20.62 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax_002)).
% 81.90/20.62 thf(f3581,conjecture,(
% 81.90/20.62 ? [X1 : $i,X0 : $i] : (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ X1) @ (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ X0))),
% 81.90/20.62 file('/export/starexec/sandbox2/benchmark/theBenchmark.p',con)).
% 81.90/20.62 thf(f3582,negated_conjecture,(
% 81.90/20.62 ~ ? [X1 : $i,X0 : $i] : (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ X1) @ (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ X0))),
% 81.90/20.62 inference(negated_conjecture,[status(cth)],[f3581])).
% 81.90/20.62 thf(f4837,plain,(
% 81.90/20.62 ! [X0 : $i] : (holdsDuring_THFTYPE_IiooI @ X0 @ $true)),
% 81.90/20.62 inference(rectify,[],[f3579])).
% 81.90/20.62 thf(f4838,plain,(
% 81.90/20.62 ! [X0 : $i] : (((holdsDuring_THFTYPE_IiooI @ X0 @ $true)) = $true)),
% 81.90/20.62 inference(fool_elimination,[],[f4837])).
% 81.90/20.62 thf(f5451,plain,(
% 81.90/20.62 (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)))),
% 81.90/20.62 inference(rectify,[],[f3580])).
% 81.90/20.62 thf(f5452,plain,(
% 81.90/20.62 (((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)))))) = $true)),
% 81.90/20.62 inference(fool_elimination,[],[f5451])).
% 81.90/20.62 thf(f6353,plain,(
% 81.90/20.62 ! [X0 : $o,X1 : $i] : ((holdsDuring_THFTYPE_IiooI @ X1 @ (~ X0)) => (~ (holdsDuring_THFTYPE_IiooI @ X1 @ X0)))),
% 81.90/20.62 inference(rectify,[],[f182])).
% 81.90/20.62 thf(f6354,plain,(
% 81.90/20.62 ! [X0 : $o,X1 : $i] : ((((holdsDuring_THFTYPE_IiooI @ X1 @ (~ X0))) = $true) => ($true = ((~ (holdsDuring_THFTYPE_IiooI @ X1 @ X0)))))),
% 81.90/20.62 inference(fool_elimination,[],[f6353])).
% 81.90/20.62 thf(f9777,plain,(
% 81.90/20.62 (likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i)),
% 81.90/20.62 inference(rectify,[],[f3578])).
% 81.90/20.62 thf(f9778,plain,(
% 81.90/20.62 (((likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i)) = $true)),
% 81.90/20.62 inference(fool_elimination,[],[f9777])).
% 81.90/20.62 thf(f9907,plain,(
% 81.90/20.62 ~ ? [X0 : $i,X1 : $i] : (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ X0) @ (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ X1))),
% 81.90/20.62 inference(rectify,[],[f3582])).
% 81.90/20.62 thf(f9908,plain,(
% 81.90/20.62 ~ ? [X0 : $i,X1 : $i] : (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ X0) @ (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ X1))) = $true)),
% 81.90/20.62 inference(fool_elimination,[],[f9907])).
% 81.90/20.62 thf(f11262,plain,(
% 81.90/20.62 ! [X1 : $i,X0 : $i] : (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ X0) @ (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ X1))) != $true)),
% 81.90/20.62 inference(ennf_transformation,[],[f9908])).
% 81.90/20.62 thf(f11809,plain,(
% 81.90/20.62 ! [X0 : $o,X1 : $i] : ((((holdsDuring_THFTYPE_IiooI @ X1 @ (~ X0))) != $true) | ($true = ((~ (holdsDuring_THFTYPE_IiooI @ X1 @ X0)))))),
% 81.90/20.62 inference(ennf_transformation,[],[f6354])).
% 81.90/20.62 thf(f12564,plain,(
% 81.90/20.62 ! [X0 : $i,X1 : $i] : (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ X1) @ (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ X0))) != $true)),
% 81.90/20.62 inference(rectify,[],[f11262])).
% 81.90/20.62 thf(f13940,plain,(
% 81.90/20.62 ( ! [X0 : $o,X1 : $i] : ((((holdsDuring_THFTYPE_IiooI @ X1 @ (~ X0))) != $true) | ($true = ((~ (holdsDuring_THFTYPE_IiooI @ X1 @ X0))))) )),
% 81.90/20.62 inference(cnf_transformation,[],[f11809])).
% 81.90/20.62 thf(f14497,plain,(
% 81.90/20.62 ( ! [X0 : $i] : ((((holdsDuring_THFTYPE_IiooI @ X0 @ $true)) = $true)) )),
% 81.90/20.62 inference(cnf_transformation,[],[f4838])).
% 81.90/20.62 thf(f15820,plain,(
% 81.90/20.62 ( ! [X0 : $i,X1 : $i] : ((((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ X1) @ (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ X0))) != $true)) )),
% 81.90/20.62 inference(cnf_transformation,[],[f12564])).
% 81.90/20.62 thf(f15944,plain,(
% 81.90/20.62 (((likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i)) = $true)),
% 81.90/20.62 inference(cnf_transformation,[],[f9778])).
% 81.90/20.62 thf(f16884,plain,(
% 81.90/20.62 (((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)))))) = $true)),
% 81.90/20.62 inference(cnf_transformation,[],[f5452])).
% 81.90/20.62 thf(f17116,definition,(
% 81.90/20.62 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 81.90/20.62 introduced(theory,[fool_exhaustiveness_axiom])).
% 81.90/20.62 thf(f17590,plain,(
% 81.90/20.62 ( ! [X0 : $o,X1 : $i] : ((((holdsDuring_THFTYPE_IiooI @ X1 @ (~ X0))) != $true) | (((holdsDuring_THFTYPE_IiooI @ X1 @ X0)) = $false)) )),
% 81.90/20.62 inference(not_proxy_clausification,[],[f13940])).
% 81.90/20.62 thf(f17785,plain,(
% 81.90/20.62 ( ! [X0 : $i,X1 : $i] : ((((likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ X1)) = $false) | (((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ X0) @ $true)) != $true)) )),
% 81.90/20.62 inference(constrained_superposition,[],[f15820,f17116])).
% 81.90/20.62 thf(f17788,plain,(
% 81.90/20.62 ( ! [X0 : $i,X1 : $o] : ((((~ X1)) = $false) | (((holdsDuring_THFTYPE_IiooI @ X0 @ X1)) = $false) | (((holdsDuring_THFTYPE_IiooI @ X0 @ $true)) != $true)) )),
% 81.90/20.62 inference(constrained_superposition,[],[f17590,f17116])).
% 81.90/20.62 thf(f17798,plain,(
% 81.90/20.62 ( ! [X0 : $i,X1 : $o] : ((((holdsDuring_THFTYPE_IiooI @ X0 @ $true)) != $true) | (((holdsDuring_THFTYPE_IiooI @ X0 @ X1)) = $false) | ($true = X1)) )),
% 81.90/20.62 inference(not_proxy_clausification,[],[f17788])).
% 81.90/20.62 thf(f17800,plain,(
% 81.90/20.62 ( ! [X0 : $i,X1 : $o] : ((((holdsDuring_THFTYPE_IiooI @ X0 @ X1)) = $false) | ($true = X1)) )),
% 81.90/20.62 inference(forward_subsumption_resolution,[],[f17798,f14497])).
% 81.90/20.62 thf(f17801,plain,(
% 81.90/20.62 ( ! [X1 : $i] : ((((likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ X1)) = $false)) )),
% 81.90/20.62 inference(forward_subsumption_resolution,[],[f17785,f14497])).
% 81.90/20.62 thf(f17853,plain,(
% 81.90/20.62 ($false = $true) | (((!! @ $i @ (^[Y0 : $i]: ((likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ Y0) => (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ Y0))))) = $true)),
% 81.90/20.62 inference(constrained_superposition,[],[f16884,f17800])).
% 81.90/20.62 thf(f17855,plain,(
% 81.90/20.62 ( ! [X1 : $i] : (($false = $true) | ((((^[Y0 : $i]: ((likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ Y0) => (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ Y0))) @ X1)) = $true)) )),
% 81.90/20.62 inference(pi_proxy_clausification,[],[f17853])).
% 81.90/20.62 thf(f17856,plain,(
% 81.90/20.62 ( ! [X1 : $i] : (((((^[Y0 : $i]: ((likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ Y0) => (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ Y0))) @ X1)) = $true)) )),
% 81.90/20.62 inference(trivial_inequality_removal,[],[f17855])).
% 81.90/20.62 thf(f17857,plain,(
% 81.90/20.62 ( ! [X1 : $i] : (((((likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ X1) => (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ X1))) = $true)) )),
% 81.90/20.62 inference(beta-eta_normalization,[],[f17856])).
% 81.90/20.62 thf(f17858,plain,(
% 81.90/20.62 ( ! [X1 : $i] : ((((likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ X1)) = $true) | (((likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ X1)) = $false)) )),
% 81.90/20.62 inference(imp_proxy_clausification,[],[f17857])).
% 81.90/20.62 thf(f17867,plain,(
% 81.90/20.62 ( ! [X1 : $i] : ((((likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ X1)) = $false) | ($false = $true)) )),
% 81.90/20.62 inference(forward_demodulation,[],[f17858,f17801])).
% 81.90/20.62 thf(f17868,plain,(
% 81.90/20.62 ( ! [X1 : $i] : ((((likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ X1)) = $false)) )),
% 81.90/20.62 inference(trivial_inequality_removal,[],[f17867])).
% 81.90/20.62 thf(f17873,plain,(
% 81.90/20.62 ($false = $true)),
% 81.90/20.62 inference(constrained_superposition,[],[f15944,f17868])).
% 81.90/20.62 thf(f17875,plain,(
% 81.90/20.62 $false),
% 81.90/20.62 inference(trivial_inequality_removal,[],[f17873])).
% 81.90/20.62 % SZS output end Proof for theBenchmark
% 81.90/20.62 % (3720572)------------------------------
% 81.90/20.62 % (3720572)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 81.90/20.62 % (3720572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 81.90/20.62 % (3720572)CaDiCaL version: 2.1.3
% 81.90/20.62 % (3720572)Termination reason: Refutation
% 81.90/20.62 % (3720572)Time elapsed: 0.319 s
% 81.90/20.62 % (3720572)Peak memory usage: 23 MB
% 81.90/20.62 % (3720572)Instructions burned: 734 (million)
% 81.90/20.62 % (3719890)Success in time 20.382 s
% 81.90/20.62 % Vampire exiting
%------------------------------------------------------------------------------