%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ITP111^2 : 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 : n018.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:10:44 AM UTC 2026
% Result : Theorem 4.16s 1.01s
% Output : Refutation 4.16s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ITP111^2 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.18 % Computer : n018.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Tue Sep 29 19:57:26 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.21 Running first-order model finding
% 0.08/0.21 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.16/0.99 % (564438)Will run a generic schedule for satisfiability detection.
% 4.16/0.99 % (564446)dis+10_1_sil=32000:sp=arity:random_seed=2922895168:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 4.16/0.99 % (564444)% WARNING: option uhcvi not known.
% 4.16/0.99 % (564445)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1469658393:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 4.16/0.99 % (564443)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1725832724_2999 on theBenchmark for (2999ds/0Mi)
% 4.16/0.99 % (564444)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1963753262:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 4.16/0.99 % (564447)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=324464338:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 4.16/0.99 % (564449)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1271733452:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 4.16/0.99 % (564444)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.16/0.99 % (564448)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1169019489:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 4.16/0.99 % (564447)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.16/0.99 % (564446)Instruction limit reached!
% 4.16/0.99 % (564446)------------------------------
% 4.16/0.99 % (564446)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.16/0.99 % (564446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.16/0.99 % (564446)CaDiCaL version: 2.1.3
% 4.16/0.99 % (564446)Termination reason: Instruction limit
% 4.16/0.99 % (564446)Termination phase: Saturation
% 4.16/0.99 % (564446)Time elapsed: 0.024 s
% 4.16/0.99 % (564446)Peak memory usage: 12 MB
% 4.16/0.99 % (564446)Instructions burned: 106 (million)
% 4.16/0.99 % (564457)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3657536376:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 4.16/0.99 % Exception at run slice level
% 4.16/0.99 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.16/0.99 % (564444)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 4.16/0.99 % Exception at run slice level
% 4.16/0.99 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.16/0.99 % (564459)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=540312520:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 4.16/0.99 % (564447)Instruction limit reached!
% 4.16/0.99 % (564447)------------------------------
% 4.16/0.99 % (564447)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.16/0.99 % (564447)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.16/0.99 % (564447)CaDiCaL version: 2.1.3
% 4.16/0.99 % (564447)Termination reason: Instruction limit
% 4.16/0.99 % (564447)Termination phase: Saturation
% 4.16/0.99 % (564447)Time elapsed: 0.051 s
% 4.16/0.99 % (564447)Peak memory usage: 13 MB
% 4.16/0.99 % (564447)Instructions burned: 118 (million)
% 4.16/0.99 % (564462)ott-21_1_sil=16000:fs=off:random_seed=736823721:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 4.16/0.99 % (564460)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=3718481141:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 4.16/0.99 % (564449)Instruction limit reached!
% 4.16/0.99 % (564449)------------------------------
% 4.16/0.99 % (564449)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.16/0.99 % (564449)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.16/0.99 % (564449)CaDiCaL version: 2.1.3
% 4.16/0.99 % (564449)Termination reason: Instruction limit
% 4.16/0.99 % (564449)Termination phase: Saturation
% 4.16/0.99 % (564449)Time elapsed: 0.071 s
% 4.16/0.99 % (564449)Peak memory usage: 14 MB
% 4.16/0.99 % (564449)Instructions burned: 159 (million)
% 4.16/0.99 % (564460)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.16/0.99 % (564460)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 4.16/0.99 % (564465)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1622779348:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 4.16/1.01 % (564462)Instruction limit reached!
% 4.16/1.01 % (564462)------------------------------
% 4.16/1.01 % (564462)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.16/1.01 % (564462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.16/1.01 % (564462)CaDiCaL version: 2.1.3
% 4.16/1.01 % (564462)Termination reason: Instruction limit
% 4.16/1.01 % (564462)Termination phase: Saturation
% 4.16/1.01 % (564462)Time elapsed: 0.042 s
% 4.16/1.01 % (564462)Peak memory usage: 13 MB
% 4.16/1.01 % (564462)Instructions burned: 183 (million)
% 4.16/1.01 % (564459)Instruction limit reached!
% 4.16/1.01 % (564459)------------------------------
% 4.16/1.01 % (564459)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.16/1.01 % (564459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.16/1.01 % (564459)CaDiCaL version: 2.1.3
% 4.16/1.01 % (564459)Termination reason: Instruction limit
% 4.16/1.01 % (564459)Termination phase: Saturation
% 4.16/1.01 % (564459)Time elapsed: 0.057 s
% 4.16/1.01 % (564459)Peak memory usage: 13 MB
% 4.16/1.01 % (564459)Instructions burned: 131 (million)
% 4.16/1.01 % (564448)Instruction limit reached!
% 4.16/1.01 % (564448)------------------------------
% 4.16/1.01 % (564448)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.16/1.01 % (564448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.16/1.01 % (564448)CaDiCaL version: 2.1.3
% 4.16/1.01 % (564448)Termination reason: Instruction limit
% 4.16/1.01 % (564448)Termination phase: Saturation
% 4.16/1.01 % (564448)Time elapsed: 0.107 s
% 4.16/1.01 % (564448)Peak memory usage: 13 MB
% 4.16/1.01 % (564448)Instructions burned: 132 (million)
% 4.16/1.01 % (564468)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2947368761:i=1179_2998 on theBenchmark for (2998ds/1179Mi)
% 4.16/1.01 % (564467)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=498486992:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 4.16/1.01 % (564469)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3385580662:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 4.16/1.01 % Exception at run slice level
% 4.16/1.01 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.16/1.01 % Exception at run slice level
% 4.16/1.01 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.16/1.01 % (564474)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3608327809:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi)
% 4.16/1.01 % (564474)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.16/1.01 % (564473)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=2376565667:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2998 on theBenchmark for (2998ds/692Mi)
% 4.16/1.01 % (564473)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.16/1.01 % (564465)Instruction limit reached!
% 4.16/1.01 % (564465)------------------------------
% 4.16/1.01 % (564465)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.16/1.01 % (564465)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.16/1.01 % (564465)CaDiCaL version: 2.1.3
% 4.16/1.01 % (564465)Termination reason: Instruction limit
% 4.16/1.01 % (564465)Termination phase: Saturation
% 4.16/1.01 % (564465)Time elapsed: 0.227 s
% 4.16/1.01 % (564465)Peak memory usage: 14 MB
% 4.16/1.01 % (564465)Instructions burned: 479 (million)
% 4.16/1.01 % (564477)fmb+10_1_sil=64000:random_seed=3913252621:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi)
% 4.16/1.01 % (564477)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 4.16/1.01 % Exception at run slice level
% 4.16/1.01 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.16/1.01 % (564479)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=788746224:i=9515:nm=5_2995 on theBenchmark for (2995ds/9515Mi)
% 4.16/1.01 % (564474)Instruction limit reached!
% 4.16/1.01 % (564474)------------------------------
% 4.16/1.01 % (564474)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.16/1.01 % (564474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.16/1.01 % (564474)CaDiCaL version: 2.1.3
% 4.16/1.01 % (564474)Termination reason: Instruction limit
% 4.16/1.01 % (564474)Termination phase: Saturation
% 4.16/1.01 % (564474)Time elapsed: 0.232 s
% 4.16/1.01 % (564474)Peak memory usage: 18 MB
% 4.16/1.01 % (564474)Instructions burned: 880 (million)
% 4.16/1.01 % (564481)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3011563701:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi)
% 4.16/1.01 % Exception at run slice level
% 4.16/1.01 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.16/1.01 % Exception at run slice level
% 4.16/1.01 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.16/1.01 % (564460)Instruction limit reached!
% 4.16/1.01 % (564460)------------------------------
% 4.16/1.01 % (564460)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.16/1.01 % (564460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.16/1.01 % (564460)CaDiCaL version: 2.1.3
% 4.16/1.01 % (564460)Termination reason: Instruction limit
% 4.16/1.01 % (564460)Termination phase: Saturation
% 4.16/1.01 % (564460)Time elapsed: 0.360 s
% 4.16/1.01 % (564460)Peak memory usage: 15 MB
% 4.16/1.01 % (564460)Instructions burned: 684 (million)
% 4.16/1.01 % (564483)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1517644901:i=5131_2995 on theBenchmark for (2995ds/5131Mi)
% 4.16/1.01 % (564483)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.16/1.01 % (564484)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=2535218678:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi)
% 4.16/1.01 % (564485)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1341904974:i=6324_2995 on theBenchmark for (2995ds/6324Mi)
% 4.16/1.01 % (564484)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 4.16/1.01 % (564484)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 4.16/1.01 % Exception at run slice level
% 4.16/1.01 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.16/1.01 % (564489)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1078733438:fmbsr=2.30978:i=2174_2994 on theBenchmark for (2994ds/2174Mi)
% 4.16/1.01 % Exception at run slice level
% 4.16/1.01 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.16/1.01 % (564491)ott-2_1_sil=16000:newcnf=on:random_seed=2788307985:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2994 on theBenchmark for (2994ds/869Mi)
% 4.16/1.01 % (564491)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.16/1.01 % (564468)Instruction limit reached!
% 4.16/1.01 % (564468)------------------------------
% 4.16/1.01 % (564468)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.16/1.01 % (564468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.16/1.01 % (564468)CaDiCaL version: 2.1.3
% 4.16/1.01 % (564468)Termination reason: Instruction limit
% 4.16/1.01 % (564468)Termination phase: Saturation
% 4.16/1.01 % (564468)Time elapsed: 0.539 s
% 4.16/1.01 % (564468)Peak memory usage: 18 MB
% 4.16/1.01 % (564468)Instructions burned: 1179 (million)
% 4.16/1.01 % (564473)Instruction limit reached!
% 4.16/1.01 % (564473)------------------------------
% 4.16/1.01 % (564473)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.16/1.01 % (564473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.16/1.01 % (564473)CaDiCaL version: 2.1.3
% 4.16/1.01 % (564473)Termination reason: Instruction limit
% 4.16/1.01 % (564473)Termination phase: Saturation
% 4.16/1.01 % (564473)Time elapsed: 0.504 s
% 4.16/1.01 % (564473)Peak memory usage: 17 MB
% 4.16/1.01 % (564473)Instructions burned: 694 (million)
% 4.16/1.01 % (564493)ott+10_1_sil=32000:tgt=ground:random_seed=1022324643:i=5114:av=off_2992 on theBenchmark for (2992ds/5114Mi)
% 4.16/1.01 % (564494)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3826428075:i=54282_2992 on theBenchmark for (2992ds/54282Mi)
% 4.16/1.01 % Exception at run slice level
% 4.16/1.01 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.16/1.01 % (564491) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-564438-564491"...
% 4.16/1.01 % (564491)...printing done.
% 4.16/1.01 % (564491)Refutation found. Thanks to Tanya!
% 4.16/1.01 % SZS status Theorem for theBenchmark
% 4.16/1.01 % SZS output start Proof for theBenchmark
% 4.16/1.01 thf(type_def_5, type, extended_ereal: $tType).
% 4.16/1.01 thf(type_def_6, type, real: $tType).
% 4.16/1.01 thf(type_def_7, type, set: $tType > $tType).
% 4.16/1.01 thf(type_def_8, type, a: $tType).
% 4.16/1.01 thf(type_def_9, type, sTfun: ($tType * $tType) > $tType).
% 4.16/1.01 thf(func_def_0, type, real_V2090557954_space: !>[X0: $tType]:($o)).
% 4.16/1.01 thf(func_def_1, type, type: !>[X0: $tType]:($o)).
% 4.16/1.01 thf(func_def_2, type, idom: !>[X0: $tType]:($o)).
% 4.16/1.01 thf(func_def_3, type, ring: !>[X0: $tType]:($o)).
% 4.16/1.01 thf(func_def_4, type, zero: !>[X0: $tType]:($o)).
% 4.16/1.01 thf(func_def_5, type, field: !>[X0: $tType]:($o)).
% 4.16/1.01 thf(func_def_6, type, uminus: !>[X0: $tType]:($o)).
% 4.16/1.01 thf(func_def_7, type, ord: !>[X0: $tType]:($o)).
% 4.16/1.01 thf(func_def_8, type, order: !>[X0: $tType]:($o)).
% 4.16/1.01 thf(func_def_9, type, mult_zero: !>[X0: $tType]:($o)).
% 4.16/1.01 thf(func_def_10, type, group_add: !>[X0: $tType]:($o)).
% 4.16/1.01 thf(func_def_11, type, no_bot: !>[X0: $tType]:($o)).
% 4.16/1.01 thf(func_def_12, type, no_top: !>[X0: $tType]:($o)).
% 4.16/1.01 thf(func_def_13, type, linorder: !>[X0: $tType]:($o)).
% 4.16/1.01 thf(func_def_14, type, preorder: !>[X0: $tType]:($o)).
% 4.16/1.01 thf(func_def_15, type, wellorder: !>[X0: $tType]:($o)).
% 4.16/1.01 thf(func_def_16, type, division_ring: !>[X0: $tType]:($o)).
% 4.16/1.01 thf(func_def_17, type, semidom_divide: !>[X0: $tType]:($o)).
% 4.16/1.01 thf(func_def_18, type, semigroup_mult: !>[X0: $tType]:($o)).
% 4.16/1.01 thf(func_def_19, type, dense_order: !>[X0: $tType]:($o)).
% 4.16/1.01 thf(func_def_20, type, linordered_idom: !>[X0: $tType]:($o)).
% 4.16/1.01 thf(func_def_21, type, linordered_ring: !>[X0: $tType]:($o)).
% 4.16/1.01 thf(func_def_22, type, linordered_field: !>[X0: $tType]:($o)).
% 4.16/1.01 thf(func_def_23, type, ab_semigroup_mult: !>[X0: $tType]:($o)).
% 4.16/1.01 thf(func_def_24, type, boolean_algebra: !>[X0: $tType]:($o)).
% 4.16/1.01 thf(func_def_25, type, ordered_ab_group_add: !>[X0: $tType]:($o)).
% 4.16/1.01 thf(func_def_26, type, topological_t0_space: !>[X0: $tType]:($o)).
% 4.16/1.01 thf(func_def_27, type, topological_t1_space: !>[X0: $tType]:($o)).
% 4.16/1.01 thf(func_def_28, type, linord581940658strict: !>[X0: $tType]:($o)).
% 4.16/1.01 thf(func_def_29, type, linord219039673up_add: !>[X0: $tType]:($o)).
% 4.16/1.01 thf(func_def_30, type, semiri1193490041visors: !>[X0: $tType]:($o)).
% 4.16/1.01 thf(func_def_31, type, linord20386208strict: !>[X0: $tType]:($o)).
% 4.16/1.01 thf(func_def_32, type, linord1659791738miring: !>[X0: $tType]:($o)).
% 4.16/1.01 thf(func_def_33, type, topolo2133971006pology: !>[X0: $tType]:($o)).
% 4.16/1.01 thf(func_def_34, type, topolo503727757_space: !>[X0: $tType]:($o)).
% 4.16/1.01 thf(func_def_35, type, canoni770627133id_add: !>[X0: $tType]:($o)).
% 4.16/1.01 thf(func_def_36, type, linord893533164strict: !>[X0: $tType]:($o)).
% 4.16/1.01 thf(func_def_37, type, semiri1923998003cancel: !>[X0: $tType]:($o)).
% 4.16/1.01 thf(func_def_38, type, euclid24285859cancel: !>[X0: $tType]:($o)).
% 4.16/1.01 thf(func_def_39, type, euclid191655569cancel: !>[X0: $tType]:($o)).
% 4.16/1.01 thf(func_def_40, type, condit1656338222tinuum: !>[X0: $tType]:($o)).
% 4.16/1.01 thf(func_def_41, type, extend1396239628finity: !>[X0: $tType]:(X0)).
% 4.16/1.01 thf(func_def_42, type, extended_MInfty: extended_ereal).
% 4.16/1.01 thf(func_def_43, type, extended_PInfty: extended_ereal).
% 4.16/1.01 thf(func_def_44, type, extended_rec_ereal: !>[X0: $tType]:(((real > X0) > X0 > X0 > extended_ereal > X0))).
% 4.16/1.01 thf(func_def_45, type, times_times: !>[X0: $tType]:((X0 > X0 > X0))).
% 4.16/1.01 thf(func_def_46, type, uminus_uminus: !>[X0: $tType]:((X0 > X0))).
% 4.16/1.01 thf(func_def_47, type, zero_zero: !>[X0: $tType]:(X0)).
% 4.16/1.01 thf(func_def_48, type, lower_582600101lsc_at: !>[X0: $tType, X1: $tType]:((X0 > (X0 > X1) > $o))).
% 4.16/1.01 thf(func_def_49, type, ord_less: !>[X0: $tType]:((X0 > X0 > $o))).
% 4.16/1.01 thf(func_def_50, type, divide_divide: !>[X0: $tType]:((X0 > X0 > X0))).
% 4.16/1.01 thf(func_def_51, type, collect: !>[X0: $tType]:(((X0 > $o) > set @ X0))).
% 4.16/1.01 thf(func_def_52, type, topolo1751647064n_open: !>[X0: $tType]:((set @ X0 > $o))).
% 4.16/1.01 thf(func_def_53, type, member: !>[X0: $tType]:((X0 > set @ X0 > $o))).
% 4.16/1.01 thf(func_def_54, type, f: (a > extended_ereal)).
% 4.16/1.01 thf(func_def_55, type, x0: a).
% 4.16/1.01 thf(func_def_57, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 4.16/1.01 thf(func_def_58, type, vIMP: ($o > $o > $o)).
% 4.16/1.01 thf(func_def_59, type, db0: !>[X0: $tType]:(X0)).
% 4.16/1.01 thf(func_def_60, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 4.16/1.01 thf(func_def_61, type, vAND: ($o > $o > $o)).
% 4.16/1.01 thf(func_def_62, type, db1: !>[X0: $tType]:(X0)).
% 4.16/1.01 thf(func_def_63, type, db2: !>[X0: $tType]:(X0)).
% 4.16/1.01 thf(func_def_64, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 4.16/1.01 thf(func_def_67, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 4.16/1.01 thf(func_def_68, type, vNOT: ($o > $o)).
% 4.16/1.01 thf(func_def_69, type, vOR: ($o > $o > $o)).
% 4.16/1.01 thf(func_def_70, type, sK0: !>[X0: $tType]:((X0 > X0 > set @ X0))).
% 4.16/1.01 thf(func_def_71, type, sK1: !>[X0: $tType]:((X0 > X0 > set @ X0))).
% 4.16/1.01 thf(func_def_72, type, sK2: !>[X0: $tType, X1: $tType]:((X1 > X0))).
% 4.16/1.01 thf(func_def_73, type, sK3: !>[X0: $tType]:((X0 > X0))).
% 4.16/1.01 thf(func_def_74, type, sK4: !>[X0: $tType]:((X0 > X0))).
% 4.16/1.01 thf(func_def_75, type, sK5: !>[X0: $tType]:((X0 > X0))).
% 4.16/1.01 thf(func_def_76, type, sK6: !>[X0: $tType]:((X0 > X0))).
% 4.16/1.01 thf(func_def_77, type, sK7: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > (X0 > $o) > (X0 > $o) > X0))).
% 4.16/1.01 thf(func_def_78, type, sK8: !>[X0: $tType]:((X0 > (X0 > $o) > (X0 > $o) > X0))).
% 4.16/1.01 thf(func_def_79, type, sK9: !>[X0: $tType]:((X0 > (X0 > $o) > (X0 > $o) > X0))).
% 4.16/1.01 thf(func_def_80, type, sK10: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > (X0 > $o) > (X0 > $o) > X0))).
% 4.16/1.01 thf(func_def_81, type, sK11: !>[X0: $tType]:((X0 > (X0 > $o) > (X0 > $o) > X0))).
% 4.16/1.01 thf(func_def_82, type, sK12: !>[X0: $tType]:((X0 > (X0 > $o) > (X0 > $o) > X0))).
% 4.16/1.01 thf(func_def_83, type, sK13: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > (X0 > $o) > (X0 > $o) > X0))).
% 4.16/1.01 thf(func_def_84, type, sK14: !>[X0: $tType]:((X0 > (X0 > $o) > (X0 > $o) > X0))).
% 4.16/1.01 thf(func_def_85, type, sK15: !>[X0: $tType]:((X0 > (X0 > $o) > (X0 > $o) > X0))).
% 4.16/1.01 thf(func_def_86, type, sK16: !>[X0: $tType]:((X0 > X0))).
% 4.16/1.01 thf(func_def_87, type, sK17: !>[X0: $tType]:((X0 > X0))).
% 4.16/1.01 thf(func_def_88, type, sK18: !>[X0: $tType]:((X0 > X0))).
% 4.16/1.01 thf(func_def_89, type, sK19: !>[X0: $tType]:((X0 > X0))).
% 4.16/1.01 thf(func_def_90, type, sK20: !>[X0: $tType, X1: $tType]:((X1 > X0))).
% 4.16/1.01 thf(func_def_91, type, sK21: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > (X0 > $o) > (X0 > $o) > X0))).
% 4.16/1.01 thf(func_def_92, type, sK22: !>[X0: $tType]:((X0 > (X0 > $o) > (X0 > $o) > X0))).
% 4.16/1.01 thf(func_def_93, type, sK23: !>[X0: $tType]:((X0 > (X0 > $o) > (X0 > $o) > X0))).
% 4.16/1.01 thf(func_def_94, type, sK24: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > X0))).
% 4.16/1.01 thf(func_def_95, type, sK25: !>[X0: $tType, X1: $tType]:(((X1 > X0) > (X1 > X0) > X1))).
% 4.16/1.01 thf(func_def_96, type, sK26: !>[X0: $tType]:((X0 > X0))).
% 4.16/1.01 thf(func_def_97, type, sK27: !>[X0: $tType, X1: $tType]:(((X1 > X0) > X1))).
% 4.16/1.01 thf(func_def_98, type, sK28: !>[X0: $tType, X1: $tType]:(((X1 > X0) > X1))).
% 4.16/1.01 thf(func_def_99, type, sK29: !>[X0: $tType, X1: $tType]:(((X0 > X1) > X0))).
% 4.16/1.01 thf(func_def_100, type, sK30: !>[X0: $tType, X1: $tType]:(((X0 > X1) > X0))).
% 4.16/1.01 thf(func_def_101, type, sK31: !>[X0: $tType, X1: $tType]:(((X1 > X0) > X1))).
% 4.16/1.01 thf(func_def_102, type, sK32: !>[X0: $tType, X1: $tType]:(((X1 > X0) > X1))).
% 4.16/1.01 thf(func_def_103, type, sK33: !>[X0: $tType, X1: $tType]:(((X0 > X1) > X0))).
% 4.16/1.01 thf(func_def_104, type, sK34: !>[X0: $tType, X1: $tType]:(((X0 > X1) > X0))).
% 4.16/1.01 thf(func_def_105, type, sK35: !>[X0: $tType]:((X0 > X0))).
% 4.16/1.01 thf(func_def_106, type, sK36: !>[X0: $tType]:((X0 > X0))).
% 4.16/1.01 thf(func_def_107, type, sK37: !>[X0: $tType]:((X0 > X0 > X0))).
% 4.16/1.01 thf(func_def_108, type, sK38: !>[X0: $tType]:(((X0 > $o) > X0))).
% 4.16/1.01 thf(func_def_109, type, sK39: !>[X0: $tType]:(((X0 > X0 > $o) > X0))).
% 4.16/1.01 thf(func_def_110, type, sK40: !>[X0: $tType]:(((X0 > X0 > $o) > X0))).
% 4.16/1.01 thf(func_def_111, type, sK41: !>[X0: $tType]:(((X0 > X0 > $o) > X0))).
% 4.16/1.01 thf(func_def_112, type, sK42: !>[X0: $tType]:(((X0 > X0 > $o) > X0))).
% 4.16/1.01 thf(func_def_113, type, sK43: !>[X0: $tType]:(((X0 > X0 > $o) > X0))).
% 4.16/1.01 thf(func_def_114, type, sK44: !>[X0: $tType]:((X0 > X0 > X0))).
% 4.16/1.01 thf(func_def_115, type, sK45: !>[X0: $tType]:((X0 > X0))).
% 4.16/1.01 thf(func_def_116, type, sK46: !>[X0: $tType]:((X0 > X0))).
% 4.16/1.01 thf(func_def_117, type, sK47: extended_ereal).
% 4.16/1.01 thf(func_def_118, type, sK48: (set @ a > a)).
% 4.16/1.01 thf(func_def_119, type, sK49: (extended_ereal > set @ a)).
% 4.16/1.01 thf(func_def_120, type, sK50: !>[X0: $tType]:((X0 > X0 > set @ X0))).
% 4.16/1.01 thf(func_def_121, type, sK51: !>[X0: $tType]:((X0 > X0 > set @ X0))).
% 4.16/1.01 thf(func_def_122, type, sK52: (extended_ereal > set @ a)).
% 4.16/1.01 thf(func_def_123, type, sK53: extended_ereal).
% 4.16/1.01 thf(func_def_124, type, sK54: (set @ a > a)).
% 4.16/1.01 thf(func_def_125, type, sK55: (extended_ereal > set @ a)).
% 4.16/1.01 thf(func_def_126, type, sK56: extended_ereal).
% 4.16/1.01 thf(func_def_127, type, sK57: (set @ a > a)).
% 4.16/1.01 thf(func_def_128, type, sK58: (extended_ereal > set @ a)).
% 4.16/1.01 thf(func_def_129, type, sK59: extended_ereal).
% 4.16/1.01 thf(func_def_130, type, sK60: (set @ a > a)).
% 4.16/1.01 thf(f1,axiom,(
% 4.16/1.01 (((f @ x0)) = extend1396239628finity @ extended_ereal) => (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = ! [X2 : extended_ereal] : ((ord_less @ extended_ereal @ X2 @ (f @ x0)) => ? [X3 : set @ a] : (! [X4 : a] : ((member @ a @ X4 @ X3) => (ord_less @ extended_ereal @ X2 @ (f @ X4))) & (member @ a @ x0 @ X3) & (topolo1751647064n_open @ a @ X3))))),
% 4.16/1.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0__092_060open_062f_Ax0_A_061_A_092_060infinity_062_A_092_060Longrightarrow_062_Alsc__at_Ax0_Af_A_061_A_I_092_060forall_062C_060f_Ax0_O_A_092_060exists_062T_O_Aopen_AT_A_092_060and_062_Ax0_A_092_060in_062_AT_A_092_060and_062_A_I_092_060forall_062y_092_060in_062T_O_AC_A_060_Af_Ay_J_J_092_060close_062)).
% 4.16/1.01 thf(f2,axiom,(
% 4.16/1.01 (((f @ x0)) = ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) => (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = ! [X0 : extended_ereal] : ((ord_less @ extended_ereal @ X0 @ (f @ x0)) => ? [X1 : set @ a] : (! [X2 : a] : ((member @ a @ X2 @ X1) => (ord_less @ extended_ereal @ X0 @ (f @ X2))) & (member @ a @ x0 @ X1) & (topolo1751647064n_open @ a @ X1))))),
% 4.16/1.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1__092_060open_062f_Ax0_A_061_A_N_A_092_060infinity_062_A_092_060Longrightarrow_062_Alsc__at_Ax0_Af_A_061_A_I_092_060forall_062C_060f_Ax0_O_A_092_060exists_062T_O_Aopen_AT_A_092_060and_062_Ax0_A_092_060in_062_AT_A_092_060and_062_A_I_092_060forall_062y_092_060in_062T_O_AC_A_060_Af_Ay_J_J_092_060close_062)).
% 4.16/1.01 thf(f3,axiom,(
% 4.16/1.01 (((f @ x0)) != ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) => ((((f @ x0)) != extend1396239628finity @ extended_ereal) => (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = ! [X0 : extended_ereal] : ((ord_less @ extended_ereal @ X0 @ (f @ x0)) => ? [X1 : set @ a] : (! [X2 : a] : ((member @ a @ X2 @ X1) => (ord_less @ extended_ereal @ X0 @ (f @ X2))) & (member @ a @ x0 @ X1) & (topolo1751647064n_open @ a @ X1)))))),
% 4.16/1.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2__092_060open_062_092_060lbrakk_062f_Ax0_A_092_060noteq_062_A_N_A_092_060infinity_062_059_Af_Ax0_A_092_060noteq_062_A_092_060infinity_062_092_060rbrakk_062_A_092_060Longrightarrow_062_Alsc__at_Ax0_Af_A_061_A_I_092_060forall_062C_060f_Ax0_O_A_092_060exists_062T_O_Aopen_AT_A_092_060and_062_Ax0_A_092_060in_062_AT_A_092_060and_062_A_I_092_060forall_062y_092_060in_062T_O_AC_A_060_Af_Ay_J_J_092_060close_062)).
% 4.16/1.01 thf(f30,axiom,(
% 4.16/1.01 ! [X0 : extended_ereal] : ~(ord_less @ extended_ereal @ X0 @ (uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))),
% 4.16/1.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_29_less__ereal_Osimps_I3_J)).
% 4.16/1.01 thf(f57,axiom,(
% 4.16/1.01 (extended_MInfty = ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal)))),
% 4.16/1.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_56_MInfty__eq__minfinity)).
% 4.16/1.01 thf(f298,conjecture,(
% 4.16/1.01 (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) != ~ ! [X0 : extended_ereal] : ((ord_less @ extended_ereal @ X0 @ (f @ x0)) => ? [X1 : set @ a] : (! [X2 : a] : ((member @ a @ X2 @ X1) => (ord_less @ extended_ereal @ X0 @ (f @ X2))) & (member @ a @ x0 @ X1) & (topolo1751647064n_open @ a @ X1))))),
% 4.16/1.01 file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0)).
% 4.16/1.01 thf(f299,negated_conjecture,(
% 4.16/1.01 ~ (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) != ~ ! [X0 : extended_ereal] : ((ord_less @ extended_ereal @ X0 @ (f @ x0)) => ? [X1 : set @ a] : (! [X2 : a] : ((member @ a @ X2 @ X1) => (ord_less @ extended_ereal @ X0 @ (f @ X2))) & (member @ a @ x0 @ X1) & (topolo1751647064n_open @ a @ X1))))),
% 4.16/1.01 inference(negated_conjecture,[status(cth)],[f298])).
% 4.16/1.01 thf(f300,plain,(
% 4.16/1.01 (((f @ x0)) = extend1396239628finity @ extended_ereal) => (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = ! [X0 : extended_ereal] : ((ord_less @ extended_ereal @ X0 @ (f @ x0)) => ? [X1 : set @ a] : (! [X2 : a] : ((member @ a @ X2 @ X1) => (ord_less @ extended_ereal @ X0 @ (f @ X2))) & (member @ a @ x0 @ X1) & (topolo1751647064n_open @ a @ X1))))),
% 4.16/1.01 inference(rectify,[],[f1])).
% 4.16/1.01 thf(f301,plain,(
% 4.16/1.01 (((f @ x0)) = extend1396239628finity @ extended_ereal) => (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = ((!! @ extended_ereal @ (^[Y0 : extended_ereal]: ((ord_less @ extended_ereal @ Y0 @ (f @ x0)) => (?? @ set @ a @ (^[Y1 : set @ a]: (((topolo1751647064n_open @ a @ Y1) & (member @ a @ x0 @ Y1)) & (!! @ a @ (^[Y2 : a]: ((member @ a @ Y2 @ Y1) => (ord_less @ extended_ereal @ Y0 @ (f @ Y2)))))))))))))),
% 4.16/1.01 inference(fool_elimination,[],[f300])).
% 4.16/1.01 thf(f302,plain,(
% 4.16/1.01 (((f @ x0)) = ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) => (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = ! [X0 : extended_ereal] : ((ord_less @ extended_ereal @ X0 @ (f @ x0)) => ? [X1 : set @ a] : (! [X2 : a] : ((member @ a @ X2 @ X1) => (ord_less @ extended_ereal @ X0 @ (f @ X2))) & (member @ a @ x0 @ X1) & (topolo1751647064n_open @ a @ X1))))),
% 4.16/1.01 inference(rectify,[],[f2])).
% 4.16/1.01 thf(f303,plain,(
% 4.16/1.01 (((f @ x0)) = ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) => (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = ((!! @ extended_ereal @ (^[Y0 : extended_ereal]: ((ord_less @ extended_ereal @ Y0 @ (f @ x0)) => (?? @ set @ a @ (^[Y1 : set @ a]: (((topolo1751647064n_open @ a @ Y1) & (member @ a @ x0 @ Y1)) & (!! @ a @ (^[Y2 : a]: ((member @ a @ Y2 @ Y1) => (ord_less @ extended_ereal @ Y0 @ (f @ Y2)))))))))))))),
% 4.16/1.01 inference(fool_elimination,[],[f302])).
% 4.16/1.01 thf(f304,plain,(
% 4.16/1.01 (((f @ x0)) != ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) => ((((f @ x0)) != extend1396239628finity @ extended_ereal) => (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = ! [X0 : extended_ereal] : ((ord_less @ extended_ereal @ X0 @ (f @ x0)) => ? [X1 : set @ a] : (! [X2 : a] : ((member @ a @ X2 @ X1) => (ord_less @ extended_ereal @ X0 @ (f @ X2))) & (member @ a @ x0 @ X1) & (topolo1751647064n_open @ a @ X1)))))),
% 4.16/1.01 inference(rectify,[],[f3])).
% 4.16/1.01 thf(f305,plain,(
% 4.16/1.01 (((f @ x0)) != ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) => ((((f @ x0)) != extend1396239628finity @ extended_ereal) => (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = ((!! @ extended_ereal @ (^[Y0 : extended_ereal]: ((ord_less @ extended_ereal @ Y0 @ (f @ x0)) => (?? @ set @ a @ (^[Y1 : set @ a]: (((topolo1751647064n_open @ a @ Y1) & (member @ a @ x0 @ Y1)) & (!! @ a @ (^[Y2 : a]: ((member @ a @ Y2 @ Y1) => (ord_less @ extended_ereal @ Y0 @ (f @ Y2))))))))))))))),
% 4.16/1.01 inference(fool_elimination,[],[f304])).
% 4.16/1.01 thf(f354,plain,(
% 4.16/1.01 ! [X0 : extended_ereal] : ~(ord_less @ extended_ereal @ X0 @ (uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))),
% 4.16/1.01 inference(rectify,[],[f30])).
% 4.16/1.01 thf(f355,plain,(
% 4.16/1.01 ! [X0 : extended_ereal] : ~ (((ord_less @ extended_ereal @ X0 @ (uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) = $true)),
% 4.16/1.01 inference(fool_elimination,[],[f354])).
% 4.16/1.01 thf(f818,plain,(
% 4.16/1.01 ~ (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) != ~ ! [X0 : extended_ereal] : ((ord_less @ extended_ereal @ X0 @ (f @ x0)) => ? [X1 : set @ a] : (! [X2 : a] : ((member @ a @ X2 @ X1) => (ord_less @ extended_ereal @ X0 @ (f @ X2))) & (member @ a @ x0 @ X1) & (topolo1751647064n_open @ a @ X1))))),
% 4.16/1.01 inference(rectify,[],[f299])).
% 4.16/1.01 thf(f819,plain,(
% 4.16/1.01 ~ (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) != ((~ (!! @ extended_ereal @ (^[Y0 : extended_ereal]: ((ord_less @ extended_ereal @ Y0 @ (f @ x0)) => (?? @ set @ a @ (^[Y1 : set @ a]: (((topolo1751647064n_open @ a @ Y1) & (member @ a @ x0 @ Y1)) & (!! @ a @ (^[Y2 : a]: ((member @ a @ Y2 @ Y1) => (ord_less @ extended_ereal @ Y0 @ (f @ Y2))))))))))))))),
% 4.16/1.01 inference(fool_elimination,[],[f818])).
% 4.16/1.01 thf(f823,plain,(
% 4.16/1.01 ! [X0 : extended_ereal] : (((ord_less @ extended_ereal @ X0 @ (uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) != $true)),
% 4.16/1.01 inference(flattening,[],[f355])).
% 4.16/1.01 thf(f843,plain,(
% 4.16/1.01 (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = ((~ (!! @ extended_ereal @ (^[Y0 : extended_ereal]: ((ord_less @ extended_ereal @ Y0 @ (f @ x0)) => (?? @ set @ a @ (^[Y1 : set @ a]: (((topolo1751647064n_open @ a @ Y1) & (member @ a @ x0 @ Y1)) & (!! @ a @ (^[Y2 : a]: ((member @ a @ Y2 @ Y1) => (ord_less @ extended_ereal @ Y0 @ (f @ Y2))))))))))))))),
% 4.16/1.01 inference(flattening,[],[f819])).
% 4.16/1.01 thf(f844,plain,(
% 4.16/1.01 (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = ((!! @ extended_ereal @ (^[Y0 : extended_ereal]: ((ord_less @ extended_ereal @ Y0 @ (f @ x0)) => (?? @ set @ a @ (^[Y1 : set @ a]: (((topolo1751647064n_open @ a @ Y1) & (member @ a @ x0 @ Y1)) & (!! @ a @ (^[Y2 : a]: ((member @ a @ Y2 @ Y1) => (ord_less @ extended_ereal @ Y0 @ (f @ Y2))))))))))))) | (((f @ x0)) != extend1396239628finity @ extended_ereal)),
% 4.16/1.01 inference(ennf_transformation,[],[f301])).
% 4.16/1.01 thf(f845,plain,(
% 4.16/1.01 (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = ((!! @ extended_ereal @ (^[Y0 : extended_ereal]: ((ord_less @ extended_ereal @ Y0 @ (f @ x0)) => (?? @ set @ a @ (^[Y1 : set @ a]: (((topolo1751647064n_open @ a @ Y1) & (member @ a @ x0 @ Y1)) & (!! @ a @ (^[Y2 : a]: ((member @ a @ Y2 @ Y1) => (ord_less @ extended_ereal @ Y0 @ (f @ Y2))))))))))))) | (((f @ x0)) != ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal)))),
% 4.16/1.01 inference(ennf_transformation,[],[f303])).
% 4.16/1.01 thf(f846,plain,(
% 4.16/1.01 ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = ((!! @ extended_ereal @ (^[Y0 : extended_ereal]: ((ord_less @ extended_ereal @ Y0 @ (f @ x0)) => (?? @ set @ a @ (^[Y1 : set @ a]: (((topolo1751647064n_open @ a @ Y1) & (member @ a @ x0 @ Y1)) & (!! @ a @ (^[Y2 : a]: ((member @ a @ Y2 @ Y1) => (ord_less @ extended_ereal @ Y0 @ (f @ Y2))))))))))))) | (((f @ x0)) = extend1396239628finity @ extended_ereal)) | (((f @ x0)) = ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal)))),
% 4.16/1.01 inference(ennf_transformation,[],[f305])).
% 4.16/1.01 thf(f847,plain,(
% 4.16/1.01 (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = ((!! @ extended_ereal @ (^[Y0 : extended_ereal]: ((ord_less @ extended_ereal @ Y0 @ (f @ x0)) => (?? @ set @ a @ (^[Y1 : set @ a]: (((topolo1751647064n_open @ a @ Y1) & (member @ a @ x0 @ Y1)) & (!! @ a @ (^[Y2 : a]: ((member @ a @ Y2 @ Y1) => (ord_less @ extended_ereal @ Y0 @ (f @ Y2))))))))))))) | (((f @ x0)) = extend1396239628finity @ extended_ereal) | (((f @ x0)) = ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal)))),
% 4.16/1.01 inference(flattening,[],[f846])).
% 4.16/1.01 thf(f1160,plain,(
% 4.16/1.01 (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = ((!! @ extended_ereal @ (^[Y0 : extended_ereal]: ((ord_less @ extended_ereal @ Y0 @ (f @ x0)) => (?? @ set @ a @ (^[Y1 : set @ a]: (((topolo1751647064n_open @ a @ Y1) & (member @ a @ x0 @ Y1)) & (!! @ a @ (^[Y2 : a]: ((member @ a @ Y2 @ Y1) => (ord_less @ extended_ereal @ Y0 @ (f @ Y2))))))))))))) | (((f @ x0)) != extend1396239628finity @ extended_ereal)),
% 4.16/1.01 inference(cnf_transformation,[],[f844])).
% 4.16/1.01 thf(f1161,plain,(
% 4.16/1.01 (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = ((!! @ extended_ereal @ (^[Y0 : extended_ereal]: ((ord_less @ extended_ereal @ Y0 @ (f @ x0)) => (?? @ set @ a @ (^[Y1 : set @ a]: (((topolo1751647064n_open @ a @ Y1) & (member @ a @ x0 @ Y1)) & (!! @ a @ (^[Y2 : a]: ((member @ a @ Y2 @ Y1) => (ord_less @ extended_ereal @ Y0 @ (f @ Y2))))))))))))) | (((f @ x0)) != ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal)))),
% 4.16/1.01 inference(cnf_transformation,[],[f845])).
% 4.16/1.01 thf(f1162,plain,(
% 4.16/1.01 (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = ((!! @ extended_ereal @ (^[Y0 : extended_ereal]: ((ord_less @ extended_ereal @ Y0 @ (f @ x0)) => (?? @ set @ a @ (^[Y1 : set @ a]: (((topolo1751647064n_open @ a @ Y1) & (member @ a @ x0 @ Y1)) & (!! @ a @ (^[Y2 : a]: ((member @ a @ Y2 @ Y1) => (ord_less @ extended_ereal @ Y0 @ (f @ Y2))))))))))))) | (((f @ x0)) = extend1396239628finity @ extended_ereal) | (((f @ x0)) = ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal)))),
% 4.16/1.01 inference(cnf_transformation,[],[f847])).
% 4.16/1.01 thf(f1204,plain,(
% 4.16/1.01 ( ! [X0 : extended_ereal] : ((((ord_less @ extended_ereal @ X0 @ (uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) != $true)) )),
% 4.16/1.01 inference(cnf_transformation,[],[f823])).
% 4.16/1.01 thf(f1231,plain,(
% 4.16/1.01 (((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal)) = extended_MInfty)),
% 4.16/1.01 inference(cnf_transformation,[],[f57])).
% 4.16/1.01 thf(f1492,plain,(
% 4.16/1.01 (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = ((~ (!! @ extended_ereal @ (^[Y0 : extended_ereal]: ((ord_less @ extended_ereal @ Y0 @ (f @ x0)) => (?? @ set @ a @ (^[Y1 : set @ a]: (((topolo1751647064n_open @ a @ Y1) & (member @ a @ x0 @ Y1)) & (!! @ a @ (^[Y2 : a]: ((member @ a @ Y2 @ Y1) => (ord_less @ extended_ereal @ Y0 @ (f @ Y2))))))))))))))),
% 4.16/1.01 inference(cnf_transformation,[],[f843])).
% 4.16/1.01 thf(f1528,plain,(
% 4.16/1.01 (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | (((~ (!! @ extended_ereal @ (^[Y0 : extended_ereal]: ((ord_less @ extended_ereal @ Y0 @ (f @ x0)) => (?? @ set @ a @ (^[Y1 : set @ a]: (((topolo1751647064n_open @ a @ Y1) & (member @ a @ x0 @ Y1)) & (!! @ a @ (^[Y2 : a]: ((member @ a @ Y2 @ Y1) => (ord_less @ extended_ereal @ Y0 @ (f @ Y2))))))))))))) = $false)),
% 4.16/1.01 inference(iff_proxy_clausification,[],[f1492])).
% 4.16/1.01 thf(f1529,plain,(
% 4.16/1.01 (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $false) | ($true = ((~ (!! @ extended_ereal @ (^[Y0 : extended_ereal]: ((ord_less @ extended_ereal @ Y0 @ (f @ x0)) => (?? @ set @ a @ (^[Y1 : set @ a]: (((topolo1751647064n_open @ a @ Y1) & (member @ a @ x0 @ Y1)) & (!! @ a @ (^[Y2 : a]: ((member @ a @ Y2 @ Y1) => (ord_less @ extended_ereal @ Y0 @ (f @ Y2))))))))))))))),
% 4.16/1.01 inference(iff_proxy_clausification,[],[f1492])).
% 4.16/1.01 thf(f1530,plain,(
% 4.16/1.01 (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $false) | (((!! @ extended_ereal @ (^[Y0 : extended_ereal]: ((ord_less @ extended_ereal @ Y0 @ (f @ x0)) => (?? @ set @ a @ (^[Y1 : set @ a]: (((topolo1751647064n_open @ a @ Y1) & (member @ a @ x0 @ Y1)) & (!! @ a @ (^[Y2 : a]: ((member @ a @ Y2 @ Y1) => (ord_less @ extended_ereal @ Y0 @ (f @ Y2)))))))))))) = $false)),
% 4.16/1.01 inference(not_proxy_clausification,[],[f1529])).
% 4.16/1.01 thf(f1531,plain,(
% 4.16/1.01 (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $false) | ($false = (((^[Y0 : extended_ereal]: ((ord_less @ extended_ereal @ Y0 @ (f @ x0)) => (?? @ set @ a @ (^[Y1 : set @ a]: (((topolo1751647064n_open @ a @ Y1) & (member @ a @ x0 @ Y1)) & (!! @ a @ (^[Y2 : a]: ((member @ a @ Y2 @ Y1) => (ord_less @ extended_ereal @ Y0 @ (f @ Y2)))))))))) @ sK47)))),
% 4.16/1.01 inference(sigma_proxy_clausification,[],[f1530])).
% 4.16/1.01 thf(f1532,plain,(
% 4.16/1.01 (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $false) | ($false = (((ord_less @ extended_ereal @ sK47 @ (f @ x0)) => (?? @ set @ a @ (^[Y0 : set @ a]: (((topolo1751647064n_open @ a @ Y0) & (member @ a @ x0 @ Y0)) & (!! @ a @ (^[Y1 : a]: ((member @ a @ Y1 @ Y0) => (ord_less @ extended_ereal @ sK47 @ (f @ Y1)))))))))))),
% 4.16/1.01 inference(beta-eta_normalization,[],[f1531])).
% 4.16/1.01 thf(f1533,plain,(
% 4.16/1.01 (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $false) | ($false = ((?? @ set @ a @ (^[Y0 : set @ a]: (((topolo1751647064n_open @ a @ Y0) & (member @ a @ x0 @ Y0)) & (!! @ a @ (^[Y1 : a]: ((member @ a @ Y1 @ Y0) => (ord_less @ extended_ereal @ sK47 @ (f @ Y1))))))))))),
% 4.16/1.01 inference(imp_proxy_clausification,[],[f1532])).
% 4.16/1.01 thf(f1534,plain,(
% 4.16/1.01 (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $false) | ($true = ((ord_less @ extended_ereal @ sK47 @ (f @ x0))))),
% 4.16/1.01 inference(imp_proxy_clausification,[],[f1532])).
% 4.16/1.01 thf(f1535,plain,(
% 4.16/1.01 ( ! [X1 : set @ a] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $false) | ($false = (((^[Y0 : set @ a]: (((topolo1751647064n_open @ a @ Y0) & (member @ a @ x0 @ Y0)) & (!! @ a @ (^[Y1 : a]: ((member @ a @ Y1 @ Y0) => (ord_less @ extended_ereal @ sK47 @ (f @ Y1))))))) @ X1)))) )),
% 4.16/1.01 inference(pi_proxy_clausification,[],[f1533])).
% 4.16/1.01 thf(f1536,plain,(
% 4.16/1.01 ( ! [X1 : set @ a] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $false) | ($false = ((((topolo1751647064n_open @ a @ X1) & (member @ a @ x0 @ X1)) & (!! @ a @ (^[Y0 : a]: ((member @ a @ Y0 @ X1) => (ord_less @ extended_ereal @ sK47 @ (f @ Y0))))))))) )),
% 4.16/1.01 inference(beta-eta_normalization,[],[f1535])).
% 4.16/1.01 thf(f1537,plain,(
% 4.16/1.01 ( ! [X1 : set @ a] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $false) | ($false = ((!! @ a @ (^[Y0 : a]: ((member @ a @ Y0 @ X1) => (ord_less @ extended_ereal @ sK47 @ (f @ Y0))))))) | ($false = (((topolo1751647064n_open @ a @ X1) & (member @ a @ x0 @ X1))))) )),
% 4.16/1.01 inference(and_proxy_clausification,[],[f1536])).
% 4.16/1.01 thf(f1538,plain,(
% 4.16/1.01 ( ! [X1 : set @ a] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $false) | ($false = (((^[Y0 : a]: ((member @ a @ Y0 @ X1) => (ord_less @ extended_ereal @ sK47 @ (f @ Y0)))) @ (sK48 @ X1)))) | ($false = (((topolo1751647064n_open @ a @ X1) & (member @ a @ x0 @ X1))))) )),
% 4.16/1.01 inference(sigma_proxy_clausification,[],[f1537])).
% 4.16/1.01 thf(f1539,plain,(
% 4.16/1.01 ( ! [X1 : set @ a] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $false) | ($false = (((^[Y0 : a]: ((member @ a @ Y0 @ X1) => (ord_less @ extended_ereal @ sK47 @ (f @ Y0)))) @ (sK48 @ X1)))) | (((member @ a @ x0 @ X1)) = $false) | (((topolo1751647064n_open @ a @ X1)) = $false)) )),
% 4.16/1.01 inference(and_proxy_clausification,[],[f1538])).
% 4.16/1.01 thf(f1540,plain,(
% 4.16/1.01 ( ! [X1 : set @ a] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $false) | ($false = (((member @ a @ (sK48 @ X1) @ X1) => (ord_less @ extended_ereal @ sK47 @ (f @ (sK48 @ X1)))))) | (((member @ a @ x0 @ X1)) = $false) | (((topolo1751647064n_open @ a @ X1)) = $false)) )),
% 4.16/1.01 inference(beta-eta_normalization,[],[f1539])).
% 4.16/1.01 thf(f1541,plain,(
% 4.16/1.01 ( ! [X1 : set @ a] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $false) | ($false = ((ord_less @ extended_ereal @ sK47 @ (f @ (sK48 @ X1))))) | (((member @ a @ x0 @ X1)) = $false) | (((topolo1751647064n_open @ a @ X1)) = $false)) )),
% 4.16/1.01 inference(imp_proxy_clausification,[],[f1540])).
% 4.16/1.01 thf(f1542,plain,(
% 4.16/1.01 ( ! [X1 : set @ a] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $false) | ($true = ((member @ a @ (sK48 @ X1) @ X1))) | (((member @ a @ x0 @ X1)) = $false) | (((topolo1751647064n_open @ a @ X1)) = $false)) )),
% 4.16/1.01 inference(imp_proxy_clausification,[],[f1540])).
% 4.16/1.01 thf(f1543,plain,(
% 4.16/1.01 (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | (((!! @ extended_ereal @ (^[Y0 : extended_ereal]: ((ord_less @ extended_ereal @ Y0 @ (f @ x0)) => (?? @ set @ a @ (^[Y1 : set @ a]: (((topolo1751647064n_open @ a @ Y1) & (member @ a @ x0 @ Y1)) & (!! @ a @ (^[Y2 : a]: ((member @ a @ Y2 @ Y1) => (ord_less @ extended_ereal @ Y0 @ (f @ Y2)))))))))))) = $true)),
% 4.16/1.01 inference(not_proxy_clausification,[],[f1528])).
% 4.16/1.01 thf(f1544,plain,(
% 4.16/1.01 ( ! [X1 : extended_ereal] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | ($true = (((^[Y0 : extended_ereal]: ((ord_less @ extended_ereal @ Y0 @ (f @ x0)) => (?? @ set @ a @ (^[Y1 : set @ a]: (((topolo1751647064n_open @ a @ Y1) & (member @ a @ x0 @ Y1)) & (!! @ a @ (^[Y2 : a]: ((member @ a @ Y2 @ Y1) => (ord_less @ extended_ereal @ Y0 @ (f @ Y2)))))))))) @ X1)))) )),
% 4.16/1.01 inference(pi_proxy_clausification,[],[f1543])).
% 4.16/1.01 thf(f1545,plain,(
% 4.16/1.01 ( ! [X1 : extended_ereal] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | ($true = (((ord_less @ extended_ereal @ X1 @ (f @ x0)) => (?? @ set @ a @ (^[Y0 : set @ a]: (((topolo1751647064n_open @ a @ Y0) & (member @ a @ x0 @ Y0)) & (!! @ a @ (^[Y1 : a]: ((member @ a @ Y1 @ Y0) => (ord_less @ extended_ereal @ X1 @ (f @ Y1)))))))))))) )),
% 4.16/1.01 inference(beta-eta_normalization,[],[f1544])).
% 4.16/1.01 thf(f1546,plain,(
% 4.16/1.01 ( ! [X1 : extended_ereal] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | ($false = ((ord_less @ extended_ereal @ X1 @ (f @ x0)))) | ($true = ((?? @ set @ a @ (^[Y0 : set @ a]: (((topolo1751647064n_open @ a @ Y0) & (member @ a @ x0 @ Y0)) & (!! @ a @ (^[Y1 : a]: ((member @ a @ Y1 @ Y0) => (ord_less @ extended_ereal @ X1 @ (f @ Y1))))))))))) )),
% 4.16/1.01 inference(imp_proxy_clausification,[],[f1545])).
% 4.16/1.01 thf(f1547,plain,(
% 4.16/1.01 ( ! [X1 : extended_ereal] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | ($false = ((ord_less @ extended_ereal @ X1 @ (f @ x0)))) | ($true = (((^[Y0 : set @ a]: (((topolo1751647064n_open @ a @ Y0) & (member @ a @ x0 @ Y0)) & (!! @ a @ (^[Y1 : a]: ((member @ a @ Y1 @ Y0) => (ord_less @ extended_ereal @ X1 @ (f @ Y1))))))) @ (sK49 @ X1))))) )),
% 4.16/1.01 inference(sigma_proxy_clausification,[],[f1546])).
% 4.16/1.01 thf(f1548,plain,(
% 4.16/1.01 ( ! [X1 : extended_ereal] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | ($false = ((ord_less @ extended_ereal @ X1 @ (f @ x0)))) | ($true = ((((topolo1751647064n_open @ a @ (sK49 @ X1)) & (member @ a @ x0 @ (sK49 @ X1))) & (!! @ a @ (^[Y0 : a]: ((member @ a @ Y0 @ (sK49 @ X1)) => (ord_less @ extended_ereal @ X1 @ (f @ Y0))))))))) )),
% 4.16/1.01 inference(beta-eta_normalization,[],[f1547])).
% 4.16/1.01 thf(f1549,plain,(
% 4.16/1.01 ( ! [X1 : extended_ereal] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | ($false = ((ord_less @ extended_ereal @ X1 @ (f @ x0)))) | ($true = ((!! @ a @ (^[Y0 : a]: ((member @ a @ Y0 @ (sK49 @ X1)) => (ord_less @ extended_ereal @ X1 @ (f @ Y0)))))))) )),
% 4.16/1.01 inference(and_proxy_clausification,[],[f1548])).
% 4.16/1.01 thf(f1550,plain,(
% 4.16/1.01 ( ! [X1 : extended_ereal] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | ($false = ((ord_less @ extended_ereal @ X1 @ (f @ x0)))) | ($true = (((topolo1751647064n_open @ a @ (sK49 @ X1)) & (member @ a @ x0 @ (sK49 @ X1)))))) )),
% 4.16/1.01 inference(and_proxy_clausification,[],[f1548])).
% 4.16/1.01 thf(f1551,plain,(
% 4.16/1.01 ( ! [X1 : extended_ereal] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | ($false = ((ord_less @ extended_ereal @ X1 @ (f @ x0)))) | ($true = ((member @ a @ x0 @ (sK49 @ X1))))) )),
% 4.16/1.01 inference(and_proxy_clausification,[],[f1550])).
% 4.16/1.01 thf(f1552,plain,(
% 4.16/1.01 ( ! [X1 : extended_ereal] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | ($false = ((ord_less @ extended_ereal @ X1 @ (f @ x0)))) | ($true = ((topolo1751647064n_open @ a @ (sK49 @ X1))))) )),
% 4.16/1.01 inference(and_proxy_clausification,[],[f1550])).
% 4.16/1.01 thf(f1553,plain,(
% 4.16/1.01 ( ! [X2 : a,X1 : extended_ereal] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | ($false = ((ord_less @ extended_ereal @ X1 @ (f @ x0)))) | ($true = (((^[Y0 : a]: ((member @ a @ Y0 @ (sK49 @ X1)) => (ord_less @ extended_ereal @ X1 @ (f @ Y0)))) @ X2)))) )),
% 4.16/1.01 inference(pi_proxy_clausification,[],[f1549])).
% 4.16/1.01 thf(f1554,plain,(
% 4.16/1.01 ( ! [X2 : a,X1 : extended_ereal] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | ($false = ((ord_less @ extended_ereal @ X1 @ (f @ x0)))) | ($true = (((member @ a @ X2 @ (sK49 @ X1)) => (ord_less @ extended_ereal @ X1 @ (f @ X2)))))) )),
% 4.16/1.01 inference(beta-eta_normalization,[],[f1553])).
% 4.16/1.01 thf(f1555,plain,(
% 4.16/1.01 ( ! [X2 : a,X1 : extended_ereal] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | ($false = ((ord_less @ extended_ereal @ X1 @ (f @ x0)))) | ($false = ((member @ a @ X2 @ (sK49 @ X1)))) | ($true = ((ord_less @ extended_ereal @ X1 @ (f @ X2))))) )),
% 4.16/1.01 inference(imp_proxy_clausification,[],[f1554])).
% 4.16/1.01 thf(f2585,plain,(
% 4.16/1.01 (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | (((f @ x0)) = extend1396239628finity @ extended_ereal) | (((f @ x0)) = ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) | (((!! @ extended_ereal @ (^[Y0 : extended_ereal]: ((ord_less @ extended_ereal @ Y0 @ (f @ x0)) => (?? @ set @ a @ (^[Y1 : set @ a]: (((topolo1751647064n_open @ a @ Y1) & (member @ a @ x0 @ Y1)) & (!! @ a @ (^[Y2 : a]: ((member @ a @ Y2 @ Y1) => (ord_less @ extended_ereal @ Y0 @ (f @ Y2)))))))))))) = $false)),
% 4.16/1.01 inference(iff_proxy_clausification,[],[f1162])).
% 4.16/1.01 thf(f2586,plain,(
% 4.16/1.01 (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $false) | (((f @ x0)) = extend1396239628finity @ extended_ereal) | (((f @ x0)) = ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) | (((!! @ extended_ereal @ (^[Y0 : extended_ereal]: ((ord_less @ extended_ereal @ Y0 @ (f @ x0)) => (?? @ set @ a @ (^[Y1 : set @ a]: (((topolo1751647064n_open @ a @ Y1) & (member @ a @ x0 @ Y1)) & (!! @ a @ (^[Y2 : a]: ((member @ a @ Y2 @ Y1) => (ord_less @ extended_ereal @ Y0 @ (f @ Y2)))))))))))) = $true)),
% 4.16/1.01 inference(iff_proxy_clausification,[],[f1162])).
% 4.16/1.01 thf(f2587,plain,(
% 4.16/1.01 ( ! [X1 : extended_ereal] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $false) | (((f @ x0)) = extend1396239628finity @ extended_ereal) | (((f @ x0)) = ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) | ($true = (((^[Y0 : extended_ereal]: ((ord_less @ extended_ereal @ Y0 @ (f @ x0)) => (?? @ set @ a @ (^[Y1 : set @ a]: (((topolo1751647064n_open @ a @ Y1) & (member @ a @ x0 @ Y1)) & (!! @ a @ (^[Y2 : a]: ((member @ a @ Y2 @ Y1) => (ord_less @ extended_ereal @ Y0 @ (f @ Y2)))))))))) @ X1)))) )),
% 4.16/1.01 inference(pi_proxy_clausification,[],[f2586])).
% 4.16/1.01 thf(f2588,plain,(
% 4.16/1.01 ( ! [X1 : extended_ereal] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $false) | (((f @ x0)) = extend1396239628finity @ extended_ereal) | (((f @ x0)) = ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) | ($true = (((ord_less @ extended_ereal @ X1 @ (f @ x0)) => (?? @ set @ a @ (^[Y0 : set @ a]: (((topolo1751647064n_open @ a @ Y0) & (member @ a @ x0 @ Y0)) & (!! @ a @ (^[Y1 : a]: ((member @ a @ Y1 @ Y0) => (ord_less @ extended_ereal @ X1 @ (f @ Y1)))))))))))) )),
% 4.16/1.01 inference(beta-eta_normalization,[],[f2587])).
% 4.16/1.01 thf(f2589,plain,(
% 4.16/1.01 ( ! [X1 : extended_ereal] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $false) | (((f @ x0)) = extend1396239628finity @ extended_ereal) | (((f @ x0)) = ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) | ($false = ((ord_less @ extended_ereal @ X1 @ (f @ x0)))) | ($true = ((?? @ set @ a @ (^[Y0 : set @ a]: (((topolo1751647064n_open @ a @ Y0) & (member @ a @ x0 @ Y0)) & (!! @ a @ (^[Y1 : a]: ((member @ a @ Y1 @ Y0) => (ord_less @ extended_ereal @ X1 @ (f @ Y1))))))))))) )),
% 4.16/1.01 inference(imp_proxy_clausification,[],[f2588])).
% 4.16/1.01 thf(f2590,plain,(
% 4.16/1.01 ( ! [X1 : extended_ereal] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $false) | (((f @ x0)) = extend1396239628finity @ extended_ereal) | (((f @ x0)) = ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) | ($false = ((ord_less @ extended_ereal @ X1 @ (f @ x0)))) | ($true = (((^[Y0 : set @ a]: (((topolo1751647064n_open @ a @ Y0) & (member @ a @ x0 @ Y0)) & (!! @ a @ (^[Y1 : a]: ((member @ a @ Y1 @ Y0) => (ord_less @ extended_ereal @ X1 @ (f @ Y1))))))) @ (sK52 @ X1))))) )),
% 4.16/1.01 inference(sigma_proxy_clausification,[],[f2589])).
% 4.16/1.01 thf(f2591,plain,(
% 4.16/1.01 ( ! [X1 : extended_ereal] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $false) | (((f @ x0)) = extend1396239628finity @ extended_ereal) | (((f @ x0)) = ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) | ($false = ((ord_less @ extended_ereal @ X1 @ (f @ x0)))) | ($true = ((((topolo1751647064n_open @ a @ (sK52 @ X1)) & (member @ a @ x0 @ (sK52 @ X1))) & (!! @ a @ (^[Y0 : a]: ((member @ a @ Y0 @ (sK52 @ X1)) => (ord_less @ extended_ereal @ X1 @ (f @ Y0))))))))) )),
% 4.16/1.01 inference(beta-eta_normalization,[],[f2590])).
% 4.16/1.01 thf(f2592,plain,(
% 4.16/1.01 ( ! [X1 : extended_ereal] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $false) | (((f @ x0)) = extend1396239628finity @ extended_ereal) | (((f @ x0)) = ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) | ($false = ((ord_less @ extended_ereal @ X1 @ (f @ x0)))) | ($true = ((!! @ a @ (^[Y0 : a]: ((member @ a @ Y0 @ (sK52 @ X1)) => (ord_less @ extended_ereal @ X1 @ (f @ Y0)))))))) )),
% 4.16/1.01 inference(and_proxy_clausification,[],[f2591])).
% 4.16/1.01 thf(f2593,plain,(
% 4.16/1.01 ( ! [X1 : extended_ereal] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $false) | (((f @ x0)) = extend1396239628finity @ extended_ereal) | (((f @ x0)) = ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) | ($false = ((ord_less @ extended_ereal @ X1 @ (f @ x0)))) | ($true = (((topolo1751647064n_open @ a @ (sK52 @ X1)) & (member @ a @ x0 @ (sK52 @ X1)))))) )),
% 4.16/1.01 inference(and_proxy_clausification,[],[f2591])).
% 4.16/1.01 thf(f2594,plain,(
% 4.16/1.01 ( ! [X1 : extended_ereal] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $false) | (((f @ x0)) = extend1396239628finity @ extended_ereal) | (((f @ x0)) = ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) | ($false = ((ord_less @ extended_ereal @ X1 @ (f @ x0)))) | ($true = ((member @ a @ x0 @ (sK52 @ X1))))) )),
% 4.16/1.01 inference(and_proxy_clausification,[],[f2593])).
% 4.16/1.01 thf(f2595,plain,(
% 4.16/1.01 ( ! [X1 : extended_ereal] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $false) | (((f @ x0)) = extend1396239628finity @ extended_ereal) | (((f @ x0)) = ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) | ($false = ((ord_less @ extended_ereal @ X1 @ (f @ x0)))) | ($true = ((topolo1751647064n_open @ a @ (sK52 @ X1))))) )),
% 4.16/1.01 inference(and_proxy_clausification,[],[f2593])).
% 4.16/1.01 thf(f2596,plain,(
% 4.16/1.01 ( ! [X2 : a,X1 : extended_ereal] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $false) | (((f @ x0)) = extend1396239628finity @ extended_ereal) | (((f @ x0)) = ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) | ($false = ((ord_less @ extended_ereal @ X1 @ (f @ x0)))) | ($true = (((^[Y0 : a]: ((member @ a @ Y0 @ (sK52 @ X1)) => (ord_less @ extended_ereal @ X1 @ (f @ Y0)))) @ X2)))) )),
% 4.16/1.01 inference(pi_proxy_clausification,[],[f2592])).
% 4.16/1.01 thf(f2597,plain,(
% 4.16/1.01 ( ! [X2 : a,X1 : extended_ereal] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $false) | (((f @ x0)) = extend1396239628finity @ extended_ereal) | (((f @ x0)) = ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) | ($false = ((ord_less @ extended_ereal @ X1 @ (f @ x0)))) | ($true = (((member @ a @ X2 @ (sK52 @ X1)) => (ord_less @ extended_ereal @ X1 @ (f @ X2)))))) )),
% 4.16/1.01 inference(beta-eta_normalization,[],[f2596])).
% 4.16/1.01 thf(f2598,plain,(
% 4.16/1.01 ( ! [X2 : a,X1 : extended_ereal] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $false) | (((f @ x0)) = extend1396239628finity @ extended_ereal) | (((f @ x0)) = ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) | ($false = ((ord_less @ extended_ereal @ X1 @ (f @ x0)))) | ($false = ((member @ a @ X2 @ (sK52 @ X1)))) | ($true = ((ord_less @ extended_ereal @ X1 @ (f @ X2))))) )),
% 4.16/1.01 inference(imp_proxy_clausification,[],[f2597])).
% 4.16/1.01 thf(f2599,plain,(
% 4.16/1.01 (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | (((f @ x0)) = extend1396239628finity @ extended_ereal) | (((f @ x0)) = ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) | ($false = (((^[Y0 : extended_ereal]: ((ord_less @ extended_ereal @ Y0 @ (f @ x0)) => (?? @ set @ a @ (^[Y1 : set @ a]: (((topolo1751647064n_open @ a @ Y1) & (member @ a @ x0 @ Y1)) & (!! @ a @ (^[Y2 : a]: ((member @ a @ Y2 @ Y1) => (ord_less @ extended_ereal @ Y0 @ (f @ Y2)))))))))) @ sK53)))),
% 4.16/1.01 inference(sigma_proxy_clausification,[],[f2585])).
% 4.16/1.01 thf(f2600,plain,(
% 4.16/1.01 (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | (((f @ x0)) = extend1396239628finity @ extended_ereal) | (((f @ x0)) = ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) | ($false = (((ord_less @ extended_ereal @ sK53 @ (f @ x0)) => (?? @ set @ a @ (^[Y0 : set @ a]: (((topolo1751647064n_open @ a @ Y0) & (member @ a @ x0 @ Y0)) & (!! @ a @ (^[Y1 : a]: ((member @ a @ Y1 @ Y0) => (ord_less @ extended_ereal @ sK53 @ (f @ Y1)))))))))))),
% 4.16/1.01 inference(beta-eta_normalization,[],[f2599])).
% 4.16/1.01 thf(f2601,plain,(
% 4.16/1.01 (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | (((f @ x0)) = extend1396239628finity @ extended_ereal) | (((f @ x0)) = ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) | ($false = ((?? @ set @ a @ (^[Y0 : set @ a]: (((topolo1751647064n_open @ a @ Y0) & (member @ a @ x0 @ Y0)) & (!! @ a @ (^[Y1 : a]: ((member @ a @ Y1 @ Y0) => (ord_less @ extended_ereal @ sK53 @ (f @ Y1))))))))))),
% 4.16/1.01 inference(imp_proxy_clausification,[],[f2600])).
% 4.16/1.01 thf(f2602,plain,(
% 4.16/1.01 (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | (((f @ x0)) = extend1396239628finity @ extended_ereal) | (((f @ x0)) = ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) | ($true = ((ord_less @ extended_ereal @ sK53 @ (f @ x0))))),
% 4.16/1.01 inference(imp_proxy_clausification,[],[f2600])).
% 4.16/1.01 thf(f2603,plain,(
% 4.16/1.01 ( ! [X1 : set @ a] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | (((f @ x0)) = extend1396239628finity @ extended_ereal) | (((f @ x0)) = ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) | ($false = (((^[Y0 : set @ a]: (((topolo1751647064n_open @ a @ Y0) & (member @ a @ x0 @ Y0)) & (!! @ a @ (^[Y1 : a]: ((member @ a @ Y1 @ Y0) => (ord_less @ extended_ereal @ sK53 @ (f @ Y1))))))) @ X1)))) )),
% 4.16/1.01 inference(pi_proxy_clausification,[],[f2601])).
% 4.16/1.01 thf(f2604,plain,(
% 4.16/1.01 ( ! [X1 : set @ a] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | (((f @ x0)) = extend1396239628finity @ extended_ereal) | (((f @ x0)) = ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) | ($false = ((((topolo1751647064n_open @ a @ X1) & (member @ a @ x0 @ X1)) & (!! @ a @ (^[Y0 : a]: ((member @ a @ Y0 @ X1) => (ord_less @ extended_ereal @ sK53 @ (f @ Y0))))))))) )),
% 4.16/1.01 inference(beta-eta_normalization,[],[f2603])).
% 4.16/1.01 thf(f2605,plain,(
% 4.16/1.01 ( ! [X1 : set @ a] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | (((f @ x0)) = extend1396239628finity @ extended_ereal) | (((f @ x0)) = ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) | ($false = ((!! @ a @ (^[Y0 : a]: ((member @ a @ Y0 @ X1) => (ord_less @ extended_ereal @ sK53 @ (f @ Y0))))))) | ($false = (((topolo1751647064n_open @ a @ X1) & (member @ a @ x0 @ X1))))) )),
% 4.16/1.01 inference(and_proxy_clausification,[],[f2604])).
% 4.16/1.01 thf(f2606,plain,(
% 4.16/1.01 ( ! [X1 : set @ a] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | (((f @ x0)) = extend1396239628finity @ extended_ereal) | (((f @ x0)) = ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) | ($false = (((^[Y0 : a]: ((member @ a @ Y0 @ X1) => (ord_less @ extended_ereal @ sK53 @ (f @ Y0)))) @ (sK54 @ X1)))) | ($false = (((topolo1751647064n_open @ a @ X1) & (member @ a @ x0 @ X1))))) )),
% 4.16/1.01 inference(sigma_proxy_clausification,[],[f2605])).
% 4.16/1.01 thf(f2607,plain,(
% 4.16/1.01 ( ! [X1 : set @ a] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | (((f @ x0)) = extend1396239628finity @ extended_ereal) | (((f @ x0)) = ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) | ($false = (((^[Y0 : a]: ((member @ a @ Y0 @ X1) => (ord_less @ extended_ereal @ sK53 @ (f @ Y0)))) @ (sK54 @ X1)))) | (((member @ a @ x0 @ X1)) = $false) | (((topolo1751647064n_open @ a @ X1)) = $false)) )),
% 4.16/1.01 inference(and_proxy_clausification,[],[f2606])).
% 4.16/1.01 thf(f2608,plain,(
% 4.16/1.01 ( ! [X1 : set @ a] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | (((f @ x0)) = extend1396239628finity @ extended_ereal) | (((f @ x0)) = ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) | ($false = (((member @ a @ (sK54 @ X1) @ X1) => (ord_less @ extended_ereal @ sK53 @ (f @ (sK54 @ X1)))))) | (((member @ a @ x0 @ X1)) = $false) | (((topolo1751647064n_open @ a @ X1)) = $false)) )),
% 4.16/1.01 inference(beta-eta_normalization,[],[f2607])).
% 4.16/1.01 thf(f2609,plain,(
% 4.16/1.01 ( ! [X1 : set @ a] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | (((f @ x0)) = extend1396239628finity @ extended_ereal) | (((f @ x0)) = ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) | ($false = ((ord_less @ extended_ereal @ sK53 @ (f @ (sK54 @ X1))))) | (((member @ a @ x0 @ X1)) = $false) | (((topolo1751647064n_open @ a @ X1)) = $false)) )),
% 4.16/1.01 inference(imp_proxy_clausification,[],[f2608])).
% 4.16/1.01 thf(f2610,plain,(
% 4.16/1.01 ( ! [X1 : set @ a] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | (((f @ x0)) = extend1396239628finity @ extended_ereal) | (((f @ x0)) = ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) | ($true = ((member @ a @ (sK54 @ X1) @ X1))) | (((member @ a @ x0 @ X1)) = $false) | (((topolo1751647064n_open @ a @ X1)) = $false)) )),
% 4.16/1.01 inference(imp_proxy_clausification,[],[f2608])).
% 4.16/1.01 thf(f2611,plain,(
% 4.16/1.01 (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | (((f @ x0)) != ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) | (((!! @ extended_ereal @ (^[Y0 : extended_ereal]: ((ord_less @ extended_ereal @ Y0 @ (f @ x0)) => (?? @ set @ a @ (^[Y1 : set @ a]: (((topolo1751647064n_open @ a @ Y1) & (member @ a @ x0 @ Y1)) & (!! @ a @ (^[Y2 : a]: ((member @ a @ Y2 @ Y1) => (ord_less @ extended_ereal @ Y0 @ (f @ Y2)))))))))))) = $false)),
% 4.16/1.01 inference(iff_proxy_clausification,[],[f1161])).
% 4.16/1.01 thf(f2625,plain,(
% 4.16/1.01 (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | (((f @ x0)) != ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) | ($false = (((^[Y0 : extended_ereal]: ((ord_less @ extended_ereal @ Y0 @ (f @ x0)) => (?? @ set @ a @ (^[Y1 : set @ a]: (((topolo1751647064n_open @ a @ Y1) & (member @ a @ x0 @ Y1)) & (!! @ a @ (^[Y2 : a]: ((member @ a @ Y2 @ Y1) => (ord_less @ extended_ereal @ Y0 @ (f @ Y2)))))))))) @ sK56)))),
% 4.16/1.01 inference(sigma_proxy_clausification,[],[f2611])).
% 4.16/1.01 thf(f2626,plain,(
% 4.16/1.01 (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | (((f @ x0)) != ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) | ($false = (((ord_less @ extended_ereal @ sK56 @ (f @ x0)) => (?? @ set @ a @ (^[Y0 : set @ a]: (((topolo1751647064n_open @ a @ Y0) & (member @ a @ x0 @ Y0)) & (!! @ a @ (^[Y1 : a]: ((member @ a @ Y1 @ Y0) => (ord_less @ extended_ereal @ sK56 @ (f @ Y1)))))))))))),
% 4.16/1.01 inference(beta-eta_normalization,[],[f2625])).
% 4.16/1.01 thf(f2628,plain,(
% 4.16/1.01 (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | (((f @ x0)) != ((uminus_uminus @ extended_ereal @ extend1396239628finity @ extended_ereal))) | ($true = ((ord_less @ extended_ereal @ sK56 @ (f @ x0))))),
% 4.16/1.01 inference(imp_proxy_clausification,[],[f2626])).
% 4.16/1.01 thf(f2637,plain,(
% 4.16/1.01 (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | (((f @ x0)) != extend1396239628finity @ extended_ereal) | (((!! @ extended_ereal @ (^[Y0 : extended_ereal]: ((ord_less @ extended_ereal @ Y0 @ (f @ x0)) => (?? @ set @ a @ (^[Y1 : set @ a]: (((topolo1751647064n_open @ a @ Y1) & (member @ a @ x0 @ Y1)) & (!! @ a @ (^[Y2 : a]: ((member @ a @ Y2 @ Y1) => (ord_less @ extended_ereal @ Y0 @ (f @ Y2)))))))))))) = $false)),
% 4.16/1.01 inference(iff_proxy_clausification,[],[f1160])).
% 4.16/1.01 thf(f2638,plain,(
% 4.16/1.01 (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $false) | (((f @ x0)) != extend1396239628finity @ extended_ereal) | (((!! @ extended_ereal @ (^[Y0 : extended_ereal]: ((ord_less @ extended_ereal @ Y0 @ (f @ x0)) => (?? @ set @ a @ (^[Y1 : set @ a]: (((topolo1751647064n_open @ a @ Y1) & (member @ a @ x0 @ Y1)) & (!! @ a @ (^[Y2 : a]: ((member @ a @ Y2 @ Y1) => (ord_less @ extended_ereal @ Y0 @ (f @ Y2)))))))))))) = $true)),
% 4.16/1.01 inference(iff_proxy_clausification,[],[f1160])).
% 4.16/1.01 thf(f2639,plain,(
% 4.16/1.01 ( ! [X1 : extended_ereal] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $false) | (((f @ x0)) != extend1396239628finity @ extended_ereal) | ($true = (((^[Y0 : extended_ereal]: ((ord_less @ extended_ereal @ Y0 @ (f @ x0)) => (?? @ set @ a @ (^[Y1 : set @ a]: (((topolo1751647064n_open @ a @ Y1) & (member @ a @ x0 @ Y1)) & (!! @ a @ (^[Y2 : a]: ((member @ a @ Y2 @ Y1) => (ord_less @ extended_ereal @ Y0 @ (f @ Y2)))))))))) @ X1)))) )),
% 4.16/1.01 inference(pi_proxy_clausification,[],[f2638])).
% 4.16/1.01 thf(f2640,plain,(
% 4.16/1.01 ( ! [X1 : extended_ereal] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $false) | (((f @ x0)) != extend1396239628finity @ extended_ereal) | ($true = (((ord_less @ extended_ereal @ X1 @ (f @ x0)) => (?? @ set @ a @ (^[Y0 : set @ a]: (((topolo1751647064n_open @ a @ Y0) & (member @ a @ x0 @ Y0)) & (!! @ a @ (^[Y1 : a]: ((member @ a @ Y1 @ Y0) => (ord_less @ extended_ereal @ X1 @ (f @ Y1)))))))))))) )),
% 4.16/1.01 inference(beta-eta_normalization,[],[f2639])).
% 4.16/1.01 thf(f2641,plain,(
% 4.16/1.01 ( ! [X1 : extended_ereal] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $false) | (((f @ x0)) != extend1396239628finity @ extended_ereal) | ($false = ((ord_less @ extended_ereal @ X1 @ (f @ x0)))) | ($true = ((?? @ set @ a @ (^[Y0 : set @ a]: (((topolo1751647064n_open @ a @ Y0) & (member @ a @ x0 @ Y0)) & (!! @ a @ (^[Y1 : a]: ((member @ a @ Y1 @ Y0) => (ord_less @ extended_ereal @ X1 @ (f @ Y1))))))))))) )),
% 4.16/1.01 inference(imp_proxy_clausification,[],[f2640])).
% 4.16/1.01 thf(f2642,plain,(
% 4.16/1.01 ( ! [X1 : extended_ereal] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $false) | (((f @ x0)) != extend1396239628finity @ extended_ereal) | ($false = ((ord_less @ extended_ereal @ X1 @ (f @ x0)))) | ($true = (((^[Y0 : set @ a]: (((topolo1751647064n_open @ a @ Y0) & (member @ a @ x0 @ Y0)) & (!! @ a @ (^[Y1 : a]: ((member @ a @ Y1 @ Y0) => (ord_less @ extended_ereal @ X1 @ (f @ Y1))))))) @ (sK58 @ X1))))) )),
% 4.16/1.01 inference(sigma_proxy_clausification,[],[f2641])).
% 4.16/1.01 thf(f2643,plain,(
% 4.16/1.01 ( ! [X1 : extended_ereal] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $false) | (((f @ x0)) != extend1396239628finity @ extended_ereal) | ($false = ((ord_less @ extended_ereal @ X1 @ (f @ x0)))) | ($true = ((((topolo1751647064n_open @ a @ (sK58 @ X1)) & (member @ a @ x0 @ (sK58 @ X1))) & (!! @ a @ (^[Y0 : a]: ((member @ a @ Y0 @ (sK58 @ X1)) => (ord_less @ extended_ereal @ X1 @ (f @ Y0))))))))) )),
% 4.16/1.01 inference(beta-eta_normalization,[],[f2642])).
% 4.16/1.01 thf(f2644,plain,(
% 4.16/1.01 ( ! [X1 : extended_ereal] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $false) | (((f @ x0)) != extend1396239628finity @ extended_ereal) | ($false = ((ord_less @ extended_ereal @ X1 @ (f @ x0)))) | ($true = ((!! @ a @ (^[Y0 : a]: ((member @ a @ Y0 @ (sK58 @ X1)) => (ord_less @ extended_ereal @ X1 @ (f @ Y0)))))))) )),
% 4.16/1.01 inference(and_proxy_clausification,[],[f2643])).
% 4.16/1.01 thf(f2645,plain,(
% 4.16/1.01 ( ! [X1 : extended_ereal] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $false) | (((f @ x0)) != extend1396239628finity @ extended_ereal) | ($false = ((ord_less @ extended_ereal @ X1 @ (f @ x0)))) | ($true = (((topolo1751647064n_open @ a @ (sK58 @ X1)) & (member @ a @ x0 @ (sK58 @ X1)))))) )),
% 4.16/1.01 inference(and_proxy_clausification,[],[f2643])).
% 4.16/1.01 thf(f2646,plain,(
% 4.16/1.01 ( ! [X1 : extended_ereal] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $false) | (((f @ x0)) != extend1396239628finity @ extended_ereal) | ($false = ((ord_less @ extended_ereal @ X1 @ (f @ x0)))) | ($true = ((member @ a @ x0 @ (sK58 @ X1))))) )),
% 4.16/1.01 inference(and_proxy_clausification,[],[f2645])).
% 4.16/1.01 thf(f2647,plain,(
% 4.16/1.01 ( ! [X1 : extended_ereal] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $false) | (((f @ x0)) != extend1396239628finity @ extended_ereal) | ($false = ((ord_less @ extended_ereal @ X1 @ (f @ x0)))) | ($true = ((topolo1751647064n_open @ a @ (sK58 @ X1))))) )),
% 4.16/1.01 inference(and_proxy_clausification,[],[f2645])).
% 4.16/1.01 thf(f2648,plain,(
% 4.16/1.01 ( ! [X2 : a,X1 : extended_ereal] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $false) | (((f @ x0)) != extend1396239628finity @ extended_ereal) | ($false = ((ord_less @ extended_ereal @ X1 @ (f @ x0)))) | ($true = (((^[Y0 : a]: ((member @ a @ Y0 @ (sK58 @ X1)) => (ord_less @ extended_ereal @ X1 @ (f @ Y0)))) @ X2)))) )),
% 4.16/1.01 inference(pi_proxy_clausification,[],[f2644])).
% 4.16/1.01 thf(f2649,plain,(
% 4.16/1.01 ( ! [X2 : a,X1 : extended_ereal] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $false) | (((f @ x0)) != extend1396239628finity @ extended_ereal) | ($false = ((ord_less @ extended_ereal @ X1 @ (f @ x0)))) | ($true = (((member @ a @ X2 @ (sK58 @ X1)) => (ord_less @ extended_ereal @ X1 @ (f @ X2)))))) )),
% 4.16/1.01 inference(beta-eta_normalization,[],[f2648])).
% 4.16/1.01 thf(f2650,plain,(
% 4.16/1.01 ( ! [X2 : a,X1 : extended_ereal] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $false) | (((f @ x0)) != extend1396239628finity @ extended_ereal) | ($false = ((ord_less @ extended_ereal @ X1 @ (f @ x0)))) | ($false = ((member @ a @ X2 @ (sK58 @ X1)))) | ($true = ((ord_less @ extended_ereal @ X1 @ (f @ X2))))) )),
% 4.16/1.01 inference(imp_proxy_clausification,[],[f2649])).
% 4.16/1.01 thf(f2651,plain,(
% 4.16/1.01 (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | (((f @ x0)) != extend1396239628finity @ extended_ereal) | ($false = (((^[Y0 : extended_ereal]: ((ord_less @ extended_ereal @ Y0 @ (f @ x0)) => (?? @ set @ a @ (^[Y1 : set @ a]: (((topolo1751647064n_open @ a @ Y1) & (member @ a @ x0 @ Y1)) & (!! @ a @ (^[Y2 : a]: ((member @ a @ Y2 @ Y1) => (ord_less @ extended_ereal @ Y0 @ (f @ Y2)))))))))) @ sK59)))),
% 4.16/1.01 inference(sigma_proxy_clausification,[],[f2637])).
% 4.16/1.01 thf(f2652,plain,(
% 4.16/1.01 (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | (((f @ x0)) != extend1396239628finity @ extended_ereal) | ($false = (((ord_less @ extended_ereal @ sK59 @ (f @ x0)) => (?? @ set @ a @ (^[Y0 : set @ a]: (((topolo1751647064n_open @ a @ Y0) & (member @ a @ x0 @ Y0)) & (!! @ a @ (^[Y1 : a]: ((member @ a @ Y1 @ Y0) => (ord_less @ extended_ereal @ sK59 @ (f @ Y1)))))))))))),
% 4.16/1.01 inference(beta-eta_normalization,[],[f2651])).
% 4.16/1.01 thf(f2653,plain,(
% 4.16/1.01 (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | (((f @ x0)) != extend1396239628finity @ extended_ereal) | ($false = ((?? @ set @ a @ (^[Y0 : set @ a]: (((topolo1751647064n_open @ a @ Y0) & (member @ a @ x0 @ Y0)) & (!! @ a @ (^[Y1 : a]: ((member @ a @ Y1 @ Y0) => (ord_less @ extended_ereal @ sK59 @ (f @ Y1))))))))))),
% 4.16/1.01 inference(imp_proxy_clausification,[],[f2652])).
% 4.16/1.01 thf(f2654,plain,(
% 4.16/1.01 (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | (((f @ x0)) != extend1396239628finity @ extended_ereal) | ($true = ((ord_less @ extended_ereal @ sK59 @ (f @ x0))))),
% 4.16/1.01 inference(imp_proxy_clausification,[],[f2652])).
% 4.16/1.01 thf(f2655,plain,(
% 4.16/1.01 ( ! [X1 : set @ a] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | (((f @ x0)) != extend1396239628finity @ extended_ereal) | ($false = (((^[Y0 : set @ a]: (((topolo1751647064n_open @ a @ Y0) & (member @ a @ x0 @ Y0)) & (!! @ a @ (^[Y1 : a]: ((member @ a @ Y1 @ Y0) => (ord_less @ extended_ereal @ sK59 @ (f @ Y1))))))) @ X1)))) )),
% 4.16/1.01 inference(pi_proxy_clausification,[],[f2653])).
% 4.16/1.01 thf(f2656,plain,(
% 4.16/1.01 ( ! [X1 : set @ a] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | (((f @ x0)) != extend1396239628finity @ extended_ereal) | ($false = ((((topolo1751647064n_open @ a @ X1) & (member @ a @ x0 @ X1)) & (!! @ a @ (^[Y0 : a]: ((member @ a @ Y0 @ X1) => (ord_less @ extended_ereal @ sK59 @ (f @ Y0))))))))) )),
% 4.16/1.01 inference(beta-eta_normalization,[],[f2655])).
% 4.16/1.01 thf(f2657,plain,(
% 4.16/1.01 ( ! [X1 : set @ a] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | (((f @ x0)) != extend1396239628finity @ extended_ereal) | ($false = ((!! @ a @ (^[Y0 : a]: ((member @ a @ Y0 @ X1) => (ord_less @ extended_ereal @ sK59 @ (f @ Y0))))))) | ($false = (((topolo1751647064n_open @ a @ X1) & (member @ a @ x0 @ X1))))) )),
% 4.16/1.01 inference(and_proxy_clausification,[],[f2656])).
% 4.16/1.01 thf(f2658,plain,(
% 4.16/1.01 ( ! [X1 : set @ a] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | (((f @ x0)) != extend1396239628finity @ extended_ereal) | ($false = (((^[Y0 : a]: ((member @ a @ Y0 @ X1) => (ord_less @ extended_ereal @ sK59 @ (f @ Y0)))) @ (sK60 @ X1)))) | ($false = (((topolo1751647064n_open @ a @ X1) & (member @ a @ x0 @ X1))))) )),
% 4.16/1.01 inference(sigma_proxy_clausification,[],[f2657])).
% 4.16/1.01 thf(f2659,plain,(
% 4.16/1.01 ( ! [X1 : set @ a] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | (((f @ x0)) != extend1396239628finity @ extended_ereal) | ($false = (((^[Y0 : a]: ((member @ a @ Y0 @ X1) => (ord_less @ extended_ereal @ sK59 @ (f @ Y0)))) @ (sK60 @ X1)))) | (((member @ a @ x0 @ X1)) = $false) | (((topolo1751647064n_open @ a @ X1)) = $false)) )),
% 4.16/1.01 inference(and_proxy_clausification,[],[f2658])).
% 4.16/1.01 thf(f2660,plain,(
% 4.16/1.01 ( ! [X1 : set @ a] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | (((f @ x0)) != extend1396239628finity @ extended_ereal) | ($false = (((member @ a @ (sK60 @ X1) @ X1) => (ord_less @ extended_ereal @ sK59 @ (f @ (sK60 @ X1)))))) | (((member @ a @ x0 @ X1)) = $false) | (((topolo1751647064n_open @ a @ X1)) = $false)) )),
% 4.16/1.01 inference(beta-eta_normalization,[],[f2659])).
% 4.16/1.01 thf(f2661,plain,(
% 4.16/1.01 ( ! [X1 : set @ a] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | (((f @ x0)) != extend1396239628finity @ extended_ereal) | ($false = ((ord_less @ extended_ereal @ sK59 @ (f @ (sK60 @ X1))))) | (((member @ a @ x0 @ X1)) = $false) | (((topolo1751647064n_open @ a @ X1)) = $false)) )),
% 4.16/1.01 inference(imp_proxy_clausification,[],[f2660])).
% 4.16/1.01 thf(f2662,plain,(
% 4.16/1.01 ( ! [X1 : set @ a] : ((((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | (((f @ x0)) != extend1396239628finity @ extended_ereal) | ($true = ((member @ a @ (sK60 @ X1) @ X1))) | (((member @ a @ x0 @ X1)) = $false) | (((topolo1751647064n_open @ a @ X1)) = $false)) )),
% 4.16/1.01 inference(imp_proxy_clausification,[],[f2660])).
% 4.16/1.01 thf(f2664,definition,(
% 4.16/1.01 spl61_1 <=> ($true = ((ord_less @ extended_ereal @ sK47 @ (f @ x0))))),
% 4.16/1.01 introduced(definition,[new_symbols(definition,[spl61_1])],[avatar_definition])).
% 4.16/1.01 thf(f2666,plain,(
% 4.16/1.01 ($true = ((ord_less @ extended_ereal @ sK47 @ (f @ x0)))) | ~spl61_1),
% 4.16/1.01 inference(avatar_component_clause,[],[f2664])).
% 4.16/1.01 thf(f2668,definition,(
% 4.16/1.01 spl61_2 <=> (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $false)),
% 4.16/1.01 introduced(definition,[new_symbols(definition,[spl61_2])],[avatar_definition])).
% 4.16/1.01 thf(f2670,plain,(
% 4.16/1.01 (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $false) | ~spl61_2),
% 4.16/1.01 inference(avatar_component_clause,[],[f2668])).
% 4.16/1.01 thf(f2671,plain,(
% 4.16/1.01 spl61_1 | spl61_2),
% 4.16/1.01 inference(avatar_split_clause,[],[f1534,f2668,f2664])).
% 4.16/1.01 thf(f2673,definition,(
% 4.16/1.01 spl61_3 <=> ! [X1 : set @ a] : (($true = ((member @ a @ (sK48 @ X1) @ X1))) | (((topolo1751647064n_open @ a @ X1)) = $false) | (((member @ a @ x0 @ X1)) = $false))),
% 4.16/1.01 introduced(definition,[new_symbols(definition,[spl61_3])],[avatar_definition])).
% 4.16/1.01 thf(f2674,plain,(
% 4.16/1.01 ( ! [X1 : set @ a] : (($true = ((member @ a @ (sK48 @ X1) @ X1))) | (((member @ a @ x0 @ X1)) = $false) | (((topolo1751647064n_open @ a @ X1)) = $false)) ) | ~spl61_3),
% 4.16/1.01 inference(avatar_component_clause,[],[f2673])).
% 4.16/1.01 thf(f2675,plain,(
% 4.16/1.01 spl61_3 | spl61_2),
% 4.16/1.01 inference(avatar_split_clause,[],[f1542,f2668,f2673])).
% 4.16/1.01 thf(f2677,definition,(
% 4.16/1.01 spl61_4 <=> ! [X1 : set @ a] : (($false = ((ord_less @ extended_ereal @ sK47 @ (f @ (sK48 @ X1))))) | (((topolo1751647064n_open @ a @ X1)) = $false) | (((member @ a @ x0 @ X1)) = $false))),
% 4.16/1.01 introduced(definition,[new_symbols(definition,[spl61_4])],[avatar_definition])).
% 4.16/1.01 thf(f2678,plain,(
% 4.16/1.01 ( ! [X1 : set @ a] : (($false = ((ord_less @ extended_ereal @ sK47 @ (f @ (sK48 @ X1))))) | (((topolo1751647064n_open @ a @ X1)) = $false) | (((member @ a @ x0 @ X1)) = $false)) ) | ~spl61_4),
% 4.16/1.01 inference(avatar_component_clause,[],[f2677])).
% 4.16/1.01 thf(f2679,plain,(
% 4.16/1.01 spl61_4 | spl61_2),
% 4.16/1.01 inference(avatar_split_clause,[],[f1541,f2668,f2677])).
% 4.16/1.01 thf(f2681,definition,(
% 4.16/1.01 spl61_5 <=> ! [X1 : extended_ereal] : (($false = ((ord_less @ extended_ereal @ X1 @ (f @ x0)))) | ($true = ((topolo1751647064n_open @ a @ (sK49 @ X1)))))),
% 4.16/1.01 introduced(definition,[new_symbols(definition,[spl61_5])],[avatar_definition])).
% 4.16/1.01 thf(f2682,plain,(
% 4.16/1.01 ( ! [X1 : extended_ereal] : (($false = ((ord_less @ extended_ereal @ X1 @ (f @ x0)))) | ($true = ((topolo1751647064n_open @ a @ (sK49 @ X1))))) ) | ~spl61_5),
% 4.16/1.01 inference(avatar_component_clause,[],[f2681])).
% 4.16/1.01 thf(f2684,definition,(
% 4.16/1.01 spl61_6 <=> (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true)),
% 4.16/1.01 introduced(definition,[new_symbols(definition,[spl61_6])],[avatar_definition])).
% 4.16/1.01 thf(f2686,plain,(
% 4.16/1.01 (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | ~spl61_6),
% 4.16/1.01 inference(avatar_component_clause,[],[f2684])).
% 4.16/1.01 thf(f2687,plain,(
% 4.16/1.01 spl61_5 | spl61_6),
% 4.16/1.01 inference(avatar_split_clause,[],[f1552,f2684,f2681])).
% 4.16/1.01 thf(f2689,definition,(
% 4.16/1.01 spl61_7 <=> ! [X1 : extended_ereal] : (($false = ((ord_less @ extended_ereal @ X1 @ (f @ x0)))) | ($true = ((member @ a @ x0 @ (sK49 @ X1)))))),
% 4.16/1.01 introduced(definition,[new_symbols(definition,[spl61_7])],[avatar_definition])).
% 4.16/1.01 thf(f2690,plain,(
% 4.16/1.01 ( ! [X1 : extended_ereal] : (($false = ((ord_less @ extended_ereal @ X1 @ (f @ x0)))) | ($true = ((member @ a @ x0 @ (sK49 @ X1))))) ) | ~spl61_7),
% 4.16/1.01 inference(avatar_component_clause,[],[f2689])).
% 4.16/1.01 thf(f2691,plain,(
% 4.16/1.01 spl61_7 | spl61_6),
% 4.16/1.01 inference(avatar_split_clause,[],[f1551,f2684,f2689])).
% 4.16/1.01 thf(f2693,definition,(
% 4.16/1.01 spl61_8 <=> ! [X2 : a,X1 : extended_ereal] : (($false = ((ord_less @ extended_ereal @ X1 @ (f @ x0)))) | ($true = ((ord_less @ extended_ereal @ X1 @ (f @ X2)))) | ($false = ((member @ a @ X2 @ (sK49 @ X1)))))),
% 4.16/1.01 introduced(definition,[new_symbols(definition,[spl61_8])],[avatar_definition])).
% 4.16/1.01 thf(f2694,plain,(
% 4.16/1.01 ( ! [X2 : a,X1 : extended_ereal] : (($true = ((ord_less @ extended_ereal @ X1 @ (f @ X2)))) | ($false = ((ord_less @ extended_ereal @ X1 @ (f @ x0)))) | ($false = ((member @ a @ X2 @ (sK49 @ X1))))) ) | ~spl61_8),
% 4.16/1.01 inference(avatar_component_clause,[],[f2693])).
% 4.16/1.01 thf(f2695,plain,(
% 4.16/1.01 spl61_8 | spl61_6),
% 4.16/1.01 inference(avatar_split_clause,[],[f1555,f2684,f2693])).
% 4.16/1.01 thf(f2702,plain,(
% 4.16/1.01 ( ! [X0 : extended_ereal] : (($true != ((ord_less @ extended_ereal @ X0 @ extended_MInfty)))) )),
% 4.16/1.01 inference(forward_demodulation,[],[f1204,f1231])).
% 4.16/1.01 thf(f2707,plain,(
% 4.16/1.01 ( ! [X1 : extended_ereal] : ((((f @ x0)) = extended_MInfty) | (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $false) | (((f @ x0)) = extend1396239628finity @ extended_ereal) | ($false = ((ord_less @ extended_ereal @ X1 @ (f @ x0)))) | ($true = ((topolo1751647064n_open @ a @ (sK52 @ X1))))) )),
% 4.16/1.01 inference(forward_demodulation,[],[f2595,f1231])).
% 4.16/1.01 thf(f2708,plain,(
% 4.16/1.01 ( ! [X1 : extended_ereal] : ((((f @ x0)) = extended_MInfty) | (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $false) | (((f @ x0)) = extend1396239628finity @ extended_ereal) | ($false = ((ord_less @ extended_ereal @ X1 @ (f @ x0)))) | ($true = ((member @ a @ x0 @ (sK52 @ X1))))) )),
% 4.16/1.01 inference(forward_demodulation,[],[f2594,f1231])).
% 4.16/1.01 thf(f2709,plain,(
% 4.16/1.01 ( ! [X2 : a,X1 : extended_ereal] : ((((f @ x0)) = extended_MInfty) | (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $false) | (((f @ x0)) = extend1396239628finity @ extended_ereal) | ($false = ((ord_less @ extended_ereal @ X1 @ (f @ x0)))) | ($false = ((member @ a @ X2 @ (sK52 @ X1)))) | ($true = ((ord_less @ extended_ereal @ X1 @ (f @ X2))))) )),
% 4.16/1.01 inference(forward_demodulation,[],[f2598,f1231])).
% 4.16/1.01 thf(f2710,plain,(
% 4.16/1.01 (((f @ x0)) = extended_MInfty) | (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | (((f @ x0)) = extend1396239628finity @ extended_ereal) | ($true = ((ord_less @ extended_ereal @ sK53 @ (f @ x0))))),
% 4.16/1.01 inference(forward_demodulation,[],[f2602,f1231])).
% 4.16/1.01 thf(f2711,plain,(
% 4.16/1.01 ( ! [X1 : set @ a] : ((((f @ x0)) = extended_MInfty) | (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | (((f @ x0)) = extend1396239628finity @ extended_ereal) | ($true = ((member @ a @ (sK54 @ X1) @ X1))) | (((member @ a @ x0 @ X1)) = $false) | (((topolo1751647064n_open @ a @ X1)) = $false)) )),
% 4.16/1.01 inference(forward_demodulation,[],[f2610,f1231])).
% 4.16/1.01 thf(f2712,plain,(
% 4.16/1.01 ( ! [X1 : set @ a] : ((((f @ x0)) = extended_MInfty) | (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | (((f @ x0)) = extend1396239628finity @ extended_ereal) | ($false = ((ord_less @ extended_ereal @ sK53 @ (f @ (sK54 @ X1))))) | (((member @ a @ x0 @ X1)) = $false) | (((topolo1751647064n_open @ a @ X1)) = $false)) )),
% 4.16/1.01 inference(forward_demodulation,[],[f2609,f1231])).
% 4.16/1.01 thf(f2716,plain,(
% 4.16/1.01 (((f @ x0)) != extended_MInfty) | (((lower_582600101lsc_at @ a @ extended_ereal @ x0 @ f)) = $true) | ($true = ((ord_less @ extended_ereal @ sK56 @ (f @ x0))))),
% 4.16/1.01 inference(forward_demodulation,[],[f2628,f1231])).
% 4.16/1.01 thf(f2720,definition,(
% 4.16/1.01 spl61_9 <=> ! [X1 : extended_ereal] : (($false = ((ord_less @ extended_ereal @ X1 @ (f @ x0)))) | ($true = ((topolo1751647064n_open @ a @ (sK58 @ X1)))))),
% 4.16/1.01 introduced(definition,[new_symbols(definition,[spl61_9])],[avatar_definition])).
% 4.16/1.01 thf(f2721,plain,(
% 4.16/1.01 ( ! [X1 : extended_ereal] : (($false = ((ord_less @ extended_ereal @ X1 @ (f @ x0)))) | ($true = ((topolo1751647064n_open @ a @ (sK58 @ X1))))) ) | ~spl61_9),
% 4.16/1.01 inference(avatar_component_clause,[],[f2720])).
% 4.16/1.01 thf(f2723,definition,(
% 4.16/1.01 spl61_10 <=> (((f @ x0)) = extend1396239628finity @ extended_ereal)),
% 4.16/1.01 introduced(definition,[new_symbols(definition,[spl61_10])],[avatar_definition])).
% 4.16/1.01 thf(f2724,plain,(
% 4.16/1.01 (((f @ x0)) = extend1396239628finity @ extended_ereal) | ~spl61_10),
% 4.16/1.01 inference(avatar_component_clause,[],[f2723])).
% 4.16/1.01 thf(f2726,plain,(
% 4.16/1.01 spl61_9 | ~spl61_10 | spl61_2),
% 4.16/1.01 inference(avatar_split_clause,[],[f2647,f2668,f2723,f2720])).
% 4.16/1.01 thf(f2728,definition,(
% 4.16/1.01 spl61_11 <=> ! [X1 : extended_ereal] : (($false = ((ord_less @ extended_ereal @ X1 @ (f @ x0)))) | ($true = ((member @ a @ x0 @ (sK58 @ X1)))))),
% 4.16/1.01 introduced(definition,[new_symbols(definition,[spl61_11])],[avatar_definition])).
% 4.16/1.01 thf(f2729,plain,(
% 4.16/1.01 ( ! [X1 : extended_ereal] : (($false = ((ord_less @ extended_ereal @ X1 @ (f @ x0)))) | ($true = ((member @ a @ x0 @ (sK58 @ X1))))) ) | ~spl61_11),
% 4.16/1.01 inference(avatar_component_clause,[],[f2728])).
% 4.16/1.01 thf(f2730,plain,(
% 4.16/1.01 spl61_11 | ~spl61_10 | spl61_2),
% 4.16/1.01 inference(avatar_split_clause,[],[f2646,f2668,f2723,f2728])).
% 4.16/1.01 thf(f2732,definition,(
% 4.16/1.01 spl61_12 <=> ! [X2 : a,X1 : extended_ereal] : (($false = ((ord_less @ extended_ereal @ X1 @ (f @ x0)))) | ($true = ((ord_less @ extended_ereal @ X1 @ (f @ X2)))) | ($false = ((member @ a @ X2 @ (sK58 @ X1)))))),
% 4.16/1.01 introduced(definition,[new_symbols(definition,[spl61_12])],[avatar_definition])).
% 4.16/1.01 thf(f2733,plain,(
% 4.16/1.01 ( ! [X2 : a,X1 : extended_ereal] : (($false = ((ord_less @ extended_ereal @ X1 @ (f @ x0)))) | ($true = ((ord_less @ extended_ereal @ X1 @ (f @ X2)))) | ($false = ((member @ a @ X2 @ (sK58 @ X1))))) ) | ~spl61_12),
% 4.16/1.01 inference(avatar_component_clause,[],[f2732])).
% 4.16/1.01 thf(f2734,plain,(
% 4.16/1.01 spl61_12 | ~spl61_10 | spl61_2),
% 4.16/1.01 inference(avatar_split_clause,[],[f2650,f2668,f2723,f2732])).
% 4.16/1.01 thf(f2736,definition,(
% 4.16/1.01 spl61_13 <=> ($true = ((ord_less @ extended_ereal @ sK59 @ (f @ x0))))),
% 4.16/1.01 introduced(definition,[new_symbols(definition,[spl61_13])],[avatar_definition])).
% 4.16/1.01 thf(f2738,plain,(
% 4.16/1.01 ($true = ((ord_less @ extended_ereal @ sK59 @ (f @ x0)))) | ~spl61_13),
% 4.16/1.01 inference(avatar_component_clause,[],[f2736])).
% 4.16/1.01 thf(f2739,plain,(
% 4.16/1.01 spl61_13 | ~spl61_10 | spl61_6),
% 4.16/1.01 inference(avatar_split_clause,[],[f2654,f2684,f2723,f2736])).
% 4.16/1.01 thf(f2741,definition,(
% 4.16/1.01 spl61_14 <=> ! [X1 : set @ a] : (($true = ((member @ a @ (sK60 @ X1) @ X1))) | (((topolo1751647064n_open @ a @ X1)) = $false) | (((member @ a @ x0 @ X1)) = $false))),
% 4.16/1.01 introduced(definition,[new_symbols(definition,[spl61_14])],[avatar_definition])).
% 4.16/1.01 thf(f2742,plain,(
% 4.16/1.01 ( ! [X1 : set @ a] : (($true = ((member @ a @ (sK60 @ X1) @ X1))) | (((member @ a @ x0 @ X1)) = $false) | (((topolo1751647064n_open @ a @ X1)) = $false)) ) | ~spl61_14),
% 4.16/1.01 inference(avatar_component_clause,[],[f2741])).
% 4.16/1.01 thf(f2743,plain,(
% 4.16/1.01 spl61_14 | ~spl61_10 | spl61_6),
% 4.16/1.01 inference(avatar_split_clause,[],[f2662,f2684,f2723,f2741])).
% 4.16/1.01 thf(f2745,definition,(
% 4.16/1.01 spl61_15 <=> ! [X1 : set @ a] : (($false = ((ord_less @ extended_ereal @ sK59 @ (f @ (sK60 @ X1))))) | (((topolo1751647064n_open @ a @ X1)) = $false) | (((member @ a @ x0 @ X1)) = $false))),
% 4.16/1.01 introduced(definition,[new_symbols(definition,[spl61_15])],[avatar_definition])).
% 4.16/1.01 thf(f2746,plain,(
% 4.16/1.01 ( ! [X1 : set @ a] : (($false = ((ord_less @ extended_ereal @ sK59 @ (f @ (sK60 @ X1))))) | (((topolo1751647064n_open @ a @ X1)) = $false) | (((member @ a @ x0 @ X1)) = $false)) ) | ~spl61_15),
% 4.16/1.01 inference(avatar_component_clause,[],[f2745])).
% 4.16/1.01 thf(f2747,plain,(
% 4.16/1.01 spl61_15 | ~spl61_10 | spl61_6),
% 4.16/1.01 inference(avatar_split_clause,[],[f2661,f2684,f2723,f2745])).
% 4.16/1.01 thf(f2752,definition,(
% 4.16/1.01 spl61_16 <=> ! [X1 : extended_ereal] : (($false = ((ord_less @ extended_ereal @ X1 @ (f @ x0)))) | ($true = ((topolo1751647064n_open @ a @ (sK52 @ X1)))))),
% 4.16/1.01 introduced(definition,[new_symbols(definition,[spl61_16])],[avatar_definition])).
% 4.16/1.01 thf(f2753,plain,(
% 4.16/1.01 ( ! [X1 : extended_ereal] : (($false = ((ord_less @ extended_ereal @ X1 @ (f @ x0)))) | ($true = ((topolo1751647064n_open @ a @ (sK52 @ X1))))) ) | ~spl61_16),
% 4.16/1.01 inference(avatar_component_clause,[],[f2752])).
% 4.16/1.01 thf(f2755,definition,(
% 4.16/1.01 spl61_17 <=> (((f @ x0)) = extended_MInfty)),
% 4.16/1.01 introduced(definition,[new_symbols(definition,[spl61_17])],[avatar_definition])).
% 4.16/1.01 thf(f2757,plain,(
% 4.16/1.01 (((f @ x0)) = extended_MInfty) | ~spl61_17),
% 4.16/1.01 inference(avatar_component_clause,[],[f2755])).
% 4.16/1.01 thf(f2758,plain,(
% 4.16/1.01 spl61_16 | spl61_10 | spl61_2 | spl61_17),
% 4.16/1.01 inference(avatar_split_clause,[],[f2707,f2755,f2668,f2723,f2752])).
% 4.16/1.01 thf(f2760,definition,(
% 4.16/1.01 spl61_18 <=> ! [X1 : extended_ereal] : (($false = ((ord_less @ extended_ereal @ X1 @ (f @ x0)))) | ($true = ((member @ a @ x0 @ (sK52 @ X1)))))),
% 4.16/1.01 introduced(definition,[new_symbols(definition,[spl61_18])],[avatar_definition])).
% 4.16/1.01 thf(f2761,plain,(
% 4.16/1.01 ( ! [X1 : extended_ereal] : (($false = ((ord_less @ extended_ereal @ X1 @ (f @ x0)))) | ($true = ((member @ a @ x0 @ (sK52 @ X1))))) ) | ~spl61_18),
% 4.16/1.02 inference(avatar_component_clause,[],[f2760])).
% 4.16/1.02 thf(f2762,plain,(
% 4.16/1.02 spl61_18 | spl61_10 | spl61_2 | spl61_17),
% 4.16/1.02 inference(avatar_split_clause,[],[f2708,f2755,f2668,f2723,f2760])).
% 4.16/1.02 thf(f2764,definition,(
% 4.16/1.02 spl61_19 <=> ! [X2 : a,X1 : extended_ereal] : (($false = ((ord_less @ extended_ereal @ X1 @ (f @ x0)))) | ($true = ((ord_less @ extended_ereal @ X1 @ (f @ X2)))) | ($false = ((member @ a @ X2 @ (sK52 @ X1)))))),
% 4.16/1.02 introduced(definition,[new_symbols(definition,[spl61_19])],[avatar_definition])).
% 4.16/1.02 thf(f2765,plain,(
% 4.16/1.02 ( ! [X2 : a,X1 : extended_ereal] : (($true = ((ord_less @ extended_ereal @ X1 @ (f @ X2)))) | ($false = ((ord_less @ extended_ereal @ X1 @ (f @ x0)))) | ($false = ((member @ a @ X2 @ (sK52 @ X1))))) ) | ~spl61_19),
% 4.16/1.02 inference(avatar_component_clause,[],[f2764])).
% 4.16/1.02 thf(f2766,plain,(
% 4.16/1.02 spl61_19 | spl61_10 | spl61_2 | spl61_17),
% 4.16/1.02 inference(avatar_split_clause,[],[f2709,f2755,f2668,f2723,f2764])).
% 4.16/1.02 thf(f2768,definition,(
% 4.16/1.02 spl61_20 <=> ($true = ((ord_less @ extended_ereal @ sK53 @ (f @ x0))))),
% 4.16/1.02 introduced(definition,[new_symbols(definition,[spl61_20])],[avatar_definition])).
% 4.16/1.02 thf(f2770,plain,(
% 4.16/1.02 ($true = ((ord_less @ extended_ereal @ sK53 @ (f @ x0)))) | ~spl61_20),
% 4.16/1.02 inference(avatar_component_clause,[],[f2768])).
% 4.16/1.02 thf(f2771,plain,(
% 4.16/1.02 spl61_20 | spl61_10 | spl61_6 | spl61_17),
% 4.16/1.02 inference(avatar_split_clause,[],[f2710,f2755,f2684,f2723,f2768])).
% 4.16/1.02 thf(f2773,definition,(
% 4.16/1.02 spl61_21 <=> ! [X1 : set @ a] : (($true = ((member @ a @ (sK54 @ X1) @ X1))) | (((topolo1751647064n_open @ a @ X1)) = $false) | (((member @ a @ x0 @ X1)) = $false))),
% 4.16/1.02 introduced(definition,[new_symbols(definition,[spl61_21])],[avatar_definition])).
% 4.16/1.02 thf(f2774,plain,(
% 4.16/1.02 ( ! [X1 : set @ a] : (($true = ((member @ a @ (sK54 @ X1) @ X1))) | (((member @ a @ x0 @ X1)) = $false) | (((topolo1751647064n_open @ a @ X1)) = $false)) ) | ~spl61_21),
% 4.16/1.02 inference(avatar_component_clause,[],[f2773])).
% 4.16/1.02 thf(f2775,plain,(
% 4.16/1.02 spl61_21 | spl61_10 | spl61_6 | spl61_17),
% 4.16/1.02 inference(avatar_split_clause,[],[f2711,f2755,f2684,f2723,f2773])).
% 4.16/1.02 thf(f2777,definition,(
% 4.16/1.02 spl61_22 <=> ! [X1 : set @ a] : (($false = ((ord_less @ extended_ereal @ sK53 @ (f @ (sK54 @ X1))))) | (((topolo1751647064n_open @ a @ X1)) = $false) | (((member @ a @ x0 @ X1)) = $false))),
% 4.16/1.02 introduced(definition,[new_symbols(definition,[spl61_22])],[avatar_definition])).
% 4.16/1.02 thf(f2778,plain,(
% 4.16/1.02 ( ! [X1 : set @ a] : (($false = ((ord_less @ extended_ereal @ sK53 @ (f @ (sK54 @ X1))))) | (((topolo1751647064n_open @ a @ X1)) = $false) | (((member @ a @ x0 @ X1)) = $false)) ) | ~spl61_22),
% 4.16/1.02 inference(avatar_component_clause,[],[f2777])).
% 4.16/1.02 thf(f2779,plain,(
% 4.16/1.02 spl61_22 | spl61_10 | spl61_6 | spl61_17),
% 4.16/1.02 inference(avatar_split_clause,[],[f2712,f2755,f2684,f2723,f2777])).
% 4.16/1.02 thf(f2793,definition,(
% 4.16/1.02 spl61_26 <=> ($true = ((ord_less @ extended_ereal @ sK56 @ (f @ x0))))),
% 4.16/1.02 introduced(definition,[new_symbols(definition,[spl61_26])],[avatar_definition])).
% 4.16/1.02 thf(f2795,plain,(
% 4.16/1.02 ($true = ((ord_less @ extended_ereal @ sK56 @ (f @ x0)))) | ~spl61_26),
% 4.16/1.02 inference(avatar_component_clause,[],[f2793])).
% 4.16/1.02 thf(f2796,plain,(
% 4.16/1.02 spl61_26 | spl61_6 | ~spl61_17),
% 4.16/1.02 inference(avatar_split_clause,[],[f2716,f2755,f2684,f2793])).
% 4.16/1.02 thf(f2805,plain,(
% 4.16/1.02 ($true = $false) | (~spl61_2 | ~spl61_6)),
% 4.16/1.02 inference(forward_demodulation,[],[f2686,f2670])).
% 4.16/1.02 thf(f2806,plain,(
% 4.16/1.02 $false | (~spl61_2 | ~spl61_6)),
% 4.16/1.02 inference(trivial_inequality_removal,[],[f2805])).
% 4.16/1.02 thf(f2807,plain,(
% 4.16/1.02 ~spl61_2 | ~spl61_6),
% 4.16/1.02 inference(avatar_contradiction_clause,[],[f2806])).
% 4.16/1.02 thf(f2809,plain,(
% 4.16/1.02 ($true = ((ord_less @ extended_ereal @ sK59 @ extend1396239628finity @ extended_ereal))) | (~spl61_10 | ~spl61_13)),
% 4.16/1.02 inference(forward_demodulation,[],[f2738,f2724])).
% 4.16/1.02 thf(f2819,plain,(
% 4.16/1.02 ( ! [X0 : extended_ereal] : (($true = ((member @ a @ x0 @ (sK49 @ X0)))) | (((ord_less @ extended_ereal @ X0 @ extend1396239628finity @ extended_ereal)) = $false)) ) | (~spl61_7 | ~spl61_10)),
% 4.16/1.02 inference(constrained_superposition,[],[f2690,f2724])).
% 4.16/1.02 thf(f2820,plain,(
% 4.16/1.02 ( ! [X0 : extended_ereal] : ((((ord_less @ extended_ereal @ X0 @ extend1396239628finity @ extended_ereal)) = $false) | ($true = ((topolo1751647064n_open @ a @ (sK49 @ X0))))) ) | (~spl61_5 | ~spl61_10)),
% 4.16/1.02 inference(constrained_superposition,[],[f2682,f2724])).
% 4.16/1.02 thf(f2823,plain,(
% 4.16/1.02 ($true = $false) | ($true = ((topolo1751647064n_open @ a @ (sK49 @ sK59)))) | (~spl61_5 | ~spl61_10 | ~spl61_13)),
% 4.16/1.02 inference(constrained_superposition,[],[f2809,f2820])).
% 4.16/1.02 thf(f2824,plain,(
% 4.16/1.02 ($true = ((topolo1751647064n_open @ a @ (sK49 @ sK59)))) | (~spl61_5 | ~spl61_10 | ~spl61_13)),
% 4.16/1.02 inference(trivial_inequality_removal,[],[f2823])).
% 4.16/1.02 thf(f2827,plain,(
% 4.16/1.02 ( ! [X0 : set @ a] : (($true = $false) | ($false = ((ord_less @ extended_ereal @ sK59 @ (f @ x0)))) | ($false = ((member @ a @ (sK60 @ X0) @ (sK49 @ sK59)))) | ($false = ((topolo1751647064n_open @ a @ X0))) | ($false = ((member @ a @ x0 @ X0)))) ) | (~spl61_8 | ~spl61_15)),
% 4.16/1.02 inference(constrained_superposition,[],[f2694,f2746])).
% 4.16/1.02 thf(f2828,plain,(
% 4.16/1.02 ( ! [X0 : set @ a] : (($false = ((ord_less @ extended_ereal @ sK59 @ (f @ x0)))) | ($false = ((member @ a @ (sK60 @ X0) @ (sK49 @ sK59)))) | ($false = ((topolo1751647064n_open @ a @ X0))) | ($false = ((member @ a @ x0 @ X0)))) ) | (~spl61_8 | ~spl61_15)),
% 4.16/1.02 inference(trivial_inequality_removal,[],[f2827])).
% 4.16/1.02 thf(f2830,plain,(
% 4.16/1.02 ( ! [X0 : set @ a] : (($false = ((ord_less @ extended_ereal @ sK59 @ extend1396239628finity @ extended_ereal))) | ($false = ((member @ a @ (sK60 @ X0) @ (sK49 @ sK59)))) | ($false = ((topolo1751647064n_open @ a @ X0))) | ($false = ((member @ a @ x0 @ X0)))) ) | (~spl61_8 | ~spl61_10 | ~spl61_15)),
% 4.16/1.02 inference(forward_demodulation,[],[f2828,f2724])).
% 4.16/1.02 thf(f2832,plain,(
% 4.16/1.02 ( ! [X0 : set @ a] : (($true = $false) | ($false = ((member @ a @ (sK60 @ X0) @ (sK49 @ sK59)))) | ($false = ((topolo1751647064n_open @ a @ X0))) | ($false = ((member @ a @ x0 @ X0)))) ) | (~spl61_8 | ~spl61_10 | ~spl61_13 | ~spl61_15)),
% 4.16/1.02 inference(forward_demodulation,[],[f2830,f2809])).
% 4.16/1.02 thf(f2833,plain,(
% 4.16/1.02 ( ! [X0 : set @ a] : (($false = ((member @ a @ x0 @ X0))) | ($false = ((topolo1751647064n_open @ a @ X0))) | ($false = ((member @ a @ (sK60 @ X0) @ (sK49 @ sK59))))) ) | (~spl61_8 | ~spl61_10 | ~spl61_13 | ~spl61_15)),
% 4.16/1.02 inference(trivial_inequality_removal,[],[f2832])).
% 4.16/1.02 thf(f2837,plain,(
% 4.16/1.02 ( ! [X0 : extended_ereal] : (($true = $false) | ($true = ((member @ a @ (sK60 @ (sK49 @ X0)) @ (sK49 @ X0)))) | ($false = ((topolo1751647064n_open @ a @ (sK49 @ X0)))) | (((ord_less @ extended_ereal @ X0 @ extend1396239628finity @ extended_ereal)) = $false)) ) | (~spl61_7 | ~spl61_10 | ~spl61_14)),
% 4.16/1.02 inference(constrained_superposition,[],[f2742,f2819])).
% 4.16/1.02 thf(f2838,plain,(
% 4.16/1.02 ( ! [X0 : extended_ereal] : (($true = ((member @ a @ (sK60 @ (sK49 @ X0)) @ (sK49 @ X0)))) | ($false = ((topolo1751647064n_open @ a @ (sK49 @ X0)))) | (((ord_less @ extended_ereal @ X0 @ extend1396239628finity @ extended_ereal)) = $false)) ) | (~spl61_7 | ~spl61_10 | ~spl61_14)),
% 4.16/1.02 inference(trivial_inequality_removal,[],[f2837])).
% 4.16/1.02 thf(f2841,plain,(
% 4.16/1.02 ( ! [X0 : extended_ereal] : (($true = $false) | (((ord_less @ extended_ereal @ X0 @ extend1396239628finity @ extended_ereal)) = $false) | ($false = ((topolo1751647064n_open @ a @ (sK49 @ X0)))) | ($false = ((member @ a @ (sK60 @ (sK49 @ X0)) @ (sK49 @ sK59))))) ) | (~spl61_7 | ~spl61_8 | ~spl61_10 | ~spl61_13 | ~spl61_15)),
% 4.16/1.02 inference(constrained_superposition,[],[f2819,f2833])).
% 4.16/1.02 thf(f2842,plain,(
% 4.16/1.02 ( ! [X0 : extended_ereal] : (($false = ((member @ a @ (sK60 @ (sK49 @ X0)) @ (sK49 @ sK59)))) | ($false = ((topolo1751647064n_open @ a @ (sK49 @ X0)))) | (((ord_less @ extended_ereal @ X0 @ extend1396239628finity @ extended_ereal)) = $false)) ) | (~spl61_7 | ~spl61_8 | ~spl61_10 | ~spl61_13 | ~spl61_15)),
% 4.16/1.02 inference(trivial_inequality_removal,[],[f2841])).
% 4.16/1.02 thf(f2862,plain,(
% 4.16/1.02 ($true = $false) | ($false = ((topolo1751647064n_open @ a @ (sK49 @ sK59)))) | ($false = ((ord_less @ extended_ereal @ sK59 @ extend1396239628finity @ extended_ereal))) | ($false = ((topolo1751647064n_open @ a @ (sK49 @ sK59)))) | ($false = ((ord_less @ extended_ereal @ sK59 @ extend1396239628finity @ extended_ereal))) | (~spl61_7 | ~spl61_8 | ~spl61_10 | ~spl61_13 | ~spl61_14 | ~spl61_15)),
% 4.16/1.02 inference(constrained_superposition,[],[f2838,f2842])).
% 4.16/1.02 thf(f2863,plain,(
% 4.16/1.02 ($true = $false) | ($false = ((topolo1751647064n_open @ a @ (sK49 @ sK59)))) | ($false = ((ord_less @ extended_ereal @ sK59 @ extend1396239628finity @ extended_ereal))) | (~spl61_7 | ~spl61_8 | ~spl61_10 | ~spl61_13 | ~spl61_14 | ~spl61_15)),
% 4.16/1.02 inference(duplicate_literal_removal,[],[f2862])).
% 4.16/1.02 thf(f2864,plain,(
% 4.16/1.02 ($false = ((topolo1751647064n_open @ a @ (sK49 @ sK59)))) | ($false = ((ord_less @ extended_ereal @ sK59 @ extend1396239628finity @ extended_ereal))) | (~spl61_7 | ~spl61_8 | ~spl61_10 | ~spl61_13 | ~spl61_14 | ~spl61_15)),
% 4.16/1.02 inference(trivial_inequality_removal,[],[f2863])).
% 4.16/1.02 thf(f2867,plain,(
% 4.16/1.02 ($true = $false) | ($false = ((ord_less @ extended_ereal @ sK59 @ extend1396239628finity @ extended_ereal))) | (~spl61_5 | ~spl61_7 | ~spl61_8 | ~spl61_10 | ~spl61_13 | ~spl61_14 | ~spl61_15)),
% 4.16/1.02 inference(forward_demodulation,[],[f2864,f2824])).
% 4.16/1.02 thf(f2868,plain,(
% 4.16/1.02 ($false = ((ord_less @ extended_ereal @ sK59 @ extend1396239628finity @ extended_ereal))) | (~spl61_5 | ~spl61_7 | ~spl61_8 | ~spl61_10 | ~spl61_13 | ~spl61_14 | ~spl61_15)),
% 4.16/1.02 inference(trivial_inequality_removal,[],[f2867])).
% 4.16/1.02 thf(f2871,plain,(
% 4.16/1.02 ($true = $false) | (~spl61_5 | ~spl61_7 | ~spl61_8 | ~spl61_10 | ~spl61_13 | ~spl61_14 | ~spl61_15)),
% 4.16/1.02 inference(constrained_superposition,[],[f2868,f2809])).
% 4.16/1.02 thf(f2875,plain,(
% 4.16/1.02 $false | (~spl61_5 | ~spl61_7 | ~spl61_8 | ~spl61_10 | ~spl61_13 | ~spl61_14 | ~spl61_15)),
% 4.16/1.02 inference(trivial_inequality_removal,[],[f2871])).
% 4.16/1.02 thf(f2876,plain,(
% 4.16/1.02 ~spl61_5 | ~spl61_7 | ~spl61_8 | ~spl61_10 | ~spl61_13 | ~spl61_14 | ~spl61_15),
% 4.16/1.02 inference(avatar_contradiction_clause,[],[f2875])).
% 4.16/1.02 thf(f2893,plain,(
% 4.16/1.02 ($true = $false) | ($true = ((member @ a @ x0 @ (sK49 @ sK53)))) | (~spl61_7 | ~spl61_20)),
% 4.16/1.02 inference(constrained_superposition,[],[f2770,f2690])).
% 4.16/1.02 thf(f2894,plain,(
% 4.16/1.02 ($true = $false) | ($true = ((topolo1751647064n_open @ a @ (sK49 @ sK53)))) | (~spl61_5 | ~spl61_20)),
% 4.16/1.02 inference(constrained_superposition,[],[f2770,f2682])).
% 4.16/1.02 thf(f3023,plain,(
% 4.16/1.02 ( ! [X0 : a] : (($true = $false) | ($true = ((ord_less @ extended_ereal @ sK47 @ (f @ X0)))) | ($false = ((member @ a @ X0 @ (sK52 @ sK47))))) ) | (~spl61_1 | ~spl61_19)),
% 4.16/1.02 inference(constrained_superposition,[],[f2666,f2765])).
% 4.16/1.02 thf(f3033,plain,(
% 4.16/1.02 ( ! [X0 : a] : (($true = ((ord_less @ extended_ereal @ sK47 @ (f @ X0)))) | ($false = ((member @ a @ X0 @ (sK52 @ sK47))))) ) | (~spl61_1 | ~spl61_19)),
% 4.16/1.02 inference(trivial_inequality_removal,[],[f3023])).
% 4.16/1.02 thf(f3131,definition,(
% 4.16/1.02 spl61_40 <=> ($false = ((ord_less @ extended_ereal @ sK53 @ (f @ x0))))),
% 4.16/1.02 introduced(definition,[new_symbols(definition,[spl61_40])],[avatar_definition])).
% 4.16/1.02 thf(f3132,plain,(
% 4.16/1.02 ($false != ((ord_less @ extended_ereal @ sK53 @ (f @ x0)))) | spl61_40),
% 4.16/1.02 inference(avatar_component_clause,[],[f3131])).
% 4.16/1.02 thf(f3133,plain,(
% 4.16/1.02 ($false = ((ord_less @ extended_ereal @ sK53 @ (f @ x0)))) | ~spl61_40),
% 4.16/1.02 inference(avatar_component_clause,[],[f3131])).
% 4.16/1.02 thf(f3151,plain,(
% 4.16/1.02 ( ! [X0 : set @ a] : (($true = $false) | ($false = ((member @ a @ (sK48 @ X0) @ (sK52 @ sK47)))) | ($false = ((topolo1751647064n_open @ a @ X0))) | ($false = ((member @ a @ x0 @ X0)))) ) | (~spl61_1 | ~spl61_4 | ~spl61_19)),
% 4.16/1.02 inference(constrained_superposition,[],[f3033,f2678])).
% 4.16/1.02 thf(f3154,plain,(
% 4.16/1.02 ( ! [X0 : set @ a] : (($false = ((member @ a @ x0 @ X0))) | ($false = ((topolo1751647064n_open @ a @ X0))) | ($false = ((member @ a @ (sK48 @ X0) @ (sK52 @ sK47))))) ) | (~spl61_1 | ~spl61_4 | ~spl61_19)),
% 4.16/1.02 inference(trivial_inequality_removal,[],[f3151])).
% 4.16/1.02 thf(f3176,plain,(
% 4.16/1.02 ($true = $false) | ($true = ((topolo1751647064n_open @ a @ (sK52 @ sK47)))) | (~spl61_1 | ~spl61_16)),
% 4.16/1.02 inference(constrained_superposition,[],[f2666,f2753])).
% 4.16/1.02 thf(f3186,plain,(
% 4.16/1.02 ($true = ((topolo1751647064n_open @ a @ (sK52 @ sK47)))) | (~spl61_1 | ~spl61_16)),
% 4.16/1.02 inference(trivial_inequality_removal,[],[f3176])).
% 4.16/1.02 thf(f3199,definition,(
% 4.16/1.02 spl61_42 <=> ($true = ((topolo1751647064n_open @ a @ (sK52 @ sK47))))),
% 4.16/1.02 introduced(definition,[new_symbols(definition,[spl61_42])],[avatar_definition])).
% 4.16/1.02 thf(f3201,plain,(
% 4.16/1.02 ($true = ((topolo1751647064n_open @ a @ (sK52 @ sK47)))) | ~spl61_42),
% 4.16/1.02 inference(avatar_component_clause,[],[f3199])).
% 4.16/1.02 thf(f3207,plain,(
% 4.16/1.02 spl61_42 | ~spl61_1 | ~spl61_16),
% 4.16/1.02 inference(avatar_split_clause,[],[f3186,f2752,f2664,f3199])).
% 4.16/1.02 thf(f3219,plain,(
% 4.16/1.02 ($true = $false) | ($true = ((member @ a @ x0 @ (sK52 @ sK47)))) | (~spl61_1 | ~spl61_18)),
% 4.16/1.02 inference(constrained_superposition,[],[f2666,f2761])).
% 4.16/1.02 thf(f3229,plain,(
% 4.16/1.02 ($true = ((member @ a @ x0 @ (sK52 @ sK47)))) | (~spl61_1 | ~spl61_18)),
% 4.16/1.02 inference(trivial_inequality_removal,[],[f3219])).
% 4.16/1.02 thf(f3247,plain,(
% 4.16/1.02 ($true = $false) | ($true = ((member @ a @ (sK48 @ (sK52 @ sK47)) @ (sK52 @ sK47)))) | ($false = ((topolo1751647064n_open @ a @ (sK52 @ sK47)))) | (~spl61_1 | ~spl61_3 | ~spl61_18)),
% 4.16/1.02 inference(constrained_superposition,[],[f2674,f3229])).
% 4.16/1.02 thf(f3252,plain,(
% 4.16/1.02 ($true = ((member @ a @ (sK48 @ (sK52 @ sK47)) @ (sK52 @ sK47)))) | ($false = ((topolo1751647064n_open @ a @ (sK52 @ sK47)))) | (~spl61_1 | ~spl61_3 | ~spl61_18)),
% 4.16/1.02 inference(trivial_inequality_removal,[],[f3247])).
% 4.16/1.02 thf(f3262,plain,(
% 4.16/1.02 ($true = $false) | ($true = ((member @ a @ (sK48 @ (sK52 @ sK47)) @ (sK52 @ sK47)))) | (~spl61_1 | ~spl61_3 | ~spl61_18 | ~spl61_42)),
% 4.16/1.02 inference(forward_demodulation,[],[f3252,f3201])).
% 4.16/1.02 thf(f3263,plain,(
% 4.16/1.02 ($true = ((member @ a @ (sK48 @ (sK52 @ sK47)) @ (sK52 @ sK47)))) | (~spl61_1 | ~spl61_3 | ~spl61_18 | ~spl61_42)),
% 4.16/1.02 inference(trivial_inequality_removal,[],[f3262])).
% 4.16/1.02 thf(f3317,plain,(
% 4.16/1.02 ( ! [X0 : set @ a] : (($true = $false) | ($false = ((ord_less @ extended_ereal @ sK53 @ (f @ x0)))) | ($false = ((member @ a @ (sK54 @ X0) @ (sK49 @ sK53)))) | ($false = ((topolo1751647064n_open @ a @ X0))) | ($false = ((member @ a @ x0 @ X0)))) ) | (~spl61_8 | ~spl61_22)),
% 4.16/1.02 inference(constrained_superposition,[],[f2694,f2778])).
% 4.16/1.02 thf(f3318,plain,(
% 4.16/1.02 ( ! [X0 : set @ a] : (($false = ((ord_less @ extended_ereal @ sK53 @ (f @ x0)))) | ($false = ((member @ a @ (sK54 @ X0) @ (sK49 @ sK53)))) | ($false = ((topolo1751647064n_open @ a @ X0))) | ($false = ((member @ a @ x0 @ X0)))) ) | (~spl61_8 | ~spl61_22)),
% 4.16/1.02 inference(trivial_inequality_removal,[],[f3317])).
% 4.16/1.02 thf(f3327,plain,(
% 4.16/1.02 ($true = $false) | ($false = ((topolo1751647064n_open @ a @ (sK52 @ sK47)))) | ($false = ((member @ a @ (sK48 @ (sK52 @ sK47)) @ (sK52 @ sK47)))) | (~spl61_1 | ~spl61_4 | ~spl61_18 | ~spl61_19)),
% 4.16/1.02 inference(constrained_superposition,[],[f3229,f3154])).
% 4.16/1.02 thf(f3328,plain,(
% 4.16/1.02 ($false = ((topolo1751647064n_open @ a @ (sK52 @ sK47)))) | ($false = ((member @ a @ (sK48 @ (sK52 @ sK47)) @ (sK52 @ sK47)))) | (~spl61_1 | ~spl61_4 | ~spl61_18 | ~spl61_19)),
% 4.16/1.02 inference(trivial_inequality_removal,[],[f3327])).
% 4.16/1.02 thf(f3334,plain,(
% 4.16/1.02 ($true = $false) | ($false = ((member @ a @ (sK48 @ (sK52 @ sK47)) @ (sK52 @ sK47)))) | (~spl61_1 | ~spl61_4 | ~spl61_18 | ~spl61_19 | ~spl61_42)),
% 4.16/1.02 inference(forward_demodulation,[],[f3328,f3201])).
% 4.16/1.02 thf(f3335,plain,(
% 4.16/1.02 ($false = ((member @ a @ (sK48 @ (sK52 @ sK47)) @ (sK52 @ sK47)))) | (~spl61_1 | ~spl61_4 | ~spl61_18 | ~spl61_19 | ~spl61_42)),
% 4.16/1.02 inference(trivial_inequality_removal,[],[f3334])).
% 4.16/1.02 thf(f3386,plain,(
% 4.16/1.02 ($true = $false) | (~spl61_1 | ~spl61_3 | ~spl61_4 | ~spl61_18 | ~spl61_19 | ~spl61_42)),
% 4.16/1.02 inference(constrained_superposition,[],[f3335,f3263])).
% 4.16/1.02 thf(f3390,plain,(
% 4.16/1.02 $false | (~spl61_1 | ~spl61_3 | ~spl61_4 | ~spl61_18 | ~spl61_19 | ~spl61_42)),
% 4.16/1.02 inference(trivial_inequality_removal,[],[f3386])).
% 4.16/1.02 thf(f3391,plain,(
% 4.16/1.02 ~spl61_1 | ~spl61_3 | ~spl61_4 | ~spl61_18 | ~spl61_19 | ~spl61_42),
% 4.16/1.02 inference(avatar_contradiction_clause,[],[f3390])).
% 4.16/1.02 thf(f3550,plain,(
% 4.16/1.02 ($true = ((ord_less @ extended_ereal @ sK47 @ extended_MInfty))) | (~spl61_1 | ~spl61_17)),
% 4.16/1.02 inference(constrained_superposition,[],[f2666,f2757])).
% 4.16/1.02 thf(f3561,plain,(
% 4.16/1.02 $false | (~spl61_1 | ~spl61_17)),
% 4.16/1.02 inference(forward_subsumption_resolution,[],[f3550,f2702])).
% 4.16/1.02 thf(f3562,plain,(
% 4.16/1.02 ~spl61_1 | ~spl61_17),
% 4.16/1.02 inference(avatar_contradiction_clause,[],[f3561])).
% 4.16/1.02 thf(f3574,plain,(
% 4.16/1.02 ($true = ((ord_less @ extended_ereal @ sK56 @ extended_MInfty))) | (~spl61_17 | ~spl61_26)),
% 4.16/1.02 inference(forward_demodulation,[],[f2795,f2757])).
% 4.16/1.02 thf(f3583,plain,(
% 4.16/1.02 $false | (~spl61_17 | ~spl61_26)),
% 4.16/1.02 inference(forward_subsumption_resolution,[],[f3574,f2702])).
% 4.16/1.02 thf(f3584,plain,(
% 4.16/1.02 ~spl61_17 | ~spl61_26),
% 4.16/1.02 inference(avatar_contradiction_clause,[],[f3583])).
% 4.16/1.02 thf(f3595,plain,(
% 4.16/1.02 ($true = ((member @ a @ x0 @ (sK49 @ sK53)))) | (~spl61_7 | ~spl61_20)),
% 4.16/1.02 inference(trivial_inequality_removal,[],[f2893])).
% 4.16/1.02 thf(f3596,plain,(
% 4.16/1.02 ($true = ((topolo1751647064n_open @ a @ (sK49 @ sK53)))) | (~spl61_5 | ~spl61_20)),
% 4.16/1.02 inference(trivial_inequality_removal,[],[f2894])).
% 4.16/1.02 thf(f3610,plain,(
% 4.16/1.02 ($true = $false) | (~spl61_20 | ~spl61_40)),
% 4.16/1.02 inference(forward_demodulation,[],[f2770,f3133])).
% 4.16/1.02 thf(f3611,plain,(
% 4.16/1.02 $false | (~spl61_20 | ~spl61_40)),
% 4.16/1.02 inference(trivial_inequality_removal,[],[f3610])).
% 4.16/1.02 thf(f3612,plain,(
% 4.16/1.02 ~spl61_20 | ~spl61_40),
% 4.16/1.02 inference(avatar_contradiction_clause,[],[f3611])).
% 4.16/1.02 thf(f3629,definition,(
% 4.16/1.02 spl61_69 <=> ($false = ((ord_less @ extended_ereal @ sK47 @ (f @ x0))))),
% 4.16/1.02 introduced(definition,[new_symbols(definition,[spl61_69])],[avatar_definition])).
% 4.16/1.02 thf(f3630,plain,(
% 4.16/1.02 ($false != ((ord_less @ extended_ereal @ sK47 @ (f @ x0)))) | spl61_69),
% 4.16/1.02 inference(avatar_component_clause,[],[f3629])).
% 4.16/1.02 thf(f3631,plain,(
% 4.16/1.02 ($false = ((ord_less @ extended_ereal @ sK47 @ (f @ x0)))) | ~spl61_69),
% 4.16/1.02 inference(avatar_component_clause,[],[f3629])).
% 4.16/1.02 thf(f3640,plain,(
% 4.16/1.02 ( ! [X0 : set @ a] : (($false = ((member @ a @ x0 @ X0))) | ($false = ((topolo1751647064n_open @ a @ X0))) | ($false = ((member @ a @ (sK54 @ X0) @ (sK49 @ sK53))))) ) | (~spl61_8 | ~spl61_22 | spl61_40)),
% 4.16/1.02 inference(forward_subsumption_resolution,[],[f3318,f3132])).
% 4.16/1.02 thf(f3798,plain,(
% 4.16/1.02 ($true = $false) | ($true = ((member @ a @ (sK54 @ (sK49 @ sK53)) @ (sK49 @ sK53)))) | ($false = ((topolo1751647064n_open @ a @ (sK49 @ sK53)))) | (~spl61_7 | ~spl61_20 | ~spl61_21)),
% 4.16/1.02 inference(constrained_superposition,[],[f2774,f3595])).
% 4.16/1.02 thf(f3803,plain,(
% 4.16/1.02 ($true = ((member @ a @ (sK54 @ (sK49 @ sK53)) @ (sK49 @ sK53)))) | ($false = ((topolo1751647064n_open @ a @ (sK49 @ sK53)))) | (~spl61_7 | ~spl61_20 | ~spl61_21)),
% 4.16/1.02 inference(trivial_inequality_removal,[],[f3798])).
% 4.16/1.02 thf(f3807,plain,(
% 4.16/1.02 ($true = $false) | ($true = ((member @ a @ (sK54 @ (sK49 @ sK53)) @ (sK49 @ sK53)))) | (~spl61_5 | ~spl61_7 | ~spl61_20 | ~spl61_21)),
% 4.16/1.02 inference(forward_demodulation,[],[f3803,f3596])).
% 4.16/1.02 thf(f3808,plain,(
% 4.16/1.02 ($true = ((member @ a @ (sK54 @ (sK49 @ sK53)) @ (sK49 @ sK53)))) | (~spl61_5 | ~spl61_7 | ~spl61_20 | ~spl61_21)),
% 4.16/1.02 inference(trivial_inequality_removal,[],[f3807])).
% 4.16/1.02 thf(f3926,plain,(
% 4.16/1.02 ($true = $false) | ($false = ((topolo1751647064n_open @ a @ (sK49 @ sK53)))) | ($false = ((member @ a @ (sK54 @ (sK49 @ sK53)) @ (sK49 @ sK53)))) | (~spl61_7 | ~spl61_8 | ~spl61_20 | ~spl61_22 | spl61_40)),
% 4.16/1.02 inference(constrained_superposition,[],[f3595,f3640])).
% 4.16/1.02 thf(f3927,plain,(
% 4.16/1.02 ($false = ((topolo1751647064n_open @ a @ (sK49 @ sK53)))) | ($false = ((member @ a @ (sK54 @ (sK49 @ sK53)) @ (sK49 @ sK53)))) | (~spl61_7 | ~spl61_8 | ~spl61_20 | ~spl61_22 | spl61_40)),
% 4.16/1.02 inference(trivial_inequality_removal,[],[f3926])).
% 4.16/1.02 thf(f3929,plain,(
% 4.16/1.02 ($true = $false) | ($false = ((member @ a @ (sK54 @ (sK49 @ sK53)) @ (sK49 @ sK53)))) | (~spl61_5 | ~spl61_7 | ~spl61_8 | ~spl61_20 | ~spl61_22 | spl61_40)),
% 4.16/1.02 inference(forward_demodulation,[],[f3927,f3596])).
% 4.16/1.02 thf(f3930,plain,(
% 4.16/1.02 ($false = ((member @ a @ (sK54 @ (sK49 @ sK53)) @ (sK49 @ sK53)))) | (~spl61_5 | ~spl61_7 | ~spl61_8 | ~spl61_20 | ~spl61_22 | spl61_40)),
% 4.16/1.02 inference(trivial_inequality_removal,[],[f3929])).
% 4.16/1.02 thf(f3941,plain,(
% 4.16/1.02 ($true = $false) | (~spl61_5 | ~spl61_7 | ~spl61_8 | ~spl61_20 | ~spl61_21 | ~spl61_22 | spl61_40)),
% 4.16/1.02 inference(constrained_superposition,[],[f3930,f3808])).
% 4.16/1.02 thf(f3945,plain,(
% 4.16/1.02 $false | (~spl61_5 | ~spl61_7 | ~spl61_8 | ~spl61_20 | ~spl61_21 | ~spl61_22 | spl61_40)),
% 4.16/1.02 inference(trivial_inequality_removal,[],[f3941])).
% 4.16/1.02 thf(f3946,plain,(
% 4.16/1.02 ~spl61_5 | ~spl61_7 | ~spl61_8 | ~spl61_20 | ~spl61_21 | ~spl61_22 | spl61_40),
% 4.16/1.02 inference(avatar_contradiction_clause,[],[f3945])).
% 4.16/1.02 thf(f3978,plain,(
% 4.16/1.02 ($true = $false) | (~spl61_1 | ~spl61_69)),
% 4.16/1.02 inference(forward_demodulation,[],[f2666,f3631])).
% 4.16/1.02 thf(f3979,plain,(
% 4.16/1.02 $false | (~spl61_1 | ~spl61_69)),
% 4.16/1.02 inference(trivial_inequality_removal,[],[f3978])).
% 4.16/1.02 thf(f3980,plain,(
% 4.16/1.02 ~spl61_1 | ~spl61_69),
% 4.16/1.02 inference(avatar_contradiction_clause,[],[f3979])).
% 4.16/1.02 thf(f3983,plain,(
% 4.16/1.02 ( ! [X1 : extended_ereal] : (($true = ((member @ a @ x0 @ (sK58 @ X1)))) | (((ord_less @ extended_ereal @ X1 @ extend1396239628finity @ extended_ereal)) = $false)) ) | (~spl61_10 | ~spl61_11)),
% 4.16/1.02 inference(forward_demodulation,[],[f2729,f2724])).
% 4.16/1.02 thf(f3984,plain,(
% 4.16/1.02 ( ! [X2 : a,X1 : extended_ereal] : (($true = ((ord_less @ extended_ereal @ X1 @ (f @ X2)))) | (((ord_less @ extended_ereal @ X1 @ extend1396239628finity @ extended_ereal)) = $false) | ($false = ((member @ a @ X2 @ (sK58 @ X1))))) ) | (~spl61_10 | ~spl61_12)),
% 4.16/1.02 inference(forward_demodulation,[],[f2733,f2724])).
% 4.16/1.02 thf(f3985,plain,(
% 4.16/1.02 ($false != ((ord_less @ extended_ereal @ sK47 @ extend1396239628finity @ extended_ereal))) | (~spl61_10 | spl61_69)),
% 4.16/1.02 inference(forward_demodulation,[],[f3630,f2724])).
% 4.16/1.02 thf(f4013,plain,(
% 4.16/1.02 ( ! [X0 : set @ a] : (($true = $false) | ($false = ((topolo1751647064n_open @ a @ X0))) | ($false = ((member @ a @ x0 @ X0))) | ($false = ((ord_less @ extended_ereal @ sK47 @ extend1396239628finity @ extended_ereal))) | ($false = ((member @ a @ (sK48 @ X0) @ (sK58 @ sK47))))) ) | (~spl61_4 | ~spl61_10 | ~spl61_12)),
% 4.16/1.02 inference(constrained_superposition,[],[f2678,f3984])).
% 4.16/1.02 thf(f4021,plain,(
% 4.16/1.02 ( ! [X0 : set @ a] : (($false = ((topolo1751647064n_open @ a @ X0))) | ($false = ((member @ a @ x0 @ X0))) | ($false = ((ord_less @ extended_ereal @ sK47 @ extend1396239628finity @ extended_ereal))) | ($false = ((member @ a @ (sK48 @ X0) @ (sK58 @ sK47))))) ) | (~spl61_4 | ~spl61_10 | ~spl61_12)),
% 4.16/1.02 inference(trivial_inequality_removal,[],[f4013])).
% 4.16/1.02 thf(f4055,plain,(
% 4.16/1.02 ( ! [X0 : set @ a] : (($false = ((member @ a @ x0 @ X0))) | ($false = ((topolo1751647064n_open @ a @ X0))) | ($false = ((member @ a @ (sK48 @ X0) @ (sK58 @ sK47))))) ) | (~spl61_4 | ~spl61_10 | ~spl61_12 | spl61_69)),
% 4.16/1.02 inference(forward_subsumption_resolution,[],[f4021,f3985])).
% 4.16/1.02 thf(f4210,plain,(
% 4.16/1.02 ( ! [X0 : extended_ereal] : ((((ord_less @ extended_ereal @ X0 @ extend1396239628finity @ extended_ereal)) = $false) | ($true = ((topolo1751647064n_open @ a @ (sK58 @ X0))))) ) | (~spl61_9 | ~spl61_10)),
% 4.16/1.02 inference(constrained_superposition,[],[f2721,f2724])).
% 4.16/1.02 thf(f4262,plain,(
% 4.16/1.02 ( ! [X0 : extended_ereal] : (($true = $false) | ($true = ((member @ a @ (sK48 @ (sK58 @ X0)) @ (sK58 @ X0)))) | ($false = ((topolo1751647064n_open @ a @ (sK58 @ X0)))) | (((ord_less @ extended_ereal @ X0 @ extend1396239628finity @ extended_ereal)) = $false)) ) | (~spl61_3 | ~spl61_10 | ~spl61_11)),
% 4.16/1.02 inference(constrained_superposition,[],[f2674,f3983])).
% 4.16/1.02 thf(f4265,plain,(
% 4.16/1.02 ( ! [X0 : extended_ereal] : (($true = ((member @ a @ (sK48 @ (sK58 @ X0)) @ (sK58 @ X0)))) | ($false = ((topolo1751647064n_open @ a @ (sK58 @ X0)))) | (((ord_less @ extended_ereal @ X0 @ extend1396239628finity @ extended_ereal)) = $false)) ) | (~spl61_3 | ~spl61_10 | ~spl61_11)),
% 4.16/1.02 inference(trivial_inequality_removal,[],[f4262])).
% 4.16/1.02 thf(f4652,plain,(
% 4.16/1.02 ( ! [X0 : extended_ereal] : (($true = $false) | (((ord_less @ extended_ereal @ X0 @ extend1396239628finity @ extended_ereal)) = $false) | ($false = ((topolo1751647064n_open @ a @ (sK58 @ X0)))) | ($false = ((member @ a @ (sK48 @ (sK58 @ X0)) @ (sK58 @ sK47))))) ) | (~spl61_4 | ~spl61_10 | ~spl61_11 | ~spl61_12 | spl61_69)),
% 4.16/1.02 inference(constrained_superposition,[],[f3983,f4055])).
% 4.16/1.02 thf(f4653,plain,(
% 4.16/1.02 ( ! [X0 : extended_ereal] : (($false = ((member @ a @ (sK48 @ (sK58 @ X0)) @ (sK58 @ sK47)))) | ($false = ((topolo1751647064n_open @ a @ (sK58 @ X0)))) | (((ord_less @ extended_ereal @ X0 @ extend1396239628finity @ extended_ereal)) = $false)) ) | (~spl61_4 | ~spl61_10 | ~spl61_11 | ~spl61_12 | spl61_69)),
% 4.16/1.02 inference(trivial_inequality_removal,[],[f4652])).
% 4.16/1.02 thf(f4832,plain,(
% 4.16/1.02 ($true = $false) | ($false = ((topolo1751647064n_open @ a @ (sK58 @ sK47)))) | ($false = ((ord_less @ extended_ereal @ sK47 @ extend1396239628finity @ extended_ereal))) | ($false = ((topolo1751647064n_open @ a @ (sK58 @ sK47)))) | ($false = ((ord_less @ extended_ereal @ sK47 @ extend1396239628finity @ extended_ereal))) | (~spl61_3 | ~spl61_4 | ~spl61_10 | ~spl61_11 | ~spl61_12 | spl61_69)),
% 4.16/1.02 inference(constrained_superposition,[],[f4265,f4653])).
% 4.16/1.02 thf(f4833,plain,(
% 4.16/1.02 ($true = $false) | ($false = ((topolo1751647064n_open @ a @ (sK58 @ sK47)))) | ($false = ((ord_less @ extended_ereal @ sK47 @ extend1396239628finity @ extended_ereal))) | (~spl61_3 | ~spl61_4 | ~spl61_10 | ~spl61_11 | ~spl61_12 | spl61_69)),
% 4.16/1.02 inference(duplicate_literal_removal,[],[f4832])).
% 4.16/1.02 thf(f4834,plain,(
% 4.16/1.02 ($false = ((topolo1751647064n_open @ a @ (sK58 @ sK47)))) | ($false = ((ord_less @ extended_ereal @ sK47 @ extend1396239628finity @ extended_ereal))) | (~spl61_3 | ~spl61_4 | ~spl61_10 | ~spl61_11 | ~spl61_12 | spl61_69)),
% 4.16/1.02 inference(trivial_inequality_removal,[],[f4833])).
% 4.16/1.02 thf(f4837,plain,(
% 4.16/1.02 ($false = ((topolo1751647064n_open @ a @ (sK58 @ sK47)))) | (~spl61_3 | ~spl61_4 | ~spl61_10 | ~spl61_11 | ~spl61_12 | spl61_69)),
% 4.16/1.02 inference(forward_subsumption_resolution,[],[f4834,f3985])).
% 4.16/1.02 thf(f4874,plain,(
% 4.16/1.02 ($false != $false) | ($true = ((topolo1751647064n_open @ a @ (sK58 @ sK47)))) | (~spl61_9 | ~spl61_10 | spl61_69)),
% 4.16/1.02 inference(constrained_superposition,[],[f3985,f4210])).
% 4.16/1.02 thf(f4881,plain,(
% 4.16/1.02 ($true = ((topolo1751647064n_open @ a @ (sK58 @ sK47)))) | (~spl61_9 | ~spl61_10 | spl61_69)),
% 4.16/1.02 inference(trivial_inequality_removal,[],[f4874])).
% 4.16/1.02 thf(f4887,plain,(
% 4.16/1.02 ($true = $false) | (~spl61_3 | ~spl61_4 | ~spl61_9 | ~spl61_10 | ~spl61_11 | ~spl61_12 | spl61_69)),
% 4.16/1.02 inference(forward_demodulation,[],[f4881,f4837])).
% 4.16/1.02 thf(f4888,plain,(
% 4.16/1.02 $false | (~spl61_3 | ~spl61_4 | ~spl61_9 | ~spl61_10 | ~spl61_11 | ~spl61_12 | spl61_69)),
% 4.16/1.02 inference(trivial_inequality_removal,[],[f4887])).
% 4.16/1.02 thf(f4889,plain,(
% 4.16/1.02 ~spl61_3 | ~spl61_4 | ~spl61_9 | ~spl61_10 | ~spl61_11 | ~spl61_12 | spl61_69),
% 4.16/1.02 inference(avatar_contradiction_clause,[],[f4888])).
% 4.16/1.02 cnf(s1, plain, spl61_1 | spl61_2, inference(sat_conversion,[],[f2671])).
% 4.16/1.02 cnf(s2, plain, spl61_2 | spl61_3, inference(sat_conversion,[],[f2675])).
% 4.16/1.02 cnf(s3, plain, spl61_2 | spl61_4, inference(sat_conversion,[],[f2679])).
% 4.16/1.02 cnf(s4, plain, spl61_5 | spl61_6, inference(sat_conversion,[],[f2687])).
% 4.16/1.02 cnf(s5, plain, spl61_6 | spl61_7, inference(sat_conversion,[],[f2691])).
% 4.16/1.02 cnf(s6, plain, spl61_6 | spl61_8, inference(sat_conversion,[],[f2695])).
% 4.16/1.02 cnf(s7, plain, spl61_2 | spl61_9 | ~spl61_10, inference(sat_conversion,[],[f2726])).
% 4.16/1.02 cnf(s8, plain, spl61_2 | ~spl61_10 | spl61_11, inference(sat_conversion,[],[f2730])).
% 4.16/1.02 cnf(s9, plain, spl61_2 | ~spl61_10 | spl61_12, inference(sat_conversion,[],[f2734])).
% 4.16/1.02 cnf(s10, plain, spl61_6 | ~spl61_10 | spl61_13, inference(sat_conversion,[],[f2739])).
% 4.16/1.02 cnf(s11, plain, spl61_6 | ~spl61_10 | spl61_14, inference(sat_conversion,[],[f2743])).
% 4.16/1.02 cnf(s12, plain, spl61_6 | ~spl61_10 | spl61_15, inference(sat_conversion,[],[f2747])).
% 4.16/1.02 cnf(s13, plain, spl61_2 | spl61_10 | spl61_16 | spl61_17, inference(sat_conversion,[],[f2758])).
% 4.16/1.02 cnf(s14, plain, spl61_2 | spl61_10 | spl61_17 | spl61_18, inference(sat_conversion,[],[f2762])).
% 4.16/1.02 cnf(s15, plain, spl61_2 | spl61_10 | spl61_17 | spl61_19, inference(sat_conversion,[],[f2766])).
% 4.16/1.02 cnf(s16, plain, spl61_6 | spl61_10 | spl61_17 | spl61_20, inference(sat_conversion,[],[f2771])).
% 4.16/1.02 cnf(s17, plain, spl61_6 | spl61_10 | spl61_17 | spl61_21, inference(sat_conversion,[],[f2775])).
% 4.16/1.02 cnf(s18, plain, spl61_6 | spl61_10 | spl61_17 | spl61_22, inference(sat_conversion,[],[f2779])).
% 4.16/1.02 cnf(s22, plain, spl61_6 | ~spl61_17 | spl61_26, inference(sat_conversion,[],[f2796])).
% 4.16/1.02 cnf(s25, plain, ~spl61_2 | ~spl61_6, inference(sat_conversion,[],[f2807])).
% 4.16/1.02 cnf(s27, plain, ~spl61_5 | ~spl61_7 | ~spl61_8 | ~spl61_10 | ~spl61_13 | ~spl61_14 | ~spl61_15, inference(sat_conversion,[],[f2876])).
% 4.16/1.02 cnf(s47, plain, ~spl61_1 | ~spl61_16 | spl61_42, inference(sat_conversion,[],[f3207])).
% 4.16/1.02 cnf(s53, plain, ~spl61_1 | ~spl61_3 | ~spl61_4 | ~spl61_18 | ~spl61_19 | ~spl61_42, inference(sat_conversion,[],[f3391])).
% 4.16/1.02 cnf(s88, plain, ~spl61_1 | ~spl61_17, inference(sat_conversion,[],[f3562])).
% 4.16/1.02 cnf(s90, plain, ~spl61_17 | ~spl61_26, inference(sat_conversion,[],[f3584])).
% 4.16/1.02 cnf(s95, plain, ~spl61_20 | ~spl61_40, inference(sat_conversion,[],[f3612])).
% 4.16/1.02 cnf(s111, plain, ~spl61_5 | ~spl61_7 | ~spl61_8 | ~spl61_20 | ~spl61_21 | ~spl61_22 | spl61_40, inference(sat_conversion,[],[f3946])).
% 4.16/1.02 cnf(s112, plain, ~spl61_1 | ~spl61_69, inference(sat_conversion,[],[f3980])).
% 4.16/1.02 cnf(s163, plain, ~spl61_3 | ~spl61_4 | ~spl61_9 | ~spl61_10 | ~spl61_11 | ~spl61_12 | spl61_69, inference(sat_conversion,[],[f4889])).
% 4.16/1.02 cnf(s165, plain, spl61_17 | spl61_10 | spl61_6, inference(rat,[],[s111,s95,s16,s17,s18,s6,s5,s4])).
% 4.16/1.02 cnf(s166, plain, ~spl61_17 | spl61_6, inference(rat,[],[s22,s90])).
% 4.16/1.02 cnf(s167, plain, spl61_6, inference(rat,[],[s27,s10,s11,s12,s165,s166,s4,s5,s6])).
% 4.16/1.02 cnf(s168, plain, ~spl61_2, inference(rat,[],[s25,s167])).
% 4.16/1.02 cnf(s169, plain, spl61_4, inference(rat,[],[s3,s168])).
% 4.16/1.02 cnf(s170, plain, spl61_3, inference(rat,[],[s2,s168])).
% 4.16/1.02 cnf(s171, plain, spl61_1, inference(rat,[],[s1,s168])).
% 4.16/1.02 cnf(s172, plain, ~spl61_69, inference(rat,[],[s112,s171])).
% 4.16/1.02 cnf(s173, plain, ~spl61_17, inference(rat,[],[s88,s171])).
% 4.16/1.02 cnf(s174, plain, spl61_10, inference(rat,[],[s47,s53,s13,s14,s15,s171,s169,s170,s168,s173])).
% 4.16/1.02 cnf(s175, plain, spl61_12, inference(rat,[],[s9,s168,s174])).
% 4.16/1.02 cnf(s176, plain, spl61_11, inference(rat,[],[s8,s168,s174])).
% 4.16/1.02 cnf(s178, plain, spl61_9, inference(rat,[],[s7,s168,s174])).
% 4.16/1.02 cnf(s179, plain, $false, inference(rat,[],[s163,s172,s175,s176,s169,s170,s174,s178])).
% 4.16/1.02 thf(f4893,plain,(
% 4.16/1.02 $false),
% 4.16/1.02 inference(avatar_sat_refutation,[],[s179])).
% 4.16/1.02 % SZS output end Proof for theBenchmark
% 4.16/1.02 % (564491)------------------------------
% 4.16/1.02 % (564491)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.16/1.02 % (564491)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.16/1.02 % (564491)CaDiCaL version: 2.1.3
% 4.16/1.02 % (564491)Termination reason: Refutation
% 4.16/1.02 % (564491)Time elapsed: 0.194 s
% 4.16/1.02 % (564491)Peak memory usage: 15 MB
% 4.16/1.02 % (564491)Instructions burned: 417 (million)
% 4.16/1.02 % (564438)Success in time 0.79 s
% 4.16/1.02 % Vampire exiting
%------------------------------------------------------------------------------