%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : CSR151^3 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n003.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:23 AM UTC 2026
% Result : Theorem 13.85s 2.39s
% Output : Refutation 13.85s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR151^3 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.17 % Computer : n003.cluster.edu
% 0.10/0.17 % Model : x86_64 x86_64
% 0.10/0.17 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.17 % Memory : 8046.5625MB
% 0.10/0.17 % OS : Linux 6.8.0-71-generic
% 0.10/0.17 % CPULimit : 300
% 0.10/0.17 % WCLimit : 300
% 0.10/0.17 % DateTime : Tue Sep 29 17:59:29 UTC 2026
% 0.10/0.18 % CPUTime :
% 0.10/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.10/0.21 Running first-order model finding
% 0.10/0.21 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.91/1.74 % (2849971)Will run a generic schedule for satisfiability detection.
% 8.91/1.74 % (2849979)dis+10_1_sil=32000:sp=arity:random_seed=3486124536:i=103:fgj=on_2998 on theBenchmark for (2998ds/103Mi)
% 8.91/1.74 % (2849977)% WARNING: option uhcvi not known.
% 8.91/1.74 % (2849977)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=270247910:i=135531:add=off:rawr=on_2998 on theBenchmark for (2998ds/135531Mi)
% 8.91/1.74 % (2849976)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4112488973_2998 on theBenchmark for (2998ds/0Mi)
% 8.91/1.74 % (2849978)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3056982017:i=88024:add=on:rawr=on_2998 on theBenchmark for (2998ds/88024Mi)
% 8.91/1.74 % (2849980)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2579272228:i=116_2998 on theBenchmark for (2998ds/116Mi)
% 8.91/1.74 % (2849981)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2158409798:i=131_2998 on theBenchmark for (2998ds/131Mi)
% 8.91/1.74 % (2849982)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1923791213:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2998 on theBenchmark for (2998ds/159Mi)
% 8.91/1.74 % (2849979)Instruction limit reached!
% 8.91/1.74 % (2849979)------------------------------
% 8.91/1.74 % (2849979)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.91/1.74 % (2849979)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.91/1.74 % (2849979)CaDiCaL version: 2.1.3
% 8.91/1.74 % (2849979)Termination reason: Instruction limit
% 8.91/1.74 % (2849979)Termination phase: Initialization
% 8.91/1.74 % (2849979)Time elapsed: 0.025 s
% 8.91/1.74 % (2849979)Peak memory usage: 16 MB
% 8.91/1.74 % (2849979)Instructions burned: 106 (million)
% 8.91/1.74 % (2849990)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2423330362:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 8.91/1.74 % (2849980)Instruction limit reached!
% 8.91/1.74 % (2849980)------------------------------
% 8.91/1.74 % (2849980)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.91/1.74 % (2849980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.91/1.74 % (2849980)CaDiCaL version: 2.1.3
% 8.91/1.74 % (2849980)Termination reason: Instruction limit
% 8.91/1.74 % (2849980)Termination phase: Initialization
% 8.91/1.74 % (2849980)Time elapsed: 0.048 s
% 8.91/1.74 % (2849980)Peak memory usage: 16 MB
% 8.91/1.74 % (2849980)Instructions burned: 118 (million)
% 8.91/1.74 % (2849981)Instruction limit reached!
% 8.91/1.74 % (2849981)------------------------------
% 8.91/1.74 % (2849981)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.91/1.74 % (2849981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.91/1.74 % (2849981)CaDiCaL version: 2.1.3
% 8.91/1.74 % (2849981)Termination reason: Instruction limit
% 8.91/1.74 % (2849981)Termination phase: Initialization
% 8.91/1.74 % (2849981)Time elapsed: 0.053 s
% 8.91/1.74 % (2849981)Peak memory usage: 16 MB
% 8.91/1.74 % (2849981)Instructions burned: 132 (million)
% 8.91/1.74 % (2849992)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=138324297:i=131:bd=preordered:fsd=on_2997 on theBenchmark for (2997ds/131Mi)
% 8.91/1.74 % (2849993)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=1927300034:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2997 on theBenchmark for (2997ds/684Mi)
% 8.91/1.74 % (2849982)Instruction limit reached!
% 8.91/1.74 % (2849982)------------------------------
% 8.91/1.74 % (2849982)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 8.91/1.74 % (2849982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.91/1.74 % (2849982)CaDiCaL version: 2.1.3
% 8.91/1.74 % (2849982)Termination reason: Instruction limit
% 8.91/1.74 % (2849982)Termination phase: Property scanning
% 8.91/1.74 % (2849982)Time elapsed: 0.086 s
% 8.91/1.74 % (2849982)Peak memory usage: 16 MB
% 8.91/1.74 % (2849982)Instructions burned: 160 (million)
% 8.91/1.74 % (2849977)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 8.91/1.74 % (2849996)ott-21_1_sil=16000:fs=off:random_seed=2922518307:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 8.91/1.74 % (2849992)Instruction limit reached!
% 8.91/1.74 % (2849992)------------------------------
% 8.91/1.74 % (2849992)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.85/2.39 % (2849992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.85/2.39 % (2849992)CaDiCaL version: 2.1.3
% 13.85/2.39 % (2849992)Termination reason: Instruction limit
% 13.85/2.39 % (2849992)Termination phase: Initialization
% 13.85/2.39 % (2849992)Time elapsed: 0.056 s
% 13.85/2.39 % (2849992)Peak memory usage: 16 MB
% 13.85/2.39 % (2849992)Instructions burned: 133 (million)
% 13.85/2.39 % (2849998)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=254585459:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 13.85/2.39 % Exception at run slice level
% 13.85/2.39 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 13.85/2.39 % (2850000)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4182485437:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 13.85/2.39 % (2849993)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 13.85/2.39 % (2849996)Instruction limit reached!
% 13.85/2.39 % (2849996)------------------------------
% 13.85/2.39 % (2849996)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.85/2.39 % (2849996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.85/2.39 % (2849996)CaDiCaL version: 2.1.3
% 13.85/2.39 % (2849996)Termination reason: Instruction limit
% 13.85/2.39 % (2849996)Termination phase: Property scanning
% 13.85/2.39 % (2849996)Time elapsed: 0.103 s
% 13.85/2.39 % (2849996)Peak memory usage: 16 MB
% 13.85/2.39 % (2849996)Instructions burned: 181 (million)
% 13.85/2.39 % Exception at run slice level
% 13.85/2.39 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 13.85/2.39 % (2849977)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 13.85/2.39 % (2850002)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3073208218:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 13.85/2.39 % (2850003)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=508325708:i=889:ins=1_2996 on theBenchmark for (2996ds/889Mi)
% 13.85/2.39 % Exception at run slice level
% 13.85/2.39 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 13.85/2.39 % (2850006)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=1510920324: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)
% 13.85/2.39 % (2849993)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 13.85/2.39 % (2849998)Instruction limit reached!
% 13.85/2.39 % (2849998)------------------------------
% 13.85/2.39 % (2849998)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.85/2.39 % (2849998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.85/2.39 % (2849998)CaDiCaL version: 2.1.3
% 13.85/2.39 % (2849998)Termination reason: Instruction limit
% 13.85/2.39 % (2849998)Termination phase: Property scanning
% 13.85/2.39 % (2849998)Time elapsed: 0.197 s
% 13.85/2.39 % (2849998)Peak memory usage: 19 MB
% 13.85/2.39 % (2849998)Instructions burned: 479 (million)
% 13.85/2.39 % (2850006)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 13.85/2.39 % (2850008)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1664948989:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 13.85/2.39 % (2849993)Instruction limit reached!
% 13.85/2.39 % (2849993)------------------------------
% 13.85/2.39 % (2849993)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.85/2.39 % (2849993)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.85/2.39 % (2849993)CaDiCaL version: 2.1.3
% 13.85/2.39 % (2849993)Termination reason: Instruction limit
% 13.85/2.39 % (2849993)Termination phase: Saturation
% 13.85/2.39 % (2849993)Time elapsed: 0.290 s
% 13.85/2.39 % (2849993)Peak memory usage: 21 MB
% 13.85/2.39 % (2849993)Instructions burned: 685 (million)
% 13.85/2.39 % (2850010)fmb+10_1_sil=64000:random_seed=1082237625:i=22061:nm=2:gsp=on_2994 on theBenchmark for (2994ds/22061Mi)
% 13.85/2.39 % (2850006)Instruction limit reached!
% 13.85/2.39 % (2850006)------------------------------
% 13.85/2.39 % (2850006)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.85/2.39 % (2850006)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.85/2.39 % (2850006)CaDiCaL version: 2.1.3
% 13.85/2.39 % (2850006)Termination reason: Instruction limit
% 13.85/2.39 % (2850006)Termination phase: Saturation
% 13.85/2.39 % (2850006)Time elapsed: 0.156 s
% 13.85/2.39 % (2850006)Peak memory usage: 22 MB
% 13.85/2.39 % (2850006)Instructions burned: 694 (million)
% 13.85/2.39 % (2850012)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1652719936:i=9515:nm=5_2993 on theBenchmark for (2993ds/9515Mi)
% 13.85/2.39 % (2850008)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 13.85/2.39 % Exception at run slice level
% 13.85/2.39 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 13.85/2.39 % (2850014)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1570741844:fmbsr=1.7:i=920_2993 on theBenchmark for (2993ds/920Mi)
% 13.85/2.39 % (2850010)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 13.85/2.39 % Exception at run slice level
% 13.85/2.39 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 13.85/2.39 % (2850017)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1855156432:i=5131_2992 on theBenchmark for (2992ds/5131Mi)
% 13.85/2.39 % Exception at run slice level
% 13.85/2.39 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 13.85/2.39 % (2850019)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1848857346:i=1472:ins=7:fdi=8:gsp=on_2992 on theBenchmark for (2992ds/1472Mi)
% 13.85/2.39 % (2850017)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 13.85/2.39 % (2850008)Instruction limit reached!
% 13.85/2.39 % (2850008)------------------------------
% 13.85/2.39 % (2850008)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.85/2.39 % (2850008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.85/2.39 % (2850008)CaDiCaL version: 2.1.3
% 13.85/2.39 % (2850008)Termination reason: Instruction limit
% 13.85/2.39 % (2850008)Termination phase: Saturation
% 13.85/2.39 % (2850008)Time elapsed: 0.375 s
% 13.85/2.39 % (2850008)Peak memory usage: 24 MB
% 13.85/2.39 % (2850008)Instructions burned: 879 (million)
% 13.85/2.39 % (2850025)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2905546576:i=6324_2990 on theBenchmark for (2990ds/6324Mi)
% 13.85/2.39 % Exception at run slice level
% 13.85/2.39 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 13.85/2.39 % (2850027)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2596655770:fmbsr=2.30978:i=2174_2990 on theBenchmark for (2990ds/2174Mi)
% 13.85/2.39 % (2850019)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 13.85/2.39 % (2850002)Instruction limit reached!
% 13.85/2.39 % (2850002)------------------------------
% 13.85/2.39 % (2850002)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.85/2.39 % (2850002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.85/2.39 % (2850002)CaDiCaL version: 2.1.3
% 13.85/2.39 % (2850002)Termination reason: Instruction limit
% 13.85/2.39 % (2850002)Termination phase: Saturation
% 13.85/2.39 % (2850002)Time elapsed: 0.710 s
% 13.85/2.39 % (2850002)Peak memory usage: 25 MB
% 13.85/2.39 % (2850002)Instructions burned: 1180 (million)
% 13.85/2.39 % (2850031)ott-2_1_sil=16000:newcnf=on:random_seed=2244198587:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2988 on theBenchmark for (2988ds/869Mi)
% 13.85/2.39 % (2850019)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 13.85/2.39 % (2850031)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 13.85/2.39 % Exception at run slice level
% 13.85/2.39 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 13.85/2.39 % (2850042)ott+10_1_sil=32000:tgt=ground:random_seed=608319389:i=5114:av=off_2987 on theBenchmark for (2987ds/5114Mi)
% 13.85/2.39 % Exception at run slice level
% 13.85/2.39 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 13.85/2.39 % (2850044)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2294055236:i=54282_2986 on theBenchmark for (2986ds/54282Mi)
% 13.85/2.39 % (2850031)Instruction limit reached!
% 13.85/2.39 % (2850031)------------------------------
% 13.85/2.39 % (2850031)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.85/2.39 % (2850031)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.85/2.39 % (2850031)CaDiCaL version: 2.1.3
% 13.85/2.39 % (2850031)Termination reason: Instruction limit
% 13.85/2.39 % (2850031)Termination phase: Saturation
% 13.85/2.39 % (2850031)Time elapsed: 0.387 s
% 13.85/2.39 % (2850031)Peak memory usage: 24 MB
% 13.85/2.39 % (2850031)Instructions burned: 869 (million)
% 13.85/2.39 % (2850079)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3748546945:i=3512:aac=none_2984 on theBenchmark for (2984ds/3512Mi)
% 13.85/2.39 % Exception at run slice level
% 13.85/2.39 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 13.85/2.39 % (2850107)dis+21_1_sil=32000:sas=cadical:random_seed=1845235013:i=3773:amm=off_2984 on theBenchmark for (2984ds/3773Mi)
% 13.85/2.39 % (2850019)Instruction limit reached!
% 13.85/2.39 % (2850019)------------------------------
% 13.85/2.39 % (2850019)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.85/2.39 % (2850019)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.85/2.39 % (2850019)CaDiCaL version: 2.1.3
% 13.85/2.39 % (2850019)Termination reason: Instruction limit
% 13.85/2.39 % (2850019)Termination phase: Saturation
% 13.85/2.39 % (2850019)Time elapsed: 0.812 s
% 13.85/2.39 % (2850019)Peak memory usage: 27 MB
% 13.85/2.39 % (2850019)Instructions burned: 1473 (million)
% 13.85/2.39 % (2850122)ott+11_1_sil=16000:gs=on:random_seed=2116601199:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2983 on theBenchmark for (2983ds/2251Mi)
% 13.85/2.39 % (2850079)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 13.85/2.39 % (2850122)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 13.85/2.39 % (2850017)Instruction limit reached!
% 13.85/2.39 % (2850017)------------------------------
% 13.85/2.39 % (2850017)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.85/2.39 % (2850017)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.85/2.39 % (2850017)CaDiCaL version: 2.1.3
% 13.85/2.39 % (2850017)Termination reason: Instruction limit
% 13.85/2.39 % (2850017)Termination phase: Saturation
% 13.85/2.39 % (2850017)Time elapsed: 1.164 s
% 13.85/2.39 % (2850017)Peak memory usage: 22 MB
% 13.85/2.39 % (2850017)Instructions burned: 5135 (million)
% 13.85/2.39 % (2850204)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2568208899:fmbsr=1.6:i=67534_2980 on theBenchmark for (2980ds/67534Mi)
% 13.85/2.39 % Exception at run slice level
% 13.85/2.39 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 13.85/2.39 % (2850206)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2162368833:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2979 on theBenchmark for (2979ds/4591Mi)
% 13.85/2.39 % (2850122) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2849971-2850122"...
% 13.85/2.39 % (2850122)...printing done.
% 13.85/2.39 % (2850122)Refutation found. Thanks to Tanya!
% 13.85/2.39 % SZS status Theorem for theBenchmark
% 13.85/2.39 % SZS output start Proof for theBenchmark
% 13.85/2.39 thf(type_def_5, type, num: $tType).
% 13.85/2.39 thf(type_def_6, type, sTfun: ($tType * $tType) > $tType).
% 13.85/2.39 thf(func_def_0, type, abstractCounterpart_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_2, type, age_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_3, type, agent_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_4, type, altitude_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_5, type, ancestor_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_8, type, arcWeight_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_9, type, atomicNumber_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_10, type, attends_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_11, type, attribute_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_12, type, authors_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_13, type, average_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_14, type, barometricPressure_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_15, type, beforeOrEqual_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_16, type, before_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_17, type, believes_THFTYPE_IiooI: ($i > $o > $o)).
% 13.85/2.39 thf(func_def_18, type, between_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_19, type, boilingPoint_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_20, type, bottom_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_22, type, capability_THFTYPE_IIioIIiioIioI: (($i > $o) > ($i > $i > $o) > $i > $o)).
% 13.85/2.39 thf(func_def_23, type, capability_THFTYPE_IiIiioIioI: ($i > ($i > $i > $o) > $i > $o)).
% 13.85/2.39 thf(func_def_24, type, causesProposition_THFTYPE_IoooI: ($o > $o > $o)).
% 13.85/2.39 thf(func_def_25, type, causesSubclass_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_26, type, causes_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_28, type, closedOn_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_29, type, color_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_30, type, completelyFills_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_31, type, component_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_32, type, conclusion_THFTYPE_IoooI: ($o > $o > $o)).
% 13.85/2.39 thf(func_def_33, type, conditionalProbability_THFTYPE_IooioI: ($o > $o > $i > $o)).
% 13.85/2.39 thf(func_def_34, type, confersNorm_THFTYPE_IioioI: ($i > $o > $i > $o)).
% 13.85/2.39 thf(func_def_35, type, confersObligation_THFTYPE_IoiioI: ($o > $i > $i > $o)).
% 13.85/2.39 thf(func_def_36, type, confersRight_THFTYPE_IoiioI: ($o > $i > $i > $o)).
% 13.85/2.39 thf(func_def_37, type, connectedEngineeringComponents_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_38, type, connected_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_39, type, connectsEngineeringComponents_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_40, type, connects_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_41, type, considers_THFTYPE_IiooI: ($i > $o > $o)).
% 13.85/2.39 thf(func_def_42, type, consistent_THFTYPE_IoooI: ($o > $o > $o)).
% 13.85/2.39 thf(func_def_43, type, containsInformation_THFTYPE_IiooI: ($i > $o > $o)).
% 13.85/2.39 thf(func_def_44, type, contains_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_45, type, contraryAttribute_THFTYPE_IiiiioI: ($i > $i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_46, type, contraryAttribute_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_47, type, contraryAttribute_THFTYPE_IioI: ($i > $o)).
% 13.85/2.39 thf(func_def_48, type, contraryAttribute_THFTYPE_IoooI: ($o > $o > $o)).
% 13.85/2.39 thf(func_def_49, type, cooccur_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_50, type, copy_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_51, type, crosses_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_52, type, date_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_53, type, daughter_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_54, type, decreasesLikelihood_THFTYPE_IoooI: ($o > $o > $o)).
% 13.85/2.39 thf(func_def_55, type, deprivesNorm_THFTYPE_IioioI: ($i > $o > $i > $o)).
% 13.85/2.39 thf(func_def_56, type, depth_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_57, type, desires_THFTYPE_IiooI: ($i > $o > $o)).
% 13.85/2.39 thf(func_def_58, type, destination_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_59, type, developmentalForm_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_60, type, diameter_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_61, type, direction_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_62, type, disjointDecomposition_THFTYPE_IiiiiiioI: ($i > $i > $i > $i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_63, type, disjointDecomposition_THFTYPE_IiiiiioI: ($i > $i > $i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_64, type, disjointDecomposition_THFTYPE_IiiiioI: ($i > $i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_65, type, disjointDecomposition_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_66, type, disjointDecomposition_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_67, type, disjointDecomposition_THFTYPE_IioI: ($i > $o)).
% 13.85/2.39 thf(func_def_68, type, disjointRelation_THFTYPE_IIiioIIiioIoI: (($i > $i > $o) > ($i > $i > $o) > $o)).
% 13.85/2.39 thf(func_def_69, type, disjointRelation_THFTYPE_IIioIIioIoI: (($i > $o) > ($i > $o) > $o)).
% 13.85/2.39 thf(func_def_70, type, disjointRelation_THFTYPE_IIioioIIioioIoI: (($i > $o > $i > $o) > ($i > $o > $i > $o) > $o)).
% 13.85/2.39 thf(func_def_71, type, disjointRelation_THFTYPE_IIoooIIoooIoI: (($o > $o > $o) > ($o > $o > $o) > $o)).
% 13.85/2.39 thf(func_def_72, type, disjointRelation_THFTYPE_IiIiioIoI: ($i > ($i > $i > $o) > $o)).
% 13.85/2.39 thf(func_def_73, type, disjointRelation_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_74, type, disjoint_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_75, type, distance_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_76, type, distributes_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_77, type, div_THFTYPE_IiiiI: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_79, type, domainSubclass_THFTYPE_IIIioIIiioIioIiioI: ((($i > $o) > ($i > $i > $o) > $i > $o) > $i > $i > $o)).
% 13.85/2.39 thf(func_def_80, type, domainSubclass_THFTYPE_IIiiiIiioI: (($i > $i > $i) > $i > $i > $o)).
% 13.85/2.39 thf(func_def_81, type, domainSubclass_THFTYPE_IIiiiiiioIiioI: (($i > $i > $i > $i > $i > $i > $o) > $i > $i > $o)).
% 13.85/2.39 thf(func_def_82, type, domainSubclass_THFTYPE_IIiioIiioI: (($i > $i > $o) > $i > $i > $o)).
% 13.85/2.39 thf(func_def_83, type, domainSubclass_THFTYPE_IIioIiioI: (($i > $o) > $i > $i > $o)).
% 13.85/2.39 thf(func_def_84, type, domainSubclass_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_85, type, domain_THFTYPE_IIIIioIIiioIioIiioIiioI: (((($i > $o) > ($i > $i > $o) > $i > $o) > $i > $i > $o) > $i > $i > $o)).
% 13.85/2.39 thf(func_def_86, type, domain_THFTYPE_IIIiiIioIiioI: ((($i > $i) > $i > $o) > $i > $i > $o)).
% 13.85/2.39 thf(func_def_87, type, domain_THFTYPE_IIIiioIIiioIoIiioI: ((($i > $i > $o) > ($i > $i > $o) > $o) > $i > $i > $o)).
% 13.85/2.39 thf(func_def_88, type, domain_THFTYPE_IIIiioIioIiioI: ((($i > $i > $o) > $i > $o) > $i > $i > $o)).
% 13.85/2.39 thf(func_def_89, type, domain_THFTYPE_IIIioIIiioIioIiioI: ((($i > $o) > ($i > $i > $o) > $i > $o) > $i > $i > $o)).
% 13.85/2.39 thf(func_def_90, type, domain_THFTYPE_IIIioIiIiioI: ((($i > $o) > $i) > $i > $i > $o)).
% 13.85/2.39 thf(func_def_91, type, domain_THFTYPE_IIIioIioIiioI: ((($i > $o) > $i > $o) > $i > $i > $o)).
% 13.85/2.39 thf(func_def_92, type, domain_THFTYPE_IIIoiIioIiioI: ((($o > $i) > $i > $o) > $i > $i > $o)).
% 13.85/2.39 thf(func_def_93, type, domain_THFTYPE_IIIoioIIiioIoIiioI: ((($o > $i > $o) > ($i > $i > $o) > $o) > $i > $i > $o)).
% 13.85/2.39 thf(func_def_94, type, domain_THFTYPE_IIiiIiioI: (($i > $i) > $i > $i > $o)).
% 13.85/2.39 thf(func_def_95, type, domain_THFTYPE_IIiiiIiioI: (($i > $i > $i) > $i > $i > $o)).
% 13.85/2.39 thf(func_def_96, type, domain_THFTYPE_IIiiiiiioIiioI: (($i > $i > $i > $i > $i > $i > $o) > $i > $i > $o)).
% 13.85/2.39 thf(func_def_97, type, domain_THFTYPE_IIiiiioIiioI: (($i > $i > $i > $i > $o) > $i > $i > $o)).
% 13.85/2.39 thf(func_def_98, type, domain_THFTYPE_IIiiioIiioI: (($i > $i > $i > $o) > $i > $i > $o)).
% 13.85/2.39 thf(func_def_99, type, domain_THFTYPE_IIiioIiioI: (($i > $i > $o) > $i > $i > $o)).
% 13.85/2.39 thf(func_def_100, type, domain_THFTYPE_IIioIiioI: (($i > $o) > $i > $i > $o)).
% 13.85/2.39 thf(func_def_101, type, domain_THFTYPE_IIioioIiioI: (($i > $o > $i > $o) > $i > $i > $o)).
% 13.85/2.39 thf(func_def_102, type, domain_THFTYPE_IIiooIiioI: (($i > $o > $o) > $i > $i > $o)).
% 13.85/2.39 thf(func_def_103, type, domain_THFTYPE_IIioooIiioI: (($i > $o > $o > $o) > $i > $i > $o)).
% 13.85/2.39 thf(func_def_104, type, domain_THFTYPE_IIoiIiioI: (($o > $i) > $i > $i > $o)).
% 13.85/2.39 thf(func_def_105, type, domain_THFTYPE_IIoiioIiioI: (($o > $i > $i > $o) > $i > $i > $o)).
% 13.85/2.39 thf(func_def_106, type, domain_THFTYPE_IIoioIiioI: (($o > $i > $o) > $i > $i > $o)).
% 13.85/2.39 thf(func_def_107, type, domain_THFTYPE_IIooIiioI: (($o > $o) > $i > $i > $o)).
% 13.85/2.39 thf(func_def_108, type, domain_THFTYPE_IIooioIiioI: (($o > $o > $i > $o) > $i > $i > $o)).
% 13.85/2.39 thf(func_def_109, type, domain_THFTYPE_IIoooIiioI: (($o > $o > $o) > $i > $i > $o)).
% 13.85/2.39 thf(func_def_110, type, domain_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_111, type, duration_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_112, type, during_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_113, type, earlier_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_115, type, element_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_116, type, employs_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_117, type, engineeringSubcomponent_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_118, type, entails_THFTYPE_IoooI: ($o > $o > $o)).
% 13.85/2.39 thf(func_def_120, type, equivalenceRelationOn_THFTYPE_IIiioIioI: (($i > $i > $o) > $i > $o)).
% 13.85/2.39 thf(func_def_121, type, equivalentContentClass_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_122, type, equivalentContentInstance_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_123, type, exactlyLocated_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_124, type, exhaustiveAttribute_THFTYPE_IiiiiiioI: ($i > $i > $i > $i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_125, type, exhaustiveAttribute_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_126, type, exhaustiveAttribute_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_127, type, exhaustiveDecomposition_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_128, type, exhaustiveDecomposition_THFTYPE_IioI: ($i > $o)).
% 13.85/2.39 thf(func_def_129, type, experiencer_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_130, type, exploits_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_131, type, expressedInLanguage_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_133, type, faces_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_134, type, familyRelation_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_135, type, father_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_136, type, fills_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_137, type, finishes_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_138, type, frequency_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_140, type, geometricDistance_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_142, type, geopoliticalSubdivision_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_143, type, graphMeasure_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_144, type, graphPart_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_145, type, grasps_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_146, type, greaterThanByQuality_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_147, type, greaterThanOrEqualTo_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_148, type, greaterThan_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_149, type, gt_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_150, type, gtet_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_151, type, hasPurposeForAgent_THFTYPE_IioioI: ($i > $o > $i > $o)).
% 13.85/2.39 thf(func_def_152, type, hasPurpose_THFTYPE_IiooI: ($i > $o > $o)).
% 13.85/2.39 thf(func_def_153, type, hasPurpose_THFTYPE_IooI: ($o > $o)).
% 13.85/2.39 thf(func_def_154, type, hasSkill_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_155, type, height_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_156, type, holdsDuring_THFTYPE_IiooI: ($i > $o > $o)).
% 13.85/2.39 thf(func_def_157, type, holdsObligation_THFTYPE_IoioI: ($o > $i > $o)).
% 13.85/2.39 thf(func_def_158, type, holdsRight_THFTYPE_IoioI: ($o > $i > $o)).
% 13.85/2.39 thf(func_def_159, type, hole_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_160, type, home_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_161, type, husband_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_162, type, identicalListItems_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_163, type, identityElement_THFTYPE_IIiiiIioI: (($i > $i > $i) > $i > $o)).
% 13.85/2.39 thf(func_def_164, type, identityElement_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_165, type, immediateInstance_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_166, type, immediateSubclass_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_167, type, inList_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_168, type, inScopeOfInterest_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_169, type, increasesLikelihood_THFTYPE_IoooI: ($o > $o > $o)).
% 13.85/2.39 thf(func_def_170, type, independentProbability_THFTYPE_IoooI: ($o > $o > $o)).
% 13.85/2.39 thf(func_def_171, type, inhabits_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_172, type, inhibits_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_173, type, initialList_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_174, type, initialPart_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_175, type, instance_THFTYPE_IIIIioIIiioIioIiioIioI: (((($i > $o) > ($i > $i > $o) > $i > $o) > $i > $i > $o) > $i > $o)).
% 13.85/2.39 thf(func_def_176, type, instance_THFTYPE_IIIiiIioIioI: ((($i > $i) > $i > $o) > $i > $o)).
% 13.85/2.39 thf(func_def_177, type, instance_THFTYPE_IIIiioIIiioIoIioI: ((($i > $i > $o) > ($i > $i > $o) > $o) > $i > $o)).
% 13.85/2.39 thf(func_def_178, type, instance_THFTYPE_IIIiioIioIioI: ((($i > $i > $o) > $i > $o) > $i > $o)).
% 13.85/2.39 thf(func_def_179, type, instance_THFTYPE_IIIioIIiioIioIioI: ((($i > $o) > ($i > $i > $o) > $i > $o) > $i > $o)).
% 13.85/2.39 thf(func_def_180, type, instance_THFTYPE_IIIioIiIioI: ((($i > $o) > $i) > $i > $o)).
% 13.85/2.39 thf(func_def_181, type, instance_THFTYPE_IIIioIioIioI: ((($i > $o) > $i > $o) > $i > $o)).
% 13.85/2.39 thf(func_def_182, type, instance_THFTYPE_IIIioioIiioIioI: ((($i > $o > $i > $o) > $i > $i > $o) > $i > $o)).
% 13.85/2.39 thf(func_def_183, type, instance_THFTYPE_IIIoioIIiioIoIioI: ((($o > $i > $o) > ($i > $i > $o) > $o) > $i > $o)).
% 13.85/2.39 thf(func_def_184, type, instance_THFTYPE_IIiiIioI: (($i > $i) > $i > $o)).
% 13.85/2.39 thf(func_def_185, type, instance_THFTYPE_IIiiiIioI: (($i > $i > $i) > $i > $o)).
% 13.85/2.39 thf(func_def_186, type, instance_THFTYPE_IIiiiiiioIioI: (($i > $i > $i > $i > $i > $i > $o) > $i > $o)).
% 13.85/2.39 thf(func_def_187, type, instance_THFTYPE_IIiiiioIioI: (($i > $i > $i > $i > $o) > $i > $o)).
% 13.85/2.39 thf(func_def_188, type, instance_THFTYPE_IIiiioIioI: (($i > $i > $i > $o) > $i > $o)).
% 13.85/2.39 thf(func_def_189, type, instance_THFTYPE_IIiioIioI: (($i > $i > $o) > $i > $o)).
% 13.85/2.39 thf(func_def_190, type, instance_THFTYPE_IIioIioI: (($i > $o) > $i > $o)).
% 13.85/2.39 thf(func_def_191, type, instance_THFTYPE_IIioioIioI: (($i > $o > $i > $o) > $i > $o)).
% 13.85/2.39 thf(func_def_192, type, instance_THFTYPE_IIiooIioI: (($i > $o > $o) > $i > $o)).
% 13.85/2.39 thf(func_def_193, type, instance_THFTYPE_IIioooIioI: (($i > $o > $o > $o) > $i > $o)).
% 13.85/2.39 thf(func_def_194, type, instance_THFTYPE_IIoiIioI: (($o > $i) > $i > $o)).
% 13.85/2.39 thf(func_def_195, type, instance_THFTYPE_IIoiioIioI: (($o > $i > $i > $o) > $i > $o)).
% 13.85/2.39 thf(func_def_196, type, instance_THFTYPE_IIoioIioI: (($o > $i > $o) > $i > $o)).
% 13.85/2.39 thf(func_def_197, type, instance_THFTYPE_IIooIioI: (($o > $o) > $i > $o)).
% 13.85/2.39 thf(func_def_198, type, instance_THFTYPE_IIooioIioI: (($o > $o > $i > $o) > $i > $o)).
% 13.85/2.39 thf(func_def_199, type, instance_THFTYPE_IIoooIioI: (($o > $o > $o) > $i > $o)).
% 13.85/2.39 thf(func_def_200, type, instance_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_201, type, instance_THFTYPE_IoioI: ($o > $i > $o)).
% 13.85/2.39 thf(func_def_202, type, instrument_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_203, type, interiorPart_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_204, type, inverse_THFTYPE_IIiioIIiioIoI: (($i > $i > $o) > ($i > $i > $o) > $o)).
% 13.85/2.39 thf(func_def_205, type, involvedInEvent_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_206, type, irreflexiveOn_THFTYPE_IIiioIioI: (($i > $i > $o) > $i > $o)).
% 13.85/2.39 thf(func_def_207, type, knows_THFTYPE_IiooI: ($i > $o > $o)).
% 13.85/2.39 thf(func_def_210, type, lAbsoluteValueFn_THFTYPE_IiiI: ($i > $i)).
% 13.85/2.39 thf(func_def_213, type, lAbstractionFn_THFTYPE_IiiI: ($i > $i)).
% 13.85/2.39 thf(func_def_215, type, lAdditionFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_254, type, lAssignmentFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_255, type, lAssignmentFn_THFTYPE_IiiiiI: ($i > $i > $i > $i)).
% 13.85/2.39 thf(func_def_271, type, lBackFn_THFTYPE_IiiI: ($i > $i)).
% 13.85/2.39 thf(func_def_276, type, lBeginFn_THFTYPE_IiiI: ($i > $i)).
% 13.85/2.39 thf(func_def_278, type, lBeginNodeFn_THFTYPE_IiiI: ($i > $i)).
% 13.85/2.39 thf(func_def_319, type, lCardinalityFn_THFTYPE_IIioIiI: (($i > $o) > $i)).
% 13.85/2.39 thf(func_def_320, type, lCardinalityFn_THFTYPE_IiiI: ($i > $i)).
% 13.85/2.39 thf(func_def_325, type, lCeilingFn_THFTYPE_IiiI: ($i > $i)).
% 13.85/2.39 thf(func_def_329, type, lCenterOfCircleFn_THFTYPE_IiiI: ($i > $i)).
% 13.85/2.39 thf(func_def_387, type, lCosineFn_THFTYPE_IiiI: ($i > $i)).
% 13.85/2.39 thf(func_def_398, type, lCutSetFn_THFTYPE_IiiI: ($i > $i)).
% 13.85/2.39 thf(func_def_405, type, lDayFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_436, type, lDivisionFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_446, type, lEditionFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_458, type, lEndFn_THFTYPE_IiiI: ($i > $i)).
% 13.85/2.39 thf(func_def_460, type, lEndNodeFn_THFTYPE_IiiI: ($i > $i)).
% 13.85/2.39 thf(func_def_475, type, lExponentiationFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_478, type, lExtensionFn_THFTYPE_IiiI: ($i > $i)).
% 13.85/2.39 thf(func_def_499, type, lFloorFn_THFTYPE_IiiI: ($i > $i)).
% 13.85/2.39 thf(func_def_511, type, lFrontFn_THFTYPE_IiiI: ($i > $i)).
% 13.85/2.39 thf(func_def_519, type, lFutureFn_THFTYPE_IiiI: ($i > $i)).
% 13.85/2.39 thf(func_def_534, type, lGigaFn_THFTYPE_IiiI: ($i > $i)).
% 13.85/2.39 thf(func_def_539, type, lGovernmentFn_THFTYPE_IiiI: ($i > $i)).
% 13.85/2.39 thf(func_def_551, type, lGraphPathFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_556, type, lGreatestCommonDivisorFn_THFTYPE_IiiI: ($i > $i)).
% 13.85/2.39 thf(func_def_567, type, lHoleHostFn_THFTYPE_IiiI: ($i > $i)).
% 13.85/2.39 thf(func_def_569, type, lHoleSkinFn_THFTYPE_IiiI: ($i > $i)).
% 13.85/2.39 thf(func_def_578, type, lHourFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_588, type, lImaginaryPartFn_THFTYPE_IiiI: ($i > $i)).
% 13.85/2.39 thf(func_def_590, type, lImmediateFamilyFn_THFTYPE_IiiI: ($i > $i)).
% 13.85/2.39 thf(func_def_592, type, lImmediateFutureFn_THFTYPE_IiiI: ($i > $i)).
% 13.85/2.39 thf(func_def_594, type, lImmediatePastFn_THFTYPE_IiiI: ($i > $i)).
% 13.85/2.39 thf(func_def_605, type, lInitialNodeFn_THFTYPE_IiiI: ($i > $i)).
% 13.85/2.39 thf(func_def_620, type, lIntervalFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_642, type, lKiloFn_THFTYPE_IiiI: ($i > $i)).
% 13.85/2.39 thf(func_def_653, type, lLeastCommonMultipleFn_THFTYPE_IiiI: ($i > $i)).
% 13.85/2.39 thf(func_def_667, type, lListConcatenateFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_669, type, lListFn_THFTYPE_IiiI: ($i > $i)).
% 13.85/2.39 thf(func_def_670, type, lListFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_672, type, lListLengthFn_THFTYPE_IiiI: ($i > $i)).
% 13.85/2.39 thf(func_def_674, type, lListOrderFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_686, type, lMagnitudeFn_THFTYPE_IiiI: ($i > $i)).
% 13.85/2.39 thf(func_def_702, type, lMaxFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_704, type, lMaximalWeightedPathFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_707, type, lMeasureFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_714, type, lMegaFn_THFTYPE_IiiI: ($i > $i)).
% 13.85/2.39 thf(func_def_718, type, lMereologicalDifferenceFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_720, type, lMereologicalProductFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_722, type, lMereologicalSumFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_726, type, lMicroFn_THFTYPE_IiiI: ($i > $i)).
% 13.85/2.39 thf(func_def_733, type, lMilliFn_THFTYPE_IiiI: ($i > $i)).
% 13.85/2.39 thf(func_def_736, type, lMinFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_739, type, lMinimalCutSetFn_THFTYPE_IiiI: ($i > $i)).
% 13.85/2.39 thf(func_def_741, type, lMinimalWeightedPathFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_744, type, lMinuteFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_756, type, lMonthFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_767, type, lMultiplicationFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_776, type, lNanoFn_THFTYPE_IiiI: ($i > $i)).
% 13.85/2.39 thf(func_def_836, type, lPastFn_THFTYPE_IiiI: ($i > $i)).
% 13.85/2.39 thf(func_def_839, type, lPathWeightFn_THFTYPE_IiiI: ($i > $i)).
% 13.85/2.39 thf(func_def_845, type, lPeriodicalIssueFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_858, type, lPicoFn_THFTYPE_IiiI: ($i > $i)).
% 13.85/2.39 thf(func_def_886, type, lPredecessorFn_THFTYPE_IiiI: ($i > $i)).
% 13.85/2.39 thf(func_def_890, type, lPremisesFn_THFTYPE_IooI: ($o > $o)).
% 13.85/2.39 thf(func_def_898, type, lProbabilityFn_THFTYPE_IoiI: ($o > $i)).
% 13.85/2.39 thf(func_def_906, type, lPropertyFn_THFTYPE_IiiI: ($i > $i)).
% 13.85/2.39 thf(func_def_943, type, lRealNumberFn_THFTYPE_IiiI: ($i > $i)).
% 13.85/2.39 thf(func_def_947, type, lReciprocalFn_THFTYPE_IiiI: ($i > $i)).
% 13.85/2.39 thf(func_def_950, type, lRecurrentTimeIntervalFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_960, type, lRelativeTimeFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_965, type, lRemainderFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_983, type, lRoundFn_THFTYPE_IiiI: ($i > $i)).
% 13.85/2.39 thf(func_def_990, type, lSecondFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_1003, type, lSeriesVolumeFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_1018, type, lSignumFn_THFTYPE_IiiI: ($i > $i)).
% 13.85/2.39 thf(func_def_1020, type, lSineFn_THFTYPE_IiiI: ($i > $i)).
% 13.85/2.39 thf(func_def_1041, type, lSpeedFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_1046, type, lSquareRootFn_THFTYPE_IiiI: ($i > $i)).
% 13.85/2.39 thf(func_def_1061, type, lSubtractionFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_1063, type, lSuccessorFn_THFTYPE_IiiI: ($i > $i)).
% 13.85/2.39 thf(func_def_1078, type, lTangentFn_THFTYPE_IiiI: ($i > $i)).
% 13.85/2.39 thf(func_def_1083, type, lTemporalCompositionFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_1087, type, lTeraFn_THFTYPE_IiiI: ($i > $i)).
% 13.85/2.39 thf(func_def_1089, type, lTerminalNodeFn_THFTYPE_IiiI: ($i > $i)).
% 13.85/2.39 thf(func_def_1103, type, lTimeIntervalFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_1138, type, lUnionFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_1141, type, lUnitFn_THFTYPE_IiiI: ($i > $i)).
% 13.85/2.39 thf(func_def_1164, type, lVelocityFn_THFTYPE_IiiiiiI: ($i > $i > $i > $i > $i)).
% 13.85/2.39 thf(func_def_1188, type, lWealthFn_THFTYPE_IiiI: ($i > $i)).
% 13.85/2.39 thf(func_def_1201, type, lWhenFn_THFTYPE_IiiI: ($i > $i)).
% 13.85/2.39 thf(func_def_1203, type, lWhereFn_THFTYPE_IiiiI: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_1212, type, lYearFn_THFTYPE_IiiI: ($i > $i)).
% 13.85/2.39 thf(func_def_1216, type, larger_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1217, type, leader_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1218, type, legalRelation_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1219, type, length_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1220, type, lessThanOrEqualTo_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1221, type, lessThan_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1223, type, linearExtent_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1224, type, links_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_1225, type, located_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1226, type, lt_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1227, type, ltet_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1228, type, manner_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1229, type, material_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1230, type, measure_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1231, type, meetsSpatially_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1232, type, meetsTemporally_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1233, type, meltingPoint_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1234, type, member_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1236, type, minus_THFTYPE_IiiiI: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_1237, type, modalAttribute_THFTYPE_IoioI: ($o > $i > $o)).
% 13.85/2.39 thf(func_def_1238, type, monetaryValue_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1239, type, mother_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1240, type, multiplicativeFactor_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1292, type, names_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1293, type, needs_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1294, type, occupiesPosition_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_1295, type, orientation_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_1296, type, origin_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1297, type, overlapsPartially_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1298, type, overlapsSpatially_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1299, type, overlapsTemporally_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1300, type, parallel_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1301, type, parent_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1302, type, part_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1303, type, partialOrderingOn_THFTYPE_IIiioIioI: (($i > $i > $o) > $i > $o)).
% 13.85/2.39 thf(func_def_1304, type, partiallyFills_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1305, type, partition_THFTYPE_IiiiiiiioI: ($i > $i > $i > $i > $i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_1306, type, partition_THFTYPE_IiiiiiioI: ($i > $i > $i > $i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_1307, type, partition_THFTYPE_IiiiiioI: ($i > $i > $i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_1308, type, partition_THFTYPE_IiiiioI: ($i > $i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_1309, type, partition_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_1310, type, partition_THFTYPE_IioI: ($i > $o)).
% 13.85/2.39 thf(func_def_1311, type, partlyLocated_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1312, type, pathLength_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1313, type, path_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1314, type, patient_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1315, type, patient_THFTYPE_IiooI: ($i > $o > $o)).
% 13.85/2.39 thf(func_def_1316, type, penetrates_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1317, type, piece_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1318, type, plus_THFTYPE_IiiiI: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_1319, type, pointOfFigure_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1320, type, pointOfIntersection_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_1321, type, possesses_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1322, type, precondition_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1323, type, prefers_THFTYPE_IioooI: ($i > $o > $o > $o)).
% 13.85/2.39 thf(func_def_1324, type, premise_THFTYPE_IoooI: ($o > $o > $o)).
% 13.85/2.39 thf(func_def_1325, type, prevents_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1326, type, properPart_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1327, type, properlyFills_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1328, type, property_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1329, type, publishes_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1330, type, radius_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1331, type, rangeSubclass_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1332, type, range_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1333, type, realization_THFTYPE_IiooI: ($i > $o > $o)).
% 13.85/2.39 thf(func_def_1334, type, refers_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1335, type, reflexiveOn_THFTYPE_IIiioIioI: (($i > $i > $o) > $i > $o)).
% 13.85/2.39 thf(func_def_1336, type, relatedEvent_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1338, type, relatedInternalConcept_THFTYPE_IIIiioIIiioIoIIiioIoI: ((($i > $i > $o) > ($i > $i > $o) > $o) > ($i > $i > $o) > $o)).
% 13.85/2.39 thf(func_def_1339, type, relatedInternalConcept_THFTYPE_IIiiIioI: (($i > $i) > $i > $o)).
% 13.85/2.39 thf(func_def_1340, type, relatedInternalConcept_THFTYPE_IIiiiIioI: (($i > $i > $i) > $i > $o)).
% 13.85/2.39 thf(func_def_1341, type, relatedInternalConcept_THFTYPE_IIiiiiiioIIiioIoI: (($i > $i > $i > $i > $i > $i > $o) > ($i > $i > $o) > $o)).
% 13.85/2.39 thf(func_def_1342, type, relatedInternalConcept_THFTYPE_IIiioIIIoiIioIoI: (($i > $i > $o) > (($o > $i) > $i > $o) > $o)).
% 13.85/2.39 thf(func_def_1343, type, relatedInternalConcept_THFTYPE_IIiioIIiiiioIoI: (($i > $i > $o) > ($i > $i > $i > $i > $o) > $o)).
% 13.85/2.39 thf(func_def_1344, type, relatedInternalConcept_THFTYPE_IIiioIIiioIoI: (($i > $i > $o) > ($i > $i > $o) > $o)).
% 13.85/2.39 thf(func_def_1345, type, relatedInternalConcept_THFTYPE_IIiioIIiooIoI: (($i > $i > $o) > ($i > $o > $o) > $o)).
% 13.85/2.39 thf(func_def_1346, type, relatedInternalConcept_THFTYPE_IIiioIioI: (($i > $i > $o) > $i > $o)).
% 13.85/2.39 thf(func_def_1347, type, relatedInternalConcept_THFTYPE_IIiooIIiioIoI: (($i > $o > $o) > ($i > $i > $o) > $o)).
% 13.85/2.39 thf(func_def_1348, type, relatedInternalConcept_THFTYPE_IIiooIIiooIoI: (($i > $o > $o) > ($i > $o > $o) > $o)).
% 13.85/2.39 thf(func_def_1349, type, relatedInternalConcept_THFTYPE_IIoiioIIoiioIoI: (($o > $i > $i > $o) > ($o > $i > $i > $o) > $o)).
% 13.85/2.39 thf(func_def_1350, type, relatedInternalConcept_THFTYPE_IIoioIIoioIoI: (($o > $i > $o) > ($o > $i > $o) > $o)).
% 13.85/2.39 thf(func_def_1351, type, relatedInternalConcept_THFTYPE_IiIiiIoI: ($i > ($i > $i) > $o)).
% 13.85/2.39 thf(func_def_1352, type, relatedInternalConcept_THFTYPE_IiIiiiIoI: ($i > ($i > $i > $i) > $o)).
% 13.85/2.39 thf(func_def_1353, type, relatedInternalConcept_THFTYPE_IiIiioIoI: ($i > ($i > $i > $o) > $o)).
% 13.85/2.39 thf(func_def_1354, type, relatedInternalConcept_THFTYPE_IiIiooIoI: ($i > ($i > $o > $o) > $o)).
% 13.85/2.39 thf(func_def_1355, type, relatedInternalConcept_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1356, type, relative_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1357, type, representsForAgent_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_1358, type, representsInLanguage_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_1359, type, represents_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1360, type, resource_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1361, type, result_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1362, type, sibling_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1363, type, side_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1365, type, smaller_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1366, type, son_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1367, type, spouse_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1368, type, starts_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1370, type, subAttribute_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1371, type, subCollection_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1372, type, subGraph_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1373, type, subList_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1374, type, subOrganization_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1376, type, subProcess_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1377, type, subProposition_THFTYPE_IoooI: ($o > $o > $o)).
% 13.85/2.39 thf(func_def_1378, type, subSystem_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1379, type, subclass_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1380, type, subrelation_THFTYPE_IIiiioIIiiioIoI: (($i > $i > $i > $o) > ($i > $i > $i > $o) > $o)).
% 13.85/2.39 thf(func_def_1381, type, subrelation_THFTYPE_IIiioIIIoiIioIoI: (($i > $i > $o) > (($o > $i) > $i > $o) > $o)).
% 13.85/2.39 thf(func_def_1382, type, subrelation_THFTYPE_IIiioIIIooIioIoI: (($i > $i > $o) > (($o > $o) > $i > $o) > $o)).
% 13.85/2.39 thf(func_def_1383, type, subrelation_THFTYPE_IIiioIIiioIoI: (($i > $i > $o) > ($i > $i > $o) > $o)).
% 13.85/2.39 thf(func_def_1384, type, subrelation_THFTYPE_IIiioIIiooIoI: (($i > $i > $o) > ($i > $o > $o) > $o)).
% 13.85/2.39 thf(func_def_1385, type, subrelation_THFTYPE_IIiioIioI: (($i > $i > $o) > $i > $o)).
% 13.85/2.39 thf(func_def_1386, type, subrelation_THFTYPE_IIioIIioIoI: (($i > $o) > ($i > $o) > $o)).
% 13.85/2.39 thf(func_def_1387, type, subrelation_THFTYPE_IIiooIIiioIoI: (($i > $o > $o) > ($i > $i > $o) > $o)).
% 13.85/2.39 thf(func_def_1388, type, subrelation_THFTYPE_IIoioIIiioIoI: (($o > $i > $o) > ($i > $i > $o) > $o)).
% 13.85/2.39 thf(func_def_1389, type, subrelation_THFTYPE_IIoooIIiioIoI: (($o > $o > $o) > ($i > $i > $o) > $o)).
% 13.85/2.39 thf(func_def_1390, type, subrelation_THFTYPE_IiIiioIoI: ($i > ($i > $i > $o) > $o)).
% 13.85/2.39 thf(func_def_1391, type, subrelation_THFTYPE_IiIoooIoI: ($i > ($o > $o > $o) > $o)).
% 13.85/2.39 thf(func_def_1392, type, subrelation_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1393, type, subset_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1395, type, subsumesContentClass_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1396, type, subsumesContentInstance_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1397, type, subsumesContentInstance_THFTYPE_IiooI: ($i > $o > $o)).
% 13.85/2.39 thf(func_def_1399, type, successorAttributeClosure_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1400, type, successorAttribute_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1401, type, superficialPart_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1402, type, surface_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1404, type, systemPart_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1405, type, temporalPart_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1406, type, temporallyBetweenOrEqual_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_1407, type, temporallyBetween_THFTYPE_IiiioI: ($i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_1408, type, time_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1409, type, times_THFTYPE_IiiiI: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_1410, type, top_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1411, type, totalOrderingOn_THFTYPE_IIiioIioI: (($i > $i > $o) > $i > $o)).
% 13.85/2.39 thf(func_def_1412, type, transactionAmount_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1413, type, traverses_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1414, type, trichotomizingOn_THFTYPE_IIiioIioI: (($i > $i > $o) > $i > $o)).
% 13.85/2.39 thf(func_def_1415, type, truth_THFTYPE_IoooI: ($o > $o > $o)).
% 13.85/2.39 thf(func_def_1416, type, typicalPart_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1417, type, typicallyContainsPart_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1419, type, uses_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1420, type, valence_THFTYPE_IIiioIioI: (($i > $i > $o) > $i > $o)).
% 13.85/2.39 thf(func_def_1421, type, valence_THFTYPE_IIioIioI: (($i > $o) > $i > $o)).
% 13.85/2.39 thf(func_def_1422, type, valence_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1423, type, version_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1424, type, wants_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1425, type, wears_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1427, type, width_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1428, type, wife_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1430, type, vNOT: ($o > $o)).
% 13.85/2.39 thf(func_def_1434, type, likes_THFTYPE_IiioI: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1438, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 13.85/2.39 thf(func_def_1439, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 13.85/2.39 thf(func_def_1440, type, vAND: ($o > $o > $o)).
% 13.85/2.39 thf(func_def_1441, type, db0: !>[X0: $tType]:(X0)).
% 13.85/2.39 thf(func_def_1442, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 13.85/2.39 thf(func_def_1443, type, db2: !>[X0: $tType]:(X0)).
% 13.85/2.39 thf(func_def_1444, type, db1: !>[X0: $tType]:(X0)).
% 13.85/2.39 thf(func_def_1445, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 13.85/2.39 thf(func_def_1446, type, vIMP: ($o > $o > $o)).
% 13.85/2.39 thf(func_def_1447, type, vOR: ($o > $o > $o)).
% 13.85/2.39 thf(func_def_1448, type, sP0: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1449, type, sP1: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1450, type, sP2: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1451, type, sP3: ($i > $o)).
% 13.85/2.39 thf(func_def_1452, type, sP4: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1453, type, sP5: ($i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_1454, type, sP6: ($i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_1455, type, sP7: ($i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_1456, type, sP8: ($i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_1457, type, sP9: ($i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_1458, type, sP10: ($i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_1459, type, sP11: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1460, type, sP12: ($i > $o)).
% 13.85/2.39 thf(func_def_1461, type, sP13: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1462, type, sP14: ($i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_1463, type, sP15: ($i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_1464, type, sP16: ($i > $i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_1465, type, sP17: ($i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_1466, type, sP18: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1467, type, sP19: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1468, type, sP20: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1469, type, sP21: ($i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_1470, type, sP22: ($i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_1471, type, sP23: ($i > $o)).
% 13.85/2.39 thf(func_def_1472, type, sP24: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1473, type, sP25: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1474, type, sP26: (($i > $i > $o) > $i > $i > $o)).
% 13.85/2.39 thf(func_def_1475, type, sP27: (($i > $i > $o) > $o)).
% 13.85/2.39 thf(func_def_1476, type, sP28: ($i > $i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_1477, type, sP29: ($i > $o)).
% 13.85/2.39 thf(func_def_1478, type, sP30: ($i > $i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_1479, type, sP31: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1480, type, sP32: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1481, type, sP33: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1482, type, sP34: ($i > $o)).
% 13.85/2.39 thf(func_def_1483, type, sP35: ($i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_1484, type, sP36: ($i > $o)).
% 13.85/2.39 thf(func_def_1485, type, sP37: ($i > $o)).
% 13.85/2.39 thf(func_def_1486, type, sP38: ($i > $i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_1487, type, sP39: ($i > $o)).
% 13.85/2.39 thf(func_def_1488, type, sP40: ($i > $o)).
% 13.85/2.39 thf(func_def_1489, type, sP41: ($i > $o)).
% 13.85/2.39 thf(func_def_1490, type, sP42: ($i > ($i > $i > $o) > $o)).
% 13.85/2.39 thf(func_def_1491, type, sP43: ($i > $o)).
% 13.85/2.39 thf(func_def_1492, type, sP44: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1493, type, sP45: ($i > $o)).
% 13.85/2.39 thf(func_def_1494, type, sP46: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1495, type, sP47: ($i > $o)).
% 13.85/2.39 thf(func_def_1496, type, sP48: ($i > $o)).
% 13.85/2.39 thf(func_def_1497, type, sP49: ($i > $o)).
% 13.85/2.39 thf(func_def_1498, type, sP50: ($i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_1499, type, sP51: ($i > $o)).
% 13.85/2.39 thf(func_def_1500, type, sP52: ($i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_1501, type, sP53: ($i > $o)).
% 13.85/2.39 thf(func_def_1502, type, sP54: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1503, type, sP55: ($i > $o)).
% 13.85/2.39 thf(func_def_1504, type, sP56: ($i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_1505, type, sP57: ($i > $o > $i > $o)).
% 13.85/2.39 thf(func_def_1506, type, sP58: ($i > $o)).
% 13.85/2.39 thf(func_def_1507, type, sP59: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1508, type, sP60: ($i > $o)).
% 13.85/2.39 thf(func_def_1509, type, sP61: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1510, type, sP62: ($i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_1511, type, sP63: ($i > $o)).
% 13.85/2.39 thf(func_def_1512, type, sP64: ($i > $o)).
% 13.85/2.39 thf(func_def_1513, type, sP65: ($i > $o)).
% 13.85/2.39 thf(func_def_1514, type, sP66: ($i > $o)).
% 13.85/2.39 thf(func_def_1515, type, sP67: ($i > $o)).
% 13.85/2.39 thf(func_def_1516, type, sP68: ($i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_1517, type, sP69: ($i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_1518, type, sP70: ($i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_1519, type, sP71: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1520, type, sP72: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1521, type, sP73: ($i > $o)).
% 13.85/2.39 thf(func_def_1522, type, sP74: ($i > ($i > $i > $o) > $i > $o)).
% 13.85/2.39 thf(func_def_1523, type, sP75: (($i > $i > $o) > $i > $o)).
% 13.85/2.39 thf(func_def_1524, type, sP76: ($i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_1525, type, sP77: (($i > $i > $o) > $i > $o)).
% 13.85/2.39 thf(func_def_1526, type, sP78: ($i > $o)).
% 13.85/2.39 thf(func_def_1527, type, sP79: ($i > $o)).
% 13.85/2.39 thf(func_def_1528, type, sP80: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1529, type, sP81: ($i > $o)).
% 13.85/2.39 thf(func_def_1530, type, sP82: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1531, type, sP83: ($i > $o)).
% 13.85/2.39 thf(func_def_1532, type, sP84: ($i > $o)).
% 13.85/2.39 thf(func_def_1533, type, sP85: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1534, type, sP86: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1535, type, sP87: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1536, type, sP88: ($i > $o)).
% 13.85/2.39 thf(func_def_1537, type, sP89: ($i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_1538, type, sP90: ($i > $i > $i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_1539, type, sP91: ($i > $o)).
% 13.85/2.39 thf(func_def_1540, type, sP92: ($i > $o)).
% 13.85/2.39 thf(func_def_1541, type, sP93: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1542, type, sP94: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1543, type, sP95: ($i > $o)).
% 13.85/2.39 thf(func_def_1544, type, sP96: ($i > $o)).
% 13.85/2.39 thf(func_def_1545, type, sP97: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1546, type, sP98: ($i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_1547, type, sP99: ($i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_1548, type, sP100: ($i > $o)).
% 13.85/2.39 thf(func_def_1549, type, sP101: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1550, type, sP102: ($o > $o > $o)).
% 13.85/2.39 thf(func_def_1551, type, sP103: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1552, type, sP104: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1553, type, sP105: ($i > $o)).
% 13.85/2.39 thf(func_def_1554, type, sP106: ($i > $o)).
% 13.85/2.39 thf(func_def_1555, type, sP107: (($i > $i > $o) > $i > $i > $o)).
% 13.85/2.39 thf(func_def_1556, type, sP108: (($i > $i > $o) > $i > $i > $o)).
% 13.85/2.39 thf(func_def_1557, type, sP109: (($i > $i > $o) > $i > $i > $o)).
% 13.85/2.39 thf(func_def_1558, type, sP110: ($i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_1559, type, sP111: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1560, type, sP112: ($i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_1561, type, sP113: ($i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_1562, type, sP114: ($i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_1563, type, sP115: ($i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_1564, type, sP116: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1565, type, sP117: ($i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_1566, type, sP118: ($i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_1567, type, sP119: ($i > $o)).
% 13.85/2.39 thf(func_def_1568, type, sP120: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1569, type, sP121: ($i > $i > $o)).
% 13.85/2.39 thf(func_def_1570, type, sP122: ($i > $i > $i > $o)).
% 13.85/2.39 thf(func_def_1571, type, sK123: ($i > $i)).
% 13.85/2.39 thf(func_def_1572, type, sK124: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_1573, type, sK125: ($i > $i)).
% 13.85/2.39 thf(func_def_1574, type, sK126: ($i > $i)).
% 13.85/2.39 thf(func_def_1575, type, sK127: ($i > $i)).
% 13.85/2.39 thf(func_def_1576, type, sK128: ($i > $o)).
% 13.85/2.39 thf(func_def_1577, type, sK129: ($i > $i)).
% 13.85/2.39 thf(func_def_1578, type, sK130: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_1579, type, sK131: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_1580, type, sK132: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_1581, type, sK133: ($i > $i)).
% 13.85/2.39 thf(func_def_1582, type, sK134: ($i > $i)).
% 13.85/2.39 thf(func_def_1583, type, sK135: ($i > $i)).
% 13.85/2.39 thf(func_def_1584, type, sK136: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_1585, type, sK137: ($i > $i)).
% 13.85/2.39 thf(func_def_1586, type, sK138: (($i > $i > $o) > $i)).
% 13.85/2.39 thf(func_def_1587, type, sK139: (($i > $i > $o) > $i)).
% 13.85/2.39 thf(func_def_1588, type, sK140: (($i > $i > $o) > $i)).
% 13.85/2.39 thf(func_def_1589, type, sK141: ($i > $i)).
% 13.85/2.39 thf(func_def_1590, type, sK142: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_1591, type, sK143: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_1592, type, sK144: ($i > $i)).
% 13.85/2.39 thf(func_def_1593, type, sK145: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_1594, type, sK146: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_1595, type, sK147: ($i > $i)).
% 13.85/2.39 thf(func_def_1596, type, sK148: ($i > $i)).
% 13.85/2.39 thf(func_def_1597, type, sK149: ($i > $i)).
% 13.85/2.39 thf(func_def_1598, type, sK150: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_1599, type, sK151: ($i > $i)).
% 13.85/2.39 thf(func_def_1600, type, sK152: ($i > $i)).
% 13.85/2.39 thf(func_def_1601, type, sK153: ($i > $i)).
% 13.85/2.39 thf(func_def_1602, type, sK154: ($i > $i)).
% 13.85/2.39 thf(func_def_1603, type, sK155: ($i > $i)).
% 13.85/2.39 thf(func_def_1604, type, sK156: ($i > $i)).
% 13.85/2.39 thf(func_def_1605, type, sK157: ($i > $i)).
% 13.85/2.39 thf(func_def_1606, type, sK158: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_1607, type, sK159: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_1608, type, sK160: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_1609, type, sK161: ($i > $i)).
% 13.85/2.39 thf(func_def_1610, type, sK162: ($i > $i)).
% 13.85/2.39 thf(func_def_1611, type, sK163: ($i > $i)).
% 13.85/2.39 thf(func_def_1612, type, sK164: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_1613, type, sK165: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_1614, type, sK166: ($i > $i)).
% 13.85/2.39 thf(func_def_1615, type, sK167: ($i > $i)).
% 13.85/2.39 thf(func_def_1616, type, sK168: ($i > $i > $i > $i)).
% 13.85/2.39 thf(func_def_1617, type, sK169: ($i > $i > $i > $i)).
% 13.85/2.39 thf(func_def_1618, type, sK170: ($i > $i)).
% 13.85/2.39 thf(func_def_1619, type, sK171: ($i > $i)).
% 13.85/2.39 thf(func_def_1620, type, sK172: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_1621, type, sK173: ($i > $i)).
% 13.85/2.39 thf(func_def_1622, type, sK174: ($i > $i > $i > $i)).
% 13.85/2.39 thf(func_def_1623, type, sK175: (($i > $i > $o) > $i)).
% 13.85/2.39 thf(func_def_1624, type, sK176: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_1625, type, sK177: ($i > $i)).
% 13.85/2.39 thf(func_def_1626, type, sK178: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_1627, type, sK179: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_1628, type, sK180: ($i > $i)).
% 13.85/2.39 thf(func_def_1629, type, sK181: ($i > $i)).
% 13.85/2.39 thf(func_def_1630, type, sK182: ($i > $i)).
% 13.85/2.39 thf(func_def_1631, type, sK183: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_1632, type, sK184: ($o > $i > $i)).
% 13.85/2.39 thf(func_def_1633, type, sK185: (($i > $i > $o) > $i)).
% 13.85/2.39 thf(func_def_1634, type, sK186: (($i > $i > $o) > $i)).
% 13.85/2.39 thf(func_def_1635, type, sK187: ($i > $i)).
% 13.85/2.39 thf(func_def_1636, type, sK188: ($i > $i > $i > $i)).
% 13.85/2.39 thf(func_def_1637, type, sK189: ($i > $i > $i > $i)).
% 13.85/2.39 thf(func_def_1638, type, sK190: ($i > $i > $i > $i)).
% 13.85/2.39 thf(func_def_1639, type, sK191: ($i > $i)).
% 13.85/2.39 thf(func_def_1640, type, sK192: ($i > $i)).
% 13.85/2.39 thf(func_def_1641, type, sK193: ($i > $i)).
% 13.85/2.39 thf(func_def_1642, type, sK194: ($i > $i)).
% 13.85/2.39 thf(func_def_1643, type, sK195: ($i > $i)).
% 13.85/2.39 thf(func_def_1644, type, sK196: ($i > $i)).
% 13.85/2.39 thf(func_def_1645, type, sK197: ($i > $o)).
% 13.85/2.39 thf(func_def_1646, type, sK198: ($i > $i)).
% 13.85/2.39 thf(func_def_1647, type, sK199: ($i > $i)).
% 13.85/2.39 thf(func_def_1648, type, sK200: ($i > $i)).
% 13.85/2.39 thf(func_def_1649, type, sK201: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_1650, type, sK202: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_1651, type, sK203: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_1652, type, sK204: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_1653, type, sK205: (($i > $i > $o) > $i)).
% 13.85/2.39 thf(func_def_1654, type, sK206: (($i > $i > $o) > $i)).
% 13.85/2.39 thf(func_def_1655, type, sK207: ($i > $i > $i > $i > $i)).
% 13.85/2.39 thf(func_def_1656, type, sK208: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_1657, type, sK209: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_1658, type, sK210: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_1659, type, sK211: ($i > $i)).
% 13.85/2.39 thf(func_def_1660, type, sK212: ($i > $i)).
% 13.85/2.39 thf(func_def_1661, type, sK213: ($i > $i)).
% 13.85/2.39 thf(func_def_1662, type, sK214: ($i > $i)).
% 13.85/2.39 thf(func_def_1663, type, sK215: ($i > $i)).
% 13.85/2.39 thf(func_def_1664, type, sK216: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_1665, type, sK217: ($i > $i > $i > $i > $i)).
% 13.85/2.39 thf(func_def_1666, type, sK218: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_1667, type, sK219: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_1668, type, sK220: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_1669, type, sK221: ($i > $i)).
% 13.85/2.39 thf(func_def_1670, type, sK222: ($i > $i)).
% 13.85/2.39 thf(func_def_1671, type, sK223: ($i > $i)).
% 13.85/2.39 thf(func_def_1672, type, sK224: ($i > $i)).
% 13.85/2.39 thf(func_def_1673, type, sK225: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_1674, type, sK226: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_1675, type, sK227: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_1676, type, sK228: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_1677, type, sK229: ($i > $i)).
% 13.85/2.39 thf(func_def_1678, type, sK230: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_1679, type, sK231: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_1680, type, sK232: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_1681, type, sK233: ($i > $o)).
% 13.85/2.39 thf(func_def_1682, type, sK234: ($i > $i)).
% 13.85/2.39 thf(func_def_1683, type, sK235: ($i > $i)).
% 13.85/2.39 thf(func_def_1684, type, sK236: ($i > $i)).
% 13.85/2.39 thf(func_def_1685, type, sK237: ($i > $i)).
% 13.85/2.39 thf(func_def_1686, type, sK238: ($i > $i > $i)).
% 13.85/2.39 thf(func_def_1687, type, sK239: ($i > $i)).
% 13.85/2.39 thf(func_def_1688, type, sK240: ($i > $i)).
% 13.85/2.39 thf(func_def_1689, type, sK241: ($i > $i)).
% 13.85/2.39 thf(func_def_1690, type, sK242: ($i > $i)).
% 13.85/2.39 thf(func_def_1691, type, sK243: ($i > $i)).
% 13.85/2.39 thf(func_def_1692, type, sK244: ($i > $i)).
% 13.85/2.39 thf(func_def_1693, type, sK245: ($i > $i)).
% 13.85/2.39 thf(func_def_1694, type, sK246: ($i > $i)).
% 13.85/2.39 thf(func_def_1695, type, sK247: ($i > $i > $i > $i)).
% 13.85/2.39 thf(func_def_1696, type, sK248: ($i > $i > $i > $i)).
% 13.85/2.39 thf(func_def_1697, type, sK249: ($i > $i)).
% 13.85/2.39 thf(func_def_1698, type, sK250: ($i > $i)).
% 13.85/2.39 thf(func_def_1699, type, sK251: ($i > $i)).
% 13.85/2.40 thf(func_def_1700, type, sK252: ($i > $i)).
% 13.85/2.40 thf(func_def_1701, type, sK253: ($i > $i)).
% 13.85/2.40 thf(func_def_1702, type, sK254: ($i > $i)).
% 13.85/2.40 thf(func_def_1703, type, sK255: ($i > $o)).
% 13.85/2.40 thf(func_def_1704, type, sK256: ($i > $i)).
% 13.85/2.40 thf(func_def_1705, type, sK257: ($i > $i > $i > $i > $i)).
% 13.85/2.40 thf(func_def_1706, type, sK258: ($i > $i > $i > $i > $i)).
% 13.85/2.40 thf(func_def_1707, type, sK259: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_1708, type, sK260: ($i > $i)).
% 13.85/2.40 thf(func_def_1709, type, sK261: ($i > $o)).
% 13.85/2.40 thf(func_def_1710, type, sK262: ($i > $i)).
% 13.85/2.40 thf(func_def_1711, type, sK263: ($i > $i)).
% 13.85/2.40 thf(func_def_1712, type, sK264: ($i > $i)).
% 13.85/2.40 thf(func_def_1713, type, sK265: ($i > $i > $i > $i)).
% 13.85/2.40 thf(func_def_1714, type, sK266: ($i > $i)).
% 13.85/2.40 thf(func_def_1715, type, sK267: ($i > $i)).
% 13.85/2.40 thf(func_def_1716, type, sK268: ($i > $i)).
% 13.85/2.40 thf(func_def_1717, type, sK269: ($i > $i)).
% 13.85/2.40 thf(func_def_1718, type, sK270: ($i > $i)).
% 13.85/2.40 thf(func_def_1719, type, sK271: ($i > $i)).
% 13.85/2.40 thf(func_def_1720, type, sK272: ($i > $i)).
% 13.85/2.40 thf(func_def_1721, type, sK273: ($i > $i)).
% 13.85/2.40 thf(func_def_1722, type, sK274: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_1723, type, sK275: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_1724, type, sK276: ($i > $i)).
% 13.85/2.40 thf(func_def_1725, type, sK277: ($i > $i > $i > $i)).
% 13.85/2.40 thf(func_def_1726, type, sK278: ($i > $i)).
% 13.85/2.40 thf(func_def_1727, type, sK279: ($i > $i)).
% 13.85/2.40 thf(func_def_1728, type, sK280: ($i > $o)).
% 13.85/2.40 thf(func_def_1729, type, sK281: ($i > $i)).
% 13.85/2.40 thf(func_def_1730, type, sK282: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_1731, type, sK283: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_1732, type, sK284: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_1733, type, sK285: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_1734, type, sK286: ($i > $i)).
% 13.85/2.40 thf(func_def_1735, type, sK287: ($i > $i)).
% 13.85/2.40 thf(func_def_1736, type, sK288: ($i > $i)).
% 13.85/2.40 thf(func_def_1737, type, sK289: ($i > $i)).
% 13.85/2.40 thf(func_def_1738, type, sK290: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_1739, type, sK291: ($i > $i)).
% 13.85/2.40 thf(func_def_1740, type, sK292: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_1741, type, sK293: ($i > $i)).
% 13.85/2.40 thf(func_def_1742, type, sK294: ($i > $i)).
% 13.85/2.40 thf(func_def_1743, type, sK295: ($i > $i)).
% 13.85/2.40 thf(func_def_1744, type, sK296: ($i > $i)).
% 13.85/2.40 thf(func_def_1745, type, sK297: ($i > $i)).
% 13.85/2.40 thf(func_def_1746, type, sK298: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_1747, type, sK299: ($i > $i)).
% 13.85/2.40 thf(func_def_1748, type, sK300: ($i > $i)).
% 13.85/2.40 thf(func_def_1749, type, sK301: ($i > $i)).
% 13.85/2.40 thf(func_def_1750, type, sK302: ($i > $i)).
% 13.85/2.40 thf(func_def_1751, type, sK303: ($i > $i)).
% 13.85/2.40 thf(func_def_1752, type, sK304: ($i > $i)).
% 13.85/2.40 thf(func_def_1753, type, sK305: ($i > $i)).
% 13.85/2.40 thf(func_def_1754, type, sK306: ($i > $i)).
% 13.85/2.40 thf(func_def_1755, type, sK307: ($i > $i)).
% 13.85/2.40 thf(func_def_1756, type, sK308: ($i > $o)).
% 13.85/2.40 thf(func_def_1757, type, sK309: ($i > $o)).
% 13.85/2.40 thf(func_def_1758, type, sK310: ($i > $i > $o)).
% 13.85/2.40 thf(func_def_1759, type, sK311: ($i > $i > $i > $i)).
% 13.85/2.40 thf(func_def_1760, type, sK312: ($i > $i)).
% 13.85/2.40 thf(func_def_1761, type, sK313: ($i > $i)).
% 13.85/2.40 thf(func_def_1762, type, sK314: ($i > $i)).
% 13.85/2.40 thf(func_def_1763, type, sK315: ($i > $i)).
% 13.85/2.40 thf(func_def_1764, type, sK316: ($i > $i)).
% 13.85/2.40 thf(func_def_1765, type, sK317: ($i > $i > $i > $i)).
% 13.85/2.40 thf(func_def_1766, type, sK318: ($i > $i)).
% 13.85/2.40 thf(func_def_1767, type, sK319: ($i > $i)).
% 13.85/2.40 thf(func_def_1768, type, sK320: ($i > $i)).
% 13.85/2.40 thf(func_def_1769, type, sK321: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_1770, type, sK322: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_1771, type, sK323: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_1772, type, sK324: ($i > $i)).
% 13.85/2.40 thf(func_def_1773, type, sK325: ($i > $i)).
% 13.85/2.40 thf(func_def_1774, type, sK326: ($i > $i > $i > $i)).
% 13.85/2.40 thf(func_def_1775, type, sK327: ($i > $i)).
% 13.85/2.40 thf(func_def_1776, type, sK328: ($i > $i)).
% 13.85/2.40 thf(func_def_1777, type, sK329: ($i > $o > $i > $i)).
% 13.85/2.40 thf(func_def_1778, type, sK330: ($i > $o > $i > $i)).
% 13.85/2.40 thf(func_def_1779, type, sK331: ($i > $o > $i > $i)).
% 13.85/2.40 thf(func_def_1780, type, sK332: ($i > $i)).
% 13.85/2.40 thf(func_def_1781, type, sK333: ($i > $i)).
% 13.85/2.40 thf(func_def_1782, type, sK334: ($i > $o)).
% 13.85/2.40 thf(func_def_1783, type, sK335: ($i > $o)).
% 13.85/2.40 thf(func_def_1784, type, sK336: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_1785, type, sK337: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_1786, type, sK338: ($i > $i)).
% 13.85/2.40 thf(func_def_1787, type, sK339: ($i > $i)).
% 13.85/2.40 thf(func_def_1788, type, sK340: ($i > $i)).
% 13.85/2.40 thf(func_def_1789, type, sK341: ($i > $i)).
% 13.85/2.40 thf(func_def_1790, type, sK342: ($i > $i)).
% 13.85/2.40 thf(func_def_1791, type, sK343: ($i > $i)).
% 13.85/2.40 thf(func_def_1792, type, sK344: ($i > $i)).
% 13.85/2.40 thf(func_def_1793, type, sK345: ($i > $i > $i > $i)).
% 13.85/2.40 thf(func_def_1794, type, sK346: ($i > $i > $i > $i)).
% 13.85/2.40 thf(func_def_1795, type, sK347: ($i > $i)).
% 13.85/2.40 thf(func_def_1796, type, sK348: ($i > $i)).
% 13.85/2.40 thf(func_def_1797, type, sK349: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_1798, type, sK350: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_1799, type, sK351: (($i > $i > $o) > $i)).
% 13.85/2.40 thf(func_def_1800, type, sK352: (($i > $i > $o) > $i)).
% 13.85/2.40 thf(func_def_1801, type, sK353: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_1802, type, sK354: ($i > $i)).
% 13.85/2.40 thf(func_def_1803, type, sK355: ($i > $i)).
% 13.85/2.40 thf(func_def_1804, type, sK356: ($i > $i)).
% 13.85/2.40 thf(func_def_1805, type, sK357: ($i > $i)).
% 13.85/2.40 thf(func_def_1806, type, sK358: ($i > $i)).
% 13.85/2.40 thf(func_def_1807, type, sK359: ($i > $i)).
% 13.85/2.40 thf(func_def_1808, type, sK360: (($i > $i > $o) > $i)).
% 13.85/2.40 thf(func_def_1809, type, sK361: (($i > $i > $o) > $i)).
% 13.85/2.40 thf(func_def_1810, type, sK362: (($i > $i > $o) > $i)).
% 13.85/2.40 thf(func_def_1811, type, sK363: ($i > $i)).
% 13.85/2.40 thf(func_def_1812, type, sK364: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_1813, type, sK365: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_1814, type, sK366: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_1815, type, sK367: ($i > $i)).
% 13.85/2.40 thf(func_def_1816, type, sK368: ($i > $i)).
% 13.85/2.40 thf(func_def_1817, type, sK369: ($i > $i)).
% 13.85/2.40 thf(func_def_1818, type, sK370: ($i > $i)).
% 13.85/2.40 thf(func_def_1819, type, sK371: ($i > $i)).
% 13.85/2.40 thf(func_def_1820, type, sK372: ($i > $i)).
% 13.85/2.40 thf(func_def_1821, type, sK373: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_1822, type, sK374: ($i > $i)).
% 13.85/2.40 thf(func_def_1823, type, sK375: ($i > $o)).
% 13.85/2.40 thf(func_def_1824, type, sK376: ($i > $i)).
% 13.85/2.40 thf(func_def_1825, type, sK377: ($i > $i)).
% 13.85/2.40 thf(func_def_1826, type, sK378: ($i > $i)).
% 13.85/2.40 thf(func_def_1827, type, sK379: ($i > $i)).
% 13.85/2.40 thf(func_def_1828, type, sK380: ($i > $i)).
% 13.85/2.40 thf(func_def_1829, type, sK381: ($i > $i)).
% 13.85/2.40 thf(func_def_1830, type, sK382: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_1831, type, sK383: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_1832, type, sK384: ($i > $i)).
% 13.85/2.40 thf(func_def_1833, type, sK385: ($i > $o)).
% 13.85/2.40 thf(func_def_1834, type, sK386: ($i > $i)).
% 13.85/2.40 thf(func_def_1835, type, sK387: ($i > $i)).
% 13.85/2.40 thf(func_def_1836, type, sK388: ($i > $i)).
% 13.85/2.40 thf(func_def_1837, type, sK389: ($i > $i)).
% 13.85/2.40 thf(func_def_1838, type, sK390: ($i > $i)).
% 13.85/2.40 thf(func_def_1839, type, sK391: ($i > $i > $i > $i)).
% 13.85/2.40 thf(func_def_1840, type, sK392: ($i > $i > $i > $i)).
% 13.85/2.40 thf(func_def_1841, type, sK393: ($i > $i)).
% 13.85/2.40 thf(func_def_1842, type, sK394: ($i > $i)).
% 13.85/2.40 thf(func_def_1843, type, sK395: ($i > $i)).
% 13.85/2.40 thf(func_def_1844, type, sK396: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_1845, type, sK397: ($i > $i)).
% 13.85/2.40 thf(func_def_1846, type, sK398: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_1847, type, sK399: ($i > $i)).
% 13.85/2.40 thf(func_def_1848, type, sK400: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_1849, type, sK401: ($i > $i)).
% 13.85/2.40 thf(func_def_1850, type, sK402: ($i > $i)).
% 13.85/2.40 thf(func_def_1851, type, sK403: ($i > $o > $i)).
% 13.85/2.40 thf(func_def_1852, type, sK404: ($i > $i)).
% 13.85/2.40 thf(func_def_1854, type, sK406: ($i > $i)).
% 13.85/2.40 thf(func_def_1855, type, sK407: ($i > $i)).
% 13.85/2.40 thf(func_def_1856, type, sK408: ($i > $i)).
% 13.85/2.40 thf(func_def_1857, type, sK409: ($i > $i)).
% 13.85/2.40 thf(func_def_1858, type, sK410: ($i > $i)).
% 13.85/2.40 thf(func_def_1859, type, sK411: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_1860, type, sK412: ($i > $i)).
% 13.85/2.40 thf(func_def_1861, type, sK413: ($i > $i)).
% 13.85/2.40 thf(func_def_1862, type, sK414: ($i > $i)).
% 13.85/2.40 thf(func_def_1863, type, sK415: ($i > $i)).
% 13.85/2.40 thf(func_def_1864, type, sK416: (($i > $i > $o) > $i > $i)).
% 13.85/2.40 thf(func_def_1865, type, sK417: (($i > $i > $o) > $i > $i)).
% 13.85/2.40 thf(func_def_1866, type, sK418: ($i > ($i > $i > $o) > $i > $i)).
% 13.85/2.40 thf(func_def_1867, type, sK419: ($i > ($i > $i > $o) > $i > $i)).
% 13.85/2.40 thf(func_def_1868, type, sK420: ($i > ($i > $i > $o) > $i > $i)).
% 13.85/2.40 thf(func_def_1869, type, sK421: ($i > $i > $i > $i)).
% 13.85/2.40 thf(func_def_1870, type, sK422: ($i > $i)).
% 13.85/2.40 thf(func_def_1871, type, sK423: ($i > $i)).
% 13.85/2.40 thf(func_def_1872, type, sK424: ($i > $i)).
% 13.85/2.40 thf(func_def_1873, type, sK425: ($i > $i)).
% 13.85/2.40 thf(func_def_1874, type, sK426: ($i > $i)).
% 13.85/2.40 thf(func_def_1875, type, sK427: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_1876, type, sK428: ($i > $i)).
% 13.85/2.40 thf(func_def_1877, type, sK429: ($i > $i)).
% 13.85/2.40 thf(func_def_1878, type, sK430: ($i > $i)).
% 13.85/2.40 thf(func_def_1879, type, sK431: ($i > $i > $o)).
% 13.85/2.40 thf(func_def_1880, type, sK432: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_1881, type, sK433: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_1882, type, sK434: ($i > $i)).
% 13.85/2.40 thf(func_def_1883, type, sK435: ($i > $i)).
% 13.85/2.40 thf(func_def_1884, type, sK436: ($i > $i)).
% 13.85/2.40 thf(func_def_1885, type, sK437: ($i > $i)).
% 13.85/2.40 thf(func_def_1886, type, sK438: ($i > $i)).
% 13.85/2.40 thf(func_def_1887, type, sK439: ($i > $i)).
% 13.85/2.40 thf(func_def_1888, type, sK440: ($i > $i)).
% 13.85/2.40 thf(func_def_1889, type, sK441: ($i > $i > $i > $i)).
% 13.85/2.40 thf(func_def_1890, type, sK442: ($i > $i)).
% 13.85/2.40 thf(func_def_1891, type, sK443: ($i > $i)).
% 13.85/2.40 thf(func_def_1892, type, sK444: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_1893, type, sK445: ($i > $i)).
% 13.85/2.40 thf(func_def_1894, type, sK446: ($i > $i)).
% 13.85/2.40 thf(func_def_1895, type, sK447: ($i > $i)).
% 13.85/2.40 thf(func_def_1896, type, sK448: ($i > $i)).
% 13.85/2.40 thf(func_def_1897, type, sK449: ($i > $i)).
% 13.85/2.40 thf(func_def_1898, type, sK450: ($i > $i)).
% 13.85/2.40 thf(func_def_1899, type, sK451: ($i > $i)).
% 13.85/2.40 thf(func_def_1900, type, sK452: ($i > $i)).
% 13.85/2.40 thf(func_def_1901, type, sK453: ($i > $i)).
% 13.85/2.40 thf(func_def_1902, type, sK454: ($o > $i)).
% 13.85/2.40 thf(func_def_1903, type, sK455: ($i > $i)).
% 13.85/2.40 thf(func_def_1904, type, sK456: ($i > $i)).
% 13.85/2.40 thf(func_def_1905, type, sK457: ($i > $i)).
% 13.85/2.40 thf(func_def_1906, type, sK458: ($i > $i > $i > $i)).
% 13.85/2.40 thf(func_def_1907, type, sK459: ($i > $i > $i > $i)).
% 13.85/2.40 thf(func_def_1908, type, sK460: ($i > $i)).
% 13.85/2.40 thf(func_def_1909, type, sK461: ($i > $i > $i > $o)).
% 13.85/2.40 thf(func_def_1910, type, sK462: ($i > $o > $i)).
% 13.85/2.40 thf(func_def_1911, type, sK463: ($i > $i > $i > $i)).
% 13.85/2.40 thf(func_def_1912, type, sK464: ($i > $i > $i > $i > $i > $i)).
% 13.85/2.40 thf(func_def_1913, type, sK465: ($i > $i)).
% 13.85/2.40 thf(func_def_1914, type, sK466: ($i > $i)).
% 13.85/2.40 thf(func_def_1915, type, sK467: ($i > $i)).
% 13.85/2.40 thf(func_def_1916, type, sK468: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_1917, type, sK469: ($i > $i)).
% 13.85/2.40 thf(func_def_1918, type, sK470: ($i > $i)).
% 13.85/2.40 thf(func_def_1919, type, sK471: ($i > $i)).
% 13.85/2.40 thf(func_def_1920, type, sK472: ($i > $i)).
% 13.85/2.40 thf(func_def_1921, type, sK473: ($i > $i)).
% 13.85/2.40 thf(func_def_1922, type, sK474: ($i > $i)).
% 13.85/2.40 thf(func_def_1923, type, sK475: ($i > $i)).
% 13.85/2.40 thf(func_def_1924, type, sK476: ($i > $i)).
% 13.85/2.40 thf(func_def_1925, type, sK477: ($i > $i > $i > $i)).
% 13.85/2.40 thf(func_def_1926, type, sK478: ($i > $i > $i > $i)).
% 13.85/2.40 thf(func_def_1927, type, sK479: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_1928, type, sK480: ($i > $i)).
% 13.85/2.40 thf(func_def_1929, type, sK481: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_1930, type, sK482: ($i > $i)).
% 13.85/2.40 thf(func_def_1931, type, sK483: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_1932, type, sK484: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_1933, type, sK485: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_1934, type, sK486: ($i > $i)).
% 13.85/2.40 thf(func_def_1935, type, sK487: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_1936, type, sK488: ($i > $i)).
% 13.85/2.40 thf(func_def_1937, type, sK489: ($i > $i)).
% 13.85/2.40 thf(func_def_1938, type, sK490: ($i > $i)).
% 13.85/2.40 thf(func_def_1939, type, sK491: ($i > $i)).
% 13.85/2.40 thf(func_def_1940, type, sK492: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_1941, type, sK493: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_1942, type, sK494: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_1943, type, sK495: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_1944, type, sK496: ($i > $i)).
% 13.85/2.40 thf(func_def_1945, type, sK497: ($i > $i)).
% 13.85/2.40 thf(func_def_1946, type, sK498: ($i > $i)).
% 13.85/2.40 thf(func_def_1947, type, sK499: ($i > $i)).
% 13.85/2.40 thf(func_def_1948, type, sK500: ($i > $i)).
% 13.85/2.40 thf(func_def_1949, type, sK501: ($i > $i > $o)).
% 13.85/2.40 thf(func_def_1950, type, sK502: ($i > $i)).
% 13.85/2.40 thf(func_def_1951, type, sK503: ($i > $o)).
% 13.85/2.40 thf(func_def_1952, type, sK504: ($o > $o > $i)).
% 13.85/2.40 thf(func_def_1953, type, sK505: ($o > $o > $i)).
% 13.85/2.40 thf(func_def_1954, type, sK506: ($i > $o > $i)).
% 13.85/2.40 thf(func_def_1955, type, sK507: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_1956, type, sK508: ($i > $i)).
% 13.85/2.40 thf(func_def_1957, type, sK509: ($i > $i)).
% 13.85/2.40 thf(func_def_1958, type, sK510: ($i > $i)).
% 13.85/2.40 thf(func_def_1959, type, sK511: ($i > $i)).
% 13.85/2.40 thf(func_def_1960, type, sK512: ($i > $i)).
% 13.85/2.40 thf(func_def_1961, type, sK513: ($i > $i)).
% 13.85/2.40 thf(func_def_1962, type, sK514: ($i > $i)).
% 13.85/2.40 thf(func_def_1963, type, sK515: (($i > $i > $o) > $i)).
% 13.85/2.40 thf(func_def_1964, type, sK516: (($i > $i > $o) > $i)).
% 13.85/2.40 thf(func_def_1965, type, sK517: ($i > $i)).
% 13.85/2.40 thf(func_def_1966, type, sK518: ($i > $i)).
% 13.85/2.40 thf(func_def_1967, type, sK519: ($i > $i > $i > $i)).
% 13.85/2.40 thf(func_def_1968, type, sK520: ($i > $i > $i > $i > $o)).
% 13.85/2.40 thf(func_def_1969, type, sK521: ($i > $i)).
% 13.85/2.40 thf(func_def_1970, type, sK522: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_1971, type, sK523: ($i > $i)).
% 13.85/2.40 thf(func_def_1972, type, sK524: ($i > $i)).
% 13.85/2.40 thf(func_def_1973, type, sK525: ($i > $i)).
% 13.85/2.40 thf(func_def_1974, type, sK526: ($i > $i)).
% 13.85/2.40 thf(func_def_1975, type, sK527: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_1976, type, sK528: ($i > $i)).
% 13.85/2.40 thf(func_def_1977, type, sK529: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_1978, type, sK530: ($i > $i)).
% 13.85/2.40 thf(func_def_1979, type, sK531: ($i > $i)).
% 13.85/2.40 thf(func_def_1980, type, sK532: ($i > $i)).
% 13.85/2.40 thf(func_def_1981, type, sK533: ($i > $i)).
% 13.85/2.40 thf(func_def_1982, type, sK534: ($i > $i)).
% 13.85/2.40 thf(func_def_1983, type, sK535: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_1984, type, sK536: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_1985, type, sK537: ($i > $i > $i > $i)).
% 13.85/2.40 thf(func_def_1986, type, sK538: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_1987, type, sK539: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_1988, type, sK540: ($i > $i)).
% 13.85/2.40 thf(func_def_1989, type, sK541: ($i > $i)).
% 13.85/2.40 thf(func_def_1990, type, sK542: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_1991, type, sK543: ($i > $i > $o)).
% 13.85/2.40 thf(func_def_1992, type, sK544: ($i > $i)).
% 13.85/2.40 thf(func_def_1993, type, sK545: ($i > $i)).
% 13.85/2.40 thf(func_def_1994, type, sK546: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_1995, type, sK547: ($i > $i)).
% 13.85/2.40 thf(func_def_1996, type, sK548: ($i > $i)).
% 13.85/2.40 thf(func_def_1997, type, sK549: ($i > $i)).
% 13.85/2.40 thf(func_def_1998, type, sK550: ($i > $i)).
% 13.85/2.40 thf(func_def_1999, type, sK551: ($i > $i)).
% 13.85/2.40 thf(func_def_2000, type, sK552: ($i > $i)).
% 13.85/2.40 thf(func_def_2001, type, sK553: ($i > $i)).
% 13.85/2.40 thf(func_def_2002, type, sK554: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_2003, type, sK555: ($i > $i)).
% 13.85/2.40 thf(func_def_2004, type, sK556: ($i > $i)).
% 13.85/2.40 thf(func_def_2005, type, sK557: ($i > $i)).
% 13.85/2.40 thf(func_def_2006, type, sK558: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_2007, type, sK559: ($i > $i)).
% 13.85/2.40 thf(func_def_2008, type, sK560: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_2009, type, sK561: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_2010, type, sK562: ($i > $i)).
% 13.85/2.40 thf(func_def_2011, type, sK563: ($i > $i)).
% 13.85/2.40 thf(func_def_2012, type, sK564: ($i > $o)).
% 13.85/2.40 thf(func_def_2013, type, sK565: ($i > $i)).
% 13.85/2.40 thf(func_def_2014, type, sK566: ($i > $i)).
% 13.85/2.40 thf(func_def_2015, type, sK567: ($i > $i)).
% 13.85/2.40 thf(func_def_2016, type, sK568: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_2017, type, sK569: ($i > $i)).
% 13.85/2.40 thf(func_def_2018, type, sK570: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_2019, type, sK571: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_2020, type, sK572: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_2021, type, sK573: ($i > $i)).
% 13.85/2.40 thf(func_def_2022, type, sK574: ($o > $i > $i)).
% 13.85/2.40 thf(func_def_2023, type, sK575: ($i > $i)).
% 13.85/2.40 thf(func_def_2024, type, sK576: ($i > $i)).
% 13.85/2.40 thf(func_def_2025, type, sK577: ($i > $i)).
% 13.85/2.40 thf(func_def_2026, type, sK578: ($i > $o)).
% 13.85/2.40 thf(func_def_2027, type, sK579: ($i > $i)).
% 13.85/2.40 thf(func_def_2028, type, sK580: ($i > $i)).
% 13.85/2.40 thf(func_def_2029, type, sK581: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_2030, type, sK582: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_2031, type, sK583: ($i > $i)).
% 13.85/2.40 thf(func_def_2032, type, sK584: ($i > $i > $i > $i)).
% 13.85/2.40 thf(func_def_2033, type, sK585: ($i > $i)).
% 13.85/2.40 thf(func_def_2034, type, sK586: ($i > $i)).
% 13.85/2.40 thf(func_def_2035, type, sK587: ($i > $i)).
% 13.85/2.40 thf(func_def_2036, type, sK588: ($i > $i)).
% 13.85/2.40 thf(func_def_2037, type, sK589: ($i > $i)).
% 13.85/2.40 thf(func_def_2038, type, sK590: ($i > $i)).
% 13.85/2.40 thf(func_def_2039, type, sK591: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_2040, type, sK592: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_2041, type, sK593: ($i > $i)).
% 13.85/2.40 thf(func_def_2042, type, sK594: ($i > $i)).
% 13.85/2.40 thf(func_def_2043, type, sK595: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_2044, type, sK596: ($i > $i > $i)).
% 13.85/2.40 thf(func_def_2045, type, sK597: ($i > $i > $i)).
% 13.85/2.40 thf(f3578,axiom,(
% 13.85/2.40 (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i) & (likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i))),
% 13.85/2.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax)).
% 13.85/2.40 thf(f3579,conjecture,(
% 13.85/2.40 (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i) & (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i))),
% 13.85/2.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p',con)).
% 13.85/2.40 thf(f3580,negated_conjecture,(
% 13.85/2.40 ~(holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i) & (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i))),
% 13.85/2.40 inference(negated_conjecture,[status(cth)],[f3579])).
% 13.85/2.40 thf(f10629,plain,(
% 13.85/2.40 (holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i) & (likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i))),
% 13.85/2.40 inference(rectify,[],[f3578])).
% 13.85/2.40 thf(f10630,plain,(
% 13.85/2.40 ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ ((likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i) & (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i)))))),
% 13.85/2.40 inference(fool_elimination,[],[f10629])).
% 13.85/2.40 thf(f10631,plain,(
% 13.85/2.40 ~(holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i) & (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i))),
% 13.85/2.40 inference(rectify,[],[f3580])).
% 13.85/2.40 thf(f10632,plain,(
% 13.85/2.40 ~ ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ ((likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i) & (likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i)))))),
% 13.85/2.40 inference(fool_elimination,[],[f10631])).
% 13.85/2.40 thf(f10633,plain,(
% 13.85/2.40 ($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ ((likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i) & (likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i)))))),
% 13.85/2.40 inference(flattening,[],[f10632])).
% 13.85/2.40 thf(f17191,plain,(
% 13.85/2.40 ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ ((likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i) & (likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i)))))),
% 13.85/2.40 inference(cnf_transformation,[],[f10630])).
% 13.85/2.40 thf(f17192,plain,(
% 13.85/2.40 ($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ ((likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i) & (likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i)))))),
% 13.85/2.40 inference(cnf_transformation,[],[f10633])).
% 13.85/2.40 thf(f17194,definition,(
% 13.85/2.40 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 13.85/2.40 introduced(theory,[fool_exhaustiveness_axiom])).
% 13.85/2.40 thf(f17786,plain,(
% 13.85/2.40 ($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ ($true & (likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i))))) | (((likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i)) = $false)),
% 13.85/2.40 inference(constrained_superposition,[],[f17192,f17194])).
% 13.85/2.40 thf(f17792,plain,(
% 13.85/2.40 ($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i)))) | (((likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i)) = $false)),
% 13.85/2.40 inference(boolean_simplification,[],[f17786])).
% 13.85/2.40 thf(f17799,definition,(
% 13.85/2.40 spl598_8 <=> (((likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i)) = $false)),
% 13.85/2.40 introduced(definition,[new_symbols(definition,[spl598_8])],[avatar_definition])).
% 13.85/2.40 thf(f17801,plain,(
% 13.85/2.40 (((likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i)) = $false) | ~spl598_8),
% 13.85/2.40 inference(avatar_component_clause,[],[f17799])).
% 13.85/2.40 thf(f17812,definition,(
% 13.85/2.40 spl598_11 <=> ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i))))),
% 13.85/2.40 introduced(definition,[new_symbols(definition,[spl598_11])],[avatar_definition])).
% 13.85/2.40 thf(f17814,plain,(
% 13.85/2.40 ($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i)))) | spl598_11),
% 13.85/2.40 inference(avatar_component_clause,[],[f17812])).
% 13.85/2.40 thf(f17815,plain,(
% 13.85/2.40 spl598_8 | ~spl598_11),
% 13.85/2.40 inference(avatar_split_clause,[],[f17792,f17812,f17799])).
% 13.85/2.40 thf(f17837,plain,(
% 13.85/2.40 ($true != $true) | ($false = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i)))) | spl598_11),
% 13.85/2.40 inference(constrained_superposition,[],[f17814,f17194])).
% 13.85/2.40 thf(f17839,plain,(
% 13.85/2.40 ($false = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i)))) | spl598_11),
% 13.85/2.40 inference(trivial_inequality_removal,[],[f17837])).
% 13.85/2.40 thf(f17856,plain,(
% 13.85/2.40 ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ ((likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i) & $true)))) | (((likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i)) = $false)),
% 13.85/2.40 inference(constrained_superposition,[],[f17191,f17194])).
% 13.85/2.40 thf(f17867,plain,(
% 13.85/2.40 ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ (likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i)))) | (((likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i)) = $false)),
% 13.85/2.40 inference(boolean_simplification,[],[f17856])).
% 13.85/2.40 thf(f17874,plain,(
% 13.85/2.40 ($true = $false) | (((likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i)) = $false) | spl598_11),
% 13.85/2.40 inference(forward_demodulation,[],[f17867,f17839])).
% 13.85/2.40 thf(f17875,plain,(
% 13.85/2.40 (((likes_THFTYPE_IiioI @ lSue_THFTYPE_i @ lBill_THFTYPE_i)) = $false) | spl598_11),
% 13.85/2.40 inference(trivial_inequality_removal,[],[f17874])).
% 13.85/2.40 thf(f17878,plain,(
% 13.85/2.40 spl598_8 | spl598_11),
% 13.85/2.40 inference(avatar_split_clause,[],[f17875,f17812,f17799])).
% 13.85/2.40 thf(f17880,plain,(
% 13.85/2.40 ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ ((likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i) & $false)))) | ~spl598_8),
% 13.85/2.40 inference(constrained_superposition,[],[f17191,f17801])).
% 13.85/2.40 thf(f17882,plain,(
% 13.85/2.40 ($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ ($false & (likes_THFTYPE_IiioI @ lMary_THFTYPE_i @ lBill_THFTYPE_i))))) | ~spl598_8),
% 13.85/2.40 inference(constrained_superposition,[],[f17192,f17801])).
% 13.85/2.40 thf(f17883,plain,(
% 13.85/2.40 ($true != ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $false))) | ~spl598_8),
% 13.85/2.40 inference(boolean_simplification,[],[f17882])).
% 13.85/2.40 thf(f17884,plain,(
% 13.85/2.40 ($true = ((holdsDuring_THFTYPE_IiooI @ (lYearFn_THFTYPE_IiiI @ n2009_THFTYPE_i) @ $false))) | ~spl598_8),
% 13.85/2.40 inference(boolean_simplification,[],[f17880])).
% 13.85/2.40 thf(f17886,plain,(
% 13.85/2.40 $false | ~spl598_8),
% 13.85/2.40 inference(global_subsumption,[],[f17884,f17883])).
% 13.85/2.40 thf(f17887,plain,(
% 13.85/2.40 ~spl598_8),
% 13.85/2.40 inference(avatar_contradiction_clause,[],[f17886])).
% 13.85/2.40 cnf(s4430, plain, spl598_8 | ~spl598_11, inference(sat_conversion,[],[f17815])).
% 13.85/2.40 cnf(s4452, plain, spl598_8 | spl598_11, inference(sat_conversion,[],[f17878])).
% 13.85/2.40 cnf(s4457, plain, ~spl598_8, inference(sat_conversion,[],[f17887])).
% 13.85/2.40 cnf(s4458, plain, spl598_11, inference(rat,[],[s4452,s4457])).
% 13.85/2.40 cnf(s4462, plain, $false, inference(rat,[],[s4430,s4458,s4457])).
% 13.85/2.40 thf(f17888,plain,(
% 13.85/2.40 $false),
% 13.85/2.40 inference(avatar_sat_refutation,[],[s4462])).
% 13.85/2.40 % SZS output end Proof for theBenchmark
% 13.85/2.40 % (2850122)------------------------------
% 13.85/2.40 % (2850122)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.85/2.40 % (2850122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.85/2.40 % (2850122)CaDiCaL version: 2.1.3
% 13.85/2.40 % (2850122)Termination reason: Refutation
% 13.85/2.40 % (2850122)Time elapsed: 0.525 s
% 13.85/2.40 % (2850122)Peak memory usage: 28 MB
% 13.85/2.40 % (2850122)Instructions burned: 1148 (million)
% 13.85/2.40 % (2849971)Success in time 2.172 s
% 13.85/2.40 % Vampire exiting
%------------------------------------------------------------------------------