%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SYO879^1 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n026.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 08:50:30 AM UTC 2026
% Result : Theorem 7.51s 1.73s
% Output : Refutation 7.51s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SYO879^1 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.08 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.13/0.27 % Computer : n026.cluster.edu
% 0.13/0.27 % Model : x86_64 x86_64
% 0.13/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.27 % Memory : 8046.5625MB
% 0.13/0.27 % OS : Linux 6.8.0-71-generic
% 0.13/0.28 % CPULimit : 300
% 0.13/0.28 % WCLimit : 300
% 0.13/0.28 % DateTime : Tue Sep 29 17:26:27 UTC 2026
% 0.13/0.28 % CPUTime :
% 0.13/0.28 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.27/0.33 Running first-order model finding
% 0.27/0.33 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 7.23/1.70 % (905804)Will run a generic schedule for satisfiability detection.
% 7.23/1.70 % (905809)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3562052445_2999 on theBenchmark for (2999ds/0Mi)
% 7.23/1.70 % (905810)% WARNING: option uhcvi not known.
% 7.23/1.70 % (905810)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3933846991:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 7.23/1.70 % (905812)dis+10_1_sil=32000:sp=arity:random_seed=4005918978:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 7.23/1.70 % (905814)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3617702184:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 7.23/1.70 % (905813)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=595594866:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 7.23/1.70 % (905811)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3228194061:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 7.23/1.70 % (905815)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=23157316:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 7.23/1.70 % Exception at run slice level
% 7.23/1.70 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 7.23/1.70 % (905813)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 7.23/1.70 % (905810)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 7.23/1.70 % (905823)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=524189054:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 7.23/1.70 % (905810)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 7.23/1.70 % (905812)Instruction limit reached!
% 7.23/1.70 % (905812)------------------------------
% 7.23/1.70 % (905812)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.23/1.70 % (905812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.23/1.70 % (905812)CaDiCaL version: 2.1.3
% 7.23/1.70 % (905812)Termination reason: Instruction limit
% 7.23/1.70 % (905812)Termination phase: Saturation
% 7.23/1.70 % (905812)Time elapsed: 0.080 s
% 7.23/1.70 % (905812)Peak memory usage: 13 MB
% 7.23/1.70 % (905812)Instructions burned: 103 (million)
% 7.23/1.70 % (905813)Instruction limit reached!
% 7.23/1.70 % (905813)------------------------------
% 7.23/1.70 % (905813)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.23/1.70 % (905813)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.23/1.70 % (905813)CaDiCaL version: 2.1.3
% 7.23/1.70 % (905813)Termination reason: Instruction limit
% 7.23/1.70 % (905813)Termination phase: Saturation
% 7.23/1.70 % (905813)Time elapsed: 0.088 s
% 7.23/1.70 % (905813)Peak memory usage: 13 MB
% 7.23/1.70 % (905813)Instructions burned: 116 (million)
% 7.23/1.70 % (905814)Instruction limit reached!
% 7.23/1.70 % (905814)------------------------------
% 7.23/1.70 % (905814)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.23/1.70 % (905814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.23/1.70 % (905814)CaDiCaL version: 2.1.3
% 7.23/1.70 % (905814)Termination reason: Instruction limit
% 7.23/1.70 % (905814)Termination phase: Saturation
% 7.23/1.70 % (905814)Time elapsed: 0.103 s
% 7.23/1.70 % (905814)Peak memory usage: 13 MB
% 7.23/1.70 % (905814)Instructions burned: 132 (million)
% 7.23/1.70 % Exception at run slice level
% 7.23/1.70 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 7.23/1.70 % (905825)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=594504860:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 7.23/1.70 % (905826)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=2851009766:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 7.23/1.70 % (905815)Instruction limit reached!
% 7.23/1.70 % (905815)------------------------------
% 7.23/1.70 % (905815)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.23/1.70 % (905815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.23/1.70 % (905815)CaDiCaL version: 2.1.3
% 7.23/1.70 % (905815)Termination reason: Instruction limit
% 7.23/1.70 % (905815)Termination phase: Saturation
% 7.51/1.73 % (905815)Time elapsed: 0.126 s
% 7.51/1.73 % (905815)Peak memory usage: 13 MB
% 7.51/1.73 % (905815)Instructions burned: 160 (million)
% 7.51/1.73 % (905828)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3435412289:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 7.51/1.73 % (905827)ott-21_1_sil=16000:fs=off:random_seed=257805051:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 7.51/1.73 % (905826)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 7.51/1.73 % (905832)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1239666305:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 7.51/1.73 % (905826)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 7.51/1.73 % (905825)Instruction limit reached!
% 7.51/1.73 % (905825)------------------------------
% 7.51/1.73 % (905825)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.51/1.73 % (905825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.51/1.73 % (905825)CaDiCaL version: 2.1.3
% 7.51/1.73 % (905825)Termination reason: Instruction limit
% 7.51/1.73 % (905825)Termination phase: Saturation
% 7.51/1.73 % (905825)Time elapsed: 0.105 s
% 7.51/1.73 % (905825)Peak memory usage: 13 MB
% 7.51/1.73 % (905825)Instructions burned: 131 (million)
% 7.51/1.73 % Exception at run slice level
% 7.51/1.73 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 7.51/1.73 % (905835)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3896717168:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 7.51/1.73 % (905836)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2490161721:i=889:ins=1_2997 on theBenchmark for (2997ds/889Mi)
% 7.51/1.73 % (905827)Instruction limit reached!
% 7.51/1.73 % (905827)------------------------------
% 7.51/1.73 % (905827)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.51/1.73 % (905827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.51/1.73 % (905827)CaDiCaL version: 2.1.3
% 7.51/1.73 % (905827)Termination reason: Instruction limit
% 7.51/1.73 % (905827)Termination phase: Saturation
% 7.51/1.73 % (905827)Time elapsed: 0.143 s
% 7.51/1.73 % (905827)Peak memory usage: 13 MB
% 7.51/1.73 % (905827)Instructions burned: 180 (million)
% 7.51/1.73 % (905839)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=1868799683:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2996 on theBenchmark for (2996ds/692Mi)
% 7.51/1.73 % Exception at run slice level
% 7.51/1.73 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 7.51/1.73 % (905839)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 7.51/1.73 % (905828)Instruction limit reached!
% 7.51/1.73 % (905828)------------------------------
% 7.51/1.73 % (905828)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.51/1.73 % (905828)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.51/1.73 % (905828)CaDiCaL version: 2.1.3
% 7.51/1.73 % (905828)Termination reason: Instruction limit
% 7.51/1.73 % (905828)Termination phase: Saturation
% 7.51/1.73 % (905828)Time elapsed: 0.212 s
% 7.51/1.73 % (905828)Peak memory usage: 15 MB
% 7.51/1.73 % (905828)Instructions burned: 478 (million)
% 7.51/1.73 % (905841)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2005269098:i=879:kws=inv_precedence:fsr=off_2996 on theBenchmark for (2996ds/879Mi)
% 7.51/1.73 % (905841)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 7.51/1.73 % (905842)fmb+10_1_sil=64000:random_seed=2723720454:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi)
% 7.51/1.73 % (905842)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 7.51/1.73 % Exception at run slice level
% 7.51/1.73 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 7.51/1.73 % (905845)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=3874138471:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi)
% 7.51/1.73 % Exception at run slice level
% 7.51/1.73 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 7.51/1.73 % (905847)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1274244914:fmbsr=1.7:i=920_2994 on theBenchmark for (2994ds/920Mi)
% 7.51/1.73 % Exception at run slice level
% 7.51/1.73 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 7.51/1.73 % (905826)Instruction limit reached!
% 7.51/1.73 % (905826)------------------------------
% 7.51/1.73 % (905826)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.51/1.73 % (905826)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.51/1.73 % (905826)CaDiCaL version: 2.1.3
% 7.51/1.73 % (905826)Termination reason: Instruction limit
% 7.51/1.73 % (905826)Termination phase: Saturation
% 7.51/1.73 % (905826)Time elapsed: 0.558 s
% 7.51/1.73 % (905826)Peak memory usage: 17 MB
% 7.51/1.73 % (905826)Instructions burned: 685 (million)
% 7.51/1.73 % (905849)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=357865812:i=5131_2993 on theBenchmark for (2993ds/5131Mi)
% 7.51/1.73 % (905849)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 7.51/1.73 % (905851)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3997728525:i=1472:ins=7:fdi=8:gsp=on_2992 on theBenchmark for (2992ds/1472Mi)
% 7.51/1.73 % (905851)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 7.51/1.73 % (905851)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 7.51/1.73 % (905841)Instruction limit reached!
% 7.51/1.73 % (905841)------------------------------
% 7.51/1.73 % (905841)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.51/1.73 % (905841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.51/1.73 % (905841)CaDiCaL version: 2.1.3
% 7.51/1.73 % (905841)Termination reason: Instruction limit
% 7.51/1.73 % (905841)Termination phase: Saturation
% 7.51/1.73 % (905841)Time elapsed: 0.459 s
% 7.51/1.73 % (905841)Peak memory usage: 17 MB
% 7.51/1.73 % (905841)Instructions burned: 880 (million)
% 7.51/1.73 % (905853)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2000548123:i=6324_2991 on theBenchmark for (2991ds/6324Mi)
% 7.51/1.73 % (905839)Instruction limit reached!
% 7.51/1.73 % (905839)------------------------------
% 7.51/1.73 % (905839)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.51/1.73 % (905839)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.51/1.73 % (905839)CaDiCaL version: 2.1.3
% 7.51/1.73 % (905839)Termination reason: Instruction limit
% 7.51/1.73 % (905839)Termination phase: Saturation
% 7.51/1.73 % (905839)Time elapsed: 0.555 s
% 7.51/1.73 % (905839)Peak memory usage: 16 MB
% 7.51/1.73 % (905839)Instructions burned: 692 (million)
% 7.51/1.73 % (905855)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=881599610:fmbsr=2.30978:i=2174_2990 on theBenchmark for (2990ds/2174Mi)
% 7.51/1.73 % Exception at run slice level
% 7.51/1.73 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 7.51/1.73 % (905857)ott-2_1_sil=16000:newcnf=on:random_seed=1039947038:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2990 on theBenchmark for (2990ds/869Mi)
% 7.51/1.73 % Exception at run slice level
% 7.51/1.73 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 7.51/1.73 % (905857)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 7.51/1.73 % (905859)ott+10_1_sil=32000:tgt=ground:random_seed=3435936797:i=5114:av=off_2989 on theBenchmark for (2989ds/5114Mi)
% 7.51/1.73 % (905835)Instruction limit reached!
% 7.51/1.73 % (905835)------------------------------
% 7.51/1.73 % (905835)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.51/1.73 % (905835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.51/1.73 % (905835)CaDiCaL version: 2.1.3
% 7.51/1.73 % (905835)Termination reason: Instruction limit
% 7.51/1.73 % (905835)Termination phase: Saturation
% 7.51/1.73 % (905835)Time elapsed: 0.911 s
% 7.51/1.73 % (905835)Peak memory usage: 17 MB
% 7.51/1.73 % (905835)Instructions burned: 1180 (million)
% 7.51/1.73 % (905861)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=247123276:i=54282_2987 on theBenchmark for (2987ds/54282Mi)
% 7.51/1.73 % Exception at run slice level
% 7.51/1.73 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 7.51/1.73 % (905863)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=3208777449:i=3512:aac=none_2986 on theBenchmark for (2986ds/3512Mi)
% 7.51/1.73 % (905857) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-905804-905857"...
% 7.51/1.73 % (905857)...printing done.
% 7.51/1.73 % (905857)Refutation found. Thanks to Tanya!
% 7.51/1.73 % SZS status Theorem for theBenchmark
% 7.51/1.73 % SZS output start Proof for theBenchmark
% 7.51/1.73 thf(type_def_5, type, sTfun: ($tType * $tType) > $tType).
% 7.51/1.73 thf(func_def_0, type, c_Eps_i: (($i > $o) > $i)).
% 7.51/1.73 thf(func_def_1, type, c_False: $o).
% 7.51/1.73 thf(func_def_2, type, c_True: $o).
% 7.51/1.73 thf(func_def_3, type, c_not: ($o > $o)).
% 7.51/1.73 thf(func_def_4, type, c_and: ($o > $o > $o)).
% 7.51/1.73 thf(func_def_5, type, c_or: ($o > $o > $o)).
% 7.51/1.73 thf(func_def_6, type, c_iff: ($o > $o > $o)).
% 7.51/1.73 thf(func_def_7, type, c_In: ($i > $i > $o)).
% 7.51/1.73 thf(func_def_8, type, c_Subq: ($i > $i > $o)).
% 7.51/1.73 thf(func_def_10, type, c_Union: ($i > $i)).
% 7.51/1.73 thf(func_def_11, type, c_Power: ($i > $i)).
% 7.51/1.73 thf(func_def_12, type, c_Repl: ($i > ($i > $i) > $i)).
% 7.51/1.73 thf(func_def_13, type, c_TransSet: ($i > $o)).
% 7.51/1.73 thf(func_def_14, type, c_atleast2: ($i > $o)).
% 7.51/1.73 thf(func_def_15, type, c_atleast3: ($i > $o)).
% 7.51/1.73 thf(func_def_16, type, c_atleast4: ($i > $o)).
% 7.51/1.73 thf(func_def_17, type, c_atleast5: ($i > $o)).
% 7.51/1.73 thf(func_def_18, type, c_atleast6: ($i > $o)).
% 7.51/1.73 thf(func_def_19, type, c_exactly2: ($i > $o)).
% 7.51/1.73 thf(func_def_20, type, c_exactly3: ($i > $o)).
% 7.51/1.73 thf(func_def_21, type, c_exactly4: ($i > $o)).
% 7.51/1.73 thf(func_def_22, type, c_exactly5: ($i > $o)).
% 7.51/1.73 thf(func_def_23, type, c_exu_i: (($i > $o) > $o)).
% 7.51/1.73 thf(func_def_24, type, c_reflexive_i: (($i > $i > $o) > $o)).
% 7.51/1.73 thf(func_def_25, type, c_irreflexive_i: (($i > $i > $o) > $o)).
% 7.51/1.73 thf(func_def_26, type, c_symmetric_i: (($i > $i > $o) > $o)).
% 7.51/1.73 thf(func_def_27, type, c_antisymmetric_i: (($i > $i > $o) > $o)).
% 7.51/1.73 thf(func_def_28, type, c_transitive_i: (($i > $i > $o) > $o)).
% 7.51/1.73 thf(func_def_29, type, c_eqreln_i: (($i > $i > $o) > $o)).
% 7.51/1.73 thf(func_def_30, type, c_per_i: (($i > $i > $o) > $o)).
% 7.51/1.73 thf(func_def_31, type, c_linear_i: (($i > $i > $o) > $o)).
% 7.51/1.73 thf(func_def_32, type, c_trichotomous_or_i: (($i > $i > $o) > $o)).
% 7.51/1.73 thf(func_def_33, type, c_partialorder_i: (($i > $i > $o) > $o)).
% 7.51/1.73 thf(func_def_34, type, c_totalorder_i: (($i > $i > $o) > $o)).
% 7.51/1.73 thf(func_def_35, type, c_strictpartialorder_i: (($i > $i > $o) > $o)).
% 7.51/1.73 thf(func_def_36, type, c_stricttotalorder_i: (($i > $i > $o) > $o)).
% 7.51/1.73 thf(func_def_37, type, c_If_i: ($o > $i > $i > $i)).
% 7.51/1.73 thf(func_def_38, type, c_exactly1of2: ($o > $o > $o)).
% 7.51/1.73 thf(func_def_39, type, c_exactly1of3: ($o > $o > $o > $o)).
% 7.51/1.73 thf(func_def_40, type, c_nIn: ($i > $i > $o)).
% 7.51/1.73 thf(func_def_41, type, c_nSubq: ($i > $i > $o)).
% 7.51/1.73 thf(func_def_42, type, c_UPair: ($i > $i > $i)).
% 7.51/1.73 thf(func_def_43, type, c_Sing: ($i > $i)).
% 7.51/1.73 thf(func_def_44, type, c_binunion: ($i > $i > $i)).
% 7.51/1.73 thf(func_def_45, type, c_SetAdjoin: ($i > $i > $i)).
% 7.51/1.73 thf(func_def_46, type, c_famunion: ($i > ($i > $i) > $i)).
% 7.51/1.73 thf(func_def_47, type, c_Sep: ($i > ($i > $o) > $i)).
% 7.51/1.73 thf(func_def_48, type, c_ReplSep: ($i > ($i > $o) > ($i > $i) > $i)).
% 7.51/1.73 thf(func_def_49, type, c_binintersect: ($i > $i > $i)).
% 7.51/1.73 thf(func_def_50, type, c_setminus: ($i > $i > $i)).
% 7.51/1.73 thf(func_def_51, type, c_inj: ($i > $i > ($i > $i) > $o)).
% 7.51/1.73 thf(func_def_52, type, c_bij: ($i > $i > ($i > $i) > $o)).
% 7.51/1.73 thf(func_def_53, type, c_atleastp: ($i > $i > $o)).
% 7.51/1.73 thf(func_def_54, type, c_equip: ($i > $i > $o)).
% 7.51/1.73 thf(func_def_55, type, c_In_rec_poly_G_i: (($i > ($i > $i) > $i) > $i > $i > $o)).
% 7.51/1.73 thf(func_def_56, type, c_In_rec_poly_i: (($i > ($i > $i) > $i) > $i > $i)).
% 7.51/1.73 thf(func_def_57, type, c_ordsucc: ($i > $i)).
% 7.51/1.73 thf(func_def_58, type, c_nat_p: ($i > $o)).
% 7.51/1.73 thf(func_def_59, type, c_nat_primrec: ($i > ($i > $i > $i) > $i > $i)).
% 7.51/1.73 thf(func_def_60, type, c_add_nat: ($i > $i > $i)).
% 7.51/1.73 thf(func_def_61, type, c_mul_nat: ($i > $i > $i)).
% 7.51/1.73 thf(func_def_62, type, c_ordinal: ($i > $o)).
% 7.51/1.73 thf(func_def_63, type, c_V_: ($i > $i)).
% 7.51/1.73 thf(func_def_64, type, c_Inj1: ($i > $i)).
% 7.51/1.73 thf(func_def_65, type, c_Inj0: ($i > $i)).
% 7.51/1.73 thf(func_def_66, type, c_Unj: ($i > $i)).
% 7.51/1.73 thf(func_def_67, type, c_combine_funcs: ($i > $i > ($i > $i) > ($i > $i) > $i > $i)).
% 7.51/1.73 thf(func_def_68, type, c_setsum: ($i > $i > $i)).
% 7.51/1.73 thf(func_def_69, type, c_proj0: ($i > $i)).
% 7.51/1.73 thf(func_def_70, type, c_proj1: ($i > $i)).
% 7.51/1.73 thf(func_def_71, type, c_binrep: ($i > $i > $i)).
% 7.51/1.73 thf(func_def_72, type, c_lam: ($i > ($i > $i) > $i)).
% 7.51/1.73 thf(func_def_73, type, c_setprod: ($i > $i > $i)).
% 7.51/1.73 thf(func_def_74, type, c_ap: ($i > $i > $i)).
% 7.51/1.73 thf(func_def_75, type, c_setsum_p: ($i > $o)).
% 7.51/1.73 thf(func_def_76, type, c_tuple_p: ($i > $i > $o)).
% 7.51/1.73 thf(func_def_77, type, c_Pi: ($i > ($i > $i) > $i)).
% 7.51/1.73 thf(func_def_78, type, c_setexp: ($i > $i > $i)).
% 7.51/1.73 thf(func_def_79, type, c_Sep2: ($i > ($i > $i) > ($i > $i > $o) > $i)).
% 7.51/1.73 thf(func_def_80, type, c_set_of_pairs: ($i > $o)).
% 7.51/1.73 thf(func_def_81, type, c_lam2: ($i > ($i > $i) > ($i > $i > $i) > $i)).
% 7.51/1.73 thf(func_def_82, type, c_PNoEq_: ($i > ($i > $o) > ($i > $o) > $o)).
% 7.51/1.73 thf(func_def_83, type, c_PNoLt_: ($i > ($i > $o) > ($i > $o) > $o)).
% 7.51/1.73 thf(func_def_84, type, c_PNoLt: ($i > ($i > $o) > $i > ($i > $o) > $o)).
% 7.51/1.73 thf(func_def_85, type, c_PNoLe: ($i > ($i > $o) > $i > ($i > $o) > $o)).
% 7.51/1.73 thf(func_def_86, type, c_PNo_downc: (($i > ($i > $o) > $o) > $i > ($i > $o) > $o)).
% 7.51/1.73 thf(func_def_87, type, c_PNo_upc: (($i > ($i > $o) > $o) > $i > ($i > $o) > $o)).
% 7.51/1.73 thf(func_def_88, type, c_SNoElts_: ($i > $i)).
% 7.51/1.73 thf(func_def_89, type, c_SNo_: ($i > $i > $o)).
% 7.51/1.73 thf(func_def_90, type, c_PSNo: ($i > ($i > $o) > $i)).
% 7.51/1.73 thf(func_def_91, type, c_SNo: ($i > $o)).
% 7.51/1.73 thf(func_def_92, type, c_SNoLev: ($i > $i)).
% 7.51/1.73 thf(func_def_93, type, c_SNoEq_: ($i > $i > $i > $o)).
% 7.51/1.73 thf(func_def_94, type, c_SNoLt: ($i > $i > $o)).
% 7.51/1.73 thf(func_def_95, type, c_SNoLe: ($i > $i > $o)).
% 7.51/1.73 thf(func_def_96, type, c_binop_on: ($i > ($i > $i > $i) > $o)).
% 7.51/1.73 thf(func_def_97, type, c_Loop: ($i > ($i > $i > $i) > ($i > $i > $i) > ($i > $i > $i) > $i > $o)).
% 7.51/1.73 thf(func_def_98, type, c_Loop_with_defs: ($i > ($i > $i > $i) > ($i > $i > $i) > ($i > $i > $i) > $i > ($i > $i > $i) > ($i > $i > $i > $i) > ($i > $i > $i) > ($i > $i > $i > $i) > ($i > $i > $i > $i) > ($i > $i > $i) > ($i > $i > $i) > ($i > $i > $i) > ($i > $i > $i) > $o)).
% 7.51/1.73 thf(func_def_99, type, c_Loop_with_defs_cex1: ($i > ($i > $i > $i) > ($i > $i > $i) > ($i > $i > $i) > $i > ($i > $i > $i) > ($i > $i > $i > $i) > ($i > $i > $i) > ($i > $i > $i > $i) > ($i > $i > $i > $i) > ($i > $i > $i) > ($i > $i > $i) > ($i > $i > $i) > ($i > $i > $i) > $o)).
% 7.51/1.73 thf(func_def_100, type, c_Loop_with_defs_cex2: ($i > ($i > $i > $i) > ($i > $i > $i) > ($i > $i > $i) > $i > ($i > $i > $i) > ($i > $i > $i > $i) > ($i > $i > $i) > ($i > $i > $i > $i) > ($i > $i > $i > $i) > ($i > $i > $i) > ($i > $i > $i) > ($i > $i > $i) > ($i > $i > $i) > $o)).
% 7.51/1.73 thf(func_def_101, type, c_combinator: ($i > $o)).
% 7.51/1.73 thf(func_def_102, type, c_combinator_equiv: ($i > $i > $o)).
% 7.51/1.73 thf(func_def_103, type, c_equip_mod: ($i > $i > $i > $o)).
% 7.51/1.73 thf(func_def_107, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 7.51/1.73 thf(func_def_108, type, db0: !>[X0: $tType]:(X0)).
% 7.51/1.73 thf(func_def_109, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 7.51/1.73 thf(func_def_110, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 7.51/1.73 thf(func_def_111, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 7.51/1.73 thf(func_def_112, type, vIMP: ($o > $o > $o)).
% 7.51/1.73 thf(func_def_113, type, db2: !>[X0: $tType]:(X0)).
% 7.51/1.73 thf(func_def_114, type, db1: !>[X0: $tType]:(X0)).
% 7.51/1.73 thf(func_def_115, type, db3: !>[X0: $tType]:(X0)).
% 7.51/1.73 thf(func_def_116, type, db4: !>[X0: $tType]:(X0)).
% 7.51/1.73 thf(func_def_117, type, db5: !>[X0: $tType]:(X0)).
% 7.51/1.73 thf(func_def_118, type, db6: !>[X0: $tType]:(X0)).
% 7.51/1.73 thf(func_def_119, type, db13: !>[X0: $tType]:(X0)).
% 7.51/1.73 thf(func_def_120, type, db12: !>[X0: $tType]:(X0)).
% 7.51/1.73 thf(func_def_121, type, db11: !>[X0: $tType]:(X0)).
% 7.51/1.73 thf(func_def_122, type, db10: !>[X0: $tType]:(X0)).
% 7.51/1.73 thf(func_def_123, type, db9: !>[X0: $tType]:(X0)).
% 7.51/1.73 thf(func_def_124, type, db14: !>[X0: $tType]:(X0)).
% 7.51/1.73 thf(func_def_125, type, db15: !>[X0: $tType]:(X0)).
% 7.51/1.73 thf(func_def_126, type, db16: !>[X0: $tType]:(X0)).
% 7.51/1.73 thf(func_def_127, type, db8: !>[X0: $tType]:(X0)).
% 7.51/1.73 thf(func_def_128, type, db7: !>[X0: $tType]:(X0)).
% 7.51/1.73 thf(func_def_129, type, db17: !>[X0: $tType]:(X0)).
% 7.51/1.73 thf(func_def_130, type, db18: !>[X0: $tType]:(X0)).
% 7.51/1.73 thf(func_def_131, type, sP0: (($i > $o) > $o)).
% 7.51/1.73 thf(func_def_132, type, sP1: (($i > $o) > $o)).
% 7.51/1.73 thf(func_def_133, type, sK2: (($i > $o) > $i)).
% 7.51/1.73 thf(func_def_134, type, sK3: (($i > $o) > $i > $i)).
% 7.51/1.73 thf(func_def_135, type, sK4: (($i > $o) > $i)).
% 7.51/1.73 thf(func_def_136, type, sK5: (($i > $o) > $i)).
% 7.51/1.73 thf(func_def_137, type, sK6: (($i > $o) > $i)).
% 7.51/1.73 thf(func_def_138, type, sK7: (($i > $o) > $i)).
% 7.51/1.73 thf(func_def_139, type, sK8: (($i > $o) > $i)).
% 7.51/1.73 thf(func_def_140, type, vNOT: ($o > $o)).
% 7.51/1.73 thf(func_def_141, type, sK9: ($i > ($i > $i) > ($i > $o) > ($i > $o) > ($i > $i > $i) > $i > $i > $i > $o)).
% 7.51/1.73 thf(func_def_142, type, sK10: ($i > ($i > $i) > ($i > $o) > ($i > $o) > $i > $i > $i > $i)).
% 7.51/1.73 thf(func_def_143, type, sK11: $o).
% 7.51/1.73 thf(func_def_144, type, sK12: $o).
% 7.51/1.73 thf(func_def_145, type, sK13: (($i > $i) > $i > $i > $i)).
% 7.51/1.73 thf(func_def_146, type, sK14: (($i > $i) > $i > $i > $i > $o)).
% 7.51/1.73 thf(func_def_147, type, sK15: ($i > $i > $i)).
% 7.51/1.73 thf(func_def_148, type, sK16: ($i > $i > $i)).
% 7.51/1.73 thf(func_def_149, type, sK17: ($i > $i > $i > $o)).
% 7.51/1.73 thf(func_def_150, type, sK18: ($i > $i > $i)).
% 7.51/1.73 thf(func_def_151, type, sK19: ($i > $i > $i)).
% 7.51/1.73 thf(func_def_152, type, sK20: ($o > $o > $o)).
% 7.51/1.73 thf(func_def_153, type, sK21: ($o > $o > $o)).
% 7.51/1.73 thf(f1,axiom,(
% 7.51/1.73 ! [X0 : ($i > $o),X1 : $i] : ((X0 @ X1) => (X0 @ (c_Eps_i @ X0)))),
% 7.51/1.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1)).
% 7.51/1.73 thf(f5,axiom,(
% 7.51/1.73 (c_not @ ? [X0 : $i] : (c_In @ X0 @ c_Empty))),
% 7.51/1.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5)).
% 7.51/1.73 thf(f7,axiom,(
% 7.51/1.73 ! [X0 : $i,X1 : $i] : (c_iff @ (c_In @ X1 @ (c_Power @ X0)) @ (c_Subq @ X1 @ X0))),
% 7.51/1.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax7)).
% 7.51/1.73 thf(f8,axiom,(
% 7.51/1.73 ! [X0 : $i,X1 : ($i > $i),X2 : $i] : (c_iff @ (c_In @ X2 @ (c_Repl @ X0 @ (^[X3 : $i] : ((X1 @ X3))))) @ ? [X3 : $i] : (c_and @ (c_In @ X3 @ X0) @ (X2 = ((X1 @ X3)))))),
% 7.51/1.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax8)).
% 7.51/1.73 thf(f13,axiom,(
% 7.51/1.73 (c_not = (^[X0 : $o] : (X0 => c_False)))),
% 7.51/1.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax13)).
% 7.51/1.73 thf(f14,axiom,(
% 7.51/1.73 (c_and = (^[X0 : $o, X1 : $o] : (! [X2 : $o] : ((X0 => (X1 => X2)) => X2))))),
% 7.51/1.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax14)).
% 7.51/1.73 thf(f16,axiom,(
% 7.51/1.73 (c_iff = (^[X0 : $o, X1 : $o] : ((c_and @ X0 => X1 @ X1 => X0))))),
% 7.51/1.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax16)).
% 7.51/1.73 thf(f17,axiom,(
% 7.51/1.73 (c_Subq = (^[X0 : $i, X1 : $i] : (! [X2 : $i] : ((c_In @ X2 @ X0) => (c_In @ X2 @ X1)))))),
% 7.51/1.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax17)).
% 7.51/1.73 thf(f109,conjecture,(
% 7.51/1.73 (c_not @ ! [X0 : ($i > $i > $o),X1 : ($i > $i > $i),X2 : ($i > $o),X3 : ($i > $o),X4 : ($i > $i),X5 : $i,X6 : $i,X7 : $i,X8 : $i,X9 : $i] : ((c_and @ ! [X10 : $i] : ((((X4 @ X9)) = X10) => ((c_and @ (X2 @ X10) @ (X7 = X5) => (c_and @ ! [X11 : $i] : (X9 = X8) @ ? [X11 : $i] : (X3 @ X10))) => ? [X11 : $i] : (X7 = X7))) @ (c_not @ (X3 @ (X4 @ (X4 @ (X1 @ X7 @ X5)))))) => (X6 = X9)))),
% 7.51/1.73 file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj)).
% 7.51/1.73 thf(f110,negated_conjecture,(
% 7.51/1.73 ~(c_not @ ! [X0 : ($i > $i > $o),X1 : ($i > $i > $i),X2 : ($i > $o),X3 : ($i > $o),X4 : ($i > $i),X5 : $i,X6 : $i,X7 : $i,X8 : $i,X9 : $i] : ((c_and @ ! [X10 : $i] : ((((X4 @ X9)) = X10) => ((c_and @ (X2 @ X10) @ (X7 = X5) => (c_and @ ! [X11 : $i] : (X9 = X8) @ ? [X11 : $i] : (X3 @ X10))) => ? [X11 : $i] : (X7 = X7))) @ (c_not @ (X3 @ (X4 @ (X4 @ (X1 @ X7 @ X5)))))) => (X6 = X9)))),
% 7.51/1.73 inference(negated_conjecture,[status(cth)],[f109])).
% 7.51/1.73 thf(f111,plain,(
% 7.51/1.73 ! [X0 : ($i > $o),X1 : $i] : ((X0 @ X1) => (X0 @ (c_Eps_i @ X0)))),
% 7.51/1.73 inference(rectify,[],[f1])).
% 7.51/1.73 thf(f112,plain,(
% 7.51/1.73 ! [X0 : ($i > $o),X1 : $i] : ((((X0 @ X1)) = $true) => (((X0 @ (c_Eps_i @ X0))) = $true))),
% 7.51/1.73 inference(fool_elimination,[],[f111])).
% 7.51/1.73 thf(f119,plain,(
% 7.51/1.73 (c_not @ ? [X0 : $i] : (c_In @ X0 @ c_Empty))),
% 7.51/1.73 inference(rectify,[],[f5])).
% 7.51/1.73 thf(f120,plain,(
% 7.51/1.73 ($true = ((c_not @ (?? @ $i @ (^[Y0 : $i]: (c_In @ Y0 @ c_Empty))))))),
% 7.51/1.73 inference(fool_elimination,[],[f119])).
% 7.51/1.73 thf(f123,plain,(
% 7.51/1.73 ! [X0 : $i,X1 : $i] : (c_iff @ (c_In @ X1 @ (c_Power @ X0)) @ (c_Subq @ X1 @ X0))),
% 7.51/1.73 inference(rectify,[],[f7])).
% 7.51/1.73 thf(f124,plain,(
% 7.51/1.73 ! [X0 : $i,X1 : $i] : (((c_iff @ (c_In @ X1 @ (c_Power @ X0)) @ (c_Subq @ X1 @ X0))) = $true)),
% 7.51/1.73 inference(fool_elimination,[],[f123])).
% 7.51/1.73 thf(f125,plain,(
% 7.51/1.73 ! [X0 : $i,X1 : ($i > $i),X2 : $i] : (c_iff @ (c_In @ X2 @ (c_Repl @ X0 @ (^[X3 : $i] : ((X1 @ X3))))) @ ? [X4 : $i] : (c_and @ (c_In @ X4 @ X0) @ (((X1 @ X4)) = X2)))),
% 7.51/1.73 inference(rectify,[],[f8])).
% 7.51/1.73 thf(f126,plain,(
% 7.51/1.73 ! [X0 : $i,X1 : ($i > $i),X2 : $i] : ($true = ((c_iff @ (c_In @ X2 @ (c_Repl @ X0 @ (^[Y0 : $i]: (X1 @ Y0)))) @ (?? @ $i @ (^[Y0 : $i]: (c_and @ (c_In @ Y0 @ X0) @ ((X1 @ Y0) = X2)))))))),
% 7.51/1.73 inference(fool_elimination,[],[f125])).
% 7.51/1.73 thf(f135,plain,(
% 7.51/1.73 (c_not = (^[X0 : $o] : (X0 => c_False)))),
% 7.51/1.73 inference(rectify,[],[f13])).
% 7.51/1.73 thf(f136,plain,(
% 7.51/1.73 (c_not = (^[Y0 : $o]: (Y0 => c_False)))),
% 7.51/1.73 inference(fool_elimination,[],[f135])).
% 7.51/1.73 thf(f137,plain,(
% 7.51/1.73 (c_and = (^[X0 : $o, X1 : $o] : (! [X2 : $o] : ((X0 => (X1 => X2)) => X2))))),
% 7.51/1.73 inference(rectify,[],[f14])).
% 7.51/1.73 thf(f138,plain,(
% 7.51/1.73 (c_and = (^[Y0 : $o]: ((^[Y1 : $o]: (!! @ $o @ (^[Y2 : $o]: ((Y0 => (Y1 => Y2)) => Y2)))))))),
% 7.51/1.73 inference(fool_elimination,[],[f137])).
% 7.51/1.73 thf(f141,plain,(
% 7.51/1.73 (c_iff = (^[X0 : $o, X1 : $o] : ((c_and @ X0 => X1 @ X1 => X0))))),
% 7.51/1.73 inference(rectify,[],[f16])).
% 7.51/1.73 thf(f142,plain,(
% 7.51/1.73 (c_iff = (^[Y0 : $o]: ((^[Y1 : $o]: (c_and @ (Y0 => Y1) @ (Y1 => Y0))))))),
% 7.51/1.73 inference(fool_elimination,[],[f141])).
% 7.51/1.73 thf(f143,plain,(
% 7.51/1.73 (c_Subq = (^[X0 : $i, X1 : $i] : (! [X2 : $i] : ((c_In @ X2 @ X0) => (c_In @ X2 @ X1)))))),
% 7.51/1.73 inference(rectify,[],[f17])).
% 7.51/1.73 thf(f144,plain,(
% 7.51/1.73 (c_Subq = (^[Y0 : $i]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((c_In @ Y2 @ Y0) => (c_In @ Y2 @ Y1))))))))),
% 7.51/1.73 inference(fool_elimination,[],[f143])).
% 7.51/1.73 thf(f306,plain,(
% 7.51/1.73 ~(c_not @ ! [X1 : ($i > $i > $i),X2 : ($i > $o),X3 : ($i > $o),X4 : ($i > $i),X5 : $i,X6 : $i,X7 : $i,X8 : $i,X9 : $i] : ((c_and @ ! [X10 : $i] : ((((X4 @ X9)) = X10) => ((c_and @ (X2 @ X10) @ (X7 = X5) => (c_and @ (X9 = X8) @ (X3 @ X10))) => (X7 = X7))) @ (c_not @ (X3 @ (X4 @ (X4 @ (X1 @ X7 @ X5)))))) => (X6 = X9)))),
% 7.51/1.73 inference(rectify,[],[f110])).
% 7.51/1.73 thf(f307,plain,(
% 7.51/1.73 ~ ($true = ((c_not @ (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ ($i > $i) @ (^[Y5 : $i > $i]: (!! @ ($i > $o) @ (^[Y6 : $i > $o]: (!! @ ($i > $o) @ (^[Y7 : $i > $o]: (!! @ ($i > $i > $i) @ (^[Y8 : $i > $i > $i]: ((c_and @ (!! @ $i @ (^[Y9 : $i]: (((Y5 @ Y0) = Y9) => ((c_and @ (Y7 @ Y9) @ ((Y4 = Y2) => (c_and @ (Y1 = Y0) @ (Y6 @ Y9)))) => (Y2 = Y2))))) @ (c_not @ (Y6 @ (Y5 @ (Y5 @ (Y8 @ Y2 @ Y4)))))) => (Y3 = Y0)))))))))))))))))))))))),
% 7.51/1.73 inference(fool_elimination,[],[f306])).
% 7.51/1.73 thf(f309,plain,(
% 7.51/1.73 ($true != ((c_not @ (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ ($i > $i) @ (^[Y5 : $i > $i]: (!! @ ($i > $o) @ (^[Y6 : $i > $o]: (!! @ ($i > $o) @ (^[Y7 : $i > $o]: (!! @ ($i > $i > $i) @ (^[Y8 : $i > $i > $i]: ((c_and @ (!! @ $i @ (^[Y9 : $i]: (((Y5 @ Y0) = Y9) => ((c_and @ (Y7 @ Y9) @ ((Y4 = Y2) => (c_and @ (Y1 = Y0) @ (Y6 @ Y9)))) => (Y2 = Y2))))) @ (c_not @ (Y6 @ (Y5 @ (Y5 @ (Y8 @ Y2 @ Y4)))))) => (Y3 = Y0)))))))))))))))))))))))),
% 7.51/1.73 inference(flattening,[],[f307])).
% 7.51/1.73 thf(f310,plain,(
% 7.51/1.73 ! [X0 : ($i > $o),X1 : $i] : ((((X0 @ (c_Eps_i @ X0))) = $true) | (((X0 @ X1)) != $true))),
% 7.51/1.73 inference(ennf_transformation,[],[f112])).
% 7.51/1.73 thf(f330,plain,(
% 7.51/1.73 ( ! [X0 : ($i > $o),X1 : $i] : ((((X0 @ X1)) != $true) | (((X0 @ (c_Eps_i @ X0))) = $true)) )),
% 7.51/1.73 inference(cnf_transformation,[],[f310])).
% 7.51/1.73 thf(f334,plain,(
% 7.51/1.73 ($true = ((c_not @ (?? @ $i @ (^[Y0 : $i]: (c_In @ Y0 @ c_Empty))))))),
% 7.51/1.73 inference(cnf_transformation,[],[f120])).
% 7.51/1.73 thf(f336,plain,(
% 7.51/1.73 ( ! [X0 : $i,X1 : $i] : ((((c_iff @ (c_In @ X1 @ (c_Power @ X0)) @ (c_Subq @ X1 @ X0))) = $true)) )),
% 7.51/1.73 inference(cnf_transformation,[],[f124])).
% 7.51/1.73 thf(f337,plain,(
% 7.51/1.73 ( ! [X2 : $i,X0 : $i,X1 : ($i > $i)] : (($true = ((c_iff @ (c_In @ X2 @ (c_Repl @ X0 @ (^[Y0 : $i]: (X1 @ Y0)))) @ (?? @ $i @ (^[Y0 : $i]: (c_and @ (c_In @ Y0 @ X0) @ ((X1 @ Y0) = X2)))))))) )),
% 7.51/1.73 inference(cnf_transformation,[],[f126])).
% 7.51/1.73 thf(f352,plain,(
% 7.51/1.73 (c_not = (^[Y0 : $o]: (Y0 => c_False)))),
% 7.51/1.73 inference(cnf_transformation,[],[f136])).
% 7.51/1.73 thf(f353,plain,(
% 7.51/1.73 (c_and = (^[Y0 : $o]: ((^[Y1 : $o]: (!! @ $o @ (^[Y2 : $o]: ((Y0 => (Y1 => Y2)) => Y2)))))))),
% 7.51/1.73 inference(cnf_transformation,[],[f138])).
% 7.51/1.73 thf(f355,plain,(
% 7.51/1.73 (c_iff = (^[Y0 : $o]: ((^[Y1 : $o]: (c_and @ (Y0 => Y1) @ (Y1 => Y0))))))),
% 7.51/1.73 inference(cnf_transformation,[],[f142])).
% 7.51/1.73 thf(f356,plain,(
% 7.51/1.73 (c_Subq = (^[Y0 : $i]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((c_In @ Y2 @ Y0) => (c_In @ Y2 @ Y1))))))))),
% 7.51/1.73 inference(cnf_transformation,[],[f144])).
% 7.51/1.73 thf(f448,plain,(
% 7.51/1.73 ($true != ((c_not @ (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ ($i > $i) @ (^[Y5 : $i > $i]: (!! @ ($i > $o) @ (^[Y6 : $i > $o]: (!! @ ($i > $o) @ (^[Y7 : $i > $o]: (!! @ ($i > $i > $i) @ (^[Y8 : $i > $i > $i]: ((c_and @ (!! @ $i @ (^[Y9 : $i]: (((Y5 @ Y0) = Y9) => ((c_and @ (Y7 @ Y9) @ ((Y4 = Y2) => (c_and @ (Y1 = Y0) @ (Y6 @ Y9)))) => (Y2 = Y2))))) @ (c_not @ (Y6 @ (Y5 @ (Y5 @ (Y8 @ Y2 @ Y4)))))) => (Y3 = Y0)))))))))))))))))))))))),
% 7.51/1.73 inference(cnf_transformation,[],[f309])).
% 7.51/1.73 thf(f451,plain,(
% 7.51/1.73 (c_iff = (^[Y0 : $o]: ((^[Y1 : $o]: ((^[Y2 : $o]: ((^[Y3 : $o]: (!! @ $o @ (^[Y4 : $o]: ((Y2 => (Y3 => Y4)) => Y4)))))) @ (Y0 => Y1) @ (Y1 => Y0))))))),
% 7.51/1.73 inference(definition_unfolding,[],[f355,f353])).
% 7.51/1.73 thf(f539,plain,(
% 7.51/1.73 ($true = (((^[Y0 : $o]: (Y0 => c_False)) @ (?? @ $i @ (^[Y0 : $i]: (c_In @ Y0 @ c_Empty))))))),
% 7.51/1.73 inference(definition_unfolding,[],[f334,f352])).
% 7.51/1.73 thf(f541,plain,(
% 7.51/1.73 ( ! [X0 : $i,X1 : $i] : (($true = (((^[Y0 : $o]: ((^[Y1 : $o]: ((^[Y2 : $o]: ((^[Y3 : $o]: (!! @ $o @ (^[Y4 : $o]: ((Y2 => (Y3 => Y4)) => Y4)))))) @ (Y0 => Y1) @ (Y1 => Y0))))) @ (c_In @ X1 @ (c_Power @ X0)) @ ((^[Y0 : $i]: ((^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: ((c_In @ Y2 @ Y0) => (c_In @ Y2 @ Y1))))))) @ X1 @ X0))))) )),
% 7.51/1.73 inference(definition_unfolding,[],[f336,f451,f356])).
% 7.51/1.73 thf(f542,plain,(
% 7.51/1.73 ( ! [X2 : $i,X0 : $i,X1 : ($i > $i)] : (($true = (((^[Y0 : $o]: ((^[Y1 : $o]: ((^[Y2 : $o]: ((^[Y3 : $o]: (!! @ $o @ (^[Y4 : $o]: ((Y2 => (Y3 => Y4)) => Y4)))))) @ (Y0 => Y1) @ (Y1 => Y0))))) @ (c_In @ X2 @ (c_Repl @ X0 @ (^[Y0 : $i]: (X1 @ Y0)))) @ (?? @ $i @ (^[Y0 : $i]: ((^[Y1 : $o]: ((^[Y2 : $o]: (!! @ $o @ (^[Y3 : $o]: ((Y1 => (Y2 => Y3)) => Y3)))))) @ (c_In @ Y0 @ X0) @ ((X1 @ Y0) = X2)))))))) )),
% 7.51/1.73 inference(definition_unfolding,[],[f337,f451,f353])).
% 7.51/1.73 thf(f543,plain,(
% 7.51/1.73 ($true != (((^[Y0 : $o]: (Y0 => c_False)) @ (!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ ($i > $i) @ (^[Y5 : $i > $i]: (!! @ ($i > $o) @ (^[Y6 : $i > $o]: (!! @ ($i > $o) @ (^[Y7 : $i > $o]: (!! @ ($i > $i > $i) @ (^[Y8 : $i > $i > $i]: (((^[Y9 : $o]: ((^[Y10 : $o]: (!! @ $o @ (^[Y11 : $o]: ((Y9 => (Y10 => Y11)) => Y11)))))) @ (!! @ $i @ (^[Y9 : $i]: (((Y5 @ Y0) = Y9) => (((^[Y10 : $o]: ((^[Y11 : $o]: (!! @ $o @ (^[Y12 : $o]: ((Y10 => (Y11 => Y12)) => Y12)))))) @ (Y7 @ Y9) @ ((Y4 = Y2) => ((^[Y10 : $o]: ((^[Y11 : $o]: (!! @ $o @ (^[Y12 : $o]: ((Y10 => (Y11 => Y12)) => Y12)))))) @ (Y1 = Y0) @ (Y6 @ Y9)))) => (Y2 = Y2))))) @ ((^[Y9 : $o]: (Y9 => c_False)) @ (Y6 @ (Y5 @ (Y5 @ (Y8 @ Y2 @ Y4)))))) => (Y3 = Y0)))))))))))))))))))))))),
% 7.51/1.73 inference(definition_unfolding,[],[f448,f352,f353,f353,f353,f352])).
% 7.51/1.73 thf(f544,plain,(
% 7.51/1.73 ($true != (((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ ($i > $i) @ (^[Y5 : $i > $i]: (!! @ ($i > $o) @ (^[Y6 : $i > $o]: (!! @ ($i > $o) @ (^[Y7 : $i > $o]: (!! @ ($i > $i > $i) @ (^[Y8 : $i > $i > $i]: ((!! @ $o @ (^[Y9 : $o]: (((!! @ $i @ (^[Y10 : $i]: (((Y5 @ Y0) = Y10) => ((!! @ $o @ (^[Y11 : $o]: (((Y7 @ Y10) => (((Y4 = Y2) => (!! @ $o @ (^[Y12 : $o]: (((Y1 = Y0) => ((Y6 @ Y10) => Y12)) => Y12)))) => Y11)) => Y11))) => (Y2 = Y2))))) => (((Y6 @ (Y5 @ (Y5 @ (Y8 @ Y2 @ Y4)))) => c_False) => Y9)) => Y9))) => (Y3 = Y0)))))))))))))))))))) => c_False)))),
% 7.51/1.73 inference(beta-eta_normalization,[],[f543])).
% 7.51/1.73 thf(f545,plain,(
% 7.51/1.73 (c_False = $false)),
% 7.51/1.73 inference(imp_proxy_clausification,[],[f544])).
% 7.51/1.73 thf(f546,plain,(
% 7.51/1.73 ($true = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ ($i > $i) @ (^[Y5 : $i > $i]: (!! @ ($i > $o) @ (^[Y6 : $i > $o]: (!! @ ($i > $o) @ (^[Y7 : $i > $o]: (!! @ ($i > $i > $i) @ (^[Y8 : $i > $i > $i]: ((!! @ $o @ (^[Y9 : $o]: (((!! @ $i @ (^[Y10 : $i]: (((Y5 @ Y0) = Y10) => ((!! @ $o @ (^[Y11 : $o]: (((Y7 @ Y10) => (((Y4 = Y2) => (!! @ $o @ (^[Y12 : $o]: (((Y1 = Y0) => ((Y6 @ Y10) => Y12)) => Y12)))) => Y11)) => Y11))) => (Y2 = Y2))))) => (((Y6 @ (Y5 @ (Y5 @ (Y8 @ Y2 @ Y4)))) => c_False) => Y9)) => Y9))) => (Y3 = Y0))))))))))))))))))))))),
% 7.51/1.73 inference(imp_proxy_clausification,[],[f544])).
% 7.51/1.73 thf(f547,plain,(
% 7.51/1.73 ( ! [X1 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (!! @ $i @ (^[Y4 : $i]: (!! @ ($i > $i) @ (^[Y5 : $i > $i]: (!! @ ($i > $o) @ (^[Y6 : $i > $o]: (!! @ ($i > $o) @ (^[Y7 : $i > $o]: (!! @ ($i > $i > $i) @ (^[Y8 : $i > $i > $i]: ((!! @ $o @ (^[Y9 : $o]: (((!! @ $i @ (^[Y10 : $i]: (((Y5 @ Y0) = Y10) => ((!! @ $o @ (^[Y11 : $o]: (((Y7 @ Y10) => (((Y4 = Y2) => (!! @ $o @ (^[Y12 : $o]: (((Y1 = Y0) => ((Y6 @ Y10) => Y12)) => Y12)))) => Y11)) => Y11))) => (Y2 = Y2))))) => (((Y6 @ (Y5 @ (Y5 @ (Y8 @ Y2 @ Y4)))) => c_False) => Y9)) => Y9))) => (Y3 = Y0))))))))))))))))))) @ X1)))) )),
% 7.51/1.73 inference(pi_proxy_clausification,[],[f546])).
% 7.51/1.73 thf(f548,plain,(
% 7.51/1.73 ( ! [X1 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (!! @ ($i > $i) @ (^[Y4 : $i > $i]: (!! @ ($i > $o) @ (^[Y5 : $i > $o]: (!! @ ($i > $o) @ (^[Y6 : $i > $o]: (!! @ ($i > $i > $i) @ (^[Y7 : $i > $i > $i]: ((!! @ $o @ (^[Y8 : $o]: (((!! @ $i @ (^[Y9 : $i]: (((Y4 @ X1) = Y9) => ((!! @ $o @ (^[Y10 : $o]: (((Y6 @ Y9) => (((Y3 = Y1) => (!! @ $o @ (^[Y11 : $o]: (((Y0 = X1) => ((Y5 @ Y9) => Y11)) => Y11)))) => Y10)) => Y10))) => (Y1 = Y1))))) => (((Y5 @ (Y4 @ (Y4 @ (Y7 @ Y1 @ Y3)))) => c_False) => Y8)) => Y8))) => (Y2 = X1))))))))))))))))))))) )),
% 7.51/1.73 inference(beta-eta_normalization,[],[f547])).
% 7.51/1.73 thf(f549,plain,(
% 7.51/1.73 ( ! [X2 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ $i @ (^[Y3 : $i]: (!! @ ($i > $i) @ (^[Y4 : $i > $i]: (!! @ ($i > $o) @ (^[Y5 : $i > $o]: (!! @ ($i > $o) @ (^[Y6 : $i > $o]: (!! @ ($i > $i > $i) @ (^[Y7 : $i > $i > $i]: ((!! @ $o @ (^[Y8 : $o]: (((!! @ $i @ (^[Y9 : $i]: (((Y4 @ X1) = Y9) => ((!! @ $o @ (^[Y10 : $o]: (((Y6 @ Y9) => (((Y3 = Y1) => (!! @ $o @ (^[Y11 : $o]: (((Y0 = X1) => ((Y5 @ Y9) => Y11)) => Y11)))) => Y10)) => Y10))) => (Y1 = Y1))))) => (((Y5 @ (Y4 @ (Y4 @ (Y7 @ Y1 @ Y3)))) => c_False) => Y8)) => Y8))) => (Y2 = X1))))))))))))))))) @ X2)))) )),
% 7.51/1.73 inference(pi_proxy_clausification,[],[f548])).
% 7.51/1.73 thf(f550,plain,(
% 7.51/1.73 ( ! [X2 : $i,X1 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ ($i > $i) @ (^[Y3 : $i > $i]: (!! @ ($i > $o) @ (^[Y4 : $i > $o]: (!! @ ($i > $o) @ (^[Y5 : $i > $o]: (!! @ ($i > $i > $i) @ (^[Y6 : $i > $i > $i]: ((!! @ $o @ (^[Y7 : $o]: (((!! @ $i @ (^[Y8 : $i]: (((Y3 @ X1) = Y8) => ((!! @ $o @ (^[Y9 : $o]: (((Y5 @ Y8) => (((Y2 = Y0) => (!! @ $o @ (^[Y10 : $o]: (((X2 = X1) => ((Y4 @ Y8) => Y10)) => Y10)))) => Y9)) => Y9))) => (Y0 = Y0))))) => (((Y4 @ (Y3 @ (Y3 @ (Y6 @ Y0 @ Y2)))) => c_False) => Y7)) => Y7))) => (Y1 = X1))))))))))))))))))) )),
% 7.51/1.73 inference(beta-eta_normalization,[],[f549])).
% 7.51/1.73 thf(f551,plain,(
% 7.51/1.73 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ $i @ (^[Y2 : $i]: (!! @ ($i > $i) @ (^[Y3 : $i > $i]: (!! @ ($i > $o) @ (^[Y4 : $i > $o]: (!! @ ($i > $o) @ (^[Y5 : $i > $o]: (!! @ ($i > $i > $i) @ (^[Y6 : $i > $i > $i]: ((!! @ $o @ (^[Y7 : $o]: (((!! @ $i @ (^[Y8 : $i]: (((Y3 @ X1) = Y8) => ((!! @ $o @ (^[Y9 : $o]: (((Y5 @ Y8) => (((Y2 = Y0) => (!! @ $o @ (^[Y10 : $o]: (((X2 = X1) => ((Y4 @ Y8) => Y10)) => Y10)))) => Y9)) => Y9))) => (Y0 = Y0))))) => (((Y4 @ (Y3 @ (Y3 @ (Y6 @ Y0 @ Y2)))) => c_False) => Y7)) => Y7))) => (Y1 = X1))))))))))))))) @ X3)))) )),
% 7.51/1.73 inference(pi_proxy_clausification,[],[f550])).
% 7.51/1.73 thf(f552,plain,(
% 7.51/1.73 ( ! [X2 : $i,X3 : $i,X1 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ ($i > $i) @ (^[Y2 : $i > $i]: (!! @ ($i > $o) @ (^[Y3 : $i > $o]: (!! @ ($i > $o) @ (^[Y4 : $i > $o]: (!! @ ($i > $i > $i) @ (^[Y5 : $i > $i > $i]: ((!! @ $o @ (^[Y6 : $o]: (((!! @ $i @ (^[Y7 : $i]: (((Y2 @ X1) = Y7) => ((!! @ $o @ (^[Y8 : $o]: (((Y4 @ Y7) => (((Y1 = X3) => (!! @ $o @ (^[Y9 : $o]: (((X2 = X1) => ((Y3 @ Y7) => Y9)) => Y9)))) => Y8)) => Y8))) => (X3 = X3))))) => (((Y3 @ (Y2 @ (Y2 @ (Y5 @ X3 @ Y1)))) => c_False) => Y6)) => Y6))) => (Y0 = X1))))))))))))))))) )),
% 7.51/1.73 inference(beta-eta_normalization,[],[f551])).
% 7.51/1.73 thf(f553,plain,(
% 7.51/1.73 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = (((^[Y0 : $i]: (!! @ $i @ (^[Y1 : $i]: (!! @ ($i > $i) @ (^[Y2 : $i > $i]: (!! @ ($i > $o) @ (^[Y3 : $i > $o]: (!! @ ($i > $o) @ (^[Y4 : $i > $o]: (!! @ ($i > $i > $i) @ (^[Y5 : $i > $i > $i]: ((!! @ $o @ (^[Y6 : $o]: (((!! @ $i @ (^[Y7 : $i]: (((Y2 @ X1) = Y7) => ((!! @ $o @ (^[Y8 : $o]: (((Y4 @ Y7) => (((Y1 = X3) => (!! @ $o @ (^[Y9 : $o]: (((X2 = X1) => ((Y3 @ Y7) => Y9)) => Y9)))) => Y8)) => Y8))) => (X3 = X3))))) => (((Y3 @ (Y2 @ (Y2 @ (Y5 @ X3 @ Y1)))) => c_False) => Y6)) => Y6))) => (Y0 = X1))))))))))))) @ X4)))) )),
% 7.51/1.73 inference(pi_proxy_clausification,[],[f552])).
% 7.51/1.73 thf(f554,plain,(
% 7.51/1.73 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i] : (($true = ((!! @ $i @ (^[Y0 : $i]: (!! @ ($i > $i) @ (^[Y1 : $i > $i]: (!! @ ($i > $o) @ (^[Y2 : $i > $o]: (!! @ ($i > $o) @ (^[Y3 : $i > $o]: (!! @ ($i > $i > $i) @ (^[Y4 : $i > $i > $i]: ((!! @ $o @ (^[Y5 : $o]: (((!! @ $i @ (^[Y6 : $i]: (((Y1 @ X1) = Y6) => ((!! @ $o @ (^[Y7 : $o]: (((Y3 @ Y6) => (((Y0 = X3) => (!! @ $o @ (^[Y8 : $o]: (((X2 = X1) => ((Y2 @ Y6) => Y8)) => Y8)))) => Y7)) => Y7))) => (X3 = X3))))) => (((Y2 @ (Y1 @ (Y1 @ (Y4 @ X3 @ Y0)))) => c_False) => Y5)) => Y5))) => (X4 = X1))))))))))))))) )),
% 7.51/1.73 inference(beta-eta_normalization,[],[f553])).
% 7.51/1.73 thf(f555,plain,(
% 7.51/1.73 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i,X5 : $i] : (($true = (((^[Y0 : $i]: (!! @ ($i > $i) @ (^[Y1 : $i > $i]: (!! @ ($i > $o) @ (^[Y2 : $i > $o]: (!! @ ($i > $o) @ (^[Y3 : $i > $o]: (!! @ ($i > $i > $i) @ (^[Y4 : $i > $i > $i]: ((!! @ $o @ (^[Y5 : $o]: (((!! @ $i @ (^[Y6 : $i]: (((Y1 @ X1) = Y6) => ((!! @ $o @ (^[Y7 : $o]: (((Y3 @ Y6) => (((Y0 = X3) => (!! @ $o @ (^[Y8 : $o]: (((X2 = X1) => ((Y2 @ Y6) => Y8)) => Y8)))) => Y7)) => Y7))) => (X3 = X3))))) => (((Y2 @ (Y1 @ (Y1 @ (Y4 @ X3 @ Y0)))) => c_False) => Y5)) => Y5))) => (X4 = X1))))))))))) @ X5)))) )),
% 7.51/1.73 inference(pi_proxy_clausification,[],[f554])).
% 7.51/1.73 thf(f556,plain,(
% 7.51/1.73 ( ! [X2 : $i,X3 : $i,X1 : $i,X4 : $i,X5 : $i] : (($true = ((!! @ ($i > $i) @ (^[Y0 : $i > $i]: (!! @ ($i > $o) @ (^[Y1 : $i > $o]: (!! @ ($i > $o) @ (^[Y2 : $i > $o]: (!! @ ($i > $i > $i) @ (^[Y3 : $i > $i > $i]: ((!! @ $o @ (^[Y4 : $o]: (((!! @ $i @ (^[Y5 : $i]: (((Y0 @ X1) = Y5) => ((!! @ $o @ (^[Y6 : $o]: (((Y2 @ Y5) => (((X5 = X3) => (!! @ $o @ (^[Y7 : $o]: (((X2 = X1) => ((Y1 @ Y5) => Y7)) => Y7)))) => Y6)) => Y6))) => (X3 = X3))))) => (((Y1 @ (Y0 @ (Y0 @ (Y3 @ X3 @ X5)))) => c_False) => Y4)) => Y4))) => (X4 = X1))))))))))))) )),
% 7.51/1.73 inference(beta-eta_normalization,[],[f555])).
% 7.51/1.73 thf(f557,plain,(
% 7.51/1.73 ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : ($i > $i),X4 : $i,X5 : $i] : (($true = (((^[Y0 : $i > $i]: (!! @ ($i > $o) @ (^[Y1 : $i > $o]: (!! @ ($i > $o) @ (^[Y2 : $i > $o]: (!! @ ($i > $i > $i) @ (^[Y3 : $i > $i > $i]: ((!! @ $o @ (^[Y4 : $o]: (((!! @ $i @ (^[Y5 : $i]: (((Y0 @ X1) = Y5) => ((!! @ $o @ (^[Y6 : $o]: (((Y2 @ Y5) => (((X5 = X3) => (!! @ $o @ (^[Y7 : $o]: (((X2 = X1) => ((Y1 @ Y5) => Y7)) => Y7)))) => Y6)) => Y6))) => (X3 = X3))))) => (((Y1 @ (Y0 @ (Y0 @ (Y3 @ X3 @ X5)))) => c_False) => Y4)) => Y4))) => (X4 = X1))))))))) @ X6)))) )),
% 7.51/1.73 inference(pi_proxy_clausification,[],[f556])).
% 7.51/1.73 thf(f558,plain,(
% 7.51/1.73 ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : ($i > $i),X4 : $i,X5 : $i] : (($true = ((!! @ ($i > $o) @ (^[Y0 : $i > $o]: (!! @ ($i > $o) @ (^[Y1 : $i > $o]: (!! @ ($i > $i > $i) @ (^[Y2 : $i > $i > $i]: ((!! @ $o @ (^[Y3 : $o]: (((!! @ $i @ (^[Y4 : $i]: (((X6 @ X1) = Y4) => ((!! @ $o @ (^[Y5 : $o]: (((Y1 @ Y4) => (((X5 = X3) => (!! @ $o @ (^[Y6 : $o]: (((X2 = X1) => ((Y0 @ Y4) => Y6)) => Y6)))) => Y5)) => Y5))) => (X3 = X3))))) => (((Y0 @ (X6 @ (X6 @ (Y2 @ X3 @ X5)))) => c_False) => Y3)) => Y3))) => (X4 = X1))))))))))) )),
% 7.51/1.73 inference(beta-eta_normalization,[],[f557])).
% 7.51/1.73 thf(f559,plain,(
% 7.51/1.73 ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : ($i > $i),X7 : ($i > $o),X4 : $i,X5 : $i] : (($true = (((^[Y0 : $i > $o]: (!! @ ($i > $o) @ (^[Y1 : $i > $o]: (!! @ ($i > $i > $i) @ (^[Y2 : $i > $i > $i]: ((!! @ $o @ (^[Y3 : $o]: (((!! @ $i @ (^[Y4 : $i]: (((X6 @ X1) = Y4) => ((!! @ $o @ (^[Y5 : $o]: (((Y1 @ Y4) => (((X5 = X3) => (!! @ $o @ (^[Y6 : $o]: (((X2 = X1) => ((Y0 @ Y4) => Y6)) => Y6)))) => Y5)) => Y5))) => (X3 = X3))))) => (((Y0 @ (X6 @ (X6 @ (Y2 @ X3 @ X5)))) => c_False) => Y3)) => Y3))) => (X4 = X1))))))) @ X7)))) )),
% 7.51/1.73 inference(pi_proxy_clausification,[],[f558])).
% 7.51/1.73 thf(f560,plain,(
% 7.51/1.73 ( ! [X2 : $i,X3 : $i,X1 : $i,X6 : ($i > $i),X7 : ($i > $o),X4 : $i,X5 : $i] : (($true = ((!! @ ($i > $o) @ (^[Y0 : $i > $o]: (!! @ ($i > $i > $i) @ (^[Y1 : $i > $i > $i]: ((!! @ $o @ (^[Y2 : $o]: (((!! @ $i @ (^[Y3 : $i]: (((X6 @ X1) = Y3) => ((!! @ $o @ (^[Y4 : $o]: (((Y0 @ Y3) => (((X5 = X3) => (!! @ $o @ (^[Y5 : $o]: (((X2 = X1) => ((X7 @ Y3) => Y5)) => Y5)))) => Y4)) => Y4))) => (X3 = X3))))) => (((X7 @ (X6 @ (X6 @ (Y1 @ X3 @ X5)))) => c_False) => Y2)) => Y2))) => (X4 = X1))))))))) )),
% 7.51/1.73 inference(beta-eta_normalization,[],[f559])).
% 7.51/1.73 thf(f561,plain,(
% 7.51/1.73 ( ! [X2 : $i,X3 : $i,X1 : $i,X8 : ($i > $o),X6 : ($i > $i),X7 : ($i > $o),X4 : $i,X5 : $i] : (($true = (((^[Y0 : $i > $o]: (!! @ ($i > $i > $i) @ (^[Y1 : $i > $i > $i]: ((!! @ $o @ (^[Y2 : $o]: (((!! @ $i @ (^[Y3 : $i]: (((X6 @ X1) = Y3) => ((!! @ $o @ (^[Y4 : $o]: (((Y0 @ Y3) => (((X5 = X3) => (!! @ $o @ (^[Y5 : $o]: (((X2 = X1) => ((X7 @ Y3) => Y5)) => Y5)))) => Y4)) => Y4))) => (X3 = X3))))) => (((X7 @ (X6 @ (X6 @ (Y1 @ X3 @ X5)))) => c_False) => Y2)) => Y2))) => (X4 = X1))))) @ X8)))) )),
% 7.51/1.73 inference(pi_proxy_clausification,[],[f560])).
% 7.51/1.73 thf(f562,plain,(
% 7.51/1.73 ( ! [X2 : $i,X3 : $i,X1 : $i,X8 : ($i > $o),X6 : ($i > $i),X7 : ($i > $o),X4 : $i,X5 : $i] : (($true = ((!! @ ($i > $i > $i) @ (^[Y0 : $i > $i > $i]: ((!! @ $o @ (^[Y1 : $o]: (((!! @ $i @ (^[Y2 : $i]: (((X6 @ X1) = Y2) => ((!! @ $o @ (^[Y3 : $o]: (((X8 @ Y2) => (((X5 = X3) => (!! @ $o @ (^[Y4 : $o]: (((X2 = X1) => ((X7 @ Y2) => Y4)) => Y4)))) => Y3)) => Y3))) => (X3 = X3))))) => (((X7 @ (X6 @ (X6 @ (Y0 @ X3 @ X5)))) => c_False) => Y1)) => Y1))) => (X4 = X1))))))) )),
% 7.51/1.73 inference(beta-eta_normalization,[],[f561])).
% 7.51/1.73 thf(f563,plain,(
% 7.51/1.73 ( ! [X2 : $i,X3 : $i,X1 : $i,X8 : ($i > $o),X6 : ($i > $i),X9 : ($i > $i > $i),X7 : ($i > $o),X4 : $i,X5 : $i] : (($true = (((^[Y0 : $i > $i > $i]: ((!! @ $o @ (^[Y1 : $o]: (((!! @ $i @ (^[Y2 : $i]: (((X6 @ X1) = Y2) => ((!! @ $o @ (^[Y3 : $o]: (((X8 @ Y2) => (((X5 = X3) => (!! @ $o @ (^[Y4 : $o]: (((X2 = X1) => ((X7 @ Y2) => Y4)) => Y4)))) => Y3)) => Y3))) => (X3 = X3))))) => (((X7 @ (X6 @ (X6 @ (Y0 @ X3 @ X5)))) => c_False) => Y1)) => Y1))) => (X4 = X1))) @ X9)))) )),
% 7.51/1.73 inference(pi_proxy_clausification,[],[f562])).
% 7.51/1.73 thf(f564,plain,(
% 7.51/1.73 ( ! [X2 : $i,X3 : $i,X1 : $i,X8 : ($i > $o),X6 : ($i > $i),X9 : ($i > $i > $i),X7 : ($i > $o),X4 : $i,X5 : $i] : (($true = (((!! @ $o @ (^[Y0 : $o]: (((!! @ $i @ (^[Y1 : $i]: (((X6 @ X1) = Y1) => ((!! @ $o @ (^[Y2 : $o]: (((X8 @ Y1) => (((X5 = X3) => (!! @ $o @ (^[Y3 : $o]: (((X2 = X1) => ((X7 @ Y1) => Y3)) => Y3)))) => Y2)) => Y2))) => (X3 = X3))))) => (((X7 @ (X6 @ (X6 @ (X9 @ X3 @ X5)))) => c_False) => Y0)) => Y0))) => (X4 = X1))))) )),
% 7.51/1.73 inference(beta-eta_normalization,[],[f563])).
% 7.51/1.73 thf(f565,plain,(
% 7.51/1.73 ( ! [X2 : $i,X3 : $i,X1 : $i,X8 : ($i > $o),X6 : ($i > $i),X9 : ($i > $i > $i),X7 : ($i > $o),X4 : $i,X5 : $i] : (($false = ((!! @ $o @ (^[Y0 : $o]: (((!! @ $i @ (^[Y1 : $i]: (((X6 @ X1) = Y1) => ((!! @ $o @ (^[Y2 : $o]: (((X8 @ Y1) => (((X5 = X3) => (!! @ $o @ (^[Y3 : $o]: (((X2 = X1) => ((X7 @ Y1) => Y3)) => Y3)))) => Y2)) => Y2))) => (X3 = X3))))) => (((X7 @ (X6 @ (X6 @ (X9 @ X3 @ X5)))) => c_False) => Y0)) => Y0))))) | ($true = ((X4 = X1)))) )),
% 7.51/1.73 inference(imp_proxy_clausification,[],[f564])).
% 7.51/1.73 thf(f566,plain,(
% 7.51/1.73 ( ! [X2 : $i,X3 : $i,X1 : $i,X8 : ($i > $o),X6 : ($i > $i),X9 : ($i > $i > $i),X7 : ($i > $o),X4 : $i,X5 : $i] : (($false = (((^[Y0 : $o]: (((!! @ $i @ (^[Y1 : $i]: (((X6 @ X1) = Y1) => ((!! @ $o @ (^[Y2 : $o]: (((X8 @ Y1) => (((X5 = X3) => (!! @ $o @ (^[Y3 : $o]: (((X2 = X1) => ((X7 @ Y1) => Y3)) => Y3)))) => Y2)) => Y2))) => (X3 = X3))))) => (((X7 @ (X6 @ (X6 @ (X9 @ X3 @ X5)))) => c_False) => Y0)) => Y0)) @ (sK9 @ X1 @ X6 @ X8 @ X7 @ X9 @ X2 @ X3 @ X5)))) | ($true = ((X4 = X1)))) )),
% 7.51/1.73 inference(sigma_proxy_clausification,[],[f565])).
% 7.51/1.73 thf(f567,plain,(
% 7.51/1.73 ( ! [X2 : $i,X3 : $i,X1 : $i,X8 : ($i > $o),X6 : ($i > $i),X9 : ($i > $i > $i),X7 : ($i > $o),X4 : $i,X5 : $i] : (($false = (((^[Y0 : $o]: (((!! @ $i @ (^[Y1 : $i]: (((X6 @ X1) = Y1) => ((!! @ $o @ (^[Y2 : $o]: (((X8 @ Y1) => (((X5 = X3) => (!! @ $o @ (^[Y3 : $o]: (((X2 = X1) => ((X7 @ Y1) => Y3)) => Y3)))) => Y2)) => Y2))) => (X3 = X3))))) => (((X7 @ (X6 @ (X6 @ (X9 @ X3 @ X5)))) => c_False) => Y0)) => Y0)) @ (sK9 @ X1 @ X6 @ X8 @ X7 @ X9 @ X2 @ X3 @ X5)))) | (X1 = X4)) )),
% 7.51/1.73 inference(equality_proxy_clausification,[],[f566])).
% 7.51/1.73 thf(f568,plain,(
% 7.51/1.73 ( ! [X2 : $i,X3 : $i,X1 : $i,X8 : ($i > $o),X6 : ($i > $i),X9 : ($i > $i > $i),X7 : ($i > $o),X4 : $i,X5 : $i] : (($false = ((((!! @ $i @ (^[Y0 : $i]: (((X6 @ X1) = Y0) => ((!! @ $o @ (^[Y1 : $o]: (((X8 @ Y0) => (((X5 = X3) => (!! @ $o @ (^[Y2 : $o]: (((X2 = X1) => ((X7 @ Y0) => Y2)) => Y2)))) => Y1)) => Y1))) => (X3 = X3))))) => (((X7 @ (X6 @ (X6 @ (X9 @ X3 @ X5)))) => c_False) => (sK9 @ X1 @ X6 @ X8 @ X7 @ X9 @ X2 @ X3 @ X5))) => (sK9 @ X1 @ X6 @ X8 @ X7 @ X9 @ X2 @ X3 @ X5)))) | (X1 = X4)) )),
% 7.51/1.73 inference(beta-eta_normalization,[],[f567])).
% 7.51/1.73 thf(f569,plain,(
% 7.51/1.73 ( ! [X2 : $i,X3 : $i,X1 : $i,X8 : ($i > $o),X6 : ($i > $i),X9 : ($i > $i > $i),X7 : ($i > $o),X4 : $i,X5 : $i] : (($false = ((sK9 @ X1 @ X6 @ X8 @ X7 @ X9 @ X2 @ X3 @ X5))) | (X1 = X4)) )),
% 7.51/1.73 inference(imp_proxy_clausification,[],[f568])).
% 7.51/1.73 thf(f570,plain,(
% 7.51/1.73 ( ! [X2 : $i,X3 : $i,X1 : $i,X8 : ($i > $o),X6 : ($i > $i),X9 : ($i > $i > $i),X7 : ($i > $o),X4 : $i,X5 : $i] : (($true = (((!! @ $i @ (^[Y0 : $i]: (((X6 @ X1) = Y0) => ((!! @ $o @ (^[Y1 : $o]: (((X8 @ Y0) => (((X5 = X3) => (!! @ $o @ (^[Y2 : $o]: (((X2 = X1) => ((X7 @ Y0) => Y2)) => Y2)))) => Y1)) => Y1))) => (X3 = X3))))) => (((X7 @ (X6 @ (X6 @ (X9 @ X3 @ X5)))) => c_False) => (sK9 @ X1 @ X6 @ X8 @ X7 @ X9 @ X2 @ X3 @ X5))))) | (X1 = X4)) )),
% 7.51/1.73 inference(imp_proxy_clausification,[],[f568])).
% 7.51/1.73 thf(f571,plain,(
% 7.51/1.73 ( ! [X2 : $i,X3 : $i,X1 : $i,X8 : ($i > $o),X6 : ($i > $i),X9 : ($i > $i > $i),X7 : ($i > $o),X4 : $i,X5 : $i] : (($false = ((!! @ $i @ (^[Y0 : $i]: (((X6 @ X1) = Y0) => ((!! @ $o @ (^[Y1 : $o]: (((X8 @ Y0) => (((X5 = X3) => (!! @ $o @ (^[Y2 : $o]: (((X2 = X1) => ((X7 @ Y0) => Y2)) => Y2)))) => Y1)) => Y1))) => (X3 = X3))))))) | (X1 = X4) | ($true = ((((X7 @ (X6 @ (X6 @ (X9 @ X3 @ X5)))) => c_False) => (sK9 @ X1 @ X6 @ X8 @ X7 @ X9 @ X2 @ X3 @ X5))))) )),
% 7.51/1.73 inference(imp_proxy_clausification,[],[f570])).
% 7.51/1.73 thf(f572,plain,(
% 7.51/1.73 ( ! [X2 : $i,X3 : $i,X1 : $i,X8 : ($i > $o),X6 : ($i > $i),X9 : ($i > $i > $i),X7 : ($i > $o),X4 : $i,X5 : $i] : (($false = (((^[Y0 : $i]: (((X6 @ X1) = Y0) => ((!! @ $o @ (^[Y1 : $o]: (((X8 @ Y0) => (((X5 = X3) => (!! @ $o @ (^[Y2 : $o]: (((X2 = X1) => ((X7 @ Y0) => Y2)) => Y2)))) => Y1)) => Y1))) => (X3 = X3)))) @ (sK10 @ X1 @ X6 @ X8 @ X7 @ X2 @ X3 @ X5)))) | (X1 = X4) | ($true = ((((X7 @ (X6 @ (X6 @ (X9 @ X3 @ X5)))) => c_False) => (sK9 @ X1 @ X6 @ X8 @ X7 @ X9 @ X2 @ X3 @ X5))))) )),
% 7.51/1.73 inference(sigma_proxy_clausification,[],[f571])).
% 7.51/1.73 thf(f573,plain,(
% 7.51/1.73 ( ! [X2 : $i,X3 : $i,X1 : $i,X8 : ($i > $o),X6 : ($i > $i),X9 : ($i > $i > $i),X7 : ($i > $o),X4 : $i,X5 : $i] : (($false = (((^[Y0 : $i]: (((X6 @ X1) = Y0) => ((!! @ $o @ (^[Y1 : $o]: (((X8 @ Y0) => (((X5 = X3) => (!! @ $o @ (^[Y2 : $o]: (((X2 = X1) => ((X7 @ Y0) => Y2)) => Y2)))) => Y1)) => Y1))) => (X3 = X3)))) @ (sK10 @ X1 @ X6 @ X8 @ X7 @ X2 @ X3 @ X5)))) | (X1 = X4) | ($false = (((X7 @ (X6 @ (X6 @ (X9 @ X3 @ X5)))) => c_False))) | ($true = ((sK9 @ X1 @ X6 @ X8 @ X7 @ X9 @ X2 @ X3 @ X5)))) )),
% 7.51/1.73 inference(imp_proxy_clausification,[],[f572])).
% 7.51/1.73 thf(f575,plain,(
% 7.51/1.73 ( ! [X2 : $i,X3 : $i,X1 : $i,X8 : ($i > $o),X6 : ($i > $i),X9 : ($i > $i > $i),X7 : ($i > $o),X4 : $i,X5 : $i] : (($false = (((^[Y0 : $i]: (((X6 @ X1) = Y0) => ((!! @ $o @ (^[Y1 : $o]: (((X8 @ Y0) => (((X5 = X3) => (!! @ $o @ (^[Y2 : $o]: (((X2 = X1) => ((X7 @ Y0) => Y2)) => Y2)))) => Y1)) => Y1))) => (X3 = X3)))) @ (sK10 @ X1 @ X6 @ X8 @ X7 @ X2 @ X3 @ X5)))) | (X1 = X4) | ($true = ((X7 @ (X6 @ (X6 @ (X9 @ X3 @ X5)))))) | ($true = ((sK9 @ X1 @ X6 @ X8 @ X7 @ X9 @ X2 @ X3 @ X5)))) )),
% 7.51/1.73 inference(imp_proxy_clausification,[],[f573])).
% 7.51/1.73 thf(f576,plain,(
% 7.51/1.73 ( ! [X2 : $i,X3 : $i,X1 : $i,X8 : ($i > $o),X6 : ($i > $i),X9 : ($i > $i > $i),X7 : ($i > $o),X4 : $i,X5 : $i] : (($false = ((((X6 @ X1) = (sK10 @ X1 @ X6 @ X8 @ X7 @ X2 @ X3 @ X5)) => ((!! @ $o @ (^[Y0 : $o]: (((X8 @ (sK10 @ X1 @ X6 @ X8 @ X7 @ X2 @ X3 @ X5)) => (((X5 = X3) => (!! @ $o @ (^[Y1 : $o]: (((X2 = X1) => ((X7 @ (sK10 @ X1 @ X6 @ X8 @ X7 @ X2 @ X3 @ X5)) => Y1)) => Y1)))) => Y0)) => Y0))) => (X3 = X3))))) | (X1 = X4) | ($true = ((X7 @ (X6 @ (X6 @ (X9 @ X3 @ X5)))))) | ($true = ((sK9 @ X1 @ X6 @ X8 @ X7 @ X9 @ X2 @ X3 @ X5)))) )),
% 7.51/1.73 inference(beta-eta_normalization,[],[f575])).
% 7.51/1.73 thf(f577,plain,(
% 7.51/1.73 ( ! [X2 : $i,X3 : $i,X1 : $i,X8 : ($i > $o),X6 : ($i > $i),X9 : ($i > $i > $i),X7 : ($i > $o),X4 : $i,X5 : $i] : (($false = (((!! @ $o @ (^[Y0 : $o]: (((X8 @ (sK10 @ X1 @ X6 @ X8 @ X7 @ X2 @ X3 @ X5)) => (((X5 = X3) => (!! @ $o @ (^[Y1 : $o]: (((X2 = X1) => ((X7 @ (sK10 @ X1 @ X6 @ X8 @ X7 @ X2 @ X3 @ X5)) => Y1)) => Y1)))) => Y0)) => Y0))) => (X3 = X3)))) | (X1 = X4) | ($true = ((X7 @ (X6 @ (X6 @ (X9 @ X3 @ X5)))))) | ($true = ((sK9 @ X1 @ X6 @ X8 @ X7 @ X9 @ X2 @ X3 @ X5)))) )),
% 7.51/1.73 inference(imp_proxy_clausification,[],[f576])).
% 7.51/1.73 thf(f580,plain,(
% 7.51/1.73 ( ! [X2 : $i,X3 : $i,X1 : $i,X8 : ($i > $o),X6 : ($i > $i),X9 : ($i > $i > $i),X7 : ($i > $o),X4 : $i,X5 : $i] : (($false = ((X3 = X3))) | (X1 = X4) | ($true = ((X7 @ (X6 @ (X6 @ (X9 @ X3 @ X5)))))) | ($true = ((sK9 @ X1 @ X6 @ X8 @ X7 @ X9 @ X2 @ X3 @ X5)))) )),
% 7.51/1.73 inference(imp_proxy_clausification,[],[f577])).
% 7.51/1.73 thf(f599,plain,(
% 7.51/1.73 ( ! [X2 : $i,X3 : $i,X1 : $i,X8 : ($i > $o),X6 : ($i > $i),X9 : ($i > $i > $i),X7 : ($i > $o),X4 : $i,X5 : $i] : ((X3 != X3) | (X1 = X4) | ($true = ((X7 @ (X6 @ (X6 @ (X9 @ X3 @ X5)))))) | ($true = ((sK9 @ X1 @ X6 @ X8 @ X7 @ X9 @ X2 @ X3 @ X5)))) )),
% 7.51/1.73 inference(equality_proxy_clausification,[],[f580])).
% 7.51/1.73 thf(f600,plain,(
% 7.51/1.73 ( ! [X2 : $i,X3 : $i,X1 : $i,X8 : ($i > $o),X6 : ($i > $i),X9 : ($i > $i > $i),X7 : ($i > $o),X4 : $i,X5 : $i] : ((X1 = X4) | ($true = ((X7 @ (X6 @ (X6 @ (X9 @ X3 @ X5)))))) | ($true = ((sK9 @ X1 @ X6 @ X8 @ X7 @ X9 @ X2 @ X3 @ X5)))) )),
% 7.51/1.73 inference(trivial_inequality_removal,[],[f599])).
% 7.51/1.73 thf(f642,plain,(
% 7.51/1.73 ( ! [X2 : $i,X0 : $i,X1 : ($i > $i)] : (($true = ((!! @ $o @ (^[Y0 : $o]: ((((c_In @ X2 @ (c_Repl @ X0 @ X1)) => (?? @ $i @ (^[Y1 : $i]: (!! @ $o @ (^[Y2 : $o]: (((c_In @ Y1 @ X0) => (((X1 @ Y1) = X2) => Y2)) => Y2)))))) => (((?? @ $i @ (^[Y1 : $i]: (!! @ $o @ (^[Y2 : $o]: (((c_In @ Y1 @ X0) => (((X1 @ Y1) = X2) => Y2)) => Y2))))) => (c_In @ X2 @ (c_Repl @ X0 @ X1))) => Y0)) => Y0)))))) )),
% 7.51/1.73 inference(beta-eta_normalization,[],[f542])).
% 7.51/1.73 thf(f643,plain,(
% 7.51/1.73 ( ! [X2 : $i,X3 : $o,X0 : $i,X1 : ($i > $i)] : (($true = (((^[Y0 : $o]: ((((c_In @ X2 @ (c_Repl @ X0 @ X1)) => (?? @ $i @ (^[Y1 : $i]: (!! @ $o @ (^[Y2 : $o]: (((c_In @ Y1 @ X0) => (((X1 @ Y1) = X2) => Y2)) => Y2)))))) => (((?? @ $i @ (^[Y1 : $i]: (!! @ $o @ (^[Y2 : $o]: (((c_In @ Y1 @ X0) => (((X1 @ Y1) = X2) => Y2)) => Y2))))) => (c_In @ X2 @ (c_Repl @ X0 @ X1))) => Y0)) => Y0)) @ X3)))) )),
% 7.51/1.73 inference(pi_proxy_clausification,[],[f642])).
% 7.51/1.73 thf(f644,plain,(
% 7.51/1.73 ( ! [X2 : $i,X3 : $o,X0 : $i,X1 : ($i > $i)] : (($true = (((((c_In @ X2 @ (c_Repl @ X0 @ X1)) => (?? @ $i @ (^[Y0 : $i]: (!! @ $o @ (^[Y1 : $o]: (((c_In @ Y0 @ X0) => (((X1 @ Y0) = X2) => Y1)) => Y1)))))) => (((?? @ $i @ (^[Y0 : $i]: (!! @ $o @ (^[Y1 : $o]: (((c_In @ Y0 @ X0) => (((X1 @ Y0) = X2) => Y1)) => Y1))))) => (c_In @ X2 @ (c_Repl @ X0 @ X1))) => X3)) => X3)))) )),
% 7.51/1.73 inference(beta-eta_normalization,[],[f643])).
% 7.51/1.73 thf(f645,plain,(
% 7.51/1.73 ( ! [X2 : $i,X3 : $o,X0 : $i,X1 : ($i > $i)] : (($false = ((((c_In @ X2 @ (c_Repl @ X0 @ X1)) => (?? @ $i @ (^[Y0 : $i]: (!! @ $o @ (^[Y1 : $o]: (((c_In @ Y0 @ X0) => (((X1 @ Y0) = X2) => Y1)) => Y1)))))) => (((?? @ $i @ (^[Y0 : $i]: (!! @ $o @ (^[Y1 : $o]: (((c_In @ Y0 @ X0) => (((X1 @ Y0) = X2) => Y1)) => Y1))))) => (c_In @ X2 @ (c_Repl @ X0 @ X1))) => X3)))) | ($true = X3)) )),
% 7.51/1.73 inference(imp_proxy_clausification,[],[f644])).
% 7.51/1.73 thf(f646,plain,(
% 7.51/1.73 ( ! [X2 : $i,X3 : $o,X0 : $i,X1 : ($i > $i)] : (($false = ((((?? @ $i @ (^[Y0 : $i]: (!! @ $o @ (^[Y1 : $o]: (((c_In @ Y0 @ X0) => (((X1 @ Y0) = X2) => Y1)) => Y1))))) => (c_In @ X2 @ (c_Repl @ X0 @ X1))) => X3))) | ($true = X3)) )),
% 7.51/1.73 inference(imp_proxy_clausification,[],[f645])).
% 7.51/1.73 thf(f647,plain,(
% 7.51/1.73 ( ! [X2 : $i,X3 : $o,X0 : $i,X1 : ($i > $i)] : (($true = (((c_In @ X2 @ (c_Repl @ X0 @ X1)) => (?? @ $i @ (^[Y0 : $i]: (!! @ $o @ (^[Y1 : $o]: (((c_In @ Y0 @ X0) => (((X1 @ Y0) = X2) => Y1)) => Y1)))))))) | ($true = X3)) )),
% 7.51/1.73 inference(imp_proxy_clausification,[],[f645])).
% 7.51/1.73 thf(f648,plain,(
% 7.51/1.73 ( ! [X2 : $i,X3 : $o,X0 : $i,X1 : ($i > $i)] : (($false = ((c_In @ X2 @ (c_Repl @ X0 @ X1)))) | ($true = X3) | ($true = ((?? @ $i @ (^[Y0 : $i]: (!! @ $o @ (^[Y1 : $o]: (((c_In @ Y0 @ X0) => (((X1 @ Y0) = X2) => Y1)) => Y1)))))))) )),
% 7.51/1.73 inference(imp_proxy_clausification,[],[f647])).
% 7.51/1.73 thf(f649,plain,(
% 7.51/1.73 ( ! [X2 : $i,X3 : $o,X0 : $i,X1 : ($i > $i)] : (($false = ((c_In @ X2 @ (c_Repl @ X0 @ X1)))) | ($true = X3) | ($true = (((^[Y0 : $i]: (!! @ $o @ (^[Y1 : $o]: (((c_In @ Y0 @ X0) => (((X1 @ Y0) = X2) => Y1)) => Y1)))) @ (sK13 @ X1 @ X0 @ X2))))) )),
% 7.51/1.73 inference(sigma_proxy_clausification,[],[f648])).
% 7.51/1.73 thf(f650,plain,(
% 7.51/1.73 ( ! [X2 : $i,X3 : $o,X0 : $i,X1 : ($i > $i)] : (($false = ((c_In @ X2 @ (c_Repl @ X0 @ X1)))) | ($true = X3) | ($true = ((!! @ $o @ (^[Y0 : $o]: (((c_In @ (sK13 @ X1 @ X0 @ X2) @ X0) => (((X1 @ (sK13 @ X1 @ X0 @ X2)) = X2) => Y0)) => Y0)))))) )),
% 7.51/1.73 inference(beta-eta_normalization,[],[f649])).
% 7.51/1.73 thf(f651,plain,(
% 7.51/1.73 ( ! [X2 : $i,X3 : $o,X0 : $i,X1 : ($i > $i),X4 : $o] : (($false = ((c_In @ X2 @ (c_Repl @ X0 @ X1)))) | ($true = X3) | ($true = (((^[Y0 : $o]: (((c_In @ (sK13 @ X1 @ X0 @ X2) @ X0) => (((X1 @ (sK13 @ X1 @ X0 @ X2)) = X2) => Y0)) => Y0)) @ X4)))) )),
% 7.51/1.73 inference(pi_proxy_clausification,[],[f650])).
% 7.51/1.73 thf(f652,plain,(
% 7.51/1.73 ( ! [X2 : $i,X3 : $o,X0 : $i,X1 : ($i > $i),X4 : $o] : (($false = ((c_In @ X2 @ (c_Repl @ X0 @ X1)))) | ($true = X3) | ($true = ((((c_In @ (sK13 @ X1 @ X0 @ X2) @ X0) => (((X1 @ (sK13 @ X1 @ X0 @ X2)) = X2) => X4)) => X4)))) )),
% 7.51/1.73 inference(beta-eta_normalization,[],[f651])).
% 7.51/1.73 thf(f653,plain,(
% 7.51/1.73 ( ! [X2 : $i,X3 : $o,X0 : $i,X1 : ($i > $i),X4 : $o] : (($false = ((c_In @ X2 @ (c_Repl @ X0 @ X1)))) | ($true = X3) | ($false = (((c_In @ (sK13 @ X1 @ X0 @ X2) @ X0) => (((X1 @ (sK13 @ X1 @ X0 @ X2)) = X2) => X4)))) | ($true = X4)) )),
% 7.51/1.73 inference(imp_proxy_clausification,[],[f652])).
% 7.51/1.73 thf(f655,plain,(
% 7.51/1.73 ( ! [X2 : $i,X3 : $o,X0 : $i,X1 : ($i > $i),X4 : $o] : (($false = ((c_In @ X2 @ (c_Repl @ X0 @ X1)))) | ($true = X3) | ($true = ((c_In @ (sK13 @ X1 @ X0 @ X2) @ X0))) | ($true = X4)) )),
% 7.51/1.73 inference(imp_proxy_clausification,[],[f653])).
% 7.51/1.73 thf(f659,plain,(
% 7.51/1.73 ( ! [X3 : $o] : (($false = X3) | ($true = X3)) )),
% 7.51/1.73 inference(imp_proxy_clausification,[],[f646])).
% 7.51/1.73 thf(f671,plain,(
% 7.51/1.73 ( ! [X0 : $i,X1 : $i] : (($true = ((!! @ $o @ (^[Y0 : $o]: ((((c_In @ X1 @ (c_Power @ X0)) => (!! @ $i @ (^[Y1 : $i]: ((c_In @ Y1 @ X1) => (c_In @ Y1 @ X0))))) => (((!! @ $i @ (^[Y1 : $i]: ((c_In @ Y1 @ X1) => (c_In @ Y1 @ X0)))) => (c_In @ X1 @ (c_Power @ X0))) => Y0)) => Y0)))))) )),
% 7.51/1.73 inference(beta-eta_normalization,[],[f541])).
% 7.51/1.73 thf(f672,plain,(
% 7.51/1.73 ( ! [X2 : $o,X0 : $i,X1 : $i] : (($true = (((^[Y0 : $o]: ((((c_In @ X1 @ (c_Power @ X0)) => (!! @ $i @ (^[Y1 : $i]: ((c_In @ Y1 @ X1) => (c_In @ Y1 @ X0))))) => (((!! @ $i @ (^[Y1 : $i]: ((c_In @ Y1 @ X1) => (c_In @ Y1 @ X0)))) => (c_In @ X1 @ (c_Power @ X0))) => Y0)) => Y0)) @ X2)))) )),
% 7.51/1.73 inference(pi_proxy_clausification,[],[f671])).
% 7.51/1.73 thf(f673,plain,(
% 7.51/1.73 ( ! [X2 : $o,X0 : $i,X1 : $i] : (($true = (((((c_In @ X1 @ (c_Power @ X0)) => (!! @ $i @ (^[Y0 : $i]: ((c_In @ Y0 @ X1) => (c_In @ Y0 @ X0))))) => (((!! @ $i @ (^[Y0 : $i]: ((c_In @ Y0 @ X1) => (c_In @ Y0 @ X0)))) => (c_In @ X1 @ (c_Power @ X0))) => X2)) => X2)))) )),
% 7.51/1.73 inference(beta-eta_normalization,[],[f672])).
% 7.51/1.73 thf(f674,plain,(
% 7.51/1.73 ( ! [X2 : $o,X0 : $i,X1 : $i] : (($false = ((((c_In @ X1 @ (c_Power @ X0)) => (!! @ $i @ (^[Y0 : $i]: ((c_In @ Y0 @ X1) => (c_In @ Y0 @ X0))))) => (((!! @ $i @ (^[Y0 : $i]: ((c_In @ Y0 @ X1) => (c_In @ Y0 @ X0)))) => (c_In @ X1 @ (c_Power @ X0))) => X2)))) | ($true = X2)) )),
% 7.51/1.73 inference(imp_proxy_clausification,[],[f673])).
% 7.51/1.73 thf(f675,plain,(
% 7.51/1.73 ( ! [X2 : $o,X0 : $i,X1 : $i] : (($false = ((((!! @ $i @ (^[Y0 : $i]: ((c_In @ Y0 @ X1) => (c_In @ Y0 @ X0)))) => (c_In @ X1 @ (c_Power @ X0))) => X2))) | ($true = X2)) )),
% 7.51/1.73 inference(imp_proxy_clausification,[],[f674])).
% 7.51/1.73 thf(f682,plain,(
% 7.51/1.73 ( ! [X2 : $o,X0 : $i,X1 : $i] : (($true = (((!! @ $i @ (^[Y0 : $i]: ((c_In @ Y0 @ X1) => (c_In @ Y0 @ X0)))) => (c_In @ X1 @ (c_Power @ X0))))) | ($true = X2)) )),
% 7.51/1.73 inference(imp_proxy_clausification,[],[f675])).
% 7.51/1.73 thf(f683,plain,(
% 7.51/1.73 ( ! [X2 : $o,X0 : $i,X1 : $i] : (($false = ((!! @ $i @ (^[Y0 : $i]: ((c_In @ Y0 @ X1) => (c_In @ Y0 @ X0)))))) | ($true = X2) | (((c_In @ X1 @ (c_Power @ X0))) = $true)) )),
% 7.51/1.73 inference(imp_proxy_clausification,[],[f682])).
% 7.51/1.73 thf(f684,plain,(
% 7.51/1.73 ( ! [X2 : $o,X0 : $i,X1 : $i] : (($false = (((^[Y0 : $i]: ((c_In @ Y0 @ X1) => (c_In @ Y0 @ X0))) @ (sK15 @ X1 @ X0)))) | ($true = X2) | (((c_In @ X1 @ (c_Power @ X0))) = $true)) )),
% 7.51/1.73 inference(sigma_proxy_clausification,[],[f683])).
% 7.51/1.73 thf(f685,plain,(
% 7.51/1.73 ( ! [X2 : $o,X0 : $i,X1 : $i] : (($false = (((c_In @ (sK15 @ X1 @ X0) @ X1) => (c_In @ (sK15 @ X1 @ X0) @ X0)))) | ($true = X2) | (((c_In @ X1 @ (c_Power @ X0))) = $true)) )),
% 7.51/1.73 inference(beta-eta_normalization,[],[f684])).
% 7.51/1.73 thf(f687,plain,(
% 7.51/1.73 ( ! [X2 : $o,X0 : $i,X1 : $i] : (($true = ((c_In @ (sK15 @ X1 @ X0) @ X1))) | ($true = X2) | (((c_In @ X1 @ (c_Power @ X0))) = $true)) )),
% 7.51/1.73 inference(imp_proxy_clausification,[],[f685])).
% 7.51/1.73 thf(f715,plain,(
% 7.51/1.73 ($true = (((?? @ $i @ (^[Y0 : $i]: (c_In @ Y0 @ c_Empty))) => c_False)))),
% 7.51/1.73 inference(beta-eta_normalization,[],[f539])).
% 7.51/1.73 thf(f716,plain,(
% 7.51/1.73 (((?? @ $i @ (^[Y0 : $i]: (c_In @ Y0 @ c_Empty)))) = $false) | (c_False = $true)),
% 7.51/1.73 inference(imp_proxy_clausification,[],[f715])).
% 7.51/1.73 thf(f717,plain,(
% 7.51/1.73 ( ! [X1 : $i] : (($false = (((^[Y0 : $i]: (c_In @ Y0 @ c_Empty)) @ X1))) | (c_False = $true)) )),
% 7.51/1.73 inference(pi_proxy_clausification,[],[f716])).
% 7.51/1.73 thf(f718,plain,(
% 7.51/1.73 ( ! [X1 : $i] : (($false = ((c_In @ X1 @ c_Empty))) | (c_False = $true)) )),
% 7.51/1.73 inference(beta-eta_normalization,[],[f717])).
% 7.51/1.73 thf(f772,definition,(
% 7.51/1.73 spl22_1 <=> ! [X10 : $o] : ($true = X10)),
% 7.51/1.73 introduced(definition,[new_symbols(definition,[spl22_1])],[avatar_definition])).
% 7.51/1.73 thf(f773,plain,(
% 7.51/1.73 ( ! [X10 : $o] : (($true = X10)) ) | ~spl22_1),
% 7.51/1.73 inference(avatar_component_clause,[],[f772])).
% 7.51/1.73 thf(f787,definition,(
% 7.51/1.73 spl22_5 <=> ! [X11 : $o] : (($false = X11) | ($true = X11))),
% 7.51/1.73 introduced(definition,[new_symbols(definition,[spl22_5])],[avatar_definition])).
% 7.51/1.73 thf(f788,plain,(
% 7.51/1.73 ( ! [X11 : $o] : (($true = X11) | ($false = X11)) ) | ~spl22_5),
% 7.51/1.73 inference(avatar_component_clause,[],[f787])).
% 7.51/1.73 thf(f794,definition,(
% 7.51/1.73 spl22_7 <=> ! [X2 : $i,X3 : $i,X1 : $i,X8 : ($i > $o),X6 : ($i > $i),X9 : ($i > $i > $i),X7 : ($i > $o),X4 : $i,X5 : $i] : ((X1 = X4) | ($true = ((sK9 @ X1 @ X6 @ X8 @ X7 @ X9 @ X2 @ X3 @ X5))) | ($true = ((X7 @ (X6 @ (X6 @ (X9 @ X3 @ X5)))))))),
% 7.51/1.73 introduced(definition,[new_symbols(definition,[spl22_7])],[avatar_definition])).
% 7.51/1.73 thf(f795,plain,(
% 7.51/1.73 ( ! [X2 : $i,X3 : $i,X1 : $i,X8 : ($i > $o),X6 : ($i > $i),X9 : ($i > $i > $i),X7 : ($i > $o),X4 : $i,X5 : $i] : ((X1 = X4) | ($true = ((sK9 @ X1 @ X6 @ X8 @ X7 @ X9 @ X2 @ X3 @ X5))) | ($true = ((X7 @ (X6 @ (X6 @ (X9 @ X3 @ X5))))))) ) | ~spl22_7),
% 7.51/1.73 inference(avatar_component_clause,[],[f794])).
% 7.51/1.73 thf(f797,plain,(
% 7.51/1.73 spl22_7),
% 7.51/1.73 inference(avatar_split_clause,[],[f600,f794])).
% 7.51/1.73 thf(f799,definition,(
% 7.51/1.73 spl22_8 <=> (c_False = $false)),
% 7.51/1.73 introduced(definition,[new_symbols(definition,[spl22_8])],[avatar_definition])).
% 7.51/1.73 thf(f801,plain,(
% 7.51/1.73 (c_False = $false) | ~spl22_8),
% 7.51/1.73 inference(avatar_component_clause,[],[f799])).
% 7.51/1.73 thf(f827,plain,(
% 7.51/1.73 spl22_8),
% 7.51/1.73 inference(avatar_split_clause,[],[f545,f799])).
% 7.51/1.73 thf(f853,definition,(
% 7.51/1.73 spl22_20 <=> (c_False = $true)),
% 7.51/1.73 introduced(definition,[new_symbols(definition,[spl22_20])],[avatar_definition])).
% 7.51/1.73 thf(f855,plain,(
% 7.51/1.73 (c_False = $true) | ~spl22_20),
% 7.51/1.73 inference(avatar_component_clause,[],[f853])).
% 7.51/1.73 thf(f858,definition,(
% 7.51/1.73 spl22_21 <=> ! [X2 : $i,X0 : $i,X1 : ($i > $i)] : (($false = ((c_In @ X2 @ (c_Repl @ X0 @ X1)))) | ($true = ((c_In @ (sK13 @ X1 @ X0 @ X2) @ X0))))),
% 7.51/1.73 introduced(definition,[new_symbols(definition,[spl22_21])],[avatar_definition])).
% 7.51/1.73 thf(f859,plain,(
% 7.51/1.73 ( ! [X2 : $i,X0 : $i,X1 : ($i > $i)] : (($false = ((c_In @ X2 @ (c_Repl @ X0 @ X1)))) | ($true = ((c_In @ (sK13 @ X1 @ X0 @ X2) @ X0)))) ) | ~spl22_21),
% 7.51/1.73 inference(avatar_component_clause,[],[f858])).
% 7.51/1.73 thf(f860,plain,(
% 7.51/1.73 spl22_1 | spl22_1 | spl22_21),
% 7.51/1.73 inference(avatar_split_clause,[],[f655,f858,f772,f772])).
% 7.51/1.73 thf(f877,plain,(
% 7.51/1.73 spl22_5),
% 7.51/1.73 inference(avatar_split_clause,[],[f659,f787])).
% 7.51/1.73 thf(f883,definition,(
% 7.51/1.73 spl22_27 <=> ! [X0 : $i,X1 : $i] : (($true = ((c_In @ (sK15 @ X1 @ X0) @ X1))) | (((c_In @ X1 @ (c_Power @ X0))) = $true))),
% 7.51/1.73 introduced(definition,[new_symbols(definition,[spl22_27])],[avatar_definition])).
% 7.51/1.73 thf(f884,plain,(
% 7.51/1.73 ( ! [X0 : $i,X1 : $i] : (($true = ((c_In @ (sK15 @ X1 @ X0) @ X1))) | (((c_In @ X1 @ (c_Power @ X0))) = $true)) ) | ~spl22_27),
% 7.51/1.73 inference(avatar_component_clause,[],[f883])).
% 7.51/1.73 thf(f885,plain,(
% 7.51/1.73 spl22_1 | spl22_27),
% 7.51/1.73 inference(avatar_split_clause,[],[f687,f883,f772])).
% 7.51/1.73 thf(f911,definition,(
% 7.51/1.73 spl22_34 <=> ! [X1 : $i] : ($false = ((c_In @ X1 @ c_Empty)))),
% 7.51/1.73 introduced(definition,[new_symbols(definition,[spl22_34])],[avatar_definition])).
% 7.51/1.73 thf(f912,plain,(
% 7.51/1.73 ( ! [X1 : $i] : (($false = ((c_In @ X1 @ c_Empty)))) ) | ~spl22_34),
% 7.51/1.73 inference(avatar_component_clause,[],[f911])).
% 7.51/1.73 thf(f913,plain,(
% 7.51/1.73 spl22_20 | spl22_34),
% 7.51/1.73 inference(avatar_split_clause,[],[f718,f911,f853])).
% 7.51/1.73 thf(f916,plain,(
% 7.51/1.73 ($true = $false) | (~spl22_8 | ~spl22_20)),
% 7.51/1.73 inference(forward_demodulation,[],[f855,f801])).
% 7.51/1.73 thf(f917,plain,(
% 7.51/1.73 $false | (~spl22_8 | ~spl22_20)),
% 7.51/1.73 inference(trivial_inequality_removal,[],[f916])).
% 7.51/1.73 thf(f918,plain,(
% 7.51/1.73 ~spl22_8 | ~spl22_20),
% 7.51/1.73 inference(avatar_contradiction_clause,[],[f917])).
% 7.51/1.73 thf(f955,plain,(
% 7.51/1.73 ( ! [X2 : $i,X3 : $i,X1 : $i,X8 : ($i > $o),X6 : ($i > $i),X9 : ($i > $i > $i),X4 : $i,X5 : $i] : ((X1 = X4) | ($true = ((sK9 @ X1 @ X6 @ X8 @ (^[Y0 : $i]: ($false)) @ X9 @ X2 @ X3 @ X5))) | ($true = (((^[Y0 : $i]: ($false)) @ (X6 @ (X6 @ (X9 @ X3 @ X5))))))) ) | ~spl22_7),
% 7.51/1.73 inference(primitive_instantiation,[],[f795])).
% 7.51/1.73 thf(f1013,plain,(
% 7.51/1.73 ( ! [X2 : $i,X3 : $i,X1 : $i,X8 : ($i > $o),X6 : ($i > $i),X9 : ($i > $i > $i),X4 : $i,X5 : $i] : ((X1 = X4) | ($true = ((sK9 @ X1 @ X6 @ X8 @ (^[Y0 : $i]: ($false)) @ X9 @ X2 @ X3 @ X5))) | ($true = $false)) ) | ~spl22_7),
% 7.51/1.73 inference(beta-eta_normalization,[],[f955])).
% 7.51/1.73 thf(f1014,plain,(
% 7.51/1.73 ( ! [X2 : $i,X3 : $i,X1 : $i,X8 : ($i > $o),X6 : ($i > $i),X9 : ($i > $i > $i),X4 : $i,X5 : $i] : ((X1 = X4) | ($true = ((sK9 @ X1 @ X6 @ X8 @ (^[Y0 : $i]: ($false)) @ X9 @ X2 @ X3 @ X5)))) ) | ~spl22_7),
% 7.51/1.73 inference(trivial_inequality_removal,[],[f1013])).
% 7.51/1.73 thf(f1138,plain,(
% 7.51/1.73 ( ! [X0 : ($i > $i),X1 : $i] : (($true = $false) | ($false = ((c_In @ X1 @ (c_Repl @ c_Empty @ X0))))) ) | (~spl22_21 | ~spl22_34)),
% 7.51/1.73 inference(constrained_superposition,[],[f912,f859])).
% 7.51/1.73 thf(f1147,plain,(
% 7.51/1.73 ( ! [X0 : ($i > $i),X1 : $i] : (($false = ((c_In @ X1 @ (c_Repl @ c_Empty @ X0))))) ) | (~spl22_21 | ~spl22_34)),
% 7.51/1.73 inference(trivial_inequality_removal,[],[f1138])).
% 7.51/1.73 thf(f1365,plain,(
% 7.51/1.73 ( ! [X0 : ($i > $o),X1 : $i] : (($true != $true) | (((X0 @ (c_Eps_i @ X0))) = $true) | (((X0 @ X1)) = $false)) ) | ~spl22_5),
% 7.51/1.73 inference(constrained_superposition,[],[f330,f788])).
% 7.51/1.73 thf(f1458,plain,(
% 7.51/1.73 ( ! [X0 : ($i > $o),X1 : $i] : ((((X0 @ (c_Eps_i @ X0))) = $true) | (((X0 @ X1)) = $false)) ) | ~spl22_5),
% 7.51/1.73 inference(trivial_inequality_removal,[],[f1365])).
% 7.51/1.73 thf(f1468,definition,(
% 7.51/1.73 spl22_40 <=> ! [X0 : ($i > $o),X1 : $i] : ((((X0 @ (c_Eps_i @ X0))) = $true) | (((X0 @ X1)) = $false))),
% 7.51/1.73 introduced(definition,[new_symbols(definition,[spl22_40])],[avatar_definition])).
% 7.51/1.73 thf(f1469,plain,(
% 7.51/1.73 ( ! [X0 : ($i > $o),X1 : $i] : ((((X0 @ (c_Eps_i @ X0))) = $true) | (((X0 @ X1)) = $false)) ) | ~spl22_40),
% 7.51/1.73 inference(avatar_component_clause,[],[f1468])).
% 7.51/1.73 thf(f1472,plain,(
% 7.51/1.73 spl22_40 | ~spl22_5),
% 7.51/1.73 inference(avatar_split_clause,[],[f1458,f787,f1468])).
% 7.51/1.73 thf(f2623,plain,(
% 7.51/1.73 ($true = $false) | (~spl22_1 | ~spl22_8)),
% 7.51/1.73 inference(constrained_superposition,[],[f801,f773])).
% 7.51/1.73 thf(f2644,plain,(
% 7.51/1.73 $false | (~spl22_1 | ~spl22_8)),
% 7.51/1.73 inference(trivial_inequality_removal,[],[f2623])).
% 7.51/1.73 thf(f2645,plain,(
% 7.51/1.73 ~spl22_1 | ~spl22_8),
% 7.51/1.73 inference(avatar_contradiction_clause,[],[f2644])).
% 7.51/1.73 thf(f2922,plain,(
% 7.51/1.73 ( ! [X0 : $i,X8 : $i,X7 : $i] : (($true = $false) | (X0 = X7) | (X0 = X8)) ) | ~spl22_7),
% 7.51/1.73 inference(constrained_superposition,[],[f1014,f569])).
% 7.51/1.73 thf(f2947,plain,(
% 7.51/1.73 ( ! [X0 : $i,X8 : $i,X7 : $i] : ((X0 = X7) | (X0 = X8)) ) | ~spl22_7),
% 7.51/1.73 inference(trivial_inequality_removal,[],[f2922])).
% 7.51/1.73 thf(f2970,definition,(
% 7.51/1.73 spl22_57 <=> ! [X16 : $i,X0 : $i] : (X0 = X16)),
% 7.51/1.73 introduced(definition,[new_symbols(definition,[spl22_57])],[avatar_definition])).
% 7.51/1.73 thf(f2971,plain,(
% 7.51/1.73 ( ! [X0 : $i,X16 : $i] : ((X0 = X16)) ) | ~spl22_57),
% 7.51/1.73 inference(avatar_component_clause,[],[f2970])).
% 7.51/1.73 thf(f3014,plain,(
% 7.51/1.73 ( ! [X0 : $i,X1 : $i] : ((((c_In @ X1 @ X0)) = $false)) ) | (~spl22_21 | ~spl22_34 | ~spl22_57)),
% 7.51/1.73 inference(constrained_superposition,[],[f1147,f2971])).
% 7.51/1.73 thf(f3016,plain,(
% 7.51/1.73 ( ! [X2 : $i,X0 : $i,X1 : ($i > $o)] : ((((X1 @ X0)) = $true) | (((X1 @ X2)) = $false)) ) | (~spl22_40 | ~spl22_57)),
% 7.51/1.73 inference(constrained_superposition,[],[f1469,f2971])).
% 7.51/1.73 thf(f3298,plain,(
% 7.51/1.73 ( ! [X0 : $i,X1 : $i] : ((X1 != X1) | (X0 = X1)) ) | ~spl22_7),
% 7.51/1.73 inference(equality_factoring,[],[f2947])).
% 7.51/1.73 thf(f3299,plain,(
% 7.51/1.73 ( ! [X0 : $i,X1 : $i] : ((X0 = X1)) ) | ~spl22_7),
% 7.51/1.73 inference(trivial_inequality_removal,[],[f3298])).
% 7.51/1.73 thf(f4827,plain,(
% 7.51/1.73 ( ! [X2 : ($i > $i),X3 : $i,X0 : $i,X1 : $i,X6 : ($i > $i),X4 : $i,X5 : ($i > $i)] : (($true = $false) | ($true = ((c_In @ X0 @ (c_Power @ X1)))) | ($true = (((^[Y0 : $i]: (c_In @ ((^[Y1 : $i]: (sK15 @ (X5 @ Y1) @ (X6 @ Y1))) @ Y0) @ (X2 @ Y0))) @ X4))) | (((X5 @ X3)) != X0) | (((X6 @ X3)) != X1) | (((X2 @ X3)) != X0)) ) | (~spl22_27 | ~spl22_40 | ~spl22_57)),
% 7.51/1.73 inference(constrained_superposition,[],[f884,f3016])).
% 7.51/1.73 thf(f5003,plain,(
% 7.51/1.73 ( ! [X2 : ($i > $i),X3 : $i,X0 : $i,X1 : $i,X6 : ($i > $i),X4 : $i,X5 : ($i > $i)] : (($true = ((c_In @ X0 @ (c_Power @ X1)))) | ($true = (((^[Y0 : $i]: (c_In @ ((^[Y1 : $i]: (sK15 @ (X5 @ Y1) @ (X6 @ Y1))) @ Y0) @ (X2 @ Y0))) @ X4))) | (((X5 @ X3)) != X0) | (((X6 @ X3)) != X1) | (((X2 @ X3)) != X0)) ) | (~spl22_27 | ~spl22_40 | ~spl22_57)),
% 7.51/1.73 inference(trivial_inequality_removal,[],[f4827])).
% 7.51/1.73 thf(f5004,plain,(
% 7.51/1.73 ( ! [X2 : ($i > $i),X3 : $i,X0 : $i,X1 : $i,X6 : ($i > $i),X4 : $i,X5 : ($i > $i)] : (($true = ((c_In @ X0 @ (c_Power @ X1)))) | ($true = ((c_In @ (sK15 @ (X5 @ X4) @ (X6 @ X4)) @ (X2 @ X4)))) | (((X5 @ X3)) != X0) | (((X6 @ X3)) != X1) | (((X2 @ X3)) != X0)) ) | (~spl22_27 | ~spl22_40 | ~spl22_57)),
% 7.51/1.73 inference(beta-eta_normalization,[],[f5003])).
% 7.51/1.73 thf(f5071,plain,(
% 7.51/1.73 ( ! [X2 : ($i > $i),X3 : $i,X0 : $i,X1 : $i,X6 : ($i > $i),X4 : $i,X5 : ($i > $i)] : (($true = ((c_In @ X0 @ (c_Power @ X1)))) | ($true = ((c_In @ (sK15 @ (X5 @ X4) @ (X6 @ X4)) @ (X2 @ X4)))) | (((X5 @ X3)) != X0) | (((X6 @ X3)) != X1)) ) | (~spl22_27 | ~spl22_40 | ~spl22_57)),
% 7.51/1.73 inference(forward_subsumption_resolution,[],[f5004,f2971])).
% 7.51/1.73 thf(f5127,plain,(
% 7.51/1.73 ( ! [X2 : ($i > $i),X3 : $i,X0 : $i,X1 : $i,X6 : ($i > $i),X4 : $i,X5 : ($i > $i)] : (($true = ((c_In @ X0 @ (c_Power @ X1)))) | ($true = ((c_In @ (sK15 @ (X5 @ X4) @ (X6 @ X4)) @ (X2 @ X4)))) | (((X5 @ X3)) != X0)) ) | (~spl22_27 | ~spl22_40 | ~spl22_57)),
% 7.51/1.73 inference(forward_subsumption_resolution,[],[f5071,f2971])).
% 7.51/1.73 thf(f5182,plain,(
% 7.51/1.73 ( ! [X2 : ($i > $i),X0 : $i,X1 : $i,X6 : ($i > $i),X4 : $i,X5 : ($i > $i)] : (($true = ((c_In @ X0 @ (c_Power @ X1)))) | ($true = ((c_In @ (sK15 @ (X5 @ X4) @ (X6 @ X4)) @ (X2 @ X4))))) ) | (~spl22_27 | ~spl22_40 | ~spl22_57)),
% 7.51/1.73 inference(forward_subsumption_resolution,[],[f5127,f2971])).
% 7.51/1.73 thf(f5246,plain,(
% 7.51/1.73 ( ! [X2 : ($i > $i),X6 : ($i > $i),X4 : $i,X5 : ($i > $i)] : (($true = $false) | ($true = ((c_In @ (sK15 @ (X5 @ X4) @ (X6 @ X4)) @ (X2 @ X4))))) ) | (~spl22_21 | ~spl22_27 | ~spl22_34 | ~spl22_40 | ~spl22_57)),
% 7.51/1.73 inference(forward_demodulation,[],[f5182,f3014])).
% 7.51/1.73 thf(f5247,plain,(
% 7.51/1.73 ( ! [X2 : ($i > $i),X6 : ($i > $i),X4 : $i,X5 : ($i > $i)] : (($true = ((c_In @ (sK15 @ (X5 @ X4) @ (X6 @ X4)) @ (X2 @ X4))))) ) | (~spl22_21 | ~spl22_27 | ~spl22_34 | ~spl22_40 | ~spl22_57)),
% 7.51/1.73 inference(trivial_inequality_removal,[],[f5246])).
% 7.51/1.73 thf(f5266,plain,(
% 7.51/1.73 ($true = $false) | (~spl22_21 | ~spl22_27 | ~spl22_34 | ~spl22_40 | ~spl22_57)),
% 7.51/1.73 inference(forward_demodulation,[],[f5247,f3014])).
% 7.51/1.73 thf(f5267,plain,(
% 7.51/1.73 $false | (~spl22_21 | ~spl22_27 | ~spl22_34 | ~spl22_40 | ~spl22_57)),
% 7.51/1.73 inference(trivial_inequality_removal,[],[f5266])).
% 7.51/1.73 thf(f5268,plain,(
% 7.51/1.73 ~spl22_21 | ~spl22_27 | ~spl22_34 | ~spl22_40 | ~spl22_57),
% 7.51/1.73 inference(avatar_contradiction_clause,[],[f5267])).
% 7.51/1.73 thf(f5269,plain,(
% 7.51/1.73 spl22_57 | ~spl22_7),
% 7.51/1.73 inference(avatar_split_clause,[],[f3299,f794,f2970])).
% 7.51/1.73 cnf(s8, plain, spl22_7, inference(sat_conversion,[],[f797])).
% 7.51/1.73 cnf(s18, plain, spl22_8, inference(sat_conversion,[],[f827])).
% 7.51/1.73 cnf(s24, plain, spl22_1 | spl22_1 | spl22_21, inference(sat_conversion,[],[f860])).
% 7.51/1.73 cnf(s25, plain, spl22_1 | spl22_21, inference(rat,[],[s24])).
% 7.51/1.73 cnf(s31, plain, spl22_5, inference(sat_conversion,[],[f877])).
% 7.51/1.73 cnf(s33, plain, spl22_1 | spl22_27, inference(sat_conversion,[],[f885])).
% 7.51/1.73 cnf(s44, plain, spl22_20 | spl22_34, inference(sat_conversion,[],[f913])).
% 7.51/1.73 cnf(s48, plain, ~spl22_8 | ~spl22_20, inference(sat_conversion,[],[f918])).
% 7.51/1.73 cnf(s54, plain, ~spl22_5 | spl22_40, inference(sat_conversion,[],[f1472])).
% 7.51/1.73 cnf(s68, plain, ~spl22_1 | ~spl22_8, inference(sat_conversion,[],[f2645])).
% 7.51/1.73 cnf(s119, plain, ~spl22_21 | ~spl22_27 | ~spl22_34 | ~spl22_40 | ~spl22_57, inference(sat_conversion,[],[f5268])).
% 7.51/1.73 cnf(s120, plain, ~spl22_7 | spl22_57, inference(sat_conversion,[],[f5269])).
% 7.51/1.73 cnf(s162, plain, spl22_40, inference(rat,[],[s54,s31])).
% 7.51/1.73 cnf(s163, plain, ~spl22_1, inference(rat,[],[s68,s18])).
% 7.51/1.73 cnf(s164, plain, ~spl22_20, inference(rat,[],[s48,s18])).
% 7.51/1.73 cnf(s170, plain, spl22_27, inference(rat,[],[s33,s163])).
% 7.51/1.73 cnf(s175, plain, spl22_21, inference(rat,[],[s25,s163])).
% 7.51/1.73 cnf(s176, plain, spl22_34, inference(rat,[],[s44,s164])).
% 7.51/1.73 cnf(s178, plain, ~spl22_57, inference(rat,[],[s119,s170,s162,s176,s175])).
% 7.51/1.73 cnf(s180, plain, ~spl22_7, inference(rat,[],[s120,s178])).
% 7.51/1.73 cnf(s181, plain, $false, inference(rat,[],[s8,s180])).
% 7.51/1.73 thf(f5470,plain,(
% 7.51/1.73 $false),
% 7.51/1.73 inference(avatar_sat_refutation,[],[s181])).
% 7.51/1.73 % SZS output end Proof for theBenchmark
% 7.51/1.73 % (905857)------------------------------
% 7.51/1.73 % (905857)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.51/1.73 % (905857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.51/1.73 % (905857)CaDiCaL version: 2.1.3
% 7.51/1.73 % (905857)Termination reason: Refutation
% 7.51/1.73 % (905857)Time elapsed: 0.384 s
% 7.51/1.73 % (905857)Peak memory usage: 17 MB
% 7.51/1.73 % (905857)Instructions burned: 826 (million)
% 7.51/1.73 % (905804)Success in time 1.383 s
% 7.51/1.73 % Vampire exiting
%------------------------------------------------------------------------------