%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ANA090^1 : TPTP v9.3.1. Released v7.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Sep 30 07:46:02 AM UTC 2026
% Result : Theorem 72.07s 14.60s
% Output : Refutation 72.07s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : ANA090^1 : TPTP v9.3.1. Released v7.0.0.
% 0.00/0.04 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.16 % Computer : n004.cluster.edu
% 0.10/0.16 % Model : x86_64 x86_64
% 0.10/0.16 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.16 % Memory : 8046.5625MB
% 0.10/0.16 % OS : Linux 6.8.0-71-generic
% 0.10/0.16 % CPULimit : 300
% 0.10/0.16 % WCLimit : 300
% 0.10/0.16 % DateTime : Tue Sep 29 17:40:52 UTC 2026
% 0.10/0.16 % CPUTime :
% 0.10/0.16 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.19 Running first-order model finding
% 0.10/0.19 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.03/0.90 % (1619372)Will run a generic schedule for satisfiability detection.
% 4.03/0.90 % (1619381)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2617925676_2999 on theBenchmark for (2999ds/0Mi)
% 4.03/0.90 % Exception at run slice level
% 4.03/0.90 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.03/0.90 % (1619382)% WARNING: option uhcvi not known.
% 4.03/0.90 % (1619382)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2177030756:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 4.03/0.90 % (1619383)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3102728476:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 4.03/0.90 % (1619384)dis+10_1_sil=32000:sp=arity:random_seed=615240717:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 4.03/0.90 % (1619386)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2050028519:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 4.03/0.90 % (1619387)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2483510573:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 4.03/0.90 % (1619388)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2887986617:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 4.03/0.90 % (1619382)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.03/0.90 % (1619382)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 4.03/0.90 % (1619386)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 4.03/0.90 % (1619397)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3181076470:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 4.03/0.90 % Exception at run slice level
% 4.03/0.90 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 4.03/0.90 % (1619407)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1511088889:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 4.03/0.90 % (1619384)Instruction limit reached!
% 4.03/0.90 % (1619384)------------------------------
% 4.03/0.90 % (1619384)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.03/0.90 % (1619384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.03/0.90 % (1619384)CaDiCaL version: 2.1.3
% 4.03/0.90 % (1619384)Termination reason: Instruction limit
% 4.03/0.90 % (1619384)Termination phase: Saturation
% 4.03/0.90 % (1619384)Time elapsed: 0.054 s
% 4.03/0.90 % (1619384)Peak memory usage: 12 MB
% 4.03/0.90 % (1619384)Instructions burned: 104 (million)
% 4.03/0.90 % (1619407)Instruction limit reached!
% 4.03/0.90 % (1619407)------------------------------
% 4.03/0.90 % (1619407)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.03/0.90 % (1619407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.03/0.90 % (1619407)CaDiCaL version: 2.1.3
% 4.03/0.90 % (1619407)Termination reason: Instruction limit
% 4.03/0.90 % (1619407)Termination phase: Saturation
% 4.03/0.90 % (1619407)Time elapsed: 0.043 s
% 4.03/0.90 % (1619407)Peak memory usage: 12 MB
% 4.03/0.90 % (1619407)Instructions burned: 133 (million)
% 4.03/0.90 % (1619386)Instruction limit reached!
% 4.03/0.90 % (1619386)------------------------------
% 4.03/0.90 % (1619386)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.03/0.90 % (1619386)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.03/0.90 % (1619386)CaDiCaL version: 2.1.3
% 4.03/0.90 % (1619386)Termination reason: Instruction limit
% 4.03/0.90 % (1619386)Termination phase: Saturation
% 4.03/0.90 % (1619386)Time elapsed: 0.063 s
% 4.03/0.90 % (1619386)Peak memory usage: 12 MB
% 4.03/0.90 % (1619386)Instructions burned: 117 (million)
% 4.03/0.90 % (1619426)ott-21_1_sil=16000:fs=off:random_seed=3724277574:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 4.03/0.90 % (1619387)Instruction limit reached!
% 4.03/0.90 % (1619387)------------------------------
% 4.03/0.90 % (1619387)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.03/0.90 % (1619387)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.03/0.90 % (1619387)CaDiCaL version: 2.1.3
% 4.03/0.90 % (1619387)Termination reason: Instruction limit
% 4.03/0.90 % (1619387)Termination phase: Saturation
% 4.03/0.90 % (1619387)Time elapsed: 0.071 s
% 4.03/0.90 % (1619387)Peak memory usage: 12 MB
% 15.63/2.49 % (1619387)Instructions burned: 132 (million)
% 15.63/2.49 % (1619422)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=3615095730:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 15.63/2.49 % (1619422)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 15.63/2.49 % (1619422)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 15.63/2.49 % (1619388)Instruction limit reached!
% 15.63/2.49 % (1619388)------------------------------
% 15.63/2.49 % (1619388)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.63/2.49 % (1619388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.63/2.49 % (1619388)CaDiCaL version: 2.1.3
% 15.63/2.49 % (1619388)Termination reason: Instruction limit
% 15.63/2.49 % (1619388)Termination phase: Saturation
% 15.63/2.49 % (1619388)Time elapsed: 0.077 s
% 15.63/2.49 % (1619388)Peak memory usage: 12 MB
% 15.63/2.49 % (1619388)Instructions burned: 161 (million)
% 15.63/2.49 % (1619429)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2463334972:i=477:bd=all_2999 on theBenchmark for (2999ds/477Mi)
% 15.63/2.49 % (1619434)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1514223306:fmbsr=1.3:i=865:ins=25_2999 on theBenchmark for (2999ds/865Mi)
% 15.63/2.49 % Exception at run slice level
% 15.63/2.49 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 15.63/2.49 % (1619439)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3866883966:i=1179_2999 on theBenchmark for (2999ds/1179Mi)
% 15.63/2.49 % (1619445)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=961777031:i=889:ins=1_2998 on theBenchmark for (2998ds/889Mi)
% 15.63/2.49 % Exception at run slice level
% 15.63/2.49 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 15.63/2.49 % (1619426)Instruction limit reached!
% 15.63/2.49 % (1619426)------------------------------
% 15.63/2.49 % (1619426)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.63/2.49 % (1619426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.63/2.49 % (1619426)CaDiCaL version: 2.1.3
% 15.63/2.49 % (1619426)Termination reason: Instruction limit
% 15.63/2.49 % (1619426)Termination phase: Saturation
% 15.63/2.49 % (1619426)Time elapsed: 0.048 s
% 15.63/2.49 % (1619426)Peak memory usage: 12 MB
% 15.63/2.49 % (1619426)Instructions burned: 183 (million)
% 15.63/2.49 % (1619452)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2836137998:i=879:kws=inv_precedence:fsr=off_2998 on theBenchmark for (2998ds/879Mi)
% 15.63/2.49 % (1619452)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 15.63/2.49 % (1619451)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=3087367624: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)
% 15.63/2.49 % (1619451)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 15.63/2.49 % (1619429)Instruction limit reached!
% 15.63/2.49 % (1619429)------------------------------
% 15.63/2.49 % (1619429)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.63/2.49 % (1619429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.63/2.49 % (1619429)CaDiCaL version: 2.1.3
% 15.63/2.49 % (1619429)Termination reason: Instruction limit
% 15.63/2.49 % (1619429)Termination phase: Saturation
% 15.63/2.49 % (1619429)Time elapsed: 0.277 s
% 15.63/2.49 % (1619429)Peak memory usage: 13 MB
% 15.63/2.49 % (1619429)Instructions burned: 478 (million)
% 15.63/2.49 % (1619452)Instruction limit reached!
% 15.63/2.49 % (1619452)------------------------------
% 15.63/2.49 % (1619452)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.63/2.49 % (1619452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.63/2.49 % (1619452)CaDiCaL version: 2.1.3
% 15.63/2.49 % (1619452)Termination reason: Instruction limit
% 15.63/2.49 % (1619452)Termination phase: Saturation
% 15.63/2.49 % (1619452)Time elapsed: 0.243 s
% 15.63/2.49 % (1619452)Peak memory usage: 15 MB
% 15.63/2.49 % (1619452)Instructions burned: 880 (million)
% 15.63/2.49 % (1619510)fmb+10_1_sil=64000:random_seed=725583308:i=22061:nm=2:gsp=on_2996 on theBenchmark for (2996ds/22061Mi)
% 35.52/5.23 % (1619510)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 35.52/5.23 % Exception at run slice level
% 35.52/5.23 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 35.52/5.23 % (1619511)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2381872046:i=9515:nm=5_2996 on theBenchmark for (2996ds/9515Mi)
% 35.52/5.23 % Exception at run slice level
% 35.52/5.23 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 35.52/5.23 % (1619422)Instruction limit reached!
% 35.52/5.23 % (1619422)------------------------------
% 35.52/5.23 % (1619422)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.52/5.23 % (1619422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.52/5.23 % (1619422)CaDiCaL version: 2.1.3
% 35.52/5.23 % (1619422)Termination reason: Instruction limit
% 35.52/5.23 % (1619422)Termination phase: Saturation
% 35.52/5.23 % (1619422)Time elapsed: 0.319 s
% 35.52/5.23 % (1619422)Peak memory usage: 15 MB
% 35.52/5.23 % (1619422)Instructions burned: 685 (million)
% 35.52/5.23 % (1619513)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2579405398:fmbsr=1.7:i=920_2995 on theBenchmark for (2995ds/920Mi)
% 35.52/5.23 % (1619515)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3839700061:i=5131_2995 on theBenchmark for (2995ds/5131Mi)
% 35.52/5.23 % Exception at run slice level
% 35.52/5.23 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 35.52/5.23 % (1619515)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 35.52/5.23 % (1619516)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1259087266:i=1472:ins=7:fdi=8:gsp=on_2995 on theBenchmark for (2995ds/1472Mi)
% 35.52/5.23 % (1619516)WARNING: Not using GeneralSplitting currently not compatible with polymorphic/higher-order inputs.
% 35.52/5.23 % (1619516)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 35.52/5.23 % (1619519)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=455887940:i=6324_2995 on theBenchmark for (2995ds/6324Mi)
% 35.52/5.23 % Exception at run slice level
% 35.52/5.23 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 35.52/5.23 % (1619522)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=615917670:fmbsr=2.30978:i=2174_2995 on theBenchmark for (2995ds/2174Mi)
% 35.52/5.23 % Exception at run slice level
% 35.52/5.23 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 35.52/5.23 % (1619524)ott-2_1_sil=16000:newcnf=on:random_seed=966364623:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2995 on theBenchmark for (2995ds/869Mi)
% 35.52/5.23 % (1619524)WARNING: Not using 'newcnf' as currently not compatible with higher-order inputs.
% 35.52/5.23 % (1619451)Instruction limit reached!
% 35.52/5.23 % (1619451)------------------------------
% 35.52/5.23 % (1619451)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.52/5.23 % (1619451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.52/5.23 % (1619451)CaDiCaL version: 2.1.3
% 35.52/5.23 % (1619451)Termination reason: Instruction limit
% 35.52/5.23 % (1619451)Termination phase: Saturation
% 35.52/5.23 % (1619451)Time elapsed: 0.349 s
% 35.52/5.23 % (1619451)Peak memory usage: 16 MB
% 35.52/5.23 % (1619451)Instructions burned: 692 (million)
% 35.52/5.23 % (1619526)ott+10_1_sil=32000:tgt=ground:random_seed=3992186238:i=5114:av=off_2994 on theBenchmark for (2994ds/5114Mi)
% 35.52/5.23 % (1619439)Instruction limit reached!
% 35.52/5.23 % (1619439)------------------------------
% 35.52/5.23 % (1619439)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 35.52/5.23 % (1619439)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.52/5.23 % (1619439)CaDiCaL version: 2.1.3
% 35.52/5.23 % (1619439)Termination reason: Instruction limit
% 35.52/5.23 % (1619439)Termination phase: Saturation
% 35.52/5.23 % (1619439)Time elapsed: 0.555 s
% 35.52/5.23 % (1619439)Peak memory usage: 16 MB
% 35.52/5.23 % (1619439)Instructions burned: 1181 (million)
% 35.52/5.23 % (1619528)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=3019637706:i=54282_2993 on theBenchmark for (2993ds/54282Mi)
% 35.52/5.23 % Exception at run slice level
% 101.17/14.54 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 101.17/14.54 % (1619530)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2756630402:i=3512:aac=none_2993 on theBenchmark for (2993ds/3512Mi)
% 101.17/14.54 % (1619530)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 101.17/14.54 % (1619524)Instruction limit reached!
% 101.17/14.54 % (1619524)------------------------------
% 101.17/14.54 % (1619524)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 101.17/14.54 % (1619524)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.17/14.54 % (1619524)CaDiCaL version: 2.1.3
% 101.17/14.54 % (1619524)Termination reason: Instruction limit
% 101.17/14.54 % (1619524)Termination phase: Saturation
% 101.17/14.54 % (1619524)Time elapsed: 0.417 s
% 101.17/14.54 % (1619524)Peak memory usage: 15 MB
% 101.17/14.54 % (1619524)Instructions burned: 871 (million)
% 101.17/14.54 % (1619532)dis+21_1_sil=32000:sas=cadical:random_seed=3672033915:i=3773:amm=off_2990 on theBenchmark for (2990ds/3773Mi)
% 101.17/14.54 % (1619516)Instruction limit reached!
% 101.17/14.54 % (1619516)------------------------------
% 101.17/14.54 % (1619516)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 101.17/14.54 % (1619516)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.17/14.54 % (1619516)CaDiCaL version: 2.1.3
% 101.17/14.54 % (1619516)Termination reason: Instruction limit
% 101.17/14.54 % (1619516)Termination phase: Saturation
% 101.17/14.54 % (1619516)Time elapsed: 0.717 s
% 101.17/14.54 % (1619516)Peak memory usage: 14 MB
% 101.17/14.54 % (1619516)Instructions burned: 1472 (million)
% 101.17/14.54 % (1619534)ott+11_1_sil=16000:gs=on:random_seed=2768733660:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2988 on theBenchmark for (2988ds/2251Mi)
% 101.17/14.54 % (1619534)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 101.17/14.54 % (1619515)Instruction limit reached!
% 101.17/14.54 % (1619515)------------------------------
% 101.17/14.54 % (1619515)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 101.17/14.54 % (1619515)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.17/14.54 % (1619515)CaDiCaL version: 2.1.3
% 101.17/14.54 % (1619515)Termination reason: Instruction limit
% 101.17/14.54 % (1619515)Termination phase: Saturation
% 101.17/14.54 % (1619515)Time elapsed: 1.199 s
% 101.17/14.54 % (1619515)Peak memory usage: 20 MB
% 101.17/14.54 % (1619515)Instructions burned: 5135 (million)
% 101.17/14.54 % (1619536)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1450526060:fmbsr=1.6:i=67534_2983 on theBenchmark for (2983ds/67534Mi)
% 101.17/14.54 % Exception at run slice level
% 101.17/14.54 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 101.17/14.54 % (1619538)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=1571166225:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2983 on theBenchmark for (2983ds/4591Mi)
% 101.17/14.54 % (1619534)Instruction limit reached!
% 101.17/14.54 % (1619534)------------------------------
% 101.17/14.54 % (1619534)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 101.17/14.54 % (1619534)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.17/14.54 % (1619534)CaDiCaL version: 2.1.3
% 101.17/14.54 % (1619534)Termination reason: Instruction limit
% 101.17/14.54 % (1619534)Termination phase: Saturation
% 101.17/14.54 % (1619534)Time elapsed: 1.032 s
% 101.17/14.54 % (1619534)Peak memory usage: 17 MB
% 101.17/14.54 % (1619534)Instructions burned: 2251 (million)
% 101.17/14.54 % (1619540)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1015726189:i=29340_2977 on theBenchmark for (2977ds/29340Mi)
% 101.17/14.54 % (1619530)Instruction limit reached!
% 101.17/14.54 % (1619530)------------------------------
% 101.17/14.54 % (1619530)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 101.17/14.54 % (1619530)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 101.17/14.54 % (1619530)CaDiCaL version: 2.1.3
% 101.17/14.54 % (1619530)Termination reason: Instruction limit
% 101.17/14.54 % (1619530)Termination phase: Saturation
% 101.17/14.54 % (1619530)Time elapsed: 1.555 s
% 101.17/14.54 % (1619530)Peak memory usage: 18 MB
% 101.17/14.54 % (1619530)Instructions burned: 3514 (million)
% 101.17/14.54 % (1619542)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3813177405:i=5211_2977 on theBenchmark for (2977ds/5211Mi)
% 72.07/14.60 % (1619532)Instruction limit reached!
% 72.07/14.60 % (1619532)------------------------------
% 72.07/14.60 % (1619532)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 72.07/14.60 % (1619532)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.07/14.60 % (1619532)CaDiCaL version: 2.1.3
% 72.07/14.60 % (1619532)Termination reason: Instruction limit
% 72.07/14.60 % (1619532)Termination phase: Saturation
% 72.07/14.60 % (1619532)Time elapsed: 1.690 s
% 72.07/14.60 % (1619532)Peak memory usage: 21 MB
% 72.07/14.60 % (1619532)Instructions burned: 3774 (million)
% 72.07/14.60 % (1619544)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=2233440227:i=5497:nm=2_2973 on theBenchmark for (2973ds/5497Mi)
% 72.07/14.60 % Exception at run slice level
% 72.07/14.60 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 72.07/14.60 % (1619546)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3670476953:fmbsr=2:i=46332_2973 on theBenchmark for (2973ds/46332Mi)
% 72.07/14.60 % Exception at run slice level
% 72.07/14.60 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 72.07/14.60 % (1619548)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=4041041314:i=14071_2973 on theBenchmark for (2973ds/14071Mi)
% 72.07/14.60 % Exception at run slice level
% 72.07/14.60 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 72.07/14.60 % (1619550)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1407340365:i=22565:add=on:rawr=on_2973 on theBenchmark for (2973ds/22565Mi)
% 72.07/14.60 % (1619526)Instruction limit reached!
% 72.07/14.60 % (1619526)------------------------------
% 72.07/14.60 % (1619526)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 72.07/14.60 % (1619526)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.07/14.60 % (1619526)CaDiCaL version: 2.1.3
% 72.07/14.60 % (1619526)Termination reason: Instruction limit
% 72.07/14.60 % (1619526)Termination phase: Saturation
% 72.07/14.60 % (1619526)Time elapsed: 2.282 s
% 72.07/14.60 % (1619526)Peak memory usage: 26 MB
% 72.07/14.60 % (1619526)Instructions burned: 5116 (million)
% 72.07/14.60 % (1619552)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3473341348:i=8173:av=off_2971 on theBenchmark for (2971ds/8173Mi)
% 72.07/14.60 % (1619538)Instruction limit reached!
% 72.07/14.60 % (1619538)------------------------------
% 72.07/14.60 % (1619538)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 72.07/14.60 % (1619538)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.07/14.60 % (1619538)CaDiCaL version: 2.1.3
% 72.07/14.60 % (1619538)Termination reason: Instruction limit
% 72.07/14.60 % (1619538)Termination phase: Saturation
% 72.07/14.60 % (1619538)Time elapsed: 1.256 s
% 72.07/14.60 % (1619538)Peak memory usage: 26 MB
% 72.07/14.60 % (1619538)Instructions burned: 4595 (million)
% 72.07/14.60 % (1619554)dis+10_16:1_sil=16000:random_seed=1546168985:i=9155:fsr=off_2970 on theBenchmark for (2970ds/9155Mi)
% 72.07/14.60 % (1619542)Instruction limit reached!
% 72.07/14.60 % (1619542)------------------------------
% 72.07/14.60 % (1619542)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 72.07/14.60 % (1619542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.07/14.60 % (1619542)CaDiCaL version: 2.1.3
% 72.07/14.60 % (1619542)Termination reason: Instruction limit
% 72.07/14.60 % (1619542)Termination phase: Saturation
% 72.07/14.60 % (1619542)Time elapsed: 2.448 s
% 72.07/14.60 % (1619542)Peak memory usage: 27 MB
% 72.07/14.60 % (1619542)Instructions burned: 5211 (million)
% 72.07/14.60 % (1619556)ott-3_8_sil=64000:random_seed=2132176012:i=20139:bs=on_2952 on theBenchmark for (2952ds/20139Mi)
% 72.07/14.60 % (1619554)Instruction limit reached!
% 72.07/14.60 % (1619554)------------------------------
% 72.07/14.60 % (1619554)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 72.07/14.60 % (1619554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.07/14.60 % (1619554)CaDiCaL version: 2.1.3
% 72.07/14.60 % (1619554)Termination reason: Instruction limit
% 72.07/14.60 % (1619554)Termination phase: Saturation
% 72.07/14.60 % (1619554)Time elapsed: 2.100 s
% 72.07/14.60 % (1619554)Peak memory usage: 26 MB
% 72.07/14.60 % (1619554)Instructions burned: 9157 (million)
% 72.07/14.60 % (1619558)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=616633208:fmbsr=2:i=32576_2949 on theBenchmark for (2949ds/32576Mi)
% 72.07/14.60 % Exception at run slice level
% 72.07/14.60 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 72.07/14.60 % (1619560)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=4287570484:i=11404_2949 on theBenchmark for (2949ds/11404Mi)
% 72.07/14.60 % (1619552)Instruction limit reached!
% 72.07/14.60 % (1619552)------------------------------
% 72.07/14.60 % (1619552)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 72.07/14.60 % (1619552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.07/14.60 % (1619552)CaDiCaL version: 2.1.3
% 72.07/14.60 % (1619552)Termination reason: Instruction limit
% 72.07/14.60 % (1619552)Termination phase: Saturation
% 72.07/14.60 % (1619552)Time elapsed: 3.729 s
% 72.07/14.60 % (1619552)Peak memory usage: 37 MB
% 72.07/14.60 % (1619552)Instructions burned: 8174 (million)
% 72.07/14.60 % (1619562)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=2180472382:i=14134_2934 on theBenchmark for (2934ds/14134Mi)
% 72.07/14.60 % (1619562)WARNING: Look ahead literal selection is not currently compatible with higher-order. Ignoring request to use
% 72.07/14.60 % (1619560)Instruction limit reached!
% 72.07/14.60 % (1619560)------------------------------
% 72.07/14.60 % (1619560)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 72.07/14.60 % (1619560)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.07/14.60 % (1619560)CaDiCaL version: 2.1.3
% 72.07/14.60 % (1619560)Termination reason: Instruction limit
% 72.07/14.60 % (1619560)Termination phase: Saturation
% 72.07/14.60 % (1619560)Time elapsed: 2.810 s
% 72.07/14.60 % (1619560)Peak memory usage: 41 MB
% 72.07/14.60 % (1619560)Instructions burned: 11408 (million)
% 72.07/14.60 % (1619564)dis+33_16_sil=32000:sac=on:random_seed=3149216579:i=15851:nm=0_2921 on theBenchmark for (2921ds/15851Mi)
% 72.07/14.60 % (1619564)Instruction limit reached!
% 72.07/14.60 % (1619564)------------------------------
% 72.07/14.60 % (1619564)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 72.07/14.60 % (1619564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.07/14.60 % (1619564)CaDiCaL version: 2.1.3
% 72.07/14.60 % (1619564)Termination reason: Instruction limit
% 72.07/14.60 % (1619564)Termination phase: Saturation
% 72.07/14.60 % (1619564)Time elapsed: 3.754 s
% 72.07/14.60 % (1619564)Peak memory usage: 41 MB
% 72.07/14.60 % (1619564)Instructions burned: 15853 (million)
% 72.07/14.60 % (1619566)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=1891660968:avsq=on:i=17627:add=on:amm=off_2883 on theBenchmark for (2883ds/17627Mi)
% 72.07/14.60 % (1619562)Instruction limit reached!
% 72.07/14.60 % (1619562)------------------------------
% 72.07/14.60 % (1619562)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 72.07/14.60 % (1619562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.07/14.60 % (1619562)CaDiCaL version: 2.1.3
% 72.07/14.60 % (1619562)Termination reason: Instruction limit
% 72.07/14.60 % (1619562)Termination phase: Saturation
% 72.07/14.60 % (1619562)Time elapsed: 6.407 s
% 72.07/14.60 % (1619562)Peak memory usage: 47 MB
% 72.07/14.60 % (1619562)Instructions burned: 14136 (million)
% 72.07/14.60 % (1619568)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=895422061:s2a=on:i=53295_2870 on theBenchmark for (2870ds/53295Mi)
% 72.07/14.60 % (1619550)Instruction limit reached!
% 72.07/14.60 % (1619550)------------------------------
% 72.07/14.60 % (1619550)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 72.07/14.60 % (1619550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.07/14.60 % (1619550)CaDiCaL version: 2.1.3
% 72.07/14.60 % (1619550)Termination reason: Instruction limit
% 72.07/14.60 % (1619550)Termination phase: Saturation
% 72.07/14.60 % (1619550)Time elapsed: 11.204 s
% 72.07/14.60 % (1619550)Peak memory usage: 73 MB
% 72.07/14.60 % (1619550)Instructions burned: 22566 (million)
% 72.07/14.60 % (1619677)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=1509790711:i=26857:ins=20_2860 on theBenchmark for (2860ds/26857Mi)
% 72.07/14.60 % Exception at run slice level
% 72.07/14.60 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 72.07/14.60 % (1619688)ott+10_1_sil=64000:plsq=on:plsqc=4:bsr=unit_only:gs=on:random_seed=3197853581:i=28120:bs=on:fsr=off_2860 on theBenchmark for (2860ds/28120Mi)
% 72.07/14.60 % (1619556)Instruction limit reached!
% 72.07/14.60 % (1619556)------------------------------
% 72.07/14.60 % (1619556)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 72.07/14.60 % (1619556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.07/14.60 % (1619556)CaDiCaL version: 2.1.3
% 72.07/14.60 % (1619556)Termination reason: Instruction limit
% 72.07/14.60 % (1619556)Termination phase: Saturation
% 72.07/14.60 % (1619556)Time elapsed: 9.574 s
% 72.07/14.60 % (1619556)Peak memory usage: 57 MB
% 72.07/14.60 % (1619556)Instructions burned: 20140 (million)
% 72.07/14.60 % (1619382) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-1619372-1619382"...
% 72.07/14.60 % (1619803)fmb+10_1_sil=256000:fmbss=7:random_seed=159858502:fmbsr=1.6:i=182295_2856 on theBenchmark for (2856ds/182295Mi)
% 72.07/14.60 % Exception at run slice level
% 72.07/14.60 User error: Finite model building is currently not compatible with polymorphism or higher-order constructs
% 72.07/14.60 % (1619382)...printing done.
% 72.07/14.60 % (1619382)Refutation found. Thanks to Tanya!
% 72.07/14.60 % SZS status Theorem for theBenchmark
% 72.07/14.60 % SZS output start Proof for theBenchmark
% 72.07/14.60 thf(type_def_5, type, 'type/realax/real': $tType).
% 72.07/14.60 thf(type_def_6, type, sTfun: ($tType * $tType) > $tType).
% 72.07/14.60 thf(func_def_0, type, 'const/sets/sup': (('type/realax/real' > $o) > 'type/realax/real')).
% 72.07/14.60 thf(func_def_1, type, 'const/sets/INSERT': !>[X0: $tType]:((X0 > (X0 > $o) > X0 > $o))).
% 72.07/14.60 thf(func_def_2, type, 'const/sets/inf': (('type/realax/real' > $o) > 'type/realax/real')).
% 72.07/14.60 thf(func_def_3, type, 'const/sets/IN': !>[X0: $tType]:((X0 > (X0 > $o) > $o))).
% 72.07/14.60 thf(func_def_4, type, 'const/sets/FINITE': !>[X0: $tType]:(((X0 > $o) > $o))).
% 72.07/14.60 thf(func_def_5, type, 'const/sets/EMPTY': !>[X0: $tType]:((X0 > $o))).
% 72.07/14.60 thf(func_def_6, type, 'const/realax/real_neg': ('type/realax/real' > 'type/realax/real')).
% 72.07/14.60 thf(func_def_7, type, 'const/realax/real_min': ('type/realax/real' > 'type/realax/real' > 'type/realax/real')).
% 72.07/14.60 thf(func_def_8, type, 'const/realax/real_max': ('type/realax/real' > 'type/realax/real' > 'type/realax/real')).
% 72.07/14.60 thf(func_def_9, type, 'const/realax/real_le': ('type/realax/real' > 'type/realax/real' > $o)).
% 72.07/14.60 thf(func_def_10, type, 'const/realax/real_abs': ('type/realax/real' > 'type/realax/real')).
% 72.07/14.60 thf(func_def_11, type, 'const/class/COND': !>[X0: $tType]:(($o > X0 > X0 > X0))).
% 72.07/14.60 thf(func_def_15, type, vEQ: !>[X0: $tType]:((X0 > X0 > $o))).
% 72.07/14.60 thf(func_def_16, type, vOR: ($o > $o > $o)).
% 72.07/14.60 thf(func_def_17, type, vPI: !>[X0: $tType]:(((X0 > $o) > $o))).
% 72.07/14.60 thf(func_def_18, type, db0: !>[X0: $tType]:(X0)).
% 72.07/14.60 thf(func_def_19, type, vLAM: !>[X0: $tType, X1: $tType]:((X1) > (X0 > X1))).
% 72.07/14.60 thf(func_def_20, type, vAND: ($o > $o > $o)).
% 72.07/14.60 thf(func_def_21, type, vSIGMA: !>[X0: $tType]:(((X0 > $o) > $o))).
% 72.07/14.60 thf(func_def_22, type, sK0: ('type/realax/real' > ('type/realax/real' > $o) > 'type/realax/real')).
% 72.07/14.60 thf(func_def_23, type, sK1: ('type/realax/real' > ('type/realax/real' > $o) > 'type/realax/real')).
% 72.07/14.60 thf(func_def_24, type, sK2: ('type/realax/real' > ('type/realax/real' > $o) > 'type/realax/real')).
% 72.07/14.60 thf(func_def_25, type, sK3: ('type/realax/real' > ('type/realax/real' > $o) > 'type/realax/real')).
% 72.07/14.60 thf(func_def_26, type, sK4: ('type/realax/real' > $o)).
% 72.07/14.60 thf(func_def_27, type, sK5: 'type/realax/real').
% 72.07/14.60 thf(func_def_28, type, vNOT: ($o > $o)).
% 72.07/14.60 thf(func_def_29, type, sK6: 'type/realax/real').
% 72.07/14.60 thf(func_def_30, type, sK7: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > X0))).
% 72.07/14.60 thf(func_def_32, type, sK9: 'type/realax/real').
% 72.07/14.60 thf(func_def_33, type, sK10: ('type/realax/real' > 'type/realax/real')).
% 72.07/14.60 thf(func_def_34, type, sK11: ('type/realax/real' > 'type/realax/real')).
% 72.07/14.60 thf(func_def_35, type, db1: !>[X0: $tType]:(X0)).
% 72.07/14.60 thf(func_def_36, type, sK12: (('type/realax/real' > $o) > 'type/realax/real')).
% 72.07/14.60 thf(func_def_37, type, sK13: (('type/realax/real' > $o) > 'type/realax/real')).
% 72.07/14.60 thf(func_def_38, type, sK14: (('type/realax/real' > $o) > 'type/realax/real')).
% 72.07/14.60 thf(func_def_39, type, sK15: (('type/realax/real' > $o) > 'type/realax/real')).
% 72.07/14.60 thf(func_def_40, type, sK16: (('type/realax/real' > $o) > 'type/realax/real')).
% 72.07/14.60 thf(func_def_41, type, sK17: (('type/realax/real' > $o) > 'type/realax/real')).
% 72.07/14.60 thf(func_def_42, type, sK18: (('type/realax/real' > $o) > 'type/realax/real')).
% 72.07/14.60 thf(func_def_43, type, sK19: ('type/realax/real' > 'type/realax/real')).
% 72.07/14.60 thf(func_def_44, type, sK20: (('type/realax/real' > $o) > 'type/realax/real')).
% 72.07/14.60 thf(func_def_45, type, sK21: ('type/realax/real' > ('type/realax/real' > 'type/realax/real' > 'type/realax/real') > 'type/realax/real')).
% 72.07/14.60 thf(func_def_46, type, sK22: ('type/realax/real' > ('type/realax/real' > 'type/realax/real' > 'type/realax/real') > 'type/realax/real')).
% 72.07/14.60 thf(func_def_47, type, sK23: ('type/realax/real' > ('type/realax/real' > 'type/realax/real' > 'type/realax/real') > 'type/realax/real')).
% 72.07/14.60 thf(func_def_48, type, sK24: ('type/realax/real' > ('type/realax/real' > 'type/realax/real' > 'type/realax/real') > 'type/realax/real')).
% 72.07/14.60 thf(func_def_49, type, sK25: ('type/realax/real' > ('type/realax/real' > 'type/realax/real' > 'type/realax/real') > 'type/realax/real')).
% 72.07/14.60 thf(func_def_50, type, sK26: ('type/realax/real' > ('type/realax/real' > 'type/realax/real' > 'type/realax/real') > 'type/realax/real')).
% 72.07/14.60 thf(func_def_51, type, sK27: ('type/realax/real' > ('type/realax/real' > 'type/realax/real' > 'type/realax/real') > 'type/realax/real')).
% 72.07/14.60 thf(func_def_52, type, sK28: ('type/realax/real' > ('type/realax/real' > 'type/realax/real' > 'type/realax/real') > 'type/realax/real')).
% 72.07/14.60 thf(func_def_53, type, sK29: ('type/realax/real' > ('type/realax/real' > 'type/realax/real' > 'type/realax/real') > 'type/realax/real')).
% 72.07/14.60 thf(func_def_54, type, sK30: ('type/realax/real' > ('type/realax/real' > 'type/realax/real' > 'type/realax/real') > 'type/realax/real')).
% 72.07/14.60 thf(func_def_55, type, db2: !>[X0: $tType]:(X0)).
% 72.07/14.60 thf(func_def_56, type, sK31: !>[X0: $tType]:(((X0 > $o) > X0))).
% 72.07/14.60 thf(func_def_57, type, sK32: (('type/realax/real' > $o) > 'type/realax/real')).
% 72.07/14.60 thf(func_def_58, type, sK33: ('type/realax/real' > ('type/realax/real' > 'type/realax/real') > ('type/realax/real' > 'type/realax/real' > 'type/realax/real') > 'type/realax/real')).
% 72.07/14.60 thf(func_def_59, type, sK34: ('type/realax/real' > ('type/realax/real' > 'type/realax/real') > ('type/realax/real' > 'type/realax/real' > 'type/realax/real') > 'type/realax/real')).
% 72.07/14.60 thf(func_def_60, type, sK35: (('type/realax/real' > $o) > 'type/realax/real')).
% 72.07/14.60 thf(func_def_61, type, sK36: (('type/realax/real' > $o) > 'type/realax/real')).
% 72.07/14.60 thf(func_def_62, type, sK37: ('type/realax/real' > ('type/realax/real' > 'type/realax/real' > 'type/realax/real') > 'type/realax/real')).
% 72.07/14.60 thf(func_def_63, type, sK38: ('type/realax/real' > ('type/realax/real' > 'type/realax/real' > 'type/realax/real') > 'type/realax/real')).
% 72.07/14.60 thf(func_def_64, type, sK39: ('type/realax/real' > ('type/realax/real' > 'type/realax/real' > 'type/realax/real') > 'type/realax/real')).
% 72.07/14.60 thf(func_def_65, type, sK40: ('type/realax/real' > ('type/realax/real' > 'type/realax/real' > 'type/realax/real') > 'type/realax/real')).
% 72.07/14.60 thf(func_def_66, type, sK41: ('type/realax/real' > ('type/realax/real' > 'type/realax/real' > 'type/realax/real') > 'type/realax/real')).
% 72.07/14.60 thf(func_def_67, type, sK42: ('type/realax/real' > ('type/realax/real' > 'type/realax/real' > 'type/realax/real') > 'type/realax/real')).
% 72.07/14.60 thf(func_def_68, type, sK43: ('type/realax/real' > ('type/realax/real' > 'type/realax/real' > 'type/realax/real') > 'type/realax/real')).
% 72.07/14.60 thf(func_def_69, type, sK44: ('type/realax/real' > ('type/realax/real' > 'type/realax/real' > 'type/realax/real') > 'type/realax/real')).
% 72.07/14.60 thf(func_def_70, type, sK45: ('type/realax/real' > ('type/realax/real' > 'type/realax/real') > ('type/realax/real' > 'type/realax/real' > 'type/realax/real') > 'type/realax/real')).
% 72.07/14.60 thf(func_def_71, type, sK46: ('type/realax/real' > ('type/realax/real' > 'type/realax/real') > ('type/realax/real' > 'type/realax/real' > 'type/realax/real') > 'type/realax/real')).
% 72.07/14.60 thf(func_def_72, type, sK47: ('type/realax/real' > ('type/realax/real' > 'type/realax/real') > ('type/realax/real' > 'type/realax/real' > 'type/realax/real') > 'type/realax/real')).
% 72.07/14.60 thf(func_def_73, type, sK48: (('type/realax/real' > $o) > 'type/realax/real')).
% 72.07/14.60 thf(func_def_74, type, sK49: ('type/realax/real' > ('type/realax/real' > 'type/realax/real') > ('type/realax/real' > 'type/realax/real' > 'type/realax/real') > 'type/realax/real')).
% 72.07/14.60 thf(func_def_75, type, sK50: ('type/realax/real' > ('type/realax/real' > 'type/realax/real') > ('type/realax/real' > 'type/realax/real' > 'type/realax/real') > 'type/realax/real')).
% 72.07/14.60 thf(func_def_76, type, sK51: ('type/realax/real' > ('type/realax/real' > 'type/realax/real') > ('type/realax/real' > 'type/realax/real' > 'type/realax/real') > 'type/realax/real')).
% 72.07/14.60 thf(func_def_77, type, sK52: ('type/realax/real' > ('type/realax/real' > 'type/realax/real') > ('type/realax/real' > 'type/realax/real' > 'type/realax/real') > 'type/realax/real')).
% 72.07/14.60 thf(func_def_78, type, sK53: ('type/realax/real' > ('type/realax/real' > 'type/realax/real') > ('type/realax/real' > 'type/realax/real' > 'type/realax/real') > 'type/realax/real')).
% 72.07/14.60 thf(func_def_79, type, sK54: !>[X0: $tType]:(((X0 > $o) > (X0 > $o) > X0 > X0))).
% 72.07/14.60 thf(func_def_80, type, sK55: (('type/realax/real' > $o) > 'type/realax/real')).
% 72.07/14.60 thf(func_def_81, type, sK56: ('type/realax/real' > ('type/realax/real' > 'type/realax/real') > ('type/realax/real' > 'type/realax/real' > 'type/realax/real') > 'type/realax/real')).
% 72.07/14.60 thf(func_def_82, type, sK57: ('type/realax/real' > ('type/realax/real' > 'type/realax/real') > ('type/realax/real' > 'type/realax/real' > 'type/realax/real') > 'type/realax/real')).
% 72.07/14.60 thf(func_def_83, type, sK58: (('type/realax/real' > $o) > 'type/realax/real')).
% 72.07/14.60 thf(func_def_84, type, sK59: ('type/realax/real' > ('type/realax/real' > 'type/realax/real') > ('type/realax/real' > 'type/realax/real' > 'type/realax/real') > 'type/realax/real')).
% 72.07/14.60 thf(func_def_85, type, sK60: ('type/realax/real' > ('type/realax/real' > 'type/realax/real') > ('type/realax/real' > 'type/realax/real' > 'type/realax/real') > 'type/realax/real')).
% 72.07/14.60 thf(func_def_86, type, sK61: ('type/realax/real' > ('type/realax/real' > 'type/realax/real') > ('type/realax/real' > 'type/realax/real' > 'type/realax/real') > 'type/realax/real')).
% 72.07/14.60 thf(func_def_87, type, sK62: ('type/realax/real' > ('type/realax/real' > 'type/realax/real') > ('type/realax/real' > 'type/realax/real' > 'type/realax/real') > 'type/realax/real')).
% 72.07/14.60 thf(func_def_88, type, sK63: ('type/realax/real' > ('type/realax/real' > 'type/realax/real') > ('type/realax/real' > 'type/realax/real' > 'type/realax/real') > 'type/realax/real')).
% 72.07/14.60 thf(func_def_89, type, sK64: 'type/realax/real').
% 72.07/14.60 thf(func_def_90, type, sK65: (('type/realax/real' > $o) > 'type/realax/real')).
% 72.07/14.60 thf(func_def_91, type, sK66: (('type/realax/real' > $o) > 'type/realax/real')).
% 72.07/14.60 thf(func_def_92, type, sK67: 'type/realax/real').
% 72.07/14.60 thf(func_def_93, type, sK68: (('type/realax/real' > $o) > 'type/realax/real')).
% 72.07/14.60 thf(func_def_94, type, sK69: 'type/realax/real').
% 72.07/14.60 thf(func_def_95, type, sK70: ('type/realax/real' > 'type/realax/real')).
% 72.07/14.60 thf(func_def_96, type, sK71: (('type/realax/real' > $o) > 'type/realax/real')).
% 72.07/14.60 thf(func_def_97, type, sK72: (('type/realax/real' > $o) > 'type/realax/real')).
% 72.07/14.60 thf(func_def_98, type, sK73: (('type/realax/real' > $o) > 'type/realax/real')).
% 72.07/14.60 thf(func_def_99, type, sK74: (('type/realax/real' > $o) > 'type/realax/real')).
% 72.07/14.60 thf(func_def_100, type, sK75: (('type/realax/real' > $o) > 'type/realax/real')).
% 72.07/14.60 thf(func_def_101, type, sK76: (('type/realax/real' > $o) > 'type/realax/real')).
% 72.07/14.60 thf(f4,axiom,(
% 72.07/14.60 ! [X0 : $tType,X1 : X0] : ~('const/sets/IN' @ X0 @ X1 @ 'const/sets/EMPTY' @ X0)),
% 72.07/14.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p','thm/sets/NOT_IN_EMPTY_')).
% 72.07/14.60 thf(f5,axiom,(
% 72.07/14.60 ! [X0 : $tType,X1 : X0,X2 : X0,X3 : (X0 > $o)] : ((('const/sets/IN' @ X0 @ X1 @ ('const/sets/INSERT' @ X0 @ X2 @ X3))) = ('const/sets/IN' @ X0 @ X1 @ X3) | (X1 = X2))),
% 72.07/14.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p','thm/sets/IN_INSERT_')).
% 72.07/14.60 thf(f6,axiom,(
% 72.07/14.60 ! [X0 : $tType,X1 : (X0 > $o),X2 : X0] : ((('const/sets/IN' @ X0 @ X2 @ X1)) = ((X1 @ X2)))),
% 72.07/14.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p','thm/sets/IN_')).
% 72.07/14.60 thf(f7,axiom,(
% 72.07/14.60 ! [X0 : $tType,X1 : (X0 > $o),X2 : (X0 > $o)] : ((X1 = X2) = ! [X3 : X0] : ((('const/sets/IN' @ X0 @ X3 @ X1)) = (('const/sets/IN' @ X0 @ X3 @ X2))))),
% 72.07/14.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p','thm/sets/EXTENSION_')).
% 72.07/14.60 thf(f8,axiom,(
% 72.07/14.60 ! [X0 : ('type/realax/real' > $o)] : ((? [X1 : 'type/realax/real'] : ! [X2 : 'type/realax/real'] : (('const/sets/IN' @ 'type/realax/real' @ X2 @ X0) => ('const/realax/real_le' @ X1 @ X2)) & (X0 != 'const/sets/EMPTY' @ 'type/realax/real')) => (! [X1 : 'type/realax/real'] : (! [X2 : 'type/realax/real'] : (('const/sets/IN' @ 'type/realax/real' @ X2 @ X0) => ('const/realax/real_le' @ X1 @ X2)) => ('const/realax/real_le' @ X1 @ ('const/sets/inf' @ X0))) & ! [X1 : 'type/realax/real'] : (('const/sets/IN' @ 'type/realax/real' @ X1 @ X0) => ('const/realax/real_le' @ ('const/sets/inf' @ X0) @ X1))))),
% 72.07/14.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p','thm/sets/INF_')).
% 72.07/14.60 thf(f9,axiom,(
% 72.07/14.60 ! [X0 : 'type/realax/real',X1 : 'type/realax/real'] : ((('const/realax/real_le' @ ('const/realax/real_abs' @ X0) @ X1)) = ('const/realax/real_le' @ X0 @ X1) & ('const/realax/real_le' @ ('const/realax/real_neg' @ X1) @ X0))),
% 72.07/14.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p','thm/real/REAL_ABS_BOUNDS_')).
% 72.07/14.60 thf(f10,axiom,(
% 72.07/14.60 ! [X0 : ('type/realax/real' > $o)] : ((? [X1 : 'type/realax/real'] : ! [X2 : 'type/realax/real'] : (('const/sets/IN' @ 'type/realax/real' @ X2 @ X0) => ('const/realax/real_le' @ X2 @ X1)) & (X0 != 'const/sets/EMPTY' @ 'type/realax/real')) => (! [X1 : 'type/realax/real'] : (! [X2 : 'type/realax/real'] : (('const/sets/IN' @ 'type/realax/real' @ X2 @ X0) => ('const/realax/real_le' @ X2 @ X1)) => ('const/realax/real_le' @ ('const/sets/sup' @ X0) @ X1)) & ! [X1 : 'type/realax/real'] : (('const/sets/IN' @ 'type/realax/real' @ X1 @ X0) => ('const/realax/real_le' @ X1 @ ('const/sets/sup' @ X0)))))),
% 72.07/14.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p','thm/sets/SUP_')).
% 72.07/14.60 thf(f11,axiom,(
% 72.07/14.60 ! [X0 : 'type/realax/real',X1 : 'type/realax/real'] : (('const/realax/real_le' @ X1 @ X0) & ('const/realax/real_le' @ X0 @ X1) = (X0 = X1))),
% 72.07/14.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p','thm/realax/REAL_LE_ANTISYM_')).
% 72.07/14.60 thf(f12,conjecture,(
% 72.07/14.60 ! [X0 : ('type/realax/real' > $o)] : ((? [X1 : 'type/realax/real'] : ! [X2 : 'type/realax/real'] : (('const/sets/IN' @ 'type/realax/real' @ X2 @ X0) => ('const/realax/real_le' @ ('const/realax/real_abs' @ X2) @ X1)) & (X0 != 'const/sets/EMPTY' @ 'type/realax/real')) => (((('const/sets/sup' @ X0)) = (('const/sets/inf' @ X0))) = ? [X2 : 'type/realax/real'] : (X0 = (('const/sets/INSERT' @ 'type/realax/real' @ X2 @ 'const/sets/EMPTY' @ 'type/realax/real')))))),
% 72.07/14.60 file('/export/starexec/sandbox2/benchmark/theBenchmark.p','thm/sets/REAL_SUP_EQ_INF_')).
% 72.07/14.60 thf(f13,negated_conjecture,(
% 72.07/14.60 ~ ! [X0 : ('type/realax/real' > $o)] : ((? [X1 : 'type/realax/real'] : ! [X2 : 'type/realax/real'] : (('const/sets/IN' @ 'type/realax/real' @ X2 @ X0) => ('const/realax/real_le' @ ('const/realax/real_abs' @ X2) @ X1)) & (X0 != 'const/sets/EMPTY' @ 'type/realax/real')) => (((('const/sets/sup' @ X0)) = (('const/sets/inf' @ X0))) = ? [X2 : 'type/realax/real'] : (X0 = (('const/sets/INSERT' @ 'type/realax/real' @ X2 @ 'const/sets/EMPTY' @ 'type/realax/real')))))),
% 72.07/14.60 inference(negated_conjecture,[status(cth)],[f12])).
% 72.07/14.60 thf(f20,plain,(
% 72.07/14.60 ! [X0 : $tType,X1 : X0] : ~('const/sets/IN' @ X0 @ X1 @ 'const/sets/EMPTY' @ X0)),
% 72.07/14.60 inference(rectify,[],[f4])).
% 72.07/14.60 thf(f21,plain,(
% 72.07/14.60 ! [X0 : $tType,X1 : X0] : ~ ((('const/sets/IN' @ X0 @ X1 @ 'const/sets/EMPTY' @ X0)) = $true)),
% 72.07/14.60 inference(fool_elimination,[],[f20])).
% 72.07/14.60 thf(f22,plain,(
% 72.07/14.60 ! [X0 : $tType,X1 : X0,X2 : X0,X3 : (X0 > $o)] : ((('const/sets/IN' @ X0 @ X1 @ ('const/sets/INSERT' @ X0 @ X2 @ X3))) = ('const/sets/IN' @ X0 @ X1 @ X3) | (X1 = X2))),
% 72.07/14.60 inference(rectify,[],[f5])).
% 72.07/14.60 thf(f23,plain,(
% 72.07/14.60 ! [X0 : $tType,X1 : X0,X2 : X0,X3 : (X0 > $o)] : ((('const/sets/IN' @ X0 @ X1 @ ('const/sets/INSERT' @ X0 @ X2 @ X3))) = (((X1 = X2) | ('const/sets/IN' @ X0 @ X1 @ X3))))),
% 72.07/14.60 inference(fool_elimination,[],[f22])).
% 72.07/14.60 thf(f24,plain,(
% 72.07/14.60 ! [X0 : $tType,X1 : (X0 > $o),X2 : (X0 > $o)] : (((X1 = X2)) = ((!! @ X0 @ (^[Y0 : X0]: (('const/sets/IN' @ X0 @ Y0 @ X1) = ('const/sets/IN' @ X0 @ Y0 @ X2))))))),
% 72.07/14.60 inference(fool_elimination,[],[f7])).
% 72.07/14.60 thf(f25,plain,(
% 72.07/14.60 ! [X0 : ('type/realax/real' > $o)] : ((? [X1 : 'type/realax/real'] : ! [X2 : 'type/realax/real'] : (('const/sets/IN' @ 'type/realax/real' @ X2 @ X0) => ('const/realax/real_le' @ X1 @ X2)) & (X0 != 'const/sets/EMPTY' @ 'type/realax/real')) => (! [X3 : 'type/realax/real'] : (! [X4 : 'type/realax/real'] : (('const/sets/IN' @ 'type/realax/real' @ X4 @ X0) => ('const/realax/real_le' @ X3 @ X4)) => ('const/realax/real_le' @ X3 @ ('const/sets/inf' @ X0))) & ! [X5 : 'type/realax/real'] : (('const/sets/IN' @ 'type/realax/real' @ X5 @ X0) => ('const/realax/real_le' @ ('const/sets/inf' @ X0) @ X5))))),
% 72.07/14.60 inference(rectify,[],[f8])).
% 72.07/14.60 thf(f26,plain,(
% 72.07/14.60 ! [X0 : ('type/realax/real' > $o)] : ((? [X1 : 'type/realax/real'] : ! [X2 : 'type/realax/real'] : (((('const/sets/IN' @ 'type/realax/real' @ X2 @ X0)) = $true) => ((('const/realax/real_le' @ X1 @ X2)) = $true)) & ('const/sets/EMPTY' @ 'type/realax/real' != X0)) => (! [X3 : 'type/realax/real'] : (! [X4 : 'type/realax/real'] : (($true = (('const/sets/IN' @ 'type/realax/real' @ X4 @ X0))) => ($true = (('const/realax/real_le' @ X3 @ X4)))) => ($true = (('const/realax/real_le' @ X3 @ ('const/sets/inf' @ X0))))) & ! [X5 : 'type/realax/real'] : (($true = (('const/sets/IN' @ 'type/realax/real' @ X5 @ X0))) => ($true = (('const/realax/real_le' @ ('const/sets/inf' @ X0) @ X5))))))),
% 72.07/14.60 inference(fool_elimination,[],[f25])).
% 72.07/14.60 thf(f27,plain,(
% 72.07/14.60 ! [X0 : 'type/realax/real',X1 : 'type/realax/real'] : ((('const/realax/real_le' @ ('const/realax/real_abs' @ X0) @ X1)) = ('const/realax/real_le' @ X0 @ X1) & ('const/realax/real_le' @ ('const/realax/real_neg' @ X1) @ X0))),
% 72.07/14.60 inference(rectify,[],[f9])).
% 72.07/14.60 thf(f28,plain,(
% 72.07/14.60 ! [X0 : 'type/realax/real',X1 : 'type/realax/real'] : ((('const/realax/real_le' @ ('const/realax/real_abs' @ X0) @ X1)) = ((('const/realax/real_le' @ ('const/realax/real_neg' @ X1) @ X0) & ('const/realax/real_le' @ X0 @ X1))))),
% 72.07/14.60 inference(fool_elimination,[],[f27])).
% 72.07/14.60 thf(f29,plain,(
% 72.07/14.60 ! [X0 : ('type/realax/real' > $o)] : ((? [X1 : 'type/realax/real'] : ! [X2 : 'type/realax/real'] : (('const/sets/IN' @ 'type/realax/real' @ X2 @ X0) => ('const/realax/real_le' @ X2 @ X1)) & (X0 != 'const/sets/EMPTY' @ 'type/realax/real')) => (! [X3 : 'type/realax/real'] : (! [X4 : 'type/realax/real'] : (('const/sets/IN' @ 'type/realax/real' @ X4 @ X0) => ('const/realax/real_le' @ X4 @ X3)) => ('const/realax/real_le' @ ('const/sets/sup' @ X0) @ X3)) & ! [X5 : 'type/realax/real'] : (('const/sets/IN' @ 'type/realax/real' @ X5 @ X0) => ('const/realax/real_le' @ X5 @ ('const/sets/sup' @ X0)))))),
% 72.07/14.60 inference(rectify,[],[f10])).
% 72.07/14.60 thf(f30,plain,(
% 72.07/14.60 ! [X0 : ('type/realax/real' > $o)] : ((? [X1 : 'type/realax/real'] : ! [X2 : 'type/realax/real'] : (((('const/sets/IN' @ 'type/realax/real' @ X2 @ X0)) = $true) => ((('const/realax/real_le' @ X2 @ X1)) = $true)) & ('const/sets/EMPTY' @ 'type/realax/real' != X0)) => (! [X3 : 'type/realax/real'] : (! [X4 : 'type/realax/real'] : (($true = (('const/sets/IN' @ 'type/realax/real' @ X4 @ X0))) => ($true = (('const/realax/real_le' @ X4 @ X3)))) => ($true = (('const/realax/real_le' @ ('const/sets/sup' @ X0) @ X3)))) & ! [X5 : 'type/realax/real'] : (($true = (('const/sets/IN' @ 'type/realax/real' @ X5 @ X0))) => ($true = (('const/realax/real_le' @ X5 @ ('const/sets/sup' @ X0)))))))),
% 72.07/14.60 inference(fool_elimination,[],[f29])).
% 72.07/14.60 thf(f31,plain,(
% 72.07/14.60 ! [X0 : 'type/realax/real',X1 : 'type/realax/real'] : (('const/realax/real_le' @ X1 @ X0) & ('const/realax/real_le' @ X0 @ X1) = (X0 = X1))),
% 72.07/14.60 inference(rectify,[],[f11])).
% 72.07/14.60 thf(f32,plain,(
% 72.07/14.60 ! [X0 : 'type/realax/real',X1 : 'type/realax/real'] : (((('const/realax/real_le' @ X0 @ X1) & ('const/realax/real_le' @ X1 @ X0))) = ((X0 = X1)))),
% 72.07/14.60 inference(fool_elimination,[],[f31])).
% 72.07/14.60 thf(f33,plain,(
% 72.07/14.60 ~ ! [X0 : ('type/realax/real' > $o)] : ((? [X1 : 'type/realax/real'] : ! [X2 : 'type/realax/real'] : (('const/sets/IN' @ 'type/realax/real' @ X2 @ X0) => ('const/realax/real_le' @ ('const/realax/real_abs' @ X2) @ X1)) & (X0 != 'const/sets/EMPTY' @ 'type/realax/real')) => (((('const/sets/sup' @ X0)) = (('const/sets/inf' @ X0))) = ? [X3 : 'type/realax/real'] : ((('const/sets/INSERT' @ 'type/realax/real' @ X3 @ 'const/sets/EMPTY' @ 'type/realax/real')) = X0)))),
% 72.07/14.60 inference(rectify,[],[f13])).
% 72.07/14.60 thf(f34,plain,(
% 72.07/14.60 ~ ! [X0 : ('type/realax/real' > $o)] : ((? [X1 : 'type/realax/real'] : ! [X2 : 'type/realax/real'] : (((('const/sets/IN' @ 'type/realax/real' @ X2 @ X0)) = $true) => ((('const/realax/real_le' @ ('const/realax/real_abs' @ X2) @ X1)) = $true)) & ('const/sets/EMPTY' @ 'type/realax/real' != X0)) => (((('const/sets/inf' @ X0) = ('const/sets/sup' @ X0))) = ((?? @ 'type/realax/real' @ (^[Y0 : 'type/realax/real']: (('const/sets/INSERT' @ 'type/realax/real' @ Y0 @ 'const/sets/EMPTY' @ 'type/realax/real') = X0))))))),
% 72.07/14.60 inference(fool_elimination,[],[f33])).
% 72.07/14.60 thf(f35,plain,(
% 72.07/14.60 ! [X0 : $tType,X1 : X0] : ((('const/sets/IN' @ X0 @ X1 @ 'const/sets/EMPTY' @ X0)) != $true)),
% 72.07/14.60 inference(flattening,[],[f21])).
% 72.07/14.60 thf(f38,plain,(
% 72.07/14.60 ! [X0 : ('type/realax/real' > $o)] : ((! [X3 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ X3 @ ('const/sets/inf' @ X0)))) | ? [X4 : 'type/realax/real'] : (($true != (('const/realax/real_le' @ X3 @ X4))) & ($true = (('const/sets/IN' @ 'type/realax/real' @ X4 @ X0))))) & ! [X5 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ ('const/sets/inf' @ X0) @ X5))) | ($true != (('const/sets/IN' @ 'type/realax/real' @ X5 @ X0))))) | (! [X1 : 'type/realax/real'] : ? [X2 : 'type/realax/real'] : (((('const/realax/real_le' @ X1 @ X2)) != $true) & ((('const/sets/IN' @ 'type/realax/real' @ X2 @ X0)) = $true)) | ('const/sets/EMPTY' @ 'type/realax/real' = X0)))),
% 72.07/14.60 inference(ennf_transformation,[],[f26])).
% 72.07/14.60 thf(f39,plain,(
% 72.07/14.60 ! [X0 : ('type/realax/real' > $o)] : ((! [X3 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ X3 @ ('const/sets/inf' @ X0)))) | ? [X4 : 'type/realax/real'] : (($true != (('const/realax/real_le' @ X3 @ X4))) & ($true = (('const/sets/IN' @ 'type/realax/real' @ X4 @ X0))))) & ! [X5 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ ('const/sets/inf' @ X0) @ X5))) | ($true != (('const/sets/IN' @ 'type/realax/real' @ X5 @ X0))))) | ! [X1 : 'type/realax/real'] : ? [X2 : 'type/realax/real'] : (((('const/realax/real_le' @ X1 @ X2)) != $true) & ((('const/sets/IN' @ 'type/realax/real' @ X2 @ X0)) = $true)) | ('const/sets/EMPTY' @ 'type/realax/real' = X0))),
% 72.07/14.60 inference(flattening,[],[f38])).
% 72.07/14.60 thf(f40,plain,(
% 72.07/14.60 ! [X0 : ('type/realax/real' > $o)] : ((! [X3 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ ('const/sets/sup' @ X0) @ X3))) | ? [X4 : 'type/realax/real'] : (($true != (('const/realax/real_le' @ X4 @ X3))) & ($true = (('const/sets/IN' @ 'type/realax/real' @ X4 @ X0))))) & ! [X5 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ X5 @ ('const/sets/sup' @ X0)))) | ($true != (('const/sets/IN' @ 'type/realax/real' @ X5 @ X0))))) | (! [X1 : 'type/realax/real'] : ? [X2 : 'type/realax/real'] : (((('const/realax/real_le' @ X2 @ X1)) != $true) & ((('const/sets/IN' @ 'type/realax/real' @ X2 @ X0)) = $true)) | ('const/sets/EMPTY' @ 'type/realax/real' = X0)))),
% 72.07/14.60 inference(ennf_transformation,[],[f30])).
% 72.07/14.60 thf(f41,plain,(
% 72.07/14.60 ! [X0 : ('type/realax/real' > $o)] : ((! [X3 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ ('const/sets/sup' @ X0) @ X3))) | ? [X4 : 'type/realax/real'] : (($true != (('const/realax/real_le' @ X4 @ X3))) & ($true = (('const/sets/IN' @ 'type/realax/real' @ X4 @ X0))))) & ! [X5 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ X5 @ ('const/sets/sup' @ X0)))) | ($true != (('const/sets/IN' @ 'type/realax/real' @ X5 @ X0))))) | ! [X1 : 'type/realax/real'] : ? [X2 : 'type/realax/real'] : (((('const/realax/real_le' @ X2 @ X1)) != $true) & ((('const/sets/IN' @ 'type/realax/real' @ X2 @ X0)) = $true)) | ('const/sets/EMPTY' @ 'type/realax/real' = X0))),
% 72.07/14.60 inference(flattening,[],[f40])).
% 72.07/14.60 thf(f42,plain,(
% 72.07/14.60 ? [X0 : ('type/realax/real' > $o)] : ((((('const/sets/inf' @ X0) = ('const/sets/sup' @ X0))) != ((?? @ 'type/realax/real' @ (^[Y0 : 'type/realax/real']: (('const/sets/INSERT' @ 'type/realax/real' @ Y0 @ 'const/sets/EMPTY' @ 'type/realax/real') = X0))))) & (? [X1 : 'type/realax/real'] : ! [X2 : 'type/realax/real'] : (((('const/realax/real_le' @ ('const/realax/real_abs' @ X2) @ X1)) = $true) | ((('const/sets/IN' @ 'type/realax/real' @ X2 @ X0)) != $true)) & ('const/sets/EMPTY' @ 'type/realax/real' != X0)))),
% 72.07/14.60 inference(ennf_transformation,[],[f34])).
% 72.07/14.60 thf(f43,plain,(
% 72.07/14.60 ? [X0 : ('type/realax/real' > $o)] : ((((('const/sets/inf' @ X0) = ('const/sets/sup' @ X0))) != ((?? @ 'type/realax/real' @ (^[Y0 : 'type/realax/real']: (('const/sets/INSERT' @ 'type/realax/real' @ Y0 @ 'const/sets/EMPTY' @ 'type/realax/real') = X0))))) & ? [X1 : 'type/realax/real'] : ! [X2 : 'type/realax/real'] : (((('const/realax/real_le' @ ('const/realax/real_abs' @ X2) @ X1)) = $true) | ((('const/sets/IN' @ 'type/realax/real' @ X2 @ X0)) != $true)) & ('const/sets/EMPTY' @ 'type/realax/real' != X0))),
% 72.07/14.60 inference(flattening,[],[f42])).
% 72.07/14.60 thf(f44,plain,(
% 72.07/14.60 ! [X0 : ('type/realax/real' > $o)] : ((! [X1 : 'type/realax/real'] : (((('const/realax/real_le' @ X1 @ ('const/sets/inf' @ X0))) = $true) | ? [X2 : 'type/realax/real'] : (((('const/realax/real_le' @ X1 @ X2)) != $true) & ((('const/sets/IN' @ 'type/realax/real' @ X2 @ X0)) = $true))) & ! [X3 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ ('const/sets/inf' @ X0) @ X3))) | ($true != (('const/sets/IN' @ 'type/realax/real' @ X3 @ X0))))) | ! [X4 : 'type/realax/real'] : ? [X5 : 'type/realax/real'] : (($true != (('const/realax/real_le' @ X4 @ X5))) & ($true = (('const/sets/IN' @ 'type/realax/real' @ X5 @ X0)))) | ('const/sets/EMPTY' @ 'type/realax/real' = X0))),
% 72.07/14.60 inference(rectify,[],[f39])).
% 72.07/14.60 thf(f45,plain,(
% 72.07/14.60 ! [X0 : ('type/realax/real' > $o)] : ((! [X1 : 'type/realax/real'] : (((('const/realax/real_le' @ X1 @ ('const/sets/inf' @ X0))) = $true) | (($true != (('const/realax/real_le' @ X1 @ (sK0 @ X1 @ X0)))) & ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK0 @ X1 @ X0) @ X0))))) & ! [X3 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ ('const/sets/inf' @ X0) @ X3))) | ($true != (('const/sets/IN' @ 'type/realax/real' @ X3 @ X0))))) | ! [X4 : 'type/realax/real'] : (($true != (('const/realax/real_le' @ X4 @ (sK1 @ X4 @ X0)))) & ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK1 @ X4 @ X0) @ X0)))) | ('const/sets/EMPTY' @ 'type/realax/real' = X0))),
% 72.07/14.60 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP,vAPP]),skolemize(X5,sK1 @ X4 @ X0),skolemize(X5,sK1 @ X4 @ X0)],[f44])).
% 72.07/14.60 thf(f46,plain,(
% 72.07/14.60 ! [X0 : ('type/realax/real' > $o)] : ((! [X1 : 'type/realax/real'] : (((('const/realax/real_le' @ ('const/sets/sup' @ X0) @ X1)) = $true) | ? [X2 : 'type/realax/real'] : (((('const/realax/real_le' @ X2 @ X1)) != $true) & ((('const/sets/IN' @ 'type/realax/real' @ X2 @ X0)) = $true))) & ! [X3 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ X3 @ ('const/sets/sup' @ X0)))) | ($true != (('const/sets/IN' @ 'type/realax/real' @ X3 @ X0))))) | ! [X4 : 'type/realax/real'] : ? [X5 : 'type/realax/real'] : (($true != (('const/realax/real_le' @ X5 @ X4))) & ($true = (('const/sets/IN' @ 'type/realax/real' @ X5 @ X0)))) | ('const/sets/EMPTY' @ 'type/realax/real' = X0))),
% 72.07/14.60 inference(rectify,[],[f41])).
% 72.07/14.60 thf(f47,plain,(
% 72.07/14.60 ! [X0 : ('type/realax/real' > $o)] : ((! [X1 : 'type/realax/real'] : (((('const/realax/real_le' @ ('const/sets/sup' @ X0) @ X1)) = $true) | (($true != (('const/realax/real_le' @ (sK2 @ X1 @ X0) @ X1))) & ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK2 @ X1 @ X0) @ X0))))) & ! [X3 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ X3 @ ('const/sets/sup' @ X0)))) | ($true != (('const/sets/IN' @ 'type/realax/real' @ X3 @ X0))))) | ! [X4 : 'type/realax/real'] : (($true != (('const/realax/real_le' @ (sK3 @ X4 @ X0) @ X4))) & ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK3 @ X4 @ X0) @ X0)))) | ('const/sets/EMPTY' @ 'type/realax/real' = X0))),
% 72.07/14.60 inference(skolemize,[status(esa),new_symbols(skolem,[vAPP,vAPP]),skolemize(X5,sK1 @ X4 @ X0),skolemize(X5,sK1 @ X4 @ X0)],[f46])).
% 72.07/14.60 thf(f48,plain,(
% 72.07/14.60 (((('const/sets/inf' @ sK4) = ('const/sets/sup' @ sK4))) != ((?? @ 'type/realax/real' @ (^[Y0 : 'type/realax/real']: (('const/sets/INSERT' @ 'type/realax/real' @ Y0 @ 'const/sets/EMPTY' @ 'type/realax/real') = sK4))))) & ! [X2 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ ('const/realax/real_abs' @ X2) @ sK5))) | ($true != (('const/sets/IN' @ 'type/realax/real' @ X2 @ sK4)))) & ('const/sets/EMPTY' @ 'type/realax/real' != sK4)),
% 72.07/14.60 inference(skolemize,[status(esa),new_symbols(skolem,[sK4,sK5]),skolemize(X0,sK4),skolemize(X1,sK5)],[f43])).
% 72.07/14.60 thf(f52,plain,(
% 72.07/14.60 ( ! [X0 : $tType,X1 : X0] : (((('const/sets/IN' @ X0 @ X1 @ 'const/sets/EMPTY' @ X0)) != $true)) )),
% 72.07/14.60 inference(cnf_transformation,[],[f35])).
% 72.07/14.60 thf(f53,plain,(
% 72.07/14.60 ( ! [X0 : $tType,X2 : X0,X3 : (X0 > $o),X1 : X0] : (((('const/sets/IN' @ X0 @ X1 @ ('const/sets/INSERT' @ X0 @ X2 @ X3))) = (((X1 = X2) | ('const/sets/IN' @ X0 @ X1 @ X3))))) )),
% 72.07/14.60 inference(cnf_transformation,[],[f23])).
% 72.07/14.60 thf(f54,plain,(
% 72.07/14.60 ( ! [X0 : $tType,X2 : X0,X1 : (X0 > $o)] : (((('const/sets/IN' @ X0 @ X2 @ X1)) = ((X1 @ X2)))) )),
% 72.07/14.60 inference(cnf_transformation,[],[f6])).
% 72.07/14.60 thf(f55,plain,(
% 72.07/14.60 ( ! [X0 : $tType,X2 : (X0 > $o),X1 : (X0 > $o)] : ((((X1 = X2)) = ((!! @ X0 @ (^[Y0 : X0]: (('const/sets/IN' @ X0 @ Y0 @ X1) = ('const/sets/IN' @ X0 @ Y0 @ X2))))))) )),
% 72.07/14.60 inference(cnf_transformation,[],[f24])).
% 72.07/14.60 thf(f56,plain,(
% 72.07/14.60 ( ! [X3 : 'type/realax/real',X0 : ('type/realax/real' > $o),X4 : 'type/realax/real'] : (($true != (('const/sets/IN' @ 'type/realax/real' @ X3 @ X0))) | ($true = (('const/realax/real_le' @ ('const/sets/inf' @ X0) @ X3))) | ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK1 @ X4 @ X0) @ X0))) | ('const/sets/EMPTY' @ 'type/realax/real' = X0)) )),
% 72.07/14.60 inference(cnf_transformation,[],[f45])).
% 72.07/14.60 thf(f57,plain,(
% 72.07/14.60 ( ! [X3 : 'type/realax/real',X0 : ('type/realax/real' > $o),X4 : 'type/realax/real'] : (($true != (('const/realax/real_le' @ X4 @ (sK1 @ X4 @ X0)))) | ($true != (('const/sets/IN' @ 'type/realax/real' @ X3 @ X0))) | ($true = (('const/realax/real_le' @ ('const/sets/inf' @ X0) @ X3))) | ('const/sets/EMPTY' @ 'type/realax/real' = X0)) )),
% 72.07/14.60 inference(cnf_transformation,[],[f45])).
% 72.07/14.60 thf(f58,plain,(
% 72.07/14.60 ( ! [X0 : ('type/realax/real' > $o),X1 : 'type/realax/real',X4 : 'type/realax/real'] : (($true = (('const/sets/IN' @ 'type/realax/real' @ (sK1 @ X4 @ X0) @ X0))) | ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK0 @ X1 @ X0) @ X0))) | ((('const/realax/real_le' @ X1 @ ('const/sets/inf' @ X0))) = $true) | ('const/sets/EMPTY' @ 'type/realax/real' = X0)) )),
% 72.07/14.60 inference(cnf_transformation,[],[f45])).
% 72.07/14.60 thf(f59,plain,(
% 72.07/14.60 ( ! [X0 : ('type/realax/real' > $o),X1 : 'type/realax/real',X4 : 'type/realax/real'] : (($true != (('const/realax/real_le' @ X4 @ (sK1 @ X4 @ X0)))) | ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK0 @ X1 @ X0) @ X0))) | ((('const/realax/real_le' @ X1 @ ('const/sets/inf' @ X0))) = $true) | ('const/sets/EMPTY' @ 'type/realax/real' = X0)) )),
% 72.07/14.60 inference(cnf_transformation,[],[f45])).
% 72.07/14.60 thf(f60,plain,(
% 72.07/14.60 ( ! [X0 : ('type/realax/real' > $o),X1 : 'type/realax/real',X4 : 'type/realax/real'] : (($true != (('const/realax/real_le' @ X1 @ (sK0 @ X1 @ X0)))) | ((('const/realax/real_le' @ X1 @ ('const/sets/inf' @ X0))) = $true) | ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK1 @ X4 @ X0) @ X0))) | ('const/sets/EMPTY' @ 'type/realax/real' = X0)) )),
% 72.07/14.60 inference(cnf_transformation,[],[f45])).
% 72.07/14.60 thf(f61,plain,(
% 72.07/14.60 ( ! [X0 : ('type/realax/real' > $o),X1 : 'type/realax/real',X4 : 'type/realax/real'] : (($true != (('const/realax/real_le' @ X4 @ (sK1 @ X4 @ X0)))) | ($true != (('const/realax/real_le' @ X1 @ (sK0 @ X1 @ X0)))) | ((('const/realax/real_le' @ X1 @ ('const/sets/inf' @ X0))) = $true) | ('const/sets/EMPTY' @ 'type/realax/real' = X0)) )),
% 72.07/14.60 inference(cnf_transformation,[],[f45])).
% 72.07/14.60 thf(f62,plain,(
% 72.07/14.60 ( ! [X0 : 'type/realax/real',X1 : 'type/realax/real'] : (((('const/realax/real_le' @ ('const/realax/real_abs' @ X0) @ X1)) = ((('const/realax/real_le' @ ('const/realax/real_neg' @ X1) @ X0) & ('const/realax/real_le' @ X0 @ X1))))) )),
% 72.07/14.60 inference(cnf_transformation,[],[f28])).
% 72.07/14.60 thf(f63,plain,(
% 72.07/14.60 ( ! [X3 : 'type/realax/real',X0 : ('type/realax/real' > $o),X4 : 'type/realax/real'] : (($true != (('const/sets/IN' @ 'type/realax/real' @ X3 @ X0))) | ($true = (('const/realax/real_le' @ X3 @ ('const/sets/sup' @ X0)))) | ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK3 @ X4 @ X0) @ X0))) | ('const/sets/EMPTY' @ 'type/realax/real' = X0)) )),
% 72.07/14.60 inference(cnf_transformation,[],[f47])).
% 72.07/14.60 thf(f64,plain,(
% 72.07/14.60 ( ! [X3 : 'type/realax/real',X0 : ('type/realax/real' > $o),X4 : 'type/realax/real'] : (($true != (('const/realax/real_le' @ (sK3 @ X4 @ X0) @ X4))) | ($true != (('const/sets/IN' @ 'type/realax/real' @ X3 @ X0))) | ($true = (('const/realax/real_le' @ X3 @ ('const/sets/sup' @ X0)))) | ('const/sets/EMPTY' @ 'type/realax/real' = X0)) )),
% 72.07/14.60 inference(cnf_transformation,[],[f47])).
% 72.07/14.60 thf(f65,plain,(
% 72.07/14.60 ( ! [X0 : ('type/realax/real' > $o),X1 : 'type/realax/real',X4 : 'type/realax/real'] : (($true = (('const/sets/IN' @ 'type/realax/real' @ (sK3 @ X4 @ X0) @ X0))) | ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK2 @ X1 @ X0) @ X0))) | ((('const/realax/real_le' @ ('const/sets/sup' @ X0) @ X1)) = $true) | ('const/sets/EMPTY' @ 'type/realax/real' = X0)) )),
% 72.07/14.60 inference(cnf_transformation,[],[f47])).
% 72.07/14.60 thf(f66,plain,(
% 72.07/14.60 ( ! [X0 : ('type/realax/real' > $o),X1 : 'type/realax/real',X4 : 'type/realax/real'] : (($true != (('const/realax/real_le' @ (sK3 @ X4 @ X0) @ X4))) | ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK2 @ X1 @ X0) @ X0))) | ((('const/realax/real_le' @ ('const/sets/sup' @ X0) @ X1)) = $true) | ('const/sets/EMPTY' @ 'type/realax/real' = X0)) )),
% 72.07/14.60 inference(cnf_transformation,[],[f47])).
% 72.07/14.60 thf(f67,plain,(
% 72.07/14.60 ( ! [X0 : ('type/realax/real' > $o),X1 : 'type/realax/real',X4 : 'type/realax/real'] : (($true != (('const/realax/real_le' @ (sK2 @ X1 @ X0) @ X1))) | ((('const/realax/real_le' @ ('const/sets/sup' @ X0) @ X1)) = $true) | ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK3 @ X4 @ X0) @ X0))) | ('const/sets/EMPTY' @ 'type/realax/real' = X0)) )),
% 72.07/14.60 inference(cnf_transformation,[],[f47])).
% 72.07/14.60 thf(f68,plain,(
% 72.07/14.60 ( ! [X0 : ('type/realax/real' > $o),X1 : 'type/realax/real',X4 : 'type/realax/real'] : (($true != (('const/realax/real_le' @ (sK3 @ X4 @ X0) @ X4))) | ($true != (('const/realax/real_le' @ (sK2 @ X1 @ X0) @ X1))) | ((('const/realax/real_le' @ ('const/sets/sup' @ X0) @ X1)) = $true) | ('const/sets/EMPTY' @ 'type/realax/real' = X0)) )),
% 72.07/14.60 inference(cnf_transformation,[],[f47])).
% 72.07/14.60 thf(f69,plain,(
% 72.07/14.60 ( ! [X0 : 'type/realax/real',X1 : 'type/realax/real'] : ((((('const/realax/real_le' @ X0 @ X1) & ('const/realax/real_le' @ X1 @ X0))) = ((X0 = X1)))) )),
% 72.07/14.60 inference(cnf_transformation,[],[f32])).
% 72.07/14.60 thf(f70,plain,(
% 72.07/14.60 ('const/sets/EMPTY' @ 'type/realax/real' != sK4)),
% 72.07/14.60 inference(cnf_transformation,[],[f48])).
% 72.07/14.60 thf(f71,plain,(
% 72.07/14.60 ( ! [X2 : 'type/realax/real'] : (($true != (('const/sets/IN' @ 'type/realax/real' @ X2 @ sK4))) | ($true = (('const/realax/real_le' @ ('const/realax/real_abs' @ X2) @ sK5)))) )),
% 72.07/14.60 inference(cnf_transformation,[],[f48])).
% 72.07/14.60 thf(f72,plain,(
% 72.07/14.60 (((('const/sets/inf' @ sK4) = ('const/sets/sup' @ sK4))) != ((?? @ 'type/realax/real' @ (^[Y0 : 'type/realax/real']: (('const/sets/INSERT' @ 'type/realax/real' @ Y0 @ 'const/sets/EMPTY' @ 'type/realax/real') = sK4)))))),
% 72.07/14.60 inference(cnf_transformation,[],[f48])).
% 72.07/14.60 thf(f74,definition,(
% 72.07/14.60 ( ! [X0 : $o] : (($true = X0) | ($false = X0)) )),
% 72.07/14.60 introduced(theory,[fool_exhaustiveness_axiom])).
% 72.07/14.60 thf(f75,plain,(
% 72.07/14.60 ($true = ((('const/sets/inf' @ sK4) = ('const/sets/sup' @ sK4)))) | ($true = ((?? @ 'type/realax/real' @ (^[Y0 : 'type/realax/real']: (('const/sets/INSERT' @ 'type/realax/real' @ Y0 @ 'const/sets/EMPTY' @ 'type/realax/real') = sK4)))))),
% 72.07/14.60 inference(xor_proxy_clausification,[],[f72])).
% 72.07/14.60 thf(f76,plain,(
% 72.07/14.60 (((('const/sets/inf' @ sK4) = ('const/sets/sup' @ sK4))) = $false) | (((?? @ 'type/realax/real' @ (^[Y0 : 'type/realax/real']: (('const/sets/INSERT' @ 'type/realax/real' @ Y0 @ 'const/sets/EMPTY' @ 'type/realax/real') = sK4)))) = $false)),
% 72.07/14.60 inference(xor_proxy_clausification,[],[f72])).
% 72.07/14.60 thf(f77,plain,(
% 72.07/14.60 ((('const/sets/inf' @ sK4)) != (('const/sets/sup' @ sK4))) | (((?? @ 'type/realax/real' @ (^[Y0 : 'type/realax/real']: (('const/sets/INSERT' @ 'type/realax/real' @ Y0 @ 'const/sets/EMPTY' @ 'type/realax/real') = sK4)))) = $false)),
% 72.07/14.60 inference(equality_proxy_clausification,[],[f76])).
% 72.07/14.60 thf(f78,plain,(
% 72.07/14.60 ( ! [X1 : 'type/realax/real'] : (((('const/sets/inf' @ sK4)) != (('const/sets/sup' @ sK4))) | ($false = (((^[Y0 : 'type/realax/real']: (('const/sets/INSERT' @ 'type/realax/real' @ Y0 @ 'const/sets/EMPTY' @ 'type/realax/real') = sK4)) @ X1)))) )),
% 72.07/14.60 inference(pi_proxy_clausification,[],[f77])).
% 72.07/14.60 thf(f79,plain,(
% 72.07/14.60 ( ! [X1 : 'type/realax/real'] : (((('const/sets/inf' @ sK4)) != (('const/sets/sup' @ sK4))) | ($false = ((('const/sets/INSERT' @ 'type/realax/real' @ X1 @ 'const/sets/EMPTY' @ 'type/realax/real') = sK4)))) )),
% 72.07/14.60 inference(beta-eta_normalization,[],[f78])).
% 72.07/14.60 thf(f80,plain,(
% 72.07/14.60 ( ! [X1 : 'type/realax/real'] : (((('const/sets/inf' @ sK4)) != (('const/sets/sup' @ sK4))) | (sK4 != (('const/sets/INSERT' @ 'type/realax/real' @ X1 @ 'const/sets/EMPTY' @ 'type/realax/real')))) )),
% 72.07/14.60 inference(equality_proxy_clausification,[],[f79])).
% 72.07/14.60 thf(f81,plain,(
% 72.07/14.60 ((('const/sets/inf' @ sK4)) = (('const/sets/sup' @ sK4))) | ($true = ((?? @ 'type/realax/real' @ (^[Y0 : 'type/realax/real']: (('const/sets/INSERT' @ 'type/realax/real' @ Y0 @ 'const/sets/EMPTY' @ 'type/realax/real') = sK4)))))),
% 72.07/14.60 inference(equality_proxy_clausification,[],[f75])).
% 72.07/14.60 thf(f82,plain,(
% 72.07/14.60 ((('const/sets/inf' @ sK4)) = (('const/sets/sup' @ sK4))) | ($true = (((^[Y0 : 'type/realax/real']: (('const/sets/INSERT' @ 'type/realax/real' @ Y0 @ 'const/sets/EMPTY' @ 'type/realax/real') = sK4)) @ sK6)))),
% 72.07/14.60 inference(sigma_proxy_clausification,[],[f81])).
% 72.07/14.60 thf(f83,plain,(
% 72.07/14.60 ((('const/sets/inf' @ sK4)) = (('const/sets/sup' @ sK4))) | ($true = ((('const/sets/INSERT' @ 'type/realax/real' @ sK6 @ 'const/sets/EMPTY' @ 'type/realax/real') = sK4)))),
% 72.07/14.60 inference(beta-eta_normalization,[],[f82])).
% 72.07/14.60 thf(f84,plain,(
% 72.07/14.60 ((('const/sets/inf' @ sK4)) = (('const/sets/sup' @ sK4))) | (sK4 = (('const/sets/INSERT' @ 'type/realax/real' @ sK6 @ 'const/sets/EMPTY' @ 'type/realax/real')))),
% 72.07/14.60 inference(equality_proxy_clausification,[],[f83])).
% 72.07/14.60 thf(f85,plain,(
% 72.07/14.60 ( ! [X0 : 'type/realax/real',X1 : 'type/realax/real'] : (($true = ((('const/realax/real_le' @ X0 @ X1) & ('const/realax/real_le' @ X1 @ X0)))) | (((X0 = X1)) = $false)) )),
% 72.07/14.60 inference(iff_proxy_clausification,[],[f69])).
% 72.07/14.60 thf(f86,plain,(
% 72.07/14.60 ( ! [X0 : 'type/realax/real',X1 : 'type/realax/real'] : ((((('const/realax/real_le' @ X0 @ X1) & ('const/realax/real_le' @ X1 @ X0))) = $false) | ($true = ((X0 = X1)))) )),
% 72.07/14.60 inference(iff_proxy_clausification,[],[f69])).
% 72.07/14.60 thf(f87,plain,(
% 72.07/14.60 ( ! [X0 : 'type/realax/real',X1 : 'type/realax/real'] : (((('const/realax/real_le' @ X1 @ X0)) = $false) | ($true = ((X0 = X1))) | ((('const/realax/real_le' @ X0 @ X1)) = $false)) )),
% 72.07/14.60 inference(and_proxy_clausification,[],[f86])).
% 72.07/14.60 thf(f88,plain,(
% 72.07/14.60 ( ! [X0 : 'type/realax/real',X1 : 'type/realax/real'] : (((('const/realax/real_le' @ X1 @ X0)) = $false) | ((('const/realax/real_le' @ X0 @ X1)) = $false) | (X0 = X1)) )),
% 72.07/14.60 inference(equality_proxy_clausification,[],[f87])).
% 72.07/14.60 thf(f90,plain,(
% 72.07/14.60 ( ! [X0 : 'type/realax/real',X1 : 'type/realax/real'] : (((('const/realax/real_le' @ X0 @ X1)) = $true) | (((X0 = X1)) = $false)) )),
% 72.07/14.60 inference(and_proxy_clausification,[],[f85])).
% 72.07/14.60 thf(f91,plain,(
% 72.07/14.60 ( ! [X0 : 'type/realax/real',X1 : 'type/realax/real'] : (((('const/realax/real_le' @ X0 @ X1)) = $true) | (X0 != X1)) )),
% 72.07/14.60 inference(equality_proxy_clausification,[],[f90])).
% 72.07/14.60 thf(f94,plain,(
% 72.07/14.60 ( ! [X0 : 'type/realax/real',X1 : 'type/realax/real'] : (((('const/realax/real_le' @ ('const/realax/real_abs' @ X0) @ X1)) = $false) | ($true = ((('const/realax/real_le' @ ('const/realax/real_neg' @ X1) @ X0) & ('const/realax/real_le' @ X0 @ X1))))) )),
% 72.07/14.60 inference(iff_proxy_clausification,[],[f62])).
% 72.07/14.60 thf(f95,plain,(
% 72.07/14.60 ( ! [X0 : 'type/realax/real',X1 : 'type/realax/real'] : (((('const/realax/real_le' @ ('const/realax/real_abs' @ X0) @ X1)) = $false) | ((('const/realax/real_le' @ X0 @ X1)) = $true)) )),
% 72.07/14.60 inference(and_proxy_clausification,[],[f94])).
% 72.07/14.60 thf(f96,plain,(
% 72.07/14.60 ( ! [X0 : 'type/realax/real',X1 : 'type/realax/real'] : (((('const/realax/real_le' @ ('const/realax/real_abs' @ X0) @ X1)) = $false) | ((('const/realax/real_le' @ ('const/realax/real_neg' @ X1) @ X0)) = $true)) )),
% 72.07/14.60 inference(and_proxy_clausification,[],[f94])).
% 72.07/14.60 thf(f99,plain,(
% 72.07/14.60 ( ! [X0 : $tType,X2 : (X0 > $o),X1 : (X0 > $o)] : ((((X1 = X2)) = $false) | ($true = ((!! @ X0 @ (^[Y0 : X0]: (('const/sets/IN' @ X0 @ Y0 @ X1) = ('const/sets/IN' @ X0 @ Y0 @ X2))))))) )),
% 72.07/14.60 inference(iff_proxy_clausification,[],[f55])).
% 72.07/14.60 thf(f100,plain,(
% 72.07/14.60 ( ! [X0 : $tType,X2 : (X0 > $o),X1 : (X0 > $o)] : ((X1 != X2) | ($true = ((!! @ X0 @ (^[Y0 : X0]: (('const/sets/IN' @ X0 @ Y0 @ X1) = ('const/sets/IN' @ X0 @ Y0 @ X2))))))) )),
% 72.07/14.60 inference(equality_proxy_clausification,[],[f99])).
% 72.07/14.60 thf(f101,plain,(
% 72.07/14.60 ( ! [X0 : $tType,X2 : (X0 > $o),X3 : X0,X1 : (X0 > $o)] : ((X1 != X2) | ($true = (((^[Y0 : X0]: (('const/sets/IN' @ X0 @ Y0 @ X1) = ('const/sets/IN' @ X0 @ Y0 @ X2))) @ X3)))) )),
% 72.07/14.60 inference(pi_proxy_clausification,[],[f100])).
% 72.07/14.60 thf(f102,plain,(
% 72.07/14.60 ( ! [X0 : $tType,X2 : (X0 > $o),X3 : X0,X1 : (X0 > $o)] : ((X1 != X2) | ($true = ((('const/sets/IN' @ X0 @ X3 @ X1) = ('const/sets/IN' @ X0 @ X3 @ X2))))) )),
% 72.07/14.60 inference(beta-eta_normalization,[],[f101])).
% 72.07/14.60 thf(f103,plain,(
% 72.07/14.60 ( ! [X0 : $tType,X2 : (X0 > $o),X3 : X0,X1 : (X0 > $o)] : ((X1 != X2) | ((('const/sets/IN' @ X0 @ X3 @ X1)) = (('const/sets/IN' @ X0 @ X3 @ X2)))) )),
% 72.07/14.60 inference(equality_proxy_clausification,[],[f102])).
% 72.07/14.60 thf(f104,plain,(
% 72.07/14.60 ( ! [X0 : $tType,X2 : (X0 > $o),X3 : X0,X1 : (X0 > $o)] : (((('const/sets/IN' @ X0 @ X3 @ X1)) = $true) | ((('const/sets/IN' @ X0 @ X3 @ X2)) = $false) | (X1 != X2)) )),
% 72.07/14.60 inference(iff_proxy_clausification,[],[f103])).
% 72.07/14.60 thf(f112,plain,(
% 72.07/14.60 ( ! [X0 : $tType,X2 : X0,X1 : (X0 > $o)] : (((('const/sets/IN' @ X0 @ X2 @ X1)) = $true) | (((X1 @ X2)) = $false)) )),
% 72.07/14.60 inference(iff_proxy_clausification,[],[f54])).
% 72.07/14.60 thf(f113,plain,(
% 72.07/14.60 ( ! [X0 : $tType,X2 : X0,X1 : (X0 > $o)] : (((('const/sets/IN' @ X0 @ X2 @ X1)) = $false) | (((X1 @ X2)) = $true)) )),
% 72.07/14.60 inference(iff_proxy_clausification,[],[f54])).
% 72.07/14.60 thf(f114,plain,(
% 72.07/14.60 ( ! [X0 : $tType,X2 : X0,X3 : (X0 > $o),X1 : X0] : (((('const/sets/IN' @ X0 @ X1 @ ('const/sets/INSERT' @ X0 @ X2 @ X3))) = $true) | ((((X1 = X2) | ('const/sets/IN' @ X0 @ X1 @ X3))) = $false)) )),
% 72.07/14.60 inference(iff_proxy_clausification,[],[f53])).
% 72.07/14.60 thf(f115,plain,(
% 72.07/14.60 ( ! [X0 : $tType,X2 : X0,X3 : (X0 > $o),X1 : X0] : (((('const/sets/IN' @ X0 @ X1 @ ('const/sets/INSERT' @ X0 @ X2 @ X3))) = $false) | ($true = (((X1 = X2) | ('const/sets/IN' @ X0 @ X1 @ X3))))) )),
% 72.07/14.60 inference(iff_proxy_clausification,[],[f53])).
% 72.07/14.60 thf(f116,plain,(
% 72.07/14.60 ( ! [X0 : $tType,X2 : X0,X3 : (X0 > $o),X1 : X0] : (((('const/sets/IN' @ X0 @ X1 @ ('const/sets/INSERT' @ X0 @ X2 @ X3))) = $false) | ((('const/sets/IN' @ X0 @ X1 @ X3)) = $true) | ($true = ((X1 = X2)))) )),
% 72.07/14.60 inference(or_proxy_clausification,[],[f115])).
% 72.07/14.60 thf(f117,plain,(
% 72.07/14.60 ( ! [X0 : $tType,X2 : X0,X3 : (X0 > $o),X1 : X0] : (((('const/sets/IN' @ X0 @ X1 @ ('const/sets/INSERT' @ X0 @ X2 @ X3))) = $false) | ((('const/sets/IN' @ X0 @ X1 @ X3)) = $true) | (X1 = X2)) )),
% 72.07/14.60 inference(equality_proxy_clausification,[],[f116])).
% 72.07/14.60 thf(f119,plain,(
% 72.07/14.60 ( ! [X0 : $tType,X2 : X0,X3 : (X0 > $o),X1 : X0] : (((('const/sets/IN' @ X0 @ X1 @ ('const/sets/INSERT' @ X0 @ X2 @ X3))) = $true) | (((X1 = X2)) = $false)) )),
% 72.07/14.60 inference(or_proxy_clausification,[],[f114])).
% 72.07/14.60 thf(f120,plain,(
% 72.07/14.60 ( ! [X0 : $tType,X2 : X0,X3 : (X0 > $o),X1 : X0] : (((('const/sets/IN' @ X0 @ X1 @ ('const/sets/INSERT' @ X0 @ X2 @ X3))) = $true) | (X1 != X2)) )),
% 72.07/14.60 inference(equality_proxy_clausification,[],[f119])).
% 72.07/14.60 thf(f122,definition,(
% 72.07/14.60 spl8_1 <=> ! [X1 : 'type/realax/real'] : (sK4 != (('const/sets/INSERT' @ 'type/realax/real' @ X1 @ 'const/sets/EMPTY' @ 'type/realax/real')))),
% 72.07/14.60 introduced(definition,[new_symbols(definition,[spl8_1])],[avatar_definition])).
% 72.07/14.60 thf(f123,plain,(
% 72.07/14.60 ( ! [X1 : 'type/realax/real'] : ((sK4 != (('const/sets/INSERT' @ 'type/realax/real' @ X1 @ 'const/sets/EMPTY' @ 'type/realax/real')))) ) | ~spl8_1),
% 72.07/14.60 inference(avatar_component_clause,[],[f122])).
% 72.07/14.60 thf(f125,definition,(
% 72.07/14.60 spl8_2 <=> ((('const/sets/inf' @ sK4)) = (('const/sets/sup' @ sK4)))),
% 72.07/14.60 introduced(definition,[new_symbols(definition,[spl8_2])],[avatar_definition])).
% 72.07/14.60 thf(f126,plain,(
% 72.07/14.60 ((('const/sets/inf' @ sK4)) = (('const/sets/sup' @ sK4))) | ~spl8_2),
% 72.07/14.60 inference(avatar_component_clause,[],[f125])).
% 72.07/14.60 thf(f127,plain,(
% 72.07/14.60 ((('const/sets/inf' @ sK4)) != (('const/sets/sup' @ sK4))) | spl8_2),
% 72.07/14.60 inference(avatar_component_clause,[],[f125])).
% 72.07/14.60 thf(f128,plain,(
% 72.07/14.60 spl8_1 | ~spl8_2),
% 72.07/14.60 inference(avatar_split_clause,[],[f80,f125,f122])).
% 72.07/14.60 thf(f130,definition,(
% 72.07/14.60 spl8_3 <=> (sK4 = (('const/sets/INSERT' @ 'type/realax/real' @ sK6 @ 'const/sets/EMPTY' @ 'type/realax/real')))),
% 72.07/14.60 introduced(definition,[new_symbols(definition,[spl8_3])],[avatar_definition])).
% 72.07/14.60 thf(f132,plain,(
% 72.07/14.60 (sK4 = (('const/sets/INSERT' @ 'type/realax/real' @ sK6 @ 'const/sets/EMPTY' @ 'type/realax/real'))) | ~spl8_3),
% 72.07/14.60 inference(avatar_component_clause,[],[f130])).
% 72.07/14.60 thf(f133,plain,(
% 72.07/14.60 spl8_3 | spl8_2),
% 72.07/14.60 inference(avatar_split_clause,[],[f84,f125,f130])).
% 72.07/14.60 thf(f134,plain,(
% 72.07/14.60 ((('const/sets/EMPTY' @ 'type/realax/real' @ sK9)) != ((sK4 @ sK9)))),
% 72.07/14.60 inference(negative_extensionality,[],[f70])).
% 72.07/14.60 thf(f135,plain,(
% 72.07/14.60 ($true = (('const/sets/EMPTY' @ 'type/realax/real' @ sK9))) | ($true = ((sK4 @ sK9)))),
% 72.07/14.60 inference(xor_proxy_clausification,[],[f134])).
% 72.07/14.60 thf(f138,definition,(
% 72.07/14.60 spl8_4 <=> ($false = ((sK4 @ sK9)))),
% 72.07/14.60 introduced(definition,[new_symbols(definition,[spl8_4])],[avatar_definition])).
% 72.07/14.60 thf(f139,plain,(
% 72.07/14.60 ($false != ((sK4 @ sK9))) | spl8_4),
% 72.07/14.60 inference(avatar_component_clause,[],[f138])).
% 72.07/14.60 thf(f140,plain,(
% 72.07/14.60 ($false = ((sK4 @ sK9))) | ~spl8_4),
% 72.07/14.60 inference(avatar_component_clause,[],[f138])).
% 72.07/14.60 thf(f147,definition,(
% 72.07/14.60 spl8_6 <=> ($true = ((sK4 @ sK9)))),
% 72.07/14.60 introduced(definition,[new_symbols(definition,[spl8_6])],[avatar_definition])).
% 72.07/14.60 thf(f149,plain,(
% 72.07/14.60 ($true = ((sK4 @ sK9))) | ~spl8_6),
% 72.07/14.60 inference(avatar_component_clause,[],[f147])).
% 72.07/14.60 thf(f151,definition,(
% 72.07/14.60 spl8_7 <=> ($true = (('const/sets/EMPTY' @ 'type/realax/real' @ sK9)))),
% 72.07/14.60 introduced(definition,[new_symbols(definition,[spl8_7])],[avatar_definition])).
% 72.07/14.60 thf(f153,plain,(
% 72.07/14.60 ($true = (('const/sets/EMPTY' @ 'type/realax/real' @ sK9))) | ~spl8_7),
% 72.07/14.60 inference(avatar_component_clause,[],[f151])).
% 72.07/14.60 thf(f154,plain,(
% 72.07/14.60 spl8_6 | spl8_7),
% 72.07/14.60 inference(avatar_split_clause,[],[f135,f151,f147])).
% 72.07/14.60 thf(f155,plain,(
% 72.07/14.60 ($true = $false) | (~spl8_4 | ~spl8_6)),
% 72.07/14.60 inference(forward_demodulation,[],[f149,f140])).
% 72.07/14.60 thf(f156,plain,(
% 72.07/14.60 $false | (~spl8_4 | ~spl8_6)),
% 72.07/14.60 inference(trivial_inequality_removal,[],[f155])).
% 72.07/14.60 thf(f157,plain,(
% 72.07/14.60 ~spl8_4 | ~spl8_6),
% 72.07/14.60 inference(avatar_contradiction_clause,[],[f156])).
% 72.07/14.60 thf(f161,plain,(
% 72.07/14.60 ( ! [X0 : 'type/realax/real'] : (($true != $true) | ($true = (('const/realax/real_le' @ ('const/realax/real_abs' @ X0) @ sK5))) | ($false = (('const/sets/IN' @ 'type/realax/real' @ X0 @ sK4)))) )),
% 72.07/14.60 inference(constrained_superposition,[],[f71,f74])).
% 72.07/14.60 thf(f164,plain,(
% 72.07/14.60 ( ! [X0 : 'type/realax/real'] : (($false = (('const/sets/IN' @ 'type/realax/real' @ X0 @ sK4))) | ($true = (('const/realax/real_le' @ ('const/realax/real_abs' @ X0) @ sK5)))) )),
% 72.07/14.60 inference(trivial_inequality_removal,[],[f161])).
% 72.07/14.60 thf(f171,plain,(
% 72.07/14.60 ( ! [X2 : 'type/realax/real',X0 : 'type/realax/real',X1 : ('type/realax/real' > $o)] : (($true != $true) | ($true != (('const/sets/IN' @ 'type/realax/real' @ X2 @ X1))) | ($true = (('const/realax/real_le' @ ('const/sets/inf' @ X1) @ X2))) | ('const/sets/EMPTY' @ 'type/realax/real' = X1) | ($false = (('const/realax/real_le' @ X0 @ (sK1 @ X0 @ X1))))) )),
% 72.07/14.60 inference(constrained_superposition,[],[f57,f74])).
% 72.07/14.60 thf(f172,plain,(
% 72.07/14.60 ( ! [X2 : 'type/realax/real',X0 : 'type/realax/real',X1 : ('type/realax/real' > $o)] : (($true != (('const/sets/IN' @ 'type/realax/real' @ X2 @ X1))) | ($true = (('const/realax/real_le' @ ('const/sets/inf' @ X1) @ X2))) | ('const/sets/EMPTY' @ 'type/realax/real' = X1) | ($false = (('const/realax/real_le' @ X0 @ (sK1 @ X0 @ X1))))) )),
% 72.07/14.60 inference(trivial_inequality_removal,[],[f171])).
% 72.07/14.60 thf(f175,plain,(
% 72.07/14.60 ( ! [X2 : 'type/realax/real',X0 : 'type/realax/real',X1 : ('type/realax/real' > $o)] : (($true != $true) | ($true != (('const/sets/IN' @ 'type/realax/real' @ X2 @ X1))) | ($true = (('const/realax/real_le' @ X2 @ ('const/sets/sup' @ X1)))) | ('const/sets/EMPTY' @ 'type/realax/real' = X1) | ($false = (('const/realax/real_le' @ (sK3 @ X0 @ X1) @ X0)))) )),
% 72.07/14.60 inference(constrained_superposition,[],[f64,f74])).
% 72.07/14.60 thf(f176,plain,(
% 72.07/14.60 ( ! [X2 : 'type/realax/real',X0 : 'type/realax/real',X1 : ('type/realax/real' > $o)] : (($true != (('const/sets/IN' @ 'type/realax/real' @ X2 @ X1))) | ($true = (('const/realax/real_le' @ X2 @ ('const/sets/sup' @ X1)))) | ('const/sets/EMPTY' @ 'type/realax/real' = X1) | ($false = (('const/realax/real_le' @ (sK3 @ X0 @ X1) @ X0)))) )),
% 72.07/14.60 inference(trivial_inequality_removal,[],[f175])).
% 72.07/14.60 thf(f177,plain,(
% 72.07/14.60 ( ! [X2 : 'type/realax/real',X0 : 'type/realax/real',X1 : ('type/realax/real' > $o)] : (($true != $true) | ($true = (('const/realax/real_le' @ ('const/sets/inf' @ X1) @ X0))) | ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK1 @ X2 @ X1) @ X1))) | ('const/sets/EMPTY' @ 'type/realax/real' = X1) | ($false = (('const/sets/IN' @ 'type/realax/real' @ X0 @ X1)))) )),
% 72.07/14.60 inference(constrained_superposition,[],[f56,f74])).
% 72.07/14.60 thf(f178,plain,(
% 72.07/14.60 ( ! [X2 : 'type/realax/real',X0 : 'type/realax/real',X1 : ('type/realax/real' > $o)] : (($true = (('const/sets/IN' @ 'type/realax/real' @ (sK1 @ X2 @ X1) @ X1))) | ($true = (('const/realax/real_le' @ ('const/sets/inf' @ X1) @ X0))) | ('const/sets/EMPTY' @ 'type/realax/real' = X1) | ($false = (('const/sets/IN' @ 'type/realax/real' @ X0 @ X1)))) )),
% 72.07/14.60 inference(trivial_inequality_removal,[],[f177])).
% 72.07/14.60 thf(f179,plain,(
% 72.07/14.60 ( ! [X2 : 'type/realax/real',X0 : 'type/realax/real',X1 : ('type/realax/real' > $o)] : (($true != $true) | ($true = (('const/realax/real_le' @ X0 @ ('const/sets/sup' @ X1)))) | ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK3 @ X2 @ X1) @ X1))) | ('const/sets/EMPTY' @ 'type/realax/real' = X1) | ($false = (('const/sets/IN' @ 'type/realax/real' @ X0 @ X1)))) )),
% 72.07/14.60 inference(constrained_superposition,[],[f63,f74])).
% 72.07/14.60 thf(f180,plain,(
% 72.07/14.60 ( ! [X2 : 'type/realax/real',X0 : 'type/realax/real',X1 : ('type/realax/real' > $o)] : (($true = (('const/sets/IN' @ 'type/realax/real' @ (sK3 @ X2 @ X1) @ X1))) | ($true = (('const/realax/real_le' @ X0 @ ('const/sets/sup' @ X1)))) | ('const/sets/EMPTY' @ 'type/realax/real' = X1) | ($false = (('const/sets/IN' @ 'type/realax/real' @ X0 @ X1)))) )),
% 72.07/14.61 inference(trivial_inequality_removal,[],[f179])).
% 72.07/14.61 thf(f181,plain,(
% 72.07/14.61 ( ! [X2 : 'type/realax/real',X0 : 'type/realax/real',X1 : ('type/realax/real' > $o)] : (($true != $true) | ($true != (('const/realax/real_le' @ X2 @ (sK0 @ X2 @ X1)))) | ($true = (('const/realax/real_le' @ X2 @ ('const/sets/inf' @ X1)))) | ('const/sets/EMPTY' @ 'type/realax/real' = X1) | ($false = (('const/realax/real_le' @ X0 @ (sK1 @ X0 @ X1))))) )),
% 72.07/14.61 inference(constrained_superposition,[],[f61,f74])).
% 72.07/14.61 thf(f182,plain,(
% 72.07/14.61 ( ! [X2 : 'type/realax/real',X0 : 'type/realax/real',X1 : ('type/realax/real' > $o)] : (($true != (('const/realax/real_le' @ X2 @ (sK0 @ X2 @ X1)))) | ($true = (('const/realax/real_le' @ X2 @ ('const/sets/inf' @ X1)))) | ('const/sets/EMPTY' @ 'type/realax/real' = X1) | ($false = (('const/realax/real_le' @ X0 @ (sK1 @ X0 @ X1))))) )),
% 72.07/14.61 inference(trivial_inequality_removal,[],[f181])).
% 72.07/14.61 thf(f183,plain,(
% 72.07/14.61 ( ! [X2 : 'type/realax/real',X0 : 'type/realax/real',X1 : ('type/realax/real' > $o)] : (($true != $true) | ($true != (('const/realax/real_le' @ (sK2 @ X2 @ X1) @ X2))) | ($true = (('const/realax/real_le' @ ('const/sets/sup' @ X1) @ X2))) | ('const/sets/EMPTY' @ 'type/realax/real' = X1) | ($false = (('const/realax/real_le' @ (sK3 @ X0 @ X1) @ X0)))) )),
% 72.07/14.61 inference(constrained_superposition,[],[f68,f74])).
% 72.07/14.61 thf(f184,plain,(
% 72.07/14.61 ( ! [X2 : 'type/realax/real',X0 : 'type/realax/real',X1 : ('type/realax/real' > $o)] : (($true != (('const/realax/real_le' @ (sK2 @ X2 @ X1) @ X2))) | ($true = (('const/realax/real_le' @ ('const/sets/sup' @ X1) @ X2))) | ('const/sets/EMPTY' @ 'type/realax/real' = X1) | ($false = (('const/realax/real_le' @ (sK3 @ X0 @ X1) @ X0)))) )),
% 72.07/14.61 inference(trivial_inequality_removal,[],[f183])).
% 72.07/14.61 thf(f192,plain,(
% 72.07/14.61 ( ! [X2 : 'type/realax/real',X0 : 'type/realax/real',X1 : ('type/realax/real' > $o)] : (($true != $true) | ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK2 @ X2 @ X1) @ X1))) | ($true = (('const/realax/real_le' @ ('const/sets/sup' @ X1) @ X2))) | ('const/sets/EMPTY' @ 'type/realax/real' = X1) | ($false = (('const/realax/real_le' @ (sK3 @ X0 @ X1) @ X0)))) )),
% 72.07/14.61 inference(constrained_superposition,[],[f66,f74])).
% 72.07/14.61 thf(f193,plain,(
% 72.07/14.61 ( ! [X2 : 'type/realax/real',X0 : 'type/realax/real',X1 : ('type/realax/real' > $o)] : (($true = (('const/sets/IN' @ 'type/realax/real' @ (sK2 @ X2 @ X1) @ X1))) | ($false = (('const/realax/real_le' @ (sK3 @ X0 @ X1) @ X0))) | ('const/sets/EMPTY' @ 'type/realax/real' = X1) | ($true = (('const/realax/real_le' @ ('const/sets/sup' @ X1) @ X2)))) )),
% 72.07/14.61 inference(trivial_inequality_removal,[],[f192])).
% 72.07/14.61 thf(f194,plain,(
% 72.07/14.61 ( ! [X2 : 'type/realax/real',X0 : 'type/realax/real',X1 : ('type/realax/real' > $o)] : (($true != $true) | ($true = (('const/realax/real_le' @ ('const/sets/sup' @ X1) @ X0))) | ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK3 @ X2 @ X1) @ X1))) | ('const/sets/EMPTY' @ 'type/realax/real' = X1) | ($false = (('const/realax/real_le' @ (sK2 @ X0 @ X1) @ X0)))) )),
% 72.07/14.61 inference(constrained_superposition,[],[f67,f74])).
% 72.07/14.61 thf(f195,plain,(
% 72.07/14.61 ( ! [X2 : 'type/realax/real',X0 : 'type/realax/real',X1 : ('type/realax/real' > $o)] : (($true = (('const/sets/IN' @ 'type/realax/real' @ (sK3 @ X2 @ X1) @ X1))) | ($false = (('const/realax/real_le' @ (sK2 @ X0 @ X1) @ X0))) | ('const/sets/EMPTY' @ 'type/realax/real' = X1) | ($true = (('const/realax/real_le' @ ('const/sets/sup' @ X1) @ X0)))) )),
% 72.07/14.61 inference(trivial_inequality_removal,[],[f194])).
% 72.07/14.61 thf(f215,definition,(
% 72.07/14.61 spl8_8 <=> ! [X1 : 'type/realax/real'] : ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK1 @ X1 @ sK4) @ sK4)))),
% 72.07/14.61 introduced(definition,[new_symbols(definition,[spl8_8])],[avatar_definition])).
% 72.07/14.61 thf(f216,plain,(
% 72.07/14.61 ( ! [X1 : 'type/realax/real'] : (($true = (('const/sets/IN' @ 'type/realax/real' @ (sK1 @ X1 @ sK4) @ sK4)))) ) | ~spl8_8),
% 72.07/14.61 inference(avatar_component_clause,[],[f215])).
% 72.07/14.61 thf(f222,definition,(
% 72.07/14.61 spl8_10 <=> ! [X1 : 'type/realax/real'] : (($true = (('const/sets/IN' @ 'type/realax/real' @ (sK0 @ X1 @ sK4) @ sK4))) | ($true = (('const/realax/real_le' @ X1 @ ('const/sets/inf' @ sK4)))))),
% 72.07/14.61 introduced(definition,[new_symbols(definition,[spl8_10])],[avatar_definition])).
% 72.07/14.61 thf(f223,plain,(
% 72.07/14.61 ( ! [X1 : 'type/realax/real'] : (($true = (('const/sets/IN' @ 'type/realax/real' @ (sK0 @ X1 @ sK4) @ sK4))) | ($true = (('const/realax/real_le' @ X1 @ ('const/sets/inf' @ sK4))))) ) | ~spl8_10),
% 72.07/14.61 inference(avatar_component_clause,[],[f222])).
% 72.07/14.61 thf(f225,definition,(
% 72.07/14.61 spl8_11 <=> ! [X0 : 'type/realax/real'] : ($true = (('const/realax/real_le' @ ('const/realax/real_abs' @ (sK1 @ X0 @ sK4)) @ sK5)))),
% 72.07/14.61 introduced(definition,[new_symbols(definition,[spl8_11])],[avatar_definition])).
% 72.07/14.61 thf(f226,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ ('const/realax/real_abs' @ (sK1 @ X0 @ sK4)) @ sK5)))) ) | ~spl8_11),
% 72.07/14.61 inference(avatar_component_clause,[],[f225])).
% 72.07/14.61 thf(f247,definition,(
% 72.07/14.61 spl8_12 <=> ! [X1 : 'type/realax/real'] : ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK3 @ X1 @ sK4) @ sK4)))),
% 72.07/14.61 introduced(definition,[new_symbols(definition,[spl8_12])],[avatar_definition])).
% 72.07/14.61 thf(f248,plain,(
% 72.07/14.61 ( ! [X1 : 'type/realax/real'] : (($true = (('const/sets/IN' @ 'type/realax/real' @ (sK3 @ X1 @ sK4) @ sK4)))) ) | ~spl8_12),
% 72.07/14.61 inference(avatar_component_clause,[],[f247])).
% 72.07/14.61 thf(f254,definition,(
% 72.07/14.61 spl8_14 <=> ! [X1 : 'type/realax/real'] : (($true = (('const/sets/IN' @ 'type/realax/real' @ (sK2 @ X1 @ sK4) @ sK4))) | ($true = (('const/realax/real_le' @ ('const/sets/sup' @ sK4) @ X1))))),
% 72.07/14.61 introduced(definition,[new_symbols(definition,[spl8_14])],[avatar_definition])).
% 72.07/14.61 thf(f255,plain,(
% 72.07/14.61 ( ! [X1 : 'type/realax/real'] : (($true = (('const/sets/IN' @ 'type/realax/real' @ (sK2 @ X1 @ sK4) @ sK4))) | ($true = (('const/realax/real_le' @ ('const/sets/sup' @ sK4) @ X1)))) ) | ~spl8_14),
% 72.07/14.61 inference(avatar_component_clause,[],[f254])).
% 72.07/14.61 thf(f257,definition,(
% 72.07/14.61 spl8_15 <=> ! [X0 : 'type/realax/real'] : ($true = (('const/realax/real_le' @ ('const/realax/real_abs' @ (sK3 @ X0 @ sK4)) @ sK5)))),
% 72.07/14.61 introduced(definition,[new_symbols(definition,[spl8_15])],[avatar_definition])).
% 72.07/14.61 thf(f258,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ ('const/realax/real_abs' @ (sK3 @ X0 @ sK4)) @ sK5)))) ) | ~spl8_15),
% 72.07/14.61 inference(avatar_component_clause,[],[f257])).
% 72.07/14.61 thf(f277,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($true != $true) | ($true = (('const/realax/real_le' @ ('const/realax/real_abs' @ (sK3 @ X0 @ sK4)) @ sK5)))) ) | ~spl8_12),
% 72.07/14.61 inference(constrained_superposition,[],[f71,f248])).
% 72.07/14.61 thf(f282,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ ('const/realax/real_abs' @ (sK3 @ X0 @ sK4)) @ sK5)))) ) | ~spl8_12),
% 72.07/14.61 inference(trivial_inequality_removal,[],[f277])).
% 72.07/14.61 thf(f284,plain,(
% 72.07/14.61 spl8_15 | ~spl8_12),
% 72.07/14.61 inference(avatar_split_clause,[],[f282,f247,f257])).
% 72.07/14.61 thf(f420,plain,(
% 72.07/14.61 ( ! [X0 : $tType,X1 : X0] : (($true != $true) | ($false = (('const/sets/EMPTY' @ X0 @ X1)))) )),
% 72.07/14.61 inference(constrained_superposition,[],[f52,f112])).
% 72.07/14.61 thf(f422,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($true != $true) | ($true = (('const/realax/real_le' @ ('const/realax/real_abs' @ X0) @ sK5))) | ($false = ((sK4 @ X0)))) )),
% 72.07/14.61 inference(constrained_superposition,[],[f71,f112])).
% 72.07/14.61 thf(f427,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ ('const/realax/real_abs' @ X0) @ sK5))) | ($false = ((sK4 @ X0)))) )),
% 72.07/14.61 inference(trivial_inequality_removal,[],[f422])).
% 72.07/14.61 thf(f429,plain,(
% 72.07/14.61 ( ! [X0 : $tType,X1 : X0] : (($false = (('const/sets/EMPTY' @ X0 @ X1)))) )),
% 72.07/14.61 inference(trivial_inequality_removal,[],[f420])).
% 72.07/14.61 thf(f455,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($true = $false) | ($true = ((sK4 @ (sK1 @ X0 @ sK4))))) ) | ~spl8_8),
% 72.07/14.61 inference(constrained_superposition,[],[f216,f113])).
% 72.07/14.61 thf(f464,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($true = ((sK4 @ (sK1 @ X0 @ sK4))))) ) | ~spl8_8),
% 72.07/14.61 inference(trivial_inequality_removal,[],[f455])).
% 72.07/14.61 thf(f537,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($false = (('const/sets/IN' @ 'type/realax/real' @ X0 @ sK4))) | ($true = (('const/sets/IN' @ 'type/realax/real' @ X0 @ 'const/sets/EMPTY' @ 'type/realax/real'))) | (sK6 = X0)) ) | ~spl8_3),
% 72.07/14.61 inference(constrained_superposition,[],[f117,f132])).
% 72.07/14.61 thf(f547,plain,(
% 72.07/14.61 ( ! [X2 : ('type/realax/real' > $o),X3 : 'type/realax/real',X0 : 'type/realax/real',X1 : 'type/realax/real'] : (($true = $false) | ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK0 @ X3 @ ('const/sets/INSERT' @ 'type/realax/real' @ X1 @ X2)) @ ('const/sets/INSERT' @ 'type/realax/real' @ X1 @ X2)))) | ($true = (('const/realax/real_le' @ X3 @ ('const/sets/inf' @ ('const/sets/INSERT' @ 'type/realax/real' @ X1 @ X2))))) | ('const/sets/EMPTY' @ 'type/realax/real' = (('const/sets/INSERT' @ 'type/realax/real' @ X1 @ X2))) | ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK1 @ X0 @ ('const/sets/INSERT' @ 'type/realax/real' @ X1 @ X2)) @ X2))) | (((sK1 @ X0 @ ('const/sets/INSERT' @ 'type/realax/real' @ X1 @ X2))) = X1)) )),
% 72.07/14.61 inference(constrained_superposition,[],[f58,f117])).
% 72.07/14.61 thf(f550,plain,(
% 72.07/14.61 ( ! [X0 : $tType,X2 : X0,X3 : (X0 > $o),X1 : X0] : (($true = $false) | ($false = (('const/sets/INSERT' @ X0 @ X2 @ X3 @ X1))) | ((('const/sets/IN' @ X0 @ X1 @ X3)) = $true) | (X1 = X2)) )),
% 72.07/14.61 inference(constrained_superposition,[],[f112,f117])).
% 72.07/14.61 thf(f551,plain,(
% 72.07/14.61 ( ! [X0 : $tType,X2 : X0,X3 : (X0 > $o),X1 : X0] : (($false = (('const/sets/INSERT' @ X0 @ X2 @ X3 @ X1))) | ((('const/sets/IN' @ X0 @ X1 @ X3)) = $true) | (X1 = X2)) )),
% 72.07/14.61 inference(trivial_inequality_removal,[],[f550])).
% 72.07/14.61 thf(f554,plain,(
% 72.07/14.61 ( ! [X2 : ('type/realax/real' > $o),X3 : 'type/realax/real',X0 : 'type/realax/real',X1 : 'type/realax/real'] : (($true = (('const/sets/IN' @ 'type/realax/real' @ (sK0 @ X3 @ ('const/sets/INSERT' @ 'type/realax/real' @ X1 @ X2)) @ ('const/sets/INSERT' @ 'type/realax/real' @ X1 @ X2)))) | ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK1 @ X0 @ ('const/sets/INSERT' @ 'type/realax/real' @ X1 @ X2)) @ X2))) | ('const/sets/EMPTY' @ 'type/realax/real' = (('const/sets/INSERT' @ 'type/realax/real' @ X1 @ X2))) | ($true = (('const/realax/real_le' @ X3 @ ('const/sets/inf' @ ('const/sets/INSERT' @ 'type/realax/real' @ X1 @ X2))))) | (((sK1 @ X0 @ ('const/sets/INSERT' @ 'type/realax/real' @ X1 @ X2))) = X1)) )),
% 72.07/14.61 inference(trivial_inequality_removal,[],[f547])).
% 72.07/14.61 thf(f562,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($false = (('const/sets/IN' @ 'type/realax/real' @ X0 @ sK4))) | (sK6 = X0)) ) | ~spl8_3),
% 72.07/14.61 inference(forward_subsumption_resolution,[],[f537,f52])).
% 72.07/14.61 thf(f569,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($true = $false) | (sK6 = ((sK0 @ X0 @ sK4))) | ($true = (('const/realax/real_le' @ X0 @ ('const/sets/inf' @ sK4))))) ) | (~spl8_3 | ~spl8_10)),
% 72.07/14.61 inference(constrained_superposition,[],[f562,f223])).
% 72.07/14.61 thf(f581,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($true = $false) | ($false = ((sK4 @ X0))) | (sK6 = X0)) ) | ~spl8_3),
% 72.07/14.61 inference(constrained_superposition,[],[f112,f562])).
% 72.07/14.61 thf(f591,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($false = ((sK4 @ X0))) | (sK6 = X0)) ) | ~spl8_3),
% 72.07/14.61 inference(trivial_inequality_removal,[],[f581])).
% 72.07/14.61 thf(f611,plain,(
% 72.07/14.61 ($false != $false) | (sK6 = sK9) | (~spl8_3 | spl8_4)),
% 72.07/14.61 inference(constrained_superposition,[],[f139,f591])).
% 72.07/14.61 thf(f613,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($true = $false) | (sK6 = ((sK1 @ X0 @ sK4)))) ) | (~spl8_3 | ~spl8_8)),
% 72.07/14.61 inference(constrained_superposition,[],[f464,f591])).
% 72.07/14.61 thf(f616,plain,(
% 72.07/14.61 (sK6 = sK9) | (~spl8_3 | spl8_4)),
% 72.07/14.61 inference(trivial_inequality_removal,[],[f611])).
% 72.07/14.61 thf(f624,plain,(
% 72.07/14.61 ($false != ((sK4 @ sK6))) | (~spl8_3 | spl8_4)),
% 72.07/14.61 inference(constrained_superposition,[],[f139,f616])).
% 72.07/14.61 thf(f638,plain,(
% 72.07/14.61 ( ! [X2 : 'type/realax/real',X0 : 'type/realax/real',X1 : ('type/realax/real' > $o)] : (($true != $true) | ($true = (('const/realax/real_le' @ ('const/sets/inf' @ X1) @ X0))) | ('const/sets/EMPTY' @ 'type/realax/real' = X1) | ($false = (('const/realax/real_le' @ X2 @ (sK1 @ X2 @ X1)))) | ($false = (('const/sets/IN' @ 'type/realax/real' @ X0 @ X1)))) )),
% 72.07/14.61 inference(constrained_superposition,[],[f172,f74])).
% 72.07/14.61 thf(f639,plain,(
% 72.07/14.61 ( ! [X2 : 'type/realax/real',X0 : 'type/realax/real',X1 : ('type/realax/real' > $o)] : (($false = (('const/realax/real_le' @ X2 @ (sK1 @ X2 @ X1)))) | ($true = (('const/realax/real_le' @ ('const/sets/inf' @ X1) @ X0))) | ('const/sets/EMPTY' @ 'type/realax/real' = X1) | ($false = (('const/sets/IN' @ 'type/realax/real' @ X0 @ X1)))) )),
% 72.07/14.61 inference(trivial_inequality_removal,[],[f638])).
% 72.07/14.61 thf(f673,definition,(
% 72.07/14.61 spl8_24 <=> ! [X0 : 'type/realax/real'] : (sK6 = ((sK3 @ X0 @ sK4)))),
% 72.07/14.61 introduced(definition,[new_symbols(definition,[spl8_24])],[avatar_definition])).
% 72.07/14.61 thf(f674,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : ((sK6 = ((sK3 @ X0 @ sK4)))) ) | ~spl8_24),
% 72.07/14.61 inference(avatar_component_clause,[],[f673])).
% 72.07/14.61 thf(f679,definition,(
% 72.07/14.61 spl8_25 <=> ! [X0 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ X0 @ ('const/sets/inf' @ sK4)))) | (sK6 = ((sK0 @ X0 @ sK4))))),
% 72.07/14.61 introduced(definition,[new_symbols(definition,[spl8_25])],[avatar_definition])).
% 72.07/14.61 thf(f680,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ X0 @ ('const/sets/inf' @ sK4)))) | (sK6 = ((sK0 @ X0 @ sK4)))) ) | ~spl8_25),
% 72.07/14.61 inference(avatar_component_clause,[],[f679])).
% 72.07/14.61 thf(f686,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : ((sK6 = ((sK1 @ X0 @ sK4)))) ) | (~spl8_3 | ~spl8_8)),
% 72.07/14.61 inference(trivial_inequality_removal,[],[f613])).
% 72.07/14.61 thf(f780,plain,(
% 72.07/14.61 ( ! [X2 : 'type/realax/real',X0 : 'type/realax/real',X1 : ('type/realax/real' > $o)] : (($true != $true) | ($true = (('const/realax/real_le' @ X0 @ ('const/sets/sup' @ X1)))) | ('const/sets/EMPTY' @ 'type/realax/real' = X1) | ($false = (('const/realax/real_le' @ (sK3 @ X2 @ X1) @ X2))) | ($false = (('const/sets/IN' @ 'type/realax/real' @ X0 @ X1)))) )),
% 72.07/14.61 inference(constrained_superposition,[],[f176,f74])).
% 72.07/14.61 thf(f781,plain,(
% 72.07/14.61 ( ! [X2 : 'type/realax/real',X0 : 'type/realax/real',X1 : ('type/realax/real' > $o)] : (($false = (('const/realax/real_le' @ (sK3 @ X2 @ X1) @ X2))) | ($true = (('const/realax/real_le' @ X0 @ ('const/sets/sup' @ X1)))) | ('const/sets/EMPTY' @ 'type/realax/real' = X1) | ($false = (('const/sets/IN' @ 'type/realax/real' @ X0 @ X1)))) )),
% 72.07/14.61 inference(trivial_inequality_removal,[],[f780])).
% 72.07/14.61 thf(f800,definition,(
% 72.07/14.61 spl8_26 <=> ! [X1 : 'type/realax/real'] : ($false = (('const/realax/real_le' @ (sK3 @ X1 @ sK4) @ X1)))),
% 72.07/14.61 introduced(definition,[new_symbols(definition,[spl8_26])],[avatar_definition])).
% 72.07/14.61 thf(f801,plain,(
% 72.07/14.61 ( ! [X1 : 'type/realax/real'] : (($false = (('const/realax/real_le' @ (sK3 @ X1 @ sK4) @ X1)))) ) | ~spl8_26),
% 72.07/14.61 inference(avatar_component_clause,[],[f800])).
% 72.07/14.61 thf(f820,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real',X1 : 'type/realax/real'] : (($true = $false) | ($true = (('const/realax/real_le' @ ('const/sets/inf' @ sK4) @ X1))) | ('const/sets/EMPTY' @ 'type/realax/real' = sK4) | ($false = (('const/sets/IN' @ 'type/realax/real' @ X1 @ sK4))) | ($true = (('const/realax/real_le' @ ('const/realax/real_abs' @ (sK1 @ X0 @ sK4)) @ sK5)))) )),
% 72.07/14.61 inference(constrained_superposition,[],[f178,f164])).
% 72.07/14.61 thf(f862,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real',X1 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ ('const/sets/inf' @ sK4) @ X1))) | ('const/sets/EMPTY' @ 'type/realax/real' = sK4) | ($false = (('const/sets/IN' @ 'type/realax/real' @ X1 @ sK4))) | ($true = (('const/realax/real_le' @ ('const/realax/real_abs' @ (sK1 @ X0 @ sK4)) @ sK5)))) )),
% 72.07/14.61 inference(trivial_inequality_removal,[],[f820])).
% 72.07/14.61 thf(f865,definition,(
% 72.07/14.61 spl8_28 <=> ! [X0 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ ('const/sets/sup' @ sK4) @ X0))) | ($false = (('const/sets/IN' @ 'type/realax/real' @ X0 @ sK4))))),
% 72.07/14.61 introduced(definition,[new_symbols(definition,[spl8_28])],[avatar_definition])).
% 72.07/14.61 thf(f866,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ ('const/sets/sup' @ sK4) @ X0))) | ($false = (('const/sets/IN' @ 'type/realax/real' @ X0 @ sK4)))) ) | ~spl8_28),
% 72.07/14.61 inference(avatar_component_clause,[],[f865])).
% 72.07/14.61 thf(f877,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : ((sK6 = ((sK0 @ X0 @ sK4))) | ($true = (('const/realax/real_le' @ X0 @ ('const/sets/inf' @ sK4))))) ) | (~spl8_3 | ~spl8_10)),
% 72.07/14.61 inference(trivial_inequality_removal,[],[f569])).
% 72.07/14.61 thf(f898,plain,(
% 72.07/14.61 spl8_25 | ~spl8_3 | ~spl8_10),
% 72.07/14.61 inference(avatar_split_clause,[],[f877,f222,f130,f679])).
% 72.07/14.61 thf(f937,plain,(
% 72.07/14.61 ( ! [X2 : 'type/realax/real',X0 : 'type/realax/real',X1 : ('type/realax/real' > $o)] : (($true = $false) | ($false = (('const/realax/real_le' @ ('const/sets/sup' @ X1) @ X0))) | ((('const/sets/sup' @ X1)) = X0) | ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK3 @ X2 @ X1) @ X1))) | ('const/sets/EMPTY' @ 'type/realax/real' = X1) | ($false = (('const/sets/IN' @ 'type/realax/real' @ X0 @ X1)))) )),
% 72.07/14.61 inference(constrained_superposition,[],[f88,f180])).
% 72.07/14.61 thf(f940,plain,(
% 72.07/14.61 ( ! [X2 : 'type/realax/real',X0 : 'type/realax/real',X1 : ('type/realax/real' > $o)] : (($true = (('const/sets/IN' @ 'type/realax/real' @ (sK3 @ X2 @ X1) @ X1))) | ($false = (('const/realax/real_le' @ ('const/sets/sup' @ X1) @ X0))) | ((('const/sets/sup' @ X1)) = X0) | ('const/sets/EMPTY' @ 'type/realax/real' = X1) | ($false = (('const/sets/IN' @ 'type/realax/real' @ X0 @ X1)))) )),
% 72.07/14.61 inference(trivial_inequality_removal,[],[f937])).
% 72.07/14.61 thf(f1632,definition,(
% 72.07/14.61 spl8_29 <=> ! [X1 : 'type/realax/real'] : (($false = (('const/realax/real_le' @ (sK2 @ X1 @ sK4) @ X1))) | ($true = (('const/realax/real_le' @ ('const/sets/sup' @ sK4) @ X1))))),
% 72.07/14.61 introduced(definition,[new_symbols(definition,[spl8_29])],[avatar_definition])).
% 72.07/14.61 thf(f1633,plain,(
% 72.07/14.61 ( ! [X1 : 'type/realax/real'] : (($false = (('const/realax/real_le' @ (sK2 @ X1 @ sK4) @ X1))) | ($true = (('const/realax/real_le' @ ('const/sets/sup' @ sK4) @ X1)))) ) | ~spl8_29),
% 72.07/14.61 inference(avatar_component_clause,[],[f1632])).
% 72.07/14.61 thf(f1636,definition,(
% 72.07/14.61 spl8_30 <=> ! [X1 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ X1 @ ('const/sets/sup' @ sK4)))) | ($false = (('const/sets/IN' @ 'type/realax/real' @ X1 @ sK4))))),
% 72.07/14.61 introduced(definition,[new_symbols(definition,[spl8_30])],[avatar_definition])).
% 72.07/14.61 thf(f1637,plain,(
% 72.07/14.61 ( ! [X1 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ X1 @ ('const/sets/sup' @ sK4)))) | ($false = (('const/sets/IN' @ 'type/realax/real' @ X1 @ sK4)))) ) | ~spl8_30),
% 72.07/14.61 inference(avatar_component_clause,[],[f1636])).
% 72.07/14.61 thf(f1641,definition,(
% 72.07/14.61 spl8_31 <=> ! [X0 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ ('const/sets/sup' @ sK4) @ X0))) | (sK6 = ((sK2 @ X0 @ sK4))))),
% 72.07/14.61 introduced(definition,[new_symbols(definition,[spl8_31])],[avatar_definition])).
% 72.07/14.61 thf(f1642,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ ('const/sets/sup' @ sK4) @ X0))) | (sK6 = ((sK2 @ X0 @ sK4)))) ) | ~spl8_31),
% 72.07/14.61 inference(avatar_component_clause,[],[f1641])).
% 72.07/14.61 thf(f1646,definition,(
% 72.07/14.61 spl8_32 <=> ! [X0 : 'type/realax/real'] : (sK6 = ((sK1 @ X0 @ sK4)))),
% 72.07/14.61 introduced(definition,[new_symbols(definition,[spl8_32])],[avatar_definition])).
% 72.07/14.61 thf(f1647,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : ((sK6 = ((sK1 @ X0 @ sK4)))) ) | ~spl8_32),
% 72.07/14.61 inference(avatar_component_clause,[],[f1646])).
% 72.07/14.61 thf(f1827,plain,(
% 72.07/14.61 spl8_32 | ~spl8_3 | ~spl8_8),
% 72.07/14.61 inference(avatar_split_clause,[],[f686,f215,f130,f1646])).
% 72.07/14.61 thf(f1972,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real',X1 : 'type/realax/real'] : (($true = $false) | (sK6 = ((sK3 @ X0 @ sK4))) | ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK2 @ X1 @ sK4) @ sK4))) | ($true = (('const/realax/real_le' @ ('const/sets/sup' @ sK4) @ X1))) | ('const/sets/EMPTY' @ 'type/realax/real' = sK4)) ) | ~spl8_3),
% 72.07/14.61 inference(constrained_superposition,[],[f562,f65])).
% 72.07/14.61 thf(f2054,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real',X1 : 'type/realax/real'] : ((sK6 = ((sK3 @ X0 @ sK4))) | ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK2 @ X1 @ sK4) @ sK4))) | ($true = (('const/realax/real_le' @ ('const/sets/sup' @ sK4) @ X1))) | ('const/sets/EMPTY' @ 'type/realax/real' = sK4)) ) | ~spl8_3),
% 72.07/14.61 inference(trivial_inequality_removal,[],[f1972])).
% 72.07/14.61 thf(f2079,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real',X1 : 'type/realax/real'] : ((sK6 = ((sK3 @ X0 @ sK4))) | ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK2 @ X1 @ sK4) @ sK4))) | ($true = (('const/realax/real_le' @ ('const/sets/sup' @ sK4) @ X1)))) ) | ~spl8_3),
% 72.07/14.61 inference(forward_subsumption_resolution,[],[f2054,f70])).
% 72.07/14.61 thf(f2095,plain,(
% 72.07/14.61 spl8_14 | spl8_24 | ~spl8_3),
% 72.07/14.61 inference(avatar_split_clause,[],[f2079,f130,f673,f254])).
% 72.07/14.61 thf(f2333,definition,(
% 72.07/14.61 spl8_42 <=> ($true = (('const/sets/IN' @ 'type/realax/real' @ sK6 @ sK4)))),
% 72.07/14.61 introduced(definition,[new_symbols(definition,[spl8_42])],[avatar_definition])).
% 72.07/14.61 thf(f2335,plain,(
% 72.07/14.61 ($true = (('const/sets/IN' @ 'type/realax/real' @ sK6 @ sK4))) | ~spl8_42),
% 72.07/14.61 inference(avatar_component_clause,[],[f2333])).
% 72.07/14.61 thf(f2495,definition,(
% 72.07/14.61 spl8_48 <=> ! [X0 : 'type/realax/real'] : ($true != (('const/realax/real_le' @ X0 @ sK6)))),
% 72.07/14.61 introduced(definition,[new_symbols(definition,[spl8_48])],[avatar_definition])).
% 72.07/14.61 thf(f2496,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($true != (('const/realax/real_le' @ X0 @ sK6)))) ) | ~spl8_48),
% 72.07/14.61 inference(avatar_component_clause,[],[f2495])).
% 72.07/14.61 thf(f3134,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($true = $false) | ($false = (('const/realax/real_le' @ X0 @ ('const/sets/sup' @ sK4)))) | ((('const/sets/sup' @ sK4)) = X0) | ($false = (('const/sets/IN' @ 'type/realax/real' @ X0 @ sK4)))) ) | ~spl8_28),
% 72.07/14.61 inference(constrained_superposition,[],[f88,f866])).
% 72.07/14.61 thf(f3151,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($false = (('const/realax/real_le' @ X0 @ ('const/sets/sup' @ sK4)))) | ((('const/sets/sup' @ sK4)) = X0) | ($false = (('const/sets/IN' @ 'type/realax/real' @ X0 @ sK4)))) ) | ~spl8_28),
% 72.07/14.61 inference(trivial_inequality_removal,[],[f3134])).
% 72.07/14.61 thf(f3265,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($true = $false) | ($true = (('const/realax/real_le' @ (sK3 @ X0 @ sK4) @ sK5)))) ) | ~spl8_15),
% 72.07/14.61 inference(constrained_superposition,[],[f258,f95])).
% 72.07/14.61 thf(f3268,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ (sK3 @ X0 @ sK4) @ sK5)))) ) | ~spl8_15),
% 72.07/14.61 inference(trivial_inequality_removal,[],[f3265])).
% 72.07/14.61 thf(f3302,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($true = $false) | ($true = (('const/realax/real_le' @ ('const/realax/real_neg' @ sK5) @ (sK1 @ X0 @ sK4))))) ) | ~spl8_11),
% 72.07/14.61 inference(constrained_superposition,[],[f226,f96])).
% 72.07/14.61 thf(f3315,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ ('const/realax/real_neg' @ sK5) @ (sK1 @ X0 @ sK4))))) ) | ~spl8_11),
% 72.07/14.61 inference(trivial_inequality_removal,[],[f3302])).
% 72.07/14.61 thf(f3334,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : ((sK6 != X0) | ($true = (('const/sets/IN' @ 'type/realax/real' @ X0 @ sK4)))) ) | ~spl8_3),
% 72.07/14.61 inference(constrained_superposition,[],[f120,f132])).
% 72.07/14.61 thf(f3341,plain,(
% 72.07/14.61 ( ! [X0 : $tType,X2 : X0,X3 : (X0 > $o),X1 : X0] : (($true = $false) | ($true = (('const/sets/INSERT' @ X0 @ X2 @ X3 @ X1))) | (X1 != X2)) )),
% 72.07/14.61 inference(constrained_superposition,[],[f113,f120])).
% 72.07/14.61 thf(f3343,plain,(
% 72.07/14.61 ( ! [X0 : $tType,X2 : X0,X3 : (X0 > $o),X1 : X0] : (($true = (('const/sets/INSERT' @ X0 @ X2 @ X3 @ X1))) | (X1 != X2)) )),
% 72.07/14.61 inference(trivial_inequality_removal,[],[f3341])).
% 72.07/14.61 thf(f3394,plain,(
% 72.07/14.61 ( ! [X0 : $tType,X2 : (X0 > $o),X1 : X0] : (($true != $true) | ($false = (('const/sets/IN' @ X0 @ X1 @ X2))) | ('const/sets/EMPTY' @ X0 != X2)) )),
% 72.07/14.61 inference(constrained_superposition,[],[f52,f104])).
% 72.07/14.61 thf(f3465,plain,(
% 72.07/14.61 ( ! [X0 : $tType,X2 : (X0 > $o),X1 : X0] : (('const/sets/EMPTY' @ X0 != X2) | ($false = (('const/sets/IN' @ X0 @ X1 @ X2)))) )),
% 72.07/14.61 inference(trivial_inequality_removal,[],[f3394])).
% 72.07/14.61 thf(f3624,definition,(
% 72.07/14.61 spl8_56 <=> ! [X0 : 'type/realax/real'] : ($false = (('const/realax/real_le' @ X0 @ sK6)))),
% 72.07/14.61 introduced(definition,[new_symbols(definition,[spl8_56])],[avatar_definition])).
% 72.07/14.61 thf(f3625,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($false = (('const/realax/real_le' @ X0 @ sK6)))) ) | ~spl8_56),
% 72.07/14.61 inference(avatar_component_clause,[],[f3624])).
% 72.07/14.61 thf(f8674,definition,(
% 72.07/14.61 spl8_89 <=> ! [X1 : 'type/realax/real'] : (($false = (('const/realax/real_le' @ ('const/sets/sup' @ sK4) @ X1))) | ($false = (('const/sets/IN' @ 'type/realax/real' @ X1 @ sK4))) | ((('const/sets/sup' @ sK4)) = X1))),
% 72.07/14.61 introduced(definition,[new_symbols(definition,[spl8_89])],[avatar_definition])).
% 72.07/14.61 thf(f8675,plain,(
% 72.07/14.61 ( ! [X1 : 'type/realax/real'] : (($false = (('const/realax/real_le' @ ('const/sets/sup' @ sK4) @ X1))) | ($false = (('const/sets/IN' @ 'type/realax/real' @ X1 @ sK4))) | ((('const/sets/sup' @ sK4)) = X1)) ) | ~spl8_89),
% 72.07/14.61 inference(avatar_component_clause,[],[f8674])).
% 72.07/14.61 thf(f8820,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real',X1 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ ('const/sets/inf' @ sK4) @ X1))) | ($false = (('const/sets/IN' @ 'type/realax/real' @ X1 @ sK4))) | ($true = (('const/realax/real_le' @ ('const/realax/real_abs' @ (sK1 @ X0 @ sK4)) @ sK5)))) )),
% 72.07/14.61 inference(forward_subsumption_resolution,[],[f862,f70])).
% 72.07/14.61 thf(f9848,definition,(
% 72.07/14.61 spl8_106 <=> ($true = (('const/realax/real_le' @ ('const/realax/real_abs' @ sK6) @ sK5)))),
% 72.07/14.61 introduced(definition,[new_symbols(definition,[spl8_106])],[avatar_definition])).
% 72.07/14.61 thf(f9849,plain,(
% 72.07/14.61 ($true != (('const/realax/real_le' @ ('const/realax/real_abs' @ sK6) @ sK5))) | spl8_106),
% 72.07/14.61 inference(avatar_component_clause,[],[f9848])).
% 72.07/14.61 thf(f9850,plain,(
% 72.07/14.61 ($true = (('const/realax/real_le' @ ('const/realax/real_abs' @ sK6) @ sK5))) | ~spl8_106),
% 72.07/14.61 inference(avatar_component_clause,[],[f9848])).
% 72.07/14.61 thf(f9876,plain,(
% 72.07/14.61 ($true = $false) | ($true = (('const/realax/real_le' @ sK6 @ sK5))) | ~spl8_106),
% 72.07/14.61 inference(constrained_superposition,[],[f95,f9850])).
% 72.07/14.61 thf(f9877,plain,(
% 72.07/14.61 ($true = (('const/realax/real_le' @ sK6 @ sK5))) | ~spl8_106),
% 72.07/14.61 inference(trivial_inequality_removal,[],[f9876])).
% 72.07/14.61 thf(f10305,plain,(
% 72.07/14.61 ($true != $true) | ($false = ((sK4 @ sK6))) | spl8_106),
% 72.07/14.61 inference(constrained_superposition,[],[f9849,f427])).
% 72.07/14.61 thf(f10308,plain,(
% 72.07/14.61 ($false = ((sK4 @ sK6))) | spl8_106),
% 72.07/14.61 inference(trivial_inequality_removal,[],[f10305])).
% 72.07/14.61 thf(f10330,plain,(
% 72.07/14.61 $false | (~spl8_3 | spl8_4 | spl8_106)),
% 72.07/14.61 inference(forward_subsumption_resolution,[],[f10308,f624])).
% 72.07/14.61 thf(f10331,plain,(
% 72.07/14.61 ~spl8_3 | spl8_4 | spl8_106),
% 72.07/14.61 inference(avatar_contradiction_clause,[],[f10330])).
% 72.07/14.61 thf(f10337,plain,(
% 72.07/14.61 ($true = $false) | ~spl8_7),
% 72.07/14.61 inference(forward_demodulation,[],[f153,f429])).
% 72.07/14.61 thf(f10338,plain,(
% 72.07/14.61 $false | ~spl8_7),
% 72.07/14.61 inference(trivial_inequality_removal,[],[f10337])).
% 72.07/14.61 thf(f10339,plain,(
% 72.07/14.61 ~spl8_7),
% 72.07/14.61 inference(avatar_contradiction_clause,[],[f10338])).
% 72.07/14.61 thf(f22820,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($true != $true) | (sK6 != X0)) ) | ~spl8_48),
% 72.07/14.61 inference(constrained_superposition,[],[f2496,f91])).
% 72.07/14.61 thf(f22887,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : ((sK6 != X0)) ) | ~spl8_48),
% 72.07/14.61 inference(trivial_inequality_removal,[],[f22820])).
% 72.07/14.61 thf(f22894,plain,(
% 72.07/14.61 $false | ~spl8_48),
% 72.07/14.61 inference(equality_resolution,[],[f22887])).
% 72.07/14.61 thf(f22895,plain,(
% 72.07/14.61 ~spl8_48),
% 72.07/14.61 inference(avatar_contradiction_clause,[],[f22894])).
% 72.07/14.61 thf(f23825,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($true = $false) | (sK6 != X0)) ) | ~spl8_56),
% 72.07/14.61 inference(constrained_superposition,[],[f91,f3625])).
% 72.07/14.61 thf(f23830,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : ((sK6 != X0)) ) | ~spl8_56),
% 72.07/14.61 inference(trivial_inequality_removal,[],[f23825])).
% 72.07/14.61 thf(f23912,plain,(
% 72.07/14.61 $false | ~spl8_56),
% 72.07/14.61 inference(equality_resolution,[],[f23830])).
% 72.07/14.61 thf(f23913,plain,(
% 72.07/14.61 ~spl8_56),
% 72.07/14.61 inference(avatar_contradiction_clause,[],[f23912])).
% 72.07/14.61 thf(f24253,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real',X1 : 'type/realax/real'] : (($true = $false) | (sK6 = ((sK3 @ X0 @ sK4))) | ($false = (('const/realax/real_le' @ (sK2 @ X1 @ sK4) @ X1))) | ('const/sets/EMPTY' @ 'type/realax/real' = sK4) | ($true = (('const/realax/real_le' @ ('const/sets/sup' @ sK4) @ X1)))) ) | ~spl8_3),
% 72.07/14.61 inference(constrained_superposition,[],[f562,f195])).
% 72.07/14.61 thf(f24264,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real',X1 : 'type/realax/real'] : (($true = $false) | (sK6 = ((sK3 @ X0 @ sK4))) | ($false = (('const/realax/real_le' @ ('const/sets/sup' @ sK4) @ X1))) | ((('const/sets/sup' @ sK4)) = X1) | ('const/sets/EMPTY' @ 'type/realax/real' = sK4) | ($false = (('const/sets/IN' @ 'type/realax/real' @ X1 @ sK4)))) ) | ~spl8_3),
% 72.07/14.61 inference(constrained_superposition,[],[f562,f940])).
% 72.07/14.61 thf(f24548,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real',X1 : 'type/realax/real'] : ((sK6 = ((sK3 @ X0 @ sK4))) | ($false = (('const/realax/real_le' @ ('const/sets/sup' @ sK4) @ X1))) | ((('const/sets/sup' @ sK4)) = X1) | ('const/sets/EMPTY' @ 'type/realax/real' = sK4) | ($false = (('const/sets/IN' @ 'type/realax/real' @ X1 @ sK4)))) ) | ~spl8_3),
% 72.07/14.61 inference(trivial_inequality_removal,[],[f24264])).
% 72.07/14.61 thf(f24559,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real',X1 : 'type/realax/real'] : ((sK6 = ((sK3 @ X0 @ sK4))) | ($false = (('const/realax/real_le' @ (sK2 @ X1 @ sK4) @ X1))) | ('const/sets/EMPTY' @ 'type/realax/real' = sK4) | ($true = (('const/realax/real_le' @ ('const/sets/sup' @ sK4) @ X1)))) ) | ~spl8_3),
% 72.07/14.61 inference(trivial_inequality_removal,[],[f24253])).
% 72.07/14.61 thf(f24676,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real',X1 : 'type/realax/real'] : ((sK6 = ((sK3 @ X0 @ sK4))) | ($false = (('const/realax/real_le' @ ('const/sets/sup' @ sK4) @ X1))) | ((('const/sets/sup' @ sK4)) = X1) | ($false = (('const/sets/IN' @ 'type/realax/real' @ X1 @ sK4)))) ) | ~spl8_3),
% 72.07/14.61 inference(forward_subsumption_resolution,[],[f24548,f70])).
% 72.07/14.61 thf(f24679,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real',X1 : 'type/realax/real'] : ((sK6 = ((sK3 @ X0 @ sK4))) | ($false = (('const/realax/real_le' @ (sK2 @ X1 @ sK4) @ X1))) | ($true = (('const/realax/real_le' @ ('const/sets/sup' @ sK4) @ X1)))) ) | ~spl8_3),
% 72.07/14.61 inference(forward_subsumption_resolution,[],[f24559,f70])).
% 72.07/14.61 thf(f24734,plain,(
% 72.07/14.61 spl8_89 | spl8_24 | ~spl8_3),
% 72.07/14.61 inference(avatar_split_clause,[],[f24676,f130,f673,f8674])).
% 72.07/14.61 thf(f24737,plain,(
% 72.07/14.61 spl8_29 | spl8_24 | ~spl8_3),
% 72.07/14.61 inference(avatar_split_clause,[],[f24679,f130,f673,f1632])).
% 72.07/14.61 thf(f24786,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real',X1 : 'type/realax/real'] : (($false = (('const/realax/real_le' @ sK6 @ X0))) | ($true = (('const/realax/real_le' @ X1 @ ('const/sets/sup' @ sK4)))) | ('const/sets/EMPTY' @ 'type/realax/real' = sK4) | ($false = (('const/sets/IN' @ 'type/realax/real' @ X1 @ sK4)))) ) | ~spl8_24),
% 72.07/14.61 inference(constrained_superposition,[],[f781,f674])).
% 72.07/14.61 thf(f24858,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real',X1 : 'type/realax/real'] : (($false = (('const/realax/real_le' @ sK6 @ X0))) | ($true = (('const/realax/real_le' @ X1 @ ('const/sets/sup' @ sK4)))) | ($false = (('const/sets/IN' @ 'type/realax/real' @ X1 @ sK4)))) ) | ~spl8_24),
% 72.07/14.61 inference(forward_subsumption_resolution,[],[f24786,f70])).
% 72.07/14.61 thf(f24867,definition,(
% 72.07/14.61 spl8_142 <=> ($true = (('const/realax/real_le' @ ('const/sets/inf' @ sK4) @ sK6)))),
% 72.07/14.61 introduced(definition,[new_symbols(definition,[spl8_142])],[avatar_definition])).
% 72.07/14.61 thf(f24869,plain,(
% 72.07/14.61 ($true = (('const/realax/real_le' @ ('const/sets/inf' @ sK4) @ sK6))) | ~spl8_142),
% 72.07/14.61 inference(avatar_component_clause,[],[f24867])).
% 72.07/14.61 thf(f24874,definition,(
% 72.07/14.61 spl8_143 <=> ! [X0 : 'type/realax/real'] : ($false = (('const/realax/real_le' @ sK6 @ X0)))),
% 72.07/14.61 introduced(definition,[new_symbols(definition,[spl8_143])],[avatar_definition])).
% 72.07/14.61 thf(f24875,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($false = (('const/realax/real_le' @ sK6 @ X0)))) ) | ~spl8_143),
% 72.07/14.61 inference(avatar_component_clause,[],[f24874])).
% 72.07/14.61 thf(f24886,plain,(
% 72.07/14.61 spl8_30 | spl8_143 | ~spl8_24),
% 72.07/14.61 inference(avatar_split_clause,[],[f24858,f673,f24874,f1636])).
% 72.07/14.61 thf(f24911,plain,(
% 72.07/14.61 ($true = $false) | (~spl8_106 | ~spl8_143)),
% 72.07/14.61 inference(constrained_superposition,[],[f24875,f9877])).
% 72.07/14.61 thf(f24979,plain,(
% 72.07/14.61 $false | (~spl8_106 | ~spl8_143)),
% 72.07/14.61 inference(trivial_inequality_removal,[],[f24911])).
% 72.07/14.61 thf(f24980,plain,(
% 72.07/14.61 ~spl8_106 | ~spl8_143),
% 72.07/14.61 inference(avatar_contradiction_clause,[],[f24979])).
% 72.07/14.61 thf(f25020,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real',X1 : 'type/realax/real'] : (($true != (('const/realax/real_le' @ X0 @ sK6))) | ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK0 @ X1 @ sK4) @ sK4))) | ($true = (('const/realax/real_le' @ X1 @ ('const/sets/inf' @ sK4)))) | ('const/sets/EMPTY' @ 'type/realax/real' = sK4)) ) | ~spl8_32),
% 72.07/14.61 inference(constrained_superposition,[],[f59,f1647])).
% 72.07/14.61 thf(f26833,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($true != $true) | ($true = (('const/realax/real_le' @ ('const/sets/inf' @ sK4) @ sK6))) | ('const/sets/EMPTY' @ 'type/realax/real' = sK4) | ($false = (('const/realax/real_le' @ X0 @ (sK1 @ X0 @ sK4))))) ) | ~spl8_42),
% 72.07/14.61 inference(constrained_superposition,[],[f172,f2335])).
% 72.07/14.61 thf(f26835,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($true != $true) | ($true = (('const/realax/real_le' @ ('const/sets/inf' @ sK4) @ sK6))) | ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK1 @ X0 @ sK4) @ sK4))) | ('const/sets/EMPTY' @ 'type/realax/real' = sK4)) ) | ~spl8_42),
% 72.07/14.61 inference(constrained_superposition,[],[f56,f2335])).
% 72.07/14.61 thf(f26846,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ ('const/sets/inf' @ sK4) @ sK6))) | ('const/sets/EMPTY' @ 'type/realax/real' = sK4) | ($false = (('const/realax/real_le' @ X0 @ (sK1 @ X0 @ sK4))))) ) | ~spl8_42),
% 72.07/14.61 inference(trivial_inequality_removal,[],[f26833])).
% 72.07/14.61 thf(f26854,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ ('const/sets/inf' @ sK4) @ sK6))) | ($false = (('const/realax/real_le' @ X0 @ (sK1 @ X0 @ sK4))))) ) | ~spl8_42),
% 72.07/14.61 inference(forward_subsumption_resolution,[],[f26846,f70])).
% 72.07/14.61 thf(f26859,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($false = (('const/realax/real_le' @ X0 @ sK6))) | ($true = (('const/realax/real_le' @ ('const/sets/inf' @ sK4) @ sK6)))) ) | (~spl8_32 | ~spl8_42)),
% 72.07/14.61 inference(forward_demodulation,[],[f26854,f1647])).
% 72.07/14.61 thf(f26863,plain,(
% 72.07/14.61 spl8_142 | spl8_56 | ~spl8_32 | ~spl8_42),
% 72.07/14.61 inference(avatar_split_clause,[],[f26859,f2333,f1646,f3624,f24867])).
% 72.07/14.61 thf(f27164,definition,(
% 72.07/14.61 spl8_150 <=> ((('const/sets/sup' @ sK4)) = sK6)),
% 72.07/14.61 introduced(definition,[new_symbols(definition,[spl8_150])],[avatar_definition])).
% 72.07/14.61 thf(f27486,definition,(
% 72.07/14.61 spl8_156 <=> ($true = (('const/realax/real_le' @ sK6 @ sK6)))),
% 72.07/14.61 introduced(definition,[new_symbols(definition,[spl8_156])],[avatar_definition])).
% 72.07/14.61 thf(f27487,plain,(
% 72.07/14.61 ($true != (('const/realax/real_le' @ sK6 @ sK6))) | spl8_156),
% 72.07/14.61 inference(avatar_component_clause,[],[f27486])).
% 72.07/14.61 thf(f27488,plain,(
% 72.07/14.61 ($true = (('const/realax/real_le' @ sK6 @ sK6))) | ~spl8_156),
% 72.07/14.61 inference(avatar_component_clause,[],[f27486])).
% 72.07/14.61 thf(f28170,plain,(
% 72.07/14.61 ($true = $false) | ($false = (('const/realax/real_le' @ sK6 @ ('const/sets/inf' @ sK4)))) | ((('const/sets/inf' @ sK4)) = sK6) | ~spl8_142),
% 72.07/14.61 inference(constrained_superposition,[],[f24869,f88])).
% 72.07/14.61 thf(f28177,plain,(
% 72.07/14.61 ($false = (('const/realax/real_le' @ sK6 @ ('const/sets/inf' @ sK4)))) | ((('const/sets/inf' @ sK4)) = sK6) | ~spl8_142),
% 72.07/14.61 inference(trivial_inequality_removal,[],[f28170])).
% 72.07/14.61 thf(f28179,definition,(
% 72.07/14.61 spl8_158 <=> ((('const/sets/inf' @ sK4)) = sK6)),
% 72.07/14.61 introduced(definition,[new_symbols(definition,[spl8_158])],[avatar_definition])).
% 72.07/14.61 thf(f28181,plain,(
% 72.07/14.61 ((('const/sets/inf' @ sK4)) = sK6) | ~spl8_158),
% 72.07/14.61 inference(avatar_component_clause,[],[f28179])).
% 72.07/14.61 thf(f28183,definition,(
% 72.07/14.61 spl8_159 <=> ($false = (('const/realax/real_le' @ sK6 @ ('const/sets/inf' @ sK4))))),
% 72.07/14.61 introduced(definition,[new_symbols(definition,[spl8_159])],[avatar_definition])).
% 72.07/14.61 thf(f28185,plain,(
% 72.07/14.61 ($false = (('const/realax/real_le' @ sK6 @ ('const/sets/inf' @ sK4)))) | ~spl8_159),
% 72.07/14.61 inference(avatar_component_clause,[],[f28183])).
% 72.07/14.61 thf(f28456,plain,(
% 72.07/14.61 ((('const/sets/sup' @ sK4)) != sK6) | (spl8_2 | ~spl8_158)),
% 72.07/14.61 inference(constrained_superposition,[],[f127,f28181])).
% 72.07/14.61 thf(f29808,plain,(
% 72.07/14.61 ($true = (('const/sets/IN' @ 'type/realax/real' @ sK6 @ sK4))) | ~spl8_3),
% 72.07/14.61 inference(equality_resolution,[],[f3334])).
% 72.07/14.61 thf(f32708,plain,(
% 72.07/14.61 ($true = $false) | (sK6 = ((sK0 @ sK6 @ sK4))) | (~spl8_25 | ~spl8_159)),
% 72.07/14.61 inference(constrained_superposition,[],[f28185,f680])).
% 72.07/14.61 thf(f32709,plain,(
% 72.07/14.61 (sK6 = ((sK0 @ sK6 @ sK4))) | (~spl8_25 | ~spl8_159)),
% 72.07/14.61 inference(trivial_inequality_removal,[],[f32708])).
% 72.07/14.61 thf(f32809,definition,(
% 72.07/14.61 spl8_176 <=> (sK6 = ((sK0 @ sK6 @ sK4)))),
% 72.07/14.61 introduced(definition,[new_symbols(definition,[spl8_176])],[avatar_definition])).
% 72.07/14.61 thf(f32811,plain,(
% 72.07/14.61 (sK6 = ((sK0 @ sK6 @ sK4))) | ~spl8_176),
% 72.07/14.61 inference(avatar_component_clause,[],[f32809])).
% 72.07/14.61 thf(f32815,plain,(
% 72.07/14.61 spl8_176 | ~spl8_25 | ~spl8_159),
% 72.07/14.61 inference(avatar_split_clause,[],[f32709,f28183,f679,f32809])).
% 72.07/14.61 thf(f33064,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($true != (('const/realax/real_le' @ sK6 @ sK6))) | ($true = (('const/realax/real_le' @ sK6 @ ('const/sets/inf' @ sK4)))) | ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK1 @ X0 @ sK4) @ sK4))) | ('const/sets/EMPTY' @ 'type/realax/real' = sK4)) ) | ~spl8_176),
% 72.07/14.61 inference(constrained_superposition,[],[f60,f32811])).
% 72.07/14.61 thf(f33065,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($true != (('const/realax/real_le' @ sK6 @ sK6))) | ($true = (('const/realax/real_le' @ sK6 @ ('const/sets/inf' @ sK4)))) | ('const/sets/EMPTY' @ 'type/realax/real' = sK4) | ($false = (('const/realax/real_le' @ X0 @ (sK1 @ X0 @ sK4))))) ) | ~spl8_176),
% 72.07/14.61 inference(constrained_superposition,[],[f182,f32811])).
% 72.07/14.61 thf(f33096,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ sK6 @ ('const/sets/inf' @ sK4)))) | ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK1 @ X0 @ sK4) @ sK4))) | ('const/sets/EMPTY' @ 'type/realax/real' = sK4)) ) | (~spl8_156 | ~spl8_176)),
% 72.07/14.61 inference(forward_subsumption_resolution,[],[f33064,f27488])).
% 72.07/14.61 thf(f33103,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ sK6 @ ('const/sets/inf' @ sK4)))) | ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK1 @ X0 @ sK4) @ sK4)))) ) | (~spl8_156 | ~spl8_176)),
% 72.07/14.61 inference(forward_subsumption_resolution,[],[f33096,f70])).
% 72.07/14.61 thf(f33110,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($true = $false) | ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK1 @ X0 @ sK4) @ sK4)))) ) | (~spl8_156 | ~spl8_159 | ~spl8_176)),
% 72.07/14.61 inference(forward_demodulation,[],[f33103,f28185])).
% 72.07/14.61 thf(f33120,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($true != (('const/realax/real_le' @ sK6 @ sK6))) | ($true = (('const/realax/real_le' @ sK6 @ ('const/sets/inf' @ sK4)))) | ($false = (('const/realax/real_le' @ X0 @ (sK1 @ X0 @ sK4))))) ) | ~spl8_176),
% 72.07/14.61 inference(forward_subsumption_resolution,[],[f33065,f70])).
% 72.07/14.61 thf(f33148,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($true = $false) | ($true != (('const/realax/real_le' @ sK6 @ sK6))) | ($false = (('const/realax/real_le' @ X0 @ (sK1 @ X0 @ sK4))))) ) | (~spl8_159 | ~spl8_176)),
% 72.07/14.61 inference(forward_demodulation,[],[f33120,f28185])).
% 72.07/14.61 thf(f33149,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($true != (('const/realax/real_le' @ sK6 @ sK6))) | ($false = (('const/realax/real_le' @ X0 @ (sK1 @ X0 @ sK4))))) ) | (~spl8_159 | ~spl8_176)),
% 72.07/14.61 inference(trivial_inequality_removal,[],[f33148])).
% 72.07/14.61 thf(f33155,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($false = (('const/realax/real_le' @ X0 @ sK6))) | ($true != (('const/realax/real_le' @ sK6 @ sK6)))) ) | (~spl8_32 | ~spl8_159 | ~spl8_176)),
% 72.07/14.61 inference(forward_demodulation,[],[f33149,f1647])).
% 72.07/14.61 thf(f33158,definition,(
% 72.07/14.61 spl8_181 <=> ($false = (('const/realax/real_le' @ sK6 @ sK6)))),
% 72.07/14.61 introduced(definition,[new_symbols(definition,[spl8_181])],[avatar_definition])).
% 72.07/14.61 thf(f33159,plain,(
% 72.07/14.61 ($false != (('const/realax/real_le' @ sK6 @ sK6))) | spl8_181),
% 72.07/14.61 inference(avatar_component_clause,[],[f33158])).
% 72.07/14.61 thf(f33160,plain,(
% 72.07/14.61 ($false = (('const/realax/real_le' @ sK6 @ sK6))) | ~spl8_181),
% 72.07/14.61 inference(avatar_component_clause,[],[f33158])).
% 72.07/14.61 thf(f33163,plain,(
% 72.07/14.61 ~spl8_156 | spl8_56 | ~spl8_32 | ~spl8_159 | ~spl8_176),
% 72.07/14.61 inference(avatar_split_clause,[],[f33155,f32809,f28183,f1646,f3624,f27486])).
% 72.07/14.61 thf(f33646,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($true = $false) | ($false = (('const/realax/real_le' @ ('const/sets/sup' @ sK4) @ X0))) | ((('const/sets/sup' @ sK4)) = X0) | ($false = (('const/sets/IN' @ 'type/realax/real' @ X0 @ sK4)))) ) | ~spl8_30),
% 72.07/14.61 inference(constrained_superposition,[],[f88,f1637])).
% 72.07/14.61 thf(f33655,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($false = (('const/realax/real_le' @ ('const/sets/sup' @ sK4) @ X0))) | ((('const/sets/sup' @ sK4)) = X0) | ($false = (('const/sets/IN' @ 'type/realax/real' @ X0 @ sK4)))) ) | ~spl8_30),
% 72.07/14.61 inference(trivial_inequality_removal,[],[f33646])).
% 72.07/14.61 thf(f33728,plain,(
% 72.07/14.61 spl8_89 | ~spl8_30),
% 72.07/14.61 inference(avatar_split_clause,[],[f33655,f1636,f8674])).
% 72.07/14.61 thf(f33745,definition,(
% 72.07/14.61 spl8_184 <=> ($false = (('const/sets/IN' @ 'type/realax/real' @ sK6 @ sK4)))),
% 72.07/14.61 introduced(definition,[new_symbols(definition,[spl8_184])],[avatar_definition])).
% 72.07/14.61 thf(f33746,plain,(
% 72.07/14.61 ($false != (('const/sets/IN' @ 'type/realax/real' @ sK6 @ sK4))) | spl8_184),
% 72.07/14.61 inference(avatar_component_clause,[],[f33745])).
% 72.07/14.61 thf(f33747,plain,(
% 72.07/14.61 ($false = (('const/sets/IN' @ 'type/realax/real' @ sK6 @ sK4))) | ~spl8_184),
% 72.07/14.61 inference(avatar_component_clause,[],[f33745])).
% 72.07/14.61 thf(f33775,plain,(
% 72.07/14.61 ($true != $true) | ($false = (('const/realax/real_le' @ sK6 @ sK6))) | spl8_156),
% 72.07/14.61 inference(constrained_superposition,[],[f27487,f74])).
% 72.07/14.61 thf(f33776,plain,(
% 72.07/14.61 ($false = (('const/realax/real_le' @ sK6 @ sK6))) | spl8_156),
% 72.07/14.61 inference(trivial_inequality_removal,[],[f33775])).
% 72.07/14.61 thf(f33817,plain,(
% 72.07/14.61 spl8_181 | spl8_156),
% 72.07/14.61 inference(avatar_split_clause,[],[f33776,f27486,f33158])).
% 72.07/14.61 thf(f34628,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real',X1 : 'type/realax/real'] : (($true = $false) | ($false = (('const/realax/real_le' @ (sK3 @ X1 @ sK4) @ X1))) | ('const/sets/EMPTY' @ 'type/realax/real' = sK4) | ($false = (('const/sets/IN' @ 'type/realax/real' @ X0 @ sK4))) | ((('const/sets/sup' @ sK4)) = X0) | ($false = (('const/sets/IN' @ 'type/realax/real' @ X0 @ sK4)))) ) | ~spl8_28),
% 72.07/14.61 inference(constrained_superposition,[],[f781,f3151])).
% 72.07/14.61 thf(f34915,definition,(
% 72.07/14.61 spl8_201 <=> ! [X0 : 'type/realax/real'] : (($false = (('const/sets/IN' @ 'type/realax/real' @ X0 @ sK4))) | ((('const/sets/sup' @ sK4)) = X0))),
% 72.07/14.61 introduced(definition,[new_symbols(definition,[spl8_201])],[avatar_definition])).
% 72.07/14.61 thf(f34916,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($false = (('const/sets/IN' @ 'type/realax/real' @ X0 @ sK4))) | ((('const/sets/sup' @ sK4)) = X0)) ) | ~spl8_201),
% 72.07/14.61 inference(avatar_component_clause,[],[f34915])).
% 72.07/14.61 thf(f35292,plain,(
% 72.07/14.61 ($true = $false) | (sK6 != sK6) | ~spl8_181),
% 72.07/14.61 inference(constrained_superposition,[],[f33160,f91])).
% 72.07/14.61 thf(f35420,plain,(
% 72.07/14.61 $false | ~spl8_181),
% 72.07/14.61 inference(trivial_inequality_removal,[],[f35292])).
% 72.07/14.61 thf(f35421,plain,(
% 72.07/14.61 ~spl8_181),
% 72.07/14.61 inference(avatar_contradiction_clause,[],[f35420])).
% 72.07/14.61 thf(f36930,definition,(
% 72.07/14.61 spl8_216 <=> ($false = (('const/realax/real_le' @ ('const/sets/sup' @ sK4) @ sK6)))),
% 72.07/14.61 introduced(definition,[new_symbols(definition,[spl8_216])],[avatar_definition])).
% 72.07/14.61 thf(f36931,plain,(
% 72.07/14.61 ($false != (('const/realax/real_le' @ ('const/sets/sup' @ sK4) @ sK6))) | spl8_216),
% 72.07/14.61 inference(avatar_component_clause,[],[f36930])).
% 72.07/14.61 thf(f36932,plain,(
% 72.07/14.61 ($false = (('const/realax/real_le' @ ('const/sets/sup' @ sK4) @ sK6))) | ~spl8_216),
% 72.07/14.61 inference(avatar_component_clause,[],[f36930])).
% 72.07/14.61 thf(f38863,plain,(
% 72.07/14.61 ($true = $false) | (~spl8_42 | ~spl8_184)),
% 72.07/14.61 inference(constrained_superposition,[],[f33747,f2335])).
% 72.07/14.61 thf(f38938,plain,(
% 72.07/14.61 $false | (~spl8_42 | ~spl8_184)),
% 72.07/14.61 inference(trivial_inequality_removal,[],[f38863])).
% 72.07/14.61 thf(f38939,plain,(
% 72.07/14.61 ~spl8_42 | ~spl8_184),
% 72.07/14.61 inference(avatar_contradiction_clause,[],[f38938])).
% 72.07/14.61 thf(f61792,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real',X1 : 'type/realax/real'] : (($true != (('const/realax/real_le' @ X0 @ sK6))) | ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK0 @ X1 @ sK4) @ sK4))) | ($true = (('const/realax/real_le' @ X1 @ ('const/sets/inf' @ sK4))))) ) | ~spl8_32),
% 72.07/14.61 inference(forward_subsumption_resolution,[],[f25020,f70])).
% 72.07/14.61 thf(f61821,plain,(
% 72.07/14.61 spl8_10 | spl8_48 | ~spl8_32),
% 72.07/14.61 inference(avatar_split_clause,[],[f61792,f1646,f2495,f222])).
% 72.07/14.61 thf(f64563,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real',X1 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ ('const/sets/sup' @ sK4) @ X1))) | ($false = (('const/sets/IN' @ 'type/realax/real' @ X1 @ sK4))) | ($true = (('const/realax/real_le' @ ('const/realax/real_abs' @ (sK1 @ X0 @ sK4)) @ sK5)))) ) | ~spl8_2),
% 72.07/14.61 inference(forward_demodulation,[],[f8820,f126])).
% 72.07/14.61 thf(f66814,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($true = $false) | ($true = (('const/realax/real_le' @ ('const/sets/inf' @ sK4) @ X0))) | ('const/sets/EMPTY' @ 'type/realax/real' = sK4) | ($false = (('const/sets/IN' @ 'type/realax/real' @ X0 @ sK4)))) ) | ~spl8_11),
% 72.07/14.61 inference(constrained_superposition,[],[f639,f3315])).
% 72.07/14.61 thf(f66853,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ ('const/sets/inf' @ sK4) @ X0))) | ('const/sets/EMPTY' @ 'type/realax/real' = sK4) | ($false = (('const/sets/IN' @ 'type/realax/real' @ X0 @ sK4)))) ) | ~spl8_11),
% 72.07/14.61 inference(trivial_inequality_removal,[],[f66814])).
% 72.07/14.61 thf(f66885,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ ('const/sets/inf' @ sK4) @ X0))) | ($false = (('const/sets/IN' @ 'type/realax/real' @ X0 @ sK4)))) ) | ~spl8_11),
% 72.07/14.61 inference(forward_subsumption_resolution,[],[f66853,f3465])).
% 72.07/14.61 thf(f66898,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ ('const/sets/sup' @ sK4) @ X0))) | ($false = (('const/sets/IN' @ 'type/realax/real' @ X0 @ sK4)))) ) | (~spl8_2 | ~spl8_11)),
% 72.07/14.61 inference(forward_demodulation,[],[f66885,f126])).
% 72.07/14.61 thf(f67306,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real',X1 : 'type/realax/real'] : (($true = $false) | ($false = (('const/realax/real_le' @ (sK3 @ X1 @ sK4) @ X1))) | ('const/sets/EMPTY' @ 'type/realax/real' = sK4) | ($false = (('const/sets/IN' @ 'type/realax/real' @ X0 @ sK4))) | ((('const/sets/sup' @ sK4)) = X0)) ) | ~spl8_28),
% 72.07/14.61 inference(duplicate_literal_removal,[],[f34628])).
% 72.07/14.61 thf(f75818,definition,(
% 72.07/14.61 spl8_357 <=> ! [X0 : 'type/realax/real'] : ((sK6 = X0) | ($false = (('const/sets/IN' @ 'type/realax/real' @ X0 @ sK4))))),
% 72.07/14.61 introduced(definition,[new_symbols(definition,[spl8_357])],[avatar_definition])).
% 72.07/14.61 thf(f75819,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($false = (('const/sets/IN' @ 'type/realax/real' @ X0 @ sK4))) | (sK6 = X0)) ) | ~spl8_357),
% 72.07/14.61 inference(avatar_component_clause,[],[f75818])).
% 72.07/14.61 thf(f80666,plain,(
% 72.07/14.61 ~spl8_150 | spl8_2 | ~spl8_158),
% 72.07/14.61 inference(avatar_split_clause,[],[f28456,f28179,f125,f27164])).
% 72.07/14.61 thf(f80675,plain,(
% 72.07/14.61 spl8_357 | ~spl8_3),
% 72.07/14.61 inference(avatar_split_clause,[],[f562,f130,f75818])).
% 72.07/14.61 thf(f80928,plain,(
% 72.07/14.61 spl8_42 | ~spl8_3),
% 72.07/14.61 inference(avatar_split_clause,[],[f29808,f130,f2333])).
% 72.07/14.61 thf(f83433,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ ('const/sets/inf' @ sK4) @ sK6))) | ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK1 @ X0 @ sK4) @ sK4))) | ('const/sets/EMPTY' @ 'type/realax/real' = sK4)) ) | ~spl8_42),
% 72.07/14.61 inference(trivial_inequality_removal,[],[f26835])).
% 72.07/14.61 thf(f83509,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real',X1 : 'type/realax/real'] : (($true = (('const/sets/IN' @ 'type/realax/real' @ (sK1 @ X0 @ sK4) @ 'const/sets/EMPTY' @ 'type/realax/real'))) | ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK0 @ X1 @ sK4) @ sK4))) | ('const/sets/EMPTY' @ 'type/realax/real' = sK4) | ($true = (('const/realax/real_le' @ X1 @ ('const/sets/inf' @ sK4)))) | (sK6 = ((sK1 @ X0 @ sK4)))) ) | ~spl8_3),
% 72.07/14.61 inference(constrained_superposition,[],[f554,f132])).
% 72.07/14.61 thf(f83566,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real',X1 : 'type/realax/real'] : (($true = (('const/sets/IN' @ 'type/realax/real' @ (sK1 @ X0 @ sK4) @ 'const/sets/EMPTY' @ 'type/realax/real'))) | ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK0 @ X1 @ sK4) @ sK4))) | ($true = (('const/realax/real_le' @ X1 @ ('const/sets/inf' @ sK4)))) | (sK6 = ((sK1 @ X0 @ sK4)))) ) | ~spl8_3),
% 72.07/14.61 inference(forward_subsumption_resolution,[],[f83509,f70])).
% 72.07/14.61 thf(f83578,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real',X1 : 'type/realax/real'] : (($true = (('const/sets/IN' @ 'type/realax/real' @ (sK0 @ X1 @ sK4) @ sK4))) | ($true = (('const/realax/real_le' @ X1 @ ('const/sets/inf' @ sK4)))) | (sK6 = ((sK1 @ X0 @ sK4)))) ) | ~spl8_3),
% 72.07/14.61 inference(forward_subsumption_resolution,[],[f83566,f52])).
% 72.07/14.61 thf(f83802,plain,(
% 72.07/14.61 ($false != $false) | ($false = (('const/sets/IN' @ 'type/realax/real' @ sK6 @ sK4))) | ((('const/sets/sup' @ sK4)) = sK6) | (~spl8_89 | spl8_216)),
% 72.07/14.61 inference(constrained_superposition,[],[f36931,f8675])).
% 72.07/14.61 thf(f83851,plain,(
% 72.07/14.61 ($false = (('const/sets/IN' @ 'type/realax/real' @ sK6 @ sK4))) | ((('const/sets/sup' @ sK4)) = sK6) | (~spl8_89 | spl8_216)),
% 72.07/14.61 inference(trivial_inequality_removal,[],[f83802])).
% 72.07/14.61 thf(f83854,plain,(
% 72.07/14.61 ((('const/sets/sup' @ sK4)) = sK6) | (~spl8_89 | spl8_184 | spl8_216)),
% 72.07/14.61 inference(forward_subsumption_resolution,[],[f83851,f33746])).
% 72.07/14.61 thf(f83855,plain,(
% 72.07/14.61 spl8_150 | ~spl8_89 | spl8_184 | spl8_216),
% 72.07/14.61 inference(avatar_split_clause,[],[f83854,f36930,f33745,f8674,f27164])).
% 72.07/14.61 thf(f84440,plain,(
% 72.07/14.61 ($true = $false) | (sK6 = ((sK2 @ sK6 @ sK4))) | (~spl8_31 | ~spl8_216)),
% 72.07/14.61 inference(constrained_superposition,[],[f36932,f1642])).
% 72.07/14.61 thf(f84444,plain,(
% 72.07/14.61 (sK6 = ((sK2 @ sK6 @ sK4))) | (~spl8_31 | ~spl8_216)),
% 72.07/14.61 inference(trivial_inequality_removal,[],[f84440])).
% 72.07/14.61 thf(f97317,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($true != (('const/realax/real_le' @ sK6 @ sK6))) | ($true = (('const/realax/real_le' @ ('const/sets/sup' @ sK4) @ sK6))) | ('const/sets/EMPTY' @ 'type/realax/real' = sK4) | ($false = (('const/realax/real_le' @ (sK3 @ X0 @ sK4) @ X0)))) ) | (~spl8_31 | ~spl8_216)),
% 72.07/14.61 inference(constrained_superposition,[],[f184,f84444])).
% 72.07/14.61 thf(f97342,plain,(
% 72.07/14.61 ($false = (('const/realax/real_le' @ sK6 @ sK6))) | ($true = (('const/realax/real_le' @ ('const/sets/sup' @ sK4) @ sK6))) | (~spl8_29 | ~spl8_31 | ~spl8_216)),
% 72.07/14.61 inference(constrained_superposition,[],[f1633,f84444])).
% 72.07/14.61 thf(f97351,plain,(
% 72.07/14.61 ($true = (('const/realax/real_le' @ ('const/sets/sup' @ sK4) @ sK6))) | (~spl8_29 | ~spl8_31 | spl8_181 | ~spl8_216)),
% 72.07/14.61 inference(forward_subsumption_resolution,[],[f97342,f33159])).
% 72.07/14.61 thf(f97364,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ ('const/sets/sup' @ sK4) @ sK6))) | ('const/sets/EMPTY' @ 'type/realax/real' = sK4) | ($false = (('const/realax/real_le' @ (sK3 @ X0 @ sK4) @ X0)))) ) | (~spl8_31 | ~spl8_156 | ~spl8_216)),
% 72.07/14.61 inference(forward_subsumption_resolution,[],[f97317,f27488])).
% 72.07/14.61 thf(f97368,plain,(
% 72.07/14.61 ($true = $false) | (~spl8_29 | ~spl8_31 | spl8_181 | ~spl8_216)),
% 72.07/14.61 inference(forward_demodulation,[],[f97351,f36932])).
% 72.07/14.61 thf(f97369,plain,(
% 72.07/14.61 $false | (~spl8_29 | ~spl8_31 | spl8_181 | ~spl8_216)),
% 72.07/14.61 inference(trivial_inequality_removal,[],[f97368])).
% 72.07/14.61 thf(f97370,plain,(
% 72.07/14.61 ~spl8_29 | ~spl8_31 | spl8_181 | ~spl8_216),
% 72.07/14.61 inference(avatar_contradiction_clause,[],[f97369])).
% 72.07/14.61 thf(f97381,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ ('const/sets/sup' @ sK4) @ sK6))) | ($false = (('const/realax/real_le' @ (sK3 @ X0 @ sK4) @ X0)))) ) | (~spl8_31 | ~spl8_156 | ~spl8_216)),
% 72.07/14.61 inference(forward_subsumption_resolution,[],[f97364,f70])).
% 72.07/14.61 thf(f97395,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($true = $false) | ($false = (('const/realax/real_le' @ (sK3 @ X0 @ sK4) @ X0)))) ) | (~spl8_31 | ~spl8_156 | ~spl8_216)),
% 72.07/14.61 inference(forward_demodulation,[],[f97381,f36932])).
% 72.07/14.61 thf(f97396,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($false = (('const/realax/real_le' @ (sK3 @ X0 @ sK4) @ X0)))) ) | (~spl8_31 | ~spl8_156 | ~spl8_216)),
% 72.07/14.61 inference(trivial_inequality_removal,[],[f97395])).
% 72.07/14.61 thf(f97411,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($false = (('const/realax/real_le' @ sK6 @ X0)))) ) | (~spl8_24 | ~spl8_31 | ~spl8_156 | ~spl8_216)),
% 72.07/14.61 inference(forward_demodulation,[],[f97396,f674])).
% 72.07/14.61 thf(f97418,plain,(
% 72.07/14.61 spl8_143 | ~spl8_24 | ~spl8_31 | ~spl8_156 | ~spl8_216),
% 72.07/14.61 inference(avatar_split_clause,[],[f97411,f36930,f27486,f1641,f673,f24874])).
% 72.07/14.61 thf(f99777,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($true = (('const/sets/IN' @ 'type/realax/real' @ (sK1 @ X0 @ sK4) @ sK4)))) ) | (~spl8_156 | ~spl8_159 | ~spl8_176)),
% 72.07/14.61 inference(trivial_inequality_removal,[],[f33110])).
% 72.07/14.61 thf(f100716,plain,(
% 72.07/14.61 spl8_8 | ~spl8_156 | ~spl8_159 | ~spl8_176),
% 72.07/14.61 inference(avatar_split_clause,[],[f99777,f32809,f28183,f27486,f215])).
% 72.07/14.61 thf(f101109,plain,(
% 72.07/14.61 spl8_32 | spl8_10 | ~spl8_3),
% 72.07/14.61 inference(avatar_split_clause,[],[f83578,f130,f222,f1646])).
% 72.07/14.61 thf(f102423,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ ('const/sets/inf' @ sK4) @ sK6))) | ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK1 @ X0 @ sK4) @ sK4)))) ) | ~spl8_42),
% 72.07/14.61 inference(forward_subsumption_resolution,[],[f83433,f70])).
% 72.07/14.61 thf(f102485,plain,(
% 72.07/14.61 spl8_8 | spl8_142 | ~spl8_42),
% 72.07/14.61 inference(avatar_split_clause,[],[f102423,f2333,f24867,f215])).
% 72.07/14.61 thf(f103718,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real',X1 : 'type/realax/real'] : (($false = (('const/realax/real_le' @ (sK3 @ X1 @ sK4) @ X1))) | ('const/sets/EMPTY' @ 'type/realax/real' = sK4) | ($false = (('const/sets/IN' @ 'type/realax/real' @ X0 @ sK4))) | ((('const/sets/sup' @ sK4)) = X0)) ) | ~spl8_28),
% 72.07/14.61 inference(trivial_inequality_removal,[],[f67306])).
% 72.07/14.61 thf(f104687,plain,(
% 72.07/14.61 spl8_11 | spl8_28 | ~spl8_2),
% 72.07/14.61 inference(avatar_split_clause,[],[f64563,f125,f865,f225])).
% 72.07/14.61 thf(f104708,plain,(
% 72.07/14.61 spl8_28 | ~spl8_2 | ~spl8_11),
% 72.07/14.61 inference(avatar_split_clause,[],[f66898,f225,f125,f865])).
% 72.07/14.61 thf(f105085,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real',X1 : 'type/realax/real'] : (($false = (('const/realax/real_le' @ (sK3 @ X1 @ sK4) @ X1))) | ($false = (('const/sets/IN' @ 'type/realax/real' @ X0 @ sK4))) | ((('const/sets/sup' @ sK4)) = X0)) ) | ~spl8_28),
% 72.07/14.61 inference(forward_subsumption_resolution,[],[f103718,f3465])).
% 72.07/14.61 thf(f105413,plain,(
% 72.07/14.61 spl8_158 | spl8_159 | ~spl8_142),
% 72.07/14.61 inference(avatar_split_clause,[],[f28177,f24867,f28183,f28179])).
% 72.07/14.61 thf(f106873,plain,(
% 72.07/14.61 ( ! [X1 : 'type/realax/real'] : ((((sK4 @ (sK70 @ X1))) != (('const/sets/INSERT' @ 'type/realax/real' @ X1 @ 'const/sets/EMPTY' @ 'type/realax/real' @ (sK70 @ X1))))) ) | ~spl8_1),
% 72.07/14.61 inference(negative_extensionality,[],[f123])).
% 72.07/14.61 thf(f106874,plain,(
% 72.07/14.61 ( ! [X1 : 'type/realax/real'] : (($true = (('const/sets/INSERT' @ 'type/realax/real' @ X1 @ 'const/sets/EMPTY' @ 'type/realax/real' @ (sK70 @ X1)))) | ($true = ((sK4 @ (sK70 @ X1))))) ) | ~spl8_1),
% 72.07/14.61 inference(xor_proxy_clausification,[],[f106873])).
% 72.07/14.61 thf(f106875,plain,(
% 72.07/14.61 ( ! [X1 : 'type/realax/real'] : (($false = (('const/sets/INSERT' @ 'type/realax/real' @ X1 @ 'const/sets/EMPTY' @ 'type/realax/real' @ (sK70 @ X1)))) | ($false = ((sK4 @ (sK70 @ X1))))) ) | ~spl8_1),
% 72.07/14.61 inference(xor_proxy_clausification,[],[f106873])).
% 72.07/14.61 thf(f107033,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real',X1 : 'type/realax/real'] : (($true = $false) | ($false = (('const/sets/IN' @ 'type/realax/real' @ X0 @ sK4))) | ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK3 @ X1 @ sK4) @ sK4))) | ((('const/sets/sup' @ sK4)) = X0) | ('const/sets/EMPTY' @ 'type/realax/real' = sK4) | ($false = (('const/sets/IN' @ 'type/realax/real' @ X0 @ sK4)))) ) | ~spl8_28),
% 72.07/14.61 inference(constrained_superposition,[],[f866,f940])).
% 72.07/14.61 thf(f107206,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real',X1 : 'type/realax/real'] : (($true = $false) | ($false = (('const/sets/IN' @ 'type/realax/real' @ X0 @ sK4))) | ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK3 @ X1 @ sK4) @ sK4))) | ((('const/sets/sup' @ sK4)) = X0) | ('const/sets/EMPTY' @ 'type/realax/real' = sK4)) ) | ~spl8_28),
% 72.07/14.61 inference(duplicate_literal_removal,[],[f107033])).
% 72.07/14.61 thf(f107207,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real',X1 : 'type/realax/real'] : (($false = (('const/sets/IN' @ 'type/realax/real' @ X0 @ sK4))) | ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK3 @ X1 @ sK4) @ sK4))) | ((('const/sets/sup' @ sK4)) = X0) | ('const/sets/EMPTY' @ 'type/realax/real' = sK4)) ) | ~spl8_28),
% 72.07/14.61 inference(trivial_inequality_removal,[],[f107206])).
% 72.07/14.61 thf(f107227,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real',X1 : 'type/realax/real'] : (($false = (('const/sets/IN' @ 'type/realax/real' @ X0 @ sK4))) | ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK3 @ X1 @ sK4) @ sK4))) | ((('const/sets/sup' @ sK4)) = X0)) ) | ~spl8_28),
% 72.07/14.61 inference(forward_subsumption_resolution,[],[f107207,f3465])).
% 72.07/14.61 thf(f110672,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($true = $false) | ($true = (('const/sets/IN' @ 'type/realax/real' @ (sK70 @ X0) @ 'const/sets/EMPTY' @ 'type/realax/real'))) | (((sK70 @ X0)) = X0) | ($true = ((sK4 @ (sK70 @ X0))))) ) | ~spl8_1),
% 72.07/14.61 inference(constrained_superposition,[],[f551,f106874])).
% 72.07/14.61 thf(f110676,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($true = (('const/sets/IN' @ 'type/realax/real' @ (sK70 @ X0) @ 'const/sets/EMPTY' @ 'type/realax/real'))) | (((sK70 @ X0)) = X0) | ($true = ((sK4 @ (sK70 @ X0))))) ) | ~spl8_1),
% 72.07/14.61 inference(trivial_inequality_removal,[],[f110672])).
% 72.07/14.61 thf(f110680,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($true = ((sK4 @ (sK70 @ X0)))) | (((sK70 @ X0)) = X0)) ) | ~spl8_1),
% 72.07/14.61 inference(forward_subsumption_resolution,[],[f110676,f52])).
% 72.07/14.61 thf(f110735,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($true = $false) | (((sK70 @ X0)) != X0) | ($false = ((sK4 @ (sK70 @ X0))))) ) | ~spl8_1),
% 72.07/14.61 inference(constrained_superposition,[],[f3343,f106875])).
% 72.07/14.61 thf(f110739,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : ((((sK70 @ X0)) != X0) | ($false = ((sK4 @ (sK70 @ X0))))) ) | ~spl8_1),
% 72.07/14.61 inference(trivial_inequality_removal,[],[f110735])).
% 72.07/14.61 thf(f118096,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real',X1 : 'type/realax/real'] : (($true = $false) | (sK6 = ((sK2 @ X0 @ sK4))) | ($false = (('const/realax/real_le' @ (sK3 @ X1 @ sK4) @ X1))) | ('const/sets/EMPTY' @ 'type/realax/real' = sK4) | ($true = (('const/realax/real_le' @ ('const/sets/sup' @ sK4) @ X0)))) ) | ~spl8_357),
% 72.07/14.61 inference(constrained_superposition,[],[f75819,f193])).
% 72.07/14.61 thf(f118310,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($true = $false) | ($true = (('const/realax/real_le' @ ('const/sets/sup' @ sK4) @ X0))) | (sK6 = ((sK2 @ X0 @ sK4)))) ) | (~spl8_14 | ~spl8_357)),
% 72.07/14.61 inference(constrained_superposition,[],[f255,f75819])).
% 72.07/14.61 thf(f118374,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($true = (('const/realax/real_le' @ ('const/sets/sup' @ sK4) @ X0))) | (sK6 = ((sK2 @ X0 @ sK4)))) ) | (~spl8_14 | ~spl8_357)),
% 72.07/14.61 inference(trivial_inequality_removal,[],[f118310])).
% 72.07/14.61 thf(f118581,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real',X1 : 'type/realax/real'] : ((sK6 = ((sK2 @ X0 @ sK4))) | ($false = (('const/realax/real_le' @ (sK3 @ X1 @ sK4) @ X1))) | ('const/sets/EMPTY' @ 'type/realax/real' = sK4) | ($true = (('const/realax/real_le' @ ('const/sets/sup' @ sK4) @ X0)))) ) | ~spl8_357),
% 72.07/14.61 inference(trivial_inequality_removal,[],[f118096])).
% 72.07/14.61 thf(f118675,plain,(
% 72.07/14.61 spl8_31 | ~spl8_14 | ~spl8_357),
% 72.07/14.61 inference(avatar_split_clause,[],[f118374,f75818,f254,f1641])).
% 72.07/14.61 thf(f118719,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real',X1 : 'type/realax/real'] : ((sK6 = ((sK2 @ X0 @ sK4))) | ($false = (('const/realax/real_le' @ (sK3 @ X1 @ sK4) @ X1))) | ($true = (('const/realax/real_le' @ ('const/sets/sup' @ sK4) @ X0)))) ) | ~spl8_357),
% 72.07/14.61 inference(forward_subsumption_resolution,[],[f118581,f70])).
% 72.07/14.61 thf(f118769,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real',X1 : 'type/realax/real'] : (($false = (('const/realax/real_le' @ sK6 @ X1))) | (sK6 = ((sK2 @ X0 @ sK4))) | ($true = (('const/realax/real_le' @ ('const/sets/sup' @ sK4) @ X0)))) ) | (~spl8_24 | ~spl8_357)),
% 72.07/14.61 inference(forward_demodulation,[],[f118719,f674])).
% 72.07/14.61 thf(f118814,plain,(
% 72.07/14.61 spl8_31 | spl8_143 | ~spl8_24 | ~spl8_357),
% 72.07/14.61 inference(avatar_split_clause,[],[f118769,f75818,f673,f24874,f1641])).
% 72.07/14.61 thf(f125611,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($true = $false) | ($false = ((sK4 @ X0))) | ((('const/sets/sup' @ sK4)) = X0)) ) | ~spl8_201),
% 72.07/14.61 inference(constrained_superposition,[],[f112,f34916])).
% 72.07/14.61 thf(f125723,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($false = ((sK4 @ X0))) | ((('const/sets/sup' @ sK4)) = X0)) ) | ~spl8_201),
% 72.07/14.61 inference(trivial_inequality_removal,[],[f125611])).
% 72.07/14.61 thf(f126253,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real',X1 : 'type/realax/real'] : ((X0 = X1) | ($false = ((sK4 @ X1))) | ($false = ((sK4 @ X0)))) ) | ~spl8_201),
% 72.07/14.61 inference(constrained_superposition,[],[f125723,f125723])).
% 72.07/14.61 thf(f129240,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($true = $false) | (sK9 = X0) | ($false = ((sK4 @ X0)))) ) | (~spl8_6 | ~spl8_201)),
% 72.07/14.61 inference(constrained_superposition,[],[f149,f126253])).
% 72.07/14.61 thf(f129245,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($false = ((sK4 @ X0))) | (sK9 = X0)) ) | (~spl8_6 | ~spl8_201)),
% 72.07/14.61 inference(trivial_inequality_removal,[],[f129240])).
% 72.07/14.61 thf(f129439,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : (($true = $false) | (((sK70 @ X0)) = X0) | (sK9 = ((sK70 @ X0)))) ) | (~spl8_1 | ~spl8_6 | ~spl8_201)),
% 72.07/14.61 inference(constrained_superposition,[],[f110680,f129245])).
% 72.07/14.61 thf(f129442,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : ((((sK70 @ X0)) = X0) | (sK9 = ((sK70 @ X0)))) ) | (~spl8_1 | ~spl8_6 | ~spl8_201)),
% 72.07/14.61 inference(trivial_inequality_removal,[],[f129439])).
% 72.07/14.61 thf(f132284,plain,(
% 72.07/14.61 ( ! [X0 : 'type/realax/real'] : ((sK9 != X0) | (sK9 = ((sK70 @ X0)))) ) | (~spl8_1 | ~spl8_6 | ~spl8_201)),
% 72.07/14.61 inference(equality_factoring,[],[f129442])).
% 72.07/14.61 thf(f132290,plain,(
% 72.07/14.61 (sK9 = ((sK70 @ sK9))) | (~spl8_1 | ~spl8_6 | ~spl8_201)),
% 72.07/14.61 inference(equality_resolution,[],[f132284])).
% 72.07/14.61 thf(f132293,plain,(
% 72.07/14.61 (sK9 != sK9) | ($false = ((sK4 @ sK9))) | (~spl8_1 | ~spl8_6 | ~spl8_201)),
% 72.07/14.61 inference(constrained_superposition,[],[f110739,f132290])).
% 72.07/14.61 thf(f132296,plain,(
% 72.07/14.61 ($false = ((sK4 @ sK9))) | (~spl8_1 | ~spl8_6 | ~spl8_201)),
% 72.07/14.61 inference(trivial_inequality_removal,[],[f132293])).
% 72.07/14.61 thf(f132298,plain,(
% 72.07/14.61 $false | (~spl8_1 | spl8_4 | ~spl8_6 | ~spl8_201)),
% 72.07/14.61 inference(forward_subsumption_resolution,[],[f132296,f139])).
% 72.07/14.61 thf(f132299,plain,(
% 72.07/14.61 ~spl8_1 | spl8_4 | ~spl8_6 | ~spl8_201),
% 72.07/14.61 inference(avatar_contradiction_clause,[],[f132298])).
% 72.07/14.61 thf(f132609,plain,(
% 72.07/14.61 spl8_201 | spl8_26 | ~spl8_28),
% 72.07/14.61 inference(avatar_split_clause,[],[f105085,f865,f800,f34915])).
% 72.07/14.61 thf(f132661,plain,(
% 72.07/14.61 spl8_12 | spl8_201 | ~spl8_28),
% 72.07/14.61 inference(avatar_split_clause,[],[f107227,f865,f34915,f247])).
% 72.07/14.61 thf(f134088,plain,(
% 72.07/14.61 ($true = $false) | (~spl8_15 | ~spl8_26)),
% 72.07/14.61 inference(constrained_superposition,[],[f801,f3268])).
% 72.07/14.61 thf(f134096,plain,(
% 72.07/14.61 $false | (~spl8_15 | ~spl8_26)),
% 72.07/14.61 inference(trivial_inequality_removal,[],[f134088])).
% 72.07/14.61 thf(f134097,plain,(
% 72.07/14.61 ~spl8_15 | ~spl8_26),
% 72.07/14.61 inference(avatar_contradiction_clause,[],[f134096])).
% 72.07/14.61 cnf(s1, plain, spl8_1 | ~spl8_2, inference(sat_conversion,[],[f128])).
% 72.07/14.61 cnf(s2, plain, spl8_2 | spl8_3, inference(sat_conversion,[],[f133])).
% 72.07/14.61 cnf(s4, plain, spl8_6 | spl8_7, inference(sat_conversion,[],[f154])).
% 72.07/14.61 cnf(s5, plain, ~spl8_4 | ~spl8_6, inference(sat_conversion,[],[f157])).
% 72.07/14.61 cnf(s12, plain, ~spl8_12 | spl8_15, inference(sat_conversion,[],[f284])).
% 72.07/14.61 cnf(s61, plain, ~spl8_3 | ~spl8_10 | spl8_25, inference(sat_conversion,[],[f898])).
% 72.07/14.61 cnf(s132, plain, ~spl8_3 | ~spl8_8 | spl8_32, inference(sat_conversion,[],[f1827])).
% 72.07/14.61 cnf(s260, plain, ~spl8_3 | spl8_14 | spl8_24, inference(sat_conversion,[],[f2095])).
% 72.07/14.61 cnf(s735, plain, ~spl8_3 | spl8_4 | spl8_106, inference(sat_conversion,[],[f10331])).
% 72.07/14.61 cnf(s738, plain, ~spl8_7, inference(sat_conversion,[],[f10339])).
% 72.07/14.61 cnf(s915, plain, ~spl8_48, inference(sat_conversion,[],[f22895])).
% 72.07/14.61 cnf(s988, plain, ~spl8_56, inference(sat_conversion,[],[f23913])).
% 72.07/14.61 cnf(s1075, plain, ~spl8_3 | spl8_24 | spl8_89, inference(sat_conversion,[],[f24734])).
% 72.07/14.61 cnf(s1078, plain, ~spl8_3 | spl8_24 | spl8_29, inference(sat_conversion,[],[f24737])).
% 72.07/14.61 cnf(s1119, plain, ~spl8_24 | spl8_30 | spl8_143, inference(sat_conversion,[],[f24886])).
% 72.07/14.61 cnf(s1126, plain, ~spl8_106 | ~spl8_143, inference(sat_conversion,[],[f24980])).
% 72.07/14.61 cnf(s1199, plain, ~spl8_32 | ~spl8_42 | spl8_56 | spl8_142, inference(sat_conversion,[],[f26863])).
% 72.07/14.61 cnf(s1251, plain, ~spl8_25 | ~spl8_159 | spl8_176, inference(sat_conversion,[],[f32815])).
% 72.07/14.61 cnf(s1278, plain, ~spl8_32 | spl8_56 | ~spl8_156 | ~spl8_159 | ~spl8_176, inference(sat_conversion,[],[f33163])).
% 72.07/14.61 cnf(s1282, plain, ~spl8_30 | spl8_89, inference(sat_conversion,[],[f33728])).
% 72.07/14.61 cnf(s1301, plain, spl8_156 | spl8_181, inference(sat_conversion,[],[f33817])).
% 72.07/14.61 cnf(s1403, plain, ~spl8_181, inference(sat_conversion,[],[f35421])).
% 72.07/14.61 cnf(s1701, plain, ~spl8_42 | ~spl8_184, inference(sat_conversion,[],[f38939])).
% 72.07/14.61 cnf(s2174, plain, spl8_10 | ~spl8_32 | spl8_48, inference(sat_conversion,[],[f61821])).
% 72.07/14.61 cnf(s3784, plain, spl8_2 | ~spl8_150 | ~spl8_158, inference(sat_conversion,[],[f80666])).
% 72.07/14.61 cnf(s3786, plain, ~spl8_3 | spl8_357, inference(sat_conversion,[],[f80675])).
% 72.07/14.61 cnf(s3838, plain, ~spl8_3 | spl8_42, inference(sat_conversion,[],[f80928])).
% 72.07/14.61 cnf(s4916, plain, ~spl8_89 | spl8_150 | spl8_184 | spl8_216, inference(sat_conversion,[],[f83855])).
% 72.07/14.61 cnf(s5251, plain, ~spl8_29 | ~spl8_31 | spl8_181 | ~spl8_216, inference(sat_conversion,[],[f97370])).
% 72.07/14.61 cnf(s5261, plain, ~spl8_24 | ~spl8_31 | spl8_143 | ~spl8_156 | ~spl8_216, inference(sat_conversion,[],[f97418])).
% 72.07/14.61 cnf(s5651, plain, spl8_8 | ~spl8_156 | ~spl8_159 | ~spl8_176, inference(sat_conversion,[],[f100716])).
% 72.07/14.61 cnf(s6095, plain, ~spl8_3 | spl8_10 | spl8_32, inference(sat_conversion,[],[f101109])).
% 72.07/14.61 cnf(s6847, plain, spl8_8 | ~spl8_42 | spl8_142, inference(sat_conversion,[],[f102485])).
% 72.07/14.61 cnf(s6929, plain, ~spl8_2 | spl8_11 | spl8_28, inference(sat_conversion,[],[f104687])).
% 72.07/14.61 cnf(s6951, plain, ~spl8_2 | ~spl8_11 | spl8_28, inference(sat_conversion,[],[f104708])).
% 72.07/14.61 cnf(s7351, plain, ~spl8_142 | spl8_158 | spl8_159, inference(sat_conversion,[],[f105413])).
% 72.07/14.61 cnf(s8938, plain, ~spl8_14 | spl8_31 | ~spl8_357, inference(sat_conversion,[],[f118675])).
% 72.07/14.61 cnf(s8950, plain, ~spl8_24 | spl8_31 | spl8_143 | ~spl8_357, inference(sat_conversion,[],[f118814])).
% 72.07/14.61 cnf(s9117, plain, ~spl8_1 | spl8_4 | ~spl8_6 | ~spl8_201, inference(sat_conversion,[],[f132299])).
% 72.07/14.61 cnf(s9330, plain, spl8_26 | ~spl8_28 | spl8_201, inference(sat_conversion,[],[f132609])).
% 72.07/14.61 cnf(s9371, plain, spl8_12 | ~spl8_28 | spl8_201, inference(sat_conversion,[],[f132661])).
% 72.07/14.61 cnf(s9549, plain, ~spl8_15 | ~spl8_26, inference(sat_conversion,[],[f134097])).
% 72.07/14.61 cnf(s9566, plain, spl8_156, inference(rat,[],[s1301,s1403])).
% 72.07/14.61 cnf(s9567, plain, ~spl8_32 | spl8_56 | ~spl8_159 | ~spl8_176, inference(rat,[],[s1278,s9566])).
% 72.07/14.61 cnf(s9602, plain, spl8_6, inference(rat,[],[s4,s738])).
% 72.07/14.61 cnf(s9603, plain, ~spl8_4, inference(rat,[],[s5,s9602])).
% 72.07/14.61 cnf(s9605, plain, spl8_10 | ~spl8_3, inference(rat,[],[s2174,s6095,s915])).
% 72.07/14.61 cnf(s9606, plain, ~spl8_159 | ~spl8_25 | spl8_8, inference(rat,[],[s1251,s5651,s9566])).
% 72.07/14.61 cnf(s9607, plain, ~spl8_24 | ~spl8_31 | spl8_150 | ~spl8_3, inference(rat,[],[s1282,s4916,s1119,s5261,s1701,s3838,s1126,s735,s9566,s9603])).
% 72.07/14.61 cnf(s9608, plain, ~spl8_31 | spl8_150 | ~spl8_3, inference(rat,[],[s4916,s5251,s1075,s1078,s9607,s1701,s3838,s1403])).
% 72.07/14.61 cnf(s9609, plain, spl8_31 | ~spl8_3, inference(rat,[],[s260,s8938,s8950,s3786,s1126,s735,s9603])).
% 72.07/14.61 cnf(s9610, plain, ~spl8_159 | ~spl8_3, inference(rat,[],[s132,s9567,s9606,s1251,s61,s9605,s988])).
% 72.07/14.61 cnf(s9611, plain, spl8_2, inference(rat,[],[s132,s1199,s6847,s7351,s9610,s3784,s9608,s9609,s3838,s2,s988])).
% 72.07/14.61 cnf(s9612, plain, spl8_1, inference(rat,[],[s1,s9611])).
% 72.07/14.61 cnf(s9613, plain, ~spl8_201, inference(rat,[],[s9117,s9603,s9602,s9612])).
% 72.07/14.61 cnf(s9615, plain, ~spl8_28, inference(rat,[],[s9549,s12,s9330,s9371,s9613])).
% 72.07/14.61 cnf(s9619, plain, ~spl8_11, inference(rat,[],[s6951,s9611,s9615])).
% 72.07/14.61 cnf(s9620, plain, $false, inference(rat,[],[s6929,s9611,s9615,s9619])).
% 72.07/14.61 thf(f134120,plain,(
% 72.07/14.61 $false),
% 72.07/14.61 inference(avatar_sat_refutation,[],[s9620])).
% 72.07/14.61 % SZS output end Proof for theBenchmark
% 72.07/14.61 % (1619382)------------------------------
% 72.07/14.61 % (1619382)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 72.07/14.61 % (1619382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 72.07/14.61 % (1619382)CaDiCaL version: 2.1.3
% 72.07/14.61 % (1619382)Termination reason: Refutation
% 72.07/14.61 % (1619382)Time elapsed: 14.347 s
% 72.07/14.61 % (1619382)Peak memory usage: 55 MB
% 72.07/14.61 % (1619382)Instructions burned: 33131 (million)
% 72.07/14.61 % (1619372)Success in time 14.399 s
% 72.07/14.61 % Vampire exiting
%------------------------------------------------------------------------------